perf(ixvm): substitution sharing, Int primitives, projection def-eq; struct-eta scope fix - #583
Merged
Conversation
Large beta-reduction traces can instantiate the same expression with many different arguments even when a subtree does not reference the substituted binder. Since the argument is part of the memo key, the kernel previously rebuilt those argument-independent subtrees for every application. Detect exact loose-BVar occurrence for single substitution and lower argument-independent subtrees through the existing memoized path. Apply the analogous substitution-window check to simultaneous substitution, including an explicit empty-list fast path. Leave the ordinary substitution walks and expr_lower_walk circuit layout unchanged. A focused bytecode check of Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm passes at 403.031B FFT. The patch intentionally excludes the mechanical expr_lower_walk helper split from the earlier experiment.
Struct-eta iota is a speculative reduction, but it unconditionally inferred the stuck major. During canonical recursor reconstruction, WHNF can encounter a loose major under a deliberately empty local-type context; attempting inference then indexed past the context and aborted with an unmatched list case. Check the major's loose-BVar range against the supplied type context before attempting struct eta. If the major is not scoped, leave the recursor stuck and let ordinary reduction continue, matching the reference behavior when speculative inference cannot establish a type. This fixes SSet.prodStdSimplex.pairingCore.Type₁.rec, which was the shared failure in FLT shard 145 and Mathlib shard 226. The focused constant and both shards pass under bytecode interpretation.
Recognize canonical Int literals and evaluate closed arithmetic, Euclidean and balanced division/modulus, natAbs, and powers through KLimbs. This avoids expanding the logical Int definitions into large Nat reduction chains during WHNF.\n\nPrimitive addresses are covered by the elaborated IxVM address-parity suite. The focused Batteries Char casing proof still needs further defeq work, but this removes the catastrophic Int expansion encountered along that path.
After bounded lazy reduction, compare application trees before falling back to eager WHNF. Recognize applications with identical projection heads and compare only their arguments, while descending through application nodes without resetting the def-eq reduction budget. This avoids pathological eager reduction of projection-heavy proof terms while preserving the existing fallback for unrelated shapes. Validated with a complete 600-shard sweep across Init, InitStd, Lean, Batteries, Mathlib, and FLT (24 workers, five-minute shard timeout): all shards passed.
Repin 77 kernel pins and shard pipeline pin from full `lake test -- --ignored ixvm` run after `ix codegen` regen.
arthurpaulino
enabled auto-merge
August 20, 2026 21:57
Member
Author
|
!benchmark aiur |
samuelburnham
approved these changes
Aug 20, 2026
|
| constant | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
10.922 s | 9.025 s | -17.4% (1.21× faster) 🟢 | 36.041 s | 31.963 s | -11.3% (1.13× faster) 🟢 | 76.51 GiB | 70.75 GiB | -7.5% (1.08× smaller) 🟢 | 10.99 MiB | 11.34 MiB | +3.2% |
70.1 ms | 77.8 ms | +11.0% (1.11× slower) |
153.04B | 134.36B | -12.2% (1.14× fewer) 🟢 |
Char.ofOrdinal_le_of_le |
7.573 s | 7.105 s | -6.2% (1.07× faster) 🟢 | 28.412 s | 27.507 s | -3.2% 🟢 | 64.37 GiB | 63.81 GiB | -0.9% | 10.99 MiB | 11.38 MiB | +3.5% |
68.7 ms | 81.1 ms | +18.0% (1.18× slower) |
107.22B | 102.61B | -4.3% 🟢 |
Array.extract_append |
11.693 s | 6.746 s | -42.3% (1.73× faster) 🟢 | 38.229 s | 24.295 s | -36.5% (1.57× faster) 🟢 | 77.76 GiB | 52.01 GiB | -33.1% (1.49× smaller) 🟢 | 10.94 MiB | 11.25 MiB | +2.9% | 68.6 ms | 69.3 ms | +0.9% | 156.30B | 97.08B | -37.9% (1.61× fewer) 🟢 |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
4.117 s | 3.736 s | -9.2% (1.10× faster) 🟢 | 16.772 s | 15.239 s | -9.1% (1.10× faster) 🟢 | 36.65 GiB | 33.97 GiB | -7.3% (1.08× smaller) 🟢 | 10.91 MiB | 11.27 MiB | +3.2% |
68.5 ms | 69.3 ms | +1.1% | 60.81B | 55.68B | -8.4% (1.09× fewer) 🟢 |
String.append |
431.5 ms | 433.2 ms | +0.4% | 2.285 s | 2.357 s | +3.1% |
4.77 GiB | 4.96 GiB | +3.9% |
9.73 MiB | 9.95 MiB | +2.2% | 59.7 ms | 62.6 ms | +4.7% |
3.28B | 3.37B | +2.6% |
Nat.add_comm |
265.2 ms | 271.9 ms | +2.5% | 1.077 s | 1.153 s | +7.1% (1.07× slower) |
4.11 GiB | 4.24 GiB | +3.1% |
8.90 MiB | 9.10 MiB | +2.3% | 54.2 ms | 54.9 ms | +1.2% | 303.18M | 308.46M | +1.7% |
Stage 2 — FRI recursion on FRI (6 constants)
| constant | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
5.466 s | 5.663 s | +3.6% |
31.792 s | 33.678 s | +5.9% (1.06× slower) |
94.87 GiB | 100.27 GiB | +5.7% (1.06× larger) |
3.97 MiB | 3.97 MiB | +0.0% | 26.4 ms | 25.2 ms | -4.4% 🟢 | 204.18B | 209.47B | +2.6% |
Char.ofOrdinal_le_of_le |
5.439 s | 5.604 s | +3.0% |
31.210 s | 33.441 s | +7.1% (1.07× slower) |
91.57 GiB | 100.89 GiB | +10.2% (1.10× larger) |
3.97 MiB | 3.97 MiB | +0.0% | 25.3 ms | 24.9 ms | -1.4% | 199.67B | 208.86B | +4.6% |
Array.extract_append |
5.417 s | 5.529 s | +2.1% | 30.730 s | 32.096 s | +4.4% |
90.46 GiB | 94.28 GiB | +4.2% |
3.97 MiB | 3.97 MiB | +0.0% | 25.2 ms | 25.9 ms | +2.9% | 196.87B | 202.37B | +2.8% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
5.338 s | 5.457 s | +2.2% | 30.733 s | 31.897 s | +3.8% |
90.00 GiB | 94.77 GiB | +5.3% (1.05× larger) |
3.97 MiB | 3.97 MiB | +0.0% | 25.6 ms | 25.2 ms | -1.6% | 193.52B | 201.58B | +4.2% |
String.append |
4.340 s | 4.462 s | +2.8% | 28.924 s | 29.217 s | +1.0% | 87.82 GiB | 87.86 GiB | +0.1% | 3.97 MiB | 3.97 MiB | +0.0% | 26.4 ms | 25.5 ms | -3.3% 🟢 | 161.13B | 166.45B | +3.3% |
Nat.add_comm |
3.617 s | 3.599 s | -0.5% | 19.439 s | 19.509 s | +0.4% | 57.76 GiB | 58.66 GiB | +1.5% | 3.97 MiB | 3.97 MiB | +0.0% | 26.1 ms | 24.8 ms | -4.9% (1.05× faster) 🟢 | 129.24B | 127.78B | -1.1% |
Pipeline total (6 constants)
| constant | total-time (main) | total-time (PR) | Δ% | pipeline-peak-ram (main) | pipeline-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
1m 7.8s | 1m 5.6s | -3.2% 🟢 | 94.87 GiB | 100.27 GiB | +5.7% (1.06× larger) |
Char.ofOrdinal_le_of_le |
59.622 s | 1m 0.9s | +2.2% | 91.57 GiB | 100.89 GiB | +10.2% (1.10× larger) |
Array.extract_append |
1m 9.0s | 56.391 s | -18.2% (1.22× faster) 🟢 | 90.46 GiB | 94.28 GiB | +4.2% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
47.505 s | 47.136 s | -0.8% | 90.00 GiB | 94.77 GiB | +5.3% (1.05× larger) |
String.append |
31.209 s | 31.574 s | +1.2% | 87.82 GiB | 87.86 GiB | +0.1% |
Nat.add_comm |
20.516 s | 20.662 s | +0.7% | 57.76 GiB | 58.66 GiB | +1.5% |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Five commits on
ap/ixvm: three kernel performance changes, one WHNF soundness/robustness fix, and the codegen regeneration with repinned FFT costs.Commits
perf(ixvm): share argument-independent substitution work
(
Ix/IxVM/Kernel/Subst.lean)Large beta-reduction traces instantiate the same expression with many different arguments. Since the argument is part of the memo key, subtrees that never mention the substituted binder were rebuilt once per argument.
expr_has_bvar_at(e, depth)predicate (with binder/let helpers) detects whether the exact binder occurs, distinguishing "mentions the binder" from "mentions only variables above it".expr_inst1: when the binder does not occur but higher loose bvars do, route throughexpr_lower(e, 1, depth + 1)— a memoized, argument-independent path shared by all arguments.expr_inst_many: analogoushas_bvar_in_range(e, depth, depth + n)window check, routing binder-free subtrees throughexpr_lower(e, n, depth + n), plus an explicit empty-substitution-list fast path.expr_lower_walkcircuit layout are unchanged.Validation: focused bytecode check of
Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorCommpasses at 403.031B FFT.fix(ixvm): decline struct eta for out-of-scope majors
(
Ix/IxVM/Kernel/Whnf.lean)Struct-eta iota is speculative, but the code unconditionally ran
k_inferon the stuck major. During canonical recursor reconstruction, WHNF can hit a loose major under a deliberately empty local type context; inference then indexed pasttypesand aborted on an unmatched list case.memo_u32_less_than(list_length(types), expr_lbr(major)). If the major's loose-bvar range exceeds the supplied context, decline eta (return stuck) and let ordinary reduction continue — matching reference behavior when speculative inference cannot establish a type.Validation: fixes
SSet.prodStdSimplex.pairingCore.Type₁.rec, the shared failure in FLT shard 145 and Mathlib shard 226; focused constant and both shards pass under bytecode interpretation.perf(ixvm): reduce closed Int primitives natively
(
Ix/IxVM/Kernel/NatPrim.lean,Ix/IxVM/Kernel/Whnf.lean)Closed Int arithmetic was previously reduced by unfolding the logical Int definitions into large Nat reduction chains during WHNF.
6 = Intin the address-keyedprim_familyclassification, dispatched viatry_int_prim_dispatch.Int.ofNat,Int.negSucc,add,sub,mul,neg,emod,ediv,bmod,bdiv,natAbs,pow.(sign, magnitude)pairs overKLimbs; closed arithmetic, Euclidean and balanced division/modulus,natAbs, and powers evaluate natively.Validation: primitive addresses covered by the elaborated IxVM address-parity suite. The focused Batteries Char casing proof still needs further def-eq work, but the catastrophic Int expansion on that path is gone.
perf(ixvm): compare projection applications structurally
(
Ix/IxVM/Kernel/DefEq.lean)Projection-heavy proof terms triggered pathological eager WHNF in the def-eq slow path.
k_is_def_eq_struct_bounded, budget 8) fails, tryk_is_def_eq_structure_treebeforeslow2_eager_fallback.try_same_proj_head_app: spines with equal length whose heads are projections with the same struct address, same index, and the same inner-expression pointer compare argument-wise only. (Pointer equality used in the positive direction only; mismatch just declines the shortcut.)k_is_def_eq_structure_tree_app: descend throughAppnodes recursively without resetting the reduction budget.Validation: complete 600-shard sweep across Init, InitStd, Lean, Batteries, Mathlib, and FLT (24 workers, five-minute shard timeout) — all shards passed.
test(ixvm): regen codegen and repin FFT costs
(
crates/ixvm-codegen/src/aiur_ixvm.rs,Tests/Ix/IxVM.lean,Tests/Main.lean)aiur_ixvm.rsviaix codegen(784 IxVM functions).6_720_706_901→6_770_109_972) from a fulllake test -- --ignored ixvmrun; rerun passes clean.