From bdb49654c5720966ec3272588f5794efa43a71ed Mon Sep 17 00:00:00 2001 From: Thomas Adams Date: Fri, 3 Jun 2022 12:27:08 -0700 Subject: [PATCH] Deleted redundant rule burnBatchAmountProportionalToBalanceReduction --- certora/specs/ERC1155Burnable.spec | 30 ------------------------------ 1 file changed, 30 deletions(-) diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec index 9e54d60c9..0408cf00f 100644 --- a/certora/specs/ERC1155Burnable.spec +++ b/certora/specs/ERC1155Burnable.spec @@ -46,36 +46,6 @@ rule burnAmountProportionalToBalanceReduction { "A larger burn must lead to a larger decrease in balance"; } -/// This rule not needed (because multipleTokenBurnBurnBatchEquivalence) -/// Unimplemented rule to verify monotonicity of burnBatch. -/// Using only burnBatch, possible approach: -/// Token with smaller and larger burn amounts -/// Round one smaller burn -/// Round two larger burn -rule burnBatchAmountProportionalToBalanceReduction { // TODO implement rule or remove - storage beforeBurn = lastStorage; - env e; - - address holder; uint256 token; - mathint startingBalance = balanceOf(holder, token); - uint256 smallBurn; uint256 largeBurn; - require smallBurn < largeBurn; - uint256[] tokens; uint256[] smallBurnAmounts; uint256[] largeBurnAmounts; - require tokens.length == 1; require smallBurnAmounts.length == 1; require largeBurnAmounts.length == 1; - require tokens[0] == token; require smallBurnAmounts[0] == smallBurn; require largeBurnAmounts[0] == largeBurn; - - // smaller burn amount - burnBatch(e, holder, tokens, smallBurnAmounts) at beforeBurn; - mathint smallBurnBalanceChange = startingBalance - balanceOf(holder, token); - - // larger burn amount - burnBatch(e, holder, tokens, largeBurnAmounts) at beforeBurn; - mathint largeBurnBalanceChange = startingBalance - balanceOf(holder, token); - - assert smallBurnBalanceChange < largeBurnBalanceChange, - "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 /// amounts. /// n.b. This rule holds for `burnBatch` as well due to rules establishing