From a355bf0de27b01ed94e2ff7019d31b741dd1c67d Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Thu, 16 Mar 2023 09:28:48 +0100
Subject: [PATCH] fix

---
 certora/specs/GovernorBaseRules.spec         | 4 +++-
 certora/specs/GovernorPreventLateQuorum.spec | 5 +++--
 certora/specs/GovernorStates.spec            | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec
index 2bcaa0839..baa4d18c4 100644
--- a/certora/specs/GovernorBaseRules.spec
+++ b/certora/specs/GovernorBaseRules.spec
@@ -142,7 +142,9 @@ invariant quorumRatioLessThanOne(uint256 blockNumber)
     quorumNumerator(blockNumber) <= quorumDenominator()
     filtered { f -> !skip(f) }
     {
-        require quorumNumeratorLength() < max_uint256;
+        preserved {
+            require quorumNumeratorLength() < max_uint256;
+        }
     }
 
 /*
diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec
index 0af3be925..cb906810b 100644
--- a/certora/specs/GovernorPreventLateQuorum.spec
+++ b/certora/specs/GovernorPreventLateQuorum.spec
@@ -23,12 +23,13 @@ use invariant votesImplySnapshotPassed
 rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg args)
     filtered { f -> !skip(f) }
 {
+    require clockSanity(e);
     requireInvariant proposalStateConsistency(pId);
     requireInvariant votesImplySnapshotPassed(e, pId);
 
     // This is not (easily) provable as an invariant 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;
+    require quorumReached(pId) <=> getExtendedDeadline(pId) > 0;
 
     uint256 deadlineBefore         = proposalDeadline(pId);
     bool    deadlineExtendedBefore = getExtendedDeadline(pId) > 0;
@@ -52,7 +53,7 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg
         ) || (
             !deadlineExtendedBefore &&
             deadlineExtendedAfter &&
-            !quorumReachedBefore && // Not sure how to prove that
+            !quorumReachedBefore &&
             quorumReachedAfter &&
             deadlineAfter == clock(e) + lateQuorumVoteExtension() &&
             votingAll(f)
diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec
index af6ffcf26..3d1c9de4d 100644
--- a/certora/specs/GovernorStates.spec
+++ b/certora/specs/GovernorStates.spec
@@ -149,7 +149,7 @@ rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg ar
     f(e, args);
 
     // Needed because the prover doesn't understand the checkpoint properties of the voting token.
-    require clock(e) > snapshot => token_getPastTotalSupply(snapshot) == cache;
+    require clock(e) > snapshot => token_getPastTotalSupply(snapshot) == totalSupply;
 
     assert quorumReached(pId) != quorumReachedBefore => (
         !quorumReachedBefore &&