IxVM kernel: prim_family dispatch, H-14 skip map, dead-code removal by arthurpaulino · Pull Request #505 · argumentcomputer/ix

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

arthurpaulino · 2026-07-21T13:40:57Z

Selective port of the IxVM-side commits from sb/aiur-perf, adapted to
current main (post-#450/#457) and re-measured. Every candidate was
benchmarked before acceptance; patches that regressed FFT cost or bought
too little for their trace-width cost were dropped (details below).

Commits

Drop dead KValNode/KVal/KValEnv (f4d87d0)
Leftover NbE value-domain types with no remaining references.
Memoized prim_family dispatch + width-safe offset-stuck placement
(bbd05c4)
prim_family(addr) classifies a Const-head address into the one
reducer family that could fire (nat/str/bitvec/native/decidable —
the address sets are disjoint), memoized per distinct address, so
whnf_const_head calls at most one family reducer instead of running
the 5-reducer gauntlet. The symbolic-Nat offset-stuck check moves from
a delta-arm probe into try_nat_dispatch's miss path (verdict 2 =
"already stuck, do not re-whnf"), where the whnf'd args already exist.
Nat-literal majors expose one constructor layer via
nat_lit_to_ctor_or_self instead of materializing succ chains.
Adaptations vs the original patch: whnf_nd_const_head (no-delta
WHNF, added on main after the patch) converted to the same family
dispatch; main's cold-extracted try_nat_binop_dispatch kept, with
the symbolic-base case routed to try_nat_offset_dispatch from its
miss arm.
H-14: ptr_val skip map + lockstep addr cursor (d42865c,
originally John C. Burnham's jcb/fixes)
check_all_skipping keys the assumption-leaf skip set on ptr_val
(sound by the interning invariant; a de-interned pointer reads as
absent and the constant just gets checked — fail-closed) and walks
addrs in lockstep with consts instead of list_lookup(addrs, pos)
per constant, which was a standalone O(closure²). addr_key is
retained for the Inductive.lean block-membership table.

Measurements

lake exe ix check Nat.add_comm, cumulative vs main:

metric	main	this PR	Δ
total trace width	34,820	34,781	−39
FFT cost (add_comm)	49,571,210	48,860,647	−1.43%

All 53 pinned targets in Tests/Ix/IxVM.lean decreased
(−0.19%..−1.43%); pins updated in the same commit as the change. Full
lake test -- --ignored ixvm suite green (kernel checks, codegen/bytecode
parity, claim smokes including the frontier-assumption path, arena).
crates/ixvm-codegen regenerated per commit; clippy clean.

Dropped after measurement

4940b9f (inline lbr guards on expr_inst1_walk App children):
regressed every pin on current main (+1.1% on the heavy targets). It
was measured pre-IxVM kernel: unblock UTF-8 decode/encode proof + Nat-layer FFT cuts #450; main's cold-extracted BVar/Let arms and the
expr_inst1 lbr fast path already capture the saving, so the App-arm
guards only added per-row width.
fbedfc8 (idx-keyed projection-definition classification): +61 total
width for −0.28% FFT on its best-case constant
(Int8.instRxcHasSize_eq). Width taxes proof size and recursive
verification on every proof; the FFT win is workload-dependent. A
width-neutral variant (keep the proj_def_info_of split, drop the
is_proj_def caller gate) is worth revisiting if the SInt/UTF-8
instance class shows up in real workloads.
H-12 output caps on pow/shiftLeft (from the Rust-side branch): not
a soundness gate — capped results stay stuck, which can only reject,
never wrongly accept. It is prover-side DoS protection, and compute is
the prover's concern in a zkVM deployment. Note the resulting
divergence: the Rust kernel caps, IxVM does not, so the Rust kernel
rejects some huge-arithmetic terms IxVM accepts (benign when Rust is
used as a conservative preflight).
b9827d4 and b86c632 were already on main (IxVM kernel: canonical level normalization + FFT-cost pinning #447, feat: Add SP1 and Zisk kernel proving backends #411/IxVM: native execution pipeline #463).

From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.)

Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`.

Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated.

samuelburnham added 3 commits July 21, 2026 05:13

johnchandlerburnham approved these changes Jul 21, 2026
View reviewed changes

johnchandlerburnham merged commit d9313cd into mainJul 21, 2026
10 checks passed