3 posts tagged with "translation"

Tezos uses the json-data-encoding library throughout the protocol to serialize data for use in RPC, writing to disk or placing in a block. RPC is a synchronous operation. Consequently, it is paramount to verify the correctness of code as well as the logical equivalence and semantics of performance-enhanced procedures to proven ones.

This library has been subject to stack overflows, as seen in issues like this. We will translate and verify this library to validate its logic and simplify debugging these issues.

After each new release of the protocol there comes a need to validate it. One of the options would be to start from scratch, but fortunately there is no need for that since many parts of the protocol are only slightly changed or stay the same. That allows us to reuse old proofs in consequent versions and speed up the validation.

Of course there is a small number of proofs which stop working due to the changes and that has to be repaired. This process can sometimes be tricky since it requires an understanding of how different functions and proofs depend on each other, but that makes it very interesting. In this post, we will show examples of broken proofs, discuss reasons for their failure, and show techniques we used to fix issues.

Recently, an important merge request landed in Tezos to implement Tenderbake. This new consensus algorithm offers deterministic finality:

"a block that has just been appended to the chain of some node is known to be final once it has two additional blocks on top of it, regardless of network latency." (Nomadic Labs' blog)

This merge request and other changes resulted in almost 10,000 new Coq lines 🐓 in the translated code.

In this blog post, we explain how we dealt with all recent code changes to maintain the Coq translation of the protocol. We use the tool coq-of-ocaml to do our translation. The resulting Coq code is what you can browse on this website. All our changes on the OCaml code are in our fork branch guillaume-claret@proto_alpha-coq-of-ocaml. The procedure to compile the protocol to Coq is in this HOWTO.