Skip to content

Commit

Permalink
⚡️ Optimise erc1155 NoBackdoor halmos Test (#255)
Browse files Browse the repository at this point in the history 
### 🕓 Changelog

This PR uncomments the `erc721` and `erc1155` `NoBackdoor` `halmos`
tests and optimises the `erc1155` `NoBackdoor` `halmos` test. In
addition, we remove the `test-parallel` flag in the `halmos`
configuration, because if both `test-parallel` and `solver-parallel` are
enabled, the (peak) number of parallel solver processes could be too
high, which could affect performance. The `erc721` `halmos` tests take
substantial amount of time as part of the CI. Henceforth, we run the
`halmos` CI pipeline each day at _03:30 a.m._ (= "nightly" tests) as
scheduled `cron` job instead of integrating it into the normal `push`
and `pull_request` pipeline.

---------

Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Co-authored-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
  • Loading branch information
@daejunpark @pcaversaccio
daejunpark and pcaversaccio authored Jun 25, 2024
1 parent a66c920 commit 0babe4d
Show file tree
Hide file tree
Showing 5 changed files with 175 additions and 140 deletions.
5 changes: 4 additions & 1 deletion .github/workflows/halmos.yml
View file
Original file line number Diff line number Diff line change
@@ -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 }}
Expand Down
4 changes: 2 additions & 2 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
1 change: 0 additions & 1 deletion test/halmos.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
200 changes: 117 additions & 83 deletions test/tokens/halmos/ERC1155TestHalmos.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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,
Expand Down
105 changes: 52 additions & 53 deletions test/tokens/halmos/ERC721TestHalmos.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down

0 comments on commit 0babe4d

Please sign in to comment.