openzeppelin-contracts/certora/applyHarness.patch

diff -druN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
--- governance/extensions/GovernorCountingSimple.sol	2023-02-27 10:59:32.652558153 +0100
+++ governance/extensions/GovernorCountingSimple.sol	2023-02-28 16:49:10.417726143 +0100
@@ -27,7 +27,7 @@
         mapping(address => bool) hasVoted;
     }
 
-    mapping(uint256 => ProposalVote) private _proposalVotes;
+    mapping(uint256 => ProposalVote) internal _proposalVotes; // HARNESS: private -> internal
 
     /**
      * @dev See {IGovernor-COUNTING_MODE}.
diff -druN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
--- governance/extensions/GovernorPreventLateQuorum.sol	2023-02-27 10:59:32.652558153 +0100
+++ governance/extensions/GovernorPreventLateQuorum.sol	2023-02-28 16:49:10.417726143 +0100
@@ -20,10 +20,10 @@
 abstract contract GovernorPreventLateQuorum is Governor {
     using SafeCast for uint256;
 
-    uint64 private _voteExtension;
+    uint64 internal _voteExtension; // HARNESS: private -> internal
 
     /// @custom:oz-retyped-from mapping(uint256 => Timers.BlockNumber)
-    mapping(uint256 => uint64) private _extendedDeadlines;
+    mapping(uint256 => uint64) internal _extendedDeadlines; // HARNESS: private -> internal
 
     /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
     event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
diff -druN governance/extensions/GovernorVotesQuorumFraction.sol governance/extensions/GovernorVotesQuorumFraction.sol
--- governance/extensions/GovernorVotesQuorumFraction.sol	2023-02-27 10:59:32.655891529 +0100
+++ governance/extensions/GovernorVotesQuorumFraction.sol	2023-02-28 16:49:10.417726143 +0100
@@ -17,10 +17,10 @@
     using SafeCast for *;
     using Checkpoints for Checkpoints.Trace224;
 
-    uint256 private _quorumNumerator; // DEPRECATED in favor of _quorumNumeratorHistory
+    uint256 internal _quorumNumerator; // DEPRECATED // MUNGED private => internal
 
     /// @custom:oz-retyped-from Checkpoints.History
-    Checkpoints.Trace224 private _quorumNumeratorHistory;
+    Checkpoints.Trace224 internal _quorumNumeratorHistory; // MUNGED private => internal
 
     event QuorumNumeratorUpdated(uint256 oldQuorumNumerator, uint256 newQuorumNumerator);
 
diff -druN governance/Governor.sol governance/Governor.sol
--- governance/Governor.sol	2023-02-27 10:59:32.652558153 +0100
+++ governance/Governor.sol	2023-02-28 16:49:10.421059488 +0100
@@ -51,7 +51,7 @@
     string private _name;
 
     /// @custom:oz-retyped-from mapping(uint256 => Governor.ProposalCore)
-    mapping(uint256 => ProposalCore) private _proposals;
+    mapping(uint256 => ProposalCore) internal _proposals; // HARNESS: private -> internal
 
     // This queue keeps track of the governor operating on itself. Calls to functions protected by the
     // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
diff -druN governance/TimelockController.sol governance/TimelockController.sol
--- governance/TimelockController.sol	2023-02-27 10:59:32.652558153 +0100
+++ governance/TimelockController.sol	2023-02-28 16:49:10.421059488 +0100
@@ -28,10 +28,10 @@
     bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
     bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
     bytes32 public constant CANCELLER_ROLE = keccak256("CANCELLER_ROLE");
-    uint256 internal constant _DONE_TIMESTAMP = uint256(1);
+    uint256 public constant _DONE_TIMESTAMP = uint256(1); // HARNESS: internal -> public
 
     mapping(bytes32 => uint256) private _timestamps;
-    uint256 private _minDelay;
+    uint256 public _minDelay; // HARNESS: private -> public
 
     /**
      * @dev Emitted when a call is scheduled as part of operation `id`.
diff -druN governance/utils/Votes.sol governance/utils/Votes.sol
--- governance/utils/Votes.sol	2023-02-27 10:59:32.655891529 +0100
+++ governance/utils/Votes.sol	2023-02-28 16:49:10.421059488 +0100
@@ -35,7 +35,25 @@
     bytes32 private constant _DELEGATION_TYPEHASH =
         keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
 
-    mapping(address => address) private _delegation;
+    // HARNESS : Hooks cannot access any information from Checkpoints yet, so I am also updating votes and fromBlock in this struct
+    struct Ckpt {
+        uint32 fromBlock;
+        uint224 votes;
+    }
+    mapping(address => Ckpt) public _checkpoints;
+
+    // HARNESSED getters
+    function numCheckpoints(address account) public view returns (uint32) {
+        return SafeCast.toUint32(_delegateCheckpoints[account]._checkpoints.length);
+    }
+    function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
+        return _delegateCheckpoints[account]._checkpoints[pos]._key;
+    }
+    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
+        return _delegateCheckpoints[account]._checkpoints[pos]._value;
+    }
+
+    mapping(address => address) public _delegation; // HARNESS: private -> public
 
     /// @custom:oz-retyped-from mapping(address => Checkpoints.History)
     mapping(address => Checkpoints.Trace224) private _delegateCheckpoints;
@@ -240,5 +258,5 @@
     /**
      * @dev Must return the voting units held by an account.
      */
