Skip to content

IxVM def-eq: rebase open pairs to their minimum loose index #546

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 1 commit into from
Aug 11, 2026
Merged

IxVM def-eq: rebase open pairs to their minimum loose index #546

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 41 additions & 2 deletions Ix/IxVM/Kernel/DefEq.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,8 +63,47 @@ def defEq := ⟦
fn k_is_def_eq(a: KExpr, b: KExpr, types: List‹KExpr›) -> G {
match ptr_val(a) - ptr_val(b) {
0 => 1, -- ptr-eq: same interned pointer = equal
_ => k_is_def_eq_core(a, b,
ctx_trim(types, lbr_max(expr_lbr(a), expr_lbr(b)))),
_ =>
let base = lbr_max(expr_lbr(a), expr_lbr(b));
match base {
0 => k_is_def_eq_core(a, b, store(ListNode.Nil)),
_ => k_def_eq_rebase(a, b, types, base),
},
}
}

-- Rebase an OPEN pair to its minimum loose index before keying.
-- The prefix trim alone cannot canonicalize a pair that references
-- only the OUTERMOST binders of a deep telescope: its lbr spans the
-- whole context, so the trim keeps every inner frame — and each
-- comparison site spells those (unreferenced) inner frames slightly
-- differently, minting a fresh memo key per site. Measured on the
-- mathlib monster: 2.48M distinct (a,b,types) core keys over 15,085
-- distinct pairs — 164x context multiplicity, the dominant cost.
--
-- Fix: `g = min(glb(a), glb(b))` frames at the inner end are loose in
-- NEITHER side, so lowering both sides by `g` and dropping those
-- frames is a bijection on derivations (context strengthening by
-- unreferenced frames — the same argument as the base=0 → Nil arm,
-- generalized). Def-eq returns a bit, so nothing needs lifting back.
-- Depth-shifted copies of the same tower also lower to the SAME
-- hash-consed pair, merging pairs across binder depths, not just
-- contexts. Kept frames only ever reference deeper (outward) frames,
-- all of which are kept.
fn k_def_eq_rebase(a: KExpr, b: KExpr, types: List‹KExpr›,
base: G) -> G {
-- Unconditional: a depth threshold (only rebase past base > 8) was
-- measured and rejected — it recovered only a third of the overhead
-- on binder-heavy Init proofs (+6.4% -> +4.2% on Array.append_assoc)
-- for no gain on the mathlib constant (its full closure was flat,
-- 8.71e11 vs 8.74e11): not worth a tuning constant.
let g = lbr_min(lbr_min(expr_glb(a, 0), expr_glb(b, 0)),
list_length(types));
match g {
0 => k_is_def_eq_core(a, b, ctx_trim(types, base)),
_ =>
k_is_def_eq_core(expr_lower(a, g, 0), expr_lower(b, g, 0),
ctx_trim(list_drop(types, g), base - g)),
}
}

Expand Down
50 changes: 50 additions & 0 deletions Ix/IxVM/Kernel/Subst.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,56 @@ def subst := ⟦
}
}

-- ============================================================================
-- expr_glb / expr_lower — def-eq key rebasing support.
--
-- `expr_glb(e, c)`: MINIMUM loose-BVar index of `e` relative to cutoff
-- `c` (i.e. min over `{i - c : BVar i loose, i ≥ c}`), or the sentinel
-- `4294967295` when `e` has no loose BVar at or above `c`. The min of a
-- term that only references the OUTERMOST binders of a deep telescope
-- is large — and every context frame below that min is unreferenced.
--
-- The lowering itself is the pre-existing `expr_lower` below; the
-- rebase caller's `g = min glb` guarantees its no-index-in-
-- `[cutoff, cutoff+shift)` precondition by construction.
-- ============================================================================
fn expr_glb(e: KExpr, c: G) -> G {
-- Fast path: no loose BVar at or above `c` (lbr ≤ c) → sentinel,
-- skipping the walk of closed subtrees entirely.
match memo_u32_less_than(expr_lbr(e), c + 1) {
1 => 4294967295,
_ => expr_glb_walk(e, c),
}
}

fn expr_glb_walk(e: KExpr, c: G) -> G {
match load(e) {
KExprNode.BVar(i) =>
match memo_u32_less_than(i, c) {
1 => 4294967295,
0 => i - c,
},
KExprNode.Srt(_) => 4294967295,
KExprNode.Const(_, _) => 4294967295,
KExprNode.Lit(_) => 4294967295,
KExprNode.App(f, a) => lbr_min(expr_glb(f, c), expr_glb(a, c)),
KExprNode.Lam(ty, body) => expr_glb_binder(ty, body, c),
KExprNode.Forall(ty, body) => expr_glb_binder(ty, body, c),
KExprNode.Let(ty, val, body) => expr_glb_let(ty, val, body, c),
KExprNode.Proj(_, _, e1) => expr_glb(e1, c),
}
}

-- Cold binder arms (same extraction pattern as `expr_lbr_let`).
fn expr_glb_binder(ty: KExpr, body: KExpr, c: G) -> G {
lbr_min(expr_glb(ty, c), expr_glb(body, c + 1))
}

