feat: Add `ix decompile` CLI, fix Rust decompile perf and tests by samuelburnham · Pull Request #490 · argumentcomputer/ix

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham · 2026-07-13T21:29:45Z

#484 made ix compile use much less RAM by keeping the environment as compact bytes instead of decoded data. Reading those bytes back costs extra work, and the flows that do read them — decompile and validate — were never measured. This branch fixes what broke and makes those flows memory-lean too.

Fixes. Two things broke in the ignored-test CI:

A kernel test that plants a corrupted constant stopped working: the new store logic skips writes to an address that already exists, so the corruption was never written and the test passed for the wrong reason.
Decompile re-decoded the entire metadata section once per mutual block instead of once total: 848s where it used to take 8.8s. Building a lookup index once up front brings it to 3.2s.

CI goes from 23.5 minutes red to ~11 minutes green.

Memory. Decompiled constants used to each hold their own copy of every common subexpression; now identical subexpressions are stored once and shared. Loading an env file keeps metadata in its compact form instead of decoding all of it up front, and validate reads the Lean env on demand instead of copying all of it into memory. One behavior at every scale, one opt-out knob (IX_COMPILE_EAGER=1). Results:

Mathlib decompiles on a 56 GB machine for the first time: 737k constants, ~4 minutes, ~30 GiB peak.
FLT ix validate used to run out of memory; it now finishes at 38.7 GiB with 0 failures.

Benchmarks. New ix decompile <env>.ixe command — the inverse of ix compile. It measures with the same texray infrastructure as ix compile --json, so the two rows share semantics. It's wired into the bench system: !benchmark decompile works on PRs, and merges to main track decompile time, throughput, and peak RAM on bencher.dev, alerting on ±10% changes. It also composes with #474's bundles: a self-contained ix pack bundle decompiles (validated closed first), and a thin bundle is rejected up front with a clear error.

Tests. The disabled rust-decompile test is replaced. The old one sent the env through a conversion step used by nothing else, and that step dropped the metadata decompile needs to recover tricky constants — so its failures were about the conversion, not decompilation. The new test runs the real pipeline (compile → serialize → load → decompile → compare every constant against the original) and passes: 143,697 of 143,697 match.

… 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.

`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.

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.

samuelburnham force-pushed the sb/ix-decompile branch from ceaf6a4 to 6dd0c6dCompare July 13, 2026 21:58

samuelburnham marked this pull request as ready for review July 13, 2026 21:58

samuelburnham requested a review from johnchandlerburnham July 13, 2026 21:58

johnchandlerburnham previously approved these changes Jul 14, 2026
View reviewed changes

samuelburnham dismissed johnchandlerburnham’s stale review via 9883651July 14, 2026 14:40

samuelburnham force-pushed the sb/ix-decompile branch from 6dd0c6d to 9883651Compare July 14, 2026 14:40

samuelburnham requested a review from johnchandlerburnham July 14, 2026 14:53

samuelburnham enabled auto-merge (squash) July 14, 2026 15:07

samuelburnham added 3 commits July 14, 2026 11:18

johnchandlerburnham previously approved these changes Jul 14, 2026
View reviewed changes

samuelburnham dismissed johnchandlerburnham’s stale review via ba9a104July 14, 2026 19:42

samuelburnham force-pushed the sb/ix-decompile branch from 9883651 to ba9a104Compare July 14, 2026 19:42

johnchandlerburnham approved these changes Jul 14, 2026
View reviewed changes

samuelburnham merged commit e94c81a into mainJul 14, 2026
17 of 18 checks passed

samuelburnham deleted the sb/ix-decompile branch July 14, 2026 19:55