diff --git a/certora/harnesses/EnumerableMapHarness.sol b/certora/harnesses/EnumerableMapHarness.sol new file mode 100644 index 000000000..3bcf1b50a --- /dev/null +++ b/certora/harnesses/EnumerableMapHarness.sol @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/utils/structs/EnumerableMap.sol"; + +contract EnumerableMapHarness { + using EnumerableMap for EnumerableMap.Bytes32ToBytes32Map; + + EnumerableMap.Bytes32ToBytes32Map private _map; + + function set(bytes32 key, bytes32 value) public returns (bool) { + return _map.set(key, value); + } + + function remove(bytes32 key) public returns (bool) { + return _map.remove(key); + } + + function contains(bytes32 key) public view returns (bool) { + return _map.contains(key); + } + + function length() public view returns (uint256) { + return _map.length(); + } + + function key_at(uint256 index) public view returns (bytes32) { + (bytes32 key,) = _map.at(index); + return key; + } + + function value_at(uint256 index) public view returns (bytes32) { + (,bytes32 value) = _map.at(index); + return value; + } + + function tryGet_contains(bytes32 key) public view returns (bool) { + (bool contained,) = _map.tryGet(key); + return contained; + } + + function tryGet_value(bytes32 key) public view returns (bytes32) { + (,bytes32 value) = _map.tryGet(key); + return value; + } + + function get(bytes32 key) public view returns (bytes32) { + return _map.get(key); + } + + function _indexOf(bytes32 key) public view returns (uint256) { + return _map._keys._inner._indexes[key]; + } +} diff --git a/certora/harnesses/EnumerableSetHarness.sol b/certora/harnesses/EnumerableSetHarness.sol new file mode 100644 index 000000000..64383e6a4 --- /dev/null +++ b/certora/harnesses/EnumerableSetHarness.sol @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/utils/structs/EnumerableSet.sol"; + +contract EnumerableSetHarness { + using EnumerableSet for EnumerableSet.Bytes32Set; + + EnumerableSet.Bytes32Set private _set; + + function add(bytes32 value) public returns (bool) { + return _set.add(value); + } + + function remove(bytes32 value) public returns (bool) { + return _set.remove(value); + } + + function contains(bytes32 value) public view returns (bool) { + return _set.contains(value); + } + + function length() public view returns (uint256) { + return _set.length(); + } + + function at_(uint256 index) public view returns (bytes32) { + return _set.at(index); + } + + function _indexOf(bytes32 value) public view returns (uint256) { + return _set._inner._indexes[value]; + } +} diff --git a/certora/run.js b/certora/run.js old mode 100644 new mode 100755 diff --git a/certora/specs.json b/certora/specs.json index 39ba8c235..6f8f57bdf 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -62,6 +62,16 @@ "contract": "InitializableHarness", "files": ["certora/harnesses/InitializableHarness.sol"] }, + { + "spec": "EnumerableSet", + "contract": "EnumerableSetHarness", + "files": ["certora/harnesses/EnumerableSetHarness.sol"] + }, + { + "spec": "EnumerableMap", + "contract": "EnumerableMapHarness", + "files": ["certora/harnesses/EnumerableMapHarness.sol"] + }, { "spec": "TimelockController", "contract": "TimelockControllerHarness", diff --git a/certora/specs/EnumerableMap.spec b/certora/specs/EnumerableMap.spec new file mode 100644 index 000000000..56ef854c6 --- /dev/null +++ b/certora/specs/EnumerableMap.spec @@ -0,0 +1,334 @@ +import "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 + ); +} diff --git a/certora/specs/EnumerableSet.spec b/certora/specs/EnumerableSet.spec new file mode 100644 index 000000000..c94ba2437 --- /dev/null +++ b/certora/specs/EnumerableSet.spec @@ -0,0 +1,247 @@ +import "helpers.spec" + +methods { + // library + add(bytes32) returns (bool) envfree + remove(bytes32) returns (bool) envfree + contains(bytes32) returns (bool) envfree + length() returns (uint256) envfree + at_(uint256) returns (bytes32) envfree + + // FV + _indexOf(bytes32) returns (uint256) envfree +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Helpers │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +function sanity() returns bool { + return length() < max_uint256; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: All indexed keys are contained │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant indexedContained(uint256 index) + index < length() => contains(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 <=> at_(index1) == at_(index2) + { + preserved remove(bytes32 key) { + requireInvariant atUniqueness(index1, to_uint256(length() - 1)); + requireInvariant atUniqueness(index2, to_uint256(length() - 1)); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: index <> key 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 added │ +│ and removed from the EnumerableSet). │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant consistencyIndex(uint256 index) + index < length() => _indexOf(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() && + 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 adding or removing elements │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateChange(env e, bytes32 key) { + require sanity(); + requireInvariant consistencyKey(key); + + uint256 lengthBefore = length(); + bool containsBefore = contains(key); + + method f; + calldataarg args; + f(e, args); + + uint256 lengthAfter = length(); + bool containsAfter = contains(key); + + assert lengthBefore != lengthAfter => ( + (f.selector == add(bytes32).selector && lengthAfter == lengthBefore + 1) || + (f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1) + ); + + assert containsBefore != containsAfter => ( + (f.selector == add(bytes32).selector && containsAfter) || + (f.selector == remove(bytes32).selector && containsBefore) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: check liveness of view functions. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule liveness_1(bytes32 key) { + requireInvariant consistencyKey(key); + + // contains never revert + contains@withrevert(key); + assert !lastReverted; +} + +rule liveness_2(uint256 index) { + requireInvariant consistencyIndex(index); + + // length never revert + uint256 length = length@withrevert(); + assert !lastReverted; + + // at reverts iff the index is out of bound + at_@withrevert(index); + assert !lastReverted <=> index < length; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: add key to EnumerableSet if not already contained │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule add(bytes32 key, bytes32 otherKey) { + require sanity(); + + uint256 lengthBefore = length(); + bool containsBefore = contains(key); + bool containsOtherBefore = contains(otherKey); + + bool added = add@withrevert(key); + bool success = !lastReverted; + + assert success && contains(key), + "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 => at_(lengthBefore) == key, + "effect: add at the end"; + + assert containsOtherBefore != contains(otherKey) => (added && key == otherKey), + "side effect: other keys are not affected"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: remove key from EnumerableSet if already contained │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule remove(bytes32 key, bytes32 otherKey) { + requireInvariant consistencyKey(key); + requireInvariant consistencyKey(otherKey); + + uint256 lengthBefore = length(); + bool containsBefore = contains(key); + bool containsOtherBefore = contains(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"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: when adding a new key, the other keys remain in set, at the same index. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule addEnumerability(bytes32 key, uint256 index) { + require sanity(); + + bytes32 atBefore = at_(index); + add(key); + bytes32 atAfter = at_@withrevert(index); + bool atAfterSuccess = !lastReverted; + + assert atAfterSuccess; + assert atBefore == atAfter; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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 atBefore = at_(index); + bytes32 lastBefore = at_(last); + + remove(key); + + // can't read last value (length decreased) + bytes32 atAfter = 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 && + atBefore != atAfter + ) => ( + atBefore == key && + atAfter == lastBefore + ); +}