diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec index 67cadd619..64ec0a684 100644 --- a/certora/specs/Governor.helpers.spec +++ b/certora/specs/Governor.helpers.spec @@ -42,6 +42,8 @@ definition QUEUED() returns uint8 = 5; definition EXPIRED() returns uint8 = 6; definition EXECUTED() returns uint8 = 7; +// This helper is an alternative to state(e, pId) that will return UNSET() instead of reverting when then proposal +// does not exist (not created yet) function safeState(env e, uint256 pId) returns uint8 { return proposalCreated(pId) ? state(e, pId): UNSET(); } @@ -54,7 +56,7 @@ definition proposalCreated(uint256 pId) returns bool = │ Filters │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -definition skip(method f) returns bool = +definition assumedSafe(method f) returns bool = f.isView || f.isFallback || f.selector == relay(address,uint256,bytes).selector || @@ -62,6 +64,19 @@ definition skip(method f) returns bool = f.selector == onERC1155Received(address,address,uint256,uint256,bytes).selector || f.selector == onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector; +// These function are covered by helperFunctionsWithRevert +definition operateOnProposal(method f) returns bool = + f.selector == propose(address[],uint256[],bytes[],string).selector || + f.selector == queue(address[],uint256[],bytes[],bytes32).selector || + f.selector == execute(address[],uint256[],bytes[],bytes32).selector || + f.selector == cancel(address[],uint256[],bytes[],bytes32).selector || + f.selector == castVote(uint256,uint8).selector || + f.selector == castVoteWithReason(uint256,uint8,string).selector || + f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector || + f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector || + f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector + +// These function are covered by helperVoteWithRevert definition voting(method f) returns bool = f.selector == castVote(uint256,uint8).selector || f.selector == castVoteWithReason(uint256,uint8,string).selector || @@ -105,6 +120,14 @@ function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 } } +// Governor function that operates on a given proposalId may or may not include the proposalId in the arguments. This +// helper restricts the call to method `f` in a way that it's operating on a specific proposal. +// +// This can be used to say "consider any function call that operates on proposal `pId`" or "consider a propose call +// that corresponds to a given pId". +// +// This is for example used when proving that not 2 proposals can be proposed with the same id: Once the proposal is +// proposed a first time, we want to prove that "any propose call that corresponds to the same id should revert". function helperFunctionsWithRevert(env e, method f, uint256 pId) { if (f.selector == propose(address[],uint256[],bytes[],string).selector) { diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec index ef5be8823..d1dc29581 100644 --- a/certora/specs/GovernorBaseRules.spec +++ b/certora/specs/GovernorBaseRules.spec @@ -27,7 +27,7 @@ rule noDoublePropose(uint256 pId, env e) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { require proposalCreated(pId); @@ -46,13 +46,9 @@ rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldata ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ 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. │ +│ This rule is checked for castVote, castVoteWithReason and castVoteWithReasonAndParams. For the signature variants │ +│ (castVoteBySig and castVoteWithReasonAndParamsBySig) we basically assume that the signature referendum is correct │ +│ without checking it. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule noDoubleVoting(uint256 pId, env e, method f) @@ -76,31 +72,20 @@ rule noDoubleVoting(uint256 pId, env e, method f) rule againstVotesDontCountTowardsQuorum(uint256 pId, env e) { bool quorumReachedBefore = quorumReached(pId); + + // Ideally we would use `helperVoteWithRevert` here, but it causes timeout. Consider changing it if/when the prover improves. castVote(e, pId, 0); + assert quorumReached(pId) == quorumReachedBefore, "quorum must not be reached with an against vote"; } -/// This version is more exhaustive, but to slow because "quorumReached" is a FV nightmare -// rule againstVotesDontCountTowardsQuorum(uint256 pId, env e, method f) -// filtered { f -> voting(f) } -// { -// address voter; -// -// bool quorumReachedBefore = quorumReached(pId); -// -// helperVoteWithRevert(e, f, pId, voter, 0); // support 0 = against -// -// assert quorumReached(pId) == quorumReachedBefore, "quorum must not be reached with an against vote"; -// } - - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: A proposal could be executed only if quorum was reached and vote succeeded │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { require !isExecuted(pId); @@ -118,7 +103,7 @@ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule noStartBeforeCreation(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { require !proposalCreated(pId); @@ -133,7 +118,7 @@ rule noStartBeforeCreation(uint256 pId, env e, method f, calldataarg args) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { require !isExecuted(pId); @@ -149,7 +134,7 @@ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) */ invariant quorumRatioLessThanOne() quorumNumerator() <= quorumDenominator() - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { preserved { require quorumNumeratorLength() < max_uint256; @@ -160,16 +145,14 @@ invariant quorumRatioLessThanOne() ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ 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. │ +│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, none of the │ +│ proposal specific functions can make changes again. Note that we prove that only the `execute()` function can set | +| isExecuted() to true in in `GorvernorChanges.spec`. | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args) filtered { f -> - !skip(f) && - f.selector != updateQuorumNumerator(uint256).selector && - f.selector != updateTimelock(address).selector -} { +rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args) + filtered { f -> operateOnProposal(f) } +{ require isExecuted(pId); requireInvariant noBothExecutedAndCanceled(pId); requireInvariant executedImplyCreated(pId); @@ -184,15 +167,13 @@ rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args │ 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. │ +│ proposal specific functions can make changes again. Note that we prove that only the `execute()` function can set | +| isExecuted() to true in in `GorvernorChanges.spec`. | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args) filtered { f -> - !skip(f) && - f.selector != updateQuorumNumerator(uint256).selector && - f.selector != updateTimelock(address).selector -} { +rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args) + filtered { f -> operateOnProposal(f) } +{ require isCanceled(pId); requireInvariant noBothExecutedAndCanceled(pId); requireInvariant canceledImplyCreated(pId); @@ -208,7 +189,7 @@ rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule privilegedUpdate(env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { address executorBefore = getExecutor(); uint256 quorumNumeratorBefore = quorumNumerator(); diff --git a/certora/specs/GovernorChanges.spec b/certora/specs/GovernorChanges.spec index 6ab149fad..bce702156 100644 --- a/certora/specs/GovernorChanges.spec +++ b/certora/specs/GovernorChanges.spec @@ -10,7 +10,7 @@ use invariant proposalStateConsistency └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule changes(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { require clockSanity(e); requireInvariant proposalStateConsistency(pId); diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec index beb9b0c6b..fd6ea4191 100644 --- a/certora/specs/GovernorFunctions.spec +++ b/certora/specs/GovernorFunctions.spec @@ -18,7 +18,6 @@ rule propose_liveness(uint256 pId, env e) { address[] targets; uint256[] values; bytes[] calldatas; string descr; require pId == hashProposal(targets, values, calldatas, descr); - //require sanityString(descr); propose@withrevert(e, targets, values, calldatas, descr); diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec index b4257f209..b4325ba36 100644 --- a/certora/specs/GovernorInvariants.spec +++ b/certora/specs/GovernorInvariants.spec @@ -97,7 +97,7 @@ invariant queuedImplyCreated(uint pId) /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: timmings │ +│ Invariant: timings │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant votesImplySnapshotPassed(env e, uint256 pId) @@ -108,7 +108,9 @@ invariant votesImplySnapshotPassed(env e, uint256 pId) ) => proposalSnapshot(pId) < clock(e) { preserved with (env e2) { - require clock(e) == clock(e2); + // In this invariant, `env e` is representing the present. And `clock(e)` the current timestamp. + // It should hold for any transitions in the pasts + require clock(e2) <= clock(e); } } diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index 808c45ae9..97f4c8f6f 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -29,7 +29,7 @@ use invariant votesImplySnapshotPassed └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { require clockSanity(e); requireInvariant proposalStateConsistency(pId); @@ -44,7 +44,7 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg bool deadlineExtendedAfter = getExtendedDeadline(pId) > 0; // deadline can never be reduced - assert deadlineBefore <= proposalDeadline(pId); + assert deadlineBefore <= deadlineAfter; // deadline can only be extended in proposal or on cast vote assert deadlineAfter != deadlineBefore => ( diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index a1dc7eada..891b42e5c 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -3,7 +3,7 @@ import "Governor.helpers.spec" import "GovernorInvariants.spec" use invariant proposalStateConsistency -// use invariant votesImplySnapshotPassed +use invariant votesImplySnapshotPassed /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -29,32 +29,21 @@ rule stateConsistency(env e, uint256 pId) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } + filtered { f -> !assumedSafe(f) } { require clockSanity(e); + require quorumNumeratorLength() < max_uint256; // 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 + (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 ) || + (stateBefore == SUCCEEDED() && stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) || + (stateBefore == QUEUED() && stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) ); } @@ -68,18 +57,26 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) { require clockSanity(e2); require clock(e2) > clock(e1); + // Force the state to be consistent with e1 (before). We want the storage related to `pId` to match what is + // possible before the time passes. We don't want the state transition include elements that cannot have happened + // before e1. This ensure that the e1 → e2 state transition is purelly a consequence of time passing. + requireInvariant votesImplySnapshotPassed(e1, pId); + 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 + (stateBefore == PENDING() && stateAfter == ACTIVE() ) || + (stateBefore == PENDING() && stateAfter == DEFEATED() ) || + (stateBefore == ACTIVE() && stateAfter == SUCCEEDED()) || + (stateBefore == ACTIVE() && stateAfter == DEFEATED() ) || + // Strange consequence of the timelock binding: + // When transitioning from ACTIVE to SUCCEEDED (because of the clock moving forward) the proposal state in + // the timelock is suddenly considered. Prior state set in the timelock can cause the proposal to already be + // queued, executed or canceled. + (stateBefore == ACTIVE() && stateAfter == CANCELED()) || + (stateBefore == ACTIVE() && stateAfter == EXECUTED()) || + (stateBefore == ACTIVE() && stateAfter == QUEUED()) ); } @@ -135,9 +132,9 @@ rule stateIsConsistentWithVotes(uint256 pId, env e) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ //// This would be nice, but its way to slow to run because "quorumReached" is a FV nightmare -//// Also, for it to work we need to prove that the checkpoints have (strictly) increase values ... what a nightmare +//// Also, for it to work we need to prove that the checkpoints have (strictly) increasing keys. // rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg args) -// filtered { f -> !skip(f) } +// filtered { f -> !assumedSafe(f) } // { // require clockSanity(e); // require clock(e) > proposalSnapshot(pId); // vote has started @@ -159,7 +156,7 @@ rule stateIsConsistentWithVotes(uint256 pId, env e) { // ); // } -//// To prove that, we need to prove that the checkpoints have (strictly) increase values ... what a nightmare +//// To prove that, we need to prove that the checkpoints have (strictly) increasing keys. //// otherwise it gives us counter example where the checkpoint history has keys: //// [ 12,12,13,13,12] and the lookup obviously fail to get the correct value // rule quorumUpdateDoesntAffectPastProposals(uint256 pId, env e) { diff --git a/requirements.txt b/requirements.txt index da3e95766..5aad982b2 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1 @@ -certora-cli==3.6.4 +certora-cli==3.6.8