Intern addresses as &[G; 32] to cut kernel FFT cost (#417)

Replace the by-value `[G; 32]` address type with `type Addr = &[G; 32]`.
Aiur `store` content-dedups structurally equal arrays to one canonical
pointer, so address equality reduces to pointer subtraction and every
function carrying addresses drops 31 columns per address argument.

`lake exe kernel String.Internal.append`: total FFT 2515875651 ->
2153021841 (-14.4%), total width 48210 -> 37860. ixvm test suite:
283 pass, 0 fail.

Author: arthurpaulino

Ix/IxVM.lean

@@ -50,10 +50,11 @@ def entrypoints := ⟦
   -- in `k_consts`/`addrs` so the target's own `whnf`/`infer` can
   -- resolve `Const` refs; the IOBuffer payload doesn't shrink.
   pub fn kernel_check_test(target_addr: [G; 32], check_deps: G) {
-    let (k_consts, addrs) = ingress_with_primitives(target_addr);
+    let target = store(target_addr);
+    let (k_consts, addrs) = ingress_with_primitives(target);
     match check_deps {
       0 =>
-        let target_pos = find_addr_idx(target_addr, addrs, 0);
+        let target_pos = find_addr_idx(target, addrs, 0);
         let ci = load(list_lookup(k_consts, target_pos));
         check_const(ci, target_pos, k_consts, addrs),
       _ => check_all(k_consts, k_consts, addrs),

Ix/IxVM/Convert.lean

@@ -38,8 +38,8 @@ def convert := ⟦
     CKDefn(Definition, G),
     CKAxio(Axiom),
     CKQuot(Quotient),
-    CKRecr(Recursor, List‹G›, [G; 32]),
-    CKIndc(Inductive, List‹G›, [G; 32]),
+    CKRecr(Recursor, List‹G›, Addr),
+    CKIndc(Inductive, List‹G›, Addr),
     CKCtor(Constructor, G)
   }
 
@@ -281,7 +281,7 @@ def convert := ⟦
   }
 
   fn convert_recursor(r: Recursor, ctx: ConvertCtx, rule_ctor_idxs: List‹G›,
-                      block_addr: [G; 32]) -> KConstantInfo {
+                      block_addr: Addr) -> KConstantInfo {
     match r {
       Recursor.Mk(k, is_unsafe, lvls, params, indices, motives, minors, &typ, rules) =>
         let ktyp = ctx_convert_expr(typ, ctx);
@@ -294,7 +294,7 @@ def convert := ⟦
   }
 
   fn convert_inductive(ind: Inductive, ctx: ConvertCtx, ctor_idxs: List‹G›,
-                       block_addr: [G; 32]) -> KConstantInfo {
+                       block_addr: Addr) -> KConstantInfo {
     match ind {
       Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, &typ, _) =>
         let ktyp = ctx_convert_expr(typ, ctx);

Ix/IxVM/Core.lean

@@ -18,6 +18,11 @@ def core := ⟦
     None
   }
 
+  -- Interned 32-element address (blake3 content hash). Aiur `store`
+  -- content-dedups structurally-equal arrays to one canonical pointer,
+  -- so address equality reduces to pointer subtraction.
+  type Addr = &[G; 32]
+
   fn list_length‹T›(list: List‹T›) -> G {
     match load(list) {
       ListNode.Nil => 0,