diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 1d3ae55a5..e339df7c3 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,12 +1,12 @@ diff -ruN .gitignore .gitignore --- .gitignore 1969-12-31 16:00:00.000000000 -0800 -+++ .gitignore 2022-08-11 21:15:52.000000000 -0700 ++++ .gitignore 2022-08-11 21:28:36.000000000 -0700 @@ -0,0 +1,2 @@ +* +!.gitignore diff -ruN access/AccessControl.sol access/AccessControl.sol ---- access/AccessControl.sol 2022-08-11 21:13:55.000000000 -0700 -+++ access/AccessControl.sol 2022-08-11 21:15:52.000000000 -0700 +--- access/AccessControl.sol 2022-08-11 21:28:00.000000000 -0700 ++++ access/AccessControl.sol 2022-08-11 21:28:36.000000000 -0700 @@ -93,7 +93,7 @@ * * _Available since v4.6._ @@ -17,8 +17,8 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol } diff -ruN access/Ownable.sol access/Ownable.sol ---- access/Ownable.sol 2022-08-11 21:13:55.000000000 -0700 -+++ access/Ownable.sol 2022-08-11 21:15:52.000000000 -0700 +--- access/Ownable.sol 2022-08-11 21:28:00.000000000 -0700 ++++ access/Ownable.sol 2022-08-11 21:28:36.000000000 -0700 @@ -30,14 +30,6 @@ } @@ -49,8 +49,8 @@ diff -ruN access/Ownable.sol access/Ownable.sol /** diff -ruN governance/Governor.sol governance/Governor.sol ---- governance/Governor.sol 2022-08-11 21:13:55.000000000 -0700 -+++ governance/Governor.sol 2022-08-11 21:15:52.000000000 -0700 +--- governance/Governor.sol 2022-08-11 21:28:00.000000000 -0700 ++++ governance/Governor.sol 2022-08-11 21:28:36.000000000 -0700 @@ -44,7 +44,7 @@ string private _name; @@ -61,8 +61,8 @@ diff -ruN governance/Governor.sol governance/Governor.sol // 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 -ruN governance/TimelockController.sol governance/TimelockController.sol ---- governance/TimelockController.sol 2022-08-11 21:13:55.000000000 -0700 -+++ governance/TimelockController.sol 2022-08-11 21:15:52.000000000 -0700 +--- governance/TimelockController.sol 2022-08-11 21:28:00.000000000 -0700 ++++ governance/TimelockController.sol 2022-08-11 21:28:36.000000000 -0700 @@ -28,10 +28,10 @@ bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE"); @@ -77,8 +77,8 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol /** * @dev Emitted when a call is scheduled as part of operation `id`. diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol ---- governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:13:55.000000000 -0700 -+++ governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:15:52.000000000 -0700 +--- governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:28:00.000000000 -0700 ++++ governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:28:36.000000000 -0700 @@ -27,7 +27,7 @@ mapping(address => bool) hasVoted; } @@ -89,8 +89,8 @@ diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions /** * @dev See {IGovernor-COUNTING_MODE}. diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol ---- governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:13:55.000000000 -0700 -+++ governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:15:52.000000000 -0700 +--- governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:28:00.000000000 -0700 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:28:36.000000000 -0700 @@ -21,8 +21,8 @@ using SafeCast for uint256; using Timers for Timers.BlockNumber; @@ -103,8 +103,8 @@ diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensi /// @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 -ruN governance/utils/Votes.sol governance/utils/Votes.sol ---- governance/utils/Votes.sol 2022-08-11 21:13:55.000000000 -0700 -+++ governance/utils/Votes.sol 2022-08-11 21:15:52.000000000 -0700 +--- governance/utils/Votes.sol 2022-08-11 21:28:00.000000000 -0700 ++++ governance/utils/Votes.sol 2022-08-11 21:28:36.000000000 -0700 @@ -35,7 +35,25 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -178,8 +178,8 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol + function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public } diff -ruN metatx/MinimalForwarder.sol metatx/MinimalForwarder.sol ---- metatx/MinimalForwarder.sol 2022-08-11 21:13:55.000000000 -0700 -+++ metatx/MinimalForwarder.sol 2022-08-11 21:15:52.000000000 -0700 +--- metatx/MinimalForwarder.sol 2022-08-11 21:28:00.000000000 -0700 ++++ metatx/MinimalForwarder.sol 2022-08-11 21:28:36.000000000 -0700 @@ -8,11 +8,6 @@ /** @@ -194,7 +194,7 @@ diff -ruN metatx/MinimalForwarder.sol metatx/MinimalForwarder.sol using ECDSA for bytes32; diff -ruN mocks/ERC20TokenizedVaultMock.sol mocks/ERC20TokenizedVaultMock.sol --- mocks/ERC20TokenizedVaultMock.sol 1969-12-31 16:00:00.000000000 -0800 -+++ mocks/ERC20TokenizedVaultMock.sol 2022-08-11 21:15:52.000000000 -0700 ++++ mocks/ERC20TokenizedVaultMock.sol 2022-08-11 21:28:36.000000000 -0700 @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: MIT + @@ -219,7 +219,7 @@ diff -ruN mocks/ERC20TokenizedVaultMock.sol mocks/ERC20TokenizedVaultMock.sol + } +} diff -ruN mocks/ERC4626Mock.sol mocks/ERC4626Mock.sol ---- mocks/ERC4626Mock.sol 2022-08-11 21:13:55.000000000 -0700 +--- mocks/ERC4626Mock.sol 2022-08-11 21:28:00.000000000 -0700 +++ mocks/ERC4626Mock.sol 1969-12-31 16:00:00.000000000 -0800 @@ -1,22 +0,0 @@ -// SPDX-License-Identifier: MIT @@ -245,8 +245,8 @@ diff -ruN mocks/ERC4626Mock.sol mocks/ERC4626Mock.sol - } -} diff -ruN mocks/MathMock.sol mocks/MathMock.sol ---- mocks/MathMock.sol 2022-08-11 21:13:55.000000000 -0700 -+++ mocks/MathMock.sol 2022-08-11 21:15:52.000000000 -0700 +--- mocks/MathMock.sol 2022-08-11 21:28:00.000000000 -0700 ++++ mocks/MathMock.sol 2022-08-11 21:28:36.000000000 -0700 @@ -29,8 +29,4 @@ ) public pure returns (uint256) { return Math.mulDiv(a, b, denominator, direction); @@ -257,8 +257,8 @@ diff -ruN mocks/MathMock.sol mocks/MathMock.sol - } } diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol ---- mocks/SafeERC20Helper.sol 2022-08-11 21:13:55.000000000 -0700 -+++ mocks/SafeERC20Helper.sol 2022-08-11 21:15:52.000000000 -0700 +--- mocks/SafeERC20Helper.sol 2022-08-11 21:28:00.000000000 -0700 ++++ mocks/SafeERC20Helper.sol 2022-08-11 21:28:36.000000000 -0700 @@ -4,7 +4,6 @@ import "../utils/Context.sol"; @@ -331,8 +331,8 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol ERC20ReturnTrueMock(address(_token)).setAllowance(allowance_); } diff -ruN proxy/Clones.sol proxy/Clones.sol ---- proxy/Clones.sol 2022-08-11 21:13:55.000000000 -0700 -+++ proxy/Clones.sol 2022-08-11 21:15:52.000000000 -0700 +--- proxy/Clones.sol 2022-08-11 21:28:00.000000000 -0700 ++++ proxy/Clones.sol 2022-08-11 21:28:36.000000000 -0700 @@ -26,10 +26,10 @@ /// @solidity memory-safe-assembly assembly { @@ -385,8 +385,8 @@ diff -ruN proxy/Clones.sol proxy/Clones.sol } diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol ---- proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:13:55.000000000 -0700 -+++ proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:15:52.000000000 -0700 +--- proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:28:00.000000000 -0700 ++++ proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:28:36.000000000 -0700 @@ -20,6 +20,7 @@ * function call, and allows initializing the storage of the proxy like a Solidity constructor. */ @@ -396,8 +396,8 @@ diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol } diff -ruN proxy/beacon/BeaconProxy.sol proxy/beacon/BeaconProxy.sol ---- proxy/beacon/BeaconProxy.sol 2022-08-11 21:13:55.000000000 -0700 -+++ proxy/beacon/BeaconProxy.sol 2022-08-11 21:15:52.000000000 -0700 +--- proxy/beacon/BeaconProxy.sol 2022-08-11 21:28:00.000000000 -0700 ++++ proxy/beacon/BeaconProxy.sol 2022-08-11 21:28:36.000000000 -0700 @@ -28,6 +28,7 @@ * - `beacon` must be a contract with the interface {IBeacon}. */ @@ -407,8 +407,8 @@ diff -ruN proxy/beacon/BeaconProxy.sol proxy/beacon/BeaconProxy.sol } diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/TransparentUpgradeableProxy.sol ---- proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:13:55.000000000 -0700 -+++ proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:15:52.000000000 -0700 +--- proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:28:00.000000000 -0700 ++++ proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:28:36.000000000 -0700 @@ -36,6 +36,7 @@ address admin_, bytes memory _data @@ -418,8 +418,8 @@ diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/Tr } diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol ---- proxy/utils/Initializable.sol 2022-08-11 21:13:55.000000000 -0700 -+++ proxy/utils/Initializable.sol 2022-08-11 21:15:52.000000000 -0700 +--- proxy/utils/Initializable.sol 2022-08-11 21:28:00.000000000 -0700 ++++ proxy/utils/Initializable.sol 2022-08-11 21:28:36.000000000 -0700 @@ -59,12 +59,12 @@ * @dev Indicates that the contract has been initialized. * @custom:oz-retyped-from bool @@ -437,7 +437,7 @@ diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol * @dev Triggered when the contract has been initialized or reinitialized. diff -ruN proxy/utils/Initializable.sol.orig proxy/utils/Initializable.sol.orig --- proxy/utils/Initializable.sol.orig 1969-12-31 16:00:00.000000000 -0800 -+++ proxy/utils/Initializable.sol.orig 2022-08-11 21:15:52.000000000 -0700 ++++ proxy/utils/Initializable.sol.orig 2022-08-11 21:28:36.000000000 -0700 @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v4.6.0) (proxy/utils/Initializable.sol) @@ -579,7 +579,7 @@ diff -ruN proxy/utils/Initializable.sol.orig proxy/utils/Initializable.sol.orig +} diff -ruN proxy/utils/Initializable.sol.rej proxy/utils/Initializable.sol.rej --- proxy/utils/Initializable.sol.rej 1969-12-31 16:00:00.000000000 -0800 -+++ proxy/utils/Initializable.sol.rej 2022-08-11 21:15:52.000000000 -0700 ++++ proxy/utils/Initializable.sol.rej 2022-08-11 21:28:36.000000000 -0700 @@ -0,0 +1,17 @@ +*************** +*** 130,136 **** @@ -599,8 +599,8 @@ diff -ruN proxy/utils/Initializable.sol.rej proxy/utils/Initializable.sol.rej + // inheritance patterns, but we only do this in the context of a constructor, and for the lowest level + // of initializers, because in other contexts the contract may have been reentered. diff -ruN security/Pausable.sol security/Pausable.sol ---- security/Pausable.sol 2022-08-11 21:13:55.000000000 -0700 -+++ security/Pausable.sol 2022-08-11 21:15:52.000000000 -0700 +--- security/Pausable.sol 2022-08-11 21:28:00.000000000 -0700 ++++ security/Pausable.sol 2022-08-11 21:28:36.000000000 -0700 @@ -35,6 +35,13 @@ } @@ -656,8 +656,8 @@ diff -ruN security/Pausable.sol security/Pausable.sol /** diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol ---- token/ERC1155/ERC1155.sol 2022-08-11 21:13:55.000000000 -0700 -+++ token/ERC1155/ERC1155.sol 2022-08-11 21:15:52.000000000 -0700 +--- token/ERC1155/ERC1155.sol 2022-08-11 21:28:00.000000000 -0700 ++++ token/ERC1155/ERC1155.sol 2022-08-11 21:28:36.000000000 -0700 @@ -21,7 +21,7 @@ using Address for address; @@ -686,8 +686,8 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol 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-08-11 21:25:35.000000000 -0700 -+++ token/ERC20/ERC20.sol 2022-08-11 21:15:52.000000000 -0700 +--- token/ERC20/ERC20.sol 2022-08-11 21:28:00.000000000 -0700 ++++ token/ERC20/ERC20.sol 2022-08-11 23:01:50.000000000 -0700 @@ -277,7 +277,7 @@ * - `account` cannot be the zero address. * - `account` must have at least `amount` tokens. @@ -698,8 +698,8 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol _beforeTokenTransfer(account, address(0), amount); diff -ruN token/ERC20/README.adoc token/ERC20/README.adoc ---- token/ERC20/README.adoc 2022-08-11 21:13:55.000000000 -0700 -+++ token/ERC20/README.adoc 2022-08-11 21:15:52.000000000 -0700 +--- token/ERC20/README.adoc 2022-08-11 21:28:00.000000000 -0700 ++++ token/ERC20/README.adoc 2022-08-11 21:28:36.000000000 -0700 @@ -24,7 +24,7 @@ * {ERC20Votes}: support for voting and vote delegation. * {ERC20VotesComp}: support for voting and vote delegation (compatible with Compound's token, with uint96 restrictions). @@ -719,8 +719,8 @@ diff -ruN token/ERC20/README.adoc token/ERC20/README.adoc == Draft EIPs diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol ---- token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:13:55.000000000 -0700 -+++ token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:15:52.000000000 -0700 +--- token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:28:00.000000000 -0700 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:28:36.000000000 -0700 @@ -40,9 +40,11 @@ require(token == address(this), "ERC20FlashMint: wrong token"); // silence warning about unused variable without the addition of bytecode. @@ -736,7 +736,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 * implementation returns the address(0) which means the fee amount will be burnt. diff -ruN token/ERC20/extensions/ERC20TokenizedVault.sol token/ERC20/extensions/ERC20TokenizedVault.sol --- token/ERC20/extensions/ERC20TokenizedVault.sol 1969-12-31 16:00:00.000000000 -0800 -+++ token/ERC20/extensions/ERC20TokenizedVault.sol 2022-08-11 21:15:52.000000000 -0700 ++++ token/ERC20/extensions/ERC20TokenizedVault.sol 2022-08-11 21:28:36.000000000 -0700 @@ -0,0 +1,217 @@ +// SPDX-License-Identifier: MIT + @@ -957,7 +957,7 @@ diff -ruN token/ERC20/extensions/ERC20TokenizedVault.sol token/ERC20/extensions/ +} diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol --- token/ERC20/extensions/ERC20Votes.sol 2022-08-11 21:16:57.000000000 -0700 -+++ token/ERC20/extensions/ERC20Votes.sol 2022-08-11 21:25:13.000000000 -0700 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-08-11 22:47:30.000000000 -0700 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -1088,9 +1088,34 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote return a + b; } diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol ---- token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:13:55.000000000 -0700 -+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:15:52.000000000 -0700 -@@ -55,7 +55,7 @@ +--- token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:28:00.000000000 -0700 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:29:19.000000000 -0700 +@@ -1,5 +1,5 @@ + // SPDX-License-Identifier: MIT +-// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/extensions/ERC20Wrapper.sol) ++// OpenZeppelin Contracts v4.4.1 (token/ERC20/extensions/ERC20Wrapper.sol) + + pragma solidity ^0.8.0; + +@@ -23,17 +23,6 @@ + } + + /** +- * @dev See {ERC20-decimals}. +- */ +- function decimals() public view virtual override returns (uint8) { +- try IERC20Metadata(address(underlying)).decimals() returns (uint8 value) { +- return value; +- } catch { +- return super.decimals(); +- } +- } +- +- /** + * @dev Allow a user to deposit underlying tokens and mint the corresponding number of wrapped tokens. + */ + function depositFor(address account, uint256 amount) public virtual returns (bool) { +@@ -55,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. */ @@ -1100,7 +1125,7 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr _mint(account, value); return value; diff -ruN token/ERC20/extensions/ERC4626.sol token/ERC20/extensions/ERC4626.sol ---- token/ERC20/extensions/ERC4626.sol 2022-08-11 21:13:55.000000000 -0700 +--- token/ERC20/extensions/ERC4626.sol 2022-08-11 21:28:00.000000000 -0700 +++ token/ERC20/extensions/ERC4626.sol 1969-12-31 16:00:00.000000000 -0800 @@ -1,217 +0,0 @@ -// SPDX-License-Identifier: MIT @@ -1321,8 +1346,8 @@ diff -ruN token/ERC20/extensions/ERC4626.sol token/ERC20/extensions/ERC4626.sol - } -} diff -ruN token/ERC20/utils/SafeERC20.sol token/ERC20/utils/SafeERC20.sol ---- token/ERC20/utils/SafeERC20.sol 2022-08-11 21:13:55.000000000 -0700 -+++ token/ERC20/utils/SafeERC20.sol 2022-08-11 21:15:52.000000000 -0700 +--- token/ERC20/utils/SafeERC20.sol 2022-08-11 21:28:00.000000000 -0700 ++++ token/ERC20/utils/SafeERC20.sol 2022-08-11 21:28:36.000000000 -0700 @@ -4,7 +4,6 @@ pragma solidity ^0.8.0; @@ -1355,8 +1380,8 @@ diff -ruN token/ERC20/utils/SafeERC20.sol token/ERC20/utils/SafeERC20.sol * @dev Imitates a Solidity high-level call (i.e. a regular function call to a contract), relaxing the requirement * on the return value: the return value is optional (but if data is returned, it must not be false). diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol ---- token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:13:55.000000000 -0700 -+++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:15:52.000000000 -0700 +--- token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:28:00.000000000 -0700 ++++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:28:36.000000000 -0700 @@ -34,7 +34,7 @@ /** * @dev Returns the balance of `account`. @@ -1367,8 +1392,8 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/ } } diff -ruN utils/Address.sol utils/Address.sol ---- utils/Address.sol 2022-08-11 21:13:55.000000000 -0700 -+++ utils/Address.sol 2022-08-11 21:15:52.000000000 -0700 +--- utils/Address.sol 2022-08-11 21:28:00.000000000 -0700 ++++ utils/Address.sol 2022-08-11 21:28:36.000000000 -0700 @@ -131,6 +131,7 @@ uint256 value, string memory errorMessage @@ -1378,8 +1403,8 @@ diff -ruN utils/Address.sol utils/Address.sol require(isContract(target), "Address: call to non-contract"); diff -ruN utils/math/Math.sol utils/math/Math.sol ---- utils/math/Math.sol 2022-08-11 21:13:55.000000000 -0700 -+++ utils/math/Math.sol 2022-08-11 21:15:52.000000000 -0700 +--- utils/math/Math.sol 2022-08-11 21:28:00.000000000 -0700 ++++ utils/math/Math.sol 2022-08-11 21:28:36.000000000 -0700 @@ -149,78 +149,4 @@ } return result; diff --git a/certora/scripts/Round2/verifyERC20Votes.sh b/certora/scripts/Round2/verifyERC20Votes.sh index dea9bc695..c9e5db059 100644 --- a/certora/scripts/Round2/verifyERC20Votes.sh +++ b/certora/scripts/Round2/verifyERC20Votes.sh @@ -2,12 +2,11 @@ certoraRun \ certora/harnesses/ERC20VotesHarness.sol \ --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ --solc solc8.2 \ - --disableLocalTypeChecking \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ --cloud \ --send_only \ - --msg "ERC20Votes" \ - + --msg "ERC20Votes $1" \ + # --disableLocalTypeChecking \ # --staging "alex/new-dt-hashing-alpha" \ diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index badf3f557..f0b9cde0d 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -29,19 +29,18 @@ ghost userVotes(address) returns uint224 { } // sums the total votes for all users -ghost totalVotes() returns mathint { +ghost totalVotes() returns uint224 { init_state axiom totalVotes() == 0; - axiom totalVotes() >= 0; } ghost lastIndex(address) returns uint32; // helper -hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { +hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { havoc userVotes assuming userVotes@new(account) == newVotes; havoc totalVotes assuming - totalVotes@new() == totalVotes@old() + to_mathint(newVotes) - to_mathint(userVotes(account)); + totalVotes@new() == totalVotes@old() + newVotes - userVotes(account); havoc lastIndex assuming lastIndex@new(account) == index; @@ -68,10 +67,16 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint // sum of user balances is >= total amount of delegated votes // fails on burn. This is because burn does not remove votes from the users invariant votes_solvency() - to_mathint(totalSupply()) >= totalVotes() + totalSupply() >= to_uint256(totalVotes()) +filtered { f -> f.selector != _burn(address, uint256).selector} { preserved with(env e) { require forall address account. numCheckpoints(account) < 1000000; -} } +} preserved burn(address a, uint256 amount) with(env e){ + require _delegates(0) == 0; + require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes()); + require balanceOf(e, _delegates(a)) < totalVotes(); + require amount < 100000; +}} // for some checkpoint, the fromBlock is less than the current block number @@ -146,10 +151,10 @@ rule transfer_safe() { require numCheckpoints(delegates(b)) < 1000000; uint256 votesA_pre = getVotes(delegates(a)); uint256 votesB_pre = getVotes(delegates(b)); - mathint totalVotes_pre = totalVotes(); + uint224 totalVotes_pre = totalVotes(); transferFrom(e, a, b, amount); - mathint totalVotes_post = totalVotes(); + uint224 totalVotes_post = totalVotes(); uint256 votesA_post = getVotes(delegates(a)); uint256 votesB_post = getVotes(delegates(b)); // if an account that has not delegated transfers balance to an account that has, it will increase the total supply of votes @@ -308,7 +313,7 @@ rule mint_doesnt_increase_totalVotes() { env e; uint256 amount; address account; - mathint totalVotes_ = totalVotes(); + uint224 totalVotes_ = totalVotes(); mint(e, account, amount); @@ -319,7 +324,7 @@ rule burn_doesnt_decrease_totalVotes() { env e; uint256 amount; address account; - mathint totalVotes_ = totalVotes(); + uint224 totalVotes_ = totalVotes(); burn(e, account, amount);