IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface

Ix/IxVM/Blake3.lean

@@ -45,6 +45,35 @@ def blake3 := ⟦
     blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
   }
 
+  -- Flatten blake3's [[U8;4];8] output into the [U8;32] form every caller wants.
+  fn blake3_flat(input: ByteStream) -> [U8; 32] {
+    let h = blake3(input);
+    [h[0][0], h[0][1], h[0][2], h[0][3],
+     h[1][0], h[1][1], h[1][2], h[1][3],
+     h[2][0], h[2][1], h[2][2], h[2][3],
+     h[3][0], h[3][1], h[3][2], h[3][3],
+     h[4][0], h[4][1], h[4][2], h[4][3],
+     h[5][0], h[5][1], h[5][2], h[5][3],
+     h[6][0], h[6][1], h[6][2], h[6][3],
+     h[7][0], h[7][1], h[7][2], h[7][3]]
+  }
+
+  -- Hash `bytes` and assert the digest equals `expected`. Used by every
+  -- IOBuffer-load path that verifies the pre-image of a content-addressed
+  -- pointer matches the bytes the prover supplied.
+  fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
+    assert_eq!(blake3_flat(bytes), expected);
+    ()
+  }
+
+  -- Hash `bytes` and intern the digest into the Store. Returned pointer is
+  -- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
+  -- site that synthesises an address from raw bytes (e.g. `expr_addr`,
+  -- `leaf_hash`, `node_hash`, `cprj_content_addr`).
+  fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
+    store(blake3_flat(bytes))
+  }
+
   fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
     match layer {
       Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),

Ix/IxVM/ClaimHarness.lean

@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
   | .abbrev => .ofNat 0xFFFFFFFF
   | .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)
 
