Uh oh!
There was an error while loading. Please reload this page.
perf: Decrease RAM overhead for ix compile - #484
Conversation
Step 0 (instrumentation, IX_QUIET-gated): - Env::const_cache_stats: entries / summed raw_bytes / materialized count, logged at compile completion and once per completed decile so OOM-killed runs still leave a growth curve. - Per-worker KEnv cache sizes, snapshotted at block completion, aggregated at each decile, and dumped per worker at exit. Step 1 (IX_COMPILE_SPILL=demote|mmap): - LazyConstant::from_constant_uncached serializes and drops the structured value (cache: None), matching the lazy-load read policy. - Env::store_const gates on the new SpillMode (parsed once from IX_COMPILE_SPILL; unknown values warn and fall back to off). mmap behaves as demote until the spill file lands (step 2). Compilation never reads stored constants back (audited: dependencies resolve via name_to_addr, aux_gen ingresses from the Lean env), so demote only affects later readers' CPU: ix compile reads bytes only; check/validate re-parse per access like the file-load path. Measured (see docs/compile-spill.md): - InitStd: peak RSS 11.10 -> 8.48 GB, byte-identical .ixe, equal wall time; the dropped caches cost ~22x their 121 MiB serialized form. - FLT: completes under a 50 GB cap for the first time on a 56 GB box (44.9 GB peak, previously OOM at 88.8%), faster at every comparable checkpoint; off-mode extrapolates to ~61-66 GB, matching the 63-68 GB CI measurement.
Under IX_COMPILE_SPILL=mmap, store_const appends each constant's bytes to an anonymous temp file (tempfile_in: O_TMPFILE, no pathname, kernel reclaims on exit even on SIGKILL; dir from IX_COMPILE_SPILL_DIR, default cwd — must be disk-backed, tmpfs pages are swap-backed and cannot evict under MemorySwapMax=0). The file seals in 256 MiB segments (IX_COMPILE_SPILL_SEGMENT_MB to override): each sealed range is mmapped read-only and its entries swap from heap bytes to windows into the mapping via from_mmap_slice, so the kernel can evict them as clean page cache under pressure. Resident accumulator heap is bounded by one unsealed segment. Hot-path details, both measured on InitStd: - Appends stage through an 8 MiB buffer; a write syscall inside the spill mutex convoys the scheduler workers (2.8s -> 10.5s before staging, 3.0s after). - Spill modes skip re-stores of an existing address (alpha-collapsed blocks re-store the shared address once per member; 106k stores vs 90k unique on InitStd) — re-appending duplicated spill bytes and re-inserting would downgrade sealed windows back to heap. Any spill I/O error disables spilling and falls back to heap-backed entries; sealed windows stay valid. Measured: InitStd bit-identical to off/demote across reruns; FLT completes under the 50 GB cap (44.9 GB peak, scheduler 34.6s vs demote 37.8s), 2 segments sealed, spill file 747.8 MiB ~= the accumulator byte sum. FLT byte-comparison surfaced pre-existing run-to-run nondeterminism in the named/metadata section (same first-diff offset across same-mode reruns, any mode; consts section deterministic) — documented in docs/compile-spill.md correctness gates, tracked separately.
Instrumentation (IX_QUIET-gated): sample /proc/self/status (VmRSS/RssAnon/RssFile) at rs_compile_env entry, after decode_env, at scheduler start, per decile, and at completion. The anon/file split is the signal the spill work changes: anon can only leave RAM via swap, file RSS is reclaimable page cache. IX_COMPILE_KENV_CLEAR_EVERY=N (default 0 = never, today's behavior) clears each worker's kernel env every N completed blocks via the existing clear_releasing_memory. The kenv is a pure cache of Lean-env-derived data (ensure_in_kenv re-ingresses on demand), so block-boundary clearing is semantics-free; InitStd output is byte-identical with N=64 and the suites pass with N=2. Measured on Mathlib under a 50 GB cap (24 workers): progress ladder off 48.3% -> mmap 66% -> mmap+clear=64 72.5%, no wall-time cost. The decomposition pins the remaining OOM gap on the decoded Rust LeanEnv (25.2 GiB anon, whole-run) and structured named/names metadata (~13 GiB anon by 62%); spilled accumulator pages and mmapped oleans are observably evicted under pressure (file RSS 6.3 -> 1.3 GiB). Roadmap with measured budgets: docs/compile-spill.md, "Mathlib on a 56 GB box".
IX_COMPILE_META=demote (default structured = today's behavior) stores each registered Named's metadata as its self-contained serialized form instead of a structured ConstantMeta DAG, decoded on demand. - metadata.rs: name references are written through a NamePut/NameGet coder — Indexed (the .ixe named-section form, u64 into the env name index) or Raw (32-byte addresses, self-contained). Same wire format otherwise, so ConstantMeta::put_raw bytes re-encode through the index bit-identically at Env::put. Public entry points renamed put_indexed/get_indexed -> put_with/get_with; put_raw/get_raw added. - env.rs: Named's meta/original fields are private behind a MetaRepr (Structured(Arc<ConstantMeta>) | Bytes(Arc<[u8]>)) with accessors meta()/original()/has_original()/set_original()/demote(). register_name demotes under the flag; set_original follows the entry's repr so promote_aux keeps demoted entries demoted. - Callers across kernel ingress, decompile, kernel egress, ffi, and ixvm-codegen migrated from field access to accessors (behavior preserved; structured mode is an Arc clone per access). Measured under the 50 GB cap, 24 workers, with IX_COMPILE_SPILL=mmap + IX_COMPILE_KENV_CLEAR_EVERY=64: - InitStd: peak RSS 8.2 -> 5.6 GiB, .ixe byte-identical, ~+10% wall (Env::put re-encode of 106k metas). - Mathlib: compile-phase anon growth flattens from 29->42+ GiB (OOM at 72.5%) to 28->32.4 GiB, and Mathlib COMPLETES on the 56 GB dev box for the first time: 45.1 GB peak, 726,513 blocks, 45.5s scheduler / 134s total, 2.9 GB .ixe. Remaining peak is the end-of-run serialization spike (~6.5 GiB) — lever 4's target.
Env::put_file serializes the environment straight to a file, entry by entry through a reusable staging buffer — nothing proportional to env size is allocated (Env::put builds one env-sized Vec, and the FFI then copies it into a Lean ByteArray before Lean writes the file). Sections and encoding are identical to Env::put; equivalence is enforced by the put_file_matches_put quickcheck test and the InitStd cmp oracle. The write goes to <out>.tmp followed by an atomic rename, so a crash cannot leave a truncated .ixe (an improvement over IO.FS.writeBinFile). rs_compile_env_to_file drives it behind the FFI and returns the byte count; CompileCmd.lean selects it under IX_COMPILE_STREAM=1 (default off — the buffered path is unchanged). Measured under the 50 GB cap with the full spill stack (IX_COMPILE_SPILL=mmap IX_COMPILE_META=demote IX_COMPILE_KENV_CLEAR_EVERY=64): - InitStd: peak RSS 5.6 -> 4.9 GiB, byte-identical output. - Mathlib: peak RSS 45.1 -> 41.8 GB, total wall 134 -> 94 s (29.6 s buffered serialize + 3.8 s ByteArray copy + 6.1 s Lean write collapse into a 22.2 s stream); RSS after serialization equals the compile plateau — the end-of-run spike is eliminated.
Skip the eager decode_env copy of the Lean environment — measured at 25.6 GiB of whole-run anonymous heap on Mathlib. Lazy mode decodes only names eagerly, keeps one LeanShared handle per constant, and decodes ConstantInfos on demand through a bounded cache. - ix_common: Env is now a struct (was a FxHashMap type alias) with an eager variant (default; the only variant on the guest) and a host-only lazy variant (name index + injected fetch + 64-shard bounded cache with oldest-biased eviction, IX_COMPILE_LEAN_ENV_CACHE entries, default 65536). Env::get returns an EnvEntry deref-guard: a plain borrow for eager (zero cost), an Arc for lazy. iter() bypasses the cache (whole-env passes are single-visit). - ffi: decode_env_lazy builds the index in parallel and injects the fetch closure; decode_env_auto dispatches on IX_COMPILE_LEAN_ENV. Thread safety is the eager path's own mechanism, unchanged: decode_env already MT-marks the reachable graph via LeanShared (lean_mark_mt -> atomic refcounting) and decodes in parallel; lean-ffi structural accessors are refcount-silent, and each element's owned handle keeps its objects alive for the Env lifetime. - Call sites: EnvEntry's Deref absorbed most accesses; the remainder migrated mechanically (as_deref() at pattern scrutinees, bound guards where borrows escape). Measured under the 50 GB cap with all levers (IX_COMPILE_LEAN_ENV=lazy IX_COMPILE_STREAM=1 IX_COMPILE_SPILL=mmap IX_COMPILE_META=demote IX_COMPILE_KENV_CLEAR_EVERY=64): - InitStd: peak RSS 4.9 -> 4.0 GiB, .ixe byte-identical, decode-phase RSS delta zero (was +2.7 GiB). - Mathlib: peak RSS 41.8 -> 19.4 GB (decode +0.1 GiB, was +25.6; compile-plateau anon 11.2 GiB), wall 94 -> 149 s at the default cache (42% hit rate) — the explicit RAM<->CPU knob; eager default keeps today's wall time. Progress ladder on the 56 GB box, Mathlib under a 50 GB cap: off OOM@48% -> spill 66% -> +kenv-clear 72.5% -> +meta demote completes @45.1 GB -> +stream 41.8 GB -> +lazy env 19.4 GB.
compile_env's setup decoded the entire Lean environment three times back-to-back: build_ref_graph, ground_consts' immediate scan, and validate_lean_ind_flags' group collection. Free when the env is an eager map; under IX_COMPILE_LEAN_ENV=lazy each sweep re-decodes every constant, and the triple sweep dominated lazy mode's wall regression. graph::setup_scan is one parallel pass producing all three outputs (ref graph, immediately-ungrounded set, inductive groups) with one decode per constant. ground_consts splits into ground_const_check + proliferate_ungrounded; validate_lean_ind_flags splits out validate_ind_groups. The unfused functions remain (other callers, tests) and the fused path is behavior-identical. Measured (full lever stack, 50 GB cap): lazy-mode wall regression eliminated — Mathlib 149 -> 93.4 s (eager: 94.4 s), InitStd 12.0 -> 6.9 s (eager: 7.0 s); .ixe byte-identical on InitStd; peak RSS unchanged (Mathlib 19.5 GB). Lazy mode now matches eager wall time while using less than half the RAM of the pre-lever-1 stack.
The scheduler module gains a "Memory tuning" overview documenting the IX_COMPILE_* knobs and the measured Mathlib outcome, the lazy-env types get self-contained doc comments, and comments that pointed at the working design doc now point at the relevant module docs instead.
The measured wall-time cost of the memory reductions is zero at scale
(Mathlib 86.5 s / 19.5 GB with pure defaults vs OOM >50 GB before; the
.ixe is byte-identical), so they stop being opt-in:
- Lazy Lean-env decode is the compile FFI entries' only path
(decode_env_for_compile; fixed 65536-entry cache — wall parity
measured InitStd through Mathlib, nothing to tune). Test/roundtrip
entries keep the eager decode_env.
- The compile CLI always streams the .ixe from Rust
(rs_compile_env_to_file); the buffered branch is gone from
CompileCmd. rs_compile_env remains for callers that want bytes in
memory.
- Worker kenvs clear unconditionally every 64 blocks (measured at zero
wall cost, several GB bounded on Mathlib).
- The mmap spill file is removed outright (crates/ixon/src/spill.rs,
tempfile dep): sealed segments made only the accumulator's ~1 GB of
bytes evictable — noise next to the demotions — and cost a Mutex on
the store path plus a file lifecycle.
One tradeoff remains env-tunable, plus parallelism:
- IX_COMPILE_DEMOTE (default on; =0 to disable) covers both demotions
— accumulator constants and named metadata as serialized bytes
(~20x smaller than structured). Off buys free post-compile
structural reads for in-process flows (ix check / ix validate).
- IX_COMPILE_WORKERS unchanged.
Replaces IX_COMPILE_SPILL{,_DIR,_SEGMENT_MB}, IX_COMPILE_META,
IX_COMPILE_KENV_CLEAR_EVERY, IX_COMPILE_LEAN_ENV{,_CACHE}, and
IX_COMPILE_STREAM.The ByteArray-returning variant had no callers — every consumer of a compiled env reads .ixe files or content addresses — so the streaming implementation takes over the rs_compile_env symbol and the rsCompileEnvBytes/rsCompileEnvBytesFFI names, now taking the output path and returning the byte count.
LazyEnvStats gains thread-summed durations for miss decodes and cache-bypassing iter sweeps, reported in the compile completion log next to the hit/miss counters, to size decode CPU against wall time.
The lazy-env EnvEntry API and the decode-time counters broke code that only compiles under --features test-ffi, which CI's clippy --all-targets --all-features gate builds but local default builds skip: the test-only FFI entries needed deref-guard adaptation, and the new instrumentation tripped pedantic cast lints (fixed by sharing the scheduler's RSS formatter, a saturating nanos helper, and a single-byte shard selector rather than allow attributes). Also records why the rust-decompile suite stays disabled: Rust decompile of synthesized _sparseCasesOn aux constants fails with "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). Reproduces at the merge base, so the bug is upstream of this branch. Measured under a 50G cap while here: rust-compile passes at 8.9 GiB peak; rust-decompile reaches its (pre-existing) failure at 18.1 GiB on this branch vs 24.8 GiB at the merge base.
The RAM work needed a lot of scaffolding to find where the bytes were; none of it earns a place in the shipped code now that the answers are in. Removed: lazy-env hit/miss and decode-time counters (LazyEnvStats), the RSS anon/file log suffix and /proc reader, per-decile accumulator composition and worker-kenv telemetry in the scheduler reporter, per-worker kenv snapshot slots and exit logs, Env::put_file section logging, ixon ConstCacheStats, the rs_compile_env RSS trace, and the IX_SKIP_DROPS escape hatch (the skip is now unconditional — the compile CLI is one-shot). Env::put keeps its pre-existing section logging; the improvements (lazy decode, streaming, demotion, kenv clearing, fused scan) are untouched, and the lazy-env shard count gains a sizing rationale.
FLT sweep (511k consts, 50G cap): wall is flat from 4096 through 1M
cache entries — 60.7/65.8/60.1/65.5/67.0 s at 4k/16k/64k/256k/1M —
because misses hide in the scheduler's dependency-stall slack, while
peak RSS climbs 11.5 -> 11.9 -> 13.0 -> 18.2 -> 24.7 GiB. Mathlib
(737k consts) confirms at 16k: 87.5 s / 17.0 GiB vs 87.3 s / 18.3 GiB
at 64k. The cache buys RAM, not speed; 16384 sits at the small end
with 4x headroom over the smallest size measured not to thrash.
Outputs byte-identical across all sizes (cmp-verified on FLT).
The cache's lock partitions are renamed shards -> segments ("shard"
already means proving shards in this repo) and their count now scales
with the machine instead of hardcoding: 4x the hardware threads
rounded to a power of two (two-byte hash window masked to the count),
so a worker per thread on large SMT boxes keeps low expected collision
rates without overpaying on small ones. FLT parity re-measured
(63.5 s / 11.7 GiB, identical bytes).samuelburnham
commented
Jul 10, 2026
!benchmark compile InitStd Mathlib |
❌ benchmark run failed
|
samuelburnham
commented
Jul 10, 2026
!benchmark compile BENCH_ENVS=InitStd,Mathlib |
|
| constant | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 4.243 s | 4.795 s | +13.0% (1.13× slower) | 24.86K | 22.00K | -11.5% (1.13× slower) | 11.21 GiB | 3.32 GiB | -70.4% (3.38× smaller) 🟢 | 306.43 MiB | 306.43 MiB | +0.0% | 105,492 | 105,492 | +0.0% |
1 constants · 1 regressed · 0 improved (|Δ| > 3.0% on any metric).
compile · Mathlib — main from: bencher @ e6daffc
| constant | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib | 43.729 s | 56.052 s | +28.2% (1.28× slower) | 16.85K | 13.14K | -22.0% (1.28× slower) | 103.53 GiB | 17.88 GiB | -82.7% (5.79× smaller) 🟢 | 2.97 GiB | 2.97 GiB | +0.0% | 736,618 | 736,618 | +0.0% |
1 constants · 1 regressed · 0 improved (|Δ| > 3.0% on any metric).
Named's meta field went private behind MetaRepr (structured or demoted-to-bytes); the guest's Muts filter now calls meta(). On the guest every entry is structured, so the call is an Arc clone. Verified via the CI-equivalent sp1-host build (guest ELF via build.rs).
The named section is the only one whose per-entry encode is CPU-heavy (demoted entries decode and re-encode through the name index), and it was written strictly sequentially — the bulk of the CI wall regression vs main. Chunks of 4096 now encode in parallel into per-entry buffers and drain to the writer in order, bounding staged memory to a few MiB. Bytes unchanged (put_file_matches_put). InitStd defaults 7.1 -> 5.8 s (now faster than the eager, undemoted configuration was); Mathlib 87.5 -> 74.7 s at 17.7 GiB under the 50G cap.
The on-demand Lean-env decode costs a few percent of wall vs the up-front eager copy (measured +0.3 s on InitStd's 6.4 s; per-constant fetches vs one batched parallel decode). Machines with RAM to spare can buy it back: IX_COMPILE_EAGER=1 restores the eager decode at the cost of the single largest memory term (~25 GB at Mathlib scale). Byte-identical output either way (cmp-verified); InitStd 5.8 -> 5.3 s at 2.7 -> 4.7 GiB.
The bounded cache's misses are dominated by foundational constants (high in-degree, referenced from blocks spread across the whole schedule) that any evicting cache keeps churning. The ref graph from setup_scan gives exact reference counts before the scheduler starts, so the top 16384 names by in-degree go into a never-evicted overlay: each decodes once on first access, reads after that are lock-free, and everything else falls through to the segments. Measured (24-core box, 50G cap, interleaved runs): Lean 12.3 -> 10.5 s (-15 %), FLT 55.8 -> 53.4 s (-4 %), InitStd and Mathlib neutral; peak RSS +0.3 GiB at most. A 4x/16x larger pin set bought RAM, not speed. Outputs byte-identical throughout.
samuelburnham
commented
Jul 11, 2026
!benchmark compile BENCH_ENVS=InitStd,Mathlib |
samuelburnham
commented
Jul 11, 2026
!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib |
❌ benchmark run failed |
❌ benchmark run failed |
samuelburnham
commented
Jul 11, 2026
!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib |
❌ benchmark run failed
|
\!benchmark's passthrough allowlist gains IX_COMPILE_EAGER / IX_COMPILE_DEMOTE / IX_COMPILE_WORKERS, and the compile job now applies passthrough env before the measured `ix compile` (previously only the prover cells did). The .ixe/row cache keys hash the passthrough content, so a knob run on the same commit measures and publishes its own row instead of silently reusing the default run's. \!benchmark compile BENCH_ENVS=Mathlib IX_COMPILE_EAGER=1
samuelburnham
commented
Jul 11, 2026
!benchmark compile BENCH_ENVS=InitStd,Mathlib |
|
| constant | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 4.243 s | 3.894 s | -8.2% (1.09× faster) 🟢 | 24.86K | 27.09K | +9.0% (1.09× faster) 🟢 | 11.21 GiB | 3.64 GiB | -67.5% (3.08× smaller) 🟢 | 306.43 MiB | 306.43 MiB | +0.0% | 105,492 | 105,492 | +0.0% |
1 constants · 0 regressed · 1 improved (|Δ| > 3.0% on any metric).
compile · Mathlib — main from: bencher @ e6daffc
| constant | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib | 43.729 s | 49.707 s | +13.7% (1.14× slower) | 16.85K | 14.82K | -12.0% (1.14× slower) | 103.53 GiB | 19.18 GiB | -81.5% (5.40× smaller) 🟢 | 2.97 GiB | 2.97 GiB | +0.0% | 736,618 | 736,618 | +0.0% |
1 constants · 1 regressed · 0 improved (|Δ| > 3.0% on any metric).
Uh oh!
There was an error while loading. Please reload this page.
… RAM (demoted metadata, cache-less constants) and measured only the compile side. This commit repairs the two read-side flows it broke and extends its memory discipline to decompilation and validation, with one uniform policy at every scale. CI fixes (ignored-test job: 23.5 min red -> ~11 min green): - kernel-tutorial's AdvNat.rec adversarial test silently inverted: demote-mode `store_const` treats a re-store of an existing address as a no-op (content addressing assumes identical bytes), which swallowed the deliberately-poisoned recursor rule and let the kernel accept the original valid constant. The poison helper now stores through `store_const_demoted(.., false)`. - Decompile Pass 2 called `stored_plan_blocks_for_original_all` once per aux block, each call scanning every `stt.env.named` entry with a full metadata decode under demote: O(blocks x env) ~ 259M decodes ~ 848 s at 143k-const scale (8.8 s pre-#484). `MutsPlanIndex` resolves every Muts entry in one parallel scan up front; `rehydrate_aux_perms_from_env` shares it. Pass 2 drops to 3.2 s - faster than pre-#484, since the index also eliminates the old per-block Arc-clone scan. Decompile memory levers (measured on the 56 GB dev box, 50 GB cap): - Cross-constant expression interning: decompile shared subterms only within a constant, so every common type/spine held one private copy per referencing constant. `DecompileState::insert_interned` canonicalizes each constant's `ExprData` nodes through a content-hash table (iterative post-order walk, per-walk pointer memo, rebuilds reuse stored hashes); the table drops when `decompile_env` returns. Mathlib decompile: OOM >50 GB during Pass 1 -> completes at 33.6 GiB peak (736,618 constants, 247 s, 0 errors). FLT decompile 30.4 -> 17.8 GB; InitStd 7.5 -> 3.3 GB; wall flat everywhere (FLT 70.4 -> 70.6 s). - `Env::get_demoted_named`: file loads can store each Named's metadata demoted as it parses. Load-then-demote pays the structured peak anyway (Mathlib: 19.8 GiB resident before Pass 1; freed arenas stay charged to a capped cgroup), demote-at-parse holds one structured entry at a time (5.5 GiB at the same point). - Pass 2's shared kenv gets a size-triggered clear (65536 ingressed names). A count cadence like the compile scheduler's is a measured ~10x Pass 2 wall regression here (the kenv is shared and a clear forces full closure re-walks), and a 32768 trigger doubled FLT Pass 2 (64 -> 131 s) to save ~2 GB; 65536 never fires through FLT/Mathlib (peaks 62k/54k) and remains a backstop against larger closures. - rs_kernel_roundtrip stops cloning dstt.env into a plain Env for comparison; `compare_envs` takes a lookup instead. Validate (`ix validate` / rs_compile_validate_aux): - The Lean env decode uses the compile CLI's lazy view with the same `IX_COMPILE_EAGER=1` escape hatch; the eager Rust copy is the largest term of the run's baseline RSS and stays resident through every phase. Costs wall on small envs (InitStd 33 -> 49 s) - accepted for a single scale-independent policy. - Phase 7's reload deserializes via `get_demoted_named`. - Whole-env promotion was tried first and rejected: re-materializing the ~20x structured forms costs +32.6 GB at FLT scale and OOMs at Mathlib scale. Never promote a big env; hoist or bound the reads. Net: FLT `ix validate` goes from OOM at 42% of Phase 5 to completing at 38.7 GiB with 0 failures (540 s); Mathlib `ix decompile` works on a 56 GB machine for the first time. Also: decompile phase logs gain an RSS anon/file suffix, Pass 2 progress reports the kenv size, and validate's PhaseResult reports per-phase durations.
… RAM (demoted metadata, cache-less constants) and measured only the compile side. This commit repairs the two read-side flows it broke and extends its memory discipline to decompilation and validation, with one uniform policy at every scale. CI fixes (ignored-test job: 23.5 min red -> ~11 min green): - kernel-tutorial's AdvNat.rec adversarial test silently inverted: demote-mode `store_const` treats a re-store of an existing address as a no-op (content addressing assumes identical bytes), which swallowed the deliberately-poisoned recursor rule and let the kernel accept the original valid constant. The poison helper now stores through `store_const_demoted(.., false)`. - Decompile Pass 2 called `stored_plan_blocks_for_original_all` once per aux block, each call scanning every `stt.env.named` entry with a full metadata decode under demote: O(blocks x env) ~ 259M decodes ~ 848 s at 143k-const scale (8.8 s pre-#484). `MutsPlanIndex` resolves every Muts entry in one parallel scan up front; `rehydrate_aux_perms_from_env` shares it. Pass 2 drops to 3.2 s - faster than pre-#484, since the index also eliminates the old per-block Arc-clone scan. Decompile memory levers (measured on the 56 GB dev box, 50 GB cap): - Cross-constant expression interning: decompile shared subterms only within a constant, so every common type/spine held one private copy per referencing constant. `DecompileState::insert_interned` canonicalizes each constant's `ExprData` nodes through a content-hash table (iterative post-order walk, per-walk pointer memo, rebuilds reuse stored hashes); the table drops when `decompile_env` returns. Mathlib decompile: OOM >50 GB during Pass 1 -> completes at 33.6 GiB peak (736,618 constants, 247 s, 0 errors). FLT decompile 30.4 -> 17.8 GB; InitStd 7.5 -> 3.3 GB; wall flat everywhere (FLT 70.4 -> 70.6 s). - `Env::get_demoted_named`: file loads can store each Named's metadata demoted as it parses. Load-then-demote pays the structured peak anyway (Mathlib: 19.8 GiB resident before Pass 1; freed arenas stay charged to a capped cgroup), demote-at-parse holds one structured entry at a time (5.5 GiB at the same point). - Pass 2's shared kenv gets a size-triggered clear (65536 ingressed names). A count cadence like the compile scheduler's is a measured ~10x Pass 2 wall regression here (the kenv is shared and a clear forces full closure re-walks), and a 32768 trigger doubled FLT Pass 2 (64 -> 131 s) to save ~2 GB; 65536 never fires through FLT/Mathlib (peaks 62k/54k) and remains a backstop against larger closures. - rs_kernel_roundtrip stops cloning dstt.env into a plain Env for comparison; `compare_envs` takes a lookup instead. Validate (`ix validate` / rs_compile_validate_aux): - The Lean env decode uses the compile CLI's lazy view with the same `IX_COMPILE_EAGER=1` escape hatch; the eager Rust copy is the largest term of the run's baseline RSS and stays resident through every phase. Costs wall on small envs (InitStd 33 -> 49 s) - accepted for a single scale-independent policy. - Phase 7's reload deserializes via `get_demoted_named`. - Whole-env promotion was tried first and rejected: re-materializing the ~20x structured forms costs +32.6 GB at FLT scale and OOMs at Mathlib scale. Never promote a big env; hoist or bound the reads. Net: FLT `ix validate` goes from OOM at 42% of Phase 5 to completing at 38.7 GiB with 0 failures (540 s); Mathlib `ix decompile` works on a 56 GB machine for the first time. Also: decompile phase logs gain an RSS anon/file suffix, Pass 2 progress reports the kenv size, and validate's PhaseResult reports per-phase durations.
* perf: Fix ignored-test fallout from #484 and bound decompile/validate RAM (demoted metadata, cache-less constants) and measured only the compile side. This commit repairs the two read-side flows it broke and extends its memory discipline to decompilation and validation, with one uniform policy at every scale. CI fixes (ignored-test job: 23.5 min red -> ~11 min green): - kernel-tutorial's AdvNat.rec adversarial test silently inverted: demote-mode `store_const` treats a re-store of an existing address as a no-op (content addressing assumes identical bytes), which swallowed the deliberately-poisoned recursor rule and let the kernel accept the original valid constant. The poison helper now stores through `store_const_demoted(.., false)`. - Decompile Pass 2 called `stored_plan_blocks_for_original_all` once per aux block, each call scanning every `stt.env.named` entry with a full metadata decode under demote: O(blocks x env) ~ 259M decodes ~ 848 s at 143k-const scale (8.8 s pre-#484). `MutsPlanIndex` resolves every Muts entry in one parallel scan up front; `rehydrate_aux_perms_from_env` shares it. Pass 2 drops to 3.2 s - faster than pre-#484, since the index also eliminates the old per-block Arc-clone scan. Decompile memory levers (measured on the 56 GB dev box, 50 GB cap): - Cross-constant expression interning: decompile shared subterms only within a constant, so every common type/spine held one private copy per referencing constant. `DecompileState::insert_interned` canonicalizes each constant's `ExprData` nodes through a content-hash table (iterative post-order walk, per-walk pointer memo, rebuilds reuse stored hashes); the table drops when `decompile_env` returns. Mathlib decompile: OOM >50 GB during Pass 1 -> completes at 33.6 GiB peak (736,618 constants, 247 s, 0 errors). FLT decompile 30.4 -> 17.8 GB; InitStd 7.5 -> 3.3 GB; wall flat everywhere (FLT 70.4 -> 70.6 s). - `Env::get_demoted_named`: file loads can store each Named's metadata demoted as it parses. Load-then-demote pays the structured peak anyway (Mathlib: 19.8 GiB resident before Pass 1; freed arenas stay charged to a capped cgroup), demote-at-parse holds one structured entry at a time (5.5 GiB at the same point). - Pass 2's shared kenv gets a size-triggered clear (65536 ingressed names). A count cadence like the compile scheduler's is a measured ~10x Pass 2 wall regression here (the kenv is shared and a clear forces full closure re-walks), and a 32768 trigger doubled FLT Pass 2 (64 -> 131 s) to save ~2 GB; 65536 never fires through FLT/Mathlib (peaks 62k/54k) and remains a backstop against larger closures. - rs_kernel_roundtrip stops cloning dstt.env into a plain Env for comparison; `compare_envs` takes a lookup instead. Validate (`ix validate` / rs_compile_validate_aux): - The Lean env decode uses the compile CLI's lazy view with the same `IX_COMPILE_EAGER=1` escape hatch; the eager Rust copy is the largest term of the run's baseline RSS and stays resident through every phase. Costs wall on small envs (InitStd 33 -> 49 s) - accepted for a single scale-independent policy. - Phase 7's reload deserializes via `get_demoted_named`. - Whole-env promotion was tried first and rejected: re-materializing the ~20x structured forms costs +32.6 GB at FLT scale and OOMs at Mathlib scale. Never promote a big env; hoist or bound the reads. Net: FLT `ix validate` goes from OOM at 42% of Phase 5 to completing at 38.7 GiB with 0 failures (540 s); Mathlib `ix decompile` works on a 56 GB machine for the first time. Also: decompile phase logs gain an RSS anon/file suffix, Pass 2 progress reports the kenv size, and validate's PhaseResult reports per-phase durations. * feat: Add `ix decompile` and its benchmark backend `ix decompile <path.ixe>` decompiles a serialized environment back to Lean constants — the inverse of `ix compile` — and with `--json` emits an env-keyed results row (decompile-time, throughput, peak-rss, file-size, constants) through the same measurement infrastructure as `ix compile --json`: wall clock and the texray tree-RSS sampler window around the measured step, so the two rows share semantics. The `rs_decompile_env` FFI loads the env with `Env::get_demoted_named`, populates `name_to_addr` for aux_gen's address resolution (mirroring validate's Phase 7 setup), and returns the constant count; a malformed decompile is a hard error so the bench cell reddens. Bundle inputs are checked up front: a bundle env (`main` set) must pass `validate_closed`, and a thin bundle (non-empty `assumptions`) is rejected — decompile needs every reachable constant carried. The bench registry gains the `decompile` backend (testbed `ix-decompile-x64-32x`): bench-main restores the compile cell's fresh `.ixe` and tracks decompile-time / throughput / peak-rss on bencher (file-size and constants duplicate the compile plots exactly, so the dashboard skips them), PR compare tables render decompile-time as seconds, and the thresholds-reset workflow accepts the `ix-decompile` token. Local reference (56 GB box, 50 GB cap): InitStd 105k consts / 3.4 GB peak, FLT 511k / 17.8 GB, Mathlib 737k / 33.6 GiB. The previous occupant of the `rs_decompile_env` symbol — decompile of a Lean-side `Ixon.RawEnv` — is removed along with its only caller (`rsDecompileEnv` in DecompileM and the disabled rust-decompile test). That flow existed only for the test: `toRawEnv` drops `Named.original` sidecars, so shape-divergent `_sparseCasesOn` blocks lost their recovery path and failed with "missing Ref metadata" — an artifact of the phantom boundary, not of decompilation (the `.ixe` format preserves the sidecars, and Mathlib's ~5k such constants decompile cleanly). A replacement test over the real serialized flow follows in the next commit. * test: Cover Rust decompile over the serialized roundtrip Replaces the removed RawEnv-based rust-decompile test with one that exercises the flow decompilation actually ships: Lean env → compile → Env::put → Env::get_demoted_named → decompile_env → per-constant hash comparison i.e. `ix decompile`'s pipeline over an in-memory `.ixe`, covering the demoted-at-parse metadata load, the `Named.original` recovery for shape-divergent aux blocks, and expression interning — without the kernel ingress/egress leg `kernel-ixon-roundtrip` adds in the middle. Where the old test failed on its own lossy FFI boundary, this one passes: 143,697/143,697 constants hash-identical on the test env, 15.9 s / 7.1 GB. The suite is enabled in the ignored set (`lake test -- --ignored rust-decompile`). compare_envs' progress lines drop their hardcoded rs_kernel_roundtrip prefix now that two roundtrips share them.
Compile: Mathlib-scale environments in ~17 GB at near-parity wall time
Problem
ix compilematerialized several whole-environment-sized structures at once: afully-decoded Rust copy of the Lean environment (~25 GB at Mathlib scale),
structured metadata for every named constant (~20× larger than its serialized
form), unbounded per-worker kernel-env caches, and an env-sized output buffer
crossing the FFI. Mathlib peaked at ~103 GB (CI-measured) and FLT at 63–68 GB —
neither compiled on ordinary development hardware.
Design
Keep every representation compact except the working set actually being read,
always-on, with every configuration producing a bit-identical
.ixe:demand, behind a bounded lock-partitioned cache, instead of materializing the
whole owned Rust copy up front. The Lean heap already holds the environment;
decode-on-fetch avoids duplicating it.
in-degrees before the scheduler starts; the top 16,384 constants go into a
never-evicted overlay (decode once, lock-free reads), absorbing repeat
decodes of foundational constants that would otherwise churn any bounded
cache.
their serialized bytes and decoded on the rare re-read.
passes share one whole-env decode instead of three.
.ixewrites straight to disk from Rust (.tmp+atomic rename); no env-sized ByteArray crosses the FFI. The CPU-heavy named
section encodes in parallel in bounded chunks.
(a pure cache; clearing is semantics-free).
Hardcoded sizes (cache entries, pin set, segment count) are justified by sweeps
recorded in the commit messages; the segment count scales with hardware
threads.
Knobs
IX_COMPILE_WORKERS=N— scheduler worker count (default: all cores).IX_COMPILE_DEMOTE=0— keep structured caches for flows that re-read thecompiled env in-process.
IX_COMPILE_EAGER=1— decode the whole environment up front on RAM-richmachines, trading the largest memory term back for the last few percent of
wall (FLT: −8% for +13 GiB; Mathlib requires a large-memory machine).
Results
Local (24 cores, 50 GB hard cap; wall from the compile step):
CI (32-core runner,
!benchmark): InitStd 1.09× faster than main at 3.1×less RAM; Mathlib 5.4× less RAM at +13.7% wall. The residual is repeat-decode
cost that grows with core count (fixed decode CPU over shrinking compute); it
is bounded above by the
IX_COMPILE_EAGER=1configuration, which the benchmarktooling can now measure directly.
Byte-identity is verified against the pre-branch binary (
cmponInitStd/Lean; FLT/Mathlib have a pre-existing ±tens-of-bytes named-section
nondeterminism unrelated to this PR).
Also in this PR
!benchmark:IX_COMPILE_*knob passthrough reaches the measured compile(cache keys include the knob config, so knob runs publish their own rows).
test-ffifeature builds fixed for the newEnvAPI (CI'sclippy --all-featuresgate).Namedmetadata accessor.rust-decompilesuite stays disabled with an accurate note: Rustdecompile of synthesized
_sparseCasesOnaux constants fails on main too(
missing Ref metadata) — pre-existing, tracked separately.Follow-ups
!benchmark compile BENCH_ENVS=Mathlib IX_COMPILE_EAGER=1tobound the many-core residual; if capacity proves to be a worthwhile dial
there, scale the lazy cache with runner RAM the way segments scale with
threads.
_sparseCasesOndecompile metadata bug upstream.