diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml new file mode 100644 index 000000000..0bc89572a --- /dev/null +++ b/.github/workflows/verify.yml @@ -0,0 +1,65 @@ +name: Certora + +on: + push: + branches: + - master + - main + - certora/erc20 + - certora/erc1155ext + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + + - name: Install python + uses: actions/setup-python@v2 + with: { python-version: 3.6, cache: 'pip' } + + - name: Install java + uses: actions/setup-java@v1 + with: { java-version: "11", java-package: jre } + + - name: Install certora + run: pip install certora-cli + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.4/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.4 + + - name: Verify rule ${{ matrix.script }} + run: | + touch certora/applyHarness.patch + make -C certora munged + echo "key length" ${#CERTORAKEY} + sh certora/scripts/${{ matrix.script }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 4 + + matrix: + script: +# - old/verifyTimelock.sh +# - old/verifyERC1155.sh +# - old/verifyERC20FlashMint.sh +# - old/verifyERC20Wrapper.sh +# - old/verifyAccessControl.sh +# - old/verifyERC20Votes.sh "checking ERC20Votes.spec on ERC20Votes.sol" +# - old/verifyERC721Votes.sh "checking ERC721Votes.spec on draft-ERC721Votes.sol and Votes.sol" + - Round3/verifyERC1155Burnable.sh + - Round3/verifyERC1155Supply.sh + - Round3/verifyERC1155Pausable.sh + - Round3/verifyInitializable.sh + - Round3/verifyGovernorPreventLateQuorum.sh + + + + diff --git a/.gitignore b/.gitignore index c60c5d945..18817cd29 100644 --- a/.gitignore +++ b/.gitignore @@ -62,3 +62,4 @@ artifacts .certora* .last_confs certora_* +resource_errors.json diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 000000000..5120aebf5 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,3 @@ +{ + "solidity.compileUsingRemoteVersion": "v0.8.2+commit.661d1103" +} \ No newline at end of file diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 0fbe9acad..e339df7c3 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,101 +1,1486 @@ diff -ruN .gitignore .gitignore ---- .gitignore 1969-12-31 19:00:00.000000000 -0500 -+++ .gitignore 2021-12-09 14:46:33.923637220 -0500 +--- .gitignore 1969-12-31 16:00:00.000000000 -0800 ++++ .gitignore 2022-08-11 21:28:36.000000000 -0700 @@ -0,0 +1,2 @@ +* +!.gitignore -diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol ---- governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -245,7 +245,7 @@ - /** - * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum. +diff -ruN access/AccessControl.sol access/AccessControl.sol +--- 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._ */ -- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) { -+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal - ProposalDetails storage details = _proposalDetails[proposalId]; - return quorum(proposalSnapshot(proposalId)) <= details.forVotes; +- function _checkRole(bytes32 role) internal view virtual { ++ function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public + _checkRole(role, _msgSender()); } -@@ -253,7 +253,7 @@ - /** - * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) { -+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal - ProposalDetails storage details = _proposalDetails[proposalId]; - return details.forVotes > details.againstVotes; + +diff -ruN access/Ownable.sol access/Ownable.sol +--- 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 @@ } -diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol ---- governance/extensions/GovernorCountingSimple.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/extensions/GovernorCountingSimple.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -64,7 +64,7 @@ - /** - * @dev See {Governor-_quorumReached}. - */ -- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) { -+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { - ProposalVote storage proposalvote = _proposalVotes[proposalId]; - return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes; -@@ -73,7 +73,7 @@ /** - * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes. +- * @dev Throws if called by any account other than the owner. +- */ +- modifier onlyOwner() { +- _checkOwner(); +- _; +- } +- +- /** + * @dev Returns the address of the current owner. */ -- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) { -+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { - ProposalVote storage proposalvote = _proposalVotes[proposalId]; + function owner() public view virtual returns (address) { +@@ -45,10 +37,11 @@ + } - return proposalvote.forVotes > proposalvote.againstVotes; -diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol ---- governance/extensions/GovernorTimelockControl.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/extensions/GovernorTimelockControl.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -111,7 +111,7 @@ - bytes[] memory calldatas, - bytes32 descriptionHash - ) internal virtual override { -- _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash); -+ _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash); + /** +- * @dev Throws if the sender is not the owner. ++ * @dev Throws if called by any account other than the owner. + */ +- function _checkOwner() internal view virtual { ++ modifier onlyOwner() { + require(owner() == _msgSender(), "Ownable: caller is not the owner"); ++ _; } /** diff -ruN governance/Governor.sol governance/Governor.sol ---- governance/Governor.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/Governor.sol 2021-12-09 14:46:56.411503587 -0500 -@@ -38,8 +38,8 @@ +--- 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; - mapping(uint256 => ProposalCore) private _proposals; -- -+ mapping(uint256 => ProposalCore) public _proposals; -+ - /** - * @dev Restrict access to governor executing address. Some module might override the _executor function to make - * sure this modifier is consistent with the execution model. -@@ -167,12 +167,12 @@ - /** - * @dev Amount of votes already cast passes the threshold limit. - */ -- function _quorumReached(uint256 proposalId) internal view virtual returns (bool); -+ function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal ++ 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 +--- 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"); + 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 Is the proposal successful or not. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool); -+ function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal - - /** - * @dev Register a vote with a given support and voting weight. -diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol ---- token/ERC20/extensions/ERC20Votes.sol 2021-12-03 15:24:56.527654330 -0500 -+++ token/ERC20/extensions/ERC20Votes.sol 2021-12-09 14:46:33.927637196 -0500 -@@ -84,7 +84,7 @@ - * - * - `blockNumber` must have been already mined - */ -- function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) { -+ function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) { - require(blockNumber < block.number, "ERC20Votes: block not yet mined"); - return _checkpointsLookup(_checkpoints[account], blockNumber); + * @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:28:00.000000000 -0700 ++++ governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:28:36.000000000 -0700 +@@ -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 +--- 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; + +- 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/utils/Votes.sol governance/utils/Votes.sol +--- 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)"); + +- 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 view virtual returns (uint256); ++ 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:28:00.000000000 -0700 ++++ metatx/MinimalForwarder.sol 2022-08-11 21:28:36.000000000 -0700 +@@ -8,11 +8,6 @@ + + /** + * @dev Simple minimal forwarder to be used together with an ERC2771 compatible contract. See {ERC2771Context}. +- * +- * MinimalForwarder is mainly meant for testing, as it is missing features to be a good production-ready forwarder. This +- * contract does not intend to have all the properties that are needed for a sound forwarding system. A fully +- * functioning forwarding system with good properties requires more complexity. We suggest you look at other projects +- * such as the GSN which do have the goal of building a system like that. + */ + contract MinimalForwarder is EIP712 { + 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:28:36.000000000 -0700 +@@ -0,0 +1,22 @@ ++// SPDX-License-Identifier: MIT ++ ++pragma solidity ^0.8.0; ++ ++import "../token/ERC20/extensions/ERC20TokenizedVault.sol"; ++ ++// mock class using ERC20 ++contract ERC20TokenizedVaultMock is ERC20TokenizedVault { ++ constructor( ++ IERC20Metadata asset, ++ string memory name, ++ string memory symbol ++ ) ERC20(name, symbol) ERC20TokenizedVault(asset) {} ++ ++ function mockMint(address account, uint256 amount) public { ++ _mint(account, amount); ++ } ++ ++ function mockBurn(address account, uint256 amount) public { ++ _burn(account, amount); ++ } ++} +diff -ruN mocks/ERC4626Mock.sol mocks/ERC4626Mock.sol +--- 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 +- +-pragma solidity ^0.8.0; +- +-import "../token/ERC20/extensions/ERC4626.sol"; +- +-// mock class using ERC20 +-contract ERC4626Mock is ERC4626 { +- constructor( +- IERC20Metadata asset, +- string memory name, +- string memory symbol +- ) ERC20(name, symbol) ERC4626(asset) {} +- +- function mockMint(address account, uint256 amount) public { +- _mint(account, amount); +- } +- +- function mockBurn(address account, uint256 amount) public { +- _burn(account, amount); +- } +-} +diff -ruN mocks/MathMock.sol mocks/MathMock.sol +--- 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); + } +- +- function sqrt(uint256 a, Math.Rounding direction) public pure returns (uint256) { +- return Math.sqrt(a, direction); +- } + } +diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol +--- 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"; + import "../token/ERC20/IERC20.sol"; +-import "../token/ERC20/extensions/draft-ERC20Permit.sol"; + import "../token/ERC20/utils/SafeERC20.sol"; + + contract ERC20ReturnFalseMock is Context { +@@ -106,43 +105,6 @@ + } + } + +-contract ERC20PermitNoRevertMock is +- ERC20("ERC20PermitNoRevertMock", "ERC20PermitNoRevertMock"), +- ERC20Permit("ERC20PermitNoRevertMock") +-{ +- function getChainId() external view returns (uint256) { +- return block.chainid; +- } +- +- function permitThatMayRevert( +- address owner, +- address spender, +- uint256 value, +- uint256 deadline, +- uint8 v, +- bytes32 r, +- bytes32 s +- ) public virtual { +- super.permit(owner, spender, value, deadline, v, r, s); +- } +- +- function permit( +- address owner, +- address spender, +- uint256 value, +- uint256 deadline, +- uint8 v, +- bytes32 r, +- bytes32 s +- ) public virtual override { +- try this.permitThatMayRevert(owner, spender, value, deadline, v, r, s) { +- // do nothing +- } catch { +- // do nothing +- } +- } +-} +- + contract SafeERC20Wrapper is Context { + using SafeERC20 for IERC20; + +@@ -172,18 +134,6 @@ + _token.safeDecreaseAllowance(address(0), amount); + } + +- function permit( +- address owner, +- address spender, +- uint256 value, +- uint256 deadline, +- uint8 v, +- bytes32 r, +- bytes32 s +- ) public { +- SafeERC20.safePermit(IERC20Permit(address(_token)), owner, spender, value, deadline, v, r, s); +- } +- + function setAllowance(uint256 allowance_) public { + ERC20ReturnTrueMock(address(_token)).setAllowance(allowance_); + } +diff -ruN proxy/Clones.sol proxy/Clones.sol +--- 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 { + let ptr := mload(0x40) +- mstore(ptr, 0x3d602d80600a3d3981f3363d3d373d3d3d363d73000000000000000000000000) +- mstore(add(ptr, 0x14), shl(0x60, implementation)) +- mstore(add(ptr, 0x28), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000) +- instance := create(0, ptr, 0x37) ++ mstore(ptr, 0x602d8060093d393df3363d3d373d3d3d363d7300000000000000000000000000) ++ mstore(add(ptr, 0x13), shl(0x60, implementation)) ++ mstore(add(ptr, 0x27), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000) ++ instance := create(0, ptr, 0x36) + } + require(instance != address(0), "ERC1167: create failed"); + } +@@ -45,10 +45,10 @@ + /// @solidity memory-safe-assembly + assembly { + let ptr := mload(0x40) +- mstore(ptr, 0x3d602d80600a3d3981f3363d3d373d3d3d363d73000000000000000000000000) +- mstore(add(ptr, 0x14), shl(0x60, implementation)) +- mstore(add(ptr, 0x28), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000) +- instance := create2(0, ptr, 0x37, salt) ++ mstore(ptr, 0x602d8060093d393df3363d3d373d3d3d363d7300000000000000000000000000) ++ mstore(add(ptr, 0x13), shl(0x60, implementation)) ++ mstore(add(ptr, 0x27), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000) ++ instance := create2(0, ptr, 0x36, salt) + } + require(instance != address(0), "ERC1167: create2 failed"); + } +@@ -64,13 +64,13 @@ + /// @solidity memory-safe-assembly + assembly { + let ptr := mload(0x40) +- mstore(ptr, 0x3d602d80600a3d3981f3363d3d373d3d3d363d73000000000000000000000000) +- mstore(add(ptr, 0x14), shl(0x60, implementation)) +- mstore(add(ptr, 0x28), 0x5af43d82803e903d91602b57fd5bf3ff00000000000000000000000000000000) +- mstore(add(ptr, 0x38), shl(0x60, deployer)) +- mstore(add(ptr, 0x4c), salt) +- mstore(add(ptr, 0x6c), keccak256(ptr, 0x37)) +- predicted := keccak256(add(ptr, 0x37), 0x55) ++ mstore(ptr, 0x602d8060093d393df3363d3d373d3d3d363d7300000000000000000000000000) ++ mstore(add(ptr, 0x13), shl(0x60, implementation)) ++ mstore(add(ptr, 0x27), 0x5af43d82803e903d91602b57fd5bf3ff00000000000000000000000000000000) ++ mstore(add(ptr, 0x37), shl(0x60, deployer)) ++ mstore(add(ptr, 0x4b), salt) ++ mstore(add(ptr, 0x6b), keccak256(ptr, 0x36)) ++ predicted := keccak256(add(ptr, 0x36), 0x55) + } + } + +diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol +--- 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. + */ + constructor(address _logic, bytes memory _data) payable { ++ assert(_IMPLEMENTATION_SLOT == bytes32(uint256(keccak256("eip1967.proxy.implementation")) - 1)); + _upgradeToAndCall(_logic, _data, false); + } + +diff -ruN proxy/beacon/BeaconProxy.sol proxy/beacon/BeaconProxy.sol +--- 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}. + */ + constructor(address beacon, bytes memory data) payable { ++ assert(_BEACON_SLOT == bytes32(uint256(keccak256("eip1967.proxy.beacon")) - 1)); + _upgradeBeaconToAndCall(beacon, data, false); + } + +diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/TransparentUpgradeableProxy.sol +--- 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 + ) payable ERC1967Proxy(_logic, _data) { ++ 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-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 + */ +- 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 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:28:36.000000000 -0700 +@@ -0,0 +1,138 @@ ++// SPDX-License-Identifier: MIT ++// OpenZeppelin Contracts (last updated v4.6.0) (proxy/utils/Initializable.sol) ++ ++pragma solidity ^0.8.2; ++ ++import "../../utils/Address.sol"; ++ ++/** ++ * @dev This is a base contract to aid in writing upgradeable contracts, or any kind of contract that will be deployed ++ * behind a proxy. Since proxied contracts do not make use of a constructor, it's common to move constructor logic to an ++ * external initializer function, usually called `initialize`. It then becomes necessary to protect this initializer ++ * function so it can only be called once. The {initializer} modifier provided by this contract will have this effect. ++ * ++ * The initialization functions use a version number. Once a version number is used, it is consumed and cannot be ++ * reused. This mechanism prevents re-execution of each "step" but allows the creation of new initialization steps in ++ * case an upgrade adds a module that needs to be initialized. ++ * ++ * For example: ++ * ++ * [.hljs-theme-light.nopadding] ++ * ``` ++ * contract MyToken is ERC20Upgradeable { ++ * function initialize() initializer public { ++ * __ERC20_init("MyToken", "MTK"); ++ * } ++ * } ++ * contract MyTokenV2 is MyToken, ERC20PermitUpgradeable { ++ * function initializeV2() reinitializer(2) public { ++ * __ERC20Permit_init("MyToken"); ++ * } ++ * } ++ * ``` ++ * ++ * TIP: To avoid leaving the proxy in an uninitialized state, the initializer function should be called as early as ++ * possible by providing the encoded function call as the `_data` argument to {ERC1967Proxy-constructor}. ++ * ++ * CAUTION: When used with inheritance, manual care must be taken to not invoke a parent initializer twice, or to ensure ++ * that all initializers are idempotent. This is not verified automatically as constructors are by Solidity. ++ * ++ * [CAUTION] ++ * ==== ++ * Avoid leaving a contract uninitialized. ++ * ++ * An uninitialized contract can be taken over by an attacker. This applies to both a proxy and its implementation ++ * contract, which may impact the proxy. To prevent the implementation contract from being used, you should invoke ++ * the {_disableInitializers} function in the constructor to automatically lock it when it is deployed: ++ * ++ * [.hljs-theme-light.nopadding] ++ * ``` ++ * /// @custom:oz-upgrades-unsafe-allow constructor ++ * constructor() { ++ * _disableInitializers(); ++ * } ++ * ``` ++ * ==== ++ */ ++abstract contract Initializable { ++ /** ++ * @dev Indicates that the contract has been initialized. ++ * @custom:oz-retyped-from bool ++ */ ++ uint8 private _initialized; ++ ++ /** ++ * @dev Indicates that the contract is in the process of being initialized. ++ */ ++ bool private _initializing; ++ ++ /** ++ * @dev Triggered when the contract has been initialized or reinitialized. ++ */ ++ event Initialized(uint8 version); ++ ++ /** ++ * @dev A modifier that defines a protected initializer function that can be invoked at most once. In its scope, ++ * `onlyInitializing` functions can be used to initialize parent contracts. Equivalent to `reinitializer(1)`. ++ */ ++ modifier initializer() { ++ bool isTopLevelCall = !_initializing; ++ require( ++ (isTopLevelCall && _initialized < 1) || (!Address.isContract(address(this)) && _initialized == 1), ++ "Initializable: contract is already initialized" ++ ); ++ _initialized = 1; ++ if (isTopLevelCall) { ++ _initializing = true; ++ } ++ _; ++ if (isTopLevelCall) { ++ _initializing = false; ++ emit Initialized(1); ++ } ++ } ++ ++ /** ++ * @dev A modifier that defines a protected reinitializer function that can be invoked at most once, and only if the ++ * contract hasn't been initialized to a greater version before. In its scope, `onlyInitializing` functions can be ++ * used to initialize parent contracts. ++ * ++ * `initializer` is equivalent to `reinitializer(1)`, so a reinitializer may be used after the original ++ * initialization step. This is essential to configure modules that are added through upgrades and that require ++ * initialization. ++ * ++ * Note that versions can jump in increments greater than 1; this implies that if multiple reinitializers coexist in ++ * a contract, executing them in the right order is up to the developer or operator. ++ */ ++ modifier reinitializer(uint8 version) { ++ require(!_initializing && _initialized < version, "Initializable: contract is already initialized"); ++ _initialized = version; ++ _initializing = true; ++ _; ++ _initializing = false; ++ emit Initialized(version); ++ } ++ ++ /** ++ * @dev Modifier to protect an initialization function so that it can only be invoked by functions with the ++ * {initializer} and {reinitializer} modifiers, directly or indirectly. ++ */ ++ modifier onlyInitializing() { ++ require(_initializing, "Initializable: contract is not initializing"); ++ _; ++ } ++ ++ /** ++ * @dev Locks the contract, preventing any future reinitialization. This cannot be part of an initializer call. ++ * Calling this in the constructor of a contract will prevent that contract from being initialized or reinitialized ++ * to any version. It is recommended to use this to lock implementation contracts that are designed to be called ++ * through proxies. ++ */ ++ function _disableInitializers() internal virtual { ++ require(!_initializing, "Initializable: contract is initializing"); ++ if (_initialized < type(uint8).max) { ++ _initialized = type(uint8).max; ++ emit Initialized(type(uint8).max); ++ } ++ } ++} +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:28:36.000000000 -0700 +@@ -0,0 +1,17 @@ ++*************** ++*** 130,136 **** ++ _setInitializedVersion(type(uint8).max); ++ } ++ ++- function _setInitializedVersion(uint8 version) private returns (bool) { ++ // If the contract is initializing we ignore whether _initialized is set in order to support multiple ++ // 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. ++--- 130,136 ---- ++ _setInitializedVersion(type(uint8).max); ++ } ++ +++ function _setInitializedVersion(uint8 version) internal returns (bool) { ++ // If the contract is initializing we ignore whether _initialized is set in order to support multiple ++ // 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:28:00.000000000 -0700 ++++ security/Pausable.sol 2022-08-11 21:28:36.000000000 -0700 +@@ -35,6 +35,13 @@ + } + + /** ++ * @dev Returns true if the contract is paused, and false otherwise. ++ */ ++ function paused() public view virtual returns (bool) { ++ return _paused; ++ } ++ ++ /** + * @dev Modifier to make a function callable only when the contract is not paused. + * + * Requirements: +@@ -42,7 +49,7 @@ + * - The contract must not be paused. + */ + modifier whenNotPaused() { +- _requireNotPaused(); ++ require(!paused(), "Pausable: paused"); + _; + } + +@@ -54,29 +61,8 @@ + * - The contract must be paused. + */ + modifier whenPaused() { +- _requirePaused(); +- _; +- } +- +- /** +- * @dev Returns true if the contract is paused, and false otherwise. +- */ +- function paused() public view virtual returns (bool) { +- return _paused; +- } +- +- /** +- * @dev Throws if the contract is paused. +- */ +- function _requireNotPaused() internal view virtual { +- require(!paused(), "Pausable: paused"); +- } +- +- /** +- * @dev Throws if the contract is not paused. +- */ +- function _requirePaused() internal view virtual { + require(paused(), "Pausable: not paused"); ++ _; + } + + /** +diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol +--- 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; + + // 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 @@ + 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) { +@@ -492,7 +492,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-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. + */ +- 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/README.adoc token/ERC20/README.adoc +--- 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). + * {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/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol +--- 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. + 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 -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:28:36.000000000 -0700 +@@ -0,0 +1,217 @@ ++// SPDX-License-Identifier: MIT ++ ++pragma solidity ^0.8.0; ++ ++import "../ERC20.sol"; ++import "../utils/SafeERC20.sol"; ++import "../../../interfaces/IERC4626.sol"; ++import "../../../utils/math/Math.sol"; ++ ++/** ++ * @dev Implementation of the ERC4626 "Tokenized Vault Standard" as defined in ++ * https://eips.ethereum.org/EIPS/eip-4626[EIP-4626]. ++ * ++ * This extension allows the minting and burning of "shares" (represented using the ERC20 inheritance) in exchange for ++ * underlying "assets" through standardized {deposit}, {mint}, {redeem} and {burn} workflows. This contract extends ++ * the ERC20 standard. Any additional extensions included along it would affect the "shares" token represented by this ++ * contract and not the "assets" token which is an independent contract. ++ * ++ * _Available since v4.7._ ++ */ ++abstract contract ERC20TokenizedVault is ERC20, IERC4626 { ++ using Math for uint256; ++ ++ IERC20Metadata private immutable _asset; ++ ++ /** ++ * @dev Set the underlying asset contract. This must be an ERC20-compatible contract (ERC20 or ERC777). ++ */ ++ constructor(IERC20Metadata asset_) { ++ _asset = asset_; ++ } ++ ++ /** @dev See {IERC4262-asset} */ ++ function asset() public view virtual override returns (address) { ++ return address(_asset); ++ } ++ ++ /** @dev See {IERC4262-totalAssets} */ ++ function totalAssets() public view virtual override returns (uint256) { ++ return _asset.balanceOf(address(this)); ++ } ++ ++ /** @dev See {IERC4262-convertToShares} */ ++ function convertToShares(uint256 assets) public view virtual override returns (uint256 shares) { ++ return _convertToShares(assets, Math.Rounding.Down); ++ } ++ ++ /** @dev See {IERC4262-convertToAssets} */ ++ function convertToAssets(uint256 shares) public view virtual override returns (uint256 assets) { ++ return _convertToAssets(shares, Math.Rounding.Down); ++ } ++ ++ /** @dev See {IERC4262-maxDeposit} */ ++ function maxDeposit(address) public view virtual override returns (uint256) { ++ return _isVaultCollateralized() ? type(uint256).max : 0; ++ } ++ ++ /** @dev See {IERC4262-maxMint} */ ++ function maxMint(address) public view virtual override returns (uint256) { ++ return type(uint256).max; ++ } ++ ++ /** @dev See {IERC4262-maxWithdraw} */ ++ function maxWithdraw(address owner) public view virtual override returns (uint256) { ++ return _convertToAssets(balanceOf(owner), Math.Rounding.Down); ++ } ++ ++ /** @dev See {IERC4262-maxRedeem} */ ++ function maxRedeem(address owner) public view virtual override returns (uint256) { ++ return balanceOf(owner); ++ } ++ ++ /** @dev See {IERC4262-previewDeposit} */ ++ function previewDeposit(uint256 assets) public view virtual override returns (uint256) { ++ return _convertToShares(assets, Math.Rounding.Down); ++ } ++ ++ /** @dev See {IERC4262-previewMint} */ ++ function previewMint(uint256 shares) public view virtual override returns (uint256) { ++ return _convertToAssets(shares, Math.Rounding.Up); ++ } ++ ++ /** @dev See {IERC4262-previewWithdraw} */ ++ function previewWithdraw(uint256 assets) public view virtual override returns (uint256) { ++ return _convertToShares(assets, Math.Rounding.Up); ++ } ++ ++ /** @dev See {IERC4262-previewRedeem} */ ++ function previewRedeem(uint256 shares) public view virtual override returns (uint256) { ++ return _convertToAssets(shares, Math.Rounding.Down); ++ } ++ ++ /** @dev See {IERC4262-deposit} */ ++ function deposit(uint256 assets, address receiver) public virtual override returns (uint256) { ++ require(assets <= maxDeposit(receiver), "ERC20TokenizedVault: deposit more than max"); ++ ++ uint256 shares = previewDeposit(assets); ++ _deposit(_msgSender(), receiver, assets, shares); ++ ++ return shares; ++ } ++ ++ /** @dev See {IERC4262-mint} */ ++ function mint(uint256 shares, address receiver) public virtual override returns (uint256) { ++ require(shares <= maxMint(receiver), "ERC20TokenizedVault: mint more than max"); ++ ++ uint256 assets = previewMint(shares); ++ _deposit(_msgSender(), receiver, assets, shares); ++ ++ return assets; ++ } ++ ++ /** @dev See {IERC4262-withdraw} */ ++ function withdraw( ++ uint256 assets, ++ address receiver, ++ address owner ++ ) public virtual override returns (uint256) { ++ require(assets <= maxWithdraw(owner), "ERC20TokenizedVault: withdraw more than max"); ++ ++ uint256 shares = previewWithdraw(assets); ++ _withdraw(_msgSender(), receiver, owner, assets, shares); ++ ++ return shares; ++ } ++ ++ /** @dev See {IERC4262-redeem} */ ++ function redeem( ++ uint256 shares, ++ address receiver, ++ address owner ++ ) public virtual override returns (uint256) { ++ require(shares <= maxRedeem(owner), "ERC20TokenizedVault: redeem more than max"); ++ ++ uint256 assets = previewRedeem(shares); ++ _withdraw(_msgSender(), receiver, owner, assets, shares); ++ ++ return assets; ++ } ++ ++ /** ++ * @dev Internal convertion function (from assets to shares) with support for rounding direction ++ * ++ * Will revert if assets > 0, totalSupply > 0 and totalAssets = 0. That corresponds to a case where any asset ++ * would represent an infinite amout of shares. ++ */ ++ function _convertToShares(uint256 assets, Math.Rounding rounding) internal view virtual returns (uint256 shares) { ++ uint256 supply = totalSupply(); ++ return ++ (assets == 0 || supply == 0) ++ ? assets.mulDiv(10**decimals(), 10**_asset.decimals(), rounding) ++ : assets.mulDiv(supply, totalAssets(), rounding); ++ } ++ ++ /** ++ * @dev Internal convertion function (from shares to assets) with support for rounding direction ++ */ ++ function _convertToAssets(uint256 shares, Math.Rounding rounding) internal view virtual returns (uint256 assets) { ++ uint256 supply = totalSupply(); ++ return ++ (supply == 0) ++ ? shares.mulDiv(10**_asset.decimals(), 10**decimals(), rounding) ++ : shares.mulDiv(totalAssets(), supply, rounding); ++ } ++ ++ /** ++ * @dev Deposit/mint common workflow ++ */ ++ function _deposit( ++ address caller, ++ address receiver, ++ uint256 assets, ++ uint256 shares ++ ) private { ++ // If _asset is ERC777, `transferFrom` can trigger a reenterancy BEFORE the transfer happens through the ++ // `tokensToSend` hook. On the other hand, the `tokenReceived` hook, that is triggered after the transfer, ++ // calls the vault, which is assumed not malicious. ++ // ++ // Conclusion: we need to do the transfer before we mint so that any reentrancy would happen before the ++ // assets are transfered and before the shares are minted, which is a valid state. ++ // slither-disable-next-line reentrancy-no-eth ++ SafeERC20.safeTransferFrom(_asset, caller, address(this), assets); ++ _mint(receiver, shares); ++ ++ emit Deposit(caller, receiver, assets, shares); ++ } ++ ++ /** ++ * @dev Withdraw/redeem common workflow ++ */ ++ function _withdraw( ++ address caller, ++ address receiver, ++ address owner, ++ uint256 assets, ++ uint256 shares ++ ) private { ++ if (caller != owner) { ++ _spendAllowance(owner, caller, shares); ++ } ++ ++ // If _asset is ERC777, `transfer` can trigger trigger a reentrancy AFTER the transfer happens through the ++ // `tokensReceived` hook. On the other hand, the `tokensToSend` hook, that is triggered before the transfer, ++ // calls the vault, which is assumed not malicious. ++ // ++ // Conclusion: we need to do the transfer after the burn so that any reentrancy would happen after the ++ // shares are burned and after the assets are transfered, which is a valid state. ++ _burn(owner, shares); ++ SafeERC20.safeTransfer(_asset, receiver, assets); ++ ++ emit Withdraw(caller, receiver, owner, assets, shares); ++ } ++ ++ function _isVaultCollateralized() private view returns (bool) { ++ return totalAssets() > 0 || totalSupply() == 0; ++ } ++} +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 22:47:30.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,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 + } + + /** +@@ -187,7 +187,7 @@ + ) internal virtual override { + super._afterTokenTransfer(from, to, amount); + +- _moveVotingPower(delegates(from), delegates(to), amount); ++ _moveVotingPower(delegates(from), delegates(to), amount); + } + + /** +@@ -195,7 +195,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 +212,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 +239,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-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. + */ +- 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/ERC20/extensions/ERC4626.sol token/ERC20/extensions/ERC4626.sol +--- 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 +- +-pragma solidity ^0.8.0; +- +-import "../ERC20.sol"; +-import "../utils/SafeERC20.sol"; +-import "../../../interfaces/IERC4626.sol"; +-import "../../../utils/math/Math.sol"; +- +-/** +- * @dev Implementation of the ERC4626 "Tokenized Vault Standard" as defined in +- * https://eips.ethereum.org/EIPS/eip-4626[EIP-4626]. +- * +- * This extension allows the minting and burning of "shares" (represented using the ERC20 inheritance) in exchange for +- * underlying "assets" through standardized {deposit}, {mint}, {redeem} and {burn} workflows. This contract extends +- * the ERC20 standard. Any additional extensions included along it would affect the "shares" token represented by this +- * contract and not the "assets" token which is an independent contract. +- * +- * _Available since v4.7._ +- */ +-abstract contract ERC4626 is ERC20, IERC4626 { +- using Math for uint256; +- +- IERC20Metadata private immutable _asset; +- +- /** +- * @dev Set the underlying asset contract. This must be an ERC20-compatible contract (ERC20 or ERC777). +- */ +- constructor(IERC20Metadata asset_) { +- _asset = asset_; +- } +- +- /** @dev See {IERC4262-asset} */ +- function asset() public view virtual override returns (address) { +- return address(_asset); +- } +- +- /** @dev See {IERC4262-totalAssets} */ +- function totalAssets() public view virtual override returns (uint256) { +- return _asset.balanceOf(address(this)); +- } +- +- /** @dev See {IERC4262-convertToShares} */ +- function convertToShares(uint256 assets) public view virtual override returns (uint256 shares) { +- return _convertToShares(assets, Math.Rounding.Down); +- } +- +- /** @dev See {IERC4262-convertToAssets} */ +- function convertToAssets(uint256 shares) public view virtual override returns (uint256 assets) { +- return _convertToAssets(shares, Math.Rounding.Down); +- } +- +- /** @dev See {IERC4262-maxDeposit} */ +- function maxDeposit(address) public view virtual override returns (uint256) { +- return _isVaultCollateralized() ? type(uint256).max : 0; +- } +- +- /** @dev See {IERC4262-maxMint} */ +- function maxMint(address) public view virtual override returns (uint256) { +- return type(uint256).max; +- } +- +- /** @dev See {IERC4262-maxWithdraw} */ +- function maxWithdraw(address owner) public view virtual override returns (uint256) { +- return _convertToAssets(balanceOf(owner), Math.Rounding.Down); +- } +- +- /** @dev See {IERC4262-maxRedeem} */ +- function maxRedeem(address owner) public view virtual override returns (uint256) { +- return balanceOf(owner); +- } +- +- /** @dev See {IERC4262-previewDeposit} */ +- function previewDeposit(uint256 assets) public view virtual override returns (uint256) { +- return _convertToShares(assets, Math.Rounding.Down); +- } +- +- /** @dev See {IERC4262-previewMint} */ +- function previewMint(uint256 shares) public view virtual override returns (uint256) { +- return _convertToAssets(shares, Math.Rounding.Up); +- } +- +- /** @dev See {IERC4262-previewWithdraw} */ +- function previewWithdraw(uint256 assets) public view virtual override returns (uint256) { +- return _convertToShares(assets, Math.Rounding.Up); +- } +- +- /** @dev See {IERC4262-previewRedeem} */ +- function previewRedeem(uint256 shares) public view virtual override returns (uint256) { +- return _convertToAssets(shares, Math.Rounding.Down); +- } +- +- /** @dev See {IERC4262-deposit} */ +- function deposit(uint256 assets, address receiver) public virtual override returns (uint256) { +- require(assets <= maxDeposit(receiver), "ERC4626: deposit more than max"); +- +- uint256 shares = previewDeposit(assets); +- _deposit(_msgSender(), receiver, assets, shares); +- +- return shares; +- } +- +- /** @dev See {IERC4262-mint} */ +- function mint(uint256 shares, address receiver) public virtual override returns (uint256) { +- require(shares <= maxMint(receiver), "ERC4626: mint more than max"); +- +- uint256 assets = previewMint(shares); +- _deposit(_msgSender(), receiver, assets, shares); +- +- return assets; +- } +- +- /** @dev See {IERC4262-withdraw} */ +- function withdraw( +- uint256 assets, +- address receiver, +- address owner +- ) public virtual override returns (uint256) { +- require(assets <= maxWithdraw(owner), "ERC4626: withdraw more than max"); +- +- uint256 shares = previewWithdraw(assets); +- _withdraw(_msgSender(), receiver, owner, assets, shares); +- +- return shares; +- } +- +- /** @dev See {IERC4262-redeem} */ +- function redeem( +- uint256 shares, +- address receiver, +- address owner +- ) public virtual override returns (uint256) { +- require(shares <= maxRedeem(owner), "ERC4626: redeem more than max"); +- +- uint256 assets = previewRedeem(shares); +- _withdraw(_msgSender(), receiver, owner, assets, shares); +- +- return assets; +- } +- +- /** +- * @dev Internal convertion function (from assets to shares) with support for rounding direction +- * +- * Will revert if assets > 0, totalSupply > 0 and totalAssets = 0. That corresponds to a case where any asset +- * would represent an infinite amout of shares. +- */ +- function _convertToShares(uint256 assets, Math.Rounding rounding) internal view virtual returns (uint256 shares) { +- uint256 supply = totalSupply(); +- return +- (assets == 0 || supply == 0) +- ? assets.mulDiv(10**decimals(), 10**_asset.decimals(), rounding) +- : assets.mulDiv(supply, totalAssets(), rounding); +- } +- +- /** +- * @dev Internal convertion function (from shares to assets) with support for rounding direction +- */ +- function _convertToAssets(uint256 shares, Math.Rounding rounding) internal view virtual returns (uint256 assets) { +- uint256 supply = totalSupply(); +- return +- (supply == 0) +- ? shares.mulDiv(10**_asset.decimals(), 10**decimals(), rounding) +- : shares.mulDiv(totalAssets(), supply, rounding); +- } +- +- /** +- * @dev Deposit/mint common workflow +- */ +- function _deposit( +- address caller, +- address receiver, +- uint256 assets, +- uint256 shares +- ) private { +- // If _asset is ERC777, `transferFrom` can trigger a reenterancy BEFORE the transfer happens through the +- // `tokensToSend` hook. On the other hand, the `tokenReceived` hook, that is triggered after the transfer, +- // calls the vault, which is assumed not malicious. +- // +- // Conclusion: we need to do the transfer before we mint so that any reentrancy would happen before the +- // assets are transfered and before the shares are minted, which is a valid state. +- // slither-disable-next-line reentrancy-no-eth +- SafeERC20.safeTransferFrom(_asset, caller, address(this), assets); +- _mint(receiver, shares); +- +- emit Deposit(caller, receiver, assets, shares); +- } +- +- /** +- * @dev Withdraw/redeem common workflow +- */ +- function _withdraw( +- address caller, +- address receiver, +- address owner, +- uint256 assets, +- uint256 shares +- ) private { +- if (caller != owner) { +- _spendAllowance(owner, caller, shares); +- } +- +- // If _asset is ERC777, `transfer` can trigger trigger a reentrancy AFTER the transfer happens through the +- // `tokensReceived` hook. On the other hand, the `tokensToSend` hook, that is triggered before the transfer, +- // calls the vault, which is assumed not malicious. +- // +- // Conclusion: we need to do the transfer after the burn so that any reentrancy would happen after the +- // shares are burned and after the assets are transfered, which is a valid state. +- _burn(owner, shares); +- SafeERC20.safeTransfer(_asset, receiver, assets); +- +- emit Withdraw(caller, receiver, owner, assets, shares); +- } +- +- function _isVaultCollateralized() private view returns (bool) { +- return totalAssets() > 0 || totalSupply() == 0; +- } +-} +diff -ruN token/ERC20/utils/SafeERC20.sol token/ERC20/utils/SafeERC20.sol +--- 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; + + import "../IERC20.sol"; +-import "../extensions/draft-IERC20Permit.sol"; + import "../../../utils/Address.sol"; + + /** +@@ -80,22 +79,6 @@ + } + } + +- function safePermit( +- IERC20Permit token, +- address owner, +- address spender, +- uint256 value, +- uint256 deadline, +- uint8 v, +- bytes32 r, +- bytes32 s +- ) internal { +- uint256 nonceBefore = token.nonces(owner); +- token.permit(owner, spender, value, deadline, v, r, s); +- uint256 nonceAfter = token.nonces(owner); +- require(nonceAfter == nonceBefore + 1, "SafeERC20: permit did not succeed"); +- } +- + /** + * @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: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`. + */ +- function _getVotingUnits(address account) internal view virtual override returns (uint256) { ++ function _getVotingUnits(address account) public view virtual override returns (uint256) { + return balanceOf(account); + } + } +diff -ruN utils/Address.sol utils/Address.sol +--- 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 + ) internal returns (bytes memory) { ++ return ""; // external calls havoc + require(address(this).balance >= value, "Address: insufficient balance for call"); + 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:28:00.000000000 -0700 ++++ utils/math/Math.sol 2022-08-11 21:28:36.000000000 -0700 +@@ -149,78 +149,4 @@ + } + return result; + } +- +- /** +- * @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/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol new file mode 100644 index 000000000..3ae6e7e8c --- /dev/null +++ b/certora/harnesses/AccessControlHarness.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v4.5.0) (access/AccessControl.sol) + +pragma solidity ^0.8.0; + +import "../munged/access/AccessControl.sol"; + +contract AccessControlHarness is AccessControl { + +} diff --git a/certora/harnesses/ERC1155/ERC1155BurnableHarness.sol b/certora/harnesses/ERC1155/ERC1155BurnableHarness.sol new file mode 100644 index 000000000..5f7fbd706 --- /dev/null +++ b/certora/harnesses/ERC1155/ERC1155BurnableHarness.sol @@ -0,0 +1,8 @@ +import "../../munged/token/ERC1155/extensions/ERC1155Burnable.sol"; + +contract ERC1155BurnableHarness is ERC1155Burnable { + constructor(string memory uri_) + ERC1155(uri_) + {} +} + diff --git a/certora/harnesses/ERC1155/ERC1155Harness.sol b/certora/harnesses/ERC1155/ERC1155Harness.sol new file mode 100644 index 000000000..94581511c --- /dev/null +++ b/certora/harnesses/ERC1155/ERC1155Harness.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; +import "../../munged/token/ERC1155/ERC1155.sol"; + +contract ERC1155Harness is ERC1155 { + + constructor(string memory uri_) + ERC1155(uri_) + {} + + function burn( address from, uint256 id, uint256 amount) public virtual { + _burn(from, id, amount); + } + function burnBatch( + address from, + uint256[] memory ids, + uint256[] memory amounts + ) public virtual { + _burnBatch(from, ids, amounts); + } + + function mint( + address to, + uint256 id, + uint256 amount, + bytes memory data + ) public virtual { + _mint(to, id, amount, data); + } + + function mintBatch( + address to, + uint256[] memory ids, + uint256[] memory amounts, + bytes memory data + ) public virtual { + _mintBatch(to, ids, amounts, data); + } +} \ No newline at end of file diff --git a/certora/harnesses/ERC1155/ERC1155PausableHarness.sol b/certora/harnesses/ERC1155/ERC1155PausableHarness.sol new file mode 100644 index 000000000..134a78748 --- /dev/null +++ b/certora/harnesses/ERC1155/ERC1155PausableHarness.sol @@ -0,0 +1,22 @@ +import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol"; + +contract ERC1155PausableHarness is ERC1155Pausable { + constructor(string memory uri_) + ERC1155(uri_) + {} + + function pause() public { + _pause(); + } + + function unpause() public { + _unpause(); + } + + function onlyWhenPausedMethod() public whenPaused { + } + + function onlyWhenNotPausedMethod() public whenNotPaused { + } +} + diff --git a/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol b/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol new file mode 100644 index 000000000..6702ede58 --- /dev/null +++ b/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol @@ -0,0 +1,61 @@ +import "../../munged/token/ERC1155/extensions/ERC1155Supply.sol"; + + +contract ERC1155SupplyHarness is ERC1155Supply { + address public owner; + constructor(string memory uri_) ERC1155(uri_) { + owner = msg.sender; + } + + // workaround for problem caused by `exists` being a CVL keyword + function exists_wrapper(uint256 id) public view virtual returns (bool) { + return exists(id); + } + + // These rules were not implemented in the base but there are changes in supply + // that are affected by the internal contracts so we implemented them. We assume + // only the owner can call any of these functions to be able to test them but also + // limit false positives. + + modifier onlyOwner { + require(msg.sender == owner); + _; + } + + function burn( address from, uint256 id, uint256 amount) public virtual onlyOwner { + _burn(from, id, amount); + } + function burnBatch( + address from, + uint256[] memory ids, + uint256[] memory amounts + ) public virtual onlyOwner { + _burnBatch(from, ids, amounts); + } + + function mint( + address to, + uint256 id, + uint256 amount, + bytes memory data + ) public virtual onlyOwner { + _mint(to, id, amount, data); + } + + function mintBatch( + address to, + uint256[] memory ids, + uint256[] memory amounts, + bytes memory data + ) public virtual onlyOwner { + _mintBatch(to, ids, amounts, data); + } + + // In order to check the invariant that zero address never holds any tokens, we need to remove the require + // from this function. + function balanceOf(address account, uint256 id) public view virtual override returns (uint256) { + // require(account != address(0), "ERC1155: address zero is not a valid owner"); + return _balances[id][account]; + } +} + diff --git a/certora/harnesses/ERC20FlashMintHarness.sol b/certora/harnesses/ERC20FlashMintHarness.sol new file mode 100644 index 000000000..aec8c2238 --- /dev/null +++ b/certora/harnesses/ERC20FlashMintHarness.sol @@ -0,0 +1,5 @@ +import "../munged/token/ERC20/extensions/ERC20FlashMint.sol"; + +contract ERC20FlashMintHarness is ERC20FlashMint { + constructor(string memory name, string memory symbol) ERC20(name, symbol) {} +} diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol new file mode 100644 index 000000000..29d060232 --- /dev/null +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -0,0 +1,9 @@ +import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol"; + +contract ERC20PermitHarness is ERC20Permit { + constructor(string memory _name, string memory _symbol) + ERC20(_name, _symbol) + ERC20Permit(_name) + {} +} + diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index 5067ecfba..c2cad2f6d 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -3,26 +3,34 @@ 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; + function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { + return _checkpoints[account][pos].fromBlock; + } + + function ckptVotes(address account, uint32 pos) public view returns (uint224) { + return _checkpoints[account][pos].fromBlock; } - /** - * @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); + function mint(address account, uint256 amount) public { + _mint(account, amount); } + + function burn(address account, uint256 amount) public { + _burn(account, amount); + } + + function unsafeNumCheckpoints(address account) public view returns (uint256) { + return _checkpoints[account].length; + } + + function delegateBySig( + address delegatee, + uint256 nonce, + uint256 expiry, + uint8 v, + bytes32 r, + bytes32 s + ) public virtual override { } + } + diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol new file mode 100644 index 000000000..b000afde4 --- /dev/null +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -0,0 +1,17 @@ +import "../munged/token/ERC20/extensions/ERC20Wrapper.sol"; + +contract ERC20WrapperHarness is ERC20Wrapper { + + constructor(IERC20 underlyingToken, string memory _name, string memory _symbol) + ERC20Wrapper(underlyingToken) + ERC20(_name, _symbol) + {} + + function underlyingTotalSupply() public view returns (uint256) { + return underlying.totalSupply(); + } + + function underlyingBalanceOf(address account) public view returns (uint256) { + return underlying.balanceOf(account); + } +} \ No newline at end of file diff --git a/certora/harnesses/ERC721VotesHarness.sol b/certora/harnesses/ERC721VotesHarness.sol new file mode 100644 index 000000000..9ff8911cd --- /dev/null +++ b/certora/harnesses/ERC721VotesHarness.sol @@ -0,0 +1,26 @@ +pragma solidity ^0.8.0; + +import "../munged/token/ERC721/extensions/draft-ERC721Votes.sol"; + +contract ERC721VotesHarness is ERC721Votes { + constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, symbol){} + + function delegateBySig( + address delegatee, + uint256 nonce, + uint256 expiry, + uint8 v, + bytes32 r, + bytes32 s + ) public virtual override { + assert(true); + } + + function mint(address account, uint256 tokenID) public { + _mint(account, tokenID); + } + + function burn(uint256 tokenID) public { + _burn(tokenID); + } +} \ No newline at end of file diff --git a/certora/harnesses/GovernorPreventLateQuorumHarness.sol b/certora/harnesses/GovernorPreventLateQuorumHarness.sol new file mode 100644 index 000000000..7cc9f5b97 --- /dev/null +++ b/certora/harnesses/GovernorPreventLateQuorumHarness.sol @@ -0,0 +1,184 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../munged/governance/extensions/GovernorPreventLateQuorum.sol"; +import "../munged/governance/Governor.sol"; +import "../munged/governance/extensions/GovernorCountingSimple.sol"; +import "../munged/governance/extensions/GovernorVotes.sol"; +import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../munged/governance/extensions/GovernorTimelockControl.sol"; +import "../munged/token/ERC20/extensions/ERC20Votes.sol"; + +contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl, GovernorPreventLateQuorum { + using SafeCast for uint256; + using Timers for Timers.BlockNumber; + constructor(IVotes _token, TimelockController _timelock, uint64 initialVoteExtension, uint256 quorumNumeratorValue) + Governor("Harness") + GovernorVotes(_token) + GovernorVotesQuorumFraction(quorumNumeratorValue) + GovernorTimelockControl(_timelock) + GovernorPreventLateQuorum(initialVoteExtension) + {} + + mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; + + // variable added to check when _castVote is called + uint256 public latestCastVoteCall; + + // Harness from GovernorPreventLateQuorum // + + function getVoteExtension() public view returns(uint64) { + return _voteExtension; + } + + function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns(bool) { + return _extendedDeadlines[proposalId].isUnset(); + } + + function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns(bool) { + return _extendedDeadlines[proposalId].isStarted(); + } + + function getExtendedDeadline(uint256 proposalId) public view returns(uint64) { + return _extendedDeadlines[proposalId].getDeadline(); + } + + // Harness from GovernorCountingSimple // + + function getAgainstVotes(uint256 proposalId) public view returns(uint256) { + ProposalVote storage proposalvote = _proposalVotes[proposalId]; + return proposalvote.againstVotes; + } + + function getAbstainVotes(uint256 proposalId) public view returns(uint256) { + ProposalVote storage proposalvote = _proposalVotes[proposalId]; + return proposalvote.abstainVotes; + } + + function getForVotes(uint256 proposalId) public view returns(uint256) { + ProposalVote storage proposalvote = _proposalVotes[proposalId]; + return proposalvote.forVotes; + } + + function quorumReached(uint256 proposalId) public view returns(bool) { + return _quorumReached(proposalId); + } + + function voteSucceeded(uint256 proposalId) public view returns(bool) { + return _voteSucceeded(proposalId); + } + + // Harness from Governor // + + function getExecutor() public view returns (address){ + return _executor(); + } + + function isExecuted(uint256 proposalId) public view returns (bool) { + return _proposals[proposalId].executed; + } + + function isCanceled(uint256 proposalId) public view returns (bool) { + return _proposals[proposalId].canceled; + } + + // The following functions are overrides required by Solidity added by Certora. // + + function proposalDeadline(uint256 proposalId) public view virtual override(Governor, GovernorPreventLateQuorum, IGovernor) returns (uint256) { + return super.proposalDeadline(proposalId); + } + + function _castVote( + uint256 proposalId, + address account, + uint8 support, + string memory reason, + bytes memory params + ) internal virtual override(Governor, GovernorPreventLateQuorum) returns (uint256) { + // flag for when _castVote is called + latestCastVoteCall = block.number; + + // added to run GovernorCountingSimple.spec + uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params); + ghost_sum_vote_power_by_id[proposalId] += deltaWeight; + + return deltaWeight; + } + + function lateQuorumVoteExtension() public view virtual override returns (uint64) { + return super.lateQuorumVoteExtension(); + } + + function setLateQuorumVoteExtension(uint64 newVoteExtension) public virtual override onlyGovernance { + super.setLateQuorumVoteExtension(newVoteExtension); + } + + // The following functions are overrides required by Solidity added by OZ Wizard. // + + function votingDelay() public pure override returns (uint256) { + return 1; // 1 block + } + + function votingPeriod() public pure override returns (uint256) { + return 45818; // 1 week + } + + function quorum(uint256 blockNumber) + public + view + override(IGovernor, GovernorVotesQuorumFraction) + returns (uint256) + { + return super.quorum(blockNumber); + } + + function state(uint256 proposalId) + public + view + override(Governor, GovernorTimelockControl) + returns (ProposalState) + { + return super.state(proposalId); + } + + function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description) + public + override(Governor, IGovernor) + returns (uint256) + { + return super.propose(targets, values, calldatas, description); + } + + function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) + internal + override(Governor, GovernorTimelockControl) + { + super._execute(proposalId, targets, values, calldatas, descriptionHash); + } + + function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) + internal + override(Governor, GovernorTimelockControl) + returns (uint256) + { + return super._cancel(targets, values, calldatas, descriptionHash); + } + + function _executor() + internal + view + override(Governor, GovernorTimelockControl) + returns (address) + { + return super._executor(); + } + + function supportsInterface(bytes4 interfaceId) + public + view + override(Governor, GovernorTimelockControl) + returns (bool) + { + return super.supportsInterface(interfaceId); + } +} \ No newline at end of file diff --git a/certora/harnesses/IERC3156FlashBorrowerHarness.sol b/certora/harnesses/IERC3156FlashBorrowerHarness.sol new file mode 100644 index 000000000..097a5c2fd --- /dev/null +++ b/certora/harnesses/IERC3156FlashBorrowerHarness.sol @@ -0,0 +1,20 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts v4.4.1 (interfaces/IERC3156FlashBorrower.sol) + +import "../munged/interfaces/IERC3156FlashBorrower.sol"; + +pragma solidity ^0.8.0; + +contract IERC3156FlashBorrowerHarness is IERC3156FlashBorrower { + bytes32 somethingToReturn; + + function onFlashLoan( + address initiator, + address token, + uint256 amount, + uint256 fee, + bytes calldata data + ) external override returns (bytes32){ + return somethingToReturn; + } +} diff --git a/certora/harnesses/InitializableBasicHarness.sol b/certora/harnesses/InitializableBasicHarness.sol new file mode 100644 index 000000000..94495ea54 --- /dev/null +++ b/certora/harnesses/InitializableBasicHarness.sol @@ -0,0 +1,73 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../munged/proxy/utils/Initializable.sol"; + +contract InitializableBasicHarness is Initializable { + + uint256 public val; + uint256 public a; + uint256 public b; + + modifier version1() { + require(_initialized == 1); + _; + } + + modifier versionN(uint8 n) { + require(_initialized == n); + _; + } + + function initialize(uint256 _val, uint256 _a, uint256 _b) public initializer { + a = _a; + b = _b; + val = _val; + } + + function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) public reinitializer(n) { + a = _a; + b = _b; + val = _val; + } + + // Versioned return functions for testing + + function returnsV1() public view version1 returns(uint256) { + return val; + } + + function returnsVN(uint8 n) public view versionN(n) returns(uint256) { + return val; + } + + function returnsAV1() public view version1 returns(uint256) { + return a; + } + + function returnsAVN(uint8 n) public view versionN(n) returns(uint256) { + return a; + } + + function returnsBV1() public view version1 returns(uint256) { + return b; + } + + function returnsBVN(uint8 n) public view versionN(n) returns(uint256) { + return b; + } + + // Harness // + function initialized() public view returns(uint8) { + return _initialized; + } + + function initializing() public view returns(bool) { + return _initializing; + } + + function thisIsContract() public view returns(bool) { + return !Address.isContract(address(this)); + } + +} diff --git a/certora/harnesses/InitializableComplexHarness.sol b/certora/harnesses/InitializableComplexHarness.sol new file mode 100644 index 000000000..e76af78bc --- /dev/null +++ b/certora/harnesses/InitializableComplexHarness.sol @@ -0,0 +1,81 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../munged/proxy/utils/Initializable.sol"; + +contract InitializableA is Initializable { + uint256 public a; + + modifier version1() { + require(_initialized == 1); + _; + } + + modifier versionN(uint8 n) { + require(_initialized == n); + _; + } + function __InitializableA_init(uint256 _a) internal onlyInitializing { + a = _a; + } + + function returnsAV1() public view version1 returns(uint256) { + return a; + } + + function returnsAVN(uint8 n) public view versionN(n) returns(uint256) { + return a; + } +} + +contract InitializableB is Initializable, InitializableA { + uint256 public b; + function __InitializableB_init(uint256 _b) internal onlyInitializing { + b = _b; + } + + function returnsBV1() public view version1 returns(uint256) { + return b; + } + + function returnsBVN(uint8 n) public view versionN(n) returns(uint256) { + return b; + } +} + +contract InitializableComplexHarness is Initializable, InitializableB { + uint256 public val; + + function initialize(uint256 _val, uint256 _a, uint256 _b) initializer public { + val = _val; + __InitializableA_init(_a); + __InitializableB_init(_b); + } + + function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) reinitializer(n) public { + val = _val; + __InitializableA_init(_a); + __InitializableB_init(_b); + } + + function returnsV1() public view version1 returns(uint256) { + return val; + } + + function returnsVN(uint8 n) public view versionN(n) returns(uint256) { + return val; + } + + // Harness // + function initialized() public view returns(uint8) { + return _initialized; + } + + function initializing() public view returns(bool) { + return _initializing; + } + + function thisIsContract() public view returns(bool) { + return !Address.isContract(address(this)); + } +} diff --git a/certora/harnesses/TimelockControllerHarness.sol b/certora/harnesses/TimelockControllerHarness.sol new file mode 100644 index 000000000..8c3f794fa --- /dev/null +++ b/certora/harnesses/TimelockControllerHarness.sol @@ -0,0 +1,13 @@ +pragma solidity ^0.8.0; + +import "../munged/governance/TimelockController.sol"; + + contract TimelockControllerHarness is TimelockController { + constructor( + uint256 minDelay, + address[] memory proposers, + address[] memory executors + ) TimelockController(minDelay, proposers, executors) { + + } +} \ No newline at end of file diff --git a/certora/harnesses/WizardControlFirstPriority.sol b/certora/harnesses/WizardControlFirstPriority.sol index 5ae7fe066..da9fe8581 100644 --- a/certora/harnesses/WizardControlFirstPriority.sol +++ b/certora/harnesses/WizardControlFirstPriority.sol @@ -7,6 +7,7 @@ import "../munged/governance/extensions/GovernorVotes.sol"; import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; import "../munged/governance/extensions/GovernorTimelockControl.sol"; import "../munged/governance/extensions/GovernorProposalThreshold.sol"; +import "../munged/token/ERC20/extensions/ERC20Votes.sol"; /* Wizard options: diff --git a/certora/harnesses/WizardFirstTry.sol b/certora/harnesses/WizardFirstTry.sol index 83fece04f..4e986ed32 100644 --- a/certora/harnesses/WizardFirstTry.sol +++ b/certora/harnesses/WizardFirstTry.sol @@ -6,6 +6,7 @@ import "../munged/governance/extensions/GovernorCountingSimple.sol"; import "../munged/governance/extensions/GovernorVotes.sol"; import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; import "../munged/governance/extensions/GovernorTimelockCompound.sol"; +import "../munged/token/ERC20/extensions/ERC20Votes.sol"; /* Wizard options: @@ -83,7 +84,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove function getVotes(address account, uint256 blockNumber) public view - override(IGovernor, GovernorVotes) + override(IGovernor, Governor) returns (uint256) { return super.getVotes(account, blockNumber); diff --git a/certora/helpers/DummyERC20A.sol b/certora/helpers/DummyERC20A.sol new file mode 100644 index 000000000..188b92608 --- /dev/null +++ b/certora/helpers/DummyERC20A.sol @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; +import "./DummyERC20Impl.sol"; + +contract DummyERC20A is DummyERC20Impl {} \ No newline at end of file diff --git a/certora/helpers/DummyERC20B.sol b/certora/helpers/DummyERC20B.sol new file mode 100644 index 000000000..0f97f1efc --- /dev/null +++ b/certora/helpers/DummyERC20B.sol @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; +import "./DummyERC20Impl.sol"; + +contract DummyERC20B is DummyERC20Impl {} \ No newline at end of file diff --git a/certora/helpers/DummyERC20Impl.sol b/certora/helpers/DummyERC20Impl.sol new file mode 100644 index 000000000..42e7f2302 --- /dev/null +++ b/certora/helpers/DummyERC20Impl.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +// with mint +contract DummyERC20Impl { + uint256 t; + mapping (address => uint256) b; + mapping (address => mapping (address => uint256)) a; + + string public name; + string public symbol; + uint public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a +b; + require (c >= a); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a>=b); + return a-b; + } + + function totalSupply() external view returns (uint256) { + return t; + } + function balanceOf(address account) external view returns (uint256) { + return b[account]; + } + function transfer(address recipient, uint256 amount) external returns (bool) { + b[msg.sender] = sub(b[msg.sender], amount); + b[recipient] = add(b[recipient], amount); + return true; + } + function allowance(address owner, address spender) external view returns (uint256) { + return a[owner][spender]; + } + function approve(address spender, uint256 amount) external returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool) { + b[sender] = sub(b[sender], amount); + b[recipient] = add(b[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + return true; + } +} \ No newline at end of file diff --git a/certora/scripts/Governor.sh b/certora/scripts/Round1/Governor.sh similarity index 100% rename from certora/scripts/Governor.sh rename to certora/scripts/Round1/Governor.sh diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/Round1/GovernorCountingSimple-counting.sh similarity index 81% rename from certora/scripts/GovernorCountingSimple-counting.sh rename to certora/scripts/Round1/GovernorCountingSimple-counting.sh index 9ed8fe34c..e3b86b555 100644 --- a/certora/scripts/GovernorCountingSimple-counting.sh +++ b/certora/scripts/Round1/GovernorCountingSimple-counting.sh @@ -3,8 +3,6 @@ make -C certora munged certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ --solc solc8.2 \ - --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --rule hasVotedCorrelation \ --msg "$1" diff --git a/certora/scripts/WizardControlFirstPriority.sh b/certora/scripts/Round1/WizardControlFirstPriority.sh similarity index 100% rename from certora/scripts/WizardControlFirstPriority.sh rename to certora/scripts/Round1/WizardControlFirstPriority.sh diff --git a/certora/scripts/WizardFirstTry.sh b/certora/scripts/Round1/WizardFirstTry.sh similarity index 100% rename from certora/scripts/WizardFirstTry.sh rename to certora/scripts/Round1/WizardFirstTry.sh diff --git a/certora/scripts/Round1/sanity.sh b/certora/scripts/Round1/sanity.sh new file mode 100644 index 000000000..afead788d --- /dev/null +++ b/certora/scripts/Round1/sanity.sh @@ -0,0 +1,35 @@ +# make -C certora munged + +# for f in certora/harnesses/Wizard*.sol +# do +# echo "Processing $f" +# file=$(basename $f) +# echo ${file%.*} +# certoraRun certora/harnesses/$file \ +# --verify ${file%.*}:certora/specs/sanity.spec "$@" \ +# --solc solc8.2 --staging shelly/forSasha \ +# --optimistic_loop \ +# --msg "checking sanity on ${file%.*}" +# --settings -copyLoopUnroll=4 +# done + +# TimelockController +certoraRun \ + certora/harnesses/TimelockControllerHarness.sol \ + --verify TimelockControllerHarness:certora/specs/sanity.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --cloud \ + --msg "sanity and keccak check" + + +# Votes +# certoraRun \ +# certora/harnesses/VotesHarness.sol \ +# --verify VotesHarness:certora/specs/sanity.spec \ +# --solc solc8.2 \ +# --optimistic_loop \ +# --cloud \ +# --settings -strictDecompiler=false,-assumeUnwindCond \ +# --msg "sanityVotes" + diff --git a/certora/scripts/sanity.sh b/certora/scripts/Round1/sanityGovernor.sh old mode 100644 new mode 100755 similarity index 100% rename from certora/scripts/sanity.sh rename to certora/scripts/Round1/sanityGovernor.sh diff --git a/certora/scripts/Round1/sanityTokens.sh b/certora/scripts/Round1/sanityTokens.sh new file mode 100755 index 000000000..30828055b --- /dev/null +++ b/certora/scripts/Round1/sanityTokens.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +make -C certora munged + +for f in certora/harnesses/ERC20{Votes,Permit,Wrapper}Harness.sol +do + echo "Processing $f" + file=$(basename $f) + echo ${file%.*} + certoraRun certora/harnesses/$file \ + --verify ${file%.*}:certora/specs/sanity.spec "$@" \ + --solc solc8.2 --staging \ + --optimistic_loop \ + --msg "checking sanity on ${file%.*}" \ + --settings -copyLoopUnroll=4,-strictDecompiler=false \ + --send_only +done diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/Round1/verifyAll.sh similarity index 95% rename from certora/scripts/verifyAll.sh rename to certora/scripts/Round1/verifyAll.sh index 90d76912c..eb71ead26 100644 --- a/certora/scripts/verifyAll.sh +++ b/certora/scripts/Round1/verifyAll.sh @@ -2,6 +2,8 @@ make -C certora munged + + for contract in certora/harnesses/Wizard*.sol; do for spec in certora/specs/*.spec; @@ -16,7 +18,7 @@ do certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ --link ${contractFile%.*}:token=ERC20VotesHarness \ --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc8.2 \ + --solc solc \ --staging shelly/forSasha \ --disableLocalTypeChecking \ --optimistic_loop \ @@ -26,7 +28,7 @@ do else certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc8.2 \ + --solc solc \ --staging shelly/forSasha \ --disableLocalTypeChecking \ --optimistic_loop \ @@ -37,3 +39,4 @@ do fi done done + diff --git a/certora/scripts/Round1/verifyGovernor.sh b/certora/scripts/Round1/verifyGovernor.sh new file mode 100755 index 000000000..2e6639422 --- /dev/null +++ b/certora/scripts/Round1/verifyGovernor.sh @@ -0,0 +1,39 @@ +#!/bin/bash + +make -C certora munged + +for contract in certora/harnesses/Wizard*.sol; +do + for spec in certora/specs/governor*.spec; + do + contractFile=$(basename $contract) + specFile=$(basename $spec) + if [[ "${specFile%.*}" != "RulesInProgress" ]]; + then + echo "Processing ${contractFile%.*} with $specFile" + if [[ "${contractFile%.*}" = *"WizardControl"* ]]; + then + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --link ${contractFile%.*}:token=ERC20VotesHarness \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --send_only \ + --msg "checking $specFile on ${contractFile%.*}" + else + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --send_only \ + --msg "checking $specFile on ${contractFile%.*}" + fi + fi + done +done diff --git a/certora/scripts/Round2/verifyAccessControl.sh b/certora/scripts/Round2/verifyAccessControl.sh new file mode 100644 index 000000000..6fb08381f --- /dev/null +++ b/certora/scripts/Round2/verifyAccessControl.sh @@ -0,0 +1,9 @@ +certoraRun \ + certora/harnesses/AccessControlHarness.sol \ + --verify AccessControlHarness:certora/specs/AccessControl.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --cloud \ + --msg "AccessControl verification" \ + --send_only + \ No newline at end of file diff --git a/certora/scripts/Round2/verifyAll2.sh b/certora/scripts/Round2/verifyAll2.sh new file mode 100644 index 000000000..e1805a2ec --- /dev/null +++ b/certora/scripts/Round2/verifyAll2.sh @@ -0,0 +1,11 @@ +#!/bin/bash + +make -C certora munged + +sh certora/scripts/Round2/verifyAccessControl.sh +sh certora/scripts/Round2/verifyERC20FlashMint.sh +sh certora/scripts/Round2/verifyERC20Votes.sh +sh certora/scripts/Round2/verifyERC20Wrapper.sh +sh certora/scripts/Round2/verifyERC721Votes.sh +sh certora/scripts/Round2/verifyERC1155.sh +sh certora/scripts/Round2/verifyTimelock.sh \ No newline at end of file diff --git a/certora/scripts/Round2/verifyERC1155.sh b/certora/scripts/Round2/verifyERC1155.sh new file mode 100644 index 000000000..733882f0f --- /dev/null +++ b/certora/scripts/Round2/verifyERC1155.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155Harness.sol \ + --verify ERC1155Harness:certora/specs/ERC1155.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --send_only \ + --cloud \ + --msg "ERC1155" + diff --git a/certora/scripts/Round2/verifyERC20FlashMint.sh b/certora/scripts/Round2/verifyERC20FlashMint.sh new file mode 100644 index 000000000..d8d03d24a --- /dev/null +++ b/certora/scripts/Round2/verifyERC20FlashMint.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/ERC20FlashMintHarness.sol certora/harnesses/IERC3156FlashBorrowerHarness.sol \ + certora/munged/token/ERC20/ERC20.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ + --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --cloud \ + --msg "ERC20FlashMint verification" \ + --send_only + \ No newline at end of file diff --git a/certora/scripts/Round2/verifyERC20Votes.sh b/certora/scripts/Round2/verifyERC20Votes.sh new file mode 100644 index 000000000..c9e5db059 --- /dev/null +++ b/certora/scripts/Round2/verifyERC20Votes.sh @@ -0,0 +1,12 @@ +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol \ + --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --cloud \ + --send_only \ + --msg "ERC20Votes $1" \ + + # --disableLocalTypeChecking \ + # --staging "alex/new-dt-hashing-alpha" \ diff --git a/certora/scripts/Round2/verifyERC20Wrapper.sh b/certora/scripts/Round2/verifyERC20Wrapper.sh new file mode 100644 index 000000000..6b60c9556 --- /dev/null +++ b/certora/scripts/Round2/verifyERC20Wrapper.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/ERC20WrapperHarness.sol \ + certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ + --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --cloud \ + --msg "ERC20Wrapper verification" \ + --send_only + \ No newline at end of file diff --git a/certora/scripts/Round2/verifyERC721Votes.sh b/certora/scripts/Round2/verifyERC721Votes.sh new file mode 100644 index 000000000..7e023ef28 --- /dev/null +++ b/certora/scripts/Round2/verifyERC721Votes.sh @@ -0,0 +1,14 @@ +certoraRun \ + certora/harnesses/ERC721VotesHarness.sol \ + certora/munged/utils/Checkpoints.sol \ + --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ + --solc solc8.2 \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --cloud \ + --send_only \ + --msg "ERC721Votes" + + # --staging "alex/new-dt-hashing-alpha" \ + diff --git a/certora/scripts/Round2/verifyTimelock.sh b/certora/scripts/Round2/verifyTimelock.sh new file mode 100644 index 000000000..270f76db9 --- /dev/null +++ b/certora/scripts/Round2/verifyTimelock.sh @@ -0,0 +1,13 @@ +certoraRun \ + certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \ + --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --cloud \ + --settings -byteMapHashingPrecision=32 \ + --msg "TimelockController verification" \ + --send_only \ + + # --staging alex/new-dt-hashing-alpha \ + \ No newline at end of file diff --git a/certora/scripts/Round3/round3.sh b/certora/scripts/Round3/round3.sh new file mode 100644 index 000000000..f976e610c --- /dev/null +++ b/certora/scripts/Round3/round3.sh @@ -0,0 +1,4 @@ +for script in ./certora/scripts/Round3/verify*.sh +do + sh $script +done \ No newline at end of file diff --git a/certora/scripts/Round3/verifyERC1155Burnable.sh b/certora/scripts/Round3/verifyERC1155Burnable.sh new file mode 100644 index 000000000..6d60cf746 --- /dev/null +++ b/certora/scripts/Round3/verifyERC1155Burnable.sh @@ -0,0 +1,8 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ + --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ + --solc solc8.4 \ + --optimistic_loop \ + --loop_iter 3 \ + --msg "ERC1155 Burnable verification all rules" + \ No newline at end of file diff --git a/certora/scripts/Round3/verifyERC1155Pausable.sh b/certora/scripts/Round3/verifyERC1155Pausable.sh new file mode 100755 index 000000000..bfddf66de --- /dev/null +++ b/certora/scripts/Round3/verifyERC1155Pausable.sh @@ -0,0 +1,7 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ + --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ + --solc solc8.4 \ + --optimistic_loop \ + --loop_iter 3 \ + --msg "ERC1155 Pausable verification all rules" diff --git a/certora/scripts/Round3/verifyERC1155Supply.sh b/certora/scripts/Round3/verifyERC1155Supply.sh new file mode 100755 index 000000000..1b688c6e3 --- /dev/null +++ b/certora/scripts/Round3/verifyERC1155Supply.sh @@ -0,0 +1,7 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ + --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ + --solc solc8.4 \ + --optimistic_loop \ + --loop_iter 3 \ + --msg "ERC1155 Supply verification all rules" diff --git a/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh b/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh new file mode 100644 index 000000000..81720cae0 --- /dev/null +++ b/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --solc solc8.4 \ + --optimistic_loop \ + --loop_iter 1 \ + --msg "GovernorPreventLateQuorum verification all rules" \ + + + diff --git a/certora/scripts/Round3/verifyInitializable.sh b/certora/scripts/Round3/verifyInitializable.sh new file mode 100644 index 000000000..30dba2bb8 --- /dev/null +++ b/certora/scripts/Round3/verifyInitializable.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/InitializableComplexHarness.sol \ + --verify InitializableComplexHarness:certora/specs/Initializable.spec \ + --solc solc8.4 \ + --optimistic_loop \ + --loop_iter 3 \ + --msg "Initializable verificaiton all rules on complex harness" \ + + + diff --git a/certora/scripts/verifyERC1155All.sh b/certora/scripts/verifyERC1155All.sh new file mode 100644 index 000000000..865374543 --- /dev/null +++ b/certora/scripts/verifyERC1155All.sh @@ -0,0 +1,11 @@ +make -C certora munged + +certoraRun \ + certora/munged/token/ERC1155/ERC1155.sol \ + --verify ERC1155:certora/specs/ERC1155.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --cloud \ + --send_only \ + --msg "ERC1155 verification all rules " \ No newline at end of file diff --git a/certora/scripts/verifyERC1155Burnable.sh b/certora/scripts/verifyERC1155Burnable.sh new file mode 100644 index 000000000..da19cc9d7 --- /dev/null +++ b/certora/scripts/verifyERC1155Burnable.sh @@ -0,0 +1,12 @@ +make -C certora munged + +certoraRun \ + certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ + --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --send_only \ + --cloud \ + --msg "ERC1155 Burnable verification all rules" + \ No newline at end of file diff --git a/certora/scripts/verifyERC1155BurnableSpecific.sh b/certora/scripts/verifyERC1155BurnableSpecific.sh new file mode 100644 index 000000000..bc98a86d7 --- /dev/null +++ b/certora/scripts/verifyERC1155BurnableSpecific.sh @@ -0,0 +1,13 @@ +make -C certora munged + +certoraRun \ + certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ + --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --cloud \ + --send_only \ + --rule $1 \ + --msg "ERC1155 Burnable verification specific rule $1" + \ No newline at end of file diff --git a/certora/scripts/verifyERC1155Pausable.sh b/certora/scripts/verifyERC1155Pausable.sh new file mode 100755 index 000000000..2c41d9f54 --- /dev/null +++ b/certora/scripts/verifyERC1155Pausable.sh @@ -0,0 +1,11 @@ +make -C certora munged + +certoraRun \ + certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ + --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --send_only \ + --cloud \ + --msg "ERC1155 Pausable verification all rules" diff --git a/certora/scripts/verifyERC1155Specific.sh b/certora/scripts/verifyERC1155Specific.sh new file mode 100644 index 000000000..438d527ca --- /dev/null +++ b/certora/scripts/verifyERC1155Specific.sh @@ -0,0 +1,13 @@ +make -C certora munged + +certoraRun \ + certora/munged/token/ERC1155/ERC1155.sol \ + --verify ERC1155:certora/specs/ERC1155.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --cloud \ + --send_only \ + --rule $1 \ + --msg "ERC1155 Burnable verification specific rule $1" + \ No newline at end of file diff --git a/certora/scripts/verifyERC1155Supply.sh b/certora/scripts/verifyERC1155Supply.sh new file mode 100755 index 000000000..09db4a55a --- /dev/null +++ b/certora/scripts/verifyERC1155Supply.sh @@ -0,0 +1,11 @@ +make -C certora munged + +certoraRun \ + certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ + --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --cloud \ + --send_only \ + --msg "ERC1155 Supply verification all rules" diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh new file mode 100644 index 000000000..4517d161d --- /dev/null +++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh @@ -0,0 +1,12 @@ +certoraRun \ + certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --solc solc \ + --optimistic_loop \ + --rule_sanity advanced \ + --send_only \ + --loop_iter 1 \ + --msg "all sanity" \ + + + diff --git a/certora/scripts/verifyInitializable.sh b/certora/scripts/verifyInitializable.sh new file mode 100644 index 000000000..f302a5c31 --- /dev/null +++ b/certora/scripts/verifyInitializable.sh @@ -0,0 +1,12 @@ +certoraRun \ + certora/harnesses/InitializableComplexHarness.sol \ + --verify InitializableComplexHarness:certora/specs/Initializable.spec \ + --solc solc \ + --optimistic_loop \ + --send_only \ + --rule_sanity advanced \ + --loop_iter 3 \ + --msg "all complex sanity" \ + + + diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec new file mode 100644 index 000000000..b57ce3113 --- /dev/null +++ b/certora/specs/AccessControl.spec @@ -0,0 +1,85 @@ +methods { + grantRole(bytes32, address) + revokeRole(bytes32, address) + _checkRole(bytes32) + safeTransferFrom(address, address, uint256, uint256, bytes) + safeBatchTransferFrom(address, address, uint256[], uint256[], bytes) + + getRoleAdmin(bytes32) returns(bytes32) envfree + hasRole(bytes32, address) returns(bool) envfree +} + + +// STATUS - verified +// If `onlyRole` modifier reverts then `grantRole()` reverts +rule onlyRoleModifierCheckGrant(env e){ + bytes32 role; address account; + + _checkRole@withrevert(e, getRoleAdmin(role)); + bool checkRevert = lastReverted; + + grantRole@withrevert(e, role, account); + bool grantRevert = lastReverted; + + assert checkRevert => grantRevert, "modifier goes bananas"; +} + + +// STATUS - verified +// check onlyRole modifier for revokeRole() +rule onlyRoleModifierCheckRevoke(env e){ + bytes32 role; address account; + + _checkRole@withrevert(e, getRoleAdmin(role)); + bool checkRevert = lastReverted; + + revokeRole@withrevert(e, role, account); + bool revokeRevert = lastReverted; + + assert checkRevert => revokeRevert, "modifier goes bananas"; +} + + +// STATUS - verified +// grantRole() does not affect another accounts +rule grantRoleEffect(env e){ + bytes32 role; address account; + bytes32 anotherRole; address nonEffectedAcc; + require account != nonEffectedAcc; + + bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc); + + grantRole(e, role, account); + + bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc); + + assert hasRoleBefore == hasRoleAfter, "modifier goes bananas"; +} + + +// STATUS - verified +// revokeRole() does not affect another accounts +rule revokeRoleEffect(env e){ + bytes32 role; address account; + bytes32 anotherRole; address nonEffectedAcc; + require account != nonEffectedAcc; + + bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc); + + revokeRole(e, role, account); + + bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc); + + assert hasRoleBefore == hasRoleAfter, "modifier goes bananas"; +} + + + + + + + + + + + diff --git a/certora/specs/ERC1155.spec b/certora/specs/ERC1155.spec new file mode 100644 index 000000000..bd88e8c09 --- /dev/null +++ b/certora/specs/ERC1155.spec @@ -0,0 +1,878 @@ +methods { + isApprovedForAll(address, address) returns(bool) envfree + balanceOf(address, uint256) returns(uint256) envfree + balanceOfBatch(address[], uint256[]) returns(uint256[]) envfree + _doSafeBatchTransferAcceptanceCheck(address, address, address, uint256[], uint256[], bytes) envfree + _doSafeTransferAcceptanceCheck(address, address, address, uint256, uint256, bytes) envfree + + setApprovalForAll(address, bool) + safeTransferFrom(address, address, uint256, uint256, bytes) + safeBatchTransferFrom(address, address, uint256[], uint256[], bytes) + mint(address, uint256, uint256, bytes) + mintBatch(address, uint256[], uint256[], bytes) + burn(address, uint256, uint256) + burnBatch(address, uint256[], uint256[]) +} + + + +///////////////////////////////////////////////// +// Approval (4/4) +///////////////////////////////////////////////// + + +// STATUS - verified +// Function $f, which is not setApprovalForAll, should not change approval +rule unexpectedAllowanceChange(method f, env e) filtered { f -> f.selector != setApprovalForAll(address, bool).selector } { + address account; address operator; + bool approveBefore = isApprovedForAll(account, operator); + + calldataarg args; + f(e, args); + + bool approveAfter = isApprovedForAll(account, operator); + + assert approveBefore == approveAfter, "You couldn't get king's approval this way!"; +} + + +// STATUS - verified +// approval can be changed only by owner +rule onlyOwnerCanApprove(env e){ + address owner; address operator; bool approved; + + bool aprovalBefore = isApprovedForAll(owner, operator); + + setApprovalForAll(e, operator, approved); + + bool aprovalAfter = isApprovedForAll(owner, operator); + + assert aprovalBefore != aprovalAfter => owner == e.msg.sender, "There should be only one owner"; +} + + +// STATUS - verified +// Chech that isApprovedForAll() revertes in planned scenarios and no more. +rule approvalRevertCases(env e){ + address account; address operator; + isApprovedForAll@withrevert(account, operator); + assert !lastReverted, "Houston, we have a problem"; +} + + +// STATUS - verified +// setApproval changes only one approval +rule onlyOneAllowanceChange(method f, env e) { + address owner; address operator; address user; + bool approved; + + bool userApproveBefore = isApprovedForAll(owner, user); + + setApprovalForAll(e, operator, approved); + + bool userApproveAfter = isApprovedForAll(owner, user); + + assert userApproveBefore != userApproveAfter => (e.msg.sender == owner && operator == user), "Imposter!"; +} + + + +///////////////////////////////////////////////// +// Balance (3/3) +///////////////////////////////////////////////// + + +// STATUS - verified +// Function $f, which is not one of transfers, mints and burns, should not change balanceOf of a user +rule unexpectedBalanceChange(method f, env e) + filtered { f -> f.selector != safeTransferFrom(address, address, uint256, uint256, bytes).selector + && f.selector != safeBatchTransferFrom(address, address, uint256[], uint256[], bytes).selector + && f.selector != mint(address, uint256, uint256, bytes).selector + && f.selector != mintBatch(address, uint256[], uint256[], bytes).selector + && f.selector != burn(address, uint256, uint256).selector + && f.selector != burnBatch(address, uint256[], uint256[]).selector } { + address from; uint256 id; + uint256 balanceBefore = balanceOf(from, id); + + calldataarg args; + f(e, args); + + uint256 balanceAfter = balanceOf(from, id); + + assert balanceBefore == balanceAfter, "How you dare to take my money?"; +} + + +// STATUS - verified +// Chech that `balanceOf()` revertes in planned scenarios and no more (only if `account` is 0) +rule balanceOfRevertCases(env e){ + address account; uint256 id; + balanceOf@withrevert(account, id); + assert lastReverted => account == 0, "Houston, we have a problem"; +} + + +// STATUS - verified +// Chech that `balanceOfBatch()` revertes in planned scenarios and no more (only if at least one of `account`s is 0) +rule balanceOfBatchRevertCases(env e){ + address[] accounts; uint256[] ids; + address account1; address account2; address account3; + uint256 id1; uint256 id2; uint256 id3; + + require accounts.length == 3; + require ids.length == 3; + + require accounts[0] == account1; require accounts[1] == account2; require accounts[2] == account3; + + balanceOfBatch@withrevert(accounts, ids); + assert lastReverted => (account1 == 0 || account2 == 0 || account3 == 0), "Houston, we have a problem"; +} + + + +///////////////////////////////////////////////// +// Transfer (13/13) +///////////////////////////////////////////////// + + +// STATUS - verified +// transfer additivity +rule transferAdditivity(env e){ + address from; address to; uint256 id; bytes data; + uint256 amount; uint256 amount1; uint256 amount2; + require amount == amount1 + amount2; + + storage initialStorage = lastStorage; + + safeTransferFrom(e, from, to, id, amount, data); + + uint256 balanceAfterSingleTransaction = balanceOf(to, id); + + safeTransferFrom(e, from, to, id, amount1, data) at initialStorage; + safeTransferFrom(e, from, to, id, amount2, data); + + uint256 balanceAfterDoubleTransaction = balanceOf(to, id); + + assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive"; +} + + +// STATUS - verified +// safeTransferFrom updates `from` and `to` balances +rule transferCorrectness(env e){ + address from; address to; uint256 id; uint256 amount; bytes data; + + require to != from; + + uint256 fromBalanceBefore = balanceOf(from, id); + uint256 toBalanceBefore = balanceOf(to, id); + + safeTransferFrom(e, from, to, id, amount, data); + + uint256 fromBalanceAfter = balanceOf(from, id); + uint256 toBalanceAfter = balanceOf(to, id); + + assert fromBalanceBefore == fromBalanceAfter + amount, "Something wet wrong"; + assert toBalanceBefore == toBalanceAfter - amount, "Something wet wrong"; +} + + +// STATUS - verified +// safeBatchTransferFrom updates `from` and `to` balances) +rule transferBatchCorrectness(env e){ + address from; address to; uint256[] ids; uint256[] amounts; bytes data; + uint256 idToCheck1; uint256 amountToCheck1; + uint256 idToCheck2; uint256 amountToCheck2; + uint256 idToCheck3; uint256 amountToCheck3; + + require to != from; + require idToCheck1 != idToCheck2 && idToCheck3 != idToCheck2 && idToCheck1 != idToCheck3; + + require ids.length == 3; + require amounts.length == 3; + require ids[0] == idToCheck1; require amounts[0] == amountToCheck1; + require ids[1] == idToCheck2; require amounts[1] == amountToCheck2; + require ids[2] == idToCheck3; require amounts[2] == amountToCheck3; + + uint256 fromBalanceBefore1 = balanceOf(from, idToCheck1); + uint256 fromBalanceBefore2 = balanceOf(from, idToCheck2); + uint256 fromBalanceBefore3 = balanceOf(from, idToCheck3); + + uint256 toBalanceBefore1 = balanceOf(to, idToCheck1); + uint256 toBalanceBefore2 = balanceOf(to, idToCheck2); + uint256 toBalanceBefore3 = balanceOf(to, idToCheck3); + + safeBatchTransferFrom(e, from, to, ids, amounts, data); + + uint256 fromBalanceAfter1 = balanceOf(from, idToCheck1); + uint256 fromBalanceAfter2 = balanceOf(from, idToCheck2); + uint256 fromBalanceAfter3 = balanceOf(from, idToCheck3); + + uint256 toBalanceAfter1 = balanceOf(to, idToCheck1); + uint256 toBalanceAfter2 = balanceOf(to, idToCheck2); + uint256 toBalanceAfter3 = balanceOf(to, idToCheck3); + + assert (fromBalanceBefore1 == fromBalanceAfter1 + amountToCheck1) + && (fromBalanceBefore2 == fromBalanceAfter2 + amountToCheck2) + && (fromBalanceBefore3 == fromBalanceAfter3 + amountToCheck3), "Something wet wrong"; + assert (toBalanceBefore1 == toBalanceAfter1 - amountToCheck1) + && (toBalanceBefore2 == toBalanceAfter2 - amountToCheck2) + && (toBalanceBefore3 == toBalanceAfter3 - amountToCheck3), "Something wet wrong"; +} + + +// STATUS - verified +// cannot transfer more than `from` balance (safeTransferFrom version) +rule cannotTransferMoreSingle(env e){ + address from; address to; uint256 id; uint256 amount; bytes data; + uint256 balanceBefore = balanceOf(from, id); + + safeTransferFrom@withrevert(e, from, to, id, amount, data); + + assert amount > balanceBefore => lastReverted, "Achtung! Scammer!"; +} + + +// STATUS - verified +// cannot transfer more than allowed (safeBatchTransferFrom version) +rule cannotTransferMoreBatch(env e){ + address from; address to; uint256[] ids; uint256[] amounts; bytes data; + uint256 idToCheck1; uint256 amountToCheck1; + uint256 idToCheck2; uint256 amountToCheck2; + uint256 idToCheck3; uint256 amountToCheck3; + + uint256 balanceBefore1 = balanceOf(from, idToCheck1); + uint256 balanceBefore2 = balanceOf(from, idToCheck2); + uint256 balanceBefore3 = balanceOf(from, idToCheck3); + + require ids.length == 3; + require amounts.length == 3; + require ids[0] == idToCheck1; require amounts[0] == amountToCheck1; + require ids[1] == idToCheck2; require amounts[1] == amountToCheck2; + require ids[2] == idToCheck3; require amounts[2] == amountToCheck3; + + safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data); + + assert (amountToCheck1 > balanceBefore1 || amountToCheck2 > balanceBefore2 || amountToCheck3 > balanceBefore3) => lastReverted, "Achtung! Scammer!"; +} + + +// STATUS - verified +// Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0 +rule transferBalanceReduceEffect(env e){ + address from; address to; address other; + uint256 id; uint256 amount; + bytes data; + + require other != to; + + uint256 otherBalanceBefore = balanceOf(other, id); + + safeTransferFrom(e, from, to, id, amount, data); + + uint256 otherBalanceAfter = balanceOf(other, id); + + assert from != other => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!"; +} + + +// STATUS - verified +// Sender calling safeTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0 +rule transferBalanceIncreaseEffect(env e){ + address from; address to; address other; + uint256 id; uint256 amount; + bytes data; + + require from != other; + + uint256 otherBalanceBefore = balanceOf(other, id); + + safeTransferFrom(e, from, to, id, amount, data); + + uint256 otherBalanceAfter = balanceOf(other, id); + + assert other != to => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!"; +} + + +// STATUS - verified +// Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0 +rule transferBatchBalanceFromEffect(env e){ + address from; address to; address other; + uint256[] ids; uint256[] amounts; + uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3; + bytes data; + + require other != to; + + uint256 otherBalanceBefore1 = balanceOf(other, id1); + uint256 otherBalanceBefore2 = balanceOf(other, id2); + uint256 otherBalanceBefore3 = balanceOf(other, id3); + + safeBatchTransferFrom(e, from, to, ids, amounts, data); + + uint256 otherBalanceAfter1 = balanceOf(other, id1); + uint256 otherBalanceAfter2 = balanceOf(other, id2); + uint256 otherBalanceAfter3 = balanceOf(other, id3); + + assert from != other => (otherBalanceBefore1 == otherBalanceAfter1 + && otherBalanceBefore2 == otherBalanceAfter2 + && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!"; +} + + +// STATUS - verified +// Sender calling safeBatchTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0 +rule transferBatchBalanceToEffect(env e){ + address from; address to; address other; + uint256[] ids; uint256[] amounts; + uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3; + bytes data; + + require other != from; + + uint256 otherBalanceBefore1 = balanceOf(other, id1); + uint256 otherBalanceBefore2 = balanceOf(other, id2); + uint256 otherBalanceBefore3 = balanceOf(other, id3); + + safeBatchTransferFrom(e, from, to, ids, amounts, data); + + uint256 otherBalanceAfter1 = balanceOf(other, id1); + uint256 otherBalanceAfter2 = balanceOf(other, id2); + uint256 otherBalanceAfter3 = balanceOf(other, id3); + + assert other != to => (otherBalanceBefore1 == otherBalanceAfter1 + && otherBalanceBefore2 == otherBalanceAfter2 + && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!"; +} + + +// STATUS - verified +// cannot transfer without approval (safeTransferFrom version) +rule noTransferForNotApproved(env e) { + address from; address operator; + address to; uint256 id; uint256 amount; bytes data; + + require from != e.msg.sender; + + bool approve = isApprovedForAll(from, e.msg.sender); + + safeTransferFrom@withrevert(e, from, to, id, amount, data); + + assert !approve => lastReverted, "You don't have king's approval!"; +} + + +// STATUS - verified +// cannot transfer without approval (safeBatchTransferFrom version) +rule noTransferBatchForNotApproved(env e) { + address from; address operator; address to; + bytes data; + uint256[] ids; uint256[] amounts; + + require from != e.msg.sender; + + bool approve = isApprovedForAll(from, e.msg.sender); + + safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data); + + assert !approve => lastReverted, "You don't have king's approval!"; +} + + +// STATUS - verified +// safeTransferFrom doesn't affect any approval +rule noTransferEffectOnApproval(env e){ + address from; address to; + address owner; address operator; + uint256 id; uint256 amount; + bytes data; + + bool approveBefore = isApprovedForAll(owner, operator); + + safeTransferFrom(e, from, to, id, amount, data); + + bool approveAfter = isApprovedForAll(owner, operator); + + assert approveBefore == approveAfter, "Something was effected"; +} + + +// STATUS - verified +// safeTransferFrom doesn't affect any approval +rule noTransferBatchEffectOnApproval(env e){ + address from; address to; + address owner; address operator; + uint256[] ids; uint256[] amounts; + bytes data; + + bool approveBefore = isApprovedForAll(owner, operator); + + safeBatchTransferFrom(e, from, to, ids, amounts, data); + + bool approveAfter = isApprovedForAll(owner, operator); + + assert approveBefore == approveAfter, "Something was effected"; +} + + + +///////////////////////////////////////////////// +// Mint (7/9) +///////////////////////////////////////////////// + + +// STATUS - verified +// Additivity of mint: mint(a); mint(b) has same effect as mint(a+b) +rule mintAdditivity(env e){ + address to; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; bytes data; + require amount == amount1 + amount2; + + storage initialStorage = lastStorage; + + mint(e, to, id, amount, data); + + uint256 balanceAfterSingleTransaction = balanceOf(to, id); + + mint(e, to, id, amount1, data) at initialStorage; + mint(e, to, id, amount2, data); + + uint256 balanceAfterDoubleTransaction = balanceOf(to, id); + + assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive"; +} + + +// STATUS - verified +// Chech that `mint()` revertes in planned scenario(s) (only if `to` is 0) +rule mintRevertCases(env e){ + address to; uint256 id; uint256 amount; bytes data; + + mint@withrevert(e, to, id, amount, data); + + assert to == 0 => lastReverted, "Should revert"; +} + + +// STATUS - verified +// Chech that `mintBatch()` revertes in planned scenario(s) (only if `to` is 0 or arrays have different length) +rule mintBatchRevertCases(env e){ + address to; uint256[] ids; uint256[] amounts; bytes data; + + require ids.length < 1000000000; + require amounts.length < 1000000000; + + mintBatch@withrevert(e, to, ids, amounts, data); + + assert (ids.length != amounts.length || to == 0) => lastReverted, "Should revert"; +} + + +// STATUS - verified +// Check that mint updates `to` balance correctly +rule mintCorrectWork(env e){ + address to; uint256 id; uint256 amount; bytes data; + + uint256 otherBalanceBefore = balanceOf(to, id); + + mint(e, to, id, amount, data); + + uint256 otherBalanceAfter = balanceOf(to, id); + + assert otherBalanceBefore == otherBalanceAfter - amount, "Something is wrong"; +} + + +// STATUS - verified +// check that mintBatch updates `bootcamp participantsfrom` balance correctly +rule mintBatchCorrectWork(env e){ + address to; + uint256 id1; uint256 id2; uint256 id3; + uint256 amount1; uint256 amount2; uint256 amount3; + uint256[] ids; uint256[] amounts; + bytes data; + + require ids.length == 3; + require amounts.length == 3; + + require id1 != id2 && id2 != id3 && id3 != id1; + require ids[0] == id1; require ids[1] == id2; require ids[2] == id3; + require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3; + + uint256 otherBalanceBefore1 = balanceOf(to, id1); + uint256 otherBalanceBefore2 = balanceOf(to, id2); + uint256 otherBalanceBefore3 = balanceOf(to, id3); + + mintBatch(e, to, ids, amounts, data); + + uint256 otherBalanceAfter1 = balanceOf(to, id1); + uint256 otherBalanceAfter2 = balanceOf(to, id2); + uint256 otherBalanceAfter3 = balanceOf(to, id3); + + assert otherBalanceBefore1 == otherBalanceAfter1 - amount1 + && otherBalanceBefore2 == otherBalanceAfter2 - amount2 + && otherBalanceBefore3 == otherBalanceAfter3 - amount3 + , "Something is wrong"; +} + + +// STATUS - verified +// The user cannot mint more than max_uint256 +rule cantMintMoreSingle(env e){ + address to; uint256 id; uint256 amount; bytes data; + + require to_mathint(balanceOf(to, id) + amount) > max_uint256; + + mint@withrevert(e, to, id, amount, data); + + assert lastReverted, "Don't be too greedy!"; +} + + +// STATUS - verified +// the user cannot mint more than max_uint256 (batch version) +rule cantMintMoreBatch(env e){ + address to; bytes data; + uint256 id1; uint256 id2; uint256 id3; + uint256 amount1; uint256 amount2; uint256 amount3; + uint256[] ids; uint256[] amounts; + + require ids.length == 3; + require amounts.length == 3; + + require ids[0] == id1; require ids[1] == id2; require ids[2] == id3; + require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3; + + require to_mathint(balanceOf(to, id1) + amount1) > max_uint256 + || to_mathint(balanceOf(to, id2) + amount2) > max_uint256 + || to_mathint(balanceOf(to, id3) + amount3) > max_uint256; + + mintBatch@withrevert(e, to, ids, amounts, data); + + assert lastReverted, "Don't be too greedy!"; +} + + +// STATUS - verified +// `mint()` changes only `to` balance +rule cantMintOtherBalances(env e){ + address to; uint256 id; uint256 amount; bytes data; + address other; + + uint256 otherBalanceBefore = balanceOf(other, id); + + mint(e, to, id, amount, data); + + uint256 otherBalanceAfter = balanceOf(other, id); + + assert other != to => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing"; +} + + +// STATUS - verified +// mintBatch changes only `to` balance +rule cantMintBatchOtherBalances(env e){ + address to; + uint256 id1; uint256 id2; uint256 id3; + uint256[] ids; uint256[] amounts; + address other; + bytes data; + + uint256 otherBalanceBefore1 = balanceOf(other, id1); + uint256 otherBalanceBefore2 = balanceOf(other, id2); + uint256 otherBalanceBefore3 = balanceOf(other, id3); + + mintBatch(e, to, ids, amounts, data); + + uint256 otherBalanceAfter1 = balanceOf(other, id1); + uint256 otherBalanceAfter2 = balanceOf(other, id2); + uint256 otherBalanceAfter3 = balanceOf(other, id3); + + assert other != to => (otherBalanceBefore1 == otherBalanceAfter1 + && otherBalanceBefore2 == otherBalanceAfter2 + && otherBalanceBefore3 == otherBalanceAfter3) + , "I like to see your money disappearing"; +} + + +///////////////////////////////////////////////// +// Burn (9/9) +///////////////////////////////////////////////// + + +// STATUS - verified +// Additivity of burn: burn(a); burn(b) has same effect as burn(a+b) +rule burnAdditivity(env e){ + address from; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; + require amount == amount1 + amount2; + + storage initialStorage = lastStorage; + + burn(e, from, id, amount); + + uint256 balanceAfterSingleTransaction = balanceOf(from, id); + + burn(e, from, id, amount1) at initialStorage; + burn(e, from, id, amount2); + + uint256 balanceAfterDoubleTransaction = balanceOf(from, id); + + assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive"; +} + + +// STATUS - verified +// Chech that `burn()` revertes in planned scenario(s) (if `from` is 0) +rule burnRevertCases(env e){ + address from; uint256 id; uint256 amount; + + burn@withrevert(e, from, id, amount); + + assert from == 0 => lastReverted, "Should revert"; +} + + +// STATUS - verified +// Chech that `balanceOf()` revertes in planned scenario(s) (if `from` is 0 or arrays have different length) +rule burnBatchRevertCases(env e){ + address from; uint256[] ids; uint256[] amounts; + + require ids.length < 1000000000; + require amounts.length < 1000000000; + + burnBatch@withrevert(e, from, ids, amounts); + + assert (from == 0 || ids.length != amounts.length) => lastReverted, "Should revert"; +} + + +// STATUS - verified +// check that burn updates `from` balance correctly +rule burnCorrectWork(env e){ + address from; uint256 id; uint256 amount; + + uint256 otherBalanceBefore = balanceOf(from, id); + + burn(e, from, id, amount); + + uint256 otherBalanceAfter = balanceOf(from, id); + + assert otherBalanceBefore == otherBalanceAfter + amount, "Something is wrong"; +} + + +// STATUS - verified +// check that burnBatch updates `from` balance correctly +rule burnBatchCorrectWork(env e){ + address from; + uint256 id1; uint256 id2; uint256 id3; + uint256 amount1; uint256 amount2; uint256 amount3; + uint256[] ids; uint256[] amounts; + + require ids.length == 3; + + require id1 != id2 && id2 != id3 && id3 != id1; + require ids[0] == id1; require ids[1] == id2; require ids[2] == id3; + require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3; + + uint256 otherBalanceBefore1 = balanceOf(from, id1); + uint256 otherBalanceBefore2 = balanceOf(from, id2); + uint256 otherBalanceBefore3 = balanceOf(from, id3); + + burnBatch(e, from, ids, amounts); + + uint256 otherBalanceAfter1 = balanceOf(from, id1); + uint256 otherBalanceAfter2 = balanceOf(from, id2); + uint256 otherBalanceAfter3 = balanceOf(from, id3); + + assert otherBalanceBefore1 == otherBalanceAfter1 + amount1 + && otherBalanceBefore2 == otherBalanceAfter2 + amount2 + && otherBalanceBefore3 == otherBalanceAfter3 + amount3 + , "Something is wrong"; +} + + +// STATUS - verified +// the user cannot burn more than they have +rule cantBurnMoreSingle(env e){ + address from; uint256 id; uint256 amount; + + require to_mathint(balanceOf(from, id) - amount) < 0; + + burn@withrevert(e, from, id, amount); + + assert lastReverted, "Don't be too greedy!"; +} + + +// STATUS - verified +// the user cannot burn more than they have (batch version) +rule cantBurnMoreBatch(env e){ + address from; + uint256 id1; uint256 id2; uint256 id3; + uint256 amount1; uint256 amount2; uint256 amount3; + uint256[] ids; uint256[] amounts; + + require ids.length == 3; + + require ids[0] == id1; require ids[1] == id2; require ids[2] == id3; + require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3; + + require to_mathint(balanceOf(from, id1) - amount1) < 0 + || to_mathint(balanceOf(from, id2) - amount2) < 0 + || to_mathint(balanceOf(from, id3) - amount3) < 0 ; + + burnBatch@withrevert(e, from, ids, amounts); + + assert lastReverted, "Don't be too greedy!"; +} + + +// STATUS - verified +// burn changes only `from` balance +rule cantBurnOtherBalances(env e){ + address from; uint256 id; uint256 amount; + address other; + + uint256 otherBalanceBefore = balanceOf(other, id); + + burn(e, from, id, amount); + + uint256 otherBalanceAfter = balanceOf(other, id); + + assert other != from => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing"; +} + + +// STATUS - verified +// burnBatch changes only `from` balance +rule cantBurnBatchOtherBalances(env e){ + address from; + uint256 id1; uint256 id2; uint256 id3; + uint256 amount1; uint256 amount2; uint256 amount3; + uint256[] ids; uint256[] amounts; + address other; + + uint256 otherBalanceBefore1 = balanceOf(other, id1); + uint256 otherBalanceBefore2 = balanceOf(other, id2); + uint256 otherBalanceBefore3 = balanceOf(other, id3); + + burnBatch(e, from, ids, amounts); + + uint256 otherBalanceAfter1 = balanceOf(other, id1); + uint256 otherBalanceAfter2 = balanceOf(other, id2); + uint256 otherBalanceAfter3 = balanceOf(other, id3); + + assert other != from => (otherBalanceBefore1 == otherBalanceAfter1 + && otherBalanceBefore2 == otherBalanceAfter2 + && otherBalanceBefore3 == otherBalanceAfter3) + , "I like to see your money disappearing"; +} + +///////////////////////////////////////////////// +// The rules below were added to this base ERC1155 spec as part of a later +// project with OpenZeppelin covering various ERC1155 extensions. +///////////////////////////////////////////////// + +/// The result of transferring a single token must be equivalent whether done +/// via safeTransferFrom or safeBatchTransferFrom. +rule singleTokenSafeTransferFromSafeBatchTransferFromEquivalence { + storage beforeTransfer = lastStorage; + env e; + + address holder; address recipient; + uint256 token; uint256 transferAmount; bytes data; + uint256[] tokens; uint256[] transferAmounts; + + mathint holderStartingBalance = balanceOf(holder, token); + mathint recipientStartingBalance = balanceOf(recipient, token); + + require tokens.length == 1; require transferAmounts.length == 1; + require tokens[0] == token; require transferAmounts[0] == transferAmount; + + // transferring via safeTransferFrom + safeTransferFrom(e, holder, recipient, token, transferAmount, data) at beforeTransfer; + mathint holderSafeTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token); + mathint recipientSafeTransferFromBalanceChange = balanceOf(recipient, token) - recipientStartingBalance; + + // transferring via safeBatchTransferFrom + safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfer; + mathint holderSafeBatchTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token); + mathint recipientSafeBatchTransferFromBalanceChange = balanceOf(recipient, token) - recipientStartingBalance; + + assert holderSafeTransferFromBalanceChange == holderSafeBatchTransferFromBalanceChange + && recipientSafeTransferFromBalanceChange == recipientSafeBatchTransferFromBalanceChange, + "Transferring a single token via safeTransferFrom or safeBatchTransferFrom must be equivalent"; +} + +/// The results of transferring multiple tokens must be equivalent whether done +/// separately via safeTransferFrom or together via safeBatchTransferFrom. +rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence { + storage beforeTransfers = lastStorage; + env e; + + address holder; address recipient; bytes data; + uint256 tokenA; uint256 tokenB; uint256 tokenC; + uint256 transferAmountA; uint256 transferAmountB; uint256 transferAmountC; + uint256[] tokens; uint256[] transferAmounts; + + mathint holderStartingBalanceA = balanceOf(holder, tokenA); + mathint holderStartingBalanceB = balanceOf(holder, tokenB); + mathint holderStartingBalanceC = balanceOf(holder, tokenC); + mathint recipientStartingBalanceA = balanceOf(recipient, tokenA); + mathint recipientStartingBalanceB = balanceOf(recipient, tokenB); + mathint recipientStartingBalanceC = balanceOf(recipient, tokenC); + + require tokens.length == 3; require transferAmounts.length == 3; + require tokens[0] == tokenA; require transferAmounts[0] == transferAmountA; + require tokens[1] == tokenB; require transferAmounts[1] == transferAmountB; + require tokens[2] == tokenC; require transferAmounts[2] == transferAmountC; + + // transferring via safeTransferFrom + safeTransferFrom(e, holder, recipient, tokenA, transferAmountA, data) at beforeTransfers; + safeTransferFrom(e, holder, recipient, tokenB, transferAmountB, data); + safeTransferFrom(e, holder, recipient, tokenC, transferAmountC, data); + mathint holderSafeTransferFromBalanceChangeA = holderStartingBalanceA - balanceOf(holder, tokenA); + mathint holderSafeTransferFromBalanceChangeB = holderStartingBalanceB - balanceOf(holder, tokenB); + mathint holderSafeTransferFromBalanceChangeC = holderStartingBalanceC - balanceOf(holder, tokenC); + mathint recipientSafeTransferFromBalanceChangeA = balanceOf(recipient, tokenA) - recipientStartingBalanceA; + mathint recipientSafeTransferFromBalanceChangeB = balanceOf(recipient, tokenB) - recipientStartingBalanceB; + mathint recipientSafeTransferFromBalanceChangeC = balanceOf(recipient, tokenC) - recipientStartingBalanceC; + + // transferring via safeBatchTransferFrom + safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfers; + mathint holderSafeBatchTransferFromBalanceChangeA = holderStartingBalanceA - balanceOf(holder, tokenA); + mathint holderSafeBatchTransferFromBalanceChangeB = holderStartingBalanceB - balanceOf(holder, tokenB); + mathint holderSafeBatchTransferFromBalanceChangeC = holderStartingBalanceC - balanceOf(holder, tokenC); + mathint recipientSafeBatchTransferFromBalanceChangeA = balanceOf(recipient, tokenA) - recipientStartingBalanceA; + mathint recipientSafeBatchTransferFromBalanceChangeB = balanceOf(recipient, tokenB) - recipientStartingBalanceB; + mathint recipientSafeBatchTransferFromBalanceChangeC = balanceOf(recipient, tokenC) - recipientStartingBalanceC; + + assert holderSafeTransferFromBalanceChangeA == holderSafeBatchTransferFromBalanceChangeA + && holderSafeTransferFromBalanceChangeB == holderSafeBatchTransferFromBalanceChangeB + && holderSafeTransferFromBalanceChangeC == holderSafeBatchTransferFromBalanceChangeC + && recipientSafeTransferFromBalanceChangeA == recipientSafeBatchTransferFromBalanceChangeA + && recipientSafeTransferFromBalanceChangeB == recipientSafeBatchTransferFromBalanceChangeB + && recipientSafeTransferFromBalanceChangeC == recipientSafeBatchTransferFromBalanceChangeC, + "Transferring multiple tokens via safeTransferFrom or safeBatchTransferFrom must be equivalent"; +} + +/// If transfer methods do not revert, the input arrays must be the same length. +rule transfersHaveSameLengthInputArrays { + env e; + + address recipient; bytes data; + uint256[] tokens; uint256[] transferAmounts; + uint max_int = 0xffffffffffffffffffffffffffffffff; + + require tokens.length >= 0 && tokens.length <= max_int; + require transferAmounts.length >= 0 && transferAmounts.length <= max_int; + + safeBatchTransferFrom(e, _, recipient, tokens, transferAmounts, data); + + uint256 tokensLength = tokens.length; + uint256 transferAmountsLength = transferAmounts.length; + + assert tokens.length == transferAmounts.length, + "If transfer methods do not revert, the input arrays must be the same length"; +} diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec new file mode 100644 index 000000000..a5507bfce --- /dev/null +++ b/certora/specs/ERC1155Burnable.spec @@ -0,0 +1,172 @@ +methods { + balanceOf(address, uint256) returns uint256 envfree + isApprovedForAll(address,address) returns bool envfree +} + +/// If a method call reduces account balances, the caller must be either the +/// holder of the account or approved to act on the holder's behalf. +rule onlyHolderOrApprovedCanReduceBalance(method f) +{ + address holder; uint256 token; uint256 amount; + uint256 balanceBefore = balanceOf(holder, token); + + env e; calldataarg args; + f(e, args); + + uint256 balanceAfter = balanceOf(holder, token); + + assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender), + "An account balance may only be reduced by the holder or a holder-approved agent"; +} + +/// Burning a larger amount of a token must reduce that token's balance more +/// than burning a smaller amount. +/// n.b. This rule holds for `burnBatch` as well due to rules establishing +/// appropriate equivance between `burn` and `burnBatch` methods. +rule burnAmountProportionalToBalanceReduction { + storage beforeBurn = lastStorage; + env e; + + address holder; uint256 token; + mathint startingBalance = balanceOf(holder, token); + uint256 smallBurn; uint256 largeBurn; + require smallBurn < largeBurn; + + // smaller burn amount + burn(e, holder, token, smallBurn) at beforeBurn; + mathint smallBurnBalanceChange = startingBalance - balanceOf(holder, token); + + // larger burn amount + burn(e, holder, token, largeBurn) at beforeBurn; + mathint largeBurnBalanceChange = startingBalance - balanceOf(holder, token); + + assert smallBurnBalanceChange < largeBurnBalanceChange, + "A larger burn must lead to a larger decrease in balance"; +} + +/// Two sequential burns must be equivalent to a single burn of the sum of their +/// amounts. +/// This rule holds for `burnBatch` as well due to rules establishing +/// appropriate equivance between `burn` and `burnBatch` methods. +rule sequentialBurnsEquivalentToSingleBurnOfSum { + storage beforeBurns = lastStorage; + env e; + + address holder; uint256 token; + mathint startingBalance = balanceOf(holder, token); + uint256 firstBurn; uint256 secondBurn; uint256 sumBurn; + require sumBurn == firstBurn + secondBurn; + + // sequential burns + burn(e, holder, token, firstBurn) at beforeBurns; + burn(e, holder, token, secondBurn); + mathint sequentialBurnsBalanceChange = startingBalance - balanceOf(holder, token); + + // burn of sum of sequential burns + burn(e, holder, token, sumBurn) at beforeBurns; + mathint sumBurnBalanceChange = startingBalance - balanceOf(holder, token); + + assert sequentialBurnsBalanceChange == sumBurnBalanceChange, + "Sequential burns must be equivalent to a burn of their sum"; +} + +/// The result of burning a single token must be equivalent whether done via +/// burn or burnBatch. +rule singleTokenBurnBurnBatchEquivalence { + storage beforeBurn = lastStorage; + env e; + + address holder; + uint256 token; uint256 burnAmount; + uint256[] tokens; uint256[] burnAmounts; + + mathint startingBalance = balanceOf(holder, token); + + require tokens.length == 1; require burnAmounts.length == 1; + require tokens[0] == token; require burnAmounts[0] == burnAmount; + + // burning via burn + burn(e, holder, token, burnAmount) at beforeBurn; + mathint burnBalanceChange = startingBalance - balanceOf(holder, token); + + // burning via burnBatch + burnBatch(e, holder, tokens, burnAmounts) at beforeBurn; + mathint burnBatchBalanceChange = startingBalance - balanceOf(holder, token); + + assert burnBalanceChange == burnBatchBalanceChange, + "Burning a single token via burn or burnBatch must be equivalent"; +} + +/// The results of burning multiple tokens must be equivalent whether done +/// separately via burn or together via burnBatch. +rule multipleTokenBurnBurnBatchEquivalence { + storage beforeBurns = lastStorage; + env e; + + address holder; + uint256 tokenA; uint256 tokenB; uint256 tokenC; + uint256 burnAmountA; uint256 burnAmountB; uint256 burnAmountC; + uint256[] tokens; uint256[] burnAmounts; + + mathint startingBalanceA = balanceOf(holder, tokenA); + mathint startingBalanceB = balanceOf(holder, tokenB); + mathint startingBalanceC = balanceOf(holder, tokenC); + + require tokens.length == 3; require burnAmounts.length == 3; + require tokens[0] == tokenA; require burnAmounts[0] == burnAmountA; + require tokens[1] == tokenB; require burnAmounts[1] == burnAmountB; + require tokens[2] == tokenC; require burnAmounts[2] == burnAmountC; + + // burning via burn + burn(e, holder, tokenA, burnAmountA) at beforeBurns; + burn(e, holder, tokenB, burnAmountB); + burn(e, holder, tokenC, burnAmountC); + mathint burnBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA); + mathint burnBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB); + mathint burnBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC); + + // burning via burnBatch + burnBatch(e, holder, tokens, burnAmounts) at beforeBurns; + mathint burnBatchBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA); + mathint burnBatchBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB); + mathint burnBatchBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC); + + assert burnBalanceChangeA == burnBatchBalanceChangeA + && burnBalanceChangeB == burnBatchBalanceChangeB + && burnBalanceChangeC == burnBatchBalanceChangeC, + "Burning multiple tokens via burn or burnBatch must be equivalent"; +} + +/// If passed empty token and burn amount arrays, burnBatch must not change +/// token balances or address permissions. +rule burnBatchOnEmptyArraysChangesNothing { + uint256 token; address nonHolderA; address nonHolderB; + + uint256 startingBalance = balanceOf(nonHolderA, token); + bool startingPermission = isApprovedForAll(nonHolderA, nonHolderB); + + env e; address holder; uint256[] noTokens; uint256[] noBurnAmounts; + require noTokens.length == 0; require noBurnAmounts.length == 0; + + burnBatch(e, holder, noTokens, noBurnAmounts); + + uint256 endingBalance = balanceOf(nonHolderA, token); + bool endingPermission = isApprovedForAll(nonHolderA, nonHolderB); + + assert startingBalance == endingBalance, + "burnBatch must not change token balances if passed empty arrays"; + assert startingPermission == endingPermission, + "burnBatch must not change account permissions if passed empty arrays"; +} + +/* +/// This rule should always fail. +rule sanity { + method f; env e; calldataarg args; + + f(e, args); + + assert false, + "This rule should always fail"; +} +*/ \ No newline at end of file diff --git a/certora/specs/ERC1155Pausable.spec b/certora/specs/ERC1155Pausable.spec new file mode 100644 index 000000000..53a66e4b6 --- /dev/null +++ b/certora/specs/ERC1155Pausable.spec @@ -0,0 +1,116 @@ +methods { + balanceOf(address, uint256) returns uint256 envfree + paused() returns bool envfree +} + +/// When a contract is in a paused state, the token balance for a given user and +/// token must not change. +rule balancesUnchangedWhenPaused() { + address user; uint256 token; + uint256 balanceBefore = balanceOf(user, token); + + require paused(); + + method f; calldataarg arg; env e; + f(e, arg); + + uint256 balanceAfter = balanceOf(user, token); + + assert balanceBefore == balanceAfter, + "Token balance for a user must not change in a paused contract"; +} + +/// When a contract is in a paused state, transfer methods must revert. +rule transferMethodsRevertWhenPaused (method f) +filtered { + f -> f.selector == safeTransferFrom(address,address,uint256,uint256,bytes).selector + || f.selector == safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector +} +{ + require paused(); + + env e; calldataarg args; + f@withrevert(e, args); + + assert lastReverted, + "Transfer methods must revert in a paused contract"; +} + +/// When a contract is in an unpaused state, calling pause() must pause. +rule pauseMethodPausesContract { + require !paused(); + + env e; + pause(e); + + assert paused(), + "Calling pause must pause an unpaused contract"; +} + +/// When a contract is in a paused state, calling unpause() must unpause. +rule unpauseMethodUnpausesContract { + require paused(); + + env e; + unpause(e); + + assert !paused(), + "Calling unpause must unpause a paused contract"; +} + +/// When a contract is in a paused state, calling pause() must revert. +rule cannotPauseWhilePaused { + require paused(); + + env e; + pause@withrevert(e); + + assert lastReverted, + "A call to pause when already paused must revert"; +} + +/// When a contract is in an unpaused state, calling unpause() must revert. +rule cannotUnpauseWhileUnpaused { + require !paused(); + + env e; + unpause@withrevert(e); + + assert lastReverted, + "A call to unpause when already unpaused must revert"; +} + +/// When a contract is in a paused state, functions with the whenNotPaused +/// modifier must revert. +rule whenNotPausedModifierCausesRevertIfPaused { + require paused(); + + env e; calldataarg args; + onlyWhenNotPausedMethod@withrevert(e, args); + + assert lastReverted, + "Functions with the whenNotPaused modifier must revert if the contract is paused"; +} + +/// When a contract is in an unpaused state, functions with the whenPaused +/// modifier must revert. +rule whenPausedModifierCausesRevertIfUnpaused { + require !paused(); + + env e; calldataarg args; + onlyWhenPausedMethod@withrevert(e, args); + + assert lastReverted, + "Functions with the whenPaused modifier must revert if the contract is not paused"; +} +/* +/// This rule should always fail. +rule sanity { + method f; env e; calldataarg args; + + f(e, args); + + assert false, + "This rule should always fail"; +} +*/ \ No newline at end of file diff --git a/certora/specs/ERC1155Supply.spec b/certora/specs/ERC1155Supply.spec new file mode 100644 index 000000000..0060ab146 --- /dev/null +++ b/certora/specs/ERC1155Supply.spec @@ -0,0 +1,82 @@ + +methods { + totalSupply(uint256) returns uint256 envfree + balanceOf(address, uint256) returns uint256 envfree + exists_wrapper(uint256) returns bool envfree + owner() returns address envfree +} + +/// given two different token ids, if totalSupply for one changes, then +/// totalSupply for other must not +rule token_totalSupply_independence(method f) +filtered { + f -> f.selector != safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector +} +{ + uint256 token1; uint256 token2; + require token1 != token2; + + uint256 token1_before = totalSupply(token1); + uint256 token2_before = totalSupply(token2); + + env e; calldataarg args; + require e.msg.sender != owner(); // owner can call mintBatch and burnBatch in our harness + f(e, args); + + uint256 token1_after = totalSupply(token1); + uint256 token2_after = totalSupply(token2); + + assert token1_after != token1_before => token2_after == token2_before, + "methods must not change the total supply of more than one token"; +} + +/******************************************************************************/ + +ghost mapping(uint256 => mathint) sumOfBalances { + init_state axiom forall uint256 token . sumOfBalances[token] == 0; +} + +hook Sstore _balances[KEY uint256 token][KEY address user] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalances[token] = sumOfBalances[token] + newValue - oldValue; +} + +/// The sum of the balances over all users must equal the total supply for a +/// given token. +invariant total_supply_is_sum_of_balances(uint256 token) + sumOfBalances[token] == totalSupply(token) + { + preserved { + requireInvariant balanceOfZeroAddressIsZero(token); + } + } + +/******************************************************************************/ + +/// The balance of a token for the zero address must be zero. +invariant balanceOfZeroAddressIsZero(uint256 token) + balanceOf(0, token) == 0 + +/// If a user has a token, then the token should exist. +rule held_tokens_should_exist { + address user; uint256 token; + + requireInvariant balanceOfZeroAddressIsZero(token); + + // This assumption is safe because of total_supply_is_sum_of_balances + require balanceOf(user, token) <= totalSupply(token); + + // note: `exists_wrapper` just calls `exists` + assert balanceOf(user, token) > 0 => exists_wrapper(token), + "if a user's balance for a token is positive, the token must exist"; +} + +/******************************************************************************/ +/* +rule sanity { + method f; env e; calldataarg args; + + f(e, args); + + assert false; +} +*/ diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec new file mode 100644 index 000000000..3142f508f --- /dev/null +++ b/certora/specs/ERC20FlashMint.spec @@ -0,0 +1,28 @@ +import "erc20.spec" + +methods { + maxFlashLoan(address) returns(uint256) envfree + _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount) +} + +ghost mapping(address => uint256) trackedBurnAmount; + +function specBurn(address account, uint256 amount) returns bool { // retuns needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'" + trackedBurnAmount[account] = amount; + return true; +} + + +// STATUS - verified +// Check that if flashLoan() call is successful, then proper amount of tokens was burnt(fee + flashLoan amount) +rule letsWatchItBurns(env e){ + address receiver; address token; uint256 amount; bytes data; + + uint256 feeBefore = flashFee(e, token, amount); + + flashLoan(e, receiver, token, amount, data); + + uint256 burned = trackedBurnAmount[receiver]; + + assert to_mathint(amount + feeBefore) == burned, "cheater"; +} diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec new file mode 100644 index 000000000..f0b9cde0d --- /dev/null +++ b/certora/specs/ERC20Votes.spec @@ -0,0 +1,332 @@ +methods { + // functions + checkpoints(address, uint32) envfree + numCheckpoints(address) returns (uint32) envfree + delegates(address) returns (address) envfree + getVotes(address) returns (uint256) envfree + getPastVotes(address, uint256) returns (uint256) + getPastTotalSupply(uint256) returns (uint256) + delegate(address) + _delegate(address, address) + // delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) + totalSupply() returns (uint256) envfree + _maxSupply() returns (uint224) envfree + + // harnesss functions + ckptFromBlock(address, uint32) returns (uint32) envfree + ckptVotes(address, uint32) returns (uint224) envfree + mint(address, uint256) + burn(address, uint256) + unsafeNumCheckpoints(address) returns (uint256) envfree + // solidity generated getters + _delegates(address) returns (address) envfree + + // external functions +} +// gets the most recent votes for a user +ghost userVotes(address) returns uint224 { + init_state axiom forall address a. userVotes(a) == 0; +} + +// sums the total votes for all users +ghost totalVotes() returns uint224 { + init_state axiom totalVotes() == 0; +} +ghost lastIndex(address) returns uint32; +// helper + +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() + newVotes - userVotes(account); + + havoc lastIndex assuming + lastIndex@new(account) == index; +} + + +ghost lastFromBlock(address) returns uint32; + +ghost doubleFromBlock(address) returns bool { + init_state axiom forall address a. doubleFromBlock(a) == false; +} + + + + +hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE { + havoc lastFromBlock assuming + lastFromBlock@new(account) == newBlock; + + havoc doubleFromBlock assuming + doubleFromBlock@new(account) == (newBlock == lastFromBlock(account)); +} + +// 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() + 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 +invariant blockNum_constrains_fromBlock(address account, uint32 index, env e) + ckptFromBlock(account, index) < e.block.number + filtered { f -> !f.isView } +{ + preserved { + require index < numCheckpoints(account); + } +} +// numCheckpoints are less than maxInt +// passes because numCheckpoints does a safeCast +// invariant maxInt_constrains_numBlocks(address account) +// numCheckpoints(account) < 4294967295 // 2^32 + +// can't have more checkpoints for a given account than the last from block +// passes +invariant fromBlock_constrains_numBlocks(address account) + numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1) + filtered { f -> !f.isView } +{ preserved with(env e) { + require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!! +}} + +// for any given checkpoint, the fromBlock must be greater than the checkpoint +// this proves the above invariant in combination with the below invariant +// if checkpoint has a greater fromBlock than the last, and the FromBlock is always greater than the pos. +// Then the number of positions must be less than the currentFromBlock +// ^note that the tool is assuming it's possible for the starting fromBlock to be 0 or anything, and does not know the current starting block +// passes + rule sanity +invariant fromBlock_greaterThanEq_pos(address account, uint32 pos) + ckptFromBlock(account, pos) >= pos + filtered { f -> !f.isView } + +// a larger index must have a larger fromBlock +// passes + rule sanity +invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2) + pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2) + filtered { f -> !f.isView } + + +// converted from an invariant to a rule to slightly change the logic +// if the fromBlock is the same as before, then the number of checkpoints stays the same +// however if the fromBlock is new than the number of checkpoints increases +// passes, fails rule sanity because tautology check seems to be bugged +rule unique_checkpoints_rule(method f) { + env e; calldataarg args; + address account; + uint32 num_ckpts_ = numCheckpoints(account); + uint32 fromBlock_ = num_ckpts_ == 0 ? 0 : ckptFromBlock(account, num_ckpts_ - 1); + + f(e, args); + + uint32 _num_ckpts = numCheckpoints(account); + uint32 _fromBlock = _num_ckpts == 0 ? 0 : ckptFromBlock(account, _num_ckpts - 1); + + + assert fromBlock_ == _fromBlock => num_ckpts_ == _num_ckpts || _num_ckpts == 1, "same fromBlock, new checkpoint"; +} + +// assumes neither account has delegated +// currently fails due to this scenario. A has maxint number of checkpoints +// an additional checkpoint is added which overflows and sets A's votes to 0 +// passes + rule sanity (- a bad tautology check) +rule transfer_safe() { + env e; + uint256 amount; + address a; address b; + require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same + require numCheckpoints(delegates(a)) < 1000000; + require numCheckpoints(delegates(b)) < 1000000; + uint256 votesA_pre = getVotes(delegates(a)); + uint256 votesB_pre = getVotes(delegates(b)); + uint224 totalVotes_pre = totalVotes(); + transferFrom(e, a, b, amount); + + 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 + assert totalVotes_pre == totalVotes_post, "transfer changed total supply"; + assert delegates(a) != 0 => votesA_pre - votesA_post == amount, "A lost the wrong amount of votes"; + assert delegates(b) != 0 => votesB_post - votesB_pre == amount, "B lost the wrong amount of votes"; +} +// for any given function f, if the delegate is changed the function must be delegate or delegateBySig +// passes +rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).selector && + f.selector != _delegate(address, address).selector && + f.selector != delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32).selector) } +{ + env e; calldataarg args; + address account; + address pre = delegates(account); + f(e, args); + address post = delegates(account); + assert pre == post, "invalid delegate change"; +} +// delegates increases the delegatee's votes by the proper amount +// passes + rule sanity +rule delegatee_receives_votes() { + env e; + address delegator; address delegatee; + + require delegates(delegator) != delegatee; + require delegatee != 0x0; + + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 votes_= getVotes(delegatee); + + _delegate(e, delegator, delegatee); + + require lastIndex(delegatee) < 1000000; + + uint256 _votes = getVotes(delegatee); + + assert _votes == votes_ + delegator_bal, "delegatee did not receive votes"; +} + +// passes + rule sanity +rule previous_delegatee_votes_removed() { + env e; + address delegator; address delegatee; address third; + + require third != delegatee; + require delegates(delegator) == third; + require numCheckpoints(third) < 1000000; + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 votes_ = getVotes(third); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(third); + + assert third != 0x0 => _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee"; +} + +// passes with rule sanity +rule delegate_contained() { + env e; + address delegator; address delegatee; address other; + + require other != delegatee; + require other != delegates(delegator); + + uint256 votes_ = getVotes(other); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(other); + + assert votes_ == _votes, "votes not contained"; +} + +rule delegate_no_frontrunning(method f) { + env e; calldataarg args; + address delegator; address delegatee; address third; address other; + + + + require numCheckpoints(delegatee) < 1000000; + require numCheckpoints(third) < 1000000; + + + f(e, args); + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 delegatee_votes_ = getVotes(delegatee); + uint256 third_votes_ = getVotes(third); + uint256 other_votes_ = getVotes(other); + require delegates(delegator) == third; + require third != delegatee; + require other != third; + require other != delegatee; + require delegatee != 0x0; + + _delegate(e, delegator, delegatee); + + uint256 _delegatee_votes = getVotes(delegatee); + uint256 _third_votes = getVotes(third); + uint256 _other_votes = getVotes(other); + + + // previous delegatee loses all of their votes + // delegatee gains that many votes + // third loses any votes delegated to them + assert _delegatee_votes == delegatee_votes_ + delegator_bal, "delegatee did not receive votes"; + assert third != 0 => _third_votes == third_votes_ - delegator_bal, "votes not removed from third"; + assert other_votes_ == _other_votes, "delegate not contained"; +} + + + +// passes +rule mint_increases_totalSupply() { + + env e; + uint256 amount; address account; + + uint256 fromBlock = e.block.number; + uint256 totalSupply_ = totalSupply(); + + mint(e, account, amount); + + uint256 _totalSupply = totalSupply(); + require _totalSupply < _maxSupply(); + + assert _totalSupply == totalSupply_ + amount, "totalSupply not increased properly"; + assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; +} + +// passes +rule burn_decreases_totalSupply() { + env e; + uint256 amount; address account; + + uint256 fromBlock = e.block.number; + uint256 totalSupply_ = totalSupply(); + + burn(e, account, amount); + + uint256 _totalSupply = totalSupply(); + + assert _totalSupply == totalSupply_ - amount, "totalSupply not decreased properly"; + assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; +} + + + +// passes +rule mint_doesnt_increase_totalVotes() { + env e; + uint256 amount; address account; + + uint224 totalVotes_ = totalVotes(); + + mint(e, account, amount); + + assert totalVotes() == totalVotes_, "totalVotes increased"; +} +// passes +rule burn_doesnt_decrease_totalVotes() { + env e; + uint256 amount; address account; + + uint224 totalVotes_ = totalVotes(); + + burn(e, account, amount); + + assert totalVotes() == totalVotes_, "totalVotes decreased"; +} \ No newline at end of file diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec new file mode 100644 index 000000000..1ab9012c2 --- /dev/null +++ b/certora/specs/ERC20Wrapper.spec @@ -0,0 +1,214 @@ +import "erc20.spec" + +methods { + underlying() returns(address) envfree + underlyingTotalSupply() returns(uint256) envfree + underlyingBalanceOf(address) returns(uint256) envfree + + depositFor(address, uint256) returns(bool) + withdrawTo(address, uint256) returns(bool) + _recover(address) returns(uint256) +} + + +// STATUS - verified +// totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency +invariant whatAboutTotal(env e) + totalSupply(e) <= underlyingTotalSupply() + filtered { f -> f.selector != certorafallback_0().selector && !f.isView} + { + preserved { + require underlyingBalanceOf(currentContract) <= underlyingTotalSupply(); + } + preserved depositFor(address account, uint256 amount) with (env e2){ + require totalSupply(e) + amount <= underlyingTotalSupply(); + } + } + + +// STATUS - verified +// totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency +invariant underTotalAndContractBalanceOfCorrelation(env e) + totalSupply(e) <= underlyingBalanceOf(currentContract) + { + preserved with (env e2) { + require underlying() != currentContract; + require e.msg.sender != currentContract; + require e.msg.sender == e2.msg.sender; + } + } + + +// STATUS - verified +// Check that values are updated correctly by `depositFor()` +rule depositForSpecBasic(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 wrapperTotalBefore = totalSupply(e); + uint256 underlyingTotalBefore = underlyingTotalSupply(); + uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); + + depositFor(e, account, amount); + + uint256 wrapperTotalAfter = totalSupply(e); + uint256 underlyingTotalAfter = underlyingTotalSupply(); + uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract); + + assert wrapperTotalBefore == wrapperTotalAfter - amount, "wrapper total wrong update"; + assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated"; + assert underlyingThisBalanceBefore == underlyingThisBalanceAfter - amount, "underlying this balance wrong update"; +} + + +// STATUS - verified +// Check that values are updated correctly by `depositFor()` +rule depositForSpecWrapper(env e){ + address account; uint256 amount; + + require underlying() != currentContract; + + uint256 wrapperUserBalanceBefore = balanceOf(e, account); + uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + + depositFor(e, account, amount); + + uint256 wrapperUserBalanceAfter = balanceOf(e, account); + uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + + assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount, "wrapper balances wrong update"; + assert account != e.msg.sender => wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount + && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update"; +} + + +// STATUS - verified +// Check that values are updated correctly by `depositFor()` +rule depositForSpecUnderlying(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account); + + depositFor(e, account, amount); + + uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account); + + assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore + && underlyingSenderBalanceAfter == underlyingUserBalanceAfter + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount, "underlying balances wrong update"; + + assert account != e.msg.sender && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update"; + + assert account != e.msg.sender && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + && underlyingUserBalanceBefore == underlyingUserBalanceAfter, "underlying balances wrong update"; +} + + +// STATUS - verified +// Check that values are updated correctly by `withdrawTo()` +rule withdrawToSpecBasic(env e){ + address account; uint256 amount; + + require underlying() != currentContract; + + uint256 wrapperTotalBefore = totalSupply(e); + uint256 underlyingTotalBefore = underlyingTotalSupply(); + + withdrawTo(e, account, amount); + + uint256 wrapperTotalAfter = totalSupply(e); + uint256 underlyingTotalAfter = underlyingTotalSupply(); + + assert wrapperTotalBefore == wrapperTotalAfter + amount, "wrapper total wrong update"; + assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated"; +} + + +// STATUS - verified +// Check that values are updated correctly by `withdrawTo()` +rule withdrawToSpecWrapper(env e){ + address account; uint256 amount; + + require underlying() != currentContract; + + uint256 wrapperUserBalanceBefore = balanceOf(e, account); + uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + + withdrawTo(e, account, amount); + + uint256 wrapperUserBalanceAfter = balanceOf(e, account); + uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + + assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount, "wrapper user balance wrong update"; + assert account != e.msg.sender => wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + amount + && wrapperUserBalanceBefore == wrapperUserBalanceAfter, "wrapper user balance wrong update"; +} + + +// STATUS - verified +// cCheck that values are updated correctly by `withdrawTo()` +rule withdrawToSpecUnderlying(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account); + uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); + + withdrawTo(e, account, amount); + + uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account); + uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract); + + assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore + && underlyingSenderBalanceAfter == underlyingUserBalanceAfter + && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update (acc == sender)"; + + assert account != e.msg.sender && account == currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter, "underlying balances wrong update (acc == contract)"; + assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount, "underlying balances wrong update (acc != contract)"; +} + + +// STATUS - verified +// Check that values are updated correctly by `_recover()` +rule recoverSpec(env e){ + address account; uint256 amount; + + uint256 wrapperTotalBefore = totalSupply(e); + uint256 wrapperUserBalanceBefore = balanceOf(e, account); + uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); + + mathint value = underlyingThisBalanceBefore - wrapperTotalBefore; + + _recover(e, account); + + uint256 wrapperTotalAfter = totalSupply(e); + uint256 wrapperUserBalanceAfter = balanceOf(e, account); + uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + + assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update"; + assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value, "wrapper balances wrong update"; + assert e.msg.sender != account => wrapperUserBalanceBefore == wrapperUserBalanceAfter - value + && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update"; +} \ No newline at end of file diff --git a/certora/specs/ERC721Votes.spec b/certora/specs/ERC721Votes.spec new file mode 100644 index 000000000..b4cc8ba3e --- /dev/null +++ b/certora/specs/ERC721Votes.spec @@ -0,0 +1,271 @@ +using Checkpoints as Checkpoints + +methods { + // functions + checkpoints(address, uint32) envfree + numCheckpoints(address) returns (uint32) envfree + getVotes(address) returns (uint256) envfree + getPastVotes(address, uint256) returns (uint256) + getPastTotalSupply(uint256) returns (uint256) + delegates(address) returns (address) envfree + delegate(address) + _delegate(address, address) + delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) + nonces(address) returns (uint256) + totalSupply() returns (uint256) envfree + _maxSupply() returns (uint224) envfree + + // harnesss functions + ckptFromBlock(address, uint32) returns (uint32) envfree + ckptVotes(address, uint32) returns (uint224) envfree + mint(address, uint256) + burn(uint256) + unsafeNumCheckpoints(address) returns (uint256) envfree + + // solidity generated getters + _delegation(address) returns (address) envfree + + // external functions + + +} + +// gets the most recent votes for a user +ghost userVotes(address) returns uint224{ + init_state axiom forall address a. userVotes(a) == 0; +} + +// sums the total votes for all users +ghost totalVotes() returns mathint { + init_state axiom totalVotes() == 0; + axiom totalVotes() >= 0; +} + +hook Sstore _checkpoints[KEY address account].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)); +} + + +ghost lastFromBlock(address) returns uint32; + +ghost doubleFromBlock(address) returns bool { + init_state axiom forall address a. doubleFromBlock(a) == false; +} + + + + +hook Sstore _checkpoints[KEY address account].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE { + havoc lastFromBlock assuming + lastFromBlock@new(account) == newBlock; + + havoc doubleFromBlock assuming + doubleFromBlock@new(account) == (newBlock == lastFromBlock(account)); +} + +// for some checkpoint, the fromBlock is less than the current block number +// passes but fails rule sanity from hash on delegate by sig +invariant timestamp_constrains_fromBlock(address account, uint32 index, env e) + ckptFromBlock(account, index) < e.block.number + filtered { f -> !f.isView } +{ + preserved { + require index < numCheckpoints(account); + } +} + +// numCheckpoints are less than maxInt +// passes because numCheckpoints does a safeCast +// invariant maxInt_constrains_numBlocks(address account) +// numCheckpoints(account) < 4294967295 // 2^32 + +// can't have more checkpoints for a given account than the last from block +// passes +invariant fromBlock_constrains_numBlocks(address account) + numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1) + filtered { f -> !f.isView } +{ preserved with(env e) { + require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!! +}} + +// for any given checkpoint, the fromBlock must be greater than the checkpoint +// this proves the above invariant in combination with the below invariant +// if checkpoint has a greater fromBlock than the last, and the FromBlock is always greater than the pos. +// Then the number of positions must be less than the currentFromBlock +// ^note that the tool is assuming it's possible for the starting fromBlock to be 0 or anything, and does not know the current starting block +// passes + rule sanity +invariant fromBlock_greaterThanEq_pos(address account, uint32 pos) + ckptFromBlock(account, pos) >= pos + filtered { f -> !f.isView } + +// a larger index must have a larger fromBlock +// passes + rule sanity +invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2) + pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2) + filtered { f -> !f.isView } + + +// converted from an invariant to a rule to slightly change the logic +// if the fromBlock is the same as before, then the number of checkpoints stays the same +// however if the fromBlock is new than the number of checkpoints increases +// passes, fails rule sanity because tautology check seems to be bugged +rule unique_checkpoints_rule(method f) { + env e; calldataarg args; + address account; + uint32 num_ckpts_ = numCheckpoints(account); + uint32 fromBlock_ = num_ckpts_ == 0 ? 0 : ckptFromBlock(account, num_ckpts_ - 1); + + f(e, args); + + uint32 _num_ckpts = numCheckpoints(account); + uint32 _fromBlock = _num_ckpts == 0 ? 0 : ckptFromBlock(account, _num_ckpts - 1); + + + assert fromBlock_ == _fromBlock => num_ckpts_ == _num_ckpts || _num_ckpts == 1, "same fromBlock, new checkpoint"; + // this assert fails consistently + // assert !doubleFromBlock(account) => ckpts_ != _ckpts, "new fromBlock but total checkpoints not being increased"; +} + +// assumes neither account has delegated +// currently fails due to this scenario. A has maxint number of checkpoints +// an additional checkpoint is added which overflows and sets A's votes to 0 +// passes + rule sanity (- a bad tautology check) +rule transfer_safe() { + env e; + uint256 ID; + address a; address b; + + require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same + require numCheckpoints(delegates(a)) < 1000000; + require numCheckpoints(delegates(b)) < 1000000; + + uint256 votesA_pre = getVotes(delegates(a)); + uint256 votesB_pre = getVotes(delegates(b)); + + mathint totalVotes_pre = totalVotes(); + + transferFrom(e, a, b, ID); + + mathint 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 + assert totalVotes_pre == totalVotes_post, "transfer changed total supply"; + assert delegates(a) != 0 => votesA_pre - 1 == votesA_post, "A lost the wrong amount of votes"; + assert delegates(b) != 0 => votesB_pre + 1 == votesB_post, "B gained the wrong amount of votes"; +} + +// for any given function f, if the delegate is changed the function must be delegate or delegateBySig +// passes +rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).selector && + f.selector != _delegate(address, address).selector && + f.selector != delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32).selector) } +{ + env e; calldataarg args; + address account; + address pre = delegates(account); + + f(e, args); + + address post = delegates(account); + + assert pre == post, "invalid delegate change"; +} + +// delegates increases the delegatee's votes by the proper amount +// passes + rule sanity +rule delegatee_receives_votes() { + env e; + address delegator; address delegatee; + + require numCheckpoints(delegatee) < 1000000; + require delegates(delegator) != delegatee; + require delegatee != 0x0; + + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 votes_= getVotes(delegatee); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(delegatee); + assert _votes == votes_ + delegator_bal, "delegatee did not receive votes"; +} + +// passes + rule sanity +rule previous_delegatee_votes_removed() { + env e; + address delegator; address delegatee; address third; + + require third != delegatee; + require delegates(delegator) == third; + require numCheckpoints(third) < 1000000; + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 votes_ = getVotes(third); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(third); + + assert third != 0x0 => _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee"; +} + +// passes with rule sanity +rule delegate_contained() { + env e; + address delegator; address delegatee; address other; + + require other != delegatee; + require other != delegates(delegator); + + uint256 votes_ = getVotes(other); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(other); + + assert votes_ == _votes, "votes not contained"; +} + +rule delegate_no_frontrunning(method f) { + env e; calldataarg args; + address delegator; address delegatee; address third; address other; + + + + require numCheckpoints(delegatee) < 1000000; + require numCheckpoints(third) < 1000000; + + + f(e, args); + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 delegatee_votes_ = getVotes(delegatee); + uint256 third_votes_ = getVotes(third); + uint256 other_votes_ = getVotes(other); + require delegates(delegator) == third; + require third != delegatee; + require other != third; + require other != delegatee; + require delegatee != 0x0; + + _delegate(e, delegator, delegatee); + + uint256 _delegatee_votes = getVotes(delegatee); + uint256 _third_votes = getVotes(third); + uint256 _other_votes = getVotes(other); + + + // previous delegatee loses all of their votes + // delegatee gains that many votes + // third loses any votes delegated to them + assert _delegatee_votes == delegatee_votes_ + delegator_bal, "delegatee did not receive votes"; + assert third != 0 => _third_votes == third_votes_ - delegator_bal, "votes not removed from third"; + assert other_votes_ == _other_votes, "delegate not contained"; +} \ No newline at end of file diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index de728ddac..583cb6288 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -17,16 +17,16 @@ methods { queue(address[], uint256[], bytes[], bytes32) returns uint256 // internal functions made public in harness: - _quorumReached(uint256) returns bool - _voteSucceeded(uint256) returns bool envfree + quorumReached(uint256) returns bool + voteSucceeded(uint256) returns bool envfree // function summarization proposalThreshold() returns uint256 envfree getVotes(address, uint256) returns uint256 => DISPATCHER(true) - getPastTotalSupply(uint256 t) returns uint256 => PER_CALLEE_CONSTANT - getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT + getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true) + getPastVotes(address, uint256) returns uint256 => DISPATCHER(true) //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true) //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) @@ -38,7 +38,9 @@ methods { // proposal was created - relation proved in noStartBeforeCreation -definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0; +definition proposalCreated(uint256 pId) returns bool = + proposalSnapshot(pId) > 0 + && proposalDeadline(pId) > 0; ////////////////////////////////////////////////////////////////////////////// @@ -47,7 +49,7 @@ definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0 function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash; - uint8 support; uint8 v; bytes32 r; bytes32 s; + uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params; if (f.selector == propose(address[], uint256[], bytes[], string).selector) { uint256 result = propose@withrevert(e, targets, values, calldatas, reason); require(result == proposalId); @@ -62,7 +64,11 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { castVoteBySig@withrevert(e, proposalId, support, v, r, s); } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) { queue@withrevert(e, targets, values, calldatas, descriptionHash); - } else { + } else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) { + castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s); + } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) { + castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params); + } else { calldataarg args; f@withrevert(e, args); } @@ -152,9 +158,9 @@ invariant noBothExecutedAndCanceled(uint256 pId) */ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){ bool isExecutedBefore = isExecuted(pId); - bool quorumReachedBefore = _quorumReached(e, pId); - bool voteSucceededBefore = _voteSucceeded(pId); - + bool quorumReachedBefore = quorumReached(e, pId); + bool voteSucceededBefore = voteSucceeded(pId); + calldataarg args; f(e, args); @@ -283,6 +289,7 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f -> && f.selector != queue(address[],uint256[],bytes[],bytes32).selector && f.selector != relay(address,uint256,bytes).selector && f.selector != 0xb9a61961 // __acceptAdmin() + && f.selector != setLateQuorumVoteExtension(uint64).selector } { env e; calldataarg args; uint256 pId; @@ -305,6 +312,7 @@ rule allFunctionsRevertIfCanceled(method f) filtered { && f.selector != queue(address[],uint256[],bytes[],bytes32).selector && f.selector != relay(address,uint256,bytes).selector && f.selector != 0xb9a61961 // __acceptAdmin() + && f.selector != setLateQuorumVoteExtension(uint64).selector } { env e; calldataarg args; uint256 pId; diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index 7af73beb6..43f1ba311 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/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 @@ -9,9 +7,6 @@ methods { proposalVotes(uint256) returns (uint256, uint256, uint256) envfree quorumNumerator() returns uint256 - _executor() returns address - - erc20votes._getPastVotes(address, uint256) returns uint256 getExecutor() returns address @@ -188,7 +183,8 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) { bool hasVotedAfter = hasVoted(e, pId, acc); - assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation"; + // want all vote categories to not decrease and at least one category to increase + assert (!hasVotedBefore && hasVotedAfter) => (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), "no correlation: some category decreased"; } diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec new file mode 100644 index 000000000..861e57ae8 --- /dev/null +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -0,0 +1,298 @@ +import "GovernorCountingSimple.spec" + +using ERC721VotesHarness as erc721votes + +methods { + quorumDenominator() returns uint256 envfree + votingPeriod() returns uint256 envfree + lateQuorumVoteExtension() returns uint64 envfree + propose(address[], uint256[], bytes[], string) + + // harness + getExtendedDeadlineIsUnset(uint256) returns bool envfree + getExtendedDeadlineIsStarted(uint256) returns bool envfree + getExtendedDeadline(uint256) returns uint64 envfree + getAgainstVotes(uint256) returns uint256 envfree + getAbstainVotes(uint256) returns uint256 envfree + getForVotes(uint256) returns uint256 envfree + + // more robust check than f.selector == _castVote(...).selector + latestCastVoteCall() returns uint256 envfree + + // timelock dispatch + getMinDelay() returns uint256 => DISPATCHER(true) + + hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) + executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => CONSTANT + scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT +} + + +////////////////////////////////////////////////////////////////////////////// +///////////////////////////// Helper Functions /////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env e) { + string reason; uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params; + if (f.selector == castVote(uint256, uint8).selector) { + castVote@withrevert(e, proposalId, support); + } else if (f.selector == castVoteWithReason(uint256, uint8, string).selector) { + castVoteWithReason@withrevert(e, proposalId, support, reason); + } else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) { + castVoteBySig@withrevert(e, proposalId, support, v, r, s); + } else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) { + castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s); + } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) { + castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params); + } else { + calldataarg args; + f@withrevert(e, args); + } +} + + +////////////////////////////////////////////////////////////////////////////// +//////////////////////////////// Definitions ///////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +// proposal deadline can be extended (but isn't) +definition deadlineExtendable(env e, uint256 pId) returns bool = + getExtendedDeadlineIsUnset(pId) // deadline == 0 + && !quorumReached(e, pId); + +// proposal deadline has been extended +definition deadlineExtended(env e, uint256 pId) returns bool = + getExtendedDeadlineIsStarted(pId) // deadline > 0 + && quorumReached(e, pId); + +definition proposalNotCreated(env e, uint256 pId) returns bool = + proposalSnapshot(pId) == 0 + && proposalDeadline(pId) == 0 + && getExtendedDeadlineIsUnset(pId) + && getAgainstVotes(pId) == 0 + && getAbstainVotes(pId) == 0 + && getForVotes(pId) == 0 + && !quorumReached(e, pId); + + +////////////////////////////////////////////////////////////////////////////// +///////////////////////////////// Invariants ///////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +/* + * I1: If a proposal has reached quorum then the proposal snapshot (start block.number) must be non-zero + * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true) + * ADVANCED SANITY NOT RAN + */ +invariant quorumReachedEffect(env e, uint256 pId) + quorumReached(e, pId) => proposalCreated(pId) // bug: 0 supply 0 votes => quorumReached + // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function + +/* + * I2: A non-existant proposal must meet the definition of one. + * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true) + * ADVANCED SANITY NOT RAN + */ +invariant proposalNotCreatedEffects(env e, uint256 pId) + !proposalCreated(pId) => proposalNotCreated(e, pId) + // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function + +/* + * I3: A created propsal must be in state deadlineExtendable or deadlineExtended. + * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true) + * ADVANCED SANITY NOT RAN + */ +invariant proposalInOneState(env e, uint256 pId) + proposalNotCreated(e, pId) || deadlineExtendable(e, pId) || deadlineExtended(e, pId) + // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function + { preserved { requireInvariant proposalNotCreatedEffects(e, pId); }} + + +////////////////////////////////////////////////////////////////////////////// +////////////////////////////////// Rules ///////////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +///////////////////////////// first set of rules ///////////////////////////// + +// R1 and R2 are assumed in R3, so we prove them first +/* + * R1: If deadline increases then we are in deadlineExtended state and castVote was called. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule deadlineChangeEffects(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + + requireInvariant quorumReachedEffect(e, pId); + + uint256 deadlineBefore = proposalDeadline(pId); + f(e, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId)); +} + + +/* + * R2: A proposal can't leave deadlineExtended state. + * RULE PASSING* + * ADVANCED SANITY PASSING + */ +rule deadlineCantBeUnextended(method f) + filtered { + f -> !f.isView + // && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function + } { + env e; calldataarg args; uint256 pId; + + require(deadlineExtended(e, pId)); + requireInvariant quorumReachedEffect(e, pId); + + f(e, args); + + assert(deadlineExtended(e, pId)); +} + + +/* + * R3: A proposal's deadline can't change in deadlineExtended state. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + + require(deadlineExtended(e, pId)); + requireInvariant quorumReachedEffect(e, pId); + + uint256 deadlineBefore = proposalDeadline(pId); + f(e, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); +} + + +//////////////////////////// second set of rules //////////////////////////// + +// HIGH LEVEL RULE R6: deadline can only extended if quorum reached w/ <= timeOfExtension left to vote +// I3, R4 and R5 are assumed in R6 so we prove them first + +/* + * R4: A change in hasVoted must be correlated with an increasing of the vote supports, i.e. casting a vote increases the total number of votes. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isView} { + address acc = e.msg.sender; + + require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power + + uint256 againstBefore = votesAgainst(); + uint256 forBefore = votesFor(); + uint256 abstainBefore = votesAbstain(); + + bool hasVotedBefore = hasVoted(e, pId, acc); + + helperFunctionsWithRevertOnlyCastVote(pId, f, e); // should be f(e, args) + + uint256 againstAfter = votesAgainst(); + uint256 forAfter = votesFor(); + uint256 abstainAfter = votesAbstain(); + + bool hasVotedAfter = hasVoted(e, pId, acc); + + // want all vote categories to not decrease and at least one category to increase + assert + (!hasVotedBefore && hasVotedAfter) => + (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), + "after a vote is cast, the number of votes for each category must not decrease"; // currently vacous but keeping for CI tests + assert + (!hasVotedBefore && hasVotedAfter) => + (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter), + "after a vote is cast, the number of votes of at least one category must increase"; +} + + +/* + * R5: An against vote does not make a proposal reach quorum. + * RULE PASSING + * --ADVANCED SANITY PASSING vacuous but keeping + */ +rule againstVotesDontCount(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + address acc = e.msg.sender; + + bool quorumBefore = quorumReached(e, pId); + uint256 againstBefore = votesAgainst(); + + f(e, args); + + bool quorumAfter = quorumReached(e, pId); + uint256 againstAfter = votesAgainst(); + + assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum must not be reached with an against vote"; +} + +/* + * R6: Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + + requireInvariant proposalInOneState(e, pId); + requireInvariant quorumReachedEffect(e, pId); + requireInvariant proposalNotCreatedEffects(e, pId); + + bool wasDeadlineExtendable = deadlineExtendable(e, pId); + uint64 extension = lateQuorumVoteExtension(); + uint256 deadlineBefore = proposalDeadline(pId); + f(e, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline must have been extendable for the deadline to be extended"; + assert deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used"; +} + +/* + * R7: `extendedDeadlineField` is set iff `_castVote` is called and quroum is reached. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + + requireInvariant proposalInOneState(e, pId); + + bool extendedBefore = deadlineExtended(e, pId); + f(e, args); + bool extendedAfter = deadlineExtended(e, pId); + uint256 extDeadline = getExtendedDeadline(pId); + + assert( + !extendedBefore && extendedAfter + => extDeadline == e.block.number + lateQuorumVoteExtension(), + "extended deadline was not set" + ); +} + +/* + * R8: Deadline can never be reduced. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule deadlineNeverReduced(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + + requireInvariant quorumReachedEffect(e, pId); + requireInvariant proposalNotCreatedEffects(e, pId); + + uint256 deadlineBefore = proposalDeadline(pId); + f(e, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert(deadlineAfter >= deadlineBefore); +} + diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec new file mode 100644 index 000000000..0adbad08c --- /dev/null +++ b/certora/specs/Initializable.spec @@ -0,0 +1,159 @@ +methods { + initialize(uint256, uint256, uint256) envfree + reinitialize(uint256, uint256, uint256, uint8) envfree + initialized() returns uint8 envfree + initializing() returns bool envfree + thisIsContract() returns bool envfree + + returnsV1() returns uint256 envfree + returnsVN(uint8) returns uint256 envfree + returnsAV1() returns uint256 envfree + returnsAVN(uint8) returns uint256 envfree + returnsBV1() returns uint256 envfree + returnsBVN(uint8) returns uint256 envfree + a() returns uint256 envfree + b() returns uint256 envfree + val() returns uint256 envfree +} + + +////////////////////////////////////////////////////////////////////////////// +//////////////////////////////// Definitions ///////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +definition isUninitialized() returns bool = initialized() == 0; + +definition isInitialized() returns bool = initialized() > 0; + +definition isInitializedOnce() returns bool = initialized() == 1; + +definition isReinitialized() returns bool = initialized() > 1; + +definition isDisabled() returns bool = initialized() == 255; + + +////////////////////////////////////////////////////////////////////////////// +///////////////////////////////// Invariants ///////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +/// @description A contract must only ever be in an initializing state while in the middle of a transaction execution. +invariant notInitializing() + !initializing() + + +////////////////////////////////////////////////////////////////////////////// +////////////////////////////////// Rules ///////////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +/// @description An initializeable contract with a function that inherits the initializer modifier must be initializable only once" +rule initOnce() { + uint256 val; uint256 a; uint256 b; + + require isInitialized(); + initialize@withrevert(val, a, b); + assert lastReverted, "contract must only be initialized once"; +} + +/// @description Successfully calling reinitialize() with a version value of 1 must result in _initialized being set to 1. +rule reinitializeEffects { + uint256 val; uint256 a; uint256 b; + + reinitialize(val, a, b, 1); + + assert isInitializedOnce(), "reinitialize(1) must set _initialized to 1"; +} + +/// @description Successfully calling initalize() must result in _initialized being set to 1. +/// @note We assume initialize() and reinitialize(1) are equivalent if this rule and the above rule, reinitalizeEffects, both pass. +rule initalizeEffects { + uint256 val; uint256 a; uint256 b; + + initialize(val, a, b); + + assert isInitializedOnce(), "initialize() must set _initialized to 1"; +} + +/// @description A disabled initializable contract must always stay disabled. +rule disabledStaysDisabled(method f) { + env e; calldataarg args; + + bool disabledBefore = isDisabled(); + f(e, args); + bool disabledAfter = isDisabled(); + + assert disabledBefore => disabledAfter, "a disabled initializer must stay disabled"; +} + +/// @description The variable _initialized must not decrease. +rule increasingInitialized(method f) { + env e; calldataarg args; + + uint8 initBefore = initialized(); + f(e, args); + uint8 initAfter = initialized(); + assert initBefore <= initAfter, "_initialized must only increase"; +} + +/// @description If reinitialize(...) was called successfuly, then the variable _initialized must increases. +rule reinitializeIncreasesInit { + uint256 val; uint8 n; uint256 a; uint256 b; + + uint8 initBefore = initialized(); + reinitialize(val, a, b, n); + uint8 initAfter = initialized(); + + assert initAfter > initBefore, "calling reinitialize must increase _initialized"; +} + +/// @description Reinitialize(n) must be callable if the contract is not in an _initializing state and n is greater than _initialized and less than 255 +rule reinitializeLiveness { + uint256 val; uint8 n; uint256 a; uint256 b; + + requireInvariant notInitializing(); + uint8 initVal = initialized(); + reinitialize@withrevert(val, a, b, n); + + assert n > initVal => !lastReverted, "reinitialize(n) call must succeed if n was greater than _initialized"; +} + +/// @description If reinitialize(n) was called successfully then n was greater than _initialized. +rule reinitializeRule { + uint256 val; uint8 n; uint256 a; uint256 b; + + uint8 initBefore = initialized(); + reinitialize(val, a, b, n); + + assert n > initBefore; +} + +/// @description Functions implemented in the parent contract that require _initialized to be a certain value are only callable when it is that value. +rule reinitVersionCheckParent { + uint8 n; + + returnsVN(n); + assert initialized() == n, "parent contract's version n functions must only be callable in version n"; +} + +/// @description Functions implemented in the child contract that require _initialized to be a certain value are only callable when it is that value. +rule reinitVersionCheckChild { + uint8 n; + + returnsAVN(n); + assert initialized() == n, "child contract's version n functions must only be callable in version n"; +} + +/// @description Functions implemented in the grandchild contract that require _initialized to be a certain value are only callable when it is that value. +rule reinitVersionCheckGrandchild { + uint8 n; + + returnsBVN(n); + assert initialized() == n, "gransdchild contract's version n functions must only be callable in version n"; +} + +// @description Calling parent initalizer function must initialize all child contracts. +rule inheritanceCheck { + uint256 val; uint8 n; uint256 a; uint256 b; + + reinitialize(val, a, b, n); + assert val() == val && a() == a && b() == b, "all child contract values must be initialized"; +} diff --git a/certora/specs/RulesInProgress.spec b/certora/specs/RulesInProgress.spec index cbad3336e..18a79d619 100644 --- a/certora/specs/RulesInProgress.spec +++ b/certora/specs/RulesInProgress.spec @@ -136,4 +136,41 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) { uint256 ps = proposalSnapshot(pId); assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla"; -} \ No newline at end of file +} + + + +/////////////////// 2nd iteration with OZ ////////////////////////// + +function executionsCall(method f, env e, address target, uint256 value, bytes data, + bytes32 predecessor, bytes32 salt, uint256 delay, + address[] targets, uint256[] values, bytes[] datas) { + if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) { + execute(e, target, value, data, predecessor, salt); + } else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) { + executeBatch(e, targets, values, datas, predecessor, salt); + } else { + calldataarg args; + f(e, args); + } +} + +// STATUS - in progress +// execute() is the only way to set timestamp to 1 +rule getTimestampOnlyChange(method f, env e){ + bytes32 id; + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay; + address[] targets; uint256[] values; bytes[] datas; + + require (targets[0] == target && values[0] == value && datas[0] == data) + || (targets[1] == target && values[1] == value && datas[1] == data) + || (targets[2] == target && values[2] == value && datas[2] == data); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas); + + assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?"; +} + diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec new file mode 100644 index 000000000..9d5df6b97 --- /dev/null +++ b/certora/specs/TimelockController.spec @@ -0,0 +1,323 @@ +methods { + getTimestamp(bytes32) returns(uint256) envfree + _DONE_TIMESTAMP() returns(uint256) envfree + PROPOSER_ROLE() returns(bytes32) envfree + _minDelay() returns(uint256) envfree + getMinDelay() returns(uint256) envfree + hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree + isOperation(bytes32) returns(bool) envfree + isOperationPending(bytes32) returns(bool) envfree + isOperationDone(bytes32) returns(bool) envfree + + isOperationReady(bytes32) returns(bool) + cancel(bytes32) + schedule(address, uint256, bytes32, bytes32, bytes32, uint256) + execute(address, uint256, bytes, bytes32, bytes32) + executeBatch(address[], uint256[], bytes[], bytes32, bytes32) + _checkRole(bytes32) => DISPATCHER(true) +} + + + +//////////////////////////////////////////////////////////////////////////// +// Functions // +//////////////////////////////////////////////////////////////////////////// + + +function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){ + require data.length < 32; + require hashOperation(target, value, data, predecessor, salt) == id; +} + + + +//////////////////////////////////////////////////////////////////////////// +// Invariants // +//////////////////////////////////////////////////////////////////////////// + + +// STATUS - verified +// `isOperation()` correctness check +invariant operationCheck(bytes32 id) + getTimestamp(id) > 0 <=> isOperation(id) +filtered { f -> !f.isView } + +// STATUS - verified +// `isOperationPending()` correctness check +invariant pendingCheck(bytes32 id) + getTimestamp(id) > _DONE_TIMESTAMP() <=> isOperationPending(id) +filtered { f -> !f.isView } + +// STATUS - verified +// `isOperationReady()` correctness check +invariant readyCheck(env e, bytes32 id) + (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id) +filtered { f -> !f.isView } + +// STATUS - verified +// `isOperationDone()` correctness check +invariant doneCheck(bytes32 id) + getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id) +filtered { f -> !f.isView } + + +//////////////////////////////////////////////////////////////////////////// +// Rules // +//////////////////////////////////////////////////////////////////////////// + + +///////////////////////////////////////////////////////////// +// STATE TRANSITIONS +///////////////////////////////////////////////////////////// + + +// STATUS - verified +// Possible transitions: form `!isOperation()` to `!isOperation()` or `isOperationPending()` only +rule unsetPendingTransitionGeneral(method f, env e){ + bytes32 id; + + require !isOperation(id); + require e.block.timestamp > 1; + + calldataarg args; + f(e, args); + + assert isOperationPending(id) || !isOperation(id); +} + + +// STATUS - verified +// Possible transitions: form `!isOperation()` to `isOperationPending()` via `schedule()` and `scheduleBatch()` only +rule unsetPendingTransitionMethods(method f, env e){ + bytes32 id; + + require !isOperation(id); + + calldataarg args; + f(e, args); + + assert isOperationPending(id) => (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector + || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector), "Why do we need to follow the schedule?"; +} + + +// STATUS - verified +// Possible transitions: form `ready()` to `isOperationDone()` via `execute()` and `executeBatch()` only +rule readyDoneTransition(method f, env e){ + bytes32 id; + + require isOperationReady(e, id); + + calldataarg args; + f(e, args); + + assert isOperationDone(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not isOperationDone yet!"; +} + + +// STATUS - verified +// isOperationPending() -> cancelled() via cancel() only +rule pendingCancelledTransition(method f, env e){ + bytes32 id; + + require isOperationPending(id); + + calldataarg args; + f(e, args); + + assert !isOperation(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?"; +} + + +// STATUS - verified +// isOperationDone() -> nowhere +rule doneToNothingTransition(method f, env e){ + bytes32 id; + + require isOperationDone(id); + + calldataarg args; + f(e, args); + + assert isOperationDone(id), "Did you find a way to escape? There is no way! HA-HA-HA"; +} + + + +///////////////////////////////////////////////////////////// +// THE REST +///////////////////////////////////////////////////////////// + + +// STATUS - verified +// only TimelockController contract can change minDelay +rule minDelayOnlyChange(method f, env e){ + uint256 delayBefore = _minDelay(); + + calldataarg args; + f(e, args); + + uint256 delayAfter = _minDelay(); + + assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!"; +} + + +// STATUS - verified +// scheduled operation timestamp == block.timestamp + delay (kind of unit test) +rule scheduleCheck(method f, env e){ + bytes32 id; + + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls"; +} + + +// STATUS - verified +// Cannot call `execute()` on a isOperationPending (not ready) operation +rule cannotCallExecute(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require isOperationPending(id) && !isOperationReady(e, id); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - verified +// Cannot call `execute()` on a !isOperation operation +rule executeRevertsFromUnset(method f, env e, env e2){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require !isOperation(id); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - verified +// Execute reverts => state returns to isOperationPending +rule executeRevertsEffectCheck(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require isOperationPending(id) && !isOperationReady(e, id); + + execute@withrevert(e, target, value, data, predecessor, salt); + bool reverted = lastReverted; + + assert lastReverted => isOperationPending(id) && !isOperationReady(e, id), "you go against execution nature"; +} + + +// STATUS - verified +// Canceled operations cannot be executed → can’t move from canceled to isOperationDone +rule cancelledNotExecuted(method f, env e){ + bytes32 id; + + require !isOperation(id); + require e.block.timestamp > 1; + + calldataarg args; + f(e, args); + + assert !isOperationDone(id), "The ship is not a creature of the air"; +} + + +// STATUS - verified +// Only proposers can schedule +rule onlyProposer(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector + || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector } { + bytes32 id; + bytes32 role; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + _checkRole@withrevert(e, PROPOSER_ROLE()); + + bool isCheckRoleReverted = lastReverted; + + calldataarg args; + f@withrevert(e, args); + + bool isScheduleReverted = lastReverted; + + assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected"; +} + + +// STATUS - verified +// if `ready` then has waited minimum period after isOperationPending() +rule cooldown(method f, env e, env e2){ + bytes32 id; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + uint256 minDelay = getMinDelay(); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + calldataarg args; + f(e, args); + + assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready"; +} + + +// STATUS - verified +// `schedule()` should change only one id's timestamp +rule scheduleChange(env e){ + bytes32 id; bytes32 otherId; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + uint256 otherIdTimestampBefore = getTimestamp(otherId); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings"; +} + + +// STATUS - verified +// `execute()` should change only one id's timestamp +rule executeChange(env e){ + bytes32 id; bytes32 otherId; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; + uint256 otherIdTimestampBefore = getTimestamp(otherId); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + execute(e, target, value, data, predecessor, salt); + + assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings"; +} + + +// STATUS - verified +// `cancel()` should change only one id's timestamp +rule cancelChange(env e){ + bytes32 id; bytes32 otherId; + + uint256 otherIdTimestampBefore = getTimestamp(otherId); + + cancel(e, id); + + assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings"; +} diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec new file mode 100644 index 000000000..b12fec167 --- /dev/null +++ b/certora/specs/erc20.spec @@ -0,0 +1,12 @@ +// erc20 methods +methods { + name() returns (string) => DISPATCHER(true) + symbol() returns (string) => DISPATCHER(true) + decimals() returns (string) => DISPATCHER(true) + totalSupply() returns (uint256) => DISPATCHER(true) + balanceOf(address) returns (uint256) => DISPATCHER(true) + allowance(address,address) returns (uint) => DISPATCHER(true) + approve(address,uint256) returns (bool) => DISPATCHER(true) + transfer(address,uint256) returns (bool) => DISPATCHER(true) + transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) +} diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec index e08f68845..bd184841a 100644 --- a/certora/specs/sanity.spec +++ b/certora/specs/sanity.spec @@ -5,7 +5,8 @@ How it works: - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails. - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously. */ - + + rule sanity(method f) { env e; calldataarg arg; diff --git a/requirements.txt b/requirements.txt new file mode 100644 index 000000000..3373e34c4 --- /dev/null +++ b/requirements.txt @@ -0,0 +1 @@ +certora-cli==3.0.0 diff --git a/resource_errors.json b/resource_errors.json new file mode 100644 index 000000000..d9bd79235 --- /dev/null +++ b/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file