fix specs

certora/specs.js

@@ -53,7 +53,7 @@ module.exports = [].concat(
   product(
     [
       ...product(['GovernorHarness'], ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates']),
-      ...product(['GovernorPreventLateHarness'], ['GovernorPreventLateHarness']),
+      ...product(['GovernorPreventLateHarness'], ['GovernorPreventLateQuorum']),
     ],
     ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
   ).map(([contract, spec, token]) => ({

certora/specs/GovernorBaseRules.spec

@@ -77,11 +77,12 @@ rule againstVotesDontCountTowardsQuorum(uint256 pId, env e, method f)
     filtered { f -> voting(f) }
 {
     address voter;
-    uint8   support = 0; // Against
 
-    helperVoteWithRevert(e, f, pId, voter, support);
+    bool quorumReachedBefore = quorumReached(pId);
 
-    assert quorumReached(pId) == quorumBefore, "quorum must not be reached with an against vote";
+    helperVoteWithRevert(e, f, pId, voter, 0); // support 0 = against
+
+    assert quorumReached(pId) == quorumReachedBefore, "quorum must not be reached with an against vote";
 }
 
 /*
@@ -137,14 +138,9 @@ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args)
 │ Invariant: The quorum numerator is always less than or equal to the quorum denominator                              │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant quorumRatioLessThanOne(env e, uint256 blockNumber)
+invariant quorumRatioLessThanOne(uint256 blockNumber)
-    quorumNumerator(e, blockNumber) <= quorumDenominator()
+    quorumNumerator(blockNumber) <= quorumDenominator()
     filtered { f -> !skip(f) }
-    {
-        preserved {
-            require clockSanity(e);
-        }
-    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐

certora/specs/GovernorPreventLateQuorum.spec

@@ -24,7 +24,7 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg
     filtered { f -> !skip(f) }
 {
     requireInvariant proposalStateConsistency(pId);
-    requireInvariant votesImplySnapshotPassed(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.

certora/specs/GovernorStates.spec

@@ -139,11 +139,11 @@ rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg ar
 {
     require clockSanity(e);
 
-    bool quorumReachedBefore = quorumReached(e, pId);
+    bool quorumReachedBefore = quorumReached(pId);
 
     f(e, args);
 
-    assert quorumReached(e, pId) != quorumReachedBefore => (
+    assert quorumReached(pId) != quorumReachedBefore => (
         !quorumReachedBefore &&
         votingAll(f)
     );