CountingSimpleMoreCleanAndAddedMoreRules

certora/specs/GovernorBase.spec

@@ -1,6 +1,7 @@
 //////////////////////////////////////////////////////////////////////////////
 ///////////////////// Governor.sol base definitions //////////////////////////
 //////////////////////////////////////////////////////////////////////////////
+
 methods {
     proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
     proposalDeadline(uint256) returns uint256 envfree
@@ -17,131 +18,175 @@ methods {
     // internal functions made public in harness:
     _quorumReached(uint256) returns bool envfree
     _voteSucceeded(uint256) returns bool envfree
-
 }
+
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
 
-    /*
+/*
-     * A proposal cannot end unless it started.
+ * A proposal cannot end unless it started.
-     */
+ */
-    invariant voteStartBeforeVoteEnd(uint256 pId)
+invariant voteStartBeforeVoteEnd(uint256 pId)
-        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
+    (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
-             && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
+         && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
 
 
-    /*
+/**
-     * A proposal cannot be both executed and canceled.
+ * A proposal cannot be both executed and canceled.
-     */
+ */
-    invariant noBothExecutedAndCanceled(uint256 pId) 
+invariant noBothExecutedAndCanceled(uint256 pId) 
-            !isExecuted(pId) || !isCanceled(pId)
+        !isExecuted(pId) || !isCanceled(pId)
 
 
-    /*
+/**
-     * A proposal cannot be neither executed nor canceled before it starts
+ * A proposal could be executed only if quorum was reached and vote succeeded
-     */
+ */
-    invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) 
+invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
-            e.block.number < proposalSnapshot(pId) 
+        isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
-                => !isExecuted(pId) && !isCanceled(pId)
 
 
-    /*
+//////////////////////////////////////////////////////////////////////////////
-     * A proposal could be executed only if quorum was reached and vote succeeded
+/////////////////////////////////// RULES ////////////////////////////////////
-     */
+//////////////////////////////////////////////////////////////////////////////
-    invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
-            isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
     
 
-    //////////////////////////////////////////////////////////////////////////////
+/*
-    /////////////////////////////////// RULES ////////////////////////////////////
+ * No functions should be allowed to run after a job is deemed as canceled
-    //////////////////////////////////////////////////////////////////////////////
+ */
-    
+rule cannotSetIfCanceled(uint256 pId, method f) filtered { f-> !f.isView }{
-    /*
+    require(isCanceled(pId));
-     * The voting must start not before the proposal’s creation time
+    env e; calldataarg args;
-     */
+    f(e, args);
-    rule noStartBeforeCreation(uint256 pId) {
+    assert(isCanceled(pId) => lastReverted == true, "Function did not revert when canceled");
-        uint previousStart = proposalSnapshot(pId);
+}
-        require previousStart == 0;
-        env e;
-        calldataarg arg;
-        propose(e, arg);
-
-        uint newStart = proposalSnapshot(pId);
-        // if created, start is after creation
-        assert(newStart != 0 => newStart >= e.block.number);
-    }
 
 
-    /*
+/*
-     * Once a proposal is created, voteStart and voteEnd are immutable
+ * No functions should be allowed to run after a job is deemed as executed
-     */
+ */
-    rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
+rule cannotSetIfExecuted(uint256 pId, method f) filtered { f-> !f.isView }{
-        uint _voteStart = proposalSnapshot(pId);
+    require(isExecuted(pId));
-        uint _voteEnd = proposalDeadline(pId);
+    env e; calldataarg args;
-        require _voteStart > 0; // proposal was created
+    f(e, args);
-
+    assert(isExecuted(pId) => lastReverted == true, "Function did not revert after executed");
-        env e;
+}
-        calldataarg arg;
-        f(e, arg);
-
-        uint voteStart_ = proposalSnapshot(pId);
-        uint voteEnd_ = proposalDeadline(pId);
-        assert _voteStart == voteStart_;
-        assert _voteEnd == voteEnd_;
-    }
 
 
-    /*
+/*
-     * A user cannot vote twice
+ * The voting must start not before the proposal’s creation time
-     */
+ */
-    rule doubleVoting(uint256 pId, uint8 sup) {
+rule noStartBeforeCreation(uint256 pId) {
-        env e;
+    uint previousStart = proposalSnapshot(pId);
-        address user = e.msg.sender;
+    require previousStart == 0;
+    env e;
+    calldataarg arg;
+    propose(e, arg);
 
-        bool votedCheck = hasVoted(e, pId, user);
+    uint newStart = proposalSnapshot(pId);
-        require votedCheck == true;
+    // if created, start is after creation
-
+    assert(newStart != 0 => newStart >= e.block.number);
-        castVote@withrevert(e, pId, sup);
+}
-        bool reverted = lastReverted;
-
-        assert votedCheck => reverted, "double voting accured";
-    }
 
 
-    /*
+/*
-     * When a proposal is created the start and end date are created in the future.
+ * Once a proposal is created, voteStart and voteEnd are immutable
-     */
+ */
-    rule proposalCreatedStartAndEndDateInFuture(address[] targets, uint256[] values, bytes[] calldatas){
+rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
-        env e;
+    uint _voteStart = proposalSnapshot(pId);
-        uint256 pId = callPropose(e, targets, values, calldatas);
+    uint _voteEnd = proposalDeadline(pId);
-        uint256 startDate = proposalSnapshot(pId);
+    require _voteStart > 0; // proposal was created
-        uint256 endDate = proposalDeadline(pId);
+
-        assert(startDate >= e.block.number && endDate >= e.block.number, "Start or end date were set in the past");
+    env e;
-    }
+    calldataarg arg;
+    f(e, arg);
+
+    uint voteStart_ = proposalSnapshot(pId);
+    uint voteEnd_ = proposalDeadline(pId);
+    assert _voteStart == voteStart_;
+    assert _voteEnd == voteEnd_;
+}
 
 
-    /**
+/*
-     * Check hashProposal hashing is reliable (different inputs lead to different buffers hashed)
+ * A user cannot vote twice
-     */
+ */
-    /*
+rule doubleVoting(uint256 pId, uint8 sup) {
-    rule checkHashProposal {
+    env e;
-        address[] t1;
+    address user = e.msg.sender;
-        address[] t2;
-        uint256[] v1;
-        uint256[] v2;
-        bytes[] c1;
-        bytes[] c2;
-        bytes32 d1;
-        bytes32 d2;
 
-        uint256 h1 = hashProposal(t1,v1,c1,d1);
+    bool votedCheck = hasVoted(e, pId, user);
-        uint256 h2 = hashProposal(t2,v2,c2,d2);
+
-        bool equalHashes = h1 == h2;
+    castVote@withrevert(e, pId, sup);
-        assert equalHashes => t1.length == t2.length;
+    bool reverted = lastReverted;
-        assert equalHashes => v1.length == v2.length;
+
-        assert equalHashes => c1.length == c2.length;
+    assert votedCheck => reverted, "double voting accured";
-        assert equalHashes => d1 == d2;
+}
-    }
+
-    */
+
+/*
+ * When a proposal is created the start and end date are created in the future.
+ */
+rule proposalCreatedStartAndEndDateInFuture(address[] targets, uint256[] values, bytes[] calldatas){
+    env e;
+    uint256 pId = callPropose(e, targets, values, calldatas);
+    uint256 startDate = proposalSnapshot(pId);
+    uint256 endDate = proposalDeadline(pId);
+    assert(startDate >= e.block.number && endDate >= e.block.number, "Start or end date were set in the past");
+}
+
+
+/**
+ * Check hashProposal hashing is reliable (different inputs lead to different buffers hashed)
+ */
+/*
+rule checkHashProposal {
+    address[] t1;
+    address[] t2;
+    uint256[] v1;
+    uint256[] v2;
+    bytes[] c1;
+    bytes[] c2;
+    bytes32 d1;
+    bytes32 d2;
+
+    uint256 h1 = hashProposal(t1,v1,c1,d1);
+    uint256 h2 = hashProposal(t2,v2,c2,d2);
+    bool equalHashes = h1 == h2;
+    assert equalHashes => t1.length == t2.length;
+    assert equalHashes => v1.length == v2.length;
+    assert equalHashes => c1.length == c2.length;
+    assert equalHashes => d1 == d2;
+}
+*/
+
+
+/**
+ * A proposal cannot be neither executed nor canceled before it starts
+ */
+rule noExecuteOrCancelBeforeStarting(uint256 pId, method f){
+    env e;
+
+    require !isExecuted(pId) && !isCanceled(pId);
+
+    calldataarg arg;
+    f(e, arg);
+
+    assert e.block.number < proposalSnapshot(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start";
+}
+
+/**
+ * A proposal cannot be neither executed nor canceled before proposal's deadline
+ */
+rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
+    env e;
+
+    requireInvariant voteStartBeforeVoteEnd(pId);
+    require !isExecuted(pId) && !isCanceled(pId);
+
+    calldataarg arg;
+    f(e, arg);
+
+    assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start";
+}

