Aiur kernel: complete port from Rust reference + kernel-arena coverage

Benchmarks/CheckNatAddComm.lean

@@ -29,36 +29,15 @@ def main : IO Unit := do
   let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
 
   let env ← get_env!
-  let constList := Lean.collectDependencies ``Nat.add_comm env.constants
-  let rawEnv ← Ix.CompileM.rsCompileEnvFFI constList
-  let ixonEnv := rawEnv.toEnv
-
-  let mut ioBuffer : Aiur.IOBuffer := default
-
-  -- Store ALL constants (including muts blocks) by Blake3 hash
-  for (addr, c) in ixonEnv.consts do
-    let (_, bytes) := Ixon.Serialize.put c |>.run default
-    let key : Array Aiur.G := addr.hash.data.map .ofUInt8
-    ioBuffer := ioBuffer.extend key (bytes.data.map .ofUInt8)
-
-  -- Store each blob:
-  -- 1. Raw bytes under prefixed key [1] ++ blake3_hash (for on-demand verified loading)
-  -- 2. Empty sentinel under plain blake3_hash (so io_get_info returns len=0, marking as blob)
-  for (addr, rawBytes) in ixonEnv.blobs do
-    let hashKey : Array Aiur.G := addr.hash.data.map .ofUInt8
-    let prefixedKey : Array Aiur.G := #[1] ++ hashKey
-    ioBuffer := ioBuffer.extend prefixedKey (rawBytes.data.map fun b => .ofNat b.toNat)
-    ioBuffer := ioBuffer.extend hashKey #[]
-
-  -- Get the blake3 address of Nat.add_comm as the target
-  let targetAddr := match ixonEnv.getAddr? (Ix.Name.fromLeanName ``Nat.add_comm) with
-    | some addr => addr
-    | none => panic! "Nat.add_comm not found in Ixon environment"
-  let targetAddrBytes : Array Aiur.G := targetAddr.hash.data.map .ofUInt8
+  let ixonEnv ← IxVM.CheckHarness.loadIxonEnv ``Nat.add_comm env
+  let ioBuffer := IxVM.CheckHarness.buildKernelCheckIOBuffer ixonEnv
+  let targetAddrBytes := IxVM.CheckHarness.kernelCheckTarget ``Nat.add_comm ixonEnv
+  -- check_deps=1 here: bench full transitive checking.
+  let input := targetAddrBytes.push 1
 
   let _ ← bgroup "Kernel typechecking" { oneShot := true } do
     throughput (.Elements ixonEnv.consts.size.toUInt64 "consts")
     bench "check Nat.add_comm"
-      (aiurSystem.prove friParameters funIdx targetAddrBytes)
+      (aiurSystem.prove friParameters funIdx input)
       ioBuffer
   return

Benchmarks/IxVM.lean

@@ -29,14 +29,8 @@ def main : IO Unit := do
   let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
 
   let env ← get_env!
