slight script changes and ghost fix

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,

certora/scripts/Governor.sh

@@ -1,2 +1,8 @@
 certoraRun certora/harnesses/GovernorHarness.sol \
-    --verify GovernorHarness:certora/specs/Privileged.spec
+    --verify GovernorHarness:certora/specs/GovernorBase.spec \
+    --solc solc8.0 \
+    --staging \
+    --msg $1 \
+    --disableLocalTypeChecking \
+    --rule voteStartBeforeVoteEnd
+

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
     

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

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.
  */

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.