From 2c08f85744a18a2cd631b71c6719e48674ae9088 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sun, 26 Sep 2021 00:21:08 +0300
Subject: [PATCH 01/39] start work on governor

---
 .../GovernorCountingSimpleHarness.sol         | 29 +++++++
 certora/harnesses/GovernorHarness.sol         | 58 ++++++++++++++
 .../GovernorProposalThresholdHarness.sol      | 58 ++++++++++++++
 .../GovernorTimelockCompoundHarness.sol       | 58 ++++++++++++++
 certora/harnesses/GovernorVotesHarness.sol    | 52 ++++++++++++
 .../GovernorVotesQuorumFractionHarness.sol    | 46 +++++++++++
 certora/scripts/Governor.sh                   |  2 +
 certora/scripts/GovernorCountingSimple.sh     |  2 +
 certora/scripts/GovernorProposalThreshold.sh  |  2 +
 certora/scripts/GovernorTimelockCompound.sh   |  2 +
 certora/scripts/GovernorVotes.sh              |  2 +
 .../GovernorVotesQuorumFractionHarness.sh     |  2 +
 certora/scripts/check.sh                      |  7 ++
 certora/specs/GovernorBase.spec               | 79 +++++++++++++++++++
 certora/specs/Privileged.spec                 | 31 ++++++++
 15 files changed, 430 insertions(+)
 create mode 100644 certora/harnesses/GovernorCountingSimpleHarness.sol
 create mode 100644 certora/harnesses/GovernorHarness.sol
 create mode 100644 certora/harnesses/GovernorProposalThresholdHarness.sol
 create mode 100644 certora/harnesses/GovernorTimelockCompoundHarness.sol
 create mode 100644 certora/harnesses/GovernorVotesHarness.sol
 create mode 100644 certora/harnesses/GovernorVotesQuorumFractionHarness.sol
 create mode 100755 certora/scripts/Governor.sh
 create mode 100755 certora/scripts/GovernorCountingSimple.sh
 create mode 100755 certora/scripts/GovernorProposalThreshold.sh
 create mode 100755 certora/scripts/GovernorTimelockCompound.sh
 create mode 100755 certora/scripts/GovernorVotes.sh
 create mode 100755 certora/scripts/GovernorVotesQuorumFractionHarness.sh
 create mode 100755 certora/scripts/check.sh
 create mode 100644 certora/specs/GovernorBase.spec
 create mode 100644 certora/specs/Privileged.spec

diff --git a/certora/harnesses/GovernorCountingSimpleHarness.sol b/certora/harnesses/GovernorCountingSimpleHarness.sol
new file mode 100644
index 000000000..52e980a81
--- /dev/null
+++ b/certora/harnesses/GovernorCountingSimpleHarness.sol
@@ -0,0 +1,29 @@
+import "../../contracts/governance/extensions/GovernorCountingSimple.sol";
+
+contract GovernorCountingSimpleHarness is GovernorCountingSimple {
+
+    mapping(uint256 => uint256) _quorum;
+
+    function quorum(uint256 blockNumber) public view override virtual returns (uint256) {
+        return _quorum[blockNumber];
+    }
+
+    mapping (address => mapping (uint256 => uint256)) _getVotes;
+
+    function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) {
+        return _getVotes[account][blockNumber];
+    }
+
+    uint256 _votingDelay;
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+    constructor(string memory name) Governor(name) {}
+
+}
\ No newline at end of file
diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
new file mode 100644
index 000000000..d2df3d450
--- /dev/null
+++ b/certora/harnesses/GovernorHarness.sol
@@ -0,0 +1,58 @@
+import "../../contracts/governance/Governor.sol";
+
+contract GovernorHarness is Governor {
+
+    mapping(uint256 => uint256) _quorum;
+
+    function quorum(uint256 blockNumber) public view override virtual returns (uint256) {
+        return _quorum[blockNumber];
+    }
+
+    mapping (address => mapping (uint256 => uint256)) _getVotes;
+
+    function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) {
+        return _getVotes[account][blockNumber];
+    }
+
+    mapping (uint256 => bool) __quoromReached;
+    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+        return __quoromReached[proposalId];
+    }
+
+    mapping (uint256 => bool) __voteSucceeded;
+    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+        return __voteSucceeded[proposalId];
+    }
+
+    //string _COUNTING_MODE;
+    function COUNTING_MODE() public pure override virtual returns (string memory) {
+        return "dummy";
+    }
+
+    mapping(uint256 => mapping(address => bool)) _hasVoted;
+    function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) {
+        return _hasVoted[proposalId][account];
+    }
+
+    uint256 _votingDelay;
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal override virtual {
+        // havoc something
+    }
+
+    constructor(string memory name) Governor(name) {}
+
+}
\ No newline at end of file
diff --git a/certora/harnesses/GovernorProposalThresholdHarness.sol b/certora/harnesses/GovernorProposalThresholdHarness.sol
new file mode 100644
index 000000000..8301a76d8
--- /dev/null
+++ b/certora/harnesses/GovernorProposalThresholdHarness.sol
@@ -0,0 +1,58 @@
+import "../../contracts/governance/extensions/GovernorProposalThreshold.sol";
+
+contract GovernorProposalThresholdHarness is GovernorProposalThreshold {
+
+    mapping(uint256 => uint256) _quorum;
+
+    function quorum(uint256 blockNumber) public view override virtual returns (uint256) {
+        return _quorum[blockNumber];
+    }
+
+    mapping (address => mapping (uint256 => uint256)) _getVotes;
+
+    function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) {
+        return _getVotes[account][blockNumber];
+    }
+
+    mapping (uint256 => bool) __quoromReached;
+    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+        return __quoromReached[proposalId];
+    }
+
+    mapping (uint256 => bool) __voteSucceeded;
+    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+        return __voteSucceeded[proposalId];
+    }
+
+    //string _COUNTING_MODE;
+    function COUNTING_MODE() public pure override virtual returns (string memory) {
+        return "dummy";
+    }
+
+    mapping(uint256 => mapping(address => bool)) _hasVoted;
+    function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) {
+        return _hasVoted[proposalId][account];
+    }
+
+    uint256 _votingDelay;
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal override virtual {
+        // havoc something
+    }
+
+    constructor(string memory name) Governor(name) {}
+
+}
\ No newline at end of file
diff --git a/certora/harnesses/GovernorTimelockCompoundHarness.sol b/certora/harnesses/GovernorTimelockCompoundHarness.sol
new file mode 100644
index 000000000..5513546ab
--- /dev/null
+++ b/certora/harnesses/GovernorTimelockCompoundHarness.sol
@@ -0,0 +1,58 @@
+import "../../contracts/governance/extensions/GovernorTimelockCompound.sol";
+
+contract GovernorTimelockCompoundHarness is GovernorTimelockCompound {
+
+    mapping(uint256 => uint256) _quorum;
+
+    function quorum(uint256 blockNumber) public view override virtual returns (uint256) {
+        return _quorum[blockNumber];
+    }
+
+    mapping (address => mapping (uint256 => uint256)) _getVotes;
+
+    function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) {
+        return _getVotes[account][blockNumber];
+    }
+
+    mapping (uint256 => bool) __quoromReached;
+    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+        return __quoromReached[proposalId];
+    }
+
+    mapping (uint256 => bool) __voteSucceeded;
+    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+        return __voteSucceeded[proposalId];
+    }
+
+    //string _COUNTING_MODE;
+    function COUNTING_MODE() public pure override virtual returns (string memory) {
+        return "dummy";
+    }
+
+    mapping(uint256 => mapping(address => bool)) _hasVoted;
+    function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) {
+        return _hasVoted[proposalId][account];
+    }
+
+    uint256 _votingDelay;
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal override virtual {
+        // havoc something
+    }
+
+    constructor(string memory name, ICompoundTimelock timelock) Governor(name) GovernorTimelockCompound(timelock) {}
+
+}
\ No newline at end of file
diff --git a/certora/harnesses/GovernorVotesHarness.sol b/certora/harnesses/GovernorVotesHarness.sol
new file mode 100644
index 000000000..65a095156
--- /dev/null
+++ b/certora/harnesses/GovernorVotesHarness.sol
@@ -0,0 +1,52 @@
+import "../../contracts/governance/extensions/GovernorVotes.sol";
+
+contract GovernorVotesHarness is GovernorVotes {
+
+    mapping(uint256 => uint256) _quorum;
+
+    function quorum(uint256 blockNumber) public view override virtual returns (uint256) {
+        return _quorum[blockNumber];
+    }
+
+    mapping (uint256 => bool) __quoromReached;
+    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+        return __quoromReached[proposalId];
+    }
+
+    mapping (uint256 => bool) __voteSucceeded;
+    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+        return __voteSucceeded[proposalId];
+    }
+
+    //string _COUNTING_MODE;
+    function COUNTING_MODE() public pure override virtual returns (string memory) {
+        return "dummy";
+    }
+
+    mapping(uint256 => mapping(address => bool)) _hasVoted;
+    function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) {
+        return _hasVoted[proposalId][account];
+    }
+
+    uint256 _votingDelay;
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal override virtual {
+        // havoc something
+    }
+
+    constructor(string memory name) Governor(name) {}
+
+}
\ No newline at end of file
diff --git a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
new file mode 100644
index 000000000..3c7015eb9
--- /dev/null
+++ b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
@@ -0,0 +1,46 @@
+import "../../contracts/governance/extensions/GovernorVotesQuorumFractionGovernor.sol";
+
+contract GovernorVotesQuorumFractionHarness is GovernorVotesQuorumFraction {
+
+    mapping (uint256 => bool) __quoromReached;
+    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+        return __quoromReached[proposalId];
+    }
+
+    mapping (uint256 => bool) __voteSucceeded;
+    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+        return __voteSucceeded[proposalId];
+    }
+
+    //string _COUNTING_MODE;
+    function COUNTING_MODE() public pure override virtual returns (string memory) {
+        return "dummy";
+    }
+
+    mapping(uint256 => mapping(address => bool)) _hasVoted;
+    function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) {
+        return _hasVoted[proposalId][account];
+    }
+
+    uint256 _votingDelay;
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal override virtual {
+        // havoc something
+    }
+
+    constructor(string memory name) Governor(name) {}
+
+}
\ No newline at end of file
diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
new file mode 100755
index 000000000..4caada718
--- /dev/null
+++ b/certora/scripts/Governor.sh
@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorHarness.sol \
+    --verify GovernorHarness:certora/specs/Privileged.spec
\ No newline at end of file
diff --git a/certora/scripts/GovernorCountingSimple.sh b/certora/scripts/GovernorCountingSimple.sh
new file mode 100755
index 000000000..95c2c2551
--- /dev/null
+++ b/certora/scripts/GovernorCountingSimple.sh
@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorCountingSimpleHarness.sol \
+    --verify GovernorCountingSimpleHarness:certora/specs/Privileged.spec
\ No newline at end of file
diff --git a/certora/scripts/GovernorProposalThreshold.sh b/certora/scripts/GovernorProposalThreshold.sh
new file mode 100755
index 000000000..cb10572fc
--- /dev/null
+++ b/certora/scripts/GovernorProposalThreshold.sh
@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorProposalThresholdHarness.sol \
+    --verify GovernorProposalThresholdHarness:certora/specs/Privileged.spec
\ No newline at end of file
diff --git a/certora/scripts/GovernorTimelockCompound.sh b/certora/scripts/GovernorTimelockCompound.sh
new file mode 100755
index 000000000..9cbdd1ea0
--- /dev/null
+++ b/certora/scripts/GovernorTimelockCompound.sh
@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorTimelockCompoundHarness.sol \
+    --verify GovernorTimelockCompoundHarness:certora/specs/Privileged.spec
\ No newline at end of file
diff --git a/certora/scripts/GovernorVotes.sh b/certora/scripts/GovernorVotes.sh
new file mode 100755
index 000000000..1dc476445
--- /dev/null
+++ b/certora/scripts/GovernorVotes.sh
@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorVotesHarness.sol \
+    --verify GovernorVotesHarness:certora/specs/Privileged.spec
\ No newline at end of file
diff --git a/certora/scripts/GovernorVotesQuorumFractionHarness.sh b/certora/scripts/GovernorVotesQuorumFractionHarness.sh
new file mode 100755
index 000000000..239339ade
--- /dev/null
+++ b/certora/scripts/GovernorVotesQuorumFractionHarness.sh
@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorVotesQuorumFractionHarness.sol \
+    --verify GovernorVotesQuorumFractionHarness:certora/specs/Privileged.spec
\ No newline at end of file
diff --git a/certora/scripts/check.sh b/certora/scripts/check.sh
new file mode 100755
index 000000000..0cb980dc3
--- /dev/null
+++ b/certora/scripts/check.sh
@@ -0,0 +1,7 @@
+echo "Usage: Contract Spec"
+echo "e.g. GovernorVotes Privileged"
+Contract=$1
+Spec=$2
+shift 2
+certoraRun certora/harnesses/${Contract}Harness.sol \
+    --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@"
\ No newline at end of file
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
new file mode 100644
index 000000000..58c07582f
--- /dev/null
+++ b/certora/specs/GovernorBase.spec
@@ -0,0 +1,79 @@
+// Governor.sol base definitions
+methods {
+    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
+}
+ghost proposalVoteStart(uint256) returns uint64 {
+    init_state axiom forall uint256 pId. proposalVoteStart(pId) == 0;
+}
+ghost proposalVoteEnd(uint256) returns uint64 {
+    init_state axiom forall uint256 pId. proposalVoteEnd(pId) == 0;
+}
+ghost proposalExecuted(uint256) returns bool {
+    init_state axiom forall uint256 pId. !proposalExecuted(pId);
+}
+ghost proposalCanceled(uint256) returns bool {
+    init_state axiom forall uint256 pId. !proposalCanceled(pId);
+}
+
+hook Sstore _proposals[KEY uint256 pId].(offset 0) uint64 newValue STORAGE {
+    havoc proposalVoteStart assuming (
+        proposalVoteStart@new(pId) == newValue
+        && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
+    );
+}
+
+hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0) STORAGE {
+    require proposalVoteStart(pId) == value;
+}
+
+
+hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE {
+    havoc proposalVoteEnd assuming (
+        proposalVoteEnd@new(pId) == newValue
+        && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2))
+    );
+}
+
+hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE {
+    require proposalVoteEnd(pId) == value;
+}
+
+rule sanityCheckVoteStart(method f, uint256 pId) {
+    uint64 preGhost = proposalVoteStart(pId);
+    uint256 pre = proposalSnapshot(pId);
+
+    env e;
+    calldataarg arg;
+    f(e, arg);
+
+    uint64 postGhost = proposalVoteStart(pId);
+    uint256 post = proposalSnapshot(pId);
+
+    assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes";
+    assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end";
+}
+
+rule sanityCheckVoteEnd(method f, uint256 pId) {
+    uint64 preGhost = proposalVoteEnd(pId);
+    uint256 pre = proposalSnapshot(pId);
+
+    env e;
+    calldataarg arg;
+    f(e, arg);
+
+    uint64 postGhost = proposalVoteEnd(pId);
+    uint256 post = proposalSnapshot(pId);
+
+    assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes";
+    assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end";
+}
+
+/**
+ * A proposal cannot end unless it started.
+ */
+invariant voteStartBeforeVoteEnd(uint256 pId) proposalVoteStart(pId) < proposalVoteEnd(pId)
+
+/**
+ * A proposal cannot be both executed and canceled.
+ */
+invariant noBothExecutedAndCanceled(uint256 pId) !proposalExecuted(pId) || !proposalCanceled(pId)
\ No newline at end of file
diff --git a/certora/specs/Privileged.spec b/certora/specs/Privileged.spec
new file mode 100644
index 000000000..f9615a619
--- /dev/null
+++ b/certora/specs/Privileged.spec
@@ -0,0 +1,31 @@
+definition knownAsNonPrivileged(method f) returns bool  = false
+/*	( 	f.selector == isWhitelistedOtoken(address).selector  ||
+		f.selector == isWhitelistedProduct(address,address,address,bool).selector ||
+		f.selector == owner().selector ||
+    	f.selector == isWhitelistedCallee(address).selector ||
+		f.selector == whitelistOtoken(address).selector ||
+		f.selector == addressBook().selector || 
+		f.selector == isWhitelistedCollateral(address).selector )*/; 
+
+
+
+rule privilegedOperation(method f, address privileged)
+description "$f can be called by more than one user without reverting"
+{
+	env e1;
+	calldataarg arg;
+	require !knownAsNonPrivileged(f);
+	require e1.msg.sender == privileged;
+
+	storage initialStorage = lastStorage;
+	invoke f(e1, arg); // privileged succeeds executing candidate privileged operation.
+	bool firstSucceeded = !lastReverted;
+
+	env e2;
+	calldataarg arg2;
+	require e2.msg.sender != privileged;
+	invoke f(e2, arg2) at initialStorage; // unprivileged
+	bool secondSucceeded = !lastReverted;
+
+	assert  !(firstSucceeded && secondSucceeded), "${f.selector} can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged";
+}

