diff --git a/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch index 57e213f34..f1688e2ab 100644 --- a/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch +++ b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch @@ -1,5 +1,14 @@ --- governance/extensions/GovernorTimelockControl.sol 2023-03-14 15:48:49.307543354 +0100 -+++ governance/extensions/GovernorTimelockControl.sol 2023-03-14 22:09:12.661420438 +0100 ++++ governance/extensions/GovernorTimelockControl.sol 2023-03-16 16:01:13.857331689 +0100 +@@ -24,7 +24,7 @@ + * _Available since v4.3._ + */ + abstract contract GovernorTimelockControl is IGovernorTimelock, Governor { +- TimelockController private _timelock; ++ TimelockController public _timelock; // FV: public for link + mapping(uint256 => bytes32) private _timelockIds; + + /** @@ -84,6 +84,11 @@ return eta == 1 ? 0 : eta; // _DONE_TIMESTAMP (1) should be replaced with a 0 value } diff --git a/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch b/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch index 39a1a0c90..98d3b25d2 100644 --- a/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch +++ b/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch @@ -1,5 +1,5 @@ --- governance/extensions/GovernorVotesQuorumFraction.sol 2023-03-07 10:48:47.733488857 +0100 -+++ governance/extensions/GovernorVotesQuorumFraction.sol 2023-03-15 22:51:51.267890807 +0100 ++++ governance/extensions/GovernorVotesQuorumFraction.sol 2023-03-15 22:52:06.424537201 +0100 @@ -62,6 +62,11 @@ return _quorumNumeratorHistory.upperLookupRecent(timepoint.toUint32()); } diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol index e758d3810..d3494d66b 100644 --- a/certora/harnesses/GovernorHarness.sol +++ b/certora/harnesses/GovernorHarness.sol @@ -40,6 +40,10 @@ contract GovernorHarness is } // Harness from Governor + function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public returns (uint256) { + return hashProposal(targets, values, calldatas, keccak256(bytes(description))); + } + function getExecutor() public view returns (address) { return _executor(); } diff --git a/certora/harnesses/GovernorPreventLateHarness.sol b/certora/harnesses/GovernorPreventLateHarness.sol index 048ceae3c..a4b1ca3f7 100644 --- a/certora/harnesses/GovernorPreventLateHarness.sol +++ b/certora/harnesses/GovernorPreventLateHarness.sol @@ -43,6 +43,10 @@ contract GovernorPreventLateHarness is } // Harness from Governor + function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public returns (uint256) { + return hashProposal(targets, values, calldatas, keccak256(bytes(description))); + } + function getExecutor() public view returns (address) { return _executor(); } diff --git a/certora/specs.js b/certora/specs.js index aac07123c..ba466b957 100644 --- a/certora/specs.js +++ b/certora/specs.js @@ -59,18 +59,41 @@ module.exports = [].concat( ).map(([contract, spec, token]) => ({ spec, contract, - files: [`certora/harnesses/${contract}.sol`, `certora/harnesses/${token}.sol`], - options: [`--link ${contract}:token=${token}`, '--optimistic_loop', '--optimistic_hashing'], + files: [ + `certora/harnesses/${contract}.sol`, + `certora/harnesses/${token}.sol`, + `certora/harnesses/TimelockControllerHarness.sol`, + ], + options: [ + `--link ${contract}:token=${token}`, + `--link ${contract}:_timelock=TimelockControllerHarness`, + '--optimistic_loop', + '--optimistic_hashing', + ], })), /// WIP part process.env.CI ? [] - : product(['GovernorHarness'], ['GovernorFunctions'], ['ERC20VotesBlocknumberHarness']).map( - ([contract, spec, token]) => ({ - spec, - contract, - files: [`certora/harnesses/${contract}.sol`, `certora/harnesses/${token}.sol`], - options: [`--link ${contract}:token=${token}`, '--optimistic_loop', '--optimistic_hashing'], - }), - ), + : product( + ['GovernorHarness'], + ['GovernorFunctions'], + ['ERC20VotesBlocknumberHarness'], + ['propose', 'castVote', 'queue', 'execute', 'cancel'], + ).map(([contract, spec, token, fn]) => ({ + spec, + contract, + files: [ + `certora/harnesses/${contract}.sol`, + `certora/harnesses/${token}.sol`, + `certora/harnesses/TimelockControllerHarness.sol`, + ], + options: [ + `--link ${contract}:token=${token}`, + `--link ${contract}:_timelock=TimelockControllerHarness`, + '--optimistic_loop', + '--optimistic_hashing', + '--rules', + ['liveness', 'effect', 'sideeffect'].map(rule => `${fn}_${rule}`).join(' '), + ], + })), ); diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec index ec7b610a7..968f0b0ee 100644 --- a/certora/specs/Governor.helpers.spec +++ b/certora/specs/Governor.helpers.spec @@ -1,5 +1,6 @@ import "helpers.spec" import "methods/IGovernor.spec" +import "methods/ITimelockController.spec" /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -108,22 +109,26 @@ function helperFunctionsWithRevert(env e, method f, uint256 pId) { if (f.selector == propose(address[],uint256[],bytes[],string).selector) { address[] targets; uint256[] values; bytes[] calldatas; string descr; - require pId == propose@withrevert(e, targets, values, calldatas, descr); + require pId == hashProposal(targets, values, calldatas, descr); + propose@withrevert(e, targets, values, calldatas, descr); } else if (f.selector == queue(address[],uint256[],bytes[],bytes32).selector) { address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == queue@withrevert(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + queue@withrevert(e, targets, values, calldatas, descrHash); } else if (f.selector == execute(address[],uint256[],bytes[],bytes32).selector) { address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == execute@withrevert(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + execute@withrevert(e, targets, values, calldatas, descrHash); } else if (f.selector == cancel(address[],uint256[],bytes[],bytes32).selector) { address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == cancel@withrevert(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + cancel@withrevert(e, targets, values, calldatas, descrHash); } else if (f.selector == castVote(uint256,uint8).selector) { diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec index 7e856dbe1..ad5115727 100644 --- a/certora/specs/GovernorBaseRules.spec +++ b/certora/specs/GovernorBaseRules.spec @@ -1,4 +1,4 @@ -import "methods/IGovernor.spec" +import "helpers.spec" import "Governor.helpers.spec" import "GovernorInvariants.spec" diff --git a/certora/specs/GovernorChanges.spec b/certora/specs/GovernorChanges.spec index 0fff10a5a..6ab149fad 100644 --- a/certora/specs/GovernorChanges.spec +++ b/certora/specs/GovernorChanges.spec @@ -1,5 +1,4 @@ import "helpers.spec" -import "methods/IGovernor.spec" import "Governor.helpers.spec" import "GovernorInvariants.spec" diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec index 317f3b30d..016c12360 100644 --- a/certora/specs/GovernorFunctions.spec +++ b/certora/specs/GovernorFunctions.spec @@ -1,5 +1,4 @@ import "helpers.spec" -import "methods/IGovernor.spec" import "Governor.helpers.spec" /* @@ -14,11 +13,10 @@ rule propose_liveness(uint256 pId, env e) { uint8 stateBefore = state(e, pId); address[] targets; uint256[] values; bytes[] calldatas; string descr; - require validString(descr); - require targets.length < 0xffff; - require values.length < 0xffff; - require calldatas.length < 0xffff; - require pId == propose@withrevert(e, targets, values, calldatas, descr); + require pId == hashProposal(targets, values, calldatas, descr); + //require validString(descr); + + propose@withrevert(e, targets, values, calldatas, descr); // liveness & double proposal assert !lastReverted <=> ( @@ -32,7 +30,9 @@ rule propose_effect(uint256 pId, env e) { require clockSanity(e); address[] targets; uint256[] values; bytes[] calldatas; string descr; - require pId == propose(e, targets, values, calldatas, descr); + require pId == hashProposal(targets, values, calldatas, descr); + + propose(e, targets, values, calldatas, descr); // effect assert state(e, pId) == PENDING(); @@ -53,7 +53,9 @@ rule propose_sideeffect(uint256 pId, env e) { address otherProposer = proposalProposer(otherId); address[] targets; uint256[] values; bytes[] calldatas; string descr; - require pId == propose(e, targets, values, calldatas, descr); + require pId == hashProposal(targets, values, calldatas, descr); + + propose(e, targets, values, calldatas, descr); // no side-effect assert state(e, otherId) != otherStateBefore => otherId == pId; @@ -157,10 +159,9 @@ rule queue_liveness(uint256 pId, env e) { uint8 stateBefore = state(e, pId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require targets.length < 0xffff; - require values.length < 0xffff; - require calldatas.length < 0xffff; - require pId == queue@withrevert(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + queue@withrevert(e, targets, values, calldatas, descrHash); // liveness assert !lastReverted <=> stateBefore == SUCCEEDED(); @@ -174,7 +175,9 @@ rule queue_effect(uint256 pId, env e) { bool queuedBefore = isQueued(pId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == queue(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + queue(e, targets, values, calldatas, descrHash); assert state(e, pId) == QUEUED(); assert isQueued(pId); @@ -191,7 +194,9 @@ rule queue_sideeffect(uint256 pId, env e) { bool otherQueuedBefore = isQueued(otherId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == queue(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + queue(e, targets, values, calldatas, descrHash); // no side-effect assert state(e, otherId) != otherStateBefore => otherId == pId; @@ -210,10 +215,9 @@ rule execute_liveness(uint256 pId, env e) { uint8 stateBefore = state(e, pId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require targets.length < 0xffff; - require values.length < 0xffff; - require calldatas.length < 0xffff; - require pId == execute@withrevert(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + execute@withrevert(e, targets, values, calldatas, descrHash); // liveness: can't check full equivalence because of execution call reverts assert !lastReverted => (stateBefore == SUCCEEDED() || stateBefore == QUEUED()); @@ -224,7 +228,9 @@ rule execute_effect(uint256 pId, env e) { require clockSanity(e); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == execute(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + execute(e, targets, values, calldatas, descrHash); // effect assert state(e, pId) == EXECUTED(); @@ -239,7 +245,9 @@ rule execute_sideeffect(uint256 pId, env e) { uint8 otherStateBefore = state(e, otherId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == execute(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + execute(e, targets, values, calldatas, descrHash); // no side-effect assert state(e, otherId) != otherStateBefore => otherId == pId; @@ -257,10 +265,9 @@ rule cancel_liveness(uint256 pId, env e) { uint8 stateBefore = state(e, pId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require targets.length < 0xffff; - require values.length < 0xffff; - require calldatas.length < 0xffff; - require pId == cancel@withrevert(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + cancel@withrevert(e, targets, values, calldatas, descrHash); // liveness assert !lastReverted <=> ( @@ -274,7 +281,9 @@ rule cancel_effect(uint256 pId, env e) { require clockSanity(e); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == cancel(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + cancel(e, targets, values, calldatas, descrHash); // effect assert state(e, pId) == CANCELED(); @@ -291,7 +300,9 @@ rule cancel_sideeffect(uint256 pId, env e) { bool otherQueuedBefore = isQueued(otherId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; - require pId == cancel(e, targets, values, calldatas, descrHash); + require pId == hashProposal(targets, values, calldatas, descrHash); + + cancel(e, targets, values, calldatas, descrHash); // no side-effect assert state(e, otherId) != otherStateBefore => otherId == pId; diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec index 4d9de20ef..9be77e244 100644 --- a/certora/specs/GovernorInvariants.spec +++ b/certora/specs/GovernorInvariants.spec @@ -1,5 +1,4 @@ import "helpers.spec" -import "methods/IGovernor.spec" import "Governor.helpers.spec" /* diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index ec85e0737..808c45ae9 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -1,5 +1,4 @@ import "helpers.spec" -import "methods/IGovernor.spec" import "Governor.helpers.spec" import "GovernorInvariants.spec" @@ -11,6 +10,15 @@ methods { use invariant proposalStateConsistency use invariant votesImplySnapshotPassed +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ This is not (easily) provable as an invariant because the prover think `_totalSupplyCheckpoints` can arbitrarily │ +│ change, which causes the quorum() to change. Not sure how to fix that. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// invariant deadlineExtendedEquivQuorumReached(uint256 pId) +// getExtendedDeadline(pId) > 0 <=> (quorumReached(pId) && !isCanceled(pId)) + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: │ @@ -27,19 +35,13 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg requireInvariant proposalStateConsistency(pId); requireInvariant votesImplySnapshotPassed(e, pId); - // This is not (easily) provable as an invariant because the prover think `_totalSupplyCheckpoints` - // can arbitrarily change, which causes the quorum() to change. Not sure how to fix that. - // require quorumReached(pId) <=> getExtendedDeadline(pId) > 0; // Timeout - uint256 deadlineBefore = proposalDeadline(pId); bool deadlineExtendedBefore = getExtendedDeadline(pId) > 0; - // bool quorumReachedBefore = quorumReached(pId); // Timeout f(e, args); uint256 deadlineAfter = proposalDeadline(pId); bool deadlineExtendedAfter = getExtendedDeadline(pId) > 0; - // bool quorumReachedAfter = quorumReached(pId); // Timeout // deadline can never be reduced assert deadlineBefore <= proposalDeadline(pId); @@ -53,8 +55,6 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg ) || ( !deadlineExtendedBefore && deadlineExtendedAfter && - // !quorumReachedBefore && - // quorumReachedAfter && deadlineAfter == clock(e) + lateQuorumVoteExtension() && votingAll(f) ) diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index 3d1c9de4d..eece8bf09 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -1,5 +1,4 @@ import "helpers.spec" -import "methods/IGovernor.spec" import "Governor.helpers.spec" import "GovernorInvariants.spec" diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index e140c11de..46a1cb1c0 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -1,29 +1,6 @@ import "helpers.spec" import "methods/IAccessControl.spec" - -methods { - TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree - PROPOSER_ROLE() returns (bytes32) envfree - EXECUTOR_ROLE() returns (bytes32) envfree - CANCELLER_ROLE() returns (bytes32) envfree - isOperation(bytes32) returns (bool) envfree - isOperationPending(bytes32) returns (bool) envfree - isOperationReady(bytes32) returns (bool) - isOperationDone(bytes32) returns (bool) envfree - getTimestamp(bytes32) returns (uint256) envfree - getMinDelay() returns (uint256) envfree - - hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree - hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree - - schedule(address, uint256, bytes, bytes32, bytes32, uint256) - scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) - execute(address, uint256, bytes, bytes32, bytes32) - executeBatch(address[], uint256[], bytes[], bytes32, bytes32) - cancel(bytes32) - - updateDelay(uint256) -} +import "methods/ITimelockController.spec" /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ diff --git a/certora/specs/methods/IGovernor.spec b/certora/specs/methods/IGovernor.spec index 6cc25599f..7737bb23e 100644 --- a/certora/specs/methods/IGovernor.spec +++ b/certora/specs/methods/IGovernor.spec @@ -35,20 +35,21 @@ methods { updateTimelock(address) // 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 - isQueued(uint256) returns bool envfree - governanceCallLength() returns uint256 envfree - getAgainstVotes(uint256) returns uint256 envfree - getForVotes(uint256) returns uint256 envfree - getAbstainVotes(uint256) returns uint256 envfree - quorumNumeratorLength() returns uint256 envfree + token_getPastTotalSupply(uint256) returns uint256 envfree + token_getPastVotes(address,uint256) returns uint256 envfree + token_clock() returns uint48 + token_CLOCK_MODE() returns string + hashProposal(address[],uint256[],bytes[],string) returns uint256 envfree + 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 + isQueued(uint256) returns bool envfree + governanceCallLength() returns uint256 envfree + getAgainstVotes(uint256) returns uint256 envfree + getForVotes(uint256) returns uint256 envfree + getAbstainVotes(uint256) returns uint256 envfree + quorumNumeratorLength() returns uint256 envfree } diff --git a/certora/specs/methods/ITimelockController.spec b/certora/specs/methods/ITimelockController.spec new file mode 100644 index 000000000..a91fe211a --- /dev/null +++ b/certora/specs/methods/ITimelockController.spec @@ -0,0 +1,22 @@ +methods { + TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree => DISPATCHER(true) + PROPOSER_ROLE() returns (bytes32) envfree => DISPATCHER(true) + EXECUTOR_ROLE() returns (bytes32) envfree => DISPATCHER(true) + CANCELLER_ROLE() returns (bytes32) envfree => DISPATCHER(true) + isOperation(bytes32) returns (bool) envfree => DISPATCHER(true) + isOperationPending(bytes32) returns (bool) envfree => DISPATCHER(true) + isOperationReady(bytes32) returns (bool) => DISPATCHER(true) + isOperationDone(bytes32) returns (bool) envfree => DISPATCHER(true) + getTimestamp(bytes32) returns (uint256) envfree => DISPATCHER(true) + getMinDelay() returns (uint256) envfree => DISPATCHER(true) + + hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree => DISPATCHER(true) + hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree => DISPATCHER(true) + + schedule(address, uint256, bytes, bytes32, bytes32, uint256) => DISPATCHER(true) + scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => DISPATCHER(true) + execute(address, uint256, bytes, bytes32, bytes32) => DISPATCHER(true) + executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) + cancel(bytes32) => DISPATCHER(true) + updateDelay(uint256) => DISPATCHER(true) +} \ No newline at end of file