# HOWTO: translating the protocol to Coq

The HOWTO is now on https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/guides/translation-of-the-protocol

<!--
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.

This uses `coq-of-ocaml` https://foobar-land.github.io/coq-of-ocaml/. We maintain an output on `coq-tezos-of-ocaml` https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml . Currently everything works, except for the interpreter / translator for which we only compile the `.mli` files.

## Translating
Note that we currently support OCaml 4.12.1, which corresponds to the OCaml version used by the development version of Tezos. Install everything in the same opam switch environment so that it works.
1) Compile Tezos from the branch https://gitlab.com/clarus1/tezos/-/tree/guillaume-claret@proto_alpha-coq-of-ocaml-proto-j (so the branch `guillaume-claret@proto_alpha-coq-of-ocaml-proto-j` in the repository `clarus1/tezos`) See [How to get Tezos](https://tezos.gitlab.io/introduction/howtoget.html#setting-up-the-development-environment-from-scratch) to compile Tezos.
2) Install the development version of `coq-of-ocaml` from the branch `master`. To install a development version, use `opam pin add coq-of-ocaml [e-mail]:foobar-land/coq-of-ocaml.git#master` for example. To test that it worked, run the command `coq-of-ocaml`. It should display the help message.
3) Clone the repository https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml . Assuming that this repository is cloned in the same parent folder as `tezos/tezos`, run from it the import script in Ruby:

gem install parallel # may need sudo mode
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 in the folder `src/Proto_alpha`.

4) From the root of the `coq-tezos-of-ocaml` project, install the Coq dependencies:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only

and run:

./configure.sh
make -j

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 some 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/nomadic-labs/coq-tezos-of-ocaml

Our current target is to specify and verify the storage (`storage.ml`). A good start to prove some properties is to look at files without much dependencies. The dependencies of a file are listed at its top with the `Require` commands. Examples of files without many dependencies are `misc.ml` or the `*_repr.ml` files.
-->