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

* IxVM: cut ingress/conversion circuit width in the Aiur kernel

FFT-cost optimizations on the kernel's ingress + Ixon-to-kernel-type
conversion path (the dominant cost when verifying a whole environment of
many constants).

Measured with `ix check --ixe arena.ixe --claim <digest>` over the
TutorialDefs arena env (780 constants): total Aiur FFT cost
7,159,028,984 -> 6,196,095,030 (-13.5%). No behavior change: the
check-env claim typechecks identically and the rbtree-map test passes.

convert_expr: pass the expression by pointer
- convert_expr / ctx_convert_expr take `e: &Expr` and `load` inside,
  instead of receiving the Expr flattened by value on every call. An
  enum-valued argument is laid out at its widest constructor, so this cuts
  inputSize: width 112 -> 68 (~-39% on that circuit). Recursive arms
  forward child pointers directly and the Share arm forwards the interned
  pointer (dropping a load). Memoization identity is preserved, since a
  pointer and its interned value coincide.

RBTreeMap: one comparison per node instead of two
- lookup / lookup_or_default / ins replace the second `u32_less_than(k, key)`
  with a field equality `key - k == 0`. By field trichotomy this is
  equivalent, and it saves +12 aux / +6 lookups per node (u32_less_than is
  the expensive gadget). lookup_or_default 85 -> 62w, ins 98 -> 75w.

RBTreeMap: factor the cold rebalance path out of balance
- rbtree_map_balance becomes a narrow color dispatch; the four wide
  Okasaki rebalance cases (red-grandchild deref + 3-node rebuild) move to
  rbtree_map_balance_fix. Aiur lays a function's width as the max over its
  match arms, so the red-parent hot path no longer carries the rebalance
  machinery: balance 122 -> 32w.

lookup_addr_pos: O(log) fast path with a sound content fallback
- The ref-address -> kernel-position lookup was an O(N) linear address_eq
  scan (the largest single ingress hotspot). It now first probes an
  interned ptr_val-keyed map (build_addr_pos_map, value = pos+1 so the
  default 0 means absent) and only falls back to the content-based
  address_eq scan (lookup_addr_pos_linear) on a miss. This is sound: a
  ptr_val hit implies content equality (the positive direction), and a
  de-interned pointer or a non-constant blob ref simply misses and takes
  the content scan, which returns 0 if truly absent. Honest constant refs
  hit the tree, so the linear scan is reduced to blob/fallback rows.

Consolidate the two ptr_val membership/position maps into one
- Delete build_addr_set: addr_pos_map already keys every constant address,
  so is_blob becomes a presence test against it (present iff constant; the
  stored position is irrelevant there). This removes a whole map build from
  ingress. The de-intern direction stays conservative -- a de-interned
  constant reads as a blob, which is content-bound and harmless. Also
  removes now-dead helpers find_block_addr_from_refs,
  find_matching_block_addr, count_block_ctors, recr_rule_count and
  count_recr_rules (only self-recursive; the recursor block is resolved via
  rec_typ_to_inductive_addr).

Document the ptr_val-key soundness invariant on build_addr_pos_map: a
pointer maps to exactly one stored value, so distinct contents can never be
conflated; a de-intern only ever makes a present key read as absent. Hence
ptr_val keys are safe only where a false "absent" is conservative -- which
is why lookup_addr_pos keeps its content-based fallback.

* IxVM: 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. So the addressing machinery ran ~N times over
overlapping data.

Ingress the union closure of all env leaves ONCE (one `load_with_deps`
with leaves[0] as target and the rest as the initial worklist), then check
every constant via the same `check_all_skipping` path `run_check` already
uses. Factor the shared post-load pipeline into `finish_ingress` and add
`ingress_env`; `run_check_env` now mirrors `run_check` over a closure that
happens to be the whole env.

Soundness: unchanged checking. Every constant is still checked 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 what a per-leaf check would reject. The adversarial
arena BAD fixtures still reject.

Measured with `ix check --ixe arena.ixe --claim <CheckEnv-digest>` over the
TutorialDefs arena (694 consts): total Aiur FFT cost
6,196,095,030 -> 3,319,451,741 (-46.4%). `lake test -- --ignored ixvm`:
297 pass, 0 fail.

Author: arthurpaulino

Ix/IxVM/Convert.lean

