Add formal verification specs for EnumerableSet & EnumerableMap (#4167)

Co-authored-by: Francisco <fg@frang.io>

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];
+    }
+}

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];
+    }
+}

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",

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
+    );
+}

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
+    );
+}