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:
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.
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:
We can now hop into the container and launch the Coq IDE with some Mi-Cho-Coq file:
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:
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:
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:
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:
Let’s now prove this contract.
Let’s start with some necessary imports:
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:
We now have some necessary modules to define for Michocoq to operate properly:
Finally, we can input our contract’s Michelson instructions:
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:
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:
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:
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:
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:
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:
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:
Using congruence, this goal was solved instantly.
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.