Structured pipeline diagnostics with PipelineM, phase timing, and --metrics JSONL

[joehendrix]

Motivation

The pipeline previously had no unified infrastructure for diagnostics or
timing. Warnings were handled ad-hoc (some printed to stderr, some silently
dropped), phase timing was manual and inconsistent, and the only structured
output (--warning-summary) wrote a single JSON blob at the end — useless
if the process was killed by a timeout. There was also no distinction between
fatal and non-fatal errors, so callers couldn't tell whether a result was
trustworthy.

This PR introduces PipelineContext/PipelineM as a shared backbone that
gives every pipeline phase consistent behavior: categorized diagnostics,
nested phase timing, fatal-error abort, and streaming metrics output that
survives timeouts.

Summary

• Introduce PipelineContext and PipelineM for structured diagnostic
  accumulation and phase timing across the entire pipeline
• Replace ad-hoc profileStep/startPhase with withPhase combinator that
  handles nesting, timing, and profile output via try/finally
• Add withRepeatedPhase for iteration-level timing (preprocess, smtEncode,
  solver) that accumulates count+duration and reports as [profile] lines
• Replace --warning-summary (single JSON blob) with --metrics <file>
  (streaming JSONL, flushed per-record for timeout resilience)
• Add --verbose program dumps: prints intermediate Laurel and Core programs
  with ---- BEGIN/END ---- delimiters for programmatic parsing
• Refactor module resolution: fatal errors on invalid/missing modules,
  unified resolveModules for dispatch, auto-resolved, and explicit modules
• Fix pyResolveOverloads to print errors from pipeline context on failure
• Split Messages.lean into data types (Messages.lean) and runtime
  infrastructure (Context.lean)
• Move Python-specific MessageKind constants to
  Languages/Python/Specs/MessageKind.lean

PipelineContext and PipelineM

PipelineContext is a structure carrying immutable config (outputMode,
profilePipeline) plus mutable state as individual IO.Ref fields:

• messagesRef — accumulated PipelineMessage diagnostics
• toolErrorsRef / userCodeErrorsRef — bucketed by impact for fast access
• currentPhaseRef — current position in the phase hierarchy (managed via
  push/pop)
• repeatedDepthRef — nesting depth of withRepeatedPhase scopes (when > 0,
  withPhase aggregates silently)
• phaseStateRef — per-phase scoped state bundling repeated-phase aggregation
  and message counts (saved/restored atomically on phase entry/exit)
• metricsHandle — optional file handle for streaming JSONL metrics

Because all state is in IO.Refs, any monad with BaseIO access can use
pipeline capabilities by passing a PipelineContext value directly —
withPhase is polymorphic over the monad ([MonadLiftT BaseIO m]).

PipelineM is defined as:

abbrev PipelineM := ReaderT PipelineContext (EIO Unit)

The EIO Unit base ensures that fatal errors (configuration errors,
internal errors, user code issues) are impossible to silently ignore — they
throw (), aborting the pipeline. Non-fatal diagnostics (warnings, known
limitations) are added to messagesRef and execution continues. Callers
that want to attempt recovery (e.g., to gather more diagnostics) can catch
the exception, but should rethrow to avoid proceeding with invalid state.

The top-level runner catches the exception and still returns all accumulated
messages — so the caller always gets complete diagnostics regardless of how
the pipeline terminated.

Phase tracking state machine

The phase system operates in two modes controlled by repeatedDepthRef:

• Mode N (normal, depth = 0): withPhase prints [start]/[end] in
  profile mode and emits JSONL timing metrics.
• Mode R (repeated, depth > 0): withPhase silently aggregates timing
  into phaseStateRef.repeatedPhases — no print, no individual metrics.

withRepeatedPhase increments repeatedDepthRef on entry and decrements
on exit. withPhase never changes the depth — it inherits the mode and
behaves accordingly.

Key invariants:

• currentPhaseRef always reflects the innermost active scope's full path
• phaseStateRef is scoped: saved on entry, restored on exit (no leakage)
• In mode R, all timing flows through phaseStateRef.repeatedPhases only

--metrics <file> (replaces --warning-summary)

