fix(bench): pass --allow-declined in ooc whole-env check-lean benchmark

Ix/Cli/BenchCmd.lean

@@ -744,9 +744,13 @@ is not a benchmark run"
     let ix ← resolveBin repo "ix"
     -- Whole-env row (keyed by the env name), plus the per-constant
     -- attribution CSV the compare drill-down reads (top movers).
+    -- Upstream libraries contain declarations outside IxC's fragment
+    -- (e.g. Lean.trustCompiler, unsafe inductives) that decline in the
+    -- record check; --allow-declined benchmarks the whole-env record check
+    -- while still failing (exit 3 / status: rejected) on any kernel reject.
     let exit ← runGuarded watchdog ceilingGb ix
-      #["check-lean", ixe, "--anon", "--json", out, "--json-name", info.name,
-        "--per-const", s!"{out}.perconst.csv"]
+      #["check-lean", ixe, "--anon", "--allow-declined", "--json", out,
+        "--json-name", info.name, "--per-const", s!"{out}.perconst.csv"]
     if exit != 0 && exit != exitRejected then
       IO.eprintln s!"[bench] whole-env check failed (exit {exit})"
     -- … plus one full-closure row per constant. ONE process for all names

Ix/Cli/CheckLeanCmd.lean

@@ -63,6 +63,7 @@ structure CheckCfg where
   workers : Nat := 1
   verbose : Bool := false
   silent : Bool := false
+  allowDeclined : Bool := false
   progressMs : Nat := 2000
   slowMs : Nat := 7000
   stackBytes : Nat := 256 * 1024 * 1024
