Skip to main content

Limitations

Gitlab

Here we present the limitations of the translation to Coq of the protocol of Tezos. We believe that for now writing proofs is more of a priority.

Environment#

The Tezos protocol relies on an environment of primitives. We axiomatize all these primitives by either:

  • giving a direct definition, or
  • giving the properties supposed to be followed by the primitives.

There can be errors in these axiomatizations. We currently rely on manual reviews to make sure there are no errors.

Side-effects#

The side-effects outside of a monad (like the direct use of exceptions or references and the assert instruction) are not represented in the translation of coq-of-ocaml. Such side-effects are quite rare in the protocol, and not a priority for us yet. The error monad and the inlined ctxt value used as a state monad are correctly translated to Coq.

Axioms#

We sometimes use axioms in the translation. For example, for the matching on GADTs, we often use the cast axiom as show in Script_comparable.v. This axiom is unsound in general. However, it should only be used in safe instances as:

  • it is generated by coq-of-ocaml;
  • we follow the types computed by the OCaml compiler.

Ignored definitions#

We ignore some of the definitions when they are too hard to translate in Coq. To ignore definitions we use the @coq_axiom_with_reason attribute in OCaml. We also ignore some .ml files by translating the corresponding .mli files to axioms. This is done with the "require_mli" configuration option of coq-of-ocaml.

We cannot prove anything on ignored definitions. Ignored definitions generally require non-trivial changes in the OCaml code, but can be translated once these changes are made.

Validation#

For now, we verify the validity of the Coq translation by manually comparing the generated Coq code and the OCaml one. We could also do some tests by extracting the Coq code back to OCaml, and checking that it still behaves like the original OCaml code. This is not done yet and would require mapping all the axioms of the protocol's environment to their OCaml counterparts. Formally verifying that coq-of-ocaml preserves the semantics of OCaml is out of reach (too complex).