-
Notifications
You must be signed in to change notification settings - Fork 1.7k
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
fix(forge): Invariant Shrinking #6530
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nits
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this is sick! some nits
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Love it, lgtm bar a few nits
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lgtm — pinging @mattsse for any final nits before merge
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
not very familiar with the invariant impl,
but the comments make sense to me
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lgtm
Motivation
https://x.com/devdacian/status/1732065261195526515
https://x.com/devdacian/status/1731900735686685094
Our current shrinking algorithm for invariants doesn't work very well, leaving a ton of extra txs in the sequence. This improves it, making it easier for devs to understand the flow for the invariant to break.
Solution
Construct either a power set or random subsequence of function calls and run them all in parallel to see if the invariant still breaks. If the new shorter subsequence still breaks the invariant, update the global shortest sequence tracker. If we used a random subsequence (not power set), recurse and try to continue to reduce until we hit the
shrink_run_limit
. If we used a power set, we are guaranteed to have hit a local minimum in sequence length after it is completed.Also adds a configuration option:
shrink_run_limit
- this is the number of sequences to try. A higher number of sequences allowed will result in more simplification (up until a local or global minimum is found).