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

added filters to revert if exec and revert if canceled

Browse Source
This commit is contained in:
Michael M
2021-11-18 15:39:18 +02:00
parent f7049de567
commit 65af47d90d
1 changed files with 13 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
certora/specs/GovernorBase.spec
View File

@ -11,6 +11,8 @@ methods {
execute(address[], uint256[], bytes[], bytes32) returns uint256 execute(address[], uint256[], bytes[], bytes32) returns uint256
hasVoted(uint256, address) returns bool hasVoted(uint256, address) returns bool
castVote(uint256, uint8) returns uint256 castVote(uint256, uint8) returns uint256
updateQuorumNumerator(uint256)
// internal functions made public in harness: // internal functions made public in harness:
_quorumReached(uint256) returns bool _quorumReached(uint256) returns bool
@ -256,6 +258,11 @@ rule checkHashProposal {
//////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
///////////////////////////// Not Categorized Yet //////////////////////////////
////////////////////////////////////////////////////////////////////////////////
/* /*
* all non-view functions should revert if proposal is executed * all non-view functions should revert if proposal is executed
*/ */
@ -263,9 +270,9 @@ rule checkHashProposal {
// that means that for different arguments passed, the same value will be returned, for example: func(a,b,c,d) == func(o,p,g,r) // that means that for different arguments passed, the same value will be returned, for example: func(a,b,c,d) == func(o,p,g,r)
// the summarization is not an under estimation in this case, because we want to check that for a specific proposal ID (pId), any // the summarization is not an under estimation in this case, because we want to check that for a specific proposal ID (pId), any
// (non view) function call is reverting. We dont care what happen with other pIds, and dont care how the hash function generates the ID. // (non view) function call is reverting. We dont care what happen with other pIds, and dont care how the hash function generates the ID.
rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selector != 0x7d5e81e2 && !f.isFallback} { rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selector != 0x7d5e81e2 && !f.isFallback && f.selector != updateQuorumNumerator(uint256).selector && f.selector != 0xa890c910} {
env e; calldataarg args; // ^ env e; calldataarg args; // ^ ^
uint256 pId; // propose uint256 pId; // propose updateTimelock
require(isExecuted(pId)); require(isExecuted(pId));
requireInvariant proposalInitiated(pId); requireInvariant proposalInitiated(pId);
requireInvariant noBothExecutedAndCanceled(pId); requireInvariant noBothExecutedAndCanceled(pId);
@ -276,9 +283,9 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selec
/* /*
* all non-view functions should revert if proposal is canceled * all non-view functions should revert if proposal is canceled
*/ */
rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView && f.selector != 0x7d5e81e2 && !f.isFallback} { rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView && f.selector != 0x7d5e81e2 && !f.isFallback && f.selector != updateQuorumNumerator(uint256).selector && f.selector != 0xa890c910} {
env e; calldataarg args; // ^ env e; calldataarg args; // ^ ^
uint256 pId; // propose uint256 pId; // propose updateTimelock
require(isCanceled(pId)); require(isCanceled(pId));
requireInvariant noBothExecutedAndCanceled(pId); requireInvariant noBothExecutedAndCanceled(pId);
requireInvariant proposalInitiated(pId); requireInvariant proposalInitiated(pId);