Repository navigation
Conversation
msooseth
force-pushed
the
stack/7-invariants
branch
2 times, most recently
from
November 13, 2026 14:34
63c8432 to
01e0775
Compare
…leaks in symbolic execution Success leaves are checked by the solver and deduplicated as they are reached. Traces, memory size and loop visit counters no longer keep earlier VMs alive, and memory snapshots at forks drop the unused zeros. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ions The end states of one call with the same accounts, block and environment become one state constrained by the disjunction of their path conditions, so the next call explores it once. Logs of earlier calls are dropped. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Two parts that differ only in a condition and its negation become one without it, and parts implied by others are dropped, so the branches of an assertion leave no disjunction behind. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Newer optics exports disjoin from Optics.Core, which made the Windows build fail with an ambiguous occurrence. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
msooseth
force-pushed
the
stack/7-invariants
branch
from
November 13, 2026 14:36
01e0775 to
80daf01
Compare
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Invariant testing keeps only feasible, slimmed states, and merges states that differ only in their path conditions into one with a shortened disjunction of those conditions. This also fixes space leaks in symbolic execution, and adds an invariant testing tutorial to the docs.
Part 7 of 7 of splitting #1248; this branch is identical to
spark-psm-invariants.Checklist