Skip to main content

Translation-of-the-protocol

Gitlab

Here we explain how to obtain an up-to-date version of the economic protocol of Tezos in Coq. The names of the branches in this document might change as we merge things, and we try to update this document if this is the case. The translation to Coq uses coq-of-ocaml. We maintain an output on this website.

Translating 🐓​

To make it works, install everything in the same "opam switch" environment.

  1. Compile Tezos from the branch of the merge request https://gitlab.com/formal-land/tezos/-/merge_requests/7 (so the branch master-with-coq-j-and-k in the repository formal-land/tezos) See How to get Tezos to compile Tezos.
  2. Install the development version of coq-of-ocaml from the branch ocaml-4.14. To install a development version, use for example:
    opam repo add default # because the install of Tezos generally disable it
    opam pin add coq-of-ocaml git@github.com:formal-land/coq-of-ocaml.git#ocaml-4.14
    To test that it worked, run the command coq-of-ocaml. It should display the help message.
  3. Clone the repository https://gitlab.com/formal-land/coq-tezos-of-ocaml:
    git clone git@gitlab.com:formal-land/coq-tezos-of-ocaml.git
  4. Assuming that coq-tezos-of-ocaml is cloned in the same folder as tezos:
    parent-folder
    ├── coq-tezos-of-ocaml
    └── tezos
    run the import script in Ruby:
    cd coq-tezos-of-ocaml
    gem install parallel # may need sudo mode
    cd scripts/j
    ruby import.rb ../../../tezos src/proto_013_PtJakart/lib_protocol ../../src/Proto_J
    cd ../..
    cd scripts/k
    ruby import.rb ../../../tezos src/proto_014_PtKathma/lib_protocol ../../src/Proto_K
    cd ../..
    cd scripts/alpha
    ruby import.rb ../../../tezos src/proto_alpha/lib_protocol ../../src/Proto_alpha
    This will (re)generate the Coq version of the protocol.
  5. Re-compile the coq-tezos-of-ocaml project, following the instructions on the README.md file. This will compile the generated Coq code to make sure it is valid, and also check the proofs.

Checking that it works​

To check that it works, you can make some changes to the OCaml source code of the protocol, re-compile Tezos and re-run the import script. By running a git diff, you should see the translated changes in Coq.

Adding proofs​

Almost anything should now be provable as we are in Coq. The convention is to write the proofs for a file A/B.v in a file A/Proofs/B.v. Then you can open a merge request on https://gitlab.com/formal-land/coq-tezos-of-ocaml

Look at the milestone Community if you want some simple tasks to start with and discover the repository.