Changed rule onlyHolderOrApprovedCanReduceBalance to include filtered block

certora/specs/ERC1155Burnable.spec

@@ -5,14 +5,20 @@ methods {
 
 /// If a method call reduces account balances, the caller must be either the 
 /// holder of the account or approved to act on the holder's behalf.
-/// n.b. This rule is passing for all methods except `_burn` and `_burnBatch`, 
+/// n.b. This rule was passing for all methods except `_burn` and `_burnBatch`, 
 /// ordinarily internal methods that are callable by our tool only because they 
-/// were changed to public for the purposes of verification.
-rule onlyHolderOrApprovedCanReduceBalance {
+/// were changed to public for the purposes of prior verification. Filtered here
+/// since they are not generally callable.
+rule onlyHolderOrApprovedCanReduceBalance(method f) 
+filtered {
+    f -> f.selector != _burn(address,uint256,uint256).selector
+      && f.selector != _burnBatch(address,uint256[],uint256[]).selector
+}
+{
     address holder; uint256 token; uint256 amount;
     uint256 balanceBefore = balanceOf(holder, token);
 
-    method f; env e; calldataarg args;
+    env e; calldataarg args;
     f(e, args);
 
     uint256 balanceAfter = balanceOf(holder, token);
@@ -46,9 +52,10 @@ rule burnAmountProportionalToBalanceReduction {
         "A larger burn must lead to a larger decrease in balance";
 }
 
-/// Two sequential burns must be equivalent to a single burn of the sum of their
+/// @decription Two sequential burns must be equivalent to a single burn of the sum of their
 /// amounts.
-/// n.b. This rule holds for `burnBatch` as well due to rules establishing 
+/// @formula <pseudocode math description 
+/// @nota_bene This rule holds for `burnBatch` as well due to rules establishing 
 /// appropriate equivance between `burn` and `burnBatch` methods.
 rule sequentialBurnsEquivalentToSingleBurnOfSum {
     storage beforeBurns = lastStorage;
@@ -99,7 +106,7 @@ rule singleTokenBurnBurnBatchEquivalence {
         "Burning a single token via burn or burnBatch must be equivalent";
 }   
 
-/// The results of burning multiple tokens must be equivalent whether done 
+/// @description The results of burning multiple tokens must be equivalent whether done 
 /// separately via burn or together via burnBatch.
 rule multipleTokenBurnBurnBatchEquivalence {
     storage beforeBurns = lastStorage;