IxVM Aiur kernel: drive mathlib shard 0 to green by arthurpaulino · Pull Request #485 · argumentcomputer/ix

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino · 2026-07-11T01:17:59Z

Summary

ix check --ixe mathlib.ixe --ixes mathlib.ixes --shard 0 died with an
opaque assert_eq mismatch: 0 != 1. Driving it to green surfaced four
independent correctness divergences between the Aiur kernel and its Rust
mirror, one shard-scale performance pathology, and some missing debugging
infrastructure. All are fixed here: shard 0 (9,357 owned constants of the
647,127-const mathlib env) typechecks end-to-end through the native
codegen kernel, lake test -- --ignored ixvm is green (599 assertions),
and the FFT pins land within ±1.1% of main (median ratio 0.997) — the
kernel surgery is cost-neutral.

Kernel fixes

Canonical block sort compares constructors (CanonicalCheck.lean).
The Indc comparator stopped at the inductive's type, so same-shape
mutual inductives (Mathlib.Tactic.Ring's ExBase/ExProd/ExSum:
identical flags, arities and types, differing only in ctor types)
collapsed into one alpha class and the block was rejected. Now mirrors
compare_kindc's ctors tail, with a real KMutCtx (same-class members
share one index; ctors mapped at i + cidx), address-based external-ref
comparison, (fields, rhs)-only rec-rule comparison, and a provably
sufficient refinement fuel bound.
whnf-aware index walks (Inductive.lean). get_result_sort_level
and the motive/rec-type index-domain collectors peeled literal Foralls
only; index binders can hide under definitional wrappers —
inductive εClosure (S : Set σ) : Set σ stores a type ending in
Set σ that only whnf exposes as σ → Prop. whnf before every peel,
mirroring the Rust walks.
Aux synthesis parity + stored-aux validation removal
(Inductive.lean). Synthesized aux types never instantiated the
occurrence's universe args (Type u vs the stored monomorphized
Type 0) and peeled binders structurally; fixed per
canonical_aux_order's construction. The stored-aux validation pass
(validate_block_auxes / is_aux_inductive) is removed outright:
stored Muts blocks only ever contain the source originals (Rust seeds
every stored member is_aux: false; auxes are transient detection
results), and the classification heuristic misclassified originals in
mixed blocks (Lean.Compiler.LCNF's Alt/FunDecl/Cases/Code),
rejecting legitimate envs.
Canonical aux order (Inductive.lean). Stored recursors bake the
compiler's canonical aux order into their motive/minor layout, while
build_flat_block discovers auxes in traversal order. The aux suffix
is now re-sorted by partition refinement over synthetic aux views,
with sentinel positions (|top| + ordinal) standing in for Rust's
synthetic addresses and stable tie handling — an unstable sort
reverses content-identical auxes whose spec params differ only in
phantom parameters (IxVMInd.DedupM) and breaks rec-type matching.

Performance

Block-membership table. derive_block_member_idxs rescanned all of
top per block with per-block memo keys — |blocks| × |top| query-map
entries ate 99% of shard-scale CPU. One shared memoized walk now builds
an rbtree from addr_key(block_addr) to address_eq-confirmed buckets;
each query is an O(log N) lookup.

Tooling

ix name-of: new subcommand resolving a content address back to
its Lean names against a .ixe env — potentially many, since
structurally equivalent constants collapse to the same address (every
matching entry in the env's named table is printed; the one-slot
addrToName index would drop aliases). Unnamed Muts blocks fall back
to scanning for projections into the block — turns an anonymized
failing address into an ix check <name> fast repro. ix addr-of
(name → address) is unchanged.
dbg! prints in the codegen kernel: emitDebug was a silent stub;
it now emits the same println! the bytecode interpreter produces, so
probe builds run at native speed. Production kernels contain no dbg!,
so generated output is unchanged there.
lake exe check shim dropped: it had drifted from ix check
(bool interp flag vs mode string); one entrypoint, no drift.

Validation

Full mathlib shard-0 native run: green, 9,357/9,357 owned consts.
Bytecode repros green for every constant that failed along the way:
Mathlib.Tactic.Ring.ExSum, εNFA.εClosure.step,
Lean.Compiler.LCNF.Cases, plus Lean.Syntax.rec /
IxVMInd.DedupM.rec / IxVMInd.DepthM.rec for the aux machinery.
lake test -- --ignored ixvm: 599 assertions, 0 failures.
verify_bytes_against was stubbed during the debugging campaign and is
restored; final pins include blake3 verification and sit within ±1.1%
of main.

Known follow-ups

Shards 1–63 have not been run (pure machine time; ~300 GB peak RSS per
shard, so sequential on a single box).

arthurpaulino · 2026-07-12T00:26:16Z

!benchmark

argument-ci-bot · 2026-07-12T00:42:27Z

`!benchmark` — main vs `de33f23`

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

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	execute-time (main)	execute-time (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	56.778 s	+3.4% ⚠️	52.610	50.900	-3.3% ⚠️	100.89 GiB	100.61 GiB	-0.3%	11.817 s	12.508 s	+5.8% (1.06× slower) ⚠️	208.4 ms	219.8 ms	+5.5% (1.05× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	42.43B	42.29B	-0.3%
`Array.extract_append`	53.157 s	55.123 s	+3.7% ⚠️	32.090	30.950	-3.6% ⚠️	92.86 GiB	92.66 GiB	-0.2%	12.727 s	13.021 s	+2.3%	210.3 ms	214.2 ms	+1.9%	33.27 MiB	34.43 MiB	+3.5% ⚠️	40.03B	39.96B	-0.2%
`Char.ofOrdinal_le_of_le`	43.097 s	43.778 s	+1.6%	66.410	65.370	-1.6%	76.04 GiB	75.49 GiB	-0.7%	8.947 s	9.087 s	+1.6%	209.1 ms	240.6 ms	+15.1% (1.15× slower) ⚠️	33.27 MiB	34.43 MiB	+3.5% ⚠️	32.73B	32.54B	-0.6%
`Vector.extract_append._proof_2`	31.148 s	32.048 s	+2.9%	46.260	44.960	-2.8%	53.50 GiB	53.32 GiB	-0.3%	6.820 s	7.167 s	+5.1% (1.05× slower) ⚠️	215.8 ms	238.4 ms	+10.5% (1.10× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	23.34B	23.29B	-0.2%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	26.605 s	+1.5%	75.260	74.160	-1.5%	48.88 GiB	48.34 GiB	-1.1%	4.401 s	4.443 s	+0.9%	205.7 ms	222.9 ms	+8.4% (1.08× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	17.43B	17.35B	-0.5%
`String.split`	24.576 s	25.436 s	+3.5% ⚠️	79.300	76.620	-3.4% ⚠️	47.09 GiB	46.75 GiB	-0.7%	4.030 s	4.182 s	+3.8% ⚠️	205.0 ms	219.6 ms	+7.1% (1.07× slower) ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	15.99B	15.89B	-0.6%
`List.mergeSort`	16.628 s	17.267 s	+3.8% ⚠️	96.100	92.540	-3.7% ⚠️	29.84 GiB	29.71 GiB	-0.4%	2.782 s	2.867 s	+3.1% ⚠️	205.2 ms	215.4 ms	+5.0% ⚠️	33.19 MiB	34.35 MiB	+3.5% ⚠️	11.63B	11.58B	-0.4%
`Vector.append`	5.218 s	5.439 s	+4.2% ⚠️	108.480	104.060	-4.1% ⚠️	8.72 GiB	8.90 GiB	+2.0%	529.2 ms	541.8 ms	+2.4%	203.3 ms	233.7 ms	+15.0% (1.15× slower) ⚠️	32.96 MiB	34.12 MiB	+3.5% ⚠️	2.60B	2.58B	-0.5%
`Nat.gcd_comm`	4.158 s	4.382 s	+5.4% (1.05× slower) ⚠️	99.800	94.700	-5.1% (1.05× slower) ⚠️	7.09 GiB	7.01 GiB	-1.0%	349.0 ms	366.4 ms	+5.0% ⚠️	218.0 ms	215.4 ms	-1.2%	32.96 MiB	34.12 MiB	+3.5% ⚠️	1.75B	1.75B	-0.2%
`String.append`	2.973 s	3.063 s	+3.0% ⚠️	118.750	115.250	-2.9%	4.42 GiB	4.57 GiB	+3.5% ⚠️	186.0 ms	189.3 ms	+1.8%	201.0 ms	223.1 ms	+11.0% (1.11× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	967.65M	963.43M	-0.4%
`Int.gcd`	2.350 s	2.469 s	+5.0% (1.05× slower) ⚠️	97.430	92.760	-4.8% (1.05× slower) ⚠️	3.25 GiB	3.27 GiB	+0.6%	121.2 ms	126.6 ms	+4.5% ⚠️	203.0 ms	206.7 ms	+1.8%	32.89 MiB	34.05 MiB	+3.5% ⚠️	605.84M	604.12M	-0.3%
`Nat.sub_le_of_le_add`	2.347 s	2.287 s	-2.6%	80.940	83.090	+2.7%	3.06 GiB	3.06 GiB	-0.0%	95.2 ms	103.9 ms	+9.2% (1.09× slower) ⚠️	204.7 ms	218.8 ms	+6.9% (1.07× slower) ⚠️	32.89 MiB	34.05 MiB	+3.5% ⚠️	510.60M	509.28M	-0.3%
`Nat.add_comm`	1.156 s	1.258 s	+8.8% (1.09× slower) ⚠️	44.100	40.530	-8.1% (1.09× slower) ⚠️	1.43 GiB	1.46 GiB	+2.3%	15.5 ms	16.0 ms	+3.0% ⚠️	194.5 ms	208.9 ms	+7.4% (1.07× slower) ⚠️	32.76 MiB	33.91 MiB	+3.5% ⚠️	53.90M	53.75M	-0.3%
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 21.4s	1m 21.4s	+0.1%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	260.46B	-0.2%

14 constants · 13 regressed · 0 improved (|Δ| > 3.0% on any metric).

Workflow logs

`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address back to its Lean names. Potentially MANY names: structurally equivalent constants collapse to the same content address, so every entry in the env's `named` table pointing at the address is printed, one per line (the `addrToName` reverse index keeps only one name per address and would silently drop the aliases). Addresses of unnamed Muts blocks fall back to scanning for projection constants into the block and printing their names. Turns an anonymized failing address surfaced by the IxVM kernel into an `ix check <name>` fast repro. Lives in its own subcommand instead of overloading `ix addr-of` (name -> address), which stays as-is.

…x walks Two mathlib-blocking divergences from the Rust kernel, found via shard 0 of the mathlib env: 1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never descended into constructors, so same-shape mutual inductives (e.g. Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities and types, differing only in ctor types) collapsed into one alpha class and the block was rejected (assert 0 != 1 in validate_block_canonical). Mirror compare_kindc's ctors tail (canonical_check.rs:299-338) via compare_kctor_idxs_ctx / compare_kctor_pair_ctx, resolving ctor positions through `top`. Further parity fixes in the same pass: * ctx is now a real KMutCtx mirror (from_id_classes): (position, class idx) pairs where same-class members share ONE index (weak- Equal, no position-derived tiebreaks) and each Indc member's ctors map at i + cidx. * External const refs compare by 32-byte address (addr_cmp, lexicographic like Rust's Address Ord) instead of by ingress position, matching the order the compile-side sort produced. * Rec-rule comparison drops the ingress-artifact global ctor idx — (fields, rhs) only, mirroring canonical_check.rs:280-289. * Refinement fuel is 1 + |members| (provably reaches fixpoint) instead of a fixed 32. * Ctx-less compare_kexpr Const arm compares levels before ref (field-order parity; equality-only callers unaffected). 2. Inductive index walks (Inductive.lean): get_result_sort_level and the motive/rec-type index-dom collectors peeled literal Foralls only. Index binders can hide under definitional wrappers — Mathlib's `inductive εClosure (S : Set σ) : Set σ` stores a type ending in `Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died with `no match case for value 3` (KExprNode.App). whnf before every peel, mirroring inductive.rs get_result_sort_level (line 2101+) and build_motive_type_flat (2521-2531). Repros (both now pass): ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode `lake test -- --ignored ixvm` green (599 assertions). Codegen regenerated; FFT pins re-bumped — pin values reflect this branch's stubbed verify_bytes_against and need one more bump when the stub is reverted. Known remaining issue: shard-scale runs crawl inside collect_block_members (per-block O(|top|) rescans whose memo keys make the query map blow up); fix planned separately.

emitDebug was a silent stub, so dbg! probes only printed under --interp bytecode — kernel debugging was pinned to the slowest engine. Emit the same println! the bytecode interpreter's Op::Debug arm produces (label + comma-separated values), with the label escaped for a Rust format-string literal. Production kernels contain no dbg!, so generated output is unchanged there; probe builds now print at native speed.

…red-aux validation Three fixes surfaced by driving mathlib shard 0 to green: 1. Perf: derive_block_member_idxs rescanned the whole `top` list per block, and each scan step's memo key included the block addr — |blocks| x |top| query-map entries dominated shard-scale runs (99% of CPU in QueryMap ops). One memoized walk now builds an rbtree from addr_key(block_addr) to buckets of (full addr, ascending member positions); every query is an O(log N) lookup + address_eq-confirmed bucket walk (4-byte key collisions cost a short walk, never a wrong member list). 2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty / synth_aux_ctor_ty never instantiated the occurrence's universe args, so synthesized types kept `Type u` (Param 0) where the block stores monomorphized `Type 0`; binder peels also assumed literal Foralls. Mirror canonical_aux_order's construction (inductive.rs:1169-1234): instantiate occurrence_us, whnf before each peel. addrs is threaded through the build_flat_block chain for the whnf calls. 3. Stored-aux validation removed: validate_block_auxes assumed Muts blocks store synthesized aux inductives and classified members with is_aux_inductive ("no own nested occurrence but some member has one"). Stored blocks only ever contain the source originals — the Rust kernel seeds every stored member is_aux:false (rs:537) and flags auxes only on transient detection (rs:755) — so the heuristic misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code, where only Cases carries the nested occurrence) and asserted on a legitimate block. Smuggled extra members remain rejected by the recursor-vs-canonical-type equality over the detected flat block. Validation: full shard-0 native run green (9357/9357 owned consts); `lake test -- --ignored ixvm` green (599 assertions; codegen regenerated, FFT pins re-bumped — still relative to this branch's stubbed verify_bytes_against). Known residual divergence (not yet observed failing): Rust reorders the detected aux portion of a flat block via canonical_aux_order before recursor checks; Aiur keeps discovery order.

The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted from the real command (its `interp` flag was still a bare bool while `ix check --interp` takes a mode string), and `lake exe ix check` rebuilds just as incrementally for day-to-day kernel iteration. One entrypoint, no drift.

Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.

Reverts the probe-branch stub (b7a0336) that disabled blake3 verification of constant/blob/claim bytes during the mathlib shard-0 debugging campaign. Codegen regenerated; FFT pins re-bumped with hashing back in the circuit. The pins land within ±1.1% of main (median ratio 0.997): the kernel work on this branch — canonical-sort comparator parity, whnf-aware index walks, the block-members table, aux-synthesis parity and canonical aux order — is cost-neutral. Nested-aux-heavy targets (DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper; small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer comparator and whnf walks. `lake test -- --ignored ixvm` green (599 assertions).

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

arthurpaulino force-pushed the ap/probe-mathlib branch 3 times, most recently from 309e1c4 to de33f23Compare July 11, 2026 11:28

arthurpaulino force-pushed the ap/probe-mathlib branch 2 times, most recently from 6051448 to 6c5daa4Compare July 14, 2026 00:13

arthurpaulino added 8 commits July 17, 2026 14:49

stub verify_bytes_against
af41d55

arthurpaulino force-pushed the ap/probe-mathlib branch from 6c5daa4 to d626ddeCompare July 17, 2026 17:49

johnchandlerburnham approved these changes Jul 17, 2026
View reviewed changes

arthurpaulino enabled auto-merge (squash) July 17, 2026 17:58

arthurpaulino merged commit 4e554d2 into mainJul 17, 2026
8 of 9 checks passed

arthurpaulino deleted the ap/probe-mathlib branch July 17, 2026 17:58

Uh oh!

Conversation

arthurpaulino commented Jul 11, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Kernel fixes

Performance

Tooling

Validation

Known follow-ups

Uh oh!

arthurpaulino commented Jul 12, 2026

Uh oh!

argument-ci-botBot commented Jul 12, 2026

!benchmark — main vs de33f23

aiur · InitStd · prove — main from: bencher @ 16455ba + base run (1 new)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

arthurpaulino commented Jul 11, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Kernel fixes

Performance

Tooling

Validation

Known follow-ups

Uh oh!

arthurpaulino commented Jul 12, 2026

Uh oh!

argument-ci-botBot commented Jul 12, 2026

!benchmark — main vs de33f23

aiur · InitStd · prove — main from: bencher @ 16455ba + base run (1 new)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

arthurpaulino commented Jul 11, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Kernel fixes

Performance

Tooling

Validation

Known follow-ups

Uh oh!

arthurpaulino commented Jul 12, 2026

Uh oh!

argument-ci-botBot commented Jul 12, 2026

!benchmark — main vs de33f23

aiur · InitStd · prove — main from: bencher @ 16455ba + base run (1 new)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

arthurpaulino commented Jul 11, 2026•
edited
Loading

`!benchmark` — main vs `de33f23`

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

arthurpaulino commented Jul 11, 2026•
edited
Loading

`!benchmark` — main vs `de33f23`

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

arthurpaulino commented Jul 11, 2026•
edited
Loading

`!benchmark` — main vs `de33f23`

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

arthurpaulino commented Jul 11, 2026•
edited
Loading

`!benchmark` — main vs `de33f23`

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

arthurpaulino commented Jul 11, 2026•
edited
Loading

`!benchmark` — main vs `de33f23`

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)