IxVM kernel: Ixon Claim-shaped entrypoint (#423)

Replaces `kernel_check_test(target_addr, check_deps)` with two
Aiur entrypoints in `Ix/IxVM/Kernel/Claim.lean`:

```rust
pub fn verify_claim(claim_digest: [G; 32])
pub fn dbg_check_const(target_addr: [G; 32])
```

## `verify_claim`

Public input is the 32-G blake3 digest of `Claim.ser claim`. Flow
mirrors `load_verified_constant`: read bytes from the IOBuffer at
key=`claim_digest`, recompute blake3, assert equality, deserialize
once into a typed Aiur `Claim` ADT, then dispatch.

```rust
pub fn verify_claim(claim_digest: [G; 32]) {
  let claim = load_verified_claim(claim_digest);
  match claim {
    Claim.Eval(i, o, asm) => run_eval(i, o, asm),
    Claim.Check(c, asm) => run_check(c, asm),
    Claim.CheckEnv(root, asm) => run_check_env(root, asm),
    Claim.Reveal(comm, info) => run_reveal(comm, info),
    Claim.Contains(t, c) => run_contains(t, c),
  }
}
```

`load_verified_claim` is the constant-load shape applied to claims:
recompute blake3, assert against the IO key, deserialize, assert
no trailing bytes.

Per-variant handlers:

* `run_check (c, asm)` — `asm=None`: full transitive `check_all`
  over the ingressed closure. `asm=Some root`: load the assumption
  tree at `root`, recompute its merkle root via `parse_atree_body`
  (mirrors `Ix.Merkle.leafHash`/`nodeHash`), assert match, then
  `check_all_skipping` — every position whose addr is in the leaf
  set is treated as an axiom (skipped), the rest are checked.

* `run_check_env (root, asm)` — load the env-tree at `root`,
  optionally load the assumption tree, then per env-leaf NOT in
  the assumption set: re-ingress its closure and `check_const`.
  Per-leaf ingress is the simplest model; closure sharing is a
  future optimization.

* `run_contains (tree_root, target)` — load assumption tree at
  `tree_root`, assert `target` appears as a leaf.

* `run_reveal (comm, info)` — load the constant at `comm`, match
  variant against `info`'s variant (Defn/Recr/Axio/Quot/CPrj/
  RPrj/IPrj/DPrj/Muts), then per-Some field assert equality.
  `Expr` fields bind via `expr_addr = blake3(put_expr e)` per
  docs/Ixon.md:970-971. Direct fields (kind, safety, lvls, idx,
  cidx, block, …) compare literally. Mismatched variant pairs
  fall off the non-exhaustive `match` — proof generation fails.

* `run_eval` — placeholder until Rust kernel pins reduction
  semantics.

## `dbg_check_const`

Non-claim debug entrypoint: subject-only `check_const`, transitive
deps trusted. Used by the arena suite and `lake exe kernel
--debug-fast`. Verifier policy must reject this funcidx as a
production claim.

## Aiur ADT mirror

`Ix/IxVM/Kernel/Claim.lean` defines mirrors of `Ix.Claim`
sub-types:

* `Claim` — 5 variants matching `Ix.Claim`.
* `RevealConstantInfo` / `RevealMutConstInfo` /
  `RevealConstructorInfo` / `RevealRecursorRule` — `Option‹...›`
  per field for selective revelation; Expr fields swapped for
  `Addr` content hashes. `(idx, info)` lists ride as
  `List‹(U64, _)›` tuples — no wrapper enum.

Parsers (`get_claim`, `get_reveal_info`,
`get_reveal_mut_const_info`, `get_reveal_ctor_info`,
`get_reveal_rule`, bitmask-gated `get_opt_*_masked`) cover every
wire-format arm. Match arms use enumerated discriminants without
default catch-alls; Aiur's non-exhaustive match suffices.

## Lean side

`Ix/IxVM/ClaimHarness.lean` (Lean ↔ Aiur glue):

* `ClaimWitness` record (`funcName`, `input`, `inputIOBuffer`).
* `buildClaimWitness (env claim trees := {}) : ClaimWitness` —
  serializes the claim, seeds it at key=`claim_digest`, ingests
  the relevant Ixon closure per variant, and seeds any
  caller-supplied `AssumptionTree` at key=`tree.root`.
* `buildDbgCheckConst (env target) : ClaimWitness`.
* `envCanonicalTree (env) : Option AssumptionTree` — convenience
  for `CheckEnv` against the env's canonical merkle root.

## Caller migrations

* `Tests/Ix/IxVM.lean::kernelCheck`        → `verify_claim`
  driving `Claim.check addr none`.
* `Tests/Ix/Kernel/Arena.lean::buildInput` → `dbg_check_const`.
* `Benchmarks/CheckNatAddComm.lean`         → `verify_claim`
  driving `Claim.check addr none`.
* `Kernel.lean` (`lake exe kernel`)         → `verify_claim`
  default; `--debug-fast` switches to `dbg_check_const`.

## Test coverage

Seven new claim-variant smoke tests wired into the `ixvm` ignored
suite via `claimSmokeTests` in `Tests/Ix/IxVM.lean`:

* `Claim Check with-asm (Nat.zero)`           — asm tree covering
  every dep; kernel ends up checking only the subject.
* `Claim Contains (synthetic 3-leaf)`         — membership against
  a synthetic 3-leaf canonical tree.
* `Claim CheckEnv (Nat.zero closure)`         — 4-const env-tree.
* `Claim Reveal Defn (kind+safety)`           — enum-tag compare.
* `Claim Reveal CPrj (all fields)`            — addr+u64 compare.
* `Claim Reveal Defn (typ Expr addr)`         — `expr_addr` vs
  Lean's `Address.blake3 (Ixon.runPut (putExpr d.typ))`.
* `Claim Reveal Muts (first component)`       — variant dispatch
  across the three `RevealMutConstInfo` sub-variants.

`Tests/Main.lean::ixvm` runner includes them alongside the
existing `kernelChecks` and `serdeNatAddComm` test cases. All 14
claim-check assertions (7 × Execute output + IOBuffer) pass under
`lake test -- --ignored ixvm`.

`lake exe kernel Nat.zero` is 1528173 FFT (vs 1527378 pre-PR —
+795 FFT for the Claim deserialization shim; acceptable).

Author: arthurpaulino

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