-  let natAddCommName := ``Nat.add_comm
-  let constList := Lean.collectDependencies natAddCommName env.constants
-  let rawEnv ← Ix.CompileM.rsCompileEnvFFI constList
-  let ixonEnv := rawEnv.toEnv
-  let ixonConsts := ixonEnv.consts.valuesIter
-  let (ioBuffer, n) := ixonConsts.fold (init := (default, 0)) fun (ioBuffer, i) c =>
-    let (_, bytes) := Ixon.Serialize.put c |>.run default
-    (ioBuffer.extend #[.ofNat i] (bytes.data.map .ofUInt8), i + 1)
+  let ixonEnv ← IxVM.CheckHarness.loadIxonEnv ``Nat.add_comm env
+  let (ioBuffer, n) := IxVM.CheckHarness.buildSerdeIOBuffer ixonEnv
 
   let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
     throughput (.Elements n.toUInt64 "consts")

Ix/Aiur/Interpret.lean

@@ -49,6 +49,31 @@ partial def ppValue : Value → String
 
 instance : ToString Value := ⟨ppValue⟩
 
+/-- Pretty-print a `Value` while auto-dereferencing pointers up to `depth`
+levels. Used by the `dbg!` interpreter helper so users see structured
+content like `App(Const(3, []), BVar(0))` instead of opaque `&0x123`. -/
+partial def ppValueDeref (store : Store) (depth : Nat) : Value → String
+  | .unit      => "()"
+  | .field g   => toString g.val.toNat
+  | .tuple vs  => "(" ++ String.intercalate ", " (vs.toList.map (ppValueDeref store depth)) ++ ")"
+  | .array vs  => "[" ++ String.intercalate ", " (vs.toList.map (ppValueDeref store depth)) ++ "]"
+  | .ctor g args =>
+      let name := g.toName.toString
+      if args.isEmpty then name
+      else name ++ "(" ++ String.intercalate ", " (args.toList.map (ppValueDeref store depth)) ++ ")"
+  | .fn g        => "fn(" ++ g.toName.toString ++ ")"
+  | .pointer _ n =>
+      if depth == 0 then "&0x" ++ natToHex n
+      else
+        match store.getByIdx n with
+        | some (vs, _) =>
+            -- Stored value is `Array Value`; for tagged enums it's
+            -- typically `[ctor]` or `[tag, fields...]`. Recurse on each.
+            match vs.toList with
+            | [v] => ppValueDeref store (depth - 1) v
+            | _   => "[" ++ String.intercalate ", " (vs.toList.map (ppValueDeref store (depth - 1))) ++ "]"
+        | none => "&0x" ++ natToHex n ++ "(unbound)"
+
 -- ---------------------------------------------------------------------------
 -- Pattern matching
 -- ---------------------------------------------------------------------------
@@ -330,7 +355,8 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
       | none   => dbg_trace s!"{label}"
       | some t =>
         let v ← interp decls bindings t
-        dbg_trace s!"{label}: {v}"
+        let store ← getStore
+        dbg_trace s!"{label}: {ppValueDeref store 16 v}"
       interp decls bindings cont
   | .ioGetInfo key => do
       let keyGs ← expectFieldArray (← interp decls bindings key)

Ix/Aiur/Semantics/BytecodeFfi.lean

@@ -56,20 +56,23 @@ namespace Bytecode.Toplevel
 private opaque execute' : @& Bytecode.Toplevel →
   @& Bytecode.FunIdx → @& Array G → (ioData : @& Array G) →
   (ioMap : @& Array (Array G × IOKeyInfo)) →
-    Array G × (Array G × Array (Array G × IOKeyInfo)) × Array Nat
+    Except String (Array G × (Array G × Array (Array G × IOKeyInfo)) × Array Nat)
 
 /-- Executes the bytecode function `funIdx` with the given `args` and `ioBuffer`,
 returning the raw output of the function, the updated `IOBuffer`, and an array
-of query counts (one per function circuit, then one per memory size). -/
+of query counts (one per function circuit, then one per memory size). Returns
+`Except.error msg` when execution fails (e.g. `assert_eq!` mismatch from a
+typechecker rejecting a constant), so callers can recover instead of crashing. -/
 def execute (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
-    Array G × IOBuffer × Array Nat :=
+    Except String (Array G × IOBuffer × Array Nat) :=
   let ioData := ioBuffer.data
   let ioMap := ioBuffer.map
-  let (output, (ioData, ioMap), queryCounts) := execute' toplevel funIdx args
-    ioData ioMap.toArray
-  let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
-  (output, ⟨ioData, ioMap⟩, queryCounts)
+  match execute' toplevel funIdx args ioData ioMap.toArray with
+  | .error e => .error e
+  | .ok (output, (ioData, ioMap), queryCounts) =>
+    let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
+    .ok (output, ⟨ioData, ioMap⟩, queryCounts)
 
 end Bytecode.Toplevel
 

Ix/IxVM.lean

@@ -9,7 +9,16 @@ public import Ix.IxVM.IxonSerialize
 public import Ix.IxVM.IxonDeserialize
 public import Ix.IxVM.Convert
 public import Ix.IxVM.KernelTypes
-public import Ix.IxVM.Kernel
+public import Ix.IxVM.Kernel.Levels
+public import Ix.IxVM.Kernel.Primitive
+public import Ix.IxVM.Kernel.Subst
+public import Ix.IxVM.Kernel.Whnf
+public import Ix.IxVM.Kernel.Infer
+public import Ix.IxVM.Kernel.DefEq
+public import Ix.IxVM.Kernel.Inductive
+public import Ix.IxVM.Kernel.CanonicalCheck
+public import Ix.IxVM.Kernel.Check
+public import Ix.IxVM.CheckHarness
 
 public section
 
@@ -33,9 +42,22 @@ def entrypoints := ⟦
     }
   }
 
