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

Merged

arthurpaulino merged 8 commits into

mainfrom

ap/utf8-tier-1d

Jun 25, 2026

Commits on Jun 24, 2026

IxVM kernel: Tier 1d def-eq short-circuit (whnf_nd + quick_def_eq + post-spine-congruence)
arthurpaulino
committed
1e0e766
IxVM kernel: drop g_or from u64_sub_with_borrow (replace with field +)
arthurpaulino
committed
fb1a13e
IxVM kernel: drop g_or from klimbs_add_carry / klimbs_sub_borrow
arthurpaulino
committed
c807fa5
IxVM kernel: hot/cold split try_nat_dispatch — extract binop arm
arthurpaulino
committed
be37cf9
IxVM kernel: hot/cold split expr_lbr — extract Let arm
arthurpaulino
committed
fb5242c
IxVM kernel: hot/cold split try_extract_nat — extract App arm
arthurpaulino
committed
e1f7ba6
Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations
arthurpaulino
committed
1e40987
IxVM kernel: document k_infer_only safety invariant + planned hint shape
arthurpaulino
committed
920b480