From c6365ef8683f320f233af4ddcaa9b928ebdfd399 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Sun, 14 Nov 2021 15:44:29 +0200
Subject: [PATCH] creating new ghost for 26 b

---
 .../GovernorCountingSimple-counting.sh        |  2 +-
 certora/specs/GovernorCountingSimple.spec     | 22 +++++++++++++++++--
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh
index 2bea57198..efb5bb59a 100644
--- a/certora/scripts/GovernorCountingSimple-counting.sh
+++ b/certora/scripts/GovernorCountingSimple-counting.sh
@@ -4,5 +4,5 @@ certoraRun certora/harnesses/GovernorBasicHarness.sol \
     --staging \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
-    --rule SumOfVotesCastEqualSumOfPowerOfVoted \
+    --rule OneIsNoMoreThanAll \
     --msg "$1"
\ No newline at end of file
diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec
index a0ae7b6d6..f1b824512 100644
--- a/certora/specs/GovernorCountingSimple.spec
+++ b/certora/specs/GovernorCountingSimple.spec
@@ -2,6 +2,7 @@ import "GovernorBase.spec"
 
 methods {
     ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
+    //_getVotes(address, uint256) returns uint256
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -41,6 +42,13 @@ hook Sstore _proposalVotes[KEY uint256 pId].abstainVotes uint256 votes (uint256
     havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
 }
 
+/*
+ghost totalVotesPossible() returns uint256{
+    init_state axiom totalVotesPossible() == 0;
+}
+
+hook Sstore _getVotes[KEY address pId][KEY uint256 blockNumber] uint256 voteWeight (uint old_voteWeight) STORAGE
+*/
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
@@ -55,6 +63,16 @@ invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 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()
+// invariant SumOfVotesCastEqualSumOfPowerOfVoted()
+//         sum_tracked_weight() == sum_all_votes_power()
 
+/*
+* totalVoted >= vote(id)
+*/
+invariant OneIsNotMoreThanAll(uint256 pId)
+        sum_all_votes_power() >= tracked_weight(pId)
+
+/*
+* totalVotesPossible (supply/weight) >= votePower(id)
+*/
+invariant possibleTotalVotes(uint pId)