Test suite for ToCString about bedrock2 HOT 1 OPEN

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.

from bedrock2.