diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 69d1fd85e..41ec3e735 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -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 + //////////////////////////////////////////////////////////////////////////////