From f239fa56dd35c7b5b52303646311c07dcef15117 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sun, 26 Sep 2021 00:25:59 +0300
Subject: [PATCH 02/39] Back to expected pattern?

---
 certora/specs/GovernorBase.spec | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 58c07582f..85c20162b 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -15,14 +15,14 @@ ghost proposalCanceled(uint256) returns bool {
     init_state axiom forall uint256 pId. !proposalCanceled(pId);
 }
 
-hook Sstore _proposals[KEY uint256 pId].(offset 0) uint64 newValue STORAGE {
+hook Sstore _proposals[KEY uint256 pId].(offset 0).(offset 0) uint64 newValue STORAGE {
     havoc proposalVoteStart assuming (
         proposalVoteStart@new(pId) == newValue
         && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
     );
 }
 
-hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0) STORAGE {
+hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0).(offset 0) STORAGE {
     require proposalVoteStart(pId) == value;
 }
 

From fdc4b0cf239df941aaf5fb8ebdad5c6c8981a2c9 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sun, 26 Sep 2021 01:39:27 +0300
Subject: [PATCH 03/39] fixes

---
 certora/specs/GovernorBase.spec | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 85c20162b..99c712872 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -2,6 +2,7 @@
 methods {
     proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
 }
+
 ghost proposalVoteStart(uint256) returns uint64 {
     init_state axiom forall uint256 pId. proposalVoteStart(pId) == 0;
 }
@@ -15,27 +16,27 @@ ghost proposalCanceled(uint256) returns bool {
     init_state axiom forall uint256 pId. !proposalCanceled(pId);
 }
 
-hook Sstore _proposals[KEY uint256 pId].(offset 0).(offset 0) uint64 newValue STORAGE {
+hook Sstore _proposals[KEY uint256 pId] uint64 newValue STORAGE {
     havoc proposalVoteStart assuming (
-        proposalVoteStart@new(pId) == newValue
+        proposalVoteStart@new(pId) == newValue & (max_uint64-1)
         && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
     );
 }
 
-hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0).(offset 0) STORAGE {
-    require proposalVoteStart(pId) == value;
+hook Sload uint64 value _proposals[KEY uint256 pId] STORAGE {
+    require proposalVoteStart(pId) == value & (max_uint64-1);
 }
 
 
 hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE {
     havoc proposalVoteEnd assuming (
-        proposalVoteEnd@new(pId) == newValue
+        proposalVoteEnd@new(pId) == newValue & (max_uint64-1)
         && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2))
     );
 }
 
 hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE {
-    require proposalVoteEnd(pId) == value;
+    require proposalVoteEnd(pId) == value & (max_uint64-1);
 }
 
 rule sanityCheckVoteStart(method f, uint256 pId) {

From 4c1d5e01c636ad8a0e822a6f1249317900c4f59c Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sun, 26 Sep 2021 01:43:16 +0300
Subject: [PATCH 04/39] fixes

---
 certora/specs/GovernorBase.spec | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 99c712872..32b0fd21b 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -16,27 +16,29 @@ ghost proposalCanceled(uint256) returns bool {
     init_state axiom forall uint256 pId. !proposalCanceled(pId);
 }
 
+definition mask_uint64() returns uint256 = max_uint64 - 1;
+
 hook Sstore _proposals[KEY uint256 pId] uint64 newValue STORAGE {
     havoc proposalVoteStart assuming (
-        proposalVoteStart@new(pId) == newValue & (max_uint64-1)
+        proposalVoteStart@new(pId) == newValue & mask_uint64()
         && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
     );
 }
 
 hook Sload uint64 value _proposals[KEY uint256 pId] STORAGE {
-    require proposalVoteStart(pId) == value & (max_uint64-1);
+    require proposalVoteStart(pId) == value & mask_uint64();
 }
 
 
 hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE {
     havoc proposalVoteEnd assuming (
-        proposalVoteEnd@new(pId) == newValue & (max_uint64-1)
+        proposalVoteEnd@new(pId) == newValue & mask_uint64()
         && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2))
     );
 }
 
 hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE {
-    require proposalVoteEnd(pId) == value & (max_uint64-1);
+    require proposalVoteEnd(pId) == value & mask_uint64();
 }
 
 rule sanityCheckVoteStart(method f, uint256 pId) {

From 22030f2fd31ac126d1ecedf99391ca9a21b934dd Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Thu, 7 Oct 2021 11:58:47 +0300
Subject: [PATCH 05/39] rule drafts

---
 certora/harnesses/GovernorHarness.sol |  4 +-
 certora/specs/GovernorBase.spec       | 72 ++++++++++++++++++++++++++-
 2 files changed, 73 insertions(+), 3 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index d2df3d450..332f8b863 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -15,12 +15,12 @@ contract GovernorHarness is Governor {
     }
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 32b0fd21b..60949c987 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -1,6 +1,11 @@
 // Governor.sol base definitions
 methods {
     proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
+    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
+
+    // internal functions made public in harness:
+    _quorumReached(uint256) returns bool envfree
+    _voteSucceeded(uint256) returns bool envfree
 }
 
 ghost proposalVoteStart(uint256) returns uint64 {
@@ -79,4 +84,69 @@ invariant voteStartBeforeVoteEnd(uint256 pId) proposalVoteStart(pId) < proposalV
 /**
  * A proposal cannot be both executed and canceled.
  */
-invariant noBothExecutedAndCanceled(uint256 pId) !proposalExecuted(pId) || !proposalCanceled(pId)
\ No newline at end of file
+invariant noBothExecutedAndCanceled(uint256 pId) !proposalExecuted(pId) || !proposalCanceled(pId)
+
+/**
+ * A proposal cannot be executed nor canceled before it starts
+ */
+invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) e.block.timestamp < proposalVoteStart(pId) => !proposalExecuted(pId) && !proposalCanceled(pId)
+
+/**
+ * The voting must start not before the proposal’s creation time
+ */
+rule noStartBeforeCreation(uint256 pId) {
+    uint previousStart = proposalVoteStart(pId);
+    require previousStart == 0;
+    env e;
+    calldataarg arg;
+    propose(e, arg);
+
+    uint newStart = proposalVoteStart(pId);
+    // if created, start is after creation
+    assert newStart != 0 => newStart > e.block.timestamp;
+}
+
+/**
+ * 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 could be executed only if quorum was reached and vote succeeded
+ */
+invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) proposalExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
+
+/**
+ * Once a proposal is created, voteStart and voteEnd are immutable
+ */
+rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
+    uint _voteStart = proposalVoteStart(pId);
+    uint _voteEnd = proposalVoteEnd(pId);
+    require _voteStart > 0; // proposal was created
+
+    env e;
+    calldataarg arg;
+    f(e, arg);
+
+    uint voteStart_ = proposalVoteStart(pId);
+    uint voteEnd_ = proposalVoteEnd(pId);
+    assert _voteStart == voteStart_;
+    assert _voteEnd == voteEnd_;
+}
\ No newline at end of file

From 6776cc6ee47ac0109e24c86af5951958adfd082c Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Tue, 2 Nov 2021 14:01:48 +0200
Subject: [PATCH 06/39] ignore certora's generated files

---
 .gitignore | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.gitignore b/.gitignore
index 0a62cf0b3..c60c5d945 100644
--- a/.gitignore
+++ b/.gitignore
@@ -57,3 +57,8 @@ allFiredEvents
 # hardhat
 cache
 artifacts
+
+# Certora
+.certora*
+.last_confs
+certora_*

From cac49bfc2ee335aae66689598a799e1c2ecf9db7 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Wed, 3 Nov 2021 17:05:06 +0200
Subject: [PATCH 07/39] sanity rule preparations

