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 \