Main.lean

import Concrete
import Concrete.Proof.ObligationCore
import Concrete.Report.CompilerLedger
import Concrete.Backend.Backend
import Concrete.Resolve.Project

open Concrete

-- Shared CLI exit-code taxonomy (ROADMAP Phase 4 #14). One source of truth for
-- every command's exit code AND the documented `EXIT CODES` help block, so the
-- codes and their documentation cannot drift.
namespace ExitCode
def ok : UInt32 := 0
def usage : UInt32 := 1
def obligationsMissing : UInt32 := 2
def staleEvidence : UInt32 := 3
def proofCheckFailure : UInt32 := 4
def solverFailure : UInt32 := 5
def internalError : UInt32 := 6

/-- (code, meaning) — the single source for both exits and the help block. -/
def taxonomy : List (UInt32 × String) :=
  [ (ok, "success (proved / clean / info printed)"),
    (usage, "invalid invocation (bad args, unknown function)"),
    (obligationsMissing, "obligations missing (eligible but unproved)"),
    (staleEvidence, "stale evidence (body changed since the proof was linked)"),
    (proofCheckFailure, "proof-check failure (Lean kernel rejected a referenced theorem)"),
    (solverFailure, "solver/checker failure (omega/bv_decide/lake could not run)"),
    (internalError, "internal compiler error") ]

/-- The `EXIT CODES` help block, generated from `taxonomy` (no hand-kept copy). -/
def helpBlock : List String :=
  "EXIT CODES:" :: taxonomy.map (fun (c, m) => s!"  {c}  {m}")
end ExitCode

-- Shared command-line flag parsing (ROADMAP Phase 4 #14b). One definition of what
-- a boolean flag and a valued flag mean, so every command parses flags the same
-- way instead of re-deriving `args.contains` / `dropWhile` inline.
namespace Cli
/-- True iff the boolean flag `name` is present. -/
def hasFlag (args : List String) (name : String) : Bool := args.contains name

/-- The value following `name` (e.g. `--out PATH`), or `none` if `name` is absent
    or the next token is itself a flag — so `--out --json` does NOT capture
    `--json` as the path. This guard is applied uniformly (several call sites
    previously omitted it). -/
def flagValue (args : List String) (name : String) : Option String :=
  match args.dropWhile (· != name) with
  | _ :: v :: _ => if v.startsWith "-" then none else some v
  | _ => none
end Cli

/-- Phase 6E #1: the grouped, context-free help page. Groups commands by use
    per the roadmap taxonomy; the full flag matrix stays in `usage` below. -/
def helpText : String := String.intercalate "\n" [
  "concrete — the Concrete compiler",
  "",
  "USAGE: concrete <command> [args]   |   concrete <file.con> [flags]",
  "",
  "DAILY:",
  "  build [file|project]      compile (project mode reads Concrete.toml)",
  "  run   [file|project]      compile and run",
  "  test  [--module <name>]   run #[test] functions",
  "  fmt   <file.con>          format (--check | --write | --stdin)",
  "",
  "REPORTS & EVIDENCE:",
  "  <file> --report <kind>    caps, unsafe, layout, proof-status, obligations, …",
  "  prove <file> <fn>         prove/check an obligation (prove --help for more)",
  "  <file> --query <kind>     semantic queries (why-capability, evidence, …)",
  "",
  "DEBUGGING:",
  "  <file> --trace-pipeline   per-stage trace naming the first failing phase",
  "  <file> --emit-trace-json  per-stage telemetry (counts, timing)",
  "  reduce <file> --predicate <p>   minimize a failing program",
  "  debug-bundle <file>       capture a reproducible failure bundle",
  "",
  "INTERNALS / COMPAT:",
  "  <file> --emit-core | --emit-ssa | --emit-llvm | --interp",
  "  diff, snapshot, audit, check, validate-bundle, --version",
  "",
  "Run `concrete` with no arguments for the full flag matrix.",
  ""]

def usage : String :=
  "Usage: concrete <file.con> [-o output] [--emit-llvm] [--emit-core] [--emit-ssa] [--emit-trace-json] [--trace-pipeline] [--test] [--test --module <name>] [--interp] [--report caps|unsafe|layout|interface|alloc|mono|authority|proof|eligibility|proof-status|obligations|extraction|lean-stubs|check-proofs|proof-diagnostics|proof-deps|proof-bundle|traceability|diagnostics-json|effects|recursion|stack-depth|fingerprints|consistency|contracts|vcs|obligation-ledger|compiler-ledger|verify|audit|arithmetic] [--query KIND|KIND:FUNCTION|fn:FUNCTION] [--fmt (legacy; use `concrete fmt`)]\n       concrete build [-o output] [--emit-llvm]\n       concrete check\n       concrete fmt <file.con> [--check | --write | --stdin]\n       concrete audit <file.con>\n       concrete prove <file.con> <module.function> [--json] [--out <path>] [--force] [--emit-link] [--emit-lean] [--emit-artifacts] [--out-dir <dir>] [--show-obligation <id>] [--replay] [--nearest-lemmas] [--check] [--workspace <dir>]\n       concrete prove --help=agent | --capabilities | --schema\n       concrete run [-- args...]\n       concrete test [--module <name>]\n       concrete diff <old.json> <new.json> [--json]\n       concrete snapshot <file.con> [-o output.json]\n       concrete debug-bundle <file.con> [-o dir]\n       concrete reduce <file.con> --predicate <pred> [-o output] [--verbose]\n       concrete --version"

/-- Capture compiler identity: version, git commit, lean toolchain. -/
def compilerIdentity : IO String := do
  let version := "0.1.0"
  let commit ← try
    let r ← IO.Process.output { cmd := "git", args := #["rev-parse", "--short", "HEAD"] }
    if r.exitCode == 0 then
      let hash := r.stdout.trimAscii.toString
      -- Check for tracked modifications and untracked files
      let d ← IO.Process.output { cmd := "git", args := #["status", "--porcelain"] }
      pure (if d.stdout.trimAscii.toString.isEmpty then hash else hash ++ "-dirty")
    else pure "unknown"
  catch _ => pure "unknown"
  let toolchain ← try
    let tc ← IO.FS.readFile ⟨"lean-toolchain"⟩
    pure tc.trimAscii.toString
  catch _ => pure "unknown"
  return s!"concrete {version} ({commit}) [{toolchain}]"

def writeFile (path : String) (content : String) : IO Unit := do
  IO.FS.writeFile ⟨path⟩ content

/-- Detect macOS SDK sysroot for clang linking. Returns `--sysroot=<path>` flag if found. -/
def getMacOSSysrootFlags : IO (Array String) := do
  -- Only relevant on macOS
  let os ← IO.Process.output { cmd := "uname", args := #["-s"] }
  if os.stdout.trimAscii.toString != "Darwin" then return #[]
  -- Use xcrun to find the SDK path
  let result ← IO.Process.output { cmd := "xcrun", args := #["--show-sdk-path"] }
  if result.exitCode == 0 then
    let sdkPath := result.stdout.trimAscii.toString
    if sdkPath.length > 0 then return #[s!"--sysroot={sdkPath}"]
  return #[]

/-- Build clang arguments for linking LLVM IR to a native binary. -/
def clangArgs (llPath : String) (outputPath : String) (extraFlags : Array String := #[]) : IO (Array String) := do
  let sysrootFlags ← getMacOSSysrootFlags
  return #[llPath, "-o", outputPath, "-Wno-override-module", "-w", "-O2"] ++ sysrootFlags ++ extraFlags

def runCmd (cmd : String) (args : Array String) : IO UInt32 := do
  let child ← IO.Process.spawn {
    cmd := cmd
    args := args
    stdout := .piped
    stderr := .piped
  }
  let exitCode ← child.wait
  if exitCode != 0 then
    let stderr ← child.stderr.readToEnd
    IO.eprintln stderr
  return exitCode

/-- Hard-error gate for runtime-safety obligations already classified as
    `VIOLATION`. This is intentionally narrower than the contracts report:
    `unproven` obligations remain report/policy facts, while `violation` means
    the compiler proved the safe program is wrong. -/
def enforceProvenRuntimeViolations (modules : List Module) (sourceMap : SourceMap) : IO Bool := do
  let ds := Report.provenViolationDiagnostics modules
  if hasErrors ds then
    IO.eprintln (renderDiagnostics ds (sourceMap := sourceMap))
    return false
  return true

/-- Validate LLVM IR via `llvm-as` (parse-only, no output).
    Returns true if valid or if llvm-as is not found on PATH.
    Returns false (and prints errors) if the IR is malformed. -/
def validateLLVMIR (llPath : String) : IO Bool := do
  -- Check if llvm-as is available
  let which ← IO.Process.output { cmd := "which", args := #["llvm-as"] }
  if which.exitCode != 0 then
    return true  -- llvm-as not available; skip validation
  let result ← IO.Process.output {
    cmd := "llvm-as"
    args := #[llPath, "-o", "/dev/null"]
  }
  if result.exitCode != 0 then
    IO.eprintln s!"LLVM IR validation failed for {llPath}:"
    IO.eprintln result.stderr
    return false
  return true


/-- Best-effort resident-set size in KB. Reads `/proc/self/statm` (Linux); returns
    `none` on any platform without it (e.g. macOS) — the telemetry field is
    platform-graceful, never a hard dependency. -/
def readRssKb : IO (Option Nat) := do
  try
    let contents ← IO.FS.readFile "/proc/self/statm"
    match contents.splitOn " " with
    | _ :: resident :: _ => match resident.toNat? with
      | some pages => pure (some (pages * 4096 / 1024))
      | none => pure none
    | _ => pure none
  catch _ => pure none

def traceTelemetry (inputPath : String) : IO UInt32 := do
  let source ← readFile inputPath
  let git ← compilerIdentity
  let rss ← readRssKb
  let srcMap := [(inputPath, source)]
  -- Run the pipeline stage by stage so we can time each pass. Timing is a debug
  -- aid, not a perf claim; the gate pins schema + monotonic sanity, not magnitudes.
  let baseDir := let parts := inputPath.splitOn "/"
    match parts.reverse with | _ :: rest => "/".intercalate rest.reverse | [] => "."
  -- Run the pipeline stage by stage so each pass can be timed. Timing is a debug
  -- aid, not a perf claim; the gate pins schema + monotonic sanity, not magnitudes.
  let mut timing : List (String × Nat) := []
  let mut t ← IO.monoMsNow
  match Pipeline.parse source with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok parsed =>
  let astNodes := Pipeline.astModuleNodes parsed.modules
  timing := timing ++ [("parse", (← IO.monoMsNow) - t)]; t ← IO.monoMsNow
  match ← Pipeline.resolveFiles baseDir parsed inputPath resolveAllModules with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok (resolved, _) =>
  let summary := Pipeline.buildSummary resolved
  timing := timing ++ [("resolve-files", (← IO.monoMsNow) - t)]; t ← IO.monoMsNow
  match Pipeline.resolve resolved summary with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok rp =>
  let resolvedProg := Pipeline.desugar rp
  timing := timing ++ [("resolve", (← IO.monoMsNow) - t)]; t ← IO.monoMsNow
  match Pipeline.check resolvedProg summary with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok () =>
  timing := timing ++ [("check", (← IO.monoMsNow) - t)]; t ← IO.monoMsNow
  match Pipeline.elaborate resolvedProg summary with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok elabProg =>
  timing := timing ++ [("elaborate", (← IO.monoMsNow) - t)]; t ← IO.monoMsNow
  match Pipeline.coreCheck elabProg with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok validCore =>
  timing := timing ++ [("coreCheck", (← IO.monoMsNow) - t)]; t ← IO.monoMsNow
  match Pipeline.monomorphize validCore with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok mono =>
  timing := timing ++ [("monomorphize", (← IO.monoMsNow) - t)]; t ← IO.monoMsNow
  match Pipeline.lower mono with
  | .error ds => IO.eprintln (renderDiagnostics ds (sourceMap := srcMap)); return 1
  | .ok ssa =>
  timing := timing ++ [("lower", (← IO.monoMsNow) - t)]
  IO.println (Pipeline.telemetryJson git astNodes validCore mono ssa 0 timing rss)
  return 0

/-- Phase 6C #3: per-stage pipeline trace as JSON. Runs the pipeline stage by
    stage, recording which stages passed and — for a rejected program — the FIRST
    stage that failed plus its diagnostic code. An accepted program reports every
    stage `ok` plus the telemetry counts. Backs `concrete <file> --trace-pipeline`. -/
def tracePipeline (inputPath : String) : IO UInt32 := do
  let source ← readFile inputPath
  let git ← compilerIdentity
  let firstCode : Diagnostics → String := fun ds => match ds.head? with | some d => d.code | none => ""
  let emit := fun (okRev : List String) (fail : Option (String × String)) (counts : String) =>
    IO.println (Pipeline.traceJson git inputPath okRev.reverse fail counts)
  match Pipeline.parse source with
  | .error ds => emit [] (some ("parse", firstCode ds)) "null"; return 0
  | .ok parsed =>
  let ok := ["parse"]
  let baseDir := let parts := inputPath.splitOn "/"
    match parts.reverse with | _ :: rest => "/".intercalate rest.reverse | [] => "."
  match ← Pipeline.resolveFiles baseDir parsed inputPath resolveAllModules with
  | .error ds => emit ok (some ("resolve-files", firstCode ds)) "null"; return 0
  | .ok (resolved, _) =>
  let ok := "resolve-files" :: ok
  let summary := Pipeline.buildSummary resolved
  match Pipeline.resolve resolved summary with
  | .error ds => emit ok (some ("resolve", firstCode ds)) "null"; return 0
  | .ok resolvedProg =>
  let ok := "resolve" :: ok
  let resolvedProg := Pipeline.desugar resolvedProg
  match Pipeline.check resolvedProg summary with
  | .error ds => emit ok (some ("check", firstCode ds)) "null"; return 0
  | .ok () =>
  let ok := "check" :: ok
  match Pipeline.elaborate resolvedProg summary with
  | .error ds => emit ok (some ("elaborate", firstCode ds)) "null"; return 0
  | .ok elabProg =>
  let ok := "elaborate" :: ok
  match Pipeline.coreCheck elabProg with
  | .error ds => emit ok (some ("coreCheck", firstCode ds)) "null"; return 0
  | .ok validCore =>
  let ok := "coreCheck" :: ok
  match Pipeline.monomorphize validCore with
  | .error ds => emit ok (some ("monomorphize", firstCode ds)) "null"; return 0
  | .ok mono =>
  let ok := "monomorphize" :: ok
  match Pipeline.lower mono with
  | .error ds => emit ok (some ("lower", firstCode ds)) "null"; return 0
  | .ok ssa =>
  let ok := "lower" :: ok
  emit ok none (Pipeline.telemetryJson git (Pipeline.astModuleNodes parsed.modules) validCore mono ssa 0)
  return 0

/-- Compile via SSA pipeline: Parse → Resolve → Check → Elab → CoreCanonicalize → CoreCheck → Mono → Lower → SSAVerify → SSACleanup → EmitSSA → clang -/
def compileSSA (inputPath : String) (outputPath : String) (emitLLVM : Bool) : IO UInt32 := do
  let source ← readFile inputPath
  match ← Pipeline.runFrontend inputPath source resolveAllModules with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := [(inputPath, source)]))
    return 1
  | .ok (parsed, _, validCore, srcMap) =>
  if !(← enforceProvenRuntimeViolations parsed.modules srcMap) then
    return 1
  match Pipeline.monomorphize validCore with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
    return 1
  | .ok mono =>
  match Pipeline.lower mono with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
    return 1
  | .ok ssa =>
    -- An executable needs an entry point. Without one, EmitSSA emits no `@main`
    -- wrapper and the failure would otherwise leak from clang/ld as an opaque
    -- "Undefined symbols: _main" (bug 025). Reject it here as a diagnostic.
    -- `--emit-llvm` is exempt: dumping IR for inspection is legitimate with no
    -- entry point (and there is no separate library/embedded build profile).
    if !emitLLVM && !(ssa.ssaModules.any fun m => m.functions.any (·.isEntryPoint)) then
      IO.eprintln "error[link]: no `main` function found; an executable needs an entry point — define `fn main() -> Int` in the root module"
      return 1
    let llvmIR := Pipeline.emit ssa
    let llPath := inputPath ++ ".ll"
    writeFile llPath llvmIR
    if emitLLVM then
      IO.println llvmIR
      return 0
    -- Validate LLVM IR (if llvm-as available)
    let llValid ← validateLLVMIR llPath
    if !llValid then
      IO.FS.removeFile ⟨llPath⟩
      return 1
    -- Compile with clang
    let args ← clangArgs llPath outputPath
    let exitCode ← runCmd "clang" args
    if exitCode != 0 then
      IO.eprintln "clang compilation failed"
      return exitCode
    -- Clean up .ll file
    IO.FS.removeFile ⟨llPath⟩
    IO.println s!"Compiled {inputPath} -> {outputPath}"
    return 0

/-- Interpret a program via the source-level interpreter (no codegen). -/
def interpProgram (inputPath : String) : IO UInt32 := do
  let source ← readFile inputPath
  match ← Pipeline.runFrontend inputPath source resolveAllModules with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := [(inputPath, source)]))
    return 1
  | .ok (_, _, validCore, _) =>
    match Interp.interpret validCore.coreModules with
    | .error msg =>
      IO.eprintln msg
      return 1
    | .ok (retVal, out) =>
      -- Match compiled binary contract byte-for-byte: program output first (the
      -- print_* buffer), then the return value on its own line — but ONLY when
      -- `main` returns a value. A Unit `main` prints no value line, exactly like
      -- the compiled binary (which used to diverge: interp printed a stray `0`).
      IO.print out
      match retVal with
      | some n => IO.println s!"{n}"
      | none => pure ()
      return 0

/-- Compile and run tests: Parse → ... → EmitSSA (test mode) → clang → run -/
def compileTest (inputPath : String) (moduleFilter : Option String := none) : IO UInt32 := do
  let source ← readFile inputPath
  match ← Pipeline.runFrontend inputPath source resolveAllModules with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := [(inputPath, source)]))
    return 1
  | .ok (parsed, _, validCore, srcMap) =>
  if !(← enforceProvenRuntimeViolations parsed.modules srcMap) then
    return 1
  match Pipeline.monomorphize validCore with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
    return 1
  | .ok mono =>
  match Pipeline.lower mono with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
    return 1
  | .ok ssa =>
    let llvmIR := Pipeline.emit ssa (testMode := true) (moduleFilter := moduleFilter)
    let llPath := inputPath ++ ".test.ll"
    let outPath := inputPath ++ ".test"
    writeFile llPath llvmIR
    -- Validate LLVM IR (if llvm-as available)
    let llValid ← validateLLVMIR llPath
    if !llValid then return 1
    let args ← clangArgs llPath outPath
    let exitCode ← runCmd "clang" args
    if exitCode != 0 then
      IO.eprintln "clang compilation failed"
      IO.eprintln s!"LLVM IR left at: {llPath}"
      return exitCode
    -- Run the test binary (keep .ll and binary for debugging)
    let child ← IO.Process.spawn {
      cmd := outPath
      stdout := .piped
      stderr := .piped
    }
    let stdout ← child.stdout.readToEnd
    let stderr ← child.stderr.readToEnd
    let exitCode ← child.wait
    IO.print stdout
    if !stderr.isEmpty then IO.eprint stderr
    if exitCode != 0 then
      IO.eprintln s!"Test binary exited with code {exitCode}"
      IO.eprintln s!"LLVM IR at: {llPath}"
      IO.eprintln s!"Binary at: {outPath}"
    else
      IO.FS.removeFile ⟨llPath⟩
      IO.FS.removeFile ⟨outPath⟩
    return exitCode

/-- Emit Core or SSA IR for inspection. Runs full pipeline including new passes. -/
def compileAndEmit (inputPath : String) (mode : String) : IO UInt32 := do
  let source ← readFile inputPath
  match ← Pipeline.runFrontend inputPath source resolveAllModules with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := [(inputPath, source)]))
    return 1
  | .ok (parsed, _, validCore, srcMap) =>
    if mode == "core" then
      for cm in validCore.coreModules do
        IO.println (ppCModule cm)
      return 0
    if !(← enforceProvenRuntimeViolations parsed.modules srcMap) then
      return 1
    match Pipeline.monomorphize validCore with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
      return 1
    | .ok mono =>
    let lowerResult := if mode == "ssa-unverified"
                        then Pipeline.lowerUnverified mono
                        else Pipeline.lower mono
    match lowerResult with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
      return 1
    | .ok ssa =>
      for sm in ssa.ssaModules do
        IO.println (ppSModule sm)
      return 0


