Skip to main content

Readme

Gitlab

Protocol proofs are located in this directory. These proofs are Coq scripts wherein we formally verify various properties of the protocol. We organize these proofs in a folder next to the code, giving each proofs file the same name as the code file to which it corresponds. Please open an issue on the GitLab repository for any remarks or concerns.

There are many properties verified within each proofs file, but we will describe just the main ones below.For a more comprehensive overview of the work being done, please have a look at the company blog.

Serialization

With the data-encoding library, we convert values to and from a binary representation, using these conversions to store values in our database. For security, it is important that our conversions be bijective. We verify this for data-encoding functions, starting from an axiomatization of data-encoding primitives. An example file containing such proofs is Proofs/Block_header_repr.v, where we verify the data-encoding functions defined in Block_header_repr.v.

Storage system

The storage system as defined in storage.ml has some complexities related to the fact that it needs to be efficient and store data in a binary format on disk. Currently, we show that it is equivalent to a simpler in-memory storage, using standard OCaml data structures such as records, sets, and maps. We validate this equivalence with a simulation proof. This simulation serves as both a specification and formal verification of the storage. This simulation can also be useful in formally verify files using the storage system. An entry-point for proofs about the storage system is Proofs/Storage.v.

Michelson language

The Mi-Cho-Coq project gives a formal specification in Coq of the language of Michelson, used to write smart contracts in Tezos. We are starting to show that this formal specification corresponds to what is in the implementation of the protocol. Since we translate the protocol to Coq, we can show that the implementation and the specification of Michelson are isomorphic. An example of such a proof can be found in Proofs/Script_typed_ir/Comparable_ty.v.

Saturation arithmetic

We plan to show that saturation arithmetic, as defined in Saturation_repr.v, is sound. We use saturation arithmetic to compute the gas fees of smart contracts more efficiently.