Skip to content

Commit 7334fb5

Browse files
QGarcheryQGarchery
authored
Merge pull request #141 from morpho-org/refactor/loop-dll
DLL loops to address(0)
2 parents f1197b3 + ed091a1 commit 7334fb5

File tree

11 files changed

+514
-428
lines changed

11 files changed

+514
-428
lines changed

‎certora/applyHarnessFifo.patch‎

Lines changed: 13 additions & 134 deletions
Original file line numberDiff line numberDiff line change
@@ -1,146 +1,25 @@
11
diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
2-
--- DoubleLinkedList.sol 2023-05-23 16:01:50.888803463 +0200
3-
+++ DoubleLinkedList.sol 2023-05-23 16:44:01.777091764 +0200
4-
@@ -18,6 +18,8 @@
2+
--- DoubleLinkedList.sol
3+
+++ DoubleLinkedList.sol
4+
@@ -16,6 +16,8 @@
5+
6+
struct List {
57
mapping(address => Account) accounts;
6-
address head;
7-
address tail;
88
+ address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion.
99
+ address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion.
1010
}
1111

1212
/* ERRORS */
13-
@@ -101,14 +103,18 @@
14-
13+
@@ -101,10 +103,12 @@
1514
uint256 numberOfIterations;
16-
address next = list.head; // If not added at the end of the list `id` will be inserted before `next`.
17-
+ list.insertedAfter = address(0); // HARNESS
18-
19-
while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) {
15+
for (; numberOfIterations < maxIterations; numberOfIterations++) {
16+
if (next == address(0) || list.accounts[next].value < value) break;
2017
+ list.insertedAfter = next; // HARNESS
21-
next = list.accounts[next].next;
22-
unchecked {
23-
++numberOfIterations;
24-
}
18+
next = getNext(list, next);
2519
}
2620

21+
if (numberOfIterations == maxIterations) next = address(0);
2722
+ list.insertedBefore = next; // HARNESS
28-
+
29-
// Account is not the new tail.
30-
if (numberOfIterations < maxIterations && next != address(0)) {
31-
// Account is the new head.
32-
diff -ruN MockDLL.sol MockDLL.sol
33-
--- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100
34-
+++ MockDLL.sol 2023-05-23 16:42:32.913885637 +0200
35-
@@ -0,0 +1,111 @@
36-
+// SPDX-License-Identifier: AGPL-3.0-only
37-
+pragma solidity ^0.8.0;
38-
+
39-
+import "./DoubleLinkedList.sol";
40-
+
41-
+contract MockDLL {
42-
+ using DoubleLinkedList for DoubleLinkedList.List;
43-
+
44-
+ // VERIFICATION INTERFACE
45-
+
46-
+ DoubleLinkedList.List public dll;
47-
+
48-
+ uint256 public maxIterations;
49-
+
50-
+ uint256 internal dummy_state_variable;
51-
+
52-
+ function dummy_state_modifying_function() public {
53-
+ // to fix a CVL error when only one function is accessible
54-
+ dummy_state_variable = 1;
55-
+ }
56-
+
57-
+ function getValueOf(address _id) public view returns (uint256) {
58-
+ return dll.getValueOf(_id);
59-
+ }
60-
+
61-
+ function getHead() public view returns (address) {
62-
+ return dll.getHead();
63-
+ }
64-
+
65-
+ function getTail() public view returns (address) {
66-
+ return dll.getTail();
67-
+ }
68-
+
69-
+ function getNext(address _id) public view returns (address) {
70-
+ return dll.getNext(_id);
71-
+ }
72-
+
73-
+ function getPrev(address _id) public view returns (address) {
74-
+ return dll.getPrev(_id);
75-
+ }
76-
+
77-
+ function remove(address _id) public {
78-
+ dll.remove(_id);
79-
+ }
80-
+
81-
+ function insertSorted(
82-
+ address _id,
83-
+ uint256 _value,
84-
+ uint256 _maxIterations
85-
+ ) public {
86-
+ dll.insertSorted(_id, _value, _maxIterations);
87-
+ }
88-
+
89-
+ // SPECIFICATION HELPERS
90-
+
91-
+ function getInsertedAfter() public view returns (address) {
92-
+ return dll.insertedAfter;
93-
+ }
94-
+
95-
+ function getInsertedBefore() public view returns (address) {
96-
+ return dll.insertedBefore;
97-
+ }
98-
+
99-
+ function getLength() public view returns (uint256) {
100-
+ uint256 len;
101-
+ for (address current = getHead(); current != address(0); current = getNext(current)) len++;
102-
+ return len;
103-
+ }
104-
+
105-
+ function linkBetween(address _start, address _end) internal view returns (bool, address) {
106-
+ if (_start == _end) return (true, address(0));
107-
+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) {
108-
+ address next = getNext(_start);
109-
+ if (next == _end) return (true, _start);
110-
+ _start = next;
111-
+ }
112-
+ return (false, address(0));
113-
+ }
114-
+
115-
+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) {
116-
+ (ret, ) = linkBetween(_start, _end);
117-
+ }
118-
+
119-
+ function getPreceding(address _end) public view returns (address last) {
120-
+ (, last) = linkBetween(getHead(), _end);
121-
+ }
122-
+
123-
+ function greaterThanUpTo(
124-
+ uint256 _value,
125-
+ address _to,
126-
+ uint256 _maxIter
127-
+ ) public view returns (bool) {
128-
+ address from = getHead();
129-
+ for (; _maxIter > 0; _maxIter--) {
130-
+ if (from == _to) return true;
131-
+ if (getValueOf(from) < _value) return false;
132-
+ from = getNext(from);
133-
+ }
134-
+ return true;
135-
+ }
136-
+
137-
+ function lenUpTo(address _to) public view returns (uint256) {
138-
+ uint256 maxIter = getLength();
139-
+ address from = getHead();
140-
+ for (; maxIter > 0; maxIter--) {
141-
+ if (from == _to) break;
142-
+ from = getNext(from);
143-
+ }
144-
+ return getLength() - maxIter;
145-
+ }
146-
+}
23+
24+
address prev = getPrev(list, next);
25+
list.accounts[id] = Account(prev, next, value);

