Scribble

Searchâ€¦

Quantification

Quantification allows us to talk about all values in a set

Universal Quantification

`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>`

. That 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.1

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

2

contract Token {

3

uint[] arr;

4

...

5

}

Copied!

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 flavour of universal quantifiers talks about all elements of an array or keys in a map. The syntax is

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

.Example 1: Forall over arrays

Example 2: Forall over maps

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

1

/// #invariant

2

/// forall(address addr in stakeHolders) stakes[addr] > 0;

3

contract Token {

4

address[] stakeHolders;

5

mapping(uint=>uint) stakes;

6

}

Copied!

In the below example, the mapping

`authorized`

stores address of operators authorized to act on behalf of a given address. The property below states that for no user is the `0x0`

address authorized to act on their behalf.1

/// #invariant

2

/// forall(address addr in authorized) authorized[addr] != address(0);

3

contract Token {

4

mapping(address=>address) authorized;

5

}

Copied!

Any

`forall`

over arrays can be equivalently expressed as a `forall`

over numeric ranges.
I.e.`forall(<type> x in arr) <expr>`

is equivalent to `forall(uint i in 0...arr.length) let x:= arr[i] in <expr>`

Note that in Solidity maps are technically defined over their complete input range (i.e. a

`mapping(uint=>uint)`

is defined for all `uint256`

s, 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 **not **remove x from the keys we store in

`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 `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.1

/// #invariant

2

/// forall(address addr in authorized)

3

/// forall(address authAddr in authorized[addr])

4

/// authAddr != address(0);

5

contract Token {

6

mapping(address=>address[]) authorized;

7

}

Copied!

Last modified 5mo ago

Copy link