+/-! ## IxVM IOBuffer interface
+
+The host seeds blake3-keyed payloads on six channels; the Aiur kernel
+consumes them via `io_get_info` + `#read_byte_stream`. One value shape
+per channel — no overloading, no in-band discriminators.
+
+Tiered by access pattern (matches kernel runtime order):
+
+| Tier   | Channel | Purpose                  | Key (32 G)              | Value shape       |
+|--------|---------|--------------------------|-------------------------|-------------------|
+| Ctrl   | 0       | claim wire bytes         | `blake3(claim_bytes)`   | claim bytes       |
+| Ctrl   | 1       | assumption tree bytes    | `tree.root`             | tree bytes        |
+| Const  | 2       | constant wire bytes      | const addr              | const bytes       |
+| Const  | 3       | Defn reducibility hint   | Defn addr               | single G          |
+| Blob   | 4       | blob discriminator       | addr                    | one byte (1=const, 0=blob) |
+| Blob   | 5       | blob raw bytes           | blob addr               | raw bytes         |
+
+Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
+Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
+fires per blob ref encountered during `build_ref_idxs_and_blobs`.
+
+Soundness:
+* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
+  against its content-addressed key.
+* ch 3 — semantically optional; controls WHNF reduction heuristic
+  only, def-eq is sound either way.
+* ch 4 — sound by erasure-correctness: a lying discriminator flips
+  the const/blob decision and the wrong-path load downstream fails
+  (a "const" blob triggers a ch 2 read returning empty → blake3
+  verify against the non-empty addr fails; a "blob" const dangles
+  references → typecheck fail).
+
+Channel numbers MUST stay in sync with the inlined `io_get_info` /
+`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
+`Ix/IxVM/Kernel/Claim.lean`.
+-/
+
 /-- Insert all per-address entries for `addr`s satisfying `keep` into
-    `ioBuffer`. Each address kind lives on its own channel; the key is
-    always the 32-G blake3 hash, with no disambiguating suffix.
-
-    | channel | key (32 G) | value          | meaning |
-    |---------|------------|----------------|---------|
-    | 0       | `addr`     | const bytes    | constant data (empty marker = `addr` is a blob) |
-    | 1       | `addr`     | raw blob bytes | referenced data (verified by Aiur via blake3) |
-    | 2       | `addr`     | single G       | Defn `ReducibilityHints` encoding |
-
-    Blob addrs also get an empty entry on channel 0 so the kernel's
-    constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
-    works without a separate query path. -/
+    `ioBuffer`. See the channel table above. -/
 def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
     (ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
   let mut ioBuffer := ioBuffer
@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
     -- serialized form the lazy entry holds — no materialization needed.
     let bytes := lc.rawBytes
     let key : Array Aiur.G := addr.hash.data.map .ofUInt8
-    ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
+    ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
+    -- Discriminator: this addr resolves to a constant.
+    ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
   for (addr, rawBytes) in ixonEnv.blobs do
     if !keep addr then continue
     let key : Array Aiur.G := addr.hash.data.map .ofUInt8
-    ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
-    ioBuffer := ioBuffer.extend 0 key #[]
+    ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
+    -- Discriminator: this addr resolves to a blob.
+    ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
   for (_, named) in ixonEnv.named do
     if !keep named.addr then continue
     match named.constMeta with
     | .defn _ _ hints _ _ _ _ _ =>
       let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
-      ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
+      ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
     | _ => pure ()
   return ioBuffer
 
@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
   match trees.get? root with
   | some tree =>
     let bytes := Ix.AssumptionTree.ser tree
-    .ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
+    .ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
   | none => .error s!"no assumption tree supplied for root {root}"
 
 /-- Build the witness for `verify_claim` against `claim`.

Ix/IxVM/Convert.lean

@@ -53,12 +53,16 @@ def convert := ⟦
   -- Universe conversion: Ixon Univ -> KLevel
   -- ============================================================================
 
-  fn convert_univ(u: Univ) -> KLevel {
-    match u {
+  -- Take `&Univ` (pointer) to shrink the per-row input width — Univ is a
+  -- 5-variant enum, by-value passing taxes every row with the widest
+  -- arm's columns. Mirror the `reference_aiur_pass_pointer_not_value`
+  -- pattern already used for `convert_expr(e: &Expr)`.
+  fn convert_univ(u: &Univ) -> KLevel {
+    match load(u) {
       Univ.Zero => KLevel.Zero,
-      Univ.Succ(&inner) => KLevel.Succ(store(convert_univ(inner))),
-      Univ.Max(&a, &b) => KLevel.Max(store(convert_univ(a)), store(convert_univ(b))),
-      Univ.IMax(&a, &b) => KLevel.IMax(store(convert_univ(a)), store(convert_univ(b))),
+      Univ.Succ(inner) => KLevel.Succ(store(convert_univ(inner))),
+      Univ.Max(a, b) => KLevel.Max(store(convert_univ(a)), store(convert_univ(b))),
+      Univ.IMax(a, b) => KLevel.IMax(store(convert_univ(a)), store(convert_univ(b))),
       Univ.Var(idx) => KLevel.Param(flatten_u64(idx)),
     }
   }
@@ -70,8 +74,8 @@ def convert := ⟦
       ListNode.Cons(idx, rest) =>
         -- universe indices are small; walk with a field index (cheap per-step
         -- field sub) instead of `list_lookup_u64`'s per-step U64 predecessor.
-        let u = load(list_lookup(univs, flatten_u64(idx)));
-        store(ListNode.Cons(store(convert_univ(u)), convert_univ_idxs(rest, univs))),
+        let u_ref = list_lookup(univs, flatten_u64(idx));
+        store(ListNode.Cons(store(convert_univ(u_ref)), convert_univ_idxs(rest, univs))),
     }
   }
 
@@ -149,8 +153,8 @@ def convert := ⟦
       Expr.Srt(univ_idx) =>
         -- field-indexed walk (see `convert_univ_idxs`): avoids the per-step
         -- U64 predecessor of `list_lookup_u64` on this hot universe lookup.
-        let u = load(list_lookup(univs, flatten_u64(univ_idx)));
-        store(KExprNode.Srt(store(convert_univ(u)))),
+        let u_ref = list_lookup(univs, flatten_u64(univ_idx));
+        store(KExprNode.Srt(store(convert_univ(u_ref)))),
 
       Expr.Var(idx) =>
         store(KExprNode.BVar(flatten_u64(idx))),
@@ -208,13 +212,6 @@ def convert := ⟦
     }
   }
 
-  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),
-    }
-  }
-
   -- ============================================================================
   -- Recursor rule conversion
   -- ============================================================================
@@ -233,11 +230,14 @@ def convert := ⟦
           RecursorRule.Mk(nfields, rhs) =>
             match load(rule_ctor_idxs) {
               ListNode.Cons(ctor_idx, rest_ctor_idxs) =>
-                let krhs = ctx_convert_expr(rhs, ctx);
-                let krule = KRecRule.Mk(ctor_idx, flatten_u64(nfields), krhs);
-                store(ListNode.Cons(
-                  krule,
-                  convert_rules(rest_rules, rest_ctor_idxs, ctx))),
+                match ctx {
+                  ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
+                    let krhs = convert_expr(rhs, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+                    let krule = KRecRule.Mk(ctor_idx, flatten_u64(nfields), krhs);
+                    store(ListNode.Cons(
+                      krule,
+                      convert_rules(rest_rules, rest_ctor_idxs, ctx))),
+                },
             },
         },
     }
@@ -248,83 +248,103 @@ def convert := ⟦
   -- ============================================================================
 
   fn convert_definition(d: Definition, ctx: ConvertCtx, hint: G) -> KConstantInfo {
-    match d {
-      Definition.Mk(kind, safety, lvls, typ, value) =>
-        let ktyp = ctx_convert_expr(typ, ctx);
-        let kval = ctx_convert_expr(value, ctx);
-        match kind {
-          DefKind.Definition =>
-            KConstantInfo.Defn(flatten_u64(lvls), ktyp, kval, safety, hint),
-          DefKind.Opaque =>
-            match safety {
-              DefinitionSafety.Unsafe =>
-                KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 1),
-              _ =>
-                KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 0),
+    match ctx {
+      ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
+        match d {
+          Definition.Mk(kind, safety, lvls, typ, value) =>
+            let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+            let kval = convert_expr(value, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+            match kind {
+              DefKind.Definition =>
+                KConstantInfo.Defn(flatten_u64(lvls), ktyp, kval, safety, hint),
+              DefKind.Opaque =>
+                match safety {
+                  DefinitionSafety.Unsafe =>
+                    KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 1),
+                  _ =>
+                    KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 0),
+                },
+              DefKind.Theorem =>
+                KConstantInfo.Thm(flatten_u64(lvls), ktyp, kval),
             },
-          DefKind.Theorem =>
-            KConstantInfo.Thm(flatten_u64(lvls), ktyp, kval),
         },
     }
   }
 
   fn convert_axiom(a: Axiom, ctx: ConvertCtx) -> KConstantInfo {
-    match a {
-      Axiom.Mk(is_unsafe, lvls, typ) =>
-        let ktyp = ctx_convert_expr(typ, ctx);
-        KConstantInfo.Axiom(flatten_u64(lvls), ktyp, is_unsafe),
+    match ctx {
+      ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
+        match a {
+          Axiom.Mk(is_unsafe, lvls, typ) =>
+            let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+            KConstantInfo.Axiom(flatten_u64(lvls), ktyp, is_unsafe),
+        },
     }
   }
 
   fn convert_quotient(q: Quotient, ctx: ConvertCtx) -> KConstantInfo {
-    match q {
-      Quotient.Mk(kind, lvls, typ) =>
-        let ktyp = ctx_convert_expr(typ, ctx);
-        KConstantInfo.Quot(flatten_u64(lvls), ktyp, kind),
+    match ctx {
+      ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
+        match q {
+          Quotient.Mk(kind, lvls, typ) =>
+            let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+            KConstantInfo.Quot(flatten_u64(lvls), ktyp, kind),
+        },
     }
   }
 
   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) =>
-        let ktyp = ctx_convert_expr(typ, ctx);
-        let krules = convert_rules(rules, rule_ctor_idxs, ctx);
-        KConstantInfo.Rec(
-          flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
-          flatten_u64(motives), flatten_u64(minors),
-          krules, k, is_unsafe, block_addr),
+    match ctx {
+      ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
+        match r {
+          Recursor.Mk(k, is_unsafe, lvls, params, indices, motives, minors, typ, rules) =>
+            let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+            let krules = convert_rules(rules, rule_ctor_idxs, ctx);
+            KConstantInfo.Rec(
+              flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
+              flatten_u64(motives), flatten_u64(minors),
+              krules, k, is_unsafe, block_addr),
+        },
     }
   }
 
   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, _) =>
-        let ktyp = ctx_convert_expr(typ, ctx);
-        KConstantInfo.Induct(
-          flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
-          ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
+    match ctx {
+      ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
+        match ind {
+          Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
+            let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+            KConstantInfo.Induct(
+              flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
+              ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
+        },
     }
   }
 
   fn convert_constructor(c: Constructor, ctx: ConvertCtx, induct_idx: G) -> KConstantInfo {
-    match c {
-      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),
-          flatten_u64(params), flatten_u64(fields), is_unsafe),
+    match ctx {
+      ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
+        match c {
+          Constructor.Mk(is_unsafe, lvls, cidx, params, fields, typ) =>
+            let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
+            KConstantInfo.Ctor(
+              flatten_u64(lvls), ktyp, induct_idx, flatten_u64(cidx),
+              flatten_u64(params), flatten_u64(fields), is_unsafe),
+        },
     }
   }
 
   -- ============================================================================
   -- Top-level conversion
   -- ============================================================================
 
-  -- Convert a single resolved input to a KConstantInfo
-  fn convert_one(input: ConvertInput) -> KConstantInfo {
-    match input {
+  -- Convert a single resolved input to a KConstantInfo. Takes &ConvertInput
+  -- (pointer) so the per-row input width is one G column, not the full
+  -- ConvertInput union width.
+  fn convert_one(input: &ConvertInput) -> KConstantInfo {
+    match load(input) {
       ConvertInput.Mk(ctx, kind) =>
         match kind {
           ConvertKind.CKDefn(d, hint) => convert_definition(d, ctx, hint),
@@ -342,7 +362,7 @@ def convert := ⟦
   fn convert_all(inputs: List‹&ConvertInput›) -> List‹&KConstantInfo› {
     match load(inputs) {
       ListNode.Nil => store(ListNode.Nil),
-      ListNode.Cons(&input, rest) =>
+      ListNode.Cons(input, rest) =>
         let ci = convert_one(input);
         store(ListNode.Cons(store(ci), convert_all(rest))),
     }