fn expr_glb_let(ty: KExpr, val: KExpr, body: KExpr, c: G) -> G {
lbr_min(lbr_min(expr_glb(ty, c), expr_glb(val, c)),
expr_glb(body, c + 1))
}

-- ============================================================================
-- expr_lift
--
Expand Down
154 changes: 85 additions & 69 deletions Tests/Ix/IxVM.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,6 +211,21 @@ public def thmMajorWant (n : Nat) (_pf : n = 1) : Nat := n
public theorem partialKRec :
(@Eq.rec Nat 0 (fun _ _ => Nat) 1 0) = (fun _ => 1) := rfl

-- Deep-telescope outer-reference shape (the mathlib
-- `Algebra.kerTensorProductMapIdToAlgHomEquiv._proof_1` failure shape,
-- minimized): the def-eq obligations under the inner binders reference
-- ONLY the outermost binder, so in de Bruijn their loose range spans
-- the whole context and the prefix trim keeps every (unreferenced)
-- inner frame. Without rebasing, each comparison site's inner-frame
-- spelling mints a fresh memo key — measured 164x context multiplicity
-- per distinct pair on the mathlib constant. Pins `k_def_eq_rebase`:
-- both sides lower by their shared minimum loose index and the
-- unreferenced frames drop from the key.
public theorem deepRebase :
∀ (n : Nat) (_a _b _c _d _e _f _g _h _i _j : Nat),
n + 0 = n :=
fun n _ _ _ _ _ _ _ _ _ _ => Nat.add_zero n

end IxVMInd

