From 3e6045155e5432b1c25a27ab97c61d689ec653e3 Mon Sep 17 00:00:00 2001 From: Nick Armstrong Date: Thu, 11 Aug 2022 20:40:13 -0700 Subject: [PATCH] reorganized scripts --- certora/scripts/{old => Round1}/Governor.sh | 0 .../GovernorCountingSimple-counting.sh | 0 .../WizardControlFirstPriority.sh | 0 .../scripts/{old => Round1}/WizardFirstTry.sh | 0 certora/scripts/{old => Round1}/sanity.sh | 0 .../scripts/{old => Round1}/sanityGovernor.sh | 0 .../scripts/{old => Round1}/sanityTokens.sh | 0 certora/scripts/{old => Round1}/verifyAll.sh | 0 .../scripts/{old => Round1}/verifyGovernor.sh | 0 .../{old => Round2}/verifyAccessControl.sh | 3 ++- certora/scripts/Round2/verifyAll2.sh | 11 ++++++++ .../scripts/{old => Round2}/verifyERC1155.sh | 1 + .../{old => Round2}/verifyERC20FlashMint.sh | 3 ++- certora/scripts/Round2/verifyERC20Votes.sh | 13 ++++++++++ .../{old => Round2}/verifyERC20Wrapper.sh | 3 ++- certora/scripts/Round2/verifyERC721Votes.sh | 14 ++++++++++ .../scripts/{old => Round2}/verifyTimelock.sh | 7 +++-- certora/scripts/old/ERC20VotesRule.sh | 23 ---------------- certora/scripts/old/verifyAll2.sh | 7 ----- certora/scripts/old/verifyERC20Votes.sh | 25 ------------------ certora/scripts/old/verifyERC721Votes.sh | 26 ------------------- 21 files changed, 50 insertions(+), 86 deletions(-) rename certora/scripts/{old => Round1}/Governor.sh (100%) rename certora/scripts/{old => Round1}/GovernorCountingSimple-counting.sh (100%) rename certora/scripts/{old => Round1}/WizardControlFirstPriority.sh (100%) rename certora/scripts/{old => Round1}/WizardFirstTry.sh (100%) rename certora/scripts/{old => Round1}/sanity.sh (100%) rename certora/scripts/{old => Round1}/sanityGovernor.sh (100%) rename certora/scripts/{old => Round1}/sanityTokens.sh (100%) rename certora/scripts/{old => Round1}/verifyAll.sh (100%) rename certora/scripts/{old => Round1}/verifyGovernor.sh (100%) rename certora/scripts/{old => Round2}/verifyAccessControl.sh (77%) create mode 100644 certora/scripts/Round2/verifyAll2.sh rename certora/scripts/{old => Round2}/verifyERC1155.sh (94%) rename certora/scripts/{old => Round2}/verifyERC20FlashMint.sh (85%) create mode 100644 certora/scripts/Round2/verifyERC20Votes.sh rename certora/scripts/{old => Round2}/verifyERC20Wrapper.sh (82%) create mode 100644 certora/scripts/Round2/verifyERC721Votes.sh rename certora/scripts/{old => Round2}/verifyTimelock.sh (71%) delete mode 100644 certora/scripts/old/ERC20VotesRule.sh delete mode 100644 certora/scripts/old/verifyAll2.sh delete mode 100644 certora/scripts/old/verifyERC20Votes.sh delete mode 100644 certora/scripts/old/verifyERC721Votes.sh diff --git a/certora/scripts/old/Governor.sh b/certora/scripts/Round1/Governor.sh similarity index 100% rename from certora/scripts/old/Governor.sh rename to certora/scripts/Round1/Governor.sh diff --git a/certora/scripts/old/GovernorCountingSimple-counting.sh b/certora/scripts/Round1/GovernorCountingSimple-counting.sh similarity index 100% rename from certora/scripts/old/GovernorCountingSimple-counting.sh rename to certora/scripts/Round1/GovernorCountingSimple-counting.sh diff --git a/certora/scripts/old/WizardControlFirstPriority.sh b/certora/scripts/Round1/WizardControlFirstPriority.sh similarity index 100% rename from certora/scripts/old/WizardControlFirstPriority.sh rename to certora/scripts/Round1/WizardControlFirstPriority.sh diff --git a/certora/scripts/old/WizardFirstTry.sh b/certora/scripts/Round1/WizardFirstTry.sh similarity index 100% rename from certora/scripts/old/WizardFirstTry.sh rename to certora/scripts/Round1/WizardFirstTry.sh diff --git a/certora/scripts/old/sanity.sh b/certora/scripts/Round1/sanity.sh similarity index 100% rename from certora/scripts/old/sanity.sh rename to certora/scripts/Round1/sanity.sh diff --git a/certora/scripts/old/sanityGovernor.sh b/certora/scripts/Round1/sanityGovernor.sh similarity index 100% rename from certora/scripts/old/sanityGovernor.sh rename to certora/scripts/Round1/sanityGovernor.sh diff --git a/certora/scripts/old/sanityTokens.sh b/certora/scripts/Round1/sanityTokens.sh similarity index 100% rename from certora/scripts/old/sanityTokens.sh rename to certora/scripts/Round1/sanityTokens.sh diff --git a/certora/scripts/old/verifyAll.sh b/certora/scripts/Round1/verifyAll.sh similarity index 100% rename from certora/scripts/old/verifyAll.sh rename to certora/scripts/Round1/verifyAll.sh diff --git a/certora/scripts/old/verifyGovernor.sh b/certora/scripts/Round1/verifyGovernor.sh similarity index 100% rename from certora/scripts/old/verifyGovernor.sh rename to certora/scripts/Round1/verifyGovernor.sh diff --git a/certora/scripts/old/verifyAccessControl.sh b/certora/scripts/Round2/verifyAccessControl.sh similarity index 77% rename from certora/scripts/old/verifyAccessControl.sh rename to certora/scripts/Round2/verifyAccessControl.sh index eb706d063..6fb08381f 100644 --- a/certora/scripts/old/verifyAccessControl.sh +++ b/certora/scripts/Round2/verifyAccessControl.sh @@ -4,5 +4,6 @@ certoraRun \ --solc solc8.2 \ --optimistic_loop \ --cloud \ - --msg "AccessControl verification" + --msg "AccessControl verification" \ + --send_only \ No newline at end of file diff --git a/certora/scripts/Round2/verifyAll2.sh b/certora/scripts/Round2/verifyAll2.sh new file mode 100644 index 000000000..e1805a2ec --- /dev/null +++ b/certora/scripts/Round2/verifyAll2.sh @@ -0,0 +1,11 @@ +#!/bin/bash + +make -C certora munged + +sh certora/scripts/Round2/verifyAccessControl.sh +sh certora/scripts/Round2/verifyERC20FlashMint.sh +sh certora/scripts/Round2/verifyERC20Votes.sh +sh certora/scripts/Round2/verifyERC20Wrapper.sh +sh certora/scripts/Round2/verifyERC721Votes.sh +sh certora/scripts/Round2/verifyERC1155.sh +sh certora/scripts/Round2/verifyTimelock.sh \ No newline at end of file diff --git a/certora/scripts/old/verifyERC1155.sh b/certora/scripts/Round2/verifyERC1155.sh similarity index 94% rename from certora/scripts/old/verifyERC1155.sh rename to certora/scripts/Round2/verifyERC1155.sh index d2c00df78..733882f0f 100644 --- a/certora/scripts/old/verifyERC1155.sh +++ b/certora/scripts/Round2/verifyERC1155.sh @@ -5,5 +5,6 @@ certoraRun \ --optimistic_loop \ --loop_iter 3 \ --send_only \ + --cloud \ --msg "ERC1155" diff --git a/certora/scripts/old/verifyERC20FlashMint.sh b/certora/scripts/Round2/verifyERC20FlashMint.sh similarity index 85% rename from certora/scripts/old/verifyERC20FlashMint.sh rename to certora/scripts/Round2/verifyERC20FlashMint.sh index 0af81e006..d8d03d24a 100644 --- a/certora/scripts/old/verifyERC20FlashMint.sh +++ b/certora/scripts/Round2/verifyERC20FlashMint.sh @@ -5,5 +5,6 @@ certoraRun \ --solc solc8.2 \ --optimistic_loop \ --cloud \ - --msg "ERC20FlashMint verification" + --msg "ERC20FlashMint verification" \ + --send_only \ No newline at end of file diff --git a/certora/scripts/Round2/verifyERC20Votes.sh b/certora/scripts/Round2/verifyERC20Votes.sh new file mode 100644 index 000000000..dea9bc695 --- /dev/null +++ b/certora/scripts/Round2/verifyERC20Votes.sh @@ -0,0 +1,13 @@ +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol \ + --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ + --solc solc8.2 \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --cloud \ + --send_only \ + --msg "ERC20Votes" \ + + + # --staging "alex/new-dt-hashing-alpha" \ diff --git a/certora/scripts/old/verifyERC20Wrapper.sh b/certora/scripts/Round2/verifyERC20Wrapper.sh similarity index 82% rename from certora/scripts/old/verifyERC20Wrapper.sh rename to certora/scripts/Round2/verifyERC20Wrapper.sh index e1ef85ef0..6b60c9556 100644 --- a/certora/scripts/old/verifyERC20Wrapper.sh +++ b/certora/scripts/Round2/verifyERC20Wrapper.sh @@ -5,5 +5,6 @@ certoraRun \ --solc solc8.2 \ --optimistic_loop \ --cloud \ - --msg "ERC20Wrapper verification" + --msg "ERC20Wrapper verification" \ + --send_only \ No newline at end of file diff --git a/certora/scripts/Round2/verifyERC721Votes.sh b/certora/scripts/Round2/verifyERC721Votes.sh new file mode 100644 index 000000000..7e023ef28 --- /dev/null +++ b/certora/scripts/Round2/verifyERC721Votes.sh @@ -0,0 +1,14 @@ +certoraRun \ + certora/harnesses/ERC721VotesHarness.sol \ + certora/munged/utils/Checkpoints.sol \ + --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ + --solc solc8.2 \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --cloud \ + --send_only \ + --msg "ERC721Votes" + + # --staging "alex/new-dt-hashing-alpha" \ + diff --git a/certora/scripts/old/verifyTimelock.sh b/certora/scripts/Round2/verifyTimelock.sh similarity index 71% rename from certora/scripts/old/verifyTimelock.sh rename to certora/scripts/Round2/verifyTimelock.sh index 5afc11911..270f76db9 100644 --- a/certora/scripts/old/verifyTimelock.sh +++ b/certora/scripts/Round2/verifyTimelock.sh @@ -4,7 +4,10 @@ certoraRun \ --solc solc8.2 \ --optimistic_loop \ --loop_iter 3 \ - --staging alex/new-dt-hashing-alpha \ + --cloud \ --settings -byteMapHashingPrecision=32 \ - --msg "TimelockController verification" + --msg "TimelockController verification" \ + --send_only \ + + # --staging alex/new-dt-hashing-alpha \ \ No newline at end of file diff --git a/certora/scripts/old/ERC20VotesRule.sh b/certora/scripts/old/ERC20VotesRule.sh deleted file mode 100644 index 28517b730..000000000 --- a/certora/scripts/old/ERC20VotesRule.sh +++ /dev/null @@ -1,23 +0,0 @@ -if [ -z "$2" ] - then - echo "Incorrect number of arguments" - echo "" - echo "Usage: (from git root)" - echo " ./certora/scripts/`basename $0` [message describing the run] [rule or invariant]" - echo "" - exit 1 -fi - -rule=$1 -msg=$2 -shift 2 - -certoraRun \ - certora/harnesses/ERC20VotesHarness.sol \ - --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ - --solc solc8.2 \ - --optimistic_loop \ - --rule ${rule} \ - --msg "${msg}" \ - --staging "alex/new-dt-hashing-alpha" \ - # --rule_sanity \ \ No newline at end of file diff --git a/certora/scripts/old/verifyAll2.sh b/certora/scripts/old/verifyAll2.sh deleted file mode 100644 index 43c73e477..000000000 --- a/certora/scripts/old/verifyAll2.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/bash - -make -C certora munged - -sh certora/scripts/verifyAllSasha -sh certora/scripts/verifyERC20Votes.sh "checking ERC20Votes.spec on ERC20Votes.sol" -sh certora/scripts/verifyERC721Votes.sh "checking ERC721Votes.spec on draft-ERC721Votes.sol and Votes.sol" \ No newline at end of file diff --git a/certora/scripts/old/verifyERC20Votes.sh b/certora/scripts/old/verifyERC20Votes.sh deleted file mode 100644 index 8bc5ed9fc..000000000 --- a/certora/scripts/old/verifyERC20Votes.sh +++ /dev/null @@ -1,25 +0,0 @@ -make -C certora munged - -if [ -z "$1" ] - then - echo "Incorrect number of arguments" - echo "" - echo "Usage: (from git root)" - echo " ./certora/scripts/`basename $0` [message describing the run]" - echo "" - exit 1 -fi - -msg=$1 -shift 1 - -certoraRun \ - certora/harnesses/ERC20VotesHarness.sol \ - --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ - --solc solc8.2 \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --send_only \ - --staging "alex/new-dt-hashing-alpha" \ - --msg "${msg}" \ diff --git a/certora/scripts/old/verifyERC721Votes.sh b/certora/scripts/old/verifyERC721Votes.sh deleted file mode 100644 index e2a7320f9..000000000 --- a/certora/scripts/old/verifyERC721Votes.sh +++ /dev/null @@ -1,26 +0,0 @@ -make -C certora munged - -if [ -z "$1" ] - then - echo "Incorrect number of arguments" - echo "" - echo "Usage: (from git root)" - echo " ./certora/scripts/`basename $0` [message describing the run]" - echo "" - exit 1 -fi - -msg=$1 -shift 1 - -certoraRun \ - certora/harnesses/ERC721VotesHarness.sol \ - certora/munged/utils/Checkpoints.sol \ - --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ - --solc solc8.2 \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --send_only \ - --staging "alex/new-dt-hashing-alpha" \ - --msg "${msg}"