address PR comments

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)
     {

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();

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);

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);
 

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);
         }
     }
 

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 => (

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) {

requirements.txt

@@ -1 +1 @@
-certora-cli==3.6.4
+certora-cli==3.6.8