diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index 6bb7cf890..089a77775 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/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 diff --git a/Ix/Cli/CheckLeanCmd.lean b/Ix/Cli/CheckLeanCmd.lean index 435e7e5b7..6873f89e1 100644 --- a/Ix/Cli/CheckLeanCmd.lean +++ b/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 "; 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" diff --git a/Tests/Ix/Kernel/CheckLeanCli.lean b/Tests/Ix/Kernel/CheckLeanCli.lean index 2c1fc3ecd..bbec7994c 100644 --- a/Tests/Ix/Kernel/CheckLeanCli.lean +++ b/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 diff --git a/docs/benchmarking.md b/docs/benchmarking.md index 4603de922..64c5d1c13 100644 --- a/docs/benchmarking.md +++ b/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 .lean → .ixe`, the default certified compiler: compile-time, file-size, constants, throughput | `ix compile --json` | | `decompile` | inverse of compile — `ix decompile .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` | diff --git a/docs/kernel.md b/docs/kernel.md index a900b856a..739191565 100644 --- a/docs/kernel.md +++ b/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 ` 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