Added tester rule for only burn

certora/specs/ERC1155Burnable.spec

@@ -1,7 +1,28 @@
+methods {
+    balanceOf(address, uint256) returns uint256 envfree
+    isApprovedForAll(address,address) returns bool envfree
+}
+
+/// If a method call reduces account balances, the caller should be either the 
+/// owner of the account or approved by the owner to act on its behalf.
+rule onlyApprovedCanReduceBalance {
+    address holder; uint256 token; uint256 amount;
+    uint256 balanceBefore = balanceOf(holder, token);
+
+    env e;
+    burn(e, holder, token, amount); // TODO Replace burn with appropriate general function
+
+    uint256 balanceAfter = balanceOf(holder, token);
+
+    assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender);
+}
+
+/// This rule should always fail.
 rule sanity {
     method f; env e; calldataarg args;
 
     f(e, args);
 
-    assert false;
+    assert false, 
+        "This rule should always fail";
 }