/-! ## Test runners -/
Expand Down Expand Up @@ -261,76 +276,77 @@ private def nameOfString (str : String) : Lean.Name :=
listed constant fails the suite, so a regression cannot land quietly
and an improvement has to be acknowledged by re-pinning. -/
private def kernelCheckEntries : List (String × Nat) := [
("HEq", 171_089_006),
("HEq.rec", 176_144_378),
("Eq.rec", 175_714_099),
("HEq", 171_089_016),
("HEq.rec", 176_144_753),
("Eq.rec", 175_714_392),
("Nat", 171_086_655),
("Nat.add", 221_989_750),
("Nat.add_comm", 400_486_243),
("Nat.decEq", 459_468_748),
("Nat.decLe", 976_494_424),
("Nat.sub_le_of_le_add", 2_368_739_790),
("Nat.shiftRight_succ", 1_766_473_720),
("Trans.mk", 177_974_041),
("Array.append_assoc", 10_475_666_394),
("Vector.append", 10_766_722_152),
("IxVMPrim.nat_add_lit", 283_686_117),
("IxVMPrim.nat_sub_lit", 309_032_587),
("IxVMPrim.nat_mul_lit", 272_033_379),
("IxVMPrim.nat_mul_big", 269_433_717),
("IxVMPrim.nat_div_lit", 1_727_009_194),
("IxVMPrim.nat_mod_lit", 1_762_676_738),
("IxVMPrim.nat_succ_lit", 194_834_551),
("IxVMPrim.nat_pred_lit", 227_421_646),
("IxVMPrim.nat_gcd_lit", 2_754_112_663),
("IxVMPrim.nat_land_lit", 4_537_647_872),
("IxVMPrim.nat_lor_lit", 4_541_364_929),
("IxVMPrim.nat_xor_lit", 4_572_011_564),
("IxVMPrim.nat_shl_lit", 314_149_762),
("IxVMPrim.nat_shr_lit", 1_750_137_811),
("IxVMPrim.nat_pow_big", 499_597_928),
("IxVMPrim.nat_beq_lit", 267_885_490),
("IxVMPrim.nat_ble_lit", 260_434_622),
("IxVMPrim.nat_cases_big", 225_988_002),
("IxVMPrim.nat_dec_le", 1_003_064_094),
("IxVMPrim.nat_dec_lt", 1_019_808_606),
("IxVMPrim.nat_dec_eq", 516_246_231),
("IxVMPrim.str_size_lit", 3_203_339_502),
("IxVMPrim.bv_to_nat_lit", 2_623_880_738),
("IxVMInd.Even", 276_200_242),
("IxVMInd.Odd", 276_202_950),
("IxVMInd.Even.rec", 300_946_951),
("IxVMInd.Odd.rec", 300_947_873),
("IxVMInd.Tree", 173_262_148),
("IxVMInd.Tree.rec", 187_000_688),
("IxVMInd.DedupM", 179_096_071),
("IxVMInd.DedupM.rec", 197_123_757),
("IxVMInd.DepthM", 176_198_889),
("IxVMInd.DepthM.rec", 191_223_293),
("String.Internal.append", 3_162_876_551),
("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 4_682_107_158),
("Lean.Syntax.rec", 3_242_420_293),
("IxVMInd.AuxTie", 454_526_297),
("IxVMInd.AuxTie.rec", 510_245_364),
("IxVMInd.HiddenIdx", 172_057_397),
("IxVMInd.HiddenIdx.rec", 175_777_691),
("IxVMInd.thmMajorUse", 653_340_064),
("IxVMInd.partialKRec", 202_704_667),
("String.Slice.Pattern.Model.NoPrefixForwardPatternModel.rec", 4_366_459_157),
("Lean.Widget.TaggedText.rec", 3_194_016_090),
("Lean.Doc.Part.rec", 3_250_962_345),
("Lean.Doc.Block.rec", 3_458_177_300),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 175_887_373),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 180_588_547),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 178_248_803),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 178_248_803),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 178_248_803),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 176_086_773),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 191_623_499),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 191_622_712),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 178_248_803),
("strOfListFoldSize", 3_609_582_757),
("strOfListFoldSizeAscii", 3_611_113_654),
("Nat.add", 223_353_205),
("Nat.add_comm", 404_014_350),
("Nat.decEq", 462_717_809),
("Nat.decLe", 1_000_820_598),
("Nat.sub_le_of_le_add", 2_426_886_641),
("Nat.shiftRight_succ", 1_811_029_372),
("Trans.mk", 177_974_474),
("Array.append_assoc", 11_059_832_101),
("Vector.append", 11_351_782_082),
("IxVMPrim.nat_add_lit", 285_061_421),
("IxVMPrim.nat_sub_lit", 310_682_485),
("IxVMPrim.nat_mul_lit", 273_417_994),
("IxVMPrim.nat_mul_big", 270_817_290),
("IxVMPrim.nat_div_lit", 1_771_412_378),
("IxVMPrim.nat_mod_lit", 1_807_654_264),
("IxVMPrim.nat_succ_lit", 194_835_041),
("IxVMPrim.nat_pred_lit", 227_699_314),
("IxVMPrim.nat_gcd_lit", 2_823_670_800),
("IxVMPrim.nat_land_lit", 4_630_762_947),
("IxVMPrim.nat_lor_lit", 4_634_453_317),
("IxVMPrim.nat_xor_lit", 4_665_078_880),
("IxVMPrim.nat_shl_lit", 315_543_537),
("IxVMPrim.nat_shr_lit", 1_794_535_176),
("IxVMPrim.nat_pow_big", 501_246_916),
("IxVMPrim.nat_beq_lit", 270_130_059),
("IxVMPrim.nat_ble_lit", 262_213_419),
("IxVMPrim.nat_cases_big", 226_262_961),
("IxVMPrim.nat_dec_le", 1_027_525_564),
("IxVMPrim.nat_dec_lt", 1_044_210_154),
("IxVMPrim.nat_dec_eq", 519_655_783),
("IxVMPrim.str_size_lit", 3_288_881_329),
("IxVMPrim.bv_to_nat_lit", 2_696_364_018),
("IxVMInd.Even", 277_576_399),
("IxVMInd.Odd", 277_579_110),
("IxVMInd.Even.rec", 302_328_271),
("IxVMInd.Odd.rec", 302_329_193),
("IxVMInd.Tree", 173_262_172),
("IxVMInd.Tree.rec", 187_001_149),
("IxVMInd.DedupM", 179_096_081),
("IxVMInd.DedupM.rec", 197_124_338),
("IxVMInd.DepthM", 176_198_913),
("IxVMInd.DepthM.rec", 191_223_904),
("String.Internal.append", 3_247_393_859),
("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 4_805_903_153),
("Lean.Syntax.rec", 3_326_915_427),
("IxVMInd.AuxTie", 456_178_826),
("IxVMInd.AuxTie.rec", 511_908_920),
("IxVMInd.HiddenIdx", 172_057_421),
("IxVMInd.HiddenIdx.rec", 175_777_957),
("IxVMInd.thmMajorUse", 667_954_713),
("IxVMInd.partialKRec", 202_711_297),
("IxVMInd.deepRebase", 288_904_843),
("String.Slice.Pattern.Model.NoPrefixForwardPatternModel.rec", 4_485_653_172),
("Lean.Widget.TaggedText.rec", 3_278_494_065),
("Lean.Doc.Part.rec", 3_335_415_391),
("Lean.Doc.Block.rec", 3_542_720_534),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 175_887_397),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 180_588_667),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 178_249_151),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 178_249_151),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 178_249_151),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 176_086_797),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 191_623_989),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 191_623_202),
("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 178_249_151),
("strOfListFoldSize", 3_702_091_157),
("strOfListFoldSizeAscii", 3_703_622_126),
]

/-- Variant of `kernelChecks`, pinned to the baseline
Expand Down
4 changes: 2 additions & 2 deletions Tests/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -223,8 +223,8 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
let actual :=
(Aiur.computeStats v2Env.compiled qc v2Env.shapes).totalFftCost.round.toUInt64.toNat
pure (LSpec.test
s!"Shard pipeline FFT matches: expected 10569112333, got {actual}"
(actual = 10_569_112_333))
s!"Shard pipeline FFT matches: expected 10601793090, got {actual}"
(actual = 10_601_793_090))
LSpec.lspecIO
(.ofList [("ixvm",
[fullSeq, aiurSeq, arenaSeq, exploitSeq, paritySeq, shardSeq])]) []),
Expand Down
Loading
Loading