Scribble Functions

How to write User defined functions

User-defined scribble functions are useful to avoid repeating similar expressions in multiple annotations. They are defined in the docstring above a smart contract using annotations structured as shown below:

/// #define {:msg "Description of your function"}
///     funName(type1 arg1, type2 arg,...) returnType <single scribble expression>;

The above annotation defines a new user-defined function with name funName that takes several arguments (arg1 of type type1, arg2 of type type2, etc.), and has as its body a single valid Scribble expression (which is also its return value). That expression must be of type returnType.

Consider the following example. We can see that the operations (x + 10) and (x + 10) * delta are repeated multiple times in annotations.

contract ExampleContract {
    uint delta;
    function set_delta(uint _delta) public {
        delta = _delta;
    }
    /// #if_succeeds {:msg "P0"} y == (x + 10) * delta + 15;
    function example(uint x, uint y) public returns (uint result) {
        ...
    }

    /// #if_succeeds {:msg "P1"} y == (x + 10) * delta + x + 10;
    function example2(uint x, uint y) public returns (uint result) {
        ...
    }

}

We can avoid those repetitions by adding user defined functions for (x+10) and (x+10) * delta above the smart contract. These functions can then be called by annotations inside the contract.

/// #define add10(uint x) uint = x + 10;
/// #define add10_times_delta(uint y) uint = add10(y) * delta;
contract ExampleContract {
    uint delta;
    function set_delta(uint _delta) public {
        delta = _delta;
    }
    /// #if_succeeds {:msg "P0"} y == add10_times_delta(x) + 15;
    function example(uint x, uint y) public returns (uint result) {
        ...
    }

    /// #if_succeeds {:msg "P1"} y == add10_times_delta(x) + add10(x);
    function example2(uint x, uint y) public returns (uint result) {
        ...
    }

}

In summary there are several important functions to remember about scribble user-defined functions:

1. They are defined in the docstring above a smart contract

2. They can be used by any annotation inside that contract, or in all inheriting contracts

3. Scribble user defined functions must be view or pure functions. I.e. they cannot modify any state, but can still access the state variables as shown in the above example.

4. The body of a user-defined function consists of a single valid Scribble expression, which is also the return value of the function

User defined functions can also be used by all inheriting contracts.