From aafb14461be6d71d02afbe57a06457725595f9af Mon Sep 17 00:00:00 2001
From: Michael George <mdgeorge@cs.cornell.edu>
Date: Fri, 6 May 2022 14:12:32 -0400
Subject: [PATCH] made the spec run

---
 .../ERC1155/ERC1155PausableHarness.sol         | 18 +++++++++++++++++-
 certora/scripts/verifyERC1155Pausable.sh       |  2 +-
 certora/specs/ERC1155Pausable.spec             |  9 +++++++++
 3 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 certora/specs/ERC1155Pausable.spec

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;
+}
+