diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index dd0df01cb..aa0bcfc5b 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -75,28 +75,28 @@ invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) /* * No functions should be allowed to run after a job is deemed as canceled */ -invariant cannotSetIfCanceled(uint256 pId) - isCanceled(pId) => lastReverted == true +rule cannotSetIfCanceled(uint256 pId, method f) filtered { f-> !f.isView }{ + require(isCanceled(pId)); + env e; calldataarg args; + f(e, args); + assert(isCanceled(pId) => lastReverted == true, "Function did not revert when canceled"); +} /* * No functions should be allowed to run after a job is deemed as executed */ -invariant cannotSetIfExecuted(uint256 pId) - isExecuted(pId) => lastReverted == true - { - preserved execute(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash) with (env e) - { - require(isExecuted(pId)); - } - } +rule cannotSetIfExecuted(uint256 pId, method f) filtered { f-> !f.isView }{ + require(isExecuted(pId)); + env e; calldataarg args; + f(e, args); + assert(isExecuted(pId) => lastReverted == true, "Function did not revert after executed"); +} /* * sum of all votes casted is equal to the sum of voting power of those who voted */ invariant SumOfVotesCastEqualSumOfPowerOfVoted(uint256 pId) - counted_weight(pId) == counter_vote_power_by_id(pId) && - counted_weight(pId) == vote_power_ghost && - counter_vote_power_by_id(pId) == vote_power_ghost + counted_weight(pId) == vote_power_ghost() ////////////////////////////////////////////////////////////////////////////// /////////////////////////////////// RULES ////////////////////////////////////