8.5/10 rules finished

certora/applyHarness.patch

@@ -24,7 +24,7 @@ diff -ruN governance/Governor.sol governance/Governor.sol
      // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
 diff -ruN governance/TimelockController.sol governance/TimelockController.sol
 --- governance/TimelockController.sol	2022-05-06 13:44:28.000000000 -0700
-+++ governance/TimelockController.sol	2022-05-12 19:13:19.000000000 -0700
++++ governance/TimelockController.sol	2022-05-15 14:10:49.000000000 -0700
 @@ -24,10 +24,10 @@
      bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE");
      bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
@@ -44,7 +44,7 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol
      ) private {
 -        (bool success, ) = target.call{value: value}(data);
 -        require(success, "TimelockController: underlying transaction reverted");
-+        return; // can't deal with external calls
++        return; // haven't dealt with external calls yet
 +        // (bool success, ) = target.call{value: value}(data);
 +        // require(success, "TimelockController: underlying transaction reverted");
  
@@ -401,12 +401,12 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/
  }
 diff -ruN utils/Address.sol utils/Address.sol
 --- utils/Address.sol	2022-05-06 13:43:21.000000000 -0700
-+++ utils/Address.sol	2022-05-15 10:58:38.000000000 -0700
++++ utils/Address.sol	2022-05-16 14:24:44.000000000 -0700
 @@ -131,6 +131,7 @@
          uint256 value,
          string memory errorMessage
      ) internal returns (bytes memory) {
-+        return "";
++        return ""; // external calls havoc
          require(address(this).balance >= value, "Address: insufficient balance for call");
          require(isContract(target), "Address: call to non-contract");
  

certora/harnesses/GovernorPreventLateQuorumHarness.sol

@@ -35,6 +35,10 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
         return _extendedDeadlines[id].isUnset();
     }
 
+    function getExtendedDeadlineIsStarted(uint256 id) public view returns(bool) {
+        return _extendedDeadlines[id].isStarted();
+    }
+
     function getExtendedDeadline(uint256 id) public view returns(uint64) {
         return _extendedDeadlines[id].getDeadline();
     }
@@ -49,15 +53,6 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
         return _voteSucceeded(proposalId);
     }
 
-    function countVote(uint256 proposalId,
-        address account,
-        uint8 support,
-        uint256 weight,
-        bytes memory // params
-        ) public view {
-        return _countVote(proposalId,account,support,weight,"");
-    }
-
     // Harness from Governor //
 
     function getExecutor() public view returns (address){

certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -1,12 +1,12 @@
 certoraRun \
     certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
-    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorCountingSimple.spec \
+    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
     --solc solc \
     --optimistic_loop \
-    --loop_iter 1 \
+    --disable_auto_cache_key_gen \
     --staging \
-    --rule_sanity advanced \
     --send_only \
+    --loop_iter 1 \
     --rule $1 \
     --msg "$1" \
 

certora/specs/GovernorBase.spec

@@ -70,7 +70,6 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
         calldataarg args;
         f@withrevert(e, args);
     }
