Uh oh!
There was an error while loading. Please reload this page.
Universe-level canonicalization and Decompilation bugfix - #541
Merged
Conversation
Whole-Mathlib validate-lean previously held the canonicalized source env from phase 1 through phase 5 as the decompile-comparison oracle (plus the elaborated Lean env for its whole run), on top of the decompile working state — several whole-env copies resident at once, which pushed a 124 GiB box deep into swap. Phase 5 now compares per-name 64-bit digests by default: derive Hashable for the Ix constant types (same field coverage as the derived BEq, O(1) at the hash-consed Name/Level/Expr leaves), digest the canon view right after phase 1, and let the whole canon env free with the phase-1 output. The decompiler runs with origEnv? := none — its per-recovery debug track is subsumed by the digest comparison at gate level. The Lean source env is released after phase 4 (its last reader). Collision odds at 205k constants are ~1e-14, and any reported mismatch is re-checkable structurally: --full-oracle restores the old whole-env BEq path + decompiler debug track, intended together with --ns to debug a digest mismatch on a small closure.
`compileLeanConsts` previously canonicalized the whole environment into one map and held it through compile — at whole-Mathlib scale that map plus the elaborated Lean env and the compile state peaked past physical RAM (~180 GiB total footprint) regardless of worker count. The driver now streams: - A name-only pre-pass canonicalizes names, building the lazy-lookup key map, the reverse name-hash view for nameForAddr, and a THIN ground-check env — groundExpr/groundConst read only name-existence and is-it-a-ctor, so two shared placeholder constants stand in for every value. - The canon pass (chunk-parallel) canonicalizes each constant TRANSIENTLY, extracting its ref set (graphConst reads nothing else), immediate ground error, and content digest. Proof bodies (thmInfo / opaqueInfo — the bulk of Mathlib, never read by dependents) are then dropped; code kinds (definitions, inductive families, ctors, recursors — read repeatedly and with retention by aux-gen and kernel ingress) are kept and become the materialized map, preserving shared structure and O(1) dependency reads. - Compile runs against the hybrid env: `Ix.Environment` gains a pure `fallback?` resolver consulted on `consts` miss (`Environment.get?`), wired through findConst, CallSiteSurgery, and compileConstNoAuxPure (aux-gen lookupConst? follows in the level-aware aux identity change). A proof body is canonicalized on demand for its own block and freed when the block returns. Materialized-env callers (every test/gate and the decompile side) leave fallback? none and are bit-for-bit unaffected. - Per-name digests ride out via LeanPipelineOut.digests; validate-lean digest mode consumes them directly, and --full-oracle materializes the whole view post-hoc only when explicitly requested. - nameForAddr gets a nameByHash map (CompileEnv, threaded through the aux driver entry points) since the streaming env has no consts keys to scan; the materialized-env scan is preserved as fallback. Canon is per-constant deterministic (chunking was already arbitrary), so compiled output is byte-identical — verified on the 191,506-constant Ix-library env: phase 1 reproduces 472,653,224 bytes / 186,459 blocks exactly, serde byte-identical, phase 5 all 191,506 constants digest-identical, wall time within 6%. On that code-heavy env the peak is compile-state-bound (~unchanged); the win scales with the proof fraction, i.e. with Mathlib. lake test green.
`CompileEnv.constants` / `ParallelState.constants` store SERIALIZED bytes instead of structured `Ixon.Constant`s. The structured map retained a whole-env-scale object graph for the entire compile; the bytes already exist when a block merges (`result.blockBytes` / `projBytes`), readers needing structure parse on demand (`Ixon.deConstantAt` — only the commit-open path), and assembly wraps entries as byte-backed `Ixon.LazyConstant`s (`cache := none`), the representation whose lazy-load path already keeps mathlib.ixe cheap. Rust peaks ~20 GiB on the same compile largely because compiled output lives as bytes; this is the same architecture. Measured on whole Mathlib (736,624 constants, 726,519 blocks): driver-retained state grows only ~16 GB across the entire compile — RSS flat from 44.8 GB at 20k blocks to 60.9 GB at 720k, with the attribution trace (IX_COMPILE_DBG=1: phase timings + live per-20k-block RSS/structure sizes) pinpointing the remaining spike as the transient working set of the final straggler waves, not retention. aux-gen-diff: serialized envs byte-IDENTICAL vs Rust through the new path, sequential + parallel drivers; lake test green.
…nonicity 10.5, 17.8)
Two fixture-driven repairs to the universe-aware nested-aux dedup introduced by #532, mirrored Rust <-> Lean throughout. 1. Lean mirror lambda-precedence bug (term axis, IxVMInd.DedupM). In Ix/AuxGen/Recursor.lean the dedup wrote (levels.zip levelHashes).all fun (a, b) => a == b && hashes.size == specHashes.size && ... and the lambda body swallowed the remaining conjuncts, so for a non-universe-polymorphic family (empty level list) the vacuous .all skipped the spec-param comparison entirely — Bar2<DedupM,Nat> and Bar2<DedupM,Bool> collapsed to one aux (2 motives instead of 3), failing decompile-diff aux-fidelity + the .rec roundtrip while Rust (explicit closure bounds) stayed correct. Parenthesized; pinned by a RecursorTests fixture (termSpecializedNested*). 2. Universe axis (new fixture IxVMInd.UnivM: PhantomBox.{0}/.{1} with the same term spec param — Lean emits distinct motives; #532 covered this at the flat-block dedup only, and no corpus fixture existed). Three downstream sites still keyed aux identity on (family, term specs) alone and are now level-aware, each with an exact-levels pass first and a level-insensitive fallback (alpha-collapse can rename a block's universe params between source and canonical): - compute_aux_perm source-canonical matching (nested.rs + AuxGen/Nested.lean): both source auxes previously mapped onto the first canonical slot, leaving slot #1 uncovered ("canonical aux #1 has no source mapping", the whole-block failure that kept this shape out of the corpus). - match_classes_against_app (recursor.rs + AuxGen/Recursor.lean): ctor-field class matching returned the first spec-matching class for both occurrences. - NestedRewriteCtx.aux_info (recursor.rs/expr_utils.rs + AuxGen/Recursor.lean/ExprUtils.lean): keyed HashMap<Name, entry>, so same-name entries overwrote and one instantiation's levels were stamped onto every occurrence (the "Succ vs Zero" congruence failures on .rec/.below/.brecOn). Now multi-valued per name: exact-levels entry preferred (identity — members store raw ctor levels post-#532), last entry as the legacy fallback for the genuine recompute case (Array.{u} occurrence vs Array.{max u v} member). source_aux_order_from_expanded widens to carry head levels; the public source_aux_order* wrappers are unchanged. AuxGen lookupConst? also routes through Environment.get? (the parent change's streaming fallback). Gates with UnivM seeded into the corpus: validate-aux 0 failures, aux-gen-diff all gates PASS (patches 1569, serialized envs byte-identical), decompile-diff all gates PASS (5442 consts, 0 errors, 0 mismatches), cargo test -p ix-compile 231 passed, clippy clean, lake test PASS.
…anonicity 10.5)
Two fixes making synthesized-expression metadata names a deterministic,
source-faithful function of the block (provenance rule, canonicity 10.5):
- whnf_lean's source-name hint map keyed by KExpr::hash_key(), which is
an intern uid — fresh for every un-interned to_kexpr_static
construction — so collect-time and restore-time keys never matched and
the restoration pass restored nothing. Key both sides with
kexpr_content_key, a pure name-erased structural digest mirroring the
ExprKey / Lean Ix.Tc content-address equivalence, and make the WHNF
no-op test structural (==) rather than uid equality. This was the
whole-Mathlib 47-byte divergence (Quiver.FreeGroupoid.redStep.{rec,
casesOn,recOn}: HomRel (Paths (Symmetrify V)) reducts intern-collapsed
to 'Paths (Paths V)' with restoration dead).
- compile_env worker loop and aux_gen prereq loop reused one KernelCtx
across blocks: name-erased caches replay alias display names recorded
by earlier blocks on the same worker, schedule-dependently. Fresh
KernelCtx per block compile (checker and aux-dump paths already were).
Fixture: Canonicity.AliasProvenance — cross-block alpha-identical
wrapper defs referenced at two spellings in one expression, both
orientations, through a reducible index wrapper (the HomRel shape) and
as sibling constructor fields. Benchmarks/Compile/CompileRedStep.lean:
228k-const repro closure (Rust 10.5s; compile-lean --rust-check is the
aligned gate).
Result: whole-Mathlib Rust and Lean outputs byte-identical
(3,152,009,710 bytes, 736,624 consts; Rust wall +2.5%).The anon-roundtrip comparator canonicalizes both sides and compares. canonExpr's only memo was .share-INDEX-keyed, which linearizes parsed constants (explicit .share nodes) but re-materializes every pointer-shared subtree of an EGRESSED constant per occurrence — exponential tree unfolding. At whole-Mathlib scale phase 3 of validate-lean spiked past 100 GiB (multi-GiB transients from KB-sized deeply-shared constants, thread-count independent) and, once the memory was fixed, the derived tree-walking == burned 5.6 hours on the same DAGs. - canonExprImpl: @[implemented_by] runtime twin with a call-local pointer-identity memo over composite nodes (ShareCommon soundness argument: immutable values, non-moving RC heap, keys are subtrees of the live root). Canonical outputs now pointer-share repeated substructure, so equal shared inputs yield the SAME output object. - exprEqDag / constEqDag: pair-pointer-memoized equality used by roundtripCompare (reference semantics: plain ==). Covers all ConstantInfo variants including Muts members. 14k-item sequential slice: 73.4 GiB / 460 s → 5.1 GiB / 13.2 s. Full 647,127-constant phase 3: >100 GiB OOM → PASS at modest memory.
Whole-Mathlib validate-lean died in phase 2, not compile: serdeGate's deEnv materializes every constant and metadata arena and serEnv rebuilds the whole 3.1 GB image to compare — a >100 GiB resident spike measured in isolation (--ixe mode, no Lean env pinned), with the 48 GiB Lean import still resident for phase 4 in a real run. Phase 4 would have stacked a third whole-env copy (the merged meta KEnv) on top. - Ixon.getEnvVerifiedLazy / deEnvVerifiedLazy: streaming verified load. Every unit is parsed with the pure reader, re-serialized with the pure writer, and compared against its input span, spans covering the image gaplessly; order/root/trailing contracts the whole-image compare used to pin are asserted directly (§1/§2/§6 address order, §5 name order, §4 order equal to topologicalSortNames of the parsed set). Constants are retained as zero-copy LazyConstant.ofSlice windows and §5 rows as NamedRow metadata windows, materialized per name on demand. Coarse dbgTrace progress markers (stdout is block-buffered mid-run). - Tc.serdeGateStreaming: the gate over the new loader. - Tc.metaRoundtripEnvStreaming: chunks respect block boundaries (meta ingress resolves Muts SIBLING names), work is enumerated from a chunk-only named table while ingress-time name→address resolution reads the chunk overlaid on a whole-env ADDRESS-ONLY stub table (cross-block references read just .addr; enumerating stubs as work ingresses their empty metas — the two roles must be split). Per chunk: materialize → chunk-local ingress → egress → compare → drop; the whole-env merged MetaEnv never exists. IX_META_EAGER=1 keeps the eager driver as a closure-scale oracle: verdicts are IDENTICAL (217,324 checked / same 2 findings on the redStep closure). - validate-lean wires phases 2-4 to the lazy parts; phase 5 interim: materializeAll (named + cached consts) after the Lean env is released. - EgressLean diff describer now prints both level lists on levels-differ mismatches. - Memory-diagnosis knobs (all env-gated, zero default cost): IX_ANON_CAP / IX_ANON_SEQ / IX_ANON_STAGE / IX_SKIP_PHASES / IX_ANON_HOLD / IX_META_EAGER; CompileDriver: IX_LOG_BLOCKS tail-gated per-block BEGIN/END trace. Whole-Mathlib result (with the DAG-compare fix in the parent commit), 124 GiB box, --workers 8, peak 95.9 GiB, no swap: 1 compile PASS 3,152,009,710 B / 726,519 blocks / 0 ungrounded (1035 s) 2 serde PASS streaming gate, all units byte-identical (235 s) 3 anon PASS 647,127 constants structurally preserved (42 s) 4 meta 714,235 checked / 111 'levels differ' findings (171 s) 5 decomp PASS 736,624 digest-identical to canonical source (4269 s) The 111 phase-4 findings are one PRE-EXISTING class, independent of this change (the eager oracle reproduces them bit-for-bit): universe LEVEL normal forms disagree between the kernel meta egress path and CanonM at value-position occurrences of ubiquitous constants (DFunLike.coe, List.nil, PSigma.casesOn in WF-recursion eq_defs, …) — 0.016% of checked rows; phase 5 passing whole-Mathlib shows the stored artifacts are faithful and the gap is in phase 4's direct comparison. Tc-ingress/egress territory.
… 10.6 stage 2) Phase 1 of plans/level_canonicalization_rust_first.md — the Rust pipeline end-to-end on the Géran-canonical univ-table spec: - compile: preseed canonicalizes tables (canon_univ before sort; every primary entry canon-fixed), compile_univ_idx interns canonical forms and mints virtual indices (univs.len + slot) into per-constant metaUnivs; sort/const/rec arms emit univPatches keyed by arena root (const patches carry the FULL arg list); BuildCallSite clones a head patch onto the CallSite root (the head's own Ref root is unreachable by replay); V3 preseed-finality debug tripwire. - decompile: patch replay at sort/ref/rec arms + call-site head via load_meta_extensions' arena-index map; ctor window installs per-ctor extensions at the PRIMARY table offset (parent extension displaced), and clears the pointer-keyed univ memo per ctor — demoted metas re-parse per access, so ctor-scoped extension Univs are ephemeral and freed addresses could collide in the memo (the jcb-caught flaky Std.DHashMap.Raw.WF Subtype.mk spelling bug; 8/8 repro now clean). - kernel ingress: decorations sourced from univPatches (virtual space univs ++ metaUnivs) at sort/ref/rec + both call-site head arms, with the stage-1 mk*-rebuild rule as fallback (never fires on canonical tables, P3; keeps raw-table fixtures exercised). - kernel egress (ixon half): EgressCtx preseeds the univ table verbatim from the ORIGINAL constant so the rebuilt layout matches the original meta's patch index space by construction (V1: measured — rebuilt first-use tables diverge from originals on 61%/98% of bodies and only the absence of meta table-refs hid it); decor-interning dropped — kexpr_to_ixon always emits the kernel-held canonical level. - level.rs: norm_level_eq ignores empty subsumption entries (O1 option (b)) — univ_eq is now the exact semantic quotient; Mathlib witness pair pinned with an eval-certified vector. - prim_addrs.rs: 56 canonical pins regenerated (build-primitives parity green); LEON new_orig pins unchanged as expected. Validation: cargo suites green (kernel 674, compile 234); validate-aux 0 fail; rust-compile 0/228,770 (incl. 577 MB serde roundtrip); kernel-ixon-roundtrip 0/150,396; whole-Mathlib ix validate 0/736,624 (all 8 phases, 3.16 GB serde); regenerated compileinitstd/redstep.ixe; census probe on the new artifact: Géran-noncanonical 0 entries, collision constants 0, src==canonical bytes.
… stage 2, Lean mirror) Phase 2 L1 of plans/level_canonicalization_rust_first.md — mirror of the Rust compile half: preseed canonicalizes the primary univ table (canonUniv before sort; univsFinal V3 tripwire), compileAndInternUnivCanon interns canonical forms and mints virtual indices into per-constant metaUnivs, sort/const arms emit arena-root-keyed univPatches (const patches carry the FULL arg list), buildCallSite clones a head patch onto the callSite root (the head's own arena root is unreachable by replay), and every per-constant meta assembly drains the channels.
…(canonicity 10.6) Phase 2 L4 — mirrors the Phase-1 prim_addrs.rs regen: 56 canonical pins in Ix/Tc/Primitive.lean and 45 IxVM address literals (NatPrim 33, Infer 11, InferOnly 1), keyed old-hex→new-hex from the Phase-1 diff. LEON orig pins unchanged. prim-addrs gate (whole-toplevel literal scan) and tc-unit primsParity green.
Each phase now prints its section heading + result the moment it completes (flushed), with phase-start markers before the long legs and a final summary + RESULT line matching ix validate's format. End-only block-buffered output twice cost us the evidence of how far a killed whole-Mathlib run got.
…ce (canonicity 10.6, Lean mirror) Phase 2 L2+L3 of plans/level_canonicalization_rust_first.md: - DecompileM (L2): BlockCtx.univPatches arena-index map from ConstantMeta; replay at sort/ref/recur arms and the surgered call-site head (patch cloned onto the callSite root by the compiler). Patch indices resolve through the ctx's already-extended univs ++ metaUnivs. The per-constant withFreshBlock design (fresh immutable ctx + fresh caches, primary ++ own extension per ctor) is structurally immune to the two Rust decompiler hazards fixed in Phase 1 (parent-extension displacement; stale univ-memo entries). - Tc IngressMeta (L3): decorations sourced from univPatches (virtual space univs ++ metaUnivs; arity-checked full-list const patches) at sort/ref/recur and both callSite head arms, with the stage-1 reduceIxonUniv-fixpoint rule as fallback (never fires on canonical tables, P3; keeps raw-table fixtures exercised). Module-doc contract updated: metaUnivs/univPatches are now META-ingress-read; anon stays metadata-blind. - Tc Egress (L3): phase 3 STRICT — both canonExpr bodies intern stored universe trees EXACTLY (reduceIxonUniv dropped; canonical tables are its fixpoints); module doc reworded, pre-normal-levels artifacts now fail the roundtrip by design (D4). - Tc Level + IxVM Levels (R5 mirror, option (b)): normLevelEq / nl_eq ignore empty subsumption entries (nl_skip_empty), making univEq / level_equal the exact semantic quotient, matching Rust norm_level_eq. Gates: tc-unit 390, decompile-unit, prim-addrs 80, ixvm, aux-gen-diff (byte-identical incl. wrapper vectors), decompile-diff (aux-fidelity 2243/0), tc-ingress-meta, tc-roundtrip (148,387 meta-checked) — all green.
Drop the staged banners and row markers; record the landed linearizer (per-atom gate inversion — formerly O1), the empty-entry-insensitive univEq (exact semantic quotient), the patch-first decoration source with the stage-1 fallback and the callSite-head re-key; add the 12.4 level-spelling-twin worked example; rewrite 17.9 as the landed record with the acceptance evidence (whole-Mathlib validate/validate-lean 0 failures, phase 4 714,346/0, byte-ALIGNED compilers, probe Géran-noncanonical 0). Ixon.md: univ-table canonicity invariant and the ConstantMeta wrapper struct with all four extension vectors incl. univPatches.
Regenerated .ixe sizes (canonical tables + univPatches), Mathlib compile/serialize timings from the ALIGNED runs, and the whole-Mathlib validate-lean column that was TBD pending the below.rec fix: phases 999.1 / 232.3 / 41.2 / 183.8 / 3,926.3 s, ~89.7 min total, 0 failures. Footnote for the phase-3 inversion (older InitStd/Lean figures predate the pointer-memo canonical compare).
…univ kernel (canonicity 10.6) The 10.6 kernel changes (nl_skip_empty empty-entry skip in nl_eq + regenerated primitive address literals) change the generated Aiur image: regenerate crates/ixvm-codegen/src/aiur_ixvm.rs via ix codegen (aiur_multi_stark.rs regenerates byte-identical) and acknowledge the resulting FFT cost shifts — 66 kernel-check pins and the shard pipeline pin, all within ±0.3%, every functional/parity check green (728 passing).
manual_contains in the diff probe; documented needless_pass_by_value allows on the quickcheck properties (the macro requires by-value Arbitrary arguments).
normLevelEq_eval rewritten for the empty-entry-insensitive comparator (canonicity 10.6 R5): the positional zip check makes the two entryNonEmpty-filtered entry lists literally equal, and dropped entries evaluate to 0, so equal denotations follow by le-antisymmetry through eval_le/le_eval — simpler than the old pigeonhole-over-sorted-keys argument. entryNonEmpty hoisted to a named def in Ix/Tc/Level.lean so the proofs can speak about it (comparator unchanged). AnonStructural's anon ExprInfo mirror gains the seventh (unit) univDecor field. Statement of normLevelEq_eval unchanged; trust audit passes for all 7 theorem roots (lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Statements green).
dump_reducible_univs / dump_named_metas / dump_const_sizes are env-driven manual probes (IXE_A=<path> cargo test -- --ignored --nocapture); CI's run-everything-ignored sweep (nextest --run-ignored all) force-runs them without inputs, where the expect on IXE_A panicked. They now print a skip note and return, keeping the sweep green without losing the documented manual usage.
samuelburnham
commented
Aug 7, 2026
Member
!benchmark compile decompile |
Contributor
|
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
FLT | 33.894 s | 33.247 s | -1.9% | 15.07K | 15.36K | +1.9% | 12.67 GiB | 12.59 GiB | -0.7% | 1.68 GiB | 1.68 GiB | +0.1% | 510,687 | 510,687 | +0.0% |
compile · InitStd — main from: base run @ 62be8e9 (not on bencher)
1 env · 1 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 3.978 s | 3.755 s | -5.6% (1.06× faster) 🟢 | 26.52K | 28.09K | +5.9% (1.06× faster) 🟢 | 3.49 GiB | 3.60 GiB | +3.2% | 301.08 MiB | 301.20 MiB | +0.0% | 105,492 | 105,492 | +0.0% |
compile · Lean — main from: base run @ 62be8e9 (not on bencher)
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Lean | 6.898 s | 7.179 s | +4.1% | 27.40K | 26.33K | -3.9% | 5.00 GiB | 5.03 GiB | +0.5% | 448.38 MiB | 448.62 MiB | +0.1% | 188,999 | 188,999 | +0.0% |
compile · Mathlib — main from: base run @ 62be8e9 (not on bencher)
1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib | 54.951 s | 46.666 s | -15.1% (1.18× faster) 🟢 | 13.41K | 15.78K | +17.8% (1.18× faster) 🟢 | 18.28 GiB | 18.41 GiB | +0.7% | 2.94 GiB | 2.94 GiB | +0.1% | 736,618 | 736,618 | +0.0% |
decompile · FLT — main from: base run @ 62be8e9 (not on bencher)
1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
FLT | 1m 10.2s | 1m 10.1s | -0.1% | 7.28K | 7.29K | +0.1% | 18.40 GiB | 18.92 GiB | +2.8% | 1.68 GiB | 1.68 GiB | +0.1% | 510,687 | 510,687 | +0.0% |
decompile · InitStd — main from: base run @ 62be8e9 (not on bencher)
1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 5.756 s | 5.889 s | +2.3% | 18.33K | 17.91K | -2.3% | 3.59 GiB | 3.62 GiB | +0.7% | 301.08 MiB | 301.20 MiB | +0.0% | 105,492 | 105,492 | +0.0% |
decompile · Lean — main from: base run @ 62be8e9 (not on bencher)
1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Lean | 11.866 s | 11.996 s | +1.1% | 15.93K | 15.76K | -1.1% | 5.00 GiB | 5.03 GiB | +0.7% | 448.38 MiB | 448.62 MiB | +0.1% | 188,999 | 188,999 | +0.0% |
decompile · Mathlib — main from: base run @ 62be8e9 (not on bencher)
1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib | 3m 14.4s | 3m 15.5s | +0.6% | 3.79K | 3.77K | -0.6% | 31.11 GiB | 31.76 GiB | +2.1% | 2.94 GiB | 2.94 GiB | +0.1% | 736,618 | 736,618 | +0.0% |
arthurpaulino
approved these changes
Aug 7, 2026
Uh oh!
There was an error while loading. Please reload this page.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Universe-level canonicalization (canonicity §10.6), alias-provenance metadata (§10.5), and whole-Mathlib scaling of the pure-Lean validator
This branch lands three related bodies of work, culminating in the §10.6 universe-level quotient: content addresses now coincide with the kernels' semantic level equality, with source spellings preserved losslessly in metadata. Whole-Mathlib validation is green in both implementations, strict everywhere, with the two compilers byte-identical.
Part I — Canonicity §10.5: metadata name provenance (prerequisite fixes)
The whole-Mathlib byte-parity investigation surfaced a 47-byte divergence (
Quiver.FreeGroupoid.redStep.{rec,casesOn,recOn}): the kernel's WHNF intern-collapsed alpha-identical wrapper defs (Paths/Symmetrify) to first-interned spellings, making synthesized metadata name choices schedule-dependent.compile: block-scope kernel contexts).KExpr::hash_key()is an intern UID while LeanTc.KExpr.addris a content digest — the source-name hint map keyed byhash_keyhad never matched (dead since birth). Fixed with a name-erased structural content key mirroring the two kernels' induced equivalence rather than their accessor spellings.aux_gen): three sites still matched auxes by (family, term-specs) only, collapsing distinct universe instantiations (DedupM/UnivMfixtures); all three now key on levels with an exact-then-insensitive two-pass, mirrored Rust↔Lean.Part II — Whole-Mathlib scaling of
ix validate-leanThe pure-Lean validator previously could not complete Mathlib (several independent >100 GiB blowups). Now it completes in ~90 min at <100 GiB:
deEnvVerifiedLazy) instead of whole-env materialization.Tc.canonExprand derivedBEqexponentially unfolded pointer-shared DAGs on egressed constants (multi-GiB transients from 2 KB constants; 5.6 h of comparison). Both are now pointer-memoized (ptrAddrUnsafe, soundness argument in-module): 73.4 GiB/460 s → 5.1 GiB/13.2 s on the bisection slice, 41 s for all of Mathlib.validate-leannow prints each phase's section heading + result the moment it completes, flushed (block-buffered end-only output twice destroyed the evidence of killed runs), matchingix validate's format.Part III — Canonicity §10.6: the universe-level quotient
The quotient. Two levels are identified exactly when the kernels' semantic equality (
univEq) holds — the endpoint quotient: content addresses coincide with kernel identity. Spellings are presentation. Declaration-level parameter list order stays structural; only spelling inside level expressions is quotiented (max u v=max v u;(max u v)+1=max (u+1) (v+1); the WF-recursioneq_defshapes).Canonical representative.
canonUniv = linearize ∘ subsumption ∘ normalizeAux— the kernels' Géran comparison form, linearized back into a term by per-atom gate inversion (each atom self-strips gates its value dominates; gate order recovered greedily outermost-first; formerly open detail O1, settled empirically). Properties P1–P6 (idempotence, roundtrip-fixpoint, mk*-fixpoint, kernel-oracle soundness, Rust↔Lean byte parity, mk* absorption) are pinned exhaustively over all ≤7-node terms plus 50k quickcheck, in both languages, with FFI cross-checks.univEqis now exact (option (b)): the normal-form comparison ignores empty subsumption entries (asnormLevelLealways did) in all three kernels (Rust, Lean Tc, IxVM). Before this, 3 of 3,253,373 whole-Mathlib entries were distinguished from their semantic equals.Restoration metadata. Per-occurrence
ConstantMeta.univPatches(arena-node-keyed; full argument lists for const occurrences) + ametaUnivsextension table under the virtual-index contract, as a fourth wrapper vector in both serializers (+ FFI codec, diff labels, generators, fixtures). Table-keyed patching is unsound (canonicalization dedups distinct spellings onto one entry — 79,088 Mathlib constants contain a collision); arena keying is exact because expression identity is spelling-injective. One structural subtlety mirrored everywhere: a surgered call-site head's arena root is unreachable during replay, so its patch is cloned onto the callSite node root.Kernel contract. Anonymous ingress never reads patches (they influence no hash and no judgment). Meta ingress decorates occurrence nodes with original spellings — folded into
metaAddronly, neveraddr(anon/meta parity preserved; checking never sees spellings) — sourced from patches with the stage-1 mk*-rebuild rule as the patchless fallback. Meta egress replays decorations. Comparators were never weakened; with canonical tables the anon roundtrip dropped itsreduceIxonUnivmodulo and is now strict.Execution order (per plan): stage 1 (decorations, no format change) → census probe → stage 2 Rust-first (compiler + kernel end-to-end on Rust-only gates) → Lean mirror against the cross-compiler gates → format break with a "pre-normal-levels .ixe; recompile it" parse hint → primitive-pin regeneration everywhere (
prim_addrs.rs,Ix/Tc/Primitive.lean, IxVM address literals — 56 pins; LEON pins unchanged) → Aiur codegen regeneration + FFT cost re-pins (66 pins, all within ±0.3%, every functional/parity check green).Probe (
dump_reducible_univs, kept as a permanent census tool): whole-Mathlib blast radius was 373,799 Géran-noncanonical entries in 134,929 constants (~1.04 M occurrences, ~10.9 MB patches, 0.34%), 84% dependent closure. Post-regen artifacts:Géran-noncanonical: 0, collision constants 0, src == canonical bytes.Bugs found and fixed along the way
univPatcheswould have been the first. Egress now preseeds each rebuilt univ table verbatim from the original constant (pairing exact by construction, debug-asserted).Std.DHashMap.Raw.WFre-run): demoted metas re-parse per access, so ctor-window extension univs were sole-owner allocations; freed addresses collided in the decompiler's*const Univ-keyed level memo, substituting arbitrary stale spellings allocator-dependently. Fixed by invalidating the memo at the window; regression-pinned with a multi-ctor patched-inductive fixture. (The Lean decompiler's per-constantwithFreshBlockdesign is immune by construction.)metaUnivsmust install at the primary table length, not the parent-extended length (latent until extensions became non-empty).Validation
ix validate(Rust 8-phase), whole-Mathlibix validate-lean(pure Lean 5-phase), whole-Mathliblevels differfindings); phase 5 all digest-identicalcompile-lean --rust-check, RedStep + MathlibDocs: §10.6 rewritten as live spec (linearizer + exact
univEq+ patch contract), §12.4 worked example, §17.9 landed record;Ixon.mduniv-table invariant + ConstantMeta wrapper layout.BENCHMARKS.mdrefreshed (regenerated artifact sizes, Mathlib timings, previously-TBD validate-lean column).Follow-ups (tracked in §17.9): kernel-side univ-table canonicity enforcement at ingress (reject, never silently canonicalize; all three kernels + foreign-
.ixepolicy); Tc Verify-layer proofs of P1/P2/P4.Format break: pre-existing
.ixeartifacts are invalidated (parse error with a recompile hint); regenerate-everything was the adopted policy (D4).