From 50a13d52b9d2c92600ab1706e2706b40f5ee134e Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 15 Mar 2023 17:13:14 +0100 Subject: [PATCH] uo --- certora/specs/GovernorPreventLateQuorum.spec | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index d8df72f94..a4eae4ea7 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -26,11 +26,6 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg requireInvariant proposalStateConsistency(pId); requireInvariant votesImplySnapshotPassed(pId); - // This should be a direct consequence of the invariant: `getExtendedDeadline(pId) > 0 => quorumReached(pId)` - // But this is not (easily) provable because the prover think `_totalSupplyCheckpoints` can arbitrarily change, - // which causes the quorum() to change. Not sure how to fix that. - require !quorumReached(pId) => getExtendedDeadline(pId) == 0; - uint256 deadlineBefore = proposalDeadline(pId); bool deadlineExtendedBefore = getExtendedDeadline(pId) > 0; bool quorumReachedBefore = quorumReached(pId); @@ -53,7 +48,7 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg ) || ( !deadlineExtendedBefore && deadlineExtendedAfter && - !quorumReachedBefore && + // !quorumReachedBefore && // Not sure how to prove that quorumReachedAfter && deadlineAfter == clock(e) + lateQuorumVoteExtension() && votingAll(f)