openzeppelin-contracts/certora/applyHarness.patch

diff -ruN access/AccessControl.sol access/AccessControl.sol
--- access/AccessControl.sol	2022-03-02 09:14:55.000000000 -0800
+++ access/AccessControl.sol	2022-04-08 17:31:22.000000000 -0700
@@ -93,7 +93,7 @@
      *
      * _Available since v4.6._
      */
-    function _checkRole(bytes32 role) internal view virtual {
+    function _checkRole(bytes32 role) public view virtual {         // HARNESS: internal -> public
         _checkRole(role, _msgSender());
     }
 
diff -ruN governance/TimelockController.sol governance/TimelockController.sol
--- governance/TimelockController.sol	2022-03-02 09:14:55.000000000 -0800
+++ governance/TimelockController.sol	2022-04-08 17:31:22.000000000 -0700
@@ -24,10 +24,10 @@
     bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE");
     bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
     bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_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`.
@@ -353,4 +353,4 @@
         emit MinDelayChange(_minDelay, newDelay);
         _minDelay = newDelay;
     }
-}
+} 
diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
--- governance/utils/Votes.sol	2022-03-02 09:14:55.000000000 -0800
+++ governance/utils/Votes.sol	2022-04-08 17:44:19.000000000 -0700
@@ -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]._blockNumber;
+    }
+    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
+        return _delegateCheckpoints[account]._checkpoints[pos]._value;
+    }
+
+    mapping(address => address) public _delegation;    
     mapping(address => Checkpoints.History) private _delegateCheckpoints;
     Checkpoints.History private _totalCheckpoints;
 
@@ -124,7 +142,7 @@
      *
      * Emits events {DelegateChanged} and {DelegateVotesChanged}.
      */
-    function _delegate(address account, address delegatee) internal virtual {
+    function _delegate(address account, address delegatee) public virtual {
         address oldDelegate = delegates(account);
         _delegation[account] = delegatee;
 
@@ -142,10 +160,10 @@
         uint256 amount
     ) internal virtual {
         if (from == address(0)) {
-            _totalCheckpoints.push(_add, amount);
+            _totalCheckpoints.push(_totalCheckpoints.latest() + amount); // Harnessed to remove function pointers
         }
         if (to == address(0)) {
-            _totalCheckpoints.push(_subtract, amount);
+            _totalCheckpoints.push(_totalCheckpoints.latest() - amount); // Harnessed to remove function pointers
         }
         _moveDelegateVotes(delegates(from), delegates(to), amount);
     }
@@ -160,11 +178,13 @@
     ) private {
         if (from != to && amount > 0) {
             if (from != address(0)) {
-                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_subtract, amount);
+                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_delegateCheckpoints[from].latest() - amount); // HARNESSED TO REMOVE FUNCTION POINTERS
+                _checkpoints[from] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS
                 emit DelegateVotesChanged(from, oldValue, newValue);
             }
             if (to != address(0)) {
-                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_add, amount);
+                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_delegateCheckpoints[to].latest() + amount); // HARNESSED TO REMOVE FUNCTION POINTERS
+                _checkpoints[to] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS
                 emit DelegateVotesChanged(to, oldValue, newValue);
             }
         }
@@ -207,5 +227,5 @@
     /**
      * @dev Must return the voting units held by an account.
      */
-    function _getVotingUnits(address) internal virtual returns (uint256);
+    function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public
 }
diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
--- token/ERC1155/ERC1155.sol	2022-03-02 09:14:55.000000000 -0800
+++ token/ERC1155/ERC1155.sol	2022-04-08 17:31:22.000000000 -0700
@@ -268,7 +268,7 @@
         uint256 id,
         uint256 amount,
         bytes memory data
-    ) internal virtual {
+    ) public virtual {              // HARNESS: internal -> public
         require(to != address(0), "ERC1155: mint to the zero address");
 
         address operator = _msgSender();
@@ -299,7 +299,7 @@
         uint256[] memory ids,
         uint256[] memory amounts,
         bytes memory data
-    ) internal virtual {
+    ) public virtual {                    // HARNESS: internal -> public
         require(to != address(0), "ERC1155: mint to the zero address");
         require(ids.length == amounts.length, "ERC1155: ids and amounts length mismatch");
 
@@ -330,7 +330,7 @@
         address from,
         uint256 id,
         uint256 amount
-    ) internal virtual {
+    ) public virtual {                // HARNESS: internal -> public
         require(from != address(0), "ERC1155: burn from the zero address");
 
         address operator = _msgSender();
@@ -361,7 +361,7 @@
         address from,
         uint256[] memory ids,
         uint256[] memory amounts
-    ) internal virtual {
+    ) public virtual {                    // HARNESS: internal -> public
         require(from != address(0), "ERC1155: burn from the zero address");
         require(ids.length == amounts.length, "ERC1155: ids and amounts length mismatch");
 
@@ -465,7 +465,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) {
@@ -486,7 +486,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 -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
--- token/ERC20/ERC20.sol	2022-03-02 09:14:55.000000000 -0800
+++ token/ERC20/ERC20.sol	2022-04-08 17:31:22.000000000 -0700
@@ -277,7 +277,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 returns (bool) {          // HARNESS: internal -> public
         require(account != address(0), "ERC20: burn from the zero address");
 
         _beforeTokenTransfer(account, address(0), amount);
@@ -292,6 +292,8 @@
         emit Transfer(account, address(0), amount);
 
         _afterTokenTransfer(account, address(0), amount);
+
+        return true;
     }
 
     /**
diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
--- token/ERC20/extensions/ERC20FlashMint.sol	2022-03-02 09:14:55.000000000 -0800
+++ token/ERC20/extensions/ERC20FlashMint.sol	2022-04-08 17:31:22.000000000 -0700
@@ -40,9 +40,11 @@
         require(token == address(this), "ERC20FlashMint: wrong token");
         // silence warning about unused variable without the addition of bytecode.
         amount;
-        return 0;
+        return fee;                 // HARNESS: made "return" nonzero
     }
 
+    uint256 public fee;             // HARNESS: added it to simulate random fee amount
+
     /**
      * @dev Performs a flash loan. New tokens are minted and sent to the
      * `receiver`, who is required to implement the {IERC3156FlashBorrower}
diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
--- token/ERC20/extensions/ERC20Votes.sol	2022-03-02 09:14:55.000000000 -0800
+++ token/ERC20/extensions/ERC20Votes.sol	2022-04-08 17:31:22.000000000 -0700
@@ -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;
+    mapping(address => Checkpoint[]) public _checkpoints;
     Checkpoint[] private _totalSupplyCheckpoints;
 
     /**
@@ -152,7 +152,7 @@
     /**
      * @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) { //harnessed to public
         return type(uint224).max;
     }
 
@@ -163,16 +163,17 @@
         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 returns (bool){ // 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
+        return true;
     }
 
     /**
@@ -187,7 +188,7 @@
     ) internal virtual override {
         super._afterTokenTransfer(from, to, amount);
 
-        _moveVotingPower(delegates(from), delegates(to), amount);
+        _moveVotingPower(delegates(from), delegates(to), amount);       
     }
 
     /**
@@ -195,7 +196,7 @@
      *
      * Emits events {DelegateChanged} and {DelegateVotesChanged}.
      */
-    function _delegate(address delegator, address delegatee) internal virtual {
+    function _delegate(address delegator, address delegatee) public virtual { // HARNESSED TO MAKE PUBLIC
         address currentDelegate = delegates(delegator);
         uint256 delegatorBalance = balanceOf(delegator);
         _delegates[delegator] = delegatee;
@@ -212,25 +213,25 @@
     ) 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(
+    // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool
+    function _writeCheckpointAdd(
         Checkpoint[] storage ckpts,
-        function(uint256, uint256) view returns (uint256) op,
         uint256 delta
     ) private returns (uint256 oldWeight, uint256 newWeight) {
         uint256 pos = ckpts.length;
         oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
-        newWeight = op(oldWeight, delta);
+        newWeight = _add(oldWeight, delta);
 
         if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) {
             ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
@@ -239,6 +240,39 @@
         }
     }
 
+    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 && ckpts[pos - 1].fromBlock == block.number) {
+            ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
+        } else {
+            ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)}));
+        }
+    }
+
+    // backup of original function
+    //
+    // function _writeCheckpoint(
+    //     Checkpoint[] storage ckpts,
+    //     function(uint256, uint256) view returns (uint256) op,
+    //     uint256 delta
+    // ) private returns (uint256 oldWeight, uint256 newWeight) {
+    //     uint256 pos = ckpts.length;
+    //     oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
+    //     newWeight = op(oldWeight, delta);
+    //
+    //     if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) {
+    //         ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
+    //     } else {
+    //         ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)}));
+    //     }
+    // }
+
     function _add(uint256 a, uint256 b) private pure returns (uint256) {
         return a + b;
     }
diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
--- token/ERC20/extensions/ERC20Wrapper.sol	2022-03-02 09:14:55.000000000 -0800
+++ token/ERC20/extensions/ERC20Wrapper.sol	2022-04-08 17:31:22.000000000 -0700
@@ -44,7 +44,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 -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
--- token/ERC721/extensions/draft-ERC721Votes.sol	2022-03-02 09:14:55.000000000 -0800
+++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-04-08 17:31:22.000000000 -0700
@@ -34,7 +34,7 @@
     /**
      * @dev Returns the balance of `account`.
      */
-    function _getVotingUnits(address account) internal virtual override returns (uint256) {
+    function _getVotingUnits(address account) public virtual override returns (uint256) {
         return balanceOf(account);
     }
 }