sanity rule preparations

certora/harnesses/GovernorProposalThresholdHarness.sol

@@ -15,12 +15,12 @@ contract GovernorProposalThresholdHarness is GovernorProposalThreshold {
     }
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
@@ -53,6 +53,11 @@ contract GovernorProposalThresholdHarness is GovernorProposalThreshold {
         // havoc something
     }
 
+    uint256 _proposalThreshold;
+    function proposalThreshold() public view override virtual returns (uint256) {
+        return _proposalThreshold;
+    }
+
     constructor(string memory name) Governor(name) {}
 
 }

certora/harnesses/GovernorTimelockCompoundHarness.sol

@@ -15,12 +15,12 @@ contract GovernorTimelockCompoundHarness is GovernorTimelockCompound {
     }
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 

certora/harnesses/GovernorVotesHarness.sol

@@ -9,12 +9,12 @@ contract GovernorVotesHarness is GovernorVotes {
     }
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
@@ -47,6 +47,5 @@ contract GovernorVotesHarness is GovernorVotes {
         // havoc something
     }
 
-    constructor(string memory name) Governor(name) {}
-
+    constructor(ERC20Votes tokenAddr) GovernorVotes(tokenAddr) {}
 }

certora/harnesses/GovernorVotesQuorumFractionHarness.sol

@@ -1,14 +1,14 @@
-import "../../contracts/governance/extensions/GovernorVotesQuorumFractionGovernor.sol";
+import "../../contracts/governance/extensions/GovernorVotesQuorumFraction.sol";
 
 contract GovernorVotesQuorumFractionHarness is GovernorVotesQuorumFraction {
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 

certora/scripts/check.sh

@@ -4,4 +4,6 @@ Contract=$1
 Spec=$2
 shift 2
 certoraRun certora/harnesses/${Contract}Harness.sol \
-    --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@"
+    --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@" \
+    --solc solc8.0
+    

certora/scripts/sanity.sh

@@ -0,0 +1,9 @@
+for f in certora/harnesses/*.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+    --solc solc8.0    
+done

certora/specs/sanity.spec

@@ -0,0 +1,14 @@
+/*
+This rule looks for a non-reverting execution path to each method, including those overridden in the harness.
+A method has such an execution path if it violates this rule.
+How it works:
+    - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails.
+    - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously.
+*/
+	
+rule sanity(method f) {
+    env e;
+    calldataarg arg;
+    f(e, arg);
+    assert false;
+}

contracts/governance/Governor.sol

@@ -154,12 +154,12 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor {
     /**
      * @dev Amount of votes already cast passes the threshold limit.
      */
-    function _quorumReached(uint256 proposalId) internal view virtual returns (bool);
+    function _quorumReached(uint256 proposalId) public view virtual returns (bool);
 
     /**
      * @dev Is the proposal successful or not.
      */
-    function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool);
 
     /**
      * @dev Register a vote with a given support and voting weight.

contracts/governance/extensions/GovernorCountingSimple.sol

@@ -64,7 +64,7 @@ abstract contract GovernorCountingSimple is Governor {
     /**
      * @dev See {Governor-_quorumReached}.
      */
-    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
         ProposalVote storage proposalvote = _proposalVotes[proposalId];
 
         return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
@@ -73,7 +73,7 @@ abstract contract GovernorCountingSimple is Governor {
     /**
      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
      */
-    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
         ProposalVote storage proposalvote = _proposalVotes[proposalId];
 
         return proposalvote.forVotes > proposalvote.againstVotes;