Mi-cho-coq tutorial • Proving our first Michelson smart 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 III: Mi-Cho-Coq

Introduction

Now that we have a rudimentary understanding of Coq, let’s start using Mi-Cho-Coq to interpret a simple Michelson contract and prove that it meets some specification. We’ll first get a Coq environment setup with Michocoq working before defining a very simple contract that doesn’t do anything when called. We’ll then prove that it does indeed nothing in Coq, which will require use to get familiar with how Michocoq works.

Getting started

The simplest way to get started working with Mi-Cho-Coq is through the CoqIDE. For convenience, we provide a Docker image with everything already setup:

host $ git clone git@gitlab.com:equisafe/nyx.git
host $ cd nyx/mi-cho-coq/
host $ docker-compose up -d
host $ docker ps
CONTAINER ID        IMAGE
dbafd3fc597d        thomasbinetruy/eqs-nyx:michocoq

We can now hop into the container and launch the Coq IDE with some Mi-Cho-Coq file:

host $ docker exec -it dbafd3fc597d /bin/bash
container $ eval $(opam env)
container $ cd tutorials/scripts
deposit.v helloworld.v
container $ coqide helloworld.v

You should now see the following:

As you can see, the file begins with multiple Michocoq imports. As you’ve probably realized by now, when working on a proof, you step through each instructions in the file you’re working on. If the instruction executes properly, it becomes highlighted in green, otherwise in red. Moreover, the IDE’s top right pane updates the (sub)goal(s) along with the current hypotheses, and the bottom right pane shows Coq’s relevant messages such as errors, computation results and documentation.

By clicking on the various arrows on the toolbar at the top, you can, from left to right:

 
• step through the file intructions one by one forward;
• step through the file intructions one by one backward;
• step through all instructions from the top of the file until the cursor location;
• jump to the beginning of the file;
• run the entire file
 

Having now opened helloworld.v in the CoqIDE, you can now step through this simple proof to make sure that the MiChoCoq imports work as expected, meaning that the first line should become highlighted in green as shown in the screenshot bellow:

A Michelson Hello World contract

As a first example, we’ll prove that our identity contract works properly. Informally, this contract is a function that returns a pair with an empty list of operations as the first element, and the current contract storage as a second when you call it with no parameter (i.e. it is called with unit as parameter). The following Michelson instructions implement such a contract:

{ CDR ;
  NIL operation ;
  PAIR }
storage nat;
parameter unit;
 

Remember that Michelson contracts are called with a single element on the stack being a pair with the contract argument as first element and current storage as second element. Let’s go through each instructions:

 
1. CDR: replaces the top element on the stack (our parameter-storage pair) with its second element (the current storage). Note that if the stack top element is not a pair, the contract will not typecheck.
2. NIL operation: pushes an empty list of operations on the stack.
3. PAIR: replaces the two top stack elements with a pair containing these two elements. In this case, we replace the current stack {stack top} NIL operation : storage {stack bottom} with PAIR (NIL operation) storage.
 

Let’s now prove this contract.

Proving our Hello World contract

Let’s start with some necessary imports:

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

These imports speak for themselves, but don’t be afraid to go dig into the relevant Michocoq files and skim over the Readme.

Let’s now define our parameter and storage definitions:

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

We now have some necessary modules to define for Michocoq to operate properly:

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

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

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

Finally, we can input our contract’s Michelson instructions:

Definition helloworld : full_contract _ ST.self_type storage_ty :=
  ( CDR ;;
    NIL operation ;;
    PAIR
  ).

Notice that the syntax is almost identical to Michelson, but that the curly braces have been replaced by parentheses and that instructions are now separated by double semi-colons. Apart from that, nothing has changed.

Let’s now define what we want to prove. Whereas we specified the contract informally at the beginning of this article, we shall now specify it formally. We’ll write the following in Coq:

 
1. Forall inputs of type parameter_ty, initial and new storages of type storage_ty and operations of type list operation;
2. After having evaluated helloworld as defined in Michelson above, the following must hold: storage_in = storage_out / ops = nil
 

In order to evaluate helloworld, we’ll use the eval fixpoint provided by Michocoq along with the input parameter and initial storage. We’ll also be passing a fuel parameter, which is not to be confused with the gas costs induced by a contract execution on Tezos. Here, fuel is of type nat which and will decrease by unity every recursive calls in eval until the function ends, ensuring termination of the function for all inputs. Indeed, Coq requires that a fixpoint terminates to ensure type consistency, hence the needed fuel parameter. Please read the “Semantics” section of Michocoq’s Readme for more information on this:

To define our contract specification in Michocoq, we write the following theorem:

