update scripts

certora/.gitignore

@@ -0,0 +1 @@
+munged

certora/applyHarness.patch

@@ -10,12 +10,6 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
          _checkRole(role, _msgSender());
      }
 
-diff -ruN .gitignore .gitignore
---- .gitignore	1970-01-01 01:00:00.000000000 +0100
-+++ .gitignore	2022-09-20 14:34:08.626268788 +0200
-@@ -0,0 +1,2 @@
-+*
-+!.gitignore
 diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
 --- governance/extensions/GovernorCountingSimple.sol	2022-09-20 11:01:10.432848512 +0200
 +++ governance/extensions/GovernorCountingSimple.sol	2022-09-20 14:34:08.632935582 +0200

certora/harnesses/WizardControlFirstPriority.sol

@@ -9,7 +9,7 @@ import "../munged/governance/extensions/GovernorTimelockControl.sol";
 import "../munged/governance/extensions/GovernorProposalThreshold.sol";
 import "../munged/token/ERC20/extensions/ERC20Votes.sol";
 
-/* 
+/*
 Wizard options:
 ProposalThreshhold = 10
 ERC20Votes
@@ -106,7 +106,7 @@ contract WizardControlFirstPriority is
     function getVotes(address account, uint256 blockNumber)
         public
         view
-        override(IGovernor, GovernorVotes)
+        override(IGovernor, Governor)
         returns (uint256)
     {
         return super.getVotes(account, blockNumber);

certora/munged/.gitignore

@@ -1,2 +0,0 @@
-*
-!.gitignore

certora/scripts/Round1/Governor.sh

@@ -1,10 +1,12 @@
-make -C certora munged
+#!/usr/bin/env bash
 
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
-    --verify GovernorHarness:certora/specs/GovernorBase.spec \
+set -euxo pipefail
+
+# Changed: GovernorHarness → GovernorPreventLateQuorumHarness
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorBase.spec \
     --solc solc \
-    --staging shelly/forSasha \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
-    --rule voteStartBeforeVoteEnd \
-    --msg "$1"
+    --rule voteStartBeforeVoteEnd

certora/scripts/Round1/GovernorCountingSimple-counting.sh

@@ -1,8 +1,11 @@
-make -C certora munged
+#!/usr/bin/env bash
 
-certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
-    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
+set -euxo pipefail
+
+# Changed: GovernorBasicHarness → GovernorPreventLateQuorumHarness
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorCountingSimple.spec \
     --solc solc \
     --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --msg "$1"
+    --settings -copyLoopUnroll=4

certora/scripts/Round1/sanity.sh

@@ -1,16 +1,19 @@
-# make -C certora munged
+#!/usr/bin/env bash
+
+set -euxo pipefail
 
 # 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 solc --staging shelly/forSasha \
-#     --optimistic_loop \
-#     --msg "checking sanity on ${file%.*}"
-#     --settings -copyLoopUnroll=4
+#     certoraRun \
+#         certora/harnesses/$file \
+#         --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+#         --solc solc \
+#         --optimistic_loop \
+#         --settings -copyLoopUnroll=4 \
+#         --msg "checking sanity on ${file%.*}"
 # done
 
 # TimelockController
@@ -19,16 +22,13 @@ certoraRun \
     --verify TimelockControllerHarness:certora/specs/sanity.spec \
     --solc solc \
     --optimistic_loop \
-    --cloud \
     --msg "sanity and keccak check"
 
-
 # Votes
 # certoraRun \
 #     certora/harnesses/VotesHarness.sol \
 #     --verify VotesHarness:certora/specs/sanity.spec \
 #     --solc solc \
 #     --optimistic_loop \
-#     --cloud \
 #     --settings -strictDecompiler=false,-assumeUnwindCond \
 #     --msg "sanityVotes"

certora/scripts/Round1/sanityGovernor.sh

@@ -1,4 +1,6 @@
-make -C certora munged
+#!/usr/bin/env bash
+
+set -euxo pipefail
 
 for f in certora/harnesses/Wizard*.sol
 do
@@ -6,9 +8,9 @@ do
     file=$(basename $f)
     echo ${file%.*}
     certoraRun certora/harnesses/$file \
-    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
-    --solc solc --staging shelly/forSasha \
-    --optimistic_loop \
-    --msg "checking sanity on ${file%.*}"
-    --settings -copyLoopUnroll=4
+        --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+        --solc solc \
+        --optimistic_loop \
+        --settings -copyLoopUnroll=4 \
+        --msg "checking sanity on ${file%.*}"
 done

certora/scripts/Round1/sanityTokens.sh

@@ -1,6 +1,6 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-make -C certora munged
+set -euxo pipefail
 
 for f in certora/harnesses/ERC20{Votes,Permit,Wrapper}Harness.sol
 do
@@ -9,8 +9,8 @@ do
     echo ${file%.*}
     certoraRun certora/harnesses/$file \
         --verify ${file%.*}:certora/specs/sanity.spec "$@" \
-        --solc solc --staging \
+        --solc solc \
         --optimistic_loop \
-        --msg "checking sanity on ${file%.*}" \
-        --settings -copyLoopUnroll=4,-strictDecompiler=false
+        --settings -copyLoopUnroll=4,-strictDecompiler=false \
+        --msg "checking sanity on ${file%.*}"
 done

certora/scripts/Round1/verifyAll.sh

@@ -1,11 +1,10 @@
-#!/bin/bash
-
-make -C certora munged
-
+#!/usr/bin/env bash
 
+set -euxo pipefail
 
 for contract in certora/harnesses/Wizard*.sol;
 do
+    # NOTE: some spec wile are not governor related, and should be run on Wizard*.sol
     for spec in certora/specs/*.spec;
     do
         contractFile=$(basename $contract)
@@ -15,24 +14,24 @@ do
             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 \
-                --msg "checking $specFile on ${contractFile%.*}"
+                certoraRun \
+                    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                    --link ${contractFile%.*}:token=ERC20VotesHarness \
+                    --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                    --solc solc \
+                    --optimistic_loop \
+                    --disableLocalTypeChecking \
+                    --settings -copyLoopUnroll=4 \
+                    --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 \
-                --msg "checking $specFile on ${contractFile%.*}"
+                certoraRun \
+                    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                    --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                    --solc solc \
+                    --optimistic_loop \
+                    --disableLocalTypeChecking \
+                    --settings -copyLoopUnroll=4 \
+                    --msg "checking $specFile on ${contractFile%.*}"
             fi
         fi
     done

certora/scripts/Round1/verifyGovernor.sh

@@ -1,10 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-make -C certora munged
+set -euxo pipefail
 
 for contract in certora/harnesses/Wizard*.sol;
 do
-    for spec in certora/specs/governor*.spec;
+    for spec in certora/specs/Governor*.spec;
     do
         contractFile=$(basename $contract)
         specFile=$(basename $spec)
@@ -13,24 +13,24 @@ do
             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 \
-                --msg "checking $specFile on ${contractFile%.*}"
+                certoraRun \
+                    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                    --link ${contractFile%.*}:token=ERC20VotesHarness \
+                    --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                    --solc solc \
+                    --optimistic_loop \
+                    --disableLocalTypeChecking \
+                    --settings -copyLoopUnroll=4 \
+                    --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 \
-                --msg "checking $specFile on ${contractFile%.*}"
+                certoraRun \
+                    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                    --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                    --solc solc \
+                    --optimistic_loop \
+                    --disableLocalTypeChecking \
+                    --settings -copyLoopUnroll=4 \
+                    --msg "checking $specFile on ${contractFile%.*}"
             fi
         fi
     done

certora/scripts/verifyERC1155All.sh

@@ -1,8 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
 certoraRun \
     certora/harnesses/ERC1155/ERC1155Harness.sol \
     --verify ERC1155Harness:certora/specs/ERC1155.spec \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --cloud \
     --msg "ERC1155 verification all rules "

certora/scripts/verifyERC1155Burnable.sh

@@ -1,8 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
 certoraRun \
     certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
     --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --cloud \
     --msg "ERC1155 Burnable verification all rules"

certora/scripts/verifyERC1155BurnableSpecific.sh

@@ -1,9 +0,0 @@
-certoraRun \
-    certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
-    --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 3 \
-    --cloud \
-    --rule $1 \
-    --msg "ERC1155 Burnable verification specific rule $1"

certora/scripts/verifyERC1155Pausable.sh

@@ -1,8 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
 certoraRun \
     certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
     --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --cloud \
     --msg "ERC1155 Pausable verification all rules"

certora/scripts/verifyERC1155Specific.sh

@@ -1,9 +0,0 @@
-certoraRun \
-    certora/munged/token/ERC1155/ERC1155.sol \
-    --verify ERC1155:certora/specs/ERC1155.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 3 \
-    --cloud \
-    --rule $1 \
-    --msg "ERC1155 Burnable verification specific rule $1"

certora/scripts/verifyERC1155Supply.sh

@@ -1,8 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
 certoraRun \
     certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
     --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --cloud \
     --msg "ERC1155 Supply verification all rules"

certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -1,3 +1,7 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
 certoraRun \
     certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \

certora/scripts/verifyInitializable.sh

@@ -1,3 +1,7 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
 certoraRun \
     certora/harnesses/InitializableComplexHarness.sol \
     --verify InitializableComplexHarness:certora/specs/Initializable.spec \

certora/specs/sanity.spec

@@ -6,7 +6,6 @@ How it works:
     - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously.
 */
 
-
 rule sanity(method f) {
     env e;
     calldataarg arg;