---
 .../harnesses/GovernorProposalThresholdHarness.sol |  9 +++++++--
 .../harnesses/GovernorTimelockCompoundHarness.sol  |  4 ++--
 certora/harnesses/GovernorVotesHarness.sol         |  7 +++----
 .../GovernorVotesQuorumFractionHarness.sol         |  6 +++---
 certora/scripts/check.sh                           |  4 +++-
 certora/scripts/sanity.sh                          |  9 +++++++++
 certora/specs/sanity.spec                          | 14 ++++++++++++++
 contracts/governance/Governor.sol                  |  4 ++--
 .../extensions/GovernorCountingSimple.sol          |  4 ++--
 9 files changed, 45 insertions(+), 16 deletions(-)
 create mode 100644 certora/scripts/sanity.sh
 create mode 100644 certora/specs/sanity.spec

diff --git a/certora/harnesses/GovernorProposalThresholdHarness.sol b/certora/harnesses/GovernorProposalThresholdHarness.sol
index 8301a76d8..1d0559a60 100644
--- a/certora/harnesses/GovernorProposalThresholdHarness.sol
+++ b/certora/harnesses/GovernorProposalThresholdHarness.sol
@@ -15,12 +15,12 @@ contract GovernorProposalThresholdHarness is GovernorProposalThreshold {
     }
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
@@ -53,6 +53,11 @@ contract GovernorProposalThresholdHarness is GovernorProposalThreshold {
         // havoc something
     }
 
+    uint256 _proposalThreshold;
+    function proposalThreshold() public view override virtual returns (uint256) {
+        return _proposalThreshold;
+    }
+
     constructor(string memory name) Governor(name) {}
 
 }
\ No newline at end of file
diff --git a/certora/harnesses/GovernorTimelockCompoundHarness.sol b/certora/harnesses/GovernorTimelockCompoundHarness.sol
index 5513546ab..f8a85e53f 100644
--- a/certora/harnesses/GovernorTimelockCompoundHarness.sol
+++ b/certora/harnesses/GovernorTimelockCompoundHarness.sol
@@ -15,12 +15,12 @@ contract GovernorTimelockCompoundHarness is GovernorTimelockCompound {
     }
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
diff --git a/certora/harnesses/GovernorVotesHarness.sol b/certora/harnesses/GovernorVotesHarness.sol
index 65a095156..8ed638e41 100644
--- a/certora/harnesses/GovernorVotesHarness.sol
+++ b/certora/harnesses/GovernorVotesHarness.sol
@@ -9,12 +9,12 @@ contract GovernorVotesHarness is GovernorVotes {
     }
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
@@ -47,6 +47,5 @@ contract GovernorVotesHarness is GovernorVotes {
         // havoc something
     }
 
-    constructor(string memory name) Governor(name) {}
-
+    constructor(ERC20Votes tokenAddr) GovernorVotes(tokenAddr) {}
 }
\ No newline at end of file
diff --git a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
index 3c7015eb9..65be741d4 100644
--- a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
+++ b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
@@ -1,14 +1,14 @@
-import "../../contracts/governance/extensions/GovernorVotesQuorumFractionGovernor.sol";
+import "../../contracts/governance/extensions/GovernorVotesQuorumFraction.sol";
 
 contract GovernorVotesQuorumFractionHarness is GovernorVotesQuorumFraction {
 
     mapping (uint256 => bool) __quoromReached;
-    function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) {
+    function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
     mapping (uint256 => bool) __voteSucceeded;
-    function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
diff --git a/certora/scripts/check.sh b/certora/scripts/check.sh
index 0cb980dc3..cdb356e90 100755
--- a/certora/scripts/check.sh
+++ b/certora/scripts/check.sh
@@ -4,4 +4,6 @@ Contract=$1
 Spec=$2
 shift 2
 certoraRun certora/harnesses/${Contract}Harness.sol \
-    --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@"
\ No newline at end of file
+    --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@" \
+    --solc solc8.0
+    
\ No newline at end of file
diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh
new file mode 100644
index 000000000..4db90ebff
--- /dev/null
+++ b/certora/scripts/sanity.sh
@@ -0,0 +1,9 @@
+for f in certora/harnesses/*.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+    --solc solc8.0    
+done
\ No newline at end of file
diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec
new file mode 100644
index 000000000..e08f68845
--- /dev/null
+++ b/certora/specs/sanity.spec
@@ -0,0 +1,14 @@
+/*
+This rule looks for a non-reverting execution path to each method, including those overridden in the harness.
+A method has such an execution path if it violates this rule.
+How it works:
+    - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails.
+    - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously.
+*/
+	
+rule sanity(method f) {
+    env e;
+    calldataarg arg;
+    f(e, arg);
+    assert false;
+}
\ No newline at end of file
diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index 741e02f7d..12aa1950b 100644
--- a/contracts/governance/Governor.sol
+++ b/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) internal view virtual returns (bool);
+    function _quorumReached(uint256 proposalId) public view virtual returns (bool);
 
     /**
      * @dev Is the proposal successful or not.
      */
-    function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool);
 
     /**
      * @dev Register a vote with a given support and voting weight.
diff --git a/contracts/governance/extensions/GovernorCountingSimple.sol b/contracts/governance/extensions/GovernorCountingSimple.sol
index 399f8d7fe..00f4d4aa8 100644
--- a/contracts/governance/extensions/GovernorCountingSimple.sol
+++ b/contracts/governance/extensions/GovernorCountingSimple.sol
@@ -63,7 +63,7 @@ abstract contract GovernorCountingSimple is Governor {
     /**
      * @dev See {Governor-_quorumReached}.
      */
-    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
         ProposalVote storage proposalvote = _proposalVotes[proposalId];
 
         return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
@@ -72,7 +72,7 @@ abstract contract GovernorCountingSimple is Governor {
     /**
      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
      */
-    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
         ProposalVote storage proposalvote = _proposalVotes[proposalId];
 
         return proposalvote.forVotes > proposalvote.againstVotes;

From 72d4e9c29c0acbf757c295e85d79b46049eda785 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Wed, 3 Nov 2021 17:09:27 +0200
Subject: [PATCH 08/39] multiple inheritance is tricky

---
 certora/harnesses/GovernorVotesHarness.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/harnesses/GovernorVotesHarness.sol b/certora/harnesses/GovernorVotesHarness.sol
index 8ed638e41..3e06c8daa 100644
--- a/certora/harnesses/GovernorVotesHarness.sol
+++ b/certora/harnesses/GovernorVotesHarness.sol
@@ -47,5 +47,5 @@ contract GovernorVotesHarness is GovernorVotes {
         // havoc something
     }
 
-    constructor(ERC20Votes tokenAddr) GovernorVotes(tokenAddr) {}
+    constructor(ERC20Votes tokenAddr, string memory name) GovernorVotes(tokenAddr) Governor(name) {}
 }
\ No newline at end of file

From a7104355359f2b64eae8acf39ac2c7377ee30317 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Wed, 3 Nov 2021 17:24:35 +0200
Subject: [PATCH 09/39] multiple inheritance is tricky x2

---
 certora/harnesses/GovernorVotesQuorumFractionHarness.sol | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
index 65be741d4..86ae202ad 100644
--- a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
+++ b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol
@@ -41,6 +41,7 @@ contract GovernorVotesQuorumFractionHarness is GovernorVotesQuorumFraction {
         // havoc something
     }
 
-    constructor(string memory name) Governor(name) {}
+    constructor(ERC20Votes tokenAddr, string memory name, uint256 quorumNumeratorValue) 
+            GovernorVotesQuorumFraction(quorumNumeratorValue) GovernorVotes(tokenAddr) Governor(name) {}
 
 }
\ No newline at end of file

From 69f87ad916810b9bd99c30ae9d1465a01932f1f7 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 11:27:44 +0200
Subject: [PATCH 10/39] slight script changes and ghost fix

---
 certora/harnesses/GovernorHarness.sol | 13 +++++++++++++
 certora/scripts/Governor.sh           |  8 +++++++-
 certora/scripts/check.sh              |  2 +-
 certora/scripts/sanity.sh             |  4 +++-
 certora/specs/GovernorBase.spec       | 28 +++++++++++++++++----------
 contracts/governance/Governor.sol     |  4 ++--
 6 files changed, 44 insertions(+), 15 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index 332f8b863..f12a3ab4e 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -8,42 +8,55 @@ contract GovernorHarness is Governor {
         return _quorum[blockNumber];
     }
 
+
     mapping (address => mapping (uint256 => uint256)) _getVotes;
 
     function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) {
         return _getVotes[account][blockNumber];
     }
 
+
     mapping (uint256 => bool) __quoromReached;
+
     function _quorumReached(uint256 proposalId) public view override virtual returns (bool) {
         return __quoromReached[proposalId];
     }
 
+
     mapping (uint256 => bool) __voteSucceeded;
+
     function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) {
         return __voteSucceeded[proposalId];
     }
 
+
     //string _COUNTING_MODE;
     function COUNTING_MODE() public pure override virtual returns (string memory) {
         return "dummy";
     }
 
+
     mapping(uint256 => mapping(address => bool)) _hasVoted;
+
     function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) {
         return _hasVoted[proposalId][account];
     }
 
+
     uint256 _votingDelay;
+
     function votingDelay() public view override virtual returns (uint256) {
         return _votingDelay;
     }
 
+
     uint256 _votingPeriod;
+    
     function votingPeriod() public view override virtual returns (uint256) {
         return _votingPeriod;
     }
 