Theorem helloworld_correct :
  forall (input : data parameter_ty) storage_in
         (ops : data (list operation)) storage_out
         (fuel : Datatypes.nat),
  fuel >= 10 ->
  eval env helloworld fuel ((input, storage_in), tt) = Return ((ops, storage_out), tt)
  <->
  storage_in = storage_out /\ ops = nil.
Proof.
Admitted.

Let’s see what differs from our initial specification written informally above.

First, and most notably, we specify that eval ... = Return .... Recall that Coq functions need to terminate, whereas Michelson functions do not (they can throw FAILWITH), hence, Michocoq wraps the evaluation results in an error monad (see the “Semantics” section of Michocoq’s Readme and the monad implementation in error.v). Essentially, if the evaluation succeeds, the result will be wrapped in Return whereas it will be wrapped in Failed if the evaluation threw.

Secondly, notice the env argument to the eval call, it provides the semantics for some extra instructions, quoting Michocoq’s Readme bellow:

The `env` parameter to `eval` is a record providing the semantics of the following instructions:  

• forging operations: CREATE_CONTRACT, SET_DELEGATE, and TRANSFER_TOKENS: these cannot be defined directly because the operation type is axiomatized.
• requesting information about the context: AMOUNT, BALANCE, CHAIN_ID, NOW, SELF, SENDER, and SOURCE
• cryptography: HASH_KEY, BLAKE2B, SHA256, SHA512, and CHECK_SIGNATURE (not yet formalized)
• serialization: PACK and UNPACK (not yet formalized)
• manipulation of addresses: ADDRESS, CONTRACT, and IMPLICIT_ACCOUNT (not yet formalized)

Let’s now prove our theorem. We’ll first introduce our variables along with the fuel hypothesis (fuel >= 10) and use a few lemmas provided by Michocoq to rewrite our goal in a form that’s simpler to manipulate. We will:

1. rewrite our goal using return_precond to handle the error monad, see the Lemma here;
2. unfold eval, which well essentially replace the eval call in our goal with its implemetation;
3. rewrite our goal using eval_precond_correct to handle the precond introduced in our goal in the previous step, see the Lemma here;
4. then, we rewrite our fuel hypothesis form fuel >= 10 to 10 <= fuel using unfold ">=" in Hfuel.;
5. finally, we simplify using simpl..

We can then start stepping through the contract using the more_fuel tactic provided by Michocoq. You should see the goal updating every time you step through the evaluation function until you reach the end of the function, where we the need to prove then “final” goal.

Let’s now see what the full proof looks like:

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 **)
  (* stepping through the Michelson instructions *)
  more_fuel ; simpl.
  more_fuel ; simpl.
  more_fuel ; simpl.
  (* We now need to prove:

     input : data parameter_ty
     storage_in : comparable.comparable_data storage_ty
     ops : data (list operation)
     storage_out : comparable.comparable_data storage_ty
     fuel : Datatypes.nat
     Hfuel : 7 <= fuel
     ______________________________________(1/1)
     (nil, storage_in, tt) = (ops, storage_out, tt) <->
     storage_in = storage_out /\ ops = nil
  *)
  intuition ; congruence.
Qed.

As you can see, once we’ve setup the proof and stepped through all contract instructions using more_fuel, the proof is very simple for our contract. It is as simple as intuition ; congruence. The intuition tactic is useful when the goal is made up of simple implications and/or conjuctions and disjuctions. In our case, it rewrites the goal as three subgoals that can all be solved using the congruence tactic. Then, rather than writing three bullets to handle each subgoals, Coq lets us use the semi-colon (;) after intuition to call the next tactic (congruence in our case) on all subgoals. Note that we could have done without intuition at the cost of a few more lines by using split and desctruct:

...
more_fuel ; simpl.
split.
- split. congruence. congruence.
- intros H. destruct H. congruence.

Finally, concerning the congruence tactic, let’s quote the “Congruence” section of the “UseAuto” chapter in Software Foundations volume II:

The tactic congruence is able to exploit equalities from the proof context in order to automatically perform the rewriting operations necessary to establish a goal.  

Source: https://softwarefoundations.cis.upenn.edu/plf-current/UseAuto.html

We had a classical use of the congruence tactic in our proof above where we had the following goal and hypothesis:

H : (nil, storage_in, tt) = (ops, storage_out, tt)
______________________________________(1/1)
storage_in = storage_out

Using congruence, this goal was solved instantly.

Conclusion

In this article, we’ve been through a Michocoq Hello World proof, where we got to formally specify our contract’s behavior and proved it. We’ve also been introduced to quite a few new tactics such as rewrite, intuition, split and congruence. In the next article, we shall prove a contract that increments by one its storage when called. But before, if you need to brush up on some Coq tactics, be sure to skim through the following cheatsheet.

Go to the next part :

• Mi-cho-coq tutorial • Proving the increment contract