The Mi-Cho-Coq library represents the bridge between Tezos smart contract and formal proof in Coq.
The Mi-Cho-Coq library  is a formalization of the Michelson language  using the Coq interactive theorem prover .
In practice, the Mi-Cho-Coq library is used to produce a formal definition of a Michelson script (e.g. the "Modeling theorem" section). Each Michelson instruction has its equivalent in the Mi-Cho-Coq library (e.g. see the syntax subsection).
The Mi-Cho-Coq library provides a formal definition (in Gallina) of the type system (Michelson types), the syntax (instructions of the Michelson), the semantics (evaluator) and the lexing and parsing (for type-checking).
It is recommended to have notions of Language theory in order to understand the following Mi-Cho-Coq definition (grammar rules).
The type system consists in the definition of types (comparable types and non-comparable ones).
The **syntax and typing of Michelson instructions are formalized as a dependent inductive type to rule out ill-typed instructions.
Notice that the inductive type
instruction defines typing rules for each instruction (
The semantics of types is defined by interpreting them with predefined Coq types (e.g. int -> Z, nat -> N, mutez -> int63). The semantics of Michelson is defined by an evaluator
eval formalized as a Fixpoint.
Notice that the evaluator defines actions that must be performed for each type of instruction.
Since evaluating a Michelson instruction might fail (whereas Coq functions cannot), the return type of this evaluator is wrapped in an exception monad (handling errors such as overflow, lexing, parsing, fuel).
Coq forbids non-terminating functions, so we use a common Coq trick to define the evaluator on diverging instructions such as LOOP: we make the evaluator structurally recursive on an extra argument of type Datatypes.nat called the fuel of the evaluator.