Verifying the implementation of the interpreter of Michelson smart contracts is of importance because one of the strengths of Tezos is to be able to formally verify the smart contracts. In order to make this verification sound, we need to show that the smart contracts verification framework 🍬 Mi-Cho-Coq is coherent with the actual implementation of Michelson. In this blog post, we show how we translated the Michelson interpreter from the OCaml language to Coq. This is the first step to show the coherence of Mi-Cho-Coq with the implementation.
The main file of the interpreter is script_interpreter.ml (around 1,800 lines). The abstract syntax tree of smart contracts is given in script_typed_ir.mli (around 1,600 lines). We translate the OCaml code to Coq using coq-of-ocaml. A difficulty in translating the interpreter is that it heavily relies on GADTs in OCaml, a feature that does not exist in Coq. We show how by adding code annotations and cast axioms we can do this translation.
The generated Coq code for the interpreter is in Script_interpreter.v.