/
dll-linkedcorrectly.spec
165 lines (133 loc) · 4.67 KB
/
dll-linkedcorrectly.spec
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
methods {
function getValueOf(address) external returns (uint256) envfree;
function getHead() external returns (address) envfree;
function getTail() external returns (address) envfree;
function getNext(address) external returns (address) envfree;
function getPrev(address) external returns (address) envfree;
function remove(address) external envfree;
function insertSorted(address, uint256, uint256) external envfree;
}
// GHOST COPIES
ghost mapping(address => address) ghostNext {
init_state axiom forall address x. ghostNext[x] == 0;
}
ghost mapping(address => address) ghostPrev {
init_state axiom forall address x. ghostPrev[x] == 0;
}
ghost mapping(address => uint256) ghostValue {
init_state axiom forall address x. ghostValue[x] == 0;
}
ghost address ghostHead;
ghost address ghostTail;
ghost uint256 ghostLength;
ghost nextstar(address, address) returns bool {
init_state axiom forall address x. forall address y. nextstar(x, y) == (x == y);
}
ghost prevstar(address, address) returns bool {
init_state axiom forall address x. forall address y. prevstar(x, y) == (x == y);
}
// HOOKS
hook Sstore currentContract.dll.head address newHead {
ghostHead = newHead;
}
hook Sstore currentContract.dll.tail address newTail {
ghostTail = newTail;
}
hook Sstore currentContract.dll.accounts[KEY address key].next address newNext {
ghostNext[key] = newNext;
}
hook Sstore currentContract.dll.accounts[KEY address key].prev address newPrev {
ghostPrev[key] = newPrev;
}
hook Sstore currentContract.dll.accounts[KEY address key].value uint256 newValue {
ghostValue[key] = newValue;
}
hook Sload address head currentContract.dll.head {
require ghostHead == head;
}
hook Sload address tail currentContract.dll.tail {
require ghostTail == tail;
}
hook Sload address next currentContract.dll.accounts[KEY address key].next {
require ghostNext[key] == next;
}
hook Sload address prev currentContract.dll.accounts[KEY address key].prev {
require ghostPrev[key] == prev;
}
hook Sload uint256 value currentContract.dll.accounts[KEY address key].value {
require ghostValue[key] == value;
}
// INVARIANTS
invariant nextPrevMatch()
// either list is empty, and both head and tail are 0,
((ghostHead == 0 && ghostTail == 0)
// or both head and tail are set and their prev resp. next points to 0.
|| (ghostHead != 0 && ghostTail != 0 && ghostNext[ghostTail] == 0 && ghostPrev[ghostHead] == 0
&& ghostValue[ghostHead] != 0 && ghostValue[ghostTail] != 0))
// for all addresses:
&& (forall address a.
// either the address is not part of the list and every field is 0.
(ghostNext[a] == 0 && ghostPrev[a] == 0 && ghostValue[a] == 0)
// or the address is part of the list, address is non-zero, value is non-zero,
// and prev and next pointer are linked correctly.
|| (a != 0 && ghostValue[a] != 0
&& ((a == ghostHead && ghostPrev[a] == 0) || ghostNext[ghostPrev[a]] == a)
&& ((a == ghostTail && ghostNext[a] == 0) || ghostPrev[ghostNext[a]] == a)));
invariant inList()
(ghostHead != 0 => ghostValue[ghostHead] != 0)
&& (ghostTail != 0 => ghostValue[ghostTail] != 0)
&& (forall address a. ghostNext[a] != 0 => ghostValue[ghostNext[a]] != 0)
&& (forall address a. ghostPrev[a] != 0 => ghostValue[ghostPrev[a]] != 0)
{
preserved {
requireInvariant nextPrevMatch();
}
}
rule insert_preserves_old {
address newElem;
address oldElem;
uint256 newValue;
uint256 maxIter;
bool oldInList = ghostValue[oldElem] != 0;
require oldElem != newElem;
insertSorted(newElem, newValue, maxIter);
assert oldInList == (ghostValue[oldElem] != 0);
}
rule insert_adds_new() {
address newElem;
uint256 newValue;
uint256 maxIter;
insertSorted(newElem, newValue, maxIter);
assert ghostValue[newElem] != 0;
assert ghostValue[newElem] == newValue;
}
rule insert_does_not_revert() {
address newElem;
uint256 newValue;
uint256 maxIter;
require newElem != 0;
require ghostValue[newElem] == 0;
require newValue != 0;
insertSorted@withrevert(newElem, newValue, maxIter);
assert !lastReverted;
}
rule remove_preserves_old {
address elem;
address oldElem;
bool oldInList = ghostValue[oldElem] != 0;
require oldElem != elem;
remove(elem);
assert oldInList == (ghostValue[oldElem] != 0);
}
rule remove_deletes() {
address elem;
remove(elem);
assert ghostValue[elem] == 0;
}
rule remove_does_not_revert() {
address elem;
require elem != 0;
require ghostValue[elem] != 0;
remove@withrevert(elem);
assert !lastReverted;
}