diff --git a/contracts/ERC1155/external/properties/ERC1155ExternalBasicProperties.sol b/contracts/ERC1155/external/properties/ERC1155ExternalBasicProperties.sol new file mode 100644 index 0000000..61ffaa6 --- /dev/null +++ b/contracts/ERC1155/external/properties/ERC1155ExternalBasicProperties.sol @@ -0,0 +1,504 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import {CryticERC1155ExternalTestBase} from "../util/ERC1155ExternalTestBase.sol"; +import "@openzeppelin/contracts/utils/Address.sol"; + +/** + * @title ERC1155 External Basic Properties + * @author Crytic (Trail of Bits) + * @notice Core invariant properties for ERC1155 multi-token implementations tested externally + * @dev Testing Mode: EXTERNAL + * @dev This contract contains fundamental properties that must hold for any correct ERC1155 + * implementation. These properties test the token through its external interface only, + * without inheriting from the implementation. This approach is useful for testing + * deployed contracts or implementations that cannot be easily inherited. + * + * Properties are organized into the following sections: + * - Balance Properties: Tests for balance queries and consistency + * - Transfer Properties: Tests for single and batch transfers + * - Approval Properties: Tests for operator approvals + * - Safety Properties: Tests for safe transfer receiver checks + * + * @custom:see https://eips.ethereum.org/EIPS/eip-1155 + */ +abstract contract CryticERC1155ExternalBasicProperties is + CryticERC1155ExternalTestBase +{ + using Address for address; + + //////////////////////////////////////////////////////////////// + // Balance Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Balance of Zero Address + * @notice The zero address should always have zero balance for all token IDs + * @dev Testing Mode: EXTERNAL + * @dev Invariant: balanceOf(address(0), id) == 0 for all id + * @dev The zero address is commonly used to represent non-existent or burned tokens. + * It should never hold any balance to prevent tokens from being lost permanently. + * @custom:property-id ERC1155-EXTERNAL-BALANCE-051 + * + * @param tokenId The token ID to check balance for + */ + function test_ERC1155external_zeroAddressBalance(uint256 tokenId) public { + assertEq( + token.balanceOf(address(0), tokenId), + 0, + "Zero address has non-zero balance" + ); + } + + /** + * @title Batch Balance Consistency + * @notice Batch balance queries must match individual balance queries + * @dev Testing Mode: EXTERNAL + * @dev Invariant: balanceOfBatch([addr1, addr2], [id1, id2]) == [balanceOf(addr1, id1), balanceOf(addr2, id2)] + * @dev This ensures that the batch balance query function returns consistent results + * with individual balance queries, which is critical for efficient multi-token operations. + * @custom:property-id ERC1155-EXTERNAL-BALANCE-052 + * + * @param tokenId Token ID to check balances for + */ + function test_ERC1155external_balanceOfBatchConsistency( + uint256 tokenId + ) public { + address[] memory accounts = new address[](3); + accounts[0] = USER1; + accounts[1] = USER2; + accounts[2] = USER3; + + uint256[] memory ids = new uint256[](3); + ids[0] = tokenId; + ids[1] = tokenId; + ids[2] = tokenId; + + uint256[] memory batchBalances = token.balanceOfBatch(accounts, ids); + + assertEq( + batchBalances[0], + token.balanceOf(USER1, tokenId), + "Batch balance mismatch for USER1" + ); + assertEq( + batchBalances[1], + token.balanceOf(USER2, tokenId), + "Batch balance mismatch for USER2" + ); + assertEq( + batchBalances[2], + token.balanceOf(USER3, tokenId), + "Batch balance mismatch for USER3" + ); + } + + //////////////////////////////////////////////////////////////// + // Transfer Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Transfer to Zero Address Should Revert + * @notice Transfers to the zero address must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: safeTransferFrom(from, address(0), id, amount, data) must revert + * @dev Preventing transfers to the zero address protects users from accidentally + * burning tokens by sending them to an address from which they cannot be recovered. + * @custom:property-id ERC1155-EXTERNAL-TRANSFER-051 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_transferToZeroAddress( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + token.safeTransferFrom( + address(this), + address(0), + tokenId, + transferAmount, + "" + ); + assertWithMsg(false, "Transfer to zero address should have reverted"); + } + + /** + * @title Transfer from Zero Address Should Revert + * @notice Transfers from the zero address must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: safeTransferFrom(address(0), to, id, amount, data) must revert + * @dev The zero address should never be able to initiate transfers as it represents + * non-existent or burned tokens. + * @custom:property-id ERC1155-EXTERNAL-TRANSFER-052 + * + * @param target The recipient address + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_transferFromZeroAddress( + address target, + uint256 tokenId, + uint256 amount + ) public { + require(target != address(0)); + token.safeTransferFrom(address(0), target, tokenId, amount, ""); + assertWithMsg(false, "Transfer from zero address should have reverted"); + } + + /** + * @title Transfer Updates Balances Correctly + * @notice Transfers must correctly update sender and receiver balances + * @dev Testing Mode: EXTERNAL + * @dev Invariant: After safeTransferFrom(A, B, id, amount): + * - balanceOf(A, id) decreases by amount + * - balanceOf(B, id) increases by amount + * @dev This fundamental property ensures conservation of tokens during transfers. + * @custom:property-id ERC1155-EXTERNAL-TRANSFER-053 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_transferUpdatesBalances( + uint256 tokenId, + uint256 amount + ) public { + uint256 senderBalance = token.balanceOf(address(this), tokenId); + uint256 receiverBalance = token.balanceOf(USER1, tokenId); + require(senderBalance > 0); + require(USER1 != address(this)); + uint256 transferAmount = amount % (senderBalance + 1); + + token.safeTransferFrom( + address(this), + USER1, + tokenId, + transferAmount, + "" + ); + + assertEq( + token.balanceOf(address(this), tokenId), + senderBalance - transferAmount, + "Sender balance not updated correctly" + ); + assertEq( + token.balanceOf(USER1, tokenId), + receiverBalance + transferAmount, + "Receiver balance not updated correctly" + ); + } + + /** + * @title Self Transfer Preserves Balance + * @notice Transferring tokens to oneself should not change balance + * @dev Testing Mode: EXTERNAL + * @dev Invariant: balanceOf(A, id) before == balanceOf(A, id) after safeTransferFrom(A, A, id, amount) + * @dev Self-transfers should be no-ops that don't break token accounting. + * @custom:property-id ERC1155-EXTERNAL-TRANSFER-054 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_selfTransfer( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + token.safeTransferFrom( + address(this), + address(this), + tokenId, + transferAmount, + "" + ); + + assertEq( + token.balanceOf(address(this), tokenId), + balance, + "Self transfer changed balance" + ); + } + + /** + * @title Batch Transfer Updates Balances Correctly + * @notice Batch transfers must correctly update all balances + * @dev Testing Mode: EXTERNAL + * @dev Invariant: safeBatchTransferFrom must update all sender and receiver balances atomically + * @dev Batch operations must maintain the same correctness guarantees as individual operations. + * @custom:property-id ERC1155-EXTERNAL-TRANSFER-055 + * + * @param tokenId1 First token ID to transfer + * @param tokenId2 Second token ID to transfer + * @param amount1 Amount of first token to transfer + * @param amount2 Amount of second token to transfer + */ + function test_ERC1155external_batchTransferUpdatesBalances( + uint256 tokenId1, + uint256 tokenId2, + uint256 amount1, + uint256 amount2 + ) public { + uint256 senderBalance1 = token.balanceOf(address(this), tokenId1); + uint256 senderBalance2 = token.balanceOf(address(this), tokenId2); + uint256 receiverBalance1 = token.balanceOf(USER1, tokenId1); + uint256 receiverBalance2 = token.balanceOf(USER1, tokenId2); + + require(senderBalance1 > 0 && senderBalance2 > 0); + require(USER1 != address(this)); + require(tokenId1 != tokenId2); + + uint256 transferAmount1 = amount1 % (senderBalance1 + 1); + uint256 transferAmount2 = amount2 % (senderBalance2 + 1); + + uint256[] memory ids = new uint256[](2); + ids[0] = tokenId1; + ids[1] = tokenId2; + + uint256[] memory amounts = new uint256[](2); + amounts[0] = transferAmount1; + amounts[1] = transferAmount2; + + token.safeBatchTransferFrom(address(this), USER1, ids, amounts, ""); + + assertEq( + token.balanceOf(address(this), tokenId1), + senderBalance1 - transferAmount1, + "Sender balance 1 not updated correctly" + ); + assertEq( + token.balanceOf(address(this), tokenId2), + senderBalance2 - transferAmount2, + "Sender balance 2 not updated correctly" + ); + assertEq( + token.balanceOf(USER1, tokenId1), + receiverBalance1 + transferAmount1, + "Receiver balance 1 not updated correctly" + ); + assertEq( + token.balanceOf(USER1, tokenId2), + receiverBalance2 + transferAmount2, + "Receiver balance 2 not updated correctly" + ); + } + + /** + * @title Batch Transfer Array Length Mismatch Should Revert + * @notice Batch transfer with mismatched array lengths must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: safeBatchTransferFrom must revert if ids.length != amounts.length + * @dev This prevents ambiguous batch operations and programming errors. + * @custom:property-id ERC1155-EXTERNAL-TRANSFER-056 + */ + function test_ERC1155external_batchTransferArrayLengthMismatch() public { + uint256[] memory ids = new uint256[](2); + ids[0] = 1; + ids[1] = 2; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = 10; + + token.safeBatchTransferFrom(address(this), USER1, ids, amounts, ""); + assertWithMsg( + false, + "Batch transfer with mismatched arrays should have reverted" + ); + } + + //////////////////////////////////////////////////////////////// + // Approval Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Set Approval for All + * @notice Setting operator approval should update approval status + * @dev Testing Mode: EXTERNAL + * @dev Invariant: After setApprovalForAll(operator, true), isApprovedForAll(sender, operator) == true + * @dev Operator approval allows efficient delegation of token management. + * @custom:property-id ERC1155-EXTERNAL-APPROVAL-051 + * + * @param operator The operator address to approve + */ + function test_ERC1155external_setApprovalForAll(address operator) public { + require(operator != address(0)); + require(operator != address(this)); + + token.setApprovalForAll(operator, true); + assertWithMsg( + token.isApprovedForAll(address(this), operator), + "Operator not approved after setApprovalForAll(true)" + ); + + token.setApprovalForAll(operator, false); + assertWithMsg( + !token.isApprovedForAll(address(this), operator), + "Operator still approved after setApprovalForAll(false)" + ); + } + + /** + * @title Non-Operator Cannot Transfer + * @notice Non-approved addresses must not be able to transfer tokens + * @dev Testing Mode: EXTERNAL + * @dev Invariant: If !isApprovedForAll(owner, operator) and operator != owner, + * then operator cannot call safeTransferFrom(owner, to, id, amount, data) + * @dev This ensures that only authorized parties can move tokens. + * @custom:property-id ERC1155-EXTERNAL-APPROVAL-052 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_nonOperatorCannotTransfer( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(address(this), tokenId); + require(balance > 0); + require(msg.sender != address(this)); + require(USER1 != address(this)); + uint256 transferAmount = amount % (balance + 1); + + // Ensure msg.sender is not an operator + token.setApprovalForAll(msg.sender, false); + require(!token.isApprovedForAll(address(this), msg.sender)); + + // msg.sender should NOT be able to transfer tokens from address(this) + hevm.prank(msg.sender); + token.safeTransferFrom( + address(this), + USER1, + tokenId, + transferAmount, + "" + ); + + assertWithMsg(false, "Non-operator transfer should have reverted"); + } + + //////////////////////////////////////////////////////////////// + // Safety Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Safe Transfer to Contract Without Receiver + * @notice Safe transfers to contracts not implementing the receiver interface must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: safeTransferFrom to a contract that doesn't implement + * onERC1155Received must revert + * @dev This protects against tokens being permanently locked in contracts. + * @custom:property-id ERC1155-EXTERNAL-SAFETY-051 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_safeTransferToNonReceiverContract( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + // unsafeReceiver returns wrong selector + token.safeTransferFrom( + address(this), + address(unsafeReceiver), + tokenId, + transferAmount, + "" + ); + + assertWithMsg( + false, + "Safe transfer to non-receiver contract should have reverted" + ); + } + + /** + * @title Safe Transfer to Valid Receiver + * @notice Safe transfers to contracts implementing the receiver interface must succeed + * @dev Testing Mode: EXTERNAL + * @dev Invariant: safeTransferFrom to a contract implementing onERC1155Received + * correctly should succeed + * @dev This ensures that properly implemented receiver contracts can accept tokens. + * @custom:property-id ERC1155-EXTERNAL-SAFETY-052 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_safeTransferToValidReceiver( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + uint256 receiverBalance = token.balanceOf( + address(safeReceiver), + tokenId + ); + + token.safeTransferFrom( + address(this), + address(safeReceiver), + tokenId, + transferAmount, + "" + ); + + assertEq( + token.balanceOf(address(safeReceiver), tokenId), + receiverBalance + transferAmount, + "Safe receiver did not receive tokens" + ); + } + + /** + * @title Safe Batch Transfer to Contract Without Receiver + * @notice Safe batch transfers to contracts not implementing the receiver interface must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: safeBatchTransferFrom to a contract that doesn't implement + * onERC1155BatchReceived must revert + * @dev This protects against tokens being permanently locked in contracts during batch operations. + * @custom:property-id ERC1155-EXTERNAL-SAFETY-053 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155external_safeBatchTransferToNonReceiverContract( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = transferAmount; + + token.safeBatchTransferFrom( + address(this), + address(unsafeReceiver), + ids, + amounts, + "" + ); + + assertWithMsg( + false, + "Safe batch transfer to non-receiver contract should have reverted" + ); + } +} diff --git a/contracts/ERC1155/external/properties/ERC1155ExternalBurnableProperties.sol b/contracts/ERC1155/external/properties/ERC1155ExternalBurnableProperties.sol new file mode 100644 index 0000000..9951814 --- /dev/null +++ b/contracts/ERC1155/external/properties/ERC1155ExternalBurnableProperties.sol @@ -0,0 +1,216 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import {CryticERC1155ExternalTestBase} from "../util/ERC1155ExternalTestBase.sol"; + +/** + * @title ERC1155 External Burnable Properties + * @author Crytic (Trail of Bits) + * @notice Invariant properties for ERC1155 tokens with burn functionality tested externally + * @dev Testing Mode: EXTERNAL + * @dev This contract contains properties that must hold for ERC1155 implementations + * with burn functionality. These properties test the token through its external + * interface only, ensuring that burning tokens correctly reduces balances and + * respects authorization requirements. + * + * Properties are organized into the following sections: + * - Burn Properties: Tests for single token burn operations + * - Batch Burn Properties: Tests for batch burn operations + * + * @custom:see https://eips.ethereum.org/EIPS/eip-1155 + */ +abstract contract CryticERC1155ExternalBurnableProperties is + CryticERC1155ExternalTestBase +{ + // Interface for burn functions - must be implemented by the external token + function burn(address account, uint256 id, uint256 amount) public virtual; + + function burnBatch( + address account, + uint256[] memory ids, + uint256[] memory amounts + ) public virtual; + + //////////////////////////////////////////////////////////////// + // Burn Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Burn Reduces Balance + * @notice Burning tokens must reduce the owner's balance by the burn amount + * @dev Testing Mode: EXTERNAL + * @dev Invariant: After burn(account, id, amount), balanceOf(account, id) decreases by amount + * @dev Burn operations must correctly update token balances to maintain accurate accounting. + * @custom:property-id ERC1155-EXTERNAL-BURN-051 + * + * @param tokenId The token ID to burn + * @param amount The amount to burn + */ + function test_ERC1155external_burnReducesBalance( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(address(this), tokenId); + require(balance > 0); + uint256 burnAmount = amount % (balance + 1); + + this.burn(address(this), tokenId, burnAmount); + + assertEq( + token.balanceOf(address(this), tokenId), + balance - burnAmount, + "Balance not reduced correctly after burn" + ); + } + + /** + * @title Burn from Another Account Requires Approval + * @notice Burning tokens from another account requires operator approval + * @dev Testing Mode: EXTERNAL + * @dev Invariant: If !isApprovedForAll(account, operator) and operator != account, + * then burn(account, id, amount) called by operator must revert + * @dev This prevents unauthorized token destruction. + * @custom:property-id ERC1155-EXTERNAL-BURN-052 + * + * @param tokenId The token ID to burn + * @param amount The amount to burn + */ + function test_ERC1155external_burnRequiresApproval( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(USER1, tokenId); + require(balance > 0); + require(msg.sender != USER1); + require(msg.sender != address(this)); + uint256 burnAmount = amount % (balance + 1); + + // Ensure msg.sender is not approved + hevm.prank(USER1); + token.setApprovalForAll(msg.sender, false); + require(!token.isApprovedForAll(USER1, msg.sender)); + + // msg.sender should NOT be able to burn USER1's tokens + hevm.prank(msg.sender); + this.burn(USER1, tokenId, burnAmount); + + assertWithMsg(false, "Burn without approval should have reverted"); + } + + //////////////////////////////////////////////////////////////// + // Batch Burn Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Batch Burn Reduces All Balances + * @notice Burning multiple tokens in a batch must reduce all balances correctly + * @dev Testing Mode: EXTERNAL + * @dev Invariant: After burnBatch(account, ids, amounts), all corresponding + * balances decrease by the specified amounts + * @dev Batch operations must maintain the same correctness as individual operations. + * @custom:property-id ERC1155-EXTERNAL-BURN-053 + * + * @param tokenId1 First token ID to burn + * @param tokenId2 Second token ID to burn + * @param amount1 Amount of first token to burn + * @param amount2 Amount of second token to burn + */ + function test_ERC1155external_batchBurnReducesBalances( + uint256 tokenId1, + uint256 tokenId2, + uint256 amount1, + uint256 amount2 + ) public { + uint256 balance1 = token.balanceOf(address(this), tokenId1); + uint256 balance2 = token.balanceOf(address(this), tokenId2); + require(balance1 > 0 && balance2 > 0); + require(tokenId1 != tokenId2); + + uint256 burnAmount1 = amount1 % (balance1 + 1); + uint256 burnAmount2 = amount2 % (balance2 + 1); + + uint256[] memory ids = new uint256[](2); + ids[0] = tokenId1; + ids[1] = tokenId2; + + uint256[] memory amounts = new uint256[](2); + amounts[0] = burnAmount1; + amounts[1] = burnAmount2; + + this.burnBatch(address(this), ids, amounts); + + assertEq( + token.balanceOf(address(this), tokenId1), + balance1 - burnAmount1, + "Balance 1 not reduced correctly after batch burn" + ); + assertEq( + token.balanceOf(address(this), tokenId2), + balance2 - burnAmount2, + "Balance 2 not reduced correctly after batch burn" + ); + } + + /** + * @title Batch Burn Array Length Mismatch Should Revert + * @notice Batch burn with mismatched array lengths must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: burnBatch must revert if ids.length != amounts.length + * @dev This prevents ambiguous batch operations and programming errors. + * @custom:property-id ERC1155-EXTERNAL-BURN-054 + */ + function test_ERC1155external_batchBurnArrayLengthMismatch() public { + uint256[] memory ids = new uint256[](2); + ids[0] = 1; + ids[1] = 2; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = 10; + + this.burnBatch(address(this), ids, amounts); + assertWithMsg( + false, + "Batch burn with mismatched arrays should have reverted" + ); + } + + /** + * @title Batch Burn Requires Approval + * @notice Batch burning tokens from another account requires operator approval + * @dev Testing Mode: EXTERNAL + * @dev Invariant: If !isApprovedForAll(account, operator) and operator != account, + * then burnBatch(account, ids, amounts) called by operator must revert + * @dev This ensures batch burn operations respect the same authorization rules. + * @custom:property-id ERC1155-EXTERNAL-BURN-055 + * + * @param tokenId The token ID to burn + * @param amount The amount to burn + */ + function test_ERC1155external_batchBurnRequiresApproval( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = token.balanceOf(USER1, tokenId); + require(balance > 0); + require(msg.sender != USER1); + require(msg.sender != address(this)); + uint256 burnAmount = amount % (balance + 1); + + // Ensure msg.sender is not approved + hevm.prank(USER1); + token.setApprovalForAll(msg.sender, false); + require(!token.isApprovedForAll(USER1, msg.sender)); + + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = burnAmount; + + // msg.sender should NOT be able to batch burn USER1's tokens + hevm.prank(msg.sender); + this.burnBatch(USER1, ids, amounts); + + assertWithMsg(false, "Batch burn without approval should have reverted"); + } +} diff --git a/contracts/ERC1155/external/properties/ERC1155ExternalMintableProperties.sol b/contracts/ERC1155/external/properties/ERC1155ExternalMintableProperties.sol new file mode 100644 index 0000000..75cb19c --- /dev/null +++ b/contracts/ERC1155/external/properties/ERC1155ExternalMintableProperties.sol @@ -0,0 +1,290 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import {CryticERC1155ExternalTestBase} from "../util/ERC1155ExternalTestBase.sol"; + +/** + * @title ERC1155 External Mintable Properties + * @author Crytic (Trail of Bits) + * @notice Invariant properties for ERC1155 tokens with mint functionality tested externally + * @dev Testing Mode: EXTERNAL + * @dev This contract contains properties that must hold for ERC1155 implementations + * with mint functionality. These properties test the token through its external + * interface only, ensuring that minting tokens correctly increases balances for + * both single and batch operations. + * + * Properties are organized into the following sections: + * - Mint Properties: Tests for single token mint operations + * - Batch Mint Properties: Tests for batch mint operations + * + * Note: The mint functions must be implemented by the inheriting contract as + * different implementations may have different access control or minting logic. + * + * @custom:see https://eips.ethereum.org/EIPS/eip-1155 + */ +abstract contract CryticERC1155ExternalMintableProperties is + CryticERC1155ExternalTestBase +{ + // Interface for mint functions - must be implemented by the inheriting contract + function mint( + address to, + uint256 id, + uint256 amount, + bytes memory data + ) public virtual; + + function mintBatch( + address to, + uint256[] memory ids, + uint256[] memory amounts, + bytes memory data + ) public virtual; + + //////////////////////////////////////////////////////////////// + // Mint Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Mint Increases Balance + * @notice Minting tokens must increase the recipient's balance by the mint amount + * @dev Testing Mode: EXTERNAL + * @dev Invariant: After mint(to, id, amount, data), balanceOf(to, id) increases by amount + * @dev Mint operations must correctly update token balances to maintain accurate accounting. + * @custom:property-id ERC1155-EXTERNAL-MINT-051 + * + * @param target The address to mint tokens to + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155external_mintIncreasesBalance( + address target, + uint256 tokenId, + uint256 amount + ) public { + require(target != address(0)); + uint256 balance = token.balanceOf(target, tokenId); + + this.mint(target, tokenId, amount, ""); + + assertEq( + token.balanceOf(target, tokenId), + balance + amount, + "Balance not increased correctly after mint" + ); + } + + /** + * @title Mint to Zero Address Should Revert + * @notice Minting tokens to the zero address must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: mint(address(0), id, amount, data) must revert + * @dev Minting to the zero address would effectively burn tokens at creation, + * which is inconsistent and should be prevented. + * @custom:property-id ERC1155-EXTERNAL-MINT-052 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155external_mintToZeroAddress( + uint256 tokenId, + uint256 amount + ) public { + this.mint(address(0), tokenId, amount, ""); + assertWithMsg(false, "Mint to zero address should have reverted"); + } + + /** + * @title Mint Respects Safe Transfer Check + * @notice Minting to a contract must respect the receiver interface check + * @dev Testing Mode: EXTERNAL + * @dev Invariant: If recipient is a contract, mint must call onERC1155Received + * and revert if the contract doesn't return the correct selector + * @dev This protects against tokens being locked in contracts that can't handle them. + * @custom:property-id ERC1155-EXTERNAL-MINT-053 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155external_mintToNonReceiverContract( + uint256 tokenId, + uint256 amount + ) public { + require(amount > 0); + + // unsafeReceiver returns wrong selector + this.mint(address(unsafeReceiver), tokenId, amount, ""); + + assertWithMsg(false, "Mint to non-receiver contract should have reverted"); + } + + /** + * @title Mint to Valid Receiver Succeeds + * @notice Minting to a contract implementing the receiver interface must succeed + * @dev Testing Mode: EXTERNAL + * @dev Invariant: mint to a contract implementing onERC1155Received correctly should succeed + * @dev This ensures that properly implemented receiver contracts can receive minted tokens. + * @custom:property-id ERC1155-EXTERNAL-MINT-054 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155external_mintToValidReceiver( + uint256 tokenId, + uint256 amount + ) public { + require(amount > 0); + uint256 receiverBalance = token.balanceOf( + address(safeReceiver), + tokenId + ); + + this.mint(address(safeReceiver), tokenId, amount, ""); + + assertEq( + token.balanceOf(address(safeReceiver), tokenId), + receiverBalance + amount, + "Safe receiver did not receive minted tokens" + ); + } + + //////////////////////////////////////////////////////////////// + // Batch Mint Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Batch Mint Increases All Balances + * @notice Minting multiple tokens in a batch must increase all balances correctly + * @dev Testing Mode: EXTERNAL + * @dev Invariant: After mintBatch(to, ids, amounts, data), all corresponding + * balances increase by the specified amounts + * @dev Batch operations must maintain the same correctness as individual operations. + * @custom:property-id ERC1155-EXTERNAL-MINT-055 + * + * @param target The address to mint tokens to + * @param tokenId1 First token ID to mint + * @param tokenId2 Second token ID to mint + * @param amount1 Amount of first token to mint + * @param amount2 Amount of second token to mint + */ + function test_ERC1155external_batchMintIncreasesBalances( + address target, + uint256 tokenId1, + uint256 tokenId2, + uint256 amount1, + uint256 amount2 + ) public { + require(target != address(0)); + require(tokenId1 != tokenId2); + + uint256 balance1 = token.balanceOf(target, tokenId1); + uint256 balance2 = token.balanceOf(target, tokenId2); + + uint256[] memory ids = new uint256[](2); + ids[0] = tokenId1; + ids[1] = tokenId2; + + uint256[] memory amounts = new uint256[](2); + amounts[0] = amount1; + amounts[1] = amount2; + + this.mintBatch(target, ids, amounts, ""); + + assertEq( + token.balanceOf(target, tokenId1), + balance1 + amount1, + "Balance 1 not increased correctly after batch mint" + ); + assertEq( + token.balanceOf(target, tokenId2), + balance2 + amount2, + "Balance 2 not increased correctly after batch mint" + ); + } + + /** + * @title Batch Mint Array Length Mismatch Should Revert + * @notice Batch mint with mismatched array lengths must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: mintBatch must revert if ids.length != amounts.length + * @dev This prevents ambiguous batch operations and programming errors. + * @custom:property-id ERC1155-EXTERNAL-MINT-056 + * + * @param target The address to mint tokens to + */ + function test_ERC1155external_batchMintArrayLengthMismatch( + address target + ) public { + require(target != address(0)); + + uint256[] memory ids = new uint256[](2); + ids[0] = 1; + ids[1] = 2; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = 10; + + this.mintBatch(target, ids, amounts, ""); + assertWithMsg( + false, + "Batch mint with mismatched arrays should have reverted" + ); + } + + /** + * @title Batch Mint to Zero Address Should Revert + * @notice Batch minting tokens to the zero address must revert + * @dev Testing Mode: EXTERNAL + * @dev Invariant: mintBatch(address(0), ids, amounts, data) must revert + * @dev This maintains consistency with single mint operations. + * @custom:property-id ERC1155-EXTERNAL-MINT-057 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155external_batchMintToZeroAddress( + uint256 tokenId, + uint256 amount + ) public { + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = amount; + + this.mintBatch(address(0), ids, amounts, ""); + assertWithMsg(false, "Batch mint to zero address should have reverted"); + } + + /** + * @title Batch Mint Respects Safe Transfer Check + * @notice Batch minting to a contract must respect the receiver interface check + * @dev Testing Mode: EXTERNAL + * @dev Invariant: If recipient is a contract, mintBatch must call onERC1155BatchReceived + * and revert if the contract doesn't return the correct selector + * @dev This protects against tokens being locked in contracts during batch operations. + * @custom:property-id ERC1155-EXTERNAL-MINT-058 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155external_batchMintToNonReceiverContract( + uint256 tokenId, + uint256 amount + ) public { + require(amount > 0); + + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = amount; + + // unsafeReceiver returns wrong selector + this.mintBatch(address(unsafeReceiver), ids, amounts, ""); + + assertWithMsg( + false, + "Batch mint to non-receiver contract should have reverted" + ); + } +} diff --git a/contracts/ERC1155/external/util/ERC1155ExternalTestBase.sol b/contracts/ERC1155/external/util/ERC1155ExternalTestBase.sol new file mode 100644 index 0000000..63ac545 --- /dev/null +++ b/contracts/ERC1155/external/util/ERC1155ExternalTestBase.sol @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../../../util/PropertiesConstants.sol"; +import "../../../util/PropertiesAsserts.sol"; +import "../../util/IERC1155Internal.sol"; +import {MockReceiver1155} from "../../internal/util/MockReceiver1155.sol"; + +abstract contract CryticERC1155ExternalTestBase is PropertiesAsserts, PropertiesConstants { + IERC1155Internal internal token; + MockReceiver1155 safeReceiver; + MockReceiver1155 unsafeReceiver; + + constructor() { + safeReceiver = new MockReceiver1155(true); + unsafeReceiver = new MockReceiver1155(false); + } +} diff --git a/contracts/ERC1155/internal/properties/ERC1155BasicProperties.sol b/contracts/ERC1155/internal/properties/ERC1155BasicProperties.sol new file mode 100644 index 0000000..4bd3614 --- /dev/null +++ b/contracts/ERC1155/internal/properties/ERC1155BasicProperties.sol @@ -0,0 +1,516 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../util/ERC1155TestBase.sol"; +import "@openzeppelin/contracts/utils/Address.sol"; + +/** + * @title ERC1155 Basic Properties + * @author Crytic (Trail of Bits) + * @notice Core invariant properties for ERC1155 multi-token implementations + * @dev Testing Mode: INTERNAL + * @dev This contract contains fundamental properties that must hold for any correct ERC1155 + * implementation. These properties test balance tracking, transfer operations, operator + * approvals, batch operations, and safe transfer callbacks. The test contract inherits + * from both the token implementation and this property contract, allowing direct access + * to internal state. + * + * Properties are organized into the following sections: + * - Balance Properties: Tests for balance queries and consistency + * - Transfer Properties: Tests for single and batch transfers + * - Approval Properties: Tests for operator approvals + * - Safety Properties: Tests for safe transfer receiver checks + * + * @custom:see https://eips.ethereum.org/EIPS/eip-1155 + */ +abstract contract CryticERC1155BasicProperties is CryticERC1155TestBase { + using Address for address; + + //////////////////////////////////////////////////////////////// + // Balance Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Balance of Zero Address + * @notice The zero address should always have zero balance for all token IDs + * @dev Testing Mode: INTERNAL + * @dev Invariant: balanceOf(address(0), id) == 0 for all id + * @dev The zero address is commonly used to represent non-existent or burned tokens. + * It should never hold any balance to prevent tokens from being lost permanently. + * @custom:property-id ERC1155-BALANCE-001 + * + * @param tokenId The token ID to check balance for + */ + function test_ERC1155_zeroAddressBalance(uint256 tokenId) public { + assertEq( + balanceOf(address(0), tokenId), + 0, + "Zero address has non-zero balance" + ); + } + + /** + * @title Batch Balance Consistency + * @notice Batch balance queries must match individual balance queries + * @dev Testing Mode: INTERNAL + * @dev Invariant: balanceOfBatch([addr1, addr2], [id1, id2]) == [balanceOf(addr1, id1), balanceOf(addr2, id2)] + * @dev This ensures that the batch balance query function returns consistent results + * with individual balance queries, which is critical for efficient multi-token operations. + * @custom:property-id ERC1155-BALANCE-002 + * + * @param tokenId Token ID to check balances for + */ + function test_ERC1155_balanceOfBatchConsistency(uint256 tokenId) public { + address[] memory accounts = new address[](3); + accounts[0] = USER1; + accounts[1] = USER2; + accounts[2] = USER3; + + uint256[] memory ids = new uint256[](3); + ids[0] = tokenId; + ids[1] = tokenId; + ids[2] = tokenId; + + uint256[] memory batchBalances = balanceOfBatch(accounts, ids); + + assertEq( + batchBalances[0], + balanceOf(USER1, tokenId), + "Batch balance mismatch for USER1" + ); + assertEq( + batchBalances[1], + balanceOf(USER2, tokenId), + "Batch balance mismatch for USER2" + ); + assertEq( + batchBalances[2], + balanceOf(USER3, tokenId), + "Batch balance mismatch for USER3" + ); + } + + //////////////////////////////////////////////////////////////// + // Transfer Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Transfer to Zero Address Should Revert + * @notice Transfers to the zero address must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: safeTransferFrom(from, address(0), id, amount, data) must revert + * @dev Preventing transfers to the zero address protects users from accidentally + * burning tokens by sending them to an address from which they cannot be recovered. + * @custom:property-id ERC1155-TRANSFER-001 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_transferToZeroAddress(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + safeTransferFrom(address(this), address(0), tokenId, transferAmount, ""); + assertWithMsg(false, "Transfer to zero address should have reverted"); + } + + /** + * @title Transfer from Zero Address Should Revert + * @notice Transfers from the zero address must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: safeTransferFrom(address(0), to, id, amount, data) must revert + * @dev The zero address should never be able to initiate transfers as it represents + * non-existent or burned tokens. + * @custom:property-id ERC1155-TRANSFER-002 + * + * @param target The recipient address + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_transferFromZeroAddress( + address target, + uint256 tokenId, + uint256 amount + ) public { + require(target != address(0)); + safeTransferFrom(address(0), target, tokenId, amount, ""); + assertWithMsg(false, "Transfer from zero address should have reverted"); + } + + /** + * @title Transfer Updates Balances Correctly + * @notice Transfers must correctly update sender and receiver balances + * @dev Testing Mode: INTERNAL + * @dev Invariant: After safeTransferFrom(A, B, id, amount): + * - balanceOf(A, id) decreases by amount + * - balanceOf(B, id) increases by amount + * @dev This fundamental property ensures conservation of tokens during transfers. + * @custom:property-id ERC1155-TRANSFER-003 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_transferUpdatesBalances(uint256 tokenId, uint256 amount) public { + uint256 senderBalance = balanceOf(address(this), tokenId); + uint256 receiverBalance = balanceOf(USER1, tokenId); + require(senderBalance > 0); + require(USER1 != address(this)); + uint256 transferAmount = amount % (senderBalance + 1); + + this.safeTransferFrom(address(this), USER1, tokenId, transferAmount, ""); + + assertEq( + balanceOf(address(this), tokenId), + senderBalance - transferAmount, + "Sender balance not updated correctly" + ); + assertEq( + balanceOf(USER1, tokenId), + receiverBalance + transferAmount, + "Receiver balance not updated correctly" + ); + } + + /** + * @title Self Transfer Preserves Balance + * @notice Transferring tokens to oneself should not change balance + * @dev Testing Mode: INTERNAL + * @dev Invariant: balanceOf(A, id) before == balanceOf(A, id) after safeTransferFrom(A, A, id, amount) + * @dev Self-transfers should be no-ops that don't break token accounting. + * @custom:property-id ERC1155-TRANSFER-004 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_selfTransfer(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + this.safeTransferFrom(address(this), address(this), tokenId, transferAmount, ""); + + assertEq( + balanceOf(address(this), tokenId), + balance, + "Self transfer changed balance" + ); + } + + /** + * @title Batch Transfer Updates Balances Correctly + * @notice Batch transfers must correctly update all balances + * @dev Testing Mode: INTERNAL + * @dev Invariant: safeBatchTransferFrom must update all sender and receiver balances atomically + * @dev Batch operations must maintain the same correctness guarantees as individual operations. + * @custom:property-id ERC1155-TRANSFER-005 + * + * @param tokenId1 First token ID to transfer + * @param tokenId2 Second token ID to transfer + * @param amount1 Amount of first token to transfer + * @param amount2 Amount of second token to transfer + */ + function test_ERC1155_batchTransferUpdatesBalances( + uint256 tokenId1, + uint256 tokenId2, + uint256 amount1, + uint256 amount2 + ) public { + uint256 senderBalance1 = balanceOf(address(this), tokenId1); + uint256 senderBalance2 = balanceOf(address(this), tokenId2); + uint256 receiverBalance1 = balanceOf(USER1, tokenId1); + uint256 receiverBalance2 = balanceOf(USER1, tokenId2); + + require(senderBalance1 > 0 && senderBalance2 > 0); + require(USER1 != address(this)); + require(tokenId1 != tokenId2); + + uint256 transferAmount1 = amount1 % (senderBalance1 + 1); + uint256 transferAmount2 = amount2 % (senderBalance2 + 1); + + uint256[] memory ids = new uint256[](2); + ids[0] = tokenId1; + ids[1] = tokenId2; + + uint256[] memory amounts = new uint256[](2); + amounts[0] = transferAmount1; + amounts[1] = transferAmount2; + + this.safeBatchTransferFrom(address(this), USER1, ids, amounts, ""); + + assertEq( + balanceOf(address(this), tokenId1), + senderBalance1 - transferAmount1, + "Sender balance 1 not updated correctly" + ); + assertEq( + balanceOf(address(this), tokenId2), + senderBalance2 - transferAmount2, + "Sender balance 2 not updated correctly" + ); + assertEq( + balanceOf(USER1, tokenId1), + receiverBalance1 + transferAmount1, + "Receiver balance 1 not updated correctly" + ); + assertEq( + balanceOf(USER1, tokenId2), + receiverBalance2 + transferAmount2, + "Receiver balance 2 not updated correctly" + ); + } + + /** + * @title Batch Transfer Array Length Mismatch Should Revert + * @notice Batch transfer with mismatched array lengths must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: safeBatchTransferFrom must revert if ids.length != amounts.length + * @dev This prevents ambiguous batch operations and programming errors. + * @custom:property-id ERC1155-TRANSFER-006 + */ + function test_ERC1155_batchTransferArrayLengthMismatch() public { + uint256[] memory ids = new uint256[](2); + ids[0] = 1; + ids[1] = 2; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = 10; + + this.safeBatchTransferFrom(address(this), USER1, ids, amounts, ""); + assertWithMsg(false, "Batch transfer with mismatched arrays should have reverted"); + } + + //////////////////////////////////////////////////////////////// + // Approval Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Set Approval for All + * @notice Setting operator approval should update approval status + * @dev Testing Mode: INTERNAL + * @dev Invariant: After setApprovalForAll(operator, true), isApprovedForAll(sender, operator) == true + * @dev Operator approval allows efficient delegation of token management. + * @custom:property-id ERC1155-APPROVAL-001 + * + * @param operator The operator address to approve + */ + function test_ERC1155_setApprovalForAll(address operator) public { + require(operator != address(0)); + require(operator != address(this)); + + this.setApprovalForAll(operator, true); + assertWithMsg( + isApprovedForAll(address(this), operator), + "Operator not approved after setApprovalForAll(true)" + ); + + this.setApprovalForAll(operator, false); + assertWithMsg( + !isApprovedForAll(address(this), operator), + "Operator still approved after setApprovalForAll(false)" + ); + } + + /** + * @title Operator Can Transfer on Behalf of Owner + * @notice Approved operators must be able to transfer owner's tokens + * @dev Testing Mode: INTERNAL + * @dev Invariant: If isApprovedForAll(owner, operator), then operator can call + * safeTransferFrom(owner, to, id, amount, data) + * @dev This is the core functionality of operator approval. + * @custom:property-id ERC1155-APPROVAL-002 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_operatorTransfer(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + require(USER1 != address(this)); + require(msg.sender != address(this)); + uint256 transferAmount = amount % (balance + 1); + + // Approve msg.sender as operator + this.setApprovalForAll(msg.sender, true); + require(isApprovedForAll(address(this), msg.sender)); + + uint256 receiverBalance = balanceOf(USER1, tokenId); + + // msg.sender should be able to transfer tokens from address(this) + hevm.prank(msg.sender); + try + IERC1155(address(this)).safeTransferFrom( + address(this), + USER1, + tokenId, + transferAmount, + "" + ) + { + assertEq( + balanceOf(address(this), tokenId), + balance - transferAmount, + "Owner balance not updated after operator transfer" + ); + assertEq( + balanceOf(USER1, tokenId), + receiverBalance + transferAmount, + "Receiver balance not updated after operator transfer" + ); + } catch { + assertWithMsg(false, "Operator transfer unexpectedly reverted"); + } + } + + /** + * @title Non-Operator Cannot Transfer + * @notice Non-approved addresses must not be able to transfer tokens + * @dev Testing Mode: INTERNAL + * @dev Invariant: If !isApprovedForAll(owner, operator) and operator != owner, + * then operator cannot call safeTransferFrom(owner, to, id, amount, data) + * @dev This ensures that only authorized parties can move tokens. + * @custom:property-id ERC1155-APPROVAL-003 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_nonOperatorCannotTransfer(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + require(msg.sender != address(this)); + require(USER1 != address(this)); + uint256 transferAmount = amount % (balance + 1); + + // Ensure msg.sender is not an operator + this.setApprovalForAll(msg.sender, false); + require(!isApprovedForAll(address(this), msg.sender)); + + // msg.sender should NOT be able to transfer tokens from address(this) + hevm.prank(msg.sender); + IERC1155(address(this)).safeTransferFrom( + address(this), + USER1, + tokenId, + transferAmount, + "" + ); + + assertWithMsg(false, "Non-operator transfer should have reverted"); + } + + //////////////////////////////////////////////////////////////// + // Safety Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Safe Transfer to Contract Without Receiver + * @notice Safe transfers to contracts not implementing the receiver interface must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: safeTransferFrom to a contract that doesn't implement + * onERC1155Received must revert + * @dev This protects against tokens being permanently locked in contracts. + * @custom:property-id ERC1155-SAFETY-001 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_safeTransferToNonReceiverContract( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + // unsafeReceiver returns wrong selector + this.safeTransferFrom( + address(this), + address(unsafeReceiver), + tokenId, + transferAmount, + "" + ); + + assertWithMsg( + false, + "Safe transfer to non-receiver contract should have reverted" + ); + } + + /** + * @title Safe Transfer to Valid Receiver + * @notice Safe transfers to contracts implementing the receiver interface must succeed + * @dev Testing Mode: INTERNAL + * @dev Invariant: safeTransferFrom to a contract implementing onERC1155Received + * correctly should succeed + * @dev This ensures that properly implemented receiver contracts can accept tokens. + * @custom:property-id ERC1155-SAFETY-002 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_safeTransferToValidReceiver( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + uint256 receiverBalance = balanceOf(address(safeReceiver), tokenId); + + this.safeTransferFrom( + address(this), + address(safeReceiver), + tokenId, + transferAmount, + "" + ); + + assertEq( + balanceOf(address(safeReceiver), tokenId), + receiverBalance + transferAmount, + "Safe receiver did not receive tokens" + ); + } + + /** + * @title Safe Batch Transfer to Contract Without Receiver + * @notice Safe batch transfers to contracts not implementing the receiver interface must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: safeBatchTransferFrom to a contract that doesn't implement + * onERC1155BatchReceived must revert + * @dev This protects against tokens being permanently locked in contracts during batch operations. + * @custom:property-id ERC1155-SAFETY-003 + * + * @param tokenId The token ID to transfer + * @param amount The amount to transfer + */ + function test_ERC1155_safeBatchTransferToNonReceiverContract( + uint256 tokenId, + uint256 amount + ) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + uint256 transferAmount = amount % (balance + 1); + + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = transferAmount; + + this.safeBatchTransferFrom( + address(this), + address(unsafeReceiver), + ids, + amounts, + "" + ); + + assertWithMsg( + false, + "Safe batch transfer to non-receiver contract should have reverted" + ); + } +} diff --git a/contracts/ERC1155/internal/properties/ERC1155BurnableProperties.sol b/contracts/ERC1155/internal/properties/ERC1155BurnableProperties.sol new file mode 100644 index 0000000..2a7147a --- /dev/null +++ b/contracts/ERC1155/internal/properties/ERC1155BurnableProperties.sol @@ -0,0 +1,235 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../util/ERC1155TestBase.sol"; +import "@openzeppelin/contracts/token/ERC1155/extensions/ERC1155Burnable.sol"; + +/** + * @title ERC1155 Burnable Properties + * @author Crytic (Trail of Bits) + * @notice Invariant properties for ERC1155 tokens with burn functionality + * @dev Testing Mode: INTERNAL + * @dev This contract contains properties that must hold for ERC1155 implementations + * with burn functionality. These properties ensure that burning tokens correctly + * reduces balances and that only authorized parties can burn tokens. + * + * Properties are organized into the following sections: + * - Burn Properties: Tests for single token burn operations + * - Batch Burn Properties: Tests for batch burn operations + * + * @custom:see https://eips.ethereum.org/EIPS/eip-1155 + */ +abstract contract CryticERC1155BurnableProperties is + CryticERC1155TestBase, + ERC1155Burnable +{ + constructor(string memory uri) CryticERC1155TestBase(uri) { + isMintableOrBurnable = true; + } + + //////////////////////////////////////////////////////////////// + // Burn Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Burn Reduces Balance + * @notice Burning tokens must reduce the owner's balance by the burn amount + * @dev Testing Mode: INTERNAL + * @dev Invariant: After burn(account, id, amount), balanceOf(account, id) decreases by amount + * @dev Burn operations must correctly update token balances to maintain accurate accounting. + * @custom:property-id ERC1155-BURN-001 + * + * @param tokenId The token ID to burn + * @param amount The amount to burn + */ + function test_ERC1155_burnReducesBalance(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + uint256 burnAmount = amount % (balance + 1); + + this.burn(address(this), tokenId, burnAmount); + + assertEq( + balanceOf(address(this), tokenId), + balance - burnAmount, + "Balance not reduced correctly after burn" + ); + } + + /** + * @title Burn from Another Account Requires Approval + * @notice Burning tokens from another account requires operator approval + * @dev Testing Mode: INTERNAL + * @dev Invariant: If !isApprovedForAll(account, operator) and operator != account, + * then burn(account, id, amount) called by operator must revert + * @dev This prevents unauthorized token destruction. + * @custom:property-id ERC1155-BURN-002 + * + * @param tokenId The token ID to burn + * @param amount The amount to burn + */ + function test_ERC1155_burnRequiresApproval(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(USER1, tokenId); + require(balance > 0); + require(msg.sender != USER1); + require(msg.sender != address(this)); + uint256 burnAmount = amount % (balance + 1); + + // Ensure msg.sender is not approved + hevm.prank(USER1); + IERC1155(address(this)).setApprovalForAll(msg.sender, false); + require(!isApprovedForAll(USER1, msg.sender)); + + // msg.sender should NOT be able to burn USER1's tokens + hevm.prank(msg.sender); + ERC1155Burnable(address(this)).burn(USER1, tokenId, burnAmount); + + assertWithMsg(false, "Burn without approval should have reverted"); + } + + /** + * @title Approved Operator Can Burn + * @notice Approved operators must be able to burn owner's tokens + * @dev Testing Mode: INTERNAL + * @dev Invariant: If isApprovedForAll(account, operator), then operator can + * call burn(account, id, amount) + * @dev This ensures operator approval extends to burn operations. + * @custom:property-id ERC1155-BURN-003 + * + * @param tokenId The token ID to burn + * @param amount The amount to burn + */ + function test_ERC1155_approvedOperatorCanBurn(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(address(this), tokenId); + require(balance > 0); + require(msg.sender != address(this)); + uint256 burnAmount = amount % (balance + 1); + + // Approve msg.sender as operator + this.setApprovalForAll(msg.sender, true); + require(isApprovedForAll(address(this), msg.sender)); + + // msg.sender should be able to burn tokens from address(this) + hevm.prank(msg.sender); + try ERC1155Burnable(address(this)).burn(address(this), tokenId, burnAmount) { + assertEq( + balanceOf(address(this), tokenId), + balance - burnAmount, + "Balance not updated after operator burn" + ); + } catch { + assertWithMsg(false, "Operator burn unexpectedly reverted"); + } + } + + //////////////////////////////////////////////////////////////// + // Batch Burn Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Batch Burn Reduces All Balances + * @notice Burning multiple tokens in a batch must reduce all balances correctly + * @dev Testing Mode: INTERNAL + * @dev Invariant: After burnBatch(account, ids, amounts), all corresponding + * balances decrease by the specified amounts + * @dev Batch operations must maintain the same correctness as individual operations. + * @custom:property-id ERC1155-BURN-004 + * + * @param tokenId1 First token ID to burn + * @param tokenId2 Second token ID to burn + * @param amount1 Amount of first token to burn + * @param amount2 Amount of second token to burn + */ + function test_ERC1155_batchBurnReducesBalances( + uint256 tokenId1, + uint256 tokenId2, + uint256 amount1, + uint256 amount2 + ) public { + uint256 balance1 = balanceOf(address(this), tokenId1); + uint256 balance2 = balanceOf(address(this), tokenId2); + require(balance1 > 0 && balance2 > 0); + require(tokenId1 != tokenId2); + + uint256 burnAmount1 = amount1 % (balance1 + 1); + uint256 burnAmount2 = amount2 % (balance2 + 1); + + uint256[] memory ids = new uint256[](2); + ids[0] = tokenId1; + ids[1] = tokenId2; + + uint256[] memory amounts = new uint256[](2); + amounts[0] = burnAmount1; + amounts[1] = burnAmount2; + + this.burnBatch(address(this), ids, amounts); + + assertEq( + balanceOf(address(this), tokenId1), + balance1 - burnAmount1, + "Balance 1 not reduced correctly after batch burn" + ); + assertEq( + balanceOf(address(this), tokenId2), + balance2 - burnAmount2, + "Balance 2 not reduced correctly after batch burn" + ); + } + + /** + * @title Batch Burn Array Length Mismatch Should Revert + * @notice Batch burn with mismatched array lengths must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: burnBatch must revert if ids.length != amounts.length + * @dev This prevents ambiguous batch operations and programming errors. + * @custom:property-id ERC1155-BURN-005 + */ + function test_ERC1155_batchBurnArrayLengthMismatch() public { + uint256[] memory ids = new uint256[](2); + ids[0] = 1; + ids[1] = 2; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = 10; + + this.burnBatch(address(this), ids, amounts); + assertWithMsg(false, "Batch burn with mismatched arrays should have reverted"); + } + + /** + * @title Batch Burn Requires Approval + * @notice Batch burning tokens from another account requires operator approval + * @dev Testing Mode: INTERNAL + * @dev Invariant: If !isApprovedForAll(account, operator) and operator != account, + * then burnBatch(account, ids, amounts) called by operator must revert + * @dev This ensures batch burn operations respect the same authorization rules. + * @custom:property-id ERC1155-BURN-006 + * + * @param tokenId The token ID to burn + * @param amount The amount to burn + */ + function test_ERC1155_batchBurnRequiresApproval(uint256 tokenId, uint256 amount) public { + uint256 balance = balanceOf(USER1, tokenId); + require(balance > 0); + require(msg.sender != USER1); + require(msg.sender != address(this)); + uint256 burnAmount = amount % (balance + 1); + + // Ensure msg.sender is not approved + hevm.prank(USER1); + IERC1155(address(this)).setApprovalForAll(msg.sender, false); + require(!isApprovedForAll(USER1, msg.sender)); + + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = burnAmount; + + // msg.sender should NOT be able to batch burn USER1's tokens + hevm.prank(msg.sender); + ERC1155Burnable(address(this)).burnBatch(USER1, ids, amounts); + + assertWithMsg(false, "Batch burn without approval should have reverted"); + } +} diff --git a/contracts/ERC1155/internal/properties/ERC1155MintableProperties.sol b/contracts/ERC1155/internal/properties/ERC1155MintableProperties.sol new file mode 100644 index 0000000..1886361 --- /dev/null +++ b/contracts/ERC1155/internal/properties/ERC1155MintableProperties.sol @@ -0,0 +1,263 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../util/ERC1155TestBase.sol"; + +/** + * @title ERC1155 Mintable Properties + * @author Crytic (Trail of Bits) + * @notice Invariant properties for ERC1155 tokens with mint functionality + * @dev Testing Mode: INTERNAL + * @dev This contract contains properties that must hold for ERC1155 implementations + * with mint functionality. These properties ensure that minting tokens correctly + * increases balances for both single and batch operations. + * + * Properties are organized into the following sections: + * - Mint Properties: Tests for single token mint operations + * - Batch Mint Properties: Tests for batch mint operations + * + * Note: The mint function must be implemented by the inheriting contract as + * different implementations may have different access control or minting logic. + * + * @custom:see https://eips.ethereum.org/EIPS/eip-1155 + */ +abstract contract CryticERC1155MintableProperties is CryticERC1155TestBase { + constructor(string memory uri) CryticERC1155TestBase(uri) { + isMintableOrBurnable = true; + } + + // Should be modified if target contract's function names are different + function mint(address to, uint256 id, uint256 amount, bytes memory data) public virtual; + + function mintBatch( + address to, + uint256[] memory ids, + uint256[] memory amounts, + bytes memory data + ) public virtual; + + //////////////////////////////////////////////////////////////// + // Mint Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Mint Increases Balance + * @notice Minting tokens must increase the recipient's balance by the mint amount + * @dev Testing Mode: INTERNAL + * @dev Invariant: After mint(to, id, amount, data), balanceOf(to, id) increases by amount + * @dev Mint operations must correctly update token balances to maintain accurate accounting. + * @custom:property-id ERC1155-MINT-001 + * + * @param target The address to mint tokens to + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155_mintIncreasesBalance( + address target, + uint256 tokenId, + uint256 amount + ) public { + require(target != address(0)); + uint256 balance = balanceOf(target, tokenId); + + this.mint(target, tokenId, amount, ""); + + assertEq( + balanceOf(target, tokenId), + balance + amount, + "Balance not increased correctly after mint" + ); + } + + /** + * @title Mint to Zero Address Should Revert + * @notice Minting tokens to the zero address must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: mint(address(0), id, amount, data) must revert + * @dev Minting to the zero address would effectively burn tokens at creation, + * which is inconsistent and should be prevented. + * @custom:property-id ERC1155-MINT-002 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155_mintToZeroAddress(uint256 tokenId, uint256 amount) public { + this.mint(address(0), tokenId, amount, ""); + assertWithMsg(false, "Mint to zero address should have reverted"); + } + + /** + * @title Mint Respects Safe Transfer Check + * @notice Minting to a contract must respect the receiver interface check + * @dev Testing Mode: INTERNAL + * @dev Invariant: If recipient is a contract, mint must call onERC1155Received + * and revert if the contract doesn't return the correct selector + * @dev This protects against tokens being locked in contracts that can't handle them. + * @custom:property-id ERC1155-MINT-003 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155_mintToNonReceiverContract(uint256 tokenId, uint256 amount) public { + require(amount > 0); + + // unsafeReceiver returns wrong selector + this.mint(address(unsafeReceiver), tokenId, amount, ""); + + assertWithMsg(false, "Mint to non-receiver contract should have reverted"); + } + + /** + * @title Mint to Valid Receiver Succeeds + * @notice Minting to a contract implementing the receiver interface must succeed + * @dev Testing Mode: INTERNAL + * @dev Invariant: mint to a contract implementing onERC1155Received correctly should succeed + * @dev This ensures that properly implemented receiver contracts can receive minted tokens. + * @custom:property-id ERC1155-MINT-004 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155_mintToValidReceiver(uint256 tokenId, uint256 amount) public { + require(amount > 0); + uint256 receiverBalance = balanceOf(address(safeReceiver), tokenId); + + this.mint(address(safeReceiver), tokenId, amount, ""); + + assertEq( + balanceOf(address(safeReceiver), tokenId), + receiverBalance + amount, + "Safe receiver did not receive minted tokens" + ); + } + + //////////////////////////////////////////////////////////////// + // Batch Mint Properties // + //////////////////////////////////////////////////////////////// + + /** + * @title Batch Mint Increases All Balances + * @notice Minting multiple tokens in a batch must increase all balances correctly + * @dev Testing Mode: INTERNAL + * @dev Invariant: After mintBatch(to, ids, amounts, data), all corresponding + * balances increase by the specified amounts + * @dev Batch operations must maintain the same correctness as individual operations. + * @custom:property-id ERC1155-MINT-005 + * + * @param target The address to mint tokens to + * @param tokenId1 First token ID to mint + * @param tokenId2 Second token ID to mint + * @param amount1 Amount of first token to mint + * @param amount2 Amount of second token to mint + */ + function test_ERC1155_batchMintIncreasesBalances( + address target, + uint256 tokenId1, + uint256 tokenId2, + uint256 amount1, + uint256 amount2 + ) public { + require(target != address(0)); + require(tokenId1 != tokenId2); + + uint256 balance1 = balanceOf(target, tokenId1); + uint256 balance2 = balanceOf(target, tokenId2); + + uint256[] memory ids = new uint256[](2); + ids[0] = tokenId1; + ids[1] = tokenId2; + + uint256[] memory amounts = new uint256[](2); + amounts[0] = amount1; + amounts[1] = amount2; + + this.mintBatch(target, ids, amounts, ""); + + assertEq( + balanceOf(target, tokenId1), + balance1 + amount1, + "Balance 1 not increased correctly after batch mint" + ); + assertEq( + balanceOf(target, tokenId2), + balance2 + amount2, + "Balance 2 not increased correctly after batch mint" + ); + } + + /** + * @title Batch Mint Array Length Mismatch Should Revert + * @notice Batch mint with mismatched array lengths must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: mintBatch must revert if ids.length != amounts.length + * @dev This prevents ambiguous batch operations and programming errors. + * @custom:property-id ERC1155-MINT-006 + * + * @param target The address to mint tokens to + */ + function test_ERC1155_batchMintArrayLengthMismatch(address target) public { + require(target != address(0)); + + uint256[] memory ids = new uint256[](2); + ids[0] = 1; + ids[1] = 2; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = 10; + + this.mintBatch(target, ids, amounts, ""); + assertWithMsg(false, "Batch mint with mismatched arrays should have reverted"); + } + + /** + * @title Batch Mint to Zero Address Should Revert + * @notice Batch minting tokens to the zero address must revert + * @dev Testing Mode: INTERNAL + * @dev Invariant: mintBatch(address(0), ids, amounts, data) must revert + * @dev This maintains consistency with single mint operations. + * @custom:property-id ERC1155-MINT-007 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155_batchMintToZeroAddress(uint256 tokenId, uint256 amount) public { + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = amount; + + this.mintBatch(address(0), ids, amounts, ""); + assertWithMsg(false, "Batch mint to zero address should have reverted"); + } + + /** + * @title Batch Mint Respects Safe Transfer Check + * @notice Batch minting to a contract must respect the receiver interface check + * @dev Testing Mode: INTERNAL + * @dev Invariant: If recipient is a contract, mintBatch must call onERC1155BatchReceived + * and revert if the contract doesn't return the correct selector + * @dev This protects against tokens being locked in contracts during batch operations. + * @custom:property-id ERC1155-MINT-008 + * + * @param tokenId The token ID to mint + * @param amount The amount to mint + */ + function test_ERC1155_batchMintToNonReceiverContract( + uint256 tokenId, + uint256 amount + ) public { + require(amount > 0); + + uint256[] memory ids = new uint256[](1); + ids[0] = tokenId; + + uint256[] memory amounts = new uint256[](1); + amounts[0] = amount; + + // unsafeReceiver returns wrong selector + this.mintBatch(address(unsafeReceiver), ids, amounts, ""); + + assertWithMsg(false, "Batch mint to non-receiver contract should have reverted"); + } +} diff --git a/contracts/ERC1155/internal/util/ERC1155TestBase.sol b/contracts/ERC1155/internal/util/ERC1155TestBase.sol new file mode 100644 index 0000000..f0271d3 --- /dev/null +++ b/contracts/ERC1155/internal/util/ERC1155TestBase.sol @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "@openzeppelin/contracts/token/ERC1155/ERC1155.sol"; +import "../../../util/PropertiesConstants.sol"; +import "../../../util/PropertiesAsserts.sol"; +import {MockReceiver1155} from "./MockReceiver1155.sol"; +import "../../../util/IHevm.sol"; + +abstract contract CryticERC1155TestBase is + ERC1155, + PropertiesAsserts, + PropertiesConstants +{ + // Is the contract allowed to change its total supply? + bool isMintableOrBurnable; + MockReceiver1155 safeReceiver; + MockReceiver1155 unsafeReceiver; + + constructor(string memory uri) ERC1155(uri) { + safeReceiver = new MockReceiver1155(true); + unsafeReceiver = new MockReceiver1155(false); + } +} diff --git a/contracts/ERC1155/internal/util/MockReceiver1155.sol b/contracts/ERC1155/internal/util/MockReceiver1155.sol new file mode 100644 index 0000000..0c4df90 --- /dev/null +++ b/contracts/ERC1155/internal/util/MockReceiver1155.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "@openzeppelin/contracts/token/ERC1155/utils/ERC1155Holder.sol"; + +contract MockReceiver1155 is ERC1155Holder { + bool shouldReceive; + + constructor(bool _shouldReceive) { + shouldReceive = _shouldReceive; + } + + function onERC1155Received( + address, + address, + uint256, + uint256, + bytes memory + ) public virtual override returns (bytes4) { + if (shouldReceive) { + return this.onERC1155Received.selector; + } + return bytes4(0); + } + + function onERC1155BatchReceived( + address, + address, + uint256[] memory, + uint256[] memory, + bytes memory + ) public virtual override returns (bytes4) { + if (shouldReceive) { + return this.onERC1155BatchReceived.selector; + } + return bytes4(0); + } +} diff --git a/contracts/ERC1155/util/IERC1155Internal.sol b/contracts/ERC1155/util/IERC1155Internal.sol new file mode 100644 index 0000000..b29288c --- /dev/null +++ b/contracts/ERC1155/util/IERC1155Internal.sol @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +interface IERC1155Internal { + function balanceOf(address account, uint256 id) external view returns (uint256); + function balanceOfBatch( + address[] calldata accounts, + uint256[] calldata ids + ) external view returns (uint256[] memory); + function setApprovalForAll(address operator, bool approved) external; + function isApprovedForAll(address account, address operator) external view returns (bool); + function safeTransferFrom( + address from, + address to, + uint256 id, + uint256 amount, + bytes calldata data + ) external; + function safeBatchTransferFrom( + address from, + address to, + uint256[] calldata ids, + uint256[] calldata amounts, + bytes calldata data + ) external; +}