FixinigTimeoutsAndTotalVotes

certora/harnesses/WizardHarness1.sol

@@ -76,7 +76,7 @@ contract WizardHarness1 is Governor, GovernorProposalThreshold, GovernorCounting
         return super.castVoteWithReason(proposalId, support, reason);
     }
 
-    function getExecutor() public returns (address){
+    function getExecutor() public view returns (address){
         return _executor();
     }
 

certora/specs/GovernorBase.spec

@@ -14,6 +14,7 @@ methods {
     hasVoted(uint256, address) returns bool
     castVote(uint256, uint8) returns uint256
     updateQuorumNumerator(uint256)
+    queue(address[], uint256[], bytes[], bytes32) returns uint256
 
 
     // internal functions made public in harness:
@@ -29,8 +30,10 @@ methods {
     getVotes(address, uint256) returns uint256 => DISPATCHER(true)
 
     erc20votes.getPastTotalSupply(uint256) returns uint256
-
     erc20votes.getPastVotes(address, uint256) returns uint256
+
+    scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => NONDET
+    executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => NONDET
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -55,6 +58,9 @@ function callFunctionWithProposal(uint256 proposalId, method f) {
         f@withrevert(e, args);
 	} else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) {
 		castVoteBySig@withrevert(e, proposalId, support, v, r, s);
+    } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) {
+		require targets.length <= 1 && values.length <= 1 && calldatas.length <= 1;
+        queue@withrevert(e, targets, values, calldatas, descriptionHash);
 	} else {
         calldataarg args;
         f@withrevert(e, args);

certora/specs/GovernorCountingSimple.spec

@@ -16,8 +16,6 @@ methods {
     erc20votes._getPastVotes(address, uint256) returns uint256
 
     getExecutor() returns address
-
-    //0xe38335e5 => DISPATCHER(true)
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -133,11 +131,35 @@ invariant OneIsNotMoreThanAll(uint256 pId)
 /*
 * totalVotesPossible >= votePower(id)
 */
-invariant possibleTotalVotes(uint256 pId, env e) 
-	tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId))
+//invariant possibleTotalVotes(uint256 pId, env e) 
+//	tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId))
+
+rule possibleTotalVotes(uint256 pId, env e, method f) {
+    require tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId));
+
+    calldataarg args;
+    f(e, args);
+
+    assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
+}
+
+//invariant voteGettersCheck(uint256 pId, address acc, env e) 
+//	erc20votes.getPastVotes(e, acc, proposalSnapshot(pId)) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId))
 
-invariant voteGettersCheck(uint256 pId, address acc, env e) 
-	erc20votes.getPastVotes(e, acc, proposalSnapshot(pId)) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId))
+rule voteGettersCheck(uint256 pId, address acc, env e, method f){
+    address[] targets;
+    uint256[] values;
+    bytes[] calldatas;
+
+    require erc20votes.getPastVotes(e, acc, proposalSnapshot(pId)) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId));
+    
+    uint256 result = callPropose(e, targets, values, calldatas);
+
+    require result == pId;
+
+    assert erc20votes.getPastVotes(e, acc, proposalSnapshot(pId)) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)),
+            "getPastVotes is greater";
+}
 
 /*
 * totalVotesPossible >= votePower(id)

contracts/governance/extensions/GovernorTimelockControl.sol

@@ -92,7 +92,8 @@ abstract contract GovernorTimelockControl is IGovernorTimelock, Governor {
 
         uint256 delay = _timelock.getMinDelay();
         _timelockIds[proposalId] = _timelock.hashOperationBatch(targets, values, calldatas, 0, descriptionHash);
-        _timelock.scheduleBatch(targets, values, calldatas, 0, descriptionHash, delay);
+        // HARNESS
+        //_timelock.scheduleBatch(targets, values, calldatas, 0, descriptionHash, delay);
 
         emit ProposalQueued(proposalId, block.timestamp + delay);