Beginning of proof of equivalence with the implementation
This is a first step to formalize the equivalence of the OCaml implementation with Mi-Cho-Coq.
- we put everything in the
src/michocoq/of_ocaml
folder for now. Rationale: it did not require edits of the build scripts; - we extract the Coq generated by
coq-of-ocaml
on the fileproto_alpha/lib_protocol/script_typed_ir.ml
as seen on https://clarus.github.io/coq-of-ocaml/tezos/#proto_alpha%2Flib_protocol%2Fscript_typed_ir.ml (huge web page, takes time to load). We adapt the code to make it type-check in Coq by:- adding a few
Parameter
for the dependencies; - removing inductive constructors which do not respect strict positivity. We cannot bypass these errors event with the https://github.com/SimonBoulier/TypingFlags plugin, surprisingly and unfortunately;
- replacing the
lambda
type by an axiom;
- adding a few
- we write conversion functions from and to the OCaml formalization of the Michelson types. Two reasons for these not being bijections:
- we dropped some constructors while importing the OCaml code;
- there are no (of few) annotations in the Mi-Cho-Coq formalization. There are also some booleans on the OCaml nodes;
- we show that the conversion is a bijection for the comparable types, and an injection for the types (it should be a bijection too but we have not shown this part yet);
- we begin to write an injection for the Mi-Cho-Coq typed syntax to OCaml.
Edited by Guillaume Claret