+
     function _countVote(
         uint256 proposalId,
         address account,
diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
index 4caada718..cba7edf6b 100755
--- a/certora/scripts/Governor.sh
+++ b/certora/scripts/Governor.sh
@@ -1,2 +1,8 @@
 certoraRun certora/harnesses/GovernorHarness.sol \
-    --verify GovernorHarness:certora/specs/Privileged.spec
\ No newline at end of file
+    --verify GovernorHarness:certora/specs/GovernorBase.spec \
+    --solc solc8.0 \
+    --staging \
+    --msg $1 \
+    --disableLocalTypeChecking \
+    --rule voteStartBeforeVoteEnd
+
diff --git a/certora/scripts/check.sh b/certora/scripts/check.sh
index cdb356e90..e3291eb1c 100755
--- a/certora/scripts/check.sh
+++ b/certora/scripts/check.sh
@@ -5,5 +5,5 @@ Spec=$2
 shift 2
 certoraRun certora/harnesses/${Contract}Harness.sol \
     --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@" \
-    --solc solc8.0
+    --solc solc8.0 --staging --rule noBothExecutedAndCanceled
     
\ No newline at end of file
diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh
index 4db90ebff..0da31d15e 100644
--- a/certora/scripts/sanity.sh
+++ b/certora/scripts/sanity.sh
@@ -5,5 +5,7 @@ do
     echo ${file%.*}
     certoraRun certora/harnesses/$file \
     --verify ${file%.*}:certora/specs/sanity.spec "$@" \
-    --solc solc8.0    
+    --solc solc8.0 \
+    --staging \
+    --msg "sanity ${file}"
 done
\ No newline at end of file
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 60949c987..b54f8c0e8 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -21,31 +21,34 @@ ghost proposalCanceled(uint256) returns bool {
     init_state axiom forall uint256 pId. !proposalCanceled(pId);
 }
 
-definition mask_uint64() returns uint256 = max_uint64 - 1;
-
-hook Sstore _proposals[KEY uint256 pId] uint64 newValue STORAGE {
+hook Sstore _proposals[KEY uint256 pId].voteStart._deadline uint64 newValue STORAGE {
     havoc proposalVoteStart assuming (
-        proposalVoteStart@new(pId) == newValue & mask_uint64()
+        proposalVoteStart@new(pId) == newValue
         && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
     );
 }
 
-hook Sload uint64 value _proposals[KEY uint256 pId] STORAGE {
-    require proposalVoteStart(pId) == value & mask_uint64();
+hook Sload uint64 value _proposals[KEY uint256 pId].voteStart._deadline STORAGE {
+    require proposalVoteStart(pId) == value;
 }
 
 
-hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE {
+hook Sstore _proposals[KEY uint256 pId].voteEnd._deadline uint64 newValue STORAGE {
     havoc proposalVoteEnd assuming (
-        proposalVoteEnd@new(pId) == newValue & mask_uint64()
+        proposalVoteEnd@new(pId) == newValue
         && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2))
     );
 }
 
-hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE {
-    require proposalVoteEnd(pId) == value & mask_uint64();
+hook Sload uint64 value _proposals[KEY uint256 pId].voteEnd._deadline STORAGE {
+    require proposalVoteEnd(pId) == value;
 }
 
+//////////////////////////////////////////////////////////////////////////////
+//////////////////////////// SANITY CHECKS ///////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+//
+
 rule sanityCheckVoteStart(method f, uint256 pId) {
     uint64 preGhost = proposalVoteStart(pId);
     uint256 pre = proposalSnapshot(pId);
@@ -76,6 +79,11 @@ rule sanityCheckVoteEnd(method f, uint256 pId) {
     assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end";
 }
 
+//////////////////////////////////////////////////////////////////////////////
+////////////////////////////// INVARIANTS ////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+//
+
 /**
  * A proposal cannot end unless it started.
  */
diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index 12aa1950b..c8c8e709c 100644
--- a/contracts/governance/Governor.sol
+++ b/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);
+    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public
 
     /**
      * @dev Is the proposal successful or not.
      */
-    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool);
+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public
 
     /**
      * @dev Register a vote with a given support and voting weight.

From e888ea4ccbafcd2533cd47a3fd5c3bc5c608f5b9 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 11:48:55 +0200
Subject: [PATCH 11/39] Hooks fixed

---
 certora/specs/GovernorBase.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index b54f8c0e8..ae7d0a073 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -82,7 +82,7 @@ rule sanityCheckVoteEnd(method f, uint256 pId) {
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
-//
+// 
 
 /**
  * A proposal cannot end unless it started.

From 6876df00aef0a676f5cb149eca84eeba4e3ff8d5 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 11:50:40 +0200
Subject: [PATCH 12/39] slight changes change for convenience +
 disableLocalTypeChecking flag for the hooks

---
 certora/scripts/Governor.sh | 1 -
 certora/scripts/sanity.sh   | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
index cba7edf6b..8450e7d03 100755
--- a/certora/scripts/Governor.sh
+++ b/certora/scripts/Governor.sh
@@ -5,4 +5,3 @@ certoraRun certora/harnesses/GovernorHarness.sol \
     --msg $1 \
     --disableLocalTypeChecking \
     --rule voteStartBeforeVoteEnd
-
diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh
index 0da31d15e..d157d6d42 100644
--- a/certora/scripts/sanity.sh
+++ b/certora/scripts/sanity.sh
@@ -8,4 +8,4 @@ do
     --solc solc8.0 \
     --staging \
     --msg "sanity ${file}"
-done
\ No newline at end of file
+done

From c00d951e06ee7bf0bd1865a580b43f91397f7b1c Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 11:51:14 +0200
Subject: [PATCH 13/39] Harness private to public

---
 contracts/governance/Governor.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index c8c8e709c..1040f9e5b 100644
--- a/contracts/governance/Governor.sol
+++ b/contracts/governance/Governor.sol
@@ -146,7 +146,7 @@ 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 
 
     /**
      * @dev Is the proposal successful or not.

From d6e79f4366b3629efc94723ae377e448e4087a07 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 12:29:04 +0200
Subject: [PATCH 14/39] Harness private to public

---
 contracts/governance/Governor.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index 1040f9e5b..c8c8e709c 100644
--- a/contracts/governance/Governor.sol
+++ b/contracts/governance/Governor.sol
@@ -146,7 +146,7 @@ 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
 
     /**
      * @dev Is the proposal successful or not.

From 21b84349d4396cc1295be7fd9529aab50ae21617 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 12:35:11 +0200
Subject: [PATCH 15/39] slight changes in scripts + disableLocalTypeChecking

---
 certora/scripts/Governor.sh | 2 +-
 certora/scripts/sanity.sh   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
index 8450e7d03..97486c2fa 100755
--- a/certora/scripts/Governor.sh
+++ b/certora/scripts/Governor.sh
@@ -4,4 +4,4 @@ certoraRun certora/harnesses/GovernorHarness.sol \
     --staging \
     --msg $1 \
     --disableLocalTypeChecking \
-    --rule voteStartBeforeVoteEnd
+    --rule voteStartBeforeVoteEnd
\ No newline at end of file
diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh
index d157d6d42..0da31d15e 100644
--- a/certora/scripts/sanity.sh
+++ b/certora/scripts/sanity.sh
@@ -8,4 +8,4 @@ do
     --solc solc8.0 \
     --staging \
     --msg "sanity ${file}"
-done
+done
\ No newline at end of file

From a2960e22b9a5357cc9d8082beda6b23505254c8f Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 12:35:37 +0200
Subject: [PATCH 16/39] hooks fixed

---
 certora/specs/GovernorBase.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index ae7d0a073..b54f8c0e8 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -82,7 +82,7 @@ rule sanityCheckVoteEnd(method f, uint256 pId) {
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
-// 
+//
 
 /**
  * A proposal cannot end unless it started.

From f7cc2548f38c4d763f64c479d682e52d1670482a Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Thu, 4 Nov 2021 12:54:23 +0200
Subject: [PATCH 17/39] scripts settings added

---
 certora/scripts/Governor.sh     | 4 +++-
 certora/scripts/sanity.sh       | 7 ++++---
 certora/specs/GovernorBase.spec | 1 -
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
index 97486c2fa..8b177300d 100755
--- a/certora/scripts/Governor.sh
+++ b/certora/scripts/Governor.sh
@@ -4,4 +4,6 @@ certoraRun certora/harnesses/GovernorHarness.sol \
     --staging \
     --msg $1 \
     --disableLocalTypeChecking \
-    --rule voteStartBeforeVoteEnd
\ No newline at end of file
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4
+    --rule sanityCheckVoteStart
diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh
index 0da31d15e..7ffaf52f7 100644
--- a/certora/scripts/sanity.sh
+++ b/certora/scripts/sanity.sh
@@ -5,7 +5,8 @@ do
     echo ${file%.*}
     certoraRun certora/harnesses/$file \
     --verify ${file%.*}:certora/specs/sanity.spec "$@" \
-    --solc solc8.0 \
-    --staging \
-    --msg "sanity ${file}"
+    --solc solc8.0 --staging \
+    --optimistic_loop \
+    --msg "checking sanity on ${file%.*}"
+    --settings -copyLoopUnroll=4
 done
\ No newline at end of file
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index b54f8c0e8..17a37b88e 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -32,7 +32,6 @@ hook Sload uint64 value _proposals[KEY uint256 pId].voteStart._deadline STORAGE
     require proposalVoteStart(pId) == value;
 }
 
-
 hook Sstore _proposals[KEY uint256 pId].voteEnd._deadline uint64 newValue STORAGE {
     havoc proposalVoteEnd assuming (
         proposalVoteEnd@new(pId) == newValue

From bfa1dd3756ced51d00a5963f3940fe56cf0c7077 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 4 Nov 2021 15:03:28 +0200
Subject: [PATCH 18/39] quotes on var in msg

---
 certora/scripts/Governor.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
index 8b177300d..c31b43cd9 100755
--- a/certora/scripts/Governor.sh
+++ b/certora/scripts/Governor.sh
@@ -2,8 +2,8 @@ certoraRun certora/harnesses/GovernorHarness.sol \
     --verify GovernorHarness:certora/specs/GovernorBase.spec \
     --solc solc8.0 \
     --staging \
-    --msg $1 \
-    --disableLocalTypeChecking \
     --optimistic_loop \
-    --settings -copyLoopUnroll=4
-    --rule sanityCheckVoteStart
+    --disableLocalTypeChecking \
+    --settings -copyLoopUnroll=4 \
+    --rule voteStartBeforeVoteEnd \
+    --msg "$1"

From f08ee568b9c7159b98bbd0c0f816f648f90cdbed Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Thu, 4 Nov 2021 17:54:26 +0200
Subject: [PATCH 19/39] checkingInvariantsWithoutGhosts

---
 certora/harnesses/GovernorHarness.sol |  8 ++++++++
 certora/scripts/Governor.sh           |  3 +--
 certora/specs/GovernorBase.spec       | 22 +++++++++++++++-------
 contracts/governance/Governor.sol     |  2 +-
 4 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index f12a3ab4e..28e556556 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -2,6 +2,14 @@ import "../../contracts/governance/Governor.sol";
 
 contract GovernorHarness is Governor {
 
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+    
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
     mapping(uint256 => uint256) _quorum;
 
     function quorum(uint256 blockNumber) public view override virtual returns (uint256) {
diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
index c31b43cd9..ccdf90203 100755
--- a/certora/scripts/Governor.sh
+++ b/certora/scripts/Governor.sh
@@ -3,7 +3,6 @@ certoraRun certora/harnesses/GovernorHarness.sol \
     --solc solc8.0 \
     --staging \
     --optimistic_loop \
-    --disableLocalTypeChecking \
     --settings -copyLoopUnroll=4 \
-    --rule voteStartBeforeVoteEnd \
+    --rule noExecuteOrCancelBeforeStarting \
     --msg "$1"
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 17a37b88e..cbe376bf0 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -2,25 +2,32 @@
 methods {
     proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
     hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
+    isExecuted(uint256) returns bool envfree
+    isCanceled(uint256) returns bool envfree
 
     // internal functions made public in harness:
     _quorumReached(uint256) returns bool envfree
     _voteSucceeded(uint256) returns bool envfree
 }
 
+/*
 ghost proposalVoteStart(uint256) returns uint64 {
     init_state axiom forall uint256 pId. proposalVoteStart(pId) == 0;
 }
 ghost proposalVoteEnd(uint256) returns uint64 {
     init_state axiom forall uint256 pId. proposalVoteEnd(pId) == 0;
 }
+*/
+
+/*
 ghost proposalExecuted(uint256) returns bool {
     init_state axiom forall uint256 pId. !proposalExecuted(pId);
 }
 ghost proposalCanceled(uint256) returns bool {
     init_state axiom forall uint256 pId. !proposalCanceled(pId);
 }
-
+*/
+/*
 hook Sstore _proposals[KEY uint256 pId].voteStart._deadline uint64 newValue STORAGE {
     havoc proposalVoteStart assuming (
         proposalVoteStart@new(pId) == newValue
@@ -42,21 +49,22 @@ hook Sstore _proposals[KEY uint256 pId].voteEnd._deadline uint64 newValue STORAG
 hook Sload uint64 value _proposals[KEY uint256 pId].voteEnd._deadline STORAGE {
     require proposalVoteEnd(pId) == value;
 }
+*/
 
 //////////////////////////////////////////////////////////////////////////////
 //////////////////////////// SANITY CHECKS ///////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 //
-
+/*
 rule sanityCheckVoteStart(method f, uint256 pId) {
-    uint64 preGhost = proposalVoteStart(pId);
+    uint64 preGhost = _proposals(pId).voteStart._deadline;
     uint256 pre = proposalSnapshot(pId);
 
     env e;
     calldataarg arg;
     f(e, arg);
 
-    uint64 postGhost = proposalVoteStart(pId);
+    uint64 postGhost = _proposals(pId).voteStart._deadline;
     uint256 post = proposalSnapshot(pId);
 
     assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes";
@@ -77,7 +85,7 @@ rule sanityCheckVoteEnd(method f, uint256 pId) {
     assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes";
     assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end";
 }
-
+*/
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
@@ -91,12 +99,12 @@ invariant voteStartBeforeVoteEnd(uint256 pId) proposalVoteStart(pId) < proposalV
 /**
  * A proposal cannot be both executed and canceled.
  */
-invariant noBothExecutedAndCanceled(uint256 pId) !proposalExecuted(pId) || !proposalCanceled(pId)
+invariant noBothExecutedAndCanceled(uint256 pId) !isExecuted(pId) || !isCanceled(pId)
 
 /**
  * A proposal cannot be executed nor canceled before it starts
  */
-invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) e.block.timestamp < proposalVoteStart(pId) => !proposalExecuted(pId) && !proposalCanceled(pId)
+invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) e.block.timestamp < proposalVoteStart(pId) => !isExecuted(pId) && !isCanceled(pId)
 
 /**
  * The voting must start not before the proposal’s creation time
diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index c8c8e709c..1c433f6cc 100644
--- a/contracts/governance/Governor.sol
+++ b/contracts/governance/Governor.sol
@@ -37,7 +37,7 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor {
 
     string private _name;
 
-    mapping(uint256 => ProposalCore) private _proposals;
+    mapping(uint256 => ProposalCore) public _proposals;
 
     /**
      * @dev Restrict access to governor executing address. Some module might override the _executor function to make

From b133fee3763a7b60d00affe2c601497c67c8b0e1 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Sun, 7 Nov 2021 17:55:03 +0200
Subject: [PATCH 20/39] WorkInProgress

---
 certora/specs/GovernorBase.spec   | 50 +++++++++++++++++++++----------
 contracts/governance/Governor.sol |  2 +-
 2 files changed, 36 insertions(+), 16 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index cbe376bf0..f70bb5154 100644
--- a/certora/specs/GovernorBase.spec
+++ b/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
     hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
     isExecuted(uint256) returns bool envfree
     isCanceled(uint256) returns bool envfree
@@ -91,39 +92,60 @@ rule sanityCheckVoteEnd(method f, uint256 pId) {
 //////////////////////////////////////////////////////////////////////////////
 //
 
+invariant inizialized()
+        forall uint256 pId. proposalSnapshot(pId) != 0 && proposalDeadline(pId) != 0 
+                => pId != 0
+
+invariant uninizialized(uint256 pId)
+        proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0
+
 /**
  * A proposal cannot end unless it started.
  */
