diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml index f4a2ff1b..c4e7c03c 100644 --- a/.github/workflows/halmos.yml +++ b/.github/workflows/halmos.yml @@ -1,6 +1,9 @@ name: 👁️ Halmos symbolic tests -on: [push, pull_request, workflow_dispatch] +on: + schedule: + - cron: "30 3 * * *" + workflow_dispatch: concurrency: group: ${{ github.workflow }}-${{ github.ref }} diff --git a/README.md b/README.md index c73ad896..dbccc579 100644 --- a/README.md +++ b/README.md @@ -212,10 +212,10 @@ Eventually, the [`halmos`](https://github.com/a16z/halmos)-based symbolic tests # Run Halmos ERC-20 symbolic tests. ~$ FOUNDRY_PROFILE=halmos halmos --contract ERC20TestHalmos --config test/halmos.toml -# Run Halmos ERC-721 symbolic tests. Be careful, this is a very time-consuming operation. +# Run Halmos ERC-721 symbolic tests. Be careful, this is a (very!) time-consuming operation. ~$ FOUNDRY_PROFILE=halmos halmos --contract ERC721TestHalmos --config test/halmos.toml -# Run Halmos ERC-1155 symbolic tests. Be careful, this is a very time-consuming operation. +# Run Halmos ERC-1155 symbolic tests. Be careful, this is a time-consuming operation. ~$ FOUNDRY_PROFILE=halmos halmos --contract ERC1155TestHalmos --config test/halmos.toml # Run Halmos math symbolic tests. diff --git a/test/halmos.toml b/test/halmos.toml index 019305bc..4b41d4d7 100644 --- a/test/halmos.toml +++ b/test/halmos.toml @@ -2,7 +2,6 @@ # Test settings. function = "testHalmos" # Run tests matching the given prefix. storage-layout = "generic" # Set the generic storage layout model. -test-parallel = true # Run tests in parallel. early-exit = true # Stop after a counterexample is found. ffi = true # Enable the foreign function interface (ffi) cheatcode. diff --git a/test/tokens/halmos/ERC1155TestHalmos.t.sol b/test/tokens/halmos/ERC1155TestHalmos.t.sol index 11f707b0..3ee5321f 100644 --- a/test/tokens/halmos/ERC1155TestHalmos.t.sol +++ b/test/tokens/halmos/ERC1155TestHalmos.t.sol @@ -53,6 +53,18 @@ contract ERC1155TestHalmos is Test, SymTest { holders[1] = address(0x31337); holders[2] = address(0xbA5eD); + /** + * @dev Assume that the holders are EOAs to avoid multiple paths that can + * occur due to `safeTransferFrom` and `safeBatchTransferFrom` (specifically + * `_check_on_erc1155_received` and `_check_on_erc1155_batch_received`) + * depending on whether there is a contract or an EOA. Please note that + * using a single `assume` with conjunctions would result in the creation of + * multiple paths, negatively impacting performance. + */ + vm.assume(holders[0].code.length == 0); + vm.assume(holders[1].code.length == 0); + vm.assume(holders[2].code.length == 0); + tokenIds = new uint256[](5); tokenIds[0] = 0; tokenIds[1] = 1; @@ -114,89 +126,111 @@ contract ERC1155TestHalmos is Test, SymTest { vm.stopPrank(); } - /** - * @dev Currently commented out due to performance and reverting path issues in Halmos. - */ - // function testHalmosAssertNoBackdoor( - // bytes4 selector, - // address caller, - // address other - // ) public { - // /** - // * @dev Using a single `assume` with conjunctions would result in the creation of - // * multiple paths, negatively impacting performance. - // */ - // vm.assume(caller != other); - // vm.assume(selector != IERC1155Extended._customMint.selector); - // vm.assume(selector != IERC1155Extended.safe_mint.selector); - // vm.assume(selector != IERC1155Extended.safe_mint_batch.selector); - // for (uint256 i = 0; i < holders.length; i++) { - // vm.assume(!erc1155.isApprovedForAll(holders[i], caller)); - // } - - // address[] memory callers; - // address[] memory others; - // for (uint256 i = 0; i < tokenIds.length; i++) { - // callers[i] = caller; - // others[i] = other; - // } - - // uint256[] memory oldBalanceCaller = erc1155.balanceOfBatch( - // callers, - // tokenIds - // ); - // uint256[] memory oldBalanceOther = erc1155.balanceOfBatch( - // others, - // tokenIds - // ); - - // vm.startPrank(caller); - // bool success; - // if (selector == IERC1155.safeTransferFrom.selector) { - // // solhint-disable-next-line avoid-low-level-calls - // (success, ) = token.call( - // abi.encodeWithSelector( - // selector, - // svm.createAddress("from"), - // svm.createAddress("to"), - // svm.createUint256("tokenId"), - // svm.createUint256("amount"), - // svm.createBytes(96, "YOLO") - // ) - // ); - // } else if (selector == IERC1155.safeBatchTransferFrom.selector) { - // uint256[] memory ids = new uint256[](5); - // uint256[] memory values = new uint256[](5); - // for (uint256 i = 0; i < ids.length; i++) { - // ids[i] = svm.createUint256("ids"); - // values[i] = svm.createUint256("values"); - // } - // // solhint-disable-next-line avoid-low-level-calls - // (success, ) = token.call( - // abi.encodeWithSelector( - // selector, - // svm.createAddress("from"), - // svm.createAddress("to"), - // ids, - // values, - // svm.createBytes(96, "YOLO") - // ) - // ); - // } else { - // bytes memory args = svm.createBytes(1_024, "WAGMI"); - // // solhint-disable-next-line avoid-low-level-calls - // (success, ) = address(token).call(abi.encodePacked(selector, args)); - // } - // vm.assume(success); - // vm.stopPrank(); - - // for (uint256 i = 0; i < tokenIds.length; i++) { - // assert( - // erc1155.balanceOf(caller, tokenIds[i]) <= oldBalanceCaller[i] - // ); - // assert(erc1155.balanceOf(other, tokenIds[i]) >= oldBalanceOther[i]); - // } - // } + function testHalmosAssertNoBackdoor( + bytes4 selector, + address caller, + address other + ) public { + /** + * @dev Using a single `assume` with conjunctions would result in the creation of + * multiple paths, negatively impacting performance. + */ + vm.assume(caller != other); + vm.assume(selector != IERC1155Extended._customMint.selector); + vm.assume(selector != IERC1155Extended.safe_mint.selector); + vm.assume(selector != IERC1155Extended.safe_mint_batch.selector); + + /** + * @dev For convenience, ignore `view` functions that use dynamic arrays. + */ + vm.assume(selector != IERC1155.balanceOfBatch.selector); + + for (uint256 i = 0; i < holders.length; i++) { + vm.assume(!erc1155.isApprovedForAll(holders[i], caller)); + } + + address[] memory callers = new address[](tokenIds.length); + address[] memory others = new address[](tokenIds.length); + for (uint256 i = 0; i < tokenIds.length; i++) { + callers[i] = caller; + others[i] = other; + } + + uint256[] memory oldBalanceCaller = erc1155.balanceOfBatch( + callers, + tokenIds + ); + uint256[] memory oldBalanceOther = erc1155.balanceOfBatch( + others, + tokenIds + ); + + vm.startPrank(caller); + bool success; + if (selector == IERC1155.safeTransferFrom.selector) { + // solhint-disable-next-line avoid-low-level-calls + (success, ) = token.call( + abi.encodeWithSelector( + selector, + svm.createAddress("owner"), + svm.createAddress("to"), + svm.createUint256("tokenId"), + svm.createUint256("amount"), + svm.createBytes(96, "YOLO") + ) + ); + } else if ( + selector == IERC1155.safeBatchTransferFrom.selector || + selector == IERC1155Extended.burn_batch.selector + ) { + uint256[] memory ids = new uint256[](5); + uint256[] memory values = new uint256[](5); + for (uint256 i = 0; i < ids.length; i++) { + ids[i] = svm.createUint256("ids"); + values[i] = svm.createUint256("values"); + } + bytes memory data = (selector == + IERC1155.safeBatchTransferFrom.selector) + ? abi.encodeWithSelector( + selector, + svm.createAddress("owner"), + svm.createAddress("to"), + ids, + values, + svm.createBytes(96, "YOLO") + ) + : abi.encodeWithSelector( + selector, + svm.createAddress("owner"), + ids, + values + ); + // solhint-disable-next-line avoid-low-level-calls + (success, ) = token.call(data); + } else if (selector == IERC1155Extended.set_uri.selector) { + // solhint-disable-next-line avoid-low-level-calls + (success, ) = token.call( + abi.encodeWithSelector( + selector, + svm.createUint256("id"), + svm.createBytes(96, "uri") + ) + ); + } else { + bytes memory args = svm.createBytes(1_024, "WAGMI"); + // solhint-disable-next-line avoid-low-level-calls + (success, ) = address(token).call(abi.encodePacked(selector, args)); + } + vm.assume(success); + vm.stopPrank(); + + for (uint256 i = 0; i < tokenIds.length; i++) { + assert( + erc1155.balanceOf(caller, tokenIds[i]) <= oldBalanceCaller[i] + ); + assert(erc1155.balanceOf(other, tokenIds[i]) >= oldBalanceOther[i]); + } + } function testHalmosSafeTransferFrom( address caller, diff --git a/test/tokens/halmos/ERC721TestHalmos.t.sol b/test/tokens/halmos/ERC721TestHalmos.t.sol index 49a59218..2ea63da0 100644 --- a/test/tokens/halmos/ERC721TestHalmos.t.sol +++ b/test/tokens/halmos/ERC721TestHalmos.t.sol @@ -94,62 +94,61 @@ contract ERC721TestHalmos is Test, SymTest { } /** - * @dev Currently commented out due to performance and reverting path issues in Halmos. * @notice Forked and adjusted accordingly from here: * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC721/test/ERC721Test.sol. */ - // function testHalmosAssertNoBackdoor( - // bytes4 selector, - // address caller, - // address other - // ) public { - // /** - // * @dev Using a single `assume` with conjunctions would result in the creation of - // * multiple paths, negatively impacting performance. - // */ - // vm.assume(caller != other); - // vm.assume(selector != IERC721Extended._customMint.selector); - // vm.assume(selector != IERC721Extended.safe_mint.selector); - // for (uint256 i = 0; i < holders.length; i++) { - // vm.assume(!erc721.isApprovedForAll(holders[i], caller)); - // } - // for (uint256 i = 0; i < tokenIds.length; i++) { - // vm.assume(erc721.getApproved(tokenIds[i]) != caller); - // } - - // uint256 oldBalanceCaller = erc721.balanceOf(caller); - // uint256 oldBalanceOther = erc721.balanceOf(other); - - // vm.startPrank(caller); - // bool success; - // if ( - // selector == - // bytes4(keccak256("safeTransferFrom(address,address,uint256,bytes)")) - // ) { - // // solhint-disable-next-line avoid-low-level-calls - // (success, ) = token.call( - // abi.encodeWithSelector( - // selector, - // svm.createAddress("from"), - // svm.createAddress("to"), - // svm.createUint256("tokenId"), - // svm.createBytes(96, "YOLO") - // ) - // ); - // } else { - // bytes memory args = svm.createBytes(1_024, "WAGMI"); - // // solhint-disable-next-line avoid-low-level-calls - // (success, ) = address(token).call(abi.encodePacked(selector, args)); - // } - // vm.assume(success); - // vm.stopPrank(); - - // uint256 newBalanceCaller = erc721.balanceOf(caller); - // uint256 newBalanceOther = erc721.balanceOf(other); - - // assert(newBalanceCaller <= oldBalanceCaller); - // assert(newBalanceOther >= oldBalanceOther); - // } + function testHalmosAssertNoBackdoor( + bytes4 selector, + address caller, + address other + ) public { + /** + * @dev Using a single `assume` with conjunctions would result in the creation of + * multiple paths, negatively impacting performance. + */ + vm.assume(caller != other); + vm.assume(selector != IERC721Extended._customMint.selector); + vm.assume(selector != IERC721Extended.safe_mint.selector); + for (uint256 i = 0; i < holders.length; i++) { + vm.assume(!erc721.isApprovedForAll(holders[i], caller)); + } + for (uint256 i = 0; i < tokenIds.length; i++) { + vm.assume(erc721.getApproved(tokenIds[i]) != caller); + } + + uint256 oldBalanceCaller = erc721.balanceOf(caller); + uint256 oldBalanceOther = erc721.balanceOf(other); + + vm.startPrank(caller); + bool success; + if ( + selector == + bytes4(keccak256("safeTransferFrom(address,address,uint256,bytes)")) + ) { + // solhint-disable-next-line avoid-low-level-calls + (success, ) = token.call( + abi.encodeWithSelector( + selector, + svm.createAddress("owner"), + svm.createAddress("to"), + svm.createUint256("tokenId"), + svm.createBytes(96, "YOLO") + ) + ); + } else { + bytes memory args = svm.createBytes(1_024, "WAGMI"); + // solhint-disable-next-line avoid-low-level-calls + (success, ) = address(token).call(abi.encodePacked(selector, args)); + } + vm.assume(success); + vm.stopPrank(); + + uint256 newBalanceCaller = erc721.balanceOf(caller); + uint256 newBalanceOther = erc721.balanceOf(other); + + assert(newBalanceCaller <= oldBalanceCaller); + assert(newBalanceOther >= oldBalanceOther); + } /** * @notice Forked and adjusted accordingly from here: