Verify a smart contract with Archetype
Archetype is a simple high-level language to develop Smart Contracts on the Tezos blockchain. It enables to formally verify contracts by transcoding them to Why3. For more information on the Archetype language, please follow the link below:
In this article, we develop, specify and formally verify a smart contract; with formal verification, we find and fix bugs, and make sure it complies with its specification.
The video below is the screening of the demo (25 minutes):
Below is the textual version of the demo.
Contract
The objective of this demo is to develop a smart contract for an on-chain loyalty program. This contract records miles and miles owners with two entry points: add and consume.
Contract assets
A mile owner is identified by an address value and possesses several miles (potentially zero). A mile is identified by a unique string id and an expiration date so that a mile cannot be consumed after its expiration date.
The schema below illustrates the basic modeling of data:
An optimization is added to the above model. A mile is augmented with a quantity value to gather several miles with the same expiration date. For example, 3 miles with the same expiration date are merged into one mile with the quantity value set to 3:
Code
The following snippet below is the archetype implementation of the contract data:
Note that the type of collection of miles (line 11) is partition: this is to specify that one mile is owned by one and only one owner. This prevents for example from adding or removing a mile straightforwardly to the mile collection. It must go through the miles collection of an owner.
When adding a mile to an owner’s miles collection, it is tested whether the mile already exists; if so, the add instruction fails.
This is implemented with a single mile collection and the miles field is implemented as a list of mile identifiers, not as a list of miles.
Actions
The add action has two arguments: an owner address and a new mile to add to this owner:
owner above (line 4) is the collection of all owners. The get method enables to retrieve one owner from its address (which is the owner identifier).
The add method (line 5) is used to add an asset to a collection (here o.miles).
The consume action takes two arguments: an owner's address ow and the number of this owner’s miles to consume qty :
The implementation of the consume action is not that straightforward because of the quantity field carried by each mile:
- the collection of the owner’s valid miles is created with the select method (line 4)
- miles are removed until the number of removed miles is equal to qty; for that, each valid mile is iterated: if current mile’s quantity is less than the remaining number of miles to remove (line 9), then the mile is removed (line 11) and the remaining value is decreased by its quantity; otherwise current mile’s quantity is decreased (line 14) and remaining number is set to 0 (line 13)
This implementation has 2 bugs: can you spot them? The verification presented in the section below will help to detect and fix them.
Specify
Note that the type of the quantity field of the mile asset is int (ie. integer line 6 in the asset section above), which may be negative. However, it does not make sense for the quantity to be equal or lower than zero. We would like to specify some constraints on the quantity field, specifically that it should remain strictly positive.
It is possible to specify such a constraint with an asset invariant (lines 5 to 7 below):
This will generate the corresponding proof obligations for all actions (add and consume).
We want to operate the contract from one address, that is that each action may only be called by this address. Archetype provides a dedicated “modifier” called by (line 4):
The security predicate only_by_role (line 2 below) may be used in the security section to specify that any action should use the called by modifier on admin:
The no_storage_fail predicate (line 3 above) is useful to state that an action (here the add action) should not fail, either with a “key not found” or “key exists” exception. It is usually best practice not to program with logical exceptions, either explicit (with try … catch mechanisms) or implicit like in smart contracts which come with a rollback mechanism in case of failure. It is better to explicitly open execution branches with if then else controls. Exceptions should be used only for hardware, network … failures, that is to say, anything the program itself does not have control over.
Obviously, this is not the case of the add action which will fail for example if ow does not correspond to any existing recorded owner.
These security predicates generate proof obligations as presented in the verification section below. The list of available security predicates may be found here.
At last, we want to make sure the implementation of the consume action complies with the basic requirement that qty miles are removed. The way to formulate such a requirement is to set up an arithmetic relation between the storage state before the execution of the action and after the execution:
The postcondition p1 (line 5 above) literally reads “the sum of quantity fields after execution of consume is equal to the sum before execution minus the value qty”.
As a recap, here is the full contract code before verification:
Verify
In this section, we verify the 4 predicates defined in the previous section:
- s0: any action may be called only by the admin role
- s1: the add action does not fail when accessing the storage
- p0: the consume action consumes exactly qty miles
- i0: the quantity value of any mile is strictly positive
The VS Code archetype extension provides a left panel which lists the predicates and enables to call why3 ide on each one to be verified:
The contract and the predicate are transcoded to the why3 format (whyml). In order to invoke the why3 ide, click on the check icon on the right of the predicate in the archetype extension panel.
In order to verify the property with why3, just right-click on the module named “Miles_with_expiration”, and select “Auto level 2” as illustrated below (here for security predicate s0):
Why3 translates the predicates in SMT language and invokes the SMT solvers (here Alter-Ergo, Z3, and CVC4). We see in the above screenshot that Why3 has generated proof obligations for both actions (add and consume).
Security predicate s0
When a predicate is validated the question mark turns green. The consume action does not turn green as illustrated below:
This is because the called by modifier is missing in the consume action. When added, the s0 property is then verified:
Security predicate s1
The no_storage_fail predicate s1 is not verified either on the contract above. When looking in details at the failing proof obligations, we see that both the “Key not found” and “Key exists” exceptions may be raised:
We see that the get method may generate a NotFound exception (see screenshot above) and that the add method may generate a KeyExist exception.
The solution is first to test the existence of an owner with id ow. In the case it does not exist, a new owner should be created. In any case, add should fail if the id of newmile is already present:
We see the effect of not allowing the code to fail: it forces us to handle all situations and make behavior explicit. Here we had simply forgotten to create an owner when necessary! s1 is now verified:
Postcondition p0
The effect of the consume action uses an iteration over the valid miles of owner ow. It is then necessary to provide why3 with loop invariants for p0 (why3 relies on Weakest Precondition calculus).
It is the trickiest part of the verification process since it requires some experience in figuring out the invariants.
In the p0 case, the invariant should use the remainder variable which is decreased from qty to 0 during iteration. At any iteration we have the relation:
mile.sum(the.quantity) =
mile.before.sum(the.quantity) - qty + remainderAt the end of the iteration, the remainder variable is equal to 0, which rewrites as p0.
However, why3 still fails to prove p0 because it is not trivial to prove that the remainder variable is equal to 0 at the end of the iteration. Another invariant may be provided for that purpose:
0 <= remainder <= toiterate.sum(the.quantity)The toiterate keyword refers to the collection of miles which have not been iterated on yet, and are still to be iterated on. At the end of the iteration, the toiterate collection is empty and the sum over it is equal to 0.
The following Archetype snippet illustrates how to provide these invariants (lines 5–8 below):
Note that we had to name the iteration (loop line 7 above).
With the code above, p0 is verified. However, 2 proof-obligations still fail.
The first one corresponds to the initialization of the second loop invariant (line 15 above):
It fails to prove that the remainder variable is greater or equal to 0 at the beginning of the iteration. Since it is equal to qty at this stage, the solution consists of adding a guard condition that requires qty to be greater or equal to 0.
The second failing proof obligation corresponds to the proof of heredity of the main loop invariant (line 6 above) in the second execution branch (lines 23,24 above) when the current mile quantity is greater than the remainder variable:
Why3 highlights the branching conditions that are not true in the current proof obligation (in purple line 317 in the above screenshot), which indicates precisely which execution branch has a problem.
The issue is that the remainder variable is set to 0 before updating the current mile quantity field. The solution is to swap instructions lines 23 and 24.
The fixed version of the consume action is presented below:
Invariant i0
The invariant i0 has to be verified every time the mile collection is modified. Here the invariant is not verified, either in the action add or consume.
In the add action, the add method (line 8 above) requires that the added mile (newmile) has a quantity field strictly positive:
The solution is to add a guard condition (lines 3–5 below):
In the consume action, the update method requires the mile quantity to be positive, as specified by the asset invariant, but solvers fail to prove it:
The branch is the else branch of the test
m.quantity < remainderwhich is
m.quantity >= remainderIndeed when quantity is equal to the remainder variable, it records a mile with a quantity value equal to 0, which does not comply with i0.
The solution is to change the branching test to
m.quantity <= remainderConclusion
Thanks to the formal verification features of Archetype, we have been able to develop a correct smart contract that implements an on-chain loyalty program:
It is now safe to transcode the archetype contract to a lower-level language like Ligo, from which it is then possible to generate the Michelson version:
Program verification is a very powerful technique to find and fix issues. It is also a very good way to boost the trust users may have in the contract, especially when verified properties are easy to read and understand.
We note however that safety is not an absolute quality but rather is relative to the properties we are able to identify and formulate.
Below is the list of software used in the demo for you to reproduce it:
- Archetype 0.1.10
- VS Code 1.39.2
- Why3 1.2.0
- Alt-Ergo 2.2.0
- CVC4 1.6
- Z3 4.8.4
Note that archetype is still in alpha version. We plan to release version 1 by the end of the year.
Follow us on Twitter to be updated on the evolution of the project:
