docs(core): trim path-condition-isolation comments

Author: fabiomadge

Strata/Languages/Core/ProgramEval.lean

@@ -54,14 +54,11 @@ 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: a procedure's
-      -- preconditions and in-scope assumptions must not leak into later
-      -- procedures. A structured `exit` out of a labeled block does not pop the
-      -- path-condition frames it accumulated (the exiting path bypasses
-      -- `Env.merge`), so without this reset those frames would be threaded into
-      -- the next procedure and verify its obligations against an inconsistent
-      -- context. Everything else (deferred obligations, fresh-name set) carries
-      -- forward unchanged. See strata-org/Strata#1390.
+      -- 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)
 

StrataTest/Languages/Core/Tests/ProcedurePathConditionIsolation.lean

@@ -11,17 +11,10 @@ import StrataDDM.Integration.Lean.HashCommands
 /-
 Regression test for strata-org/Strata#1390.
 
-`Program.eval` threads one `Env` through every procedure. A path that leaves a
-labeled block via a structured `exit` does not get its path conditions popped
-(the exiting path bypasses `Env.merge`), so a procedure's preconditions and
-in-scope assumptions used to leak into the next procedure's verification
-context. When the leaked set was contradictory, the next procedure proved false
-obligations vacuously — a silent green pass.
-
-`first` has an unsatisfiable precondition (`n >= 1` and `n <= 0`) and a
-non-final structured `exit`. `second` has no spec; its `assert false` must be
-reported as failing, not silently accepted. Before the fix this reported
-`✅ pass`.
+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