/-- Stable schema version for `concrete prove` machine-readable output. -/
def proveSchemaVersion : String := "1"

/-- Run pipeline to needed depth and produce a report. -/
def compileAndQuery (inputPath : String) (query : String) : IO UInt32 := do
  let source ← readFile inputPath
  let mainSrcMap : SourceMap := [(inputPath, source)]
  match ← Pipeline.runFrontend inputPath source resolveAllModules with
  | .error ds =>
    IO.eprintln (renderDiagnostics ds (sourceMap := mainSrcMap))
    return 1
  | .ok (parsed, _, validCore, srcMap) =>
    let locMap := Report.buildFnLocMap parsed.modules inputPath
    let simpleLocMap := locMap.map fun e => (e.qualName, (e.file, e.fnSpan.line))
    let registry ← loadRegistryWithLinks inputPath parsed.modules validCore.coreModules
    let pc := extractProofCore validCore simpleLocMap registry
    -- Traceability queries need the backend pipeline
    let parts := query.splitOn ":"
    if parts[0]! == "traceability" then
      match Pipeline.monomorphize validCore with
      | .error ds =>
        IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
        return 1
      | .ok mono =>
        match Pipeline.lower mono with
        | .error ds =>
          IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
          return 1
        | .ok ssa =>
          let fnFilter := if parts.length == 2 then some parts[1]! else none
          IO.println (Report.queryTraceability validCore.coreModules mono.coreModules ssa.ssaModules locMap fnFilter (registry := registry) (pc := pc))
          return 0
    else
      match Report.queryFacts validCore.coreModules locMap query (registry := registry) (pc := pc) with
      | .ok result =>
        IO.println result
        return 0
      | .error msg =>
        IO.eprintln s!"error: {msg}"
        return 1

-- ============================================================
-- Concrete.toml project support
-- ============================================================


/-- Empty-content stand-in for a CModule, used to preserve a parent
    wrapper (and thus the qualified-name prefix) without dragging in
    sibling functions when scoping. -/
private def emptyWrapper (m : CModule) (subs : List CModule) : CModule :=
  { m with functions := [], structs := [], enums := []
         , externFns := [], constants := []
         , traitDefs := [], traitImpls := [], newtypes := []
         , submodules := subs }

/-- Match a single subtree by bare name, preserving parent wrappers so
    downstream iteration produces fully-qualified names like
    `pkg.<sub>.<leaf>` instead of just `<leaf>`. -/
partial def scopeSubtreeByName
    (m : CModule) (targetNames : List String) : Option CModule :=
  if targetNames.contains m.name then some m
  else
    let scopedSubs := m.submodules.filterMap fun sm => scopeSubtreeByName sm targetNames
    if scopedSubs.isEmpty then none
    else some (emptyWrapper m scopedSubs)

/-- Find any nested CModule subtree whose `name` matches one of `targetNames`.
    Bare-name fallback used when a path-derived module path isn't available
    (e.g. when inputPath lives outside `<projectRoot>/src/`). Note: this
    fallback merges duplicate basenames across subtrees; prefer
    `findMatchingSubtreesByPath` whenever a project root is known. -/
def findMatchingSubtrees (mods : List CModule) (targetNames : List String) : List CModule :=
  mods.filterMap fun m => scopeSubtreeByName m targetNames

/-- Match a single subtree by qualified path suffix, preserving parent
    wrappers so qualified names retain their full prefix. -/
partial def scopeSubtreeByPath
    (m : CModule) (targetPath : List String) (currentPath : List String)
    : Option CModule :=
  let p := currentPath ++ [m.name]
  let isMatch :=
    if targetPath.length > p.length then false
    else (p.drop (p.length - targetPath.length)) == targetPath
  if isMatch then some m
  else
    let scopedSubs := m.submodules.filterMap fun sm => scopeSubtreeByPath sm targetPath p
    if scopedSubs.isEmpty then none
    else some (emptyWrapper m scopedSubs)

/-- Find subtrees whose qualified path (root → leaf) ends with `targetPath`.
    Disambiguates duplicate basenames in different subtrees: with
    `targetPath := ["a", "foo"]`, `pkg.a.foo` matches but `pkg.b.foo`
    does not. Preserves the qualified-name prefix via empty parent
    wrappers (so iteration yields `pkg.a.foo.<fn>`, not `foo.<fn>`). -/
def findMatchingSubtreesByPath
    (mods : List CModule) (targetPath : List String) : List CModule :=
  mods.filterMap fun m => scopeSubtreeByPath m targetPath []

