diff --git a/certora/run.sh b/certora/run.sh deleted file mode 100644 index ec757145f..000000000 --- a/certora/run.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash - -for receipt in $(cat certora/matrix.json | jq -r ".[$1] | @base64") -do - FILE=$(echo $receipt | base64 --decode | jq -r '.file') - NAME=$(echo $receipt | base64 --decode | jq -r '.name') - SPEC=$(echo $receipt | base64 --decode | jq -r '.spec') - ARGS=$(echo $receipt | base64 --decode | jq -r '.args//""') - DISABLED=$(echo $receipt | base64 --decode | jq -r '.disabled//false') - - - echo "Running $SPEC on $FILE:$NAME ..." - if [[ $DISABLED == 'true' ]]; - then - echo "disabled" - else - certoraRun $FILE --verify $NAME:$SPEC --solc solc --optimistic_loop --loop_iter 3 $ARGS --cloud - fi -done - -# [00] ERC1155.spec -- pass -# [01] ERC1155Burnable.spec -- pass -# [02] ERC1155Pausable.spec -- pass -# [03] ERC1155Supply.spec -- pass -# [04] GovernorPreventLateQuorum.spec -- nope -# [05] Initializable.spec -- nope \ No newline at end of file diff --git a/certora/scripts/verifyERC1155All.sh b/certora/scripts/verifyERC1155All.sh index 865374543..baa0b5684 100644 --- a/certora/scripts/verifyERC1155All.sh +++ b/certora/scripts/verifyERC1155All.sh @@ -1,11 +1,8 @@ -make -C certora munged - certoraRun \ - certora/munged/token/ERC1155/ERC1155.sol \ - --verify ERC1155:certora/specs/ERC1155.spec \ - --solc solc8.2 \ + certora/harnesses/ERC1155/ERC1155Harness.sol \ + --verify ERC1155Harness:certora/specs/ERC1155.spec \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --cloud \ - --send_only \ --msg "ERC1155 verification all rules " \ No newline at end of file diff --git a/certora/scripts/verifyERC1155Burnable.sh b/certora/scripts/verifyERC1155Burnable.sh index da19cc9d7..275466a0a 100644 --- a/certora/scripts/verifyERC1155Burnable.sh +++ b/certora/scripts/verifyERC1155Burnable.sh @@ -1,12 +1,8 @@ -make -C certora munged - certoraRun \ certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --send_only \ --cloud \ --msg "ERC1155 Burnable verification all rules" - \ No newline at end of file diff --git a/certora/scripts/verifyERC1155BurnableSpecific.sh b/certora/scripts/verifyERC1155BurnableSpecific.sh index bc98a86d7..d43dc8fb0 100644 --- a/certora/scripts/verifyERC1155BurnableSpecific.sh +++ b/certora/scripts/verifyERC1155BurnableSpecific.sh @@ -1,13 +1,9 @@ -make -C certora munged - certoraRun \ certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --cloud \ - --send_only \ --rule $1 \ --msg "ERC1155 Burnable verification specific rule $1" - \ No newline at end of file diff --git a/certora/scripts/verifyERC1155Pausable.sh b/certora/scripts/verifyERC1155Pausable.sh index 2c41d9f54..0b99acc45 100755 --- a/certora/scripts/verifyERC1155Pausable.sh +++ b/certora/scripts/verifyERC1155Pausable.sh @@ -1,11 +1,8 @@ -make -C certora munged - certoraRun \ certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --send_only \ --cloud \ --msg "ERC1155 Pausable verification all rules" diff --git a/certora/scripts/verifyERC1155Specific.sh b/certora/scripts/verifyERC1155Specific.sh index 438d527ca..97b387710 100644 --- a/certora/scripts/verifyERC1155Specific.sh +++ b/certora/scripts/verifyERC1155Specific.sh @@ -1,13 +1,9 @@ -make -C certora munged - certoraRun \ certora/munged/token/ERC1155/ERC1155.sol \ --verify ERC1155:certora/specs/ERC1155.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --cloud \ - --send_only \ --rule $1 \ --msg "ERC1155 Burnable verification specific rule $1" - \ No newline at end of file diff --git a/certora/scripts/verifyERC1155Supply.sh b/certora/scripts/verifyERC1155Supply.sh index 09db4a55a..6008d615a 100755 --- a/certora/scripts/verifyERC1155Supply.sh +++ b/certora/scripts/verifyERC1155Supply.sh @@ -1,11 +1,8 @@ -make -C certora munged - certoraRun \ certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ - --solc solc8.2 \ + --solc solc \ --optimistic_loop \ --loop_iter 3 \ --cloud \ - --send_only \ --msg "ERC1155 Supply verification all rules" diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh index 4517d161d..363335e0e 100644 --- a/certora/scripts/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh @@ -3,10 +3,6 @@ certoraRun \ --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ --solc solc \ --optimistic_loop \ - --rule_sanity advanced \ - --send_only \ --loop_iter 1 \ + --rule_sanity advanced \ --msg "all sanity" \ - - - diff --git a/certora/scripts/verifyInitializable.sh b/certora/scripts/verifyInitializable.sh index f302a5c31..30a0e7436 100644 --- a/certora/scripts/verifyInitializable.sh +++ b/certora/scripts/verifyInitializable.sh @@ -3,10 +3,6 @@ certoraRun \ --verify InitializableComplexHarness:certora/specs/Initializable.spec \ --solc solc \ --optimistic_loop \ - --send_only \ - --rule_sanity advanced \ --loop_iter 3 \ + --rule_sanity advanced \ --msg "all complex sanity" \ - - -