Rocq version of the semantics of CakeML

Several people have contacted us asking to have the CakeML semantics in provers other than HOL4. There is an [AFP entry](https://devel.isa-afp.org/entries/CakeML.html) with the CakeML semantics ported to Isabelle/HOL via Lem. However, people have also requested to have the semantics in ACL2 and Coq.

_This issue is about producing a clean port for the Coq proof assistant._

There are two parts to this: (1) writing the definition in Coq in an idiomatic and nice way, and more importantly (2) engineering some way of automatically producing some evidence that the new formulation in Coq is accurate w.r.t. the HOL4 definitions that are used in the compiler proofs. Ideally, (2) should be able to detect and automatically flag discrepancies that need fixing in the Coq version when the CakeML semantics in HOL4 is updated.

I suggest that (2) is based on different forms of automatic testing. I believe this could be a nice topic for a Masters thesis, or a warm-up project for someone joining CakeML with a background in Coq.