-    function _getVotingUnits(address) internal view virtual returns (uint256);
+    function _getVotingUnits(address) public view virtual returns (uint256); // HARNESS: internal -> public
 }
diff -druN proxy/utils/Initializable.sol proxy/utils/Initializable.sol
--- proxy/utils/Initializable.sol	2023-02-27 10:59:32.655891529 +0100
+++ proxy/utils/Initializable.sol	2023-02-28 16:49:10.421059488 +0100
@@ -60,12 +60,12 @@
      * @dev Indicates that the contract has been initialized.
      * @custom:oz-retyped-from bool
      */
-    uint8 private _initialized;
+    uint8 internal _initialized; // HARNESS: private -> internal
 
     /**
      * @dev Indicates that the contract is in the process of being initialized.
      */
-    bool private _initializing;
+    bool internal _initializing; // HARNESS: private -> internal
 
     /**
      * @dev Triggered when the contract has been initialized or reinitialized.
diff -druN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
--- token/ERC1155/ERC1155.sol	2023-02-27 10:59:32.655891529 +0100
+++ token/ERC1155/ERC1155.sol	2023-02-28 16:49:10.421059488 +0100
@@ -21,7 +21,7 @@
     using Address for address;
 
     // Mapping from token ID to account balances
-    mapping(uint256 => mapping(address => uint256)) private _balances;
+    mapping(uint256 => mapping(address => uint256)) internal _balances; // HARNESS: private -> internal
 
     // Mapping from account to operator approvals
     mapping(address => mapping(address => bool)) private _operatorApprovals;
@@ -451,7 +451,7 @@
         uint256 id,
         uint256 amount,
         bytes memory data
-    ) private {
+    ) public { // HARNESS: private -> public
         if (to.isContract()) {
             try IERC1155Receiver(to).onERC1155Received(operator, from, id, amount, data) returns (bytes4 response) {
                 if (response != IERC1155Receiver.onERC1155Received.selector) {
@@ -472,7 +472,7 @@
         uint256[] memory ids,
         uint256[] memory amounts,
         bytes memory data
-    ) private {
+    ) public { // HARNESS: private -> public
         if (to.isContract()) {
             try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns (
                 bytes4 response
diff -druN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
--- token/ERC20/ERC20.sol	2023-02-27 10:59:32.655891529 +0100
+++ token/ERC20/ERC20.sol	2023-02-28 16:49:10.421059488 +0100
@@ -248,7 +248,7 @@
      *
      * - `account` cannot be the zero address.
      */