-   
 }
 
 /*

certora/specs/GovernorCountingSimple.spec

@@ -183,7 +183,8 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
     
     bool hasVotedAfter = hasVoted(e, pId, acc);
 
-    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter, "no correlation";
+    // want all vote categories to not decrease and at least one category to increase
+    assert (!hasVotedBefore && hasVotedAfter) => (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), "no correlation: some category decreased";
 }
 
 

certora/specs/GovernorPreventLateQuorum.spec

@@ -1,22 +1,8 @@
-//////////////////////////////////////////////////////////////////////////////
-///////////////////// Governor.sol base definitions //////////////////////////
-//////////////////////////////////////////////////////////////////////////////
+import "GovernorCountingSimple.spec"
 
 using ERC721VotesHarness as erc721votes
-using ERC20VotesHarness as erc20votes
 
 methods {
-    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
-    proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd
-    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
-    isExecuted(uint256) returns bool envfree
-    isCanceled(uint256) returns bool envfree
-    execute(address[], uint256[], bytes[], bytes32) returns uint256
-    hasVoted(uint256, address) returns bool
-    castVote(uint256, uint8) returns uint256
-    updateQuorumNumerator(uint256)
-    queue(address[], uint256[], bytes[], bytes32) returns uint256
-    quorumNumerator() returns uint256 envfree
     quorumDenominator() returns uint256 envfree
     votingPeriod() returns uint256 envfree
     lateQuorumVoteExtension() returns uint64 envfree
@@ -24,20 +10,12 @@ methods {
 
     // harness
     getExtendedDeadlineIsUnset(uint256) returns bool envfree
+    getExtendedDeadlineIsStarted(uint256) returns bool envfree
     getExtendedDeadline(uint256) returns uint64 envfree
-    quorumReached(uint256) returns bool envfree
-    voteSucceeded(uint256) returns bool envfree
-    quorum(uint256) returns uint256
-    latestCastVoteCall() returns uint256 envfree // more robust check than f.selector == _castVote(...).selector
+    
+    // more robust check than f.selector == _castVote(...).selector
+    latestCastVoteCall() returns uint256 envfree 
 
-    // function summarization
-    proposalThreshold() returns uint256 envfree
-
-    // erc20votes dispatch
-    getVotes(address, uint256) returns uint256 => DISPATCHER(true)
-    // erc721votes/Votes dispatch
-    getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true)
-    getPastVotes(address, uint256) returns uint256 => DISPATCHER(true)
     // timelock dispatch
     getMinDelay() returns uint256 => DISPATCHER(true)
     
@@ -46,34 +24,72 @@ methods {
     scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT
 }
 
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////// Helper Functions ///////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env e) {
+    string reason; uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params;
+    if (f.selector == castVote(uint256, uint8).selector) {
+		castVote@withrevert(e, proposalId, support);
+	} else if  (f.selector == castVoteWithReason(uint256, uint8, string).selector) {
+        castVoteWithReason@withrevert(e, proposalId, support, reason);
+	} else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) {
+		castVoteBySig@withrevert(e, proposalId, support, v, r, s);
+	} else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) {
+        castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s);
+    } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) {
+        castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params);
+    } else {
+        calldataarg args;
+        f@withrevert(e, args);
+    }
+}
+
+
 //////////////////////////////////////////////////////////////////////////////
 //////////////////////////////// Definitions /////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
-// where can invariants help?
-// can I replace definitions with invariants?
+// proposal deadline can be extended (but isn't)
+definition deadlineExtendable(env e, uint256 pId) returns bool = 
+    getExtendedDeadlineIsUnset(pId)
+    && !quorumReached(e, pId);
 
-// create definition for extended
-definition deadlineCanBeExtended(uint256 pId) returns bool = 
-    getExtendedDeadlineIsUnset(pId) &&
-    !quorumReached(pId);
+// proposal deadline has been extended
+definition deadlineExtended(env e, uint256 pId) returns bool = 
+    getExtendedDeadlineIsStarted(pId)
+    && quorumReached(e, pId);
 
-definition deadlineHasBeenExtended(uint256 pId) returns bool = 
-    !getExtendedDeadlineIsUnset(pId) &&
-    quorumReached(pId);
 
-definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// Invariants /////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+/*
+ * I1: A propsal must be in state deadlineExtendable or deadlineExtended.
+ * --INVARIANT PASSING // fails for updateQuorumNumerator
+ * --ADVANCED SANITY PASSING // can't sanity test failing rules, not sure how it works for invariants
+ */
+invariant proposalInOneState(env e, uint256 pId)
+    deadlineExtendable(e, pId) || deadlineExtended(e, pId)
+    { preserved { require proposalCreated(pId); } }
+
 
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////////// Rules /////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
-// RULE deadline can only be extended only once PASSING but vacuous
-    // 1. if deadline changes then we have state transition to deadlineHasBeenExtended RULE PASSING; ADV SANITY PASSING
-rule deadlineChangeEffects(method f) 
-    filtered {
-        f -> !f.isView
-    } {
+///////////////////////////// first set of rules /////////////////////////////
+
+// R1 and R2 are assumed in R3, so we prove them first
+/*
+ * R1: If deadline increases then we are in deadlineExtended state and castVote was called.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING 
+ */ 
+rule deadlineChangeEffects(method f) filtered {f -> !f.isView} {
     env e; calldataarg args; uint256 pId;
 
     require (proposalCreated(pId));
@@ -82,10 +98,15 @@ rule deadlineChangeEffects(method f)
     f(e, args);
     uint256 deadlineAfter = proposalDeadline(pId);
     
-    assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(pId));
+    assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId));
 }
 
-    // 2. cant unextend RULE PASSING*; ADV SANITY PASSING
+
+/*
+ * R2: A proposal can't leave deadlineExtended state.
+ * RULE PASSING*
+ * ADVANCED SANITY PASSING 
+ */ 
 rule deadlineCantBeUnextended(method f) 
     filtered {
         f -> !f.isView
@@ -93,23 +114,24 @@ rule deadlineCantBeUnextended(method f)
     } {
     env e; calldataarg args; uint256 pId;
 
-    require(deadlineHasBeenExtended(pId));
+    require(deadlineExtended(e, pId));
     require(proposalCreated(pId));
     
     f(e, args);
     
-    assert(deadlineHasBeenExtended(pId));
+    assert(deadlineExtended(e, pId));
 }
 
