From f40c48a83d529b4cda7163345044e739bf8c366d Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Sat, 27 Nov 2021 20:22:25 +0200
Subject: [PATCH] madeVeryfyAllMoreFlexible

---
 certora/README.md                                      |  2 +-
 ...irstPriority.sol => WizardControlFirstPriority.sol} |  2 +-
 certora/scripts/WizardControlFirstPriority.sh          | 10 ++++++++++
 certora/scripts/WizardFirstPriority.sh                 |  9 ---------
 certora/scripts/verifyAll.sh                           |  4 ++--
 5 files changed, 14 insertions(+), 13 deletions(-)
 rename certora/harnesses/{WizardFirstPriority.sol => WizardControlFirstPriority.sol} (96%)
 create mode 100644 certora/scripts/WizardControlFirstPriority.sh
 delete mode 100644 certora/scripts/WizardFirstPriority.sh

diff --git a/certora/README.md b/certora/README.md
index 1ad6507f2..16fcd69bf 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -18,7 +18,7 @@ sh certora/scripts/WizardFirstPriority.sh <meaningful comment>
 After the job is complete, the results will be available on
 [the Certora portal](https://vaas-stg.certora.com/).
 
-The `verifyAll` script runs all spec files agains all contracts in the `certora/harness` that start with `Wizard` meaning that a contract generated in [wizard](https://wizard.openzeppelin.com/#governor). If you want to verify new wizard's instance you also need to harness this contract. We don't recommend to do it because a list of harnesses may go beyond wizard's contract. Moreover, the set of setting to run the Certora verification service may vary. The main goal of this script is to run all specs written by the team against all contracts properly harnessed.
+The `verifyAll` script runs all spec files agains all contracts in the `certora/harness` that start with `Wizard` meaning that a contract generated in [wizard](https://wizard.openzeppelin.com/#governor). If you want to verify new wizard's instance you also need to give it a name starting with "Wizard..." or "WizardControl..." if you use `TimelockController` and harness this contract. We don't recommend to do it because a list of harnesses may go beyond wizard's contract. Moreover, the set of setting to run the Certora verification service may vary. The main goal of this script is to run all specs written by the team against all contracts properly harnessed.
 
 The `WizardFirstPriority` and `WizardFirstTry` scripts run one of the scripts for the corresponding contract. In order to run another spec you should change spec file name `<specName>` in the script (flag `--verify`):
 
diff --git a/certora/harnesses/WizardFirstPriority.sol b/certora/harnesses/WizardControlFirstPriority.sol
similarity index 96%
rename from certora/harnesses/WizardFirstPriority.sol
rename to certora/harnesses/WizardControlFirstPriority.sol
index 7cf7f5223..ffb4f2d97 100644
--- a/certora/harnesses/WizardFirstPriority.sol
+++ b/certora/harnesses/WizardControlFirstPriority.sol
@@ -15,7 +15,7 @@ ERC20Votes
 TimelockCOntroller
 */
 
-contract WizardFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
+contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
     constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction)
         Governor(name)
         GovernorVotes(_token)
diff --git a/certora/scripts/WizardControlFirstPriority.sh b/certora/scripts/WizardControlFirstPriority.sh
new file mode 100644
index 000000000..ba7b26482
--- /dev/null
+++ b/certora/scripts/WizardControlFirstPriority.sh
@@ -0,0 +1,10 @@
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
+    --link WizardControlFirstPriority:token=ERC20VotesHarness \
+    --verify WizardFirstPriority:certora/specs/GovernorBase.spec \
+    --solc solc8.2 \
+    --disableLocalTypeChecking \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule executedImplyStartAndEndDateNonZero \
+    --msg "$1"
\ No newline at end of file
diff --git a/certora/scripts/WizardFirstPriority.sh b/certora/scripts/WizardFirstPriority.sh
deleted file mode 100644
index 1a491bbda..000000000
--- a/certora/scripts/WizardFirstPriority.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstPriority.sol \
-    --link WizardFirstPriority:token=ERC20VotesHarness \
-    --verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \
-    --solc solc8.2 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule noVoteForSomeoneElse \
-    --msg "$1"
\ No newline at end of file
diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh
index d2ce48350..864aa47bd 100644
--- a/certora/scripts/verifyAll.sh
+++ b/certora/scripts/verifyAll.sh
@@ -5,10 +5,10 @@ do
         contractFile=$(basename $contract)
         specFile=$(basename $spec)
         echo "Processing ${contractFile%.*} with $specFile"
-        if [ "${contractFile%.*}" = "WizardFirstPriority" ];
+        if [[ "${contractFile%.*}" = *"WizardControl"* ]];
         then
             certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
-            --link WizardFirstPriority:token=ERC20VotesHarness \
+            --link ${contractFile%.*}:token=ERC20VotesHarness \
             --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
             --solc solc8.2 \
             --staging shelly/forSasha \