From c33e7bd3409c7839ba95b98f68ce4a6547cbb1d5 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Mon, 13 Mar 2023 17:26:38 +0100 Subject: [PATCH] update governor specs --- certora/diff/governance_Governor.sol.patch | 2 +- ...tensions_GovernorTimelockControl.sol.patch | 14 ++++++ certora/harnesses/GovernorHarness.sol | 4 ++ certora/specs.js | 38 ++++++++++----- certora/specs/Governor.helpers.spec | 18 +++++-- certora/specs/GovernorChanges.spec | 27 +++++++++++ certora/specs/GovernorFunctions.spec | 48 ++++++++++++++----- certora/specs/GovernorInvariants.spec | 21 ++++---- certora/specs/GovernorStates.spec | 17 +++---- certora/specs/methods/IGovernor.spec | 1 + 10 files changed, 144 insertions(+), 46 deletions(-) create mode 100644 certora/diff/governance_extensions_GovernorTimelockControl.sol.patch create mode 100644 certora/specs/GovernorChanges.spec diff --git a/certora/diff/governance_Governor.sol.patch b/certora/diff/governance_Governor.sol.patch index e3ad3e9b3..aa667d8d2 100644 --- a/certora/diff/governance_Governor.sol.patch +++ b/certora/diff/governance_Governor.sol.patch @@ -1,5 +1,5 @@ --- governance/Governor.sol 2023-03-07 10:48:47.730155491 +0100 -+++ governance/Governor.sol 2023-03-13 14:07:30.704202049 +0100 ++++ governance/Governor.sol 2023-03-13 15:30:49.107167674 +0100 @@ -216,6 +216,21 @@ return _proposals[proposalId].proposer; } diff --git a/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch new file mode 100644 index 000000000..5d5cf28f6 --- /dev/null +++ b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch @@ -0,0 +1,14 @@ +--- governance/extensions/GovernorTimelockControl.sol 2023-03-07 10:48:47.733488857 +0100 ++++ governance/extensions/GovernorTimelockControl.sol 2023-03-13 16:18:10.255122179 +0100 +@@ -84,6 +84,11 @@ + return eta == 1 ? 0 : eta; // _DONE_TIMESTAMP (1) should be replaced with a 0 value + } + ++ // FV ++ function _proposalQueueId(uint256 proposalId) internal view returns (bytes32) { ++ return _timelockIds[proposalId]; ++ } ++ + /** + * @dev Function to queue a proposal to the timelock. + */ diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol index 52a09416d..a8a2652de 100644 --- a/certora/harnesses/GovernorHarness.sol +++ b/certora/harnesses/GovernorHarness.sol @@ -64,6 +64,10 @@ contract GovernorHarness is return _isCanceled(proposalId); } + function isQueued(uint256 proposalId) public view returns (bool) { + return _proposalQueueId(proposalId) != bytes32(0); + } + function governanceCallLength() public view returns (uint256) { return _governanceCallLength(); } diff --git a/certora/specs.js b/certora/specs.js index 630865542..525afd51f 100644 --- a/certora/specs.js +++ b/certora/specs.js @@ -44,22 +44,36 @@ module.exports = [ }, // Governor ...product( - ['GovernorInvariants', 'GovernorBaseRules', 'GovernorStates'], + ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates'], ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'], ).map(([spec, token]) => ({ spec, contract: 'GovernorHarness', - files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`], - options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'], + 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'], - // })), + ...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 f43e5606f..5e44b7fa1 100644 --- a/certora/specs/Governor.helpers.spec +++ b/certora/specs/Governor.helpers.spec @@ -1,5 +1,18 @@ +import "helpers.spec" import "methods/IGovernor.spec" +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Sanity │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +function clockSanity(env e) returns bool { + return + e.block.number < max_uint48() && + e.block.timestamp < max_uint48() && + clock(e) > 0; +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ States │ @@ -16,8 +29,7 @@ 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; + return proposalCreated(pId) ? state(e, pId): UNSET(); } definition proposalCreated(uint256 pId) returns bool = @@ -122,4 +134,4 @@ function helperFunctionsWithRevert(env e, method f, uint256 pId) { { require false; } -} \ No newline at end of file +} diff --git a/certora/specs/GovernorChanges.spec b/certora/specs/GovernorChanges.spec new file mode 100644 index 000000000..2404bbc61 --- /dev/null +++ b/certora/specs/GovernorChanges.spec @@ -0,0 +1,27 @@ +import "helpers.spec" +import "methods/IGovernor.spec" +import "Governor.helpers.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: internal variables can only change though specific functions calls │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule changes(uint256 pId, env e) { + require nonpayable(e); + require clockSanity(e); + + address user; + + bool isExecutedBefore = isExecuted(pId); + bool isCanceledBefore = isCanceled(pId); + bool isQueuedBefore = isQueued(pId); + bool hasVotedBefore = hasVoted(pId, user); + + method f; calldataarg args; f(e, args); + + assert isExecuted(pId) != isExecutedBefore => (!isExecutedBefore && f.selector == execute(address[],uint256[],bytes[],bytes32).selector); + assert isCanceled(pId) != isCanceledBefore => (!isCanceledBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector); + assert isQueued(pId) != isQueuedBefore => (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector); + assert hasVoted(pId, user) != hasVotedBefore => (!hasVotedBefore && voting(f)); +} diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec index ec50c044a..b834663b9 100644 --- a/certora/specs/GovernorFunctions.spec +++ b/certora/specs/GovernorFunctions.spec @@ -9,6 +9,7 @@ import "Governor.helpers.spec" */ rule propose(uint256 pId, env e) { require nonpayable(e); + require clockSanity(e); uint256 otherId; @@ -18,8 +19,8 @@ rule propose(uint256 pId, env e) { 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); + address[] targets; uint256[] values; bytes[] calldatas; string descr; + require pId == propose@withrevert(e, targets, values, calldatas, descr); bool success = !lastReverted; // liveness & double proposal @@ -49,6 +50,7 @@ rule castVote(uint256 pId, env e, method f) filtered { f -> voting(f) } { require nonpayable(e); + require clockSanity(e); uint8 support; address voter; @@ -96,17 +98,24 @@ rule castVote(uint256 pId, env e, method f) assert getAbstainVotes(otherId) != otherAbstainVotesBefore => (otherId == pId); } - +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: queue effect and liveness. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ rule queue(uint256 pId, env e) { require nonpayable(e); + require clockSanity(e); uint256 otherId; - uint8 stateBefore = state(e, pId); - uint8 otherStateBefore = state(e, otherId); + uint8 stateBefore = state(e, pId); + uint8 otherStateBefore = state(e, otherId); + bool queuedBefore = isQueued(pId) + bool otherQueuedBefore = isQueued(otherId) - address[] targets; uint256[] values; bytes[] calldatas; string reason; - require pId == queue@withrevert(e, targets, values, calldatas, reason); + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == queue@withrevert(e, targets, values, calldatas, descrHash); bool success = !lastReverted; // liveness @@ -115,22 +124,31 @@ rule queue(uint256 pId, env e) { // effect assert success => ( state(e, pId) == QUEUED() + !queuedBefore && + isQueued(pId) ); // no side-effect assert state(e, otherId) != otherStateBefore => otherId == pId; + assert isQueued(otherId) != queuedBefore => otherId == pId; } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: execute effect and liveness. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ rule execute(uint256 pId, env e) { require nonpayable(e); + require clockSanity(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); + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == execute@withrevert(e, targets, values, calldatas, descrHash); bool success = !lastReverted; // liveness: can't check full equivalence because of execution call reverts @@ -145,16 +163,22 @@ rule execute(uint256 pId, env e) { assert state(e, otherId) != otherStateBefore => otherId == pId; } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: cancel (public) effect and liveness. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ rule cancel(uint256 pId, env e) { require nonpayable(e); + require clockSanity(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); + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == cancel@withrevert(e, targets, values, calldatas, descrHash); bool success = !lastReverted; // liveness @@ -170,4 +194,4 @@ rule cancel(uint256 pId, env e) { // 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 0a6ad61eb..1247789fa 100644 --- a/certora/specs/GovernorInvariants.spec +++ b/certora/specs/GovernorInvariants.spec @@ -8,7 +8,7 @@ import "Governor.helpers.spec" └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule clockMode(env e) { - require e.block.number < max_uint48() && e.block.timestamp < max_uint48(); + require clockSanity(e); assert clock(e) == e.block.number || clock(e) == e.block.timestamp; assert clock(e) == token_clock(e); @@ -31,7 +31,7 @@ invariant proposalStateConsistency(uint256 pId) (proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0) { preserved with (env e) { - require clock(e) > 0; + require clockSanity(e); } } @@ -44,8 +44,8 @@ invariant canceledImplyCreated(uint pId) isCanceled(pId) => proposalCreated(pId) { preserved with (env e) { + require clockSanity(e); requireInvariant proposalStateConsistency(pId); - require clock(e) > 0; } } @@ -58,21 +58,22 @@ invariant executedImplyCreated(uint pId) isExecuted(pId) => proposalCreated(pId) { preserved with (env e) { + require clockSanity(e); requireInvariant proposalStateConsistency(pId); - require clock(e) > 0; } } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: The state UNSET() correctly catch uninitialized proposal. │ +│ Invariant: queued => created │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant proposalStateConsistencyUnset(env e, uint256 pId) - proposalCreated(pId) <=> safeState(e, pId) == UNSET() +invariant queuedImplyCreated(uint pId) + isQueued(pId) => proposalCreated(pId) { - preserved { - require clock(e) > 0; + preserved with (env e) { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); } } @@ -103,4 +104,4 @@ invariant noBothExecutedAndCanceled(uint256 pId) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant governanceCallLength() - governanceCallLength() == 0 \ No newline at end of file + governanceCallLength() == 0 diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index af5cef792..958d7ae47 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -31,7 +31,7 @@ rule stateConsistency(env e, uint256 pId) { rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args) filtered { f -> !skip(f) } { - require clock(e) > 0; // Sanity + require clockSanity(e); uint8 stateBefore = state(e, pId); f(e, args); @@ -64,7 +64,8 @@ rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule stateTransitionWait(uint256 pId, env e1, env e2) { - require clock(e1) > 0; // Sanity + require clockSanity(e1); + require clockSanity(e2); require clock(e2) > clock(e1); uint8 stateBefore = state(e1, pId); @@ -87,25 +88,25 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) { │ Rule: State corresponds to the vote timing and results │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule stateFollowsVoteTimmingAndResult(uint256 pId, env e) { - require clock(e) > 0; // Sanity +rule stateIsConsistentWithVotes(uint256 pId, env e) { + require clockSanity(e); requireInvariant proposalStateConsistency(pId); uint8 currentState = state(e, pId); uint48 currentClock = clock(e); - // Pending = before vote starts + // Pending: before vote starts assert currentState == PENDING() => ( proposalSnapshot(pId) >= currentClock ); - // Active = after vote starts & before vote ends + // Active: after vote starts & before vote ends assert currentState == ACTIVE() => ( proposalSnapshot(pId) < currentClock && proposalDeadline(pId) >= currentClock ); - // Succeeded = after vote end, with vote successful and quorum reached + // Succeeded: after vote end, with vote successful and quorum reached assert currentState == SUCCEEDED() => ( proposalDeadline(pId) < currentClock && ( @@ -114,7 +115,7 @@ rule stateFollowsVoteTimmingAndResult(uint256 pId, env e) { ) ); - // Succeeded = after vote end, with vote not successful or quorum not reached + // Defeated: after vote end, with vote not successful or quorum not reached assert currentState == DEFEATED() => ( proposalDeadline(pId) < currentClock && ( diff --git a/certora/specs/methods/IGovernor.spec b/certora/specs/methods/IGovernor.spec index ea0308c18..ba75f8089 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 + isQueued(uint256) returns bool envfree governanceCallLength() returns uint256 envfree getAgainstVotes(uint256) returns uint256 envfree getForVotes(uint256) returns uint256 envfree