Introduction

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 several kinds of Scribble annotations.

Property Annotations

Property annotations directly correspond to specific properties the user wants to check. There are 4 types of properties supported currently:

1. if_succeeds properties are usually specified before functions. They specify conditions that must hold if the function returns successfully. (if_succeeds can also be specified on contracts. For more details on their semantics see this section).

2. invariant properties are specified only before contracts. They specify conditions that must hold whenever we are NOT executing code in the contract (more info in this section).

3. if_updated properties are specified only before state variables. They specify conditions that must be checked whenever we are updating the value of a state variable (or some of part of the state variable in the case of complex data structures such as arrays, structs and maps). More info in this section.

4. assert properties are specified before a statement in the body of the function. They specify a condition that must be checked inline before the target statement, and can refer to any local variable in scope for the target statement. For more details see this section.

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.

Since its tedious to write {:msg "some message"} you can also just write "some message" as shorthand. So for example the below is a valid annotation:

/// #if_succeeds "x increases" x > old(x);

The expressions that are allowed in custom properties are mostly a subset of the pure Solidity expressions, with some additional syntactic sugar. For more details see this section.

Utility Annotations

Utility annotations are helpers that make writing property annotations easier. We currently support:

1. Scribble user-defined functions - helpful for defining commonly used predicates and reducing code duplication
2. Scribble macro annotations allow automatically annotating a contract with a whole set of predefined annotations (from a macro definition)
3. Backend tool hints (#try and #require) - annotations providing guidance to backend tools

Examples

To give you a quick intro to scribble annotations lets look at two small examples uinsg the #if_succeeds annotation.

Using old

In the below contract the function inc increments the value of the state variable x by 1. The property x == old(x) + 1 captures exactly this behavior.

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.