# 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).

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

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 {
mapping(uint=>uint) stakes;
}``````

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

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