fix specs

certora/specs/Governor.helpers.spec

@@ -45,7 +45,7 @@ definition voting(method f) returns bool =
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 support) returns uint256 {
-    string reason; bytes params; uint8 v; bytes32 s; bytes32 r;
+    string reason; bytes params;
 
     if (f.selector == castVote(uint256,uint8).selector)
     {
@@ -64,39 +64,38 @@ function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8
     }
     else
     {
-        calldataarg args;
-        f@withrevert(e, args);
+        require false;
         return 0;
     }
 }
 
 function helperFunctionsWithRevert(env e, method f, uint256 pId) {
-    if (f.selector == propose(address[], uint256[], bytes[], string).selector)
+    if (f.selector == propose(address[],uint256[],bytes[],string).selector)
     {
-        address[] targets; uint256[] values; bytes[] calldatas; string description;
-        require pId == propose@withrevert(e, targets, values, calldatas, description);
+        address[] targets; uint256[] values; bytes[] calldatas; string descr;
+        require pId == propose@withrevert(e, targets, values, calldatas, descr);
     }
-    else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector)
+    else if (f.selector == queue(address[],uint256[],bytes[],bytes32).selector)
     {
-        address[] targets; uint256[] values; bytes[] calldatas; bytes32 description;
-        require pId == queue@withrevert(e, targets, values, calldatas, description);
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+        require pId == queue@withrevert(e, targets, values, calldatas, descrHash);
     }
-    else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector)
+    else if (f.selector == execute(address[],uint256[],bytes[],bytes32).selector)
     {
-        address[] targets; uint256[] values; bytes[] calldatas; bytes32 description;
-        require pId == execute@withrevert(e, targets, values, calldatas, description);
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+        require pId == execute@withrevert(e, targets, values, calldatas, descrHash);
     }
-    else if (f.selector == cancel(address[], uint256[], bytes[], bytes32).selector)
+    else if (f.selector == cancel(address[],uint256[],bytes[],bytes32).selector)
     {
-        address[] targets; uint256[] values; bytes[] calldatas; bytes32 description;
-        require pId == cancel@withrevert(e, targets, values, calldatas, description);
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+        require pId == cancel@withrevert(e, targets, values, calldatas, descrHash);
     }
-    else if (f.selector == castVote(uint256, uint8).selector)
+    else if (f.selector == castVote(uint256,uint8).selector)
     {
         uint8 support;
         castVote@withrevert(e, pId, support);
     }
-    else if  (f.selector == castVoteWithReason(uint256, uint8, string).selector)
+    else if (f.selector == castVoteWithReason(uint256,uint8,string).selector)
     {
         uint8 support; string reason;
         castVoteWithReason@withrevert(e, pId, support, reason);
@@ -106,7 +105,7 @@ function helperFunctionsWithRevert(env e, method f, uint256 pId) {
         uint8 support; string reason; bytes params;
         castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params);
     }
-    else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector)
+    else if (f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector)
     {
         uint8 support; uint8 v; bytes32 r; bytes32 s;
         castVoteBySig@withrevert(e, pId, support, v, r, s);
@@ -118,7 +117,6 @@ function helperFunctionsWithRevert(env e, method f, uint256 pId) {
     }
     else
     {
-        calldataarg args;
-        f@withrevert(e, args);
+        require false;
     }
 }

certora/specs/GovernorBase.spec

@@ -99,14 +99,14 @@ rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldata
     require proposalCreated(pId);
 
     uint256 voteStart = proposalSnapshot(pId);
