NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix governor changes spec

Browse Source
This commit is contained in:
Hadrien Croubois
2023-03-14 10:02:10 +01:00
parent e35daecf95
commit 704e265c41
2 changed files with 18 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
certora/specs/Governor.helpers.spec
View File

@ -54,6 +54,13 @@ definition voting(method f) returns bool =
f.selector == castVoteWithReason(uint256,uint8,string).selector ||
f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector;
definition votingBySig(method f) returns bool =
f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector ||
f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector;
definition votingAll(method f) returns bool =
voting(f) || votingBySig(f);
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helper functions │
@ -79,7 +86,8 @@ function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8
}
else
{
require false;
calldataarg args;
f(e, args);
return 0;
}
}
@ -132,6 +140,7 @@ function helperFunctionsWithRevert(env e, method f, uint256 pId) {
}
else
{
require false;
calldataarg args;
f(e, args);
}
}

9
certora/specs/GovernorChanges.spec
View File

@ -22,6 +22,11 @@ rule changes(uint256 pId, env e) {
assert isExecuted(pId) != isExecutedBefore => (!isExecutedBefore && f.selector == execute(address[],uint256[],bytes[],bytes32).selector);
assert isCanceled(pId) != isCanceledBefore => (!isCanceledBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector);
assert isQueued(pId) != isQueuedBefore => (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector);
assert hasVoted(pId, user) != hasVotedBefore => (!hasVotedBefore && voting(f));
assert hasVoted(pId, user) != hasVotedBefore => (!hasVotedBefore && votingAll(f));
// queue is cleared on cancel
assert isQueued(pId) != isQueuedBefore => (
(!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) ||
(isQueuedBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector)
);
}