Refactor DoubleEndedQueue

.changeset/strong-poems-thank.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`DoubleEndedQueue`: refactor internal structure to use `uint128` instead of `int128`. This has no effect on the library interface.

certora/harnesses/DoubleEndedQueueHarness.sol

@@ -29,11 +29,11 @@ contract DoubleEndedQueueHarness {
         _deque.clear();
     }
 
-    function begin() external view returns (int128) {
+    function begin() external view returns (uint128) {
         return _deque._begin;
     }
 
-    function end() external view returns (int128) {
+    function end() external view returns (uint128) {
         return _deque._end;
     }
 

certora/run.js

@@ -28,6 +28,11 @@ const argv = require('yargs')
       type: 'number',
       default: 4,
     },
+    verbose: {
+      alias: 'v',
+      type: 'count',
+      default: 0,
+    },
     options: {
       alias: 'o',
       type: 'array',
@@ -65,6 +70,9 @@ for (const { spec, contract, files, options = [] } of specs) {
 // Run certora, aggregate the output and print it at the end
 async function runCertora(spec, contract, files, options = []) {
   const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
+  if (argv.verbose) {
+    console.log('Running:', args.join(' '));
+  }
   const child = proc.spawn('certoraRun', args);
 
   const stream = new PassThrough();

certora/specs/helpers/helpers.spec

@@ -2,9 +2,6 @@
 definition nonpayable(env e) returns bool = e.msg.value == 0;
 definition nonzerosender(env e) returns bool = e.msg.sender != 0;
 
-// constants
-definition max_uint48() returns mathint = (1 << 48) - 1;
-
 // math
 definition min(mathint a, mathint b) returns mathint = a < b ? a : b;
 definition max(mathint a, mathint b) returns mathint = a > b ? a : b;

contracts/utils/structs/DoubleEndedQueue.sol

@@ -22,6 +22,11 @@ library DoubleEndedQueue {
      */
     error QueueEmpty();
 
+    /**
+     * @dev A push operation couldn't be completed due to the queue being full.
+     */
+    error QueueFull();
+
     /**
      * @dev An operation (e.g. {at}) couldn't be completed due to an index being out of bounds.
      */
@@ -40,18 +45,19 @@ library DoubleEndedQueue {
      * data[end - 1].
      */
     struct Bytes32Deque {
-        int128 _begin;
-        int128 _end;
-        mapping(int128 => bytes32) _data;
+        uint128 _begin;
+        uint128 _end;
+        mapping(uint128 => bytes32) _data;
     }
 
     /**
      * @dev Inserts an item at the end of the queue.
      */
     function pushBack(Bytes32Deque storage deque, bytes32 value) internal {
-        int128 backIndex = deque._end;
-        deque._data[backIndex] = value;
         unchecked {
+            uint128 backIndex = deque._end;
+            if (backIndex + 1 == deque._begin) revert QueueFull();
+            deque._data[backIndex] = value;
             deque._end = backIndex + 1;
         }
     }
@@ -62,26 +68,26 @@ library DoubleEndedQueue {
      * Reverts with `QueueEmpty` if the queue is empty.
      */
     function popBack(Bytes32Deque storage deque) internal returns (bytes32 value) {
-        if (empty(deque)) revert QueueEmpty();
-        int128 backIndex;
         unchecked {
-            backIndex = deque._end - 1;
+            uint128 backIndex = deque._end;
+            if (backIndex == deque._begin) revert QueueEmpty();
+            --backIndex;
+            value = deque._data[backIndex];
+            delete deque._data[backIndex];
+            deque._end = backIndex;
         }
-        value = deque._data[backIndex];
-        delete deque._data[backIndex];
-        deque._end = backIndex;
     }
 
     /**
      * @dev Inserts an item at the beginning of the queue.
      */
     function pushFront(Bytes32Deque storage deque, bytes32 value) internal {
-        int128 frontIndex;
         unchecked {
-            frontIndex = deque._begin - 1;
+            uint128 frontIndex = deque._begin - 1;
+            if (frontIndex == deque._end) revert QueueFull();
+            deque._data[frontIndex] = value;
+            deque._begin = frontIndex;
         }
-        deque._data[frontIndex] = value;
-        deque._begin = frontIndex;
     }
 
     /**
@@ -90,11 +96,11 @@ library DoubleEndedQueue {
      * Reverts with `QueueEmpty` if the queue is empty.
      */
     function popFront(Bytes32Deque storage deque) internal returns (bytes32 value) {
-        if (empty(deque)) revert QueueEmpty();
-        int128 frontIndex = deque._begin;
-        value = deque._data[frontIndex];
-        delete deque._data[frontIndex];
         unchecked {
+            uint128 frontIndex = deque._begin;
+            if (frontIndex == deque._end) revert QueueEmpty();
+            value = deque._data[frontIndex];
+            delete deque._data[frontIndex];
             deque._begin = frontIndex + 1;
         }
     }
@@ -106,8 +112,7 @@ library DoubleEndedQueue {
      */
     function front(Bytes32Deque storage deque) internal view returns (bytes32 value) {
         if (empty(deque)) revert QueueEmpty();
-        int128 frontIndex = deque._begin;
-        return deque._data[frontIndex];
+        return deque._data[deque._begin];
     }
 
     /**
@@ -117,11 +122,9 @@ library DoubleEndedQueue {
      */
     function back(Bytes32Deque storage deque) internal view returns (bytes32 value) {
         if (empty(deque)) revert QueueEmpty();
-        int128 backIndex;
         unchecked {
-            backIndex = deque._end - 1;
+            return deque._data[deque._end - 1];
         }
-        return deque._data[backIndex];
     }
 
     /**
@@ -131,10 +134,10 @@ library DoubleEndedQueue {
      * Reverts with `QueueOutOfBounds` if the index is out of bounds.
      */
     function at(Bytes32Deque storage deque, uint256 index) internal view returns (bytes32 value) {
-        // int256(deque._begin) is a safe upcast
-        int128 idx = SafeCast.toInt128(int256(deque._begin) + SafeCast.toInt256(index));
-        if (idx >= deque._end) revert QueueOutOfBounds();
-        return deque._data[idx];
+        if (index >= length(deque)) revert QueueOutOfBounds();
+        unchecked {
+            return deque._data[deque._begin + SafeCast.toUint128(index)];
+        }
     }
 
     /**
@@ -152,17 +155,16 @@ library DoubleEndedQueue {
      * @dev Returns the number of items in the queue.
      */
     function length(Bytes32Deque storage deque) internal view returns (uint256) {
-        // The interface preserves the invariant that begin <= end so we assume this will not overflow.
-        // We also assume there are at most int256.max items in the queue.
+        // We also assume there are at most uint128.max items in the queue.
         unchecked {
-            return uint256(int256(deque._end) - int256(deque._begin));
+            return uint256(deque._end - deque._begin);
         }
     }
 
     /**
      * @dev Returns true if the queue is empty.
      */
     function empty(Bytes32Deque storage deque) internal view returns (bool) {
-        return deque._end <= deque._begin;
+        return deque._end == deque._begin;
     }
 }

requirements.txt

@@ -1 +1 @@
-certora-cli==3.6.4
+certora-cli==4.3.1