Add DoubleEndedQueue FV (#4147)

Co-authored-by: Francisco <fg@frang.io>
Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>

certora/harnesses/DoubleEndedQueueHarness.sol

@@ -0,0 +1,59 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/utils/structs/DoubleEndedQueue.sol";
+
+contract DoubleEndedQueueHarness {
+    using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque;
+
+    DoubleEndedQueue.Bytes32Deque private _deque;
+
+    function pushFront(bytes32 value) external {
+        _deque.pushFront(value);
+    }
+
+    function pushBack(bytes32 value) external {
+        _deque.pushBack(value);
+    }
+
+    function popFront() external returns (bytes32 value) {
+        return _deque.popFront();
+    }
+
+    function popBack() external returns (bytes32 value) {
+        return _deque.popBack();
+    }
+
+    function clear() external {
+        _deque.clear();
+    }
+
+    function begin() external view returns (int128) {
+        return _deque._begin;
+    }
+
+    function end() external view returns (int128) {
+        return _deque._end;
+    }
+
+    function length() external view returns (uint256) {
+        return _deque.length();
+    }
+
+    function empty() external view returns (bool) {
+        return _deque.empty();
+    }
+
+    function front() external view returns (bytes32 value) {
+        return _deque.front();
+    }
+
+    function back() external view returns (bytes32 value) {
+        return _deque.back();
+    }
+
+    function at_(uint256 index) external view returns (bytes32 value) {
+        return _deque.at(index);
+    }
+}

certora/specs.json

@@ -9,6 +9,11 @@
     "contract": "AccessControlHarness",
     "files": ["certora/harnesses/AccessControlHarness.sol"]
   },