-  pub fn kernel_check_test(target_addr: [G; 32]) {
-    let (k_consts, nat_idx, str_idx) = ingress_with_primitives(target_addr);
-    k_check_all_go(k_consts, k_consts, nat_idx, str_idx, 0)
+  -- `check_deps` controls whether transitive dependencies are
+  -- typechecked along with the target. When 1, runs `check_all`
+  -- (current behavior). When 0, runs `check_const` only on the target
+  -- — saving the per-dep `validate_const_well_scoped`, `k_check`,
+  -- recursor canonical-build, positivity, etc. Deps still need to be
+  -- 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);
+    match check_deps {
+      0 =>
+        let target_pos = find_addr_idx(target_addr, 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),
+    }
   }
 
   fn level_cmp_tests() {
@@ -155,7 +177,15 @@ def ixVM : Except Aiur.Global Aiur.Source.Toplevel := do
   let vm ← vm.merge convert
   let vm ← vm.merge ingress
   let vm ← vm.merge kernelTypes
-  let vm ← vm.merge kernel
+  let vm ← vm.merge levels
+  let vm ← vm.merge primitive
+  let vm ← vm.merge subst
+  let vm ← vm.merge whnf
+  let vm ← vm.merge infer
+  let vm ← vm.merge defEq
+  let vm ← vm.merge inductive_check
+  let vm ← vm.merge canonicalCheck
+  let vm ← vm.merge check
   vm.merge entrypoints
 
 end IxVM

Ix/IxVM/CheckHarness.lean

@@ -0,0 +1,134 @@
+module
+public import Ix.Aiur.Protocol
+public import Ix.Ixon
+public import Ix.CompileM
+public import Ix.Common
+
+public section
+
+namespace IxVM.CheckHarness
+
+/-- Run the Lean → Ixon FFI pipeline for `name`'s transitive closure. -/
+def loadIxonEnv (name : Lean.Name) (leanEnv : Lean.Environment) : IO Ixon.Env := do
+  let constList := Lean.collectDependencies name leanEnv.constants
+  let rawEnv ← Ix.CompileM.rsCompileEnvFFI constList
+  pure rawEnv.toEnv
+
+/-- Compile the union of `names`'s transitive closures into one shared
+    Ixon env. Drivers like `KernelArena.lean` use this to pay the
+    Lean→Ixon compile cost once and then build per-target IOBuffers via
+    `buildKernelCheckIOBufferFor`. -/
+def loadSharedIxonEnv (names : Array Lean.Name) (leanEnv : Lean.Environment) :
+    IO Ixon.Env := do
+  let constList := names.foldl (init := []) fun acc n =>
+    Lean.collectDependencies n leanEnv.constants ++ acc
+  let mut seen : Lean.NameSet := {}
+  let mut deduped : List (Lean.Name × Lean.ConstantInfo) := []
+  for entry in constList do
+    if !seen.contains entry.fst then
+      seen := seen.insert entry.fst
+      deduped := entry :: deduped
+  let rawEnv ← Ix.CompileM.rsCompileEnvFFI deduped
+  pure rawEnv.toEnv
+
+/-- Walk the Constant ref-graph from `target` to compute the set of
+    addresses needed to type-check it. Mirrors Aiur's `load_with_deps`:
+    follow `Constant.refs` plus the projection's `block_addr` (the parent
+    Muts wrapper) for IPrj/CPrj/RPrj/DPrj. -/
+partial def closureFrom (env : Ixon.Env) (target : Address) : Std.HashSet Address := Id.run do
+  let mut visited : Std.HashSet Address := {}
+  let mut worklist : Array Address := #[target]
+  while !worklist.isEmpty do
+    let addr := worklist.back!
+    worklist := worklist.pop
+    if visited.contains addr then continue
+    visited := visited.insert addr
+    match env.consts.get? addr with
+    | none => pure ()
+    | some c =>
+      for r in c.refs do
+        if !visited.contains r then worklist := worklist.push r
+      let blockAddr? : Option Address := match c.info with
+        | .iPrj p => some p.block
+        | .cPrj p => some p.block
+        | .rPrj p => some p.block
+        | .dPrj p => some p.block
+        | _ => none
+      match blockAddr? with
+      | some ba => if !visited.contains ba then worklist := worklist.push ba
+      | none => pure ()
+  return visited
+
+/-- Build the `ixon_serde_test` / `ixon_serde_blake3_bench` IOBuffer:
+    one entry per const, keyed by its index. Returns the buffer and the
+    count `n` (which the Aiur entrypoint receives as input). -/
+def buildSerdeIOBuffer (ixonEnv : Ixon.Env) : Aiur.IOBuffer × Nat :=
+  ixonEnv.consts.valuesIter.fold (init := (default, 0)) fun (ioBuffer, i) c =>
+    let (_, bytes) := Ixon.Serialize.put c |>.run default
+    (ioBuffer.extend #[.ofNat i] (bytes.data.map .ofUInt8), i + 1)
+
+/-- Encode a `Lean.ReducibilityHints` as a single `G` per the convention
+    Aiur's `load_constant_hint` decodes (opaque → 0, abbrev → 0xFFFFFFFF,
+    regular n → clamp(1 + n, 0xFFFFFFFE)). -/
+private def hintToG : Lean.ReducibilityHints → Aiur.G
+  | .opaque => .ofNat 0
+  | .abbrev => .ofNat 0xFFFFFFFF
+  | .regular n =>
+    let v := 1 + n.toNat
+    .ofNat (if v > 0xFFFFFFFE then 0xFFFFFFFE else v)
+
+/-- Insert all per-address entries for `addr`s satisfying `keep` into
+    `ioBuffer`, following the IOBuffer convention:
+
+    | key                    | value          | meaning |
+    |------------------------|----------------|---------|
+    | `addr` (32 G)          | const bytes    | primary data; empty value = `addr` is a blob |
+    | `addr ++ [0]` (33 G)   | raw blob bytes | referenced data (verified by Aiur via blake3) |
+    | `addr ++ [1]` (33 G)   | single G       | Defn `ReducibilityHints` encoding |
+
+    Suffix tags use `Array.push` (O(1) amortized) rather than prefix
+    `++ Array` (O(n) allocation). -/
+private def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
+    (ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
+  let mut ioBuffer := ioBuffer
+  for (addr, c) in ixonEnv.consts do
+    if !keep addr then continue
+    let (_, bytes) := Ixon.Serialize.put c |>.run default
+    let key : Array Aiur.G := addr.hash.data.map .ofUInt8
+    ioBuffer := ioBuffer.extend key (bytes.data.map .ofUInt8)
+  for (addr, rawBytes) in ixonEnv.blobs do
+    if !keep addr then continue
+    let hashKey : Array Aiur.G := addr.hash.data.map .ofUInt8
+    ioBuffer := ioBuffer.extend (hashKey.push 0)
+      (rawBytes.data.map fun b => .ofNat b.toNat)
+    ioBuffer := ioBuffer.extend hashKey #[]
+  for (_, named) in ixonEnv.named do
+    if !keep named.addr then continue
+    match named.constMeta with
+    | .defn _ _ hints _ _ _ _ _ =>
+      let hashKey : Array Aiur.G := named.addr.hash.data.map .ofUInt8
+      ioBuffer := ioBuffer.extend (hashKey.push 1) #[hintToG hints]
+    | _ => pure ()
+  return ioBuffer
+
+/-- Build the full `kernel_check_test` IOBuffer for the entire `ixonEnv`. -/
+def buildKernelCheckIOBuffer (ixonEnv : Ixon.Env) : Aiur.IOBuffer :=
+  addEntries ixonEnv (fun _ => true) default
+
+/-- Blake3 address bytes of `name` (the target input to `kernel_check_test`). -/
+def kernelCheckTarget (name : Lean.Name) (ixonEnv : Ixon.Env) : Array Aiur.G :=
+  match ixonEnv.getAddr? (Ix.Name.fromLeanName name) with
+  | some addr => addr.hash.data.map .ofUInt8
+  | none => panic! s!"{name} not found in Ixon environment"
+
+/-- Build a minimal `kernel_check_test` IOBuffer reachable from `target`
+    in `ixonEnv`. Used by drivers (e.g. `KernelArena.lean`) that compile
+    a single shared env once and then check many targets against it. -/
+def buildKernelCheckIOBufferFor (ixonEnv : Ixon.Env) (target : Address) :
+    Aiur.IOBuffer :=
+  let closure := closureFrom ixonEnv target
+  addEntries ixonEnv closure.contains default
+
+end IxVM.CheckHarness
+
+end