-invariant voteStartBeforeVoteEnd(uint256 pId) proposalVoteStart(pId) < proposalVoteEnd(pId)
+//invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId)
+// ALARM
+invariant voteStartBeforeVoteEnd(uint256 pId)
+        (proposalSnapshot(pId) == 0 <=> proposalDeadline(pId) == 0) &&
+        proposalSnapshot(pId) < proposalDeadline(pId)
 
 /**
  * A proposal cannot be both executed and canceled.
  */
+ // @AK - no violations
 invariant noBothExecutedAndCanceled(uint256 pId) !isExecuted(pId) || !isCanceled(pId)
 
 /**
- * A proposal cannot be executed nor canceled before it starts
+ * A proposal cannot be neither executed nor canceled before it starts
  */
-invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) e.block.timestamp < proposalVoteStart(pId) => !isExecuted(pId) && !isCanceled(pId)
+  // @AK - violations convert to a rule
+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
+ */
+  // @AK - no violations
+invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
 
 /**
  * The voting must start not before the proposal’s creation time
  */
 rule noStartBeforeCreation(uint256 pId) {
-    uint previousStart = proposalVoteStart(pId);
+    uint previousStart = proposalSnapshot(pId);
     require previousStart == 0;
     env e;
     calldataarg arg;
     propose(e, arg);
 
-    uint newStart = proposalVoteStart(pId);
+    uint newStart = proposalSnapshot(pId);
     // if created, start is after creation
-    assert newStart != 0 => newStart > e.block.timestamp;
+    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;
@@ -142,26 +164,24 @@ rule checkHashProposal {
     assert equalHashes => c1.length == c2.length;
     assert equalHashes => d1 == d2;
 }
+*/
 
-/**
- * A proposal could be executed only if quorum was reached and vote succeeded
- */
-invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) proposalExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
 
 /**
  * Once a proposal is created, voteStart and voteEnd are immutable
  */
+ // @AK - no violations
 rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
-    uint _voteStart = proposalVoteStart(pId);
-    uint _voteEnd = proposalVoteEnd(pId);
+    uint _voteStart = proposalSnapshot(pId);
+    uint _voteEnd = proposalDeadline(pId);
     require _voteStart > 0; // proposal was created
 
     env e;
     calldataarg arg;
     f(e, arg);
 
-    uint voteStart_ = proposalVoteStart(pId);
-    uint voteEnd_ = proposalVoteEnd(pId);
+    uint voteStart_ = proposalSnapshot(pId);
+    uint voteEnd_ = proposalDeadline(pId);
     assert _voteStart == voteStart_;
     assert _voteEnd == voteEnd_;
-}
\ No newline at end of file
+}
diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index 1c433f6cc..df85e2bbb 100644
--- a/contracts/governance/Governor.sol
+++ b/contracts/governance/Governor.sol
@@ -38,7 +38,7 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor {
     string private _name;
 
     mapping(uint256 => ProposalCore) public _proposals;
-
+ 
     /**
      * @dev Restrict access to governor executing address. Some module might override the _executor function to make
      * sure this modifier is consistant with the execution model.

From 0ebc0d584452c643479c0d0ad0135721adf41bfd Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Mon, 8 Nov 2021 11:44:04 +0200
Subject: [PATCH 21/39] someCleaning

---
 certora/specs/GovernorBase.spec | 95 +++------------------------------
 1 file changed, 7 insertions(+), 88 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index f70bb5154..b37ba6e22 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -11,99 +11,15 @@ methods {
     _voteSucceeded(uint256) returns bool envfree
 }
 
-/*
-ghost proposalVoteStart(uint256) returns uint64 {
-    init_state axiom forall uint256 pId. proposalVoteStart(pId) == 0;
-}
-ghost proposalVoteEnd(uint256) returns uint64 {
-    init_state axiom forall uint256 pId. proposalVoteEnd(pId) == 0;
-}
-*/
-
-/*
-ghost proposalExecuted(uint256) returns bool {
-    init_state axiom forall uint256 pId. !proposalExecuted(pId);
-}
-ghost proposalCanceled(uint256) returns bool {
-    init_state axiom forall uint256 pId. !proposalCanceled(pId);
-}
-*/
-/*
-hook Sstore _proposals[KEY uint256 pId].voteStart._deadline uint64 newValue STORAGE {
-    havoc proposalVoteStart assuming (
-        proposalVoteStart@new(pId) == newValue
-        && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
-    );
-}
-
-hook Sload uint64 value _proposals[KEY uint256 pId].voteStart._deadline STORAGE {
-    require proposalVoteStart(pId) == value;
-}
-
-hook Sstore _proposals[KEY uint256 pId].voteEnd._deadline uint64 newValue STORAGE {
-    havoc proposalVoteEnd assuming (
-        proposalVoteEnd@new(pId) == newValue
-        && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2))
-    );
-}
-
-hook Sload uint64 value _proposals[KEY uint256 pId].voteEnd._deadline STORAGE {
-    require proposalVoteEnd(pId) == value;
-}
-*/
-
-//////////////////////////////////////////////////////////////////////////////
-//////////////////////////// SANITY CHECKS ///////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-//
-/*
-rule sanityCheckVoteStart(method f, uint256 pId) {
-    uint64 preGhost = _proposals(pId).voteStart._deadline;
-    uint256 pre = proposalSnapshot(pId);
-
-    env e;
-    calldataarg arg;
-    f(e, arg);
-
-    uint64 postGhost = _proposals(pId).voteStart._deadline;
-    uint256 post = proposalSnapshot(pId);
-
-    assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes";
-    assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end";
-}
-
-rule sanityCheckVoteEnd(method f, uint256 pId) {
-    uint64 preGhost = proposalVoteEnd(pId);
-    uint256 pre = proposalSnapshot(pId);
-
-    env e;
-    calldataarg arg;
-    f(e, arg);
-
-    uint64 postGhost = proposalVoteEnd(pId);
-    uint256 post = proposalSnapshot(pId);
-
-    assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes";
-    assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end";
-}
-*/
 //////////////////////////////////////////////////////////////////////////////
 ////////////////////////////// INVARIANTS ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
-//
 
-invariant inizialized()
-        forall uint256 pId. proposalSnapshot(pId) != 0 && proposalDeadline(pId) != 0 
-                => pId != 0
-
-invariant uninizialized(uint256 pId)
-        proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0
 
 /**
  * A proposal cannot end unless it started.
  */
 //invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId)
-// ALARM
 invariant voteStartBeforeVoteEnd(uint256 pId)
         (proposalSnapshot(pId) == 0 <=> proposalDeadline(pId) == 0) &&
         proposalSnapshot(pId) < proposalDeadline(pId)
@@ -111,22 +27,26 @@ invariant voteStartBeforeVoteEnd(uint256 pId)
 /**
  * A proposal cannot be both executed and canceled.
  */
- // @AK - no violations
 invariant noBothExecutedAndCanceled(uint256 pId) !isExecuted(pId) || !isCanceled(pId)
 
 /**
  * A proposal cannot be neither executed nor canceled before it starts
  */
-  // @AK - violations convert to a rule
 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
  */
-  // @AK - no violations
 invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
 
+
+
+//////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////// RULES ////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
 /**
  * The voting must start not before the proposal’s creation time
  */
@@ -170,7 +90,6 @@ rule checkHashProposal {
 /**
  * Once a proposal is created, voteStart and voteEnd are immutable
  */
- // @AK - no violations
 rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
     uint _voteStart = proposalSnapshot(pId);
     uint _voteEnd = proposalDeadline(pId);

From ac729e0ecf8006dd8b0c0a28cdf4d89965918be5 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Mon, 8 Nov 2021 14:57:51 +0200
Subject: [PATCH 22/39] fix simple vote end before start

---
 certora/specs/GovernorBase.spec | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index b37ba6e22..69d1fd85e 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -21,8 +21,8 @@ methods {
  */
 //invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId)
 invariant voteStartBeforeVoteEnd(uint256 pId)
-        (proposalSnapshot(pId) == 0 <=> proposalDeadline(pId) == 0) &&
-        proposalSnapshot(pId) < proposalDeadline(pId)
+        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
+             && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
 
 /**
  * A proposal cannot be both executed and canceled.

From 7a5bd86ef4dfa34dcdcdb8392d69231b69609a2b Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 15:57:19 +0200
Subject: [PATCH 23/39] added invariants if executed or canceled always revert

---
 certora/specs/GovernorBase.spec | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 69d1fd85e..41ec3e735 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -40,6 +40,18 @@ invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) e.block.number < p
  */
 invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
 
+/*
+ * No functions should be allowed to run after a job is deemed as canceled
+ */
+invariant cannotSetIfCanceled(uint256 pId)
+    isCanceled(pId) => lastReverted == true
+
+/*
+ * No functions should be allowed to run after a job is deemed as executed
+ */
+invariant cannotSetIfExecuted(uint256 pId)
+    isExecuted(pId) => lastReverted == true
+
 
 
 //////////////////////////////////////////////////////////////////////////////

From ad7993d7d5234170f8445d982e28b5bab161cea0 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 15:57:53 +0200
Subject: [PATCH 24/39] idea for sum of votes

---
 certora/harnesses/GovernorHarness.sol | 54 ++++++++++++++++++++++++++-
 1 file changed, 52 insertions(+), 2 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index 28e556556..27a5598e1 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -64,6 +64,19 @@ contract GovernorHarness is Governor {
         return _votingPeriod;
     }
 
+    constructor(string memory name) Governor(name) {}
+
+    // _countVots == Sum of castVote
+    // 
+    // RHS:
+    // 1) use counter_vote_power as a counter
+    // 2) use counter_vote_power as a temp var for a ghost
+    // 
+    // LHS:
+    // mapping of count
+    // countMap
+
+    mapping(uint256 => mapping(address => uint256)) counted_weight_by_id;
 
     function _countVote(
         uint256 proposalId,
@@ -71,9 +84,46 @@ contract GovernorHarness is Governor {
         uint8 support,
         uint256 weight
     ) internal override virtual {
-        // havoc something
+        counted_weight_by_id[proposalId][account] += weight;
     }
 
-    constructor(string memory name) Governor(name) {}
 
+    mapping(uint256 => uint256) counter_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;
+    }
+
+    function castVoteWithReason(
+        uint256 proposalId,
+        uint8 support,
+        string calldata reason
+    ) public virtual override returns (uint256) {
+        address voter = _msgSender();
+        counter_vote_power_by_id[proposalId] += _castVote(proposalId, voter, support, reason);
+        return _castVote(proposalId, voter, support, reason);
+    }
+
+    function castVoteBySig(
+        uint256 proposalId,
+        uint8 support,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public virtual override returns (uint256) {
+        address voter = ECDSA.recover(
+            _hashTypedDataV4(keccak256(abi.encode(BALLOT_TYPEHASH, proposalId, support))),
+            v,
+            r,
+            s
+        );
+        counter_vote_power_by_id[proposalId] += _castVote(proposalId, voter, support, "");
+        return _castVote(proposalId, voter, support, "");
+    }
 }
\ No newline at end of file

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 25/39] 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) {
+
+}

From 37a4975544e34194134432ccdeeb0a0fd07adcb7 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 17:51:28 +0200
Subject: [PATCH 26/39] fixed function revert if executed

---
 certora/specs/GovernorBase.spec | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index ba8b9c93e..ac1dfb6b3 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -61,7 +61,13 @@ invariant cannotSetIfCanceled(uint256 pId)
  * No functions should be allowed to run after a job is deemed as executed
  */
 invariant cannotSetIfExecuted(uint256 pId)
-    isExecuted(pId) => lastReverted == true
+    isExecuted(pId) => lastReverted == true 
+    {
+        preserved execute(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash) with (env e)
+        {
+            require(isExecuted(pId));
+        }
+    }
 
 
 

From c819e0b06358ca2bc5f28da7b10070dea70a46c8 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 17:57:53 +0200
Subject: [PATCH 27/39] added ghost and counter implementation for
 castWithReason and castBySig

---
 certora/harnesses/GovernorHarness.sol | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index 880f706d6..e6182ff8e 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -120,8 +120,13 @@ contract GovernorHarness is Governor {
         string calldata reason
     ) public virtual override returns (uint256) {
         address voter = _msgSender();
-        counter_vote_power_by_id[proposalId] += _castVote(proposalId, voter, support, reason);
-        return _castVote(proposalId, voter, support, reason);
+        // 2)
+        ghost_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, reason);
+        
+        // 1)
+        counter_vote_power_by_id[proposalId] += ghost_vote_power_by_id[proposalId];
+
+        return ghost_vote_power_by_id[proposalId];
     }
 
     function castVoteBySig(
@@ -137,7 +142,12 @@ contract GovernorHarness is Governor {
             r,
             s
         );
-        counter_vote_power_by_id[proposalId] += _castVote(proposalId, voter, support, "");
-        return _castVote(proposalId, voter, support, "");
+        // 2)
+        ghost_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, "");
+
+        // 1)
+        counter_vote_power_by_id[proposalId] += ghost_vote_power_by_id[proposalId];
+
+        return ghost_vote_power_by_id[proposalId];
     }
 }
