filtered out timeouts

certora/specs/GovernorBase.spec

@@ -276,8 +276,13 @@ rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
  // non of the proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc 
  // we connected the executed attribute to the execute() function, showing that only execute() can
  // change it, and that it will always change it.
-rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selector != updateQuorumNumerator(uint256).selector && 
-                                                            !f.isFallback && f.selector != updateTimelock(address).selector} {
+rule allFunctionsRevertIfExecuted(method f) filtered { f ->
+    !f.isView && !f.isFallback
+      && f.selector != updateTimelock(address).selector
+      && f.selector != updateQuorumNumerator(uint256).selector
+      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
+      && f.selector != __acceptAdmin().selector
+} {
     env e; calldataarg args;
     uint256 pId;
     require(isExecuted(pId));
@@ -292,8 +297,13 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selec
 /*
  * All proposal specific (non-view) functions should revert if proposal is canceled
  */
-rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView && f.selector != updateQuorumNumerator(uint256).selector && 
-                                                            !f.isFallback && f.selector != updateTimelock(address).selector} {
+rule allFunctionsRevertIfCanceled(method f) filtered {
+    f -> !f.isView && !f.isFallback
+      && f.selector != updateTimelock(address).selector
+      && f.selector != updateQuorumNumerator(uint256).selector
+      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
+      && f.selector != __acceptAdmin().selector
+} {
     env e; calldataarg args;
     uint256 pId;
     require(isCanceled(pId));
@@ -308,7 +318,9 @@ rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView && f.selec
 /*
  * Proposal can be switched to executed only via execute() function
  */
-rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) {
+rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) filtered {
+    f -> f.selector != queue(address[],uint256[],bytes[],bytes32).selector
+} {
     env e; calldataarg args;
     uint256 pId;
     bool executedBefore = isExecuted(pId);

certora/specs/GovernorCountingSimple.spec

@@ -125,36 +125,6 @@ invariant OneIsNotMoreThanAll(uint256 pId)
 //////////////////////////////////////////////////////////////////////////////
 
 
-//NOT FINISHED
-/*
-* the sum of voting power of those who voted is less or equal to the maximum possible votes, per each proposal
-*/
-rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
-
-    // add requireinvariant  for all i, j. i = i - 1 && i < j => checkpointlookup[i] < checkpointlookup[j];
-    require tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId));
-
-    uint256 againstB;
-    uint256 forB;
-    uint256 absatinB;
-    againstB, forB, absatinB = proposalVotes(pId);
-
-    calldataarg args;
-    //f(e, args);
-
-    castVote(e, pId, sup);
-
-    uint256 against;
-    uint256 for;
-    uint256 absatin;
-    against, for, absatin = proposalVotes(pId);
-
-    uint256 ps = proposalSnapshot(pId);
-
-    assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
-}
-
-
 /*
  * Only sender's voting status can be changed by execution of any cast vote function
  */