diff --git a/.github/workflows/formal-verifiation.yml b/.github/workflows/formal-verifiation.yml index 94f8854e1..cb2bddfff 100644 --- a/.github/workflows/formal-verifiation.yml +++ b/.github/workflows/formal-verifiation.yml @@ -47,9 +47,18 @@ jobs: echo 'file:' ${{ matrix.params.file }} echo 'name:' ${{ matrix.params.name }} echo 'spec:' ${{ matrix.params.spec }} + echo 'args:' ${{ matrix.params.args || '' }} + touch certora/applyHarness.patch make -C certora munged - certoraRun ${{ matrix.params.file }} --verify ${{ matrix.params.name }}:${{ matrix.params.spec }} --solc solc --optimistic_loop --loop_iter 3 --rule_sanity advanced --cloud + + certoraRun ${{ matrix.params.file }} \ + --verify ${{ matrix.params.name }}:${{ matrix.params.spec }} \ + --solc solc \ + --optimistic_loop + --loop_iter 3 \ + --cloud \ + ${{ matrix.params.args || '' }} env: CERTORAKEY: ${{ secrets.CERTORAKEY }} strategy: diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 90967d1b0..b4cde7fd1 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -9,13 +9,13 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol + function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public _checkRole(role, _msgSender()); } - + diff -ruN access/Ownable.sol access/Ownable.sol --- access/Ownable.sol 2022-09-09 10:15:55.887175731 +0200 +++ access/Ownable.sol 2022-09-20 14:34:08.629602185 +0200 @@ -30,14 +30,6 @@ } - + /** - * @dev Throws if called by any account other than the owner. - */ @@ -30,7 +30,7 @@ diff -ruN access/Ownable.sol access/Ownable.sol function owner() public view virtual returns (address) { @@ -45,10 +37,11 @@ } - + /** - * @dev Throws if the sender is not the owner. + * @dev Throws if called by any account other than the owner. @@ -40,7 +40,7 @@ diff -ruN access/Ownable.sol access/Ownable.sol require(owner() == _msgSender(), "Ownable: caller is not the owner"); + _; } - + /** diff -ruN .gitignore .gitignore --- .gitignore 1970-01-01 01:00:00.000000000 +0100 @@ -54,10 +54,10 @@ diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions @@ -27,7 +27,7 @@ mapping(address => bool) hasVoted; } - + - mapping(uint256 => ProposalVote) private _proposalVotes; + mapping(uint256 => ProposalVote) internal _proposalVotes; - + /** * @dev See {IGovernor-COUNTING_MODE}. diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol @@ -66,24 +66,24 @@ diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensi @@ -21,8 +21,8 @@ using SafeCast for uint256; using Timers for Timers.BlockNumber; - + - uint64 private _voteExtension; - mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines; + uint64 internal _voteExtension; // PRIVATE => INTERNAL + mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines; // 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 -ruN governance/Governor.sol governance/Governor.sol --- governance/Governor.sol 2022-09-20 11:01:10.429515094 +0200 +++ governance/Governor.sol 2022-09-20 14:34:08.629602185 +0200 @@ -44,7 +44,7 @@ - + string private _name; - + - mapping(uint256 => ProposalCore) private _proposals; + mapping(uint256 => ProposalCore) internal _proposals; - + // 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 @@ -95,11 +95,11 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol bytes32 public constant CANCELLER_ROLE = keccak256("CANCELLER_ROLE"); - uint256 internal constant _DONE_TIMESTAMP = uint256(1); + uint256 public constant _DONE_TIMESTAMP = uint256(1); - + mapping(bytes32 => uint256) private _timestamps; - uint256 private _minDelay; + uint256 public _minDelay; - + /** * @dev Emitted when a call is scheduled as part of operation `id`. diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol @@ -108,7 +108,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol @@ -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 { @@ -131,7 +131,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol + mapping(address => address) public _delegation; mapping(address => Checkpoints.History) private _delegateCheckpoints; Checkpoints.History private _totalCheckpoints; - + @@ -124,7 +142,7 @@ * * Emits events {DelegateChanged} and {DelegateVotesChanged}. @@ -140,7 +140,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol + function _delegate(address account, address delegatee) public virtual { address oldDelegate = delegates(account); _delegation[account] = delegatee; - + @@ -142,10 +160,10 @@ uint256 amount ) internal virtual { @@ -181,7 +181,7 @@ diff -ruN metatx/MinimalForwarder.sol metatx/MinimalForwarder.sol --- metatx/MinimalForwarder.sol 2022-09-20 11:16:48.456850883 +0200 +++ metatx/MinimalForwarder.sol 2022-09-20 14:34:08.632935582 +0200 @@ -8,11 +8,6 @@ - + /** * @dev Simple minimal forwarder to be used together with an ERC2771 compatible contract. See {ERC2771Context}. - * @@ -234,17 +234,17 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol --- mocks/SafeERC20Helper.sol 2022-09-20 14:24:58.013407601 +0200 +++ mocks/SafeERC20Helper.sol 2022-09-20 15:09:17.135329080 +0200 @@ -4,7 +4,6 @@ - + import "../utils/Context.sol"; import "../token/ERC20/IERC20.sol"; -import "../token/ERC20/extensions/draft-ERC20Permit.sol"; import "../token/ERC20/utils/SafeERC20.sol"; - + contract ERC20ReturnFalseMock is Context { @@ -106,42 +105,43 @@ } } - + -contract ERC20PermitNoRevertMock is - ERC20("ERC20PermitNoRevertMock", "ERC20PermitNoRevertMock"), - ERC20Permit("ERC20PermitNoRevertMock") @@ -318,13 +318,13 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol +// } +// } +// } - + contract SafeERC20Wrapper is Context { using SafeERC20 for IERC20; @@ -172,18 +172,6 @@ _token.safeDecreaseAllowance(address(0), amount); } - + - function permit( - address owner, - address spender, @@ -350,7 +350,7 @@ diff -ruN proxy/beacon/BeaconProxy.sol proxy/beacon/BeaconProxy.sol + assert(_BEACON_SLOT == bytes32(uint256(keccak256("eip1967.proxy.beacon")) - 1)); _upgradeBeaconToAndCall(beacon, data, false); } - + diff -ruN proxy/Clones.sol proxy/Clones.sol --- proxy/Clones.sol 2022-09-20 14:24:58.013407601 +0200 +++ proxy/Clones.sol 2022-09-20 14:59:00.690035663 +0200 @@ -400,7 +400,7 @@ diff -ruN proxy/Clones.sol proxy/Clones.sol + predicted := keccak256(add(ptr, 0x44), 0x55) } } - + diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol --- proxy/ERC1967/ERC1967Proxy.sol 2022-09-09 10:15:55.890509851 +0200 +++ proxy/ERC1967/ERC1967Proxy.sol 2022-09-20 14:34:24.806582310 +0200 @@ -411,7 +411,7 @@ diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol + assert(_IMPLEMENTATION_SLOT == bytes32(uint256(keccak256("eip1967.proxy.implementation")) - 1)); _upgradeToAndCall(_logic, _data, false); } - + diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/TransparentUpgradeableProxy.sol --- proxy/transparent/TransparentUpgradeableProxy.sol 2022-09-09 10:15:55.890509851 +0200 +++ proxy/transparent/TransparentUpgradeableProxy.sol 2022-09-20 14:34:24.806582310 +0200 @@ -422,7 +422,7 @@ diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/Tr + assert(_ADMIN_SLOT == bytes32(uint256(keccak256("eip1967.proxy.admin")) - 1)); _changeAdmin(admin_); } - + diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol --- proxy/utils/Initializable.sol 2022-09-20 11:16:48.456850883 +0200 +++ proxy/utils/Initializable.sol 2022-09-20 14:34:24.806582310 +0200 @@ -432,13 +432,13 @@ diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol */ - uint8 private _initialized; + uint8 internal _initialized; - + /** * @dev Indicates that the contract is in the process of being initialized. */ - bool private _initializing; + bool internal _initializing; - + /** * @dev Triggered when the contract has been initialized or reinitialized. diff -ruN security/Pausable.sol security/Pausable.sol @@ -446,7 +446,7 @@ diff -ruN security/Pausable.sol security/Pausable.sol +++ security/Pausable.sol 2022-09-20 14:34:24.809915708 +0200 @@ -35,6 +35,13 @@ } - + /** + * @dev Returns true if the contract is paused, and false otherwise. + */ @@ -466,7 +466,7 @@ diff -ruN security/Pausable.sol security/Pausable.sol + require(!paused(), "Pausable: paused"); _; } - + @@ -54,29 +61,8 @@ * - The contract must be paused. */ @@ -496,18 +496,18 @@ diff -ruN security/Pausable.sol security/Pausable.sol require(paused(), "Pausable: not paused"); + _; } - + /** diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol --- token/ERC1155/ERC1155.sol 2022-09-20 11:01:10.432848512 +0200 +++ token/ERC1155/ERC1155.sol 2022-09-20 14:34:24.809915708 +0200 @@ -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; // MUNGED private => internal - + // Mapping from account to operator approvals mapping(address => mapping(address => bool)) private _operatorApprovals; @@ -471,7 +471,7 @@ @@ -538,7 +538,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol - 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 -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol --- token/ERC20/extensions/ERC20FlashMint.sol 2022-09-20 11:01:10.432848512 +0200 @@ -550,7 +550,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 - return 0; + return fee; // HARNESS: made "return" nonzero } - + + uint256 public fee; // HARNESS: added it to simulate random fee amount + /** @@ -783,13 +783,13 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote @@ -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; - + /** @@ -165,7 +165,7 @@ /** @@ -799,26 +799,26 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + function _maxSupply() public view virtual returns (uint224) { //harnessed to public return type(uint224).max; } - + @@ -176,16 +176,16 @@ 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 } - + /** @@ -208,7 +208,7 @@ * @@ -838,7 +838,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + 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 @@ -848,7 +848,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote @@ -255,6 +256,55 @@ } } - + + // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool + function _writeCheckpointAdd( + Checkpoint[] storage ckpts, @@ -908,12 +908,12 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr // 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}. - */ @@ -947,33 +947,33 @@ diff -ruN token/ERC20/README.adoc token/ERC20/README.adoc * {ERC20Wrapper}: wrapper to create an ERC20 backed by another ERC20, with deposit and withdraw methods. Useful in conjunction with {ERC20Votes}. -* {ERC4626}: tokenized vault that manages shares (represented as ERC20) that are backed by assets (another ERC20). +* {ERC20TokenizedVault}: tokenized vault that manages shares (represented as ERC20) that are backed by assets (another ERC20). - + Finally, there are some utilities to interact with ERC20 contracts in various ways. - + @@ -63,7 +63,7 @@ - + {{ERC20FlashMint}} - + -{{ERC4626}} +{{ERC20TokenizedVault}} - + == Draft EIPs - + diff -ruN token/ERC20/utils/SafeERC20.sol token/ERC20/utils/SafeERC20.sol --- token/ERC20/utils/SafeERC20.sol 2022-09-09 10:15:55.893843970 +0200 +++ token/ERC20/utils/SafeERC20.sol 2022-09-20 14:34:28.259983206 +0200 @@ -4,7 +4,6 @@ pragma solidity ^0.8.0; - + import "../IERC20.sol"; -import "../extensions/draft-IERC20Permit.sol"; import "../../../utils/Address.sol"; - + /** @@ -80,22 +79,6 @@ } } - + - function safePermit( - IERC20Permit token, - address owner, @@ -1016,85 +1016,3 @@ diff -ruN utils/Address.sol utils/Address.sol require(address(this).balance >= value, "Address: insufficient balance for call"); (bool success, bytes memory returndata) = target.call{value: value}(data); return verifyCallResultFromTarget(target, success, returndata, errorMessage); -diff -ruN utils/math/Math.sol utils/math/Math.sol ---- utils/math/Math.sol 2022-09-20 14:24:58.016740934 +0200 -+++ utils/math/Math.sol 2022-09-20 14:34:29.036665098 +0200 -@@ -342,4 +342,78 @@ - return result + (rounding == Rounding.Up && 1 << (result * 8) < value ? 1 : 0); - } - } -+ -+ /** -+ * @dev Returns the square root of a number. It the number is not a perfect square, the value is rounded down. -+ * -+ * Inspired by Henry S. Warren, Jr.'s "Hacker's Delight" (Chapter 11). -+ */ -+ function sqrt(uint256 a) internal pure returns (uint256) { -+ if (a == 0) { -+ return 0; -+ } -+ -+ // For our first guess, we get the biggest power of 2 which is smaller than the square root of the target. -+ // We know that the "msb" (most significant bit) of our target number `a` is a power of 2 such that we have -+ // `msb(a) <= a < 2*msb(a)`. -+ // We also know that `k`, the position of the most significant bit, is such that `msb(a) = 2**k`. -+ // This gives `2**k < a <= 2**(k+1)` → `2**(k/2) <= sqrt(a) < 2 ** (k/2+1)`. -+ // Using an algorithm similar to the msb conmputation, we are able to compute `result = 2**(k/2)` which is a -+ // good first aproximation of `sqrt(a)` with at least 1 correct bit. -+ uint256 result = 1; -+ uint256 x = a; -+ if (x >> 128 > 0) { -+ x >>= 128; -+ result <<= 64; -+ } -+ if (x >> 64 > 0) { -+ x >>= 64; -+ result <<= 32; -+ } -+ if (x >> 32 > 0) { -+ x >>= 32; -+ result <<= 16; -+ } -+ if (x >> 16 > 0) { -+ x >>= 16; -+ result <<= 8; -+ } -+ if (x >> 8 > 0) { -+ x >>= 8; -+ result <<= 4; -+ } -+ if (x >> 4 > 0) { -+ x >>= 4; -+ result <<= 2; -+ } -+ if (x >> 2 > 0) { -+ result <<= 1; -+ } -+ -+ // At this point `result` is an estimation with one bit of precision. We know the true value is a uint128, -+ // since it is the square root of a uint256. Newton's method converges quadratically (precision doubles at -+ // every iteration). We thus need at most 7 iteration to turn our partial result with one bit of precision -+ // into the expected uint128 result. -+ unchecked { -+ result = (result + a / result) >> 1; -+ result = (result + a / result) >> 1; -+ result = (result + a / result) >> 1; -+ result = (result + a / result) >> 1; -+ result = (result + a / result) >> 1; -+ result = (result + a / result) >> 1; -+ result = (result + a / result) >> 1; -+ return min(result, a / result); -+ } -+ } -+ -+ /** -+ * @notice Calculates sqrt(a), following the selected rounding direction. -+ */ -+ function sqrt(uint256 a, Rounding rounding) internal pure returns (uint256) { -+ uint256 result = sqrt(a); -+ if (rounding == Rounding.Up && result * result < a) { -+ result += 1; -+ } -+ return result; -+ } - } diff --git a/certora/matrix.json b/certora/matrix.json index 3724f049b..2a537f529 100644 --- a/certora/matrix.json +++ b/certora/matrix.json @@ -6,10 +6,6 @@ "file": "certora/harnesses/ERC1155/ERC1155BurnableHarness.sol", "name": "ERC1155BurnableHarness", "spec": "certora/specs/ERC1155Burnable.spec" -},{ - "file": "certora/harnesses/ERC1155/ERC1155BurnableHarness.sol", - "name": "ERC1155BurnableHarness", - "spec": "certora/specs/ERC1155Burnable.spec" },{ "file": "certora/harnesses/ERC1155/ERC1155PausableHarness.sol", "name": "ERC1155PausableHarness", @@ -19,12 +15,15 @@ "name": "ERC1155SupplyHarness", "spec": "certora/specs/ERC1155Supply.spec" },{ + "disabled": true, "file": "certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol", "name": "GovernorPreventLateQuorumHarness", - "spec": "certora/specs/GovernorPreventLateQuorum.spec" + "spec": "certora/specs/GovernorPreventLateQuorum.spec", + "args": "--rule_sanity advanced" },{ "disabled": true, "file": "certora/harnesses/InitializableComplexHarness.sol", "name": "InitializableComplexHarness", - "spec": "certora/specs/Initializable.spec" + "spec": "certora/specs/Initializable.spec", + "args": "--rule_sanity advanced" }] diff --git a/certora/run.sh b/certora/run.sh new file mode 100644 index 000000000..ec757145f --- /dev/null +++ b/certora/run.sh @@ -0,0 +1,26 @@ +#!/bin/bash + +for receipt in $(cat certora/matrix.json | jq -r ".[$1] | @base64") +do + FILE=$(echo $receipt | base64 --decode | jq -r '.file') + NAME=$(echo $receipt | base64 --decode | jq -r '.name') + SPEC=$(echo $receipt | base64 --decode | jq -r '.spec') + ARGS=$(echo $receipt | base64 --decode | jq -r '.args//""') + DISABLED=$(echo $receipt | base64 --decode | jq -r '.disabled//false') + + + echo "Running $SPEC on $FILE:$NAME ..." + if [[ $DISABLED == 'true' ]]; + then + echo "disabled" + else + certoraRun $FILE --verify $NAME:$SPEC --solc solc --optimistic_loop --loop_iter 3 $ARGS --cloud + fi +done + +# [00] ERC1155.spec -- pass +# [01] ERC1155Burnable.spec -- pass +# [02] ERC1155Pausable.spec -- pass +# [03] ERC1155Supply.spec -- pass +# [04] GovernorPreventLateQuorum.spec -- nope +# [05] Initializable.spec -- nope \ No newline at end of file