Removed reference to _burn and _mint

certora/specs/ERC1155Supply.spec

@@ -9,9 +9,7 @@ methods {
 /// totalSupply for other should not
 rule token_totalSupply_independence(method f)
 filtered {
-    f -> f.selector != _burnBatch(address,uint256[],uint256[]).selector
-      && f.selector != _mintBatch(address,uint256[],uint256[],bytes).selector
-      && f.selector != safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector
+    f -> f.selector != safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector
 }
 {
     uint256 token1; uint256 token2;
@@ -32,17 +30,112 @@ filtered {
 
 /// TODO possibly show equivalence between batch and non-batch methods
 /// in order to leverage non-batch rules wrt batch rules
-
+/*
+/// The result of transferring a single token must be equivalent whether done 
+/// via safeTransferFrom or safeBatchTransferFrom.
 rule singleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
-    assert false, 
-    "TODO implement this rule using burn version as structural model";
-}
+    storage beforeTransfer = lastStorage;
+    env e;
+
+    address holder; address recipient;
+    uint256 token; uint256 transferAmount; bytes data;
+    uint256[] tokens; uint256[] transferAmounts;
+
+/// safeTransferFrom(address,address,uint256,uint256,bytes)
+/// safeBatchTransferFrom(address,address,uint256[],uint256[],bytes)
+
+    mathint holderStartingBalance = balanceOf(holder, token);
+    mathint recipientStartingBalance = balanceOf(recipient, token);
+
+    require tokens.length == 1; require transferAmounts.length == 1;
+    require tokens[0] == token; require transferAmounts[0] == transferAmount;
+
+    // transferring via safeTransferFrom
+    safeTransferFrom(e, holder, recipient, token, transferAmount, data) at beforeTransfer;
+    mathint safeTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
+
+    // transferring via safeBatchTransferFrom
+    safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfer;
+    mathint safeBatchTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
+
+    assert safeTransferFromBalanceChange == safeBatchTransferFromBalanceChange, 
+        "Transferring a single token via safeTransferFrom or safeBatchTransferFrom must be equivalent";
+}   
 
 rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
     assert false, 
     "TODO implement this rule using burn version as structural model";
 }
 
+/*
+
+/// The results of burning multiple tokens must be equivalent whether done 
+/// separately via burn or together via burnBatch.
+rule multipleTokenBurnBurnBatchEquivalence {
+    storage beforeBurns = lastStorage;
+    env e;
+
+    address holder;
+    uint256 tokenA; uint256 tokenB; uint256 tokenC;
+    uint256 burnAmountA; uint256 burnAmountB; uint256 burnAmountC;
+    uint256[] tokens; uint256[] burnAmounts;
+
+    mathint startingBalanceA = balanceOf(holder, tokenA);
+    mathint startingBalanceB = balanceOf(holder, tokenB);
+    mathint startingBalanceC = balanceOf(holder, tokenC);
+
+    require tokens.length == 3; require burnAmounts.length == 3;
+    require tokens[0] == tokenA; require burnAmounts[0] == burnAmountA;
+    require tokens[1] == tokenB; require burnAmounts[1] == burnAmountB;
+    require tokens[2] == tokenC; require burnAmounts[2] == burnAmountC;
+
+    // burning via burn
+    burn(e, holder, tokenA, burnAmountA) at beforeBurns;
+    burn(e, holder, tokenB, burnAmountB);
+    burn(e, holder, tokenC, burnAmountC);
+    mathint burnBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA);
+    mathint burnBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB);
+    mathint burnBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC);
+
+    // burning via burnBatch
+    burnBatch(e, holder, tokens, burnAmounts) at beforeBurns;
+    mathint burnBatchBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA);
+    mathint burnBatchBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB);
+    mathint burnBatchBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC);
+
+    assert burnBalanceChangeA == burnBatchBalanceChangeA
+        && burnBalanceChangeB == burnBatchBalanceChangeB
+        && burnBalanceChangeC == burnBatchBalanceChangeC, 
+        "Burning multiple tokens via burn or burnBatch must be equivalent";
+}
+
+/// If passed empty token and burn amount arrays, burnBatch must not change 
+/// token balances or address permissions.
+rule burnBatchOnEmptyArraysChangesNothing {
+    env e;
+
+    address holder; uint256 token;
+    address nonHolderA; address nonHolderB;
+    uint256 startingBalance = balanceOf(holder, token);
+    bool startingPermissionNonHolderA = isApprovedForAll(holder, nonHolderA);
+    bool startingPermissionNonHolderB = isApprovedForAll(holder, nonHolderB);
+    uint256[] noTokens; uint256[] noBurnAmounts;
+    require noTokens.length == 0; require noBurnAmounts.length == 0;
+
+    burnBatch(e, holder, noTokens, noBurnAmounts);
+    uint256 endingBalance = balanceOf(holder, token);
+    bool endingPermissionNonHolderA = isApprovedForAll(holder, nonHolderA);
+    bool endingPermissionNonHolderB = isApprovedForAll(holder, nonHolderB);
+
+    assert startingBalance == endingBalance, 
+        "burnBatch must not change token balances if passed empty arrays";
+    assert startingPermissionNonHolderA == endingPermissionNonHolderA 
+        && startingPermissionNonHolderB == endingPermissionNonHolderB, 
+        "burnBatch must not change account permissions if passed empty arrays";
+}
+
+*/
+
 /******************************************************************************/
 
 ghost mapping(uint256 => mathint) sumOfBalances {