Formal Verification
Introduction
The design of our specification language takes
inspiration from the
Scribble specification language
and
we expect the language to evolve gradually as we gain more experience in using it.
We rely on the following principles and design goals to guide language evolution:
All properties are expressed as specially formatted docstrings. For example:
- Specifications are easy to understand by developers and auditors.
- Specifications are simple to reason about.
- Specifications can be efficiently checked using off-the-shelf analysis tools.
- A small number of core specification constructs are sufficient to express and
reason about more advanced constructs.
All properties are expressed as specially formatted docstrings. For example:
contract Foo {
/// #if_succeeds {:msg "P0"} y == x + 1;
function foo(uint256 x) public returns (uint256 y) {
return x + 1;
}
}
In the above sample
if_succeeds {:msg "P0"} y == x + 1;
is the property. Note the semicolon at the end - it is required for all properties.
Annotations
In our specification language you can formalise properties
by writing annotations for contracts, state variables and functions.
All annotations appear in docstrings, and begin with the pound sign # followed by a specific keyword. There are several different kinds of annotations at your disposal:
All annotations appear in docstrings, and begin with the pound sign # followed by a specific keyword. There are several different kinds of annotations at your disposal:
If you place an annotation in a normal comment (/* */ or //), instead of a docstring comment (/** **/ or ///) it will be ignored!
Note that if you forget the pound sign (#) your annotation will also be ignored! We will issue a warning in most cases when this happens.
Function Annotations
Function annotations are what you can use to describe
how a function should behave. You'll commonly use them to ensure that
the function has the right side-effects, and that the return values are
correct. For example:
/// #if_succeeds $result > 0;
function positiveNumber() external returns (uint) {
...
}
State Variable Annotations
State variable annotations allow you to describe properties
that should hold for a particular variable whenver its updated. For example,
you might specify that a variable can only change under particular circumstances:
contract Example {
/// #if_updated msg.sender == owner || owner == address(0);
address owner;
}
Contract Annotations
Contract annotations allow you to describe properties
that concern multiple variables and functions. The most common contract
annotation will be an invariant, which is used to describe properties
that hold before and after each transaction. For example:
/// #invariant sum(balances) == totalSupply;
contract Token {
...
}
Assert Annotations
Assert annotations allow users to insert an annotation
in the middle of a function, before a specific statement. They can refer
to any local variable in scope. For example:
contract Example {
mapping(address=>uint) balances;
function setBalances(address memory[] addrs, uint[] memory amounts) public {
for (uint i = 0; i < addrs.length; i++) {
/// #assert amounts[i] > 0;
balances[addrs[i]] = amounts[i];
}
}
}
Expressions
Property annotations usually consist of three elements:
/// <property_type> <msg> <condition>
For example:
/// #if_succeeds {:msg "This is an example"} a == 1;
The property type is one of several expected keywords
(if_succeeds, invariant, if_updated, assert). The <msg> part defines
a human readable label for the property. It is either in the format
{:msg "The label"} or just the short-hand "The label".
Simple Expressions
You can use the following standard Solidity expressions in expressions:
For the same reason, while our specification language allows function calls, it only allows calls to pure and view functions.
- Numbers, boolean litearls and addresse literals.
- Identifiers naming state variables and function arguments and return values.
- Member accesses (e.g. a.foo where a is a struct).
- Index accesses (e.g. a[5] where a is an array or a map).
- Unary operators : - and !.
- Binary operators : +, -, *, /, %, **, <<, >>, |, &, ^, <, ≤, >, ≥, ==, !=, &&, ||.
- Ternary operators (e.g. x < y ? x : y).
- Function calls (e.g. foo(1,true, x)).
For the same reason, while our specification language allows function calls, it only allows calls to pure and view functions.
Previously Operator
previously(formula) refers to the previous value of formula.
That is, the operator returns the formula’s value in the state prior to the transaction.
Note that in the block where the contract is deployed, previously(formula) equals formula,
since there is no prior block where formula is defined.
For example:
For example:
contract A {
uint a = 0;
function foo() public {
a = a + 1;
}
}
Expression | T0 | T1 | T2 | T3 | T4 | T5 |
---|---|---|---|---|---|---|
previously(a >= 2) | F | F | F | T | T | T |
Since Operator
since(p, q) is interpreted as "in the transaction sequence executed,
q was true at least once, and since then p was always true".
For example:
For example:
contract A {
uint a = 0;
function foo() public {
a = a + 1;
}
}
Expression | T0 | T1 | T2 | T3 | T4 | T5 |
---|---|---|---|---|---|---|
since(a > 0, a == 1) | T | T | F | F | F | F |
Always Operator
always(formula) is true if formula holds in the current state
and all previous states.
For example:
For example:
contract A {
uint a = 0;
function foo() public {
a = a + 1;
}
}
Expression | T0 | T1 | T2 | T3 | T4 | T5 |
---|---|---|---|---|---|---|
always(a < 3) | T | T | T | F | F | F |
Once Operator
once(formula) is true if formula holds in the current state or any previous states.
For example:
For example:
contract A {
uint a = 0;
function foo() public {
a = a + 1;
}
}
Expression | T0 | T1 | T2 | T3 | T4 | T5 |
---|---|---|---|---|---|---|
once(a == 4) | F | F | F | F | T | T |
Referring to the Previous State
syntax: old( <expression> )
You can't use old() in invariants!
When writing properties, you'll often want to describe how state is
expected to change. For example, you might expect some persons balance to increase.
To write these properties, you'll be able to use the old() construct.
You can talk about state changing only in if_succeds and if_updated invariants. In the case of if_succeeds invariants old(expression) refers to the value of the expression before the function began executing. In the case of if_updated old(expression) refers to the value of the expression before the annotated variable was updated.
For example:
You can talk about state changing only in if_succeds and if_updated invariants. In the case of if_succeeds invariants old(expression) refers to the value of the expression before the function began executing. In the case of if_updated old(expression) refers to the value of the expression before the annotated variable was updated.
For example:
/// #if_succeeds {:msg "The balance of the sender before a transaction is equal to the balance after."} old(balance[mgs.sender]) == balance[msg.sender];
Note that the type of the expression inside old(expression)
can be any primitive value type - e.g. number, fixed bytes, address, boolean, etc.
However we disallow reference types such as arrays, maps, structs, strings and bytes.
This is done to limit the overhead of our instrumentation, since making a copy of such
(usually dynamically sized) types may require loops.
Implication
syntax: <expression> ==> <expression>
In our annotations, we'll often use implications to specify some
kind of conditional logic.
An implication like A ==> B describes that B must be true if A is true. If A isn't true, then it doesn't matter whether B is true or false. In natural language, you can usually describe an implication as: If A, then also B.
For example:
An implication like A ==> B describes that B must be true if A is true. If A isn't true, then it doesn't matter whether B is true or false. In natural language, you can usually describe an implication as: If A, then also B.
For example:
/// #if_succeeds {:msg "If the input to a function is negative, then the output is as well."} input < 0 ==> output < 0;
function convert(uint input) public returns (uint output) { ... }
Unchecked Sum
syntax: unchecked_sum( <expression> )
Sometimes a property wants to talk about the sum of numeric values
in an array or a map. For such cases we have introduced the unchecked_sum() builtin function.
You can apply it to both numeric maps and arrays.
For example:
For example:
/// #invariant {:msg "The sum of balances is equal to the mintedTokens variable."} unchecked_sum(balances) == mintedTokens;
contract Token {
uint mintedTokens;
mapping(address=>uint) balances;
...
}
The return type for unchecked_sum() is always either uint256 or int256
(depending on whether the underlying map/array is signed). While it may seem confusing
that unchecked_sum(arr) is int256 even if arr itself is int8, this was done on purpose,
to minimize the chance of overflow when working with small integer types.
Updated 12 months ago