From dfafd796928b773fa0515c61c447306be2bf25d6 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 15 Mar 2023 17:16:47 +0100 Subject: [PATCH] uo --- certora/specs/GovernorPreventLateQuorum.spec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index a4eae4ea7..5ed48a555 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -26,6 +26,10 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg requireInvariant proposalStateConsistency(pId); requireInvariant votesImplySnapshotPassed(pId); + // 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); @@ -48,7 +52,7 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg ) || ( !deadlineExtendedBefore && deadlineExtendedAfter && - // !quorumReachedBefore && // Not sure how to prove that + !quorumReachedBefore && // Not sure how to prove that quorumReachedAfter && deadlineAfter == clock(e) + lateQuorumVoteExtension() && votingAll(f)