IxVM kernel: Ixon Claim-shaped entrypoint

Benchmarks/CheckNatAddComm.lean

@@ -24,20 +24,20 @@ def main : IO Unit := do
     | throw (IO.userError "Merging failed")
   let .ok compiled := toplevel.compile
     | throw (IO.userError "Compilation failed")
-  let some funIdx := compiled.getFuncIdx `kernel_check_test
-    | throw (IO.userError "Aiur function not found")
+  let some funIdx := compiled.getFuncIdx `verify_claim
+    | throw (IO.userError "verify_claim entrypoint missing")
   let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
 
   let env ← get_env!
-  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 ixonEnv ← IxVM.ClaimHarness.loadIxonEnv ``Nat.add_comm env
+  let target ← IxVM.ClaimHarness.lookupAddr ixonEnv ``Nat.add_comm
+  -- `assumptions = none` = full transitive typecheck.
+  let witness ← IO.ofExcept <| IxVM.ClaimHarness.buildClaimWitness ixonEnv
+    (Ix.Claim.check target none)
 
   let _ ← bgroup "Kernel typechecking" { oneShot := true } do
     throughput (.Elements ixonEnv.consts.size.toUInt64 "consts")
     bench "check Nat.add_comm"
-      (aiurSystem.prove friParameters funIdx input)
-      ioBuffer
+      (aiurSystem.prove friParameters funIdx witness.input)
+      witness.inputIOBuffer
   return

Benchmarks/IxVM.lean

@@ -29,8 +29,8 @@ def main : IO Unit := do
   let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
 
   let env ← get_env!
-  let ixonEnv ← IxVM.CheckHarness.loadIxonEnv ``Nat.add_comm env
-  let (ioBuffer, n) := IxVM.CheckHarness.buildSerdeIOBuffer ixonEnv
+  let ixonEnv ← IxVM.ClaimHarness.loadIxonEnv ``Nat.add_comm env
+  let (ioBuffer, n) := IxVM.ClaimHarness.buildSerdeIOBuffer ixonEnv
 
   let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
     throughput (.Elements n.toUInt64 "consts")

Ix/IxVM.lean

@@ -18,7 +18,8 @@ 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 import Ix.IxVM.Kernel.Claim
+public import Ix.IxVM.ClaimHarness
 
 public section
 
@@ -42,25 +43,6 @@ def entrypoints := ⟦
     }
   }
 
-  -- `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 target = store(target_addr);
-    let (k_consts, addrs) = ingress_with_primitives(target);
-    match check_deps {
-      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),
-    }
-  }
-
   fn level_cmp_tests() {
     -- Zero ≤ anything
     assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
@@ -187,6 +169,7 @@ def ixVM : Except Aiur.Global Aiur.Source.Toplevel := do
   let vm ← vm.merge inductive_check
   let vm ← vm.merge canonicalCheck
   let vm ← vm.merge check
+  let vm ← vm.merge claim
   vm.merge entrypoints
 
 end IxVM