forall (<type> <id> in <expression>...<expression>) <expression>
forall (<type> <id> in <expression>) <expression>
forall(<type> <id> in <expression>...<expression>) <expression>.
uint iin 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
int8is too small of a type to store the array length (which is
forall (<type> <id> in <expression>) <expression>.
authorizedis 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
0x0address authorized to act on their behalf.
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
forallstatements 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
authorizedUsersstores a list of addresses of operators authorized to act on behalf of a given address. The property below states that the
0x0address is not authorized to act on anyone's behalf.