IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into from
Jun 25, 2026
Merged

IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
1e0e766
IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…
arthurpaulino Jun 19, 2026
fb1a13e
IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)
arthurpaulino Jun 19, 2026
c807fa5
IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow
arthurpaulino Jun 19, 2026
be37cf9
IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm
arthurpaulino Jun 19, 2026
fb5242c
IxVM kernel: hot/cold split expr_lbr — extract Let arm
arthurpaulino Jun 19, 2026
e1f7ba6
IxVM kernel: hot/cold split try_extract_nat — extract App arm
arthurpaulino Jun 19, 2026
1e40987
Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations
arthurpaulino Jun 19, 2026
920b480
IxVM kernel: document k_infer_only safety invariant + planned hint shape
arthurpaulino Jun 24, 2026
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
64 changes: 59 additions & 5 deletions Ix/IxVM/Kernel/DefEq.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
}
}

-- 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) =>
Expand All@@ -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),
}
}
Expand Down
139 changes: 139 additions & 0 deletions Ix/IxVM/Kernel/Infer.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
--
-- ## 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 {
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,
},
}
}

Comment thread
arthurpaulino marked this conversation as resolved.
-- ============================================================================
-- Helpers: extract const declared type, Nat/Str literal types.
-- ============================================================================
Expand Down
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into

from

Jun 25, 2026
 Merged


IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts
#450
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


8 commits


Select commit
Hold shift + click to select a range
1e0e766

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…


arthurpaulino Jun 19, 2026
fb1a13e

IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)


arthurpaulino Jun 19, 2026
c807fa5

IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow


arthurpaulino Jun 19, 2026
be37cf9

IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm


arthurpaulino Jun 19, 2026
fb5242c

IxVM kernel: hot/cold split expr_lbr — extract Let arm


arthurpaulino Jun 19, 2026
e1f7ba6

IxVM kernel: hot/cold split try_extract_nat — extract App arm


arthurpaulino Jun 19, 2026
1e40987

Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations


arthurpaulino Jun 19, 2026
920b480

IxVM kernel: document k_infer_only safety invariant + planned hint shape


arthurpaulino Jun 24, 2026

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


64 changes: 59 additions & 5 deletions
Ix/IxVM/Kernel/DefEq.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
 }
 }

 -- 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) =>
Expand All@@ -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),
 }
 }
Expand Down

139 changes: 139 additions & 0 deletions
Ix/IxVM/Kernel/Infer.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
 --
 -- ## 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 {
 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,
 },
 }
 }

Comment thread
arthurpaulino marked this conversation as resolved.

 -- ============================================================================
 -- Helpers: extract const declared type, Nat/Str literal types.
 -- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into

from

Jun 25, 2026
 Merged


IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts
#450
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


8 commits


Select commit
Hold shift + click to select a range
1e0e766

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…


arthurpaulino Jun 19, 2026
fb1a13e

IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)


arthurpaulino Jun 19, 2026
c807fa5

IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow


arthurpaulino Jun 19, 2026
be37cf9

IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm


arthurpaulino Jun 19, 2026
fb5242c

IxVM kernel: hot/cold split expr_lbr — extract Let arm


arthurpaulino Jun 19, 2026
e1f7ba6

IxVM kernel: hot/cold split try_extract_nat — extract App arm


arthurpaulino Jun 19, 2026
1e40987

Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations


arthurpaulino Jun 19, 2026
920b480

IxVM kernel: document k_infer_only safety invariant + planned hint shape


arthurpaulino Jun 24, 2026

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


64 changes: 59 additions & 5 deletions
Ix/IxVM/Kernel/DefEq.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
 }
 }

 -- 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) =>
Expand All@@ -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),
 }
 }
Expand Down

139 changes: 139 additions & 0 deletions
Ix/IxVM/Kernel/Infer.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
 --
 -- ## 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 {
 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,
 },
 }
 }

Comment thread
arthurpaulino marked this conversation as resolved.

 -- ============================================================================
 -- Helpers: extract const declared type, Nat/Str literal types.
 -- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into

from

Jun 25, 2026
 Merged


IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts
#450
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


8 commits


Select commit
Hold shift + click to select a range
1e0e766

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…


arthurpaulino Jun 19, 2026
fb1a13e

IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)


arthurpaulino Jun 19, 2026
c807fa5

IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow


arthurpaulino Jun 19, 2026
be37cf9

IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm


arthurpaulino Jun 19, 2026
fb5242c

IxVM kernel: hot/cold split expr_lbr — extract Let arm


arthurpaulino Jun 19, 2026
e1f7ba6

IxVM kernel: hot/cold split try_extract_nat — extract App arm


arthurpaulino Jun 19, 2026
1e40987

Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations


arthurpaulino Jun 19, 2026
920b480

IxVM kernel: document k_infer_only safety invariant + planned hint shape


arthurpaulino Jun 24, 2026

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


64 changes: 59 additions & 5 deletions
Ix/IxVM/Kernel/DefEq.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
 }
 }

 -- 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) =>
Expand All@@ -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),
 }
 }
Expand Down

139 changes: 139 additions & 0 deletions
Ix/IxVM/Kernel/Infer.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
 --
 -- ## 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 {
 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,
 },
 }
 }

Comment thread
arthurpaulino marked this conversation as resolved.

 -- ============================================================================
 -- Helpers: extract const declared type, Nat/Str literal types.
 -- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into

from

Jun 25, 2026
 Merged


IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts
#450
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


8 commits


