From d4e9d8d54d8999cab71f6f642ec897decd9dcf3f Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 28 Feb 2023 12:10:50 +0100 Subject: [PATCH] fix error in one of the governor rules --- certora/specs/GovernorBase.spec | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 1c177d235..c1e285a06 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -283,16 +283,13 @@ rule noStartBeforeCreation(uint256 pId) { /* - * A proposal can neither be executed nor canceled before it ends + * A proposal cannot be executed before it ends */ - // By induction it cannot be executed nor canceled before it starts, due to voteStartBeforeVoteEnd -rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){ - require !isExecuted(pId) && !isCanceled(pId); - - env e; calldataarg args; + // By induction it cannot be executed before it starts, due to voteStartBeforeVoteEnd +rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args){ + require !isExecuted(pId); f(e, args); - - assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline"; + assert isExecuted(pId) => (e.block.number >= proposalDeadline(pId)), "executed before deadline"; } ////////////////////////////////////////////////////////////////////////////////