Mi-cho-coq tutorial • Proving the increment contract

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 IV: Proving the increment storage contract

Introduction

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

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:

{ CDR ;
   PUSH 1n ;
   ADD ;
   NIL operation ;
   PAIR
 }
storage nat;
parameter unit;

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.

Proof

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:

Require Import Michocoq.macros.
Import Michocoq.syntax.
Require Import Michocoq.semantics.
Require Import Michocoq.util.
Import error.
Require Import ZArith.

Definition parameter_ty := unit.
Definition storage_ty := nat.

Module ST : (SelfType with Definition self_type := parameter_ty).
  Definition self_type := parameter_ty.
End ST.

Module increment(C:ContractContext)(E:Env ST C).

Module semantics := Semantics ST C E. Import semantics.

Let’s now define increment’s Michelson:

Definition increment : full_contract _ ST.self_type storage_ty :=
  ( CDR ;;
    PUSH nat (nat_constant 1) ;;
    ADD ;;
    NIL operation ;;
    PAIR
 ).

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:

Theorem increment_correct :
  forall (input : data unit) storage_in
         (ops : data (list operation)) storage_out
         (fuel : Datatypes.nat),
  fuel >= 10 ->
  eval env increment fuel ((input, storage_in), tt) = Return ((ops, storage_out), tt)
  <->
  N.add storage_in 1 = storage_out /\
  ops = nil.
Proof.
Admitted.

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:

Proof.
  (** proof prologue **)
  intros input storage_in ops storage_out fuel Hfuel.
  rewrite return_precond.
  unfold eval.
  rewrite eval_precond_correct.
  unfold ">=" in Hfuel.
  simpl.

  (** our actual proof **)
  do 4 more_fuel ; simpl.
  destruct storage_in.
  - (* storage_in = 0 *) 
    more_fuel.
    simpl. split.
    * intros. split ; congruence.
    * intuition. congruence.
  - (* storage_in = positive 
       we'll need to destruct "positive" into
       its three constructors. *)
    more_fuel ; simpl. destruct p.
    * simpl. split.
      + intros. split ; congruence.
      + intros. destruct H. congruence.
    * simpl. split.
      + intros. split ; congruence.
      + intros. destruct H. congruence.
    * simpl. split.
      + intros. split ; congruence.
      + intros. destruct H. congruence.
Qed.

Conclusion

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.

Go to the next part :

• Mi-cho-coq tutorial • Proving if conditions