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

all rules checked no structure organization

Browse Source
This commit is contained in:
Michael M
2021-11-23 16:57:14 +02:00
parent 9344f697f9
commit 0894724496
1 changed files with 38 additions and 33 deletions
Download Patch File Download Diff File Expand all files Collapse all files

71
certora/specs/GovernorBase.spec
View File

@ -272,39 +272,6 @@ rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
///////////////////////////// Not Categorized Yet //////////////////////////////
////////////////////////////////////////////////////////////////////////////////
/*
* All non-view functions should revert if proposal is executed
*/
rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selector != updateQuorumNumerator(uint256).selector &&
!f.isFallback && f.selector != updateTimelock(address).selector} {
env e; calldataarg args;
uint256 pId;
require(isExecuted(pId));
requireInvariant noBothExecutedAndCanceled(pId);
requireInvariant executedImplyStartAndEndDateNonZero(pId);
helperFunctionsWithRevert(pId, f, e);
assert(lastReverted, "Function was not reverted");
}
/*
* All non-view functions should revert if proposal is canceled
*/
rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView && f.selector != updateQuorumNumerator(uint256).selector &&
!f.isFallback && f.selector != updateTimelock(address).selector} {
env e; calldataarg args;
uint256 pId;
require(isCanceled(pId));
requireInvariant noBothExecutedAndCanceled(pId);
requireInvariant canceledImplyStartAndEndDateNonZero(pId);
helperFunctionsWithRevert(pId, f, e);
assert(lastReverted, "Function was not reverted");
}
/*
* Shows that executed can only change due to execute()
*/
@ -320,3 +287,41 @@ rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] c
bool executedAfter = isExecuted(pId);
assert(executedAfter != executedBefore, "executed property did not change");
}
/*
* All proposal specific (non-view) functions should revert if proposal is executed
*/
// In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID,
// non of the proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc
// we connected the executed attribute to the execute() function, showing that only execute() can
// change it, and that it will always change it.
rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selector != updateQuorumNumerator(uint256).selector &&
!f.isFallback && f.selector != updateTimelock(address).selector} {
env e; calldataarg args;
uint256 pId;
require(isExecuted(pId));
requireInvariant noBothExecutedAndCanceled(pId);
requireInvariant executedImplyStartAndEndDateNonZero(pId);
helperFunctionsWithRevert(pId, f, e);
assert(lastReverted, "Function was not reverted");
}
/*
* All proposal specific (non-view) functions should revert if proposal is canceled
*/
rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView && f.selector != updateQuorumNumerator(uint256).selector &&
!f.isFallback && f.selector != updateTimelock(address).selector} {
env e; calldataarg args;
uint256 pId;
require(isCanceled(pId));
requireInvariant noBothExecutedAndCanceled(pId);
requireInvariant canceledImplyStartAndEndDateNonZero(pId);
helperFunctionsWithRevert(pId, f, e);
assert(lastReverted, "Function was not reverted");
}