Writes streaming JSONL (one JSON object per line, flushed immediately after
each record). If the process is killed mid-pipeline, all records should remain.

Record types:

• timing — phase start/end in ms, with optional count for aggregated phases
• diagnostic — pipeline messages with phase, file, category, impact, location
• outcome — result/exit_code/total_ms, written last (absence = killed)

Example output:

{"type":"timing","phase":"pythonAndSpecToLaurel","start_ms":0,"end_ms":97}
{"type":"diagnostic","phase":"pythonAndSpecToLaurel.resolveAndBuildPrelude","file":"specs/builtins.ion","category":"unsupportedUnion","impact":"knownLimitation","message":"unsupported overload form for 'dict.update'"}
{"type":"timing","phase":"verification.vcDischarge.solver","start_ms":0,"end_ms":1102,"count":12}
{"type":"outcome","result":"verified","exit_code":0,"total_ms":1830}

--verbose program dumps

When outputMode == .verbose, the pipeline prints intermediate programs to
stdout with delimiters for programmatic parsing:

---- BEGIN Laurel Program ----
<full Laurel program text>
---- END Laurel Program ----
---- BEGIN Core Program ----
<full Core program text>
---- END Core Program ----

Module resolution refactoring

• resolveModuleEntry now takes a parsed ModuleName (not a string)
• Single resolveModules handles dispatch, auto-resolved, and explicit modules
• invalidModuleName changed from internalWarning to configurationError (fatal)
• Merged missingDispatchModule + missingExplicitPySpec into missingPySpecModule
• Eliminated duplicate message scenario where both invalid-name and missing-module
  errors fired for the same input

pyResolveOverloads error handling

When readDispatchOverloads encounters a fatal error (e.g., nonexistent file),
the command now reads pctx.messagesRef and prints all accumulated messages
to stderr before exiting with a non-zero code — instead of silently yielding
empty results.

Profile output format

--profile emits structured [start]/[end]/[profile] lines to stdout:

[start] pythonAndSpecToLaurel (time: 0ms)
  [start] readPythonIon (time: 0ms)
  [end] readPythonIon (time: 2ms)
  [start] resolveAndBuildPrelude (time: 2ms)
  [end] resolveAndBuildPrelude (time: 97ms)
  [warnings] resolveAndBuildPrelude: 2 unsupportedUnion
[end] pythonAndSpecToLaurel (time: 97ms)
[start] verification (time: 105ms)
  [start] vcDischarge (time: 320ms)
    [profile] preprocess (×12, total: 45ms, avg: 3ms)
    [profile] solver (×12, total: 1102ms, avg: 91ms)
  [end] vcDischarge (time: 1185ms)
[end] verification (time: 1185ms)

Design: impact drives behavior

Each MessageKind has a MessageImpact that determines pipeline behavior:

Impact	Fatal?	Meaning
configurationError	yes	Invalid arguments or unreadable on-disk pyspecs
internalError	yes	Unexpected failure preventing output
userCodeIssue	yes	Issue in the user's source code
internalWarning	no	Unexpected condition that didn't prevent output
knownLimitation	no	Documented gap in modeling

Note: emitMessageAndAbort is the function that aborts — callers choose
whether to abort. A caller may use emitMessage (continues) and check
isFatal at phase boundaries for custom abort strategies.

Not addressed: [statistics] output

The [statistics] lines (transform counters like Evaluator.simulatedStmts,
FilterProcedures.erasedProcedures) are orthogonal to phase timing. They
currently bypass PipelineContext — printed via bare IO.println in
Core.verify and StrataMainLib.lean — so they don't respect phase nesting
or indentation. Integrating statistics into the phase system is future work.

Key files changed

