We are excited to announce that a verified implementation of the FA1.2 contract is available.
The documentation is available on the assets.tqtezos.com site.
This article provides more information about the verification process, including the design of the FA1.2 properties.
FA1.2 Implementation
Previously, we gave an overview of the FA12 implementation with the Archetype language, a high-level domain-specific language dedicated to the development of verified smart contracts for the Tezos blockchain.
The main change in the current version is the use of getter declarations to implement the getTotalSupply getBalance and getAllowance entry points.
getter getAllowance (owner : address, spender : address) : nat {
return (allowance[(owner, spender)].amount)
}
getter getBalance (owner : address) : nat {
return (ledger[owner].tokens)
}
getter getTotalSupply () : nat {
return totalsupply
}
Other contracts may call these entries to get data from the contract. It is syntax sugar and is equivalent to the former implementation. More information may be found in this article.
The specification is now declared separately from the implementation. An entry point specification is declared with the following syntax:
specification entry getAllowance (owner : address, spender : address) : nat {
postcondition p1 {
// ...
}
}
Michelson Generation
Archetype now provides its own Michelson generator (since version 1.2.0).
An example instance of the FA1.2 Archetype contract is available at the following address:
KT1DvC4vS8hykGRCmoqGnnk1RV2wfFyp3BDv
The origination cost is 2.5ꜩ.
Formal properties
Formal properties are made of two types of properties, contract invariant and entry postcondition:
- a contract invariant is a property that is true regardless of the state of the contract storage or balance.
- an entry postcondition says something about the effect of the execution on the contract storage, balance, and generated operations; it therefore usually compares the states of the contract before and after execution.
One contract invariant is declared in the FA1.2 specification.
The effect of an entry point on the contract storage must be described for each storage asset and variable.
The storage of the FA12 is made of two assets, ledger and allowance. Postconditions must therefore describe the evolution of each asset collection, operations, and must describe situations of explicit failure.
An entry point without any effect on the environment (storage, operations) would have the following specification:
specification entry noeffect () {
postcondition noeffect_p1 {
ledger = before.ledger // no effect on ledger assets
}
postcondition noeffect_p2 {
allowance = before.allowance // no effect on allowance assets
}
postcondition noeffect_p3 {
length (operations) = 0 // no operation generated
}
}
The before prefix on asset collection refers to the state of the asset collection before the entry point execution.
Asset update
The transfer entry point decreases the number of tokens of the %from address. This property is formulated as follows:
%from <> %to ->
let some before_ledger_from = before.ledger[%from] in
let some after_ledger_from = ledger[%from] in
after_ledger_from = { before_ledger_from with
tokens = (before_ledger_from.tokens - value)
}
otherwise false
otherwise false
It reads: if %from is different from %to then the %from token holder after execution is equal to the %from token holder before execution except for the tokens field which is decreased by value.
The let some ... in ... otherwise ... declaration is necessary because the [ ] operator on asset collection returns an option of asset; the otherwise branch is used to state property when the asset does not exist.
The property false is stated to describe a contradiction, that is an impossible situation: indeed postconditions apply when the entry point does not fail.
The transfer entry fails when the %from token holder is not found in ledger, therefore the second false; and when it exists before execution, it must exist after execution (there is no remove instruction in the entry’s code).
When %from is equal to %to, the ledger is unchanged; this property is formulated as:
%from = %to -> ledger = before.ledger
Unchanged records
It is also necessary to state that in any case, token holders different from %from and %to are unchanged. This property is formulated as:
forall tokenholder in ledger,
tokenholder.holder <> %from ->
tokenholder.holder <> %to ->
before.ledger[tokenholder.holder] = some(tokenholder)
it reads: for every token holder in the ledger collection after execution, if it is different from %from, if it is different from %to, then it is equal to this token holder before execution.
Fails
When the entry may explicitly fail, that is when it uses the fail instruction, it is possible to describe the conditions for failure, that is all conditions that lead to failure.
Then transfer entry fails when the number of tokens of the %from address is not enough, that is lower than value:
fails with (msg : string) :
let some after_ledger_from = ledger[%from] in
msg = "NotEnoughBalance" and
after_ledger_from.tokens < value
otherwise true
Check out the approve failure conditions.
Verification
Archetype transcodes the contract (execution and specification) to the Why3 language. Why3 is a generic platform for program verification.
The generated Why3 source is made of two modules:
- the
Fa12module is the transcoded contract itself - the
Fa12_storagemodule provides the contract storage definition with asset collection types
The two asset collection types are obtained by cloning the polymorphic collection type in Archetype theory.
The Fa12 module is verified in about 30 seconds by SMT solvers. It consists of 108 proof obligations generated by Why3 divided as follows:
| Entry | Nb. proof obligations |
|---|---|
| transfer | 63 |
| approve | 36 |
| getTotalSupply | 3 |
| getBalance | 3 |
| getAllowance | 3 |
the Fa12_storage module provides the theory that is used to prove the contract specification. This theory must be verified to have the highest level of confidence in the verification process.
106 proof obligations are generated for the Fa12_storage module. Currently, only 61 of them are verified, and we are working on verifying the rest of them.
