`Program.eval` propagates `Env.error` across procedures, silently dropping obligations from later procedures

[PROgram52bc]

Summary

Strata/Languages/Core/ProgramEval.lean:Program.eval threads a single Env through every procedure declaration in source order. If any procedure's evaluation sets Env.error, the error is left in place by Procedure.fixupError (Strata/Languages/Core/ProcedureEval.lean:23-27) and the errored env is passed as the input env to subsequent procedures. Inside Statement.eval and evalAuxGo, every statement short-circuits when env.error.isSome is true (Strata/Languages/Core/StatementEval.lean:625-637), so subsequent procedures' bodies produce no deferred obligations. extractObligations then walks empty bodies and reports All 0 goals passed, even when the affected procedures contain asserts that should produce failing VCs.

The error is never surfaced — there is no warning in stdout, in --profile output, or in --verbose output. The user sees a clean green pass.

Severity

Soundness. A real assertion that should fail is silently reported as passing whenever the verifier happens to evaluate a contaminating procedure earlier in the program. The trigger is not exotic — the funcDecl conflict in the reproduction below is a 17-line program that uses only documented Core syntax.

Reproduction

Save the following as repro.core.st and run strata verify --check-mode deductive repro.core.st:

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

Output:

Successfully parsed.
All 0 goals passed.

proc_c contains a literal assert false and there is no enclosing assumption strong enough to discharge it. The verifier should report a failing VC. Instead it reports a clean pass.

Why

proc_a is evaluated first and adds foo to Env.exprEnv's factory via the funcDecl arm of Statement.evalOneStmt/evalAuxGo (Strata/Languages/Core/StatementEval.lean:609-625). proc_b is then evaluated against the same threaded Env; its function foo declaration calls Env.addFactoryFunc foo (Strata/Languages/Core/Env.lean:241-247), which fails because foo is already in the factory. evalAuxGo writes Env.error := some (.Misc "A function of name foo already exists! …") (StatementEval.lean:625). proc_c is then evaluated against the errored env; every command short-circuits on env.error.isSome (StatementEval.lean:637), so the assert false never reaches deferObligation and proc_c produces zero deferred obligations. Program.eval returns this single accumulated env to toCoreProofObligationProgram (Strata/Languages/Core/Core.lean:135-152), which extracts an empty obligations list, and the verifier prints All 0 goals passed.

Empirical confirmation

A trace dbg_trace added at ProgramEval.lean:62 to print Env.error and Env.deferred.size after each Procedure.eval:

[ProgramEval] after proc_a: error=none                                   deferred.size=0
[ProgramEval] after proc_b: error=Misc(A function of name foo …)         deferred.size=0
[ProgramEval] after proc_c: error=Misc(A function of name foo …)         deferred.size=0

proc_b's funcDecl conflict sets the error; proc_c's eval inherits it and contributes no obligations. deferred.size stays at 0 through every subsequent procedure.

Reordering rescues the obligation

If proc_c is moved ahead of the conflicting pair:

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

Output:

Successfully parsed.
repro.core.st(7, 2) [assert_0]: ❌ fail
Finished with 0 goals passed, 1 failed.

Same procedures, same error — but proc_c's obligation is collected before the error is set, so it survives.

Trace with reordered input

[ProgramEval] after proc_c: error=none                                   deferred.size=1
[ProgramEval] after proc_a: error=none                                   deferred.size=1
[ProgramEval] after proc_b: error=Misc(A function of name foo …)         deferred.size=1

Root cause

Strata/Languages/Core/ProgramEval.lean walks program.decls sequentially:

| .proc proc _md =>
  let (E, procStats) := Procedure.eval declsE proc
  go rest E (stats.merge procStats)

The post-eval Env is passed as the input env for the next procedure.

Procedure.fixupError (ProcedureEval.lean:23-27) intentionally preserves the error:

def fixupError (E : Env) : Env :=
  match E.error with
  | none => { E with exprEnv.state := E.exprEnv.state.pop,
                     pathConditions := E.pathConditions.pop }
  | some _ => E

