diff --git a/certora/harnesses/DoubleEndedQueueHarness.sol b/certora/harnesses/DoubleEndedQueueHarness.sol new file mode 100644 index 000000000..b4f0bc841 --- /dev/null +++ b/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); + } +} diff --git a/certora/specs.json b/certora/specs.json index 80fbf26af..cd68af65e 100644 --- a/certora/specs.json +++ b/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", diff --git a/certora/specs/DoubleEndedQueue.spec b/certora/specs/DoubleEndedQueue.spec new file mode 100644 index 000000000..2412b4cc8 --- /dev/null +++ b/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"; +}