refactor: minimize munging

morpho-org · Jul 11, 2024 · fe1d00f · fe1d00f
1 parent dfba522
commit fe1d00f
Show file tree

Hide file tree

Showing 6 changed files with 202 additions and 214 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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;
+    }
+}