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:

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.

We are aware that this will make it difficult or impossible to express certain properties. We encourage users to reach out if they encounter such properties. However, it is not our itention to support every property imaginable. We consider it a great success if our specification language is able to capture 95% of the properties that users want to express.
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:

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:

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)).

Some Solidity expressions can change the state of a smart contract (e.g. i++ and (somewhat surprisingly) i=1 are both expressions modifying state in Solidity) . In our specification language we forbid such expressions, as we don't want annotations to change state in any way.
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:

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:

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:

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:

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:

/// #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:

/// #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:

/// #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.