4 posts tagged with "michelson"

The backward compatibility is an important property to maintain between two releases of the protocol of Tezos. For example, this ensures that existing smart contracts still work after a protocol upgrade. That property can be hard to ensure by the protocol developers as the codebase's size increases. At the time of writing, there are 86,346 lines of code in src/proto_alpha/lib_protocol in the master branch of Tezos, counting all the .ml and .mli files.

We propose using formal verification to check that the backward compatibility is preserved after each protocol release, with a mathematical degree of certainty. More precisely, we show that for every inputs and storage contexts, a smart contract working with version Jakarta of Tezos will generate the exact same output running on the next version K. Even if there are infinitely many possible inputs, we can verify all of them by writing a mathematical proof in the formal system Coq.

In this blog post, we describe our plan for this verification effort.

Verifying the implementation of the interpreter of Michelson smart contracts is of importance because one of the strengths of Tezos is to be able to formally verify the smart contracts. In order to make this verification sound, we need to show that the smart contracts verification framework 🍬 Mi-Cho-Coq is coherent with the actual implementation of Michelson. In this blog post, we show how we translated the Michelson interpreter from the OCaml language to Coq. This is the first step to show the coherence of Mi-Cho-Coq with the implementation.

The main file of the interpreter is script_interpreter.ml (around 1,800 lines). The abstract syntax tree of smart contracts is given in script_typed_ir.mli (around 1,600 lines). We translate the OCaml code to Coq using coq-of-ocaml. A difficulty in translating the interpreter is that it heavily relies on GADTs in OCaml, a feature that does not exist in Coq. We show how by adding code annotations and cast axioms we can do this translation.

The generated Coq code for the interpreter is in Script_interpreter.v.

Mi-Cho-Coq is a Coq framework which we use to verify smart contracts written in Michelson, the language of smart contracts for Tezos. You can get an introduction to formal verification on Michelson code on opentezos.com/formal-verification.

We want the highest possible level of confidence in the result of our verification work but there is a gap between Mi-Cho-Coq, which was manually written in Coq, and the Tezos protocol. To fill this gap, we want to prove that the semantics of the Michelson language defined in Mi-Cho-Coq exactly matches the mechanic translation of the Michelson interpreter from the Tezos protocol, which we import to Coq using coq-of-ocaml. Defining a bijection between the two type grammars is a requirement for this project. A difficulty is that, because Michelson evolves quickly and Mi-Cho-Coq is handwritten, some recent features are missing in Mi-Cho-Coq. This verification work can also help in identifying them.

An issue with recursive functions is that they may raise a stack-overflow error if the number of recursive calls is too high. To avoid these errors, many functions in Tezos are written in tail-recursive style. This style is usually harder to read and this could lead to mistakes in the code. We show in this post how we verify a tail-recursive function by comparing it to its naive non tail-recursive version.