Skip to content

Commit

Permalink
Refactor DoubleEndedQueue (#4150)
Browse files Browse the repository at this point in the history
Co-authored-by: Francisco <fg@frang.io>
  • Loading branch information
Amxx and frangio authored Jul 27, 2023
1 parent 7222a31 commit 7c02b5c
Show file tree
Hide file tree
Showing 7 changed files with 104 additions and 160 deletions.
5 changes: 5 additions & 0 deletions .changeset/strong-poems-thank.md
Original file line number Diff line number Diff line change
@@ -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.
4 changes: 2 additions & 2 deletions certora/harnesses/DoubleEndedQueueHarness.sol
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
8 changes: 8 additions & 0 deletions certora/run.js
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,11 @@ const argv = require('yargs')
type: 'number',
default: 4,
},
verbose: {
alias: 'v',
type: 'count',
default: 0,
},
options: {
alias: 'o',
type: 'array',
Expand Down Expand Up @@ -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();
Expand Down
174 changes: 54 additions & 120 deletions certora/specs/DoubleEndedQueue.spec

Large diffs are not rendered by default.

3 changes: 0 additions & 3 deletions certora/specs/helpers/helpers.spec
Original file line number Diff line number Diff line change
Expand Up @@ -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;
68 changes: 34 additions & 34 deletions contracts/utils/structs/DoubleEndedQueue.sol
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@
// OpenZeppelin Contracts (last updated v4.9.0) (utils/structs/DoubleEndedQueue.sol)
pragma solidity ^0.8.19;

import {SafeCast} from "../math/SafeCast.sol";

/**
* @dev A sequence of items with the ability to efficiently push and pop items (i.e. insert and remove) on both ends of
* the sequence (called front and back). Among other access patterns, it can be used to implement efficient LIFO and
Expand All @@ -22,6 +20,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.
*/
Expand All @@ -40,18 +43,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;
}
}
Expand All @@ -62,26 +66,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;
}

/**
Expand All @@ -90,11 +94,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;
}
}
Expand All @@ -106,8 +110,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];
}

/**
Expand All @@ -117,11 +120,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];
}

/**
Expand All @@ -131,10 +132,11 @@ 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();
// By construction, length is a uint128, so the check above ensures that index can be safely downcast to uint128.
unchecked {
return deque._data[deque._begin + uint128(index)];
}
}

/**
Expand All @@ -152,17 +154,15 @@ 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.
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;
}
}
2 changes: 1 addition & 1 deletion requirements.txt
Original file line number Diff line number Diff line change
@@ -1 +1 @@
certora-cli==3.6.4
certora-cli==4.3.1

0 comments on commit 7c02b5c

Please sign in to comment.