try optimise GovernorStates

certora/specs/GovernorFunctions.spec

@@ -111,8 +111,8 @@ rule queue(uint256 pId, env e) {
 
     uint8 stateBefore       = state(e, pId);
     uint8 otherStateBefore  = state(e, otherId);
-    bool  queuedBefore      = isQueued(pId)
+    bool  queuedBefore      = isQueued(pId);
-    bool  otherQueuedBefore = isQueued(otherId)
+    bool  otherQueuedBefore = isQueued(otherId);
 
     address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
     require pId == queue@withrevert(e, targets, values, calldatas, descrHash);
@@ -176,6 +176,7 @@ rule cancel(uint256 pId, env e) {
 
     uint8 stateBefore       = state(e, pId);
     uint8 otherStateBefore  = state(e, otherId);
+    bool  otherQueuedBefore = isQueued(otherId);
 
     address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
     require pId == cancel@withrevert(e, targets, values, calldatas, descrHash);
@@ -189,9 +190,11 @@ rule cancel(uint256 pId, env e) {
 
     // effect
     assert success => (
-        state(e, pId) == CANCELED()
+        state(e, pId) == CANCELED() &&
+        !isQueued(pId) // cancel resets timelockId
     );
 
     // no side-effect
     assert state(e, otherId) != otherStateBefore  => otherId == pId;
+    assert isQueued(otherId) != otherQueuedBefore => otherId == pId;
 }

certora/specs/GovernorStates.spec

@@ -92,35 +92,39 @@ rule stateIsConsistentWithVotes(uint256 pId, env e) {
     require clockSanity(e);
     requireInvariant proposalStateConsistency(pId);
 
-    uint8  currentState = state(e, pId);
     uint48  currentClock  = clock(e);
+    uint8   currentState  = state(e, pId);
+    uint256 snapshot      = proposalSnapshot(pId);
+    uint256 deadline      = proposalDeadline(pId);
+    bool    quorumSuccess = quorumReached(pId);
+    bool    voteSuccess   = voteSucceeded(pId);
 
     // Pending: before vote starts
     assert currentState == PENDING() => (
-        proposalSnapshot(pId) >= currentClock
+        snapshot >= currentClock
     );
 
     // Active: after vote starts & before vote ends
     assert currentState == ACTIVE() => (
-        proposalSnapshot(pId) < currentClock &&
+        snapshot < currentClock &&
-        proposalDeadline(pId) >= currentClock
+        deadline >= currentClock
     );
 
     // Succeeded: after vote end, with vote successful and quorum reached
     assert currentState == SUCCEEDED() => (
-        proposalDeadline(pId) < currentClock &&
+        deadline < currentClock &&
         (
-            quorumReached(pId) &&
+            quorumSuccess &&
-            voteSucceeded(pId)
+            voteSuccess
         )
     );
 
     // Defeated: after vote end, with vote not successful or quorum not reached
     assert currentState == DEFEATED() => (
-        proposalDeadline(pId) < currentClock &&
+        deadline < currentClock &&
         (
-            !quorumReached(pId) ||
+            !quorumSuccess ||
-            !voteSucceeded(pId)
+            !voteSuccess
         )
     );
 }