+  {
+    "spec": "DoubleEndedQueue",
+    "contract": "DoubleEndedQueueHarness",
+    "files": ["certora/harnesses/DoubleEndedQueueHarness.sol"]
+  },
   {
     "spec": "Ownable",
     "contract": "OwnableHarness",

certora/specs/DoubleEndedQueue.spec

@@ -0,0 +1,366 @@
+import "helpers.spec"
+
+methods {
+    pushFront(bytes32)                    envfree
+    pushBack(bytes32)                     envfree
+    popFront()          returns (bytes32) envfree
+    popBack()           returns (bytes32) envfree
+    clear()                               envfree
+
+    // exposed for FV
+    begin()             returns (int128)  envfree
+    end()               returns (int128)  envfree
+    
+    // view
+    length()            returns (uint256) envfree
+    empty()             returns (bool)    envfree
+    front()             returns (bytes32) envfree
+    back()              returns (bytes32) envfree
+    at_(uint256)        returns (bytes32) envfree // at is a reserved word
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+function min_int128() returns mathint {
+    return -(1 << 127);
+}
+
+function max_int128() returns mathint {
+    return (1 << 127) - 1;
+}
+
+// Could be broken in theory, but not in practice
+function boundedQueue() returns bool {
+    return 
+        max_int128() > to_mathint(end()) &&
+        min_int128() < to_mathint(begin());
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: end is larger or equal than begin                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant boundariesConsistency()
+    end() >= begin()
+    filtered { f -> !f.isView }
+    { preserved { require boundedQueue(); } }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: length is end minus begin                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant lengthConsistency()
+    length() == to_mathint(end()) - to_mathint(begin())
+    filtered { f -> !f.isView }
+    { preserved { require boundedQueue(); } }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: empty() is length 0 and no element exists                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant emptiness()
+    empty() <=> length() == 0
+    filtered { f -> !f.isView }
+    { preserved { require boundedQueue(); } }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: front points to the first index and back points to the last one                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant queueEndings()
+    at_(length() - 1) == back() && at_(0) == front()
+    filtered { f -> !f.isView }
+    { 
+        preserved { 
+            requireInvariant boundariesConsistency(); 
+            require boundedQueue(); 
+        } 
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: pushFront adds an element at the beginning of the queue                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushFront(bytes32 value) {
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+    
+    pushFront@withrevert(value);
+    
+    // liveness
+    assert !lastReverted, "never reverts";
+    
+    // effect
+    assert front() == value, "front set to value";
+    assert length() == lengthBefore + 1, "queue extended";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pushFront preserves the previous values in the queue with a +1 offset                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushFrontConsistency(uint256 index) {
+    require boundedQueue();
+
+    bytes32 beforeAt = at_(index);
+
+    bytes32 value;
+    pushFront(value);
+
+    // try to read value
+    bytes32 afterAt = at_@withrevert(index + 1);
+
+    assert !lastReverted, "value still there";
+    assert afterAt == beforeAt, "data is preserved";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: pushBack adds an element at the end of the queue                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushBack(bytes32 value) {
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+    
+    pushBack@withrevert(value);
+    
+    // liveness
+    assert !lastReverted, "never reverts";
+    
+    // effect
+    assert back() == value, "back set to value";
+    assert length() == lengthBefore + 1, "queue increased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pushBack preserves the previous values in the queue                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushBackConsistency(uint256 index) {
+    require boundedQueue();
+
+    bytes32 beforeAt = at_(index);
+
+    bytes32 value;
+    pushBack(value);
+
+    // try to read value
+    bytes32 afterAt = at_@withrevert(index);
+
+    assert !lastReverted, "value still there";
+    assert afterAt == beforeAt, "data is preserved";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: popFront removes an element from the beginning of the queue                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popFront {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+    bytes32 frontBefore = front@withrevert();
+
+    bytes32 popped = popFront@withrevert();
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> lengthBefore != 0, "never reverts if not previously empty";
+
+    // effect
+    assert success => frontBefore == popped, "previous front is returned";
+    assert success => length() == lengthBefore - 1, "queue decreased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: at(x) is preserved and offset to at(x - 1) after calling popFront                                             |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popFrontConsistency(uint256 index) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    // Read (any) value that is not the front (this asserts the value exists / the queue is long enough)
+    require index > 1;
+    bytes32 before = at_(index);
+
+    popFront();
+
+    // try to read value
+    bytes32 after = at_@withrevert(index - 1);
+    
+    assert !lastReverted, "value still exists in the queue";
+    assert before == after, "values are offset and not modified";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: popBack removes an element from the end of the queue                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popBack {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+    bytes32 backBefore = back@withrevert();
+
+    bytes32 popped = popBack@withrevert();
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> lengthBefore != 0, "never reverts if not previously empty";
+
+    // effect
+    assert success => backBefore == popped, "previous back is returned";
+    assert success => length() == lengthBefore - 1, "queue decreased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: at(x) is preserved after calling popBack                                                                     |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popBackConsistency(uint256 index) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    // Read (any) value that is not the back (this asserts the value exists / the queue is long enough)
+    require index < length() - 1;
+    bytes32 before = at_(index);
+
+    popBack();
+
+    // try to read value
+    bytes32 after = at_@withrevert(index);
+    
+    assert !lastReverted, "value still exists in the queue";
+    assert before == after, "values are offset and not modified";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: clear sets length to 0                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule clear {
+    clear@withrevert();
+    
+    // liveness
+    assert !lastReverted, "never reverts";
+    
+    // effect
+    assert length() == 0, "sets length to 0";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: front/back access reverts only if the queue is empty or querying out of bounds                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyEmptyRevert(env e) {
+    require nonpayable(e);
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    method f;
+    calldataarg args;
+
+    bool emptyBefore = empty();
+
+    f@withrevert(e, args);
+
+    assert lastReverted => (
+        (f.selector == front().selector && emptyBefore) ||
+        (f.selector == back().selector && emptyBefore) ||
+        (f.selector == popFront().selector  && emptyBefore) ||
+        (f.selector == popBack().selector  && emptyBefore) ||
+        f.selector == at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert
+    ), "only revert if empty or out of bounds";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: at(index) only reverts if index is out of bounds                                                                  |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyOutOfBoundsRevert(uint256 index) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    at_@withrevert(index);
+
+    assert lastReverted <=> index >= length(), "only reverts if index is out of bounds";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only clear/push/pop operations can change the length of the queue                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noLengthChange(env e) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    method f;
+    calldataarg args;
+
+    uint256 lengthBefore = length();
+    f(e, args);
+    uint256 lengthAfter = length();
+
+    assert lengthAfter != lengthBefore => (
+        (f.selector == pushFront(bytes32).selector && lengthAfter == lengthBefore + 1) ||
+        (f.selector == pushBack(bytes32).selector && lengthAfter == lengthBefore + 1) ||
+        (f.selector == popBack().selector && lengthAfter == lengthBefore - 1) ||
+        (f.selector == popFront().selector && lengthAfter == lengthBefore - 1) ||
+        (f.selector == clear().selector && lengthAfter == 0)
+    ), "length is only affected by clear/pop/push operations";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only push/pop can change values bounded in the queue (outside values aren't cleared)                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDataChange(env e) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    method f;
+    calldataarg args;
+
+    uint256 index;
+    bytes32 atBefore = at_(index);
+    f(e, args);
+    bytes32 atAfter = at_@withrevert(index);
+    bool atAfterSuccess = !lastReverted;
+
+    assert !atAfterSuccess <=> (
+        f.selector == clear().selector ||
+        (f.selector == popBack().selector && index == length()) ||
+        (f.selector == popFront().selector && index == length())
+    ), "indexes of the queue are only removed by clear or pop";
+
+    assert atAfterSuccess && atAfter != atBefore => (
+        f.selector == popFront().selector ||
+        f.selector == pushFront(bytes32).selector
+    ), "values of the queue are only changed by popFront or pushFront";
+}