forall (<type> <id> in <expression>...<expression>) <expression>
forall (<type> <id> in <expression>) <expression>
forall(<type> <id> in <expression>...<expression>) <expression>
. arr
is sorted.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
).forall (<type> <id> in <expression>) <expression>
.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.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>
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.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
.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
: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.