diff --git a/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol b/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol new file mode 100644 index 000000000..53b73dc6c --- /dev/null +++ b/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol @@ -0,0 +1,8 @@ +import "../../munged/token/ERC1155/extensions/ERC1155Supply.sol"; + +contract ERC1155SupplyHarness is ERC1155Supply { + constructor(string memory uri_) + ERC1155(uri_) + {} +} + diff --git a/certora/scripts/verifyERC1155Supply.sh b/certora/scripts/verifyERC1155Supply.sh new file mode 100755 index 000000000..dba264693 --- /dev/null +++ b/certora/scripts/verifyERC1155Supply.sh @@ -0,0 +1,8 @@ +certoraRun \ + certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ + --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 3 \ + --cloud \ + --msg "ERC1155 Supply verification" diff --git a/certora/specs/ERC1155Supply.spec b/certora/specs/ERC1155Supply.spec new file mode 100644 index 000000000..70f738896 --- /dev/null +++ b/certora/specs/ERC1155Supply.spec @@ -0,0 +1,9 @@ + +rule sanity { + method f; env e; calldataarg args; + + f(e, args); + + assert false; +} +