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:
In Chapter III, we got familiar with MiChoCoq and how to use it to prove the simplest of all Michelson contracts, one that does nothing. In this chapter, we’ll be proving the increment contract.
The increment contract we will implement has a natural number as a storage, takes unit as a parameter, and returns no operations along with an incremented storage:
This contract works similarly to the identity contract we proved in the previous chapter except that it increments the popped storage by one before returning it in a pair.
Let’s setup the proof file as we did in Chapter III. This time we’ll also import the ZArith module as we’ll be needing it. Other than that, the code is structurally identical to what we did in Chapter III:
Let’s now define increment’s Michelson:
As you can see, the PUSH instruction is a little more complex than in Michelson, it takes 2 arguments. We can see in its definition that the first argument is a type and its second argument is concrete_data of that type. Hence, Michelson’s PUSH 1n becomes PUSH nat (nat_constant 1).
Let’s now formally specify our contract:
Notice how we specify that the evaluation should have increased the storage by unity: N.add storage_in 1 = storage_out. We’re using the function N.add in order to add 1 to storage_in and specify that it should equal storage_out. This means that we’ll need to perform a case analysis on storage_in. Recall that a natural number is defined as an inductive data type that takes two constructors, zero and the successor of a number. In Chapter II, we defined natural numbers as O and S n. In Coq however, they are defined slightly differently. You can evaluate Print N. in the CoqIDE and the Messages window will show its definition: Inductive N : Set := N0 : N | Npos : positive -> N. Hence Coq defines natural numbers slightly differently, a member of this type is either a positive natural, or zero. We can evaluate Print positive. to see how its defined:
Inductive positive : Set := xI : positive -> positive | xO : positive -> positive | xH : positive
As we can see, a positive can be one of three constructors. Please have a look at the comment above the implementation of positive in the Code source code to see why that is. Nevertheless, this means that we’ll need to prove the following cases:
1. storage_in = 0;
2. storage_in = Npos, which will need to be further destructed into its three constructors.
From there on, the proof is pretty straightforward as each of these cases are easy to prove individually:
We’ve seen in this chapter how to use natural numbers in a Michocoq contract definition and how to prove properties about them. This involved gathering a deeper understanding of how natural numbers are represented in Coq.
In the next chapter, we will be investigating a contract involving a condition, which will require us to be much more creative in our proofs as this will be our first non-trivial contract to prove. In particular, we’ll be defining and proving some of our own Lemmas we’ll be needing.