‎certora/applyHarnessSimple.patch‎

Lines changed: 18 additions & 120 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
2-
--- DoubleLinkedList.sol 2023-05-23 16:01:50.888803463 +0200
3-
+++ DoubleLinkedList.sol 2023-05-23 16:34:10.324900474 +0200
4-
@@ -18,6 +18,8 @@
2+
--- DoubleLinkedList.sol
3+
+++ DoubleLinkedList.sol
4+
@@ -16,6 +16,8 @@
5+
6+
struct List {
57
mapping(address => Account) accounts;
6-
address head;
7-
address tail;
88
+ address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion.
99
+ address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion.
1010
}
1111

1212
/* ERRORS */
13-
@@ -93,24 +95,23 @@
13+
@@ -90,21 +92,20 @@
1414
/// @param list The list to search in.
1515
/// @param id The address of the account.
1616
/// @param value The value of the account.
@@ -21,120 +21,18 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
2121
if (id == address(0)) revert AddressIsZero();
2222
if (list.accounts[id].value != 0) revert AccountAlreadyInserted();
2323

24-
- uint256 numberOfIterations;
25-
- address next = list.head; // If not added at the end of the list `id` will be inserted before `next`.
26-
+ list.insertedAfter = address(0);
27-
+ address next = list.head; // `id` will be inserted before `next`.
24+
address next = getHead(list); // `id` will be inserted before `next`.
2825

