Skip to content
This repository was archived by the owner on Dec 17, 2025. It is now read-only.

Commit 8c19f7d

Browse files
QGarcheryQGarchery
authored
Merge pull request #100 from morpho-dao/test/certora-3
Certora verification of the DLL
2 parents a6b4829 + 1f83dd8 commit 8c19f7d

12 files changed

Lines changed: 1054 additions & 9 deletions

‎.gitignore‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,3 +33,10 @@ yarn-error.log*
3333
# test
3434
/test-ts/output-tree-structure.txt
3535
*.ansi
36+
37+
#certora
38+
certora/munged-simple/*
39+
certora/munged-fifo/*
40+
.certora*
41+
last_conf*
42+
certora_debug_log.txt

‎certora/applyHarnessFIFO.patch‎

Lines changed: 150 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,150 @@
1+
diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
2+
--- DoubleLinkedList.sol 2022-12-16 20:15:34.039800632 +0100
3+
+++ DoubleLinkedList.sol 2022-12-16 20:33:41.874106437 +0100
4+
@@ -18,6 +18,8 @@
5+
mapping(address => Account) accounts;
6+
address head;
7+
address tail;
8+
+ address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion.
9+
+ address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion.
10+
}
11+
12+
/// ERRORS ///
13+
@@ -106,18 +108,22 @@
14+
15+
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 (
20+
numberOfIterations < _maxIterations &&
21+
next != address(0) &&
22+
_list.accounts[next].value >= _value
23+
) {
24+
+ _list.insertedAfter = next; // HARNESS
25+
next = _list.accounts[next].next;
26+
unchecked {
27+
++numberOfIterations;
28+
}
29+
}
30+
31+
+ _list.insertedBefore = next; // HARNESS
32+
+
33+
// Account is not the new tail.
34+
if (numberOfIterations < _maxIterations && next != address(0)) {
35+
// Account is the new head.
36+
diff -ruN MockDLL.sol MockDLL.sol
37+
--- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100
38+
+++ MockDLL.sol 2022-12-16 20:35:27.432652652 +0100
39+
@@ -0,0 +1,111 @@
40+
+// SPDX-License-Identifier: GNU AGPLv3
41+
+pragma solidity ^0.8.0;
42+
+
43+
+import "./DoubleLinkedList.sol";
44+
+
45+
+contract MockDLL {
46+
+ using DoubleLinkedList for DoubleLinkedList.List;
47+
+
48+
+ // VERIFICATION INTERFACE
49+
+
50+
+ DoubleLinkedList.List public dll;
51+
+
52+
+ uint256 public maxIterations;
53+
+
54+
+ uint256 internal dummy_state_variable;
55+
+
56+
+ function dummy_state_modifying_function() public {
57+
+ // to fix a CVL error when only one function is accessible
58+
+ dummy_state_variable = 1;
59+
+ }
60+
+
61+
+ function getValueOf(address _id) public view returns (uint256) {
62+
+ return dll.getValueOf(_id);
63+
+ }
64+
+
65+
+ function getHead() public view returns (address) {
66+
+ return dll.getHead();
67+
+ }
68+
+
69+
+ function getTail() public view returns (address) {
70+
+ return dll.getTail();
71+
+ }
72+
+
73+
+ function getNext(address _id) public view returns (address) {
74+
+ return dll.getNext(_id);
75+
+ }
76+
+
77+
+ function getPrev(address _id) public view returns (address) {
78+
+ return dll.getPrev(_id);
79+
+ }
80+
+
81+
+ function remove(address _id) public {
82+
+ dll.remove(_id);
83+
+ }
84+
+
85+
+ function insertSorted(
86+
+ address _id,
87+
+ uint256 _value,
88+
+ uint256 _maxIterations
89+
+ ) public {
90+
+ dll.insertSorted(_id, _value, _maxIterations);
91+
+ }
92+
+
93+
+ // SPECIFICATION HELPERS
94+
+
95+
+ function getInsertedAfter() public view returns (address) {
96+
+ return dll.insertedAfter;
97+
+ }
98+
+
99+
+ function getInsertedBefore() public view returns (address) {
100+
+ return dll.insertedBefore;
101+
+ }
102+
+
103+
+ function getLength() public view returns (uint256) {
104+
+ uint256 len;
105+
+ for (address current = getHead(); current != address(0); current = getNext(current)) len++;
106+
+ return len;
107+
+ }
108+
+
109+
+ function linkBetween(address _start, address _end) internal view returns (bool, address) {
110+
+ if (_start == _end) return (true, address(0));
111+
+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) {
112+
+ address next = getNext(_start);
113+
+ if (next == _end) return (true, _start);
114+
+ _start = next;
115+
+ }
116+
+ return (false, address(0));
117+
+ }
118+
+
119+
+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) {
120+
+ (ret, ) = linkBetween(_start, _end);
121+
+ }
122+
+
123+
+ function getPreceding(address _end) public view returns (address last) {
124+
+ (, last) = linkBetween(getHead(), _end);
125+
+ }
126+
+
127+
+ function greaterThanUpTo(
128+
+ uint256 _value,
129+
+ address _to,
130+
+ uint256 _maxIter
131+
+ ) public view returns (bool) {
132+
+ address from = getHead();
133+
+ for (; _maxIter > 0; _maxIter--) {
134+
+ if (from == _to) return true;
135+
+ if (getValueOf(from) < _value) return false;
136+
+ from = getNext(from);
137+
+ }
138+
+ return true;
139+
+ }
140+
+
141+
+ function lenUpTo(address _to) public view returns (uint256) {
142+
+ uint256 maxIter = getLength();
143+
+ address from = getHead();
144+
+ for (; maxIter > 0; maxIter--) {
145+
+ if (from == _to) break;
146+
+ from = getNext(from);
147+
+ }
148+
+ return getLength() - maxIter;
149+
+ }
150+
+}

‎certora/applyHarnessSimple.patch‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
2+
--- DoubleLinkedList.sol 2022-10-25 18:11:24.798784245 +0200
3+
+++ DoubleLinkedList.sol 2022-11-11 11:24:29.066289033 +0100
4+
@@ -18,6 +18,8 @@
5+
mapping(address => Account) accounts;
6+
address head;
7+
address tail;
8+
+ address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion.
9+
+ address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion.
10+
}
11+
12+
/// ERRORS ///
13+
@@ -93,33 +95,27 @@
14+
/// @param _list The list to search in.
15+
/// @param _id The address of the account.
16+
/// @param _value The value of the account.
17+
- /// @param _maxIterations The max number of iterations.
18+
function insertSorted(
19+
List storage _list,
20+
address _id,
21+
- uint256 _value,
22+
- uint256 _maxIterations
23+
+ uint256 _value
24+
) internal {
25+
if (_value == 0) revert ValueIsZero();
26+
if (_id == address(0)) revert AddressIsZero();
27+
if (_list.accounts[_id].value != 0) revert AccountAlreadyInserted();
28+
29+
- uint256 numberOfIterations;
30+
- address next = _list.head; // If not added at the end of the list `_id` will be inserted before `next`.
31+
+ _list.insertedAfter = address(0);
32+
+ address next = _list.head; // `_id` will be inserted before `next`.
33+
34+
- while (
35+
- numberOfIterations < _maxIterations &&
36+
- next != address(0) &&
37+
- _list.accounts[next].value >= _value
38+
- ) {
39+
+ while (next != address(0) && _list.accounts[next].value >= _value) {
40+
+ _list.insertedAfter = next;
41+
next = _list.accounts[next].next;
42+
- unchecked {
43+
- ++numberOfIterations;
44+
- }
45+
}
46+
47+
+ _list.insertedBefore = next;
48+
+
49+
// Account is not the new tail.
50+
- if (numberOfIterations < _maxIterations && next != address(0)) {
51+
+ if (next != address(0)) {
52+
// Account is the new head.
53+
if (next == _list.head) {
54+
_list.accounts[_id] = Account({prev: address(0), next: next, value: _value});
55+
diff -ruN MockDLL.sol MockDLL.sol
56+
--- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100
57+
+++ MockDLL.sol 2022-11-11 11:27:17.368989154 +0100
58+
@@ -0,0 +1,91 @@
59+
+// SPDX-License-Identifier: GNU AGPLv3
60+
+pragma solidity ^0.8.0;
61+
+
62+
+import "./DoubleLinkedList.sol";
63+
+
64+
+contract MockDLL {
65+
+ using DoubleLinkedList for DoubleLinkedList.List;
66+
+
67+
+ // VERIFICATION INTERFACE
68+
+
69+
+ DoubleLinkedList.List public dll;
70+
+
71+
+ uint256 internal dummy_state_variable;
72+
+
73+
+ function dummy_state_modifying_function() public {
74+
+ // to fix a CVL error when only one function is accessible
75+
+ dummy_state_variable = 1;
76+
+ }
77+
+
78+
+ function getValueOf(address _id) public view returns (uint256) {
79+
+ return dll.getValueOf(_id);
80+
+ }
81+
+
82+
+ function getHead() public view returns (address) {
83+
+ return dll.getHead();
84+
+ }
85+
+
86+
+ function getTail() public view returns (address) {
87+
+ return dll.getTail();
88+
+ }
89+
+
90+
+ function getNext(address _id) public view returns (address) {
91+
+ return dll.getNext(_id);
92+
+ }
93+
+
94+
+ function getPrev(address _id) public view returns (address) {
95+
+ return dll.getPrev(_id);
96+
+ }
97+
+
98+
+ function remove(address _id) public {
99+
+ dll.remove(_id);
100+
+ }
101+
+
102+
+ function insertSorted(address _id, uint256 _value) public {
103+
+ dll.insertSorted(_id, _value);
104+
+ }
105+
+
106+
+ // SPECIFICATION HELPERS
107+
+
108+
+ function getInsertedAfter() public view returns (address) {
109+
+ return dll.insertedAfter;
110+
+ }
111+
+
112+
+ function getInsertedBefore() public view returns (address) {
113+
+ return dll.insertedBefore;
114+
+ }
115+
+
116+
+ function getLength() internal view returns (uint256) {
117+
+ uint256 len;
118+
+ for (address current = getHead(); current != address(0); current = getNext(current)) len++;
119+
+ return len;
120+
+ }
121+
+
122+
+ function linkBetween(address _start, address _end) internal view returns (bool, address) {
123+
+ if (_start == _end) return (true, address(0));
124+
+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) {
125+
+ address next = getNext(_start);
126+
+ if (next == _end) return (true, _start);
127+
+ _start = next;
128+
+ }
129+
+ return (false, address(0));
130+
+ }
131+
+
132+
+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) {
133+
+ (ret, ) = linkBetween(_start, _end);
134+
+ }
135+
+
136+
+ function getPreceding(address _end) public view returns (address last) {
137+
+ (, last) = linkBetween(getHead(), _end);
138+
+ }
139+
+
140+
+ function isDecrSortedFrom(address _start) public view returns (bool) {
141+
+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) {
142+
+ address next = getNext(_start);
143+
+ if (next == address(0)) return true;
144+
+ if (getValueOf(_start) < getValueOf(next)) return false;
145+
+ _start = getNext(_start);
146+
+ }
147+
+ return true;
148+
+ }
149+
+}

‎certora/makefile‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
help:
2+
@echo "usage: two possible munging, either simple DLL of DLL with FIFO"
3+
4+
munged-simple: $(wildcard ../src/*.sol) applyHarnessSimple.patch
5+
@rm -rf munged-simple
6+
@cp -r ../src munged-simple
7+
@patch -p0 -d munged-simple < applyHarnessSimple.patch
8+
9+
record-simple:
10+
diff -ruN ../contracts munged-simple | sed 's+\.\./src/++g' | sed 's+munged-simple/++g' > applyHarnessSimple.patch
11+
12+
munged-fifo: $(wildcard ../src/*.sol) applyHarnessFIFO.patch
13+
@rm -rf munged-fifo
14+
@cp -r ../src munged-fifo
15+
@patch -p0 -d munged-fifo < applyHarnessFIFO.patch
16+
17+
record-fifo:
18+
diff -ruN ../src munged-fifo | sed 's+\.\./src/++g' | sed 's+munged-fifo/++g' > applyHarnessFIFO.patch
19+
20+
clean:
21+
rm -rf munged-simple munged-fifo
22+
23+
.PHONY: help clean # do not add munged here, as it is useful to protect munged edits

‎certora/scripts/dll-fifo.sh‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#!/bin/sh
2+
3+
make -C certora munged-fifo
4+
5+
certoraRun \
6+
certora/munged-fifo/MockDLL.sol \
7+
--verify MockDLL:certora/specs/dll-fifo.spec \
8+
--loop_iter 4 \
9+
--optimistic_loop \
10+
--send_only \
11+
--msg "FIFO DLL verification" \
12+
--staging \
13+
$@

‎certora/scripts/dll-simple.sh‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#!/bin/sh
2+
3+
make -C certora munged-simple
4+
5+
certoraRun \
6+
certora/munged-simple/MockDLL.sol \
7+
--verify MockDLL:certora/specs/dll-simple.spec \
8+
--loop_iter 7 \
9+
--optimistic_loop \
10+
--send_only \
11+
--msg "Simple DLL verification" \
12+
--staging \
13+
$@

‎certora/scripts/sanity-fifo.sh‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#!/bin/sh
2+
3+
make -C certora munged-fifo
4+
5+
certoraRun \
6+
certora/munged-fifo/MockDLL.sol \
7+
--verify MockDLL:certora/specs/sanity.spec \
8+
--loop_iter 7 \
9+
--optimistic_loop \
10+
--send_only \
11+
--staging \
12+
--msg "FIFO DLL sanity" \
13+
$@

‎certora/scripts/sanity-simple.sh‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#!/bin/sh
2+
3+
make -C certora munged-simple
4+
5+
certoraRun \
6+
certora/munged-simple/MockDLL.sol \
7+
--verify MockDLL:certora/specs/sanity.spec \
8+
--loop_iter 7 \
9+
--optimistic_loop \
10+
--send_only \
11+
--staging \
12+
--msg "Simple DLL sanity" \
13+
$@

0 commit comments

Comments
 (0)