diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 3957b54f3..32adf065f 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-03-02 09:14:55.000000000 -0800 -+++ access/AccessControl.sol 2022-04-08 17:31:22.000000000 -0700 +--- access/AccessControl.sol 2022-05-06 13:44:28.000000000 -0700 ++++ access/AccessControl.sol 2022-05-09 09:49:26.000000000 -0700 @@ -93,7 +93,7 @@ * * _Available since v4.6._ @@ -10,9 +10,21 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol _checkRole(role, _msgSender()); } +diff -ruN governance/Governor.sol governance/Governor.sol +--- governance/Governor.sol 2022-05-09 09:11:10.000000000 -0700 ++++ governance/Governor.sol 2022-05-09 09:49:26.000000000 -0700 +@@ -42,7 +42,7 @@ + + string private _name; + +- mapping(uint256 => ProposalCore) private _proposals; ++ mapping(uint256 => ProposalCore) internal _proposals; + + // This queue keeps track of the governor operating on itself. Calls to functions protected by the + // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute}, diff -ruN governance/TimelockController.sol governance/TimelockController.sol ---- governance/TimelockController.sol 2022-03-02 09:14:55.000000000 -0800 -+++ governance/TimelockController.sol 2022-04-08 17:31:22.000000000 -0700 +--- governance/TimelockController.sol 2022-05-06 13:44:28.000000000 -0700 ++++ governance/TimelockController.sol 2022-05-09 09:49:26.000000000 -0700 @@ -24,10 +24,10 @@ bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE"); bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); @@ -32,9 +44,23 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol } -} +} +diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol +--- governance/extensions/GovernorPreventLateQuorum.sol 2022-05-09 09:11:01.000000000 -0700 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2022-05-09 09:49:26.000000000 -0700 +@@ -21,8 +21,8 @@ + using SafeCast for uint256; + using Timers for Timers.BlockNumber; + +- uint64 private _voteExtension; +- mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines; ++ uint64 internal _voteExtension; ++ mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines; + + /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period. + event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline); diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol ---- governance/utils/Votes.sol 2022-03-02 09:14:55.000000000 -0800 -+++ governance/utils/Votes.sol 2022-04-08 17:44:19.000000000 -0700 +--- governance/utils/Votes.sol 2022-05-06 13:44:28.000000000 -0700 ++++ governance/utils/Votes.sol 2022-05-09 09:49:26.000000000 -0700 @@ -35,7 +35,25 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -108,8 +134,8 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol + function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public } diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol ---- token/ERC1155/ERC1155.sol 2022-03-02 09:14:55.000000000 -0800 -+++ token/ERC1155/ERC1155.sol 2022-04-08 17:31:22.000000000 -0700 +--- token/ERC1155/ERC1155.sol 2022-05-06 13:44:28.000000000 -0700 ++++ token/ERC1155/ERC1155.sol 2022-05-09 09:49:26.000000000 -0700 @@ -268,7 +268,7 @@ uint256 id, uint256 amount, @@ -165,8 +191,8 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns ( bytes4 response diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol ---- token/ERC20/ERC20.sol 2022-03-02 09:14:55.000000000 -0800 -+++ token/ERC20/ERC20.sol 2022-04-08 17:31:22.000000000 -0700 +--- token/ERC20/ERC20.sol 2022-05-06 13:44:28.000000000 -0700 ++++ token/ERC20/ERC20.sol 2022-05-09 09:49:26.000000000 -0700 @@ -277,7 +277,7 @@ * - `account` cannot be the zero address. * - `account` must have at least `amount` tokens. @@ -186,8 +212,8 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol /** diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol ---- token/ERC20/extensions/ERC20FlashMint.sol 2022-03-02 09:14:55.000000000 -0800 -+++ token/ERC20/extensions/ERC20FlashMint.sol 2022-04-08 17:31:22.000000000 -0700 +--- token/ERC20/extensions/ERC20FlashMint.sol 2022-05-06 13:44:28.000000000 -0700 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2022-05-09 09:49:26.000000000 -0700 @@ -40,9 +40,11 @@ require(token == address(this), "ERC20FlashMint: wrong token"); // silence warning about unused variable without the addition of bytecode. @@ -202,8 +228,8 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 * @dev Performs a flash loan. New tokens are minted and sent to the * `receiver`, who is required to implement the {IERC3156FlashBorrower} diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol ---- token/ERC20/extensions/ERC20Votes.sol 2022-03-02 09:14:55.000000000 -0800 -+++ token/ERC20/extensions/ERC20Votes.sol 2022-04-08 17:31:22.000000000 -0700 +--- token/ERC20/extensions/ERC20Votes.sol 2022-05-06 13:43:21.000000000 -0700 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-05-09 09:49:26.000000000 -0700 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -335,8 +361,8 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote return a + b; } diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol ---- token/ERC20/extensions/ERC20Wrapper.sol 2022-03-02 09:14:55.000000000 -0800 -+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-04-08 17:31:22.000000000 -0700 +--- token/ERC20/extensions/ERC20Wrapper.sol 2022-05-06 13:44:28.000000000 -0700 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-05-09 09:49:26.000000000 -0700 @@ -44,7 +44,7 @@ * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal * function that can be exposed with access control if desired. @@ -347,8 +373,8 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr _mint(account, value); return value; diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol ---- token/ERC721/extensions/draft-ERC721Votes.sol 2022-03-02 09:14:55.000000000 -0800 -+++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-04-08 17:31:22.000000000 -0700 +--- token/ERC721/extensions/draft-ERC721Votes.sol 2022-05-06 13:44:28.000000000 -0700 ++++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-05-09 09:49:26.000000000 -0700 @@ -34,7 +34,7 @@ /** * @dev Returns the balance of `account`. diff --git a/certora/harnesses/GovernorPreventLateQuorumHarness.sol b/certora/harnesses/GovernorPreventLateQuorumHarness.sol new file mode 100644 index 000000000..e13bb62e5 --- /dev/null +++ b/certora/harnesses/GovernorPreventLateQuorumHarness.sol @@ -0,0 +1,159 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../munged/governance/extensions/GovernorPreventLateQuorum.sol"; +import "../munged/governance/Governor.sol"; +import "../munged/governance/extensions/GovernorCountingSimple.sol"; +import "../munged/governance/extensions/GovernorVotes.sol"; +import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../munged/governance/extensions/GovernorTimelockControl.sol"; +import "../munged/token/ERC20/extensions/ERC20Votes.sol"; + +contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl, GovernorPreventLateQuorum { + using SafeCast for uint256; + using Timers for Timers.BlockNumber; + constructor(IVotes _token, TimelockController _timelock, uint64 initialVoteExtension, uint256 quorumNumeratorValue) + Governor("Harness") + GovernorVotes(_token) + GovernorVotesQuorumFraction(quorumNumeratorValue) + GovernorTimelockControl(_timelock) + GovernorPreventLateQuorum(initialVoteExtension) + {} + + // variable added to check when _castVote is called + uint256 public latestCastVoteCall; + + // Harness from GovernorPreventLateQuorum // + + function getVoteExtension() public view returns(uint64) { + return _voteExtension; + } + + function getExtendedDeadlineIsUnset(uint256 id) public view returns(bool) { + return _extendedDeadlines[id].isUnset(); + } + + function getExtendedDeadline(uint256 id) public view returns(uint64) { + return _extendedDeadlines[id].getDeadline(); + } + + // Harness from GovernorCountingSimple // + + function quorumReached(uint256 proposalId) public view returns(bool) { + return _quorumReached(proposalId); + } + + // Harness from Governor // + + function isExecuted(uint256 proposalId) public view returns (bool) { + return _proposals[proposalId].executed; + } + + function isCanceled(uint256 proposalId) public view returns (bool) { + return _proposals[proposalId].canceled; + } + + // The following functions are overrides required by Solidity added by Certora. // + + function proposalDeadline(uint256 proposalId) public view virtual override(Governor, GovernorPreventLateQuorum, IGovernor) returns (uint256) { + return super.proposalDeadline(proposalId); + } + + function _castVote( + uint256 proposalId, + address account, + uint8 support, + string memory reason, + bytes memory params + ) internal virtual override(Governor, GovernorPreventLateQuorum) returns (uint256) { + latestCastVoteCall = block.number; + return super._castVote(proposalId, account, support, reason, params); + } + + function castVote( + uint256 proposalId, + address account, + uint8 support, + string memory reason, + bytes memory params + ) public returns(uint256) { + return _castVote(proposalId, account, support, reason, params); + } + + function lateQuorumVoteExtension() public view virtual override returns (uint64) { + return super.lateQuorumVoteExtension(); + } + + function setLateQuorumVoteExtension(uint64 newVoteExtension) public virtual override onlyGovernance { + super.setLateQuorumVoteExtension(newVoteExtension); + } + + // The following functions are overrides required by Solidity added by OZ Wizard. // + + function votingDelay() public pure override returns (uint256) { + return 1; // 1 block + } + + function votingPeriod() public pure override returns (uint256) { + return 45818; // 1 week + } + + function quorum(uint256 blockNumber) + public + view + override(IGovernor, GovernorVotesQuorumFraction) + returns (uint256) + { + return super.quorum(blockNumber); + } + + function state(uint256 proposalId) + public + view + override(Governor, GovernorTimelockControl) + returns (ProposalState) + { + return super.state(proposalId); + } + + function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description) + public + override(Governor, IGovernor) + returns (uint256) + { + return super.propose(targets, values, calldatas, description); + } + + function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) + internal + override(Governor, GovernorTimelockControl) + { + super._execute(proposalId, targets, values, calldatas, descriptionHash); + } + + function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) + internal + override(Governor, GovernorTimelockControl) + returns (uint256) + { + return super._cancel(targets, values, calldatas, descriptionHash); + } + + function _executor() + internal + view + override(Governor, GovernorTimelockControl) + returns (address) + { + return super._executor(); + } + + function supportsInterface(bytes4 interfaceId) + public + view + override(Governor, GovernorTimelockControl) + returns (bool) + { + return super.supportsInterface(interfaceId); + } +} \ No newline at end of file diff --git a/certora/munged/governance/Governor.sol b/certora/munged/governance/Governor.sol index 8907d9468..75e634c3d 100644 --- a/certora/munged/governance/Governor.sol +++ b/certora/munged/governance/Governor.sol @@ -42,7 +42,7 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor { string private _name; - mapping(uint256 => ProposalCore) private _proposals; + mapping(uint256 => ProposalCore) internal _proposals; // This queue keeps track of the governor operating on itself. Calls to functions protected by the // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute}, diff --git a/certora/munged/governance/extensions/GovernorPreventLateQuorum.sol b/certora/munged/governance/extensions/GovernorPreventLateQuorum.sol index 5b58f6032..453d03b68 100644 --- a/certora/munged/governance/extensions/GovernorPreventLateQuorum.sol +++ b/certora/munged/governance/extensions/GovernorPreventLateQuorum.sol @@ -21,8 +21,8 @@ abstract contract GovernorPreventLateQuorum is Governor { using SafeCast for uint256; using Timers for Timers.BlockNumber; - uint64 private _voteExtension; - mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines; + uint64 internal _voteExtension; + mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines; /// @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 --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh new file mode 100644 index 000000000..ed102853c --- /dev/null +++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh @@ -0,0 +1,9 @@ +certoraRun \ + certora/harnesses/ERC721VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --solc solc \ + --optimistic_loop \ + --loop_iter 3 \ + --cloud \ + --rule $1 \ + --msg "GovernorPreventLateQuorum $1" \ No newline at end of file diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec new file mode 100644 index 000000000..a9b13bd45 --- /dev/null +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -0,0 +1,115 @@ +////////////////////////////////////////////////////////////////////////////// +///////////////////// Governor.sol base definitions ////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +using ERC721VotesHarness as erc20votes + +methods { + proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart + proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd + hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree + isExecuted(uint256) returns bool envfree + isCanceled(uint256) returns bool envfree + execute(address[], uint256[], bytes[], bytes32) returns uint256 + hasVoted(uint256, address) returns bool + castVote(uint256, uint8) returns uint256 + updateQuorumNumerator(uint256) + queue(address[], uint256[], bytes[], bytes32) returns uint256 + quorumNumerator() returns uint256 envfree + quorumDenominator() returns uint256 envfree + votingPeriod() returns uint256 envfree + lateQuorumVoteExtension() returns uint64 envfree + + // harness + getExtendedDeadlineIsUnset(uint256) returns bool envfree + getExtendedDeadline(uint256) returns uint64 envfree + quorumReached(uint256) returns bool envfree + latestCastVoteCall() returns uint256 envfree // more robust check than f.selector == _castVote(...).selector + + // function summarization + proposalThreshold() returns uint256 envfree + + getVotes(address, uint256) returns uint256 => DISPATCHER(true) + + getPastTotalSupply(uint256 t) returns uint256 => PER_CALLEE_CONSTANT + getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT +} + +////////////////////////////////////////////////////////////////////////////// +//////////////////////////////// Definitions ///////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +// create definition for extended +definition deadlineCanBeExtended(uint256 id) returns bool = + getExtendedDeadlineIsUnset(id) && + getExtendedDeadline(id) == 0 && + !quorumReached(id); + +definition deadlineHasBeenExtended(uint256 id) returns bool = + !getExtendedDeadlineIsUnset(id) && + getExtendedDeadline(id) > 0 && + quorumReached(id); + + + +// RULE deadline can only be extended once + // 1. if deadline changes then we have state transition from deadlineCanBeExtended to deadlineHasBeenExtended +rule deadlineChangeEffects(method f) filtered {f -> !f.isView /* bottleneck, restrict for faster testing && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } { + env e; calldataarg args; uint256 id; + + require (latestCastVoteCall() < e.block.number); + require (quorumNumerator() <= quorumDenominator()); + require deadlineCanBeExtended(id); + require (proposalDeadline(id) < e.block.number + && proposalDeadline(id) >= proposalSnapshot(id) + votingPeriod() + && proposalSnapshot(id) > e.block.number); + + uint256 deadlineBefore = proposalDeadline(id); + f(e, args); + uint256 deadlineAfter = proposalDeadline(id); + + assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(id)); +} + + // 2. cant unextend +rule deadlineCantBeUnextended(method f) filtered {f -> !f.isView /* && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } { + env e; calldataarg args; uint256 id; + require(deadlineHasBeenExtended(id)); + f(e, args); + assert(deadlineHasBeenExtended(id)); +} + + // 3. extended => can't change deadline + //@note if deadline changed, then it wasnt extended and castvote was called +rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView /* && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } { + env e; calldataarg args; + uint256 id; + require(deadlineHasBeenExtended(id)); // stays true + require (proposalDeadline(id) < e.block.number + && proposalDeadline(id) >= proposalSnapshot(id) + votingPeriod() + && proposalSnapshot(id) > e.block.number); + uint256 deadlineBefore = proposalDeadline(id); + f(e, args); + uint256 deadlineAfter = proposalDeadline(id); + assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); +} + + +// RULE deadline can only extended if quorum reached w/ <= timeOfExtension left to vote +// 3 rules + // 1. voting increases total votes + // 2. number of votes > quorum => quorum reached + // 3. deadline can only extended if quorum reached w/ <= timeOfExtension left to vote +rule deadlineCanOnlyBeExtenededIfQuorumReached() { + env e; method f; calldataarg args; + uint256 id; + require(getExtendedDeadlineIsUnset(id)); + f(e, args); + assert(false); +} + +// RULE extendedDeadline is used iff quorum is reached w/ <= extensionTime left to vote + +// RULE extendedDeadlineField is set iff quroum is reached + +// RULE if the deadline/extendedDeadline has not been reached, you can still vote (base) \ No newline at end of file