update

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(

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)
     {

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";
-}

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) {