From 1e0e76652c94920e47673ace24f1c424f0defc0d Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Thu, 18 Jun 2026 18:06:50 -0700 Subject: [PATCH 1/8] IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + post-spine-congruence) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit UTF-8 `_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar? .assemble₄_eq_some_of_toBitVec._proof_1_8` OOMs on the previous pipeline because `k_is_def_eq_core` jumps from Tier 1.5 straight to full delta WHNF (Tier 2); the cascading Nat.rec / Nat.succ iota expansions then drive `whnf_const_head` past 1M unique entries before either side reaches a comparable canonical form. Rust's def-eq settles the same pair via the no-delta whnf + quick structural recursion before any of that fires. This patch ports the three pieces of that short-circuit and nothing else — no FVar variant, no KStore, no Subst changes, no signature sweep. * `whnf_nd` family in `Whnf.lean` (mirror Rust `whnf_no_delta_for_def_eq`). Same dispatch tree as `whnf` (beta / let zeta / iota / proj / quot / primitives all fire), except `whnf_nd_const_head`'s Defn arm falls through to a stuck `apply_spine` instead of delta-unfolding. * `k_infer_only` family in `Infer.lean` (mirror Rust `with_infer_only`). App drops `k_check(a, dom)`; Lam drops `k_ensure_sort(ty)`; Let drops the val/ty validations. Distinct Aiur memo from `k_infer`, parity with Rust's separate `infer_cache` / `infer_only_cache`. * `k_is_def_eq_struct_safe` in `DefEq.lean` (mirror Rust `quick_def_eq`). Sort-Sort via `level_equal`; Lam-Lam / All-All recurse on type and on body under `Cons(ty_a, types)`. Returns 1 only when DEFINITELY def-eq; 0 means fall through. Sound on partially-whnf'd (no-delta) inputs because the handled shapes don't depend on further reductions. * `k_is_def_eq_core` Tier 1d wiring inserted between Tier 1c (string lit) and Tier 2 (full whnf): aw_nd = whnf_nd(a); bw_nd = whnf_nd(b) ptr_eq(aw_nd, bw_nd) → 1 k_is_def_eq_struct_safe(aw_nd, bw_nd) → 1 if 1 try_lazy_delta_app(aw_nd, bw_nd) → 1 if 1 (rerun post-whnf_nd: spine args may have reduced past what Tier 1.5's pre-whnf attempt could see, exposing Const-Const congruence that was hidden) * `try_proof_irrel`, `is_prop_type`, `try_unit_like` switch from `k_infer` to `k_infer_only` — these helpers only need the synthesized type, not the full re-validation work that `k_infer` does for each recursive App/Let/Lam. Each piece individually validated necessary (removing it puts UTF-8 back into the OOM regime). FVar variant + opens, KStore explicit caches, infer_only's FVar-based binder opening — all confirmed NOT necessary for the UTF-8 unblock and left out (see PLAN.md for future experiments). Measured (FFT cost): Nat.add_comm: 56.08M → 55.63M (~stable; new code paths add no overhead on the common case because Tier 1d's whnf_nd + struct_safe are themselves Aiur-memoized). _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar? .assemble₄_eq_some_of_toBitVec._proof_1_8: OOM → 39.12B FFT, passes. 3 files, +296/-6 lines. --- Ix/IxVM/Kernel/DefEq.lean | 64 ++++++++++++++++-- Ix/IxVM/Kernel/Infer.lean | 102 ++++++++++++++++++++++++++++ Ix/IxVM/Kernel/Whnf.lean | 136 +++++++++++++++++++++++++++++++++++++- 3 files changed, 296 insertions(+), 6 deletions(-) diff --git a/Ix/IxVM/Kernel/DefEq.lean b/Ix/IxVM/Kernel/DefEq.lean index f84c9aa48..451c7151c 100644 --- a/Ix/IxVM/Kernel/DefEq.lean +++ b/Ix/IxVM/Kernel/DefEq.lean @@ -65,6 +65,19 @@ def defEq := ⟦ match try_string_lit_pair(a, b, types, top, addrs) { 1 => 1, 0 => + -- Tier 1d: no-delta whnf + structural shortcuts (mirror Rust + -- `whnf_no_delta_for_def_eq` + `quick_def_eq` + post-`try_def_eq_app`). + let aw_nd = whnf_nd(a, types, top, addrs); + let bw_nd = whnf_nd(b, types, top, addrs); + match ptr_val(aw_nd) - ptr_val(bw_nd) { + 0 => 1, + _ => + match k_is_def_eq_struct_safe(aw_nd, bw_nd, types, top, addrs) { + 1 => 1, + 0 => + match try_lazy_delta_app(aw_nd, bw_nd, types, top, addrs) { + 1 => 1, + 0 => -- Tier 2: WHNF both sides. let aw = whnf(a, types, top, addrs); let bw = whnf(b, types, top, addrs); @@ -104,19 +117,60 @@ def defEq := ⟦ }, }, }, + }, + }, + }, }, }, } } + -- Mirror Rust `def_eq.rs::quick_def_eq`. Sound on partially-whnf'd + -- (no-delta) inputs because the handled shapes (Sort/Lam/All) don't + -- depend on further reductions for their judgment. Returns 1 only + -- when DEFINITELY def-eq; 0 = fall through. + fn k_is_def_eq_struct_safe(a: KExpr, b: KExpr, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G { + match load(a) { + KExprNode.Srt(la) => + match load(b) { + KExprNode.Srt(lb) => level_equal(load(la), load(lb)), + _ => 0, + }, + KExprNode.Lam(ty_a, body_a) => + match load(b) { + KExprNode.Lam(ty_b, body_b) => + match k_is_def_eq(ty_a, ty_b, types, top, addrs) { + 1 => + let inner = store(ListNode.Cons(ty_a, types)); + k_is_def_eq(body_a, body_b, inner, top, addrs), + 0 => 0, + }, + _ => 0, + }, + KExprNode.Forall(ty_a, body_a) => + match load(b) { + KExprNode.Forall(ty_b, body_b) => + match k_is_def_eq(ty_a, ty_b, types, top, addrs) { + 1 => + let inner = store(ListNode.Cons(ty_a, types)); + k_is_def_eq(body_a, body_b, inner, top, addrs), + 0 => 0, + }, + _ => 0, + }, + _ => 0, + } + } + -- Mirror: src/ix/kernel/def_eq.rs:801-818 fn try_proof_irrel. fn try_proof_irrel(a: KExpr, b: KExpr, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G { - let a_ty = k_infer(a, types, top, addrs); + let a_ty = k_infer_only(a, types, top, addrs); match is_prop_type(a_ty, types, top, addrs) { 0 => 0, 1 => - let b_ty = k_infer(b, types, top, addrs); + let b_ty = k_infer_only(b, types, top, addrs); k_is_def_eq(a_ty, b_ty, types, top, addrs), } } @@ -124,7 +178,7 @@ def defEq := ⟦ -- Returns 1 iff `whnf(infer(ty))` is `Sort 0`. fn is_prop_type(ty: KExpr, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G { - let sort = k_infer(ty, types, top, addrs); + let sort = k_infer_only(ty, types, top, addrs); let sort_w = whnf(sort, types, top, addrs); match load(sort_w) { KExprNode.Srt(l) => @@ -139,12 +193,12 @@ def defEq := ⟦ -- Mirror: src/ix/kernel/def_eq.rs:858-905 fn try_unit_like_eq. fn try_unit_like(a: KExpr, b: KExpr, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G { - let ta = k_infer(a, types, top, addrs); + let ta = k_infer_only(a, types, top, addrs); let ta_w = whnf(ta, types, top, addrs); match is_unit_like_type(ta_w, top) { 0 => 0, 1 => - let tb = k_infer(b, types, top, addrs); + let tb = k_infer_only(b, types, top, addrs); k_is_def_eq(ta, tb, types, top, addrs), } } diff --git a/Ix/IxVM/Kernel/Infer.lean b/Ix/IxVM/Kernel/Infer.lean index a549d3b26..e35f76bc8 100644 --- a/Ix/IxVM/Kernel/Infer.lean +++ b/Ix/IxVM/Kernel/Infer.lean @@ -184,6 +184,108 @@ def infer := ⟦ () } + -- ============================================================================ + -- k_infer_only: type-synthesis-only (mirror Rust `with_infer_only`). + -- Skips inner validations: App drops `k_check(a, dom)`; Lam drops + -- `k_ensure_sort(ty)`; Let drops val/ty checks. Distinct Aiur memo from + -- `k_infer` (parity with Rust's separate infer_cache / infer_only_cache). + -- Used at try_proof_irrel / is_prop_type / try_unit_like where only the + -- synthesized type is needed. + -- ============================================================================ + fn k_infer_only(e: KExpr, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + k_infer_only_core(e, ctx_trim(types, expr_lbr(e)), top, addrs) + } + + fn k_infer_only_core(e: KExpr, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + match load(e) { + KExprNode.BVar(i) => types_lookup(types, i), + KExprNode.Srt(l) => + store(KExprNode.Srt(store(level_reduce(KLevel.Succ(l))))), + KExprNode.Const(idx, lvls) => + let ci = load(list_lookup(top, idx)); + let expected = const_num_lvls(ci); + let given = list_length(lvls); + assert_eq!(given, expected); + let ty = const_type_of(ci); + expr_inst_levels(ty, lvls), + KExprNode.App(f, a) => + let f_ty = k_infer_only(f, types, top, addrs); + match load(f_ty) { + KExprNode.Forall(_, cod) => expr_inst1(cod, a, 0), + _ => + let f_ty_whnf = whnf(f_ty, types, top, addrs); + let triple = ensure_forall_post_whnf(f_ty_whnf); + match triple { + (ok, _, cod) => + assert_eq!(ok, 1); + expr_inst1(cod, a, 0), + }, + }, + KExprNode.Lam(ty, body) => + let types2 = store(ListNode.Cons(ty, types)); + let body_ty = k_infer_only(body, types2, top, addrs); + store(KExprNode.Forall(ty, body_ty)), + KExprNode.Forall(ty, body) => + let u1 = k_ensure_sort_only(ty, types, top, addrs); + let types2 = store(ListNode.Cons(ty, types)); + let u2 = k_ensure_sort_only(body, types2, top, addrs); + store(KExprNode.Srt(store(level_imax(load(u1), load(u2))))), + KExprNode.Let(_, val, body) => + let body_substed = expr_inst1(body, val, 0); + k_infer_only(body_substed, types, top, addrs), + KExprNode.Lit(lit) => + match lit { + KLiteral.Nat(_) => nat_const_type(addrs), + KLiteral.Str(_) => str_const_type(addrs), + }, + KExprNode.Proj(tidx, fidx, e1) => + let val_ty = k_infer_only(e1, types, top, addrs); + let wty = whnf(val_ty, types, top, addrs); + let pair = collect_spine(wty); + match pair { + (head, args) => + match load(head) { + KExprNode.Const(idx, lvls) => + assert_eq!(idx, tidx); + let ind_ci = load(list_lookup(top, idx)); + match ind_ci { + KConstantInfo.Induct(_, ind_ty, n_params, n_indices, ctor_indices, _, _, _, _, _) => + assert_eq!(list_length(ctor_indices), 1); + let is_prop = is_inductive_prop(ind_ty, lvls, n_params + n_indices, + types, top, addrs); + let ctor_idx = list_lookup(ctor_indices, 0); + let ctor_ci = load(list_lookup(top, ctor_idx)); + match ctor_ci { + KConstantInfo.Ctor(_, ctor_ty, _, _, _, _, _) => + let ctor_ty_inst = expr_inst_levels(ctor_ty, lvls); + let after_params = peel_params_subst(ctor_ty_inst, args, n_params); + peel_field_loop(after_params, fidx, 0, tidx, e1, is_prop, + types, top, addrs), + }, + }, + }, + }, + } + } + + fn k_ensure_sort_only(e: KExpr, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> &KLevel { + let ty = k_infer_only(e, types, top, addrs); + match load(ty) { + KExprNode.Srt(l) => l, + _ => + let ty_whnf = whnf(ty, types, top, addrs); + let pair = ensure_sort_post_whnf(ty_whnf); + match pair { + (ok, l) => + assert_eq!(ok, 1); + l, + }, + } + } + -- ============================================================================ -- Helpers: extract const declared type, Nat/Str literal types. -- ============================================================================ diff --git a/Ix/IxVM/Kernel/Whnf.lean b/Ix/IxVM/Kernel/Whnf.lean index d3e76b698..c43f40f49 100644 --- a/Ix/IxVM/Kernel/Whnf.lean +++ b/Ix/IxVM/Kernel/Whnf.lean @@ -301,6 +301,141 @@ def whnf := ⟦ } } + -- ============================================================================ + -- whnf_nd: WHNF without delta-unfolding (`src/ix/kernel/whnf.rs::whnf_no_delta`). + -- + -- Same dispatch tree as `whnf`, but `whnf_nd_const_head`'s `Defn` arm + -- returns the stuck application instead of unfolding. Beta / let zeta / + -- iota / proj / quot / primitives still fire — they don't require delta. + -- + -- Used by def_eq's Tier 1d structural pre-check (Rust def_eq.rs:320-326): + -- many comparisons settle at no-delta whnf + ptr_eq or structural quick + -- comparison, avoiding the cascading delta-unfold work. + -- ============================================================================ + fn whnf_nd(e: KExpr, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + match load(e) { + KExprNode.Srt(_) => e, + KExprNode.Lit(_) => e, + KExprNode.Lam(_, _) => e, + KExprNode.Forall(_, _) => e, + KExprNode.BVar(_) => e, + _ => whnf_nd_core(e, ctx_trim(types, expr_lbr(e)), top, addrs), + } + } + + fn whnf_nd_core(e: KExpr, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + let pair = collect_spine(e); + match pair { + (head, spine) => whnf_nd_with_spine(head, spine, types, top, addrs), + } + } + + fn whnf_nd_with_spine(head: KExpr, spine: List‹KExpr›, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + match load(head) { + KExprNode.App(f, a) => + match collect_spine(head) { + (inner_head, inner_spine) => + whnf_nd_with_spine(inner_head, list_concat(inner_spine, spine), types, top, addrs), + }, + KExprNode.Lam(ty, body) => + whnf_nd_apply_beta(spine, head, types, top, addrs), + KExprNode.Const(idx, lvls) => + whnf_nd_const_head(idx, lvls, head, spine, types, top, addrs), + KExprNode.Let(_, val, body) => + let next = expr_inst1(body, val, 0); + whnf_nd_with_spine(next, spine, types, top, addrs), + KExprNode.Proj(tidx, fidx, inner) => + whnf_nd_proj_head(tidx, fidx, inner, spine, types, top, addrs), + _ => apply_spine(head, spine), + } + } + + fn whnf_nd_apply_beta(spine: List‹KExpr›, lam: KExpr, types: List‹KExpr›, + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + match peel_beta(lam, spine, store(ListNode.Nil)) { + (deep, consumed, rest) => + match list_length(consumed) { + 0 => apply_spine(lam, spine), + 1 => + let body2 = expr_inst1(deep, list_lookup(consumed, 0), 0); + whnf_nd_with_spine(body2, rest, types, top, addrs), + _ => + let body2 = expr_inst_many(deep, consumed, 0); + whnf_nd_with_spine(body2, rest, types, top, addrs), + }, + } + } + + fn whnf_nd_proj_head(tidx: G, fidx: G, inner: KExpr, spine: List‹KExpr›, + types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + let inner_whnf = whnf_nd(inner, types, top, addrs); + let inner_pair = collect_spine(inner_whnf); + match inner_pair { + (inner_head, inner_args) => + let fvd_pair = try_reduce_fin_val_decidable_rec(tidx, fidx, inner_head, inner_args, addrs); + match fvd_pair { + (1, rewritten) => whnf_nd_with_spine(rewritten, spine, types, top, addrs), + (0, _) => + match load(inner_head) { + KExprNode.Const(cidx, _) => + let cci = load(list_lookup(top, cidx)); + match cci { + KConstantInfo.Ctor(_, _, _, _, nparams, _, _) => + let field = list_lookup_or_nil(inner_args, nparams + fidx); + whnf_nd_with_spine(field, spine, types, top, addrs), + _ => + let stuck = store(KExprNode.Proj(tidx, fidx, inner_whnf)); + apply_spine(stuck, spine), + }, + _ => + let stuck = store(KExprNode.Proj(tidx, fidx, inner_whnf)); + apply_spine(stuck, spine), + }, + }, + } + } + + -- The difference from `whnf_const_head`: Defn arm returns stuck instead of + -- unfolding. Iota, quot, primitives, proj-defs still apply. + fn whnf_nd_const_head(idx: G, lvls: List‹&KLevel›, head: KExpr, spine: List‹KExpr›, + types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + let head_addr = list_lookup(addrs, idx); + let ci = load(list_lookup(top, idx)); + match ci { + KConstantInfo.Rec(num_lvls, _, num_params, num_indices, num_motives, num_minors, rules, k_flag, _, _) => + let iota = try_iota(lvls, spine, num_lvls, num_params, num_indices, num_motives, num_minors, rules, k_flag, types, top, addrs); + match iota { + (1, reduced2) => whnf_nd(reduced2, types, top, addrs), + (0, _) => apply_spine(head, spine), + }, + KConstantInfo.Quot(_, _, kind) => + let qiota = try_quot_iota(kind, spine, types, top, addrs); + match qiota { + (1, reduced_q) => whnf_nd(reduced_q, types, top, addrs), + (0, _) => apply_spine(head, spine), + }, + _ => + let addr_prim = match prim_any_addr(head_addr) { + 1 => try_address_primitives(head_addr, idx, lvls, spine, types, top, addrs), + _ => (0, store(KExprNode.BVar(0))), + }; + match addr_prim { + (1, reduced) => whnf_nd(reduced, types, top, addrs), + (0, _) => + let proj_def_pair = try_reduce_projection_definition(idx, spine, top); + match proj_def_pair { + (1, reduced_pd) => whnf_nd(reduced_pd, types, top, addrs), + (0, _) => + -- Defn / Thm / etc.: STUCK in no-delta mode. The whole point. + apply_spine(head, spine), + }, + }, + } + } + -- No fuel limit (unlike Rust's `MAX_WHNF_FUEL = 10_000` in -- `src/ix/kernel/tc.rs`). In a zk prover context, divergent input simply -- fails to produce a proof — the caller guarantees termination, so a @@ -641,7 +776,6 @@ def whnf := ⟦ match is_rec { 0 => let major = list_lookup(spine, major_idx); - -- Prop guard: refuse if major's type is Prop. let major_ty = k_infer(major, types, top, addrs); let prop_p = is_prop_type(major_ty, types, top, addrs); match prop_p { From fb1a13e1eecd03a1177419997c88bc134724691c Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Fri, 19 Jun 2026 04:46:06 -0700 Subject: [PATCH 2/8] IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `u64_sub_with_borrow` combines two per-byte borrow bits with `g_or`. The two bits are MUTUALLY EXCLUSIVE: `u_t = borrow(a_i - b_i)` and `u_r = borrow((a_i + 256 - b_i) - br_in)`. If `u_t = 1` the intermediate `t_i ≥ 1`, so subtracting `br_in ∈ {0,1}` cannot underflow ⇒ `u_r = 0`. Field `+` substitutes for `g_or` directly (per the same pattern as `u64_add` in `ByteStream.lean`). Per Aiur cost model, `g_or` adds +1 aux + 1 lookup per call; field `+` is free. 8 g_or call sites in `u64_sub_with_borrow` each charged on every one of the function's 2.23M rows. Measured (FFT cost) on UTF-8 `_proof_1_8`: 39.12B → 38.14B (-2.6%) Nat.add_comm unchanged (55.63M). See [[reference_aiur_carry_add]]. --- Ix/IxVM/Kernel/Primitive.lean | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/Ix/IxVM/Kernel/Primitive.lean b/Ix/IxVM/Kernel/Primitive.lean index 9300ea1c8..8e052ba11 100644 --- a/Ix/IxVM/Kernel/Primitive.lean +++ b/Ix/IxVM/Kernel/Primitive.lean @@ -745,31 +745,36 @@ def primitive := ⟦ } -- Mirror: byte-wise u64_sub with explicit final borrow. + -- Per-byte: u_t = borrow(a_i - b_i); u_r = borrow((a_i + 256 - b_i) - br_in). + -- u_t = 1 ⇒ a_i + 256 - b_i ≥ 1 ⇒ subtracting br_in ∈ {0,1} cannot underflow + -- ⇒ u_r = 0. So `u_t` and `u_r` are mutually-exclusive 0/1 values; field `+` + -- substitutes for `g_or` (which charges +1 aux +1 lookup per call). See + -- [[reference_aiur_carry_add]]. fn u64_sub_with_borrow(a: U64, b: U64) -> (U64, G) { let [a0, a1, a2, a3, a4, a5, a6, a7] = a; let [b0, b1, b2, b3, b4, b5, b6, b7] = b; let (r0, br1) = u8_sub(a0, b0); let (t1, u_t1) = u8_sub(a1, b1); let (r1, u_r1) = u8_sub(t1, br1); - let br2 = g_or(to_field(u_t1), to_field(u_r1)); + let br2 = to_field(u_t1) + to_field(u_r1); let (t2, u_t2) = u8_sub(a2, b2); let (r2, u_r2) = u8_sub(t2, u8_from_field_unsafe(br2)); - let br3 = g_or(to_field(u_t2), to_field(u_r2)); + let br3 = to_field(u_t2) + to_field(u_r2); let (t3, u_t3) = u8_sub(a3, b3); let (r3, u_r3) = u8_sub(t3, u8_from_field_unsafe(br3)); - let br4 = g_or(to_field(u_t3), to_field(u_r3)); + let br4 = to_field(u_t3) + to_field(u_r3); let (t4, u_t4) = u8_sub(a4, b4); let (r4, u_r4) = u8_sub(t4, u8_from_field_unsafe(br4)); - let br5 = g_or(to_field(u_t4), to_field(u_r4)); + let br5 = to_field(u_t4) + to_field(u_r4); let (t5, u_t5) = u8_sub(a5, b5); let (r5, u_r5) = u8_sub(t5, u8_from_field_unsafe(br5)); - let br6 = g_or(to_field(u_t5), to_field(u_r5)); + let br6 = to_field(u_t5) + to_field(u_r5); let (t6, u_t6) = u8_sub(a6, b6); let (r6, u_r6) = u8_sub(t6, u8_from_field_unsafe(br6)); - let br7 = g_or(to_field(u_t6), to_field(u_r6)); + let br7 = to_field(u_t6) + to_field(u_r6); let (t7, u_t7) = u8_sub(a7, b7); let (r7, u_r7) = u8_sub(t7, u8_from_field_unsafe(br7)); - let final_borrow = g_or(to_field(u_t7), to_field(u_r7)); + let final_borrow = to_field(u_t7) + to_field(u_r7); ([r0, r1, r2, r3, r4, r5, r6, r7], final_borrow) } From c807fa59104212b108dc9ddb34705fdaed73b409 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Fri, 19 Jun 2026 04:48:51 -0700 Subject: [PATCH 3/8] IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Same mutually-exclusive-carry pattern as `u64_sub_with_borrow`: * `klimbs_add_carry`: u64_add of (la, lb) yields carry1; u64_add of (sum1, carry_in) yields carry2. carry1=1 ⇒ sum1 ≤ 2^64-2 ⇒ carry2=0. * `klimbs_sub_borrow`: symmetric for borrows. Replace `g_or(c1, c2)` with `c1 + c2` (field +). Both helpers run on hot Nat-primitive paths. Measured on UTF-8 `_proof_1_8`: 38.14B → 38.07B (-0.18%) Nat.add_comm unchanged. See [[reference_aiur_carry_add]]. --- Ix/IxVM/Kernel/Primitive.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Ix/IxVM/Kernel/Primitive.lean b/Ix/IxVM/Kernel/Primitive.lean index 8e052ba11..f4fe25e49 100644 --- a/Ix/IxVM/Kernel/Primitive.lean +++ b/Ix/IxVM/Kernel/Primitive.lean @@ -732,7 +732,9 @@ def primitive := ⟦ let pair2 = u64_add(sum1, [u8_from_field_unsafe(carry), 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]); match pair2 { (sum2, carry2) => - let total_carry = g_or(to_field(carry1), to_field(carry2)); + -- carry1, carry2 mutually exclusive: carry1=1 ⇒ sum1 ≤ + -- 2^64-2 ⇒ sum1 + carry_in ≤ 2^64-1 ⇒ carry2=0. + let total_carry = to_field(carry1) + to_field(carry2); store(ListNode.Cons(sum2, klimbs_add_carry(ra, rb, total_carry))), }, }, @@ -819,7 +821,9 @@ def primitive := ⟦ let pair2 = u64_sub_with_borrow(sum1, [u8_from_field_unsafe(borrow), 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]); match pair2 { (sum2, br2) => - let total = g_or(br1, br2); + -- br1, br2 mutually exclusive: br1=1 ⇒ sum1 ≥ 1 ⇒ + -- sum1 - borrow ≥ 0 ⇒ br2=0. + let total = br1 + br2; let rec_pair = klimbs_sub_borrow(ra, rb, total); match rec_pair { (rest_res, br_final) => From be37cf929c2abbd8b83dd0f4b4c4947ec4deb1f8 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Fri, 19 Jun 2026 04:57:26 -0700 Subject: [PATCH 4/8] =?UTF-8?q?IxVM=20kernel:=20hot/cold=20split=20try=5Fn?= =?UTF-8?q?at=5Fdispatch=20=E2=80=94=20extract=20binop=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `try_nat_dispatch` ran 1.12M rows in UTF-8 `_proof_1_8` at width 90, charging 5.16% of total FFT. Width was floored by its widest match arm (the binop branch with 2× whnf + 2× try_extract_nat + try_nat_binop_addr + apply_spine), even on Nat.succ / Nat.pred rows that never touched it. Factor binop dispatch into its own `try_nat_binop_dispatch` fn. Main dispatcher narrows to the max of succ / pred arms (single whnf + try_extract_nat + klimbs_succ/dec + apply_spine). The cold fn's width only charges the rows that actually dispatch a binop. Measured on UTF-8 `_proof_1_8`: 38.07B → 37.80B (-0.7%) Nat.add_comm unchanged. --- Ix/IxVM/Kernel/Primitive.lean | 56 ++++++++++++++++++++--------------- 1 file changed, 32 insertions(+), 24 deletions(-) diff --git a/Ix/IxVM/Kernel/Primitive.lean b/Ix/IxVM/Kernel/Primitive.lean index f4fe25e49..97d40b006 100644 --- a/Ix/IxVM/Kernel/Primitive.lean +++ b/Ix/IxVM/Kernel/Primitive.lean @@ -1383,8 +1383,6 @@ def primitive := ⟦ let is_succ = address_eq(head_addr, nat_succ_addr()); match is_succ { 1 => - -- Mirror: whnf.rs:1789-1822 try_reduce_nat_succ_iter. Single arg; - -- whnf, fold to Lit(n+1) on hit. match u32_less_than(spine_len, 1) { 1 => (0, store(KExprNode.BVar(0))), 0 => @@ -1410,30 +1408,40 @@ def primitive := ⟦ _ => (0, store(KExprNode.BVar(0))), }, }, - 0 => - -- Binary ops: require 2 args. - match u32_less_than(spine_len, 2) { - 1 => (0, store(KExprNode.BVar(0))), - 0 => - let a0_w = whnf(list_lookup(spine, 0), types, top, addrs); - let a1_w = whnf(list_lookup(spine, 1), types, top, addrs); - let pa = try_extract_nat(a0_w, addrs); - let pb = try_extract_nat(a1_w, addrs); - match pa { - (1, na) => - match pb { - (1, nb) => - match try_nat_binop_addr(head_addr, na, nb, addrs) { - (1, result) => - let post = list_drop(spine, 2); - (1, apply_spine(result, post)), - (0, _) => (0, store(KExprNode.BVar(0))), - }, - _ => (0, store(KExprNode.BVar(0))), - }, - _ => (0, store(KExprNode.BVar(0))), + 0 => try_nat_binop_dispatch(head_addr, spine, spine_len, types, top, addrs), + }, + } + } + + -- Cold-extracted binop arm (mirror [[reference_aiur_hot_cold_split]]). + -- Binop dispatch is the widest arm of `try_nat_dispatch` (2× whnf + 2× + -- try_extract_nat + try_nat_binop_addr + apply_spine), so it pays + -- max-arm-width on every Nat.succ/Nat.pred row when inlined. Factored + -- here so its width only charges the rows that actually dispatch a + -- binop. + fn try_nat_binop_dispatch(head_addr: Addr, spine: List‹KExpr›, spine_len: G, + types: List‹KExpr›, top: List‹&KConstantInfo›, + addrs: List‹Addr›) -> (G, KExpr) { + match u32_less_than(spine_len, 2) { + 1 => (0, store(KExprNode.BVar(0))), + 0 => + let a0_w = whnf(list_lookup(spine, 0), types, top, addrs); + let a1_w = whnf(list_lookup(spine, 1), types, top, addrs); + let pa = try_extract_nat(a0_w, addrs); + let pb = try_extract_nat(a1_w, addrs); + match pa { + (1, na) => + match pb { + (1, nb) => + match try_nat_binop_addr(head_addr, na, nb, addrs) { + (1, result) => + let post = list_drop(spine, 2); + (1, apply_spine(result, post)), + (0, _) => (0, store(KExprNode.BVar(0))), }, + _ => (0, store(KExprNode.BVar(0))), }, + _ => (0, store(KExprNode.BVar(0))), }, } } From fb5242c3aeadf7359b4e1a5b341ad69b3845ba36 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Fri, 19 Jun 2026 05:02:19 -0700 Subject: [PATCH 5/8] =?UTF-8?q?IxVM=20kernel:=20hot/cold=20split=20expr=5F?= =?UTF-8?q?lbr=20=E2=80=94=20extract=20Let=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `expr_lbr` ran 1.47M rows in UTF-8 `_proof_1_8` at width 39, charging 3.01% of total FFT. The Let arm (3 recursive expr_lbr calls + 2 lbr_max + 1 lbr_dec) is the widest match arm, charged on every row of expr_lbr even though Let is rare in most expressions encountered. Factor the Let arm into `expr_lbr_let(ty, val, body)`. Main expr_lbr narrows to max of the 2-recursion arms (App / Lam / Forall). Cold fn only charges Let-arm rows. Measured: Nat.add_comm: 55.63M → 55.50M (-0.2%) UTF-8 `_proof_1_8`: 37.80B → 37.62B (-0.5%) --- Ix/IxVM/Kernel/Subst.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Ix/IxVM/Kernel/Subst.lean b/Ix/IxVM/Kernel/Subst.lean index e37d1e0d7..17bc657fd 100644 --- a/Ix/IxVM/Kernel/Subst.lean +++ b/Ix/IxVM/Kernel/Subst.lean @@ -56,13 +56,19 @@ def subst := ⟦ lbr_max(expr_lbr(ty), lbr_dec(expr_lbr(body))), KExprNode.Forall(ty, body) => lbr_max(expr_lbr(ty), lbr_dec(expr_lbr(body))), - KExprNode.Let(ty, val, body) => - lbr_max(lbr_max(expr_lbr(ty), expr_lbr(val)), - lbr_dec(expr_lbr(body))), + KExprNode.Let(ty, val, body) => expr_lbr_let(ty, val, body), KExprNode.Proj(_, _, e1) => expr_lbr(e1), } } + -- Cold-extracted Let arm: 3 recursive expr_lbr calls is the widest arm, + -- charged on every row of `expr_lbr` even though Let is rare in most + -- expressions. Its own circuit costs only the Let-arm rows. + fn expr_lbr_let(ty: KExpr, val: KExpr, body: KExpr) -> G { + lbr_max(lbr_max(expr_lbr(ty), expr_lbr(val)), + lbr_dec(expr_lbr(body))) + } + fn lbr_max(a: G, b: G) -> G { match u32_less_than(a, b) { 1 => b, From e1f7ba6e365ff1ec853a696e984cfa9471e0a279 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Fri, 19 Jun 2026 05:08:06 -0700 Subject: [PATCH 6/8] =?UTF-8?q?IxVM=20kernel:=20hot/cold=20split=20try=5Fe?= =?UTF-8?q?xtract=5Fnat=20=E2=80=94=20extract=20App=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `try_extract_nat` ran 1.12M rows at width 45, charging 2.68% of UTF-8 `_proof_1_8` total FFT. The App arm (list_lookup + address_eq + recursive try_extract_nat + klimbs_succ) is the widest match arm; the Lit / Const / default arms are leaf compares. Factor App into `try_extract_nat_app(f, a, addrs)`. Main extractor narrows to leaf-arm width. Cold fn only charges App-arm rows. Measured on UTF-8 `_proof_1_8`: 37.62B → 37.31B (-0.8%) Nat.add_comm unchanged. --- Ix/IxVM/Kernel/Primitive.lean | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/Ix/IxVM/Kernel/Primitive.lean b/Ix/IxVM/Kernel/Primitive.lean index 97d40b006..da0e73fd5 100644 --- a/Ix/IxVM/Kernel/Primitive.lean +++ b/Ix/IxVM/Kernel/Primitive.lean @@ -1293,19 +1293,25 @@ def primitive := ⟦ 1 => (1, store(ListNode.Nil)), 0 => (0, store(ListNode.Nil)), }, - KExprNode.App(f, a) => - match load(f) { - KExprNode.Const(idx, _) => - let head_addr_ = list_lookup(addrs, idx); - match address_eq(head_addr_, nat_succ_addr()) { - 1 => - match try_extract_nat(a, addrs) { - (1, pred_limbs) => (1, klimbs_succ(pred_limbs)), - _ => (0, store(ListNode.Nil)), - }, - 0 => (0, store(ListNode.Nil)), + KExprNode.App(f, a) => try_extract_nat_app(f, a, addrs), + _ => (0, store(ListNode.Nil)), + } + } + + -- Cold-extracted App arm: list_lookup + address_eq + recursive + -- try_extract_nat + klimbs_succ is the widest arm; pulling it out lets + -- `try_extract_nat`'s main width drop to the leaf-arm width. + fn try_extract_nat_app(f: KExpr, a: KExpr, addrs: List‹Addr›) -> (G, KLimbs) { + match load(f) { + KExprNode.Const(idx, _) => + let head_addr_ = list_lookup(addrs, idx); + match address_eq(head_addr_, nat_succ_addr()) { + 1 => + match try_extract_nat(a, addrs) { + (1, pred_limbs) => (1, klimbs_succ(pred_limbs)), + _ => (0, store(ListNode.Nil)), }, - _ => (0, store(ListNode.Nil)), + 0 => (0, store(ListNode.Nil)), }, _ => (0, store(ListNode.Nil)), } From 1e409874864a90d52b0c35d61c86a2afe1b3d24b Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Fri, 19 Jun 2026 05:21:31 -0700 Subject: [PATCH 7/8] Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Updates 41 pinned FFT costs in `Tests/Ix/IxVM.lean::kernelCheckEntries` to match the new kernel's output. All pins moved DOWN — every constant got cheaper, none regressed. Largest reductions (% change): Vector.append: 4_023_268_168 → 3_160_970_390 (-21.4%) Array.append_assoc: 3_938_574_533 → 3_079_334_815 (-21.8%) String.Internal.append: 793_580_333 → 775_968_134 ( -2.2%) bv_to_nat_lit: 635_780_327 → 619_870_154 ( -2.5%) nat_gcd_lit: 665_518_356 → 649_859_784 ( -2.4%) Nat.sub_le_of_le_add: 567_575_653 → 557_867_526 ( -1.7%) IxVMPrim.nat_mod_lit: 414_695_549 → 407_517_834 ( -1.7%) IxVMPrim.nat_div_lit: 405_607_545 → 398_641_590 ( -1.7%) IxVMPrim.nat_shr_lit: 411_128_901 → 404_158_486 ( -1.7%) Nat.decLe: 209_641_496 → 206_196_563 ( -1.6%) Nat.add_comm: 56_084_908 → 55_504_714 ( -1.0%) `lake test -- --ignored ixvm` passes with 0 FFT mismatches. --- Tests/Ix/IxVM.lean | 82 +++++++++++++++++++++++----------------------- 1 file changed, 41 insertions(+), 41 deletions(-) diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 776b93661..807f27eb2 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -115,52 +115,52 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : observed cost in the message so it can be pasted back. -/ private def kernelCheckEntries : List (String × Nat) := [ -- Stdlib - ("HEq", 1_716_582), - ("HEq.rec", 2_692_988), - ("Eq.rec", 2_575_400), - ("Nat", 1_857_523), - ("Nat.add", 13_343_000), - ("Nat.add_comm", 56_084_908), - ("Nat.decEq", 71_921_625), - ("Nat.decLe", 209_641_496), - ("Nat.sub_le_of_le_add", 567_575_653), + ("HEq", 1_716_231), + ("HEq.rec", 2_689_147), + ("Eq.rec", 2_573_006), + ("Nat", 1_857_475), + ("Nat.add", 13_174_565), + ("Nat.add_comm", 55_504_714), + ("Nat.decEq", 70_617_453), + ("Nat.decLe", 206_196_563), + ("Nat.sub_le_of_le_add", 557_867_526), -- Newly-unlocked targets (level_leq Géran normalize). - ("Trans.mk", 2_911_629), - ("Array.append_assoc", 3_938_574_533), - ("Vector.append", 4_023_268_168), + ("Trans.mk", 2_902_315), + ("Array.append_assoc", 3_079_334_815), + ("Vector.append", 3_160_970_390), -- Primitive reduction theorems (`IxVMPrim`) - ("IxVMPrim.nat_add_lit", 28_639_807), - ("IxVMPrim.nat_sub_lit", 34_436_244), - ("IxVMPrim.nat_mul_lit", 25_101_067), - ("IxVMPrim.nat_mul_big", 24_580_879), - ("IxVMPrim.nat_div_lit", 405_607_545), - ("IxVMPrim.nat_mod_lit", 414_695_549), - ("IxVMPrim.nat_succ_lit", 7_330_826), - ("IxVMPrim.nat_pred_lit", 14_804_098), - ("IxVMPrim.nat_gcd_lit", 665_518_356), - ("IxVMPrim.nat_land_lit", 1_138_665_214), - ("IxVMPrim.nat_lor_lit", 1_139_887_801), - ("IxVMPrim.nat_xor_lit", 1_149_371_965), - ("IxVMPrim.nat_shl_lit", 35_417_490), - ("IxVMPrim.nat_shr_lit", 411_128_901), - ("IxVMPrim.nat_beq_lit", 24_752_029), - ("IxVMPrim.nat_ble_lit", 23_016_526), - ("IxVMPrim.nat_dec_le", 216_661_883), - ("IxVMPrim.nat_dec_lt", 220_751_034), - ("IxVMPrim.nat_dec_eq", 86_118_842), - ("IxVMPrim.str_size_lit", 802_563_877), - ("IxVMPrim.bv_to_nat_lit", 635_780_327), + ("IxVMPrim.nat_add_lit", 28_456_739), + ("IxVMPrim.nat_sub_lit", 34_198_852), + ("IxVMPrim.nat_mul_lit", 24_891_009), + ("IxVMPrim.nat_mul_big", 24_371_642), + ("IxVMPrim.nat_div_lit", 398_641_590), + ("IxVMPrim.nat_mod_lit", 407_517_834), + ("IxVMPrim.nat_succ_lit", 7_328_956), + ("IxVMPrim.nat_pred_lit", 14_758_385), + ("IxVMPrim.nat_gcd_lit", 649_859_784), + ("IxVMPrim.nat_land_lit", 1_116_700_968), + ("IxVMPrim.nat_lor_lit", 1_117_922_443), + ("IxVMPrim.nat_xor_lit", 1_127_404_404), + ("IxVMPrim.nat_shl_lit", 35_193_480), + ("IxVMPrim.nat_shr_lit", 404_158_486), + ("IxVMPrim.nat_beq_lit", 24_527_554), + ("IxVMPrim.nat_ble_lit", 22_813_110), + ("IxVMPrim.nat_dec_le", 213_176_101), + ("IxVMPrim.nat_dec_lt", 217_273_299), + ("IxVMPrim.nat_dec_eq", 84_744_092), + ("IxVMPrim.str_size_lit", 784_847_922), + ("IxVMPrim.bv_to_nat_lit", 619_870_154), -- Mutual block + multi-member recursors - ("IxVMInd.Even", 26_482_492), - ("IxVMInd.Odd", 26_245_849), - ("IxVMInd.Even.rec", 32_164_273), - ("IxVMInd.Odd.rec", 32_163_380), + ("IxVMInd.Even", 26_296_709), + ("IxVMInd.Odd", 26_060_068), + ("IxVMInd.Even.rec", 31_974_039), + ("IxVMInd.Odd.rec", 31_973_146), -- Nested inductive + aux recursor (Tree.mk : List Tree → Tree) - ("IxVMInd.Tree", 2_633_415), - ("IxVMInd.Tree.rec", 4_858_321), + ("IxVMInd.Tree", 2_632_931), + ("IxVMInd.Tree.rec", 4_855_972), -- Edge cases from prelude - ("String.Internal.append", 793_580_333), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_197_925_029), + ("String.Internal.append", 775_968_134), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_173_017_464), ] private def nameOfString (str : String) : Lean.Name := From 920b48079bc1ec1ee9708336621c9ec3549e79e8 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Wed, 24 Jun 2026 10:39:34 -0700 Subject: [PATCH 8/8] IxVM kernel: document k_infer_only safety invariant + planned hint shape MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `k_infer_only` section header skipped over the fact that the function is only sound on well-typed inputs (since it drops `k_check(a, dom)` on `App`, `k_ensure_sort(ty)` on `Lam`, val/ty checks on `Let`). Spell out: * The invariant — only call on terms produced by `whnf` of a well-typed term, never on arbitrary inputs. * Why the current sites (`try_proof_irrel`, `is_prop_type`, `try_unit_like`) respect it. * The planned non-deterministic-hint dispatch (`Hint::{None, KInfer, KInferOnly}`) that lets us share `k_infer`'s memo where a hit already exists instead of paying the parallel `infer_only` memo cost. --- Ix/IxVM/Kernel/Infer.lean | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/Ix/IxVM/Kernel/Infer.lean b/Ix/IxVM/Kernel/Infer.lean index e35f76bc8..d082168c1 100644 --- a/Ix/IxVM/Kernel/Infer.lean +++ b/Ix/IxVM/Kernel/Infer.lean @@ -191,6 +191,43 @@ def infer := ⟦ -- `k_infer` (parity with Rust's separate infer_cache / infer_only_cache). -- Used at try_proof_irrel / is_prop_type / try_unit_like where only the -- synthesized type is needed. + -- + -- ## Safety invariant + -- + -- `k_infer_only` is NOT safe to call on an arbitrary term — only on terms + -- already known to be well-typed (i.e., terms that would have passed + -- `k_infer`). The reason: our overall invariant is that evaluation only + -- happens after typechecking. `k_infer_only` evaluates types (e.g. the + -- substitution `B[a/x]` on an `App` arm) WITHOUT first checking that the + -- substituted-in argument `a` has the proper type (the dropped + -- `k_check(a, dom)`). On an untyped or ill-typed term, that substitution + -- can take us out of the well-typed fragment, after which subsequent + -- `whnf` / `def_eq` work is unsound. + -- + -- The current call sites (`try_proof_irrel`, `is_prop_type`, + -- `try_unit_like`) honor this invariant because they hand `k_infer_only` + -- a term obtained by `whnf`-ing a well-typed input. `whnf` of a + -- well-typed term yields a structurally different but still well-typed + -- term, so the no-checks shortcut is sound there even though the result + -- term itself was never the direct subject of `k_infer`. + -- + -- ## Future: shared memo via non-deterministic hint + -- + -- `k_infer_only`'s separate memo (parity with Rust) means an `infer_only` + -- call cannot reuse an existing `k_infer` hit on the same input. A + -- planned improvement: at each `try_proof_irrel` / `try_unit_like` site, + -- the prover supplies a hint `enum Hint { None, KInfer, KInferOnly }`: + -- 1. `None` — term is not unit-like and not a proof; skip both + -- and fall through to deep `def_eq`. + -- 2. `KInfer` — `k_infer`'s memo is a hit on this input; call + -- `k_infer` (cheap, reuses the cached row) and + -- check the result is a proof / unit-like. + -- 3. `KInferOnly` — `k_infer`'s memo would miss; call `k_infer_only` + -- (cheaper than a fresh `k_infer`) and check. + -- Dispatching on the hint with a `match` lets us share `k_infer`'s memo + -- where available and fall back to `k_infer_only` only when the cheaper + -- path won't pay off, instead of unconditionally paying the parallel + -- `infer_only` memo cost. -- ============================================================================ fn k_infer_only(e: KExpr, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr {