Skip to content

perf: decompile Pass-2 restructure + compile hot-path batch (post-#572 perf pass) - #579

Merged
johnchandlerburnham merged 3 commits into
mainfrom
jcb/perf-optimization
Aug 20, 2026
Merged

perf: decompile Pass-2 restructure + compile hot-path batch (post-#572 perf pass)#579
johnchandlerburnham merged 3 commits into
mainfrom
jcb/perf-optimization

Conversation

@johnchandlerburnham

@johnchandlerburnham johnchandlerburnham commented Aug 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Performance pass over the decompile and compile pipelines, following up on the post-#572 benchmark reports (FLT decompile +114% time / +110% RAM was the headline regression). Three commits on main (post-#578): thin LTO, Rust-side phase/RSS instrumentation, and the algorithmic batch. Serialized bytes are unchanged everywhere — verified end-to-end at Mathlib scale (see Validation).

Headline numbers (Mathlib, 736,624 consts, 32-core / 124 GiB box)

Decompile (ix decompile compilemathlib.ixe, CI-comparable: local baseline 151.2 s ≈ CI's 152.5 s row):

before after Δ
Pass 2 ingress 18.8 s 6.0 s −68 %
Pass 2 gen 75.9 s 62.2 s −18 %
wall total 151.2 s 120.9 s −20 %
peak RSS 34.8 GiB 30.5 GiB −4.3 GiB
constrained run (65536-entry clear knob, 7 clears) 228.0 s 136.1 s −40 %
cost per kenv clear ~10 s ~1.9 s −81 %

The constrained row is the FLT mechanism reproduced locally: FLT's dependency closure crosses the old default kenv-clear threshold, so its CI row was paying a full closure re-walk on every clear. That cliff is now flattened three ways (a clear-surviving refs memo + cheap re-ensure + a threshold FLT never reaches), so the FLT row should recover most of the regression plus RAM.

Compile (ix compile CompileMathlib.lean, A/B on this branch's base vs tip, byte-identical outputs):

base perf Δ
setup_scan 11.1 s 9.2 s −17 %
scheduler 32.8 s 30.0 s −8.5 %
compile+serialize+write 59.5 s 55.0 s −7.6 %

What changed

Decompile Pass 2

  • get_constant_info_references rewritten as a single-accumulator iterative DAG walk (visited set keyed on Expr's digest-backed Hash/Eq) instead of materializing+merging+cloning a NameSet per expression node. Feeds both compile's setup_scan and decompile's Pass-2 ingress BFS. Result sets are value-identical; no consumer reads set iteration order into bytes (SCC members and every serialized section re-sort canonically).
  • Ingress BFS refs memo survives kenv clears: the BFS's ingressed set doubles as the kenv-content tracker, so the periodic kenv clear wiped the only BFS memo and every clear re-walked the whole closure — a Θ(N²/L) term, and the mechanism behind FLT's +114 %. The discovered reference lists now survive clears (the reference graph doesn't change when the kenv does); names absent from work_env stay unmemoized so late-appearing aux constants are re-probed live.
  • Aux ingress walker dedup moves into KernelCtx: ingress_target_type_deps / ingress_field_deps kept a per-call seen, re-expanding the full reference closure for every block (Θ(blocks × closure)). The set is now kenv-lifetime (aux_ingress_seen), keyed by resolved id — not bare name — so an address shifted by later aux registration reads as unseen and re-ingresses under the new id, exactly as the per-call sets healed it. Fresh-per-block in compile (§10.5 unchanged); cleared with the kenv in decompile. collect_const_refs additionally gains a digest-keyed visited set (shared subterms walked once, not once per occurrence). Measured: Pass-2 gen −18 %.
  • Pre-warm ingests proofs as type-only stubs: the Pass-2 BFS ingested theorem/opaque constants with full proof terms (~47 KB/name measured) while the gen-phase walkers deliberately use type-only stubs for the same kinds. The new ensure_in_kenv_of_prewarm ingests thm/opaque as type-only Axio stubs — sufficient for kernel TC (proof irrelevance; opaque never unfolds) and the exact fidelity ingress_type_stub already gives. With per-entry kenv cost collapsed, the clear default rises 131072 → 1048576 and becomes a rare backstop; the IX_DECOMPILE_KENV_CLEAR_ENTRIES knob semantics are unchanged. Validated by a full-Mathlib decompile with 0 aux_gen errors across 6,598 regenerated blocks (plus the congruence checks).
  • Free wins: lean_env (a third whole-env copy) drops after Pass 1.5 instead of living to end of decompile_env; rs_decompile_env skips the ~30 GiB destructor churn on exit (one-shot CLI, mirroring rs_compile_env) and reports read/parse spans — the pre-Pass-1 .ixe parse is ~37 s of the wall and is now visible (largest remaining chunk; future target).

Lean mirrors land in the same commit: AuxKernelCtx.auxIngressSeen + drainIngressQueue + collectConstRefs visited set + ensureInKenvOfPrewarm wired into both Pass-2 driver variants (Ix/AuxGen/Kernel.lean, Ix/AuxGen/Recursor.lean, Ix/DecompileDriver.lean).

Compile

  • Digest-keyed maps drop SipHash: every blake3-digest-keyed map in ixon/sharing.rs moves from std::HashMap to FxHashMap (keys are already uniform digests; every order-sensitive consumer re-sorts).
  • Merkle root computed once, in parallel: new host-only merkle_root_canonical_sorted (parallel leaf/level hashing for callers holding sorted unique leaves, bit-identical root). rs_compile_env computes the const table + root once and hands both to the new put_file_with_header; previously the par-sort and the ~2·N-node tree ran twice per compile.
  • Block-context addresses hoisted: compile_definition/inductive/recursor take the block-context address list as a parameter, computed once per block (was: full ctx sort + re-intern per member, O(M² log M) per block).
  • Metadata moves instead of cloning: mutual-path ConstantMeta moves out of all_metas via remove instead of two deep clones per constant.
  • Instrumentation: IX_COMPILE_DBG=1 now lights the Rust side too (scheduler phases with RSS attribution, Env::put_file per-section timers — the §4 serial name topo-sort is timed separately and shows 1.9 s at Mathlib scale, the next serializer target).
  • Thin LTO on the release profile (no embedded guest builds in this workspace; external guest builds use their own profiles).

Validation

  • Whole-Mathlib byte identity: ix compile of CompileMathlib.lean on this branch's pre-perf base vs tip → cmp identical (3,326,436,547 bytes).
  • Whole-Mathlib decompile: 0 aux_gen errors, 0 congruence failures (default and constrained-knob runs).
  • --ignored parity gates: validate-aux (3,699 matches / 0 mismatches), aux-gen-diff (plain-defn mismatches 0), decompile-diff (plain fidelity + callsite replay PASS; Pass-2 plan parity 300/300; aux-fidelity PASS) — these cover the Lean mirror changes.
  • cargo test --workspace --release: 1,256 passed / 0 failed (incl. put_file_matches_put for the put_file_with_header split).
  • lake test: 2,668 checks, exit 0.
  • cargo clippy --workspace --release --all-targets clean; cargo fmt --check clean.

Explicitly not touched

Fresh-per-block KernelCtx in the compile scheduler (§10.5 determinism), wire format (no Env::VERSION change), DEMOTE/EAGER defaults, and the Lean drivers' performance (mirrors are behavior-parity only, per BENCHMARKS.md ground rules).

Follow-up targets surfaced by the new instrumentation (measured, not yet done): the ~37 s decompile pre-phase (.ixe parse — per-member Muts block re-parsing lives there), the §4 name topo-sort in the serializer (1.9 s serial), and the prove-side items from the benchmark digest (targeted hint-row promotion, FFT pin re-baseline, sequencing the two ixvm test envs).

@johnchandlerburnham
perf: enable thin LTO for release builds
440fe50 
Cross-crate inlining across the ixon/compile/ffi boundary — the hot
loops (blake3 digests, subterm sharing, serialization) span crates.
Byte-output invariant: codegen-only change.
@johnchandlerburnham

johnchandlerburnham commented Aug 20, 2026

Copy link
Copy Markdown
Member Author

!benchmark compile decompile

@johnchandlerburnham

johnchandlerburnham commented Aug 20, 2026

Copy link
Copy Markdown
Member Author

!benchmark ooc

@johnchandlerburnham

johnchandlerburnham commented Aug 20, 2026

Copy link
Copy Markdown
Member Author

!benchmark aiur

arthurpaulino
arthurpaulino reviewed Aug 20, 2026
View reviewed changes
Comment thread Ix/Aiur/Statistics.lean Outdated
@argument-ci-bot

argument-ci-bot Bot commented Aug 20, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 7db0341

backends: compile decompile · envs: InitStd,Lean,Mathlib,FLT · set: primary · shard: 0

compile · FLT — main from: base run @ 7918b0c (not on bencher)

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

env compile-time (main) compile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
FLT 57.028 s 46.357 s -18.7% (1.23× faster) 🟢 13.69K 16.85K +23.0% (1.23× faster) 🟢 20.71 GiB 19.90 GiB -3.9% 🟢 3.20 GiB 3.20 GiB +0.0% 780,906 780,906 +0.0%

compile · InitStd — main from: base run @ 7918b0c (not on bencher)

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

env compile-time (main) compile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd 4.294 s 3.743 s -12.8% (1.15× faster) 🟢 27.27K 31.28K +14.7% (1.15× faster) 🟢 3.92 GiB 4.00 GiB +2.0% 324.65 MiB 324.65 MiB +0.0% 117,084 117,084 +0.0%

compile · Lean — main from: base run @ 7918b0c (not on bencher)

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

env compile-time (main) compile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
Lean 8.582 s 7.385 s -13.9% (1.16× faster) 🟢 24.08K 27.98K +16.2% (1.16× faster) 🟢 5.43 GiB 5.39 GiB -0.8% 481.18 MiB 481.18 MiB +0.0% 206,647 206,647 +0.0%

compile · Mathlib — main from: base run @ 7918b0c (not on bencher)

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

env compile-time (main) compile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
Mathlib 56.256 s 43.614 s -22.5% (1.29× faster) 🟢 13.71K 17.68K +29.0% (1.29× faster) 🟢 18.98 GiB 19.29 GiB +1.7% 3.10 GiB 3.10 GiB +0.0% 771,129 771,129 +0.0%

decompile · FLT — main from: base run @ 7918b0c (not on bencher)

1 constant · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

constant decompile-time (main) decompile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
FLT 2m 33.4s 1m 56.7s -23.9% (1.31× faster) 🟢 5.09K 6.69K +31.4% (1.31× faster) 🟢 39.55 GiB 33.55 GiB -15.2% (1.18× smaller) 🟢 3.20 GiB 3.20 GiB +0.0% 780,906 780,906 +0.0%

decompile · InitStd — main from: base run @ 7918b0c (not on bencher)

1 constant · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

constant decompile-time (main) decompile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
InitStd 6.327 s 4.335 s -31.5% (1.46× faster) 🟢 18.51K 27.01K +46.0% (1.46× faster) 🟢 4.21 GiB 3.79 GiB -10.1% (1.11× smaller) 🟢 324.65 MiB 324.65 MiB +0.0% 117,084 117,084 +0.0%

decompile · Lean — main from: base run @ 7918b0c (not on bencher)

1 constant · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

constant decompile-time (main) decompile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
Lean 13.423 s 9.511 s -29.1% (1.41× faster) 🟢 15.39K 21.73K +41.1% (1.41× faster) 🟢 5.44 GiB 5.00 GiB -8.2% (1.09× smaller) 🟢 481.18 MiB 481.18 MiB +0.0% 206,647 206,647 +0.0%

decompile · Mathlib — main from: base run @ 7918b0c (not on bencher)

1 constant · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

constant decompile-time (main) decompile-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% env-size (main) env-size (PR) Δ% constants (main) constants (PR) Δ%
Mathlib 2m 20.5s 1m 46.7s -24.0% (1.32× faster) 🟢 5.49K 7.22K +31.6% (1.32× faster) 🟢 38.06 GiB 32.27 GiB -15.2% (1.18× smaller) 🟢 3.10 GiB 3.10 GiB +0.0% 771,129 771,129 +0.0%

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Aug 20, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 7db0341

backends: ooc · envs: InitStd · set: primary · shard: 0

ooc · InitStd — main from: base run @ 7918b0c (not on bencher)

15 env/constants · 6 with regressions · 4 with improvements (|Δ| > 3.0% on any metric).

comparison table (15 env/constants)
env/constant check-time (main) check-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
InitStd 7.250 s 7.268 s +0.2% 13.63K 13.59K -0.2% 2.35 GiB 2.35 GiB -0.4%
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual 3.407 s 3.406 s -0.0% 1.82K 1.82K +0.0% 2.24 GiB 2.32 GiB +4.0% ⚠️
Array.extract_append 517.4 ms 517.2 ms -0.0% 3.12K 3.12K +0.0% 1.27 GiB 1.20 GiB -5.7% (1.06× smaller) 🟢
Vector.extract_append._proof_2 512.6 ms 512.5 ms -0.0% 2.66K 2.66K +0.0% 1.60 GiB 1.56 GiB -2.7%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 280.0 ms 279.3 ms -0.2% 9.93K 9.96K +0.2% 1.22 GiB 1.25 GiB +3.1% ⚠️
Char.ofOrdinal_le_of_le 274.1 ms 273.9 ms -0.1% 10.13K 10.14K +0.1% 1.53 GiB 1.60 GiB +4.8% ⚠️
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 264.7 ms 264.7 ms -0.0% 7.07K 7.08K +0.0% 1.64 GiB 1.77 GiB +7.6% (1.08× larger) ⚠️
String.split 264.0 ms 264.1 ms +0.0% 6.95K 6.94K -0.0% 1.37 GiB 1.28 GiB -6.5% (1.07× smaller) 🟢
List.mergeSort 261.7 ms 261.7 ms +0.0% 5.79K 5.79K -0.0% 1.04 GiB 1011.56 MiB -4.7% 🟢
Nat.gcd_comm 254.4 ms 254.9 ms +0.2% 1.65K 1.64K -0.2% 907.60 MiB 962.73 MiB +6.1% (1.06× larger) ⚠️
Vector.append 254.6 ms 254.7 ms +0.0% 2.10K 2.10K -0.0% 787.81 MiB 807.54 MiB +2.5%
String.append 253.3 ms 253.4 ms +0.0% 1.30K 1.30K -0.0% 1.28 GiB 1.35 GiB +6.0% (1.06× larger) ⚠️
Nat.sub_le_of_le_add 252.9 ms 253.2 ms +0.1% 727.680 726.750 -0.1% 658.41 MiB 642.10 MiB -2.5%
Int.gcd 252.6 ms 252.6 ms +0.0% 882.860 882.790 -0.0% 760.47 MiB 764.31 MiB +0.5%
Nat.add_comm 252.2 ms 252.3 ms +0.1% 182.410 182.300 -0.1% 520.78 MiB 500.57 MiB -3.9% 🟢
per-constant drill-down — Σ check 202.06s → 204.76s (+1.3%), Σ cost -0.0%; 0 cost mover(s), 52 time-only mover(s)

Each entry is one constant's own check within the whole-env run (deps ingress lazily; each dep is checked in its own entry; entries sum to the env) — not the full-closure scope of the headline --consts measurements.

Time-only movers (cost flat — scheduling/locality noise)

constant main PR Δtime Δcost (Zisk) driver
Std.DTreeMap.Internal.Impl.SizedBalancedTree.mk.noConfusion 0.9ms 15ms +1584.8% (16.85× slower) ⚠️ +0.0% —
Lean.Grind.CommRing.Poly.addConst.go.induct_unfolding 1.0ms 13ms +1148.8% (12.49× slower) ⚠️ +0.0% —
Std.Internal.List.minKey?_eraseKey_eq_of_beq_minKey?_eq_false 2.0ms 21ms +951.1% (10.51× slower) ⚠️ +0.0% —
Std.DTreeMap.Internal.Impl.Const.Equiv.beq_congr 2.2ms 23ms +940.3% (10.40× slower) ⚠️ +0.0% —
Std.TreeMap.Raw.getElem!_union_of_not_mem_right 1.3ms 13ms +937.5% (10.38× slower) ⚠️ +0.0% —

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Aug 20, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 7db0341

backends: aiur=prove · envs: InitStd · set: primary · shard: 0

aiur · InitStd · prove — main from: base run @ 7918b0c (not on bencher)

6 constants · 6 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).

Stage 1 — IxVM on FRI (6 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
Array.extract_append 11.302 s 11.654 s +3.1% ⚠️ 35.515 s 36.473 s +2.7% 77.77 GiB 77.77 GiB +0.0% 10.94 MiB 10.94 MiB +0.0% 71.1 ms 70.7 ms -0.5% 156.30B 156.30B +0.0%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 10.623 s 10.756 s +1.3% 34.862 s 34.235 s -1.8% 76.48 GiB 76.49 GiB +0.0% 10.99 MiB 10.99 MiB +0.0% 66.8 ms 69.6 ms +4.3% ⚠️ 153.04B 153.04B +0.0%
Char.ofOrdinal_le_of_le 7.212 s 7.375 s +2.3% 26.516 s 27.884 s +5.2% (1.05× slower) ⚠️ 64.29 GiB 64.40 GiB +0.2% 11.00 MiB 11.00 MiB +0.0% 74.1 ms 74.8 ms +1.0% 107.22B 107.22B +0.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 4.025 s 4.014 s -0.3% 15.586 s 15.990 s +2.6% 36.68 GiB 36.66 GiB -0.0% 10.91 MiB 10.91 MiB +0.0% 71.8 ms 73.4 ms +2.3% 60.82B 60.82B +0.0%
String.append 415.2 ms 429.0 ms +3.3% ⚠️ 2.189 s 2.174 s -0.7% 5.85 GiB 5.19 GiB -11.2% (1.13× smaller) 🟢 9.74 MiB 9.74 MiB +0.0% 61.0 ms 60.1 ms -1.6% 3.28B 3.28B +0.0%
Nat.add_comm 257.9 ms 295.1 ms +14.4% (1.14× slower) ⚠️ 1.081 s 1.160 s +7.3% (1.07× slower) ⚠️ 4.48 GiB 4.06 GiB -9.4% (1.10× smaller) 🟢 8.90 MiB 8.90 MiB +0.0% 53.5 ms 57.4 ms +7.2% (1.07× slower) ⚠️ 303.19M 303.19M +0.0%
Stage 2 — FRI recursion on FRI (6 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
Array.extract_append 5.254 s 5.389 s +2.6% 28.616 s 29.729 s +3.9% ⚠️ 90.51 GiB 90.52 GiB +0.0% 3.97 MiB 3.97 MiB +0.0% 24.7 ms 24.3 ms -1.6% 198.33B 198.33B +0.0%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 5.394 s 5.476 s +1.5% 29.937 s 30.205 s +0.9% 94.61 GiB 94.99 GiB +0.4% 3.97 MiB 3.97 MiB +0.0% 24.5 ms 24.4 ms -0.3% 203.36B 203.36B +0.0%
Char.ofOrdinal_le_of_le 5.303 s 5.449 s +2.7% 29.672 s 30.500 s +2.8% 94.61 GiB 94.97 GiB +0.4% 3.97 MiB 3.97 MiB +0.0% 24.9 ms 24.7 ms -0.9% 203.66B 203.66B +0.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 5.058 s 5.257 s +3.9% ⚠️ 28.629 s 29.809 s +4.1% ⚠️ 89.98 GiB 90.01 GiB +0.0% 3.97 MiB 3.97 MiB +0.0% 24.9 ms 25.2 ms +1.1% 197.42B 197.42B +0.0%
String.append 4.280 s 4.341 s +1.4% 27.195 s 27.950 s +2.8% 87.80 GiB 87.85 GiB +0.1% 3.97 MiB 3.97 MiB +0.0% 24.2 ms 24.2 ms -0.2% 165.44B 165.44B +0.0%
Nat.add_comm 3.502 s 3.693 s +5.5% (1.05× slower) ⚠️ 18.715 s 18.254 s -2.5% 57.75 GiB 57.79 GiB +0.1% 3.97 MiB 3.97 MiB +0.0% 25.3 ms 25.1 ms -0.5% 127.65B 127.65B +0.0%
Pipeline total (6 constants)
constant total-time (main) total-time (PR) Δ% pipeline-peak-ram (main) pipeline-peak-ram (PR) Δ%
Array.extract_append 1m 4.1s 1m 6.2s +3.2% ⚠️ 90.51 GiB 90.52 GiB +0.0%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 1m 4.8s 1m 4.4s -0.6% 94.61 GiB 94.99 GiB +0.4%
Char.ofOrdinal_le_of_le 56.188 s 58.384 s +3.9% ⚠️ 94.61 GiB 94.97 GiB +0.4%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 44.215 s 45.799 s +3.6% ⚠️ 89.98 GiB 90.01 GiB +0.0%
String.append 29.384 s 30.125 s +2.5% 87.80 GiB 87.85 GiB +0.1%
Nat.add_comm 19.796 s 19.413 s -1.9% 57.75 GiB 57.79 GiB +0.1%

Workflow logs

@johnchandlerburnham
diag: phase-level attribution for the Rust compile path
d97c761 
Closes the instrumentation gap ahead of the perf pass (the Rust side
had no RSS attribution):

- crates/compile/src/diag.rs: rss_log_suffix moves out of decompile.rs
  so the compile scheduler can use it; setup phases 1/2/3/5/7, the
  periodic progress tick, scheduler-drained and complete lines now
  carry rss/anon/file GiB.
- IX_COMPILE_DBG=1 (the Lean driver's phase knob) now also lights up
  the Rust-side IX_VERBOSE logging in compile_env, so one flag
  attributes the whole pipeline. (Env::put/put_file get the same alias
  plus per-section timers in the companion perf commit, which owns
  serialize.rs.)
- stale doc fix: compile/env.rs claimed worker kernel envs 'clear
  periodically'; they are fresh per block (canonicity §10.5).

No behavior change outside env-gated logging.
@johnchandlerburnham
perf: decompile Pass-2 restructure + compile hot-path batch
97e1b62 
Decompile (Mathlib 736k-const measurements; default-threshold run
151.2s -> 133.2s before the prewarm-stub change):

- get_constant_info_references: single-accumulator iterative DAG walk
  (visited keyed on Expr's digest Hash/Eq) instead of a per-node
  NameSet materialize+merge+clone per expr node. Feeds compile's
  setup_scan and decompile's Pass-2 ingress BFS. Value-identical sets;
  no consumer reads set iteration order into bytes (SCC members and
  serialized sections re-sort canonically) - held by the parity gates.
- Pass-2 ingress BFS: run-scoped refs memo surviving the kenv clear
  (the clear wiped the only BFS memo, making each clear re-walk the
  whole closure - the Θ(N²/L) term behind FLT's +114% decompile).
  Names absent from work_env stay unmemoized (aux constants appear
  only when their block regenerates).
- aux ingress walkers: per-call seen sets move into
  KernelCtx.aux_ingress_seen (resolved-id-keyed, cleared with the
  kenv; per-block-fresh in compile per §10.5), so a block no longer
  re-expands the whole closure that previous blocks already ingressed
  (Θ(blocks x closure) -> amortized O(closure)). collect_const_refs
  gains a digest-keyed visited set (shared subterms walked once).
  Measured: Pass-2 gen 75.9s -> 62.7s on Mathlib. Lean mirrors:
  Ix/AuxGen/Kernel.lean (AuxKernelCtx.auxIngressSeen),
  Ix/AuxGen/Recursor.lean (drainIngressQueue + visited set).
- Pass-2 prewarm (ensure_in_kenv_of_prewarm): theorem/opaque values
  ingress as type-only Axio stubs - the fidelity ingress_type_stub
  already gives thms the gen walkers discover, sufficient for kernel
  TC (proof irrelevance; opaque never unfolds). Full proof ingestion
  was the dominant share of Pass-2 kenv RSS (~47 KB/name measured),
  which is what forced the periodic clears; the clear default rises
  131072 -> 1048576 and becomes a rare backstop (FLT-scale closures
  no longer cross it). Lean mirror: ensureInKenvOfPrewarm, both
  Pass-2 driver variants.
- lean_env (a third whole-env copy) now drops after Pass 1.5 instead
  of living to end of decompile_env.

Compile:

- ixon/sharing.rs: all blake3-digest-keyed maps move from SipHash
  std HashMap to FxHashMap (keys are already uniform digests; every
  order-sensitive consumer re-sorts).
- merkle_root_canonical_sorted (host-only): parallel leaf+level
  hashing for callers holding sorted unique leaves; bit-identical
  root. Env::put/put_file use it; rs_compile_env computes the const
  table + root once and hands both to put_file_with_header - the sort
  and the ~2N-node tree ran twice per compile.
- Env::put_file: per-section timers mirroring Env::put (same
  IX_VERBOSE/IX_COMPILE_DBG knobs; §4's serial name topo sort timed
  separately).
- compile_definition/inductive/recursor take the block-context
  address list as a parameter, computed once per block (was: full
  ctx sort + re-intern per member, O(M² log M) per block).
- mutual-path ConstantMeta moves out of all_metas via remove instead
  of two deep clones per constant.

Bytes are unchanged by construction everywhere; gated by
put_file_matches_put, aux-gen-diff, decompile-diff, validate-aux and
the Mathlib-scale roundtrip.
@johnchandlerburnham
johnchandlerburnham enabled auto-merge (squash) August 20, 2026 13:13
@johnchandlerburnham
johnchandlerburnham merged commit 43429d2 into main Aug 20, 2026
11 checks passed
@johnchandlerburnham
johnchandlerburnham deleted the jcb/perf-optimization branch August 20, 2026 14:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@arthurpaulino arthurpaulino arthurpaulino left review comments
@samuelburnham samuelburnham samuelburnham approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@johnchandlerburnham @arthurpaulino @samuelburnham