\ No newline at end of file

From 34cb4bdc9c91778eda4ea591f5830f2162fc8ec4 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 19:00:22 +0200
Subject: [PATCH 28/39] ghosts and invariant unfinished

---
 certora/specs/GovernorBase.spec | 46 +++++++++++++++++++++++----------
 1 file changed, 33 insertions(+), 13 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index ac1dfb6b3..dd0df01cb 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -1,4 +1,6 @@
-// Governor.sol base definitions
+//////////////////////////////////////////////////////////////////////////////
+///////////////////// Governor.sol base definitions //////////////////////////
+//////////////////////////////////////////////////////////////////////////////
 methods {
     proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
     proposalDeadline(uint256) returns uint256 envfree
@@ -14,8 +16,24 @@ methods {
     // internal functions made public in harness:
     _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_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 ////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
@@ -38,18 +56,21 @@ invariant voteStartBeforeVoteEnd(uint256 pId)
 /**
  * A proposal cannot be both executed and canceled.
  */
-invariant noBothExecutedAndCanceled(uint256 pId) !isExecuted(pId) || !isCanceled(pId)
+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)
+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)
+invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
+        isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
 
 /*
  * No functions should be allowed to run after a job is deemed as canceled
@@ -69,7 +90,13 @@ invariant cannotSetIfExecuted(uint256 pId)
         }
     }
 
-
+/*
+ * sum of all votes casted is equal to the sum of voting power of those who voted
+ */
+invariant SumOfVotesCastEqualSumOfPowerOfVoted(uint256 pId)
+        counted_weight(pId) == counter_vote_power_by_id(pId) &&
+         counted_weight(pId) == vote_power_ghost &&
+         counter_vote_power_by_id(pId) == vote_power_ghost
 
 //////////////////////////////////////////////////////////////////////////////
 /////////////////////////////////// RULES ////////////////////////////////////
@@ -149,10 +176,3 @@ rule doubleVoting(uint256 pId, uint8 sup) {
 
     assert reverted, "double voting accured";
 }
-
-/**
-* 
-*/
-rule votingSumAndPower(uint256 pId, uint8 sup, method f) {
-
-}

From 44a8fed4105595040a3a29a4785f9d8add357b59 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 20:16:53 +0200
Subject: [PATCH 29/39] cannot set if executed and canceled as rules (not
 working)

---
 certora/specs/GovernorBase.spec | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index dd0df01cb..aa0bcfc5b 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -75,28 +75,28 @@ invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId)
 /*
  * No functions should be allowed to run after a job is deemed as canceled
  */
-invariant cannotSetIfCanceled(uint256 pId)
-    isCanceled(pId) => lastReverted == true
+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
  */
-invariant cannotSetIfExecuted(uint256 pId)
-    isExecuted(pId) => lastReverted == true 
-    {
-        preserved execute(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash) with (env e)
-        {
-            require(isExecuted(pId));
-        }
-    }
+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");
+}
 
 /*
  * sum of all votes casted is equal to the sum of voting power of those who voted
  */
 invariant SumOfVotesCastEqualSumOfPowerOfVoted(uint256 pId)
-        counted_weight(pId) == counter_vote_power_by_id(pId) &&
-         counted_weight(pId) == vote_power_ghost &&
-         counter_vote_power_by_id(pId) == vote_power_ghost
+        counted_weight(pId) == vote_power_ghost()
 
 //////////////////////////////////////////////////////////////////////////////
 /////////////////////////////////// RULES ////////////////////////////////////

From 07d637980c25b280da159491b10f1856024981ea Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Tue, 9 Nov 2021 11:18:23 +0200
Subject: [PATCH 30/39] FirstWizardHarness

---
 certora/harnesses/GovernorBasicHarness.sol | 124 +++++++++++++++++++++
 certora/scripts/Governor.sh                |   2 +-
 certora/scripts/GovernorBasic.sh           |   8 ++
 certora/specs/GovernorBase.spec            |   7 +-
 4 files changed, 139 insertions(+), 2 deletions(-)
 create mode 100644 certora/harnesses/GovernorBasicHarness.sol
 create mode 100644 certora/scripts/GovernorBasic.sh

diff --git a/certora/harnesses/GovernorBasicHarness.sol b/certora/harnesses/GovernorBasicHarness.sol
new file mode 100644
index 000000000..1b9dce2a6
--- /dev/null
+++ b/certora/harnesses/GovernorBasicHarness.sol
@@ -0,0 +1,124 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../../contracts/governance/Governor.sol";
+import "../../contracts/governance/extensions/GovernorCountingSimple.sol";
+import "../../contracts/governance/extensions/GovernorVotes.sol";
+import "../../contracts/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../../contracts/governance/extensions/GovernorTimelockCompound.sol";
+
+/* 
+Wizard options:
+ERC20Votes
+TimelockCompound
+*/
+
+contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
+    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
+        Governor(name)
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumFraction)
+        GovernorTimelockCompound(_timelock)
+    {}
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+    
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    uint256 _votingDelay;
+
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+/*
+    function votingDelay() public pure override returns (uint256) {
+        return _votingDelay;
+    }
+
+
+    function votingPeriod() public pure override returns (uint256) {
+        return _votingPeriod;
+    }
+*/
+
+    // The following functions are overrides required by Solidity.
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(blockNumber);
+    }
+
+    function getVotes(address account, uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotes)
+        returns (uint256)
+    {
+        return super.getVotes(account, blockNumber);
+    }
+
+    function state(uint256 proposalId)
+        public
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (ProposalState)
+    {
+        return super.state(proposalId);
+    }
+
+    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
+        public
+        override(Governor, IGovernor)
+        returns (uint256)
+    {
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockCompound)
+    {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockCompound)
+        returns (uint256)
+    {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor()
+        internal
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (address)
+    {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}
diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
index ccdf90203..d3b7f9b3f 100755
--- a/certora/scripts/Governor.sh
+++ b/certora/scripts/Governor.sh
@@ -4,5 +4,5 @@ certoraRun certora/harnesses/GovernorHarness.sol \
     --staging \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
-    --rule noExecuteOrCancelBeforeStarting \
+    --rule voteStartBeforeVoteEnd \
     --msg "$1"
diff --git a/certora/scripts/GovernorBasic.sh b/certora/scripts/GovernorBasic.sh
new file mode 100644
index 000000000..b720c28ec
--- /dev/null
+++ b/certora/scripts/GovernorBasic.sh
@@ -0,0 +1,8 @@
+certoraRun certora/harnesses/GovernorBasicHarness.sol \
+    --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \
+    --solc solc8.2 \
+    --staging \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule doubleVoting \
+    --msg "$1"
\ No newline at end of file
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index aa0bcfc5b..b0952a534 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -7,7 +7,7 @@ methods {
     hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
     isExecuted(uint256) returns bool envfree
     isCanceled(uint256) returns bool envfree
-    initialized(uint256) returns bool envfree
+    // initialized(uint256) returns bool envfree
 
     hasVoted(uint256, address) returns bool
 
@@ -176,3 +176,8 @@ rule doubleVoting(uint256 pId, uint8 sup) {
 
     assert reverted, "double voting accured";
 }
+
+/**
+* 
+*/
+//rule votingSumAndPower(uint256 pId, uint8 sup, method f) {}

From 96df9799c3275fd0abf65b7c312c81f350eb7925 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Tue, 9 Nov 2021 15:10:07 +0200
Subject: [PATCH 31/39] specificSpecForSumRule

---
 certora/harnesses/GovernorBasicHarness.sol    | 19 ++--
 .../GovernorCountingSimple-counting.sh        |  8 ++
 certora/specs/GovernorBase.spec               | 24 +----
 certora/specs/GovernorCountingSimple.spec     | 87 +++++++++++++++++++
 contracts/governance/Governor.sol             |  4 +-
 .../GovernorCompatibilityBravo.sol            |  4 +-
 .../extensions/GovernorCountingSimple.sol     |  2 +-
 7 files changed, 114 insertions(+), 34 deletions(-)
 create mode 100644 certora/scripts/GovernorCountingSimple-counting.sh
 create mode 100644 certora/specs/GovernorCountingSimple.spec

diff --git a/certora/harnesses/GovernorBasicHarness.sol b/certora/harnesses/GovernorBasicHarness.sol
index 1b9dce2a6..57cd3c58c 100644
--- a/certora/harnesses/GovernorBasicHarness.sol
+++ b/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) {
-        return _votingPeriod;
+    function _castVote(
+        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.
 
diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh
new file mode 100644
index 000000000..2bea57198
--- /dev/null
+++ b/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"
\ No newline at end of file
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index b0952a534..dad38fc48 100644
--- a/certora/specs/GovernorBase.spec
+++ b/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) {}
diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec
new file mode 100644
index 000000000..197dae1c0
--- /dev/null
+++ b/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()
+
diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index df85e2bbb..3aecd3a1c 100644
--- a/contracts/governance/Governor.sol
+++ b/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.
diff --git a/contracts/governance/compatibility/GovernorCompatibilityBravo.sol b/contracts/governance/compatibility/GovernorCompatibilityBravo.sol
index cbdd72791..e0261ea38 100644
--- a/contracts/governance/compatibility/GovernorCompatibilityBravo.sol
+++ b/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;
     }
diff --git a/contracts/governance/extensions/GovernorCountingSimple.sol b/contracts/governance/extensions/GovernorCountingSimple.sol
index 00f4d4aa8..fae6b5c5b 100644
--- a/contracts/governance/extensions/GovernorCountingSimple.sol
+++ b/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");
         }

From 6ac85d8d150f34de1a6d13598939811ca4aa6158 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Tue, 9 Nov 2021 15:16:44 +0200
Subject: [PATCH 32/39] RemovedInsertedBugForSumRule

---
 certora/specs/GovernorBase.spec                            | 2 +-
 contracts/governance/extensions/GovernorCountingSimple.sol | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index dad38fc48..5b24bae2c 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -147,7 +147,7 @@ rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
 }
 
 /**
-* Check if it's possible to vote two time. Relevant to GovernorCountingSimpleHarness.sol contract
+* A user cannot vote twice
 */
 rule doubleVoting(uint256 pId, uint8 sup) {
     env e;
diff --git a/contracts/governance/extensions/GovernorCountingSimple.sol b/contracts/governance/extensions/GovernorCountingSimple.sol
index fae6b5c5b..00f4d4aa8 100644
--- a/contracts/governance/extensions/GovernorCountingSimple.sol
+++ b/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");
         }

From 85855b8cc7af95fa6c532a9787bf2b4315863e67 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Tue, 9 Nov 2021 21:09:54 +0200
Subject: [PATCH 33/39] FixedTypoInEnvfreeWord

