diff --git a/certora/harnesses/ERC1155/ERC1155PausableHarness.sol b/certora/harnesses/ERC1155/ERC1155PausableHarness.sol index 23675091d..134a78748 100644 --- a/certora/harnesses/ERC1155/ERC1155PausableHarness.sol +++ b/certora/harnesses/ERC1155/ERC1155PausableHarness.sol @@ -1,6 +1,22 @@ -import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol" +import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol"; contract ERC1155PausableHarness is ERC1155Pausable { + constructor(string memory uri_) + ERC1155(uri_) + {} + function pause() public { + _pause(); + } + + function unpause() public { + _unpause(); + } + + function onlyWhenPausedMethod() public whenPaused { + } + + function onlyWhenNotPausedMethod() public whenNotPaused { + } } diff --git a/certora/scripts/verifyERC1155Pausable.sh b/certora/scripts/verifyERC1155Pausable.sh index e1af9c3d0..fe7d1a024 100755 --- a/certora/scripts/verifyERC1155Pausable.sh +++ b/certora/scripts/verifyERC1155Pausable.sh @@ -1,5 +1,5 @@ certoraRun \ - certora/harness/ERC1155/ERC1155PausableHarness.sol \ + certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ --solc solc8.2 \ --optimistic_loop \ diff --git a/certora/specs/ERC1155Pausable.spec b/certora/specs/ERC1155Pausable.spec new file mode 100644 index 000000000..70f738896 --- /dev/null +++ b/certora/specs/ERC1155Pausable.spec @@ -0,0 +1,9 @@ + +rule sanity { + method f; env e; calldataarg args; + + f(e, args); + + assert false; +} +