From c38babecd9b049ab0922eca07bde05ba0d1912da Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Tue, 23 Nov 2021 12:47:21 +0200
Subject: [PATCH] helper function name change

---
 certora/specs/GovernorBase.spec | 28 +++++++---------------------
 1 file changed, 7 insertions(+), 21 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 89cb88a3e..9a986877d 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -56,7 +56,7 @@ definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0
 ///////////////////////////// Helper Functions ///////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
-function callFunctionWithProposal(uint256 proposalId, method f) {
+function helperFunctionWithRevert(uint256 proposalId, method f) {
     address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash;
     uint8 support; uint8 v; bytes32 r; bytes32 s;
 	env e;
@@ -294,8 +294,9 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f -> !f.isView && f.selec
     uint256 pId;
     require(isExecuted(pId));
     requireInvariant noBothExecutedAndCanceled(pId);
+    requireInvariant executedImplyStartAndEndDateNonZero(pId);
 
-    callFunctionWithProposal(pId, f);
+    helperFunctionWithRevert(pId, f);
 
     assert(lastReverted, "Function was not reverted");
 }
@@ -309,8 +310,9 @@ rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView && f.selec
     uint256 pId;
     require(isCanceled(pId));
     requireInvariant noBothExecutedAndCanceled(pId);
+    requireInvariant canceledImplyStartAndEndDateNonZero(pId);
 
-    callFunctionWithProposal(pId, f);
+    helperFunctionWithRevert(pId, f);
 
     assert(lastReverted, "Function was not reverted");
 }
@@ -324,25 +326,9 @@ rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] c
     bool executedBefore = isExecuted(pId);
     require(!executedBefore);
 
-    callFunctionWithProposal(pId, f);
+    helperFunctionWithRevert(pId, f);
     require(!lastReverted);
-    
+
     bool executedAfter = isExecuted(pId);
     assert(executedAfter != executedBefore, "executed property did not change");
 }
-
-
-/*
-* User should not be able to affect proposal threshold
-*/
-rule unaffectedThreshhold(method f){
-    uint256 thresholdBefore = proposalThreshold();
-
-    env e;
-    calldataarg args;
-    f(e, args);
-
-    uint256 thresholdAfter = proposalThreshold();
-
-    assert thresholdBefore == thresholdAfter, "threshold was changed";
-}