From bd3427d5ffd588d5803c09ecb7de1e502cb9a34d Mon Sep 17 00:00:00 2001
From: Thomas Adams <thomas.harlan.adams@gmail.com>
Date: Tue, 31 May 2022 13:56:04 -0700
Subject: [PATCH] Included rule burnAmountProportionalToBalanceReduction
 (passing)

---
 certora/specs/ERC1155Burnable.spec | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec
index 059dae2a8..dcc792361 100644
--- a/certora/specs/ERC1155Burnable.spec
+++ b/certora/specs/ERC1155Burnable.spec
@@ -18,6 +18,29 @@ rule onlyHolderOrApprovedCanReduceBalance {
         "An account balance may only be reduced by the holder or a holder-approved agent";
 }
 
+/// Burning a larger amount of a token must reduce that token's balance more 
+/// than burning a smaller amount.
+rule burnAmountProportionalToBalanceReduction {
+    storage beforeBurn = lastStorage;
+    env e;
+    
+    address holder; uint256 token;
+    mathint startingBalance = balanceOf(holder, token); // 10
+    uint256 smallBurn; uint256 largeBurn; // 4, 7
+    require smallBurn < largeBurn;
+
+    // smaller burn amount
+    burn(e, holder, token, smallBurn) at beforeBurn;
+    mathint smallBurnBalanceChange = startingBalance - balanceOf(holder, token); // 4
+
+    // larger burn amount
+    burn(e, holder, token, largeBurn) at beforeBurn;
+    mathint largeBurnBalanceChange = startingBalance - balanceOf(holder, token); // 7
+
+    assert smallBurnBalanceChange < largeBurnBalanceChange, 
+        "A larger burn must lead to a larger decrease in balance";
+}
+
 /// This rule should always fail.
 rule sanity {
     method f; env e; calldataarg args;