diff --git a/certora/specs/ERC1155Supply.spec b/certora/specs/ERC1155Supply.spec index 4ca61f4a2..d624201a0 100644 --- a/certora/specs/ERC1155Supply.spec +++ b/certora/specs/ERC1155Supply.spec @@ -115,6 +115,22 @@ rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence { "Transferring multiple tokens via safeTransferFrom or safeBatchTransferFrom must be equivalent"; } +/// If transfer methods do not revert, the input arrays must be the same length. +rule transfersHaveSameLengthInputArrays { + env e; + + address holder; address recipient; bytes data; + uint256[] tokens; uint256[] transferAmounts; + + safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data); + + uint256 tokensLength = tokens.length; + uint256 transferAmountsLength = transferAmounts.length; + + assert tokens.length == transferAmounts.length, + "If transfer methods do not revert, the input arrays must be the same length"; +} + /* /// If passed empty token and burn amount arrays, burnBatch must not change @@ -144,6 +160,8 @@ rule burnBatchOnEmptyArraysChangesNothing { */ +/// TODO + /******************************************************************************/ ghost mapping(uint256 => mathint) sumOfBalances {