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