-    function _mint(address account, uint256 amount) internal virtual {
+    function _mint(address account, uint256 amount) public virtual { // HARNESS: internal -> public
         require(account != address(0), "ERC20: mint to the zero address");
 
         _beforeTokenTransfer(address(0), account, amount);
@@ -274,7 +274,7 @@
      * - `account` cannot be the zero address.
      * - `account` must have at least `amount` tokens.
      */
-    function _burn(address account, uint256 amount) internal virtual {
+    function _burn(address account, uint256 amount) public virtual { // HARNESS: internal -> public
         require(account != address(0), "ERC20: burn from the zero address");
 
         _beforeTokenTransfer(account, address(0), amount);
diff -druN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Capped.sol
--- token/ERC20/extensions/ERC20Capped.sol	2023-02-22 15:43:36.624717708 +0100
+++ token/ERC20/extensions/ERC20Capped.sol	2023-02-28 16:49:10.421059488 +0100
@@ -30,7 +30,7 @@
     /**
      * @dev See {ERC20-_mint}.
      */
-    function _mint(address account, uint256 amount) internal virtual override {
+    function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public
         require(ERC20.totalSupply() + amount <= cap(), "ERC20Capped: cap exceeded");
         super._mint(account, amount);
     }
diff -druN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
--- token/ERC20/extensions/ERC20FlashMint.sol	2023-02-27 10:59:32.655891529 +0100
+++ token/ERC20/extensions/ERC20FlashMint.sol	2023-02-28 16:49:10.421059488 +0100
@@ -53,9 +53,11 @@
         // silence warning about unused variable without the addition of bytecode.
         token;
         amount;
-        return 0;
+        return fee; // HARNESS: made "return" nonzero
     }
 
+    uint256 public fee; // HARNESS: added it to simulate random fee amount
+
     /**
      * @dev Returns the receiver address of the flash fee. By default this
      * implementation returns the address(0) which means the fee amount will be burnt.
diff -druN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
--- token/ERC20/extensions/ERC20Votes.sol	2023-02-27 10:59:32.655891529 +0100
+++ token/ERC20/extensions/ERC20Votes.sol	2023-02-28 16:49:10.421059488 +0100
@@ -33,8 +33,8 @@
     bytes32 private constant _DELEGATION_TYPEHASH =
         keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
 
-    mapping(address => address) private _delegates;
-    mapping(address => Checkpoint[]) private _checkpoints;
+    mapping(address => address) public _delegates; // HARNESS: private -> public
+    mapping(address => Checkpoint[]) public _checkpoints;  // HARNESS: private -> public
     Checkpoint[] private _totalSupplyCheckpoints;
 
     /**
@@ -186,27 +186,27 @@
     /**
      * @dev Maximum token supply. Defaults to `type(uint224).max` (2^224^ - 1).
      */
-    function _maxSupply() internal view virtual returns (uint224) {
+    function _maxSupply() public view virtual returns (uint224) {  // HARNESS: internal -> public
         return type(uint224).max;
     }
 
     /**
      * @dev Snapshots the totalSupply after it has been increased.
      */
-    function _mint(address account, uint256 amount) internal virtual override {
+    function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public
         super._mint(account, amount);
         require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes");
 
-        _writeCheckpoint(_totalSupplyCheckpoints, _add, amount);
+        _writeCheckpointAdd(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer
     }
 
     /**
      * @dev Snapshots the totalSupply after it has been decreased.
      */
-    function _burn(address account, uint256 amount) internal virtual override {
+    function _burn(address account, uint256 amount) public virtual override { // HARNESS: internal -> public (to comply with the ERC20 harness)
         super._burn(account, amount);
 
-        _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount);
+        _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer
     }
 
     /**
@@ -225,7 +225,7 @@
      *
      * Emits events {IVotes-DelegateChanged} and {IVotes-DelegateVotesChanged}.
      */
-    function _delegate(address delegator, address delegatee) internal virtual {
+    function _delegate(address delegator, address delegatee) public virtual { // HARNESS: internal -> public
         address currentDelegate = delegates(delegator);
         uint256 delegatorBalance = balanceOf(delegator);
         _delegates[delegator] = delegatee;
@@ -238,35 +238,60 @@
     function _moveVotingPower(address src, address dst, uint256 amount) private {
         if (src != dst && amount > 0) {
             if (src != address(0)) {
-                (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[src], _subtract, amount);
+                (uint256 oldWeight, uint256 newWeight) = _writeCheckpointSub(_checkpoints[src], amount); // HARNESS: new version without pointer
                 emit DelegateVotesChanged(src, oldWeight, newWeight);
             }
 
             if (dst != address(0)) {
-                (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount);
+                (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount); // HARNESS: new version without pointer
                 emit DelegateVotesChanged(dst, oldWeight, newWeight);
             }
         }
     }
 
-    function _writeCheckpoint(
-        Checkpoint[] storage ckpts,
-        function(uint256, uint256) view returns (uint256) op,
-        uint256 delta
-    ) private returns (uint256 oldWeight, uint256 newWeight) {
+    // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool
+    // function _writeCheckpoint(
+    //     Checkpoint[] storage ckpts,
+    //     function(uint256, uint256) view returns (uint256) op,
+    //     uint256 delta
+    // ) private returns (uint256 oldWeight, uint256 newWeight) {
+    //     uint256 pos = ckpts.length;
+
+    //     unchecked {
+    //         Checkpoint memory oldCkpt = pos == 0 ? Checkpoint(0, 0) : _unsafeAccess(ckpts, pos - 1);
+
+    //         oldWeight = oldCkpt.votes;
+    //         newWeight = op(oldWeight, delta);
+
+    //         if (pos > 0 && oldCkpt.fromBlock == clock()) {
+    //             _unsafeAccess(ckpts, pos - 1).votes = SafeCast.toUint224(newWeight);
+    //         } else {
+    //             ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
+    //         }
+    //     }
+    // }
+
+    function _writeCheckpointAdd(Checkpoint[] storage ckpts, uint256 delta) private returns (uint256 oldWeight, uint256 newWeight) {
         uint256 pos = ckpts.length;
+        oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
+        newWeight = _add(oldWeight, delta);
 
-        unchecked {
-            Checkpoint memory oldCkpt = pos == 0 ? Checkpoint(0, 0) : _unsafeAccess(ckpts, pos - 1);
+        if (pos > 0 && ckpts[pos - 1].fromBlock == clock()) {
+            ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
+        } else {
+            ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
+        }
+    }
 
-            oldWeight = oldCkpt.votes;
-            newWeight = op(oldWeight, delta);
+    function _writeCheckpointSub(Checkpoint[] storage ckpts, uint256 delta) private returns (uint256 oldWeight, uint256 newWeight) {
+        uint256 pos = ckpts.length;
+        oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
+        newWeight = _subtract(oldWeight, delta);
 
-            if (pos > 0 && oldCkpt.fromBlock == clock()) {
-                _unsafeAccess(ckpts, pos - 1).votes = SafeCast.toUint224(newWeight);
-            } else {
-                ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
-            }
+        if (pos > 0 && ckpts[pos - 1].fromBlock == clock()) {
+            ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
+        } else {
+            ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
         }
     }
 
diff -druN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
--- token/ERC20/extensions/ERC20Wrapper.sol	2023-02-27 10:59:32.655891529 +0100
+++ token/ERC20/extensions/ERC20Wrapper.sol	2023-02-28 16:49:10.421059488 +0100
@@ -62,7 +62,7 @@
      * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
      * function that can be exposed with access control if desired.
      */
-    function _recover(address account) internal virtual returns (uint256) {
+    function _recover(address account) public virtual returns (uint256) { // HARNESS: internal -> public
         uint256 value = _underlying.balanceOf(address(this)) - totalSupply();
         _mint(account, value);
         return value;
diff -druN token/ERC721/extensions/ERC721Votes.sol token/ERC721/extensions/ERC721Votes.sol
--- token/ERC721/extensions/ERC721Votes.sol	2023-02-27 10:59:32.655891529 +0100
+++ token/ERC721/extensions/ERC721Votes.sol	2023-02-28 16:49:10.421059488 +0100
@@ -35,7 +35,7 @@
     /**
      * @dev Returns the balance of `account`.
      */
-    function _getVotingUnits(address account) internal view virtual override returns (uint256) {
+    function _getVotingUnits(address account) public view virtual override returns (uint256) { // HARNESS: internal -> public
         return balanceOf(account);
     }
 }
diff -druN utils/Address.sol utils/Address.sol
--- utils/Address.sol	2023-02-27 10:59:32.659224903 +0100
+++ utils/Address.sol	2023-02-28 16:49:10.421059488 +0100
@@ -197,7 +197,7 @@
         bool success,
         bytes memory returndata,
         string memory errorMessage
-    ) internal view returns (bytes memory) {
+    ) internal view returns (bytes memory val) { // MUNGED undeterministic return causes error for Prover
         if (success) {
             if (returndata.length == 0) {
                 // only check isContract if the call was successful and the return data is empty
@@ -220,7 +220,7 @@
         bool success,
         bytes memory returndata,
         string memory errorMessage
-    ) internal pure returns (bytes memory) {
+    ) internal pure returns (bytes memory val) { // MUNGED undeterministic return causes error for Prover
         if (success) {
             return returndata;
         } else {
diff -druN utils/Checkpoints.sol utils/Checkpoints.sol
--- utils/Checkpoints.sol	2023-02-27 10:59:32.659224903 +0100
+++ utils/Checkpoints.sol	2023-02-28 16:49:10.424392833 +0100
@@ -84,13 +84,13 @@
      *
      * Returns previous value and new value.
      */
-    function push(
-        History storage self,
-        function(uint256, uint256) view returns (uint256) op,
-        uint256 delta
-    ) internal returns (uint256, uint256) {
-        return push(self, op(latest(self), delta));
-    }
+    // function push(
+    //     History storage self,
+    //     function(uint256, uint256) view returns (uint256) op,
+    //     uint256 delta
+    // ) internal returns (uint256, uint256) {
+    //     return push(self, op(latest(self), delta));
+    // }
 
     /**
      * @dev Returns the value in the most recent checkpoint, or zero if there are no checkpoints.