Verify a smart contract with Archetype

Benoit Rognier
Nov 5, 2019 · 10 min read

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

Contract assets

The schema below illustrates the basic modeling of data:

Image for post
Image for post

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:

Image for post
Image for post
3 miles with the same expiration date …
Image for post
Image for post
… merged into one asset.

Code

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

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

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

  • 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:

Image for post
Image for post
Archetype contract in VS Code

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):

Image for post
Image for post
Why3 ide 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

Image for post
Image for post

This is because the called by modifier is missing in the consume action. When added, the s0 property is then verified:

Image for post
Image for post

Security predicate s1

Image for post
Image for post
A failing proof obligation for s1: the “get” method may generate a NotFound exception

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:

Image for post
Image for post

Postcondition p0

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 + remainder

At 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):

Image for post
Image for post

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:

Image for post
Image for post

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

In the add action, the add method (line 8 above) requires that the added mile (newmile) has a quantity field strictly positive:

Image for post
Image for post
add method of owner’s mile collection requires a quantity field > 0

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:

Image for post
Image for post

The branch is the else branch of the test

m.quantity < remainder

which is

m.quantity >= remainder

Indeed 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 <= remainder

Conclusion

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:

Image for post
Image for post
Archetype generation commands
Image for post
Image for post
Ligo version of the contract

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:

Image for post
Image for post

Get Best Software Deals Directly In Your Inbox

Image for post
Image for post

Coinmonks

Coinmonks is a non-profit Crypto educational publication.

Sign up for Coinmonks

By Coinmonks

A newsletter that brings you week's best crypto and blockchain stories and trending news directly in your inbox, by CoinCodeCap.com Take a look

By signing up, you will create a Medium account if you don’t already have one. Review our Privacy Policy for more information about our privacy practices.

Check your inbox
Medium sent you an email at to complete your subscription.

Benoit Rognier

Written by

CEO and co-founder of edukera

Coinmonks

Coinmonks

Coinmonks is a non-profit Crypto educational publication. Follow us on Twitter @coinmonks Our other project — https://coincodecap.com

Benoit Rognier

Written by

CEO and co-founder of edukera

Coinmonks

Coinmonks

Coinmonks is a non-profit Crypto educational publication. Follow us on Twitter @coinmonks Our other project — https://coincodecap.com

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store