Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

⚡️ Optimise erc1155 NoBackdoor halmos Test #255

Merged
merged 14 commits into from
Jun 25, 2024
Merged

⚡️ Optimise erc1155 NoBackdoor halmos Test #255

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
d21b5fd
uncomment testHalmosAssertNoBackdoor tests
daejunpark Jun 22, 2024
b7cb254
ERC1155TestHalmos: ensure a single setup path by assuming holders are…
daejunpark Jun 22, 2024
33451b6
ERC1155TestHalmos: fix setup error
daejunpark Jun 22, 2024
7091e9f
ERC1155TestHalmos: provide a specific size for dynamic array argument…
daejunpark Jun 22, 2024
ba19065
ERC1155TestHalmos: ignore view functions that take dynamic arrays
daejunpark Jun 22, 2024
efa7af4
halmos.toml: disable test parallel
daejunpark Jun 22, 2024
2da764a
Merge branch 'main' into halmos
pcaversaccio Jun 23, 2024
e597e1c
♻️ Cleanup
pcaversaccio Jun 24, 2024
ad8d8d8
♻️ Testing `erc721`
pcaversaccio Jun 24, 2024
f5593d3
♻️ Fix wrong trigger
pcaversaccio Jun 24, 2024
479f0ea
♻️ Well guess what, fix does not work
pcaversaccio Jun 24, 2024
72e9356
♻️ Post-ci-test cleanup
pcaversaccio Jun 24, 2024
a515106
♻️ Use Ternary Operator
pcaversaccio Jun 24, 2024
f583ba5
♻️ Consistency with Vyper implementation
pcaversaccio Jun 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion .github/workflows/halmos.yml
View file
Open in desktop
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
1 change: 0 additions & 1 deletion test/halmos.toml
View file
Open in desktop
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.
pcaversaccio marked this conversation as resolved.
Show resolved Hide resolved
early-exit = true # Stop after a counterexample is found.
ffi = true # Enable the foreign function interface (ffi) cheatcode.

Expand Down
204 changes: 121 additions & 83 deletions test/tokens/halmos/ERC1155TestHalmos.t.sol
View file
Open in desktop
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,115 @@ 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("from"),
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;

if (selector == IERC1155.safeBatchTransferFrom.selector) {
data = abi.encodeWithSelector(
selector,
svm.createAddress("from"),
svm.createAddress("to"),
ids,
values,
svm.createBytes(96, "YOLO")
);
} else {
data = 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
Open in desktop
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("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);
}

/**
* @notice Forked and adjusted accordingly from here:
Expand Down