-    // 3. extended => can't change deadline RULE PASSING; ADV SANITY PASSING
-        //@note if deadline changed, then it wasnt extended and castvote was called
-rule canExtendDeadlineOnce(method f) 
-    filtered {
-        f -> !f.isView 
-    } {
+
+/*
+ * R3: A proposal's deadline can't change in deadlineExtended state.
+ * RULE PASSING*
+ * ADVANCED SANITY PASSING 
+ */ 
+rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} {
     env e; calldataarg args; uint256 pId;
 
-    require(deadlineHasBeenExtended(pId));
+    require(deadlineExtended(e, pId));
     require(proposalCreated(pId)); 
     
     uint256 deadlineBefore = proposalDeadline(pId);
@@ -118,3 +140,145 @@ rule canExtendDeadlineOnce(method f)
     
     assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice");
 }
+
+
+//////////////////////////// second set of rules ////////////////////////////
+
+// HIGH LEVEL RULE R6: deadline can only extended if quorum reached w/ <= timeOfExtension left to vote
+// I1, R4 and R5 are assumed in R6 so we prove them first
+
+/*
+ * R4: A change in hasVoted must be correlated with an increasing of the vote supports, i.e. casting a vote increases the total number of votes.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING
+ */
+rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isView} {
+    address acc = e.msg.sender;
+
+    require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power
+    
+    uint256 againstBefore = votesAgainst();
+    uint256 forBefore = votesFor();
+    uint256 abstainBefore = votesAbstain();
+
+    bool hasVotedBefore = hasVoted(e, pId, acc);
+
+    helperFunctionsWithRevertOnlyCastVote(pId, f, e);
+
+    uint256 againstAfter = votesAgainst();
+    uint256 forAfter = votesFor();
+    uint256 abstainAfter = votesAbstain();
+    
+    bool hasVotedAfter = hasVoted(e, pId, acc);
+
+    // want all vote categories to not decrease and at least one category to increase
+    assert 
+        (!hasVotedBefore && hasVotedAfter) => 
+        (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), 
+        "no correlation: some category decreased"; // currently vacous but keeping for CI tests
+    assert 
+        (!hasVotedBefore && hasVotedAfter) => 
+        (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter),
+        "no correlation: no category increased";
+}
+
+
+/*
+ * R5: An against vote does not make a proposal reach quorum.
+ * RULE PASSING
+ * --ADVANCED SANITY PASSING vacuous but keeping
+ */
+rule againstVotesDontCount(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId; 
+    address acc = e.msg.sender;
+    
+    bool quorumBefore = quorumReached(e, pId);
+    uint256 againstBefore = votesAgainst();
+
+    f(e, args);
+
+    bool quorumAfter = quorumReached(e, pId);
+    uint256 againstAfter = votesAgainst();
+
+    assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum reached with against vote"; 
+}
+
+/*
+ * R6: Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote
+ * RULE PASSING
+ * ADVANCED SANITY PASSING 
+ */
+rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+
+    // need invariant that proves that a propsal must be in state deadlineExtendable or deadlineExtended
+    require(deadlineExtended(e, pId) || deadlineExtendable(e, pId));
+    require(proposalCreated(pId));
+
+    bool wasDeadlineExtendable = deadlineExtendable(e, pId);
+    uint64 extension = lateQuorumVoteExtension();
+    uint256 deadlineBefore = proposalDeadline(pId);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(pId);
+    
+    assert(deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline was not extendable");
+    assert(deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used");
+}
+
+/*
+ * R7: `extendedDeadlineField` is set iff `_castVote` is called and quroum is reached.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING 
+ */
+rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+    require(deadlineExtended(e, pId) || deadlineExtendable(e, pId));
+    
+    bool extendedBefore = deadlineExtended(e, pId);
+    f(e, args);
+    bool extendedAfter = deadlineExtended(e, pId);
+    uint256 extDeadline = getExtendedDeadline(pId);
+    
+    assert(
+        !extendedBefore && extendedAfter
+        => extDeadline == e.block.number + lateQuorumVoteExtension(),
+        "extended deadline was not set"
+    );
+}
+
+/*
+* R8: If the deadline for a proposal has not been reached, users can still vote.
+* --RULE PASSING
+* --ADVANCED SANITY PASSING
+*/
+rule canVote(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+    address acc = e.msg.sender;
+    uint256 deadline = proposalDeadline(pId);
+    bool votedBefore = hasVoted(e, pId, acc);
+    
+    require(proposalCreated(pId));
+    require(deadline >= e.block.number);
+    // last error? 
+    helperFunctionsWithRevertOnlyCastVote(pId, f, e);
+    bool votedAfter = hasVoted(e, pId, acc);
+    
+    assert !votedBefore && votedAfter => deadline >= e.block.number;
+}
+
+/*
+ * R9: Deadline can never be reduced.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING
+ */
+rule deadlineNeverReduced(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+    require(proposalCreated(pId));
+
+    uint256 deadlineBefore = proposalDeadline(pId);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(pId);
+
+    assert(deadlineAfter >= deadlineBefore);
+}
+