test: simplify symbolic tests using new halmos cheatcode

[daejunpark]

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 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

• The PR title adheres to the conventional commits standard
• The PR has been tagged with change type label(s) (i.e. documentation, feature, bugfix, or chore)
• The PR's changes adhere to all the requirements in the contribution guidelines
• All commits have been signed

---

PR-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

• 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}