Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into remotes/origin/certora/erc20

certora/harnesses/ERC20VotesHarness.sol

@@ -2,27 +2,4 @@ import "../munged/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)) public _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);
-    }
 }

certora/specs/GovernorCountingSimple.spec

@@ -1,7 +1,5 @@
 import "GovernorBase.spec"
 
-using ERC20VotesHarness as erc20votes
-
 methods {
     ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
 
@@ -11,8 +9,6 @@ methods {
     quorumNumerator() returns uint256
     _executor() returns address
 
-    erc20votes._getPastVotes(address, uint256) returns uint256
-
     getExecutor() returns address
 
     timelock() returns address