---
 certora/specs/GovernorCountingSimple.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec
index 197dae1c0..d3094896f 100644
--- a/certora/specs/GovernorCountingSimple.spec
+++ b/certora/specs/GovernorCountingSimple.spec
@@ -14,7 +14,7 @@ methods {
     castVote(uint256, uint8) returns uint256
 
     // internal functions made public in harness:
-    _quorumReached(uint256) returns bool envfre
+    _quorumReached(uint256) returns bool envfree
     _voteSucceeded(uint256) returns bool envfree
 
     // getter for checking the sums

From 52924aaec0792d081dd4dcc854949f82f20fb65e Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Wed, 10 Nov 2021 15:07:34 +0200
Subject: [PATCH 34/39] Changed deltaWeight type from uint to uin256

---
 certora/harnesses/GovernorBasicHarness.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/harnesses/GovernorBasicHarness.sol b/certora/harnesses/GovernorBasicHarness.sol
index 57cd3c58c..6a36475d4 100644
--- a/certora/harnesses/GovernorBasicHarness.sol
+++ b/certora/harnesses/GovernorBasicHarness.sol
@@ -51,7 +51,7 @@ contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes
         string memory reason
     ) internal override virtual returns (uint256) {
         
-        uint deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
         ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
 
         return deltaWeight;        

From eb87bb482238aa30e04a77e3747de9c094b0fc08 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Wed, 10 Nov 2021 15:10:37 +0200
Subject: [PATCH 35/39] aesthetic

---
 certora/specs/GovernorBase.spec | 232 +++++++++++++++-----------------
 1 file changed, 108 insertions(+), 124 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 5b24bae2c..9faa14f9f 100644
--- a/certora/specs/GovernorBase.spec
+++ b/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.
- */
-//invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId)
-invariant voteStartBeforeVoteEnd(uint256 pId)
+    /*
+     * A proposal cannot end unless it started.
+     */
+    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
- */
-rule noStartBeforeCreation(uint256 pId) {
-    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;
-}
-
-/**
- * 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
+     */
+    invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) 
+            e.block.number < proposalSnapshot(pId) 
+                => !isExecuted(pId) && !isCanceled(pId)
 
 
-/**
- * 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
+    /*
+     * A proposal could be executed only if quorum was reached and vote succeeded
+     */
+    invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
+            isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
 
-    env e;
-    calldataarg arg;
-    f(e, arg);
 
-    uint voteStart_ = proposalSnapshot(pId);
-    uint voteEnd_ = proposalDeadline(pId);
-    assert _voteStart == voteStart_;
-    assert _voteEnd == voteEnd_;
-}
+    //////////////////////////////////////////////////////////////////////////////
+    /////////////////////////////////// RULES ////////////////////////////////////
+    //////////////////////////////////////////////////////////////////////////////
+    
+    /*
+     * The voting must start not before the proposal’s creation time
+     */
+    rule noStartBeforeCreation(uint256 pId) {
+        uint previousStart = proposalSnapshot(pId);
+        require previousStart == 0;
+        env e;
+        calldataarg arg;
+        propose(e, arg);
 
-/**
-* A user cannot vote twice
-*/
-rule doubleVoting(uint256 pId, uint8 sup) {
-    env e;
-    address user = e.msg.sender;
+        uint newStart = proposalSnapshot(pId);
+        // if created, start is after creation
+        assert(newStart != 0 => newStart >= e.block.number);
+    }
 
-    bool votedCheck = hasVoted(e, pId, user);
-    require votedCheck == true;
 
-    castVote@withrevert(e, pId, sup);
-    bool reverted = lastReverted;
+    /*
+     * 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
 
-    assert votedCheck => reverted, "double voting accured";
-}
+        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;
+    }
+    */

From b52832ca7f2442044da2faedf465e97ba6255a46 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Wed, 10 Nov 2021 15:26:29 +0200
Subject: [PATCH 36/39] Cleaned harness + callPropose

---
 certora/harnesses/GovernorHarness.sol | 74 +++++----------------------
 1 file changed, 14 insertions(+), 60 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index e6182ff8e..fce0c5c18 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -74,6 +74,16 @@ contract GovernorHarness is Governor {
     }
 
 
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal override virtual {
+        // havoc something
+    }
+
+
     constructor(string memory name) Governor(name) {}
 
     // _countVots == Sum of castVote
@@ -86,68 +96,12 @@ contract GovernorHarness is Governor {
     // mapping of count
     // countMap
 
-    mapping(uint256 => uint256) counted_weight;
-
     // uint decision;
     // uint numberOfOptions;
-    function _countVote(
-        uint256 proposalId,
-        address account,
-        uint8 support,
-        uint256 weight
-    ) internal override virtual {
-        counted_weight[proposalId] += weight;
-    }
 
-    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();
-        // 2)
-        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(
-        uint256 proposalId,
-        uint8 support,
-        string calldata reason
-    ) public virtual override returns (uint256) {
-        address voter = _msgSender();
-        // 2)
-        ghost_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, reason);
-        
-        // 1)
-        counter_vote_power_by_id[proposalId] += ghost_vote_power_by_id[proposalId];
-
-        return ghost_vote_power_by_id[proposalId];
-    }
-
-    function castVoteBySig(
-        uint256 proposalId,
-        uint8 support,
-        uint8 v,
-        bytes32 r,
-        bytes32 s
-    ) public virtual override returns (uint256) {
-        address voter = ECDSA.recover(
-            _hashTypedDataV4(keccak256(abi.encode(BALLOT_TYPEHASH, proposalId, support))),
-            v,
-            r,
-            s
-        );
-        // 2)
-        ghost_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, "");
-
-        // 1)
-        counter_vote_power_by_id[proposalId] += ghost_vote_power_by_id[proposalId];
-
-        return ghost_vote_power_by_id[proposalId];
+    function callPropose(address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas) public virtual returns (uint256) {
+        return super.propose(targets, values, calldatas, "");
     }
 }
\ No newline at end of file

From 2a0532daccc5e48172d63aa8ce733620d0dae219 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Thu, 11 Nov 2021 17:28:22 +0200
Subject: [PATCH 37/39] CountingSimpleMoreCleanAndAddedMoreRules

---
 certora/specs/GovernorBase.spec           | 253 +++++++++++++---------
 certora/specs/GovernorCountingSimple.spec |  31 +--
 2 files changed, 151 insertions(+), 133 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 9faa14f9f..ba4565ad0 100644
--- a/certora/specs/GovernorBase.spec
+++ b/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.
-     */
-    invariant voteStartBeforeVoteEnd(uint256 pId)
-        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
-             && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
+/*
+ * A proposal cannot end unless it started.
+ */
+invariant voteStartBeforeVoteEnd(uint256 pId)
+    (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
+         && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
 
 
-    /*
-     * A proposal cannot be both executed and canceled.
-     */
-    invariant noBothExecutedAndCanceled(uint256 pId) 
-            !isExecuted(pId) || !isCanceled(pId)
+/**
+ * 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)
 
 
-    /*
-     * A proposal could be executed only if quorum was reached and vote succeeded
-     */
-    invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
-            isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
-
-
-    //////////////////////////////////////////////////////////////////////////////
-    /////////////////////////////////// RULES ////////////////////////////////////
-    //////////////////////////////////////////////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////// RULES ////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
     
-    /*
-     * The voting must start not before the proposal’s creation time
-     */
-    rule noStartBeforeCreation(uint256 pId) {
-        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);
-    }
+/*
+ * 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");
+}
 
 
-    /*
-     * 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_;
-    }
+/*
+ * 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");
+}
 
 
-    /*
-     * A user cannot vote twice
-     */
-    rule doubleVoting(uint256 pId, uint8 sup) {
-        env e;
-        address user = e.msg.sender;
+/*
+ * The voting must start not before the proposal’s creation time
+ */
+rule noStartBeforeCreation(uint256 pId) {
+    uint previousStart = proposalSnapshot(pId);
+    require previousStart == 0;
+    env e;
+    calldataarg arg;
+    propose(e, arg);
 
-        bool votedCheck = hasVoted(e, pId, user);
-        require votedCheck == true;
-
-        castVote@withrevert(e, pId, sup);
-        bool reverted = lastReverted;
-
-        assert votedCheck => reverted, "double voting accured";
-    }
+    uint newStart = proposalSnapshot(pId);
+    // if created, start is after creation
+    assert(newStart != 0 => newStart >= e.block.number);
+}
 
 
-    /*
-     * 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");
-    }
+/*
+ * 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_;
+}
 
 
-    /**
-     * 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;
+/*
+ * A user cannot vote twice
+ */
+rule doubleVoting(uint256 pId, uint8 sup) {
+    env e;
+    address user = e.msg.sender;
 
-        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;
-    }
-    */
+    bool votedCheck = hasVoted(e, pId, user);
+
+    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;
+}
+*/
+
+
+/**
+ * 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";
+}
\ No newline at end of file
diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec
index d3094896f..a0ae7b6d6 100644
--- a/certora/specs/GovernorCountingSimple.spec
+++ b/certora/specs/GovernorCountingSimple.spec
@@ -1,23 +1,6 @@
-//////////////////////////////////////////////////////////////////////////////
-///////////////////// Governor.sol base definitions //////////////////////////
-//////////////////////////////////////////////////////////////////////////////
+import "GovernorBase.spec"
+
 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;

From 2ecba5326bc1f8ec3353fd2dc1284193448a66b5 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Fri, 12 Nov 2021 09:02:51 +0200
Subject: [PATCH 38/39] reorganization + violated rules

---
 certora/specs/GovernorBase.spec | 281 ++++++++++++++++++--------------
 1 file changed, 162 insertions(+), 119 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index ba4565ad0..4cea34323 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -18,124 +18,169 @@ 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.
- */
-invariant voteStartBeforeVoteEnd(uint256 pId)
-    (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
-         && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
+ //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+ ///////////////////////////////////////////////////// State Diagram //////////////////////////////////////////////////////////
+ //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+ //                                                                                                                          //
+ //                                                                castVote(s)()                                             //
+ //  -------------  propose()  ----------------------  time pass  ---------------       time passes         -----------      //
+ // | No Proposal | --------> | Before Start (Delay) | --------> | Voting Period | ----------------------> | execute() |     //
+ //  -------------             ----------------------             --------------- -> Executed/Canceled      -----------      //
+ //  ------------------------------------------------------------|---------------|-------------------------|-------------->  //
+ // t                                                          start            end                     timelock             //
+ //                                                                                                                          //
+ //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+*/
 
 
-/**
- * A proposal cannot be both executed and canceled.
- */
-invariant noBothExecutedAndCanceled(uint256 pId) 
-        !isExecuted(pId) || !isCanceled(pId)
+
+///////////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// Global Valid States /////////////////////////////////
+///////////////////////////////////////////////////////////////////////////////////////
+
+    // not complete
+    /*
+     * If any of the properties are non zero, the rest has to be non zero 
+     */
+     // start   !0  !0  !0
+     // end =   !0  !0  !0
+     // exe = 0  0  1   1
+     // can = 0  1  0   1
+    invariant proposalInitiated(uint256 pId)
+            (proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0) &&
+            (isCanceled(pId) => proposalSnapshot(pId) != 0) &&
+            (isExecuted(pId) => proposalSnapshot(pId) != 0)
+
+    // pass
+    /*
+     * A proposal cannot end unless it started.
+     */
+    invariant voteStartBeforeVoteEnd(uint256 pId)
+        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
+             && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
 
 
-/**
- * A proposal could be executed only if quorum was reached and vote succeeded
- */
-invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) 
-        isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId)
+    // pass
+    /*
+     * A proposal cannot be both executed and canceled.
+     */
+    invariant noBothExecutedAndCanceled(uint256 pId) 
+            !isExecuted(pId) || !isCanceled(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));
-    env e; calldataarg args;
-    f(e, args);
-    assert(isCanceled(pId) => lastReverted == true, "Function did not revert when canceled");
-}
+///////////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////// In-State Rules /////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////////////////
+
+//==========================================
+//------------- Voting Period --------------
+//==========================================
+
+    // pass
+    /*
+     * 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";
+    }
 
 
-/*
- * 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");
-}
+///////////////////////////////////////////////////////////////////////////////////////
+//////////////////////////// State Transitions Rules //////////////////////////////////
+///////////////////////////////////////////////////////////////////////////////////////
+
+//===========================================
+//-------- Propose() --> End of Time --------
+//===========================================
+
+    // pass
+    /*
+     * The voting must start not before the proposal’s creation time
+     */
+    rule noStartBeforeCreation(uint256 pId) {
+        uint256 previousStart = proposalSnapshot(pId);
+        require previousStart == 0;
+        env e;
+        calldataarg arg;
+        propose(e, arg);
+
+        uint newStart = proposalSnapshot(pId);
+        // if created, start is after current block number (creation block)
+        assert(newStart != previousStart => newStart >= e.block.number);
+    }
 
 
-/*
- * The voting must start not before the proposal’s creation time
- */
-rule noStartBeforeCreation(uint256 pId) {
-    uint previousStart = proposalSnapshot(pId);
-    require previousStart == 0;
-    env e;
-    calldataarg arg;
-    propose(e, arg);
+    // pass
+    /*
+     * 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 - relation proved in noStartBeforeCreation
 
-    uint newStart = proposalSnapshot(pId);
-    // if created, start is after creation
-    assert(newStart != 0 => newStart >= e.block.number);
-}
+        env e;
+        calldataarg arg;
+        f(e, arg);
 
+        uint voteStart_ = proposalSnapshot(pId);
+        uint voteEnd_ = proposalDeadline(pId);
+        assert _voteStart == voteStart_;
+        assert _voteEnd == voteEnd_;
+    }
 
-/*
- * 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
+    // pass
+    /*
+     * A proposal cannot be neither executed nor canceled before it starts
+     */
+    rule noExecuteOrCancelBeforeStarting(uint256 pId, method f){
+        env e;
 
-    env e;
-    calldataarg arg;
-    f(e, arg);
+        require !isExecuted(pId) && !isCanceled(pId);
 
-    uint voteStart_ = proposalSnapshot(pId);
-    uint voteEnd_ = proposalDeadline(pId);
-    assert _voteStart == voteStart_;
-    assert _voteEnd == voteEnd_;
-}
+        calldataarg arg;
+        f(e, arg);
 
+        assert e.block.number < proposalSnapshot(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start";
+    }
 
-/*
- * A user cannot vote twice
- */
-rule doubleVoting(uint256 pId, uint8 sup) {
-    env e;
-    address user = e.msg.sender;
+//============================================
+//--- End of Voting Period --> End of Time ---
+//============================================
 
-    bool votedCheck = hasVoted(e, pId, user);
+    // pass
+    /*
+     * A proposal cannot be neither executed nor canceled before proposal's deadline
+     */
+    rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
+        env e;
 
-    castVote@withrevert(e, pId, sup);
-    bool reverted = lastReverted;
+        requireInvariant voteStartBeforeVoteEnd(pId);
+        require !isExecuted(pId) && !isCanceled(pId);
 
-    assert votedCheck => reverted, "double voting accured";
-}
+        calldataarg arg;
+        f(e, arg);
 
+        assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline";
+    }
 