29-
- while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) {
30-
+ while (next != address(0) && list.accounts[next].value >= value) {
31-
+ list.insertedAfter = next;
32-
next = list.accounts[next].next;
33-
- unchecked {
34-
- ++numberOfIterations;
35-
- }
26+
- uint256 numberOfIterations;
27+
- for (; numberOfIterations < maxIterations; numberOfIterations++) {
28+
+ for (;;) {
29+
if (next == address(0) || list.accounts[next].value < value) break;
30+
+ list.insertedAfter = next; // HARNESS
31+
next = getNext(list, next);
3632
}
3733

38-
+ list.insertedBefore = next;
39-
+
40-
// Account is not the new tail.
41-
- if (numberOfIterations < maxIterations && next != address(0)) {
42-
+ if (next != address(0)) {
43-
// Account is the new head.
44-
if (next == list.head) {
45-
list.accounts[id] = Account({prev: address(0), next: next, value: value});
46-
diff -ruN MockDLL.sol MockDLL.sol
47-
--- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100
48-
+++ MockDLL.sol 2023-05-23 16:16:00.233326262 +0200
49-
@@ -0,0 +1,91 @@
50-
+// SPDX-License-Identifier: AGPL-3.0-only
51-
+pragma solidity ^0.8.0;
52-
+
53-
+import "./DoubleLinkedList.sol";
54-
+
55-
+contract MockDLL {
56-
+ using DoubleLinkedList for DoubleLinkedList.List;
57-
+
58-
+ // VERIFICATION INTERFACE
59-
+
60-
+ DoubleLinkedList.List public dll;
61-
+
62-
+ uint256 internal dummy_state_variable;
63-
+
64-
+ function dummy_state_modifying_function() public {
65-
+ // to fix a CVL error when only one function is accessible
66-
+ dummy_state_variable = 1;
67-
+ }
68-
+
69-
+ function getValueOf(address _id) public view returns (uint256) {
70-
+ return dll.getValueOf(_id);
71-
+ }
72-
+
73-
+ function getHead() public view returns (address) {
74-
+ return dll.getHead();
75-
+ }
76-
+
77-
+ function getTail() public view returns (address) {
78-
+ return dll.getTail();
79-
+ }
80-
+
81-
+ function getNext(address _id) public view returns (address) {
82-
+ return dll.getNext(_id);
83-
+ }
84-
+
85-
+ function getPrev(address _id) public view returns (address) {
86-
+ return dll.getPrev(_id);
87-
+ }
88-
+
89-
+ function remove(address _id) public {
90-
+ dll.remove(_id);
91-
+ }
92-
+
93-
+ function insertSorted(address _id, uint256 _value) public {
94-
+ dll.insertSorted(_id, _value);
95-
+ }
96-
+
97-
+ // SPECIFICATION HELPERS
98-
+
99-
+ function getInsertedAfter() public view returns (address) {
100-
+ return dll.insertedAfter;
101-
+ }
102-
+
103-
+ function getInsertedBefore() public view returns (address) {
104-
+ return dll.insertedBefore;
105-
+ }
106-
+
107-
+ function getLength() internal view returns (uint256) {
108-
+ uint256 len;
109-
+ for (address current = getHead(); current != address(0); current = getNext(current)) len++;
110-
+ return len;
111-
+ }
112-
+
113-
+ function linkBetween(address _start, address _end) internal view returns (bool, address) {
114-
+ if (_start == _end) return (true, address(0));
115-
+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) {
116-
+ address next = getNext(_start);
117-
+ if (next == _end) return (true, _start);
118-
+ _start = next;
119-
+ }
120-
+ return (false, address(0));
121-
+ }
122-
+
123-
+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) {
124-
+ (ret, ) = linkBetween(_start, _end);
125-
+ }
126-
+
127-
+ function getPreceding(address _end) public view returns (address last) {
128-
+ (, last) = linkBetween(getHead(), _end);
129-
+ }
130-
+
131-
+ function isDecrSortedFrom(address _start) public view returns (bool) {
132-
+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) {
133-
+ address next = getNext(_start);
134-
+ if (next == address(0)) return true;
135-
+ if (getValueOf(_start) < getValueOf(next)) return false;
136-
+ _start = getNext(_start);
137-
+ }
138-
+ return true;
139-
+ }
140-
+}
34+
- if (numberOfIterations == maxIterations) next = address(0);
35+
+ list.insertedBefore = next; // HARNESS
36+
37+
address prev = getPrev(list, next);
38+
list.accounts[id] = Account(prev, next, value);

‎certora/confs/DllFifo.conf‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
{
2-
"files": [
3-
"certora/munged-fifo/MockDLL.sol",
4-
],
5-
"solc": "solc-0.8.17",
6-
"verify": "MockDLL:certora/specs/DllFifo.spec",
7-
"loop_iter": "4",
8-
"optimistic_loop": true,
9-
"rule_sanity": "basic",
10-
"server": "production",
11-
"msg": "FIFO DLL",
2+
"files": [
3+
"certora/helpers/MockDllFifo.sol"
4+
],
5+
"solc": "solc-0.8.17",
6+
"verify": "MockDllFifo:certora/specs/DllFifo.spec",
7+
"loop_iter": "4",
8+
"optimistic_loop": true,
9+
"rule_sanity": "basic",
10+
"server": "production",
11+
"msg": "FIFO DLL"
1212
}

‎certora/confs/DllSimple.conf‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
{
2-
"files": [
3-
"certora/munged-simple/MockDLL.sol",
4-
],
5-
"solc": "solc-0.8.17",
6-
"verify": "MockDLL:certora/specs/DllSimple.spec",
7-
"loop_iter": "7",
8-
"optimistic_loop": true,
9-
"rule_sanity": "basic",
10-
"server": "production",
11-
"msg": "Simple DLL",
2+
"files": [
3+
"certora/helpers/MockDllSimple.sol"
4+
],
5+
"solc": "solc-0.8.17",
6+
"verify": "MockDllSimple:certora/specs/DllSimple.spec",
7+
"loop_iter": "7",
8+
"optimistic_loop": true,
9+
"rule_sanity": "basic",
10+
"server": "production",
11+
"msg": "Simple DLL"
1212
}

0 commit comments

Comments
 (0)