IxVM: cut Aiur-kernel ingress cost (per-pass width + CheckEnv ingest-once)

[arthurpaulino]

Two complementary optimizations to the IxVM Aiur kernel's data-ingress path —
the layer that turns prover-supplied bytes into kernel types before typechecking.
Pure performance: no change to what is accepted/rejected.

All numbers measured with ix check --ixe arena.ixe --claim <CheckEnv-digest>
over the TutorialDefs arena env (694 constants), constrained blake3:

stage	total Aiur FFT cost	Δ
baseline (main)	7,159,028,984	—
after commit 1 (width)	6,196,095,030	−13.5%
after commit 2 (ingest-once)	3,319,451,741	−53.6% overall

lake test -- --ignored ixvm: 297 pass, 0 fail (incl. adversarial arena BAD
fixtures still rejected). lake test -- --ignored rbtree-map: pass.

---

Commit 1 — shrink the per-pass ingress/conversion circuit width

Aiur circuit cost is width × height × log2(height), width = inputSize + selectors + auxiliaries + 4·(1+lookups). This commit cuts width on the hottest
ingress/conversion functions:

• convert_expr/ctx_convert_expr take e: &Expr (pointer, load inside)
  instead of the Expr flattened by value — an enum arg is laid out at its widest
  constructor, so this cuts inputSize: width 112 → 68 (−39%). Recursive arms
  forward child pointers; the Share arm forwards the interned pointer (drops a
  load). Memoization identity preserved (pointer ↔ interned value).
• RBTreeMap lookup/lookup_or_default/ins: replace the second
  u32_less_than(k, key) with a field equality key - k == 0 (field trichotomy
  ⇒ equivalent), saving +12 aux / +6 lookups per node. lookup_or_default 85→62w,
  ins 98→75w.
• rbtree_map_balance: factor the 4 wide Okasaki rebalance cases into a cold
  rbtree_map_balance_fix; the red-parent hot path no longer carries the rebalance
  machinery (Aiur lays width as the max over arms). balance 122 → 32w.
• lookup_addr_pos: ref-address→kernel-position was an O(N) linear
  address_eq scan; now a ptr_val-keyed map fast path with a content-based
  fallback (lookup_addr_pos_linear) on miss — sound because a ptr_val hit
  implies content equality, and a de-interned/blob miss falls back to the content
  scan.
• Consolidate two ptr_val maps into one: delete build_addr_set —
  addr_pos_map already keys every constant address, so is_blob is a presence
  test against it. Also removes dead helpers (find_block_addr_from_refs,
  find_matching_block_addr, count_block_ctors, recr_rule_count,
  count_recr_rules). Documents the ptr_val-key soundness invariant.

Commit 2 — CheckEnv ingests the env once instead of per leaf

check_env_iter re-ran the full ingress_with_primitives(leaf) pipeline for
every env leaf, re-deriving the layout/positioning/convert/addr-table passes
over each leaf's heavily-overlapping closure. Those passes are keyed by per-leaf
list arguments, so Aiur's content-memoization did not collapse them across leaves
(only the content-keyed load_verified_* / convert_* were deduped). The
addressing machinery effectively ran ~N times over overlapping data.

This factors the shared post-load pipeline into finish_ingress and adds
ingress_env, which loads the union closure of all env leaves in one
load_with_deps (leaves[0] as target, the rest as the initial worklist).
run_check_env now mirrors run_check: ingest once, then check_all_skipping.

Soundness: the checking is unchanged — every constant is still checked exactly
once (check_const runs 711× = env consts + primitives), and the single
check_canonical_block_sort(top) over the union is a stronger global order than
the per-leaf closures it replaces. Refs resolve by content, so the union check
cannot accept anything a per-leaf check would reject. Structurally identical to a
run_check over a closure that happens to be the whole env, so soundness rides on
that existing, tested pattern.

---

How the two interact

Complementary, no overlap in code (commit 2 reuses the functions commit 1
optimized via finish_ingress). Different axes: commit 1 lowers the cost of one
ingress pass; commit 2 lowers the number of passes (N→1) for CheckEnv. Their
effects overlap on the CheckEnv path (both attack ingress cost), so the deltas are
not strictly additive — ingest-once subsumes most of commit 1's CheckEnv value.
Commit 1 remains the relevant ingress win for the single-claim path
(ix check <name> → run_check), where there is no per-leaf multiplication for
ingest-once to remove.

Scope / notes

• Pure performance + dead-code removal; no change to acceptance/rejection.
• After these changes the ingress/convert/layout layer is ~1.7% of CheckEnv cost;
  the remaining cost is dominated by the irreducible floor (blake3 content
  verification ~46%) and genuine kernel typecheck work (expr_inst1, k_infer,
  whnf telescopes). Further ingress optimization has diminishing returns.
• Follow-up worth adding: a dedicated CheckEnv soundness test embedding a
  known-bad constant in the env and asserting rejection (current coverage checks
  good/bad via verify_const and the arena claim end-to-end).