From 9ceea68fc0bdd14c526b3e3a90dbc9769931a7d6 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Tue, 2 Jun 2026 11:37:53 -0700 Subject: [PATCH] IxVM: context-suffix memo keys for closed terms + drop dead KValNode MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two changes to the Aiur kernel core, both behavior-preserving. Closed-term context normalization in whnf / k_infer / k_is_def_eq: a closed term (`expr_lbr(e) == 0`) reads nothing from the local binder-type context `types` — its only reader, `types_lookup`, is reached via a `BVar` lookup, which a closed term has none of. So the result is independent of `types`; collapse it to `Nil`. The same closed subterm appearing under different binder depths then shares one memo key `(e, Nil, top, addrs)` instead of missing on a per-depth `types`, so Aiur's content-memoization reuses it. Open terms keep their real context. Sound: a closed term reduces and infers only over closed subterms. Remove the dead `KValNode`/`KVal`/`KValEnv` NbE value domain: defined but referenced nowhere (the live kernel runs on de-Bruijn `KExpr`); vestigial from an abandoned NbE direction. Measured with `ix check --ixe arena.ixe --claim ` over the TutorialDefs arena (694 consts): 7,159,028,984 -> 7,151,454,776 FFT (-0.11%). `lake test -- --ignored ixvm`: 297 pass, 0 fail. (The closed-term win is larger on a faster ingress base, where the kernel core is a bigger share of total.) --- Ix/IxVM/Kernel/DefEq.lean | 8 ++++++++ Ix/IxVM/Kernel/Infer.lean | 7 +++++++ Ix/IxVM/Kernel/Whnf.lean | 14 +++++++++++--- Ix/IxVM/KernelTypes.lean | 27 --------------------------- 4 files changed, 26 insertions(+), 30 deletions(-) diff --git a/Ix/IxVM/Kernel/DefEq.lean b/Ix/IxVM/Kernel/DefEq.lean index c5dde3b6..2227a86c 100644 --- a/Ix/IxVM/Kernel/DefEq.lean +++ b/Ix/IxVM/Kernel/DefEq.lean @@ -39,6 +39,14 @@ def defEq := ⟦ -- ============================================================================ fn k_is_def_eq(a: KExpr, b: KExpr, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G { + -- When both sides are closed, the context can't affect the result; + -- collapse it so closed comparisons share a memo key across contexts. + -- `expr_lbr >= 0`, so the sum is 0 iff both sides are closed. + let lbr = expr_lbr(a) + expr_lbr(b); + let types = match lbr { + 0 => store(ListNode.Nil), + _ => types, + }; -- Tier 1: pointer equality short-circuit. match ptr_val(a) - ptr_val(b) { 0 => 1, diff --git a/Ix/IxVM/Kernel/Infer.lean b/Ix/IxVM/Kernel/Infer.lean index 0aafb651..eac50ed8 100644 --- a/Ix/IxVM/Kernel/Infer.lean +++ b/Ix/IxVM/Kernel/Infer.lean @@ -54,6 +54,13 @@ def infer := ⟦ -- ============================================================================ fn k_infer(e: KExpr, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { + -- Closed terms don't depend on the local context: collapse it so the + -- same closed subterm under different binder depths shares a memo key. + let lbr = expr_lbr(e); + let types = match lbr { + 0 => store(ListNode.Nil), + _ => types, + }; match load(e) { KExprNode.BVar(i) => types_lookup(types, i), diff --git a/Ix/IxVM/Kernel/Whnf.lean b/Ix/IxVM/Kernel/Whnf.lean index a80c5ddb..73ccb5f3 100644 --- a/Ix/IxVM/Kernel/Whnf.lean +++ b/Ix/IxVM/Kernel/Whnf.lean @@ -224,9 +224,17 @@ def whnf := ⟦ KExprNode.Forall(_, _) => e, KExprNode.BVar(_) => e, _ => - let pair = collect_spine(e); - match pair { - (head, spine) => whnf_with_spine(head, spine, types, top, addrs), + -- Closed-term context normalization: when `e` has no loose BVars, + -- whnf's result cannot depend on `types` (every spine major is + -- closed, so the `k_infer`/`is_prop_type` calls in the struct-iota + -- path never hit a BVar). Pass `Nil` so the same closed term whnf'd + -- under different contexts shares one memo key + -- `(head, spine, Nil, top, addrs)` -> cache hits. Open `e` keeps its + -- real context. Sound: a closed term reduces only to closed terms. + let (head, spine) = collect_spine(e); + match expr_lbr(e) { + 0 => whnf_with_spine(head, spine, store(ListNode.Nil), top, addrs), + _ => whnf_with_spine(head, spine, types, top, addrs), }, } } diff --git a/Ix/IxVM/KernelTypes.lean b/Ix/IxVM/KernelTypes.lean index 950a8f2c..3577bdbe 100644 --- a/Ix/IxVM/KernelTypes.lean +++ b/Ix/IxVM/KernelTypes.lean @@ -50,33 +50,6 @@ def kernelTypes := ⟦ type KExpr = &KExprNode - -- ============================================================================ - -- Values (NbE semantic domain) - -- ============================================================================ - - enum KValNode { - Srt(&KLevel), - Lit(KLiteral), - Lam(KVal, KExpr, KValEnv), - Pi(KVal, KExpr, KValEnv), - Ctor(G, List‹&KLevel›, G, List‹KVal›), - FVar(G, KVal, List‹KVal›), - Axiom(G, List‹&KLevel›, List‹KVal›), - Defn(G, List‹&KLevel›, List‹KVal›), - Thm(G, List‹&KLevel›, List‹KVal›), - Opaque(G, List‹&KLevel›, List‹KVal›), - Quot(G, List‹&KLevel›, List‹KVal›), - Induct(G, List‹&KLevel›, List‹KVal›), - Rec(G, List‹&KLevel›, List‹KVal›), - Proj(G, G, KVal, List‹KVal›), - Thunk(KExpr, KValEnv) - } - - type KVal = &KValNode - - -- Value environment (de Bruijn indexed, front = most recent binder) - type KValEnv = List‹KVal› - -- ============================================================================ -- Recursor Rule --