/-- Convert a source file path to its package-relative module path
    segments, given the project root. Returns `none` when the file is
    not under `<projectRoot>/src/`. The package entries `src/main.con`
    and `src/lib.con` map to `[]` (use the parsed top-level name to
    locate the package's root module). `src/foo/mod.con` maps to
    `["foo"]` (the file declares the parent directory's module). -/
def filePathToModulePath (projectRoot inputPath : String) : Option (List String) :=
  let srcPrefix := projectRoot ++ "/src/"
  if !inputPath.startsWith srcPrefix then none
  else
    let chars := inputPath.toList
    let rel := String.ofList (chars.drop srcPrefix.length)
    if !rel.endsWith ".con" then none
    else
      let stripped := String.ofList (rel.toList.take (rel.length - 4))
      let parts := stripped.splitOn "/"
      let parts := if parts.length > 1 && parts.getLast? == some "mod"
                   then parts.dropLast else parts
      some parts

/-- Scope `userModules` (a project's full user-package set) to the modules
    declared in `inputPath`. Uses path-derived qualified module paths to
    disambiguate duplicate basenames across subtrees; falls back to bare
    parsed-name matching when the file is outside `<projectRoot>/src/`. -/
def scopeUserModulesToFile (userModules : List CModule) (inputPath projectRoot : String)
    : IO (List CModule) := do
  let source ← try readFile inputPath catch _ => pure ""
  if source.isEmpty then return userModules
  match Pipeline.parse source with
  | .error _ => return userModules
  | .ok parsedFile =>
    let parsedNames := parsedFile.modules.map (·.name)
    -- Path-derived match (preferred — handles duplicate basenames).
    let pathMatched : List CModule :=
      match filePathToModulePath projectRoot inputPath with
      | none => []
      | some [] => []  -- File isn't under src/; nothing to do.
      -- src/main.con and src/lib.con are package entries: the file's
      -- parsed top-level module names ARE the package's top-level
      -- modules, so bare-name lookup is correct here.
      | some ["main"] | some ["lib"] => findMatchingSubtrees userModules parsedNames
      | some path => findMatchingSubtreesByPath userModules path
    if !pathMatched.isEmpty then return pathMatched
    -- Fallback: bare-name match. Used when inputPath isn't under
    -- `<projectRoot>/src/` (e.g. exotic layouts or symlinked files).
    let nameMatched := findMatchingSubtrees userModules parsedNames
    if nameMatched.isEmpty then return userModules else return nameMatched

/-- Discharge call-site contract obligations with `bv_decide`. Each candidate is
    `(index, leanBoolGoal)`; returns the indices that kernel-check. Runs one
    batched `lake env lean` (all goals), falling back to per-goal runs only if
    the batch fails. No external SMT — `bv_decide` is a kernel decision procedure. -/
def bvDischargeCallSites (candidates : List (Nat × String)) : IO (List Nat) := do
  if candidates.isEmpty then return []
  let mkSrc (cs : List (Nat × String)) : String :=
    "import Std.Tactic.BVDecide\n\n"
      ++ String.join (cs.map (fun (i, g) => s!"theorem cobl_{i} : {g} = true := by bv_decide\n"))
  let runLean (src : String) : IO UInt32 := do
    let tmpDir ← IO.Process.output { cmd := "mktemp", args := #["-d"] }
    let dir := tmpDir.stdout.trimAscii.toString
    IO.FS.writeFile ⟨dir ++ "/cobl.lean"⟩ src
    let r ← IO.Process.output { cmd := "lake", args := #["env", "lean", dir ++ "/cobl.lean"],
                                env := #[("LAKE_TERM_ANSI", "0")] }
    let _ ← IO.Process.output { cmd := "rm", args := #["-rf", dir] }
    return r.exitCode
  if (← runLean (mkSrc candidates)) == 0 then
    return candidates.map (·.1)
  else
    let mut proved : List Nat := []
    for c in candidates do
      if (← runLean (mkSrc [c])) == 0 then proved := proved ++ [c.1]
    return proved

/-- Discharge nonlinear integer-overflow goals with `bv_decide`. Each candidate
    is `(key, propGoal)` where the goal is a quantified BitVec proposition
    (`∀ (v : BitVec w), … → BitVec.ule e hi`); returns the keys that kernel-check.
    `intros; bv_decide` introduces the operands and bound hypotheses, then
    bitblasts — an LRAT-checked kernel decision, no external SMT. Batched,
    falling back per-goal. -/
def bvDischargeOverflow (candidates : List (String × String)) : IO (List String) := do
  if candidates.isEmpty then return []
  let indexed := (List.range candidates.length).zip candidates
  let mkSrc (cs : List (Nat × (String × String))) : String :=
    "import Std.Tactic.BVDecide\n\n"
      ++ String.join (cs.map (fun (i, (_, g)) => s!"theorem ovf_{i} : {g} := by intros; bv_decide\n"))
  let runLean (src : String) : IO UInt32 := do
    let tmpDir ← IO.Process.output { cmd := "mktemp", args := #["-d"] }
    let dir := tmpDir.stdout.trimAscii.toString
    IO.FS.writeFile ⟨dir ++ "/ovf.lean"⟩ src
    let r ← IO.Process.output { cmd := "lake", args := #["env", "lean", dir ++ "/ovf.lean"],
                                env := #[("LAKE_TERM_ANSI", "0")] }
    let _ ← IO.Process.output { cmd := "rm", args := #["-rf", dir] }
    return r.exitCode
  if (← runLean (mkSrc indexed)) == 0 then
    return candidates.map (·.1)
  else
    let mut proved : List String := []
    for c in indexed do
      if (← runLean (mkSrc [c])) == 0 then proved := proved ++ [c.2.1]
    return proved

/-- Discharge loop init/variant VCs with `omega`. Each candidate is
    `(key, leanGoal)`; returns the keys that kernel-check. These VCs are linear
    integer facts over `Int` (the same domain as the preservation proof), so the
    decision procedure is `omega`, not `bv_decide` (bitvector-only). Batched,
    falling back per-goal. No external SMT — `omega` is a kernel decision
    procedure with a checked certificate. -/
def kernelDischargeLoopVCs (candidates : List (String × String)) : IO (List String) := do
  if candidates.isEmpty then return []
  let indexed := (List.range candidates.length).zip candidates
  let mkSrc (cs : List (Nat × (String × String))) : String :=
    String.join (cs.map (fun (i, (_, g)) => s!"theorem lvc_{i} : {g} := by intros; omega\n"))
  let runLean (src : String) : IO UInt32 := do
    let tmpDir ← IO.Process.output { cmd := "mktemp", args := #["-d"] }
    let dir := tmpDir.stdout.trimAscii.toString
    IO.FS.writeFile ⟨dir ++ "/lvc.lean"⟩ src
    let r ← IO.Process.output { cmd := "lake", args := #["env", "lean", dir ++ "/lvc.lean"],
                                env := #[("LAKE_TERM_ANSI", "0")] }
    let _ ← IO.Process.output { cmd := "rm", args := #["-rf", dir] }
    return r.exitCode
  if (← runLean (mkSrc indexed)) == 0 then
    return candidates.map (·.1)
  else
    let mut proved : List String := []
    for c in indexed do
      if (← runLean (mkSrc [c])) == 0 then proved := proved ++ [c.2.1]
    return proved

-- (Phase 3 #14) The former `computeVacuousQuals` / `computeAssumeQuals` /
-- `computeSolverTrustedQuals` side channels are gone: policy now reads these
-- facts from the one obligation ledger via `computePolicyQuals` (below), which
-- projects `ObligationCore.{vacuousFunctions,assumeFunctions,solverTrustedIds}`.

/-- Build the VC schedule and fold in the kernel-checked discharge results
    (omega over the linear goals; `bv_decide` over the BitVec call-site and
    overflow goals). The proved/`counterexample`/constant verdicts already
    decided structurally by `collectVCs` are preserved; only `planned` VCs are
    upgraded — and only to `proved_by_kernel_decision` (or `arithmetic_proved`
    for loop preservation), never to an external-solver class. -/
def computeVCsDischarged (modules : List Concrete.Module) (locMap : Report.FnLocMap)
    (registry : Concrete.ProofRegistry) : IO (List Report.VC) := do
  let vcs := Report.collectVCs modules locMap registry
  let omegaGoals := Report.callPrecondGoals modules ++ Report.assertGoals modules
    ++ Report.vacuityGoals modules ++ Report.loopVCGoals modules
    ++ Report.boundsGoals modules ++ Report.divGoals modules ++ Report.overflowGoals modules
  let omegaProved ← kernelDischargeLoopVCs omegaGoals
  let obs := Report.callSiteObligations modules
  let cands := ((List.range obs.length).zip obs).filterMap fun (i, o) => o.leanGoal.map (fun g => (i, g))
  let bvIdx ← bvDischargeCallSites cands
  let bvCallKeys := bvIdx.filterMap fun i => obs[i]?.map (·.key)
  let ovfBV := (Report.overflowBVGoals modules).filter (fun (k, _) => !omegaProved.contains k)
  let bvOvfKeys ← bvDischargeOverflow ovfBV
  return Report.dischargeVCs vcs omegaProved (bvCallKeys ++ bvOvfKeys)

/-- Read the value Z3 assigned to variable `v` from `(get-model)` output. Handles
    both `... Int 100000)` and the negative `... Int (- 5))` shapes, across lines.
    The declared name IS the source variable name, so no remapping is needed. -/
def smtModelValue (out v : String) : Option String :=
  match ((out.splitOn s!"define-fun {v} () Int").drop 1).head? with
  | none => none
  | some after =>
    let cs := after.toList.dropWhile (fun c => !c.isDigit && c != '-')
    match cs with
    | [] => none
    | c :: rest =>
      if c == '-' then
        let num := (rest.dropWhile (· == ' ')).takeWhile Char.isDigit
        if num.isEmpty then none else some (String.ofList ('-' :: num))
      else
        let num := cs.takeWhile Char.isDigit
        if num.isEmpty then none else some (String.ofList num)

/-- Solver identity + version for provenance, e.g. "z3 4.16.0", or "z3 (unavailable)"
    when Z3 is not on PATH. `z3 --version` prints "Z3 version X.Y.Z - 64 bit". -/
def z3VersionId : IO String := do
  try
    let o ← IO.Process.output { cmd := "z3", args := #["--version"] }
    if o.exitCode != 0 then return "z3 (unavailable)"
    -- extract the version token after "version"
    let toks := o.stdout.trimAscii.toString.splitOn " "
    match toks.dropWhile (· != "version") with
    | _ :: v :: _ => return s!"z3 {v}"
    | _ => return "z3"
  catch _ => return "z3 (unavailable)"

/-- External-SMT adapter (Phase 2 #8/#10). One solver (Z3), pinned timeout. For each
    `(vcKey, smtlibScript)` it writes the script, runs `z3 -T:<timeout>`, and reads
    the first line: `unsat` → `solver_trusted` (solver-proved, solver in the TCB —
    NOT a kernel-checked class), `sat` → `counterexample` (with the model parsed
    back to source variables via `(get-model)`), `unknown`/`timeout` accordingly. If
    Z3 is not on PATH the honest verdict is `solver_error` for every query — an
    absent solver never yields a proof. Only ever called behind an explicit flag.
    Returns `(vcKey, resultClass, counterexampleModel)`. -/
def smtDischarge (queries : List (String × String)) (timeoutSec : Nat)
    (timeoutMs : Option Nat := none)
    : IO (List (String × String × List (String × String))) := do
  if queries.isEmpty then return []
  -- a configured tiny millisecond soft-timeout (`-t:<ms>`) forces `unknown`; the
  -- default is the per-run wall timeout (`-T:<sec>`).
  let timeoutArg := match timeoutMs with
    | some ms => "-t:" ++ toString ms
    | none => "-T:" ++ toString timeoutSec
  let haveZ3 ← (try
      let o ← IO.Process.output { cmd := "bash", args := #["-c", "command -v z3"] }
      pure (o.exitCode == 0)
    catch _ => pure false)
  if !haveZ3 then
    return queries.map (fun (k, _) => (k, "solver_error", []))
  let mut res : List (String × String × List (String × String)) := []
  for (k, script) in queries do
    let r ← (try
        let mk ← IO.Process.output { cmd := "mktemp", args := #["-t", "concrete-vc-XXXXXX"] }
        let path := mk.stdout.trimAscii.toString
        IO.FS.writeFile ⟨path⟩ script
        let out ← IO.Process.output { cmd := "z3", args := #[timeoutArg, path] }
        let _ ← IO.Process.output { cmd := "rm", args := #["-f", path] }
        let stdout := out.stdout
        let line := ((stdout.trimAscii.toString.splitOn "\n").head?.getD "").trimAscii.toString
        if line == "unsat" then pure ("solver_trusted", ([] : List (String × String)))
        else if line == "sat" then
          -- the declared vars are the source names; read each from the model.
          let vars := (script.splitOn "\n").filterMap fun l =>
            let t := l.trimAscii.toString
            if t.startsWith "(declare-const " then ((t.drop "(declare-const ".length).toString.splitOn " ").head?
            else none
          let model := vars.filterMap fun vn => (smtModelValue stdout vn).map (fun x => (vn, x))
          pure ("counterexample", model)
        else if line == "unknown" then pure ("unknown", [])
        else if line == "timeout" then pure ("timeout", [])
        else pure ("solver_error", [])
      catch _ => pure ("solver_error", ([] : List (String × String))))
    res := res ++ [(k, r.1, r.2)]
  return res

/-- Lean replay (Phase 2 #12). Given `(vcKey, leanTheoremSource)` pairs, write each
    theorem to a file and run `lake env lean` on it. Returns the keys Lean
    INDEPENDENTLY closed (exit 0) — those graduate from `solver_trusted` to
    `proved_by_lean_replay`. Only the in-toolchain tactic in the source (`omega`)
    is used; no Mathlib. A theorem omega cannot close simply fails to compile and
    its key is not returned, so the VC honestly stays `solver_trusted`. -/
def leanReplayCheck (goals : List (String × String)) : IO (List String) := do
  if goals.isEmpty then return []
  let mut closed : List String := []
  for (k, src) in goals do
    let ok ← (try
        let tmpDir ← IO.Process.output { cmd := "mktemp", args := #["-d"] }
        let dir := tmpDir.stdout.trimAscii.toString
        IO.FS.writeFile ⟨dir ++ "/vc_replay.lean"⟩ src
        let r ← IO.Process.output { cmd := "lake", args := #["env", "lean", dir ++ "/vc_replay.lean"],
                                    env := #[("LAKE_TERM_ANSI", "0")] }
        let _ ← IO.Process.output { cmd := "rm", args := #["-rf", dir] }
        pure (r.exitCode == 0)
      catch _ => pure false)
    if ok then closed := closed ++ [k]
  return closed

/-- Phase 3 #14: policy inputs derived from the ONE obligation ledger. Builds the
    discharged ledger (folding the external-SMT path when a solver-evidence stance
    is set, so `solver_trusted` is present), then projects the vacuous / assume /
    solver-trusted facts the release policy acts on — replacing the three
    `compute*Quals` side channels. Returns `(vacuousQuals, assumeQuals,
    solverTrustedQuals)`, dep-filtered exactly as before. -/
def computePolicyQuals (policy : Concrete.ProjectPolicy) (modules : List Concrete.Module)
    (depNames : List String) (locMap : Report.FnLocMap) (registry : Concrete.ProofRegistry) :
    IO (List String × List String × List String) := do
  let dvcs ← computeVCsDischarged modules locMap registry
  -- fold the external-SMT path into the ledger only when a stance is set (matches
  -- the old computeSolverTrustedQuals gating; otherwise no solver runs).
  let dvcs ← if policy.solverEvidence.isEmpty then pure dvcs else do
    let smtGoals := Report.overflowSmtGoals modules
    if smtGoals.isEmpty then pure dvcs else do
      let replayGoals := Report.leanReplayGoals modules
      let dvcs := Report.markSmtEligible dvcs smtGoals replayGoals
      let solverId ← z3VersionId
      let results ← smtDischarge smtGoals 5
      let dvcs := Report.foldSmtResults dvcs results solverId
      let trusted := dvcs.filterMap fun v => if v.status == "solver_trusted" then some v.id else none
      let rg := replayGoals.filter (fun (k, _) => trusted.contains k)
      let replayed ← leanReplayCheck rg
      pure (Report.foldReplayResults dvcs replayed)
  let ledger := Concrete.ObligationCore.ledgerOfVCs dvcs
  let keep := fun (q : String) => !depNames.any (fun d => q.startsWith (d ++ "."))
  let vac := (Concrete.ObligationCore.vacuousFunctions ledger).filter keep
  let asm := (Concrete.ObligationCore.assumeFunctions ledger).filter keep
  let st := Concrete.ObligationCore.solverTrustedIds ledger
  return (vac, asm, st)

/-- Render the contracts report plus the call-site obligation section AS A VIEW
    over the one discharged ObligationCore ledger (Phase 3 #15 / #18e).

    Instead of re-running the per-family discharge (the old duplicate path that
    `check_contracts_ledger_parity.sh` guards), this reads `computeVCsDischarged`
    — the exact same ledger `--report obligation-ledger` and policy consume — and
    slices the proved-key sets out of it: a key is omega-proved iff its discharged
    VC carries engine `omega`, bv-proved iff engine `bv_decide` (`dischargeVCs`
    sets the engine per adapter). Each render helper matches only its own family's
    keys, so passing the shared sets is byte-identical to the former separate
    discharge — now single-source, so the two surfaces cannot diverge. -/
def renderContracts (parsedModules : List Concrete.Module) (registry : Concrete.ProofRegistry)
    (locMap : Report.FnLocMap) : IO String := do
  let dvcs ← computeVCsDischarged parsedModules locMap registry
  let omegaProved := dvcs.filterMap fun v => if v.engine == "omega" then some v.id else none
  let bvProved    := dvcs.filterMap fun v => if v.engine == "bv_decide" then some v.id else none
  let obs := Report.callSiteObligations parsedModules
  -- renderCallSites wants bv-proved call sites as obligation INDICES, not keys.
  let bvCallIdx := (List.range obs.length).filter fun i =>
    match obs[i]? with | some o => bvProved.contains o.key | none => false
  let boundsObls := Report.boundsObligations parsedModules
  let divObls := Report.divObligations parsedModules
  let ovfObls := Report.overflowObligations parsedModules
  -- Every helper below is handed the SAME omega/bv proved-key sets and filters its
  -- own family's keys (loop / vacuity / assert / #pre / #bounds / #div / #ovf are
  -- disjoint key spaces). overflow alone needs both (omega vs bv rendering).
  return Report.contractsReport parsedModules registry omegaProved omegaProved
    ++ Report.renderCallSites obs bvCallIdx omegaProved
    ++ Report.renderAssertAssume parsedModules omegaProved
    ++ Report.renderBounds boundsObls omegaProved
    ++ Report.renderDiv divObls omegaProved
    ++ Report.renderOverflow ovfObls omegaProved bvProved

/-- Walk up from `path` for the directory holding a Lake workspace.

Kernel replay used to invoke `lake` with no `cwd`, so the workspace came from the
PROCESS working directory and the verdict depended on where the caller stood
(R-0004 slice 4). Resolving from the input makes the answer a property of what is
being checked. Returns `none` rather than guessing a default: a wrong workspace
would replay against the wrong library and report confident nonsense. -/
partial def findLakeWorkspace (path : String) : IO (Option System.FilePath) := do
  let abs ← IO.FS.realPath (System.FilePath.mk path)
  let rec up (dir : System.FilePath) (fuel : Nat) : IO (Option System.FilePath) := do
    match fuel with
    | 0 => return none
    | fuel + 1 =>
      if (← (dir / "lakefile.toml").pathExists) || (← (dir / "lakefile.lean").pathExists) then
        return some dir
      match dir.parent with
      | some p => if p == dir then return none else up p fuel
      | none => return none
  -- Start at the file's directory; a file path has a parent, a directory is its
  -- own starting point.
  let start := if (← abs.isDir) then abs else (abs.parent.getD abs)
  up start 64

/-- Run pipeline and check a profile constraint.
    If the input file lives inside a `Concrete.toml` project, route
    through project mode so std and other dependencies resolve. -/
def compileAndReport (inputPath : String) (reportType : String)
    (proveTarget : Option String := none) (proveOut : Option String := none)
    (proveForce : Bool := false) (proveEmitLink : Bool := false)
    (proveShowObl : Option String := none) (proveReplay : Bool := false)
    (proveJson : Bool := false) (proveNearestLemmas : Bool := false)
    (proveEmitLean : Bool := false) (proveStdout : Bool := false)
    (proveEmitArtifacts : Bool := false) (proveOutDir : Option String := none)
    (proveCheck : Bool := false) (proveWorkspace : Option String := none)
    (proveNearestId : Option String := none) (reportJson : Bool := false)
    (smtRun : Bool := false) (smtEmit : Bool := false)
    (smtReplay : Bool := false) (emitLeanReplay : Bool := false)
    (smtTimeoutMs : Option Nat := none) : IO UInt32 := do
  let source ← readFile inputPath
  let mainSrcMap : SourceMap := [(inputPath, source)]
  -- Interface report only needs parse + resolveFiles + summary
  if reportType == "interface" then
    match Pipeline.parse source with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := mainSrcMap))
      return 1
    | .ok parsed =>
    match ← Pipeline.resolveFiles (dirOf inputPath) parsed inputPath resolveAllModules with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := mainSrcMap))
      return 1
    | .ok (resolved, _) =>
      let summary := Pipeline.buildSummary resolved
      IO.println (Report.interfaceReport summary.entries)
      return 0
  -- All other reports need the full frontend. If the file is inside a
  -- Concrete.toml project, route through project mode so dependency imports
  -- (e.g. std) resolve; mirrors compileAndCheck.
  let inputDir := dirOf inputPath
  -- Returns (parsed, fullValidCore, scopedValidCore, srcMap). In project
  -- mode the two validCores differ: full covers the entire user package
  -- (used for pc/registry validation, so sibling-file entries don't
  -- appear "unknown"), scoped covers just the file the user invoked
  -- (used to drive report output). In standalone mode they're identical.
  let frontendResult : Except UInt32 (ParsedProgram × ValidatedCore × ValidatedCore × SourceMap) ←
    match ← findProjectRoot inputDir with
    | some root =>
      match ← loadProject root with
      | .error ec => pure (Except.error ec)
      | .ok ctx =>
        let { validCore, parsed, allSrcMap, depNames, .. } := ctx
        let userModules := validCore.coreModules.filter fun m => !depNames.contains m.name
        let fullValidCore : ValidatedCore := { validCore with coreModules := userModules }
        let scopedModules ← scopeUserModulesToFile userModules inputPath root
        let scopedValidCore : ValidatedCore := { validCore with coreModules := scopedModules }
        pure (Except.ok (parsed, fullValidCore, scopedValidCore, allSrcMap))
    | none =>
      match ← Pipeline.runFrontend inputPath source resolveAllModules with
      | .error ds =>
        IO.eprintln (renderDiagnostics ds (sourceMap := mainSrcMap))
        pure (Except.error 1)
      | .ok (parsed, _, validCore, srcMap) =>
        pure (Except.ok (parsed, validCore, validCore, srcMap))
  match frontendResult with
  | .error ec => return ec
  | .ok (parsed, fullValidCore, scopedValidCore, srcMap) =>
    let locMap := Report.buildFnLocMap parsed.modules inputPath
    let simpleLocMap := locMap.map fun e => (e.qualName, (e.file, e.fnSpan.line))
    -- The registry is the in-source proof links (#[proof_by]/#[spec]/...)
    -- synthesized from the FULL user package.
    let registry := Report.synthesizeSourceLinks parsed.modules fullValidCore.coreModules
    -- pc and registry validation run on the FULL user package: a
    -- registry entry naming a function defined in a sibling file must
    -- still validate when the user is querying just one file.
    let pc := extractProofCore fullValidCore simpleLocMap registry
    -- Report output still iterates only the scoped modules.
    let validCore := scopedValidCore
    -- Validate registry against ProofCore and surface warnings/errors
    let regIssues := Concrete.validateRegistry pc registry
    for issue in regIssues do
      IO.eprintln (Concrete.renderRegistryIssue issue)
    let hasRegistryErrors := regIssues.any (·.isError)
    -- `concrete prove <function>`: read-only per-function proof scaffold.
    -- Writes nothing unless --out is given (and then refuses to clobber).
    if let some target := proveTarget then
      match Report.proveResolve pc target with
      | .error msg => IO.eprintln msg; return 1
      | .ok qual =>
        -- --emit-link: print the in-source proof-link block (text or JSON).
        if proveEmitLink then
          IO.println (if proveJson then Report.emitProofLinkJson registry qual inputPath
                      else Report.emitProofLink registry qual)
          return 0
        let provedVCs ← kernelDischargeLoopVCs (Report.loopVCGoals parsed.modules)
        -- --nearest-lemmas: proof-recipe hints per obligation kind + features.
        if proveNearestLemmas then
          IO.println (Report.nearestLemmas pc parsed.modules qual provedVCs proveJson proveNearestId)
          return 0
        -- --emit-lean: compilable single-function Lean proof stub (ends in `sorry`).
        if proveEmitLean then
          let stub := Report.emitLeanStub pc registry parsed.modules qual provedVCs
          match proveOut with
          | some path =>
            if proveStdout then IO.println stub; return 0
            if (← System.FilePath.pathExists path) && !proveForce then
              IO.eprintln s!"refusing to overwrite existing '{path}' (pass --force to clobber)."
              return 1
            if let some parent := (System.FilePath.mk path).parent then
              IO.FS.createDirAll parent
            IO.FS.writeFile path stub
            IO.println s!"wrote Lean proof stub for {qual} to {path}"
            return 0
          | none => IO.println stub; return 0
        -- --emit-artifacts: write a reproducible bundle per failed obligation.
        if proveEmitArtifacts then
          let proveStatus := (pc.obligations.find? (·.functionId.qualName == qual)).map (·.status.canonical) |>.getD "missing"
          let obs := Report.callSiteObligations parsed.modules
          let myCands := ((List.range obs.length).zip obs).filterMap fun (i, o) =>
            if o.caller == qual then o.leanGoal.map (fun g => (i, g)) else none
          let bvProved ← bvDischargeCallSites myCands
          let failingCalls := myCands.filter (fun (i, _) => !bvProved.contains i)
          let arts := Report.proveArtifacts pc registry parsed.modules qual inputPath provedVCs failingCalls proveStatus
          if arts.isEmpty then
            IO.println s!"no failed obligations for {qual} (nothing to emit)."
            return 0
          let baseDir := (proveOutDir.getD ".build/prove") ++ "/" ++ Report.artifactDirName qual
          for a in arts do
            let dir := baseDir ++ "/" ++ a.dirName
            IO.FS.createDirAll dir
            IO.FS.writeFile (dir ++ "/context.json") a.context
            IO.FS.writeFile (dir ++ "/failed.lean") a.failedLean
            IO.FS.writeFile (dir ++ "/command.txt") a.command
            IO.FS.writeFile (dir ++ "/README.txt") a.readme
            IO.println s!"wrote {dir}/  (context.json, failed.lean, command.txt, README.txt)"
          IO.println s!"{arts.length} failed-obligation artifact(s) under {baseDir}/"
          return 0
        -- --check: run the Lean kernel on this function's linked theorem(s) and
        -- map the result back to obligation id / theorem / status / span / error.
        -- The closed repair loop: agents read structured status, not raw stderr.
        if proveCheck then
          let q := Report.jsonStr
          -- (obligationId, theorem, originalObligationStatus) for this function
          let mut checks : List (String × String × String) := []
          for o in pc.obligations do
            if o.functionId.qualName == qual then
              match o.spec with
              | some s =>
                if !checks.any (fun (_, t, _) => t == s.proofName) then
                  checks := checks ++ [(s!"{qual}#refines_spec", s.proofName, o.status.canonical)]
              | none => pure ()
          for e in registry do
            if e.function == qual then
              match e.ensuresProof with
              | some t => if !checks.any (fun (_, tt, _) => tt == t) then
                            checks := checks ++ [(s!"{qual}#ensures", t, "ensures")]
              | none => pure ()
          let srcLine := ((parsed.modules.flatMap Report.allFunctions).find?
            (fun (pfx, fn) => pfx ++ fn.name == qual)).map (fun (_, fn) => fn.span.line) |>.getD 0
          let stubCmd := s!"concrete prove {inputPath} {qual} --emit-lean --out failed.lean --force"
          -- No linked theorem: report missing_theorem without invoking Lean.
          if checks.isEmpty then
            if proveJson then
              IO.println (String.join ["{\n  \"function\": ", q qual, ",\n  \"schema_version\": ", q proveSchemaVersion,
                ",\n  \"all_checked\": false,\n  \"checks\": [\n",
                "    {\"obligation_id\": ", q s!"{qual}#refines_spec", ", \"theorem\": null, \"status\": \"missing_theorem\"",
                ", \"source_line\": ", toString srcLine, ", \"stub_command\": ", q stubCmd, "}\n  ],\n",
                "  \"lean_error\": ", q "no #[proof_by]/#[ensures_proof] theorem linked on this function",
                ",\n  \"summary\": ", q "0 checked, 1 missing theorem", "\n}"])
            else
              IO.println s!"=== concrete prove --check: {qual} ===\n\n  ✗ {qual}#refines_spec — no linked theorem (missing_theorem)\n\nSummary: 0 checked, 1 missing theorem."
            return 2
          -- Invoke the Lean kernel once on all linked theorems.
          let tmp ← IO.Process.output { cmd := "mktemp", args := #["-d"] }
          let tmpPath := tmp.stdout.trimAscii.toString ++ "/prove_check.lean"
          -- `import Examples` too: flagship example proofs live in the separate
          -- `Examples` Lake library, not the compiler umbrella (see check-proofs).
          let mut src := "import Concrete\nimport Examples\n\n-- Auto-generated by `concrete prove --check`.\n"
          for (_, thm, _) in checks do src := src ++ s!"#check @{thm}\n"
          IO.FS.writeFile ⟨tmpPath⟩ src
          let r ← IO.Process.output { cmd := "lake", args := #["env", "lean", tmpPath], env := #[("LAKE_TERM_ANSI", "0")] }
          let combined := r.stdout.trimAscii.toString ++ "\n" ++ r.stderr.trimAscii.toString
          let _ ← IO.Process.output { cmd := "rm", args := #["-rf", tmp.stdout.trimAscii.toString] }
          let has := fun (s sub : String) => (s.splitOn sub).length != 1
          let anyNeedle := checks.any (fun (_, thm, _) => has combined s!"`{thm}`")
          let envFailure := r.exitCode != 0 && !anyNeedle
          let results := checks.map fun (id, thm, st) =>
            let failed := has combined s!"`{thm}`"
            let status :=
              if envFailure then "env_failure"
              else if failed then (if has combined "unknown" then "missing_theorem" else "failed")
              else if st == "stale" then "stale"
              else "checked"
            (id, thm, status)
          let allChecked := results.all (fun (_, _, st) => st == "checked")
          let exitCode : UInt32 :=
            if envFailure then 5
            else if results.any (fun (_, _, st) => st == "failed") then 4
            else if results.any (fun (_, _, st) => st == "missing_theorem") then 2
            else if results.any (fun (_, _, st) => st == "stale") then 3
            else 0
          let leanErr := if allChecked then "" else String.ofList (combined.toList.take 800)
          if proveJson then
            let body := results.map fun (id, thm, st) =>
              String.join ["    {\"obligation_id\": ", q id, ", \"theorem\": ", q thm, ", \"status\": ", q st,
                ", \"source_line\": ", toString srcLine, ", \"stub_command\": ", q stubCmd, "}"]
            IO.println (String.join ["{\n  \"function\": ", q qual, ",\n  \"schema_version\": ", q proveSchemaVersion,
              ",\n  \"toolchain\": ", q ((← (try IO.FS.readFile ⟨"lean-toolchain"⟩ catch _ => pure "unknown")).trimAscii.toString),
              ",\n  \"all_checked\": ", (if allChecked then "true" else "false"),
              ",\n  \"checks\": [\n", ",\n".intercalate body, "\n  ],\n",
              "  \"lean_error\": ", q leanErr,
              ",\n  \"summary\": ", q s!"{results.countP (fun (_,_,s) => s == "checked")} checked, {results.countP (fun (_,_,s) => s != "checked")} not checked",
              "\n}"])
          else
            let mut out := s!"=== concrete prove --check: {qual} ===\n\n"
            for (id, thm, st) in results do
              let mark := if st == "checked" then "✓" else "✗"
              out := out ++ s!"  {mark} {id} — {thm} ({st})\n"
            if !leanErr.isEmpty then out := out ++ s!"\nLean output:\n{leanErr}\n"
            out := out ++ s!"\nSummary: {results.countP (fun (_,_,s) => s == "checked")} checked, {results.countP (fun (_,_,s) => s != "checked")} not checked"
            IO.println out
          return exitCode
        -- --workspace DIR: compose the read-only surfaces into one directory.
        if let some wsArg := proveWorkspace then
          let dir := if wsArg.isEmpty then s!".build/prove/{Report.artifactDirName qual}/workspace" else wsArg
          let files := Report.workspaceFiles pc registry parsed.modules qual inputPath proveSchemaVersion provedVCs
          IO.FS.createDirAll dir
          for (rel, contents) in files do
            let path := dir ++ "/" ++ rel
            if let some parent := (System.FilePath.mk path).parent then
              IO.FS.createDirAll parent
            IO.FS.writeFile path contents
            if rel.endsWith ".sh" then
              let _ ← IO.Process.output { cmd := "chmod", args := #["+x", path] }
          IO.println s!"wrote proof workspace for {qual} to {dir}/ ({files.length} files)"
          return 0
        -- --show-obligation <id>: print one obligation in full (text or JSON).
        if let some oblId := proveShowObl then
          IO.println (if proveJson then Report.showObligationJson parsed.modules qual oblId provedVCs inputPath
                      else Report.showObligation parsed.modules qual oblId provedVCs)
          return 0
        -- --replay: re-run omega / bv_decide discharge and report per obligation.
        if proveReplay then
          let myLoop := (Report.loopVCGoals parsed.modules).filter (fun (k, _) => k.startsWith (qual ++ "@"))
          let obs := Report.callSiteObligations parsed.modules
          let myCands := ((List.range obs.length).zip obs).filterMap fun (i, o) =>
            if o.caller == qual then o.leanGoal.map (fun g => (i, g)) else none
          let bvProved ← bvDischargeCallSites myCands
          if proveJson then
            let q := Report.jsonStr
            let loopObs := myLoop.map fun (k, _) =>
              s!"\{\"id\": {q k}, \"engine\": \"omega\", \"closes\": {if provedVCs.contains k then "true" else "false"}}"
            let callObs := myCands.map fun (i, _) =>
              s!"\{\"id\": {q s!"{qual}#call{i}"}, \"engine\": \"bv_decide\", \"closes\": {if bvProved.contains i then "true" else "false"}}"
            let allPass := myLoop.all (fun (k, _) => provedVCs.contains k) && myCands.all (fun (i, _) => bvProved.contains i)
            IO.println (String.join [
              "{\n",
              s!"  \"function\": {q qual},\n",
              s!"  \"all_pass\": {if allPass then "true" else "false"},\n",
              s!"  \"obligations\": [{", ".intercalate (loopObs ++ callObs)}],\n",
              s!"  \"next_actions\": [\{\"kind\": \"run_audit\", \"command\": {q s!"concrete audit {inputPath}"}, \"output_format\": \"text\", \"resolves\": {if allPass then "\"proved\"" else "\"stale\""}}]\n",
              "}" ])
            return (if myLoop.all (fun (k, _) => provedVCs.contains k) && myCands.all (fun (i, _) => bvProved.contains i) then 0 else 4)
          let mut out := s!"=== concrete prove --replay: {qual} ===\n"
          out := out ++ "\nloop obligations (omega):\n"
          if myLoop.isEmpty then out := out ++ "  (none)\n"
          for (k, _) in myLoop do
            out := out ++ (if provedVCs.contains k then s!"  ok   {k} — still closes\n" else s!"  FAIL {k} — no longer closes\n")
          out := out ++ "\ncall-site obligations (bv_decide):\n"
          if myCands.isEmpty then out := out ++ "  (none)\n"
          for (i, _) in myCands do
            out := out ++ (if bvProved.contains i then s!"  ok   call obligation #{i} — still closes\n" else s!"  FAIL call obligation #{i} — no longer closes\n")
          IO.println out
          return 0
        -- Process exit code follows the documented taxonomy (see --help=agent):
        --   0 proved/clean · 2 obligations missing · 3 stale evidence.
        let proveStatus := (pc.obligations.find? (·.functionId.qualName == qual)).map (·.status.canonical) |>.getD "missing"
        let proveExit : UInt32 := match proveStatus with
          | "stale" => ExitCode.staleEvidence
          | "missing" => ExitCode.obligationsMissing
          | "blocked" => ExitCode.obligationsMissing
          | _ => ExitCode.ok
        -- --json: structured proof context + next_actions.
        if proveJson then
          IO.println (Report.proveReportJson pc registry parsed.modules qual provedVCs inputPath proveSchemaVersion)
          return proveExit
        let report := Report.proveReport pc registry parsed.modules qual provedVCs
        match proveOut with
        | none => IO.println report; return proveExit
        | some path =>
          if (← System.FilePath.pathExists path) && !proveForce then
            IO.eprintln s!"refusing to overwrite '{path}' (pass --force to replace it)"
            return 1
          writeFile path report
          IO.println s!"wrote proof scaffold to {path}"
          return 0
    if reportType == "backend-contracts" then
      -- The guarantees the code generator commits to (Phase 4 #17a), rendered from
      -- the same Concrete.Backend facts the emitter uses, plus this program's
      -- trusted boundaries. Human + JSON from one source.
      if reportJson then IO.println (Concrete.Backend.toJson validCore.coreModules 1)
      else IO.println (Concrete.Backend.report validCore.coreModules)
      return 0
    if reportType == "contracts" then
      IO.println (← renderContracts parsed.modules registry locMap)
      return 0
    if reportType == "obligation-ledger" then
      -- Phase 3: the unified ObligationCore ledger — the discharged VC families
      -- (runtime-safety, contracts incl. clause diagnostics) PLUS the proof-link
      -- freshness family (#11), projected into the one schema.
      let dvcs ← computeVCsDischarged parsed.modules locMap registry
      let vcLedger := Concrete.ObligationCore.ledgerOfVCs dvcs
      let proofLinks := Concrete.ObligationCore.proofLinkLedger
        (Report.proofStatusEntries validCore.coreModules locMap registry pc)
      let ledger := vcLedger ++ proofLinks
      if reportJson then IO.println (Concrete.ObligationCore.ledgerJson ledger 1)
      else IO.println (Concrete.ObligationCore.ledgerReport ledger)
      return 0
    if reportType == "vcs" then
      let dvcs ← computeVCsDischarged parsed.modules locMap registry
      -- External-SMT path is OPT-IN. Without --smt/--emit-smt nothing here touches
      -- a solver and no VC ever advertises `smt` — the kernel boundary is the default.
      let smtGoals := Report.overflowSmtGoals parsed.modules
      let replayGoals := Report.leanReplayGoals parsed.modules
      if smtEmit then
        -- stable SMT-LIB output path: emit the scripts (no solver needed).
        if smtGoals.isEmpty then IO.println "; no SMT-eligible VCs (nonlinear arithmetic) in this file"
        for (k, script) in smtGoals do
          IO.println s!";; ==== {k} ====\n{script}\n"
        return 0
      if emitLeanReplay then
        -- Lean replay artifact: the same obligation as a kernel-checkable theorem.
        if replayGoals.isEmpty then IO.println "-- no SMT-eligible VCs to replay in this file"
        for (k, src) in replayGoals do
          IO.println s!"-- ==== {k} ====\n-- check: lake env lean vc_replay.lean\n{src}\n"
        return 0
      let dvcs := if smtRun || smtEmit then Report.markSmtEligible dvcs smtGoals replayGoals else dvcs
      let dvcs ← if smtRun then do
          let solverId ← z3VersionId
          let results ← smtDischarge smtGoals 5 smtTimeoutMs
          let dvcs := Report.foldSmtResults dvcs results solverId
          -- --replay: try to kernel-check each solver_trusted VC in Lean; a success
          -- graduates it to proved_by_lean_replay (solver dropped from the claim).
          if smtReplay then
            let trusted := dvcs.filterMap fun v => if v.status == "solver_trusted" then some v.id else none
            let rg := replayGoals.filter (fun (k, _) => trusted.contains k)
            let replayed ← leanReplayCheck rg
            pure (Report.foldReplayResults dvcs replayed)
          else pure dvcs
        else pure dvcs
      -- Phase 3 #18d: the VC schedule IS a list of obligations (one record type),
      -- so the VC reports render it directly — no conversion glue.
      if reportJson then
        IO.println (Report.vcsJson dvcs 1)
      else
        IO.println (Report.vcsReport dvcs)
      return 0
    if reportType == "caps" then
      IO.println (Report.capabilityReport validCore.coreModules)
      return 0
    if reportType == "unsafe" then
      IO.println (Report.unsafeReport validCore.coreModules pc)
      return 0
    if reportType == "layout" then
      IO.println (Report.layoutReport validCore.coreModules)
      return 0
    if reportType == "alloc" then
      IO.println (Report.allocReport validCore.coreModules)
      return 0
    if reportType == "authority" then
      IO.println (Report.authorityReport validCore.coreModules)
      return 0
    if reportType == "proof" then
      IO.println (Report.proofReport validCore.coreModules pc)
      return 0
    if reportType == "eligibility" then
      IO.println (Report.eligibilityReport pc)
      return 0
    if reportType == "proof-status" then
      IO.println (Report.proofStatusReport validCore.coreModules locMap srcMap (registry := registry) (pc := pc))
      return (if hasRegistryErrors then 1 else 0)
    if reportType == "obligations" then
      IO.println (Report.obligationsReport validCore.coreModules locMap registry pc)
      return (if hasRegistryErrors then 1 else 0)
    if reportType == "proof-deps" then
      IO.println (Report.proofDepsReport pc)
      return 0
    if reportType == "proof-diagnostics" then
      IO.println (Report.proofDiagnosticsReport (pc := pc))
      return 0
    if reportType == "proof-bundle" then
      let ms ← IO.monoMsNow
      let timestamp := toString ms
      let ident ← compilerIdentity
      IO.println (Report.proofBundleJson inputPath timestamp ident validCore.coreModules locMap (registry := registry) (pc := pc))
      return (if hasRegistryErrors then 1 else 0)
    if reportType == "extraction" then
      IO.println (Report.extractionReport (registry := registry) (pc := pc))
      return 0
    if reportType == "lean-stubs" then
      IO.println (Report.leanStubsReport pc (registry := registry))
      return 0
    if reportType == "check-proofs" then
      -- Collect all proof names from obligations with specs attached
      let proofNames := pc.obligations.filterMap fun o =>
        match o.spec with
        | some s =>
          -- `unbound` is replayable too, and must be: kernel replay is how a
          -- link WITHOUT a stored subject earns one. Excluding it would leave
          -- no path from unbound to bound — you could never obtain the receipt
          -- the fingerprint is supposed to record.
          if o.status == .proved || o.status == .stale || o.status == .unbound then
            some (o.functionId.qualName, s.proofName, s.source, o.status)
          else none
        | none => none
      if proofNames.isEmpty then
        if reportJson then
          IO.println "{\n  \"schema_version\": \"1\",\n  \"all_checked\": true,\n  \"checks\": [],\n  \"lean_error\": \"\",\n  \"summary\": {\"verified\": 0, \"failed\": 0, \"total\": 0}\n}"
        else
          IO.println "=== Lean Proof Kernel Check ===\n\nNo proved, stale, or unbound obligations with proof names to check."
        return 0
      -- Generate temp Lean file with #check for each theorem
      let tmpDir ← IO.Process.output { cmd := "mktemp", args := #["-d"] }
      let tmpPath := tmpDir.stdout.trimAscii.toString ++ "/check_proofs.lean"
      -- Import the compiler umbrella (`Concrete`) for infrastructure/refinement
      -- theorems, AND the `Examples` library for the flagship example-correctness
      -- proofs (`Examples.<Ex>.Proofs.*`). The example proofs were moved out of the
      -- compiler lib into their own `Examples` Lake library, so `import Concrete`
      -- alone no longer makes them reachable for `#check`; this proof-check target
      -- is the one place that legitimately imports the example proof code.
      let mut leanSrc := "import Concrete\nimport Examples\n\n"
      leanSrc := leanSrc ++ "-- Auto-generated by `concrete --report check-proofs`\n"
      leanSrc := leanSrc ++ "-- Verifies that referenced Lean theorems exist and type-check.\n\n"
      for (fn, proofName, _, _) in proofNames do
        leanSrc := leanSrc ++ s!"-- {fn}\n#check @{proofName}\n\n"
      -- Also kernel-check source-contract discharge theorems (the `ensures_proof`
      -- naming the theorem that proves a `#[ensures(...)]` obligation), so an
      -- obligation reported `proved_by_lean` is backed by a real kernel check.
      let ensuresThms := registry.filterMap fun e => e.ensuresProof.map (e.function, ·)
      for (fn, thm) in ensuresThms do
        leanSrc := leanSrc ++ s!"-- {fn} (ensures)\n#check @{thm}\n\n"
      IO.FS.writeFile ⟨tmpPath⟩ leanSrc
      -- Resolve the proof workspace from the INPUT, not the process working
      -- directory (R-0004 slice 4). `lake` finds its workspace by walking up
      -- from wherever it is invoked, so with no `cwd` set this verdict depended
      -- on where the user happened to stand: the same file by absolute path gave
      -- "3 verified, 0 failed" from the repo root and "0 verified, 3 failed"
      -- from /tmp. Worse, it blamed each theorem with `theorem_lookup` — the
      -- theorems were fine; the workspace was never found.
      -- Input first, then the caller's own directory. Resolving ONLY from the
      -- input was too strict and broke a legitimate case: a tool that copies
      -- sources to a temp dir and replays them from inside the repo (which is
      -- how check_purecore_proofs.sh exercises std). Such an input has no
      -- workspace of its own, and the caller's workspace is then the only
      -- available answer — refusing it made 12 real, kernel-verified std proofs
      -- report as unreachable.
      --
      -- The cwd-independence property is preserved where it means something: an
      -- input that HAS a workspace always resolves to that one, so the same file
      -- gives the same verdict from anywhere. Only an input with no workspace
      -- falls back, and the report names which workspace was used so the answer
      -- is never anonymous.
      let wsFromInput ← findLakeWorkspace inputPath
      let wsRoot ← match wsFromInput with
        | some w => pure (some w)
        | none   => findLakeWorkspace "."
      match wsRoot with
      | none =>
        -- Say what is actually wrong. Reporting N missing theorems for one
        -- missing workspace sends the reader to look for the wrong thing.
        let msg := s!"cannot locate a Lake workspace for '{inputPath}' (no lakefile.toml or lakefile.lean in any parent directory), so the Lean theorems it references cannot be replayed"
        if reportJson then
          IO.println s!"\{\n  \"schema_version\": \"1\",\n  \"all_checked\": false,\n  \"checks\": [],\n  \"lean_error\": \"{msg}\",\n  \"summary\": \{\"verified\": 0, \"failed\": 0, \"total\": 0}\n}"
        else
          IO.println s!"=== Lean Proof Kernel Check ===\n\nerror: {msg}"
        return 1
      | some ws =>
      -- Invoke lake env lean to check the file, from the resolved workspace.
      let result ← IO.Process.output {
        cmd := "lake"
        args := #["env", "lean", tmpPath]
        cwd := ws
        env := #[("LAKE_TERM_ANSI", "0")]
      }
      -- Parse results: Lean may put errors on stdout or stderr
      let combined := result.stdout.trimAscii.toString ++ "\n" ++ result.stderr.trimAscii.toString
      let mut verified : List String := []
      let mut failed : List (String × String) := []
      for (fn, proofName, _, _) in proofNames do
        -- Check if this proof name produced an error (Lean uses backticks in error messages)
        let errNeedle := s!"`{proofName}`"
        let stderrParts := combined.splitOn errNeedle
        let hasError := stderrParts.length != 1
        if hasError then
          failed := failed ++ [(fn, proofName)]
        else
          verified := verified ++ [fn]
      -- If exit code non-zero but no specific failures found, mark all as failed
      if result.exitCode != 0 && failed.isEmpty then
        for (fn, proofName, _, _) in proofNames do
          if !failed.any (fun (f, _) => f == fn) then
            failed := failed ++ [(fn, proofName)]
        verified := []
      let generalFailure := result.exitCode != 0 && failed.isEmpty
      let tc ← try
        let tcContent ← IO.FS.readFile ⟨"lean-toolchain"⟩
        pure tcContent.trimAscii.toString
      catch _ => pure "unknown"
      -- --json: structured whole-file proof-check summary (human output unchanged).
      if reportJson then
        let q := Report.jsonStr
        let lineOf := fun (fn : String) =>
          ((parsed.modules.flatMap Report.allFunctions).find?
            (fun (pfx, f) => pfx ++ f.name == fn)).map (fun (_, f) => f.span.line) |>.getD 0
        let has := fun (sub : String) => (combined.splitOn sub).length != 1
        let statusOf := fun (thm : String) (oblStatus : String) =>
          if generalFailure then "env_failure"
          else if has s!"`{thm}`" then (if has "unknown" then "missing_theorem" else "failed")
          else if oblStatus == "stale" then "stale"
          else "checked"
        let checkObj := fun (fn thm kind origin oblStatus : String) =>
          String.join ["    {\"function\": ", q fn, ", \"theorem\": ", q thm, ", \"obligation_kind\": ", q kind,
            ", \"origin\": ", q origin, ", \"status\": ", q (statusOf thm oblStatus),
            ", \"source_line\": ", toString (lineOf fn), "}"]
        let refChecks := proofNames.map fun (fn, pn, src, st) =>
          checkObj fn pn "refinement" (if src == .registry then "source_linked" else "hardcoded") st.canonical
        let ensChecks := ensuresThms.map fun (fn, thm) => checkObj fn thm "ensures" "source_linked" "proved"
        let allObjs := refChecks ++ ensChecks
        let leanErr := if generalFailure || !failed.isEmpty then String.ofList (combined.toList.take 800) else ""
        IO.println (String.join [
          "{\n  \"schema_version\": ", q "1", ",\n  \"toolchain\": ", q tc,
          ",\n  \"all_checked\": ", (if failed.isEmpty && !generalFailure then "true" else "false"),
          ",\n  \"checks\": [\n", ",\n".intercalate allObjs, "\n  ],\n",
          "  \"lean_error\": ", q leanErr,
          ",\n  \"summary\": {\"verified\": ", toString verified.length, ", \"failed\": ", toString failed.length,
          ", \"total\": ", toString (proofNames.length + ensuresThms.length), "}\n}"])
        let _ ← IO.Process.output { cmd := "rm", args := #["-rf", tmpDir.stdout.trimAscii.toString] }
        return (if failed.isEmpty && !generalFailure then 0 else 1)
      -- Render report
      let mut out := "=== Lean Proof Kernel Check ===\n"
      -- Name the workspace. Slice 4 needs a deterministic workspace identity in
      -- the receipt, and a verdict that does not say where it was produced
      -- cannot be audited — especially in the fallback case above.
      out := out ++ s!"\nWorkspace: {ws}"
      out := out ++ (if wsFromInput.isSome then " (from input)\n" else " (from working directory; the input is outside any workspace)\n")
      out := out ++ s!"\nToolchain: "
      out := out ++ tc ++ "\n"
      if !verified.isEmpty then
        out := out ++ s!"\n  Kernel-verified ({verified.length}):\n"
        for fn in verified do
          let proofName := (proofNames.find? fun (f, _, _, _) => f == fn).map (·.2.1) |>.getD "?"
          let source := (proofNames.find? fun (f, _, _, _) => f == fn).map (·.2.2.1) |>.getD .hardcoded
          let sourceTag := if source == .registry then "registry" else "hardcoded"
          out := out ++ s!"    ✓ {fn} — {proofName} ({sourceTag})\n"
      if !failed.isEmpty then
        out := out ++ s!"\n  Failed ({failed.length}):\n"
        for (fn, proofName) in failed do
          out := out ++ s!"    ✗ {fn} — {proofName} (theorem not found)\n"
      if !ensuresThms.isEmpty then
        out := out ++ s!"\n  Contract obligations — #[ensures] discharge ({ensuresThms.length}):\n"
        for (fn, thm) in ensuresThms do
          let mark := if (combined.splitOn s!"`{thm}`").length != 1 then "✗" else "✓"
          out := out ++ s!"    {mark} {fn} — ensures discharged by {thm}\n"
      if generalFailure then
        out := out ++ s!"\n  Lean check failed (exit code {result.exitCode}):\n"
        out := out ++ s!"    {combined.take 500}\n"
      -- Generate taxonomy diagnostics for failures
      let checkDiags := Concrete.checkProofResultsToDiagnostics
        (failed.map fun (fn, pn) => (fn, pn, true))
      if !checkDiags.isEmpty then
        out := out ++ s!"\n  Diagnostics ({checkDiags.length}):\n"
        for d in checkDiags do
          out := out ++ s!"    [{d.kind.code}] {d.function}: failure={d.failureClass}, repair={d.repairClass}\n"
      out := out ++ s!"\nSummary: {verified.length} verified, {failed.length} failed"
      if generalFailure then
        out := out ++ " (general compilation error)"
      -- Clean up temp dir
      let _ ← IO.Process.output { cmd := "rm", args := #["-rf", tmpDir.stdout.trimAscii.toString] }
      IO.println out
      return (if failed.isEmpty && !generalFailure then 0 else 1)
    if reportType == "diagnostics-json" then
      IO.println (Report.diagnosticsJson validCore.coreModules locMap (registry := registry) (pc := pc))
      return 0
    if reportType == "schema" then
      IO.println Report.schemaReport
      return 0
    if reportType == "diagnostic-codes" then
      IO.println Report.diagnosticCodesReport
      return 0
    if reportType == "effects" then
      IO.println (Report.effectsReport validCore.coreModules locMap pc)
      return 0
    if reportType == "arithmetic" then
      IO.println (Report.arithmeticReport validCore.coreModules locMap)
      return 0
    if reportType == "recursion" then
      IO.println (Report.recursionReport pc)
      return 0
    if reportType == "stack-depth" then
      IO.println (Report.stackDepthReport validCore.coreModules locMap pc)
      return 0
    if reportType == "fingerprints" then
      IO.println (Report.fingerprintReport pc)
      return 0
    if reportType == "consistency" then
      let violations := pc.selfCheck
      IO.println (ConsistencyViolation.render violations)
      if violations.isEmpty then return 0 else return 1
    if reportType == "audit" then
      -- fold the kernel-checked VC discharge into the reviewer artifact (no
      -- external solver by default — SMT evidence stays opt-in via --report vcs --smt).
      -- Phase 3 #18d: one record type — the audit VC summary reads the obligation
      -- schedule directly.
      let auditVCs ← computeVCsDischarged parsed.modules locMap registry
      let vcSum := Report.vcAuditSummary auditVCs
      IO.println (Report.auditReport validCore.coreModules locMap srcMap (registry := registry) (pc := pc) (vcSummary := vcSum))
      if Report.hasContracts parsed.modules then
        IO.println (← renderContracts parsed.modules registry locMap)
      return (if hasRegistryErrors then 1 else 0)
    if reportType == "verify" then
      -- Pass-by-pass verify gates: post-elab, post-mono, post-lower,
      -- post-cleanup. Each gate's diagnostics are reported separately
      -- per docs/VERIFY_GATES.md. Earlier failures (mono refusing to
      -- run, lower aborting entirely) surface via the standard
      -- Pipeline.* error path; runVerifyGates short-circuits at the
      -- first such failure.
      let r := Pipeline.runVerifyGates validCore
      IO.println (renderVerifyGates r.postElab r.postMono r.postLower r.postCleanup)
      if r.errorCount > 0 then return 1 else return 0
    if reportType == "traceability" then
      match Pipeline.monomorphize validCore with
      | .error ds =>
        IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
        return 1
      | .ok mono =>
        match Pipeline.lower mono with
        | .error ds =>
          IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
          return 1
        | .ok ssa =>
          IO.println (Report.traceabilityReport validCore.coreModules mono.coreModules ssa.ssaModules locMap (registry := registry) (pc := pc))
          return 0
    if reportType == "mono" then
      match Pipeline.monomorphize validCore with
      | .error ds =>
        IO.eprintln (renderDiagnostics ds (sourceMap := srcMap))
        return 1
      | .ok mono =>
        IO.println (Report.monoReport validCore.coreModules mono.coreModules)
        return 0
    IO.eprintln s!"Unknown report type: {reportType}. Use: caps, unsafe, layout, interface, alloc, mono, authority, proof, eligibility, proof-status, obligations, extraction, proof-diagnostics, proof-deps, proof-bundle, lean-stubs, check-proofs, traceability, diagnostics-json, schema, diagnostic-codes, effects, recursion, fingerprints, consistency, vcs, obligation-ledger, backend-contracts, verify, audit"
    return 1

def compileAndCheck (inputPath : String) (checkType : String) : IO UInt32 := do
  if checkType != "predictable" then
    IO.eprintln s!"Unknown check type: {checkType}. Use: predictable"
    return 1
  let inputDir := dirOf inputPath
  match ← findProjectRoot inputDir with
  | some root =>
    match ← loadProject root with
    | .error exitCode => return exitCode
    | .ok ctx =>
      let { validCore, parsed, allSrcMap, depNames, .. } := ctx
      -- Drop dependency modules (std etc.) so the report focuses on
      -- user-package code.
      let userModules := validCore.coreModules.filter fun m => !depNames.contains m.name
      -- Build the ProofCore from the FULL user package: recursion
      -- classification, call graph, and extern info must reflect every
      -- caller — even ones in sibling files — for a per-file query to
      -- be accurate.
      let fullUserValidCore : ValidatedCore := { validCore with coreModules := userModules }
      let locMap := Report.buildFnLocMap parsed.modules inputPath
      let simpleLocMap := locMap.map fun (e : Report.FnLocEntry) => (e.qualName, (e.file, e.fnSpan.line))
      let pc := extractProofCore fullUserValidCore simpleLocMap
      -- Scope to the specific file the user invoked for the report
      -- output itself.
      let scopedModules ← scopeUserModulesToFile userModules inputPath root
      let (pass, report) := Report.checkPredictable scopedModules locMap allSrcMap pc
      IO.println report
      return if pass then 0 else 1
  | none =>
    -- Standalone mode (no Concrete.toml in the ancestor chain).
    let source ← readFile inputPath
    match ← Pipeline.runFrontend inputPath source resolveAllModules with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := [(inputPath, source)]))
      return 1
    | .ok (parsed, _, validCore, _) =>
      let locMap := Report.buildFnLocMap parsed.modules inputPath
      let simpleLocMap := locMap.map fun (e : Report.FnLocEntry) => (e.qualName, (e.file, e.fnSpan.line))
      let pc := extractProofCore validCore simpleLocMap
      let srcMap : SourceMap := [(inputPath, source)]
      let (pass, report) := Report.checkPredictable validCore.coreModules locMap srcMap pc
      IO.println report
      return if pass then 0 else 1

/-- Compile a project from Concrete.toml. -/
def compileBuild (projectRoot : String) (outputPath : Option String) (emitLLVM : Bool) (quiet : Bool := false) : IO UInt32 := do
  match ← loadProject projectRoot (stripTestFns := true) with
  | .error exitCode => return exitCode
  | .ok ctx =>
    let { validCore, parsed, allSrcMap, tomlContent, mainPath, depNames, policy, policyWarnings,
          policyLocMap, registry, pc, .. } := ctx
    -- [policy], location map, registry, and ProofCore all come from loadProject.
    for w in policyWarnings do IO.eprintln w
    if !(← enforceProvenRuntimeViolations parsed.modules allSrcMap) then
      return 1
    if !policy.isEmpty then
      let (vac, asm, st) ← computePolicyQuals policy parsed.modules depNames policyLocMap registry
      let policyDs := enforcePolicy policy validCore.coreModules
        (locMap := policyLocMap) (pc := pc) (depNames := depNames) (vacuousQuals := vac)
        (assumeQuals := asm) (solverTrustedQuals := st)
      if hasErrors policyDs then
        IO.eprintln (renderDiagnostics policyDs (sourceMap := allSrcMap))
        return 1
    match Pipeline.monomorphize validCore with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := allSrcMap))
      return 1
    | .ok mono =>
    match Pipeline.lower mono with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := allSrcMap))
      return 1
    | .ok ssa =>
      let llvmIR := Pipeline.emit ssa
      let llPath := mainPath ++ ".ll"
      writeFile llPath llvmIR
      if emitLLVM then
        IO.println llvmIR
        return 0
      -- Validate LLVM IR (if llvm-as available)
      let llValid ← validateLLVMIR llPath
      if !llValid then
        IO.FS.removeFile ⟨llPath⟩
        return 1
      -- Determine output path
      let outPath := match outputPath with
        | some p => p
        | none =>
          -- Extract package name from Concrete.toml
          let nameLines := tomlContent.splitOn "\n" |>.filter (·.trimAscii.toString.startsWith "name")
          match nameLines with
          | l :: _ =>
            match l.splitOn "\"" with
            | _ :: n :: _ => n
            | _ => "a.out"
          | _ => "a.out"
      let args ← clangArgs llPath outPath
      let exitCode ← runCmd "clang" args
      if exitCode != 0 then
        IO.eprintln "clang compilation failed"
        return exitCode
      IO.FS.removeFile ⟨llPath⟩
      if !quiet then
        IO.println s!"Built {outPath}"
        -- Print proof summary line (user package only)
        IO.println (Report.proofSummaryLine (pc.scopeToUser depNames))
      return 0

/-- Run tests for a project from Concrete.toml. Like compileBuild but in test mode. -/
partial def compileTestBuild (projectRoot : String) (moduleFilter : Option String := none) : IO UInt32 := do
  match ← loadProject projectRoot with
  | .error exitCode => return exitCode
  | .ok ctx =>
    let { validCore, parsed, allSrcMap, mainPath, depNames, policy, policyWarnings,
          policyLocMap, registry, pc, .. } := ctx
    -- [policy], location map, registry, and ProofCore all come from loadProject.
    for w in policyWarnings do IO.eprintln w
    if !(← enforceProvenRuntimeViolations parsed.modules allSrcMap) then
      return 1
    if !policy.isEmpty then
      let (vac, asm, st) ← computePolicyQuals policy parsed.modules depNames policyLocMap registry
      let policyDs := enforcePolicy policy validCore.coreModules
        (locMap := policyLocMap) (pc := pc) (depNames := depNames) (vacuousQuals := vac)
        (assumeQuals := asm) (solverTrustedQuals := st)
      if hasErrors policyDs then
        IO.eprintln (renderDiagnostics policyDs (sourceMap := allSrcMap))
        return 1
    match Pipeline.monomorphize validCore with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := allSrcMap))
      return 1
    | .ok mono =>
    match Pipeline.lower mono with
    | .error ds =>
      IO.eprintln (renderDiagnostics ds (sourceMap := allSrcMap))
      return 1
    | .ok ssa =>
      let llvmIR := Pipeline.emit ssa (testMode := true) (moduleFilter := moduleFilter)
      let llPath := mainPath ++ ".test.ll"
      let outPath := "/tmp/concrete_test_" ++ toString (← IO.monoMsNow)
      writeFile llPath llvmIR
      -- Validate LLVM IR (if llvm-as available)
      let llValid ← validateLLVMIR llPath
      if !llValid then return 1
      let args ← clangArgs llPath outPath
      let exitCode ← runCmd "clang" args
      if exitCode != 0 then
        IO.eprintln "clang compilation failed"
        IO.eprintln s!"LLVM IR left at: {llPath}"
        return exitCode
      let child ← IO.Process.spawn {
        cmd := outPath
        stdout := .piped
        stderr := .piped
      }
      let stdout ← child.stdout.readToEnd
      let stderr ← child.stderr.readToEnd
      let testExit ← child.wait
      IO.print stdout
      if !stderr.isEmpty then IO.eprint stderr
      if testExit != 0 then
        IO.eprintln s!"Test binary exited with code {testExit}"
        IO.eprintln s!"LLVM IR at: {llPath}"
        IO.eprintln s!"Binary at: {outPath}"
      else
        IO.FS.removeFile ⟨llPath⟩
        try IO.FS.removeFile ⟨outPath⟩ catch _ => pure ()
      return testExit

/-- `concrete prove --help=agent`: the agent entrypoint. Prints the
    proof-authoring sequence, stable output formats, the exit-code taxonomy, and
    the next command to run for each common status. -/
def proveAgentHelp : String := String.intercalate "\n" ([
  "concrete prove — agent guide (schema v" ++ proveSchemaVersion ++ ")",
  "",
  "PURPOSE: author and verify a Lean proof for one Concrete function.",
  "",
  "WORKFLOW (each step prints what to do next):",
  "  1. concrete prove <file> <module.fn> --json     # proof context + next_actions",
  "  2. concrete prove <file> <module.fn> --show-obligation <id>   # one obligation",
  "     concrete prove <file> <module.fn> --nearest-lemmas [<id>]  # tactic/lemma hints (all, or one obligation)",
  "  3. concrete prove <file> <module.fn> --emit-lean             # compilable Lean stub",
  "     concrete prove <file> <module.fn> --emit-artifacts        # one bundle per UNPROVED obligation",
  "  4. write the Lean proof in Concrete/Proof.lean (see PROOFKIT_GUIDE)",
  "  5. concrete prove <file> <module.fn> --emit-link             # in-source link block",
  "     (paste #[spec]/#[proof_by]/#[proof_coverage]/#[proof_fingerprint] above the fn)",
  "  6. concrete prove <file> <module.fn> --check [--json]        # kernel-verify THIS fn's theorem",
  "     concrete <file> --report check-proofs                     # kernel-verify all linked proofs",
  "  7. concrete prove <file> <module.fn> --replay                # re-run omega/bv_decide",
  "",
  "ALL-IN-ONE:",
  "  concrete prove <file> <module.fn> --workspace [dir]          # generate a self-contained",
  "    proof workspace (manifest.json, context.json, obligations/, <Fn>Proofs.lean, link.con.txt,",
  "    check.sh, replay.sh, README.md). Disposable build output; default dir .build/prove/<fn>/workspace.",
  "",
  "DISCOVERY (no file needed):",
  "  concrete prove --capabilities      # JSON: supported features + schema version",
  "  concrete prove --schema            # JSON schema for --json output",
  "  concrete prove --help=agent        # this guide",
  "",
  "OUTPUT FORMATS: text (default) or JSON (--json on prove/--show-obligation/--replay).",
  "  JSON is stable and carries the same obligation ids/statuses as",
  "  `--report contracts` and `concrete audit`. Every JSON response has next_actions.",
  "",
  ] ++ ExitCode.helpBlock ++ [
  "",
  "PROOF MODEL: in-source links only (no proof-registry.json). A function carries",
  "  #[spec]/#[proof_by]/#[ensures_proof]/#[proof_coverage]/#[proof_fingerprint]." ])

/-- `concrete prove --capabilities`: machine-readable feature discovery. -/
def proveCapabilitiesJson : String := String.intercalate "\n" [
  "{",
  "  \"schema_version\": \"" ++ proveSchemaVersion ++ "\",",
  "  \"features\": {",
  "    \"prove_json\": true,",
  "    \"show_obligation_json\": true,",
  "    \"emit_lean\": true,",
  "    \"emit_link\": true,",
  "    \"nearest_lemmas\": true,",
  "    \"replay_json\": true,",
  "    \"failed_artifacts\": true,",
  "    \"check\": true,",
  "    \"workspace\": true",
  "  },",
  "  \"obligation_kinds\": [\"invariant_init\", \"invariant_preservation\", \"loop_exit_post_link\", \"variant_nonnegative\", \"variant_decreases\", \"array_bounds\", \"division_nonzero\", \"integer_overflow\", \"ensures\"],",
  "  \"evidence_classes\": [\"proved_by_lean\", \"proved_by_kernel_decision\", \"partial\", \"stale\", \"missing\", \"blocked\", \"ineligible\", \"trusted\", \"tested_by_oracle\", \"runtime_checked\"],",
  "  \"proof_model\": \"in_source_links\",",
  "  \"link_attributes\": [\"spec\", \"proof_by\", \"ensures_proof\", \"proof_coverage\", \"proof_fingerprint\"],",
  "  \"mcp_available\": false",
  "}" ]

/-- `concrete prove --schema`: JSON schema (+ version) for `--json` output. -/
def proveSchemaJson : String := String.intercalate "\n" [
  "{",
  "  \"schema_version\": \"" ++ proveSchemaVersion ++ "\",",
  "  \"title\": \"concrete prove --json\",",
  "  \"type\": \"object\",",
  "  \"properties\": {",
  "    \"schema_version\": {\"type\": \"string\"},",
  "    \"function\": {\"type\": \"string\", \"description\": \"qualified name\"},",
  "    \"eligible\": {\"type\": \"boolean\"},",
  "    \"exclusion_reason\": {\"type\": [\"string\", \"null\"]},",
  "    \"body_fingerprint\": {\"type\": \"string\"},",
  "    \"proof_link\": {\"type\": [\"object\", \"null\"], \"description\": \"spec, proof, ensures_proof, coverage, fingerprint, origin (source_linked|hardcoded)\"},",
  "    \"status\": {\"type\": \"string\", \"enum\": [\"proved\", \"stale\", \"missing\", \"blocked\", \"ineligible\", \"trusted\"]},",
  "    \"evidence_class\": {\"type\": \"string\"},",
  "    \"obligations\": {\"type\": \"array\", \"items\": {\"type\": \"object\", \"description\": \"id, kind, status, hypotheses, conclusion, engine, theorem_shape\"}},",
  "    \"replay_command\": {\"type\": \"string\"},",
  "    \"proofkit_imports\": {\"type\": \"array\", \"items\": {\"type\": \"string\"}},",
  "    \"suggested_theorems\": {\"type\": \"array\", \"items\": {\"type\": \"string\"}},",
  "    \"next_actions\": {\"type\": \"array\", \"items\": {\"type\": \"object\", \"description\": \"kind, command, output_format, resolves\"}}",
  "  },",
  "  \"required\": [\"schema_version\", \"function\", \"status\", \"next_actions\"]",
  "}" ]

/-- Shared project-root prologue (ROADMAP Phase 4 #14): discover the enclosing
    project root, or emit the one canonical "no Concrete.toml" diagnostic and exit
    with `ExitCode.usage`. Every project-scoped command goes through here, so the
    discovery, the message, and the exit code are defined once. -/
def withProjectRoot (k : String → IO UInt32)
    (hint : String := "create one with [package] section, or run from a project directory") : IO UInt32 := do
  let cwd ← IO.currentDir
  match ← findProjectRoot cwd.toString with
  | none =>
    IO.eprintln s!"error: no Concrete.toml found in current directory or parent\nhint: {hint}"
    return ExitCode.usage
  | some root => k root

/-- `concrete <file> --report profile [--profile <name>]` — ROADMAP #10 Stage 1
    (profile mechanism only; no compilation, no codegen). Resolve the active build
    profile with precedence CLI flag > Concrete.toml `[profile]` > default, then
    print its policy bundle. An unknown profile name is rejected. -/
def reportProfile (inputPath : String) (cliProfile : Option String) : IO UInt32 := do
  match cliProfile with
  | some nm =>
    -- 1. CLI flag wins.
    match Concrete.BuildProfile.ofString? nm with
    | some p => IO.println (Concrete.renderProfileReport p .cli); return 0
    | none =>
      IO.eprintln s!"error: unknown profile '{nm}' (known: {Concrete.BuildProfile.known})"
      return ExitCode.usage
  | none =>
    -- 2. Concrete.toml [profile] name, if the file is inside a project.
    let manifestName ← (do
      match ← findProjectRoot (dirOf inputPath) with
      | some root =>
        let tomlPath := root ++ "/Concrete.toml"
        if ← System.FilePath.pathExists tomlPath then
          return Concrete.parseProfileName (← IO.FS.readFile tomlPath)
        else return none
      | none => return none)
    match manifestName with
    | some nm =>
      match Concrete.BuildProfile.ofString? nm with
      | some p => IO.println (Concrete.renderProfileReport p .manifest); return 0
      | none =>
        IO.eprintln s!"error: Concrete.toml [profile] name '{nm}' is unknown (known: {Concrete.BuildProfile.known})"
        return ExitCode.usage
    | none =>
      -- 3. Default profile.
      IO.println (Concrete.renderProfileReport Concrete.defaultProfile .default)
      return 0

def main (args : List String) : IO UInt32 := do
  -- Phase 6E #1: help is the most reliable command — it must work from ANY
  -- directory, before any file/project parsing, and never throw. `concrete
  -- --help`, `concrete help`, and `concrete <cmd> --help` all reach here first.
  if args.head? == some "--help" || args.head? == some "help" || args.head? == some "-h"
     || args.contains "--help" then
    IO.println helpText
    return 0
  -- Phase 6E #3: daily command aliases. Normalized to the legacy flag spelling
  -- UP FRONT, so an alias is byte-identical to the flag form by construction
  -- (`concrete report caps f.con` == `concrete f.con --report caps`;
  -- `concrete trace f.con [--json]` == `concrete f.con --trace-pipeline`).
  -- Legacy spellings keep working untouched (6E #4 compatibility).
  let args := match args with
    | "report" :: kind :: file :: rest => file :: "--report" :: kind :: rest
    | "trace" :: file :: rest => file :: "--trace-pipeline" :: rest.filter (· != "--json")
    | a => a
  -- `concrete --report compiler-ledger [--json]` — the project-scoped non-proof
  -- fact store (Phase 4 #2). Project mode: loads the one ProjectContext and renders
  -- its CompilerLedger (toolchain id filled here, lazily).
  if args.head? == some "--report" && args[1]? == some "compiler-ledger" then
    let json := Cli.hasFlag args "--json"
    return ← withProjectRoot (hint := "`--report compiler-ledger` reads a project; run from a project directory") fun root => do
      match ← loadProject root with
      | .error exitCode => return exitCode
      | .ok ctx =>
        let toolId ← compilerIdentity
        let l := { ctx.ledger with toolchainId := toolId }
        IO.println (if json then l.toJson 1 else l.render)
        return 0
  -- Check for "build" command first (before generic single-arg pattern)
  if args.head? == some "build" then
    return ← withProjectRoot fun root => do
      let emitLLVM := Cli.hasFlag args "--emit-llvm"
      let outPath := Cli.flagValue args "-o"
      compileBuild root outPath emitLLVM
  -- concrete run [-- args...]
  if args.head? == some "run" then
    return ← withProjectRoot fun root => do
      -- Build to a temporary path
      let tmpBin := "/tmp/concrete_run_" ++ toString (← IO.monoMsNow)
      let buildResult ← compileBuild root (some tmpBin) (emitLLVM := false) (quiet := true)
      if buildResult != 0 then return buildResult
      -- Extract user args after "--"
      let userArgs := match args.dropWhile (· != "--") with
        | _ :: rest => rest
        | [] => []
      -- Run the built binary
      let child ← IO.Process.spawn {
        cmd := tmpBin
        args := userArgs.toArray
        stdin := .inherit
        stdout := .inherit
        stderr := .inherit
      }
      let exitCode ← child.wait
      -- Clean up temp binary
      try IO.FS.removeFile ⟨tmpBin⟩ catch _ => pure ()
      return exitCode
  -- concrete test [--module <name>]
  if args.head? == some "test" then
    return ← withProjectRoot fun root => do
      let modFilter := Cli.flagValue args "--module"
      compileTestBuild root modFilter
  -- concrete check — run frontend + proof status without codegen
  if args.head? == some "check" then
    return ← withProjectRoot fun root => do
      match ← loadProject root (stripTestFns := true) with
      | .error exitCode => return exitCode
      | .ok ctx =>
        let { validCore, parsed, allSrcMap, depNames, policy, policyWarnings,
              policyLocMap, registry, pc, ledger, .. } := ctx
        -- [policy], location map, registry, ProofCore, and diagnostics all come from
        -- loadProject. Registry diagnostics are rendered FROM the ledger (Phase 4 #4).
        for w in policyWarnings do IO.eprintln w
        if !(← enforceProvenRuntimeViolations parsed.modules allSrcMap) then
          return 1
        for d in ledger.diagnostics do
          if d.code == "registry" then IO.eprintln d.message
        if !policy.isEmpty then
          let (vac, asm, st) ← computePolicyQuals policy parsed.modules depNames policyLocMap registry
          let policyDs := enforcePolicy policy validCore.coreModules
            (locMap := policyLocMap) (pc := pc) (depNames := depNames) (vacuousQuals := vac)
            (assumeQuals := asm) (solverTrustedQuals := st)
          if hasErrors policyDs then
            IO.eprintln (renderDiagnostics policyDs (sourceMap := allSrcMap))
            return 1
        -- Scope to user package for reporting and exit code
        let userModules := validCore.coreModules.filter fun m => !depNames.contains m.name
        let userPc := pc.scopeToUser depNames
        -- Print proof status report (user package only)
        let srcMap := ctx.allSrcMap
        IO.println (Report.proofStatusReport userModules policyLocMap srcMap (registry := registry) (pc := userPc))
        -- Print next steps if any
        let nextSteps := Report.proofNextSteps userPc
        if !nextSteps.isEmpty then IO.println nextSteps
        -- Show dependency context
        let depOblCount := pc.obligations.length - userPc.obligations.length
        if depOblCount > 0 then
          IO.println s!"\n({depOblCount} dependency obligations hidden — use --report proof-status for full view)"
        -- Exit code: 0 if all user-package eligible proved, 1 if any stale/missing/blocked
        let hasIssues := userPc.obligations.any fun o =>
          o.status == .stale || o.status == .missing || o.status == .blocked
        let hasRegistryErrors := ledger.diagnostics.any (fun d => d.code == "registry" && d.severity == "error")
        return (if hasIssues || hasRegistryErrors then 1 else 0)
  -- concrete diff <old.json> <new.json> [--json]
  if args.head? == some "diff" then
    let rest := args.drop 1
    match rest with
    | [oldPath, newPath] =>
      let oldJson ← try pure (some (← readFile oldPath)) catch _ => pure none
      let newJson ← try pure (some (← readFile newPath)) catch _ => pure none
      match oldJson, newJson with
      | none, _ =>
        IO.eprintln s!"error: file not found: {oldPath}"
        return 1
      | _, none =>
        IO.eprintln s!"error: file not found: {newPath}"
        return 1
      | some oldJ, some newJ =>
      let (oldParsed, oldWarns) := Report.parseFactsWarn oldJ
      let (newParsed, newWarns) := Report.parseFactsWarn newJ
      for w in oldWarns do IO.eprintln s!"{oldPath}: {w}"
      for w in newWarns do IO.eprintln s!"{newPath}: {w}"
      match oldParsed, newParsed with
      | some oldFacts, some newFacts =>
        match Report.diffFacts oldFacts newFacts with
        | .error e =>
          IO.eprintln s!"error: {e}"
          return 2
        | .ok entries =>
          IO.println (Report.renderDiffReport entries)
          return (if entries.any (·.drift == "weakened") then 1 else 0)
      | none, _ =>
        IO.eprintln s!"error: could not parse JSON from {oldPath}"
        return 1
      | _, none =>
        IO.eprintln s!"error: could not parse JSON from {newPath}"
        return 1
    | [oldPath, newPath, "--json"] =>
      let oldJson2 ← try pure (some (← readFile oldPath)) catch _ => pure none
      let newJson2 ← try pure (some (← readFile newPath)) catch _ => pure none
      match oldJson2, newJson2 with
      | none, _ =>
        IO.eprintln s!"error: file not found: {oldPath}"
        return 1
      | _, none =>
        IO.eprintln s!"error: file not found: {newPath}"
        return 1
      | some oldJ2, some newJ2 =>
      let (oldParsed2, oldWarns2) := Report.parseFactsWarn oldJ2
      let (newParsed2, newWarns2) := Report.parseFactsWarn newJ2
      for w in oldWarns2 do IO.eprintln s!"{oldPath}: {w}"
      for w in newWarns2 do IO.eprintln s!"{newPath}: {w}"
      match oldParsed2, newParsed2 with
      | some oldFacts, some newFacts =>
        match Report.diffFacts oldFacts newFacts with
        | .error e =>
          IO.eprintln s!"error: {e}"
          return 2
        | .ok entries =>
          IO.println (Report.renderDiffJson entries)
          return (if entries.any (·.drift == "weakened") then 1 else 0)
      | none, _ =>
        IO.eprintln s!"error: could not parse JSON from {oldPath}"
        return 1
      | _, none =>
        IO.eprintln s!"error: could not parse JSON from {newPath}"
        return 1
    | _ =>
      IO.eprintln "Usage: concrete diff <old.json> <new.json> [--json]"
      return 1
  -- concrete snapshot <file.con> [-o output.json]
  if args.head? == some "snapshot" then
    let rest := args.drop 1
    let inputPath := match rest with
      | p :: _ => some p
      | [] => none
    match inputPath with
    | none =>
      IO.eprintln "Usage: concrete snapshot <file.con> [-o output.json]"
      return 1
    | some inp =>
      let outputPath := match rest with
        | _ :: "-o" :: p :: _ => p
        | _ =>
          if inp.endsWith ".con" then
            String.ofList (inp.toList.take (inp.length - 4)) ++ ".facts.json"
          else inp ++ ".facts.json"
      let source ← readFile inp
      let mainSrcMap : SourceMap := [(inp, source)]
      match ← Pipeline.runFrontend inp source resolveAllModules with
      | .error ds =>
        IO.eprintln (renderDiagnostics ds (sourceMap := mainSrcMap))
        return 1
      | .ok (parsed, _, validCore, _srcMap) =>
        let locMap := Report.buildFnLocMap parsed.modules inp
        let simpleLocMap := locMap.map fun e => (e.qualName, (e.file, e.fnSpan.line))
        let registry ← loadRegistryWithLinks inp parsed.modules validCore.coreModules
        let pc := extractProofCore validCore simpleLocMap registry
        -- Collect core facts (same as diagnostics-json) plus source-contract facts
        -- (AST metadata, absent from Core) so `concrete diff` can detect contract
        -- API drift (precondition strengthening, postcondition weakening).
        let coreFacts := Report.collectCoreFacts validCore.coreModules locMap registry pc
          ++ Report.collectContractFacts parsed.modules
        -- Run backend pipeline for traceability facts
        let (traceFacts, traceWarns) ← match Pipeline.monomorphize validCore with
          | .error ds =>
            let msg := ds.map (·.message) |> ", ".intercalate
            pure ([], [s!"warning: snapshot incomplete — monomorphization failed: {msg}"])
          | .ok mono =>
            match Pipeline.lower mono with
            | .error ds =>
              let msg := ds.map (·.message) |> ", ".intercalate
              pure ([], [s!"warning: snapshot incomplete — lowering failed: {msg}"])
            | .ok ssa =>
              pure (Report.collectTraceabilityFacts
                validCore.coreModules mono.coreModules ssa.ssaModules locMap (registry := registry) (pc := pc), [])
        for w in traceWarns do IO.eprintln w
        -- Generate timestamp
        let ms ← IO.monoMsNow
        let timestamp := toString ms
        let json := Report.snapshotJson inp timestamp coreFacts traceFacts
        writeFile outputPath json
        let factCount := coreFacts.length + traceFacts.length
        IO.println s!"Snapshot written: {outputPath} ({factCount} facts)"
        return 0
  -- concrete debug-bundle <file.con> [-o dir]
  if args.head? == some "debug-bundle" then
    let rest := args.drop 1
    let inputPath := match rest with
      | p :: _ => some p
      | [] => none
    match inputPath with
    | none =>
      IO.eprintln "Usage: concrete debug-bundle <file.con> [-o dir]"
      return 1
    | some inp =>
      let bundleDir := match rest with
        | _ :: "-o" :: p :: _ => p
        | _ =>
          if inp.endsWith ".con" then
            String.ofList (inp.toList.take (inp.length - 4)) ++ ".debug-bundle"
          else inp ++ ".debug-bundle"
      let source ← readFile inp
      let compilerVersion ← compilerIdentity
      let st ← DebugBundle.capturePipeline inp source resolveAllModules
      DebugBundle.writeBundle bundleDir st compilerVersion
      let status := match st.failStage with
        | some stage => s!"failed at {stage}"
        | none => "complete (no failure)"
      IO.println s!"Debug bundle written: {bundleDir}/ — {status}"
      return (if st.failStage.isSome then 1 else 0)
  -- concrete validate-bundle <dir>
  if args.head? == some "validate-bundle" then
    let rest := args.drop 1
    match rest with
    | [bundleDir] =>
      let issues ← DebugBundle.validateBundle bundleDir
      if issues.isEmpty then
        IO.println s!"Bundle {bundleDir} is valid."
        return 0
      else
        for issue in issues do IO.eprintln issue
        let errors := issues.filter (·.startsWith "error")
        if errors.isEmpty then
          IO.println s!"Bundle {bundleDir} has {issues.length} warning(s)."
          return 0
        else
          IO.eprintln s!"Bundle {bundleDir} has {errors.length} error(s)."
          return 1
    | _ =>
      IO.eprintln "Usage: concrete validate-bundle <dir>"
      return 1
  -- concrete reduce <file.con> --predicate <pred> [-o output] [--verbose]
  if args.head? == some "reduce" then
    let rest := args.drop 1
    let inputPath := match rest with
      | p :: _ => some p
      | [] => none
    match inputPath with
    | none =>
      IO.eprintln "Usage: concrete reduce <file.con> --predicate <pred> [-o output] [--verbose]"
      IO.eprintln "Predicates: parse-error, resolve-error, check-error, elab-error, core-check-error,"
      IO.eprintln "            mono-error, lower-error, consistency-violation, verify-warning, crash"
      IO.eprintln "Substring match: check-error:expected Int"
      IO.eprintln "External:        external:scripts/reduce/expect-error-code.sh E0708"
      IO.eprintln "                 (the candidate file is appended as the final argument)"
      return 1
    | some inp =>
      let predStr := match rest with
        | _ :: "--predicate" :: p :: _ => some p
        | _ => none
      match predStr with
      | none =>
        IO.eprintln "error: --predicate is required"
        return 1
      | some ps =>
        match Reduce.parsePredicate ps with
        | none =>
          IO.eprintln s!"error: unknown predicate '{ps}'"
          return 1
        | some pred =>
          let outputPath := match rest with
            | _ :: _ =>
              let rec findO : List String → Option String
                | "-o" :: p :: _ => some p
                | _ :: rest => findO rest
                | [] => none
              findO rest
            | [] => none
          let outputPath := outputPath.getD (inp ++ ".reduced")
          let verbose := rest.any (· == "--verbose")
          let source ← readFile inp
          if verbose then IO.eprintln s!"Reducing {inp} with predicate '{ps}'..."
          let result ← Reduce.reduce source pred resolveAllModules verbose
          writeFile outputPath result
          let origLines := (source.splitOn "\n").length
          let redLines := (result.splitOn "\n").length
          IO.println s!"Reduced: {origLines} → {redLines} lines — {outputPath}"
          return 0
  -- concrete fmt — format source files (Phase 6 #1). CLI promotion of the legacy
  -- `--fmt` flag to a real subcommand. Default: format to stdout. `--check`: exit
  -- nonzero if formatting would change the file. `--write`: rewrite in place.
  -- `--stdin`: read stdin, write stdout. A file is "formatted" iff
  -- formatProgram(parse(it)) == it (formatProgram emits exactly one trailing \n).
  if args.head? == some "fmt" then
    let rest := args.drop 1
    let check := Cli.hasFlag rest "--check"
    let write := Cli.hasFlag rest "--write"
    let stdin := Cli.hasFlag rest "--stdin"
    if stdin then
      let source ← (← IO.getStdin).readToEnd
      match parse source with
      | .error e => IO.eprintln s!"parse error: {renderDiagnostics e}"; return 1
      | .ok modules => IO.print (formatProgram modules); return 0
    -- positional path = first non-flag argument
    match rest.filter (fun a => !a.startsWith "-") |>.head? with
    | none =>
      IO.eprintln "Usage: concrete fmt <file.con> [--check | --write | --stdin]"
      return 1
    | some path =>
      let source ← readFile path
      match parse source with
      | .error e => IO.eprintln s!"parse error in {path}: {renderDiagnostics e}"; return 1
      | .ok modules =>
        let formatted := formatProgram modules
        if check then
          if formatted == source then return 0
          else
            IO.eprintln s!"{path}: not formatted (run `concrete fmt --write {path}`)"
            return 1
        else if write then
          if formatted == source then return 0
          else
            writeFile path formatted
            IO.println s!"formatted {path}"
            return 0
        else
          IO.print formatted
          return 0
  -- concrete audit <file.con> — alias for `concrete <file> --report audit`
  if args.head? == some "audit" then
    match args.drop 1 with
    | [inputPath] => return (← compileAndReport inputPath "audit")
    | _ =>
      IO.eprintln "Usage: concrete audit <file.con>"
      return 1
  -- concrete prove <file.con> <module.function> [--out <path>] [--force]
  --   Read-only proof-scaffold generator. Prints to stdout; --out writes a
  --   stub file (refusing to overwrite without --force). Never auto-proves.
  if args.head? == some "prove" then
    let pargs := args.drop 1
    -- Discovery commands (no file/function needed) — the agent entrypoint.
    if Cli.hasFlag pargs "--help=agent" then IO.println proveAgentHelp; return 0
    if Cli.hasFlag pargs "--capabilities" then IO.println proveCapabilitiesJson; return 0
    if Cli.hasFlag pargs "--schema" then IO.println proveSchemaJson; return 0
    match pargs with
    | inputPath :: target :: rest =>
      let force := Cli.hasFlag rest "--force"
      let emitLink := Cli.hasFlag rest "--emit-link"
      let replay := Cli.hasFlag rest "--replay"
      let proveJson := Cli.hasFlag rest "--json"
      let nearestLemmas := Cli.hasFlag rest "--nearest-lemmas"
      let nearestId := Cli.flagValue rest "--nearest-lemmas"
      let emitLean := Cli.hasFlag rest "--emit-lean"
      let emitArtifacts := Cli.hasFlag rest "--emit-artifacts"
      let check := Cli.hasFlag rest "--check"
      -- `--workspace` with no value means "default workspace" (empty string sentinel).
      let workspace := if Cli.hasFlag rest "--workspace"
        then some (Cli.flagValue rest "--workspace" |>.getD "") else none
      let stdout := Cli.hasFlag rest "--stdout"
      let outDir := Cli.flagValue rest "--out-dir"
      let outPath := Cli.flagValue rest "--out"
      let showObl := Cli.flagValue rest "--show-obligation"
      return (← compileAndReport inputPath "prove"
        (proveTarget := some target) (proveOut := outPath) (proveForce := force)
        (proveEmitLink := emitLink) (proveShowObl := showObl) (proveReplay := replay)
        (proveJson := proveJson) (proveNearestLemmas := nearestLemmas)
        (proveEmitLean := emitLean) (proveStdout := stdout)
        (proveEmitArtifacts := emitArtifacts) (proveOutDir := outDir)
        (proveCheck := check) (proveWorkspace := workspace)
        (proveNearestId := nearestId))
    | _ =>
      IO.eprintln "Usage: concrete prove <file.con> <module.function> [--json] [--out <path>] [--force] [--emit-link] [--emit-lean] [--emit-artifacts] [--out-dir <dir>] [--show-obligation <id>] [--replay] [--nearest-lemmas] [--check] [--workspace <dir>]\n       concrete prove --help=agent | --capabilities | --schema   (discovery; no file needed)"
      return 1
  -- concrete --version
  if args == ["--version"] then
    let id ← compilerIdentity
    IO.println id
    return 0
  -- `concrete <file> --diagnostics-json` — frontend diagnostics as JSON, rendered
  -- from the SAME structured Diagnostic records the human output uses (Phase 4 #4).
  if args.length == 2 && args[1]? == some "--diagnostics-json" then
    let inputPath := args.headD ""
    let source ← readFile inputPath
    -- Error-tolerant path (Phase 4 #12a): a failing pass does not erase diagnostics
    -- from passes that can still run. Returns only diagnostics + a `partial` flag —
    -- structurally never a codegen/proof artifact.
    let (ds, isPartial) ← Pipeline.runFrontendDiagnostics inputPath source resolveAllModules
    IO.println (Concrete.diagnosticsToJson ds 1 isPartial)
    return (if Concrete.hasErrors ds then 1 else 0)
  -- Unknown command / missing input file (Phase 4 #15): the single-file dispatch
  -- below treats the first argument as a source path. If it is neither a recognized
  -- subcommand (all handled above) nor a readable file, fail cleanly here instead of
  -- letting the later `readFile` throw an uncaught exception.
  if let some first := args.head? then
    if !first.startsWith "-" && !(← System.FilePath.pathExists first) then
      IO.eprintln s!"error: '{first}' is not a readable file or a known command\nhint: run `concrete` with no arguments to see usage"
      return ExitCode.usage
  match args with
  | [] =>
    IO.eprintln usage
    return 1
  | [inputPath] =>
    let outputPath := if inputPath.endsWith ".con" then String.ofList (inputPath.toList.take (inputPath.length - 4)) else inputPath ++ ".out"
    compileSSA inputPath outputPath false
  | [inputPath, "--test"] =>
    compileTest inputPath
  | [inputPath, "--test", "--module", moduleName] =>
    compileTest inputPath (moduleFilter := some moduleName)
  | [inputPath, "--emit-llvm"] =>
    compileSSA inputPath "" true
  | [inputPath, "--interp"] =>
    interpProgram inputPath
  | [inputPath, "--emit-core"] =>
    compileAndEmit inputPath "core"
  | [inputPath, "--emit-ssa"] =>
    compileAndEmit inputPath "ssa"
  | [inputPath, "--emit-ssa-unverified"] =>
    compileAndEmit inputPath "ssa-unverified"
  | [inputPath, "--emit-trace-json"] =>
    traceTelemetry inputPath
  | [inputPath, "--trace-pipeline"] =>
    tracePipeline inputPath
  | [inputPath, "-o", outputPath] =>
    compileSSA inputPath outputPath false
  | [inputPath, "--check", checkType] =>
    compileAndCheck inputPath checkType
  -- ROADMAP #10 Stage 1: build-profile report (must precede the generic
  -- `--report <type>` arm; "profile" is not a compileAndReport report type).
  | [inputPath, "--report", "profile"] =>
    reportProfile inputPath none
  | [inputPath, "--report", "profile", "--profile", name] =>
    reportProfile inputPath (some name)
  | [inputPath, "--report", reportType] =>
    compileAndReport inputPath reportType
  | [inputPath, "--report", reportType, "--json"] =>
    compileAndReport inputPath reportType (reportJson := true)
  | [inputPath, "--report", reportType, "--emit-smt"] =>
    compileAndReport inputPath reportType (smtEmit := true)
  | [inputPath, "--report", reportType, "--emit-lean-replay"] =>
    compileAndReport inputPath reportType (emitLeanReplay := true)
  | [inputPath, "--report", reportType, "--smt"] =>
    compileAndReport inputPath reportType (smtRun := true)
  | [inputPath, "--report", reportType, "--smt", "--json"] =>
    compileAndReport inputPath reportType (reportJson := true) (smtRun := true)
  | [inputPath, "--report", reportType, "--smt", "--replay"] =>
    compileAndReport inputPath reportType (smtRun := true) (smtReplay := true)
  | [inputPath, "--report", reportType, "--smt", "--replay", "--json"] =>
    compileAndReport inputPath reportType (reportJson := true) (smtRun := true) (smtReplay := true)
  | [inputPath, "--report", reportType, "--smt", "--smt-timeout-ms", ms, "--json"] =>
    compileAndReport inputPath reportType (reportJson := true) (smtRun := true)
      (smtTimeoutMs := ms.toNat?)
  | [inputPath, "--report", reportType, "--smt", "--smt-timeout-ms", ms] =>
    compileAndReport inputPath reportType (smtRun := true) (smtTimeoutMs := ms.toNat?)
  | [inputPath, "--query", query] =>
    compileAndQuery inputPath query
  -- LEGACY: `--fmt` flag, superseded by the `concrete fmt` subcommand (Phase 6
  -- #1). Kept byte-identical for the golden-format baselines; documented as
  -- deprecated. New usage should prefer `concrete fmt`.
  | [inputPath, "--fmt"] =>
    let source ← readFile inputPath
    match parse source with
    | .error e =>
      IO.eprintln s!"parse error: {renderDiagnostics e}"
      return 1
    | .ok modules =>
      IO.print (formatProgram modules)
      return 0
  | _ =>
    IO.eprintln usage
    return 1