@@ -136,14 +136,14 @@ def convert := ⟦
   }
 
   fn convert_expr(
-    e: Expr,
+    e: &Expr,
     sharing: List‹&Expr›,
     ref_idxs: List‹G›,
     recur_idxs: List‹G›,
     lit_blobs: List‹ByteStream›,
     univs: List‹&Univ›
   ) -> KExpr {
-    match e {
+    match load(e) {
       Expr.Srt(univ_idx) =>
         let u = load(list_lookup_u64(univs, univ_idx));
         store(KExprNode.Srt(store(convert_univ(u)))),
@@ -161,7 +161,7 @@ def convert := ⟦
         let levels = convert_univ_idxs(univ_idxs, univs);
         store(KExprNode.Const(const_idx, levels)),
 
-      Expr.Prj(type_ref_idx, field_idx, &inner) =>
+      Expr.Prj(type_ref_idx, field_idx, inner) =>
         let type_idx = list_lookup(ref_idxs, flatten_u64(type_ref_idx));
         store(KExprNode.Proj(
           type_idx,
@@ -177,34 +177,33 @@ def convert := ⟦
         let limbs = bytes_to_limbs(bs);
         store(KExprNode.Lit(KLiteral.Nat(limbs))),
 
-      Expr.App(&f, &a) =>
+      Expr.App(f, a) =>
         store(KExprNode.App(
           convert_expr(f, sharing, ref_idxs, recur_idxs, lit_blobs, univs),
           convert_expr(a, sharing, ref_idxs, recur_idxs, lit_blobs, univs))),
 
-      Expr.Lam(&ty, &body) =>
+      Expr.Lam(ty, body) =>
         store(KExprNode.Lam(
           convert_expr(ty, sharing, ref_idxs, recur_idxs, lit_blobs, univs),
           convert_expr(body, sharing, ref_idxs, recur_idxs, lit_blobs, univs))),
 
-      Expr.All(&ty, &body) =>
+      Expr.All(ty, body) =>
         store(KExprNode.Forall(
           convert_expr(ty, sharing, ref_idxs, recur_idxs, lit_blobs, univs),
           convert_expr(body, sharing, ref_idxs, recur_idxs, lit_blobs, univs))),
 
-      Expr.Let(_, &ty, &val, &body) =>
+      Expr.Let(_, ty, val, body) =>
         store(KExprNode.Let(
           convert_expr(ty, sharing, ref_idxs, recur_idxs, lit_blobs, univs),
           convert_expr(val, sharing, ref_idxs, recur_idxs, lit_blobs, univs),
           convert_expr(body, sharing, ref_idxs, recur_idxs, lit_blobs, univs))),
 
       Expr.Share(idx) =>
-        let shared = load(list_lookup_u64(sharing, idx));
-        convert_expr(shared, sharing, ref_idxs, recur_idxs, lit_blobs, univs),
+        convert_expr(list_lookup_u64(sharing, idx), sharing, ref_idxs, recur_idxs, lit_blobs, univs),
     }
   }
 
-  fn ctx_convert_expr(e: Expr, ctx: ConvertCtx) -> KExpr {
+  fn ctx_convert_expr(e: &Expr, ctx: ConvertCtx) -> KExpr {
     match ctx {
       ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
         convert_expr(e, sharing, ref_idxs, recur_idxs, lit_blobs, univs),
@@ -226,7 +225,7 @@ def convert := ⟦
       ListNode.Nil => store(ListNode.Nil),
       ListNode.Cons(rule, rest_rules) =>
         match rule {
-          RecursorRule.Mk(nfields, &rhs) =>
+          RecursorRule.Mk(nfields, rhs) =>
             match load(rule_ctor_idxs) {
               ListNode.Cons(ctor_idx, rest_ctor_idxs) =>
                 let krhs = ctx_convert_expr(rhs, ctx);
@@ -245,7 +244,7 @@ def convert := ⟦
 
   fn convert_definition(d: Definition, ctx: ConvertCtx, hint: G) -> KConstantInfo {
     match d {
-      Definition.Mk(kind, safety, lvls, &typ, &value) =>
+      Definition.Mk(kind, safety, lvls, typ, value) =>
         let ktyp = ctx_convert_expr(typ, ctx);
         let kval = ctx_convert_expr(value, ctx);
         match kind {
@@ -266,15 +265,15 @@ def convert := ⟦
 
   fn convert_axiom(a: Axiom, ctx: ConvertCtx) -> KConstantInfo {
     match a {
-      Axiom.Mk(is_unsafe, lvls, &typ) =>
+      Axiom.Mk(is_unsafe, lvls, typ) =>
         let ktyp = ctx_convert_expr(typ, ctx);
         KConstantInfo.Axiom(flatten_u64(lvls), ktyp, is_unsafe),
     }
   }
 
   fn convert_quotient(q: Quotient, ctx: ConvertCtx) -> KConstantInfo {
     match q {
-      Quotient.Mk(kind, lvls, &typ) =>
+      Quotient.Mk(kind, lvls, typ) =>
         let ktyp = ctx_convert_expr(typ, ctx);
         KConstantInfo.Quot(flatten_u64(lvls), ktyp, kind),
     }
@@ -283,7 +282,7 @@ def convert := ⟦
   fn convert_recursor(r: Recursor, ctx: ConvertCtx, rule_ctor_idxs: List‹G›,
                       block_addr: Addr) -> KConstantInfo {
     match r {
-      Recursor.Mk(k, is_unsafe, lvls, params, indices, motives, minors, &typ, rules) =>
+      Recursor.Mk(k, is_unsafe, lvls, params, indices, motives, minors, typ, rules) =>
         let ktyp = ctx_convert_expr(typ, ctx);
         let krules = convert_rules(rules, rule_ctor_idxs, ctx);
         KConstantInfo.Rec(
@@ -296,7 +295,7 @@ def convert := ⟦
   fn convert_inductive(ind: Inductive, ctx: ConvertCtx, ctor_idxs: List‹G›,
                        block_addr: Addr) -> KConstantInfo {
     match ind {
-      Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, &typ, _) =>
+      Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
         let ktyp = ctx_convert_expr(typ, ctx);
         KConstantInfo.Induct(
           flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
@@ -306,7 +305,7 @@ def convert := ⟦
 
   fn convert_constructor(c: Constructor, ctx: ConvertCtx, induct_idx: G) -> KConstantInfo {
     match c {
-      Constructor.Mk(is_unsafe, lvls, cidx, params, fields, &typ) =>
+      Constructor.Mk(is_unsafe, lvls, cidx, params, fields, typ) =>
         let ktyp = ctx_convert_expr(typ, ctx);
         KConstantInfo.Ctor(
           flatten_u64(lvls), ktyp, induct_idx, flatten_u64(cidx),