Coq version of the semantics of CakeML

[myreen]

Several people have contacted us asking to have the CakeML semantics in provers other than HOL4. There is an AFP entry 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.

[myreen]

This is similar to #580

[charguer]

Regarding (1) I'd be happy to help out writing a semantics in idiomatic Coq style. Questions, though: should it be Small-step? Big-step? Pretty-big-step? All? Including divergence?

I would also be interested in proving that the toy language for which I have developed characteristic formulae in Coq has a semantics that relates (one way or the other) to the CakeML semantics. This would allow Coq users to prove practical imperative algorithms that then get compiled using CakeML.

Regarding (2), the Dedukti tool (https://deducteam.github.io/) has make recent progress that might get the cross-checking of formal definitions within reach. In any case, it would be a highly relevant case study for its developers. The interest of this tool is that it would work for all provers.

[myreen]

@charguer Having your help in writing the semantics is most appreciated!

Regarding style: I think it's most important that the Coq definitions are nice to work with in Coq and that the correspondence to the HOL4 definitions can effectively be testable or even better proved (as part of the normal CakeML regression test -- we can install some release version of Coq on the regression machines).

Regarding divergence: the CakeML semantics in HOL4 is expressed in functional big-step style and covers both terminating and non-terminating behaviours. I would hope the Coq definitions can be equally complete.

The Dedukti tool sounds interesting for getting some kind of evidence that the definitions are right. For testing, one might look into QuickChick, if it can be made to interface with HOL4 as an external tool.