diff --git a/certora/diff/governance_Governor.sol.patch b/certora/diff/governance_Governor.sol.patch index 68710da65..e3ad3e9b3 100644 --- a/certora/diff/governance_Governor.sol.patch +++ b/certora/diff/governance_Governor.sol.patch @@ -1,6 +1,6 @@ --- 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 @@ ++++ governance/Governor.sol 2023-03-13 14:07:30.704202049 +0100 +@@ -216,6 +216,21 @@ return _proposals[proposalId].proposer; } @@ -13,6 +13,11 @@ + function _isCanceled(uint256 proposalId) internal view returns (bool) { + return _proposals[proposalId].canceled; + } ++ ++ // FV ++ function _governanceCallLength() public view returns (uint256) { ++ return _governanceCall.length(); ++ } + /** * @dev Amount of votes already cast passes the threshold limit. diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch new file mode 100644 index 000000000..312fc4ff6 --- /dev/null +++ b/certora/diff/token_ERC721_ERC721.sol.patch @@ -0,0 +1,14 @@ +--- token/ERC721/ERC721.sol 2023-03-07 10:48:47.736822221 +0100 ++++ token/ERC721/ERC721.sol 2023-03-09 19:50:20.555856358 +0100 +@@ -199,6 +199,11 @@ + return _owners[tokenId]; + } + ++ // FV ++ function _getApproved(uint256 tokenId) internal view returns (address) { ++ return _tokenApprovals[tokenId]; ++ } ++ + /** + * @dev Returns whether `tokenId` exists. + * diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol index ca841ea88..52a09416d 100644 --- a/certora/harnesses/GovernorHarness.sol +++ b/certora/harnesses/GovernorHarness.sol @@ -64,6 +64,10 @@ contract GovernorHarness is return _isCanceled(proposalId); } + function governanceCallLength() public view returns (uint256) { + return _governanceCallLength(); + } + // Harness from GovernorCountingSimple function getAgainstVotes(uint256 proposalId) public view returns (uint256) { (uint256 againstVotes,,) = proposalVotes(proposalId); diff --git a/certora/run.js b/certora/run.js index 175cedd88..50e8a1dcf 100644 --- a/certora/run.js +++ b/certora/run.js @@ -22,14 +22,15 @@ if (request.startsWith('-')) { const [reqSpec, reqContract] = request.split(':').reverse(); const specs = require(__dirname + '/specs.js') - .filter(entry => !reqSpec || micromatch(entry.spec, reqSpec)) - .filter(entry => !reqContract || micromatch(entry.contract, reqContract)); + .filter(entry => !reqSpec || micromatch.isMatch(entry.spec, reqSpec)) + .filter(entry => !reqContract || micromatch.isMatch(entry.contract, reqContract)); if (specs.length === 0) { console.error(`Error: Requested spec '${request}' not found in specs.json`); process.exit(1); } +console.table(specs.map(spec => `${spec.contract}:${spec.spec} ${spec.options.join(' ')}`)) for (const { spec, contract, files, options = [] } of Object.values(specs)) { limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]); } diff --git a/certora/specs.js b/certora/specs.js index 3df135200..630865542 100644 --- a/certora/specs.js +++ b/certora/specs.js @@ -1,6 +1,7 @@ const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat()))); module.exports = [ + // AccessControl { spec: 'AccessControl', contract: 'AccessControlHarness', @@ -16,6 +17,7 @@ module.exports = [ contract: 'Ownable2StepHarness', files: ['certora/harnesses/Ownable2StepHarness.sol'], }, + // Tokens { spec: 'ERC20', contract: 'ERC20PermitHarness', @@ -34,13 +36,15 @@ module.exports = [ files: ['certora/harnesses/ERC20PermitHarness.sol', 'certora/harnesses/ERC20WrapperHarness.sol'], options: ['--link ERC20WrapperHarness:_underlying=ERC20PermitHarness', '--optimistic_loop'], }, + // Proxy { spec: 'Initializable', contract: 'InitializableHarness', files: ['certora/harnesses/InitializableHarness.sol'], }, + // Governor ...product( - ['GovernorBase', 'GovernorInvariants', 'GovernorStates', /*'GovernorFunctions'*/], + ['GovernorInvariants', 'GovernorBaseRules', 'GovernorStates'], ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'], ).map(([spec, token]) => ({ spec, @@ -48,4 +52,14 @@ module.exports = [ files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`], options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'], })), + // WIP part + // ...product( + // ['GovernorFunctions'], + // ['ERC20VotesBlocknumberHarness'], + // ).map(([spec, token]) => ({ + // spec, + // contract: 'GovernorHarness', + // files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`], + // options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'], + // })), ]; diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec index bd6b4b3fc..f43e5606f 100644 --- a/certora/specs/Governor.helpers.spec +++ b/certora/specs/Governor.helpers.spec @@ -20,6 +20,9 @@ function safeState(env e, uint256 pId) returns uint8 { return lastReverted ? UNSET() : result; } +definition proposalCreated(uint256 pId) returns bool = + proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0; + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Filters │ diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBaseRules.spec similarity index 62% rename from certora/specs/GovernorBase.spec rename to certora/specs/GovernorBaseRules.spec index 6f4fcab93..3063adae4 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBaseRules.spec @@ -1,80 +1,11 @@ import "methods/IGovernor.spec" import "Governor.helpers.spec" +import "GovernorInvariants.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) +use invariant proposalStateConsistency +use invariant canceledImplyCreated +use invariant executedImplyCreated +use invariant noBothExecutedAndCanceled /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -143,7 +74,7 @@ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, f(e, args); - assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed"; + assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum not met or vote not succesfull"; } /* @@ -216,21 +147,24 @@ rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule stateOnlyAfterFunc(uint256 pId, env e, method f) { - bool createdBefore = proposalCreated(pId); + bool createdBefore = proposalCreated(pId); bool executedBefore = isExecuted(pId); bool canceledBefore = isCanceled(pId); helperFunctionsWithRevert(e, f, pId); - assert (proposalCreated(pId) != createdBefore) - => (createdBefore == false && f.selector == propose(address[], uint256[], bytes[], string).selector), - "proposalCreated only changes in the propose method"; + 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 (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"; + 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 index 40ad27213..ec50c044a 100644 --- a/certora/specs/GovernorFunctions.spec +++ b/certora/specs/GovernorFunctions.spec @@ -95,3 +95,79 @@ rule castVote(uint256 pId, env e, method f) assert getForVotes(otherId) != otherForVotesBefore => (otherId == pId); assert getAbstainVotes(otherId) != otherAbstainVotesBefore => (otherId == pId); } + + +rule queue(uint256 pId, env e) { + require nonpayable(e); + + uint256 otherId; + + uint8 stateBefore = state(e, pId); + uint8 otherStateBefore = state(e, otherId); + + address[] targets; uint256[] values; bytes[] calldatas; string reason; + require pId == queue@withrevert(e, targets, values, calldatas, reason); + bool success = !lastReverted; + + // liveness + assert success <=> stateBefore == SUCCEEDED(); + + // effect + assert success => ( + state(e, pId) == QUEUED() + ); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; +} + +rule execute(uint256 pId, env e) { + require nonpayable(e); + + uint256 otherId; + + uint8 stateBefore = state(e, pId); + uint8 otherStateBefore = state(e, otherId); + + address[] targets; uint256[] values; bytes[] calldatas; string reason; + require pId == execute@withrevert(e, targets, values, calldatas, reason); + bool success = !lastReverted; + + // liveness: can't check full equivalence because of execution call reverts + assert success => (stateBefore == SUCCEEDED() || stateBefore == QUEUED()); + + // effect + assert success => ( + state(e, pId) == EXECUTED() + ); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; +} + +rule cancel(uint256 pId, env e) { + require nonpayable(e); + + uint256 otherId; + + uint8 stateBefore = state(e, pId); + uint8 otherStateBefore = state(e, otherId); + + address[] targets; uint256[] values; bytes[] calldatas; string reason; + require pId == cancel@withrevert(e, targets, values, calldatas, reason); + bool success = !lastReverted; + + // liveness + assert success <=> ( + stateBefore == PENDING() && + e.msg.sender == proposalProposer(pId) + ); + + // effect + assert success => ( + state(e, pId) == CANCELED() + ); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; +} \ No newline at end of file diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec index 223f504b9..dfe95e81f 100644 --- a/certora/specs/GovernorInvariants.spec +++ b/certora/specs/GovernorInvariants.spec @@ -8,32 +8,70 @@ import "Governor.helpers.spec" └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule clockMode(env e) { + require e.block.number < max_uint48() && e.block.timestamp < max_uint48(); + assert clock(e) == e.block.number || clock(e) == e.block.timestamp; assert clock(e) == token_clock(e); + + /// This causes a failure in the prover + // assert CLOCK_MODE(e) == token_CLOCK_MODE(e); } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: Proposal is UNSET iff the proposer, the snapshot and the deadline are unset. │ +│ 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 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) +invariant proposalStateConsistency(uint256 pId) + (proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0) && + (proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0) { - preserved { + preserved with (env e) { require clock(e) > 0; } } -invariant createdConsistencyWeak(uint256 pId) - proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0 && - proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 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: The state UNSET() correctly catched uninitialized proposal. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant proposalStateConsistencyUnset(env e, uint256 pId) + proposalCreated(pId) <=> safeState(e, pId) == UNSET() + { + preserved { require clock(e) > 0; } } @@ -47,7 +85,7 @@ invariant voteStartBeforeVoteEnd(uint256 pId) proposalSnapshot(pId) <= proposalDeadline(pId) { preserved { - requireInvariant createdConsistencyWeak(pId); + requireInvariant proposalStateConsistency(pId); } } @@ -61,21 +99,8 @@ invariant noBothExecutedAndCanceled(uint256 pId) /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable │ +│ Invariant: the "governance call" dequeue is empty │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -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"; -} +invariant governanceCallLength() + governanceCallLength() == 0 \ No newline at end of file diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index b7737ce24..0e548b6e6 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -1,6 +1,9 @@ import "helpers.spec" import "methods/IGovernor.spec" import "Governor.helpers.spec" +import "GovernorInvariants.spec" + +use invariant proposalStateConsistency /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -78,3 +81,45 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) { stateBefore == EXECUTED() => false ); } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: State corresponds to the vote timming and results │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateFollowsVoteTimmingAndResult(uint256 pId, env e) { + require clock(e) > 0; // Sanity + requireInvariant proposalStateConsistency(pId); + + uint8 currentState = state(e, pId); + uint48 currentClock = clock(e); + + // Pending = before vote starts + assert currentState == PENDING() => ( + proposalSnapshot(pId) >= currentClock + ); + + // Active = after vote starts & before vote ends + assert currentState == ACTIVE() => ( + proposalSnapshot(pId) < currentClock && + proposalDeadline(pId) >= currentClock + ); + + // Succeeded = after vote end, with vote successfull and quorum reached + assert currentState == SUCCEEDED() => ( + proposalDeadline(pId) < currentClock && + ( + quorumReached(pId) && + voteSucceeded(pId) + ) + ); + + // Succeeded = after vote end, with vote not successfull or quorum not reached + assert currentState == DEFEATED() => ( + proposalDeadline(pId) < currentClock && + ( + !quorumReached(pId) || + !voteSucceeded(pId) + ) + ); +} diff --git a/certora/specs/helpers.spec b/certora/specs/helpers.spec index 24842d62f..20a11336e 100644 --- a/certora/specs/helpers.spec +++ b/certora/specs/helpers.spec @@ -1 +1,3 @@ definition nonpayable(env e) returns bool = e.msg.value == 0; + +definition max_uint48() returns uint48 = 0xffffffffffff; \ No newline at end of file diff --git a/certora/specs/methods/IGovernor.spec b/certora/specs/methods/IGovernor.spec index 53f43b713..ea0308c18 100644 --- a/certora/specs/methods/IGovernor.spec +++ b/certora/specs/methods/IGovernor.spec @@ -39,6 +39,7 @@ methods { voteSucceeded(uint256) returns bool envfree isExecuted(uint256) returns bool envfree isCanceled(uint256) returns bool envfree + governanceCallLength() returns uint256 envfree getAgainstVotes(uint256) returns uint256 envfree getForVotes(uint256) returns uint256 envfree getAbstainVotes(uint256) returns uint256 envfree diff --git a/requirements.txt b/requirements.txt index 797b3598d..da3e95766 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1 @@ -certora-cli==3.6.3 +certora-cli==3.6.4