diff --git a/audit/2020-10-certora.pdf b/audit/2020-10-certora.pdf new file mode 100644 index 000000000..ac5994391 Binary files /dev/null and b/audit/2020-10-certora.pdf differ diff --git a/certora/Makefile b/certora/Makefile index 6ef6b2bf6..06e8318dc 100644 --- a/certora/Makefile +++ b/certora/Makefile @@ -16,7 +16,9 @@ munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) patch -p0 -d $@ < $(PATCH) record: - diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH) + diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH) + +refresh: munged record clean: git clean -fdX diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index a0d61ef51..166366b8b 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,6 +1,6 @@ -diff -ruN access/AccessControl.sol access/AccessControl.sol ---- access/AccessControl.sol 2022-09-27 10:26:58.548890299 +0200 -+++ access/AccessControl.sol 2022-09-27 17:51:32.011301116 +0200 +diff -druN access/AccessControl.sol access/AccessControl.sol +--- access/AccessControl.sol 2022-10-31 11:08:30.540461238 +0100 ++++ access/AccessControl.sol 2022-11-04 16:35:52.557358427 +0100 @@ -93,7 +93,7 @@ * * _Available since v4.6._ @@ -9,68 +9,82 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol + function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public _checkRole(role, _msgSender()); } - -diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol ---- governance/extensions/GovernorCountingSimple.sol 2022-09-27 10:26:58.548890299 +0200 -+++ governance/extensions/GovernorCountingSimple.sol 2022-09-27 17:51:32.011301116 +0200 + +diff -druN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol +--- governance/extensions/GovernorCountingSimple.sol 2022-10-31 11:08:30.540461238 +0100 ++++ governance/extensions/GovernorCountingSimple.sol 2022-11-04 16:35:52.557358427 +0100 @@ -27,7 +27,7 @@ mapping(address => bool) hasVoted; } - + - mapping(uint256 => ProposalVote) private _proposalVotes; + mapping(uint256 => ProposalVote) internal _proposalVotes; // HARNESS: private -> internal - + /** * @dev See {IGovernor-COUNTING_MODE}. -diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol +diff -druN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol --- governance/extensions/GovernorPreventLateQuorum.sol 2022-08-31 13:44:36.377724869 +0200 -+++ governance/extensions/GovernorPreventLateQuorum.sol 2022-09-27 17:51:32.011301116 +0200 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2022-11-04 16:35:52.557358427 +0100 @@ -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; // HARNESS: private -> internal + mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines; // HARNESS: private -> internal - + /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period. event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline); -diff -ruN governance/Governor.sol governance/Governor.sol ---- governance/Governor.sol 2022-09-29 10:07:27.126075551 +0200 -+++ governance/Governor.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN governance/extensions/GovernorVotesQuorumFraction.sol governance/extensions/GovernorVotesQuorumFraction.sol +--- governance/extensions/GovernorVotesQuorumFraction.sol 2022-10-31 11:08:30.540461238 +0100 ++++ governance/extensions/GovernorVotesQuorumFraction.sol 2022-11-04 16:35:52.557358427 +0100 +@@ -16,8 +16,8 @@ + abstract contract GovernorVotesQuorumFraction is GovernorVotes { + using Checkpoints for Checkpoints.History; + +- uint256 private _quorumNumerator; // DEPRECATED +- Checkpoints.History private _quorumNumeratorHistory; ++ uint256 internal _quorumNumerator; // DEPRECATED // MUNGED private => internal ++ Checkpoints.History internal _quorumNumeratorHistory; // MUNGED private => internal + + event QuorumNumeratorUpdated(uint256 oldQuorumNumerator, uint256 newQuorumNumerator); + +diff -druN governance/Governor.sol governance/Governor.sol +--- governance/Governor.sol 2022-11-04 16:13:34.398935222 +0100 ++++ governance/Governor.sol 2022-11-04 16:35:52.560691845 +0100 @@ -44,7 +44,7 @@ - + string private _name; - + - mapping(uint256 => ProposalCore) private _proposals; + mapping(uint256 => ProposalCore) internal _proposals; // HARNESS: private -> internal - + // This queue keeps track of the governor operating on itself. Calls to functions protected by the // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute}, -diff -ruN governance/TimelockController.sol governance/TimelockController.sol ---- governance/TimelockController.sol 2022-09-29 10:07:27.126075551 +0200 -+++ governance/TimelockController.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN governance/TimelockController.sol governance/TimelockController.sol +--- governance/TimelockController.sol 2022-11-03 12:06:09.356515929 +0100 ++++ governance/TimelockController.sol 2022-11-04 16:35:52.560691845 +0100 @@ -28,10 +28,10 @@ bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE"); bytes32 public constant CANCELLER_ROLE = keccak256("CANCELLER_ROLE"); - uint256 internal constant _DONE_TIMESTAMP = uint256(1); + uint256 public constant _DONE_TIMESTAMP = uint256(1); // HARNESS: internal -> public - + mapping(bytes32 => uint256) private _timestamps; - uint256 private _minDelay; + uint256 public _minDelay; // HARNESS: private -> public - + /** * @dev Emitted when a call is scheduled as part of operation `id`. -diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol ---- governance/utils/Votes.sol 2022-09-27 10:26:58.548890299 +0200 -+++ governance/utils/Votes.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN governance/utils/Votes.sol governance/utils/Votes.sol +--- governance/utils/Votes.sol 2022-11-03 12:06:09.356515929 +0100 ++++ governance/utils/Votes.sol 2022-11-04 16:35:52.560691845 +0100 @@ -35,7 +35,25 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); - + - mapping(address => address) private _delegation; + // HARNESS : Hooks cannot access any information from Checkpoints yet, so I am also updating votes and fromBlock in this struct + struct Ckpt { @@ -93,7 +107,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol + mapping(address => address) public _delegation; // HARNESS: private -> public mapping(address => Checkpoints.History) private _delegateCheckpoints; Checkpoints.History private _totalCheckpoints; - + @@ -124,7 +142,7 @@ * * Emits events {DelegateChanged} and {DelegateVotesChanged}. @@ -102,7 +116,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol + function _delegate(address account, address delegatee) public virtual { // HARNESS: internal -> public address oldDelegate = delegates(account); _delegation[account] = delegatee; - + @@ -142,10 +160,10 @@ uint256 amount ) internal virtual { @@ -139,21 +153,21 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol - function _getVotingUnits(address) internal view virtual returns (uint256); + function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public } -diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol ---- mocks/SafeERC20Helper.sol 2022-09-26 19:10:21.166619395 +0200 -+++ mocks/SafeERC20Helper.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol +--- mocks/SafeERC20Helper.sol 2022-11-02 19:02:32.463724228 +0100 ++++ mocks/SafeERC20Helper.sol 2022-11-04 16:35:52.560691845 +0100 @@ -4,7 +4,6 @@ - + import "../utils/Context.sol"; import "../token/ERC20/IERC20.sol"; -import "../token/ERC20/extensions/draft-ERC20Permit.sol"; import "../token/ERC20/utils/SafeERC20.sol"; - + contract ERC20ReturnFalseMock is Context { @@ -106,42 +105,43 @@ } } - + -contract ERC20PermitNoRevertMock is - ERC20("ERC20PermitNoRevertMock", "ERC20PermitNoRevertMock"), - ERC20Permit("ERC20PermitNoRevertMock") @@ -161,7 +175,15 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol - function getChainId() external view returns (uint256) { - return block.chainid; - } -- ++// Harness remove ? ++// contract ERC20PermitNoRevertMock is ++// ERC20("ERC20PermitNoRevertMock", "ERC20PermitNoRevertMock"), ++// ERC20Permit("ERC20PermitNoRevertMock") ++// { ++// function getChainId() external view returns (uint256) { ++// return block.chainid; ++// } + - function permitThatMayRevert( - address owner, - address spender, @@ -173,7 +195,18 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol - ) public { - super.permit(owner, spender, value, deadline, v, r, s); - } -- ++// function permitThatMayRevert( ++// address owner, ++// address spender, ++// uint256 value, ++// uint256 deadline, ++// uint8 v, ++// bytes32 r, ++// bytes32 s ++// ) public { ++// super.permit(owner, spender, value, deadline, v, r, s); ++// } + - function permit( - address owner, - address spender, @@ -190,27 +223,6 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol - } - } -} -+// Harness remove ? -+// 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 { -+// super.permit(owner, spender, value, deadline, v, r, s); -+// } -+ +// function permit( +// address owner, +// address spender, @@ -227,37 +239,37 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol +// } +// } +// } - + contract SafeERC20Wrapper is Context { using SafeERC20 for IERC20; -diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol ---- proxy/utils/Initializable.sol 2022-09-29 10:07:27.126075551 +0200 -+++ proxy/utils/Initializable.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN proxy/utils/Initializable.sol proxy/utils/Initializable.sol +--- proxy/utils/Initializable.sol 2022-11-03 12:06:09.356515929 +0100 ++++ proxy/utils/Initializable.sol 2022-11-04 16:35:52.560691845 +0100 @@ -59,12 +59,12 @@ * @dev Indicates that the contract has been initialized. * @custom:oz-retyped-from bool */ - uint8 private _initialized; + uint8 internal _initialized; // HARNESS: private -> internal - + /** * @dev Indicates that the contract is in the process of being initialized. */ - bool private _initializing; + bool internal _initializing; // HARNESS: private -> internal - + /** * @dev Triggered when the contract has been initialized or reinitialized. -diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol ---- token/ERC1155/ERC1155.sol 2022-09-27 10:26:58.548890299 +0200 -+++ token/ERC1155/ERC1155.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol +--- token/ERC1155/ERC1155.sol 2022-10-31 11:08:30.547127922 +0100 ++++ token/ERC1155/ERC1155.sol 2022-11-04 16:35:52.560691845 +0100 @@ -21,7 +21,7 @@ using Address for address; - + // Mapping from token ID to account balances - mapping(uint256 => mapping(address => uint256)) private _balances; + mapping(uint256 => mapping(address => uint256)) internal _balances; // HARNESS: private -> internal - + // Mapping from account to operator approvals mapping(address => mapping(address => bool)) private _operatorApprovals; @@ -471,7 +471,7 @@ @@ -278,9 +290,9 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol 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-09-27 10:26:58.548890299 +0200 -+++ token/ERC20/ERC20.sol 2022-09-29 10:09:07.479688477 +0200 +diff -druN token/ERC20/ERC20.sol token/ERC20/ERC20.sol +--- token/ERC20/ERC20.sol 2022-10-31 11:08:30.547127922 +0100 ++++ token/ERC20/ERC20.sol 2022-11-04 16:35:52.560691845 +0100 @@ -256,7 +256,7 @@ * * - `account` cannot be the zero address. @@ -288,7 +300,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol - function _mint(address account, uint256 amount) internal virtual { + function _mint(address account, uint256 amount) public virtual { // HARNESS: internal -> public require(account != address(0), "ERC20: mint to the zero address"); - + _beforeTokenTransfer(address(0), account, amount); @@ -282,7 +282,7 @@ * - `account` cannot be the zero address. @@ -297,11 +309,11 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol - function _burn(address account, uint256 amount) internal virtual { + function _burn(address account, uint256 amount) public virtual { // HARNESS: internal -> public require(account != address(0), "ERC20: burn from the zero address"); - + _beforeTokenTransfer(account, address(0), amount); -diff -ruN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Capped.sol +diff -druN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Capped.sol --- token/ERC20/extensions/ERC20Capped.sol 2022-08-31 13:44:36.381058287 +0200 -+++ token/ERC20/extensions/ERC20Capped.sol 2022-09-29 10:09:41.376517581 +0200 ++++ token/ERC20/extensions/ERC20Capped.sol 2022-11-04 16:35:52.560691845 +0100 @@ -30,7 +30,7 @@ /** * @dev See {ERC20-_mint}. @@ -311,9 +323,9 @@ diff -ruN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Cap require(ERC20.totalSupply() + amount <= cap(), "ERC20Capped: cap exceeded"); super._mint(account, amount); } -diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol ---- token/ERC20/extensions/ERC20FlashMint.sol 2022-09-29 10:07:27.126075551 +0200 -+++ token/ERC20/extensions/ERC20FlashMint.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol +--- token/ERC20/extensions/ERC20FlashMint.sol 2022-11-03 12:06:09.356515929 +0100 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2022-11-04 16:35:52.560691845 +0100 @@ -51,9 +51,11 @@ // silence warning about unused variable without the addition of bytecode. token; @@ -321,25 +333,25 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 - return 0; + return fee; // HARNESS: made "return" nonzero } - + + uint256 public fee; // HARNESS: added it to simulate random fee amount + /** * @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/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol ---- token/ERC20/extensions/ERC20Votes.sol 2022-09-27 10:26:58.548890299 +0200 -+++ token/ERC20/extensions/ERC20Votes.sol 2022-09-29 10:09:45.489874234 +0200 +diff -druN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol +--- token/ERC20/extensions/ERC20Votes.sol 2022-11-03 12:06:09.356515929 +0100 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-11-04 16:35:52.560691845 +0100 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); - + - mapping(address => address) private _delegates; - mapping(address => Checkpoint[]) private _checkpoints; + mapping(address => address) public _delegates; // HARNESS: private -> public + mapping(address => Checkpoint[]) public _checkpoints; // HARNESS: private -> public Checkpoint[] private _totalSupplyCheckpoints; - + /** @@ -165,27 +165,27 @@ /** @@ -349,7 +361,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + function _maxSupply() public view virtual returns (uint224) { // HARNESS: internal -> public return type(uint224).max; } - + /** * @dev Snapshots the totalSupply after it has been increased. */ @@ -357,22 +369,22 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public super._mint(account, amount); require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes"); - + - _writeCheckpoint(_totalSupplyCheckpoints, _add, amount); + _writeCheckpointAdd(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer } - + /** * @dev Snapshots the totalSupply after it has been decreased. */ - function _burn(address account, uint256 amount) internal virtual override { + function _burn(address account, uint256 amount) public virtual override { // HARNESS: internal -> public (to comply with the ERC20 harness) super._burn(account, amount); - + - _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount); + _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer } - + /** @@ -208,7 +208,7 @@ * @@ -383,7 +395,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote address currentDelegate = delegates(delegator); uint256 delegatorBalance = balanceOf(delegator); _delegates[delegator] = delegatee; -@@ -225,12 +225,13 @@ +@@ -225,36 +225,86 @@ ) private { if (src != dst && amount > 0) { if (src != address(0)) { @@ -392,33 +404,55 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + emit DelegateVotesChanged(src, oldWeight, newWeight); } - + if (dst != address(0)) { - (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount); + (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount); // HARNESS: new version without pointer emit DelegateVotesChanged(dst, oldWeight, newWeight); } } -@@ -255,6 +256,55 @@ - } } - + +- function _writeCheckpoint( ++ // function _writeCheckpoint( ++ // Checkpoint[] storage ckpts, ++ // function(uint256, uint256) view returns (uint256) op, ++ // uint256 delta ++ // ) private returns (uint256 oldWeight, uint256 newWeight) { ++ // uint256 pos = ckpts.length; ++ ++ // Checkpoint memory oldCkpt = pos == 0 ? Checkpoint(0, 0) : _unsafeAccess(ckpts, pos - 1); ++ ++ // oldWeight = oldCkpt.votes; ++ // newWeight = op(oldWeight, delta); ++ ++ // if (pos > 0 && oldCkpt.fromBlock == block.number) { ++ // _unsafeAccess(ckpts, pos - 1).votes = SafeCast.toUint224(newWeight); ++ // } else { ++ // ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)})); ++ // } ++ // } ++ + // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool + function _writeCheckpointAdd( -+ Checkpoint[] storage ckpts, -+ uint256 delta -+ ) private returns (uint256 oldWeight, uint256 newWeight) { -+ uint256 pos = ckpts.length; + 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 = _add(oldWeight, delta); -+ + +- Checkpoint memory oldCkpt = pos == 0 ? Checkpoint(0, 0) : _unsafeAccess(ckpts, pos - 1); + 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)})); + } + } -+ + +- oldWeight = oldCkpt.votes; +- newWeight = op(oldWeight, delta); + function _writeCheckpointSub( + Checkpoint[] storage ckpts, + uint256 delta @@ -426,14 +460,16 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + uint256 pos = ckpts.length; + oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes; + newWeight = _subtract(oldWeight, delta); -+ + +- if (pos > 0 && oldCkpt.fromBlock == block.number) { +- _unsafeAccess(ckpts, pos - 1).votes = SafeCast.toUint224(newWeight); + 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)})); -+ } -+ } -+ + } else { + ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)})); + } + } + + // backup of original function + // + // function _writeCheckpoint( @@ -455,9 +491,9 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote 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 +diff -druN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol --- token/ERC20/extensions/ERC20Wrapper.sol 2022-08-31 13:44:36.381058287 +0200 -+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-09-28 11:25:39.319711517 +0200 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-11-04 16:35:52.560691845 +0100 @@ -55,7 +55,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. @@ -467,9 +503,9 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr uint256 value = underlying.balanceOf(address(this)) - totalSupply(); _mint(account, value); return value; -diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol ---- token/ERC721/extensions/draft-ERC721Votes.sol 2022-09-29 10:07:27.126075551 +0200 -+++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-09-27 17:51:32.014634743 +0200 +diff -druN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol +--- token/ERC721/extensions/draft-ERC721Votes.sol 2022-11-03 12:06:09.356515929 +0100 ++++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-11-04 16:35:52.560691845 +0100 @@ -49,7 +49,7 @@ /** * @dev Returns the balance of `account`. @@ -479,4 +515,48 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/ return balanceOf(account); } } - +diff -druN utils/Address.sol utils/Address.sol +--- utils/Address.sol 2022-11-03 12:06:09.356515929 +0100 ++++ utils/Address.sol 2022-11-04 16:35:52.564025262 +0100 +@@ -197,7 +197,7 @@ + bool success, + bytes memory returndata, + string memory errorMessage +- ) internal view returns (bytes memory) { ++ ) internal view returns (bytes memory val) { // MUNGED undeterministic return causes error for Prover + if (success) { + if (returndata.length == 0) { + // only check isContract if the call was successful and the return data is empty +@@ -220,7 +220,7 @@ + bool success, + bytes memory returndata, + string memory errorMessage +- ) internal pure returns (bytes memory) { ++ ) internal pure returns (bytes memory val) { // MUNGED undeterministic return causes error for Prover + if (success) { + return returndata; + } else { +diff -druN utils/Checkpoints.sol utils/Checkpoints.sol +--- utils/Checkpoints.sol 2022-11-02 12:17:36.976298213 +0100 ++++ utils/Checkpoints.sol 2022-11-04 16:35:52.564025262 +0100 +@@ -83,13 +83,13 @@ + * + * Returns previous value and new value. + */ +- function push( +- History storage self, +- function(uint256, uint256) view returns (uint256) op, +- uint256 delta +- ) internal returns (uint256, uint256) { +- return push(self, op(latest(self), delta)); +- } ++ // function push( ++ // History storage self, ++ // function(uint256, uint256) view returns (uint256) op, ++ // uint256 delta ++ // ) internal returns (uint256, uint256) { ++ // return push(self, op(latest(self), delta)); ++ // } + + /** + * @dev Returns the value in the most recent checkpoint, or zero if there are no checkpoints. diff --git a/certora/harnesses/GovernorFullHarness.sol b/certora/harnesses/GovernorFullHarness.sol index 026a32eae..c4ce83959 100644 --- a/certora/harnesses/GovernorFullHarness.sol +++ b/certora/harnesses/GovernorFullHarness.sol @@ -19,6 +19,7 @@ contract GovernorFullHarness is { using SafeCast for uint256; using Timers for Timers.BlockNumber; + using Checkpoints for Checkpoints.History; constructor( IVotes _token, @@ -37,6 +38,25 @@ contract GovernorFullHarness is // variable added to check when _castVote is called uint256 public latestCastVoteCall; + + // Harness from Votes // + + function getPastTotalSupply(uint256 blockNumber) public view returns(uint256) { + return token.getPastTotalSupply(blockNumber); + } + // Harness from GovernorVotesQuorumFraction // + + function getQuorumNumeratorLength() public view returns(uint256) { + return _quorumNumeratorHistory._checkpoints.length; + } + + function getQuorumNumeratorLatest() public view returns(uint256) { + return _quorumNumeratorHistory.latest(); + } + + function getDeprecatedQuorumNumerator() public view returns(uint256) { + return _quorumNumerator; + } // Harness from GovernorPreventLateQuorum // diff --git a/certora/scripts/noCI/Round1/verifyAll.sh b/certora/scripts/noCI/Round1/verifyAll.sh index a7d3c8ed2..68cada876 100644 --- a/certora/scripts/noCI/Round1/verifyAll.sh +++ b/certora/scripts/noCI/Round1/verifyAll.sh @@ -4,7 +4,7 @@ set -euxo pipefail for contract in certora/harnesses/Wizard*.sol; do - # NOTE: some spec wile are not governor related, and should be run on Wizard*.sol + # NOTE: some spec files are not governor related, and should be run on Wizard*.sol for spec in certora/specs/*.spec; do contractFile=$(basename $contract) diff --git a/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh b/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh similarity index 87% rename from certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh rename to certora/scripts/passes/verifyGovernorPreventLateQuorum.sh index 8b74837e1..35ff726c3 100644 --- a/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh @@ -6,8 +6,7 @@ certoraRun \ certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ - --solc solc \ --optimistic_loop \ --loop_iter 1 \ - --rule_sanity advanced \ + --rule_sanity \ $@ diff --git a/certora/specs/ERC1155.spec b/certora/specs/ERC1155.spec index bd88e8c09..3804ba5db 100644 --- a/certora/specs/ERC1155.spec +++ b/certora/specs/ERC1155.spec @@ -15,7 +15,6 @@ methods { } - ///////////////////////////////////////////////// // Approval (4/4) ///////////////////////////////////////////////// @@ -25,7 +24,7 @@ methods { // 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); + bool approveBefore = isApprovedForAll(account, operator); calldataarg args; f(e, args); @@ -33,7 +32,7 @@ rule unexpectedAllowanceChange(method f, env e) filtered { f -> f.selector != se bool approveAfter = isApprovedForAll(account, operator); assert approveBefore == approveAfter, "You couldn't get king's approval this way!"; -} +} // STATUS - verified @@ -52,7 +51,7 @@ rule onlyOwnerCanApprove(env e){ // STATUS - verified -// Chech that isApprovedForAll() revertes in planned scenarios and no more. +// Check that isApprovedForAll() revertes in planned scenarios and no more. rule approvalRevertCases(env e){ address account; address operator; isApprovedForAll@withrevert(account, operator); @@ -63,7 +62,7 @@ rule approvalRevertCases(env e){ // STATUS - verified // setApproval changes only one approval rule onlyOneAllowanceChange(method f, env e) { - address owner; address operator; address user; + address owner; address operator; address user; bool approved; bool userApproveBefore = isApprovedForAll(owner, user); @@ -73,7 +72,7 @@ rule onlyOneAllowanceChange(method f, env e) { bool userApproveAfter = isApprovedForAll(owner, user); assert userApproveBefore != userApproveAfter => (e.msg.sender == owner && operator == user), "Imposter!"; -} +} @@ -84,12 +83,12 @@ rule onlyOneAllowanceChange(method f, env e) { // 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) +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 != 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); @@ -100,11 +99,11 @@ rule unexpectedBalanceChange(method f, env e) 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) +// Check 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); @@ -113,14 +112,14 @@ rule balanceOfRevertCases(env e){ // STATUS - verified -// Chech that `balanceOfBatch()` revertes in planned scenarios and no more (only if at least one of `account`s is 0) +// Check 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.length == 3; + require ids.length == 3; require accounts[0] == account1; require accounts[1] == account2; require accounts[2] == account3; @@ -187,9 +186,9 @@ rule transferBatchCorrectness(env e){ require to != from; require idToCheck1 != idToCheck2 && idToCheck3 != idToCheck2 && idToCheck1 != idToCheck3; - - require ids.length == 3; - require amounts.length == 3; + + 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; @@ -245,8 +244,8 @@ rule cannotTransferMoreBatch(env e){ uint256 balanceBefore2 = balanceOf(from, idToCheck2); uint256 balanceBefore3 = balanceOf(from, idToCheck3); - require ids.length == 3; - require amounts.length == 3; + 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; @@ -261,7 +260,7 @@ rule cannotTransferMoreBatch(env e){ // 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; + uint256 id; uint256 amount; bytes data; require other != to; @@ -280,7 +279,7 @@ rule transferBalanceReduceEffect(env e){ // 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; + uint256 id; uint256 amount; bytes data; require from != other; @@ -315,8 +314,8 @@ rule transferBatchBalanceFromEffect(env e){ uint256 otherBalanceAfter2 = balanceOf(other, id2); uint256 otherBalanceAfter3 = balanceOf(other, id3); - assert from != other => (otherBalanceBefore1 == otherBalanceAfter1 - && otherBalanceBefore2 == otherBalanceAfter2 + assert from != other => (otherBalanceBefore1 == otherBalanceAfter1 + && otherBalanceBefore2 == otherBalanceAfter2 && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!"; } @@ -341,8 +340,8 @@ rule transferBatchBalanceToEffect(env e){ uint256 otherBalanceAfter2 = balanceOf(other, id2); uint256 otherBalanceAfter3 = balanceOf(other, id3); - assert other != to => (otherBalanceBefore1 == otherBalanceAfter1 - && otherBalanceBefore2 == otherBalanceAfter2 + assert other != to => (otherBalanceBefore1 == otherBalanceAfter1 + && otherBalanceBefore2 == otherBalanceAfter2 && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!"; } @@ -360,13 +359,13 @@ rule noTransferForNotApproved(env e) { 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; + address from; address operator; address to; bytes data; uint256[] ids; uint256[] amounts; @@ -377,7 +376,7 @@ rule noTransferBatchForNotApproved(env e) { safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data); assert !approve => lastReverted, "You don't have king's approval!"; -} +} // STATUS - verified @@ -385,7 +384,7 @@ rule noTransferBatchForNotApproved(env e) { rule noTransferEffectOnApproval(env e){ address from; address to; address owner; address operator; - uint256 id; uint256 amount; + uint256 id; uint256 amount; bytes data; bool approveBefore = isApprovedForAll(owner, operator); @@ -443,8 +442,8 @@ rule mintAdditivity(env e){ } -// STATUS - verified -// Chech that `mint()` revertes in planned scenario(s) (only if `to` is 0) +// STATUS - verified +// Check that `mint()` revertes in planned scenario(s) (only if `to` is 0) rule mintRevertCases(env e){ address to; uint256 id; uint256 amount; bytes data; @@ -455,7 +454,7 @@ rule mintRevertCases(env e){ // STATUS - verified -// Chech that `mintBatch()` revertes in planned scenario(s) (only if `to` is 0 or arrays have different length) +// Check 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; @@ -478,7 +477,7 @@ rule mintCorrectWork(env e){ mint(e, to, id, amount, data); uint256 otherBalanceAfter = balanceOf(to, id); - + assert otherBalanceBefore == otherBalanceAfter - amount, "Something is wrong"; } @@ -487,13 +486,13 @@ rule mintCorrectWork(env e){ // check that mintBatch updates `bootcamp participantsfrom` balance correctly rule mintBatchCorrectWork(env e){ address to; - uint256 id1; uint256 id2; uint256 id3; + 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 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; @@ -508,7 +507,7 @@ rule mintBatchCorrectWork(env e){ 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 @@ -524,7 +523,7 @@ rule cantMintMoreSingle(env e){ require to_mathint(balanceOf(to, id) + amount) > max_uint256; mint@withrevert(e, to, id, amount, data); - + assert lastReverted, "Don't be too greedy!"; } @@ -533,22 +532,22 @@ rule cantMintMoreSingle(env e){ // 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 id1; uint256 id2; uint256 id3; uint256 amount1; uint256 amount2; uint256 amount3; uint256[] ids; uint256[] amounts; - require ids.length == 3; + 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 + 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!"; } @@ -564,7 +563,7 @@ rule cantMintOtherBalances(env e){ mint(e, to, id, amount, data); uint256 otherBalanceAfter = balanceOf(other, id); - + assert other != to => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing"; } @@ -573,7 +572,7 @@ rule cantMintOtherBalances(env e){ // mintBatch changes only `to` balance rule cantMintBatchOtherBalances(env e){ address to; - uint256 id1; uint256 id2; uint256 id3; + uint256 id1; uint256 id2; uint256 id3; uint256[] ids; uint256[] amounts; address other; bytes data; @@ -587,9 +586,9 @@ rule cantMintBatchOtherBalances(env e){ uint256 otherBalanceAfter1 = balanceOf(other, id1); uint256 otherBalanceAfter2 = balanceOf(other, id2); uint256 otherBalanceAfter3 = balanceOf(other, id3); - - assert other != to => (otherBalanceBefore1 == otherBalanceAfter1 - && otherBalanceBefore2 == otherBalanceAfter2 + + assert other != to => (otherBalanceBefore1 == otherBalanceAfter1 + && otherBalanceBefore2 == otherBalanceAfter2 && otherBalanceBefore3 == otherBalanceAfter3) , "I like to see your money disappearing"; } @@ -622,7 +621,7 @@ rule burnAdditivity(env e){ // STATUS - verified -// Chech that `burn()` revertes in planned scenario(s) (if `from` is 0) +// Check that `burn()` revertes in planned scenario(s) (if `from` is 0) rule burnRevertCases(env e){ address from; uint256 id; uint256 amount; @@ -633,7 +632,7 @@ rule burnRevertCases(env e){ // STATUS - verified -// Chech that `balanceOf()` revertes in planned scenario(s) (if `from` is 0 or arrays have different length) +// Check 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; @@ -656,7 +655,7 @@ rule burnCorrectWork(env e){ burn(e, from, id, amount); uint256 otherBalanceAfter = balanceOf(from, id); - + assert otherBalanceBefore == otherBalanceAfter + amount, "Something is wrong"; } @@ -665,11 +664,11 @@ rule burnCorrectWork(env e){ // check that burnBatch updates `from` balance correctly rule burnBatchCorrectWork(env e){ address from; - uint256 id1; uint256 id2; uint256 id3; + uint256 id1; uint256 id2; uint256 id3; uint256 amount1; uint256 amount2; uint256 amount3; uint256[] ids; uint256[] amounts; - require ids.length == 3; + require ids.length == 3; require id1 != id2 && id2 != id3 && id3 != id1; require ids[0] == id1; require ids[1] == id2; require ids[2] == id3; @@ -684,7 +683,7 @@ rule burnBatchCorrectWork(env e){ 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 @@ -700,7 +699,7 @@ rule cantBurnMoreSingle(env e){ require to_mathint(balanceOf(from, id) - amount) < 0; burn@withrevert(e, from, id, amount); - + assert lastReverted, "Don't be too greedy!"; } @@ -709,21 +708,21 @@ rule cantBurnMoreSingle(env e){ // the user cannot burn more than they have (batch version) rule cantBurnMoreBatch(env e){ address from; - uint256 id1; uint256 id2; uint256 id3; + uint256 id1; uint256 id2; uint256 id3; uint256 amount1; uint256 amount2; uint256 amount3; uint256[] ids; uint256[] amounts; - require ids.length == 3; + 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 + 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!"; } @@ -739,7 +738,7 @@ rule cantBurnOtherBalances(env e){ burn(e, from, id, amount); uint256 otherBalanceAfter = balanceOf(other, id); - + assert other != from => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing"; } @@ -748,7 +747,7 @@ rule cantBurnOtherBalances(env e){ // burnBatch changes only `from` balance rule cantBurnBatchOtherBalances(env e){ address from; - uint256 id1; uint256 id2; uint256 id3; + uint256 id1; uint256 id2; uint256 id3; uint256 amount1; uint256 amount2; uint256 amount3; uint256[] ids; uint256[] amounts; address other; @@ -762,19 +761,19 @@ rule cantBurnBatchOtherBalances(env e){ uint256 otherBalanceAfter1 = balanceOf(other, id1); uint256 otherBalanceAfter2 = balanceOf(other, id2); uint256 otherBalanceAfter3 = balanceOf(other, id3); - - assert other != from => (otherBalanceBefore1 == otherBalanceAfter1 - && otherBalanceBefore2 == otherBalanceAfter2 + + 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 +// 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 +/// The result of transferring a single token must be equivalent whether done /// via safeTransferFrom or safeBatchTransferFrom. rule singleTokenSafeTransferFromSafeBatchTransferFromEquivalence { storage beforeTransfer = lastStorage; @@ -801,11 +800,11 @@ rule singleTokenSafeTransferFromSafeBatchTransferFromEquivalence { mathint recipientSafeBatchTransferFromBalanceChange = balanceOf(recipient, token) - recipientStartingBalance; assert holderSafeTransferFromBalanceChange == holderSafeBatchTransferFromBalanceChange - && recipientSafeTransferFromBalanceChange == recipientSafeBatchTransferFromBalanceChange, + && recipientSafeTransferFromBalanceChange == recipientSafeBatchTransferFromBalanceChange, "Transferring a single token via safeTransferFrom or safeBatchTransferFrom must be equivalent"; -} +} -/// The results of transferring multiple tokens must be equivalent whether done +/// The results of transferring multiple tokens must be equivalent whether done /// separately via safeTransferFrom or together via safeBatchTransferFrom. rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence { storage beforeTransfers = lastStorage; @@ -853,7 +852,7 @@ rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence { && holderSafeTransferFromBalanceChangeC == holderSafeBatchTransferFromBalanceChangeC && recipientSafeTransferFromBalanceChangeA == recipientSafeBatchTransferFromBalanceChangeA && recipientSafeTransferFromBalanceChangeB == recipientSafeBatchTransferFromBalanceChangeB - && recipientSafeTransferFromBalanceChangeC == recipientSafeBatchTransferFromBalanceChangeC, + && recipientSafeTransferFromBalanceChangeC == recipientSafeBatchTransferFromBalanceChangeC, "Transferring multiple tokens via safeTransferFrom or safeBatchTransferFrom must be equivalent"; } @@ -873,6 +872,6 @@ rule transfersHaveSameLengthInputArrays { uint256 tokensLength = tokens.length; uint256 transferAmountsLength = transferAmounts.length; - assert tokens.length == 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 index a5507bfce..929c35e89 100644 --- a/certora/specs/ERC1155Burnable.spec +++ b/certora/specs/ERC1155Burnable.spec @@ -1,3 +1,16 @@ +//// ## Verification of `ERC1155Burnable` +//// +//// `ERC1155Burnable` extends the `ERC1155` functionality by wrapping the internal +//// methods `_burn` and `_burnBatch` in the public methods `burn` and `burnBatch`, +//// adding a requirement that the caller of either method be the account holding +//// the tokens or approved to act on that account's behalf. +//// +//// ### Assumptions and Simplifications +//// +//// - No changes made using the harness +//// +//// ### Properties + methods { balanceOf(address, uint256) returns uint256 envfree isApprovedForAll(address,address) returns bool envfree @@ -22,7 +35,7 @@ rule onlyHolderOrApprovedCanReduceBalance(method f) /// 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. +/// appropriate equivalence between `burn` and `burnBatch` methods. rule burnAmountProportionalToBalanceReduction { storage beforeBurn = lastStorage; env e; @@ -47,7 +60,7 @@ rule burnAmountProportionalToBalanceReduction { /// 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. +/// appropriate equivalence between `burn` and `burnBatch` methods. rule sequentialBurnsEquivalentToSingleBurnOfSum { storage beforeBurns = lastStorage; env e; @@ -72,6 +85,7 @@ rule sequentialBurnsEquivalentToSingleBurnOfSum { /// The result of burning a single token must be equivalent whether done via /// burn or burnBatch. +/// @title Single token `burn` / `burnBatch` equivalence rule singleTokenBurnBurnBatchEquivalence { storage beforeBurn = lastStorage; env e; @@ -98,7 +112,8 @@ rule singleTokenBurnBurnBatchEquivalence { } /// The results of burning multiple tokens must be equivalent whether done -/// separately via burn or together via burnBatch. +/// separately via `burn` or together via `burnBatch`. +/// @title Multiple token `burn` / `burnBatch` equivalence rule multipleTokenBurnBurnBatchEquivalence { storage beforeBurns = lastStorage; env e; @@ -137,7 +152,7 @@ rule multipleTokenBurnBurnBatchEquivalence { "Burning multiple tokens via burn or burnBatch must be equivalent"; } -/// If passed empty token and burn amount arrays, burnBatch must not change +/// 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; @@ -169,4 +184,4 @@ rule sanity { 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 index 53a66e4b6..a6601b936 100644 --- a/certora/specs/ERC1155Pausable.spec +++ b/certora/specs/ERC1155Pausable.spec @@ -1,3 +1,15 @@ +//// ## Verification of `ERC1155Pausable` +//// +//// `ERC1155Pausable` extends existing `Pausable` functionality by requiring that a +//// contract not be in a `paused` state prior to a token transfer. +//// +//// ### Assumptions and Simplifications +//// - Internal methods `_pause` and `_unpause` wrapped by functions callable from CVL +//// - Dummy functions created to verify `whenPaused` and `whenNotPaused` modifiers +//// +//// +//// ### Properties + methods { balanceOf(address, uint256) returns uint256 envfree paused() returns bool envfree @@ -36,7 +48,7 @@ filtered { "Transfer methods must revert in a paused contract"; } -/// When a contract is in an unpaused state, calling pause() must pause. +/// When a contract is in an unpaused state, calling `pause()` must pause. rule pauseMethodPausesContract { require !paused(); @@ -80,8 +92,9 @@ rule cannotUnpauseWhileUnpaused { "A call to unpause when already unpaused must revert"; } -/// When a contract is in a paused state, functions with the whenNotPaused +/// When a contract is in a paused state, functions with the `whenNotPaused` /// modifier must revert. +/// @title `whenNotPaused` modifier causes revert if paused rule whenNotPausedModifierCausesRevertIfPaused { require paused(); @@ -92,8 +105,9 @@ rule whenNotPausedModifierCausesRevertIfPaused { "Functions with the whenNotPaused modifier must revert if the contract is paused"; } -/// When a contract is in an unpaused state, functions with the whenPaused +/// When a contract is in an unpaused state, functions with the `whenPaused` /// modifier must revert. +/// @title `whenPaused` modifier causes revert if unpaused rule whenPausedModifierCausesRevertIfUnpaused { require !paused(); @@ -113,4 +127,4 @@ rule sanity { 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 index 0060ab146..00842aacc 100644 --- a/certora/specs/ERC1155Supply.spec +++ b/certora/specs/ERC1155Supply.spec @@ -1,3 +1,14 @@ +//// ## Verification of `ERC1155Supply` +//// +//// `ERC1155Supply` extends the `ERC1155` functionality. The contract creates a publicly callable `totalSupply` wrapper for the private `_totalSupply` method, a public `exists` method to check for a positive balance of a given token, and updates `_beforeTokenTransfer` to appropriately change the mapping `_totalSupply` in the context of minting and burning tokens. +//// +//// ### Assumptions and Simplifications +//// - The `exists` method was wrapped in the `exists_wrapper` method because `exists` is a keyword in CVL. +//// - The public functions `burn`, `burnBatch`, `mint`, and `mintBatch` were implemented in the harnessing contract make their respective internal functions callable by the CVL. This was used to test the increase and decrease of `totalSupply` when tokens are minted and burned. +//// - We created the `onlyOwner` modifier to be used in the above functions so that they are not called in unrelated rules. +//// +//// ### Properties + methods { totalSupply(uint256) returns uint256 envfree @@ -6,8 +17,8 @@ methods { owner() returns address envfree } -/// given two different token ids, if totalSupply for one changes, then -/// totalSupply for other must not +/// Given two different token ids, if total supply for one changes, then +/// total supply for other must not. rule token_totalSupply_independence(method f) filtered { f -> f.selector != safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index bc9cc8b13..1807444b7 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -1,4 +1,4 @@ -import "erc20.spec" +import "erc20methods.spec" /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec index e014147f8..99c0db480 100644 --- a/certora/specs/ERC20FlashMint.spec +++ b/certora/specs/ERC20FlashMint.spec @@ -1,4 +1,4 @@ -import "erc20.spec" +import "erc20methods.spec" methods { maxFlashLoan(address) returns(uint256) envfree @@ -7,7 +7,7 @@ methods { ghost mapping(address => uint256) trackedBurnAmount; -// 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'" +// returns is 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'" function specBurn(address account, uint256 amount) returns bool { trackedBurnAmount[account] = amount; return true; diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index b99895f45..83a3a360e 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -1,4 +1,4 @@ -import "erc20.spec" +import "erc20methods.spec" methods { // IVotes @@ -62,10 +62,6 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint doubleFromBlock@new(account) == (newBlock == lastFromBlock(account)); } -/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// -// Invariants // -/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// - // 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() @@ -74,7 +70,8 @@ invariant votes_solvency() { preserved with(env e) { require forall address account. numCheckpoints(account) < 1000000; - } preserved _burn(address a, uint256 amount) with(env e) { + } + preserved _burn(address a, uint256 amount) with(env e) { require _delegates(0) == 0; require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(_delegates(a)) + balanceOf(_delegates(a2)) <= totalVotes()); require balanceOf(_delegates(a)) < totalVotes(); @@ -82,7 +79,18 @@ invariant votes_solvency() } } +// 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 } + +// 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 } @@ -108,9 +116,6 @@ invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2) pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2) filtered { f -> !f.isView } -/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// -// Rules // -/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// // 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 @@ -154,6 +159,7 @@ rule transfer_safe() { 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) @@ -262,7 +268,6 @@ rule delegate_no_frontrunning(method f) { assert other_votes_ == _other_votes, "delegate not contained"; } -// passes rule onMint() { env e; uint256 amount; @@ -274,11 +279,10 @@ rule onMint() { _mint(e, account, amount); - assert totalVotes() == totalVotesBefore, "totalVotes decreased"; - assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly"; + assert totalVotes() == totalVotesBefore, "totalVotes changed"; + assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore, "previous totalSupply not saved properly"; } -// passes rule onBurn() { env e; uint256 amount; @@ -290,6 +294,6 @@ rule onBurn() { _burn(e, account, amount); - assert totalVotes() == totalVotesBefore, "totalVotes decreased"; - assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly"; + assert totalVotes() == totalVotesBefore, "totalVotes changed"; + assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore, "previous totalSupply not saved properly"; } diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index b052e3c87..3d9bba667 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -56,6 +56,11 @@ invariant underTotalAndContractBalanceOfCorrelation(env e) require balanceOf(account) >= amount; requireInvariant totalSupplyIsSumOfBalances; } + preserved depositFor(address account, uint256 amount) with (env e3){ + require totalSupply() + amount <= underlyingBalanceOf(currentContract); + require underlyingBalanceOf(currentContract) + amount < max_uint256; + require underlying() != currentContract; + } } /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index c0fce61b2..def58708c 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -2,8 +2,6 @@ ///////////////////// Governor.sol base definitions ////////////////////////// ////////////////////////////////////////////////////////////////////////////// -using ERC20VotesHarness as erc20votes - methods { proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index baf932e19..9e1d45dd9 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -1,18 +1,68 @@ import "GovernorCountingSimple.spec" +using ERC20VotesHarness as token + +/*** +## Verification of `GovernorPreventLateQuorum` + +`GovernorPreventLateQuorum` extends the Governor group of contracts to add the +feature of giving voters more time to vote in the case that a proposal reaches +quorum with less than `voteExtension` amount of time left to vote. + +### Assumptions and Simplifications + +None + +#### Harnessing +- The contract that the specification was verified against is + `GovernorPreventLateQuorumHarness`, which inherits from all of the Governor + contracts — excluding Compound variations — and implements a number of view + functions to gain access to values that are impossible/difficult to access in + CVL. It also implements all of the required functions not implemented in the + abstract contracts it inherits from. + +- `_castVote` was overridden to add an additional flag before calling the parent + version. This flag stores the `block.number` in a variable + `latestCastVoteCall` and is used as a way to check when any of variations of + `castVote` are called. + +#### Munging + +- Various variables' visibility was changed from private to internal or from + internal to public throughout the Governor contracts in order to make them + accessible in the spec. + +- Arbitrary low level calls are assumed to change nothing and thus the function + `_execute` is changed to do nothing. The tool normally havocs in this + situation, assuming all storage can change due to possible reentrancy. We + assume, however, there is no risk of reentrancy because `_execute` is a + protected call locked behind the timelocked governance vote. All other + governance functions are verified separately. +*/ + methods { + // summarized + hashProposal(address[],uint256[],bytes[],bytes32) returns (uint256) => NONDET + _hashTypedDataV4(bytes32) returns (bytes32) + + // envfree + quorumNumerator(uint256) returns uint256 quorumDenominator() returns uint256 envfree votingPeriod() returns uint256 envfree lateQuorumVoteExtension() returns uint64 envfree propose(address[], uint256[], bytes[], string) // harness + getDeprecatedQuorumNumerator() returns uint256 envfree + getQuorumNumeratorLength() returns uint256 envfree + getQuorumNumeratorLatest() returns uint256 envfree 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 + getPastTotalSupply(uint256) returns (uint256) envfree // more robust check than f.selector == _castVote(...).selector latestCastVoteCall() returns uint256 envfree @@ -26,99 +76,141 @@ methods { } -////////////////////////////////////////////////////////////////////////////// -///////////////////////////// Helper Functions /////////////////////////////// -////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +// 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) { + 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); } } +/// Restricting out common reasons why rules break. We assume quorum length won't overflow (uint256) and that functions +/// called in env `e2` have a `block.number` greater than or equal `e1`'s `block.number`. +function setup(env e1, env e2) { + require getQuorumNumeratorLength() + 1 < max_uint; + require e2.block.number >= e1.block.number; +} -////////////////////////////////////////////////////////////////////////////// -//////////////////////////////// Definitions ///////////////////////////////// -////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//// #### Definitions // +//////////////////////////////////////////////////////////////////////////////// -// proposal deadline can be extended (but isn't) +/// The proposal with proposal id `pId` has a deadline which is extendable. definition deadlineExtendable(env e, uint256 pId) returns bool = getExtendedDeadlineIsUnset(pId) // deadline == 0 && !quorumReached(e, pId); -// proposal deadline has been extended +/// The proposal with proposal id `pId` has a deadline which has been extended. definition deadlineExtended(env e, uint256 pId) returns bool = getExtendedDeadlineIsStarted(pId) // deadline > 0 && quorumReached(e, pId); +/// The proposal with proposal id `pId` has not been created. 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); + && getForVotes(pId) == 0; +/// Method f is a version of `castVote` whose state changing effects are covered by `castVoteBySig`. +/// @dev castVoteBySig allows anyone to cast a vote for anyone else if they can supply the signature. Specifically, +/// it covers the case where the msg.sender supplies a signature for themselves which is normally done using the normal +/// `castVote`. +definition castVoteSubset(method f) returns bool = + f.selector == castVote(uint256, uint8).selector || + f.selector == castVoteWithReason(uint256, uint8, string).selector || + f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector || + f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector; +//////////////////////////////////////////////////////////////////////////////// +//// ### Properties // +//////////////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////////////// +// Invariants // +//////////////////////////////////////////////////////////////////////////////// + +/** + * If a proposal has reached quorum then the proposal snapshot (start `block.number`) must be non-zero + */ +invariant quorumReachedEffect(env e1, uint256 pId) + quorumReached(e1, pId) && getPastTotalSupply(0) > 0 => proposalCreated(pId) // bug: 0 supply 0 votes => quorumReached + // relay havocs external contracts, changing pastTotalSupply and thus quorumReached + filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } + { + preserved with (env e2) { + setup(e1, e2); + } + } + +/** + * A created proposal must be in state `deadlineExtendable` or `deadlineExtended`. + */ +invariant proposalInOneState(env e1, uint256 pId) + getPastTotalSupply(0) > 0 => (proposalNotCreated(e1, pId) || deadlineExtendable(e1, pId) || deadlineExtended(e1, pId)) + filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } + { + preserved with (env e2) { + require proposalCreated(pId); + setup(e1, e2); + } + } +/** + * The quorum numerator is always less than or equal to the quorum denominator. + */ +invariant quorumNumerLTEDenom(env e1, uint256 blockNumber) + quorumNumerator(e1, blockNumber) <= quorumDenominator() + { + preserved with (env e2) { + setup(e1, e2); + } + } + +/** + * The deprecated quorum numerator variable `_quorumNumerator` is always 0 in a contract that is not upgraded. + */ +invariant deprecatedQuorumStateIsUninitialized() + getDeprecatedQuorumNumerator() == 0 + ////////////////////////////////////////////////////////////////////////////// -///////////////////////////////// Invariants ///////////////////////////////// +// Rules // ////////////////////////////////////////////////////////////////////////////// -/* - * 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 +/** + * `updateQuorumNumerator` can only change quorum requirements for future proposals. + * @dev In the case that the array containing past quorum numerators overflows, this rule will fail. */ -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 +rule quorumReachedCantChange(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { + env e1; uint256 pId; + bool _quorumReached = quorumReached(e1, pId); -/* - * 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 + env e2; uint256 newQuorumNumerator; + setup(e1, e2); + updateQuorumNumerator(e2, newQuorumNumerator); + + env e3; + bool quorumReached_ = quorumReached(e3, pId); + + assert _quorumReached == quorumReached_, "function changed quorumReached"; +} + +///////////////////////////// #### first set of rules //////////////////////// + +//// The rules [`deadlineChangeEffects`](#deadlineChangeEffects) and [`deadlineCantBeUnextended`](#deadlineCantBeUnextended) +//// are assumed in rule [`canExtendDeadlineOnce`](#canExtendDeadlineOnce), so we prove them first. + +/** + * If deadline increases then we are in `deadlineExtended` state and `castVote` + * was called. */ -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} { +rule deadlineChangeEffects(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { env e; calldataarg args; uint256 pId; requireInvariant quorumReachedEffect(e, pId); @@ -131,57 +223,53 @@ rule deadlineChangeEffects(method f) filtered {f -> !f.isView} { } -/* - * R2: A proposal can't leave deadlineExtended state. - * RULE PASSING* - * ADVANCED SANITY PASSING +/** + * @title Deadline can't be unextended + * @notice A proposal can't leave `deadlineExtended` state. */ -rule deadlineCantBeUnextended(method f) - filtered { - f -> !f.isView - // && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function - } { - env e; calldataarg args; uint256 pId; +rule deadlineCantBeUnextended(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { + env e1; env e2; env e3; env e4; calldataarg args; uint256 pId; + setup(e1, e2); - require(deadlineExtended(e, pId)); - requireInvariant quorumReachedEffect(e, pId); + require(deadlineExtended(e1, pId)); + requireInvariant quorumReachedEffect(e1, pId); - f(e, args); + f(e2, args); - assert(deadlineExtended(e, pId)); + assert(deadlineExtended(e1, pId)); } -/* - * R3: A proposal's deadline can't change in deadlineExtended state. - * RULE PASSING - * ADVANCED SANITY PASSING +/** + * A proposal's deadline can't change in `deadlineExtended` state. */ -rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} { - env e; calldataarg args; uint256 pId; +rule canExtendDeadlineOnce(method f) filtered {f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector} { + env e1; env e2; calldataarg args; uint256 pId; - require(deadlineExtended(e, pId)); - requireInvariant quorumReachedEffect(e, pId); + require(deadlineExtended(e1, pId)); + require(proposalSnapshot(pId) > 0); + requireInvariant quorumReachedEffect(e1, pId); + setup(e1, e2); uint256 deadlineBefore = proposalDeadline(pId); - f(e, args); + f(e2, args); uint256 deadlineAfter = proposalDeadline(pId); assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); } -//////////////////////////// second set of rules //////////////////////////// +/////////////////////// #### 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 +//// The main rule in this section is [the deadline can only be extended if quorum reached with <= `timeOfExtension` left to vote](#deadlineExtnededIfQuorumReached) +//// The other rules of this section are assumed in the proof, 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 +/** + * 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 hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isView} { +rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector} { address acc = e.msg.sender; require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power @@ -211,13 +299,11 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f. "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 +/** + * @title Against votes don't count + * @notice An against vote does not make a proposal reach quorum. */ -rule againstVotesDontCount(method f) filtered {f -> !f.isView} { +rule againstVotesDontCount(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { env e; calldataarg args; uint256 pId; address acc = e.msg.sender; @@ -232,63 +318,65 @@ rule againstVotesDontCount(method f) filtered {f -> !f.isView} { 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 +/** + * Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote */ -rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} { - env e; calldataarg args; uint256 pId; + // not reasonable rule since tool can arbitrarily pick a pre-state where quorum is reached +// rule deadlineExtendedIfQuorumReached(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { +// env e; calldataarg args; uint256 pId; - requireInvariant proposalInOneState(e, pId); - requireInvariant quorumReachedEffect(e, pId); - requireInvariant proposalNotCreatedEffects(e, pId); +// requireInvariant proposalInOneState(e, pId); +// requireInvariant quorumReachedEffect(e, pId); +// require proposalCreated(pId); +// require getPastTotalSupply(proposalSnapshot(pId)) >= 100; +// require quorumNumerator(e, proposalSnapshot(pId)) > 0; - bool wasDeadlineExtendable = deadlineExtendable(e, pId); - uint64 extension = lateQuorumVoteExtension(); - uint256 deadlineBefore = proposalDeadline(pId); - f(e, args); - uint256 deadlineAfter = proposalDeadline(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"; -} +// 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 +/** + * `extendedDeadlineField` is set if and only if `_castVote` is called and quorum is reached. */ -rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} { - env e; calldataarg args; uint256 pId; + // tool picks a state where quorum is unreached but extendedDeadline is set and then casts a vote which causes quorum + // to be reached, so the rule breaks. Need to write a rule that says that if quorum is unreached, then extendedDeadline + // must be unset. +// rule extendedDeadlineValueSetIfQuorumReached(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { +// env e; calldataarg args; uint256 pId; +// setup(e, e); +// requireInvariant proposalInOneState(e, pId); +// require lateQuorumVoteExtension() + e.block.number < max_uint64; - requireInvariant proposalInOneState(e, pId); +// bool extendedBefore = deadlineExtended(e, pId); +// f(e, args); +// bool extendedAfter = deadlineExtended(e, pId); +// uint256 extDeadline = getExtendedDeadline(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" +// ); +// } - assert( - !extendedBefore && extendedAfter - => extDeadline == e.block.number + lateQuorumVoteExtension(), - "extended deadline was not set" - ); -} - -/* - * R8: Deadline can never be reduced. - * RULE PASSING - * ADVANCED SANITY PASSING +/** + * Deadline can never be reduced. */ -rule deadlineNeverReduced(method f) filtered {f -> !f.isView} { - env e; calldataarg args; uint256 pId; +rule deadlineNeverReduced(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { + env e1; env e2; calldataarg args; uint256 pId; - requireInvariant quorumReachedEffect(e, pId); - requireInvariant proposalNotCreatedEffects(e, pId); + requireInvariant quorumReachedEffect(e1, pId); + require proposalCreated(pId); + setup(e1, e2); uint256 deadlineBefore = proposalDeadline(pId); - f(e, args); + f(e2, args); uint256 deadlineAfter = proposalDeadline(pId); assert(deadlineAfter >= deadlineBefore); diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec index 0adbad08c..62f30b1d2 100644 --- a/certora/specs/Initializable.spec +++ b/certora/specs/Initializable.spec @@ -1,3 +1,33 @@ +//// ## Verification of `Initializable` +//// +//// `Initializable` is a contract used to make constructors for upgradable +//// contracts. This is accomplished by applying the `initializer` modifier to any +//// function that serves as a constructor, which makes this function only +//// callable once. The secondary modifier `reinitializer` allows for upgrades +//// that should run at most once after the contract is upgraded. +//// +//// +//// ### Assumptions and Simplifications +//// We assume `initializer()` and `reinitializer(1)` are equivalent if they +//// both guarantee `_initialized` to be set to 1 after a successful call. This +//// allows us to use `reinitializer(n)` as a general version that also handles +//// the regular `initialzer` case. +//// +//// #### Harnessing +//// Two harness versions were implemented, a simple flat contract, and a +//// Multi-inheriting contract. The two versions together help us ensure there are +//// No unexpected results because of different implementations. `Initializable` can +//// Be used in many different ways but we believe these 2 cases provide good +//// Coverage for all cases. In both harnesses we use getter functions for +//// `_initialized` and `_initializing` and implement `initializer` and +//// `reinitializer` functions that use their respective modifiers. We also +//// Implement some versioned functions that are only callable in specific +//// Versions of the contract to mimic upgrading contracts. +//// +//// #### Munging +//// Variables `_initialized` and `_initializing` were changed to have internal +//// visibility to be harnessable. + methods { initialize(uint256, uint256, uint256) envfree reinitialize(uint256, uint256, uint256, uint8) envfree @@ -17,35 +47,47 @@ methods { } -////////////////////////////////////////////////////////////////////////////// -//////////////////////////////// Definitions ///////////////////////////////// -////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//// #### Definitions //// +//////////////////////////////////////////////////////////////////////////////// +//// ***`isUninitialized:`*** A contract's `_initialized` variable is equal to 0. definition isUninitialized() returns bool = initialized() == 0; +//// ***`isInitialized:`*** A contract's `_initialized` variable is greater than 0. definition isInitialized() returns bool = initialized() > 0; +//// ***`isInitializedOnce:`*** A contract's `_initialized` variable is equal to 1. definition isInitializedOnce() returns bool = initialized() == 1; +//// ***`isReinitialized:`*** A contract's `_initialized` variable is greater than 1. definition isReinitialized() returns bool = initialized() > 1; +//// ***`isDisabled:`*** A contract's `_initialized` variable is equal to 255. definition isDisabled() returns bool = initialized() == 255; ////////////////////////////////////////////////////////////////////////////// -///////////////////////////////// Invariants ///////////////////////////////// +//// ### Properties /////////////////////////// ////////////////////////////////////////////////////////////////////////////// -/// @description A contract must only ever be in an initializing state while in the middle of a transaction execution. +////////////////////////////////////////////////////////////////////////////// +// Invariants ///////////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +/// A contract must only ever be in an initializing state while in the middle +/// of a transaction execution. invariant notInitializing() !initializing() ////////////////////////////////////////////////////////////////////////////// -////////////////////////////////// Rules ///////////////////////////////////// +// Rules ///////////////////////////////////// ////////////////////////////////////////////////////////////////////////////// -/// @description An initializeable contract with a function that inherits the initializer modifier must be initializable only once" +/// @title Only initialized once +/// @notice An initializable contract with a function that inherits the +/// initializer modifier must be initializable only once rule initOnce() { uint256 val; uint256 a; uint256 b; @@ -54,7 +96,8 @@ rule initOnce() { 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. +/// 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; @@ -63,9 +106,10 @@ rule reinitializeEffects { 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 { +/// Successfully calling `initialize()` must result in `_initialized` being set to 1. +/// @dev We assume `initialize()` and `reinitialize(1)` are equivalent if this rule +/// and the [above rule][#reinitializeEffects] both pass. +rule initializeEffects { uint256 val; uint256 a; uint256 b; initialize(val, a, b); @@ -73,7 +117,7 @@ rule initalizeEffects { assert isInitializedOnce(), "initialize() must set _initialized to 1"; } -/// @description A disabled initializable contract must always stay disabled. +/// A disabled initializable contract must always stay disabled. rule disabledStaysDisabled(method f) { env e; calldataarg args; @@ -84,7 +128,7 @@ rule disabledStaysDisabled(method f) { assert disabledBefore => disabledAfter, "a disabled initializer must stay disabled"; } -/// @description The variable _initialized must not decrease. +/// The variable `_initialized` must not decrease. rule increasingInitialized(method f) { env e; calldataarg args; @@ -94,7 +138,9 @@ rule increasingInitialized(method f) { assert initBefore <= initAfter, "_initialized must only increase"; } -/// @description If reinitialize(...) was called successfuly, then the variable _initialized must increases. +/// If `reinitialize(...)` was called successfully, then the variable +/// `_initialized` must increase. +/// @title Reinitialize increases `init` rule reinitializeIncreasesInit { uint256 val; uint8 n; uint256 a; uint256 b; @@ -105,7 +151,9 @@ rule reinitializeIncreasesInit { 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 +/// `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; @@ -116,7 +164,8 @@ rule reinitializeLiveness { 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. +/// If `reinitialize(n)` was called successfully then `n` was greater than +/// `_initialized`. rule reinitializeRule { uint256 val; uint8 n; uint256 a; uint256 b; @@ -126,7 +175,9 @@ rule reinitializeRule { 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. +/// Functions implemented in the parent contract that require `_initialized` to +/// be a certain value are only callable when it is that value. +/// @title Reinitialize version check parent rule reinitVersionCheckParent { uint8 n; @@ -134,7 +185,9 @@ rule reinitVersionCheckParent { 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. +/// Functions implemented in the child contract that require `_initialized` to +/// be a certain value are only callable when it is that value. +/// @title Reinitialize version check child rule reinitVersionCheckChild { uint8 n; @@ -142,7 +195,9 @@ rule reinitVersionCheckChild { 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. +/// Functions implemented in the grandchild contract that require `_initialized` +/// to be a certain value are only callable when it is that value. +/// @title Reinitialize version check grandchild rule reinitVersionCheckGrandchild { uint8 n; @@ -150,10 +205,11 @@ rule reinitVersionCheckGrandchild { 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. +/// Calling parent initializer 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 18a79d619..877b437fc 100644 --- a/certora/specs/RulesInProgress.spec +++ b/certora/specs/RulesInProgress.spec @@ -140,15 +140,15 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) { -/////////////////// 2nd iteration with OZ ////////////////////////// +/////////////////// 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) { +function executionsCall(method f, env e, address target, uint256 value, bytes data, + bytes32 predecessor, bytes32 salt, uint256 delay, + address[] targets, uint256[] values, bytes[] calldatas) { 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); + executeBatch(e, targets, values, calldatas, predecessor, salt); } else { calldataarg args; f(e, args); @@ -160,17 +160,16 @@ function executionsCall(method f, env e, address target, uint256 value, bytes da 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; + address[] targets; uint256[] values; bytes[] calldatas; - 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); + require (targets[0] == target && values[0] == value && calldatas[0] == data) + || (targets[1] == target && values[1] == value && calldatas[1] == data) + || (targets[2] == target && values[2] == value && calldatas[2] == data); hashIdCorrelation(id, target, value, data, predecessor, salt); - executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas); + executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, calldatas); - assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + 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/erc20.spec b/certora/specs/erc20methods.spec similarity index 100% rename from certora/specs/erc20.spec rename to certora/specs/erc20methods.spec diff --git a/resource_errors.json b/resource_errors.json deleted file mode 100644 index d9bd79235..000000000 --- a/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "topics": [] -} \ No newline at end of file