wip

certora/specs/GovernorFunctions.spec

@@ -1,6 +1,8 @@
 import "helpers.spec"
 import "Governor.helpers.spec"
+import "GovernorInvariants.spec"
 
+use invariant proposalStateConsistency
 use invariant queuedImplyVoteOver
 
 /*
@@ -233,7 +235,7 @@ rule execute_sideeffect(uint256 pId, env e, uint256 otherId) {
 rule cancel_liveness(uint256 pId, env e) {
     require nonpayable(e);
     require clockSanity(e);
-    requireInvariant queuedImplyVoteOver(pId);
+    requireInvariant queuedImplyVoteOver(e, pId);
 
     uint8 stateBefore = state(e, pId);
 

certora/specs/GovernorInvariants.spec

@@ -40,12 +40,14 @@ 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 ||
+        getForVotes(pId)     > 0 ||
+        getAbstainVotes(pId) > 0
+    ) => proposalSnapshot(pId) < clock(e)
     {
-        preserved {
-            require clockSanity(e);
+        preserved with (env e2) {
+            require clock(e) == clock(e2);
         }
     }