• Strata/Pipeline/Messages.lean — pure data types: Phase, MessageImpact, MessageKind, PipelineMessage
• Strata/Pipeline/Context.lean — runtime: PipelineContext, PipelineM, withPhase, withRepeatedPhase, emitMetric, OutputMode
• Strata/Languages/Python/Specs/MessageKind.lean — Python-specific MessageKind constants
• Strata/Pipeline/PyAnalyzeLaurel.lean — top-level pipeline orchestration, --verbose program dumps, metricsHandle threading
• Strata/Languages/Core/Verifier.lean — replaced manual timing with withRepeatedPhase
• Strata/Languages/Laurel/LaurelCompilationPipeline.lean — replaced profileStep with withPhase
• Strata/Languages/Python/PySpecPipeline.lean — fatal abort via throw, module resolution refactor, diagnostic metric emission
• StrataMainLib.lean — --metrics flag, outcome record emission, error printing in pyResolveOverloads
• StrataTest/Pipeline/PhaseTimingTest.lean — phase timing integration tests

[tautschnig]

verboseWarnings : Bool := false is a hardcoded constant — there's no way for users to enable verbose warnings without editing source code. This should either be:

1. A CLI flag (e.g., --verbose-pyspec-warnings) passed through to pythonAndSpecToLaurel, or
2. Controlled by the existing --verbose flag that's already available in the pipeline

The existing quiet parameter already suppresses the count line. Adding a verbose parameter (or reusing the one from the caller) would be cleaner than a dead constant.

[tautschnig]

@keyboardDrummer-bot Please resolve git conflicts.

[tautschnig]

Main concerns

1. Real regression in pyResolveOverloadsCommand (see inline on StrataMain.lean:943). The old EIO String-returning readDispatchOverloads surfaced dispatch-file read failures via exitFailure. The new BaseIO (OverloadTable × PipelineState) version emits a fatal .pySpecReadError into the state and returns an empty table — but the command tuple-destructures (overloads, _), throwing the state away. A broken dispatch file now silently produces an empty overload table and a zero-module stdout.
2. shouldAbort is a load-bearing invariant that the type system doesn't enforce. buildPySpecLaurel and readDispatchOverloads return (α × PipelineState) with α constructed via Inhabited.default on fatal paths (return default in resolveAndBuildLaurelPrelude). Callers that forget to check shouldAbort silently proceed with empty/zero results — pyResolveOverloadsCommand is one case today. It would be worth either (a) returning a sum (PipelineRun α := .ok α | .aborted (msgs : Array PipelineMessage)), or (b) wrapping BaseIO (α × PipelineState) in a helper runPipelineOrThrow : … → EIO String α for callers that want legacy semantics, and documenting loudly in the structure docstring that a PySpecLaurelResult returned alongside shouldAbort = true is meaningless. See inline.
3. Duplicate warnings for invalid module names. resolveModuleEntry emits .invalidModuleName on parse failure and returns none; resolveAndBuildLaurelPrelude then emits .missingDispatchModule / .missingExplicitPySpec for every none. So an invalid name in --dispatch yields two messages (one internalWarning + one configurationError) where one is enough. See inline.
4. LT / Ord instances disagree on Phase and MessageKind. Both types derive Ord (lex over all fields) and hand-roll LT (lex over only some fields). On MessageKind the hand-rolled LT ignores the impact field entirely, so compare a b = .eq can coexist with a ≠ b. The qsort usage in toSummaryJson uses the hand-rolled LT, which is fine, but the two orderings should agree. Suggest dropping the derived Ord (or dropping the hand-rolled LT and using ltOfOrd).
5. MessageImpact.isFatal has no proof/test coverage and the (impact, isFatal) contract lives in three places. The mapping impact→fatal is encoded in: the isFatal function, the impact field of each MessageKind constant, and readers of isFatal in emitMessage. Adding a new impact level is a three-file change with no compiler help. At minimum, please add a #guard-level lock-in (see inline) and/or a small theorem bank (also inline).

Testing / proof suggestions

