envfreeViolationFix

certora/harnesses/ERC20VotesHarness.sol

@@ -3,7 +3,7 @@ import "../../contracts/token/ERC20/extensions/ERC20Votes.sol";
 contract ERC20VotesHarness is ERC20Votes {
     constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
 
-    mapping(address => mapping(uint256 => uint256)) _getPastVotes;
+    mapping(address => mapping(uint256 => uint256)) public _getPastVotes;
 
     function _afterTokenTransfer(
         address from,
@@ -26,10 +26,12 @@ contract ERC20VotesHarness is ERC20Votes {
         _getPastVotes[delegatee][block.number] += balanceOf(delegator);
     }
 
+    /*
     function getPastVotes(address account, uint256 blockNumber) public view virtual override returns (uint256) {
         uint256 gpv = super.getPastVotes(account, blockNumber);
         require (_getPastVotes[account][blockNumber] == gpv);
         return gpv;
     }
+    */
 
 }

certora/specs/GovernorBase.spec

@@ -13,7 +13,7 @@ methods {
     castVote(uint256, uint8) returns uint256
 
     // internal functions made public in harness:
-    _quorumReached(uint256) returns bool envfree
+    _quorumReached(uint256) returns bool
     _voteSucceeded(uint256) returns bool envfree
 
 
@@ -23,7 +23,7 @@ methods {
     hashProposal(address[], uint256[], bytes[], bytes32) => CONSTANT
     proposalThreshold() returns uint256 envfree
 
-    getVotes(address, uint256) returns uint256 envfree => DISPATCHER(true)
+    getVotes(address, uint256) returns uint256 => DISPATCHER(true)
     //getVotes(address, uint256) => DISPATCHER(true)
 
     getPastTotalSupply(uint256) returns uint256 envfree => DISPATCHER(true)
@@ -117,8 +117,8 @@ invariant noBothExecutedAndCanceled(uint256 pId)
 /**
  * A proposal could be executed only if quorum was reached and vote succeeded
  */
-invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
-        isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
+invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e) 
+        isExecuted(pId) => _quorumReached(e, pId) && _voteSucceeded(pId)
 
 
 ///////////////////////////////////////////////////////////////////////////////////////

certora/specs/GovernorCountingSimple.spec

@@ -8,12 +8,14 @@ methods {
     // castVoteBySig(uint256,uint8,uint8,bytes32,bytes32) returns uint256
 	
 	snapshot(uint256) returns uint64 envfree
-    quorum(uint256) returns uint256 envfree
+    quorum(uint256) returns uint256
     proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
 
     quorumNumerator() returns uint256
     updateQuorumNumerator(uint256)
     _executor() returns address
+
+    erc20votes._getPastVotes(address, uint256) returns uint256 envfree
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -89,6 +91,8 @@ hook Sstore erc20votes._getPastVotes[KEY address uId][KEY uint256 blockNumber] u
 	                                && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn));
 }
 
+invariant checkGetVotesGhost(address uId, uint256 blockNumber)
+    erc20votes._getPastVotes(uId, blockNumber) == getPastVotes(uId, blockNumber)
 
 
 //////////////////////////////////////////////////////////////////////////////
@@ -183,13 +187,14 @@ rule votingWeightMonotonicity(method f){
 // can't use link because contracts are abstract, they don't have bytecode/constructor
 // add implementation harness
 rule quorumMonotonicity(method f, uint256 blockNumber){
-    uint256 quorumBefore = quorum(blockNumber);
-
     env e; 
+    
+    uint256 quorumBefore = quorum(e, blockNumber);
+    
     calldataarg args;
     f(e, args);
 
-    uint256 quorumAfter = quorum(blockNumber);
+    uint256 quorumAfter = quorum(e, blockNumber);
 
     assert quorumBefore <= quorumAfter, "Quorum was decreased somehow";
 }
@@ -241,7 +246,7 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f -
     address acc = e.msg.sender;
 
     bool hasVotedBefore = hasVoted(e, pId, acc);
-    uint256 votesBefore = getVotes(acc, bn);
+    uint256 votesBefore = getVotes(e, acc, bn);
     require votesBefore > 0;
 
     //calldataarg args;
@@ -253,7 +258,7 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f -
     uint256 abstainAfter = votesAbstain();
     //againstAfter, forAfter, abstainAfter = proposalVotes(pId);
 
-    uint256 votesAfter = getVotes(acc, bn);
+    uint256 votesAfter = getVotes(e, acc, bn);
     bool hasVotedAfter = hasVoted(e, pId, acc);
 
     assert hasVotedBefore != hasVotedAfter => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";