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

added invariants if executed or canceled always revert

Browse Source
This commit is contained in:
Michael M
2021-11-08 15:57:19 +02:00
parent ac729e0ecf
commit 7a5bd86ef4
1 changed files with 12 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
certora/specs/GovernorBase.spec
View File

@ -40,6 +40,18 @@ invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) e.block.number < p
*/
invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
/*
* No functions should be allowed to run after a job is deemed as canceled
*/
invariant cannotSetIfCanceled(uint256 pId)
isCanceled(pId) => lastReverted == true
/*
* No functions should be allowed to run after a job is deemed as executed
*/
invariant cannotSetIfExecuted(uint256 pId)
isExecuted(pId) => lastReverted == true
//////////////////////////////////////////////////////////////////////////////