NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

use solc without version & remove send_only

Browse Source
This commit is contained in:
Hadrien Croubois
2022-09-21 17:41:13 +02:00
parent cc7837fb46
commit 3252e54f2b
23 changed files with 30 additions and 72 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
certora/scripts/Round1/Governor.sh
View File

@ -2,7 +2,7 @@ make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
--verify GovernorHarness:certora/specs/GovernorBase.spec \ --verify GovernorHarness:certora/specs/GovernorBase.spec \
--solc solc8.0 \ --solc solc \
--staging shelly/forSasha \ --staging shelly/forSasha \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \

2
certora/scripts/Round1/GovernorCountingSimple-counting.sh
View File

@ -2,7 +2,7 @@ make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
--verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--msg "$1" --msg "$1"

2
certora/scripts/Round1/WizardControlFirstPriority.sh
View File

@ -3,7 +3,7 @@ make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
--link WizardControlFirstPriority:token=ERC20VotesHarness \ --link WizardControlFirstPriority:token=ERC20VotesHarness \
--verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \ --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
--solc solc8.2 \ --solc solc \
--disableLocalTypeChecking \ --disableLocalTypeChecking \
--staging shelly/forSasha \ --staging shelly/forSasha \
--optimistic_loop \ --optimistic_loop \

2
certora/scripts/Round1/WizardFirstTry.sh
View File

@ -2,7 +2,7 @@ make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
--verify WizardFirstTry:certora/specs/GovernorBase.spec \ --verify WizardFirstTry:certora/specs/GovernorBase.spec \
--solc solc8.2 \ --solc solc \
--staging shelly/forSasha \ --staging shelly/forSasha \
--optimistic_loop \ --optimistic_loop \
--disableLocalTypeChecking \ --disableLocalTypeChecking \

7
certora/scripts/Round1/sanity.sh
View File

@ -7,7 +7,7 @@
# echo ${file%.*} # echo ${file%.*}
# certoraRun certora/harnesses/$file \ # certoraRun certora/harnesses/$file \
# --verify ${file%.*}:certora/specs/sanity.spec "$@" \ # --verify ${file%.*}:certora/specs/sanity.spec "$@" \
# --solc solc8.2 --staging shelly/forSasha \ # --solc solc --staging shelly/forSasha \
# --optimistic_loop \ # --optimistic_loop \
# --msg "checking sanity on ${file%.*}" # --msg "checking sanity on ${file%.*}"
# --settings -copyLoopUnroll=4 # --settings -copyLoopUnroll=4
@ -17,7 +17,7 @@
certoraRun \ certoraRun \
certora/harnesses/TimelockControllerHarness.sol \ certora/harnesses/TimelockControllerHarness.sol \
--verify TimelockControllerHarness:certora/specs/sanity.spec \ --verify TimelockControllerHarness:certora/specs/sanity.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--cloud \ --cloud \
--msg "sanity and keccak check" --msg "sanity and keccak check"
@ -27,9 +27,8 @@ certoraRun \
# certoraRun \ # certoraRun \
# certora/harnesses/VotesHarness.sol \ # certora/harnesses/VotesHarness.sol \
# --verify VotesHarness:certora/specs/sanity.spec \ # --verify VotesHarness:certora/specs/sanity.spec \
# --solc solc8.2 \ # --solc solc \
# --optimistic_loop \ # --optimistic_loop \
# --cloud \ # --cloud \
# --settings -strictDecompiler=false,-assumeUnwindCond \ # --settings -strictDecompiler=false,-assumeUnwindCond \
# --msg "sanityVotes" # --msg "sanityVotes"

2
certora/scripts/Round1/sanityGovernor.sh
View File

@ -7,7 +7,7 @@ do
echo ${file%.*} echo ${file%.*}
certoraRun certora/harnesses/$file \ certoraRun certora/harnesses/$file \
--verify ${file%.*}:certora/specs/sanity.spec "$@" \ --verify ${file%.*}:certora/specs/sanity.spec "$@" \
--solc solc8.2 --staging shelly/forSasha \ --solc solc --staging shelly/forSasha \
--optimistic_loop \ --optimistic_loop \
--msg "checking sanity on ${file%.*}" --msg "checking sanity on ${file%.*}"
--settings -copyLoopUnroll=4 --settings -copyLoopUnroll=4

5
certora/scripts/Round1/sanityTokens.sh
View File

