madeVeryfyAllMoreFlexible

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`):
 

certora/harnesses/WizardFirstPriority.sol → 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)

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"

certora/scripts/WizardFirstPriority.sh

@@ -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"

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 \