mirror
/
openzeppelin-contracts
mirror of https://github.com/OpenZeppelin/openzeppelin-contracts
2
1
Fork 1
Code Issues Releases Wiki Activity

Refactor DoubleEndedQueue (#4150)

Browse Source 
Co-authored-by: Francisco <fg@frang.io>
pull/4487/head
Hadrien Croubois 2 years ago committed by GitHub
parent 7222a31d54
commit 7c02b5cab2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 104 additions and 160 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 5
      .changeset/strong-poems-thank.md
  2. 4
      certora/harnesses/DoubleEndedQueueHarness.sol
  3. 8
      certora/run.js
  4. 174
      certora/specs/DoubleEndedQueue.spec
  5. 3
      certora/specs/helpers/helpers.spec
  6. 68
      contracts/utils/structs/DoubleEndedQueue.sol
  7. 2
      requirements.txt

5
.changeset/strong-poems-thank.md
Unescape View File

@ -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
certora/harnesses/DoubleEndedQueueHarness.sol
Unescape View File

@ -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;
}

8
certora/run.js
Unescape View File

@ -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();

174
certora/specs/DoubleEndedQueue.spec
Unescape View File

@ -1,64 +1,25 @@
import "helpers/helpers.spec"
import "helpers/helpers.spec";
methods {
pushFront(bytes32) envfree
pushBack(bytes32) envfree
popFront() returns (bytes32) envfree
popBack() returns (bytes32) envfree
clear() envfree
function pushFront(bytes32) external envfree;
function pushBack(bytes32) external envfree;
function popFront() external returns (bytes32) envfree;
function popBack() external returns (bytes32) envfree;
function clear() external envfree;
// exposed for FV
begin() returns (int128) envfree
end() returns (int128) envfree
function begin() external returns (uint128) envfree;
function end() external returns (uint128) 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
function length() external returns (uint256) envfree;
function empty() external returns (bool) envfree;
function front() external returns (bytes32) envfree;
function back() external returns (bytes32) envfree;
function at_(uint256) external 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(); } }
definition full() returns bool = length() == max_uint128;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@ -68,22 +29,19 @@ invariant lengthConsistency()
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()
invariant queueFront()
at_(0) == front()
filtered { f -> !f.isView }
invariant queueBack()
at_(require_uint256(length() - 1)) == back()
filtered { f -> !f.isView }
{
preserved {
requireInvariant boundariesConsistency();
require boundedQueue();
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@ -91,18 +49,18 @@ invariant queueEndings()
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule pushFront(bytes32 value) {
require boundedQueue();
uint256 lengthBefore = length();
bool fullBefore = full();
pushFront@withrevert(value);
bool success = !lastReverted;
// liveness
assert !lastReverted, "never reverts";
assert success <=> !fullBefore, "never revert if not previously full";
// effect
assert front() == value, "front set to value";
assert length() == lengthBefore + 1, "queue extended";
assert success => front() == value, "front set to value";
assert success => to_mathint(length()) == lengthBefore + 1, "queue extended";
}
/*
@ -111,15 +69,13 @@ rule pushFront(bytes32 value) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule pushFrontConsistency(uint256 index) {
require boundedQueue();
bytes32 beforeAt = at_(index);
bytes32 value;
pushFront(value);
// try to read value
bytes32 afterAt = at_@withrevert(index + 1);
bytes32 afterAt = at_@withrevert(require_uint256(index + 1));
assert !lastReverted, "value still there";
assert afterAt == beforeAt, "data is preserved";
@ -131,18 +87,18 @@ rule pushFrontConsistency(uint256 index) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule pushBack(bytes32 value) {
require boundedQueue();
uint256 lengthBefore = length();
bool fullBefore = full();
pushBack@withrevert(value);
bool success = !lastReverted;
// liveness
assert !lastReverted, "never reverts";
assert success <=> !fullBefore, "never revert if not previously full";
// effect
assert back() == value, "back set to value";
assert length() == lengthBefore + 1, "queue increased";
assert success => back() == value, "back set to value";
assert success => to_mathint(length()) == lengthBefore + 1, "queue increased";
}
/*
@ -151,8 +107,6 @@ rule pushBack(bytes32 value) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule pushBackConsistency(uint256 index) {
require boundedQueue();
bytes32 beforeAt = at_(index);
bytes32 value;
@ -171,9 +125,6 @@ rule pushBackConsistency(uint256 index) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule popFront {
requireInvariant boundariesConsistency();
require boundedQueue();
uint256 lengthBefore = length();
bytes32 frontBefore = front@withrevert();
@ -185,7 +136,7 @@ rule popFront {
// effect
assert success => frontBefore == popped, "previous front is returned";
assert success => length() == lengthBefore - 1, "queue decreased";
assert success => to_mathint(length()) == lengthBefore - 1, "queue decreased";
}
/*
@ -194,9 +145,6 @@ rule 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);
@ -204,7 +152,7 @@ rule popFrontConsistency(uint256 index) {
popFront();
// try to read value
bytes32 after = at_@withrevert(index - 1);
bytes32 after = at_@withrevert(require_uint256(index - 1));
assert !lastReverted, "value still exists in the queue";
assert before == after, "values are offset and not modified";
@ -216,9 +164,6 @@ rule popFrontConsistency(uint256 index) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule popBack {
requireInvariant boundariesConsistency();
require boundedQueue();
uint256 lengthBefore = length();
bytes32 backBefore = back@withrevert();
@ -230,7 +175,7 @@ rule popBack {
// effect
assert success => backBefore == popped, "previous back is returned";
assert success => length() == lengthBefore - 1, "queue decreased";
assert success => to_mathint(length()) == lengthBefore - 1, "queue decreased";
}
/*
@ -239,11 +184,8 @@ rule 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;
require to_mathint(index) < length() - 1;
bytes32 before = at_(index);
popBack();
@ -275,24 +217,25 @@ rule clear {
│ Rule: front/back access reverts only if the queue is empty or querying out of bounds │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyEmptyRevert(env e) {
rule onlyEmptyOrFullRevert(env e) {
require nonpayable(e);
requireInvariant boundariesConsistency();
require boundedQueue();
method f;
calldataarg args;
bool emptyBefore = empty();
bool fullBefore = full();
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
(f.selector == sig:front().selector && emptyBefore) ||
(f.selector == sig:back().selector && emptyBefore) ||
(f.selector == sig:popFront().selector && emptyBefore) ||
(f.selector == sig:popBack().selector && emptyBefore) ||
(f.selector == sig:pushFront(bytes32).selector && fullBefore ) ||
(f.selector == sig:pushBack(bytes32).selector && fullBefore ) ||
f.selector == sig:at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert
), "only revert if empty or out of bounds";
}
@ -302,9 +245,6 @@ rule onlyEmptyRevert(env e) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOutOfBoundsRevert(uint256 index) {
requireInvariant boundariesConsistency();
require boundedQueue();
at_@withrevert(index);
assert lastReverted <=> index >= length(), "only reverts if index is out of bounds";
@ -316,9 +256,6 @@ rule onlyOutOfBoundsRevert(uint256 index) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule noLengthChange(env e) {
requireInvariant boundariesConsistency();
require boundedQueue();
method f;
calldataarg args;
@ -327,11 +264,11 @@ rule noLengthChange(env e) {
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)
(f.selector == sig:pushFront(bytes32).selector && to_mathint(lengthAfter) == lengthBefore + 1) ||
(f.selector == sig:pushBack(bytes32).selector && to_mathint(lengthAfter) == lengthBefore + 1) ||
(f.selector == sig:popBack().selector && to_mathint(lengthAfter) == lengthBefore - 1) ||
(f.selector == sig:popFront().selector && to_mathint(lengthAfter) == lengthBefore - 1) ||
(f.selector == sig:clear().selector && lengthAfter == 0)
), "length is only affected by clear/pop/push operations";
}
@ -341,9 +278,6 @@ rule noLengthChange(env e) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule noDataChange(env e) {
requireInvariant boundariesConsistency();
require boundedQueue();
method f;
calldataarg args;
@ -354,13 +288,13 @@ rule noDataChange(env e) {
bool atAfterSuccess = !lastReverted;
assert !atAfterSuccess <=> (
f.selector == clear().selector ||
(f.selector == popBack().selector && index == length()) ||
(f.selector == popFront().selector && index == length())
(f.selector == sig:clear().selector ) ||
(f.selector == sig:popBack().selector && index == length()) ||
(f.selector == sig: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
f.selector == sig:popFront().selector ||
f.selector == sig:pushFront(bytes32).selector
), "values of the queue are only changed by popFront or pushFront";
}

3
certora/specs/helpers/helpers.spec
Unescape View File

@ -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
contracts/utils/structs/DoubleEndedQueue.sol
Unescape View File

@ -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
@ -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.
*/
@ -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;
}
}
@ -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;
}
/**
@ -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;
}
}
@ -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];
}
/**
@ -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];
}
/**
@ -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)];
}
}
/**
@ -152,10 +154,8 @@ 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);
}
}
@ -163,6 +163,6 @@ library DoubleEndedQueue {
* @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
requirements.txt
Unescape View File

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

Write Preview
Loading…
Cancel
Save