From d7884251aaf7fed9514cdaaa229108e81c35b56e Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Tue, 14 Mar 2023 21:33:13 +0100
Subject: [PATCH] update

---
 certora/specs.js                     |  2 +-
 certora/specs/Governor.helpers.spec  |  1 +
 certora/specs/GovernorBaseRules.spec | 28 ----------------------------
 certora/specs/GovernorChanges.spec   |  2 +-
 4 files changed, 3 insertions(+), 30 deletions(-)

diff --git a/certora/specs.js b/certora/specs.js
index 19d62e150..3ab802a14 100644
--- a/certora/specs.js
+++ b/certora/specs.js
@@ -47,7 +47,7 @@ module.exports = [
     spec: 'TimelockController',
     contract: 'TimelockControllerHarness',
     files: ['certora/harnesses/TimelockControllerHarness.sol'],
-    options: ['--optimistic_hashing', '--optimistic_loop']
+    options: ['--optimistic_hashing', '--optimistic_loop'],
   },
   // Governor
   ...product(
diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec
index 737310fba..8bc0d8310 100644
--- a/certora/specs/Governor.helpers.spec
+++ b/certora/specs/Governor.helpers.spec
@@ -68,6 +68,7 @@ definition votingAll(method f) returns bool =
 */
 function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 support) returns uint256 {
     string reason; bytes params;
+    require reason.length >= 0;
 
     if (f.selector == castVote(uint256,uint8).selector)
     {
diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec
index 992921c4a..405a1085c 100644
--- a/certora/specs/GovernorBaseRules.spec
+++ b/certora/specs/GovernorBaseRules.spec
@@ -144,31 +144,3 @@ rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args
 
     assert lastReverted, "Function was not reverted";
 }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: Proposal can be switched state only by specific functions                                                     │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule stateOnlyAfterFunc(uint256 pId, env e, method f) {
-    bool createdBefore  = proposalCreated(pId);
-    bool executedBefore = isExecuted(pId);
-    bool canceledBefore = isCanceled(pId);
-
-    helperFunctionsWithRevert(e, f, pId);
-
-    assert (proposalCreated(pId) != createdBefore) => (
-        createdBefore == false &&
-        f.selector == propose(address[], uint256[], bytes[], string).selector
-    ), "proposalCreated only changes in the propose method";
-
-    assert (isExecuted(pId) != executedBefore) => (
-        executedBefore == false &&
-        f.selector == execute(address[], uint256[], bytes[], bytes32).selector
-    ), "isExecuted only changes in the execute method";
-
-    assert (isCanceled(pId) != canceledBefore) => (
-        canceledBefore == false &&
-        f.selector == cancel(address[], uint256[], bytes[], bytes32).selector
-    ), "isCanceled only changes in the cancel method";
-}
diff --git a/certora/specs/GovernorChanges.spec b/certora/specs/GovernorChanges.spec
index bd3ff681f..c521f7995 100644
--- a/certora/specs/GovernorChanges.spec
+++ b/certora/specs/GovernorChanges.spec
@@ -4,7 +4,7 @@ import "Governor.helpers.spec"
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: internal variables can only change though specific functions calls                                            │
+│ Rule: Proposal can be switched state only by specific functions                                                     │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule changes(uint256 pId, env e) {