IxVM kernel: Ixon Claim-shaped entrypoint

[arthurpaulino]

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

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.

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).