Combined with evalAuxGo's if good.isEmpty then (Ewns, noStats, …) short-circuit (StatementEval.lean:637), every command in every subsequent procedure becomes a no-op once any earlier procedure has errored. The error is never surfaced to the user — it sits in Env, silently shaping the rest of the run.

Where the error is swallowed

Three distinct consumers each have an opportunity to surface the error and none of them do.

1. Procedure.fixupError (Strata/Languages/Core/ProcedureEval.lean:23-27). First chance to drop the error. The clean path pops the procedure's scope frame and returns; the error path returns the env unchanged:

def fixupError (E : Env) : Env :=
  match E.error with
  | none => { E with exprEnv.state := E.exprEnv.state.pop,
                     pathConditions := E.pathConditions.pop }
  | some _ => E   -- error preserved, scope NOT popped, no signal raised

Doesn't clear error, doesn't lift it into an Except, doesn't even pop the procedure's scope frame. The error rides along inside the env.

2. Program.eval's go recursion (Strata/Languages/Core/ProgramEval.lean:61-63). Where the contamination becomes cross-procedural:

| .proc proc _md =>
  let (E, procStats) := Procedure.eval declsE proc
  go rest E (stats.merge procStats)   -- passes errored E to next proc

The function's return type is Except Strata.DiagnosticModel (List Env × Statistics). The Except channel is reserved for DDM-level failures: axiom-stack mismatch (line 50), top-level function/recFuncBlock factory conflict (lines 66, 71). Per-procedure PE errors land in Env.error instead, and go doesn't promote them into the Except. So Program.eval returns .ok even when every later procedure was contaminated.

3. toCoreProofObligationProgram (Strata/Languages/Core/Core.lean:135-152). The final swallow point. After Program.eval:

let (pEs, evalStats) ← Program.eval E
...
let postEvalEnv ← match pEs with
  | [e] => pure e
  | _ => throw (DiagnosticModel.fromMessage s!"... expected exactly 1 evaluation Env, got {pEs.length}")
let blocks := postEvalEnv.deferred.toList.map fun ob => ...

Reads postEvalEnv.deferred to build the obligations program; never inspects postEvalEnv.error. The error has been sitting in Env.error since StatementEval.lean:622-625, but this consumer walks past it. Without the deferred obligations the contaminated procedures would have produced, extractObligations walks empty bodies and the verifier prints All N goals passed.

The pattern across all three: the error is real data sitting in a field, but no consumer ever checks Env.error. Inside evalAuxGo itself the error short-circuits subsequent statements (StatementEval.lean:637), but at every procedure or program-level boundary above that, it is read past silently.

The funcDecl conflict above is the cleanest user-facing trigger that passes the upstream guards (callElim's pre-PE existence check, precondElim's already in factory. check). The contamination mechanism, however, is independent of the trigger — any current or future PE error path has the same effect.

Suggested fix

Reset Env.error (and the per-procedure scope state) at the boundary between procedures so per-procedure failures stay local to that procedure. Two reasonable places:

1. In Procedure.eval's return: drop error and pop the leftover procedure scope before handing the env back. fixupError already does the no-error case; the question is whether to also pop on the error path or to just clear error so the next procedure starts clean.

2. In Program.eval's go: between procedures, take the input env's factory, program, top-frame pathConditions, and any axioms/distincts already accumulated, and discard everything else (error, leftover scope frames). Ensures cross-procedure independence by construction.

Either way, the user should also see some signal that a procedure errored during PE — at minimum a stat (Evaluator.peErrorByProc: …), ideally a stderr warning. Today the error is silently dropped on the floor and a clean-looking All N goals passed is the only output.

Files involved

• Strata/Languages/Core/ProgramEval.lean:61-63 — the threading.
• Strata/Languages/Core/ProcedureEval.lean:23-27 — fixupError keeps errors.
• Strata/Languages/Core/StatementEval.lean:625-637 — evalAuxGo's good.isEmpty short-circuit.
• Strata/Languages/Core/StatementEval.lean:609-625 — funcDecl evaluation, where the empirical trigger above writes Env.error.
• Strata/Languages/Core/Env.lean:358-364 — Env.merge correctly short-circuits to error envs, which makes ITE branches contaminate the merged env the same way procedures contaminate their successors.