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

Add symbolic tests with Halmos #445

Open
wants to merge 4 commits into
base: main
Choose a base branch
from

Conversation

daejunpark
Copy link

This adds symbolic tests using Halmos. (This post explains more about the benefit of symbolic testing.)

The tested (or verified) properties for mint(), burn(), and transfer() are:

  • They revert for invalid inputs (e.g., minting zero quantity; minting or transferring to zero address; burning or transferring non-existing tokens or without approvals; etc.)
  • Only mint() updates nextTokenId, and it does so properly.
  • They update the token balance and ownership properly for relevant users.
  • They never alters the token balance and ownership for irrelevant users.

Note:

  • The tests currently need to refer to private functions and storage variables to describe the above properties, thus running these tests requires temporarily change their visibility from private to internal during testing. This is currently handled in the CI, but may need more scripting to be run locally.
  • Running these symbolic tests is added in the CI, but it currently takes >30min in the Github Actions (~15min in my laptop), so it may be considered to trigger it less frequently, if time is an issue. The running time can be improved later once Halmos supports utilizing multiple cores.

@daejunpark
Copy link
Author

daejunpark commented Feb 3, 2023

The newly added CI workflow result can be seen here:
https://github.com/daejunpark/ERC721A/actions/runs/4200111179/jobs/7285788074

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.

None yet

1 participant