Test suite for ToCString

[andres-erbsen]

Do we still have a verified interpreter for the pure subset of bedrock2? It would be neat to run it side-by-side with ToCString on a comprehensive set of programs.

I'm imagining a setup like having a directory of examples, each of which would implement a pure computation list byte -> list byte, and we'd diff the output of in-Coq execution and gcc-compiled C code.

Alternatively, we could carefully implement known-answer tests in bedrock2 and run them using ToCString and gcc, but this might be more work in aggregate than maintaining an interpreter (@samuelgruetter wdyt?) and it is really the correspondance between the semantics and ToCString+gcc that we want to check, not specific known answers.

Oh, here's another idea: we could use a RISC-V emulator to run the RISC-V backend and use that as the reference instead. This seems less elegant than an in-Coq interpreter on its own, but it might be both less work and faster.

[samuelgruetter]

We have an interpreter for the source language here, but IIRC, it was never proven equivalent to the inductively defined semantics.

However, for the intermediate language FlatImp, I proved equivalence to inductively defined semantics here, but that's 3 years old and has not been maintained since.

The primitives typeclass in riscv-coq can be instantiated with a deterministic interpreter that can be run in Coq. For instance, here I execute inside Coq a handwritten risc-v program that computes Fibonacci numbers.

Turning this Fibonacci example into a function that takes a bedrock2 source program and a list byte, compiles the program using the bedrock2 compiler, and interprets it using riscv-coq and spits out a list byte as the result looks quite doable to me.

Another potentially useful reference might be this one from silveroak, which runs this simple driver, compiled by the bedrock2 compiler, on a riscv-coq machine connected to a Cava device.