further script cleanup

This commit is contained in:
Hadrien Croubois
2022-09-23 12:47:45 +02:00
parent 3075181276
commit d916e2edf4
9 changed files with 49 additions and 33 deletions

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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