Mi-cho-coq tutorial • Formal Proving
In this new series of blog posts, we will be introducing Coq and Mi-Cho-Coq for proving Tezos smart contracts written in or compiled to Michelson. This series is structured as follows:
- 01. Formal proving: What is it about, what are Coq and Mi-Cho-Coq, and why will we need them.
- 02. A quick introduction to Coq
- 03. A quick introduction to Mi-Cho-Coq: proving our first Michelson smart contract.
- 04. Proving the increment contract
- 05. Proving if conditions.
- 06. Proving a token minting entrypoint
Chapter I
Introduction
When designing and implementing an algorithm, affirming that its implementation obeys a precise specification is very much a non-trivial problem. For example, how to make sure that Paris’ line 1 automated metro PID controller code is implemented properly? What about a trading routine at a multinational bank which’s execution will affect millions of transactions a day? A simpler way is to implement a second program that will perform automated tests on the first one. The shortcomings of this method is that these tests are ran on a finite amount of datapoints. Let me explain.
Say the task is to implement the identity function (id) which, given x returns x. If the only test is to check that id(0) == 0, then both of the following implementations would be valid since they’d both pass the test.
What we would like to do rather, is test that for all x in the natural numbers, id(x) = x as this test would fail for id2. Which brings us to Coq.
Coq: a proof assistant
Let’s try to imagine what might be a proof assistant. Say I have to prove the following: for all a, b in the real numbers, (a + b)^2 = a^2 + 2ab + b^2. What I might do is as follows:
(a + b)^2 = a^2 + 2ab + b^2
Step 1: develop the left hand side
(a + b)^2 = (a + b)(a + b) = a^2 + ab + ba + b^2
Step 2: simplify the left hand side
a^2 + ab + ba + b^2 = a^2 + 2ab + b^2
Step 3: compare the left and right hand sides
a^2 + 2ab + b^2 = a^2 + 2ab + b^2
What’s interesting here is that what I did as a mathematician is develop a strategy:
- develop and simplify the left hand side,
- compare left hand side to the right hand one and establish they are equal.
Moreover, I also did the manual work of development and simplification, which is very error prone even in this case, imagine what it must be like when simplifying complex dynamical systems by hand… So it’d be nice if I could tell my computer about the tactics I wanted to employ and it did the rest? That’s essentially what a proof assistant is for. Of course here, a proof in Coq would for this identity would surely be much longer since we have taken many things for granted in the above proof. Nonetheless, the idea is that a Coq will assist its users in proving propositions by showing them the results of each steps forward they make in their proofs.
In Chapter II, we’ll see how to get started with Coq.
Mi-Cho-Coq: a Michelson interpreter written in Coq
Mi-Cho-Coq is a Michelson interpreter written in Coq. Since Michelson contract entrypoints are all pure functions that return a pair of operation list and updated storage, one can execute each entrypoints in the Mi-Cho-Coq interpreter and witness its result. It is then possible to establish specifications that the entrypoints must implement guaranteeing that the specification is met for all possible inputs.
Say for instance that we have the following Michelson program that makes its new storage the input it was called with:
# Identity contract
{ parameter nat ; storage nat ; code { CDR ; NIL operation ; PAIR ; } }
We’d like to prove that forall input in nat, Identity(input) = new_storage and operations = nil, and that’s exactly what Mi-Cho-Coq will allow us to do. Proving this contract will also be our first proof using Mi-Cho-Coq which we’ll introduce more thoroughly in Chapter III.
Conclusion
In this chapter, we’ve motivated the need for formal proving of smart contracts, and introduced some of the key concepts needed to understand the next chapters covering Coq and Mi-Cho-Coq.
.png)
