Refactor pipeline timing: withPhase/withRepeatedPhase combinators, fatal abort via EIO

Replace manual profileStep/startPhase calls with structured withPhase
combinator that handles nesting, timing, and profile output. Add
withRepeatedPhase for accumulating iteration-level timing (preprocess,
smtEncode, solver) without per-iteration overhead.

Key changes:
- PipelineM is now ReaderT PipelineContext (EIO Unit); fatal messages abort
  via throw rather than shouldAbortRef polling
- Phase simplified to Array String (removed PhaseName/Ord/index)
- withPhase saves/restores parent phase and repeated-phases state
- withRepeatedPhase accumulates count+duration, flushed as [profile] lines
- All output goes to stdout with flush for reliable capture on timeout
- pythonAndSpecToLaurel takes PipelineContext directly (not Option)
- Verifier.verify/verifySingleEnv accept optional PipelineContext

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: joehendrix

Strata/Languages/Core/Verifier.lean

@@ -21,7 +21,9 @@ import Strata.Transform.LoopElim
 import Strata.Transform.ANFEncoder
 import Strata.Languages.Core.ObligationExtraction
 public import Strata.Transform.IrrelevantAxioms
-import Strata.Util.Profile
+public import Strata.Pipeline.Messages
+
+open Strata.Pipeline (PipelineContext)
 
 ---------------------------------------------------------------------
 
@@ -1021,23 +1023,23 @@ def verifySingleEnv (oblProgram : Program)
     -- irrelevant axiom removal to determine which axioms to prune.
     (axiomProgram : Option Program := .none)
     (externalPhases : List AbstractedPhase := [])
-    (corePhases : List AbstractedPhase := coreAbstractedPhases) :
+    (corePhases : List AbstractedPhase := coreAbstractedPhases)
+    (pipelineCtx : Option PipelineContext := none) :
     EIO DiagnosticModel (VCResults × Statistics) := do
   -- Build SMT encoding context from the obligations program itself
   let E ← EIO.ofExcept (Core.buildEnv options oblProgram moreFns (registerCustomFunctions := true) |>.map (·.1))
   let p := E.program
