diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index 7a35618..d76321b 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,146 +1,25 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2023-05-23 16:01:50.888803463 +0200 -+++ DoubleLinkedList.sol 2023-05-23 16:44:01.777091764 +0200 -@@ -18,6 +18,8 @@ +--- DoubleLinkedList.sol ++++ DoubleLinkedList.sol +@@ -16,6 +16,8 @@ + + struct List { mapping(address => Account) accounts; - address head; - address tail; + address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion. + address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion. } /* ERRORS */ -@@ -101,14 +103,18 @@ - +@@ -101,10 +103,12 @@ uint256 numberOfIterations; - address next = list.head; // If not added at the end of the list `id` will be inserted before `next`. -+ list.insertedAfter = address(0); // HARNESS - - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + for (; numberOfIterations < maxIterations; numberOfIterations++) { + if (next == address(0) || list.accounts[next].value < value) break; + list.insertedAfter = next; // HARNESS - next = list.accounts[next].next; - unchecked { - ++numberOfIterations; - } + next = getNext(list, next); } + if (numberOfIterations == maxIterations) next = address(0); + list.insertedBefore = next; // HARNESS -+ - // Account is not the new tail. - if (numberOfIterations < maxIterations && next != address(0)) { - // Account is the new head. -diff -ruN MockDLL.sol MockDLL.sol ---- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2023-05-23 16:42:32.913885637 +0200 -@@ -0,0 +1,111 @@ -+// SPDX-License-Identifier: AGPL-3.0-only -+pragma solidity ^0.8.0; -+ -+import "./DoubleLinkedList.sol"; -+ -+contract MockDLL { -+ using DoubleLinkedList for DoubleLinkedList.List; -+ -+ // VERIFICATION INTERFACE -+ -+ DoubleLinkedList.List public dll; -+ -+ uint256 public maxIterations; -+ -+ uint256 internal dummy_state_variable; -+ -+ function dummy_state_modifying_function() public { -+ // to fix a CVL error when only one function is accessible -+ dummy_state_variable = 1; -+ } -+ -+ function getValueOf(address _id) public view returns (uint256) { -+ return dll.getValueOf(_id); -+ } -+ -+ function getHead() public view returns (address) { -+ return dll.getHead(); -+ } -+ -+ function getTail() public view returns (address) { -+ return dll.getTail(); -+ } -+ -+ function getNext(address _id) public view returns (address) { -+ return dll.getNext(_id); -+ } -+ -+ function getPrev(address _id) public view returns (address) { -+ return dll.getPrev(_id); -+ } -+ -+ function remove(address _id) public { -+ dll.remove(_id); -+ } -+ -+ function insertSorted( -+ address _id, -+ uint256 _value, -+ uint256 _maxIterations -+ ) public { -+ dll.insertSorted(_id, _value, _maxIterations); -+ } -+ -+ // SPECIFICATION HELPERS -+ -+ function getInsertedAfter() public view returns (address) { -+ return dll.insertedAfter; -+ } -+ -+ function getInsertedBefore() public view returns (address) { -+ return dll.insertedBefore; -+ } -+ -+ function getLength() public view returns (uint256) { -+ uint256 len; -+ for (address current = getHead(); current != address(0); current = getNext(current)) len++; -+ return len; -+ } -+ -+ function linkBetween(address _start, address _end) internal view returns (bool, address) { -+ if (_start == _end) return (true, address(0)); -+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { -+ address next = getNext(_start); -+ if (next == _end) return (true, _start); -+ _start = next; -+ } -+ return (false, address(0)); -+ } -+ -+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { -+ (ret, ) = linkBetween(_start, _end); -+ } -+ -+ function getPreceding(address _end) public view returns (address last) { -+ (, last) = linkBetween(getHead(), _end); -+ } -+ -+ function greaterThanUpTo( -+ uint256 _value, -+ address _to, -+ uint256 _maxIter -+ ) public view returns (bool) { -+ address from = getHead(); -+ for (; _maxIter > 0; _maxIter--) { -+ if (from == _to) return true; -+ if (getValueOf(from) < _value) return false; -+ from = getNext(from); -+ } -+ return true; -+ } -+ -+ function lenUpTo(address _to) public view returns (uint256) { -+ uint256 maxIter = getLength(); -+ address from = getHead(); -+ for (; maxIter > 0; maxIter--) { -+ if (from == _to) break; -+ from = getNext(from); -+ } -+ return getLength() - maxIter; -+ } -+} + + address prev = getPrev(list, next); + list.accounts[id] = Account(prev, next, value); diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index 9fb9d16..fd5e6c9 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,16 +1,16 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2023-05-23 16:01:50.888803463 +0200 -+++ DoubleLinkedList.sol 2023-05-23 16:34:10.324900474 +0200 -@@ -18,6 +18,8 @@ +--- DoubleLinkedList.sol ++++ DoubleLinkedList.sol +@@ -16,6 +16,8 @@ + + struct List { mapping(address => Account) accounts; - address head; - address tail; + address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion. + address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion. } /* ERRORS */ -@@ -93,24 +95,23 @@ +@@ -90,21 +92,20 @@ /// @param list The list to search in. /// @param id The address of the account. /// @param value The value of the account. @@ -21,120 +21,18 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol if (id == address(0)) revert AddressIsZero(); if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); -- uint256 numberOfIterations; -- address next = list.head; // If not added at the end of the list `id` will be inserted before `next`. -+ list.insertedAfter = address(0); -+ address next = list.head; // `id` will be inserted before `next`. + address next = getHead(list); // `id` will be inserted before `next`. -- while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { -+ while (next != address(0) && list.accounts[next].value >= value) { -+ list.insertedAfter = next; - next = list.accounts[next].next; -- unchecked { -- ++numberOfIterations; -- } +- uint256 numberOfIterations; +- for (; numberOfIterations < maxIterations; numberOfIterations++) { ++ for (;;) { + if (next == address(0) || list.accounts[next].value < value) break; ++ list.insertedAfter = next; // HARNESS + next = getNext(list, next); } -+ list.insertedBefore = next; -+ - // Account is not the new tail. -- if (numberOfIterations < maxIterations && next != address(0)) { -+ if (next != address(0)) { - // Account is the new head. - if (next == list.head) { - list.accounts[id] = Account({prev: address(0), next: next, value: value}); -diff -ruN MockDLL.sol MockDLL.sol ---- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2023-05-23 16:16:00.233326262 +0200 -@@ -0,0 +1,91 @@ -+// SPDX-License-Identifier: AGPL-3.0-only -+pragma solidity ^0.8.0; -+ -+import "./DoubleLinkedList.sol"; -+ -+contract MockDLL { -+ using DoubleLinkedList for DoubleLinkedList.List; -+ -+ // VERIFICATION INTERFACE -+ -+ DoubleLinkedList.List public dll; -+ -+ uint256 internal dummy_state_variable; -+ -+ function dummy_state_modifying_function() public { -+ // to fix a CVL error when only one function is accessible -+ dummy_state_variable = 1; -+ } -+ -+ function getValueOf(address _id) public view returns (uint256) { -+ return dll.getValueOf(_id); -+ } -+ -+ function getHead() public view returns (address) { -+ return dll.getHead(); -+ } -+ -+ function getTail() public view returns (address) { -+ return dll.getTail(); -+ } -+ -+ function getNext(address _id) public view returns (address) { -+ return dll.getNext(_id); -+ } -+ -+ function getPrev(address _id) public view returns (address) { -+ return dll.getPrev(_id); -+ } -+ -+ function remove(address _id) public { -+ dll.remove(_id); -+ } -+ -+ function insertSorted(address _id, uint256 _value) public { -+ dll.insertSorted(_id, _value); -+ } -+ -+ // SPECIFICATION HELPERS -+ -+ function getInsertedAfter() public view returns (address) { -+ return dll.insertedAfter; -+ } -+ -+ function getInsertedBefore() public view returns (address) { -+ return dll.insertedBefore; -+ } -+ -+ function getLength() internal view returns (uint256) { -+ uint256 len; -+ for (address current = getHead(); current != address(0); current = getNext(current)) len++; -+ return len; -+ } -+ -+ function linkBetween(address _start, address _end) internal view returns (bool, address) { -+ if (_start == _end) return (true, address(0)); -+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { -+ address next = getNext(_start); -+ if (next == _end) return (true, _start); -+ _start = next; -+ } -+ return (false, address(0)); -+ } -+ -+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { -+ (ret, ) = linkBetween(_start, _end); -+ } -+ -+ function getPreceding(address _end) public view returns (address last) { -+ (, last) = linkBetween(getHead(), _end); -+ } -+ -+ function isDecrSortedFrom(address _start) public view returns (bool) { -+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { -+ address next = getNext(_start); -+ if (next == address(0)) return true; -+ if (getValueOf(_start) < getValueOf(next)) return false; -+ _start = getNext(_start); -+ } -+ return true; -+ } -+} +- if (numberOfIterations == maxIterations) next = address(0); ++ list.insertedBefore = next; // HARNESS + + address prev = getPrev(list, next); + list.accounts[id] = Account(prev, next, value); diff --git a/certora/confs/DllFifo.conf b/certora/confs/DllFifo.conf index 9f343df..3b6d13a 100644 --- a/certora/confs/DllFifo.conf +++ b/certora/confs/DllFifo.conf @@ -1,12 +1,12 @@ { - "files": [ - "certora/munged-fifo/MockDLL.sol", - ], - "solc": "solc-0.8.17", - "verify": "MockDLL:certora/specs/DllFifo.spec", - "loop_iter": "4", - "optimistic_loop": true, - "rule_sanity": "basic", - "server": "production", - "msg": "FIFO DLL", + "files": [ + "certora/helpers/MockDllFifo.sol" + ], + "solc": "solc-0.8.17", + "verify": "MockDllFifo:certora/specs/DllFifo.spec", + "loop_iter": "4", + "optimistic_loop": true, + "rule_sanity": "basic", + "server": "production", + "msg": "FIFO DLL" } diff --git a/certora/confs/DllSimple.conf b/certora/confs/DllSimple.conf index 1477691..dd16af5 100644 --- a/certora/confs/DllSimple.conf +++ b/certora/confs/DllSimple.conf @@ -1,12 +1,12 @@ { - "files": [ - "certora/munged-simple/MockDLL.sol", - ], - "solc": "solc-0.8.17", - "verify": "MockDLL:certora/specs/DllSimple.spec", - "loop_iter": "7", - "optimistic_loop": true, - "rule_sanity": "basic", - "server": "production", - "msg": "Simple DLL", + "files": [ + "certora/helpers/MockDllSimple.sol" + ], + "solc": "solc-0.8.17", + "verify": "MockDllSimple:certora/specs/DllSimple.spec", + "loop_iter": "7", + "optimistic_loop": true, + "rule_sanity": "basic", + "server": "production", + "msg": "Simple DLL" } diff --git a/certora/helpers/MockDllFifo.sol b/certora/helpers/MockDllFifo.sol new file mode 100644 index 0000000..2531de0 --- /dev/null +++ b/certora/helpers/MockDllFifo.sol @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import {DoubleLinkedList} from "../munged-fifo/DoubleLinkedList.sol"; + +contract MockDllFifo { + using DoubleLinkedList for DoubleLinkedList.List; + + // VERIFICATION INTERFACE + + DoubleLinkedList.List public dll; + + uint256 public maxIterations; + + function getValueOf(address _id) public view returns (uint256) { + return dll.getValueOf(_id); + } + + function getHead() public view returns (address) { + return dll.getHead(); + } + + function getTail() public view returns (address) { + return dll.getTail(); + } + + function getNext(address _id) public view returns (address) { + return dll.getNext(_id); + } + + function getPrev(address _id) public view returns (address) { + return dll.getPrev(_id); + } + + function remove(address _id) public { + dll.remove(_id); + } + + function insertSorted(address _id, uint256 _value, uint256 _maxIterations) public { + dll.insertSorted(_id, _value, _maxIterations); + } + + // SPECIFICATION HELPERS + + function getInsertedAfter() public view returns (address) { + return dll.insertedAfter; + } + + function getInsertedBefore() public view returns (address) { + return dll.insertedBefore; + } + + function getLength() public view returns (uint256) { + uint256 len; + for (address current = getHead(); current != address(0); current = getNext(current)) { + len++; + } + return len; + } + + function linkBetween(address _start, address _end) internal view returns (bool, address) { + if (_start == _end) return (true, address(0)); + for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { + address next = getNext(_start); + if (next == _end) return (true, _start); + _start = next; + } + return (false, address(0)); + } + + function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { + (ret,) = linkBetween(_start, _end); + } + + function getPreceding(address _end) public view returns (address last) { + (, last) = linkBetween(getHead(), _end); + } + + function greaterThanUpTo(uint256 _value, address _to, uint256 _maxIter) public view returns (bool) { + address from = getHead(); + for (; _maxIter > 0; _maxIter--) { + if (from == _to) return true; + if (getValueOf(from) < _value) return false; + from = getNext(from); + } + return true; + } + + function lenUpTo(address _to) public view returns (uint256) { + uint256 maxIter = getLength(); + address from = getHead(); + for (; maxIter > 0; maxIter--) { + if (from == _to) break; + from = getNext(from); + } + return getLength() - maxIter; + } +} diff --git a/certora/helpers/MockDllSimple.sol b/certora/helpers/MockDllSimple.sol new file mode 100644 index 0000000..376e5d5 --- /dev/null +++ b/certora/helpers/MockDllSimple.sol @@ -0,0 +1,86 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import {DoubleLinkedList} from "../munged-simple/DoubleLinkedList.sol"; + +contract MockDllSimple { + using DoubleLinkedList for DoubleLinkedList.List; + + // VERIFICATION INTERFACE + + DoubleLinkedList.List public dll; + + function getValueOf(address _id) public view returns (uint256) { + return dll.getValueOf(_id); + } + + function getHead() public view returns (address) { + return dll.getHead(); + } + + function getTail() public view returns (address) { + return dll.getTail(); + } + + function getNext(address _id) public view returns (address) { + return dll.getNext(_id); + } + + function getPrev(address _id) public view returns (address) { + return dll.getPrev(_id); + } + + function remove(address _id) public { + dll.remove(_id); + } + + function insertSorted(address _id, uint256 _value) public { + dll.insertSorted(_id, _value); + } + + // SPECIFICATION HELPERS + + function getInsertedAfter() public view returns (address) { + return dll.insertedAfter; + } + + function getInsertedBefore() public view returns (address) { + return dll.insertedBefore; + } + + function getLength() internal view returns (uint256) { + uint256 len; + for (address current = getHead(); current != address(0); current = getNext(current)) { + len++; + } + return len; + } + + function linkBetween(address _start, address _end) internal view returns (bool, address) { + if (_start == _end) return (true, address(0)); + for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { + address next = getNext(_start); + if (next == _end) return (true, _start); + _start = next; + } + return (false, address(0)); + } + + function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { + (ret,) = linkBetween(_start, _end); + } + + function getPreceding(address _end) public view returns (address last) { + (, last) = linkBetween(getHead(), _end); + } + + function isDecrSortedFrom(address _start) public view returns (bool) { + for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { + address next = getNext(_start); + if (next == address(0)) return true; + if (getValueOf(_start) < getValueOf(next)) return false; + _start = getNext(_start); + } + return true; + } +} diff --git a/certora/makefile b/certora/makefile index e22c5bd..f3a1e41 100644 --- a/certora/makefile +++ b/certora/makefile @@ -7,7 +7,7 @@ munged-simple: $(wildcard ../src/*.sol) applyHarnessSimple.patch @patch -p0 -d munged-simple < applyHarnessSimple.patch record-simple: - diff -ruN ../src munged-simple | sed 's+\.\./src/++g' | sed 's+munged-simple/++g' > applyHarnessSimple.patch + diff -ruN ../src munged-simple | sed 's,\.\./src/\|munged-simple/,,g' | sed 's,\(\(\-\-\-\|+++\) [^[:space:]]*\).*,\1,' > applyHarnessSimple.patch munged-fifo: $(wildcard ../src/*.sol) applyHarnessFifo.patch @rm -rf munged-fifo @@ -15,9 +15,9 @@ munged-fifo: $(wildcard ../src/*.sol) applyHarnessFifo.patch @patch -p0 -d munged-fifo < applyHarnessFifo.patch record-fifo: - diff -ruN ../src munged-fifo | sed 's+\.\./src/++g' | sed 's+munged-fifo/++g' > applyHarnessFifo.patch + diff -ruN ../src munged-fifo | sed 's,\.\./src/\|munged-fifo/,,g' | sed 's,\(\(\-\-\-\|+++\) [^[:space:]]*\).*,\1,' > applyHarnessFifo.patch clean: rm -rf munged-simple munged-fifo -.PHONY: help clean # do not add munged here, as it is useful to protect munged edits +.PHONY: help clean record-simple record-fifo # do not add munged folders here, as it is useful to protect munged edits diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index 6f81c7c..f0ce8c3 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -20,32 +20,39 @@ methods { // DEFINITIONS -definition isInDLL(address id) returns bool = +definition isInDll(address id) returns bool = getValueOf(id) != 0; definition isLinked(address id) returns bool = - getPrev(id) != 0 || getNext(id) != 0; + id != 0 && (getPrev(id) != 0 || getNext(id) != 0 || getPrev(0) == id || getNext(0) == id); -definition isEmpty(address id) returns bool = - ! isInDLL(id) && ! isLinked(id); +definition isEmptyEquiv() returns bool = + getNext(0) == 0 <=> getPrev(0) == 0; + +definition isLinkedToZero(address id) returns bool = + isLinked(id) => + (getNext(id) == 0 => getPrev(0) == id) && + (getPrev(id) == 0 => getNext(0) == id); definition isTwoWayLinked(address first, address second) returns bool = - first != 0 && second != 0 => (getNext(first) == second <=> getPrev(second) == first); + (first != 0 => getPrev(second) == first => getNext(first) == second) && + (second != 0 => getNext(first) == second => getPrev(second) == first); definition isHeadWellFormed() returns bool = - getPrev(getHead()) == 0 && (getHead() != 0 => isInDLL(getHead())); + getPrev(getHead()) == 0 && (getHead() != 0 => isInDll(getHead())); definition isTailWellFormed() returns bool = - getNext(getTail()) == 0 && (getTail() != 0 => isInDLL(getTail())); + getNext(getTail()) == 0 && (getTail() != 0 => isInDll(getTail())); definition hasNoPrevIsHead(address addr) returns bool = - isInDLL(addr) && getPrev(addr) == 0 => addr == getHead(); + isInDll(addr) && getPrev(addr) == 0 => addr == getHead(); definition hasNoNextIsTail(address addr) returns bool = - isInDLL(addr) && getNext(addr) == 0 => addr == getTail(); + isInDll(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { - requireInvariant zeroEmpty(); + requireInvariant emptyZero(); + requireInvariant emptyEquiv(); requireInvariant headWellFormed(); requireInvariant tailWellFormed(); requireInvariant tipsZero(); @@ -56,53 +63,95 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). -invariant zeroEmpty() - isEmpty(0) +invariant emptyZero() + ! isInDll(0); + +invariant emptyEquiv() + isEmptyEquiv() + { preserved remove(address id) { + safeAssumptions(); + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +invariant linkedToZero(address addr) + isLinkedToZero(addr) filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant twoWayLinked(0, id); + requireInvariant twoWayLinked(id, 0); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } -rule zeroEmptyPreservedInsertSorted(address id, uint256 value) { - address prev; +rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; - require isEmpty(0); + require isLinkedToZero(addr); + safeAssumptions(); + requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); - requireInvariant noNextIsTail(prev); - requireInvariant tipsZero(); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); insertSorted(id, value, maxIterations()); require prev == getInsertedAfter(); + require next == getInsertedBefore(); - assert isEmpty(0); + assert isLinkedToZero(addr); } invariant headWellFormed() isHeadWellFormed() + filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getNext(id)); + requireInvariant linkedIsInDll(getNext(id)); + requireInvariant linkedToZero(id); } } +rule headWellFormedPreservedInsertSorted(address id, uint256 value) { + address prev; address next; + + require isHeadWellFormed(); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + + insertSorted(id, value, maxIterations()); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isHeadWellFormed(); +} + invariant tailWellFormed() isTailWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getPrev(id)); + requireInvariant linkedIsInDll(getPrev(id)); + requireInvariant linkedToZero(id); } } rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { - address next; address prev; + address prev; address next; require isTailWellFormed(); - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); @@ -117,7 +166,6 @@ rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { invariant tipsZero() getTail() == 0 <=> getHead() == 0 { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant noNextIsTail(id); requireInvariant noPrevIsHead(id); } @@ -135,7 +183,7 @@ invariant noPrevIsHead(address addr) } rule noPrevIsHeadPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoPrevIsHead(addr); @@ -164,7 +212,7 @@ invariant noNextIsTail(address addr) } rule noNextisTailPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoNextIsTail(addr); @@ -181,8 +229,38 @@ rule noNextisTailPreservedInsertSorted(address id, uint256 value) { assert hasNoNextIsTail(addr); } -invariant linkedIsInDLL(address addr) - isLinked(addr) => isInDLL(addr) +invariant inDllIsLinked(address addr) + isInDll(addr) => isLinked(addr) + filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +rule inDllIsLinkedPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; + + require isInDll(addr) => isLinked(addr); + + safeAssumptions(); + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); + + insertSorted(id, value, maxIterations()); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isInDll(addr) => isLinked(addr); +} + +invariant linkedIsInDll(address addr) + isLinked(addr) => isInDll(addr) filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { safeAssumptions(); @@ -192,10 +270,10 @@ invariant linkedIsInDLL(address addr) } rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; - require isLinked(addr) => isInDLL(addr); - require isLinked(getPrev(next)) => isInDLL(getPrev(next)); + require isLinked(addr) => isInDll(addr); + require isLinked(getPrev(next)) => isInDll(getPrev(next)); safeAssumptions(); requireInvariant twoWayLinked(getPrev(next), next); @@ -208,7 +286,7 @@ rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); require next == getInsertedBefore(); - assert isLinked(addr) => isInDLL(addr); + assert isLinked(addr) => isInDll(addr); } invariant twoWayLinked(address first, address second) @@ -222,34 +300,36 @@ invariant twoWayLinked(address first, address second) } rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { - address first; address second; address next; + address first; address second; address prev; address next; require isTwoWayLinked(first, second); require isTwoWayLinked(getPrev(next), next); + require isTwoWayLinked(prev, getNext(prev)); safeAssumptions(); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); insertSorted(id, value, maxIterations()); + require prev == getInsertedAfter(); require next == getInsertedBefore(); assert isTwoWayLinked(first, second); } invariant forwardLinked(address addr) - isInDLL(addr) => isForwardLinkedBetween(getHead(), addr) + isInDll(addr) => isForwardLinkedBetween(getHead(), addr) filtered { f -> f.selector != sig:remove(address).selector && f.selector != sig:insertSorted(address, uint256, uint256).selector } rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { address addr; address prev; - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); - require isInDLL(getTail()) => isForwardLinkedBetween(getHead(), getTail()); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(getTail()) => isForwardLinkedBetween(getHead(), getTail()); safeAssumptions(); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); requireInvariant twoWayLinked(prev, getNext(prev)); requireInvariant noNextIsTail(prev); @@ -257,7 +337,7 @@ rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule forwardLinkedPreservedRemove(address id) { @@ -265,7 +345,7 @@ rule forwardLinkedPreservedRemove(address id) { require prev == getPreceding(id); - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); safeAssumptions(); requireInvariant noPrevIsHead(id); @@ -275,7 +355,7 @@ rule forwardLinkedPreservedRemove(address id) { remove(id); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule removeRemoves(address id) { @@ -283,7 +363,7 @@ rule removeRemoves(address id) { remove(id); - assert !isInDLL(id); + assert !isInDll(id); } rule insertSortedInserts(address id, uint256 value) { @@ -291,7 +371,7 @@ rule insertSortedInserts(address id, uint256 value) { insertSorted(id, value, maxIterations()); - assert isInDLL(id); + assert isInDll(id); } rule insertSortedDecreasingOrder(address id, uint256 value) { @@ -301,25 +381,24 @@ rule insertSortedDecreasingOrder(address id, uint256 value) { safeAssumptions(); requireInvariant twoWayLinked(prev, getNext(prev)); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); insertSorted(id, value, maxIter); require prev == getInsertedAfter(); - uint256 positionInDLL = lenUpTo(id); - - assert positionInDLL > maxIter => greaterThanUpTo(value, 0, maxIter) && id == getTail(); - assert positionInDLL <= maxIter => greaterThanUpTo(value, id, getLength()) && value > getValueOf(getNext(id)); + uint256 positionInDll = lenUpTo(id); + assert positionInDll > maxIter => greaterThanUpTo(value, 0, maxIter) && id == getTail(); + assert positionInDll <= maxIter => greaterThanUpTo(value, id, getLength()) && value > getValueOf(getNext(id)); } // DERIVED RESULTS // result: isForwardLinkedBetween(getHead(), getTail()) -// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows -// otherwise, from tailWellFormed(), we know that isInDLL(getTail()) so the result follows from forwardLinked(getTail()). +// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows. +// Otherwise, from tailWellFormed(), we know that isInDll(getTail()) so the result follows from forwardLinked(getTail()). -// result: forall addr. isForwardLinkedBetween(addr, getTail()) +// result: forall addr. isInDll(addr) => isForwardLinkedBetween(addr, getTail()) // explanation: it can be obtained from the previous result and forwardLinked. // Going from head to tail should lead to addr in between (otherwise addr is never reached because there is nothing after the tail). @@ -330,6 +409,5 @@ rule insertSortedDecreasingOrder(address id, uint256 value) { // explanation: it comes from the fact that every non zero address that is in the DLL is linked to getHead(). // result: there are no cycles that do not contain the 0 address -// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() -// is part of the cycle. This is absurd because we know from headWellFormed() that the previous element of -// getHead() is the 0 address. +// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() is part of the cycle. +// The result follows because we know from headWellFormed() that the previous element of getHead() is the 0 address. diff --git a/certora/specs/DllSimple.spec b/certora/specs/DllSimple.spec index 07ba5cd..c560d07 100644 --- a/certora/specs/DllSimple.spec +++ b/certora/specs/DllSimple.spec @@ -16,32 +16,37 @@ methods { // DEFINITIONS -definition isInDLL(address id) returns bool = +definition isInDll(address id) returns bool = getValueOf(id) != 0; definition isLinked(address id) returns bool = - getPrev(id) != 0 || getNext(id) != 0; + id != 0 && (getPrev(id) != 0 || getNext(id) != 0 || getPrev(0) == id || getNext(0) == id); -definition isEmpty(address id) returns bool = - ! isInDLL(id) && ! isLinked(id); +definition isEmptyEquiv() returns bool = + getNext(0) == 0 <=> getPrev(0) == 0; + +definition isLinkedToZero(address id) returns bool = + isLinked(id) => + (getNext(id) == 0 => getPrev(0) == id) && + (getPrev(id) == 0 => getNext(0) == id); definition isTwoWayLinked(address first, address second) returns bool = - first != 0 && second != 0 => (getNext(first) == second <=> getPrev(second) == first); + (first != 0 => getPrev(second) == first => getNext(first) == second) && + (second != 0 => getNext(first) == second => getPrev(second) == first); definition isHeadWellFormed() returns bool = - getPrev(getHead()) == 0 && (getHead() != 0 => isInDLL(getHead())); + getPrev(getHead()) == 0 && (getHead() != 0 => isInDll(getHead())); definition isTailWellFormed() returns bool = - getNext(getTail()) == 0 && (getTail() != 0 => isInDLL(getTail())); + getNext(getTail()) == 0 && (getTail() != 0 => isInDll(getTail())); definition hasNoPrevIsHead(address addr) returns bool = - isInDLL(addr) && getPrev(addr) == 0 => addr == getHead(); + isInDll(addr) && getPrev(addr) == 0 => addr == getHead(); definition hasNoNextIsTail(address addr) returns bool = - isInDLL(addr) && getNext(addr) == 0 => addr == getTail(); + isInDll(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { - requireInvariant zeroEmpty(); requireInvariant headWellFormed(); requireInvariant tailWellFormed(); requireInvariant tipsZero(); @@ -52,50 +57,94 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). -invariant zeroEmpty() - isEmpty(0) +invariant emptyZero() + ! isInDll(0); + +invariant emptyEquiv() + isEmptyEquiv() + { preserved remove(address id) { + safeAssumptions(); + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +invariant linkedToZero(address addr) + isLinkedToZero(addr) filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant twoWayLinked(0, id); + requireInvariant twoWayLinked(id, 0); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; -rule zeroEmptyPreservedInsertSorted(address id, uint256 value) { - address prev; + require isLinkedToZero(addr); - require isEmpty(0); + requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); - requireInvariant noNextIsTail(prev); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); insertSorted(id, value); require prev == getInsertedAfter(); + require next == getInsertedBefore(); - assert isEmpty(0); + assert isLinkedToZero(addr); } invariant headWellFormed() isHeadWellFormed() + filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getNext(id)); + requireInvariant linkedIsInDll(getNext(id)); + requireInvariant linkedToZero(id); } } +rule headWellFormedPreservedInsertSorted(address id, uint256 value) { + address prev; address next; + + require isHeadWellFormed(); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + + insertSorted(id, value); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isHeadWellFormed(); +} + invariant tailWellFormed() isTailWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getPrev(id)); + requireInvariant linkedIsInDll(getPrev(id)); + requireInvariant linkedToZero(id); } } rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { - address next; address prev; + address prev; address next; require isTailWellFormed(); - requireInvariant zeroEmpty(); + requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); @@ -110,7 +159,6 @@ rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { invariant tipsZero() getTail() == 0 <=> getHead() == 0 { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant noNextIsTail(id); requireInvariant noPrevIsHead(id); } @@ -128,7 +176,7 @@ invariant noPrevIsHead(address addr) } rule noPrevIsHeadPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoPrevIsHead(addr); @@ -157,7 +205,7 @@ invariant noNextIsTail(address addr) } rule noNextisTailPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoNextIsTail(addr); @@ -174,8 +222,37 @@ rule noNextisTailPreservedInsertSorted(address id, uint256 value) { assert hasNoNextIsTail(addr); } -invariant linkedIsInDLL(address addr) - isLinked(addr) => isInDLL(addr) +invariant inDllIsLinked(address addr) + isInDll(addr) => isLinked(addr) + filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +rule inDllIsLinkedPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; + + require isInDll(addr) => isLinked(addr); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); + + insertSorted(id, value); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isInDll(addr) => isLinked(addr); +} + +invariant linkedIsInDll(address addr) + isLinked(addr) => isInDll(addr) filtered { f -> f.selector != sig:insertSorted(address,uint256).selector } { preserved remove(address id) { safeAssumptions(); @@ -185,10 +262,10 @@ invariant linkedIsInDLL(address addr) } rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; - require isLinked(addr) => isInDLL(addr); - require isLinked(getPrev(next)) => isInDLL(getPrev(next)); + require isLinked(addr) => isInDll(addr); + require isLinked(getPrev(next)) => isInDll(getPrev(next)); safeAssumptions(); requireInvariant twoWayLinked(getPrev(next), next); @@ -201,7 +278,7 @@ rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); require next == getInsertedBefore(); - assert isLinked(addr) => isInDLL(addr); + assert isLinked(addr) => isInDll(addr); } invariant twoWayLinked(address first, address second) @@ -215,30 +292,32 @@ invariant twoWayLinked(address first, address second) } rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { - address first; address second; address next; + address first; address second; address prev; address next; require isTwoWayLinked(first, second); require isTwoWayLinked(getPrev(next), next); + require isTwoWayLinked(prev, getNext(prev)); safeAssumptions(); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); insertSorted(id, value); + require prev == getInsertedAfter(); require next == getInsertedBefore(); assert isTwoWayLinked(first, second); } invariant forwardLinked(address addr) - isInDLL(addr) => isForwardLinkedBetween(getHead(), addr) + isInDll(addr) => isForwardLinkedBetween(getHead(), addr) filtered { f -> f.selector != sig:remove(address).selector && f.selector != sig:insertSorted(address, uint256).selector } rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { address addr; address prev; - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); safeAssumptions(); requireInvariant twoWayLinked(prev, getNext(prev)); @@ -248,7 +327,7 @@ rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule forwardLinkedPreservedRemove(address id) { @@ -256,7 +335,7 @@ rule forwardLinkedPreservedRemove(address id) { require prev == getPreceding(id); - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); safeAssumptions(); requireInvariant noPrevIsHead(id); @@ -266,7 +345,7 @@ rule forwardLinkedPreservedRemove(address id) { remove(id); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule removeRemoves(address id) { @@ -274,7 +353,7 @@ rule removeRemoves(address id) { remove(id); - assert !isInDLL(id); + assert !isInDll(id); } rule insertSortedInserts(address id, uint256 value) { @@ -282,7 +361,7 @@ rule insertSortedInserts(address id, uint256 value) { insertSorted(id, value); - assert isInDLL(id); + assert isInDll(id); } invariant decrSorted() @@ -297,10 +376,10 @@ invariant decrSorted() // DERIVED RESULTS // result: isForwardLinkedBetween(getHead(), getTail()) -// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows -// otherwise, from tailWellFormed(), we know that isInDLL(getTail()) so the result follows from forwardLinked(getTail()). +// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows. +// Otherwise, from tailWellFormed(), we know that isInDll(getTail()) so the result follows from forwardLinked(getTail()). -// result: forall addr. isForwardLinkedBetween(addr, getTail()) +// result: forall addr. isInDll(addr) => isForwardLinkedBetween(addr, getTail()) // explanation: it can be obtained from the previous result and forwardLinked. // Going from head to tail should lead to addr in between (otherwise addr is never reached because there is nothing after the tail). @@ -311,6 +390,5 @@ invariant decrSorted() // explanation: it comes from the fact that every non zero address that is in the DLL is linked to getHead(). // result: there are no cycles that do not contain the 0 address -// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() -// is part of the cycle. This is absurd because we know from headWellFormed() that the previous element of -// getHead() is the 0 address. +// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() is part of the cycle. +// The result follows because we know from headWellFormed() that the previous element of getHead() is the 0 address. diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol index ef931a3..009e94f 100644 --- a/src/DoubleLinkedList.sol +++ b/src/DoubleLinkedList.sol @@ -16,8 +16,6 @@ library DoubleLinkedList { struct List { mapping(address => Account) accounts; - address head; - address tail; } /* ERRORS */ @@ -36,7 +34,7 @@ library DoubleLinkedList { /* INTERNAL */ - /// @notice Returns the `account` linked to `id`. + /// @notice Returns the value of the account linked to `id`. /// @param list The list to search in. /// @param id The address of the account. /// @return The value of the account. @@ -48,14 +46,14 @@ library DoubleLinkedList { /// @param list The list to get the head. /// @return The address of the head. function getHead(List storage list) internal view returns (address) { - return list.head; + return list.accounts[address(0)].next; } /// @notice Returns the address at the tail of the `list`. /// @param list The list to get the tail. /// @return The address of the tail. function getTail(List storage list) internal view returns (address) { - return list.tail; + return list.accounts[address(0)].prev; } /// @notice Returns the next id address from the current `id`. @@ -79,12 +77,11 @@ library DoubleLinkedList { /// @param id The address of the account. function remove(List storage list, address id) internal { Account memory account = list.accounts[id]; + if (id == address(0)) revert AddressIsZero(); if (account.value == 0) revert AccountDoesNotExist(); - if (account.prev != address(0)) list.accounts[account.prev].next = account.next; - else list.head = account.next; - if (account.next != address(0)) list.accounts[account.next].prev = account.prev; - else list.tail = account.prev; + list.accounts[account.prev].next = account.next; + list.accounts[account.next].prev = account.prev; delete list.accounts[id]; } @@ -99,47 +96,19 @@ library DoubleLinkedList { if (id == address(0)) revert AddressIsZero(); if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); - uint256 numberOfIterations; - address next = list.head; // If not added at the end of the list `id` will be inserted before `next`. + address next = getHead(list); // `id` will be inserted before `next`. - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { - next = list.accounts[next].next; - unchecked { - ++numberOfIterations; - } + uint256 numberOfIterations; + for (; numberOfIterations < maxIterations; numberOfIterations++) { + if (next == address(0) || list.accounts[next].value < value) break; + next = getNext(list, next); } - // Account is not the new tail. - if (numberOfIterations < maxIterations && next != address(0)) { - // Account is the new head. - if (next == list.head) { - list.accounts[id] = Account({prev: address(0), next: next, value: value}); - list.head = id; - list.accounts[next].prev = id; - } - // Account is not the new head. - else { - address prev = list.accounts[next].prev; - list.accounts[id] = Account({prev: prev, next: next, value: value}); - list.accounts[prev].next = id; - list.accounts[next].prev = id; - } - } - // Account is the new tail. - else { - // Account is the new head. - if (list.head == address(0)) { - list.accounts[id] = Account({prev: address(0), next: address(0), value: value}); - list.head = id; - list.tail = id; - } - // Account is not the new head. - else { - address tail = list.tail; - list.accounts[id] = Account({prev: tail, next: address(0), value: value}); - list.accounts[tail].next = id; - list.tail = id; - } - } + if (numberOfIterations == maxIterations) next = address(0); + + address prev = getPrev(list, next); + list.accounts[id] = Account(prev, next, value); + list.accounts[prev].next = id; + list.accounts[next].prev = id; } } diff --git a/test/TestDoubleLinkedList.t.sol b/test/TestDoubleLinkedList.t.sol index f746022..9457d8a 100644 --- a/test/TestDoubleLinkedList.t.sol +++ b/test/TestDoubleLinkedList.t.sol @@ -11,7 +11,7 @@ contract TestDoubleLinkedList is Test { address[] public accounts; address public ADDR_ZERO = address(0); - DoubleLinkedList.List public list; + DoubleLinkedList.List internal list; function setUp() public { accounts = new address[](NDS);