IxVM kernel: cut Aiur FFT cost on reduction- and check-heavy shards

[arthurpaulino]

Summary

Eight commits across six optimization areas in the Aiur IxVM kernel, each
targeting a specific hotspot found by profiling per-function FFT cost on real
shards of a compiled Init environment. No semantics change — every shard still
checks without error, and the full lake test -- --ignored ixvm suite passes
(297 tests) at every step.

Cumulative effect on a reduction-heavy shard (Init shard 9, one owned constant,
deep reduction): 45.5G → 16.6G total FFT (−64%). The structural/keyed-lookup
areas (1–5) account for 45.5G → 37.8G; the Nat-reduction area (6) takes it the
rest of the way by collapsing two symbolic-arithmetic blowups from O(n)/O(n²) to
O(1). That same area makes a previously intractable proof class — the UTF-8 codec
lemma ByteArray.utf8DecodeChar?_utf8EncodeChar_append, whose checking spawns
deep Nat.add x 0xC0 succ-towers and c >>> 6/12/18 division-towers — reduce in
constant rather than tower-depth cost.

Method

Built a .ixe of the Init closure, profiled and sharded it
(ix profile → ix shard --shards 64), then ran ix check per shard or per
constant and read the per-function FFT table. Shards 10 (check-heavy: lookups,
address compares, deserialize) and 9 (reduction-heavy: whnf, substitution, spine
collection) exercised different profiles; small hand-built reproducers
(x + D = …, x >>> D = …) isolated and scaled the symbolic-arithmetic blowups.

Aiur cost model behind the changes: FFT ≈ per-function width × row height,
charged at the function's max-arm width on every row. Levers: (a) factor a
wide/rare arm into its own circuit, (b) cut row count via better memoization,
(c) replace linear scans with keyed lookups, (d) keep symbolic primitives compact
so they never materialize a tower.

Areas

1. Cheaper Expr.Share / universe lookups — commit 3774860.
The sharing-table and universe-array lookups walked the list with
list_lookup_u64 (per-step U64 predecessor). Switched to a field index and, for
Expr.Share, to list_drop — which returns the sublist pointer, so repeated
lookups dedup in the memo cache. Shard 10: total FFT 3.89G → 2.11G; the merged
pointer-list walk fell from 1.93G to 5.8M.

2. Hot/cold split of address_eq — commit 69b6936.
The primitive-dispatch gauntlet compares each Const head against ~50 hardcoded
addresses, making address_eq (a full 32-limb compare, width 109) the hottest
circuit. Almost every comparison differs at limb 0. Split it: address_eq
compares limb 0 only and delegates the rest to address_eq_tail, whose height is
just the rare limb-0 matches. (A nested match in the same function does nothing —
Aiur charges full width per row regardless of arm; the split must be a function
boundary.) Shard 10: width 109 → 80, 509.8M → 374.1M; total 2.106G → 1.973G.

3. Hot/cold split of whnf_with_spine — commit 0e30d78.
On reduction-heavy consts this is the single hottest circuit (width 89 × 3.36M
rows), its width set by two arms a minority of rows reach: Const-head and
Proj-head dispatch. Factored both into whnf_const_head / whnf_proj_head. The
Proj arm is the jackpot — 3.4K rows but nearly half the width. Shard 9: width
89 → 34, 6.48G → 2.48G.

4. Non-tail, single-definition collect_spine — commit 5b7fabc.
collect_spine peeled the App chain with a tail-recursive accumulator. Tail
recursion buys nothing in Aiur (stack depth is free), and the accumulator landed
in the memo key, blocking reuse — 0 cache hits across 5.38M rows. Rewrote it
non-tail, keyed on the expression alone (2.19M hits now), and merged the two
verbatim copies into one definition in kernelTypes. Shard 9: 2.65G → 0.96G.

5. Keyed skip-set for sharded check — commit a52967f.
The largest address_eq source on a sharded check was addr_in_list, an O(N)
linear scan of the assumption-leaf list per checked const (1.81M calls on shard
9). Replaced with an RBTreeMap skip-set keyed on the first 4 address bytes:
build once, membership = one rbtree lookup + one confirming address_eq. Shard 9:
address_eq 2.07M rows / 3.48G → 274K rows / 0.40G; total 41.7G → 37.8G.

6. Compact symbolic Nat reduction — commits dbc4177, 5dcab7f, d50c9a6.
Nat primitives applied to (symbolic base, literal) delta-unfolded into towers
the kernel then re-walked: Nat.add x 0xC0 → succ^192(x), and Nat.div x 2
(what x >>> k unfolds to, k times) → an exploding division algorithm. Three
coordinated commits keep them compact:

• dbc4177: try_nat_linear_rec reduces Nat.rec base (succ-step) (Lit n) with
  a symbolic base directly to Nat.add base (Lit n) instead of n iota steps.
• 5dcab7f: whnf (try_nat_offset_stuck) leaves Nat.add base (Lit n) stuck as
  a compact offset; def-eq (nat_offset_of + try_def_eq_nat) decomposes each
  side to base + KLimbs and decides base ≟ base on equal offsets.
• d50c9a6: generalizes the stuck rule to Nat.div/Nat.mod base (Lit k)
  (k ≥ 2), so symbolic >>> reduces to nested-stuck-div in O(1).

Benchmarks: x + D = Nat.rec x succ-step D goes O(D) → depth-independent
(328M → 28.5M at D=512, −91%); x >>> 18 = (x >>> 9) >>> 9 goes 15.65G → 455M
(−97%), matching x >>> 6. All magnitudes stay KLimbs (no Goldilocks
collapse); only de Bruijn / top-position indices are G.

Soundness

• Areas 1–4 are structural/refactor rewrites with identical results (each shard
  still checks).
• Area 2: address_eq returns the same value as a full 32-limb compare — one
  differing limb proves inequality.
• Area 5: key collisions overwrite, sound because the only effect is a missed
  skip (a frontier const gets rechecked, never wrongly trusted); the confirming
  address_eq rules out false positives; the 4-byte key makes collisions
  negligible regardless.
• Area 6: keeping Nat.add/div/mod symbolic literal stuck is the correct normal
  form (these are irreducible for a symbolic base). try_def_eq_nat returns
  eq = 1 only when offsets are equal and bases are def-eq (+ k is injective);
  otherwise it falls back to the generic path. The full ixvm suite passes (297
  tests), BAD negative cases still get rejected (no false accept), and
  recursor-on-symbolic-offset reduces correctly.