certora/specs/GovernorCountingSimple.spec

@@ -1,23 +1,6 @@
-//////////////////////////////////////////////////////////////////////////////
+import "GovernorBase.spec"
-///////////////////// Governor.sol base definitions //////////////////////////
+
-//////////////////////////////////////////////////////////////////////////////
 methods {
-    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
-    proposalDeadline(uint256) returns uint256 envfree
-    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
-    isExecuted(uint256) returns bool envfree
-    isCanceled(uint256) returns bool envfree
-    // initialized(uint256) returns bool envfree
-
-    hasVoted(uint256, address) returns bool
-
-    castVote(uint256, uint8) returns uint256
-
-    // internal functions made public in harness:
-    _quorumReached(uint256) returns bool envfree
-    _voteSucceeded(uint256) returns bool envfree
-
-    // getter for checking the sums
     ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
 }
 
@@ -40,29 +23,19 @@ ghost sum_tracked_weight() returns uint256 {
     init_state axiom sum_tracked_weight() == 0;
 }
 
-/*
-function update_tracked_weights(uint256 pId, uint256 votes, uint256 old_votes) {
-    havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && 
-                                                    (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-    havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-}*/
-
 hook Sstore _proposalVotes[KEY uint256 pId].againstVotes uint256 votes (uint256 old_votes) STORAGE {
-    //update_tracked_weights(pId, votes, old_votes);
     havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && 
                                                     (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
     havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
 }
 
 hook Sstore _proposalVotes[KEY uint256 pId].forVotes uint256 votes (uint256 old_votes) STORAGE {
-    //update_tracked_weights(pId, votes, old_votes);
     havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && 
                                                     (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
     havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
 }
 
 hook Sstore _proposalVotes[KEY uint256 pId].abstainVotes uint256 votes (uint256 old_votes) STORAGE {
-    //update_tracked_weights(pId, votes, old_votes);
     havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && 
                                                     (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
     havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;