Postcondition

An entrypoint's postcondition says what the execution of the entrypoint changes in the contract storage when it does not fail.

Say the contract storage is made of S items (int, string, map, list, ...) and that the contract code is made of E entrypoints. There is S postconditions to describe the effect of one entrpoint on the S storage items, which is a total number of postconditions of E * S for the entire contract.

Basics#

Consider the basic contract with one storage item value and one entrypoint set:

archetype trivial
variable value : string = ""
entry set(v : string) { value := v }

There needs only one postcondition to describe the effect of the entrypoint on the storage:

specification entry set(v : string) {
postcondition p {
value = v
}
}

If the entrypoint can only be called by the owner address, the postcondition becomes:

caller = owner -> value = v

The form of the postcondition above is:

<CONDITION> -> <CHANGE>

which reads If CONDITION holds, then CHANGE occurs, or CONDITION implies CHANGE.

No change#

When an entrypoint does not change a storage item, it is stated with the following postcondition:

<ITEM> = before.<ITEM>

The prefix keyword before is used to refer to the state of the storage item ITEM before entrypoint execution. The storage item without prefix refers to the storage item after entrypoint execution.

For example, below is the postcondition for the entrypoint transfer of the FA 1.2 fungible token contract regarding the ledger storage item. It states that this storage item does not change if the parameter address %from is equal to the parameter address %to:

%from = %to -> ledger = before.ledger

Branches#

To be complete, the postcondition above must say what changes when %from is different from %to.

A general form of the postcondition is actually:

<CONDITION1> -> <CHANGE1> and
<CONDITION2> -> <CHANGE2> and
...
<CONDITIONn> -> <CHANGEn>

where conditions 1 to n are such that they cover all branches of execution. More formally, conditions are such that the following statement is true:

<CONDITION1> or <CONDITION2> or ... <CONDITIONn>

The postcondition for the tranfer entrypoint regarding the ledger item is then:

%from = %to -> ledger = before.ledger and
%from <> %to -> <CHANGE>

Note that it is equivalent either to declare one postcondition formed as the conjunction of n implication statements, or to declare n postconditions of the form of an implication:

postcondition p {
<CONDITION1> -> <CHANGE1> and <CONDITION2> -> <CHANGE2>
}

is equivalent to:

postcondition p1 {
<CONDITION1> -> <CHANGE1>
}
postcondition p2 {
<CONDITION2> -> <CHANGE2>
}

The later form is preferred since it attributes an id to each implication statement, making the output from the formal system in charge of proving them more explicit.

Collections#

This section deals with collections of pairs of key and value. Archetype provides 3 types of collections: Michelson map and big_map, and asset used in examples below.

Conversly to code language, retrieving an asset with key k from an asset collection c does not fail and the non existence is managed with the keyword otherwise:

let some a = c[k] in
<EXISTSk> (* there is an asset with key 'k' *)
otherwise
<NOTEXISTk> (* there is no asset with key 'k' *)

Identified object#

When an object a with known id k in a collection c is changed, the postcondition has the following structure:

let some a = c[k] in
let some ba = before.c[k] in
<CHANGE>
otherwise
<NOTEXISTkBEFORE>
otherwise
<NOTEXISTkAFTER>

where:

  • a is the object associated to k after entrypoint execution
  • ba is the object associated to k before execution
  • CHANGE is the change in object a statement
  • NOTEXISTkBEFORE is the statement when a does not exist before
  • NOTEXISTkAFTER is the statement when a does not exist after

For example, below is the postcondition p3_approve for the entrypoint approve of the FA 1.2 fungible token contract regarding the allowance asset with key (caller,spender). It corresponds to the addupdate code instruction.

let some a = allowance[(caller,spender)] in
let some ba = before.allowance[(caller,spender)] in
(* object is updated when object exists before *)
a = { ba with amount = value }
otherwise
(* object is added when it does not exist before *)
a = { addr_owner = caller; addr_spender = spender; amount = value }
otherwise
false

The false statement means there is a logical contradiction. In the case above, it is not possible that the object with key (caller,spender) does not exist, as it is the semantic of the addupdate instruction (see code above in 'entrypoint' tab).

The otherwise statements are presented below for instructions add, remove, update and addupdate:

let some a = c[k] in
let some ba = before.c[k] in
false (* add fails if key already exists *)
otherwise
a = <ADDEDOBJECT>
otherwise
false (* object should exist after *)

No change#

Postconditions say which objects are not changed with a statement of the following form:

forall a in c,
<NOTCHANGED> ->
let some ba = before.c[k] in
a = ba
otherwise
false

where CHANGED is the statement to say that object a is not a changed object.

When object with key k is the only object changed, the postcondition is:

forall a in c,
a.<KEY> <> k ->
let some ba = before.c[k] in
a = ba
otherwise
false

where KEY is the key field of the asset.

Unknown ids#

When changed objects are not known by their ids, but rather by a business rule based on object data, the goal is to state the effect of the change on the collection.

For example, below is the postcondition p2 for the entrypoint consume of the Miles contract. It states that the entrypoint reduces by parameter value quantity the total number of miles, which is the business intent of the entrypoint:

mile.sum(the.amount) = before.mile.sum(the.amount) - quantity

The total number of miles is obtained by summing the field amount because miles are stored per bunch associated to an expiration date.

Note that in this case, it is more complex to state exactly which miles are changed or not changed, as it is the result of an iteration process over a sorted and filtered set of miles.

It is interesting though to make sure that only not expired miles are consumed (removed), since it is another key functional element of the contract:

forall m in removed.mile, m.expiration > now

Note that Archetype specification language provides convenient handlers for removed or added assets. Another way to phrase this property is:

forall bm in before.mile,
let some m = mile[bm.id] in
false (* no mile is added by the entrypoint *)
otherwise
m.expiration > now