Select commit
Hold shift + click to select a range
1e0e766

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…


arthurpaulino Jun 19, 2026
fb1a13e

IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)


arthurpaulino Jun 19, 2026
c807fa5

IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow


arthurpaulino Jun 19, 2026
be37cf9

IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm


arthurpaulino Jun 19, 2026
fb5242c

IxVM kernel: hot/cold split expr_lbr — extract Let arm


arthurpaulino Jun 19, 2026
e1f7ba6

IxVM kernel: hot/cold split try_extract_nat — extract App arm


arthurpaulino Jun 19, 2026
1e40987

Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations


arthurpaulino Jun 19, 2026
920b480

IxVM kernel: document k_infer_only safety invariant + planned hint shape


arthurpaulino Jun 24, 2026

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


64 changes: 59 additions & 5 deletions
Ix/IxVM/Kernel/DefEq.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
 }
 }

 -- 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) =>
Expand All@@ -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),
 }
 }
Expand Down

139 changes: 139 additions & 0 deletions
Ix/IxVM/Kernel/Infer.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
 --
 -- ## 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 {
 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,
 },
 }
 }

Comment thread
arthurpaulino marked this conversation as resolved.

 -- ============================================================================
 -- Helpers: extract const declared type, Nat/Str literal types.
 -- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into

from

Jun 25, 2026
 Merged


IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts
#450
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


8 commits


Select commit
Hold shift + click to select a range
1e0e766

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…


arthurpaulino Jun 19, 2026
fb1a13e

IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)


arthurpaulino Jun 19, 2026
c807fa5

IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow


arthurpaulino Jun 19, 2026
be37cf9

IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm


arthurpaulino Jun 19, 2026
fb5242c

IxVM kernel: hot/cold split expr_lbr — extract Let arm


arthurpaulino Jun 19, 2026
e1f7ba6

IxVM kernel: hot/cold split try_extract_nat — extract App arm


arthurpaulino Jun 19, 2026
1e40987

Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations


arthurpaulino Jun 19, 2026
920b480

IxVM kernel: document k_infer_only safety invariant + planned hint shape


arthurpaulino Jun 24, 2026

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


64 changes: 59 additions & 5 deletions
Ix/IxVM/Kernel/DefEq.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
 }
 }

 -- 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) =>
Expand All@@ -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),
 }
 }
Expand Down

139 changes: 139 additions & 0 deletions
Ix/IxVM/Kernel/Infer.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
 --
 -- ## 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 {
 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,
 },
 }
 }

Comment thread
arthurpaulino marked this conversation as resolved.

 -- ============================================================================
 -- Helpers: extract const declared type, Nat/Str literal types.
 -- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into

from

Jun 25, 2026
 Merged


IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts
#450
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


8 commits


Select commit
Hold shift + click to select a range
1e0e766

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…


arthurpaulino Jun 19, 2026
fb1a13e

IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)


arthurpaulino Jun 19, 2026
c807fa5

IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow


arthurpaulino Jun 19, 2026
be37cf9

IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm


arthurpaulino Jun 19, 2026
fb5242c

IxVM kernel: hot/cold split expr_lbr — extract Let arm


arthurpaulino Jun 19, 2026
e1f7ba6

IxVM kernel: hot/cold split try_extract_nat — extract App arm


arthurpaulino Jun 19, 2026
1e40987

Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations


arthurpaulino Jun 19, 2026
920b480

IxVM kernel: document k_infer_only safety invariant + planned hint shape


arthurpaulino Jun 24, 2026

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


64 changes: 59 additions & 5 deletions
Ix/IxVM/Kernel/DefEq.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
 }
 }

 -- 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) =>
Expand All@@ -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),
 }
 }
Expand Down

139 changes: 139 additions & 0 deletions
Ix/IxVM/Kernel/Infer.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
 --
 -- ## 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 {
 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,
 },
 }
 }

Comment thread
arthurpaulino marked this conversation as resolved.

 -- ============================================================================
 -- Helpers: extract const declared type, Nat/Str literal types.
 -- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts#450

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 8 commits into

from

Jun 25, 2026
 Merged


IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts
#450
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


8 commits


Select commit
Hold shift + click to select a range
1e0e766

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + p…


arthurpaulino Jun 19, 2026
fb1a13e

IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)


arthurpaulino Jun 19, 2026
c807fa5

IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow


arthurpaulino Jun 19, 2026
be37cf9

IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm


arthurpaulino Jun 19, 2026
fb5242c

IxVM kernel: hot/cold split expr_lbr — extract Let arm


arthurpaulino Jun 19, 2026
e1f7ba6

IxVM kernel: hot/cold split try_extract_nat — extract App arm


arthurpaulino Jun 19, 2026
1e40987

Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations


arthurpaulino Jun 19, 2026
920b480

IxVM kernel: document k_infer_only safety invariant + planned hint shape


arthurpaulino Jun 24, 2026

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


64 changes: 59 additions & 5 deletions
Ix/IxVM/Kernel/DefEq.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -104,27 +117,68 @@ 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),
 }
 }

 -- 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) =>
Expand All@@ -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),
 }
 }
Expand Down

139 changes: 139 additions & 0 deletions
Ix/IxVM/Kernel/Infer.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -184,6 +184,145 @@ 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.
 --
 -- ## 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 {
 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,
 },
 }
 }

Comment thread
arthurpaulino marked this conversation as resolved.

 -- ============================================================================
 -- Helpers: extract const declared type, Nat/Str literal types.
 -- ============================================================================
Expand Down
Loading