diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 1f805d5e0..21f060524 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -16,7 +16,10 @@ name: Benchmark main # 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel # (the same kernel, out-of-circuit and parallel — far faster) # over the whole env, tracking throughput. -# 5. aiur-recursive — the aiur-recursive toy +# 5. decompile — restore that `.ixe` and decompile it back to Lean constants +# (the inverse of step 1); tracks decompile-time / +# throughput / peak-rss. +# 6. aiur-recursive — the aiur-recursive toy # (bench-recursive-verifier): # prove fixed tiny statements, run the in-circuit # multi-stark verifier over each proof, then prove THAT @@ -617,3 +620,80 @@ jobs: --threshold-measure peak-rss --threshold-test percentage --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10 --threshold-lower-boundary _ + + # Decompile — the inverse of compile. Restore the compile job's cached + # `.ixe` and decompile it back to Lean constants. One env-keyed row per + # benched env, mirroring the `compile` cell. A malformed decompile exits + # nonzero and reddens this step; deep roundtrip fidelity is gated by the + # canonical checks (`ix validate` / roundtrip tests), not measured here. No + # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over + # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check. + decompile: + name: decompile-${{ matrix.bench }} + needs: [compile, plan] + runs-on: warp-ubuntu-latest-x64-32x + timeout-minutes: 60 + strategy: + fail-fast: false + matrix: + bench: ${{ fromJson(needs.plan.outputs.bench-envs) }} + steps: + - uses: actions/checkout@v6 + - uses: actions/cache/restore@v5 + with: + path: ~/.local/bin + key: bench-bins-${{ github.sha }} + - run: echo "$HOME/.local/bin" >> $GITHUB_PATH + # Provision the toolchain so `ix` finds libleanshared (no package build). + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + # (The path list must match the compile job's save exactly.) + - uses: actions/cache/restore@v5 + with: + path: | + ${{ matrix.bench }}.ixe + zkshards-${{ matrix.bench }} + key: bench-ixe-${{ github.sha }}-${{ matrix.bench }} + fail-on-cache-miss: true + # A malformed decompile exits nonzero → red X here; a clean run's row + # uploads below. + - name: Run decompile benchmark + run: | + ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \ + --ixe ${{ matrix.bench }}.ixe --out bench.json + # Upload whatever clean rows exist even when the run step reddened the + # job — bmf drops every non-ok (rejected/oom) row. + - name: Convert to Bencher Metric Format + id: bmf + if: ${{ !cancelled() }} + run: | + ix bench bmf --in bench.json --out bench-bmf.json + cat bench-bmf.json + # constants is deterministic → pinned (0/0); decompile-time / throughput + # / peak-rss are noisy wall-clock → percentage bounds. file-size (the + # input `.ixe`) duplicates the compile cell's, so it uploads for the + # row's completeness but rides no threshold here. + - uses: ./.github/actions/bencher-track + if: ${{ !cancelled() && steps.bmf.outcome == 'success' }} + with: + testbed: ix-decompile-x64-32x + workload: ix-decompile + file: bench-bmf.json + key: ${{ secrets.BENCHER_API_KEY }} + github-token: ${{ secrets.GITHUB_TOKEN }} + thresholds: | + --threshold-measure constants --threshold-test percentage + --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0 + --threshold-lower-boundary 0 + --threshold-measure decompile-time --threshold-test percentage + --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10 + --threshold-lower-boundary _ + --threshold-measure throughput --threshold-test percentage + --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _ + --threshold-lower-boundary 0.10 + --threshold-measure peak-rss --threshold-test percentage + --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10 + --threshold-lower-boundary _ diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index 458177d18..0d06a606e 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -1,7 +1,7 @@ # `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv) # through chosen prover backend(s) and post a main-vs-PR comparison table. # -# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute] +# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute] # (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it # with a note in the config summary) # BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive; @@ -20,10 +20,12 @@ # Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` / # `sp1` / `ooc` run `execute`; `compile` runs `ix compile .lean → # .ixe` (the same cell bench-main.yml uploads under testbed -# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy -# (bench-recursive-verifier's fixed configs — env-independent, so it -# always schedules exactly one cell no matter what BENCH_ENVS says). -# The optional bare `execute` token flips `aiur` to +# `ix-compile-*`); `decompile` runs `ix decompile .ixe` over the +# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`); +# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's +# fixed configs — env-independent, so it always schedules exactly one cell +# no matter what BENCH_ENVS says). The optional bare `execute` token flips +# `aiur` to # execute-only (Phase 1, skipping the prove); bench-main runs both aiur # modes as separate cells on separate testbeds, so either kind of cell # fetches a cached main-side baseline from bencher. (aiur's third mode, diff --git a/.github/workflows/bencher-thresholds-reset.yml b/.github/workflows/bencher-thresholds-reset.yml index 0ff3309e8..b4b5947fd 100644 --- a/.github/workflows/bencher-thresholds-reset.yml +++ b/.github/workflows/bencher-thresholds-reset.yml @@ -22,7 +22,7 @@ name: Bencher thresholds reset # cancel by removing it before merge. Naming convention: one label per token, # `bencher-thresholds-reset:` where is a workload (a backend # testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix: -# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or +# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or # `all` (the merge step expands an `all` label into every workload). Labeling # requires Triage+, so PR authors from forks cannot self-queue a reset. The # label shares the command/workflow name; the ref it moves is @@ -44,7 +44,7 @@ on: # GitHub requires literal choice options, so this list stays static: # keep it (and the jobs' valid= lists below) in sync with the # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs). - options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all] + options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all] sha: description: "Commit to anchor to (default: HEAD)" required: false @@ -77,7 +77,7 @@ jobs: # (backendSpecs) minus the runner-arch suffix. Static because this # job runs on a cheap runner with no built `ix`; keep in sync when # adding a backend. - valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute" + valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute" if [ "$EVENT" = workflow_dispatch ]; then # Reset the chosen workload(s) at the given commit; no PR scan. sha="${INPUT_SHA:-$HEAD_SHA}" @@ -133,7 +133,7 @@ jobs: # which the merge job expands into every workload). Same static # list as the reset job; keep both in sync with backendSpecs in # Ix/Cli/BenchCmd.lean. - valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute" + valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute" accepted="$valid all" # Parse the workload token(s) after the command, lowercased. workloads=$(printf '%s' "$BODY" \ diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index 8380b90a7..f6b7a0d26 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [ { name := "compile", defaultMode := "execute", testbeds := [("execute", "ix-compile-x64-32x")], metrics := [("execute", ["compile-time", "throughput", "peak-rss", + "file-size", "constants"])] }, + -- The inverse of compile: decompiles the env's `.ixe` back to Lean + -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe` + -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than + -- producing one. + { name := "decompile", defaultMode := "execute", + testbeds := [("execute", "ix-decompile-x64-32x")], + metrics := [("execute", ["decompile-time", "throughput", "peak-rss", "file-size", "constants"])] } ] @@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do if exit != 0 then IO.eprintln s!"[bench] ix compile failed (exit {exit})" return 1 + | "decompile" => + -- The inverse of compile: consume the env's `.ixe` (the compile cell's + -- fresh artifact) and decompile it back to Lean constants. Env-keyed row, + -- like compile. A malformed decompile exits nonzero and reddens the cell; + -- deep roundtrip fidelity is gated by the canonical roundtrip checks + -- (`ix validate` / the roundtrip tests), not measured here. + let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String)) + let ix ← resolveBin repo "ix" + let exit ← runGuarded watchdog ceilingGb ix + #["decompile", ixe, "--json", out, "--json-name", info.name] + if exit != 0 then + IO.eprintln s!"[bench] ix decompile failed (exit {exit})" | "ooc" => let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String)) let ix ← resolveBin repo "ix" @@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do -- row too. let expected := match backend with | "compile" => #[info.name] + | "decompile" => #[info.name] | "ooc" => #[info.name] ++ names | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray | _ => names @@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli| "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced." FLAGS: - backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive" + backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive" env : String; "Benchmark env from the registry (default: InitStd)" mode : String; "prove | execute | recursive (default: the backend's defaultMode)" out : String; "Benchmark results JSON output path (default: bench.json)" diff --git a/Ix/Cli/BenchPlots.lean b/Ix/Cli/BenchPlots.lean index c54fa44c5..fd1ffcd63 100644 --- a/Ix/Cli/BenchPlots.lean +++ b/Ix/Cli/BenchPlots.lean @@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String := | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage" | "ix-compile", "file-size" => "Ix Environment Size" | "ix-compile", "constants" => "Ix Input Constants" + | "ix-decompile", "decompile-time" => "Ix Decompile Time" + | "ix-decompile", "throughput" => "Ix Decompile Throughput" + | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage" | "aiur-check-prove", "prove-time" => "Aiur Prove Time" | "aiur-check-prove", "throughput" => "Aiur Prove Throughput" | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage" @@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String := "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment column only ("Zisk Cycles" / max-shard-cycles carry the sharding trend), and zisk `constants` charts on the cross-kernel overlay below - instead of alone. -/ + instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so + its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix + Input Constants" exactly — the decompile cell tracks only its own + decompile-time / throughput / peak-rss trends. -/ def plotSkips : List (String × String) := [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"), - ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")] + ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"), + ("ix-decompile", "file-size"), ("ix-decompile", "constants")] /-- Canonical units per measure slug, asserted on every sync: bencher auto-creates a measure with placeholder units ("Measure (units)") on @@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String := if slug.startsWith "phase-" then some "seconds (s)" else [("execute-peak-rss", "bytes (B)"), ("compile-time", "seconds (s)"), + ("decompile-time", "seconds (s)"), ("execute-time", "seconds (s)"), ("prove-time", "seconds (s)"), ("verify-time", "seconds (s)"), @@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String := /-- Dashboard group order (compile first, then aiur prove/execute, zisk, ooc); unranked workloads (a future backend) sort last. -/ def workloadOrder : List String := - ["ix-compile", "aiur-check-prove", "aiur-check-execute", + ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute", "aiur-check-recursive", "aiur-recursive", "zisk-check-execute", "ooc-check"] @@ -127,7 +135,8 @@ structure PlotSpec where /-- One spec per bench-main testbed: its measure slugs and the benchmark row names uploaded there, mirroring the row emitters — compile keys one row per env (benched or not: the compile matrix is deliberately - wider), ooc one whole-env row plus one full-closure row per primary, + wider), decompile one row per benched env (a `.ixe` consumer), ooc one + whole-env row plus one full-closure row per primary, the per-constant backends one row per primary. Dynamic sub-rows (`/shard-N`) are left out: their multiplicity shifts with the shard manifest, and the parent row carries the headline trend. -/ @@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do return (BenchCmd.envSpecs.map (·.name)).toArray if b.name == "aiur-recursive" then return (BenchCmd.recursiveConfigs.map (·.1)).toArray + -- decompile is env-keyed like compile but a `.ixe` consumer: one row + -- per benched env (it runs only where a benched `.ixe` exists). + if b.name == "decompile" then + return benched.toArray let mut ns : Array String := #[] for env in benched do if b.name == "ooc" then ns := ns.push env diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean index 5c32614a1..83153e260 100644 --- a/Ix/Cli/BenchReport.lean +++ b/Ix/Cli/BenchReport.lean @@ -43,7 +43,7 @@ def metricKind (metric : String) : String := then "bytes" else if metric.startsWith "phase-" then "seconds" else if ["execute-time", "prove-time", "verify-time", "check-time", - "compile-time"].contains metric then "seconds" + "compile-time", "decompile-time"].contains metric then "seconds" else if ["fft-cost", "cycles", "steps", "max-shard-cycles", "throughput"].contains metric then "count" else if ["constants", "shards"].contains metric then "int" diff --git a/Ix/Cli/DecompileCmd.lean b/Ix/Cli/DecompileCmd.lean new file mode 100644 index 000000000..60f2bac96 --- /dev/null +++ b/Ix/Cli/DecompileCmd.lean @@ -0,0 +1,83 @@ +/- + `ix decompile `: decompile a serialized `.ixe` environment back to + Lean constants — the inverse of `ix compile`. This is the decompile + benchmark's measured tool (env-keyed row, mirroring `ix compile --json`). + + With `--json` the run records one env-keyed results row (decompile-time, + file-size, constants, throughput, peak-rss). A malformed decompile is a hard + error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity + is gated by the canonical roundtrip checks (`ix validate` / the roundtrip + tests), which need the original Lean env a `.ixe` can't supply — so this + performance tool does not reproduce them. +-/ +module +public import Cli +public import Ix.Common +public import Ix.TracingTexray +public import Ix.Benchmark.Results + +public section + +open System (FilePath) + +namespace Ix.Cli.DecompileCmd + +/-- Decompile a `.ixe` from disk, returning the decompiled constant + count. A malformed decompile throws (hard error). Implemented in + `crates/ffi/src/compile.rs::rs_decompile_env`. -/ +@[extern "rs_decompile_env"] +opaque rsDecompileEnvFFI : @& String → IO Nat + +def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do + let some pathArg := p.positionalArg? "path" + | p.printError "error: must specify to a .ixe file" + return Ix.Benchmark.Results.exitUsage + let envPath := pathArg.as! String + + -- Window the tree-RSS sampler around the decompile, mirroring + -- `ix compile --json` so the two rows share measurement + -- infrastructure and peak-rss semantics. + let benched := (p.flag? "json").isSome + if benched then + TracingTexray.startSampler + TracingTexray.resetPeakTreeRss + + IO.println s!"Decompiling {envPath}" + let start ← IO.monoMsNow + let constants ← rsDecompileEnvFFI envPath + let elapsed := (← IO.monoMsNow) - start + IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}" + + if let some flag := p.flag? "json" then + let key := (p.flag? "json-name").map (·.as! String) + |>.getD ((FilePath.mk envPath).fileStem.getD "env") + let secs := elapsed.toFloat / 1000.0 + let tput := if elapsed > 0 + then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0 + let peakRss ← TracingTexray.peakTreeRssBytes + -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte + -- counterpart to compile's output `.ixe`). + let size := (← (FilePath.mk envPath).metadata).byteSize.toNat + Ix.Benchmark.Results.writeRow (flag.as! String) key "ok" + [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs) + , ("file-size", Lean.toJson size) + , ("constants", Lean.toJson constants) + , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput) + , ("peak-rss", Lean.toJson peakRss) ] + + return 0 + +end Ix.Cli.DecompileCmd + +open Ix.Cli.DecompileCmd in +def decompileCmd : Cli.Cmd := `[Cli| + decompile VIA runDecompileCmd; + "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests." + + FLAGS: + json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object." + "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)." + + ARGS: + path : String; "Path to the serialized `.ixe` environment to decompile." +] diff --git a/Ix/DecompileM.lean b/Ix/DecompileM.lean index e2f548a93..f59874a48 100644 --- a/Ix/DecompileM.lean +++ b/Ix/DecompileM.lean @@ -811,16 +811,6 @@ def decompileAllParallelIO (ixonEnv : Ixon.Env) IO.println s!" [Decompile] Done: {result.size} ok, {errors.size} errors in {elapsed}ms" pure (result, errors) -/-! ## Rust FFI Decompilation -/ - -@[extern "rs_decompile_env"] -opaque rsDecompileEnvFFI : @& Ixon.RawEnv → Except DecompileError (Array (Ix.Name × Ix.ConstantInfo)) - -/-- Decompile an Ixon.Env to Ix.ConstantInfo using Rust. -/ -def rsDecompileEnv (env : Ixon.Env) : Except DecompileError (Std.HashMap Ix.Name Ix.ConstantInfo) := do - let arr ← rsDecompileEnvFFI env.toRawEnv - return arr.foldl (init := {}) fun m (name, info) => m.insert name info - end Ix.DecompileM end diff --git a/Main.lean b/Main.lean index c3bdbd4b5..580309aeb 100644 --- a/Main.lean +++ b/Main.lean @@ -6,6 +6,7 @@ import Ix.Cli.CodegenCmd import Ix.Cli.CheckRsCmd import Ix.Cli.ClaimCmd import Ix.Cli.CompileCmd +import Ix.Cli.DecompileCmd import Ix.Cli.DiffCmd import Ix.Cli.IngressCmd import Ix.Cli.PackCmd @@ -30,6 +31,7 @@ def ixCmd : Cli.Cmd := `[Cli| --storeCmd; benchCmd; compileCmd; + decompileCmd; checkCmd; checkRsCmd; claimCmd; diff --git a/Tests/Ix/RustDecompile.lean b/Tests/Ix/RustDecompile.lean index 43e8ef4f1..4222ddcad 100644 --- a/Tests/Ix/RustDecompile.lean +++ b/Tests/Ix/RustDecompile.lean @@ -1,127 +1,43 @@ /- - Rust decompilation tests. - Tests the Rust FFI endpoint for decompilation by compiling with Rust, - decompiling with Rust, and comparing against the original environment. + Rust decompile roundtrip test. + + Exercises `Lean env → compile → serialize → deserialize → decompile → + Lean` — the `ix decompile` pipeline over the serialized `.ixe` + boundary (demoted-at-parse metadata load, `Named.original` recovery + for shape-divergent aux blocks, expression interning) — and + hash-compares every constant against the original. + `kernel-ixon-roundtrip` covers the kernel ingress/egress leg instead. -/ - -module -public import Ix.Ixon -public import Ix.Environment -public import Ix.Address -public import Ix.Common -public import Ix.Meta -public import Ix.CompileM -public import Ix.DecompileM -public import Lean -public import LSpec -public import Tests.Ix.Fixtures +import Ix.Common +import Ix.Meta +import LSpec open LSpec namespace Tests.RustDecompile -/-- Test Rust decompilation: compile → rsDecompileEnv → hash comparison -/ -def testRustDecompile : TestSeq := - .individualIO "Rust Decompilation Roundtrip" none (do - let leanEnv ← get_env! - let totalConsts := leanEnv.constants.toList.length - - IO.println s!"[Test] Rust Decompilation Roundtrip Test" - IO.println s!"[Test] Environment has {totalConsts} constants" - IO.println "" - - -- Step 1: Run Rust compilation pipeline - IO.println s!"[Step 1] Running Rust compilation pipeline..." - let rustStart ← IO.monoMsNow - let phases ← Ix.CompileM.rsCompilePhases leanEnv - let rustTime := (← IO.monoMsNow) - rustStart - IO.println s!"[Step 1] Rust: {phases.compileEnv.constCount} compiled in {rustTime}ms" - IO.println s!"[Step 1] names={phases.compileEnv.names.size}, named={phases.compileEnv.named.size}, consts={phases.compileEnv.consts.size}, blobs={phases.compileEnv.blobs.size}" - IO.println "" - - -- Step 2: Decompile with Rust - IO.println s!"[Step 2] Decompiling with Rust (rsDecompileEnv)..." - let decompStart ← IO.monoMsNow - let decompiled ← match Ix.DecompileM.rsDecompileEnv phases.compileEnv with - | .ok env => pure env - | .error e => do - IO.println s!"[Step 2] FAILED: {toString e}" - return (false, 0, 0, some (toString e)) - let decompTime := (← IO.monoMsNow) - decompStart - IO.println s!"[Step 2] {decompiled.size} constants decompiled in {decompTime}ms" - IO.println "" +/-- FFI: run the serialized decompile roundtrip and collect per-constant + diff messages. Empty array = decompile agrees with the original Lean + env. - -- Count by constant type - let mut nDefn := (0 : Nat); let mut nAxiom := (0 : Nat) - let mut nInduct := (0 : Nat); let mut nCtor := (0 : Nat) - let mut nRec := (0 : Nat); let mut nQuot := (0 : Nat) - let mut nOpaque := (0 : Nat); let mut nThm := (0 : Nat) - for (_, info) in decompiled do - match info with - | .defnInfo _ => nDefn := nDefn + 1 - | .axiomInfo _ => nAxiom := nAxiom + 1 - | .inductInfo _ => nInduct := nInduct + 1 - | .ctorInfo _ => nCtor := nCtor + 1 - | .recInfo _ => nRec := nRec + 1 - | .quotInfo _ => nQuot := nQuot + 1 - | .opaqueInfo _ => nOpaque := nOpaque + 1 - | .thmInfo _ => nThm := nThm + 1 - IO.println s!"[Types] defn={nDefn}, thm={nThm}, opaque={nOpaque}, axiom={nAxiom}, induct={nInduct}, ctor={nCtor}, rec={nRec}, quot={nQuot}" - IO.println "" + Implemented in `crates/ffi/src/kernel.rs::rs_decompile_roundtrip`. -/ +@[extern "rs_decompile_roundtrip"] +opaque rsDecompileRoundtripFFI : + @& List (Lean.Name × Lean.ConstantInfo) → IO (Array String) - -- Step 3: Hash-based comparison against original Ix.Environment - let ixEnv := phases.rawEnv - IO.println s!"[Step 3] Original Ix.Environment has {ixEnv.consts.size} constants" - IO.println s!"[Compare] Hash-comparing {decompiled.size} decompiled constants..." - let compareStart ← IO.monoMsNow - - let mut nMatch := (0 : Nat); let mut nMismatch := (0 : Nat); let mut nMissing := (0 : Nat) - let mut firstMismatches : Array (Ix.Name × String) := #[] - for (name, decompInfo) in decompiled do - match ixEnv.consts.get? name with - | some origInfo => - let decompTyHash := decompInfo.getCnst.type.getHash - let origTyHash := origInfo.getCnst.type.getHash - if decompTyHash != origTyHash then - nMismatch := nMismatch + 1 - if firstMismatches.size < 10 then - firstMismatches := firstMismatches.push (name, s!"type hash mismatch") - else - let valMismatch := match decompInfo, origInfo with - | .defnInfo dv, .defnInfo ov => dv.value.getHash != ov.value.getHash - | .thmInfo dv, .thmInfo ov => dv.value.getHash != ov.value.getHash - | .opaqueInfo dv, .opaqueInfo ov => dv.value.getHash != ov.value.getHash - | _, _ => false - if valMismatch then - nMismatch := nMismatch + 1 - if firstMismatches.size < 10 then - firstMismatches := firstMismatches.push (name, s!"value hash mismatch") - else - nMatch := nMatch + 1 - | none => - nMissing := nMissing + 1 - if firstMismatches.size < 10 then - firstMismatches := firstMismatches.push (name, "not in original") - - let compareTime := (← IO.monoMsNow) - compareStart - IO.println s!"[Compare] Matched: {nMatch}, Mismatched: {nMismatch}, Missing: {nMissing} ({compareTime}ms)" - if !firstMismatches.isEmpty then - IO.println s!"[Compare] First mismatches:" - for (name, diff) in firstMismatches do - IO.println s!" {name}: {diff}" - IO.println "" - - let success := nMismatch == 0 && nMissing == 0 - if success then +def testRoundtrip : TestSeq := + .individualIO "rust decompile roundtrip" none (do + let leanEnv ← get_env! + let errors ← rsDecompileRoundtripFFI leanEnv.constants.toList + if errors.isEmpty then return (true, 0, 0, none) else - return (false, 0, 0, some s!"{nMismatch} mismatches, {nMissing} missing") + IO.println s!"[rust-decompile] {errors.size} errors:" + for msg in errors[:min 20 errors.size] do + IO.println s!" {msg}" + return (false, 0, 0, some s!"{errors.size} roundtrip mismatches") ) .done -/-! ## Test Suite -/ - -public def rustDecompileSuiteIO : List TestSeq := [ - testRustDecompile, -] +def rustDecompileSuiteIO : List TestSeq := [testRoundtrip] end Tests.RustDecompile diff --git a/Tests/Main.lean b/Tests/Main.lean index 165805972..8a1eebd06 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -64,11 +64,7 @@ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ --("compile", Tests.Compile.compileSuiteIO), --("decompile", Tests.Decompile.decompileSuiteIO), ("rust-serialize", Tests.RustSerialize.rustSerializeSuiteIO), - -- Rust decompile of synthesized `_sparseCasesOn` aux constants fails - -- ("missing Ref metadata": their aux_gen metadata arena misaligns - -- with the serialized expr, and pure-aux constants have no - -- `Named.original` sidecar to recover from), disabled - --("rust-decompile", Tests.RustDecompile.rustDecompileSuiteIO), + ("rust-decompile", Tests.RustDecompile.rustDecompileSuiteIO), ("commit-io", Tests.Commit.suiteIO), ("kernel-ixon-roundtrip", Tests.Ix.Kernel.Roundtrip.suite), --("kernel-lean-roundtrip", Tests.Ix.Kernel.RoundtripNoCompile.suite), diff --git a/crates/compile/src/decompile.rs b/crates/compile/src/decompile.rs index db94ac238..57f940935 100644 --- a/crates/compile/src/decompile.rs +++ b/crates/compile/src/decompile.rs @@ -51,6 +51,15 @@ use std::sync::Arc; pub struct DecompileState { /// Decompiled environment pub env: DashMap, + /// Canonical expression nodes keyed by content hash. Decompilation + /// rebuilds every constant's expressions with sharing local to that + /// constant, so structurally equal subterms (common types, applied + /// prefixes) would otherwise each hold a private copy per referencing + /// constant — a multiple of the whole env's footprint. Constants + /// entering `env` are canonicalized through this table + /// ([`Self::insert_interned`]); `decompile_env` drops the table + /// before returning, since `env` keeps the canonical `Arc`s alive. + expr_intern: DashMap<[u8; 32], LeanExpr>, } #[derive(Debug)] @@ -62,6 +71,184 @@ impl DecompileState { pub fn stats(&self) -> DecompileStateStats { DecompileStateStats { env: self.env.len() } } + + /// Insert a decompiled constant, canonicalizing its expressions + /// through [`Self::expr_intern`]. + fn insert_interned(&self, name: Name, ci: LeanConstantInfo) { + self.env.insert(name, self.intern_ci(ci)); + } + + /// Canonicalize every expression field of `ci` — see + /// [`Self::expr_intern`]. + fn intern_ci(&self, mut ci: LeanConstantInfo) -> LeanConstantInfo { + match &mut ci { + LeanConstantInfo::AxiomInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + }, + LeanConstantInfo::DefnInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + v.value = self.intern_expr(&v.value); + }, + LeanConstantInfo::ThmInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + v.value = self.intern_expr(&v.value); + }, + LeanConstantInfo::OpaqueInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + v.value = self.intern_expr(&v.value); + }, + LeanConstantInfo::QuotInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + }, + LeanConstantInfo::InductInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + }, + LeanConstantInfo::CtorInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + }, + LeanConstantInfo::RecInfo(v) => { + v.cnst.typ = self.intern_expr(&v.cnst.typ); + for rule in &mut v.rules { + rule.rhs = self.intern_expr(&rule.rhs); + } + }, + } + ci + } + + /// Canonicalize one expression DAG bottom-up through + /// [`Self::expr_intern`]. Iterative — proof terms nest far deeper + /// than the stack allows for recursion. Nodes are rebuilt only when + /// a child changed; hashes are content-derived from child hashes, so + /// a rebuild with content-equal children reuses the stored hash. + fn intern_expr(&self, root: &LeanExpr) -> LeanExpr { + use ix_common::env::ExprData as ED; + + if let Some(hit) = self.expr_intern.get(root.get_hash().as_bytes()) { + return hit.clone(); + } + + // Per-walk memo keyed by node pointer: within-constant sharing + // makes the same `Arc` reachable from several parents. + let mut memo: FxHashMap<*const ED, LeanExpr> = FxHashMap::default(); + // (node, children_done) + let mut stack: Vec<(LeanExpr, bool)> = vec![(root.clone(), false)]; + + while let Some((e, children_done)) = stack.pop() { + let key: *const ED = Arc::as_ptr(&e.0); + if memo.contains_key(&key) { + continue; + } + if !children_done { + if let Some(hit) = self.expr_intern.get(e.get_hash().as_bytes()) { + memo.insert(key, hit.clone()); + continue; + } + stack.push((e.clone(), true)); + match e.as_data() { + ED::App(f, a, _) => { + stack.push((f.clone(), false)); + stack.push((a.clone(), false)); + }, + ED::Lam(_, t, b, _, _) | ED::ForallE(_, t, b, _, _) => { + stack.push((t.clone(), false)); + stack.push((b.clone(), false)); + }, + ED::LetE(_, t, v, b, _, _) => { + stack.push((t.clone(), false)); + stack.push((v.clone(), false)); + stack.push((b.clone(), false)); + }, + ED::Mdata(_, inner, _) => stack.push((inner.clone(), false)), + ED::Proj(_, _, s, _) => stack.push((s.clone(), false)), + ED::Bvar(..) + | ED::Fvar(..) + | ED::Mvar(..) + | ED::Sort(..) + | ED::Const(..) + | ED::Lit(..) => {}, + } + continue; + } + + // Children are canonicalized (they were pushed after this node's + // revisit frame, so they popped first). + let child = |c: &LeanExpr| -> LeanExpr { + memo + .get(&Arc::as_ptr(&c.0)) + .expect("intern walk: child not canonicalized before parent") + .clone() + }; + let same = + |c: &LeanExpr, i: &LeanExpr| -> bool { Arc::ptr_eq(&c.0, &i.0) }; + let rebuilt = match e.as_data() { + ED::App(f, a, h) => { + let (fi, ai) = (child(f), child(a)); + if same(f, &fi) && same(a, &ai) { + e.clone() + } else { + LeanExpr(Arc::new(ED::App(fi, ai, *h))) + } + }, + ED::Lam(n, t, b, bi, h) => { + let (ti, bdi) = (child(t), child(b)); + if same(t, &ti) && same(b, &bdi) { + e.clone() + } else { + LeanExpr(Arc::new(ED::Lam(n.clone(), ti, bdi, bi.clone(), *h))) + } + }, + ED::ForallE(n, t, b, bi, h) => { + let (ti, bdi) = (child(t), child(b)); + if same(t, &ti) && same(b, &bdi) { + e.clone() + } else { + LeanExpr(Arc::new(ED::ForallE(n.clone(), ti, bdi, bi.clone(), *h))) + } + }, + ED::LetE(n, t, v, b, nd, h) => { + let (ti, vi, bdi) = (child(t), child(v), child(b)); + if same(t, &ti) && same(v, &vi) && same(b, &bdi) { + e.clone() + } else { + LeanExpr(Arc::new(ED::LetE(n.clone(), ti, vi, bdi, *nd, *h))) + } + }, + ED::Mdata(kv, inner, h) => { + let ii = child(inner); + if same(inner, &ii) { + e.clone() + } else { + LeanExpr(Arc::new(ED::Mdata(kv.clone(), ii, *h))) + } + }, + ED::Proj(n, i, s, h) => { + let si = child(s); + if same(s, &si) { + e.clone() + } else { + LeanExpr(Arc::new(ED::Proj(n.clone(), i.clone(), si, *h))) + } + }, + ED::Bvar(..) + | ED::Fvar(..) + | ED::Mvar(..) + | ED::Sort(..) + | ED::Const(..) + | ED::Lit(..) => e.clone(), + }; + let canonical = self + .expr_intern + .entry(*e.get_hash().as_bytes()) + .or_insert(rebuilt) + .clone(); + memo.insert(key, canonical); + } + + memo + .remove(&Arc::as_ptr(&root.0)) + .expect("intern walk: root not canonicalized") + } } /// Per-block decompilation cache. @@ -1749,7 +1936,7 @@ fn decompile_projection( Some(MutConst::Defn(def)) => { let info = decompile_definition(def, &named_meta, &mut cache, stt, dstt)?; - dstt.env.insert(name.clone(), info); + dstt.insert_interned(name.clone(), info); }, other => { return Err(projection_mismatch_error( @@ -1767,7 +1954,8 @@ fn decompile_projection( Some(MutConst::Indc(ind)) => { let (ind_val, ctors) = decompile_inductive(ind, &named_meta, &mut cache, stt, dstt)?; - dstt.env.insert(name.clone(), LeanConstantInfo::InductInfo(ind_val)); + dstt + .insert_interned(name.clone(), LeanConstantInfo::InductInfo(ind_val)); for ctor in ctors { dstt .env @@ -1789,7 +1977,7 @@ fn decompile_projection( ConstantInfo::RPrj(proj) => match mutuals.get(proj.idx as usize) { Some(MutConst::Recr(rec)) => { let info = decompile_recursor(rec, &named_meta, &mut cache, stt, dstt)?; - dstt.env.insert(name.clone(), info); + dstt.insert_interned(name.clone(), info); }, other => { return Err(projection_mismatch_error( @@ -1865,7 +2053,7 @@ fn decompile_const( }; cache.load_meta_extensions(&named_meta); let info = decompile_definition(def, &named_meta, &mut cache, stt, dstt)?; - dstt.env.insert(name.clone(), info); + dstt.insert_interned(name.clone(), info); }, Constant { info: ConstantInfo::Recr(rec), sharing, refs, univs } => { @@ -1884,7 +2072,7 @@ fn decompile_const( // `meta_sharing` slot. cache.load_meta_extensions(&named_meta); let info = decompile_recursor(rec, &named_meta, &mut cache, stt, dstt)?; - dstt.env.insert(name.clone(), info); + dstt.insert_interned(name.clone(), info); }, Constant { info: ConstantInfo::Axio(ax), sharing, refs, univs } => { @@ -1900,7 +2088,7 @@ fn decompile_const( // load extensions for consistency with the other branches. cache.load_meta_extensions(&named_meta); let info = decompile_axiom(ax, &named_meta, &mut cache, stt, dstt)?; - dstt.env.insert(name.clone(), info); + dstt.insert_interned(name.clone(), info); }, Constant { info: ConstantInfo::Quot(quot), sharing, refs, univs } => { @@ -1916,7 +2104,7 @@ fn decompile_const( // axioms. Load extensions for consistency. cache.load_meta_extensions(&named_meta); let info = decompile_quotient(quot, &named_meta, &mut cache, stt, dstt)?; - dstt.env.insert(name.clone(), info); + dstt.insert_interned(name.clone(), info); }, Constant { info: ConstantInfo::DPrj(_), .. } @@ -3483,51 +3671,32 @@ fn decompile_named_const( /// in-memory perm lookups see the same permutation compile produced, /// even when `stt` was reconstructed from a deserialized Ixon env. /// -/// Walk every Muts-tagged Named entry; if it carries a stored +/// Walk every Muts-tagged index entry; if it carries a stored /// `aux_layout`, locate the block's source-order first inductive name /// via one of its primary members' `Indc.all[0]` and populate /// `stt.aux_perms[first_name] = layout`. /// /// Idempotent: if `stt.aux_perms` already has an entry for the name, we /// leave it alone (compile-in-progress stt wins over rehydrated copy). -fn rehydrate_aux_perms_from_env(stt: &CompileState) { +fn rehydrate_aux_perms_from_env( + stt: &CompileState, + muts_index: &MutsPlanIndex, +) { use ixon::metadata::ConstantMetaInfo; - let mut n_muts = 0usize; let mut n_muts_with_layout = 0usize; let mut n_populated = 0usize; - // Fast path: every Muts entry is scanned; for non-nested blocks this - // is a single `None` check and a no-op. The cost scales with the - // number of mutual blocks in the env, not their sizes. - for muts_entry in stt.env.named.iter() { - let muts_named = muts_entry.value(); - let muts_meta = muts_named.meta(); - let (muts_all, aux_layout) = match &muts_meta.info { - ConstantMetaInfo::Muts { all, aux_layout: Some(layout) } => { - n_muts += 1; - n_muts_with_layout += 1; - (all, layout.clone()) - }, - ConstantMetaInfo::Muts { .. } => { - n_muts += 1; - continue; - }, - _ => continue, - }; - if muts_all.is_empty() || muts_all[0].is_empty() { + for entry in &muts_index.entries { + let Some(aux_layout) = entry.aux_layout.clone() else { continue; - } - - // muts_all[0][0] is the name-hash address of the first canonical - // class representative. Look up its Named entry to find the Indc - // metadata, which carries `all` in source order. - let first_rep_addr = &muts_all[0][0]; - let first_rep_name = match stt.env.get_name(first_rep_addr) { - Some(n) => n, - None => continue, }; - let rep_named = match stt.env.named.get(&first_rep_name) { + n_muts_with_layout += 1; + + // The first canonical class representative's Named entry carries + // the Indc metadata, whose `all` is in source order. + let first_rep_name = &entry.class_names[0][0]; + let rep_named = match stt.env.named.get(first_rep_name) { Some(r) => r, None => continue, }; @@ -3562,8 +3731,9 @@ fn rehydrate_aux_perms_from_env(stt: &CompileState) { if std::env::var_os("IX_AUX_LAYOUT_DEBUG").is_some() { eprintln!( - "[rehydrate_aux_perms] scanned {n_muts} Muts entries, \ - {n_muts_with_layout} had stored aux_layout, {n_populated} populated" + "[rehydrate_aux_perms] scanned {} Muts entries, \ + {n_muts_with_layout} had stored aux_layout, {n_populated} populated", + muts_index.entries.len(), ); } } @@ -3610,6 +3780,107 @@ struct StoredPlanBlock { flat_names: Vec, } +/// ` · rss X.X GiB (anon Y.Y, file Z.Z)` sampled from +/// `/proc/self/status`, appended to phase logs. Anon can only leave RAM +/// via swap; file RSS is reclaimable page cache — the split shows which +/// memory-reduction lever applies. Empty when procfs is unavailable. +fn rss_log_suffix() -> String { + let Ok(status) = std::fs::read_to_string("/proc/self/status") else { + return String::new(); + }; + let field_kb = |name: &str| -> Option { + status + .lines() + .find(|l| l.starts_with(name)) + .and_then(|l| l.split_whitespace().nth(1)) + .and_then(|v| v.parse().ok()) + }; + let gib_tenths = |kb: u64| -> (u64, u64) { + let tenths = kb * 10 / (1024 * 1024); + (tenths / 10, tenths % 10) + }; + match (field_kb("VmRSS:"), field_kb("RssAnon:"), field_kb("RssFile:")) { + (Some(rss), Some(anon), Some(file)) => { + let (r, rt) = gib_tenths(rss); + let (a, at) = gib_tenths(anon); + let (f, ft) = gib_tenths(file); + format!(" · rss {r}.{rt} GiB (anon {a}.{at}, file {f}.{ft})") + }, + _ => String::new(), + } +} + +/// One `Muts`-tagged Named entry, pre-resolved for plan lookups. +struct MutsIndexEntry { + class_names: Vec>, + flat_names: Vec, + aux_layout: Option, +} + +/// Every `Muts`-tagged Named entry with its class-name lists resolved, +/// built in one parallel scan over `stt.env.named` (one metadata decode +/// per entry). +/// +/// Under `IX_COMPILE_DEMOTE` (the default) `Named::meta()` is a full +/// arena decode per call, so a whole-env scan that touches every +/// entry's metadata costs one decode per entry per scan. Per-block +/// consumers like `stored_plan_blocks_for_original_all` must therefore +/// query an index rather than rescan the named section — O(blocks × env) +/// decodes dominate Pass 2 otherwise. `stt.env` is immutable during +/// decompile, so one scan up front serves every block. +struct MutsPlanIndex { + entries: Vec, + /// Flat member name → indices into `entries`, so a block's plan + /// lookup only inspects entries sharing at least one member. + by_member: FxHashMap>, +} + +fn build_muts_plan_index(stt: &CompileState) -> MutsPlanIndex { + use ixon::metadata::ConstantMetaInfo; + use rayon::prelude::*; + + let entries: Vec = stt + .env + .named + .par_iter() + .filter_map(|entry| { + let meta = entry.value().meta(); + let ConstantMetaInfo::Muts { all, aux_layout } = &meta.info else { + return None; + }; + let mut class_names = Vec::with_capacity(all.len()); + let mut flat_names = Vec::new(); + for class in all { + let names = names_from_addrs(class, stt)?; + if names.is_empty() { + return None; + } + flat_names.extend(names.iter().cloned()); + class_names.push(names); + } + if flat_names.is_empty() { + return None; + } + Some(MutsIndexEntry { + class_names, + flat_names, + aux_layout: aux_layout.clone(), + }) + }) + .collect(); + + let mut by_member: FxHashMap> = FxHashMap::default(); + for (i, entry) in entries.iter().enumerate() { + for name in &entry.flat_names { + by_member + .entry(name.clone()) + .or_default() + .push(u32::try_from(i).expect("muts index entry count exceeds u32")); + } + } + MutsPlanIndex { entries, by_member } +} + fn names_from_addrs( addrs: &[Address], stt: &CompileState, @@ -3628,40 +3899,29 @@ fn indc_source_all(name: &Name, stt: &CompileState) -> Option> { fn stored_plan_blocks_for_original_all( original_all: &[Name], stt: &CompileState, + muts_index: &MutsPlanIndex, ) -> Vec { let original_set: FxHashSet = original_all.iter().cloned().collect(); let mut candidates = Vec::new(); let mut seen: FxHashSet> = FxHashSet::default(); - for muts_entry in stt.env.named.iter() { - let muts_meta = muts_entry.value().meta(); - let ConstantMetaInfo::Muts { all, aux_layout } = &muts_meta.info else { - continue; - }; + // Only entries sharing a member with `original_all` can pass the + // subset filter below, so the by-member index is a complete + // candidate set. + let mut candidate_ids: Vec = original_all + .iter() + .flat_map(|n| muts_index.by_member.get(n).into_iter().flatten().copied()) + .collect(); + candidate_ids.sort_unstable(); + candidate_ids.dedup(); - let mut class_names = Vec::with_capacity(all.len()); - let mut flat_names = Vec::new(); - let mut valid = true; - for class in all { - let Some(names) = names_from_addrs(class, stt) else { - valid = false; - break; - }; - if names.is_empty() { - valid = false; - break; - } - flat_names.extend(names.iter().cloned()); - class_names.push(names); - } - if !valid || flat_names.is_empty() { - continue; - } - if !flat_names.iter().all(|name| original_set.contains(name)) { + for id in candidate_ids { + let entry = &muts_index.entries[id as usize]; + if !entry.flat_names.iter().all(|name| original_set.contains(name)) { continue; } - let same_source_all = flat_names.iter().any(|name| { + let same_source_all = entry.flat_names.iter().any(|name| { indc_source_all(name, stt) .is_some_and(|source_all| source_all.as_slice() == original_all) }); @@ -3669,13 +3929,13 @@ fn stored_plan_blocks_for_original_all( continue; } - if !seen.insert(flat_names.clone()) { + if !seen.insert(entry.flat_names.clone()) { continue; } candidates.push(StoredPlanBlock { - class_names, - aux_layout: aux_layout.clone(), - flat_names, + class_names: entry.class_names.clone(), + aux_layout: entry.aux_layout.clone(), + flat_names: entry.flat_names.clone(), }); } @@ -3732,6 +3992,7 @@ fn install_decompile_call_site_plans( aux_members: &[(AuxKind, Name)], env: &LeanEnv, stt: &CompileState, + muts_index: &MutsPlanIndex, ) -> Result<(), DecompileError> { use crate::compile::{aux_gen, surgery}; @@ -3740,7 +4001,8 @@ fn install_decompile_call_site_plans( } let original_all: Vec = all_names.to_vec(); - let mut plan_blocks = stored_plan_blocks_for_original_all(&original_all, stt); + let mut plan_blocks = + stored_plan_blocks_for_original_all(&original_all, stt, muts_index); if plan_blocks.is_empty() { plan_blocks = fallback_plan_blocks_from_sort(all_names, env, stt)?; } @@ -3869,6 +4131,7 @@ fn decompile_block_aux_gen( kctx: &mut crate::compile::KernelCtx, stt: &CompileState, dstt: &DecompileState, + muts_index: &MutsPlanIndex, ) -> Vec<(Name, DecompileError)> { use crate::compile::aux_gen::{ below::{BelowConstant, generate_below_constants}, @@ -4015,7 +4278,7 @@ fn decompile_block_aux_gen( } for (n, ci) in roundtripped { if rec_members.contains(&&n) || env.contains_key(&n) { - dstt.env.insert(n, ci); + dstt.insert_interned(n, ci); } } }, @@ -4023,7 +4286,10 @@ fn decompile_block_aux_gen( eprintln!("[decompile] roundtrip_block .rec failed: {e}"); for (n, rv) in &canonical_recs { if rec_members.contains(&n) { - dstt.env.insert(n.clone(), LeanConstantInfo::RecInfo(rv.clone())); + dstt.insert_interned( + n.clone(), + LeanConstantInfo::RecInfo(rv.clone()), + ); } } aux_gen_errors.push((all_names[0].clone(), e)); @@ -4045,12 +4311,18 @@ fn decompile_block_aux_gen( if !env.contains_key(n) { env.insert(n.clone(), ci.clone()); } - dstt.env.entry(n.clone()).or_insert_with(|| ci.clone()); + if !dstt.env.contains_key(n) { + dstt.insert_interned(n.clone(), ci.clone()); + } } - if let Err(e) = - install_decompile_call_site_plans(all_names, aux_members, env, stt) - { + if let Err(e) = install_decompile_call_site_plans( + all_names, + aux_members, + env, + stt, + muts_index, + ) { aux_gen_errors.push((all_names[0].clone(), e)); } @@ -4120,7 +4392,7 @@ fn decompile_block_aux_gen( match roundtrip_block(&[mc], &generated_consts, orig_env, stt, dstt) { Ok(roundtripped) if !roundtripped.is_empty() => { for (n, ci) in roundtripped { - dstt.env.insert(n, ci); + dstt.insert_interned(n, ci); } }, Ok(_) => { @@ -4129,7 +4401,7 @@ fn decompile_block_aux_gen( if !recover_aux_from_original(&aux_def.name, stt, dstt) && let Some(ci) = generated_consts.get(&aux_def.name) { - dstt.env.insert(aux_def.name.clone(), ci.clone()); + dstt.insert_interned(aux_def.name.clone(), ci.clone()); } }, Err(e) => { @@ -4140,7 +4412,7 @@ fn decompile_block_aux_gen( if !recover_aux_from_original(&aux_def.name, stt, dstt) && let Some(ci) = generated_consts.get(&aux_def.name) { - dstt.env.insert(aux_def.name.clone(), ci.clone()); + dstt.insert_interned(aux_def.name.clone(), ci.clone()); } aux_gen_errors.push((aux_def.name.clone(), e)); }, @@ -4214,7 +4486,7 @@ fn decompile_block_aux_gen( match roundtrip_block(&[mc], &generated_consts, orig_env, stt, dstt) { Ok(roundtripped) if !roundtripped.is_empty() => { for (n, ci) in roundtripped { - dstt.env.insert(n, ci); + dstt.insert_interned(n, ci); } }, Ok(_) => { @@ -4223,7 +4495,7 @@ fn decompile_block_aux_gen( if !recover_aux_from_original(&aux_def.name, stt, dstt) && let Some(ci) = generated_consts.get(&aux_def.name) { - dstt.env.insert(aux_def.name.clone(), ci.clone()); + dstt.insert_interned(aux_def.name.clone(), ci.clone()); } }, Err(e) => { @@ -4234,7 +4506,7 @@ fn decompile_block_aux_gen( if !recover_aux_from_original(&aux_def.name, stt, dstt) && let Some(ci) = generated_consts.get(&aux_def.name) { - dstt.env.insert(aux_def.name.clone(), ci.clone()); + dstt.insert_interned(aux_def.name.clone(), ci.clone()); } aux_gen_errors.push((aux_def.name.clone(), e)); }, @@ -4304,7 +4576,9 @@ fn decompile_block_aux_gen( if !env.contains_key(n) { env.insert(n.clone(), ci.clone()); } - dstt.env.entry(n.clone()).or_insert_with(|| ci.clone()); + if !dstt.env.contains_key(n) { + dstt.insert_interned(n.clone(), ci.clone()); + } } // Insert .below constants via roundtrip_block. @@ -4345,7 +4619,7 @@ fn decompile_block_aux_gen( ) { Ok(roundtripped) => { for (n, ci) in roundtripped { - dstt.env.insert(n, ci); + dstt.insert_interned(n, ci); } }, Err(e) => { @@ -4446,7 +4720,7 @@ fn decompile_block_aux_gen( match roundtrip_block(&[mc], &generated_consts, orig_env, stt, dstt) { Ok(roundtripped) => { for (n, ci) in roundtripped { - dstt.env.insert(n, ci); + dstt.insert_interned(n, ci); } }, Err(e) => { @@ -4517,7 +4791,7 @@ fn decompile_block_aux_gen( ) { Ok(roundtripped) => { for (n, ci) in roundtripped { - dstt.env.insert(n, ci); + dstt.insert_interned(n, ci); } }, Err(e) => { @@ -4555,7 +4829,9 @@ fn decompile_block_aux_gen( if !env.contains_key(n) { env.insert(n.clone(), ci.clone()); } - dstt.env.entry(n.clone()).or_insert_with(|| ci.clone()); + if !dstt.env.contains_key(n) { + dstt.insert_interned(n.clone(), ci.clone()); + } } // Populate the ephemeral kenv with .below types so brecOn's TcScope @@ -4622,7 +4898,7 @@ fn decompile_block_aux_gen( match roundtrip_block(&[mc], &generated_consts, orig_env, stt, dstt) { Ok(roundtripped) if !roundtripped.is_empty() => { for (n, ci) in roundtripped { - dstt.env.insert(n, ci); + dstt.insert_interned(n, ci); } }, Ok(_) => { @@ -4632,7 +4908,7 @@ fn decompile_block_aux_gen( // `brecon_def_to_lean` applies the same kind/safety/hints // matrix that the compile path used. if !recover_aux_from_original(&d.name, stt, dstt) { - dstt.env.insert(d.name.clone(), brecon_def_to_lean(d)); + dstt.insert_interned(d.name.clone(), brecon_def_to_lean(d)); } }, Err(e) => { @@ -4641,7 +4917,7 @@ fn decompile_block_aux_gen( // post-preseed, the roundtrip is byte-exact corpus-wide, // so any error here is a regression. if !recover_aux_from_original(&d.name, stt, dstt) { - dstt.env.insert(d.name.clone(), brecon_def_to_lean(d)); + dstt.insert_interned(d.name.clone(), brecon_def_to_lean(d)); } aux_gen_errors.push((d.name.clone(), e)); }, @@ -4703,6 +4979,19 @@ pub fn decompile_env( let dstt = DecompileState::default(); + // Pre-pass: index every Muts-tagged Named entry in one parallel scan. + // Rehydration below and Pass 2's per-block call-site planning both + // read Muts metadata, which under the demoted repr costs a full + // decode per access — the index bounds that to one decode per entry. + let t_idx = std::time::Instant::now(); + let muts_index = build_muts_plan_index(stt); + eprintln!( + "[decompile] muts plan index built in {:.2}s ({} entries){}", + t_idx.elapsed().as_secs_f32(), + muts_index.entries.len(), + rss_log_suffix(), + ); + // Pre-pass: Rehydrate `stt.aux_perms` from persisted Muts metadata. // // When `stt` was freshly constructed from a deserialized Ixon env, @@ -4712,7 +5001,7 @@ pub fn decompile_env( // before Pass 2 runs aux_gen against the decompiled blocks. // // See `docs/ix_canonicity.md` §10.2 / §17.3. - rehydrate_aux_perms_from_env(stt); + rehydrate_aux_perms_from_env(stt, &muts_index); // Pass 1: Decompile all non-aux_gen constants (parallel). // Aux_gen constants (named.original.is_some() && is_aux_gen_suffix) are @@ -4727,9 +5016,10 @@ pub fn decompile_env( decompile_named_const(name, named, stt, &dstt) })?; eprintln!( - "[decompile] Pass 1 done in {:.2}s ({} constants in dstt.env)", + "[decompile] Pass 1 done in {:.2}s ({} constants in dstt.env){}", t_p1.elapsed().as_secs_f32(), dstt.env.len(), + rss_log_suffix(), ); // Pass 1.5: Lean-faithful inductive flags @@ -4842,9 +5132,11 @@ pub fn decompile_env( sorted }; eprintln!( - "[decompile] Pass 2 prep done in {:.2}s: {} aux_gen blocks to regenerate", + "[decompile] Pass 2 prep done in {:.2}s: {} aux_gen blocks to \ + regenerate{}", t_p2_prep.elapsed().as_secs_f32(), sorted_block_keys.len(), + rss_log_suffix(), ); // Shared kernel context for aux_gen (accumulates across blocks). @@ -4866,6 +5158,16 @@ pub fn decompile_env( // for every block (still O(n) across all blocks combined). let mut ingressed: FxHashSet = FxHashSet::default(); + // Size trigger for the kenv clear at the bottom of the block loop. + // A full clear makes later blocks re-walk their whole ingress + // closures, so the threshold must sit above the kenv working set of + // any env that fits in RAM comfortably — those runs must never clear + // (a threshold inside their working set trades a large Pass 2 wall + // regression for little memory). It exists as a backstop against + // unbounded growth on envs whose closure union would otherwise + // dominate decompile RSS. + const KENV_CLEAR_ENTRIES: usize = 65536; + // Progress tracking. Per-block progress logs (every `log_stride` blocks or // every 5 s) are opt-in via `IX_DECOMPILE_PROGRESS`; slow-block warnings // (any single block exceeding `slow_threshold`) are always emitted. @@ -4916,6 +5218,7 @@ pub fn decompile_env( &mut kctx, stt, &dstt, + &muts_index, ); aux_gen_errors.extend(errors); @@ -4959,18 +5262,37 @@ pub fn decompile_env( let pct = 100.0 * done as f32 / total_blocks as f32; eprintln!( "[decompile] Pass 2 progress: {done}/{total_blocks} blocks \ - ({pct:.1}%), elapsed {elapsed:.1}s, eta {remaining}s, kenv={}", + ({pct:.1}%), elapsed {elapsed:.1}s, eta {remaining}s, kenv={}{}", ingressed.len(), + rss_log_suffix(), ); t_last_log = now; } } + + // Bounded kenv growth: the kenv is a pure cache (`ensure_in_kenv_of` + // re-ingresses on demand and aux_gen re-ensures the prelude), so + // clearing at block boundaries is semantics-free. Unbounded, it + // grows to the union of every block's ingress closure. + // + // Unlike the compile scheduler's per-worker count cadence + // (`KENV_CLEAR_EVERY`), this kenv is shared across all blocks and a + // clear forces the next blocks to re-walk their full transitive + // closures. Trigger on size instead: envs whose closures stay under + // the threshold never clear (and pay nothing); larger envs trade a + // few re-ingress walks for a bounded working set. + if ingressed.len() > KENV_CLEAR_ENTRIES { + kctx.kenv.clear_releasing_memory(); + ingressed.clear(); + expr_utils::ensure_prelude_in_kenv_of(stt, &mut kctx); + } } eprintln!( - "[decompile] Pass 2 done in {:.2}s ({} aux_gen errors, kenv={})", + "[decompile] Pass 2 done in {:.2}s ({} aux_gen errors, kenv={}){}", t_p2.elapsed().as_secs_f32(), aux_gen_errors.len(), ingressed.len(), + rss_log_suffix(), ); if !aux_gen_errors.is_empty() { @@ -4983,6 +5305,11 @@ pub fn decompile_env( } } + // The intern table's job is done — `dstt.env` keeps the canonical + // `Arc`s alive, and consumers only read `env`. + let mut dstt = dstt; + dstt.expr_intern = DashMap::new(); + Ok(dstt) } diff --git a/crates/ffi/src/compile.rs b/crates/ffi/src/compile.rs index f3a9234e5..f2765110a 100644 --- a/crates/ffi/src/compile.rs +++ b/crates/ffi/src/compile.rs @@ -3,7 +3,7 @@ //! Provides `extern "C"` functions callable from Lean via `@[extern]`: //! - `rs_compile_env` / `rs_compile_env_full`: compile a Lean environment to Ixon //! - `rs_compile_phases`: run individual pipeline phases (canon, condense, graph, compile) -//! - `rs_decompile_env`: decompile Ixon back to Lean environment +//! - `rs_decompile_env`: decompile a serialized `.ixe` env back to Lean constants //! - `rs_roundtrip_*`: roundtrip FFI tests for Lean↔Rust type conversions //! - `build_*` / `decode_*`: convert between Lean constructor layouts and Rust types @@ -11,9 +11,9 @@ use std::sync::Arc; use crate::lean::{ LeanIxBlock, LeanIxCompileError, LeanIxCompilePhases, LeanIxCondensedBlocks, - LeanIxConstantInfo, LeanIxDecompileError, LeanIxName, LeanIxRawEnvironment, - LeanIxSerializeError, LeanIxonRawBlob, LeanIxonRawComm, LeanIxonRawConst, - LeanIxonRawEnv, LeanIxonRawNameEntry, LeanIxonRawNamed, + LeanIxDecompileError, LeanIxName, LeanIxRawEnvironment, LeanIxSerializeError, + LeanIxonRawBlob, LeanIxonRawComm, LeanIxonRawConst, LeanIxonRawEnv, + LeanIxonRawNameEntry, LeanIxonRawNamed, }; use ix_common::address::Address; use ix_common::env::Name; @@ -32,13 +32,12 @@ use ixon::{Comm, ConstantMeta}; use lean_ffi::object::LeanIOResult; use lean_ffi::object::LeanNat; use lean_ffi::object::{ - LeanArray, LeanBorrowed, LeanByteArray, LeanExcept, LeanList, LeanOwned, - LeanProd, LeanRef, LeanString, + LeanArray, LeanBorrowed, LeanByteArray, LeanList, LeanOwned, LeanProd, + LeanRef, LeanString, }; use crate::builder::LeanBuildCache; use crate::lean::LeanIxAddress; -use crate::lean_ixon::env::decoded_to_ixon_env; #[cfg(feature = "test-ffi")] use crate::lean::{LeanIxBlockCompareDetail, LeanIxBlockCompareResult}; @@ -1482,32 +1481,92 @@ pub extern "C" fn rs_roundtrip_serialize_error( // Decompilation FFI // ============================================================================= -/// FFI: Decompile an Ixon.RawEnv → Except DecompileError (Array (Ix.Name × Ix.ConstantInfo)). Pure. +/// FFI: decompile a serialized `.ixe` env from disk — the inverse of +/// `rs_compile_env` — returning the decompiled constant count. +/// +/// A `decompile_env` failure (malformed output) is a hard error, +/// returned as an IO error so the caller reddens the cell. Timing and +/// peak-RSS are measured by the Lean caller around this call, with the +/// same texray infrastructure `ix compile --json` uses. Deeper +/// compile→decompile roundtrip fidelity is gated by the canonical +/// roundtrip tests (`ix validate` / `rs_decompile_roundtrip`), which +/// need the original Lean env a `.ixe` can't supply — the bench does +/// not reproduce them here. +/// +/// Lean signature: +/// ```lean +/// @[extern "rs_decompile_env"] +/// opaque rsDecompileEnvFFI : @& String → IO Nat +/// ``` #[unsafe(no_mangle)] pub extern "C" fn rs_decompile_env( - raw_env_obj: LeanIxonRawEnv, -) -> LeanExcept { - let decoded = raw_env_obj.decode(); - let env = decoded_to_ixon_env(&decoded); + path: LeanString>, +) -> LeanIOResult { + let path = path.as_str().to_string(); - // Wrap in CompileState (decompile_env only uses .env) - let stt = CompileState { env, ..CompileState::default() }; + let bytes = match std::fs::read(&path) { + Ok(b) => b, + Err(e) => { + return LeanIOResult::error_string(&format!( + "rs_decompile_env: failed to read {path}: {e}" + )); + }, + }; + // Demoted-at-parse load: decompile reads each entry's metadata a + // bounded number of times, and the whole named section's structured + // form costs a large multiple of its encoding — enough to dominate + // the decompile's peak RSS on the biggest envs. One load path at + // every scale also keeps the bench rows comparable across envs. + let mut slice: &[u8] = &bytes; + let env = match ixon::env::Env::get_demoted_named(&mut slice) { + Ok(env) => env, + Err(e) => { + return LeanIOResult::error_string(&format!( + "rs_decompile_env: failed to deserialize {path}: {e}" + )); + }, + }; - match decompile_env(&stt) { - Ok(dstt) => { - let entries: Vec<_> = dstt.env.into_iter().collect(); - let mut cache = LeanBuildCache::with_capacity(entries.len()); - - let arr = LeanArray::alloc(entries.len()); - for (i, (name, info)) in entries.iter().enumerate() { - let name_obj = LeanIxName::build(&mut cache, name); - let info_obj = LeanIxConstantInfo::build(&mut cache, info); - let pair = LeanProd::new(name_obj, info_obj); - arr.set(i, pair); - } + // The env owns its bytes after parsing; release the file buffer + // before the decompile allocates next to it. + drop(bytes); + + // Decompile needs every reachable constant carried: a thin bundle + // deliberately omits its assumed subtrees, and a bundle with a broken + // closure would otherwise surface deep inside the decompile as a + // confusing per-constant error. Whole envs (`main = None`) carry + // everything by construction and skip the closure walk. + if !env.assumptions.is_empty() { + return LeanIOResult::error_string(&format!( + "rs_decompile_env: {path} is a thin bundle ({} assumptions); \ + decompile needs a self-contained env", + env.assumptions.len() + )); + } + if env.main.is_some() + && let Err(e) = env.validate_closed() + { + return LeanIOResult::error_string(&format!( + "rs_decompile_env: {path}: {e}" + )); + } - LeanExcept::ok(arr) - }, - Err(e) => LeanExcept::error(LeanIxDecompileError::build(&e)), + // decompile_env reads only `stt.env`; Pass 2 (aux_gen regeneration) + // reconstructs the block structure from the env itself — + // `name_to_addr` so aux_gen resolves addresses for the names it + // regenerates (mirroring `rs_compile_validate_aux`'s Phase 7 setup). + let stt = CompileState { env, ..CompileState::default() }; + for entry in stt.env.named.iter() { + stt.name_to_addr.insert(entry.key().clone(), entry.value().addr.clone()); } + + let dstt = match decompile_env(&stt) { + Ok(d) => d, + Err(e) => { + return LeanIOResult::error_string(&format!( + "rs_decompile_env: decompile of {path} failed: {e:?}" + )); + }, + }; + LeanIOResult::ok(LeanOwned::from_nat_u64(dstt.env.len() as u64)) } diff --git a/crates/ffi/src/kernel.rs b/crates/ffi/src/kernel.rs index 41c1dbade..462aa4008 100644 --- a/crates/ffi/src/kernel.rs +++ b/crates/ffi/src/kernel.rs @@ -447,10 +447,14 @@ fn poison_second_rec_rule_returns_first_minor( let mut rec_constant: ixon::constant::Constant = (*rec_arc).clone(); drop(rec_arc); + // The stores below must use `store_const_demoted(.., false)`: + // `store_const` under `DEMOTE` treats a re-store of an existing address + // as a no-op (content addressing assumes identical bytes), and this + // helper deliberately stores *different* bytes at the original address. match &mut rec_constant.info { IxonCI::Recr(rec) => { poison_recursor_rule_payload(rec)?; - ixon_env.store_const(rec_addr.clone(), rec_constant); + ixon_env.store_const_demoted(rec_addr.clone(), rec_constant, false); Ok(rec_addr) }, IxonCI::Muts(members) => { @@ -468,7 +472,7 @@ fn poison_second_rec_rule_returns_first_minor( rec_name.pretty() )); } - ixon_env.store_const(rec_addr.clone(), rec_constant); + ixon_env.store_const_demoted(rec_addr.clone(), rec_constant, false); Ok(rec_addr) }, IxonCI::RPrj(proj) => { @@ -515,7 +519,7 @@ fn poison_second_rec_rule_returns_first_minor( )); }, } - ixon_env.store_const(block_addr, block_constant); + ixon_env.store_const_demoted(block_addr, block_constant, false); Ok(rec_addr) }, other => Err(format!( @@ -3522,6 +3526,97 @@ fn build_uniform_error(count: usize, msg: &str) -> LeanIOResult { // `decompile_env`, which the production CLI path (`rs_kernel_check_consts`) // doesn't need. Cfg-gating keeps `lake build ix` (no `test-ffi`) lean. +/// FFI: exercise the serialized decompile pipeline +/// Lean → compile → serialize → deserialize → decompile → Lean, and +/// compare each constant against the original. This is `ix decompile`'s +/// path (an in-memory `.ixe`): the demoted-at-parse metadata load, the +/// `Named.original` recovery for shape-divergent aux blocks, and +/// expression interning — without the kernel ingress/egress leg +/// [`rs_kernel_roundtrip`] adds. +/// +/// Lean signature: +/// ```lean +/// @[extern "rs_decompile_roundtrip"] +/// opaque rsDecompileRoundtripFFI : +/// @& List (Lean.Name × Lean.ConstantInfo) → IO (Array String) +/// ``` +/// Returns an `Array String` of per-constant diff messages. Empty = pass. +#[cfg(feature = "test-ffi")] +#[unsafe(no_mangle)] +pub extern "C" fn rs_decompile_roundtrip( + env_consts: LeanList>, +) -> LeanIOResult { + let total_start = Instant::now(); + + let t0 = Instant::now(); + let rust_env = decode_env(env_consts); + eprintln!("[rs_decompile_roundtrip] read env: {:>8.1?}", t0.elapsed()); + + let t1 = Instant::now(); + let rust_env_arc = Arc::new(rust_env); + let compile_state = + match compile_env_with_options(&rust_env_arc, CompileOptions::default()) { + Ok(s) => s, + Err(e) => { + return build_string_array(&[format!("compile error: {e:?}")]); + }, + }; + eprintln!("[rs_decompile_roundtrip] compile: {:>8.1?}", t1.elapsed()); + + let t2 = Instant::now(); + let mut bytes = Vec::new(); + if let Err(e) = compile_state.env.put(&mut bytes) { + return build_string_array(&[format!("serialize error: {e}")]); + } + drop(compile_state); + let mut slice: &[u8] = &bytes; + let env = match ixon::env::Env::get_demoted_named(&mut slice) { + Ok(env) => env, + Err(e) => { + return build_string_array(&[format!("deserialize error: {e}")]); + }, + }; + eprintln!( + "[rs_decompile_roundtrip] serialize: {:>8.1?} ({} bytes)", + t2.elapsed(), + bytes.len() + ); + drop(bytes); + + let stt = CompileState { env, ..CompileState::default() }; + for entry in stt.env.named.iter() { + stt.name_to_addr.insert(entry.key().clone(), entry.value().addr.clone()); + } + + let t3 = Instant::now(); + let dstt = match decompile_env(&stt) { + Ok(d) => d, + Err(e) => { + return build_string_array(&[format!("decompile error: {e:?}")]); + }, + }; + eprintln!( + "[rs_decompile_roundtrip] decompile: {:>8.1?} ({} consts)", + t3.elapsed(), + dstt.env.len() + ); + + let t4 = Instant::now(); + let (errors, checked, not_found) = + compare_envs(&rust_env_arc, |n| dstt.env.get(n)); + eprintln!( + "[rs_decompile_roundtrip] verify: {:>8.1?} (checked {checked}, not_found {not_found}, errors {})", + t4.elapsed(), + errors.len() + ); + eprintln!( + "[rs_decompile_roundtrip] total: {:>8.1?}", + total_start.elapsed() + ); + + build_string_array(&errors) +} + /// FFI: exercise the full pipeline /// Lean → Ixon → kernel → Ixon' → decompile → Lean, and compare each /// constant against the original. @@ -3612,23 +3707,12 @@ pub extern "C" fn rs_kernel_roundtrip( dstt.env.len() ); - // Build a plain Lean `Env` from decompile's DashMap for the standard - // compare_envs / find_diff flow. - let t5 = Instant::now(); - let mut decompiled_env = ix_common::env::Env::default(); - for entry in dstt.env.iter() { - decompiled_env.insert(entry.key().clone(), entry.value().clone()); - } - eprintln!( - "[rs_kernel_roundtrip] build lean env:{:>8.1?} ({} consts)", - t5.elapsed(), - decompiled_env.len() - ); - - // Compare decompiled env against original, content-hash by content-hash. + // Compare decompiled env against original, content-hash by + // content-hash, reading decompile's DashMap directly — a plain-`Env` + // copy of it would double the resident decompiled env at peak. let t6 = Instant::now(); let (errors, checked, not_found) = - compare_envs(&rust_env_arc, &decompiled_env); + compare_envs(&rust_env_arc, |n| dstt.env.get(n)); eprintln!( "[rs_kernel_roundtrip] verify: {:>8.1?} (checked {checked}, not_found {not_found}, errors {})", t6.elapsed(), @@ -3646,13 +3730,18 @@ pub extern "C" fn rs_kernel_roundtrip( build_string_array(&errors) } -/// Compare two envs for structural equality under content-hashing. Returns +/// Compare the original env against a decompiled/egressed side for +/// structural equality under content-hashing. Returns /// `(errors, checked, not_found)`. `errors` is capped at 50 to keep outputs /// manageable. +/// +/// The compared side is a lookup rather than an `Env` so callers can pass +/// whatever map already holds their constants (e.g. decompile's DashMap) +/// instead of copying into a fresh `Env`. #[cfg(feature = "test-ffi")] -fn compare_envs( +fn compare_envs>( original: &ix_common::env::Env, - egressed: &ix_common::env::Env, + lookup: impl Fn(&Name) -> Option, ) -> (Vec, usize, usize) { use ix_common::env::ConstantInfo as LCI; @@ -3662,7 +3751,7 @@ fn compare_envs( let mut not_found = 0usize; for (name, orig_ci) in original.iter() { - match egressed.get(name) { + match lookup(name) { None => { not_found += 1; }, @@ -3711,7 +3800,7 @@ fn compare_envs( } if checked.is_multiple_of(10000) && checked > 0 { eprintln!( - "[rs_kernel_roundtrip] verify: {checked}/{total} ({} errors so far)", + "[compare_envs] verify: {checked}/{total} ({} errors so far)", errors.len() ); } @@ -3935,7 +4024,8 @@ pub extern "C" fn rs_kernel_roundtrip_no_compile( // Compare. let t3 = Instant::now(); - let (errors, checked, not_found) = compare_envs(&rust_env_arc, &egressed_env); + let (errors, checked, not_found) = + compare_envs(&rust_env_arc, |n| egressed_env.get(n)); eprintln!( "[rs_kernel_roundtrip_no_compile] verify: {:>8.1?} (checked {checked}, not_found {not_found}, errors {})", t3.elapsed(), diff --git a/crates/ffi/src/lean_env.rs b/crates/ffi/src/lean_env.rs index a053ee737..a1e78d96a 100644 --- a/crates/ffi/src/lean_env.rs +++ b/crates/ffi/src/lean_env.rs @@ -1773,11 +1773,18 @@ struct PhaseResult { pass: usize, fail: usize, failures: Vec, + started: std::time::Instant, } impl PhaseResult { fn new(name: &'static str) -> Self { - PhaseResult { name, pass: 0, fail: 0, failures: Vec::new() } + PhaseResult { + name, + pass: 0, + fail: 0, + failures: Vec::new(), + started: std::time::Instant::now(), + } } fn record_pass(&mut self) { @@ -1792,7 +1799,11 @@ impl PhaseResult { } fn report(&self) { - println!("{VALIDATE_PREFIX} Phase: {}", self.name); + println!( + "{VALIDATE_PREFIX} Phase: {} ({:.1?})", + self.name, + self.started.elapsed(), + ); println!("{VALIDATE_PREFIX} {} pass, {} fail", self.pass, self.fail); for f in &self.failures { println!("{VALIDATE_PREFIX} ✗ {f}"); @@ -1821,8 +1832,14 @@ extern "C" fn rs_compile_validate_aux( let t_total = std::time::Instant::now(); // ── Decode ────────────────────────────────────────────────────────── + // Same on-demand view as the compile CLI, with the same escape + // hatch: the eager Rust copy of the Lean env is the single largest + // term of the run's baseline RSS and stays resident through every + // phase, while the lazy view's re-decode cost is bounded by the + // shared cache. `IX_COMPILE_EAGER=1` restores the eager copy for + // machines with RAM to spare. println!("{VALIDATE_PREFIX} decoding..."); - let env = decode_env(obj); + let env = decode_env_for_compile(obj); let n = env.len(); println!("{VALIDATE_PREFIX} decoded {n} constants"); let env = Arc::new(env); @@ -3747,10 +3764,14 @@ extern "C" fn rs_compile_validate_aux( let t3 = std::time::Instant::now(); let dstt2 = { // Deserialize inside a short sub-scope so the borrow on `serialized` - // ends before we drop it. + // ends before we drop it. Metadata is stored demoted as it parses: + // the whole named section's structured form costs a large multiple + // of its encoding and would sit resident through the re-decompile, + // while decompile reads each entry's metadata a bounded number of + // times. let fresh_env = { let mut buf: &[u8] = &serialized; - match ixon::env::Env::get(&mut buf) { + match ixon::env::Env::get_demoted_named(&mut buf) { Ok(fe) => Some(fe), Err(e) => { p7.record_fail(format!("deserialize FAILED: {e}")); diff --git a/crates/ixon/src/serialize.rs b/crates/ixon/src/serialize.rs index e4981eeaf..15f872216 100644 --- a/crates/ixon/src/serialize.rs +++ b/crates/ixon/src/serialize.rs @@ -1735,6 +1735,20 @@ impl Env { /// `parse_lazy_index` enforces the same; the early-stop readers /// (`get_anon`, `get_anon_mmap`) cannot make that check by design. pub fn get(buf: &mut &[u8]) -> Result { + Self::get_inner(buf, false) + } + + /// [`Self::get`], storing each `Named`'s metadata in the demoted + /// (serialized-bytes) repr as it is parsed. The structured metadata + /// for a whole env costs a large multiple of its encoding, so + /// consumers that read metadata a bounded number of times per entry + /// (decompile) use this to keep the structured residency to one + /// entry at a time instead of the whole named section. + pub fn get_demoted_named(buf: &mut &[u8]) -> Result { + Self::get_inner(buf, true) + } + + fn get_inner(buf: &mut &[u8], demote_named: bool) -> Result { // Header: tag + stored merkle root (verified at the end against // the recomputed root; empty const sets store `zero_address()`) + // bundle fields. @@ -1818,7 +1832,10 @@ impl Env { let num_named = get_u64(buf)?; for _ in 0..num_named { let name_addr = get_address(buf)?; - let named = get_named_indexed(buf, &name_reverse_index)?; + let mut named = get_named_indexed(buf, &name_reverse_index)?; + if demote_named { + named.demote(); + } let name = names_lookup.get(&name_addr).cloned().ok_or_else(|| { format!("Env::get: missing name for addr {:?}", name_addr) })?; diff --git a/docs/benchmarking.md b/docs/benchmarking.md index 5e9bd042d..515f4cd34 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -102,6 +102,7 @@ a PR tree and compare them — exactly what the PR workflow does. | `sp1` | SP1 VM execute (currently disabled in the registry) | `sp1-host` | | `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per primary (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` | | `compile` | `ix compile .lean → .ixe`: 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` | All tools emit the same rows, and all the constant-driven ones take the same `--consts`/`--consts-file` grammar (`bench-recursive-verifier` instead takes @@ -166,8 +167,8 @@ breakdowns. bench-main's compile job pre-cuts these artifacts ## `!benchmark` grammar ``` -!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute] - [KEY=VALUE …] +!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) + [execute] [KEY=VALUE …] BENCH_ENVS=InitStd,Mathlib # default InitStd (case-insensitive); a # compile-only request may name any registry # env (Lean, FLT compile fine, just unbenched)