specificSpecForSumRule

certora/harnesses/GovernorBasicHarness.sol

@@ -41,16 +41,21 @@ contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes
         return _votingPeriod;
     }
 
-/*
-    function votingDelay() public pure override returns (uint256) {
-        return _votingDelay;
-    }
 
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
 
-    function votingPeriod() public pure override returns (uint256) {
+    function _castVote(
-        return _votingPeriod;
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason
+    ) internal override virtual returns (uint256) {
+        
+        uint deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+
+        return deltaWeight;        
     }
-*/
 
     // The following functions are overrides required by Solidity.
 

certora/scripts/GovernorCountingSimple-counting.sh

@@ -0,0 +1,8 @@
+certoraRun certora/harnesses/GovernorBasicHarness.sol \
+    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
+    --solc solc8.2 \
+    --staging \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule SumOfVotesCastEqualSumOfPowerOfVoted \
+    --msg "$1"

certora/specs/GovernorBase.spec

@@ -19,20 +19,10 @@ methods {
 
     // getter for checking the sums
     counter_vote_power_by_id(uint256) returns uint256 envfree
-    ghost_vote_power_by_id(uint256) returns uint256 envfree
+    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
     counted_weight(uint256) returns uint256 envfree
 }
 
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// GHOSTS /////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-ghost vote_power_ghost() returns uint256;
-
-hook Sstore ghost_vote_power_by_id[KEY uint256 pId] uint256 current_power STORAGE{
-    havoc vote_power_ghost assuming vote_power_ghost@new() == vote_power_ghost@old() + current_power;
-}
-
 
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
@@ -92,11 +82,6 @@ rule cannotSetIfExecuted(uint256 pId, method f) filtered { f-> !f.isView }{
     assert(isExecuted(pId) => lastReverted == true, "Function did not revert after executed");
 }
 
-/*
- * sum of all votes casted is equal to the sum of voting power of those who voted
- */
-invariant SumOfVotesCastEqualSumOfPowerOfVoted(uint256 pId)
-        counted_weight(pId) == vote_power_ghost()
 
 //////////////////////////////////////////////////////////////////////////////
 /////////////////////////////////// RULES ////////////////////////////////////
@@ -174,10 +159,5 @@ rule doubleVoting(uint256 pId, uint8 sup) {
     castVote@withrevert(e, pId, sup);
     bool reverted = lastReverted;
 
-    assert reverted, "double voting accured";
+    assert votedCheck => reverted, "double voting accured";
 }
-
-/**
-* 
-*/
-//rule votingSumAndPower(uint256 pId, uint8 sup, method f) {}

certora/specs/GovernorCountingSimple.spec

@@ -0,0 +1,87 @@
+//////////////////////////////////////////////////////////////////////////////
+///////////////////// 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 envfre
+    _voteSucceeded(uint256) returns bool envfree
+
+    // getter for checking the sums
+    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
+}
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// GHOSTS /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+ghost sum_all_votes_power() returns uint256 {
+    init_state axiom sum_all_votes_power() == 0;
+}
+
+hook Sstore ghost_sum_vote_power_by_id[KEY uint256 pId] uint256 current_power (uint256 old_power) STORAGE{
+    havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
+}
+
+ghost tracked_weight(uint256) returns uint256 {
+    init_state axiom forall uint256 p. tracked_weight(p) == 0;
+}
+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;
+}
+
+//////////////////////////////////////////////////////////////////////////////
+////////////////////////////// INVARIANTS ////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
+/*
+ * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal
+ */
+invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId)
+        tracked_weight(pId) == ghost_sum_vote_power_by_id(pId)
+
+/*
+ * sum of all votes casted is equal to the sum of voting power of those who voted
+ */
+invariant SumOfVotesCastEqualSumOfPowerOfVoted()
+        sum_tracked_weight() == sum_all_votes_power()
+

contracts/governance/Governor.sol

@@ -146,12 +146,12 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor {
     /**
      * @dev Amount of votes already cast passes the threshold limit.
      */
-    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public
+    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
 
     /**
      * @dev Is the proposal successful or not.
      */
-    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public
+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
 
     /**
      * @dev Register a vote with a given support and voting weight.

contracts/governance/compatibility/GovernorCompatibilityBravo.sol

@@ -260,7 +260,7 @@ abstract contract GovernorCompatibilityBravo is
     /**
      * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
      */
-    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
         ProposalDetails storage details = _proposalDetails[proposalId];
         return quorum(proposalSnapshot(proposalId)) < details.forVotes;
     }
@@ -268,7 +268,7 @@ abstract contract GovernorCompatibilityBravo is
     /**
      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
      */
-    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
         ProposalDetails storage details = _proposalDetails[proposalId];
         return details.forVotes > details.againstVotes;
     }

contracts/governance/extensions/GovernorCountingSimple.sol

@@ -97,7 +97,7 @@ abstract contract GovernorCountingSimple is Governor {
         } else if (support == uint8(VoteType.For)) {
             proposalvote.forVotes += weight;
         } else if (support == uint8(VoteType.Abstain)) {
-            proposalvote.abstainVotes += weight;
+     //       proposalvote.abstainVotes += weight;
         } else {
             revert("GovernorVotingSimple: invalid value for enum VoteType");
         }