fix(eval): isolate Env.error at procedure boundary (issue #1185)

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;
+};

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.

Strata/Languages/Core/Env.lean

@@ -356,10 +356,16 @@ 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 :=
+  -- 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
+    { 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)
 

Strata/Languages/Core/ProcedureEval.lean

@@ -21,17 +21,23 @@ 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
+  -- 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 }
 
 /--
 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.
 The differences across paths are:
 
 - `deferred`: path-specific proof obligations (each already carries its own

StrataTest/Languages/Core/Tests/EnvMergeErrorPreservesDeferred.lean

@@ -0,0 +1,135 @@
+/-
+  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.
+
+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
+
+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
+
+
+/-! ### 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] }
+
+/--
+info: 2
+-/
+#guard_msgs in
+#eval (Env.merge dummyCond E_err_a E_err_b).deferred.size
+
+-- 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"
+-/
+#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

StrataTest/Languages/Core/Tests/ProgramEvalErrorIsolation.lean

@@ -0,0 +1,88 @@
+/-
+  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`
+
+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
+
+
+/-- 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;
+
+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 collisionThenAssertFalse (options := .quiet)
+
+
+/-- 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;
+
+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 assertFalseThenCollision (options := .quiet)
+
+
+end Strata