fix(eval): isolate Env.error at procedure boundary (issue #1185)#1190
Open
PROgram52bc wants to merge 8 commits into
Open
fix(eval): isolate Env.error at procedure boundary (issue #1185)#1190PROgram52bc wants to merge 8 commits into
PROgram52bc wants to merge 8 commits into
Conversation
added 7 commits
May 19, 2026 15:45
The first test (issue1185Repro) currently fails: `assert false` in proc_c is silently dropped because proc_b's funcDecl collision contaminates `Env.error` and short-circuits subsequent statement evaluation. The reorder regression (issue1185Reordered) already passes pre-fix; we lock it in to protect against regression.
Closes a soundness leak where one procedure's partial-evaluation error (e.g., function redefinition) would contaminate Env.error, causing StatementEval.evalAuxGo (line 618-619) to short-circuit every statement in subsequent procedures. The contaminated env produced zero deferred obligations, so a literal `assert false` in a later procedure was silently passed. fixupError now pops scope+PC frames and clears Env.error on every path, so each procedure's evaluation starts from a clean error state. Clean deferred obligations from any path are preserved as-is — each obligation carries its own assumption list and is independently provable. Issue: #1185
Cases 1, 2, and 4 currently fail. `Env.merge` returns the errored side verbatim (case 1: returns E1 with empty deferred, dropping E2's; case 2: mirror; case 4: returns E1 with one deferred, dropping E2's). Case 3 (clean+clean, four obligations total) passes via the existing `performMerge` path. Issue: #1185
When one ITE branch errors, Env.merge previously returned that side verbatim — silently discarding the clean branch's already-accumulated deferred obligations. This is the within-procedure analogue of the cross-procedure leak fixed by the previous commit: an obligation generated by sound symbolic execution should not be erased because a sibling path crashed. Now Env.merge keeps the errored side's structural fields (state, scope, error, pathConditions) but unions `deferred` from both sides. Path conditions on the non-errored side are dropped on the error path; this is fine because the merged env carries an error and future statements short-circuit before consulting PCs. Issue: #1185
The Issue #1185 commits (d55ac1c fixupError, eeb0dfa Env.merge) both referenced `StatementEval.lean:618-619` for the error-state short-circuit. That range was inherited from the issue report and is now off — the short-circuit lives at lines 632-633 (the `evalAuxGo` `if good.isEmpty` return), not 618-619 (which sit inside `addFactoryFunc` match arms). Env.merge's reference was corrected when its commit was amended; this commit corrects fixupError's matching reference. No code change. Issue: #1185
End-to-end test on the exact 17-line program from the issue. Pre-fix, the CLI reported "All 0 goals passed". Post-fix, it correctly reports proc_c's `assert false` as failing. This catches any regression that bypasses the in-tree Lean #guard_msgs tests (e.g., wiring changes in the CLI surface). Issue: #1185
The Env.merge fix from eeb0dfa kept E1's error value when both sides error (an arbitrary choice — the merged env carries an error flag either way and the caller short-circuits regardless), but the comment didn't say so. The Case 4 test happened to merge two envs with the same error string, hiding the asymmetry. Final whole-PR review flagged this as a minor maintainability issue. Add one line to Env.merge's comment explaining the both-errored choice, and add Case 5 to EnvMergeErrorPreservesDeferred.lean that merges two envs with DISTINCT error values to lock in the contract. Issue: #1185
Remove "Issue #1185" pointers from the cross-procedure error-isolation fix (fixupError, Env.merge) and its tests. Rename test-program defs issue1185Repro / issue1185Reordered to collisionThenAssertFalse / assertFalseThenCollision to describe what they exercise rather than where they came from. Tighten the surrounding comments to keep only the load-bearing "why" — error must not leak across the procedure boundary, deferred must be unioned across the error wall — and drop brittle file:line cross-references. No behavior change.
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
1 participant
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.
Summary
Fixes issue #1185 —
Program.evalpropagatedEnv.erroracross procedures, silently dropping later procedures' obligations and reporting "All 0 goals passed" even with a literalassert falsein scope.Two surgical fixes restore local invariants:
Procedure.fixupError(Strata/Languages/Core/ProcedureEval.lean:23-31) now unconditionally pops scope/PC frames AND clearsEnv.error, so each procedure's evaluation starts from a clean error state.Env.merge(Strata/Languages/Core/Env.lean:358-373) now unionsdeferredacross the error wall when one ITE branch errors, preserving the clean branch's already-accumulated obligations.Scope is deliberately minimal: visibility/UX (stderr warnings, per-procedure error stat,
peErrorsfield) was considered and explicitly cut to a follow-up. No new types, helpers, fields, or signature changes.Test plan
lake build StrataTestpasses (verified locally — 608/608 jobs).StrataTest.Languages.Core.Tests.ProgramEvalErrorIsolation(new) — issue's exact 17-line repro reportsassert_0: ❌ fail; reorder regression still passes.StrataTest.Languages.Core.Tests.EnvMergeErrorPreservesDeferred(new) — 5 cases covering errored/clean combinations ofEnv.merge, including the both-errored asymmetry contract.Examples/IsolatedProcEvalError.core.st(new CLI golden) —Examples/run_examples.shreportsTest passed.Notes for reviewers
*WF.lean,VerifierProofs.lean, andStatementSemanticsProps.lean(4091 lines combined): no proof referencesfixupError,mergeResults,Procedure.eval,Program.eval,Env.merge,performMerge, orEnv.error. Themergereferences inVerifierProofs.leanare aboutSMT.Result.merge(solver-result lattice join), unrelated.ProofObligation.assumptionsisPathConditions Expression(a value-typed list of assumptions baked in at obligation creation), so an obligation carried across an error boundary remains independently provable.Commits
ecf402211test: failing repro for cross-procedure leakd55ac1c33fix: clear Env.error and pop frames in fixupError unconditionallycaec30bd4test: failing unit tests for Env.merge deferred preservationeeb0dfa3dfix: union deferred obligations across Env.merge error wall2e260c4b8docs: fix stale StatementEval line reference in fixupError commentd22edcf9ftest: CLI golden regression490d5cbb8test/docs: document Env.merge both-errored asymmetryCloses #1185