-  let profile := options.profile
+  let pctx ← match pipelineCtx with
+    | some ctx => pure ctx
+    | none => (PipelineContext.create (outputMode := .quiet) : BaseIO _)
+
     -- Extract obligations from the obligations program via ObligationExtraction
   let obligations ← match Core.ObligationExtraction.extractObligations oblProgram with
     | .ok obs => pure obs
     | .error e => .error (DiagnosticModel.fromFormat f!"ObligationExtraction error: {e}")
   let mut stats : Statistics := ({} : Statistics)
     |>.increment s!"{Evaluator.Stats.verify_numObligations}" obligations.size
   let mut results := (#[] : VCResults)
-  let mut preprocessNs : Nat := 0
-  let mut smtEncodeNs : Nat := 0
-  let mut solverNs : Nat := 0
-  let mut peResolvedCount : Nat := 0
   for obligation in obligations do
     -- Determine which checks to perform based on metadata or check mode/amount
     let (satisfiabilityCheck, validityCheck) :=
@@ -1051,10 +1053,8 @@ def verifySingleEnv (oblProgram : Program)
         | .deductive, _ =>
           if obligation.property.passWhenUnreachable then (false, true) else (true, false)
         | .bugFinding, _ => (true, false)
-    let t0 ← IO.monoNanosNow
-    let (obligation, peSatResult?, peValResult?) ← preprocessObligation obligation p options satisfiabilityCheck validityCheck axiomCache axiomNames axiomProgram
-    let t1 ← IO.monoNanosNow
-    preprocessNs := preprocessNs + (t1 - t0)
+    let (obligation, peSatResult?, peValResult?) ← pctx.withRepeatedPhase "preprocess" do
+      preprocessObligation obligation p options satisfiabilityCheck validityCheck axiomCache axiomNames axiomProgram
     -- If evaluator resolved both checks, we're done, unless we always want to generate SMT queries
     if not options.alwaysGenerateSMT then
       if let (some peSat, some peVal) := (peSatResult?, peValResult?) then
@@ -1070,7 +1070,6 @@ def verifySingleEnv (oblProgram : Program)
         let result : VCResult := { obligation, outcome := .ok outcome, verbose := options.verbose,
                                     checkLevel := options.checkLevel, checkMode := options.checkMode, lexprModel := [] }
         results := results.push result
-        peResolvedCount := peResolvedCount + 1
         if result.isFailure || result.isImplementationError || result.isTimeout then
           if options.verbose >= .debug then
             let prog := f!"\n\n[DEBUG] Evaluated program:\n{Core.formatProgram p}"
@@ -1080,10 +1079,8 @@ def verifySingleEnv (oblProgram : Program)
     -- Need the solver for at least one check
     let needSatCheck := satisfiabilityCheck && peSatResult?.isNone
     let needValCheck := validityCheck && peValResult?.isNone
-    let t2 ← IO.monoNanosNow
-    let maybeTerms := ProofObligation.toSMTTerms E obligation { SMT.Context.default with uniqueBoundNames := options.uniqueBoundNames } options.useArrayTheory
-    let t3 ← IO.monoNanosNow
-    smtEncodeNs := smtEncodeNs + (t3 - t2)
+    let maybeTerms ← pctx.withRepeatedPhase "smtEncode" do
+      pure (ProofObligation.toSMTTerms E obligation { SMT.Context.default with uniqueBoundNames := options.uniqueBoundNames } options.useArrayTheory)
     match maybeTerms with
     | .error err =>
       let result := { obligation,
@@ -1099,12 +1096,10 @@ def verifySingleEnv (oblProgram : Program)
       if options.stopOnFirstError then break
     | .ok (assumptionTerms, varDefs, varDecls, obligationTerm, ctx, encStats) =>
       stats := stats.merge encStats
-      let t4 ← IO.monoNanosNow
-      let result ← getObligationResult assumptionTerms obligationTerm ctx obligation p options
+      let result ← pctx.withRepeatedPhase "solver" do
+        getObligationResult assumptionTerms obligationTerm ctx obligation p options
                     counter tempDir needSatCheck needValCheck (externalPhases ++ corePhases)
                     (varDefinitions := varDefs) (varDeclarations := varDecls)
-      let t5 ← IO.monoNanosNow
-      solverNs := solverNs + (t5 - t4)
       -- Merge evaluator results with solver results
       let result := match result.outcome with
         | .ok solverOutcome =>
@@ -1120,11 +1115,6 @@ def verifySingleEnv (oblProgram : Program)
           let prog := f!"\n\n[DEBUG] Evaluated program:\n{Core.formatProgram p}"
           dbg_trace f!"\n\nResult: {result}\n{prog}"
         if options.stopOnFirstError then break
-  if profile then
-    let _ ← (IO.println s!"[profile]     Preprocess obligations: {nsToMs preprocessNs}ms" |>.toBaseIO)
-    let _ ← (IO.println s!"[profile]     SMT encoding: {nsToMs smtEncodeNs}ms" |>.toBaseIO)
-    let _ ← (IO.println s!"[profile]     Solver/file writing: {nsToMs solverNs}ms" |>.toBaseIO)
-    let _ ← (IO.println s!"[profile]     Obligations: {obligations.size} total, {peResolvedCount} resolved by evaluator" |>.toBaseIO)
   return (results, stats)
 
 /-- Run the Strata Core verification pipeline on a program: transform,
@@ -1142,12 +1132,17 @@ def verify (program : Program)
     (externalPhases : List AbstractedPhase := [])
     (prefixPhases : List PipelinePhase := [])
     (keepAllFilesPrefix : Option String := none)
+    (pipelineCtx : Option PipelineContext := none)
     : EIO DiagnosticModel VCResults := do
   let profile := options.profile
+  let pctx ← match pipelineCtx with
+    | some ctx => pure ctx
+    | none => (PipelineContext.create (outputMode := .quiet) : BaseIO _)
+
   let factory ← EIO.ofExcept (Core.Factory.addFactory moreFns)
   let pipelinePhases := prefixPhases ++ corePipelinePhases (procs := proceduresToVerify) (options := options) (moreFns := moreFns)
   let phases := pipelinePhases.map (·.phase)
-  let (oblProgram, pipelineStats) ← profileStep profile "  Program transformations" do
+  let (oblProgram, pipelineStats) ← pctx.withPhase "programTransformations" do
     if let some pfx := keepAllFilesPrefix then
       if let some parent := (System.FilePath.mk pfx).parent then
         IO.toEIO (fun e => DiagnosticModel.fromFormat f!"{e}")
@@ -1172,23 +1167,17 @@ def verify (program : Program)
         throw e
     .ok (current, state.statistics)
   let allStats := pipelineStats
-  -- Extract axiom names from the original program. The oblProgram (output of
-  -- toCoreProofObligationProgram) inlines axioms as assume statements but does
-  -- not preserve axiom declarations, so we use the pre-transform program for
-  -- axiom identity.
   let axiomNames := program.decls.filterMap fun decl =>
     match decl with | .ax a _ => some a.name | _ => none
-  -- Build the axiom relevance cache from the original program (which has
-  -- axiom declarations). The cache is reused across all obligations.
-  let axiomCache? ← profileStep profile "  Build axiom relevance cache" do
+  let axiomCache? ← pctx.withPhase "buildAxiomCache" do
     pure (if options.removeIrrelevantAxioms == .Off then .none
           else .some (IrrelevantAxioms.Cache.build program))
   let counter ← IO.toEIO (fun e => DiagnosticModel.fromFormat f!"{e}") (IO.mkRef 0)
-  let VCss ← profileStep profile "  VC discharge" do
+  let VCss ← pctx.withPhase "vcDischarge" do
     if options.checkOnly then
       pure []
     else
-      pure [← verifySingleEnv oblProgram moreFns options counter tempDir axiomCache? axiomNames (axiomProgram := program) externalPhases phases]
+      pure [← verifySingleEnv oblProgram moreFns options counter tempDir axiomCache? axiomNames (axiomProgram := program) externalPhases phases (pipelineCtx := pipelineCtx)]
   let allStats := VCss.foldl (fun acc (_, s) => acc.merge s) allStats
   if profile then
     let _ ← (IO.println allStats.format |>.toBaseIO)

Strata/Languages/Laurel/LaurelCompilationPipeline.lean

@@ -12,7 +12,6 @@ import Strata.Languages.Laurel.EliminateValueReturns
 import Strata.Languages.Laurel.ConstrainedTypeElim
 import Strata.Languages.Laurel.TypeAliasElim
 import Strata.Languages.Core.Verifier
-import Strata.Util.Profile
 import Strata.Util.Statistics
 
 /-!
@@ -144,7 +143,8 @@ When `keepAllFilesPrefix` is provided (via the `PipelineM` context), the
 program state after each named Laurel pass is written to
 `{prefix}.{n}.{passName}.laurel.st`.
 -/
-private def runLaurelPasses (options : LaurelTranslateOptions) (program : Program)
+private def runLaurelPasses (options : LaurelTranslateOptions)
+    (pctx : Strata.Pipeline.PipelineContext) (program : Program)
     : PipelineM (Program × SemanticModel × List DiagnosticModel × Statistics) := do
   let program := { program with
     staticProcedures := coreDefinitionsForLaurel.staticProcedures ++ program.staticProcedures,
@@ -172,8 +172,7 @@ private def runLaurelPasses (options : LaurelTranslateOptions) (program : Progra
   let mut allStats : Statistics := {}
 
   for pass in laurelPipeline do
-    let (program', diags, stats) ← profileStep options.profile s!"  {pass.name}" do
-      pure (pass.run program model)
+    let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run program model)
     program := program'
     allDiags := allDiags ++ diags
     allStats := allStats.merge stats
@@ -193,9 +192,13 @@ When `keepAllFilesPrefix` is provided, the program state after each named
 Laurel-to-Laurel pass is written to `{prefix}.{n}.{passName}.laurel.st`.
 -/
 def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
-    : IO TranslateResultWithLaurel :=
+    (pipelineCtx : Option Strata.Pipeline.PipelineContext := none)
+    : IO TranslateResultWithLaurel := do
+  let pctx ← match pipelineCtx with
+    | some ctx => pure ctx
+    | none => Strata.Pipeline.PipelineContext.create (outputMode := .quiet)
   runPipelineM options.keepAllFilesPrefix do
-    let (program, model, passDiags, stats) ← runLaurelPasses options program
+    let (program, model, passDiags, stats) ← runLaurelPasses options pctx program
     let ordered := orderProgram program
 
     -- This early return is a simple way to protect against duplicative errors. Without this return,

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -25,6 +25,7 @@ public import Strata.Languages.Laurel.CoreDefinitionsForLaurel
 public import Strata.Languages.Laurel.CoreGroupingAndOrdering
 import Strata.DDM.Util.DecimalRat
 import Strata.DL.Imperative.Stmt
+import Strata.Pipeline.Messages
 import Strata.DL.Imperative.MetaData
 import Strata.DL.Lambda.LExpr
 import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator

Strata/Languages/Python/PySpecPipeline.lean

@@ -18,7 +18,6 @@ public import Strata.Pipeline.Messages
 import Strata.Languages.Python.Specs.IdentifyOverloads
 import Strata.Languages.Python.Specs.ToLaurel
 import Strata.Util.DecideProp
-import Strata.Util.Profile
 import all Strata.DDM.Util.String
 
 /-! ## PySpec Pipeline
@@ -45,37 +44,34 @@ public structure PySpecLaurelResult where
   exhaustiveClasses : Std.HashSet String := {}
   deriving Inhabited
 
-/-- A default pipeline context for sub-pipelines that don't need output. -/
-private def defaultPipelineContext : BaseIO Pipeline.PipelineContext :=
-  Pipeline.PipelineContext.create (outputMode := .quiet)
-
 /-- Emit a pipeline message. Tags with the current phase from state.
-    Sets `shouldAbort` if the kind's impact is fatal.
+    Throws `()` if the kind's impact is fatal, aborting the pipeline.
     In verbose mode, prints the message immediately to stderr. -/
 public def emitMessage (kind : Pipeline.MessageKind) (message : String)
     (file : System.FilePath := default) (loc : SourceRange := default) : Pipeline.PipelineM Unit := do
   let ctx ← read
   let phase ← ctx.currentPhaseRef.get
   ctx.messagesRef.modify (·.push { file, loc, phase, kind, message })
-  if kind.impact.isFatal then
-    ctx.shouldAbortRef.set true
   if ctx.outputMode == .verbose then
     let tag := if kind.impact.isFatal then "error" else "warning"
     let indent := String.replicate ((phase.depth - 1) * 2) ' '
     let _ ← (do IO.eprintln s!"{indent}[{tag}] {file}: {message}"; (← IO.getStderr).flush : IO Unit).toBaseIO
+  if kind.impact.isFatal then
+    throw ()
 
 /-- Append a batch of messages to the pipeline state.
+    Throws `()` if any message has fatal impact.
     In verbose mode, prints each message immediately to stderr. -/
 public def addMessages (msgs : Array Pipeline.PipelineMessage) : Pipeline.PipelineM Unit := do
   let ctx ← read
   ctx.messagesRef.modify (· ++ msgs)
-  if msgs.any (·.kind.impact.isFatal) then
-    ctx.shouldAbortRef.set true
   if ctx.outputMode == .verbose then
     for msg in msgs do
       let tag := if msg.kind.impact.isFatal then "error" else "warning"
       let indent := String.replicate ((msg.phase.depth - 1) * 2) ' '
       let _ ← (do IO.eprintln s!"{indent}[{tag}] {msg.file}: {msg.message}"; (← IO.getStderr).flush : IO Unit).toBaseIO
+  if msgs.any (·.kind.impact.isFatal) then
+    throw ()
 
 /-! ### Private Helpers -/
 
@@ -237,7 +233,7 @@ private def buildPySpecLaurelM (pyspecEntries : Array (String × String))
 public def buildPySpecLaurel
     (ctx : Pipeline.PipelineContext)
     (pyspecEntries : Array (String × String))
-    (overloads : OverloadTable) : BaseIO PySpecLaurelResult :=
+    (overloads : OverloadTable) : EIO Unit PySpecLaurelResult :=
   buildPySpecLaurelM pyspecEntries overloads |>.run ctx
 
 /-- Read dispatch Ion files and merge their overload tables. -/
@@ -260,7 +256,7 @@ private def readDispatchOverloadsM
 /-- Read dispatch Ion files and merge their overload tables. -/
 public def readDispatchOverloads
     (ctx : Pipeline.PipelineContext)
-    (dispatchPaths : Array String) : BaseIO OverloadTable :=
+    (dispatchPaths : Array String) : EIO Unit OverloadTable :=
   readDispatchOverloadsM dispatchPaths |>.run ctx
 
 /-- Resolve a module name to a `(modulePrefix, ionPath)` pair for
@@ -434,9 +430,11 @@ public def splitProcNames (prog : Core.Program)
 public def translateCombinedLaurelWithLowered (combined : Laurel.Program)
     (keepAllFilesPrefix : Option String := none)
     (profile : Bool := false)
+    (pipelineCtx : Option Pipeline.PipelineContext := none)
     : IO (Option Core.Program × List DiagnosticModel × Laurel.Program × Statistics) := do
   let (coreOption, errors, lowered, stats) ←
-    Laurel.translateWithLaurel { inlineFunctionsWhenPossible := true, keepAllFilesPrefix, profile } combined
+    Laurel.translateWithLaurel { inlineFunctionsWhenPossible := true, keepAllFilesPrefix, profile }
+      combined (pipelineCtx := pipelineCtx)
   return (coreOption.map appendCorePartOfRuntime, errors, lowered, stats)
 
 /-- Translate a combined Laurel program to Core and prepend the full
@@ -534,22 +532,22 @@ public def pythonAndSpecToLaurel
     (pyspecModules : Array String := #[])
     (sourcePath : Option String := none)
     (specDir : System.FilePath := ".")
-    (profile : Bool := false)
+    (pipelineCtx : Pipeline.PipelineContext)
     : BaseIO PythonToLaurelResult := do
   let stmts ←
-    match ← profileStep profile "Read Python Ion"
+    match ← pipelineCtx.withPhase "readPythonIon"
         (Python.readPythonStrata pythonIonPath |>.toBaseIO) with
     | .ok r => pure r
     | .error msg => return .failure (.internal msg) #[]
 
-  let ctx ← defaultPipelineContext
-  let result ←
-    profileStep profile "Resolve and build Laurel prelude" $
-      resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir |>.run ctx
-  let pyspecWarnings ← ctx.messagesRef.get
+  let resultOrAbort ←
+    pipelineCtx.withPhase "resolveAndBuildPrelude"
+      (resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir |>.run pipelineCtx).toBaseIO
+  let pyspecWarnings ← pipelineCtx.messagesRef.get
 
-  if ← ctx.shouldAbortRef.get then
-    return .failure (.internal "Pipeline aborted due to fatal errors") pyspecWarnings
+  let result ← match resultOrAbort with
+    | .error () => return .failure (.internal "Pipeline aborted due to fatal errors") pyspecWarnings
+    | .ok r => pure r
 
   let preludeInfo := buildPreludeInfo result
   let metadataPath := sourcePath.getD pythonIonPath

Strata/Languages/Python/Specs.lean

@@ -356,7 +356,7 @@ def shouldSkip (name : String) : PySpecM Bool := do
   let nameIdent := { pythonModule := toString ctx.currentModule, name }
   return nameIdent ∈ ctx.skipNames
 
-private def pySpecParsingPhase : Phase := Phase.base "pySpecParsing" 1
+private def pySpecParsingPhase : Phase := Phase.base "pySpecParsing"
 
 def specErrorAt (file : System.FilePath) (loc : SourceRange) (message : String) : PySpecM Unit := do
   let e : PipelineMessage := { file, loc, phase := pySpecParsingPhase, kind := .pySpecParsingError, message }

Strata/Languages/Python/Specs/ToLaurel.lean

@@ -90,7 +90,7 @@ abbrev ToLaurelM := ReaderT ToLaurelContext (StateM ToLaurelState)
 /-- Report an error during translation. Phase is set to pySpecToLaurel since
     this monad always runs during that phase. -/
 def reportError (kind : MessageKind) (loc : SourceRange) (message : String) : ToLaurelM Unit := do
-  let phase := Phase.base "pySpecToLaurel" 2
+  let phase := Phase.base "pySpecToLaurel"
   let e : PipelineMessage := ⟨(←read).filepath, loc, phase, kind, message⟩
   modify fun s => { s with errors := s.errors.push e }