improve stateTransitionWait

certora/diff/governance_Governor.sol.patch

@@ -1,6 +1,6 @@
---- governance/Governor.sol	2023-03-07 10:48:47.730155491 +0100
-+++ governance/Governor.sol	2023-03-14 22:09:12.664754077 +0100
-@@ -216,6 +216,21 @@
+--- governance/Governor.sol	2023-05-03 09:17:45.566699712 +0200
++++ governance/Governor.sol	2023-05-04 15:18:42.667741565 +0200
+@@ -224,6 +224,21 @@
          return _proposals[proposalId].proposer;
      }
  

certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch

@@ -1,6 +1,6 @@
---- 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 @@
+--- governance/extensions/GovernorPreventLateQuorum.sol	2023-05-03 09:17:45.566699712 +0200
++++ governance/extensions/GovernorPreventLateQuorum.sol	2023-05-04 15:18:42.657742113 +0200
+@@ -82,6 +82,11 @@
          return _voteExtension;
      }
  

certora/diff/governance_extensions_GovernorTimelockControl.sol.patch

@@ -1,5 +1,5 @@
---- governance/extensions/GovernorTimelockControl.sol	2023-03-14 15:48:49.307543354 +0100
-+++ governance/extensions/GovernorTimelockControl.sol	2023-03-16 16:01:13.857331689 +0100
+--- governance/extensions/GovernorTimelockControl.sol	2023-05-04 11:44:55.587737817 +0200
++++ governance/extensions/GovernorTimelockControl.sol	2023-05-04 15:18:42.661075263 +0200
 @@ -24,7 +24,7 @@
   * _Available since v4.3._
   */
@@ -21,3 +21,13 @@
      /**
       * @dev Function to queue a proposal to the timelock.
       */
+@@ -163,4 +168,9 @@
+         emit TimelockChange(address(_timelock), address(newTimelock));
+         _timelock = newTimelock;
+     }
++
++    // FV
++    function timelockId(uint256 proposalId) public view returns (bytes32) {
++        return _timelockIds[proposalId];
++    }
+ }

certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch

@@ -1,7 +1,7 @@
---- governance/extensions/GovernorVotesQuorumFraction.sol	2023-03-07 10:48:47.733488857 +0100
-+++ governance/extensions/GovernorVotesQuorumFraction.sol	2023-03-15 22:52:06.424537201 +0100
-@@ -62,6 +62,11 @@
-         return _quorumNumeratorHistory.upperLookupRecent(timepoint.toUint32());
+--- governance/extensions/GovernorVotesQuorumFraction.sol	2023-05-03 09:17:45.570033048 +0200
++++ governance/extensions/GovernorVotesQuorumFraction.sol	2023-05-04 15:18:42.664408414 +0200
+@@ -61,6 +61,11 @@
+         return _quorumNumeratorHistory.upperLookupRecent(SafeCast.toUint32(timepoint));
      }
  
 +    // FV

certora/diff/token_ERC721_ERC721.sol.patch

@@ -1,5 +1,5 @@
---- token/ERC721/ERC721.sol	2023-03-07 10:48:47.736822221 +0100
-+++ token/ERC721/ERC721.sol	2023-03-09 19:49:39.669338673 +0100
+--- token/ERC721/ERC721.sol	2023-04-27 22:16:54.864065073 +0200
++++ token/ERC721/ERC721.sol	2023-05-04 15:18:42.671074716 +0200
 @@ -199,6 +199,11 @@
          return _owners[tokenId];
      }

certora/run.js

@@ -59,7 +59,7 @@ if (process.exitCode) {
 }
 
 for (const { spec, contract, files, options = [] } of specs) {
-  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]);
+  limit(runCertora, spec, contract, files, [...options, ...argv.options].flatMap(opt => opt.split(' ')));
 }
 
 // Run certora, aggregate the output and print it at the end

certora/specs/GovernorStates.spec

@@ -57,6 +57,11 @@ rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args)
 │ Rule: State transitions caused by time passing                                                                      │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
+// The timelockId can be set in states QUEUED, EXECUTED and CANCELED. However, checking the full scope of this results
+// in a timeout. This is a weaker version that is still usefull
+invariant noTimelockBeforeEndOfVote(env e, uint256 pId)
+    state(e, pId) == ACTIVE() => timelockId(pId) == 0
+
 rule stateTransitionWait(uint256 pId, env e1, env e2) {
     require clockSanity(e1);
     require clockSanity(e2);
@@ -66,6 +71,7 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) {
     // possible before the time passes. We don't want the state transition include elements that cannot have happened
     // before e1. This ensure that the e1 → e2 state transition is purelly a consequence of time passing.
     requireInvariant votesImplySnapshotPassed(e1, pId);
+    requireInvariant noTimelockBeforeEndOfVote(e1, pId);
 
     uint8 stateBefore = state(e1, pId);
     uint8 stateAfter  = state(e2, pId);
@@ -74,14 +80,7 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) {
         (stateBefore == PENDING() && stateAfter == ACTIVE()   ) ||
         (stateBefore == PENDING() && stateAfter == DEFEATED() ) ||
         (stateBefore == ACTIVE()  && stateAfter == SUCCEEDED()) ||
-        (stateBefore == ACTIVE()  && stateAfter == DEFEATED() ) ||
-        // Strange consequence of the timelock binding:
-        // When transitioning from ACTIVE to SUCCEEDED (because of the clock moving forward) the proposal state in
-        // the timelock is suddenly considered. Prior state set in the timelock can cause the proposal to already be
-        // queued, executed or canceled.
-        (stateBefore == ACTIVE()  && stateAfter == CANCELED()) ||
-        (stateBefore == ACTIVE()  && stateAfter == EXECUTED()) ||
-        (stateBefore == ACTIVE()  && stateAfter == QUEUED())
+        (stateBefore == ACTIVE()  && stateAfter == DEFEATED() )
     );
 }
 

certora/specs/methods/IGovernor.spec

@@ -52,4 +52,5 @@ methods {
     getForVotes(uint256)                             returns uint256 envfree
     getAbstainVotes(uint256)                         returns uint256 envfree
     quorumNumeratorLength()                          returns uint256 envfree
+    timelockId(uint256)                              returns bytes32 envfree
 }