From d916e2edf4c4bd7bb969cb8143cc98edbcf29eeb Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Fri, 23 Sep 2022 12:47:45 +0200 Subject: [PATCH] further script cleanup --- .../scripts/Round1/WizardControlFirstPriority.sh | 13 +++++++------ certora/scripts/Round1/WizardFirstTry.sh | 11 ++++++----- certora/scripts/Round2/verifyAccessControl.sh | 5 ++++- certora/scripts/Round2/verifyERC1155.sh | 5 ++++- certora/scripts/Round2/verifyERC20FlashMint.sh | 11 ++++++++--- certora/scripts/Round2/verifyERC20Votes.sh | 10 +++++----- certora/scripts/Round2/verifyERC20Wrapper.sh | 8 +++++--- certora/scripts/Round2/verifyERC721Votes.sh | 12 ++++++------ certora/scripts/Round2/verifyTimelock.sh | 7 ++++--- 9 files changed, 49 insertions(+), 33 deletions(-) diff --git a/certora/scripts/Round1/WizardControlFirstPriority.sh b/certora/scripts/Round1/WizardControlFirstPriority.sh index fd3f155e0..da7d172a4 100644 --- a/certora/scripts/Round1/WizardControlFirstPriority.sh +++ b/certora/scripts/Round1/WizardControlFirstPriority.sh @@ -1,12 +1,13 @@ -make -C certora munged +#!/usr/bin/env bash -certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \ +set -euxo pipefail + +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \ --link WizardControlFirstPriority:token=ERC20VotesHarness \ --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \ --solc solc \ - --disableLocalTypeChecking \ - --staging shelly/forSasha \ --optimistic_loop \ + --disableLocalTypeChecking \ --settings -copyLoopUnroll=4 \ - --rule canVoteDuringVotingPeriod \ - --msg "$1" + --rule canVoteDuringVotingPeriod diff --git a/certora/scripts/Round1/WizardFirstTry.sh b/certora/scripts/Round1/WizardFirstTry.sh index b475abf90..8d2f546db 100644 --- a/certora/scripts/Round1/WizardFirstTry.sh +++ b/certora/scripts/Round1/WizardFirstTry.sh @@ -1,10 +1,11 @@ -make -C certora munged +#!/usr/bin/env bash -certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \ +set -euxo pipefail + +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \ --verify WizardFirstTry:certora/specs/GovernorBase.spec \ --solc solc \ - --staging shelly/forSasha \ --optimistic_loop \ --disableLocalTypeChecking \ - --settings -copyLoopUnroll=4 \ - --msg "$1" + --settings -copyLoopUnroll=4 diff --git a/certora/scripts/Round2/verifyAccessControl.sh b/certora/scripts/Round2/verifyAccessControl.sh index 1763556d0..83ab08018 100644 --- a/certora/scripts/Round2/verifyAccessControl.sh +++ b/certora/scripts/Round2/verifyAccessControl.sh @@ -1,7 +1,10 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/AccessControlHarness.sol \ --verify AccessControlHarness:certora/specs/AccessControl.spec \ --solc solc \ --optimistic_loop \ - --cloud \ --msg "AccessControl verification" diff --git a/certora/scripts/Round2/verifyERC1155.sh b/certora/scripts/Round2/verifyERC1155.sh index 7826003aa..3bccdc0f6 100644 --- a/certora/scripts/Round2/verifyERC1155.sh +++ b/certora/scripts/Round2/verifyERC1155.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" diff --git a/certora/scripts/Round2/verifyERC20FlashMint.sh b/certora/scripts/Round2/verifyERC20FlashMint.sh index 75e6e37fd..7370d4bec 100644 --- a/certora/scripts/Round2/verifyERC20FlashMint.sh +++ b/certora/scripts/Round2/verifyERC20FlashMint.sh @@ -1,8 +1,13 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ - certora/harnesses/ERC20FlashMintHarness.sol certora/harnesses/IERC3156FlashBorrowerHarness.sol \ - certora/munged/token/ERC20/ERC20.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ + certora/harnesses/ERC20FlashMintHarness.sol \ + certora/harnesses/IERC3156FlashBorrowerHarness.sol \ + certora/munged/token/ERC20/ERC20.sol \ + certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ --solc solc \ --optimistic_loop \ - --cloud \ --msg "ERC20FlashMint verification" diff --git a/certora/scripts/Round2/verifyERC20Votes.sh b/certora/scripts/Round2/verifyERC20Votes.sh index 815a6136e..79530d58d 100644 --- a/certora/scripts/Round2/verifyERC20Votes.sh +++ b/certora/scripts/Round2/verifyERC20Votes.sh @@ -1,11 +1,11 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/ERC20VotesHarness.sol \ --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --cloud \ - --msg "ERC20Votes $1" \ - - # --disableLocalTypeChecking \ - # --staging "alex/new-dt-hashing-alpha" \ + --msg "ERC20Votes" \ No newline at end of file diff --git a/certora/scripts/Round2/verifyERC20Wrapper.sh b/certora/scripts/Round2/verifyERC20Wrapper.sh index 1d07e3b58..71d49cf0f 100644 --- a/certora/scripts/Round2/verifyERC20Wrapper.sh +++ b/certora/scripts/Round2/verifyERC20Wrapper.sh @@ -1,8 +1,10 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ - certora/harnesses/ERC20WrapperHarness.sol \ - certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ + certora/harnesses/ERC20WrapperHarness.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ --solc solc \ --optimistic_loop \ - --cloud \ --msg "ERC20Wrapper verification" diff --git a/certora/scripts/Round2/verifyERC721Votes.sh b/certora/scripts/Round2/verifyERC721Votes.sh index e92355f87..b9e7a8340 100644 --- a/certora/scripts/Round2/verifyERC721Votes.sh +++ b/certora/scripts/Round2/verifyERC721Votes.sh @@ -1,12 +1,12 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ - certora/harnesses/ERC721VotesHarness.sol \ - certora/munged/utils/Checkpoints.sol \ + certora/harnesses/ERC721VotesHarness.sol certora/munged/utils/Checkpoints.sol \ --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ --solc solc \ - --disableLocalTypeChecking \ --optimistic_loop \ + --disableLocalTypeChecking \ --settings -copyLoopUnroll=4 \ - --cloud \ --msg "ERC721Votes" - - # --staging "alex/new-dt-hashing-alpha" \ diff --git a/certora/scripts/Round2/verifyTimelock.sh b/certora/scripts/Round2/verifyTimelock.sh index 13e73bf63..2de5d4388 100644 --- a/certora/scripts/Round2/verifyTimelock.sh +++ b/certora/scripts/Round2/verifyTimelock.sh @@ -1,11 +1,12 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \ --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --cloud \ --settings -byteMapHashingPrecision=32 \ --msg "TimelockController verification" - - # --staging alex/new-dt-hashing-alpha \