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