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

[arthurpaulino]

Brings the Aiur-source kernel typechecker to parity with the Rust
kernel for the full stdlib, the lean-kernel-arena tutorial fixtures,
and the curated ixvm test list. Validated via a new arena test suite
plus the existing per-name kernel checks: 281/0 in
lake test -- --ignored ixvm.

Aiur source (Ix/IxVM/...):

• Kernel/{Whnf,DefEq,Levels,Infer,Subst,Inductive,Check, CanonicalCheck,Primitive}.lean: complete kernel split out from the
  monolithic Kernel.lean (deleted along with KERNEL.md). Mirrors
  src/ix/kernel/*.rs module-by-module.
• Ingress.lean: load Constants + blobs from the IOBuffer with
  blake3 verification; build per-position addrs/top. Compute
  constructor content-hash addresses entirely in-Aiur via
  cprj_content_addr (no IOBuffer side channel) so
  check_eq_type's address_eq against eq_refl_addr succeeds
  when an inductive's ctors weren't transitively loaded as
  independent CPrjs. Append synthetic Axiom Sort 0 entries for
  every hardcoded *_addr() primitive so internal expansions
  (str_lit_to_ctor, decidability dispatch, etc.) can construct
  Const(idx, _) references that resolve via find_addr_idx_safe
  even when the primitive isn't in the user's syntactic closure.
• IxVM.lean: kernel_check_test(target_addr, check_deps)
  entrypoint. check_deps = 1 runs check_all over every loaded
  const; check_deps = 0 runs check_const only on the target
  (saves the per-dep validation work — significant for proving
  since recursor canonical-build dominates).
• KernelTypes.lean, Convert.lean, Core.lean: supporting
  types/conversions for the kernel proper.

Rust side (src/aiur/execute.rs, src/ffi/aiur/protocol.rs,
src/aiur/{trace,synthesis}.rs):

• Refactor bytecode execute to return Result<_, ExecError>
  instead of panicking on assertion failures, missing match cases,
  or out-of-bounds. Plumbed through the FFI as Except String α so
  Lean callers can classify Aiur kernel rejections as expected
  outcomes rather than process crashes.
• synthesis::AiurSystem::prove keeps panic semantics by
  .expect-ing the inner Result (prover assumes valid input).
• trace.rs updated for the new IOBuffer return types.

Lean-side IO buffer / harness (Ix/IxVM/CheckHarness.lean):

• IOBuffer convention reorganized fundamental-first with suffix tags
  (addr.push(tag) is O(1) amortized; prefix [tag] ++ addr
  allocates):
  | addr | const bytes (or empty = blob marker) |
  | addr ++ [0] | raw blob bytes |
  | addr ++ [1] | single G (Defn ReducibilityHints) |
• loadIxonEnv (single-target) + loadSharedIxonEnv (union of N
  targets, one compile shared across many drivers).
• closureFrom walks Constant.refs + projection block_addr from
  a target. buildKernelCheckIOBufferFor restricts every per-address
  entry to that closure for a minimal per-target IOBuffer.
• addEntries helper dedupes the per-tag insertion logic between
  the full-env and per-target builders.

Tests (Tests/Ix/IxVM.lean, Tests/Ix/Kernel/Arena.lean,
Tests/Main.lean):

• Tests.Ix.IxVM reorganized into clear sections: IxVMPrim
  (primitive-reduction theorems), IxVMInd (mutual + nested
  inductives), serdeNatAddComm / kernelCheck / kernelChecks
  runners.
• Tests.Ix.Kernel.Arena drives the Aiur kernel against every
  lean-kernel-arena tutorial fixture (good must typecheck, bad must
  be rejected). Two knownIncompatible skips: tut06_bad01
  (Anon-mode dup levelParams hygiene check) and
  Tests.Ix.Kernel.TutorialDefs.AdvNat.rec (malformed rec rule
  sanitized by aux-gen). Both hold against the Rust kernel via
  Meta-mode-only / bespoke-FFI paths the Aiur kernel can't see.
• Tests.Main's ixvm runner builds an AiurTestEnv once and
  weaves both mkAiurTests's output and arenaTests's output into
  the same LSpec suite.

Misc:

• Tests/Aiur/Common.lean: surface execute's Except properly.
• Benchmarks/{CheckNatAddComm,IxVM}.lean: pass check_deps = 1
  explicitly to preserve existing semantics.
• Kernel.lean exe: handle the Except return.

Outstanding TODOs

Carried forward unchanged from the original Aiur kernel port:

• Ix/IxVM/Kernel/Primitive.lean::u64_add_with_carry
  Duplicates ByteStream.lean::u64_add to expose the final carry as
  (U64, G). Should be deleted once ByteStream.u64_add itself is
  patched to return the carry — the patch ripples beyond the kernel
  (Blake3, IxonSerialize, ByteStream itself), so a follow-up.

• Ix/IxVM/Kernel/Primitive.lean::divmod_256 (and u64_mul's
  schoolbook). Currently use divmod_256 byte-by-byte arithmetic.
  Should be replaced with a proper u8_mul Aiur gadget once it
  lands. Tracked on a separate branch.

WHNF fuel cap

Aiur deliberately omits Rust's MAX_WHNF_FUEL = 10_000. In a zk
prover context, divergent input fails to produce a proof — the caller
guarantees termination, so a soundness-preserving early abort isn't
needed. Documented inline at Whnf.lean::whnf.

Provenance

Each Aiur file/function carries Mirror: src/ix/kernel/... citations
so the Rust authority for any branch is one-grep away.