From 751277a1ab20f3536f83859df12081e9a4759b60 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Mon, 8 Nov 2021 17:18:36 +0200
Subject: [PATCH] MoreRulesToTheGodOfRules

---
 certora/harnesses/GovernorHarness.sol     | 32 +++++++++++++++------
 certora/scripts/GovernorCountingSimple.sh |  8 +++++-
 certora/specs/GovernorBase.spec           | 34 +++++++++++++++++++++++
 3 files changed, 64 insertions(+), 10 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index 27a5598e1..880f706d6 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -10,6 +10,15 @@ contract GovernorHarness is Governor {
         return _proposals[proposalId].canceled;
     }
 
+
+    function initialized(uint256 proposalId) public view returns (bool){
+        if (_proposals[proposalId].voteStart._deadline != 0 && _proposals[proposalId].voteEnd._deadline != 0) {
+            return true;
+        }
+        return false;
+    }
+
+
     mapping(uint256 => uint256) _quorum;
 
     function quorum(uint256 blockNumber) public view override virtual returns (uint256) {
@@ -64,6 +73,7 @@ contract GovernorHarness is Governor {
         return _votingPeriod;
     }
 
+
     constructor(string memory name) Governor(name) {}
 
     // _countVots == Sum of castVote
@@ -76,28 +86,32 @@ contract GovernorHarness is Governor {
     // mapping of count
     // countMap
 
-    mapping(uint256 => mapping(address => uint256)) counted_weight_by_id;
+    mapping(uint256 => uint256) counted_weight;
 
+    // uint decision;
+    // uint numberOfOptions;
     function _countVote(
         uint256 proposalId,
         address account,
         uint8 support,
         uint256 weight
     ) internal override virtual {
-        counted_weight_by_id[proposalId][account] += weight;
+        counted_weight[proposalId] += weight;
     }
 
-
-    mapping(uint256 => uint256) counter_vote_power_by_id;
+    mapping(uint256 => uint256) public counter_vote_power_by_id;
+    mapping(uint256 => uint256) public ghost_vote_power_by_id;
     
     function castVote(uint256 proposalId, uint8 support) public virtual override returns (uint256) {
         address voter = _msgSender();
-        // 1)
-        counter_vote_power_by_id[proposalId] += _castVote(proposalId, voter, support, "");
-        return _castVote(proposalId, voter, support, "");
         // 2)
-        // counter_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, "");
-        // return counter_vote_power;
+        ghost_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, "");
+        
+        // 1)
+        counter_vote_power_by_id[proposalId] += ghost_vote_power_by_id[proposalId];
+
+        // return _castVote(proposalId, voter, support, "");
+        return ghost_vote_power_by_id[proposalId];
     }
 
     function castVoteWithReason(
diff --git a/certora/scripts/GovernorCountingSimple.sh b/certora/scripts/GovernorCountingSimple.sh
index 95c2c2551..da013a4ef 100755
--- a/certora/scripts/GovernorCountingSimple.sh
+++ b/certora/scripts/GovernorCountingSimple.sh
@@ -1,2 +1,8 @@
 certoraRun certora/harnesses/GovernorCountingSimpleHarness.sol \
-    --verify GovernorCountingSimpleHarness:certora/specs/Privileged.spec
\ No newline at end of file
+    --verify GovernorCountingSimpleHarness:certora/specs/GovernorBase.spec \
+    --solc solc8.0 \
+    --staging \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule doubleVoting \
+    --msg "$1"
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 41ec3e735..ba8b9c93e 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -5,6 +5,11 @@ methods {
     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
@@ -23,6 +28,12 @@ methods {
 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.
@@ -116,3 +127,26 @@ rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
     assert _voteStart == voteStart_;
     assert _voteEnd == voteEnd_;
 }
+
+/**
+* Check if it's possible to vote two time. Relevant to GovernorCountingSimpleHarness.sol contract
+*/
+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 reverted, "double voting accured";
+}
+
+/**
+* 
+*/
+rule votingSumAndPower(uint256 pId, uint8 sup, method f) {
+
+}