From e1120b91372556fc6b56b5dd7f506e929ce0e261 Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Tue, 14 Mar 2023 10:23:49 +0100
Subject: [PATCH] try optimise GovernorStates

---
 certora/specs/GovernorFunctions.spec | 15 +++++++++------
 certora/specs/GovernorStates.spec    | 26 +++++++++++++++-----------
 2 files changed, 24 insertions(+), 17 deletions(-)

diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec
index b834663b9..35fc57365 100644
--- a/certora/specs/GovernorFunctions.spec
+++ b/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  otherQueuedBefore = isQueued(otherId)
+    bool  queuedBefore      = isQueued(pId);
+    bool  otherQueuedBefore = isQueued(otherId);
 
     address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
     require pId == queue@withrevert(e, targets, values, calldatas, descrHash);
@@ -174,8 +174,9 @@ rule cancel(uint256 pId, env e) {
 
     uint256 otherId;
 
-    uint8 stateBefore      = state(e, pId);
-    uint8 otherStateBefore = state(e, otherId);
+    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 state(e, otherId) != otherStateBefore  => otherId == pId;
+    assert isQueued(otherId) != otherQueuedBefore => otherId == pId;
 }
diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec
index 958d7ae47..417b7b0c6 100644
--- a/certora/specs/GovernorStates.spec
+++ b/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);
+    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 &&
-        proposalDeadline(pId) >= currentClock
+        snapshot < currentClock &&
+        deadline >= currentClock
     );
 
     // Succeeded: after vote end, with vote successful and quorum reached
     assert currentState == SUCCEEDED() => (
-        proposalDeadline(pId) < currentClock &&
+        deadline < currentClock &&
         (
-            quorumReached(pId) &&
-            voteSucceeded(pId)
+            quorumSuccess &&
+            voteSuccess
         )
     );
 
     // Defeated: after vote end, with vote not successful or quorum not reached
     assert currentState == DEFEATED() => (
-        proposalDeadline(pId) < currentClock &&
+        deadline < currentClock &&
         (
-            !quorumReached(pId) ||
-            !voteSucceeded(pId)
+            !quorumSuccess ||
+            !voteSuccess
         )
     );
 }