@ -9,9 +9,8 @@ do
echo ${file%.*} echo ${file%.*}
certoraRun certora/harnesses/$file \ certoraRun certora/harnesses/$file \
--verify ${file%.*}:certora/specs/sanity.spec "$@" \ --verify ${file%.*}:certora/specs/sanity.spec "$@" \
--solc solc8.2 --staging \ --solc solc --staging \
--optimistic_loop \ --optimistic_loop \
--msg "checking sanity on ${file%.*}" \ --msg "checking sanity on ${file%.*}" \
--settings -copyLoopUnroll=4,-strictDecompiler=false \ --settings -copyLoopUnroll=4,-strictDecompiler=false
--send_only
done done

5
certora/scripts/Round1/verifyAll.sh
View File

@ -7,7 +7,7 @@ make -C certora munged
for contract in certora/harnesses/Wizard*.sol; for contract in certora/harnesses/Wizard*.sol;
do do
for spec in certora/specs/*.spec; for spec in certora/specs/*.spec;
do do
contractFile=$(basename $contract) contractFile=$(basename $contract)
specFile=$(basename $spec) specFile=$(basename $spec)
if [[ "${specFile%.*}" != "RulesInProgress" ]]; if [[ "${specFile%.*}" != "RulesInProgress" ]];
@ -23,7 +23,6 @@ do
--disableLocalTypeChecking \ --disableLocalTypeChecking \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--send_only \
--msg "checking $specFile on ${contractFile%.*}" --msg "checking $specFile on ${contractFile%.*}"
else else
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
@ -33,10 +32,8 @@ do
--disableLocalTypeChecking \ --disableLocalTypeChecking \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--send_only \
--msg "checking $specFile on ${contractFile%.*}" --msg "checking $specFile on ${contractFile%.*}"
fi fi
fi fi
done done
done done

8
certora/scripts/Round1/verifyGovernor.sh
View File

@ -5,7 +5,7 @@ make -C certora munged
for contract in certora/harnesses/Wizard*.sol; for contract in certora/harnesses/Wizard*.sol;
do do
for spec in certora/specs/governor*.spec; for spec in certora/specs/governor*.spec;
do do
contractFile=$(basename $contract) contractFile=$(basename $contract)
specFile=$(basename $spec) specFile=$(basename $spec)
if [[ "${specFile%.*}" != "RulesInProgress" ]]; if [[ "${specFile%.*}" != "RulesInProgress" ]];
@ -16,22 +16,20 @@ do
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
--link ${contractFile%.*}:token=ERC20VotesHarness \ --link ${contractFile%.*}:token=ERC20VotesHarness \
--verify ${contractFile%.*}:certora/specs/$specFile "$@" \ --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
--solc solc8.2 \ --solc solc \
--staging shelly/forSasha \ --staging shelly/forSasha \
--disableLocalTypeChecking \ --disableLocalTypeChecking \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--send_only \
--msg "checking $specFile on ${contractFile%.*}" --msg "checking $specFile on ${contractFile%.*}"
else else
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
--verify ${contractFile%.*}:certora/specs/$specFile "$@" \ --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
--solc solc8.2 \ --solc solc \
--staging shelly/forSasha \ --staging shelly/forSasha \
--disableLocalTypeChecking \ --disableLocalTypeChecking \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--send_only \
--msg "checking $specFile on ${contractFile%.*}" --msg "checking $specFile on ${contractFile%.*}"
fi fi
fi fi

6
certora/scripts/Round2/verifyAccessControl.sh
View File

@ -1,9 +1,7 @@
certoraRun \ certoraRun \
certora/harnesses/AccessControlHarness.sol \ certora/harnesses/AccessControlHarness.sol \
--verify AccessControlHarness:certora/specs/AccessControl.spec \ --verify AccessControlHarness:certora/specs/AccessControl.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--cloud \ --cloud \
--msg "AccessControl verification" \ --msg "AccessControl verification"
--send_only

11
certora/scripts/Round2/verifyAll2.sh
View File

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

4
certora/scripts/Round2/verifyERC1155.sh
View File

@ -1,10 +1,8 @@
certoraRun \ certoraRun \
certora/harnesses/ERC1155/ERC1155Harness.sol \ certora/harnesses/ERC1155/ERC1155Harness.sol \
--verify ERC1155Harness:certora/specs/ERC1155.spec \ --verify ERC1155Harness:certora/specs/ERC1155.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--loop_iter 3 \ --loop_iter 3 \
--send_only \
--cloud \ --cloud \
--msg "ERC1155" --msg "ERC1155"

6
certora/scripts/Round2/verifyERC20FlashMint.sh
View File

@ -2,9 +2,7 @@ certoraRun \
certora/harnesses/ERC20FlashMintHarness.sol certora/harnesses/IERC3156FlashBorrowerHarness.sol \ certora/harnesses/ERC20FlashMintHarness.sol certora/harnesses/IERC3156FlashBorrowerHarness.sol \
certora/munged/token/ERC20/ERC20.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ certora/munged/token/ERC20/ERC20.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \
--verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--cloud \ --cloud \
--msg "ERC20FlashMint verification" \ --msg "ERC20FlashMint verification"
--send_only

3
certora/scripts/Round2/verifyERC20Votes.sh
View File

@ -1,11 +1,10 @@
certoraRun \ certoraRun \
certora/harnesses/ERC20VotesHarness.sol \ certora/harnesses/ERC20VotesHarness.sol \
--verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--cloud \ --cloud \
--send_only \
--msg "ERC20Votes $1" \ --msg "ERC20Votes $1" \
# --disableLocalTypeChecking \ # --disableLocalTypeChecking \

6
certora/scripts/Round2/verifyERC20Wrapper.sh
View File

@ -2,9 +2,7 @@ certoraRun \
certora/harnesses/ERC20WrapperHarness.sol \ certora/harnesses/ERC20WrapperHarness.sol \
certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \
--verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--cloud \ --cloud \
--msg "ERC20Wrapper verification" \ --msg "ERC20Wrapper verification"
--send_only

4
certora/scripts/Round2/verifyERC721Votes.sh
View File

@ -2,13 +2,11 @@ certoraRun \
certora/harnesses/ERC721VotesHarness.sol \ certora/harnesses/ERC721VotesHarness.sol \
certora/munged/utils/Checkpoints.sol \ certora/munged/utils/Checkpoints.sol \
--verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \
--solc solc8.2 \ --solc solc \
--disableLocalTypeChecking \ --disableLocalTypeChecking \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--cloud \ --cloud \
--send_only \
--msg "ERC721Votes" --msg "ERC721Votes"
# --staging "alex/new-dt-hashing-alpha" \ # --staging "alex/new-dt-hashing-alpha" \

6
certora/scripts/Round2/verifyTimelock.sh
View File

@ -1,13 +1,11 @@
certoraRun \ certoraRun \
certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \ certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \
--verify TimelockControllerHarness:certora/specs/TimelockController.spec \ --verify TimelockControllerHarness:certora/specs/TimelockController.spec \
--solc solc8.2 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--loop_iter 3 \ --loop_iter 3 \
--cloud \ --cloud \
--settings -byteMapHashingPrecision=32 \ --settings -byteMapHashingPrecision=32 \
--msg "TimelockController verification" \ --msg "TimelockController verification"
--send_only \
# --staging alex/new-dt-hashing-alpha \ # --staging alex/new-dt-hashing-alpha \

4
certora/scripts/Round3/round3.sh
View File

@ -1,4 +0,0 @@
for script in ./certora/scripts/Round3/verify*.sh
do
sh $script
done

3
certora/scripts/Round3/verifyERC1155Burnable.sh
View File

@ -1,8 +1,7 @@
certoraRun \ certoraRun \
certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
--verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
--solc solc8.4 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--loop_iter 3 \ --loop_iter 3 \
--msg "ERC1155 Burnable verification all rules" --msg "ERC1155 Burnable verification all rules"

2
certora/scripts/Round3/verifyERC1155Pausable.sh
View File

@ -1,7 +1,7 @@
certoraRun \ certoraRun \
certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
--verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
--solc solc8.4 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--loop_iter 3 \ --loop_iter 3 \
--msg "ERC1155 Pausable verification all rules" --msg "ERC1155 Pausable verification all rules"

2
certora/scripts/Round3/verifyERC1155Supply.sh
View File

@ -1,7 +1,7 @@
certoraRun \ certoraRun \
certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
--verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
--solc solc8.4 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--loop_iter 3 \ --loop_iter 3 \
--msg "ERC1155 Supply verification all rules" --msg "ERC1155 Supply verification all rules"

5
certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh
View File

@ -1,10 +1,7 @@
certoraRun \ certoraRun \
certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
--verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
--solc solc8.4 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--loop_iter 1 \ --loop_iter 1 \
--msg "GovernorPreventLateQuorum verification all rules" \ --msg "GovernorPreventLateQuorum verification all rules" \

5
certora/scripts/Round3/verifyInitializable.sh
View File

@ -1,10 +1,7 @@
certoraRun \ certoraRun \
certora/harnesses/InitializableComplexHarness.sol \ certora/harnesses/InitializableComplexHarness.sol \
--verify InitializableComplexHarness:certora/specs/Initializable.spec \ --verify InitializableComplexHarness:certora/specs/Initializable.spec \
--solc solc8.4 \ --solc solc \
--optimistic_loop \ --optimistic_loop \
--loop_iter 3 \ --loop_iter 3 \
--msg "Initializable verificaiton all rules on complex harness" \ --msg "Initializable verificaiton all rules on complex harness" \