diff --git a/certora/diff/governance_Governor.sol.patch b/certora/diff/governance_Governor.sol.patch new file mode 100644 index 000000000..68710da65 --- /dev/null +++ b/certora/diff/governance_Governor.sol.patch @@ -0,0 +1,19 @@ +--- governance/Governor.sol 2023-03-07 10:48:47.730155491 +0100 ++++ governance/Governor.sol 2023-03-10 10:13:31.926616811 +0100 +@@ -216,6 +216,16 @@ + return _proposals[proposalId].proposer; + } + ++ // FV ++ function _isExecuted(uint256 proposalId) internal view returns (bool) { ++ return _proposals[proposalId].executed; ++ } ++ ++ // FV ++ function _isCanceled(uint256 proposalId) internal view returns (bool) { ++ return _proposals[proposalId].canceled; ++ } ++ + /** + * @dev Amount of votes already cast passes the threshold limit. + */ diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol index 0cb1e55d4..b869bd7dc 100644 --- a/certora/harnesses/AccessControlHarness.sol +++ b/certora/harnesses/AccessControlHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/access/AccessControl.sol"; diff --git a/certora/harnesses/ERC20FlashMintHarness.sol b/certora/harnesses/ERC20FlashMintHarness.sol index 119eb4768..39af9371f 100644 --- a/certora/harnesses/ERC20FlashMintHarness.sol +++ b/certora/harnesses/ERC20FlashMintHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/token/ERC20/ERC20.sol"; diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol index dd0aacae2..effae5f9b 100644 --- a/certora/harnesses/ERC20PermitHarness.sol +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/token/ERC20/extensions/ERC20Permit.sol"; diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol new file mode 100644 index 000000000..edc8ce67b --- /dev/null +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -0,0 +1,29 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract ERC20VotesHarness is ERC20Votes { + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} + + function mint(address account, uint256 amount) external { + _mint(account, amount); + } + + function burn(address account, uint256 amount) external { + _burn(account, amount); + } + + // inspection + function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { + return checkpoints(account, pos).fromBlock; + } + + function ckptVotes(address account, uint32 pos) public view returns (uint224) { + return checkpoints(account, pos).votes; + } + + function maxSupply() public view returns (uint224) { + return _maxSupply(); + } +} diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index 50a96cc17..2ff93e749 100644 --- a/certora/harnesses/ERC20WrapperHarness.sol +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/token/ERC20/extensions/ERC20Wrapper.sol"; diff --git a/certora/harnesses/ERC3156FlashBorrowerHarness.sol b/certora/harnesses/ERC3156FlashBorrowerHarness.sol index 0ad29a16e..c9cb829aa 100644 --- a/certora/harnesses/ERC3156FlashBorrowerHarness.sol +++ b/certora/harnesses/ERC3156FlashBorrowerHarness.sol @@ -1,9 +1,8 @@ // SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; import "../patched/interfaces/IERC3156FlashBorrower.sol"; -pragma solidity ^0.8.0; - contract ERC3156FlashBorrowerHarness is IERC3156FlashBorrower { bytes32 somethingToReturn; diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol new file mode 100644 index 000000000..ca841ea88 --- /dev/null +++ b/certora/harnesses/GovernorHarness.sol @@ -0,0 +1,160 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../patched/governance/Governor.sol"; +import "../patched/governance/extensions/GovernorCountingSimple.sol"; +import "../patched/governance/extensions/GovernorTimelockControl.sol"; +import "../patched/governance/extensions/GovernorVotes.sol"; +import "../patched/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract GovernorHarness is + Governor, + GovernorCountingSimple, + GovernorTimelockControl, + GovernorVotes, + GovernorVotesQuorumFraction +{ + constructor(IVotes _token, TimelockController _timelock, uint256 _quorumNumeratorValue) + Governor("Harness") + GovernorTimelockControl(_timelock) + GovernorVotes(_token) + GovernorVotesQuorumFraction(_quorumNumeratorValue) + {} + + // Harness from Votes + function token_getPastTotalSupply(uint256 blockNumber) public view returns(uint256) { + return token.getPastTotalSupply(blockNumber); + } + + function token_getPastVotes(address account, uint256 blockNumber) public view returns(uint256) { + return token.getPastVotes(account, blockNumber); + } + + function token_clock() public view returns (uint48) { + return token.clock(); + } + + function token_CLOCK_MODE() public view returns (string memory) { + return token.CLOCK_MODE(); + } + + // Harness from Governor + function getExecutor() public view returns (address) { + return _executor(); + } + + function proposalProposer(uint256 proposalId) public view returns (address) { + return _proposalProposer(proposalId); + } + + function quorumReached(uint256 proposalId) public view returns (bool) { + return _quorumReached(proposalId); + } + + function voteSucceeded(uint256 proposalId) public view returns (bool) { + return _voteSucceeded(proposalId); + } + + function isExecuted(uint256 proposalId) public view returns (bool) { + return _isExecuted(proposalId); + } + + function isCanceled(uint256 proposalId) public view returns (bool) { + return _isCanceled(proposalId); + } + + // Harness from GovernorCountingSimple + function getAgainstVotes(uint256 proposalId) public view returns (uint256) { + (uint256 againstVotes,,) = proposalVotes(proposalId); + return againstVotes; + } + + function getForVotes(uint256 proposalId) public view returns (uint256) { + (,uint256 forVotes,) = proposalVotes(proposalId); + return forVotes; + } + + function getAbstainVotes(uint256 proposalId) public view returns (uint256) { + (,,uint256 abstainVotes) = proposalVotes(proposalId); + return abstainVotes; + } + + /// The following functions are overrides required by Solidity added by Certora. + // mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; + // + // function _castVote( + // uint256 proposalId, + // address account, + // uint8 support, + // string memory reason, + // bytes memory params + // ) internal virtual override returns (uint256) { + // uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params); + // ghost_sum_vote_power_by_id[proposalId] += deltaWeight; + // return deltaWeight; + // } + + // 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); + } +} diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol index 4d30e5041..dd53cc6fe 100644 --- a/certora/harnesses/Ownable2StepHarness.sol +++ b/certora/harnesses/Ownable2StepHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/access/Ownable2Step.sol"; diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol index 93cbb4770..c9e06d1dc 100644 --- a/certora/harnesses/OwnableHarness.sol +++ b/certora/harnesses/OwnableHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/access/Ownable.sol"; diff --git a/certora/run.js b/certora/run.js index f3234c1a3..7623f95c6 100644 --- a/certora/run.js +++ b/certora/run.js @@ -8,26 +8,27 @@ const MAX_PARALLEL = 4; -let specs = require(__dirname + '/specs.json'); - const proc = require('child_process'); const { PassThrough } = require('stream'); const events = require('events'); const limit = require('p-limit')(MAX_PARALLEL); +const strToRegex = str => new RegExp(`^${str.replace(/[.+?^${}()|[\]\\]/g, '\\$&').replace(/[*]/g, '.$&')}$`); + let [, , request = '', ...extraOptions] = process.argv; if (request.startsWith('-')) { extraOptions.unshift(request); request = ''; } +const [reqSpec, reqContract] = request.split(':').reverse(); -if (request) { - const [reqSpec, reqContract] = request.split(':').reverse(); - specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract)); - if (specs.length === 0) { - console.error(`Error: Requested spec '${request}' not found in specs.json`); - process.exit(1); - } +const specs = require(__dirname + '/specs.js') + .filter(entry => !reqSpec || strToRegex(reqSpec).test(entry.spec)) + .filter(entry => !reqContract || strToRegex(reqContract).test(entry.contract)); + +if (specs.length === 0) { + console.error(`Error: Requested spec '${request}' not found in specs.json`); + process.exit(1); } for (const { spec, contract, files, options = [] } of Object.values(specs)) { diff --git a/certora/specs.json b/certora/specs.js similarity index 65% rename from certora/specs.json rename to certora/specs.js index 228e85fe4..1f1879246 100644 --- a/certora/specs.json +++ b/certora/specs.js @@ -1,4 +1,7 @@ -[ +/// This helper will be handy when we want to do cross product. Ex: all governor specs on all variations of the clock mode. +const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat()))); + +module.exports = [ { "spec": "AccessControl", "contract": "AccessControlHarness", @@ -45,5 +48,18 @@ "spec": "Initializable", "contract": "InitializableHarness", "files": ["certora/harnesses/InitializableHarness.sol"] - } -] + }, + ...[ "GovernorBase", "GovernorInvariants", "GovernorStates", "GovernorFunctions" ].map(spec => ({ + spec, + "contract": "GovernorHarness", + "files": [ + "certora/harnesses/GovernorHarness.sol", + "certora/harnesses/ERC20VotesHarness.sol" + ], + "options": [ + "--link GovernorHarness:token=ERC20VotesHarness", + "--optimistic_loop", + "--optimistic_hashing" + ] + })) +]; \ No newline at end of file diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec new file mode 100644 index 000000000..5f849876d --- /dev/null +++ b/certora/specs/Governor.helpers.spec @@ -0,0 +1,124 @@ +import "methods/IGovernor.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ States │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition UNSET() returns uint8 = 255; +definition PENDING() returns uint8 = 0; +definition ACTIVE() returns uint8 = 1; +definition CANCELED() returns uint8 = 2; +definition DEFEATED() returns uint8 = 3; +definition SUCCEEDED() returns uint8 = 4; +definition QUEUED() returns uint8 = 5; +definition EXPIRED() returns uint8 = 6; +definition EXECUTED() returns uint8 = 7; + +function safeState(env e, uint256 pId) returns uint8 { + uint8 result = state@withrevert(e, pId); + return lastReverted ? UNSET() : result; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Filters │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition skip(method f) returns bool = + f.isView || + f.isFallback || + f.selector == relay(address,uint256,bytes).selector || + f.selector == 0xb9a61961 || // __acceptAdmin() + f.selector == onERC721Received(address,address,uint256,bytes).selector || + f.selector == onERC1155Received(address,address,uint256,uint256,bytes).selector || + f.selector == onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector; + +definition voting(method f) returns bool = + f.selector == castVote(uint256,uint8).selector || + f.selector == castVoteWithReason(uint256,uint8,string).selector || + f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Helper functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 support) returns uint256 { + string reason; bytes params; uint8 v; bytes32 s; bytes32 r; + + if (f.selector == castVote(uint256,uint8).selector) + { + require e.msg.sender == voter; + return castVote@withrevert(e, pId, support); + } + else if (f.selector == castVoteWithReason(uint256,uint8,string).selector) + { + require e.msg.sender == voter; + return castVoteWithReason@withrevert(e, pId, support, reason); + } + else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) + { + require e.msg.sender == voter; + return castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params); + } + else + { + calldataarg args; + f@withrevert(e, args); + return 0; + } +} + +function helperFunctionsWithRevert(env e, method f, uint256 pId) { + if (f.selector == propose(address[], uint256[], bytes[], string).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; string description; + require pId == propose@withrevert(e, targets, values, calldatas, description); + } + else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 description; + require pId == queue@withrevert(e, targets, values, calldatas, description); + } + else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 description; + require pId == execute@withrevert(e, targets, values, calldatas, description); + } + else if (f.selector == cancel(address[], uint256[], bytes[], bytes32).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 description; + require pId == cancel@withrevert(e, targets, values, calldatas, description); + } + else if (f.selector == castVote(uint256, uint8).selector) + { + uint8 support; + castVote@withrevert(e, pId, support); + } + else if (f.selector == castVoteWithReason(uint256, uint8, string).selector) + { + uint8 support; string reason; + castVoteWithReason@withrevert(e, pId, support, reason); + } + else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) + { + uint8 support; string reason; bytes params; + castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params); + } + else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) + { + uint8 support; uint8 v; bytes32 r; bytes32 s; + castVoteBySig@withrevert(e, pId, support, v, r, s); + } + else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) + { + uint8 support; string reason; bytes params; uint8 v; bytes32 r; bytes32 s; + castVoteWithReasonAndParamsBySig@withrevert(e, pId, support, reason, params, v, r, s); + } + else + { + calldataarg args; + f@withrevert(e, args); + } +} \ No newline at end of file diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec new file mode 100644 index 000000000..977993980 --- /dev/null +++ b/certora/specs/GovernorBase.spec @@ -0,0 +1,250 @@ +import "methods/IGovernor.spec" +import "Governor.helpers.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Definitions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +definition proposalCreated(uint256 pId) returns bool = + proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Votes start and end are either initialized (non zero) or uninitialized (zero) simultaneously │ +│ │ +│ This invariant assumes that the block number cannot be 0 at any stage of the contract cycle │ +│ This is very safe assumption as usually the 0 block is genesis block which is uploaded with data │ +│ by the developers and will not be valid to raise proposals (at the current way that block chain is functioning) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant proposalStateConsistency(uint256 pId) + (proposalProposer(pId) != 0 <=> proposalSnapshot(pId) != 0) && (proposalProposer(pId) != 0 <=> proposalDeadline(pId) != 0) + { + preserved with (env e) { + require clock(e) > 0; + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: cancel => created │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant canceledImplyCreated(uint pId) + isCanceled(pId) => proposalCreated(pId) + { + preserved with (env e) { + requireInvariant proposalStateConsistency(pId); + require clock(e) > 0; + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: executed => created │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant executedImplyCreated(uint pId) + isExecuted(pId) => proposalCreated(pId) + { + preserved with (env e) { + requireInvariant proposalStateConsistency(pId); + require clock(e) > 0; + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Votes start before it ends │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant voteStartBeforeVoteEnd(uint256 pId) + proposalSnapshot(pId) <= proposalDeadline(pId) + { + preserved { + requireInvariant proposalStateConsistency(pId); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: A proposal cannot be both executed and canceled simultaneously │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant noBothExecutedAndCanceled(uint256 pId) + !isExecuted(pId) || !isCanceled(pId) + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: No double proposition │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noDoublePropose(uint256 pId, env e) { + require proposalCreated(pId); + + address[] targets; uint256[] values; bytes[] calldatas; string reason; + uint256 result = propose(e, targets, values, calldatas, reason); + + assert result != pId, "double proposal"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg) { + require proposalCreated(pId); + + uint256 voteStart = proposalSnapshot(pId); + uint256 voteEnd = proposalDeadline(pId); + address proposer = proposalProposer(pId); + + f(e, arg); + + assert voteStart == proposalSnapshot(pId), "Start date was changed"; + assert voteEnd == proposalDeadline(pId), "End date was changed"; + assert proposer == proposalProposer(pId), "Proposer was changed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: A user cannot vote twice │ +│ │ +│ Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is │ +│ counted on the fact that the 3 functions themselves makes no changes, but rather call an internal function to │ +│ execute. That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it │ +│ is quite trivial to understand why this is ok. For castVoteBySig we basically assume that the signature referendum │ +│ is correct without checking it. We could check each function separately and pass the rule, but that would have │ +│ uglyfied the code with no concrete benefit, as it is evident that nothing is happening in the first 2 functions │ +│ (calling a view function), and we do not desire to check the signature verification. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noDoubleVoting(uint256 pId, env e, uint8 sup) { + bool votedCheck = hasVoted(pId, e.msg.sender); + + castVote@withrevert(e, pId, sup); + + assert votedCheck => lastReverted, "double voting occurred"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: A proposal could be executed only if quorum was reached and vote succeeded │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, calldataarg args) { + require !isExecuted(pId); + + bool quorumReachedBefore = quorumReached(pId); + bool voteSucceededBefore = voteSucceeded(pId); + + f(e, args); + + assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Voting cannot start at a block number prior to proposal’s creation block number │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noStartBeforeCreation(uint256 pId, env e, method f, calldataarg args){ + require !proposalCreated(pId); + f(e, args); + assert proposalCreated(pId) => proposalSnapshot(pId) >= clock(e), "starts before proposal"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: A proposal cannot be executed before it ends │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) { + require !isExecuted(pId); + f(e, args); + assert isExecuted(pId) => proposalDeadline(pId) <= clock(e), "executed before deadline"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: All proposal specific (non-view) functions should revert if proposal is executed │ +│ │ +│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, non of the │ +│ proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc we connected the executed │ +│ attribute to the execute() function, showing that only execute() can change it, and that it will always change it. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args) filtered { + f -> !f.isView && !f.isFallback + && f.selector != updateTimelock(address).selector + && f.selector != updateQuorumNumerator(uint256).selector + && f.selector != relay(address,uint256,bytes).selector + && f.selector != 0xb9a61961 // __acceptAdmin() + && f.selector != onERC721Received(address,address,uint256,bytes).selector + && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector + && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector +} { + require isExecuted(pId); + requireInvariant noBothExecutedAndCanceled(pId); + requireInvariant executedImplyCreated(pId); + + helperFunctionsWithRevert(pId, f, e); + + assert lastReverted, "Function was not reverted"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: All proposal specific (non-view) functions should revert if proposal is canceled │ +│ │ +│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, non of the │ +│ proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc we connected the executed │ +│ attribute to the execute() function, showing that only execute() can change it, and that it will always change it. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args) filtered { + f -> !f.isView && !f.isFallback + && f.selector != updateTimelock(address).selector + && f.selector != updateQuorumNumerator(uint256).selector + && f.selector != relay(address,uint256,bytes).selector + && f.selector != 0xb9a61961 // __acceptAdmin() + && f.selector != onERC721Received(address,address,uint256,bytes).selector + && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector + && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector +} { + require isCanceled(pId); + requireInvariant noBothExecutedAndCanceled(pId); + requireInvariant canceledImplyCreated(pId); + + helperFunctionsWithRevert(pId, f, e); + + assert lastReverted, "Function was not reverted"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Proposal can be switched state only by specific functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateOnlyAfterFunc(uint256 pId, env e, method f) { + bool createdBefore = proposalCreated(pId); + bool executedBefore = isExecuted(pId); + bool canceledBefore = isCanceled(pId); + + helperFunctionsWithRevert(pId, f, e); + + assert (proposalCreated(pId) != createdBefore) + => (createdBefore == false && f.selector == propose(address[], uint256[], bytes[], string).selector), + "proposalCreated only changes in the propose method"; + + assert (isExecuted(pId) != executedBefore) + => (executedBefore == false && f.selector == execute(address[], uint256[], bytes[], bytes32).selector), + "isExecuted only changes in the execute method"; + + assert (isCanceled(pId) != canceledBefore) + => (canceledBefore == false && f.selector == cancel(address[], uint256[], bytes[], bytes32).selector), + "isCanceled only changes in the cancel method"; +} diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec new file mode 100644 index 000000000..40ad27213 --- /dev/null +++ b/certora/specs/GovernorFunctions.spec @@ -0,0 +1,97 @@ +import "helpers.spec" +import "methods/IGovernor.spec" +import "Governor.helpers.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: propose effect and liveness. Includes "no double proposition" │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule propose(uint256 pId, env e) { + require nonpayable(e); + + uint256 otherId; + + uint8 stateBefore = state(e, pId); + uint8 otherStateBefore = state(e, otherId); + uint256 otherVoteStart = proposalSnapshot(otherId); + uint256 otherVoteEnd = proposalDeadline(otherId); + address otherProposer = proposalProposer(otherId); + + address[] targets; uint256[] values; bytes[] calldatas; string reason; + require pId == propose@withrevert(e, targets, values, calldatas, reason); + bool success = !lastReverted; + + // liveness & double proposal + assert success <=> stateBefore == UNSET(); + + // effect + assert success => ( + state(e, pId) == PENDING() && + proposalProposer(pId) == e.msg.sender && + proposalSnapshot(pId) == clock(e) + votingDelay() && + proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod() + ); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; + assert proposalSnapshot(otherId) == otherVoteStart; + assert proposalDeadline(otherId) == otherVoteEnd; + assert proposalProposer(otherId) == otherProposer; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: votes effect and liveness. Includes "A user cannot vote twice" │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule castVote(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + require nonpayable(e); + + uint8 support; + address voter; + address otherVoter; + uint256 otherId; + + uint8 stateBefore = state(e, pId); + bool hasVotedBefore = hasVoted(pId, voter); + bool otherVotedBefore = hasVoted(otherId, otherVoter); + uint256 againstVotesBefore = getAgainstVotes(pId); + uint256 forVotesBefore = getForVotes(pId); + uint256 abstainVotesBefore = getAbstainVotes(pId); + uint256 otherAgainstVotesBefore = getAgainstVotes(otherId); + uint256 otherForVotesBefore = getForVotes(otherId); + uint256 otherAbstainVotesBefore = getAbstainVotes(otherId); + + // voting weight overflow check + uint256 voterWeight = token_getPastVotes(voter, proposalSnapshot(pId)); + require againstVotesBefore + voterWeight <= max_uint256; + require forVotesBefore + voterWeight <= max_uint256; + require abstainVotesBefore + voterWeight <= max_uint256; + + uint256 weight = helperVoteWithRevert(e, f, pId, voter, support); + bool success = !lastReverted; + + assert success <=> ( + stateBefore == ACTIVE() && + !hasVotedBefore && + (support == 0 || support == 1 || support == 2) + ); + + assert success => ( + state(e, pId) == ACTIVE() && + voterWeight == weight && + getAgainstVotes(pId) == againstVotesBefore + (support == 0 ? weight : 0) && + getForVotes(pId) == forVotesBefore + (support == 1 ? weight : 0) && + getAbstainVotes(pId) == abstainVotesBefore + (support == 2 ? weight : 0) && + hasVoted(pId, voter) + ); + + // no side-effect + assert hasVoted(otherId, otherVoter) != otherVotedBefore => (otherId == pId && otherVoter == voter); + assert getAgainstVotes(otherId) != otherAgainstVotesBefore => (otherId == pId); + assert getForVotes(otherId) != otherForVotesBefore => (otherId == pId); + assert getAbstainVotes(otherId) != otherAbstainVotesBefore => (otherId == pId); +} diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec new file mode 100644 index 000000000..a8a200ca3 --- /dev/null +++ b/certora/specs/GovernorInvariants.spec @@ -0,0 +1,72 @@ +import "helpers.spec" +import "methods/IGovernor.spec" +import "Governor.helpers.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: clock is consistent between the goernor and the token │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule clockMode(env e) { + assert clock(e) == e.block.number || clock(e) == e.block.timestamp; + assert clock(e) == token_clock(e); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Proposal is UNSET iff the proposer, the snapshot and the deadline are unset. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant createdConsistency(env e, uint256 pId) + safeState(e, pId) == UNSET() <=> proposalProposer(pId) == 0 && + safeState(e, pId) == UNSET() <=> proposalSnapshot(pId) == 0 && + safeState(e, pId) == UNSET() <=> proposalDeadline(pId) == 0 && + safeState(e, pId) == UNSET() => !isExecuted(pId) && + safeState(e, pId) == UNSET() => !isCanceled(pId) + { + preserved { + require clock(e) > 0; + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Votes start before it ends │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant voteStartBeforeVoteEnd(uint256 pId) + proposalSnapshot(pId) <= proposalDeadline(pId) + { + preserved with (env e) { + requireInvariant createdConsistency(e, pId); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: A proposal cannot be both executed and canceled simultaneously │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant noBothExecutedAndCanceled(uint256 pId) + !isExecuted(pId) || !isCanceled(pId) + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg) + filtered { f -> !skip(f) } +{ + require state(e, pId) != UNSET(); + + uint256 voteStart = proposalSnapshot(pId); + uint256 voteEnd = proposalDeadline(pId); + address proposer = proposalProposer(pId); + + f(e, arg); + + assert voteStart == proposalSnapshot(pId), "Start date was changed"; + assert voteEnd == proposalDeadline(pId), "End date was changed"; + assert proposer == proposalProposer(pId), "Proposer was changed"; +} diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec new file mode 100644 index 000000000..d2ddf9947 --- /dev/null +++ b/certora/specs/GovernorStates.spec @@ -0,0 +1,212 @@ +import "helpers.spec" +import "methods/IGovernor.spec" +import "Governor.helpers.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: state returns one of the value in the enumeration │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateConsistency(env e, uint256 pId) { + uint8 result = state(e, pId); + assert ( + result == PENDING() || + result == ACTIVE() || + result == CANCELED() || + result == DEFEATED() || + result == SUCCEEDED() || + result == QUEUED() || + result == EXECUTED() + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: State transition │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !skip(f) } +{ + require clock(e) > 0; // Sanity + + uint8 stateBefore = state(e, pId); + f(e, args); + uint8 stateAfter = state(e, pId); + + assert (stateBefore != stateAfter) => ( + stateBefore == UNSET() => ( + stateAfter == PENDING() && f.selector == propose(address[],uint256[],bytes[],string).selector + ) && + stateBefore == PENDING() => ( + (stateAfter == CANCELED() && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector) + ) && + stateBefore == SUCCEEDED() => ( + (stateAfter == QUEUED() && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) || + (stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) + ) && + stateBefore == QUEUED() => ( + (stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) + ) && + stateBefore == ACTIVE() => false && + stateBefore == CANCELED() => false && + stateBefore == DEFEATED() => false && + stateBefore == EXECUTED() => false + ); +} + +rule stateTransitionWait(uint256 pId, env e1, env e2) { + require clock(e1) > 0; // Sanity + require clock(e2) > clock(e1); + + uint8 stateBefore = state(e1, pId); + uint8 stateAfter = state(e2, pId); + + assert (stateBefore != stateAfter) => ( + stateBefore == PENDING() => ( + stateAfter == ACTIVE() + ) && + stateBefore == ACTIVE() => ( + stateAfter == SUCCEEDED() || + stateAfter == DEFEATED() + ) && + stateBefore == UNSET() => false && + stateBefore == SUCCEEDED() => false && + stateBefore == QUEUED() => false && + stateBefore == CANCELED() => false && + stateBefore == DEFEATED() => false && + stateBefore == EXECUTED() => false + ); +} + + + + + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg) + filtered { f -> !skip(f) } +{ + require state(e, pId) != UNSET(); + + uint256 voteStart = proposalSnapshot(pId); + uint256 voteEnd = proposalDeadline(pId); + address proposer = proposalProposer(pId); + + f(e, arg); + + assert voteStart == proposalSnapshot(pId), "Start date was changed"; + assert voteEnd == proposalDeadline(pId), "End date was changed"; + assert proposer == proposalProposer(pId), "Proposer was changed"; +} + + + + + + + + + + + + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: propose effect and liveness. Includes "no double proposition" │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule propose(uint256 pId, env e) { + require nonpayable(e); + + uint256 otherId; + + uint8 stateBefore = state(e, pId); + uint8 otherStateBefore = state(e, otherId); + uint256 otherVoteStart = proposalSnapshot(otherId); + uint256 otherVoteEnd = proposalDeadline(otherId); + address otherProposer = proposalProposer(otherId); + + address[] targets; uint256[] values; bytes[] calldatas; string reason; + require pId == propose@withrevert(e, targets, values, calldatas, reason); + bool success = !lastReverted; + + // liveness & double proposal + assert success <=> stateBefore == UNSET(); + + // effect + assert success => ( + state(e, pId) == PENDING() && + proposalProposer(pId) == e.msg.sender && + proposalSnapshot(pId) == clock(e) + votingDelay() && + proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod() + ); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; + assert proposalSnapshot(otherId) == otherVoteStart; + assert proposalDeadline(otherId) == otherVoteEnd; + assert proposalProposer(otherId) == otherProposer; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: votes effect and liveness. Includes "A user cannot vote twice" │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule castVote(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + require nonpayable(e); + + uint8 support; + address voter; + address otherVoter; + uint256 otherId; + + uint8 stateBefore = state(e, pId); + bool hasVotedBefore = hasVoted(pId, voter); + bool otherVotedBefore = hasVoted(otherId, otherVoter); + uint256 againstVotesBefore = getAgainstVotes(pId); + uint256 forVotesBefore = getForVotes(pId); + uint256 abstainVotesBefore = getAbstainVotes(pId); + uint256 otherAgainstVotesBefore = getAgainstVotes(otherId); + uint256 otherForVotesBefore = getForVotes(otherId); + uint256 otherAbstainVotesBefore = getAbstainVotes(otherId); + + // voting weight overflow check + uint256 voterWeight = token_getPastVotes(voter, proposalSnapshot(pId)); + require againstVotesBefore + voterWeight <= max_uint256; + require forVotesBefore + voterWeight <= max_uint256; + require abstainVotesBefore + voterWeight <= max_uint256; + + uint256 weight = helperVoteWithRevert(e, f, pId, voter, support); + bool success = !lastReverted; + + assert success <=> ( + stateBefore == ACTIVE() && + !hasVotedBefore && + (support == 0 || support == 1 || support == 2) + ); + + assert success => ( + state(e, pId) == ACTIVE() && + voterWeight == weight && + getAgainstVotes(pId) == againstVotesBefore + (support == 0 ? weight : 0) && + getForVotes(pId) == forVotesBefore + (support == 1 ? weight : 0) && + getAbstainVotes(pId) == abstainVotesBefore + (support == 2 ? weight : 0) && + hasVoted(pId, voter) + ); + + // no side-effect + assert hasVoted(otherId, otherVoter) != otherVotedBefore => (otherId == pId && otherVoter == voter); + assert getAgainstVotes(otherId) != otherAgainstVotesBefore => (otherId == pId); + assert getForVotes(otherId) != otherForVotesBefore => (otherId == pId); + assert getAbstainVotes(otherId) != otherAbstainVotesBefore => (otherId == pId); +} diff --git a/certora/specs/methods/IGovernor.spec b/certora/specs/methods/IGovernor.spec new file mode 100644 index 000000000..53f43b713 --- /dev/null +++ b/certora/specs/methods/IGovernor.spec @@ -0,0 +1,45 @@ +// includes some non standard (from extension) and harness functions +methods { + name() returns string envfree + version() returns string envfree + clock() returns uint48 + CLOCK_MODE() returns string + COUNTING_MODE() returns string envfree + hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree + state(uint256) returns uint8 + proposalThreshold() returns uint256 envfree + proposalSnapshot(uint256) returns uint256 envfree + proposalDeadline(uint256) returns uint256 envfree + votingDelay() returns uint256 envfree + votingPeriod() returns uint256 envfree + quorum(uint256) returns uint256 envfree + getVotes(address,uint256) returns uint256 envfree + getVotesWithParams(address,uint256,bytes) returns uint256 envfree + hasVoted(uint256,address) returns bool envfree + + propose(address[],uint256[],bytes[],string) returns uint256 + execute(address[],uint256[],bytes[],bytes32) returns uint256 + queue(address[], uint256[], bytes[], bytes32) returns uint256 + cancel(address[],uint256[],bytes[],bytes32) returns uint256 + castVote(uint256,uint8) returns uint256 + castVoteWithReason(uint256,uint8,string) returns uint256 + castVoteWithReasonAndParams(uint256,uint8,string,bytes) returns uint256 + castVoteBySig(uint256,uint8,uint8,bytes32,bytes32) returns uint256 + castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32) returns uint256 + updateQuorumNumerator(uint256) + + // harness + token_getPastTotalSupply(uint256) returns uint256 envfree + token_getPastVotes(address,uint256) returns uint256 envfree + token_clock() returns uint48 + token_CLOCK_MODE() returns string + getExecutor() returns address envfree + proposalProposer(uint256) returns address envfree + quorumReached(uint256) returns bool envfree + voteSucceeded(uint256) returns bool envfree + isExecuted(uint256) returns bool envfree + isCanceled(uint256) returns bool envfree + getAgainstVotes(uint256) returns uint256 envfree + getForVotes(uint256) returns uint256 envfree + getAbstainVotes(uint256) returns uint256 envfree +} \ No newline at end of file