perf: lazy §5 metadata windows on the demoted env load path - #585
Merged
Conversation
The decompile pre-phase parsed every §5 named entry's metadata into the structured form and immediately re-serialized it into the demoted bytes repr — 12.0 s of the 16.6 s Mathlib `.ixe` parse, all serial, paid before any pass starts. `Env::get_demoted_named` now keeps each entry's meta_len-framed window verbatim (one contiguous arena + the shared §4 reverse index) and decodes on demand through the same grammar helpers `get_named_indexed` parses with (`LazyMetaWindow`; a OnceLock split memo makes `has_original` cheap after any meta decode — the muts-plan sweep warms every entry before the passes). Both decompile FFI entries use this loader, so `import_ixe` gets the same load-time cut. Wire format untouched; `Env::get` still parses §5 eagerly and rejects interior corruption at load (lazy loads surface it on first decode instead — documented on `get_demoted_named`). Also on the read path: §2 per-const blake3 verification became a parallel sweep after the serial framing pass; the §4 names lookup is pre-sized (it rehash-doubled through 4.7M inserts); the final merkle-root check uses the parallel `_sorted` variant (§2 already proved the key set sorted+unique). Write path: `topological_sort_names` walks ancestor chains iteratively with a pre-sized visited set — emission order (wire bytes) unchanged. New `[Env::get]` per-section timers behind IX_VERBOSE/IX_COMPILE_DBG mirror `put_file`'s. New test: demoted_load_matches_structured_load pins lazy ≡ structured on every accessor plus byte-identical re-serialization (compared between the two loads: §4 emits the parent-closure of `env.names`, so synthetic envs without registered parent components permute §4 on reload — pipeline envs register every component and are unaffected).
Member
Author
|
!benchmark compile decompile |
johnchandlerburnham
enabled auto-merge
August 21, 2026 09:28
|
| 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 |
50.657 s | 45.568 s | -10.0% (1.11× faster) 🟢 | 15.42K | 17.14K | +11.2% (1.11× faster) 🟢 | 19.78 GiB | 19.77 GiB | -0.0% | 3.20 GiB | 3.20 GiB | +0.0% | 780,906 | 780,906 | +0.0% |
compile · InitStd — main from: base run @ 58cc959 (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.683 s | 3.682 s | -21.4% (1.27× faster) 🟢 | 25.00K | 31.80K | +27.2% (1.27× faster) 🟢 | 4.00 GiB | 3.96 GiB | -1.0% | 324.65 MiB | 324.65 MiB | +0.0% | 117,084 | 117,084 | +0.0% |
compile · Lean — main from: base run @ 58cc959 (not on bencher)
1 env · 0 with regressions · 0 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 |
7.755 s | 7.546 s | -2.7% | 26.65K | 27.38K | +2.8% | 5.29 GiB | 5.27 GiB | -0.5% | 481.18 MiB | 481.18 MiB | +0.0% | 206,647 | 206,647 | +0.0% |
compile · Mathlib — main from: base run @ 58cc959 (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 |
48.971 s | 43.753 s | -10.7% (1.12× faster) 🟢 | 15.75K | 17.62K | +11.9% (1.12× faster) 🟢 | 19.31 GiB | 18.99 GiB | -1.6% | 3.10 GiB | 3.10 GiB | +0.0% | 771,129 | 771,129 | +0.0% |
decompile · FLT — main from: base run @ 58cc959 (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 |
1m 56.6s | 1m 46.9s | -8.4% (1.09× faster) 🟢 | 6.70K | 7.31K | +9.1% (1.09× faster) 🟢 | 33.54 GiB | 32.16 GiB | -4.1% 🟢 | 3.20 GiB | 3.20 GiB | +0.0% | 780,906 | 780,906 | +0.0% |
decompile · InitStd — main from: base run @ 58cc959 (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 |
4.304 s | 3.314 s | -23.0% (1.30× faster) 🟢 | 27.20K | 35.33K | +29.9% (1.30× faster) 🟢 | 3.84 GiB | 3.66 GiB | -4.5% 🟢 | 324.65 MiB | 324.65 MiB | +0.0% | 117,084 | 117,084 | +0.0% |
decompile · Lean — main from: base run @ 58cc959 (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 |
9.125 s | 7.705 s | -15.6% (1.18× faster) 🟢 | 22.65K | 26.82K | +18.4% (1.18× faster) 🟢 | 4.97 GiB | 4.80 GiB | -3.3% 🟢 | 481.18 MiB | 481.18 MiB | +0.0% | 206,647 | 206,647 | +0.0% |
decompile · Mathlib — main from: base run @ 58cc959 (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 |
1m 46.7s | 1m 36.9s | -9.2% (1.10× faster) 🟢 | 7.23K | 7.96K | +10.1% (1.10× faster) 🟢 | 32.32 GiB | 30.97 GiB | -4.2% 🟢 | 3.10 GiB | 3.10 GiB | +0.0% | 771,129 | 771,129 | +0.0% |
arthurpaulino
approved these changes
Aug 21, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Headline numbers (Mathlib, 771,135 consts / 3.33 GB env, A/B on the same box)
ix decompile, section split from the new[Env::get]timers:.ixeparseEvery pass timing is flat (muts plan 0.60→0.56 s, Pass 1 14.6→14.5 s, Pass 2 65.1→64.9 s): the work removed from the load was not pushed into the passes.
The same loader serves
import_ixe, so a selective import (the TruthMines process-boundary use) stops paying a full §5 metadata parse for the whole env before materializing its first constant.What changed
Env::get_demoted_namedused to parse every §5 entry's metadata into the structured form and immediately re-serialize it into the demoted bytes repr — paying a full parse plus a full re-encode per entry, serially, before any pass starts. It now keeps each entry'smeta_len-framed window verbatim (one contiguous arena plus the shared §4 reverse index) and decodes on demand: newMetaRepr::Window/LazyMetaWindowinenv.rs, decoding through the same three grammar helpersget_named_indexeditself now parses with (single source for the window grammar). AOnceLocksplit memo (meta length + original address, ~40 B/entry) is filled by any meta decode — the decompiler's muts-plan sweep reads every entry's meta up front, sohas_original()/original()on the passes stay as cheap as the old materialized slots. The mutating original-slot APIs materialize the window first, soNamedstays total. RSS drops because the indexed windows are the compact encoding (varint name indices) while the old demoted blobs re-encoded every name reference as a raw 32-byte address.get_demoted_named: interior §5 corruption that the eager loaders reject at load now surfaces as a panic on first decode (window framing is still validated at load; §2 constants keep their per-entry hash check).Env::getrecomputed the root with the serial builder even though §2's order check proves the key set sorted and duplicate-free — now uses the parallelmerkle_root_canonical_sortedfrom perf: decompile Pass-2 restructure + compile hot-path batch (post-#572 perf pass) #579 (host-only, same cfg pattern as the write side).[Env::get]per-section timers behindIX_VERBOSE/IX_COMPILE_DBG, mirroringput_file's — these produced the section split above.Validation
ix compileofCompileMathlib.leanat this branch vs the pre-branch reference →cmpidentical (3,326,436,547 bytes).ix validate: 0 failures across all phases (compile, aux congruence, two decompiles through the lazy loader, serialize, per-constant roundtrip fidelity).demoted_load_matches_structured_load: lazy load ≡ structured load on everyNamedaccessor (meta, original, has_original, hints), mutation APIs materialize correctly, and the two loads re-serialize byte-identically — including entries whose metadata carries name references through the §4 index. (It also surfaced a pre-existing latent quirk, unchanged here: §4 emits the parent-closure ofenv.names, so a synthetic env whose multi-component names lack registered parents permutes §4 on reload. Pipeline envs register every component — whole-env byte roundtrips hold in CI.)--ignoredgates: validate-aux 0 failures; aux-gen-diff drift/patches/plans/driver gates PASS with all gated mismatch counts 0; decompile-diff plain 3,660/0 and aux-family 2,504/0, Pass-2 plan parity 300/300.cargo test --workspace --release: all suites pass (0 failures).--all-featuresdev and--release) with-D warnings, andcargo fmt --check: clean.Explicitly not touched
Wire format (no
Env::VERSIONchange),Env::get's eager/validating semantics, the Lean-side deserializers, and the decompile passes themselves. Remaining decompile targets after this: Pass 2 gen (59 s, the dominant phase — per-accessLazyConstantre-parse territory) and Pass 1 (14.5 s), plus the prove-side items tracked separately.