Contract specification

Search…
Formalise contract properties
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:
1
forall b in bid, b.value <= max_bid
Copied!
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:
1
variable max_bid : tez = 0tz
2
​
3
action declare_winner () {
4
  specification {
5
     p : forall b in bid, b.value <= max_bid;
6
  }
7
  effect {
8
     max_bid := ... (* code to compute max_bid *)
9
  }
10
}
Copied!
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.
To practice formalisation of logical properties, you can solve online edukera formalisation exercises.
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:
1
asset mile identified by id {
2
   id : string;
3
   quantity : int;
4
} with { 
5
  i : quantity > 0;
6
}
Copied!
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):
1
forall x in mile, x.quantity > 0
Copied!
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:
1
states =
2
| Created initial
3
| Confirmed
4
| Canceled
5
| Terminated with { i : balance = 0 }
Copied!
This generates the following pre and post condition for all actions and transitions:
1
if state = Terminated then balance = 0
Copied!
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:
1
before.amount < amount
Copied!
This property is placed in the specification section of the action:
1
variable amount : int = 0
2
​
3
action add_amount () {
4
  specification {
5
    p : before.amount < amount
6
  }
7
  effect {
8
    (* do something to increase amount *)
9
  }
10
}
Copied!
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:
1
forall x in goods.removed, x.expiration < now
Copied!
The schema below illustrates the three sets of assets resulting from the action effect:
action effect on asset collection
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):
1
variable stock : int = 0
2
​
3
asset goods identified by id {
4
   id : string;
5
   quantity : int;
6
} with {
7
  a : stock = goods.sum(quantity)
8
}
9
​
10
action empty_stock () {
11
  specification {
12
    postcondition p {
13
       stock = 0   (* this specifies that the effect of empty_stock is to
14
                      set 'stock' to zero *)
15
       invariant for goods_loop {
16
          0 <= stock <= toiterate goods.sum(quantity)
17
       }
18
    }
19
  }
20
  effect {
21
    ... 
22
    for : goods_loop g in goods do
23
       ... (* decrease stock somehow *)
24
    done
25
    ...
26
  }
27
}
Copied!
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:
1
0 <= stock <= 0
Copied!
which ensures post condition p (line 12). The loop invariant generates verification tasks on its own.
Loop invariants may refer to local variables declared in the effect section.
Archetype ensures iteration terminaison by design.
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:
1
only_in_action (add goods, add_goods)
Copied!
The following specifies that only the admin role can do any kind of storage data:
1
only_by_role (anychange, admin)
Copied!
The following specifies that the role owner does not change any data:
1
not_by_role (anychange, owner)
Copied!
Archetype provides the following predicates:
no_storage_fail (ACTION)
specifies that ACTION cannot logically fail
on storage access (key not found when
reading and setting, and key already
present when adding an asset)
only_by_role (CHANGE, ROLE)
specifies that only ROLE can perform CHANGE
only_in_action (CHANGE, ACTION)
specifies that only ACTION can perform CHANGE
only_by_role_in_action (CHANGE, ROLE, ACTION)
specifies that only ROLE can perform CHANGE in ACTION
not_by_role (CHANGE, ROLE)
specifies that ROLE can not performCHANGE
not_in_action (CHANGE, ACTION)
specifies that ACTION can not perform CHANGE
not_by_role_in_action (CHANGE, ROLE, ACTION)
specifies that ROLE can not perform CHANGE in ACTION
ROLE
CHANGE
ACTION
a variable typed role
a list of ROLE separated by or
add ASSET
remove ASSET
update (ASSET FIELD | VARIABLE)
a list of above CHANGE separated by or
transfers
transfer to ROLE
anychange
anychange but ACTION
nochange
a contract action name
a list of ACTION separated by or
anyaction
anyaction but ACTION
noaction
Metadata (TZIP-16)
Next - Contract library
Governance
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub
Contents