From ec5d501791f3ac6794ed11a97306ce9afff06c6f Mon Sep 17 00:00:00 2001
From: Michael George <mdgeorge@cs.cornell.edu>
Date: Thu, 2 Dec 2021 15:06:29 -0500
Subject: [PATCH] filtered out timeouts

---
 certora/specs/GovernorBase.spec           | 22 +++++++++++++----
 certora/specs/GovernorCountingSimple.spec | 30 -----------------------
 2 files changed, 17 insertions(+), 35 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 8487804ab..7cec399c2 100644
--- a/certora/specs/GovernorBase.spec
+++ b/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);
diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec
index 47f67aa90..6d2d5fbb7 100644
--- a/certora/specs/GovernorCountingSimple.spec
+++ b/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
  */