• emitMessage/addMessages behavioral locks (small state-threading theorems — see PipelineMessages.lean inline).
• Snapshot / roundtrip for PipelineMessage.toSummaryJson so the external JSON schema can't drift silently (inline).
• Regression test for the pyResolveOverloadsCommand dispatch-file-read failure path (bullet #1).
• Regression test that a bad --dispatch <modname> produces one message and an exit with a single configurationError, not two overlapping warnings (bullet #3).
• Small theorems on Phase and MessageKind orderings (∀ a b, a < b ↔ compare a b = .lt to lock in LT/Ord agreement).

Refactoring notes

• mergeOverloads: the old Option-based paramName <|> n.paramName semantics are now gone (the field is String), which is an improvement; the new code does emit .overloadParamNameDisagreement when two registrations conflict, which is great.
• PipelineM: StateT PipelineState BaseIO means any BaseIO effect can be mixed in. In practice only readDDM escapes into it. Consider narrowing (e.g. ExceptT Abort (StateT … BaseIO)) so the abort control flow is visible in types and return default isn't needed.
• Consider consolidating MessageImpact and PipelineError (in PySpecPipeline.lean): today the PipelineError.userCode branch exits with code 1 (hard fatal) while MessageImpact.userCodeIssue is non-fatal. The semantic gap is defensible but undocumented; a comment explaining why the two vocabularies exist would help.

[tautschnig]

Substantial pipeline refactor. The PR delivers what the description promises: PipelineContext + PipelineM with proper diagnostic accumulation, withPhase / withRepeatedPhase replacing ad-hoc profileStep, streaming JSONL metrics via --metrics, fatal-abort via EIO Unit, and cleaner module resolution. lake build passes. The structural-output-survives-timeout property is genuinely useful.

1. The "impact drives behavior" claim in the PR description isn't enforced by code. The PR body's table says:

| Impact                | Fatal? |
| configurationError    | yes    |
| internalError         | yes    |
| internalWarning       | no     |
| knownLimitation       | no     |
| userCodeIssue         | no     |

But whether a message aborts depends entirely on whether the caller uses emitFatalMessage vs emitMessage (see Messages.lean:461-481). Nothing in PipelineM enforces the mapping:

• emitFatalMessage .overloadResolveWarning msg … would throw despite the .internalWarning impact.
• emitMessage .internalError msg … would accumulate a fatal-impact message without aborting.

Today's in-tree callers are consistent with the table, but the invariant is tribal knowledge. Two low-cost options:

• Derive behavior from impact — make emitMessage check if kind.impact.isFatal then throw () and drop emitFatalMessage entirely. This makes the table the contract.
• Retain both but guard — emitFatalMessage panic!s on non-fatal impact; emitMessage panic!s on fatal impact. Keeps the current call-site readability; enforces the invariant.

Related: MessageImpact.isError (Messages.lean:73) returns true for .userCodeIssue but the PR body's table marks it non-fatal. isError here means "display as 'error' tag", not "abort the pipeline". Calling the predicate isError for a display concern and leaving the abort concern nameless is confusing — consider displayAsError + isFatal as two explicit predicates.

2. PipelineM = ReaderT PipelineContext (EIO Unit) throws () on abort. The unit-typed error channel means any caller doing try … catch e => … gets zero information from e — they have to go read ctx.messagesRef to reconstruct what happened. Two suggestions:

• Throw a typed error (PipelineAbort with a reason or message ref) so catch is self-documenting.
• Or document the ()-throwing convention explicitly in the PipelineM docstring, including the required "inspect messagesRef on abort" recovery pattern. Currently the docstring says "throws () to abort" but not how a caller should react.

3. metricsHandle is never explicitly closed. StrataMain.lean:640 opens the file, threads it through PipelineContext, but nothing calls h.close / withFile / equivalent. Lean's GC will finalize the handle, but:

• If the outcome record emission at StrataMain.lean:651-657 fails partway through, the handle is leaked.
• For long-running pipelines with the process still live, the outcome record may be buffered (even with per-record flush — the OS page cache is a separate layer).
• No guarantee the OS flushes before a SIGKILL.

The PR body claims "all records written up to that point remain on disk" — per-record h.flush at Messages.lean:304 does flush, which is fflush() equivalent; on most systems that reaches the OS buffer but not the disk (that's fsync). For timeout resilience, fsync on each record is expensive but correct. Worth a docstring note clarifying the guarantee, and wrapping the handle in IO.FS.withFile-style resource management. Inline on PyAnalyzeLaurel.lean:41.

4. Thread safety: PipelineContext uses plain IO.Refs. If the pipeline ever parallelizes (e.g., parallel per-obligation SMT), messagesRef, timingRef, repeatedPhasesRef, currentPhaseRef will race. Not a problem today, but the design choice should be stated in the docstring ("single-threaded; adopt IO.Mutex before parallelizing"). Inline on Messages.lean:255.

5. withPhase's finally may emit multiple [end] lines if the action itself called withPhase but threw before its own finally ran. The finally in withPhase (Messages.lean:374-382) saves and restores the parent phase; but if a nested withPhase is interrupted by a throw before its own finally, the state is in a partial save-restore pattern. The outer finally restores to the outermost parent, which should be correct — but worth a test case that throws mid-nested-phase to confirm [end] lines match [start] lines in the profile output.

6. Test coverage is thin for the new infrastructure. The existing tests (AnalyzeLaurelTest.lean, ToLaurelTest.lean) exercise the happy path and a few error paths through the new PipelineM. Not exercised:

• Streaming JSONL output when the process is interrupted (can't be tested easily, but a fixture that verifies the JSONL is well-formed on normal exit would catch structural regressions).
• Multiple fatal errors accumulating before abort (the PR body notes "multiple error-impact messages may accumulate before or across aborts" but no test pins this down).
• withRepeatedPhase aggregation (count + total) — the test suite calls through to the verifier but doesn't assert on the aggregated output.
• Error path in pyResolveOverloads (T1 says a negative test was added; I see ToLaurelTest.lean grew by 250 lines — worth confirming the happy-and-error-path coverage is balanced).

Proof-coverage suggestions (each small):

/-- `emitFatalMessage` always throws. -/
theorem emitFatalMessage_throws (kind : MessageKind) (msg : String) (file : System.FilePath) :
    (emitFatalMessage kind msg file).run ctx = .error () ∧
    (∃ msgs', ctx.messagesRef.get = pure msgs' ∧ msgs'.size > 0)

/-- Metric file accumulates one record per `emitMetric` call. -/
theorem emitMetric_appends_line (ctx : PipelineContext) (j : Lean.Json) :
    ctx.metricsHandle.isSome →
    (emitMetric ctx j).run = append j.compress ++ "\n" to file

/-- `withPhase` restores current phase regardless of whether action threw. -/
theorem withPhase_restores_phase (ctx : PipelineContext) (name : String) (action : PipelineM α) :
    let before ← ctx.currentPhaseRef.get
    let _ ← try (withPhase name action).run ctx catch _ => pure ()
    ctx.currentPhaseRef.get = before

The third is the one I'd most want — it's the exception-safety invariant of withPhase, and without it, a throw inside the action can leave the phase hierarchy desynchronized, producing unmatched [start]/[end] in profile output.

Refactor callouts:

• MessageKind block (Messages.lean:102-215) has 30+ constants, each { category := "…", impact := .X }. My earlier macro suggestion (T8) was declined and I'll drop it — but worth a #guard at the bottom of the block checking the category string matches the constant name for each (prevents { category := "unsupportdUnion", … }-style typos).
• Messages.lean:258 (private mk ::) + several private fieldRef : fields — good encapsulation, but the create constructor now has 9 fields. Consider .mkDefault with the common shape and individual setters for the rare overrides.
• withPhase / withRepeatedPhase / emitMessage / emitFatalMessage — four entry points with similar shapes. A PipelineAction typeclass or a single runPipeline combinator that takes the phase/message/abort intent explicitly would consolidate.

[aqjune-aws]

Approving since the nested [profile] feature works now and lake exe strata verify --profile Examples/HeapReasoning.core.st prints a reasonable output

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[MikaelMayer]

Just one comment and I'm good !

[shigoel]

Minor comment on mergeOverloads semantics.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

• --verbose Laurel/Core program dumps: restored in b53969b2f
• Unused MessageKind placeholder constants: removed in 39bd5c0a8 (used ones moved to Languages/Python/Specs/MessageKind.lean)
• Latent index bug (timingRef): already resolved in earlier commit
• --skip-verification behavior and userCodeIssue fatality: design observations, unchanged and not blockers