From 3252e54f2b24a980d512d523548e32c000f39137 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 21 Sep 2022 17:41:13 +0200 Subject: [PATCH] use solc without version & remove send_only --- certora/scripts/Round1/Governor.sh | 2 +- .../scripts/Round1/GovernorCountingSimple-counting.sh | 2 +- certora/scripts/Round1/WizardControlFirstPriority.sh | 2 +- certora/scripts/Round1/WizardFirstTry.sh | 2 +- certora/scripts/Round1/sanity.sh | 7 +++---- certora/scripts/Round1/sanityGovernor.sh | 2 +- certora/scripts/Round1/sanityTokens.sh | 5 ++--- certora/scripts/Round1/verifyAll.sh | 5 +---- certora/scripts/Round1/verifyGovernor.sh | 8 +++----- certora/scripts/Round2/verifyAccessControl.sh | 6 ++---- certora/scripts/Round2/verifyAll2.sh | 11 ----------- certora/scripts/Round2/verifyERC1155.sh | 4 +--- certora/scripts/Round2/verifyERC20FlashMint.sh | 6 ++---- certora/scripts/Round2/verifyERC20Votes.sh | 3 +-- certora/scripts/Round2/verifyERC20Wrapper.sh | 6 ++---- certora/scripts/Round2/verifyERC721Votes.sh | 4 +--- certora/scripts/Round2/verifyTimelock.sh | 6 ++---- certora/scripts/Round3/round3.sh | 4 ---- certora/scripts/Round3/verifyERC1155Burnable.sh | 3 +-- certora/scripts/Round3/verifyERC1155Pausable.sh | 2 +- certora/scripts/Round3/verifyERC1155Supply.sh | 2 +- .../scripts/Round3/verifyGovernorPreventLateQuorum.sh | 5 +---- certora/scripts/Round3/verifyInitializable.sh | 5 +---- 23 files changed, 30 insertions(+), 72 deletions(-) delete mode 100644 certora/scripts/Round2/verifyAll2.sh delete mode 100644 certora/scripts/Round3/round3.sh diff --git a/certora/scripts/Round1/Governor.sh b/certora/scripts/Round1/Governor.sh index 53ade5060..5ca0f239b 100755 --- a/certora/scripts/Round1/Governor.sh +++ b/certora/scripts/Round1/Governor.sh @@ -2,7 +2,7 @@ make -C certora munged certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ --verify GovernorHarness:certora/specs/GovernorBase.spec \ - --solc solc8.0 \ + --solc solc \ --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ diff --git a/certora/scripts/Round1/GovernorCountingSimple-counting.sh b/certora/scripts/Round1/GovernorCountingSimple-counting.sh index e3b86b555..2d209d3f9 100644 --- a/certora/scripts/Round1/GovernorCountingSimple-counting.sh +++ b/certora/scripts/Round1/GovernorCountingSimple-counting.sh @@ -2,7 +2,7 @@ make -C certora munged certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ --msg "$1" diff --git a/certora/scripts/Round1/WizardControlFirstPriority.sh b/certora/scripts/Round1/WizardControlFirstPriority.sh index b815986ee..fd3f155e0 100644 --- a/certora/scripts/Round1/WizardControlFirstPriority.sh +++ b/certora/scripts/Round1/WizardControlFirstPriority.sh @@ -3,7 +3,7 @@ make -C certora munged certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \ --link WizardControlFirstPriority:token=ERC20VotesHarness \ --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \ - --solc solc8.2 \ + --solc solc \ --disableLocalTypeChecking \ --staging shelly/forSasha \ --optimistic_loop \ diff --git a/certora/scripts/Round1/WizardFirstTry.sh b/certora/scripts/Round1/WizardFirstTry.sh index fd5a32ab4..b475abf90 100644 --- a/certora/scripts/Round1/WizardFirstTry.sh +++ b/certora/scripts/Round1/WizardFirstTry.sh @@ -2,7 +2,7 @@ make -C certora munged certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \ --verify WizardFirstTry:certora/specs/GovernorBase.spec \ - --solc solc8.2 \ + --solc solc \ --staging shelly/forSasha \ --optimistic_loop \ --disableLocalTypeChecking \ diff --git a/certora/scripts/Round1/sanity.sh b/certora/scripts/Round1/sanity.sh index afead788d..be8f404a6 100644 --- a/certora/scripts/Round1/sanity.sh +++ b/certora/scripts/Round1/sanity.sh @@ -7,7 +7,7 @@ # echo ${file%.*} # certoraRun certora/harnesses/$file \ # --verify ${file%.*}:certora/specs/sanity.spec "$@" \ -# --solc solc8.2 --staging shelly/forSasha \ +# --solc solc --staging shelly/forSasha \ # --optimistic_loop \ # --msg "checking sanity on ${file%.*}" # --settings -copyLoopUnroll=4 @@ -17,7 +17,7 @@ certoraRun \ certora/harnesses/TimelockControllerHarness.sol \ --verify TimelockControllerHarness:certora/specs/sanity.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --cloud \ --msg "sanity and keccak check" @@ -27,9 +27,8 @@ certoraRun \ # certoraRun \ # certora/harnesses/VotesHarness.sol \ # --verify VotesHarness:certora/specs/sanity.spec \ -# --solc solc8.2 \ +# --solc solc \ # --optimistic_loop \ # --cloud \ # --settings -strictDecompiler=false,-assumeUnwindCond \ # --msg "sanityVotes" - diff --git a/certora/scripts/Round1/sanityGovernor.sh b/certora/scripts/Round1/sanityGovernor.sh index b6cdb4ec3..f979dd364 100755 --- a/certora/scripts/Round1/sanityGovernor.sh +++ b/certora/scripts/Round1/sanityGovernor.sh @@ -7,7 +7,7 @@ do echo ${file%.*} certoraRun certora/harnesses/$file \ --verify ${file%.*}:certora/specs/sanity.spec "$@" \ - --solc solc8.2 --staging shelly/forSasha \ + --solc solc --staging shelly/forSasha \ --optimistic_loop \ --msg "checking sanity on ${file%.*}" --settings -copyLoopUnroll=4 diff --git a/certora/scripts/Round1/sanityTokens.sh b/certora/scripts/Round1/sanityTokens.sh index 30828055b..308a00623 100755 --- a/certora/scripts/Round1/sanityTokens.sh +++ b/certora/scripts/Round1/sanityTokens.sh @@ -9,9 +9,8 @@ do echo ${file%.*} certoraRun certora/harnesses/$file \ --verify ${file%.*}:certora/specs/sanity.spec "$@" \ - --solc solc8.2 --staging \ + --solc solc --staging \ --optimistic_loop \ --msg "checking sanity on ${file%.*}" \ - --settings -copyLoopUnroll=4,-strictDecompiler=false \ - --send_only + --settings -copyLoopUnroll=4,-strictDecompiler=false done diff --git a/certora/scripts/Round1/verifyAll.sh b/certora/scripts/Round1/verifyAll.sh index eb71ead26..d770a8963 100644 --- a/certora/scripts/Round1/verifyAll.sh +++ b/certora/scripts/Round1/verifyAll.sh @@ -7,7 +7,7 @@ make -C certora munged for contract in certora/harnesses/Wizard*.sol; do for spec in certora/specs/*.spec; - do + do contractFile=$(basename $contract) specFile=$(basename $spec) if [[ "${specFile%.*}" != "RulesInProgress" ]]; @@ -23,7 +23,6 @@ do --disableLocalTypeChecking \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --send_only \ --msg "checking $specFile on ${contractFile%.*}" else certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ @@ -33,10 +32,8 @@ do --disableLocalTypeChecking \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --send_only \ --msg "checking $specFile on ${contractFile%.*}" fi fi done done - diff --git a/certora/scripts/Round1/verifyGovernor.sh b/certora/scripts/Round1/verifyGovernor.sh index 2e6639422..0ce0eb1e5 100755 --- a/certora/scripts/Round1/verifyGovernor.sh +++ b/certora/scripts/Round1/verifyGovernor.sh @@ -5,7 +5,7 @@ make -C certora munged for contract in certora/harnesses/Wizard*.sol; do for spec in certora/specs/governor*.spec; - do + do contractFile=$(basename $contract) specFile=$(basename $spec) if [[ "${specFile%.*}" != "RulesInProgress" ]]; @@ -16,22 +16,20 @@ do certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ --link ${contractFile%.*}:token=ERC20VotesHarness \ --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc8.2 \ + --solc solc \ --staging shelly/forSasha \ --disableLocalTypeChecking \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --send_only \ --msg "checking $specFile on ${contractFile%.*}" else certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc8.2 \ + --solc solc \ --staging shelly/forSasha \ --disableLocalTypeChecking \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --send_only \ --msg "checking $specFile on ${contractFile%.*}" fi fi diff --git a/certora/scripts/Round2/verifyAccessControl.sh b/certora/scripts/Round2/verifyAccessControl.sh index 6fb08381f..1763556d0 100644 --- a/certora/scripts/Round2/verifyAccessControl.sh +++ b/certora/scripts/Round2/verifyAccessControl.sh @@ -1,9 +1,7 @@ certoraRun \ certora/harnesses/AccessControlHarness.sol \ --verify AccessControlHarness:certora/specs/AccessControl.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --cloud \ - --msg "AccessControl verification" \ - --send_only - \ No newline at end of file + --msg "AccessControl verification" diff --git a/certora/scripts/Round2/verifyAll2.sh b/certora/scripts/Round2/verifyAll2.sh deleted file mode 100644 index e1805a2ec..000000000 --- a/certora/scripts/Round2/verifyAll2.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/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/Round2/verifyERC1155.sh b/certora/scripts/Round2/verifyERC1155.sh index 733882f0f..7826003aa 100644 --- a/certora/scripts/Round2/verifyERC1155.sh +++ b/certora/scripts/Round2/verifyERC1155.sh @@ -1,10 +1,8 @@ certoraRun \ certora/harnesses/ERC1155/ERC1155Harness.sol \ --verify ERC1155Harness:certora/specs/ERC1155.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --send_only \ --cloud \ --msg "ERC1155" - diff --git a/certora/scripts/Round2/verifyERC20FlashMint.sh b/certora/scripts/Round2/verifyERC20FlashMint.sh index d8d03d24a..75e6e37fd 100644 --- a/certora/scripts/Round2/verifyERC20FlashMint.sh +++ b/certora/scripts/Round2/verifyERC20FlashMint.sh @@ -2,9 +2,7 @@ certoraRun \ 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 solc8.2 \ + --solc solc \ --optimistic_loop \ --cloud \ - --msg "ERC20FlashMint verification" \ - --send_only - \ No newline at end of file + --msg "ERC20FlashMint verification" diff --git a/certora/scripts/Round2/verifyERC20Votes.sh b/certora/scripts/Round2/verifyERC20Votes.sh index c9e5db059..815a6136e 100644 --- a/certora/scripts/Round2/verifyERC20Votes.sh +++ b/certora/scripts/Round2/verifyERC20Votes.sh @@ -1,11 +1,10 @@ certoraRun \ certora/harnesses/ERC20VotesHarness.sol \ --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ --cloud \ - --send_only \ --msg "ERC20Votes $1" \ # --disableLocalTypeChecking \ diff --git a/certora/scripts/Round2/verifyERC20Wrapper.sh b/certora/scripts/Round2/verifyERC20Wrapper.sh index 6b60c9556..1d07e3b58 100644 --- a/certora/scripts/Round2/verifyERC20Wrapper.sh +++ b/certora/scripts/Round2/verifyERC20Wrapper.sh @@ -2,9 +2,7 @@ certoraRun \ certora/harnesses/ERC20WrapperHarness.sol \ certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --cloud \ - --msg "ERC20Wrapper verification" \ - --send_only - \ No newline at end of file + --msg "ERC20Wrapper verification" diff --git a/certora/scripts/Round2/verifyERC721Votes.sh b/certora/scripts/Round2/verifyERC721Votes.sh index 7e023ef28..e92355f87 100644 --- a/certora/scripts/Round2/verifyERC721Votes.sh +++ b/certora/scripts/Round2/verifyERC721Votes.sh @@ -2,13 +2,11 @@ certoraRun \ certora/harnesses/ERC721VotesHarness.sol \ certora/munged/utils/Checkpoints.sol \ --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ - --solc solc8.2 \ + --solc solc \ --disableLocalTypeChecking \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ --cloud \ - --send_only \ --msg "ERC721Votes" # --staging "alex/new-dt-hashing-alpha" \ - diff --git a/certora/scripts/Round2/verifyTimelock.sh b/certora/scripts/Round2/verifyTimelock.sh index 270f76db9..13e73bf63 100644 --- a/certora/scripts/Round2/verifyTimelock.sh +++ b/certora/scripts/Round2/verifyTimelock.sh @@ -1,13 +1,11 @@ certoraRun \ certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \ --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --cloud \ --settings -byteMapHashingPrecision=32 \ - --msg "TimelockController verification" \ - --send_only \ + --msg "TimelockController verification" # --staging alex/new-dt-hashing-alpha \ - \ No newline at end of file diff --git a/certora/scripts/Round3/round3.sh b/certora/scripts/Round3/round3.sh deleted file mode 100644 index f976e610c..000000000 --- a/certora/scripts/Round3/round3.sh +++ /dev/null @@ -1,4 +0,0 @@ -for script in ./certora/scripts/Round3/verify*.sh -do - sh $script -done \ No newline at end of file diff --git a/certora/scripts/Round3/verifyERC1155Burnable.sh b/certora/scripts/Round3/verifyERC1155Burnable.sh index 6d60cf746..5980967d2 100644 --- a/certora/scripts/Round3/verifyERC1155Burnable.sh +++ b/certora/scripts/Round3/verifyERC1155Burnable.sh @@ -1,8 +1,7 @@ certoraRun \ certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ - --solc solc8.4 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --msg "ERC1155 Burnable verification all rules" - \ No newline at end of file diff --git a/certora/scripts/Round3/verifyERC1155Pausable.sh b/certora/scripts/Round3/verifyERC1155Pausable.sh index bfddf66de..41472c51e 100755 --- a/certora/scripts/Round3/verifyERC1155Pausable.sh +++ b/certora/scripts/Round3/verifyERC1155Pausable.sh @@ -1,7 +1,7 @@ certoraRun \ certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ - --solc solc8.4 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --msg "ERC1155 Pausable verification all rules" diff --git a/certora/scripts/Round3/verifyERC1155Supply.sh b/certora/scripts/Round3/verifyERC1155Supply.sh index 1b688c6e3..91a866870 100755 --- a/certora/scripts/Round3/verifyERC1155Supply.sh +++ b/certora/scripts/Round3/verifyERC1155Supply.sh @@ -1,7 +1,7 @@ certoraRun \ certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ - --solc solc8.4 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --msg "ERC1155 Supply verification all rules" diff --git a/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh b/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh index 81720cae0..663ce0121 100644 --- a/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh @@ -1,10 +1,7 @@ certoraRun \ certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ - --solc solc8.4 \ + --solc solc \ --optimistic_loop \ --loop_iter 1 \ --msg "GovernorPreventLateQuorum verification all rules" \ - - - diff --git a/certora/scripts/Round3/verifyInitializable.sh b/certora/scripts/Round3/verifyInitializable.sh index 30dba2bb8..3aa43ea8c 100644 --- a/certora/scripts/Round3/verifyInitializable.sh +++ b/certora/scripts/Round3/verifyInitializable.sh @@ -1,10 +1,7 @@ certoraRun \ certora/harnesses/InitializableComplexHarness.sol \ --verify InitializableComplexHarness:certora/specs/Initializable.spec \ - --solc solc8.4 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --msg "Initializable verificaiton all rules on complex harness" \ - - -