Formal property

A formal property is a logical formula about the relations between data values and/or asset collections properties. It is made of:

• logical connectors: and, or, -> (logical implication), not, ...

• quantifiers: the universal quantifier forall __and the existential quantifier exists

• atomic predicates, which are the relations between values and/or asset collection:

  • between values (integers, tez, ...): =, <=, >=, <, >, ...

  • between asset collections: subset, diff, ...

  • between an asset and a collection: mem (member of), ...

For example, say you are dealing with an auction contract which has to decide the maximum bid over all bids stored in the bid asset collection, and say this value is stored in the max_bid variable over. The following is the way to express that max_bid is the highest bid:

forall b : bid, b.value <= max_bid

It reads that any stored bid value is less or equal than max_bid.

This property would typically serve as formal specification of the function declare_winner which computes max_bid as follows:

variable max_bid tez = 0tz
​
action declare_winner = {
  specification {
     p : forall b : bid, b.value <= max_bid;
  }
  effect {
     max_bid := ... (* code to compute max_bid *)
  }
}

This generates a verification task which consists in proving that the effect of the declare_winner action on the max_bid is actually to set it to the maximum bid value.

Data invariant

It is possible to specify the property a data is supposed to have throughout the life of the contract, regardless of the calls made to the contract and the changes of values of other data.

For example, say a quantity field of an asset mile should remain strictly positive. Use the with keyword to introduce the property, as illustrated below:

asset mile identified by id = {
   id : string;
   quantity : int;
} with { 
  i : quantity > 0
}

This generates as many verification tasks as the number of actions/transitions in the contract. Each verification task consists in proving that the property below holds after it is executed (it's called the post-condition), under the assumption it holds before (called the pre-condition):

forall x : mile, x.quantity > 0

It is also possible to declare a state invariant.

Say for example the contract should not hold any currency in the state Terminated. The following would generate the necessary verification tasks:

states =
| Created initial
| Confirmed
| Canceled
| Terminated with { i : balance = 0 }

This generates the following pre and post condition for all actions and transitions:

if state = Terminated then balance = 0

Effect specification

Before and after

When formalising action property, it is usually necessary to express that the value of a storage data after the execution of the action has a certain relation towards the same value before the execution.

Say for example the variable amount must increase due to the effect of action add_amount. The keyword before is used to refer to the variable value before the effect of the action. Hence this property is formalised:

before amount < amount

This property is placed in the specification section of the action:

variable amount int = 0
​
action add_amount = {
  specification {
    p : before amount < amount
  }
  effect {
    (* do something to increase amount *)
  }
}

For asset collection, archetype provides dedicated keywords to refer to added, removed and unmoved assets by action effect.

Say for example you want to express the only obsolete goods assets may have been removed by the action effect, that is asset with expiration date before now. This property is formalised:

forall x : removed goods, x.expiration < now

The schema below illustrates the three sets of assets resulting from the action effect:

Loop invariant

With imperative languages like archetype, iterations are done with loops. For formal verification purpose, it is necessary to provide loop invariant properties.

A loop invariant is a property which is true during iteration. More precisely, the invariant holds:

• at the beginning of the loop, when no object has been iterated yet (initialisation)

• at each step of the iteration (conservation)

• at the end of the iteration (terminaison)

  A loop invariant usually depends on the already iterated assets, or on the assets stil to iterate. Specific keywords are dedicated to these asset collections:

• toiterate refers to the assets stil to iterate on

• iterated refers to the assets already iterated

For example say you want to prove that the stock value is equal to 0 after iterating over the collection of goods. The loop invariant states that stock is upper-bounded by the sum of the quantity value over the goods assets stil to iterate. The following snippet illustrates how to declare this property as the loop invariant (line 15):

variable stock int = 0
​
asset goods identified by id= {
   id : string
   quantity : int
} with {
  a : stock = goods.sum(quantity)
}
​
action empty_stock = {
  specification {
    postcondition p = {
       stock = 0   (* this specifies that the effect of empty_stock is to
                      set 'stock' to zero *)
       invariant for goods_loop {
          i : 0 <= stock <= toiterate goods.sum(quantity)
       }
    }
  }
  effect {
    ... 
    for : goods_loop (g in goods) {
       ... (* decrease stock somehow *)
    }
    ...
  }
}

Note the invariant section for the loop labeled goods_loop at line 13.

At the end of the iteration, the toiterate collection is empty, and the loop invariant reduces to:

0 <= stock <= 0

which ensures post condition p (line 12). The loop invariant generates verification tasks on its own.

Assert

As in many languages, it is possible to insert assert instructions in the effect of actions and transitions.

The difference in archetype is that an assert instruction generates a verification task, which means that it is verified before the contract is deployed.

As such, an assert instruction does not generate any execution code.

Security predicates

In order to provide security guarantee to contract readers, it is usually useful to state which action may change an asset collection or a variable.

For example, the following specifies that only the action add_goods may add a goods asset:

only_in_action (add goods) add_goods

The following specifies that only the admin role can do any kind of storage data:

only_by_role anychange admin

The following specifies that the role owner does not change any data:

not_by_role anychange owner

Archetype provides the following predicates: