aesthetic

certora/specs/GovernorBase.spec

@@ -7,6 +7,7 @@ methods {
     hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
     isExecuted(uint256) returns bool envfree
     isCanceled(uint256) returns bool envfree
+    execute(address[], uint256[], bytes[], bytes32) returns uint256
     // initialized(uint256) returns bool envfree
 
     hasVoted(uint256, address) returns bool
@@ -17,147 +18,130 @@ methods {
     _quorumReached(uint256) returns bool envfree
     _voteSucceeded(uint256) returns bool envfree
 
-    // getter for checking the sums
-    counter_vote_power_by_id(uint256) returns uint256 envfree
-    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
-    counted_weight(uint256) returns uint256 envfree
 }
-
-
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
 
-/**
+    /*
- * A proposal cannot end unless it started.
+     * A proposal cannot end unless it started.
- */
+     */
-//invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId)
+    invariant voteStartBeforeVoteEnd(uint256 pId)
-invariant voteStartBeforeVoteEnd(uint256 pId)
         (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
              && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
-        /*
-        proposalSnapshot(pId) < proposalDeadline(pId) || (proposalSnapshot(pId) == 0 && proposalDeadline(pId) == 0)
-        { preserved {
-            require initialized(pId) == true;
-        }}
-        */
-
-/**
- * A proposal cannot be both executed and canceled.
- */
-invariant noBothExecutedAndCanceled(uint256 pId) 
-        !isExecuted(pId) || !isCanceled(pId)
-
-/**
- * A proposal cannot be neither executed nor canceled before it starts
- */
-invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) 
-        e.block.number < proposalSnapshot(pId) 
-            => !isExecuted(pId) && !isCanceled(pId)
-
-/**
- * A proposal could be executed only if quorum was reached and vote succeeded
- */
-invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
-        isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
-
-/*
- * 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));
-    env e; calldataarg args;
-    f(e, args);
-    assert(isCanceled(pId) => lastReverted == true, "Function did not revert when canceled");
-}
-
-/*
- * No functions should be allowed to run after a job is deemed as executed
- */
-rule cannotSetIfExecuted(uint256 pId, method f) filtered { f-> !f.isView }{
-    require(isExecuted(pId));
-    env e; calldataarg args;
-    f(e, args);
-    assert(isExecuted(pId) => lastReverted == true, "Function did not revert after executed");
-}
 
 
-//////////////////////////////////////////////////////////////////////////////
+    /*
-/////////////////////////////////// RULES ////////////////////////////////////
+     * A proposal cannot be both executed and canceled.
-//////////////////////////////////////////////////////////////////////////////
+     */
+    invariant noBothExecutedAndCanceled(uint256 pId) 
+            !isExecuted(pId) || !isCanceled(pId)
 
 
-/**
+    /*
- * The voting must start not before the proposal’s creation time
+     * A proposal cannot be neither executed nor canceled before it starts
- */
+     */
-rule noStartBeforeCreation(uint256 pId) {
+    invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) 
-    uint previousStart = proposalSnapshot(pId);
+            e.block.number < proposalSnapshot(pId) 
-    require previousStart == 0;
+                => !isExecuted(pId) && !isCanceled(pId)
-    env e;
-    calldataarg arg;
-    propose(e, arg);
-
-    uint newStart = proposalSnapshot(pId);
-    // if created, start is after creation
-    assert newStart != 0 => newStart >= e.block.number;
-}
-
-/**
- * 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;
-}
-*/
 
 
-/**
+    /*
- * Once a proposal is created, voteStart and voteEnd are immutable
+     * A proposal could be executed only if quorum was reached and vote succeeded
- */
+     */
-rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
+    invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
-    uint _voteStart = proposalSnapshot(pId);
+            isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
-    uint _voteEnd = proposalDeadline(pId);
-    require _voteStart > 0; // proposal was created
 
-    env e;
-    calldataarg arg;
-    f(e, arg);
 
-    uint voteStart_ = proposalSnapshot(pId);
+    //////////////////////////////////////////////////////////////////////////////
-    uint voteEnd_ = proposalDeadline(pId);
+    /////////////////////////////////// RULES ////////////////////////////////////
-    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";
+    /*
-}
+     * Once a proposal is created, voteStart and voteEnd are immutable
+     */
+    rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
+        uint _voteStart = proposalSnapshot(pId);
+        uint _voteEnd = proposalDeadline(pId);
+        require _voteStart > 0; // proposal was created
+
+        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
+     */
+    rule doubleVoting(uint256 pId, uint8 sup) {
+        env e;
+        address user = e.msg.sender;
+
+        bool votedCheck = hasVoted(e, pId, user);
+        require votedCheck == true;
+
+        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.
+     */
+    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;
+    }
+    */