someCleaning

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);