Coq translation of the Tezos protocol

Announcements
1

A post to present the coq-tezos-of-ocaml project, aiming to help verify the crypto-currency Tezos. This project contains a translation in Coq of the economic protocol written in OCaml. We generate this translation using coq-of-ocaml. The translation is a shallow embedding of OCaml in Coq, expecting the side-effects to be into monads (mainly the state and errors effects for Tezos).

There are about 40.000 lines of generated Coq code, for around 30.000 lines of OCaml code as input. We write proofs on the translation in order to look for bugs. This matters as Tezos is a decentralized network, so a bug would allow stealing a large amount of money with minimal legal risks. Most of the proof work is yet to be done. Among things we want to verify are:

  • the equivalence between the Michelson interpreter and the Mi-Cho-Coq specification used to verify smart-contracts (the initial goal of the project);
  • the validity of the storage system, showing it can be simulated by standard OCaml data-structures;
  • all possible code invariants which would otherwise be verified by unit-testing.

An example of code translation to Coq from the protocol is the following:

(* input in amendment.ml *)
let may_start_new_voting_period ctxt =
  Voting_period.is_last_block ctxt >>=? fun is_last ->
  if is_last then start_new_voting_period ctxt else return ctxt

(* output in Amendment.v *)
Definition may_start_new_voting_period (ctxt : Alpha_context.context)
  : M=? Alpha_context.context :=
  let=? is_last := Alpha_context.Voting_period.is_last_block ctxt in
  if is_last then
    start_new_voting_period ctxt
  else
    return=? ctxt.

Contributions are welcomed, especially to write new proofs. For that, you can look at the contribute page.

2 Likes