From fe1d00f941d206287b4dcd2baa84d7231353b84c Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 13:31:29 +0200 Subject: [PATCH] refactor: minimize munging --- certora/applyHarnessFifo.patch | 115 ------------------------------ certora/applyHarnessSimple.patch | 95 ------------------------ certora/confs/DllFifo.conf | 4 +- certora/confs/DllSimple.conf | 4 +- certora/helpers/MockDllFifo.sol | 105 +++++++++++++++++++++++++++ certora/helpers/MockDllSimple.sol | 93 ++++++++++++++++++++++++ 6 files changed, 202 insertions(+), 214 deletions(-) create mode 100644 certora/helpers/MockDllFifo.sol create mode 100644 certora/helpers/MockDllSimple.sol diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index d0e4042..8222e01 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -26,118 +26,3 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol address prev = list.accounts[next].prev; list.accounts[id] = Account(prev, next, value); -diff -ruN MockDLL.sol MockDLL.sol ---- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2024-07-11 10:58:47.037997151 +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; -+ } -+} diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index fa62a59..fa8d984 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -39,98 +39,3 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol address prev = list.accounts[next].prev; list.accounts[id] = Account(prev, next, value); -diff -ruN MockDLL.sol MockDLL.sol ---- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2024-07-11 12:42:15.108949766 +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; -+ } -+} diff --git a/certora/confs/DllFifo.conf b/certora/confs/DllFifo.conf index 9f343df..1bc933d 100644 --- a/certora/confs/DllFifo.conf +++ b/certora/confs/DllFifo.conf @@ -1,9 +1,9 @@ { "files": [ - "certora/munged-fifo/MockDLL.sol", + "certora/helpers/MockDllFifo.sol", ], "solc": "solc-0.8.17", - "verify": "MockDLL:certora/specs/DllFifo.spec", + "verify": "MockDllFifo:certora/specs/DllFifo.spec", "loop_iter": "4", "optimistic_loop": true, "rule_sanity": "basic", diff --git a/certora/confs/DllSimple.conf b/certora/confs/DllSimple.conf index 1477691..c099557 100644 --- a/certora/confs/DllSimple.conf +++ b/certora/confs/DllSimple.conf @@ -1,9 +1,9 @@ { "files": [ - "certora/munged-simple/MockDLL.sol", + "certora/helpers/MockDllSimple.sol", ], "solc": "solc-0.8.17", - "verify": "MockDLL:certora/specs/DllSimple.spec", + "verify": "MockDllSimple:certora/specs/DllSimple.spec", "loop_iter": "7", "optimistic_loop": true, "rule_sanity": "basic", diff --git a/certora/helpers/MockDllFifo.sol b/certora/helpers/MockDllFifo.sol new file mode 100644 index 0000000..26cc3b4 --- /dev/null +++ b/certora/helpers/MockDllFifo.sol @@ -0,0 +1,105 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import "../munged-fifo/DoubleLinkedList.sol"; + +contract MockDllFifo { + 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; + } +} diff --git a/certora/helpers/MockDllSimple.sol b/certora/helpers/MockDllSimple.sol new file mode 100644 index 0000000..a835202 --- /dev/null +++ b/certora/helpers/MockDllSimple.sol @@ -0,0 +1,93 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import "../munged-simple/DoubleLinkedList.sol"; + +contract MockDllSimple { + 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; + } +}