-/*
- * 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");
-}
-
+////////////////////////////////////////////////////////////////////////////////
+////////////////////// Integrity Of Functions (Unit Tests) /////////////////////
+////////////////////////////////////////////////////////////////////////////////
 
 /**
  * Check hashProposal hashing is reliable (different inputs lead to different buffers hashed)
@@ -161,32 +206,30 @@ rule checkHashProposal {
 }
 */
 
+////////////////////////////////////////////////////////////////////////////////
+//////////////////////////////// High Level Rules //////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
 
-/**
- * A proposal cannot be neither executed nor canceled before it starts
- */
-rule noExecuteOrCancelBeforeStarting(uint256 pId, method f){
-    env e;
+    // not passing
+    /*
+     * all non-view functions should revert if proposal is executed
+     */
+    rule allFunctionsRevertIfExecuted(uint256 pId, method f) filtered { f -> !f.isView } {
+        env e; calldataarg args;
+        require(isExecuted(pId));
+        f@withrevert(e,args);
+        assert(lastReverted == true, "Function was not reverted");
+    }
 
-    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";
-}
\ No newline at end of file
+    // not passing
+    /*
+     * all non-view functions should revert if proposal is canceled
+     */
+    rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView } {
+        env e; calldataarg args;
+        uint256 pId = e.msg.value;
+        require(isCanceled(pId));
+        requireInvariant noBothExecutedAndCanceled(pId);
+        f@withrevert(e,args);
+        assert(lastReverted == true, "Function was not reverted");
+    }
\ No newline at end of file

From 4337957a6b871c37c0652c6f27e73cb607cdcf48 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Date: Fri, 12 Nov 2021 14:12:03 +0200
Subject: [PATCH 39/39] codeCleaningNumberIDontKnow

---
 certora/specs/GovernorBase.spec | 229 ++++++++++++++++----------------
 1 file changed, 115 insertions(+), 114 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 4cea34323..88fe278f8 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -37,41 +37,45 @@ methods {
 */
 
 
-
 ///////////////////////////////////////////////////////////////////////////////////////
 ///////////////////////////////// Global Valid States /////////////////////////////////
 ///////////////////////////////////////////////////////////////////////////////////////
 
-    // not complete
-    /*
-     * If any of the properties are non zero, the rest has to be non zero 
-     */
-     // start   !0  !0  !0
-     // end =   !0  !0  !0
-     // exe = 0  0  1   1
-     // can = 0  1  0   1
-    invariant proposalInitiated(uint256 pId)
-            (proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0) &&
-            (isCanceled(pId) => proposalSnapshot(pId) != 0) &&
-            (isExecuted(pId) => proposalSnapshot(pId) != 0)
 
-    // pass
-    /*
-     * A proposal cannot end unless it started.
-     */
-    invariant voteStartBeforeVoteEnd(uint256 pId)
-        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
-             && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
+/*
+ * If any of the properties are non zero, the rest has to be non zero 
+ */
+ // start   !0  !0  !0
+ // end =   !0  !0  !0
+ // exe = 0  0  1   1
+ // can = 0  1  0   1
+invariant proposalInitiated(uint256 pId)
+        (proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0) &&
+        (isCanceled(pId) => proposalSnapshot(pId) != 0) &&
+        (isExecuted(pId) => proposalSnapshot(pId) != 0)
 
 
-    // pass
-    /*
-     * A proposal cannot be both executed and canceled.
-     */
-    invariant noBothExecutedAndCanceled(uint256 pId) 
-            !isExecuted(pId) || !isCanceled(pId)
+/*
+ * A proposal cannot end unless it started.
+ */
+invariant voteStartBeforeVoteEnd(uint256 pId)
+    (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
+         && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
 
 
+/*
+ * A proposal cannot be both executed and canceled.
+ */
+invariant noBothExecutedAndCanceled(uint256 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)
+
 
 ///////////////////////////////////////////////////////////////////////////////////////
 ////////////////////////////////// In-State Rules /////////////////////////////////////
@@ -81,22 +85,20 @@ methods {
 //------------- Voting Period --------------
 //==========================================
 
-    // pass
-    /*
-     * 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;
+/*
+ * A user cannot vote twice
+ */
+rule doubleVoting(uint256 pId, uint8 sup) {
+    env e;
+    address user = e.msg.sender;        
+    bool votedCheck = hasVoted(e, pId, user);
 
-        castVote@withrevert(e, pId, sup);
-        bool reverted = lastReverted;
+    castVote@withrevert(e, pId, sup);
+    bool reverted = lastReverted;
 
-        assert votedCheck => reverted, "double voting accured";
-    }
+    assert votedCheck => reverted, "double voting accured";
+}
 
 
 ///////////////////////////////////////////////////////////////////////////////////////
@@ -107,76 +109,75 @@ methods {
 //-------- Propose() --> End of Time --------
 //===========================================
 
-    // pass
-    /*
-     * The voting must start not before the proposal’s creation time
-     */
-    rule noStartBeforeCreation(uint256 pId) {
-        uint256 previousStart = proposalSnapshot(pId);
-        require previousStart == 0;
-        env e;
-        calldataarg arg;
-        propose(e, arg);
 
-        uint newStart = proposalSnapshot(pId);
-        // if created, start is after current block number (creation block)
-        assert(newStart != previousStart => newStart >= e.block.number);
-    }
+/*
+ * The voting must start not before the proposal’s creation time
+ */
+rule noStartBeforeCreation(uint256 pId) {
+    uint256 previousStart = proposalSnapshot(pId);
+    require previousStart == 0;
+    env e;
+    calldataarg arg;
+    propose(e, arg);
+
+    uint newStart = proposalSnapshot(pId);
+    // if created, start is after current block number (creation block)
+    assert(newStart != previousStart => newStart >= e.block.number);
+}
 
 
-    // pass
-    /*
-     * 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 - relation proved in noStartBeforeCreation
+/*
+ * 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 - relation proved in noStartBeforeCreation
 
-        env e;
-        calldataarg arg;
-        f(e, arg);
+    env e;
+    calldataarg arg;
+    f(e, arg);
 
-        uint voteStart_ = proposalSnapshot(pId);
-        uint voteEnd_ = proposalDeadline(pId);
-        assert _voteStart == voteStart_;
-        assert _voteEnd == voteEnd_;
-    }
+    uint voteStart_ = proposalSnapshot(pId);
+    uint voteEnd_ = proposalDeadline(pId);
+    assert _voteStart == voteStart_;
+    assert _voteEnd == voteEnd_;
+}
 
-    // pass
-    /*
-     * A proposal cannot be neither executed nor canceled before it starts
-     */
-    rule noExecuteOrCancelBeforeStarting(uint256 pId, method f){
-        env e;
 
-        require !isExecuted(pId) && !isCanceled(pId);
+/*
+ * A proposal cannot be neither executed nor canceled before it starts
+ */
+rule noExecuteOrCancelBeforeStarting(uint256 pId, method f){
+    env e;
 
-        calldataarg arg;
-        f(e, arg);
+    require !isExecuted(pId) && !isCanceled(pId);
 
-        assert e.block.number < proposalSnapshot(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start";
-    }
+    calldataarg arg;
+    f(e, arg);
+
+    assert e.block.number < proposalSnapshot(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start";
+}
 
 //============================================
 //--- End of Voting Period --> End of Time ---
 //============================================
 
-    // pass
-    /*
-     * 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);
+/*
+ * A proposal cannot be neither executed nor canceled before proposal's deadline
+ */
+rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
+    env e;
 
-        calldataarg arg;
-        f(e, arg);
+    requireInvariant voteStartBeforeVoteEnd(pId);
+    require !isExecuted(pId) && !isCanceled(pId);
 
-        assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline";
-    }
+    calldataarg arg;
+    f(e, arg);
+
+    assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline";
+}
 
 ////////////////////////////////////////////////////////////////////////////////
 ////////////////////// Integrity Of Functions (Unit Tests) /////////////////////
@@ -210,26 +211,26 @@ rule checkHashProposal {
 //////////////////////////////// High Level Rules //////////////////////////////
 ////////////////////////////////////////////////////////////////////////////////
 
-    // not passing
-    /*
-     * all non-view functions should revert if proposal is executed
-     */
-    rule allFunctionsRevertIfExecuted(uint256 pId, method f) filtered { f -> !f.isView } {
-        env e; calldataarg args;
-        require(isExecuted(pId));
-        f@withrevert(e,args);
-        assert(lastReverted == true, "Function was not reverted");
-    }
 
-    // not passing
-    /*
-     * all non-view functions should revert if proposal is canceled
-     */
-    rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView } {
-        env e; calldataarg args;
-        uint256 pId = e.msg.value;
-        require(isCanceled(pId));
-        requireInvariant noBothExecutedAndCanceled(pId);
-        f@withrevert(e,args);
-        assert(lastReverted == true, "Function was not reverted");
-    }
\ No newline at end of file
+/*
+ * all non-view functions should revert if proposal is executed
+ */
+rule allFunctionsRevertIfExecuted(uint256 pId, method f) filtered { f -> !f.isView } {
+    env e; calldataarg args;
+    require(isExecuted(pId));
+    f@withrevert(e,args);
+    assert(lastReverted == true, "Function was not reverted");
+}
+
+
+/*
+ * all non-view functions should revert if proposal is canceled
+ */
+rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView } {
+    env e; calldataarg args;
+    uint256 pId = e.msg.value;
+    require(isCanceled(pId));
+    requireInvariant noBothExecutedAndCanceled(pId);
+    f@withrevert(e,args);
+    assert(lastReverted == true, "Function was not reverted");
+}