From b5980a569c429e729c88c03bce7fcbb402184105 Mon Sep 17 00:00:00 2001
From: Michael George <mdgeorge@cs.cornell.edu>
Date: Fri, 17 Dec 2021 09:22:06 -0500
Subject: [PATCH] reorganized governance verification in preparation for erc20
 verification

---
 certora/scripts/Governor.sh                          | 10 ----------
 certora/scripts/GovernorCountingSimple-counting.sh   | 10 ----------
 certora/scripts/WizardControlFirstPriority.sh        | 12 ------------
 certora/scripts/WizardFirstTry.sh                    | 10 ----------
 certora/scripts/{verifyAll.sh => verifyGovernor.sh}  |  2 +-
 certora/specs/{ => governor}/GovernorBase.spec       |  0
 .../specs/{ => governor}/GovernorCountingSimple.spec |  0
 certora/specs/{ => governor}/RulesInProgress.spec    |  0
 8 files changed, 1 insertion(+), 43 deletions(-)
 delete mode 100755 certora/scripts/Governor.sh
 delete mode 100644 certora/scripts/GovernorCountingSimple-counting.sh
 delete mode 100644 certora/scripts/WizardControlFirstPriority.sh
 delete mode 100644 certora/scripts/WizardFirstTry.sh
 rename certora/scripts/{verifyAll.sh => verifyGovernor.sh} (96%)
 rename certora/specs/{ => governor}/GovernorBase.spec (100%)
 rename certora/specs/{ => governor}/GovernorCountingSimple.spec (100%)
 rename certora/specs/{ => governor}/RulesInProgress.spec (100%)

diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh
deleted file mode 100755
index 53ade5060..000000000
--- a/certora/scripts/Governor.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
-    --verify GovernorHarness:certora/specs/GovernorBase.spec \
-    --solc solc8.0 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule voteStartBeforeVoteEnd \
-    --msg "$1"
diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh
deleted file mode 100644
index 9ed8fe34c..000000000
--- a/certora/scripts/GovernorCountingSimple-counting.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
-    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
-    --solc solc8.2 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule hasVotedCorrelation \
-    --msg "$1"
diff --git a/certora/scripts/WizardControlFirstPriority.sh b/certora/scripts/WizardControlFirstPriority.sh
deleted file mode 100644
index b815986ee..000000000
--- a/certora/scripts/WizardControlFirstPriority.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
-    --link WizardControlFirstPriority:token=ERC20VotesHarness \
-    --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
-    --solc solc8.2 \
-    --disableLocalTypeChecking \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule canVoteDuringVotingPeriod \
-    --msg "$1"
diff --git a/certora/scripts/WizardFirstTry.sh b/certora/scripts/WizardFirstTry.sh
deleted file mode 100644
index fd5a32ab4..000000000
--- a/certora/scripts/WizardFirstTry.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
-    --verify WizardFirstTry:certora/specs/GovernorBase.spec \
-    --solc solc8.2 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --disableLocalTypeChecking \
-    --settings -copyLoopUnroll=4 \
-    --msg "$1"
diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyGovernor.sh
similarity index 96%
rename from certora/scripts/verifyAll.sh
rename to certora/scripts/verifyGovernor.sh
index 90d76912c..2e6639422 100644
--- a/certora/scripts/verifyAll.sh
+++ b/certora/scripts/verifyGovernor.sh
@@ -4,7 +4,7 @@ make -C certora munged
 
 for contract in certora/harnesses/Wizard*.sol;
 do
-    for spec in certora/specs/*.spec;
+    for spec in certora/specs/governor*.spec;
     do      
         contractFile=$(basename $contract)
         specFile=$(basename $spec)
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/governor/GovernorBase.spec
similarity index 100%
rename from certora/specs/GovernorBase.spec
rename to certora/specs/governor/GovernorBase.spec
diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/governor/GovernorCountingSimple.spec
similarity index 100%
rename from certora/specs/GovernorCountingSimple.spec
rename to certora/specs/governor/GovernorCountingSimple.spec
diff --git a/certora/specs/RulesInProgress.spec b/certora/specs/governor/RulesInProgress.spec
similarity index 100%
rename from certora/specs/RulesInProgress.spec
rename to certora/specs/governor/RulesInProgress.spec