AddedLinkAndFixingGhost

certora/harnesses/ERC20VotesHarness.sol

@@ -2,4 +2,34 @@ 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;
+
+    function _afterTokenTransfer(
+        address from,
+        address to,
+        uint256 amount
+    ) internal virtual override {
+        super._afterTokenTransfer(from, to, amount);
+        _getPastVotes[from][block.number] -= amount;
+        _getPastVotes[to][block.number] += amount;
+    }
+
+    /**
+     * @dev Change delegation for `delegator` to `delegatee`.
+     *
+     * Emits events {DelegateChanged} and {DelegateVotesChanged}.
+     */
+    function _delegate(address delegator, address delegatee) internal virtual override{
+        super._delegate(delegator, delegatee);
+        _getPastVotes[delegator][block.number] -= balanceOf(delegator);
+        _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/scripts/GovernorCountingSimple-counting.sh

@@ -1,4 +1,4 @@
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
+certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
     --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
     --solc solc8.2 \
     --staging shelly/forSasha \

certora/scripts/WizardHarness1.sh

@@ -1,8 +1,9 @@
 certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardHarness1.sol \
+    --link WizardHarness1:token=ERC20VotesHarness \
     --verify WizardHarness1:certora/specs/GovernorCountingSimple.spec \
     --solc solc8.2 \
     --staging shelly/forSasha \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
-    --rule SumOfVotesCastEqualSumOfPowerOfVoted \
+    --rule hasVotedCorrelation \
     --msg "$1"

certora/specs/GovernorCountingSimple.spec

@@ -1,5 +1,7 @@
 import "GovernorBase.spec"
 
+using ERC20VotesHarness as erc20votes
+
 methods {
     ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
     // castVote(uint256, uint8) returns uint256
@@ -81,12 +83,11 @@ ghost totalVotesPossible(uint256) returns uint256 {
 }
 
 // Was done with _getVotes by mistake. Should check GovernorBasicHarness but _getVotes is from GovernorHarness
-//hook Sstore _getVotes[KEY address uId][KEY uint256 blockNumber] uint256 voteWeight(uint256 old_voteWeight) STORAGE {
-//	havoc totalVotesPossible assuming forall uint256 bn.
-//	                                (bn == blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn) - old_voteWeight + voteWeight)
-//	                                && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn));
-//    
-//}
+hook Sstore erc20votes._getPastVotes[KEY address uId][KEY uint256 blockNumber] uint256 voteWeight(uint256 old_voteWeight) STORAGE {
+	havoc totalVotesPossible assuming forall uint256 bn.
+	                                (bn == blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn) - old_voteWeight + voteWeight)
+	                                && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn));
+}
 
 
 
@@ -118,8 +119,8 @@ invariant OneIsNotMoreThanAll(uint256 pId)
 /*
 * totalVotesPossible >= votePower(id)
 */
-//invariant possibleTotalVotes(uint256 pId) 
-//	tracked_weight(pId) <= totalVotesPossible(snapshot(pId))
+invariant possibleTotalVotes(uint256 pId) 
+	tracked_weight(pId) <= totalVotesPossible(snapshot(pId))
 
 /*
 * totalVotesPossible >= votePower(id)
@@ -255,7 +256,7 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f -
     uint256 votesAfter = getVotes(acc, bn);
     bool hasVotedAfter = hasVoted(e, pId, acc);
 
-    assert hasVotedBefore != hasVotedAfter => againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter, "no correlation";
+    assert hasVotedBefore != hasVotedAfter => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
 }
 
 

contracts/token/ERC20/extensions/ERC20Votes.sol

@@ -84,7 +84,7 @@ abstract contract ERC20Votes is ERC20Permit {
      *
      * - `blockNumber` must have been already mined
      */
-    function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) {
+    function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) {
         require(blockNumber < block.number, "ERC20Votes: block not yet mined");
         return _checkpointsLookup(_checkpoints[account], blockNumber);
     }