fix attempt

certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch

@@ -1,4 +1,4 @@
---- governance/extensions/GovernorPreventLateQuorum.sol	2023-03-07 10:48:47.733488857 +0100
+--- governance/extensions/GovernorPreventLateQuorum.sol	2023-03-15 17:13:06.879632860 +0100
 +++ governance/extensions/GovernorPreventLateQuorum.sol	2023-03-15 14:14:59.121060484 +0100
 @@ -84,6 +84,11 @@
          return _voteExtension;

certora/specs/GovernorBaseRules.spec

@@ -141,6 +141,9 @@ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args)
 invariant quorumRatioLessThanOne(uint256 blockNumber)
     quorumNumerator(blockNumber) <= quorumDenominator()
     filtered { f -> !skip(f) }
+    {
+        require quorumNumeratorLength() < max_uint256;
+    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐

certora/specs/GovernorInvariants.spec

@@ -41,9 +41,9 @@ invariant proposalStateConsistency(uint256 pId)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant votesImplySnapshotPassed(env e, uint256 pId)
-    getAgainstVotes(pId) == 0 => proposalSnapshot(pId) < clock(e) &&
-    getForVotes(pId)     == 0 => proposalSnapshot(pId) < clock(e) &&
-    getAbstainVotes(pId) == 0 => proposalSnapshot(pId) < clock(e)
+    getAgainstVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e) &&
+    getForVotes(pId)     > 0 => proposalSnapshot(pId) <= clock(e) &&
+    getAbstainVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e)
     {
         preserved {
             require clockSanity(e);

certora/specs/GovernorStates.spec

@@ -4,6 +4,7 @@ import "Governor.helpers.spec"
 import "GovernorInvariants.spec"
 
 use invariant proposalStateConsistency
+use invariant votesImplySnapshotPassed
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -138,6 +139,7 @@ rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg ar
     filtered { f -> !skip(f) }
 {
     require clockSanity(e);
+    requireInvariant votesImplySnapshotPassed(e, pId);
 
     bool quorumReachedBefore = quorumReached(pId);
 

certora/specs/methods/IGovernor.spec

@@ -50,4 +50,5 @@ methods {
     getAgainstVotes(uint256)            returns uint256 envfree
     getForVotes(uint256)                returns uint256 envfree
     getAbstainVotes(uint256)            returns uint256 envfree
+    quorumNumeratorLength()             returns uint256 envfree
 }