diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec index 23c036e81..e673507e3 100644 --- a/certora/specs/ERC1155Burnable.spec +++ b/certora/specs/ERC1155Burnable.spec @@ -5,15 +5,7 @@ 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 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 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); @@ -52,10 +44,9 @@ rule burnAmountProportionalToBalanceReduction { "A larger burn must lead to a larger decrease in balance"; } -/// @decription Two sequential burns must be equivalent to a single burn of the sum of their +/// Two sequential burns must be equivalent to a single burn of the sum of their /// amounts. -/// @formula