fix(core): isolate path conditions at the procedure boundary#1391
Merged
fabiomadge merged 2 commits intoJun 22, 2026
Merged
Conversation
fabiomadge
changed the title
`Program.eval` threads one `Env` through every procedure in source order. A path that leaves a labeled block via a structured `exit` does not get its path-condition frames popped (the exiting path bypasses `Env.merge`), so a procedure's preconditions and in-scope assumptions leaked into the next procedure's verification context. When the leaked set was contradictory, the next procedure proved false obligations vacuously — a silent green pass (unsound). Laurel lowers every non-final `return` to a structured `exit`, so ordinary early-return code triggered this. Reset `pathConditions` to the pre-procedure state in the `.proc` fold so a procedure's assumptions cannot leak into later procedures; carry deferred obligations and the fresh-name set forward unchanged. Adds ProcedurePathConditionIsolation regression test (first has an unsatisfiable precondition + a structured exit; second's `assert false` must fail, not silently pass). Full StrataTest stays green. Fixes #1390
fabiomadge
force-pushed
the
fix/core-pathcond-leak-procedure-boundary
branch
from
3d90445 to
8e68ec8
Compare
ssomayyajula
approved these changes
Jun 22, 2026
joscoh
approved these changes
Jun 22, 2026
Merged
via the queue into
reviewed-kbd-will-merge-to-main
with commit Jun 22, 2026
064e019
18 checks passed
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
3 participants
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.
Fixes #1390.
Problem:
Program.evalthreads oneEnvthrough all procedures. A structuredexitout of a labeled block doesn't pop its path-condition frames (.blockexit popsexprEnv.state, notpathConditions; the exiting path bypassesEnv.merge), so a procedure's preconditions/assumptions leak into later procedures. A contradictory leaked set then makes the next procedure prove false obligations vacuously — silent unsound pass. Laurel lowers non-finalreturntoexit "$body", so ordinary early-return code hits it.Fix: reset
pathConditionsto the pre-procedure state in the.procfold (deferred obligations and fresh names carry forward). A.block-level reset was rejected — breaks fall-through.Test:
ProcedurePathConditionIsolation— unsatisfiable-preconditionfirst+ structuredexit,second'sassert falsemust fail. Red without the fix, green with it; fullStrataTestgreen (539). Control matrix + scope in #1390.