reorganized scripts

certora/scripts/Round1/Governor.sh

@@ -0,0 +1,10 @@
+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"

certora/scripts/Round1/GovernorCountingSimple-counting.sh

@@ -0,0 +1,8 @@
+make -C certora munged
+
+certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
+    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --msg "$1"

certora/scripts/Round1/WizardControlFirstPriority.sh

@@ -0,0 +1,12 @@
+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"

certora/scripts/Round1/WizardFirstTry.sh

@@ -0,0 +1,10 @@
+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"

certora/scripts/Round1/sanity.sh

@@ -0,0 +1,35 @@
+# make -C certora munged
+
+# for f in certora/harnesses/Wizard*.sol
+# do
+#     echo "Processing $f"
+#     file=$(basename $f)
+#     echo ${file%.*}
+#     certoraRun certora/harnesses/$file \
+#     --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+#     --solc solc8.2 --staging shelly/forSasha \
+#     --optimistic_loop \
+#     --msg "checking sanity on ${file%.*}"
+#     --settings -copyLoopUnroll=4
+# done
+
+# TimelockController
+certoraRun \
+    certora/harnesses/TimelockControllerHarness.sol \
+    --verify TimelockControllerHarness:certora/specs/sanity.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --cloud \
+    --msg "sanity and keccak check"
+
+
+# Votes
+# certoraRun \
+#     certora/harnesses/VotesHarness.sol \
+#     --verify VotesHarness:certora/specs/sanity.spec \
+#     --solc solc8.2 \
+#     --optimistic_loop \
+#     --cloud \
+#     --settings -strictDecompiler=false,-assumeUnwindCond \
+#     --msg "sanityVotes"
+

certora/scripts/Round1/sanityGovernor.sh

@@ -0,0 +1,14 @@
+make -C certora munged
+
+for f in certora/harnesses/Wizard*.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+    --solc solc8.2 --staging shelly/forSasha \
+    --optimistic_loop \
+    --msg "checking sanity on ${file%.*}"
+    --settings -copyLoopUnroll=4
+done

certora/scripts/Round1/sanityTokens.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+
+make -C certora munged
+
+for f in certora/harnesses/ERC20{Votes,Permit,Wrapper}Harness.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+        --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+        --solc solc8.2 --staging \
+        --optimistic_loop \
+        --msg "checking sanity on ${file%.*}" \
+        --settings -copyLoopUnroll=4,-strictDecompiler=false \
+        --send_only
+done

certora/scripts/Round1/verifyAll.sh

@@ -0,0 +1,42 @@
+#!/bin/bash
+
+make -C certora munged
+
+
+
+for contract in certora/harnesses/Wizard*.sol;
+do
+    for spec in certora/specs/*.spec;
+    do      
+        contractFile=$(basename $contract)
+        specFile=$(basename $spec)
+        if [[ "${specFile%.*}" != "RulesInProgress" ]];
+        then
+            echo "Processing ${contractFile%.*} with $specFile"
+            if [[ "${contractFile%.*}" = *"WizardControl"* ]];
+            then
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --link ${contractFile%.*}:token=ERC20VotesHarness \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            else
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            fi
+        fi
+    done
+done
+

certora/scripts/Round1/verifyGovernor.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+
+make -C certora munged
+
+for contract in certora/harnesses/Wizard*.sol;
+do
+    for spec in certora/specs/governor*.spec;
+    do      
+        contractFile=$(basename $contract)
+        specFile=$(basename $spec)
+        if [[ "${specFile%.*}" != "RulesInProgress" ]];
+        then
+            echo "Processing ${contractFile%.*} with $specFile"
+            if [[ "${contractFile%.*}" = *"WizardControl"* ]];
+            then
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --link ${contractFile%.*}:token=ERC20VotesHarness \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc8.2 \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            else
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc8.2 \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            fi
+        fi
+    done
+done