diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 4fde4b0a5..dafed0e22 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -53,6 +53,12 @@ jobs: - old/verifyAccessControl.sh - old/verifyERC20Votes.sh "checking ERC20Votes.spec on ERC20Votes.sol" - old/verifyERC721Votes.sh "checking ERC721Votes.spec on draft-ERC721Votes.sol and Votes.sol" + - Round3/verifyERC1155Burnable.sh + - Round3/verifyERC1155Supply.sh + - Round3/verifyERC1155Pausable.sh + - Round3/verifyERC1155Initializable.sh + - Round3/verifyERC1155GovernorPreventLateQuorum.sh + diff --git a/certora/scripts/Round3/round3.sh b/certora/scripts/Round3/round3.sh new file mode 100644 index 000000000..f976e610c --- /dev/null +++ b/certora/scripts/Round3/round3.sh @@ -0,0 +1,4 @@ +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 new file mode 100644 index 000000000..0231296c7 --- /dev/null +++ b/certora/scripts/Round3/verifyERC1155Burnable.sh @@ -0,0 +1,8 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ + --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ + --solc solc8.2 \ + --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 new file mode 100755 index 000000000..0292037b6 --- /dev/null +++ b/certora/scripts/Round3/verifyERC1155Pausable.sh @@ -0,0 +1,7 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ + --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ + --solc solc8.2 \ + --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 new file mode 100755 index 000000000..4677e0694 --- /dev/null +++ b/certora/scripts/Round3/verifyERC1155Supply.sh @@ -0,0 +1,7 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ + --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ + --solc solc8.2 \ + --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 new file mode 100644 index 000000000..b99f0b8aa --- /dev/null +++ b/certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 1 \ + --msg "GovernorPreventLateQuorum verification all rules" \ + + + diff --git a/certora/scripts/Round3/verifyInitializable.sh b/certora/scripts/Round3/verifyInitializable.sh new file mode 100644 index 000000000..291f1757e --- /dev/null +++ b/certora/scripts/Round3/verifyInitializable.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/InitializableComplexHarness.sol \ + --verify InitializableComplexHarness:certora/specs/Initializable.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --msg "Initializable verificaiton all rules on complex harness" \ + + +