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>. 
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
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 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
Example 1: Forall over arrays
In the below example, we check that each stakeholder has a positive stake
/// #invariant
///   forall(address addr in stakeHolders) stakes[addr] > 0;
contract Token {
   address[] stakeHolders;
   mapping(uint=>uint) stakes;
}
Example 2: Forall over maps
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.
/// #invariant
///   forall(address addr in authorized) authorized[addr] != 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> 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 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
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 addr in authorized)
///       forall(address authAddr in authorized[addr])
///             authAddr != address(0);
contract Token {
   mapping(address=>address[]) authorized;
}
Language - Previous
Expressions
Next - Tutorials
Property Checking with Scribble and MythX
Last updated 2 months ago