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.

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

test: simplify symbolic tests using new halmos cheatcode #430

Closed

Conversation

daejunpark
Copy link
Contributor

@daejunpark daejunpark commented Sep 20, 2024

[this is a temporary pr to be upstreamed after halmos v2 is released.]

this pr improves symbolic tests using new halmos cheatcode createCalldata().

previously, symbolic tests required custom calldata generators to handle dynamic size arrays and bytes. the new createCalldata() cheatcode now seamlessly supports such dynamically-sized parameters by considering all combinations of size candidates. these can be specified using additional flags --array-lengths and --default-bytes-lengths (see 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.


PR-Codex overview

The focus of this PR is to refactor the check_Invariants_PostMigration function and remove unnecessary code in IdRegistrySymTest.

Detailed summary

  • Refactored check_Invariants_PostMigration function in IdRegistrySymTest
  • Removed _calldataFor function from IdRegistrySymTest
  • Updated check_Invariants function in KeyRegistrySymTest to use svm.createCalldata
  • Removed split_cases and mk_calldata functions from KeyRegistrySymTest
  • Added slice function to KeyRegistrySymTest

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

@daejunpark
Copy link
Contributor Author

wrong base repo, close for now.

@daejunpark daejunpark closed this Sep 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant