Skip to main content

Contribute

Gitlab

πŸ‡

The main work needed is to write proofs.

In this project, we present a translation in Coq of the implementation of the economic protocol of Tezos. This translation by itself does not provide any additional safety. It is only useful if we can verify properties on this translation. Since we translate OCaml code to vanilla Coq code, it should be possible to verify arbitrarily complex properties given the right lemmas.

We believe that this project represents a unique opportunity to write interesting Coq proofs, as:

  • there is a lot of code to verify (around 50.000 lines);
  • this is about a real implementation with a lot of money at stake (Tezos);
  • the code is mostly purely functional or monadic (high-level, no low-level issues like pointers analysis, few encodings);
  • this is updated as the OCaml source code changes. So the aim is also to write maintainable proofs, interacting with the OCaml developers.

Contact​

If you want to start writing proofs about the protocol and want to communicate about that, please either:

To make a contribution, open a merge request on coq-tezos-of-ocaml/-/merge_requests.

Code structure​

The code is in the GitLab repository coq-tezos-of-ocaml, with the latest protocol version in the folder src/Proto_alpha/. Since the protocol structure is flat (all the files in the same folder), the Coq translation is also flat. The translated files have the same name as in OCaml but are capitalized to follow the Coq's convention. For example, apply.ml is translated to Apply.v.

We translate the .mli file of the environment in Environment.v. Because this is a .mli file, we generate a translation with one Coq axiom per declaration in OCaml. In the folder Environment/, we have one file per module of the environment. These files are written by hand. They contain the concrete definitions or the axiomatized specifications of the environment. We check, by module inclusion, that the definitions in the Environment/ folder are compatible with the declarations in the Environment.v file.

We put our proofs files in Proofs/ folders, using the same name as the file they are referring to. For example, the proofs about the Apply.v file would be put into Proofs/Apply.v. We also have a folder Environment/Proofs/ for the definitions of the environment in Environment/. This follows the convention used by some projects of putting test files in a test/ folder, with the same name as the tested file.

For .ml files which would be too hard to translate to Coq, we translate the corresponding .mli file to axioms. Otherwise, we only translate the .mlΒ file.

Examples to start with​

Here are a few examples to start contributing to the formal verification of the protocol of Tezos:

  • having lemmas about the Environment/Map.v and Environment/_Set.v data structures;
  • filling up definitions for parts of the environment that are axioms but could be replaced by definitions. For example, in Environment/List.v, there are still many primitives declared as Parameter, which should be replaced by a corresponding Definition. Having the usual lemmas about the list primitives could be useful too.
  • verifying properties about files without too many dependencies, like for example Misc.v;
  • verifying properties about high-level files, like Apply.v, using axioms about what is needed when there are calls to other files.

Also, we are currently verifying the storage of the protocol, what should help to reason about functions using the storage. A function may use the storage when it is parametrized by the context ctxt. This is an inlined state monad.

Re-generate the Coq translation​

To see how to re-generate the Coq translation of the protocol, look at this HOWTO document. This can be useful to understand how the translation works or to update the OCaml source to simplify the proofs.