Expressions

How to write Scribble expressions

Scribble properties usually consist of three elements:

/// <specification_type> <msg> <condition>

Example:

/// #if_succeeds {:msg "This is an example"} a == 1;

The condition is an expression that evaluates to a boolean (True / False). For the most part, you use the same syntax here as in regular Solidity expressions. But, we have added some special functions and operators that make property writing that much easier.

Solidity

You write Scribble expressions in exactly the same way that you would write normal solidity expressions.

  1. Numbers, booleans and addresses

  2. State variables

  3. Function arguments and return values

  4. Member accesses (e.g. a.foo where a is a struct)

  5. Index accesses (e.g. a[5] where a is an array)

  6. Unary operations like - and !

  7. Binary opreations: +, -, *, /, %, **, <<, >>, |, &, ^, <, <=, >, >=, ==, !=, &&, ||

  8. Ternary operators (e.g. x < y ? x : y)

As of Solidity 0.8.0 all arithmetic is checked by default - that is an exception is thrown (i.e. your code reverts) whenver an overflow or underflow happens. Scribble arithmetic on the other hand is unchecked - that is overflows/underflows would happen silently, without a revert. This is on purpose, as we want to minimize the conditions under which an exception would originate from the instrumentation. However this requires users to be mindful of whether overflow may happen in arithmetic inside properties.

Changing State

Some Solidity expressions can change the state of a smart contract (e.g. i++ updates the value of i). This is something that we want to avoid doing in a specification language.

The reason? Scribble annotations are about the smart contract, they shouldn't actually change the contract. If we're altering how a smart contract works with our properties, then we're not testing / verifying the original contract anymore.

Pure and View

Scribble only allows function calls to pure and view functions.

Functions that are not pure or view can accidentally change the contract as we're checking properties. As a result, the properties calling into them could also result in changes.

Updating Expressions

Some expressions directly update a variable (e.g. i++), these are not allowed by Scribble.

Scribble Language Features

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.

In short, you use old( expression ) to get the value of expression as it was at the beginning of a transaction.

Example 1: Constant
Example 2: Ownership
Example 3: Expression
Example 1: Constant

The balance of the sender before a transaction is equal to the balance after.

Scribble:

old(balance[mgs.sender]) == balance[msg.sender]
Example 2: Ownership

The old owner is not the new owner

Scribble:

old(owner) != owner
Example 3: Expression

The sum of balances between the sender and receiver is the same before and after a transaction.

You can put any expression in old(...), not just single variables.

old(balance[sender] + balance[receiver]) == balance[sender] + balance[receiver]

Binding return values

let <variable> := <expression> in <expression>

Function return values
Binding constants
Multiple lets
Function return values

In this example we assume there is a function unpack() that returns three values: amount, sender and receiver.

In this example, we'll write a property that only uses one of the variables (the amount) and checks that it is bigger than zero.

If you don't use a variable replace it with `_` to make your property easy to read.

let amount, sender, _ := unpack(packedTransaction) in amout >= 0;
Binding constants

You are not limited to binding function return values.

Take the following expression for example, this evaluates to 25.

let x := 5 in x * x
Multiple lets

Sometimes you might need multiple let bindings.

In the following example we first bind the balance variable, and then we use it to compute and bind halfBalance. Which we end up using to check halfBalance >= amount.

Both balance and halfBalance can be used in the final expression!

/// if_succeeds {:msg "You can only extract half of the current balance in one time"}
/// let balance = token.balanceOf(this) in
/// let halfBalance = balance / 2 in
/// halfBalance >= amount;
function extractFunds(uint amount) public returns (bool) {
...
}

Let-bindings and `old()` expressions

Sometimes you may want to use the let- binding variable inside of an old() expression in the body of the let, as in the contrived example below:

contract Foo {
uint x;
/// #if_succeeds let t:= x in old(t+1) > 10;
function foo() public {
...
}
}

However running the above code through scribble would result in the following error:

tmp.sol:5:5 TypeError: Variable t is defined in the new context in (let t := x in (old((t + 1)) > 10)) but used in an old() expression
In:
if_succeeds let t:= x in old(t+1) > 10;

The issue we are running into is, that the expression that t is bound to is implicitly computed after the original function was called, but we are attempting to use it in a computation that is executed before the original function was called. Since doing this requires time travel, we obviously cannot make it happen. The fix in such a scenario is to wrap the expression that t is bound to in an old() expression like so:

/// #if_succeeds let t:= old(x) in old(t+1) > 10;
function foo() public {
...
}

If that doesn't fix our problem, then we should re-think the property we are trying to express.

Implication

<expression> ==> <expression>

In our annotations, we'll often use implications to specify some kind of conditional logic ( behaviours 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.

Fun Fact: A ==> B is equivalent to (B || !A)

Example 1: Simple implication
Example 2: Ownership
Example 1: Simple implication

If the input to a function is negative, then the output is as well.

/// #if_succeeds {:msg "negativity"} input < 0 ==> output < 0;
function convert(uint input) public returns (uint output) { ... }
Example 2: Ownership

If there is a change to the owner variable, then the sender was the old owner.

owner != old(owner) ==> msg.sender == old(owner)

Unchecked sum

unchecked_sum(<expression>)

Sometimes a property wants to talk about the sum of 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.

Example 1: Token balances
Example 2: Constant Supply
Example 1: Token balances

This example uses sum() to ensure that the sum of balances is equal to the mintedTokens variable.

/// #invariant unchecked_sum(balances) == mintedTokens;
contract Token {
uint mintedTokens;
mapping(address=>uint) balances;
...
}
Example 2: Constant Supply

Here you can see how we use sum to make sure no new tokens get minted.

/// #if_succeeds old(unchecked_sum(balances)) == unchecked_sum(balances);
contract Token {
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.

Speaking of overflow, as the name unchecked_sum suggests, the computation of the sum is UNCHECKED and thus may overflow silently. It is up to the user to add additional invariants to ensure that the sum of entries in an array doesn't overflow. In the future we may add a checked version of the sum, that fails loudly when the summation overflows.