-    uint256 voteEnd = proposalDeadline(pId);
-    address proposer = proposalProposer(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";
+    assert voteEnd   == proposalDeadline(pId), "End date was changed";
+    assert proposer  == proposalProposer(pId), "Proposer was changed";
 }
 
 /*
@@ -177,21 +177,14 @@ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) {
 │ attribute to the execute() function, showing that only execute() can change it, and that it will always change it.  │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args) filtered {
-    f -> !f.isView && !f.isFallback
-    && f.selector != updateTimelock(address).selector
-    && f.selector != updateQuorumNumerator(uint256).selector
-    && f.selector != relay(address,uint256,bytes).selector
-    && f.selector != 0xb9a61961 // __acceptAdmin()
-    && f.selector != onERC721Received(address,address,uint256,bytes).selector
-    && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector
-    && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector
-} {
+rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args)
+    filtered { f -> !skip(f) }
+{
     require isExecuted(pId);
     requireInvariant noBothExecutedAndCanceled(pId);
     requireInvariant executedImplyCreated(pId);
 
-    helperFunctionsWithRevert(pId, f, e);
+    helperFunctionsWithRevert(e, f, pId);
 
     assert lastReverted, "Function was not reverted";
 }
@@ -205,21 +198,14 @@ rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args
 │ attribute to the execute() function, showing that only execute() can change it, and that it will always change it.  │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args) filtered {
-    f -> !f.isView && !f.isFallback
-    && f.selector != updateTimelock(address).selector
-    && f.selector != updateQuorumNumerator(uint256).selector
-    && f.selector != relay(address,uint256,bytes).selector
-    && f.selector != 0xb9a61961 // __acceptAdmin()
-    && f.selector != onERC721Received(address,address,uint256,bytes).selector
-    && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector
-    && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector
-} {
+rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args)
+    filtered { f -> !skip(f) }
+{
     require isCanceled(pId);
     requireInvariant noBothExecutedAndCanceled(pId);
     requireInvariant canceledImplyCreated(pId);
 
-    helperFunctionsWithRevert(pId, f, e);
+    helperFunctionsWithRevert(e, f, pId);
 
     assert lastReverted, "Function was not reverted";
 }
@@ -234,7 +220,7 @@ rule stateOnlyAfterFunc(uint256 pId, env e, method f) {
     bool executedBefore = isExecuted(pId);
     bool canceledBefore = isCanceled(pId);
 
-    helperFunctionsWithRevert(pId, f, e);
+    helperFunctionsWithRevert(e, f, pId);
 
     assert (proposalCreated(pId) != createdBefore)
         => (createdBefore == false && f.selector == propose(address[], uint256[], bytes[], string).selector),

certora/specs/GovernorInvariants.spec

@@ -21,14 +21,23 @@ 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)
+    safeState(e, pId) == UNSET()  => !isExecuted(pId) &&
+    safeState(e, pId) == UNSET()  => !isCanceled(pId)
     {
         preserved {
             require clock(e) > 0;
         }
     }
 
+invariant createdConsistencyWeak(uint256 pId)
+    proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0 &&
+    proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0
+    {
+        preserved with (env e) {
+            require clock(e) > 0;
+        }
+    }
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariant: Votes start before it ends                                                                               │
@@ -37,8 +46,8 @@ invariant createdConsistency(env e, uint256 pId)
 invariant voteStartBeforeVoteEnd(uint256 pId)
     proposalSnapshot(pId) <= proposalDeadline(pId)
     {
-        preserved with (env e) {
-            requireInvariant createdConsistency(e, pId);
+        preserved {
+            requireInvariant createdConsistencyWeak(pId);
         }
     }
 

certora/specs/GovernorStates.spec

@@ -22,7 +22,7 @@ rule stateConsistency(env e, uint256 pId) {
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: State transition                                                                                              │
+│ Rule: State transitions caused by function calls                                                                    │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args)
@@ -55,6 +55,11 @@ rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args)
     );
 }
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: State transitions caused by time passing                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
 rule stateTransitionWait(uint256 pId, env e1, env e2) {
     require clock(e1) > 0; // Sanity
     require clock(e2) > clock(e1);
@@ -63,14 +68,9 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) {
     uint8 stateAfter  = state(e2, pId);
 
     assert (stateBefore != stateAfter) => (
-        stateBefore == PENDING() => (
-            stateAfter == ACTIVE()
-        ) &&
-        stateBefore == ACTIVE() => (
-            stateAfter == SUCCEEDED() ||
-            stateAfter == DEFEATED()
-        ) &&
-        stateBefore == UNSET() => false &&
+        stateBefore == PENDING()   => stateAfter == ACTIVE() &&
+        stateBefore == ACTIVE()    => (stateAfter == SUCCEEDED() || stateAfter == DEFEATED()) &&
+        stateBefore == UNSET()     => false &&
         stateBefore == SUCCEEDED() => false &&
         stateBefore == QUEUED()    => false &&
         stateBefore == CANCELED()  => false &&
@@ -78,135 +78,3 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) {
         stateBefore == EXECUTED()  => false
     );
 }
-
-
-
-
-
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable                                     │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-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";
-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: propose effect and liveness. Includes "no double proposition"                                                 │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule propose(uint256 pId, env e) {
-    require nonpayable(e);
-
-    uint256 otherId;
-
-    uint8   stateBefore      = state(e, pId);
-    uint8   otherStateBefore = state(e, otherId);
-    uint256 otherVoteStart   = proposalSnapshot(otherId);
-    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);
-    bool success = !lastReverted;
-
-    // liveness & double proposal
-    assert success <=> stateBefore == UNSET();
-
-    // effect
-    assert success => (
-        state(e, pId)         == PENDING()    &&
-        proposalProposer(pId) == e.msg.sender &&
-        proposalSnapshot(pId) == clock(e) + votingDelay() &&
-        proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod()
-    );
-
-    // no side-effect
-    assert state(e, otherId)         != otherStateBefore => otherId == pId;
-    assert proposalSnapshot(otherId) == otherVoteStart;
-    assert proposalDeadline(otherId) == otherVoteEnd;
-    assert proposalProposer(otherId) == otherProposer;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: votes effect and liveness. Includes "A user cannot vote twice"                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule castVote(uint256 pId, env e, method f)
-    filtered { f -> voting(f) }
-{
-    require nonpayable(e);
-
-    uint8   support;
-    address voter;
-    address otherVoter;
-    uint256 otherId;
-
-    uint8   stateBefore             = state(e, pId);
-    bool    hasVotedBefore          = hasVoted(pId, voter);
-    bool    otherVotedBefore        = hasVoted(otherId, otherVoter);
-    uint256 againstVotesBefore      = getAgainstVotes(pId);
-    uint256 forVotesBefore          = getForVotes(pId);
-    uint256 abstainVotesBefore      = getAbstainVotes(pId);
-    uint256 otherAgainstVotesBefore = getAgainstVotes(otherId);
-    uint256 otherForVotesBefore     = getForVotes(otherId);
-    uint256 otherAbstainVotesBefore = getAbstainVotes(otherId);
-
-    // voting weight overflow check
-    uint256 voterWeight = token_getPastVotes(voter, proposalSnapshot(pId));
-    require againstVotesBefore + voterWeight <= max_uint256;
-    require forVotesBefore     + voterWeight <= max_uint256;
-    require abstainVotesBefore + voterWeight <= max_uint256;
-
-    uint256 weight = helperVoteWithRevert(e, f, pId, voter, support);
-    bool success = !lastReverted;
-
-    assert success <=> (
-        stateBefore == ACTIVE() &&
-        !hasVotedBefore &&
-        (support == 0 || support == 1 || support == 2)
-    );
-
-    assert success => (
-        state(e, pId)        == ACTIVE() &&
-        voterWeight          == weight &&
-        getAgainstVotes(pId) == againstVotesBefore + (support == 0 ? weight : 0) &&
-        getForVotes(pId)     == forVotesBefore     + (support == 1 ? weight : 0) &&
-        getAbstainVotes(pId) == abstainVotesBefore + (support == 2 ? weight : 0) &&
-        hasVoted(pId, voter)
-    );
-
-    // no side-effect
-    assert hasVoted(otherId, otherVoter) != otherVotedBefore        => (otherId == pId && otherVoter == voter);
-    assert getAgainstVotes(otherId)      != otherAgainstVotesBefore => (otherId == pId);
-    assert getForVotes(otherId)          != otherForVotesBefore     => (otherId == pId);
-    assert getAbstainVotes(otherId)      != otherAbstainVotesBefore => (otherId == pId);
-}