All scribble 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.

There are 2 types of properties supported currently:

1. if_succeeds properties are specified only before functions. They specify conditions that must hold if the function returns successfully

2. invariant properties are specified only before contracts. They specify conditions that must hold whenever we are NOT executing code in the contract.

All properties allow adding a human-readable message using {:msg "message"}. This is helpful when mapping the properties to their description in other documents, or just as a reminder about the intent of a complex property.

The expressions that are allowed in custom properties are mostly a subset of Solidity expressions, with some additional syntactic sugar described below.

We will first outline some small differences between if_succeeds and invariant expressions, and then describe in-depth the allowed expressions.

Examples

Lets look at several examples.

Using old

In the below contract inc increments the variable of the state var x by 1. The property x == old(x) + 1 captures exactly the same intuition.

contract Foo {
    int x = 1;
    /// #if_succeeds {:msg "P0"} x == old(x) + 1;
    function inc() public {
        x = x + 1;
    }
}

Note that we can also write that property as x == old(x + 1) since the value of the constant 1 doesn't change before and after the function.

Incrementing contract

For the contract from the previous example we can also add a contract invariant stating that x >= 1 as shown below:

/// #invariant {:msg "P1"} x >= 1;
contract Foo {
    int x = 1;
    /// #if_succeeds {:msg "P0"} x == old(x) + 1;
    function inc() public {
        x = x + 1;
    }
}

Expressing pre/post conditions using implication

In verification people often think of function pre- and post- conditions (these come from Hoare logic). One can encode a precondition P and post-condition Q as: P ==> Q. So for example for the sillyDiv function below, we can express a pre-condition (y != 0) and post-condition (z == x/y) as y!=0 ==> z == x/y.

contract Div {
    /// #if_succeeds {:msg "P0"} y != 0 ==> z == x / y;
    function sillyDiv(uint x, uint y) public returns (uint z) {
        return y != 0 ? x/y : 0;
    }
}

Note that this specification is incomplete - it doesn't say what happens when y == 0. We can make it complete by adding another property:

contract Div {
    /// #if_succeeds {:msg "P0"} y != 0 ==> z == x / y;
    /// #if_succeeds {:msg "P0"} y == 0 ==> z == 0;
    function sillyDiv(uint x, uint y) public returns (uint z) {
        return y != 0 ? x/y : 0;
    }
}

Multiple if_succeeds annotations for the same functions are conjoined together. The same holds for multiple invariant annotations for a contract.