@@ -254,6 +255,11 @@ def CheckReport.passed (r : CheckReport) : Nat := (r.targets.filter (success ∘
 def CheckReport.typed (r : CheckReport) : Nat := (r.targets.filter (·.outcome == "typed")).size
 def CheckReport.failures (r : CheckReport) : Array (String × String) :=
   (r.targets.filter (!success ·.outcome)).map fun t => (t.target.label, s!"{t.outcome}: {t.reason}")
+/-- Whether any checked target or record in the closure was rejected by the
+kernel or reader (`outcome == "reject"`), as opposed to declined as outside
+`IxC`'s fragment (`"decline"`) or blocked solely by a declined dependency. -/
+def CheckReport.hasReject (r : CheckReport) : Bool :=
+  r.targets.any (·.outcome == "reject") || r.rows.any (·.outcome == "reject")
 
 /-- The user axioms a run's verdict is conditional on: the conditional
 whole-artifact entry's, otherwise those its declaration checks read and accepted. -/
@@ -286,12 +292,16 @@ def exitConditional : UInt32 := 5
 
 /-- What a completed run did not check, if anything: a selected or capped run covers
 only its selection; a run that asked for the whole artifact (`wholeRequested`) of an
-artifact with no role binding covers only the per-declaration checks. -/
-def coverageNotice (report : CheckReport) (wholeRequested : Bool) : Option String :=
+artifact with no role binding covers only the per-declaration checks; `--allow-declined`
+checks records only and makes no whole-artifact admission claim. -/
+def coverageNotice (report : CheckReport) (wholeRequested : Bool)
+    (allowDeclined : Bool := false) : Option String :=
   match report.artifactAdmission with
   | some _ => none
   | none =>
-    if report.bound then
+    if allowDeclined then
+      some "[check-lean] record check (--allow-declined); no whole-artifact receipt"
+    else if report.bound then
       if wholeRequested then
         some "[check-lean] whole-artifact admission did not run because declaration checks failed"
       else some "[check-lean] selected checking only; no whole-artifact receipt"
@@ -304,22 +314,27 @@ whole-artifact admission did not run; only the per-declaration checks ran \
 whole-artifact admission could run"
 
 /-- The exit status of a completed run: a refusal (`exitRejected`) when a
-checked declaration failed; otherwise a usage error when a host statement was
+checked declaration failed (or, under `allowDeclined`, when any target or
+record was `"reject"`ed); otherwise a usage error when a host statement was
 asked for (`hostRequested`) and the run issued none; otherwise `exitPartial`
-when the whole artifact was asked for and its admission did not run; otherwise
-`exitConditional` when the verdict is conditional on user axioms; else 0. -/
-def runExit (report : CheckReport) (wholeRequested : Bool) (hostRequested : Bool := false) : UInt32 :=
-  if !report.failures.isEmpty then Ix.Benchmark.Results.exitRejected
+when the whole artifact was asked for (without `allowDeclined`) and its
+admission did not run; otherwise `exitConditional` when the verdict is
+conditional on user axioms; else 0. -/
+def runExit (report : CheckReport) (wholeRequested : Bool) (hostRequested : Bool := false)
+    (allowDeclined : Bool := false) : UInt32 :=
+  let failed := if allowDeclined then report.hasReject else !report.failures.isEmpty
+  if failed then Ix.Benchmark.Results.exitRejected
   else if hostRequested && report.hostStatement.isNone then Ix.Benchmark.Results.exitUsage
-  else if wholeRequested && report.artifactAdmission.isNone then exitPartial
+  else if !allowDeclined && wholeRequested && report.artifactAdmission.isNone then exitPartial
   else if !report.conditionalOn.isEmpty then exitConditional
   else 0
 
 /-- The results-row status of a completed run (`Ix.Benchmark.Results`): its
 exit status (`runExit`, no host statement asked for) by name. `rejected` (3),
 `partial` (`exitPartial`), `conditional` (`exitConditional`), else `ok`. -/
-def runStatus (report : CheckReport) (wholeRequested : Bool) : String :=
-  let code := runExit report wholeRequested
+def runStatus (report : CheckReport) (wholeRequested : Bool)
+    (allowDeclined : Bool := false) : String :=
+  let code := runExit report wholeRequested (allowDeclined := allowDeclined)
   if code == Ix.Benchmark.Results.exitRejected then "rejected"
   else if code == exitPartial then "partial"
   else if code == exitConditional then "conditional"
@@ -459,7 +474,7 @@ def runPrepared (p : PreparedInput) (cfg : CheckCfg) (selection : Selection)
       | .ok report =>
         let report := { report with
           bound := p.bound, roles := if whole then some (roleCounts p report.rows) else none }
-        if !whole || !report.failures.isEmpty then return .ok report
+        if !whole || cfg.allowDeclined || !report.failures.isEmpty then return .ok report
         let started ← IO.monoMsNow
         let admitted ← IO.lazyPure fun _ => checkWhole p selection maxGroups
         let elapsed := (← IO.monoMsNow) - started
@@ -497,7 +512,9 @@ def checkConfig (p : Cli.Parsed) : IO (Except DriverError CheckCfg) := do
   if workers == 0 then return .error (.usage "--workers must be greater than zero")
   let progress ← envNat ["IX_KERNEL_CHECK_PROGRESS_MS", "IX_PROGRESS_MS"] 2000
   let slow ← envNat ["IX_KERNEL_CHECK_SLOW_MS"] 7000
-  return do pure { workers, verbose := p.hasFlag "verbose", progressMs := ← progress, slowMs := ← slow }
+  return do pure {
+    workers, verbose := p.hasFlag "verbose", allowDeclined := p.hasFlag "allow-declined"
+    progressMs := ← progress, slowMs := ← slow }
 
 private def csvField (s : String) : String :=
   if s.any (fun c => c == ',' || c == '"')
@@ -545,12 +562,12 @@ is the number of records the run checked or read, whole-artifact or per name;
 `throughput` is that count per second of `check-time`. `status` is the run's
 exit status by name (`runStatus`): `rejected`, `partial`, `conditional` or `ok`. -/
 private def writeJsonReportRow (jsonPath key : String) (report : CheckReport)
-    (wholeRequested : Bool) : IO Unit := do
+    (wholeRequested : Bool) (allowDeclined : Bool := false) : IO Unit := do
   let secs := report.elapsedMs.toFloat / 1000.0
   let tput := if report.elapsedMs > 0
     then report.records.toFloat * 1000.0 / report.elapsedMs.toFloat else 0.0
   let peakRss := (← statusKb "VmHWM:") * 1024
-  let status := runStatus report wholeRequested
+  let status := runStatus report wholeRequested allowDeclined
   Ix.Benchmark.Results.writeRow jsonPath key status
     [ ("constants", Lean.toJson report.records)
     , ("check-time", Ix.Benchmark.Results.jsonRound 3 secs)
@@ -590,7 +607,7 @@ def parseOptions (p : Cli.Parsed) (path : String) : IO (Except DriverError Optio
     only := (← ConstsFile.gather p), cap := (p.flag? "max").map (·.as! Nat)
     json? := string "json", jsonName? := string "json-name", perConst? := string "per-const"
     failOut? := string "fail-out", hostOut? := string "host-out", hostStore := p.hasFlag "host-store" }
-  if o.hostRequested && (o.hasConsts || o.cap.isSome) then
+  if o.hostRequested && (o.hasConsts || o.cap.isSome || o.cfg.allowDeclined) then
     return .error (.usage "[check-lean] host statement output requires a complete bound artifact check")
   if o.perName?.isSome && o.failOut?.isSome then
     return .error (.usage "[check-lean] --json per-name rows and --fail-out cannot be combined")
@@ -659,7 +676,7 @@ def runPerName (o : Options) (p : PreparedInput) (json : String) :
         refused := refused.push name
       | .error e => return .error e
       | .ok report =>
-        writeJsonReportRow json (key name) report false
+        writeJsonReportRow json (key name) report false o.cfg.allowDeclined
         userAxioms := report.userAxioms.foldl (·.insert ·) userAxioms
         merged := { merged with
           targets := merged.targets ++ report.targets, rows := merged.rows ++ report.rows
@@ -693,7 +710,7 @@ uncertified, no host statement ({report.artifactMs}ms)"
   | none =>
     if report.failures.isEmpty && !report.userAxioms.isEmpty then
       for line in conditionalLines p "selected checking" report.userAxioms do IO.println line
-    if let some notice := coverageNotice report o.wholeRequested then IO.println notice
+    if let some notice := coverageNotice report o.wholeRequested o.cfg.allowDeclined then IO.println notice
   if let some statement := report.hostStatement then
     let hostBytes ← IO.ofExcept statement.bytes
     let address := Address.admissionHash hostBytes
@@ -714,7 +731,7 @@ admission: this run is CONDITIONAL on {axioms.size} user axioms and issues no ho
   IO.println s!"[check-lean] authenticated input {report.inputMs}ms; run preparation {report.prepareMs}ms; selected checker {report.subjectMicros / 1000}ms; support checker {report.supportMicros / 1000}ms; reading {report.readMicros / 1000}ms; run {report.elapsedMs}ms"
   IO.println s!"##check-lean## {report.elapsedMs} {report.passed} {report.failures.size} {report.targetsCovered}"
   if let some json := o.json? then
-    writeJsonReportRow json (o.jsonName?.getD "env") report o.wholeRequested
+    writeJsonReportRow json (o.jsonName?.getD "env") report o.wholeRequested o.cfg.allowDeclined
 
 def runCheckLeanCmd (p : Cli.Parsed) : IO UInt32 := do
   let some path := p.positionalArg? "path" | p.printError "error: must specify <path>"; return 2
@@ -727,7 +744,8 @@ def runCheckLeanCmd (p : Cli.Parsed) : IO UInt32 := do
       pure h
     let bytes ← IO.FS.readBinFile o.path
     IO.println s!"Running IxC record check ({if o.anon then "anon" else "meta"} mode\
-{if o.allowUserAxioms then "; user axioms allowed" else ""})"
+{if o.allowUserAxioms then "; user axioms allowed" else ""}\
+{if o.cfg.allowDeclined then "; declined allowed" else ""})"
     let prepared ← match ← prepareInput bytes o.anon o.allowUserAxioms with
       | .ok prep => pure prep
       | .error e => return (← refuse out e)
@@ -745,12 +763,12 @@ def runCheckLeanCmd (p : Cli.Parsed) : IO UInt32 := do
       IO.println s!"##check-lean## {(← IO.monoMsNow) - startAll} {report.passed} {failed + unresolved.size} {o.only.size}"
       return if !unresolved.isEmpty then Ix.Benchmark.Results.exitUsage
         else if !refused.isEmpty then Ix.Benchmark.Results.exitRejected
-        else runExit report false
+        else runExit report false (allowDeclined := o.cfg.allowDeclined)
     match ← runPrepared prepared o.cfg o.selection o.cap out with
     | .error e => return (← refuse out e)
     | .ok report =>
       emitReport o prepared report out
-      return runExit report o.wholeRequested o.hostRequested
+      return runExit report o.wholeRequested o.hostRequested o.cfg.allowDeclined
   catch e => IO.eprintln s!"[check-lean] {e}"; return 1
 
 end Ix.Cli.CheckLeanCmd
@@ -763,6 +781,7 @@ def checkLeanCmd : Cli.Cmd := `[Cli|
     anon; "Anonymous keys and #hex display labels"
     workers : Nat; "Requested workers (>0); the tier-capable path reports effective 1"
     "allow-user-axioms"; "Admit safe axioms beyond the standard three; the role binding must bind sorryAx, propext and Classical.choice. A whole run whose declarations hold any runs the uncertified conditional entry, lists the axioms, issues no host statement and exits 5; so does a selected run that reads one"
+    "allow-declined"; "Record-check mode: tolerate declarations outside IxC's fragment (decline) and their dependents (blocked), failing with exit 3 only on a kernel or reader reject; skips whole-artifact admission and issues no host statement"
     "fail-out" : String; "Write failing selected labels in consts-file format"
     "host-out" : String; "Write the checked whole-artifact host admission statement (certified, unconditional runs only)"
     "host-store"; "Persist the checked host admission statement in the content-addressed store"

Tests/Ix/Kernel/CheckLeanCli.lean

@@ -213,6 +213,31 @@ private def check : IO Nat := do
       anonRows.stderr.contains "missing: unresolved")
       s!"unresolved name aborted the per-name rows\n{anonRows.stderr}"
     expect (← call #["--consts", "CliAlias0", "--json", results.toString, "--fail-out", failures.toString] #[]) 2
+    -- `--allow-declined`: record-check mode tolerates `decline` and `blocked`
+    -- (when no record was rejected), skips whole-artifact admission, still
+    -- fails with exit 3 / `rejected` on `reject`, and rejects host-statement output.
+    reset ()
+    let declinedOk ← call #["--allow-declined", "--consts",
+      String.intercalate "," [label "fidelityAxiom", "BlockedSubject"], "--json", results.toString] #[]
+    expect declinedOk 0
+    ensure ((← status (label "fidelityAxiom")) == some "ok" && (← status "BlockedSubject") == some "ok")
+      s!"--allow-declined did not mark declined/blocked rows ok: {← IO.FS.readFile results}"
+    reset ()
+    let declinedReject ← call #["--allow-declined", "--json", results.toString, "--json-name", "fixture"] #[]
+    expect declinedReject 3
+    ensure ((← status "fixture") == some "rejected")
+      s!"--allow-declined hid a kernel reject: {← IO.FS.readFile results}"
+    reset ()
+    calls.modify (· + 1)
+    let cleanDeclined ← IO.Process.output {
+      cmd := ix.toString,
+      args := #["check-lean", cleanPath.toString, "--allow-declined", "--json", results.toString],
+      env := neutral }
+    expect cleanDeclined 0
+    ensure ((← status "env") == some "ok" &&
+      cleanDeclined.stdout.contains "record check (--allow-declined); no whole-artifact receipt")
+      s!"--allow-declined whole run was not ok: {← IO.FS.readFile results}\n{cleanDeclined.stdout}"
+    expect (← call #["--allow-declined", "--host-store"] #[]) 2
     let count ← calls.get
     IO.println s!"check-lean CLI: {count} process controls; modes, exact aliases/cap, all five outcomes, fail-out, usage/infra exits, --json/--json-name/--per-const rows passed"
     return count

docs/benchmarking.md

@@ -213,7 +213,7 @@ FFT cost from 115.65B to 99.33B (−14.1%), and `total-time` from 63.85s to
 | backend | what it measures | tool |
 |---|---|---|
 | `aiur`    | the Aiur proof pipeline, per constant: the `ixvm` stage proves the IxVM typecheck, the `fri-verifier` stage executes and proves the in-circuit multi-stark verifier over that fresh proof (the KZG stages fold in as they land, each with its own measure prefix), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). Each stage's measures carry its prefix (`ixvm-prove-time`, `fri-verifier-fft-cost`, …). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`). The direct `--recursive --join` diagnostic takes exactly two constants as singleton `CheckEnv` shards and appends one pair row carrying `join-{execute-time,fft-cost,prove-time,peak-rss,proof-size,verify-time}`; the InitStd prove cell schedules this pair in a separate process after the per-constant runs. | `bench-typecheck --recursive` |
-| `ooc`     | out-of-circuit Lean kernel (`IxC`): whole-env row + one full-closure row per constant (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-lean --anon --json` |
+| `ooc`     | out-of-circuit Lean kernel (`IxC`): whole-env record-check row (`--allow-declined`, failing on any kernel `reject`) + one strict full-closure row per constant (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-lean --anon --json` |
 | `compile` | `ix compile <env>.lean → <env>.ixe`, the default certified compiler: compile-time, file-size, constants, throughput | `ix compile --json` |
 | `decompile` | inverse of compile — `ix decompile <env>.ixe → Lean consts`: decompile-time, throughput, peak-rss, constants, file-size (input `.ixe`). Consumes the compile cell's `.ixe` rather than producing one; a malformed decompile reddens the cell. Deep roundtrip fidelity is gated by the canonical checks (`ix validate` / roundtrip tests), which need the original Lean env the `.ixe` can't supply | `ix decompile --json` |
 

docs/kernel.md

@@ -1293,11 +1293,18 @@ axiom prints the same list under `selected checking:`.
 | --- | --- |
 | 0 | everything asked for passed; for a whole bound run, through the certified entry |
 | 1 | an infrastructure failure |
-| 2 | a usage error: a bad flag or selector, a selected name that resolves to no declaration, or a host statement the run cannot issue (a selected, capped, unbound or conditional run) |
-| 3 | a declaration failed, or the artifact was refused |
+| 2 | a usage error: a bad flag or selector, a selected name that resolves to no declaration, or a host statement the run cannot issue (a selected, capped, unbound, `--allow-declined` or conditional run) |
+| 3 | a declaration failed (or, under `--allow-declined`, a declaration or dependency record was rejected), or the artifact was refused |
 | 4 | partial: every declaration passed, but the whole artifact asked for carries no role binding, so its admission did not run |
 | 5 | conditional: everything passed, but only with the listed user axioms admitted |
 
+`--allow-declined` runs the record-by-record check (as the `ooc` whole-env
+benchmark uses it on upstream libraries that contain `Lean.trustCompiler` or
+`unsafe inductive` declarations): declarations outside `IxC`'s fragment
+(`decline`) and their dependents (`blocked`) are tolerated, whole-artifact
+admission does not run and no host statement can be issued, and the run exits 3
+only when a checked declaration or support record has outcome `reject`.
+
 `--json <file>` writes benchmark results rows (`Ix.Benchmark.Results`). A run
 writes one row, keyed by `--json-name` (default `env`). With a selection it
 runs each name's full closure on its own and writes one row per name, keyed