diff --git a/certora/scripts/noCI/Round3/verifyERC1155Burnable.sh b/certora/scripts/noCI/Round3/verifyERC1155Burnable.sh deleted file mode 100644 index 5980967d2..000000000 --- a/certora/scripts/noCI/Round3/verifyERC1155Burnable.sh +++ /dev/null @@ -1,7 +0,0 @@ -certoraRun \ - certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ - --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ - --solc solc \ - --optimistic_loop \ - --loop_iter 3 \ - --msg "ERC1155 Burnable verification all rules" diff --git a/certora/scripts/noCI/Round3/verifyERC1155Pausable.sh b/certora/scripts/noCI/Round3/verifyERC1155Pausable.sh deleted file mode 100755 index 41472c51e..000000000 --- a/certora/scripts/noCI/Round3/verifyERC1155Pausable.sh +++ /dev/null @@ -1,7 +0,0 @@ -certoraRun \ - certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ - --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ - --solc solc \ - --optimistic_loop \ - --loop_iter 3 \ - --msg "ERC1155 Pausable verification all rules" diff --git a/certora/scripts/noCI/Round3/verifyERC1155Supply.sh b/certora/scripts/noCI/Round3/verifyERC1155Supply.sh deleted file mode 100755 index 91a866870..000000000 --- a/certora/scripts/noCI/Round3/verifyERC1155Supply.sh +++ /dev/null @@ -1,7 +0,0 @@ -certoraRun \ - certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ - --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ - --solc solc \ - --optimistic_loop \ - --loop_iter 3 \ - --msg "ERC1155 Supply verification all rules" diff --git a/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh b/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh index 663ce0121..720caf0aa 100644 --- a/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh @@ -1,7 +1,15 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ - certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + certora/harnesses/ERC20VotesHarness.sol \ + certora/harnesses/ERC721VotesHarness.sol \ + certora/munged/governance/TimelockController.sol \ + certora/harnesses/GovernorPreventLateQuorumHarness.sol \ --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ --solc solc \ --optimistic_loop \ --loop_iter 1 \ - --msg "GovernorPreventLateQuorum verification all rules" \ + --rule_sanity advanced \ + --msg "all sanity" \ diff --git a/certora/scripts/noCI/Round3/verifyInitializable.sh b/certora/scripts/noCI/Round3/verifyInitializable.sh deleted file mode 100644 index 3aa43ea8c..000000000 --- a/certora/scripts/noCI/Round3/verifyInitializable.sh +++ /dev/null @@ -1,7 +0,0 @@ -certoraRun \ - certora/harnesses/InitializableComplexHarness.sol \ - --verify InitializableComplexHarness:certora/specs/Initializable.spec \ - --solc solc \ - --optimistic_loop \ - --loop_iter 3 \ - --msg "Initializable verificaiton all rules on complex harness" \ diff --git a/certora/scripts/noCI/verifyERC1155All.sh b/certora/scripts/noCI/verifyERC1155All.sh deleted file mode 100644 index 26484e9dc..000000000 --- a/certora/scripts/noCI/verifyERC1155All.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/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 \ - --msg "ERC1155 verification all rules " \ No newline at end of file diff --git a/certora/scripts/noCI/verifyGovernorPreventLateQuorum.sh b/certora/scripts/noCI/verifyGovernorPreventLateQuorum.sh deleted file mode 100644 index 720caf0aa..000000000 --- a/certora/scripts/noCI/verifyGovernorPreventLateQuorum.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/usr/bin/env bash - -set -euxo pipefail - -certoraRun \ - certora/harnesses/ERC20VotesHarness.sol \ - certora/harnesses/ERC721VotesHarness.sol \ - certora/munged/governance/TimelockController.sol \ - certora/harnesses/GovernorPreventLateQuorumHarness.sol \ - --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ - --solc solc \ - --optimistic_loop \ - --loop_iter 1 \ - --rule_sanity advanced \ - --msg "all sanity" \ diff --git a/certora/scripts/noCI/Round2/verifyAccessControl.sh b/certora/scripts/passes/verifyAccessControl.sh similarity index 84% rename from certora/scripts/noCI/Round2/verifyAccessControl.sh rename to certora/scripts/passes/verifyAccessControl.sh index 312a4c22a..6353cfa72 100644 --- a/certora/scripts/noCI/Round2/verifyAccessControl.sh +++ b/certora/scripts/passes/verifyAccessControl.sh @@ -7,5 +7,4 @@ certoraRun \ --verify AccessControlHarness:certora/specs/AccessControl.spec \ --solc solc \ --optimistic_loop \ - --msg "AccessControl verification" \ $@ diff --git a/certora/scripts/noCI/Round2/verifyERC1155.sh b/certora/scripts/passes/verifyERC1155.sh similarity index 91% rename from certora/scripts/noCI/Round2/verifyERC1155.sh rename to certora/scripts/passes/verifyERC1155.sh index 3d336d3aa..7564598ac 100644 --- a/certora/scripts/noCI/Round2/verifyERC1155.sh +++ b/certora/scripts/passes/verifyERC1155.sh @@ -8,5 +8,4 @@ certoraRun \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --msg "ERC1155" \ $@ diff --git a/certora/scripts/noCI/verifyERC1155Burnable.sh b/certora/scripts/passes/verifyERC1155Burnable.sh similarity index 82% rename from certora/scripts/noCI/verifyERC1155Burnable.sh rename to certora/scripts/passes/verifyERC1155Burnable.sh index 73763aae4..e6556c3e5 100644 --- a/certora/scripts/noCI/verifyERC1155Burnable.sh +++ b/certora/scripts/passes/verifyERC1155Burnable.sh @@ -8,4 +8,4 @@ certoraRun \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --msg "ERC1155 Burnable verification all rules" + $@ diff --git a/certora/scripts/noCI/verifyERC1155Pausable.sh b/certora/scripts/passes/verifyERC1155Pausable.sh similarity index 82% rename from certora/scripts/noCI/verifyERC1155Pausable.sh rename to certora/scripts/passes/verifyERC1155Pausable.sh index 3870f979c..41f9ad763 100755 --- a/certora/scripts/noCI/verifyERC1155Pausable.sh +++ b/certora/scripts/passes/verifyERC1155Pausable.sh @@ -8,4 +8,4 @@ certoraRun \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --msg "ERC1155 Pausable verification all rules" + $@ diff --git a/certora/scripts/noCI/verifyERC1155Supply.sh b/certora/scripts/passes/verifyERC1155Supply.sh similarity index 82% rename from certora/scripts/noCI/verifyERC1155Supply.sh rename to certora/scripts/passes/verifyERC1155Supply.sh index 153963c4c..c23c94313 100755 --- a/certora/scripts/noCI/verifyERC1155Supply.sh +++ b/certora/scripts/passes/verifyERC1155Supply.sh @@ -8,4 +8,4 @@ certoraRun \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --msg "ERC1155 Supply verification all rules" + $@ diff --git a/certora/scripts/noCI/Round2/verifyERC721Votes.sh b/certora/scripts/passes/verifyERC721Votes.sh similarity index 92% rename from certora/scripts/noCI/Round2/verifyERC721Votes.sh rename to certora/scripts/passes/verifyERC721Votes.sh index 42724444e..6240cb1c3 100644 --- a/certora/scripts/noCI/Round2/verifyERC721Votes.sh +++ b/certora/scripts/passes/verifyERC721Votes.sh @@ -9,5 +9,4 @@ certoraRun \ --optimistic_loop \ --disableLocalTypeChecking \ --settings -copyLoopUnroll=4 \ - --msg "ERC721Votes" \ $@ diff --git a/certora/scripts/noCI/verifyInitializable.sh b/certora/scripts/passes/verifyInitializable.sh similarity index 80% rename from certora/scripts/noCI/verifyInitializable.sh rename to certora/scripts/passes/verifyInitializable.sh index 00358e18a..2e069d984 100644 --- a/certora/scripts/noCI/verifyInitializable.sh +++ b/certora/scripts/passes/verifyInitializable.sh @@ -8,5 +8,4 @@ certoraRun \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --rule_sanity advanced \ - --msg "all complex sanity" \ + $@ diff --git a/certora/scripts/noCI/Round2/verifyTimelock.sh b/certora/scripts/passes/verifyTimelock.sh similarity index 88% rename from certora/scripts/noCI/Round2/verifyTimelock.sh rename to certora/scripts/passes/verifyTimelock.sh index 14599a6a4..c515ec9b6 100644 --- a/certora/scripts/noCI/Round2/verifyTimelock.sh +++ b/certora/scripts/passes/verifyTimelock.sh @@ -9,5 +9,4 @@ certoraRun \ --optimistic_loop \ --loop_iter 3 \ --settings -byteMapHashingPrecision=32 \ - --msg "TimelockController verification" \ $@ diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 228771ae5..bc9cc8b13 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -1,4 +1,4 @@ -import "interfaces/erc20.spec" +import "erc20.spec" /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ diff --git a/certora/specs/interfaces/erc20.spec b/certora/specs/erc20.spec similarity index 100% rename from certora/specs/interfaces/erc20.spec rename to certora/specs/erc20.spec