Quantification

Quantification allows us to talk about all values in a set

Universal Quantification

Syntax:

forall (<type> <id> in <expression>...<expression>) <expression>

forall (<type> <id> in <expression>) <expression>

Universal quantifiers are powerful expressions that allow users to talk about all values that fit a criteria. Scribble supports 2 types of universal quantifiers - quantifiers over numeric ranges and quantifiers over arrays and maps.

Numeric ranges

Quantifiers can talk about properties that hold over all numbers in a given range. The syntax for such quantifiers is forall(<type> <id> in <expression>...<expression>) <expression>.

The start expression is inclusive, while the end range expression is exclusive.

The most common use-case of quantification over numeric ranges is describing all indices of an array (see below example).

Example 1: Forall over arrays

In the below example we check that the array arr is sorted.

/// #invariant forall(uint i in 0...arr.length-1) arr[i] < arr[i+1];
contract Token {
   uint[] arr;
   ...
}

Note that the type of the quantifier variable (uint i in the above example) must always be a numeric type, and it must be able to fit both the start and end expressions. So for example you can't write: forall (int8 i in 0...arr.length-1) ... in the above example instead, since int8 is too small of a type to store the array length (which is uint256).

Arrays/maps

The second flavor of universal quantifiers talks about all indices in an array or keys in a map. The syntax is forall (<type> <id> in <expression>) <expression>.

Example 1: Forall over arrays

In the below example, we check that each stakeholder has a positive stake

/// #invariant
///   forall(uint i in stakeHolders) stakes[stakeHolders[i]] > 0;
contract Token {
   address[] stakeHolders;
   mapping(uint=>uint) stakes;
}

Example 2: Forall over maps

In the below example, the mapping authorized is a mapping from account addresses to operators addresses, authorized to act on behalf of the given account. The property below states that for no account is the 0x0 address authorized to act on their behalf.

/// #invariant
///   forall(address acct in authorized) authorized[acct] != address(0);
contract Token {
   mapping(address=>address) authorized;
}

Any forall over arrays can be equivalently expressed as a forall over numeric ranges. I.e.forall(<type> i in arr) <expr> is equivalent to forall(uint i in 0...arr.length) <expr>

Note that in Solidity maps are technically defined over their complete input range (i.e. a mapping(uint=>uint) is defined for all uint256s, just its 0 for most of them). Due to this, when we say that we "quantify over all keys in a map", we mean all keys that have: 1. Been set explicitly at least once 2. Have not been deleted with the delete keyword.

To support this, under the hood we re-write all annotated maps with our custom data type that track key insertion and deletions.

The delete operation is equivalent to zeroing out a value. However, we do not treat them equivalently. Given a map m, when you do delete m[x] , we will remove x from the keys that we store in m . However, if you do m[x] = 0 we will not remove x from the keys we store in m.

You can nest forall statements arbitrarily. For example, we can extend the example above to store a list of authorized users for a given address and require that none of the authorized users is 0x0:

Authorized Users 2

In the below example, the mapping authorizedUsers stores a list of addresses of operators authorized to act on behalf of a given address. The property below states that the 0x0 address is not authorized to act on anyone's behalf.

/// #invariant
///    forall(address acct in authorized)
///       forall(uint i in authorized[acct])
///             authorized[acct][i] != address(0);
contract Token {
   mapping(address=>address[]) authorized;
}