fix(core): isolate path conditions at the procedure boundary (#1391)

Fixes #1390.

**Problem:** `Program.eval` threads one `Env` through all procedures. A
structured `exit` out of a labeled block doesn't pop its path-condition
frames (`.block` exit pops `exprEnv.state`, not `pathConditions`; the
exiting path bypasses `Env.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-final `return` to
`exit "$body"`, so ordinary early-return code hits it.

**Fix:** reset `pathConditions` to the pre-procedure state in the
`.proc` fold (deferred obligations and fresh names carry forward). A
`.block`-level reset was rejected — breaks fall-through.

**Test:** `ProcedurePathConditionIsolation` — unsatisfiable-precondition
`first` + structured `exit`, `second`'s `assert false` must fail. Red
without the fix, green with it; full `StrataTest` green (539). Control
matrix + scope in #1390.

Author: fabiomadge

Strata/Languages/Core/ProgramEval.lean

@@ -54,6 +54,12 @@ def eval (E : Env) : Except Strata.DiagnosticModel (List Env × Statistics) :=
 
     | .proc proc _md =>
       let (E, procStats) := Procedure.eval declsE proc
+      -- Reset path conditions to the pre-procedure state so a procedure's
+      -- assumptions don't leak into later ones: a structured `exit` bypasses
+      -- `Env.merge` and leaves its frames unpopped, which would otherwise be
+      -- threaded into the next procedure (strata-org/Strata#1390). Deferred
+      -- obligations and fresh names carry forward.
+      let E := { E with pathConditions := declsE.pathConditions }
       go rest E (stats.merge procStats)
 
     | .func func _ => do

StrataTest/Languages/Core/Tests/ProcedurePathConditionIsolation.lean

@@ -0,0 +1,57 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+meta import Strata.Languages.Core
+import StrataDDM.Integration.Lean.HashCommands
+
+/-
+Regression test for strata-org/Strata#1390.
+
+A structured `exit` bypasses `Env.merge`, so a procedure's path conditions used
+to leak into later procedures; a contradictory leaked set then proved their
+false obligations vacuously. `first` has an unsatisfiable precondition + a
+structured `exit`; `second`'s `assert false` must fail, not silently pass.
+-/
+
+meta section
+open StrataDDM (Program)
+
+namespace Strata
+
+def leakViaStructuredExit : Program :=
+#strata
+program Core;
+
+procedure first(n : int)
+spec {
+  requires [c1]: (n >= 1);
+  requires [c2]: (n <= 0);
+}
+{
+  body: {
+    if (n > 5) { exit body; }
+  }
+};
+
+procedure second()
+{
+  assert [bad]: false;
+};
+#end
+
+/--
+info:
+Obligation: bad
+Property: assert
+Result: ❌ fail
+-/
+#guard_msgs in
+#eval Core.verify leakViaStructuredExit (options := .quiet)
+
+end Strata
+
+end