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] 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