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.
To practice the formalisation of logical properties, you can solve online edukera formalisation exercises.
Five kinds of properties may be distinguished:
postcondition: a postcondition says something about the evolution of the storage data after the execution of an entry point
contract invariant: an invariant is a property about the contract storage that is true before and after any call to entry points (asset invariant are a special case of contract invariant)
loop invariant: a loop invariant is an invariant property applied to the body of a loop instruction: it says what stays true throughout the iteration process
exceptional property: an exceptional property says something about the storage data at failing point
assert: an assert property is a property local to an execution point; as such it may relate local execution variables to storage data
Postconditions
A contract entry may specify postconditions. A postcondition is typically a property about the relation between the contract's storage before and after the execution of the entry point.
Before and after
Say for example the variable amount must increase due to the effect of the entry add_amount. The keyword before is used to refer to the variable value before the effect of the action. Hence this property is formalized:
1
before.amount < amount
Copied!
This property is placed in the specification section of the entry:
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!
In why3, this will generate a verification task to verify that the value of amount value after executing add_amount is greater than the value of amount before.
For asset collection, archetype provides dedicated keywords to refer to added and removed assets by entry effect.
Say for example you want to express that only obsolete goods assets may have been removed by the action effect, where obsolete means with an expiration date is before now. This property is formalized:
1
forall x in removed.goods, x.expiration < now
Copied!
The schema below illustrates the three sets of assets resulting from the action effect:
action effect on asset collection
This property could typically serve as a postcondition of the function remove_obsolete:
1
​
2
entry remove_obsolete(){
3
specification {
4
p : forall x in removed.goods, x.expiration < now
5
}
6
effect {
7
/* effect to remove obsolete ... */
8
}
9
}
Copied!
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 that is true at any step of the iteration. More precisely, the invariant holds:
at the beginning of the loop, when no object has been iterated yet (initialization)
at each step of the iteration (conservation)
at the end of the iteration (terminaison)
A loop invariant usually depends on the iterated assets, or on the assets still to iterate. Specific keywords are dedicated to these views of asset:
toiterate refers to the assets still 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 {
4
id : string;
5
quantity : int;
6
}with{
7
inv : stock = goods.sum(quantity)
8
}
9
​
10
entry empty_stock(){
11
specification {
12
postcondition p {
13
/* the effect of empty_stock is to set 'stock' to zero */
14
stock =0
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 22.
At the end of the iteration, the toiterate view is empty, and the loop invariant reduces to:
1
0<= stock <=0
Copied!
which ensures the postcondition 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.
Invariants
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. Such a property is called an invariant.
Asset invariant
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!
State invariant
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
|Terminatedwith{ i : balance =0}
Copied!
This generates the following pre and post condition for all actions and transitions:
1
if state =Terminatedthen balance =0
Copied!
Variable invariant
Variables may also be equipped with invariants.
1
variable total : int =0with{
2
i1 :0<= variable <10
3
}
Copied!
The variable invariant may only refer to the variable itself. When dealing with multi-variables/assets properties, a contract invariant may be used.
Contract invariant
More complex contract invariants may be placed in the specification section at root level.
1
archetype acontract
2
​
3
entry main(){
4
/* ... */
5
}
6
​
7
specification {
8
p :/* forall ... */
9
}
Copied!
Assert
It is possible to specify a property in the effect section of an entry (or transition) with the assert instruction. An assert property is transcoded to a verification task in why3. As such, it does not generate any execution code.
Contrary to postconditions, asserts do have access to local variables in the same way as a standard instructions.
1
entry anentry(i : int){
2
specification {
3
assert a {
4
x > i
5
}
6
}
7
effect {
8
var x = i +1;
9
assert a;
10
}
11
}
Copied!
It is possible to refer to a variable at a specific step of execution by declaring a code label in the code.
1
entry anentry(i : int){
2
specification {
3
assert a {
4
at(s).x > x /* at(s).x is the value of x at label declaration (here i) */
5
}
6
}
7
effect {
8
var x = i;
9
label s;
10
x +=1;
11
assert a;
12
}
13
}
Copied!
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:
predicate
description
no_storage_fail (ACTION)
specifies that ACTIONcannot 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 onlyROLE
can perform CHANGE
only_in_action (CHANGE, ACTION)
specifies that onlyACTION
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