During our work on verification of Tezos source code,
we run into an interesting question: how to implement OCaml's GADTs in Coq?
The essence of this problem, as well as its solution, were described in
the article: Translating the Michelson interpreter
where we show how we introduce casts in the generated Coq code.
In this article, we will consider subsequent work in this direction.
To reach one of our main goals, proof of the compatibility of the parsing
and unparsing functions for the Michelson types and values,
we need to avoid casts. A powerful Coq's instrument, the dependent types, will help
us to solve the casts problem. We create a kind of clone of coq-of-ocaml's
code, which is a dependently typed version.
The whole process can be structured as follows:
- the
Simulationsfolder (along with its purpose and content), - definition of dependent types,
- definition of functions with dependent types (analogs of functions with casts),
- proof of the equivalence between functions with dependent types and functions with casts,
- proof of assertions and properties for functions with dependent types.
and this is how it is all organized in the repository:
- we keep files, generated by
coq-of-ocamlin folderProto_alpha - we keep dependently-defined types and functions in folder
Simulations - we keep our proofs in folder
Proofs