import "helpers/helpers.spec"
methods {
// library
set(bytes32,bytes32) returns (bool) envfree
remove(bytes32) returns (bool) envfree
contains(bytes32) returns (bool) envfree
length() returns (uint256) envfree
key_at(uint256) returns (bytes32) envfree
value_at(uint256) returns (bytes32) envfree
tryGet_contains(bytes32) returns (bool) envfree
tryGet_value(bytes32) returns (bytes32) envfree
get(bytes32) returns (bytes32) envfree
// FV
_indexOf(bytes32) returns (uint256) envfree
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helpers │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
function sanity() returns bool {
return length() < max_uint256;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: the value mapping is empty for keys that are not in the EnumerableMap. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant noValueIfNotContained(bytes32 key)
!contains(key) => tryGet_value(key) == 0
{
preserved set(bytes32 otherKey, bytes32 someValue) {
require sanity();
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: All indexed keys are contained │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant indexedContained(uint256 index)
index < length() => contains(key_at(index))
{
preserved {
requireInvariant consistencyIndex(index);
requireInvariant consistencyIndex(to_uint256(length() - 1));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: A value can only be stored at a single location │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant atUniqueness(uint256 index1, uint256 index2)
index1 == index2 <=> key_at(index1) == key_at(index2)
{
preserved remove(bytes32 key) {
requireInvariant atUniqueness(index1, to_uint256(length() - 1));
requireInvariant atUniqueness(index2, to_uint256(length() - 1));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: index <> value relationship is consistent │
│ │
│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another. │
│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are set │
│ and removed from the EnumerableMap). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant consistencyIndex(uint256 index)
index < length() => _indexOf(key_at(index)) == index + 1
{
preserved remove(bytes32 key) {
requireInvariant consistencyIndex(to_uint256(length() - 1));
}
}
invariant consistencyKey(bytes32 key)
contains(key) => (
_indexOf(key) > 0 &&
_indexOf(key) <= length() &&
key_at(to_uint256(_indexOf(key) - 1)) == key
)
{
preserved remove(bytes32 otherKey) {
requireInvariant consistencyKey(otherKey);
requireInvariant atUniqueness(
to_uint256(_indexOf(key) - 1),
to_uint256(_indexOf(otherKey) - 1)
);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: state only changes by setting or removing elements │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule stateChange(env e, bytes32 key) {
require sanity();
requireInvariant consistencyKey(key);
uint256 lengthBefore = length();
bool containsBefore = contains(key);
bytes32 valueBefore = tryGet_value(key);
method f;
calldataarg args;
f(e, args);
uint256 lengthAfter = length();
bool containsAfter = contains(key);
bytes32 valueAfter = tryGet_value(key);
assert lengthBefore != lengthAfter => (
(f.selector == set(bytes32,bytes32).selector && lengthAfter == lengthBefore + 1) ||
(f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1)
);
assert containsBefore != containsAfter => (
(f.selector == set(bytes32,bytes32).selector && containsAfter) ||
(f.selector == remove(bytes32).selector && !containsAfter)
);
assert valueBefore != valueAfter => (
(f.selector == set(bytes32,bytes32).selector && containsAfter) ||
(f.selector == remove(bytes32).selector && !containsAfter && valueAfter == 0)
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: check liveness of view functions. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule liveness_1(bytes32 key) {
requireInvariant consistencyKey(key);
// contains never revert
bool contains = contains@withrevert(key);
assert !lastReverted;
// tryGet never reverts (key)
tryGet_contains@withrevert(key);
assert !lastReverted;
// tryGet never reverts (value)
tryGet_value@withrevert(key);
assert !lastReverted;
// get reverts iff the key is not in the map
get@withrevert(key);
assert !lastReverted <=> contains;
}
rule liveness_2(uint256 index) {
requireInvariant consistencyIndex(index);
// length never revert
uint256 length = length@withrevert();
assert !lastReverted;
// key_at reverts iff the index is out of bound
key_at@withrevert(index);
assert !lastReverted <=> index < length;
// value_at reverts iff the index is out of bound
value_at@withrevert(index);
assert !lastReverted <=> index < length;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: get and tryGet return the expected values. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule getAndTryGet(bytes32 key) {
requireInvariant noValueIfNotContained(key);
bool contained = contains(key);
bool tryContained = tryGet_contains(key);
bytes32 tryValue = tryGet_value(key);
bytes32 value = get@withrevert(key); // revert is not contained
assert contained == tryContained;
assert contained => tryValue == value;
assert !contained => tryValue == 0;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: set key-value in EnumerableMap │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule set(bytes32 key, bytes32 value, bytes32 otherKey) {
require sanity();
uint256 lengthBefore = length();
bool containsBefore = contains(key);
bool containsOtherBefore = contains(otherKey);
bytes32 otherValueBefore = tryGet_value(otherKey);
bool added = set@withrevert(key, value);
bool success = !lastReverted;
assert success && contains(key) && get(key) == value,
"liveness & immediate effect";
assert added <=> !containsBefore,
"return value: added iff not contained";
assert length() == lengthBefore + to_mathint(added ? 1 : 0),
"effect: length increases iff added";
assert added => (key_at(lengthBefore) == key && value_at(lengthBefore) == value),
"effect: add at the end";
assert containsOtherBefore != contains(otherKey) => (added && key == otherKey),
"side effect: other keys are not affected";
assert otherValueBefore != tryGet_value(otherKey) => key == otherKey,
"side effect: values attached to other keys are not affected";
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: remove key from EnumerableMap │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule remove(bytes32 key, bytes32 otherKey) {
requireInvariant consistencyKey(key);
requireInvariant consistencyKey(otherKey);
uint256 lengthBefore = length();
bool containsBefore = contains(key);
bool containsOtherBefore = contains(otherKey);
bytes32 otherValueBefore = tryGet_value(otherKey);
bool removed = remove@withrevert(key);
bool success = !lastReverted;
assert success && !contains(key),
"liveness & immediate effect";
assert removed <=> containsBefore,
"return value: removed iff contained";
assert length() == lengthBefore - to_mathint(removed ? 1 : 0),
"effect: length decreases iff removed";
assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey),
"side effect: other keys are not affected";
assert otherValueBefore != tryGet_value(otherKey) => key == otherKey,
"side effect: values attached to other keys are not affected";
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: when adding a new key, the other keys remain in set, at the same index. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setEnumerability(bytes32 key, bytes32 value, uint256 index) {
require sanity();
bytes32 atKeyBefore = key_at(index);
bytes32 atValueBefore = value_at(index);
set(key, value);
bytes32 atKeyAfter = key_at@withrevert(index);
assert !lastReverted;
bytes32 atValueAfter = value_at@withrevert(index);
assert !lastReverted;
assert atKeyAfter == atKeyBefore;
assert atValueAfter != atValueBefore => (
key == atKeyBefore &&
value == atValueAfter
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: when removing a existing key, the other keys remain in set, at the same index (except for the last one). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule removeEnumerability(bytes32 key, uint256 index) {
uint256 last = length() - 1;
requireInvariant consistencyKey(key);
requireInvariant consistencyIndex(index);
requireInvariant consistencyIndex(last);
bytes32 atKeyBefore = key_at(index);
bytes32 atValueBefore = value_at(index);
bytes32 lastKeyBefore = key_at(last);
bytes32 lastValueBefore = value_at(last);
remove(key);
// can't read last value & keys (length decreased)
bytes32 atKeyAfter = key_at@withrevert(index);
assert lastReverted <=> index == last;
bytes32 atValueAfter = value_at@withrevert(index);
assert lastReverted <=> index == last;
// One value that is allowed to change is if previous value was removed,
// in that case the last value before took its place.
assert (
index != last &&
atKeyBefore != atKeyAfter
) => (
atKeyBefore == key &&
atKeyAfter == lastKeyBefore
);
assert (
index != last &&
atValueBefore != atValueAfter
) => (
atValueAfter == lastValueBefore
);
}