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 file proto_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;
• 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.