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
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
import "helpers/helpers.spec";
import "methods/IAccessControl.spec";
methods {
function PROPOSER_ROLE() external returns (bytes32) envfree;
function EXECUTOR_ROLE() external returns (bytes32) envfree;
function CANCELLER_ROLE() external returns (bytes32) envfree;
function isOperation(bytes32) external returns (bool);
function isOperationPending(bytes32) external returns (bool);
function isOperationReady(bytes32) external returns (bool);
function isOperationDone(bytes32) external returns (bool);
function getTimestamp(bytes32) external returns (uint256) envfree;
function getMinDelay() external returns (uint256) envfree;
function hashOperation(address, uint256, bytes, bytes32, bytes32) external returns(bytes32) envfree;
function hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) external returns(bytes32) envfree;
function schedule(address, uint256, bytes, bytes32, bytes32, uint256) external;
function scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) external;
function execute(address, uint256, bytes, bytes32, bytes32) external;
function executeBatch(address[], uint256[], bytes[], bytes32, bytes32) external;
function cancel(bytes32) external;
function updateDelay(uint256) external;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helpers │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
// Uniformly handle scheduling of batched and non-batched operations.
function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
if (f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) {
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
schedule@withrevert(e, target, value, data, predecessor, salt, delay);
} else if (f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) {
address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt;
require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay);
} else {
calldataarg args;
f@withrevert(e, args);
}
}
// Uniformly handle execution of batched and non-batched operations.
function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) {
if (f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector) {
address target; uint256 value; bytes data; bytes32 salt;
require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
execute@withrevert(e, target, value, data, predecessor, salt);
} else if (f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
address[] targets; uint256[] values; bytes[] payloads; bytes32 salt;
require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
executeBatch@withrevert(e, targets, values, payloads, predecessor, salt);
} else {
calldataarg args;
f@withrevert(e, args);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition DONE_TIMESTAMP() returns uint256 = 1;
definition UNSET() returns uint8 = 0x1;
definition PENDING() returns uint8 = 0x2;
definition DONE() returns uint8 = 0x4;
definition isUnset(env e, bytes32 id) returns bool = !isOperation(e, id);
definition isPending(env e, bytes32 id) returns bool = isOperationPending(e, id);
definition isDone(env e, bytes32 id) returns bool = isOperationDone(e, id);
definition state(env e, bytes32 id) returns uint8 = (isUnset(e, id) ? UNSET() : 0) | (isPending(e, id) ? PENDING() : 0) | (isDone(e, id) ? DONE() : 0);
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariants: consistency of accessors │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant isOperationCheck(env e, bytes32 id)
isOperation(e, id) <=> getTimestamp(id) > 0
filtered { f -> !f.isView }
invariant isOperationPendingCheck(env e, bytes32 id)
isOperationPending(e, id) <=> getTimestamp(id) > DONE_TIMESTAMP()
filtered { f -> !f.isView }
invariant isOperationDoneCheck(env e, bytes32 id)
isOperationDone(e, id) <=> getTimestamp(id) == DONE_TIMESTAMP()
filtered { f -> !f.isView }
invariant isOperationReadyCheck(env e, bytes32 id)
isOperationReady(e, id) <=> (isOperationPending(e, id) && getTimestamp(id) <= e.block.timestamp)
filtered { f -> !f.isView }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: a proposal id is either unset, pending or done │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant stateConsistency(bytes32 id, env e)
// Check states are mutually exclusive
(isUnset(e, id) <=> (!isPending(e, id) && !isDone(e, id) )) &&
(isPending(e, id) <=> (!isUnset(e, id) && !isDone(e, id) )) &&
(isDone(e, id) <=> (!isUnset(e, id) && !isPending(e, id))) &&
// Check that the state helper behaves as expected:
(isUnset(e, id) <=> state(e, id) == UNSET() ) &&
(isPending(e, id) <=> state(e, id) == PENDING() ) &&
(isDone(e, id) <=> state(e, id) == DONE() ) &&
// Check substate
isOperationReady(e, id) => isPending(e, id)
filtered { f -> !f.isView }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: state transition rules │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule stateTransition(bytes32 id, env e, method f, calldataarg args) {
require e.block.timestamp > 1; // Sanity
uint8 stateBefore = state(e, id);
f(e, args);
uint8 stateAfter = state(e, id);
// Cannot jump from UNSET to DONE
assert stateBefore == UNSET() => stateAfter != DONE();
// UNSET → PENDING: schedule or scheduleBatch
assert stateBefore == UNSET() && stateAfter == PENDING() => (
f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
);
// PENDING → UNSET: cancel
assert stateBefore == PENDING() && stateAfter == UNSET() => (
f.selector == sig:cancel(bytes32).selector
);
// PENDING → DONE: execute or executeBatch
assert stateBefore == PENDING() && stateAfter == DONE() => (
f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector ||
f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
);
// DONE is final
assert stateBefore == DONE() => stateAfter == DONE();
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: minimum delay can only be updated through a timelock execution │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule minDelayOnlyChange(env e) {
uint256 delayBefore = getMinDelay();
method f; calldataarg args;
f(e, args);
assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == sig:updateDelay(uint256).selector), "Unauthorized delay update";
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: schedule liveness and effects │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
} {
require nonpayable(e);
// Basic timestamp assumptions
require e.block.timestamp > 1;
require e.block.timestamp + delay < max_uint256;
require e.block.timestamp + getMinDelay() < max_uint256;
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
uint8 stateBefore = state(e, id);
bool isDelaySufficient = delay >= getMinDelay();
bool isProposerBefore = hasRole(PROPOSER_ROLE(), e.msg.sender);
helperScheduleWithRevert(e, f, id, delay);
bool success = !lastReverted;
// liveness
assert success <=> (
stateBefore == UNSET() &&
isDelaySufficient &&
isProposerBefore
);
// effect
assert success => state(e, id) == PENDING(), "State transition violation";
assert success => getTimestamp(id) == require_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set";
// no side effect
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: execute liveness and effects │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector ||
f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
} {
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
uint8 stateBefore = state(e, id);
bool isOperationReadyBefore = isOperationReady(e, id);
bool isExecutorOrOpen = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0);
bool predecessorDependency = predecessor == to_bytes32(0) || isDone(e, predecessor);
helperExecuteWithRevert(e, f, id, predecessor);
bool success = !lastReverted;
// The underlying transaction can revert, and that would cause the execution to revert. We can check that all non
// reverting calls meet the requirements in terms of proposal readiness, access control and predecessor dependency.
// We can't however guarantee that these requirements being meet ensure liveness of the proposal, because the
// proposal can revert for reasons beyond our control.
// liveness, should be `<=>` but can only check `=>` (see comment above)
assert success => (
stateBefore == PENDING() &&
isOperationReadyBefore &&
predecessorDependency &&
isExecutorOrOpen
);
// effect
assert success => state(e, id) == DONE(), "State transition violation";
// no side effect
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: cancel liveness and effects │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule cancel(env e, bytes32 id) {
require nonpayable(e);
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
uint8 stateBefore = state(e, id);
bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender);
cancel@withrevert(e, id);
bool success = !lastReverted;
// liveness
assert success <=> (
stateBefore == PENDING() &&
isCanceller
);
// effect
assert success => state(e, id) == UNSET(), "State transition violation";
// no side effect
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
}