This PR improves symbolic tests using new halmos cheatcode createCalldata().
Previously, symbolic tests required custom calldata generators to handle dynamic-sized arrays and bytes. The new createCalldata() cheatcode now seamlessly supports such dynamically-sized parameters by considering all combinations of size candidates. These sizes can be specified using the additional flags --array-lengths and --default-bytes-lengths (refer to halmos -h for more details.)
With this new cheatcode, the symbolic tests are now much simpler to understand and maintain, while also accounting for more combinations of dynamic parameter sizes.
Change Summary
Replaced the custom calldata generator _calldataFor() with the createCalldata() cheatcode.
Merge Checklist
Choose all relevant options below by adding an x now or at any time before submitting for review
This PR focuses on simplifying the handling of function selectors and calldata in various smart contract tests. It removes unnecessary functions and improves the way calldata is generated, enhancing code clarity and maintainability.
Detailed summary
Updated check_Invariants functions to remove bytes4 selector parameter.
Replaced _calldataFor function with direct calldata creation using svm.createCalldata.
Removed redundant function definitions across multiple test contracts.
Added a new slice function for byte manipulation.
✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}
Motivation
This PR improves symbolic tests using new halmos cheatcode
createCalldata()
.Previously, symbolic tests required custom calldata generators to handle dynamic-sized arrays and bytes. The new
createCalldata()
cheatcode now seamlessly supports such dynamically-sized parameters by considering all combinations of size candidates. These sizes can be specified using the additional flags--array-lengths
and--default-bytes-lengths
(refer tohalmos -h
for more details.)With this new cheatcode, the symbolic tests are now much simpler to understand and maintain, while also accounting for more combinations of dynamic parameter sizes.
Change Summary
Replaced the custom calldata generator
_calldataFor()
with thecreateCalldata()
cheatcode.Merge Checklist
Choose all relevant options below by adding an
x
now or at any time before submitting for reviewPR-Codex overview
This PR focuses on simplifying the handling of function selectors and calldata in various smart contract tests. It removes unnecessary functions and improves the way calldata is generated, enhancing code clarity and maintainability.
Detailed summary
check_Invariants
functions to removebytes4 selector
parameter._calldataFor
function with direct calldata creation usingsvm.createCalldata
.slice
function for byte manipulation.