From ecf402211181aed408397b45303b376a038c9eba Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:45:19 -0700 Subject: [PATCH 1/8] test: add failing repro for issue #1185 cross-procedure error leak 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. --- .../Core/Tests/ProgramEvalErrorIsolation.lean | 90 +++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean b/StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean new file mode 100644 index 000000000..92feeab5e --- /dev/null +++ b/StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean @@ -0,0 +1,90 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + + +import Strata.Languages.Core.Verifier + +/-! ## Tests for cross-procedure error isolation in `Program.eval` + +Regression tests for issue #1185 — when one procedure's partial evaluation +errors (e.g., function-name collision), the error must NOT contaminate +subsequent procedures' evaluation. Each procedure's evaluation should start +from a clean `Env.error` state. -/ + +--------------------------------------------------------------------- +namespace Strata + + +/-- Issue #1185 exact repro. proc_a registers `foo`; proc_b's redefinition of + `foo` raises a partial-evaluation error; proc_c's `assert false` MUST still + be evaluated and reported as failing. Pre-fix: "All 0 goals passed" (the + soundness bug). Post-fix: assert_0 reports ❌ fail. -/ +private def issue1185Repro := +#strata +program Core; + +procedure proc_a() +{ + function foo(y : int) : int { y + 1 } +}; + +procedure proc_b() +{ + function foo(y : int) : int { y + 2 } +}; + +procedure proc_c() +{ + assert false; +}; +#end + + +/-- +info: +Obligation: assert_0 +Property: assert +Result: ❌ fail +-/ +#guard_msgs in +#eval verify issue1185Repro (options := .quiet) + + +/-- Reorder regression: proc_c first, then the colliding pair. This already + worked pre-fix (the issue's "Reordering Rescues the Obligation" section). + Protect against regression. -/ +private def issue1185Reordered := +#strata +program Core; + +procedure proc_c() +{ + assert false; +}; + +procedure proc_a() +{ + function foo(y : int) : int { y + 1 } +}; + +procedure proc_b() +{ + function foo(y : int) : int { y + 2 } +}; +#end + + +/-- +info: +Obligation: assert_0 +Property: assert +Result: ❌ fail +-/ +#guard_msgs in +#eval verify issue1185Reordered (options := .quiet) + + +end Strata From d55ac1c33f24743f1eb8c0c37cdbf8eedd9b9cb3 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 15:56:05 -0700 Subject: [PATCH 2/8] fix(eval): clear Env.error and pop frames in fixupError unconditionally MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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: strata-org/Strata#1185 --- Strata/Languages/Core/ProcedureEval.lean | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/Strata/Languages/Core/ProcedureEval.lean b/Strata/Languages/Core/ProcedureEval.lean index 9ea328f41..c1f1f4d90 100644 --- a/Strata/Languages/Core/ProcedureEval.lean +++ b/Strata/Languages/Core/ProcedureEval.lean @@ -21,10 +21,14 @@ open Std open Statement Lambda LExpr def fixupError (E : Env) : Env := - match E.error with - | none => { E with exprEnv.state := E.exprEnv.state.pop, - pathConditions := E.pathConditions.pop } - | some _ => E + -- Issue #1185: pop frames AND clear `error` unconditionally. Keeping `error` + -- across the procedure boundary contaminates subsequent procedures + -- (StatementEval.lean:618-619 short-circuits on Env.error.isSome). Clean-path + -- obligations already in `E.deferred` are preserved as-is — they are + -- independently provable (each carries its own assumption list). + { E with error := none, + exprEnv.state := E.exprEnv.state.pop, + pathConditions := E.pathConditions.pop } /-- Merge multiple procedure evaluation results into one. @@ -32,6 +36,9 @@ Merge multiple procedure evaluation results into one. After `fixupError`, all paths through a procedure have identical variable state and path conditions — the procedure scope and its path-condition scope have been popped, leaving only the outer (global) scope which is the same on every path. +This holds for both clean and errored paths: `fixupError` pops frames and +clears `Env.error` unconditionally, so an errored procedure does not +contaminate the env handed to the next procedure (see issue #1185). The differences across paths are: - `deferred`: path-specific proof obligations (each already carries its own From caec30bd432cd0e510700c2b5d8c4425d7d0b271 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 16:03:33 -0700 Subject: [PATCH 3/8] test: add failing unit tests for Env.merge deferred preservation 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: strata-org/Strata#1185 --- .../Tests/EnvMergeErrorPreservesDeferred.lean | 108 ++++++++++++++++++ 1 file changed, 108 insertions(+) create mode 100644 StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean diff --git a/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean b/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean new file mode 100644 index 000000000..2dd9d4a44 --- /dev/null +++ b/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean @@ -0,0 +1,108 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + + +import Strata.Languages.Core.Env + +/-! ## Tests for `Env.merge` preserving deferred obligations across an error wall. + +Regression test for the second leak documented in issue #1185: when one ITE +branch errors during partial evaluation, `Env.merge` must NOT silently discard +the clean branch's already-accumulated `deferred` obligations. Pre-fix it +returned the errored side verbatim; post-fix it unions `deferred`. -/ + +--------------------------------------------------------------------- +namespace Core + +open Imperative +open Lambda + +/-- A synthetic obligation we can recognize. The exact shape doesn't matter + for this test — we only check counts and identity preservation. -/ +private def synthOblig : ProofObligation Expression := { + label := "test_oblig", + property := .assert, + assumptions := [], + obligation := LExpr.true (), + metadata := MetaData.empty +} + +/-- E1: errored, empty deferred. -/ +private def E_errored : Env := + { Env.init (empty_factory := true) with + error := some (.Misc f!"simulated PE error") } + +/-- E2: clean, one synthetic obligation. -/ +private def E_clean_one_oblig : Env := + { Env.init (empty_factory := true) with + deferred := #[synthOblig] } + +/-- E3: clean, two synthetic obligations. -/ +private def E_clean_two_oblig : Env := + { Env.init (empty_factory := true) with + deferred := #[synthOblig, synthOblig] } + +/-- A dummy condition expression. The error-path branches in `Env.merge` do + not consult `cond`, so any LExpr will do. -/ +private def dummyCond : Expression.Expr := LExpr.true () + + +/-! ### Case 1: E1 errored, E2 clean — merged carries E2's deferred -/ + +/-- +info: 1 +-/ +#guard_msgs in +#eval (Env.merge dummyCond E_errored E_clean_one_oblig).deferred.size + +/-- +info: true +-/ +#guard_msgs in +#eval (Env.merge dummyCond E_errored E_clean_one_oblig).error.isSome + + +/-! ### Case 2: E1 clean, E2 errored — merged still carries E1's deferred -/ + +/-- +info: 1 +-/ +#guard_msgs in +#eval (Env.merge dummyCond E_clean_one_oblig E_errored).deferred.size + +/-- +info: true +-/ +#guard_msgs in +#eval (Env.merge dummyCond E_clean_one_oblig E_errored).error.isSome + + +/-! ### Case 3: both clean, two obligations on each side — union has 4 -/ + +/-- +info: 4 +-/ +#guard_msgs in +#eval (Env.merge dummyCond E_clean_two_oblig E_clean_two_oblig).deferred.size + + +/-! ### Case 4: both errored — merged carries union of both sides' deferred -/ + +/-- E_err_with_oblig: errored, one synthetic obligation (e.g., from clean + statements before the error fired). -/ +private def E_err_with_oblig : Env := + { Env.init (empty_factory := true) with + error := some (.Misc f!"simulated PE error 2"), + deferred := #[synthOblig] } + +/-- +info: 2 +-/ +#guard_msgs in +#eval (Env.merge dummyCond E_err_with_oblig E_err_with_oblig).deferred.size + + +end Core From eeb0dfa3dfc3dfdf9a4db3aeb16892797de6a572 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 16:17:43 -0700 Subject: [PATCH 4/8] fix(eval): union deferred obligations across Env.merge error wall MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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: strata-org/Strata#1185 --- Strata/Languages/Core/Env.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean index 1089a1ce9..2f3716615 100644 --- a/Strata/Languages/Core/Env.lean +++ b/Strata/Languages/Core/Env.lean @@ -356,10 +356,17 @@ def Env.performMerge (cond : Expression.Expr) (E1 E2 : Env) { E1 with exprEnv := exprEnv, pathConditions := pcs, deferred := deferred } def Env.merge (cond : Expression.Expr) (E1 E2 : Env) : Env := + -- Issue #1185: when one branch errors, return the errored side's structure + -- (state, scope, error, pathConditions) but UNION `deferred` across both + -- sides. Without the union, an errored ITE branch silently discards its + -- sibling's already-accumulated proof obligations. Path conditions on the + -- non-errored side are dropped on the error path, but this is fine: the + -- merged env carries an error, so future statements short-circuit + -- (StatementEval.lean:632-633) and PCs are never consulted again. if h1: E1.error.isSome then - E1 + { E1 with deferred := E1.deferred ++ E2.deferred } else if h2: E2.error.isSome then - E2 + { E2 with deferred := E1.deferred ++ E2.deferred } else Env.performMerge cond E1 E2 (by simp_all) (by simp_all) From 2e260c4b8ec50045e8a64121e3225005189f4878 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 16:25:16 -0700 Subject: [PATCH 5/8] docs(eval): fix stale StatementEval line reference in fixupError comment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Issue #1185 commits (d55ac1c33 fixupError, eeb0dfa3d 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: strata-org/Strata#1185 --- Strata/Languages/Core/ProcedureEval.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Core/ProcedureEval.lean b/Strata/Languages/Core/ProcedureEval.lean index c1f1f4d90..ecc2bbd5c 100644 --- a/Strata/Languages/Core/ProcedureEval.lean +++ b/Strata/Languages/Core/ProcedureEval.lean @@ -23,7 +23,7 @@ open Statement Lambda LExpr def fixupError (E : Env) : Env := -- Issue #1185: pop frames AND clear `error` unconditionally. Keeping `error` -- across the procedure boundary contaminates subsequent procedures - -- (StatementEval.lean:618-619 short-circuits on Env.error.isSome). Clean-path + -- (StatementEval.lean:632-633 short-circuits on Env.error.isSome). Clean-path -- obligations already in `E.deferred` are preserved as-is — they are -- independently provable (each carries its own assumption list). { E with error := none, From d22edcf9f95ce630f8d029b149c7ae5cb1eef2d2 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 16:38:43 -0700 Subject: [PATCH 6/8] test: add CLI golden regression for 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: strata-org/Strata#1185 --- Examples/IsolatedProcEvalError.core.st | 31 +++++++++++++++++++ .../IsolatedProcEvalError.core.expected | 3 ++ 2 files changed, 34 insertions(+) create mode 100644 Examples/IsolatedProcEvalError.core.st create mode 100644 Examples/expected/IsolatedProcEvalError.core.expected diff --git a/Examples/IsolatedProcEvalError.core.st b/Examples/IsolatedProcEvalError.core.st new file mode 100644 index 000000000..758dd482b --- /dev/null +++ b/Examples/IsolatedProcEvalError.core.st @@ -0,0 +1,31 @@ +program Core; +// +// Copyright Strata Contributors +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +procedure proc_a() +{ + function foo(y : int) : int { y + 1 } +}; + +procedure proc_b() +{ + function foo(y : int) : int { y + 2 } +}; + +procedure proc_c() +{ + assert false; +}; diff --git a/Examples/expected/IsolatedProcEvalError.core.expected b/Examples/expected/IsolatedProcEvalError.core.expected new file mode 100644 index 000000000..f14504da1 --- /dev/null +++ b/Examples/expected/IsolatedProcEvalError.core.expected @@ -0,0 +1,3 @@ +Successfully parsed. +IsolatedProcEvalError.core.st(30, 2) [assert_0]: ❌ fail +Finished with 0 goals passed, 1 failed. From 490d5cbb8970b0683f9725209ad22a519aa21b63 Mon Sep 17 00:00:00 2001 From: David Deng Date: Tue, 19 May 2026 16:56:38 -0700 Subject: [PATCH 7/8] test/docs(eval): document Env.merge both-errored asymmetry MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Env.merge fix from eeb0dfa3d 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: strata-org/Strata#1185 --- Strata/Languages/Core/Env.lean | 4 ++- .../Tests/EnvMergeErrorPreservesDeferred.lean | 30 +++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean index 2f3716615..3a7fe6a2c 100644 --- a/Strata/Languages/Core/Env.lean +++ b/Strata/Languages/Core/Env.lean @@ -362,7 +362,9 @@ def Env.merge (cond : Expression.Expr) (E1 E2 : Env) : Env := -- sibling's already-accumulated proof obligations. Path conditions on the -- non-errored side are dropped on the error path, but this is fine: the -- merged env carries an error, so future statements short-circuit - -- (StatementEval.lean:632-633) and PCs are never consulted again. + -- (StatementEval.lean:632-633) and PCs are never consulted again. When both + -- sides error, E1's error value is kept (the choice is arbitrary; both sides + -- carry an error flag and the caller's short-circuit fires regardless). if h1: E1.error.isSome then { E1 with deferred := E1.deferred ++ E2.deferred } else if h2: E2.error.isSome then diff --git a/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean b/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean index 2dd9d4a44..e58367bda 100644 --- a/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean +++ b/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean @@ -105,4 +105,34 @@ info: 2 #eval (Env.merge dummyCond E_err_with_oblig E_err_with_oblig).deferred.size +/-! ### Case 5: both errored with DIFFERENT errors — E1's error is kept -/ + +private def E_err_a : Env := + { Env.init (empty_factory := true) with + error := some (.Misc f!"error A"), + deferred := #[synthOblig] } + +private def E_err_b : Env := + { Env.init (empty_factory := true) with + error := some (.Misc f!"error B"), + deferred := #[synthOblig] } + +-- Both errored: deferred is unioned (size 2). +/-- +info: 2 +-/ +#guard_msgs in +#eval (Env.merge dummyCond E_err_a E_err_b).deferred.size + +-- E1 wins on the error value when both error: arbitrary controller choice, not +-- a soundness requirement (the merged env carries an error flag and +-- short-circuits regardless). The actual value is `some "[ERROR] error A"`, +-- not `some "[ERROR] error B"`, despite both inputs erroring. +/-- +info: some "[ERROR] error A" +-/ +#guard_msgs in +#eval ((Env.merge dummyCond E_err_a E_err_b).error.map fun e => f!"{e}").map fun f => Std.Format.pretty f + + end Core From bd672b49767cafc5094ac121d3facef9ab61c641 Mon Sep 17 00:00:00 2001 From: David Deng Date: Wed, 20 May 2026 11:06:29 -0700 Subject: [PATCH 8/8] docs(eval): drop issue #1185 references and tighten comments MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- Strata/Languages/Core/Env.lean | 15 ++++------ Strata/Languages/Core/ProcedureEval.lean | 13 ++++----- .../Tests/EnvMergeErrorPreservesDeferred.lean | 15 ++++------ .../Core/Tests/ProgramEvalErrorIsolation.lean | 28 +++++++++---------- 4 files changed, 31 insertions(+), 40 deletions(-) diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean index 3a7fe6a2c..ef2a81b88 100644 --- a/Strata/Languages/Core/Env.lean +++ b/Strata/Languages/Core/Env.lean @@ -356,15 +356,12 @@ def Env.performMerge (cond : Expression.Expr) (E1 E2 : Env) { E1 with exprEnv := exprEnv, pathConditions := pcs, deferred := deferred } def Env.merge (cond : Expression.Expr) (E1 E2 : Env) : Env := - -- Issue #1185: when one branch errors, return the errored side's structure - -- (state, scope, error, pathConditions) but UNION `deferred` across both - -- sides. Without the union, an errored ITE branch silently discards its - -- sibling's already-accumulated proof obligations. Path conditions on the - -- non-errored side are dropped on the error path, but this is fine: the - -- merged env carries an error, so future statements short-circuit - -- (StatementEval.lean:632-633) and PCs are never consulted again. When both - -- sides error, E1's error value is kept (the choice is arbitrary; both sides - -- carry an error flag and the caller's short-circuit fires regardless). + -- When one branch errors, take that side's structure (state, scope, error, + -- pathConditions) but UNION `deferred`, so the sibling's already-accumulated + -- obligations survive the error wall. Dropping the non-errored side's path + -- conditions is sound: the merged env carries an error and downstream + -- evaluation short-circuits before PCs are consulted again. When both sides + -- error, E1's error value wins arbitrarily — the error flag is what matters. if h1: E1.error.isSome then { E1 with deferred := E1.deferred ++ E2.deferred } else if h2: E2.error.isSome then diff --git a/Strata/Languages/Core/ProcedureEval.lean b/Strata/Languages/Core/ProcedureEval.lean index ecc2bbd5c..f781ed828 100644 --- a/Strata/Languages/Core/ProcedureEval.lean +++ b/Strata/Languages/Core/ProcedureEval.lean @@ -21,11 +21,10 @@ open Std open Statement Lambda LExpr def fixupError (E : Env) : Env := - -- Issue #1185: pop frames AND clear `error` unconditionally. Keeping `error` - -- across the procedure boundary contaminates subsequent procedures - -- (StatementEval.lean:632-633 short-circuits on Env.error.isSome). Clean-path - -- obligations already in `E.deferred` are preserved as-is — they are - -- independently provable (each carries its own assumption list). + -- Clearing `error` and popping frames must be unconditional: a leftover + -- error short-circuits the next procedure's evaluation in `StatementEval`. + -- Clean-path obligations in `E.deferred` survive — each carries its own + -- assumptions and is independently provable. { E with error := none, exprEnv.state := E.exprEnv.state.pop, pathConditions := E.pathConditions.pop } @@ -35,10 +34,10 @@ Merge multiple procedure evaluation results into one. After `fixupError`, all paths through a procedure have identical variable state and path conditions — the procedure scope and its path-condition scope have been -popped, leaving only the outer (global) scope which is the same on every path. +popped, leaving only the outer (global) scope, which is the same on every path. This holds for both clean and errored paths: `fixupError` pops frames and clears `Env.error` unconditionally, so an errored procedure does not -contaminate the env handed to the next procedure (see issue #1185). +contaminate the env handed to the next procedure. The differences across paths are: - `deferred`: path-specific proof obligations (each already carries its own diff --git a/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean b/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean index e58367bda..44e07f256 100644 --- a/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean +++ b/StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean @@ -9,10 +9,10 @@ import Strata.Languages.Core.Env /-! ## Tests for `Env.merge` preserving deferred obligations across an error wall. -Regression test for the second leak documented in issue #1185: when one ITE -branch errors during partial evaluation, `Env.merge` must NOT silently discard -the clean branch's already-accumulated `deferred` obligations. Pre-fix it -returned the errored side verbatim; post-fix it unions `deferred`. -/ +When one ITE branch errors during partial evaluation, `Env.merge` must NOT +silently discard the clean branch's already-accumulated `deferred` +obligations. The merge unions `deferred` across the error wall so those +obligations still reach the verifier. -/ --------------------------------------------------------------------- namespace Core @@ -117,17 +117,14 @@ private def E_err_b : Env := error := some (.Misc f!"error B"), deferred := #[synthOblig] } --- Both errored: deferred is unioned (size 2). /-- info: 2 -/ #guard_msgs in #eval (Env.merge dummyCond E_err_a E_err_b).deferred.size --- E1 wins on the error value when both error: arbitrary controller choice, not --- a soundness requirement (the merged env carries an error flag and --- short-circuits regardless). The actual value is `some "[ERROR] error A"`, --- not `some "[ERROR] error B"`, despite both inputs erroring. +-- E1 wins arbitrarily — the merged env carries an error flag either way, +-- so downstream short-circuits regardless of which side's value is kept. /-- info: some "[ERROR] error A" -/ diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean b/StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean index 92feeab5e..ffd90de39 100644 --- a/StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean +++ b/StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean @@ -9,20 +9,19 @@ import Strata.Languages.Core.Verifier /-! ## Tests for cross-procedure error isolation in `Program.eval` -Regression tests for issue #1185 — when one procedure's partial evaluation -errors (e.g., function-name collision), the error must NOT contaminate -subsequent procedures' evaluation. Each procedure's evaluation should start -from a clean `Env.error` state. -/ +When one procedure's partial evaluation errors (e.g., function-name +collision), the error must NOT contaminate subsequent procedures' +evaluation. Each procedure's evaluation should start from a clean +`Env.error` state. -/ --------------------------------------------------------------------- namespace Strata -/-- Issue #1185 exact repro. proc_a registers `foo`; proc_b's redefinition of - `foo` raises a partial-evaluation error; proc_c's `assert false` MUST still - be evaluated and reported as failing. Pre-fix: "All 0 goals passed" (the - soundness bug). Post-fix: assert_0 reports ❌ fail. -/ -private def issue1185Repro := +/-- proc_a registers `foo`; proc_b's redefinition of `foo` raises a + partial-evaluation error; proc_c's `assert false` MUST still be + evaluated and reported as failing. -/ +private def collisionThenAssertFalse := #strata program Core; @@ -50,13 +49,12 @@ Property: assert Result: ❌ fail -/ #guard_msgs in -#eval verify issue1185Repro (options := .quiet) +#eval verify collisionThenAssertFalse (options := .quiet) -/-- Reorder regression: proc_c first, then the colliding pair. This already - worked pre-fix (the issue's "Reordering Rescues the Obligation" section). - Protect against regression. -/ -private def issue1185Reordered := +/-- Reordered variant: proc_c runs before the colliding pair. Guards against + a regression where ordering becomes load-bearing again. -/ +private def assertFalseThenCollision := #strata program Core; @@ -84,7 +82,7 @@ Property: assert Result: ❌ fail -/ #guard_msgs in -#eval verify issue1185Reordered (options := .quiet) +#eval verify assertFalseThenCollision (options := .quiet) end Strata