Aiur kernel: complete port from Rust reference

[arthurpaulino]

Splits the prior monolithic NbE-based draft into a substitution-based, file-per-concern Aiur kernel that mirrors src/ix/kernel/*.rs and now typechecks every primitive case + mutual + nested-aux recursor that the Rust kernel handles (modulo a deliberate WHNF fuel-cap omission, see below). Replaces the deleted Ix/IxVM/Kernel.lean (~2k lines of dead NbE code) with:

  Ix/IxVM/Kernel/Subst.lean         — expr_lift, expr_inst1, expr_lbr
  Ix/IxVM/Kernel/Levels.lean        — universe leq/eq (Lean4Lean port)
  Ix/IxVM/Kernel/Whnf.lean          — whnf, iota, K-target, struct-eta,
                                      cleanup_nat_offset_major
  Ix/IxVM/Kernel/Primitive.lean     — Nat / String / BitVec / Decidable
  Ix/IxVM/Kernel/Infer.lean         — k_infer, k_check, k_ensure_sort,
                                      proof-irrelevance, Prop-projection
  Ix/IxVM/Kernel/DefEq.lean         — tiered structural / WHNF / lazy-delta /
                                      eta / proof-irrelevance / unit-like
  Ix/IxVM/Kernel/Inductive.lean     — A1-A4, H1, S3/S3b mutual peer
                                      agreement, K-target, flat-aware
                                      recursor type + rule synthesis,
                                      block-canonical sort
  Ix/IxVM/Kernel/CanonicalCheck.lean — Indc-only canonical block sort,
                                      ctx-aware partition refinement
  Ix/IxVM/Kernel/Check.lean         — per-kind dispatch entrypoint

Soundness

• compute_is_rec (H1): constructively recompute the inductive's is_rec flag and assert equal to declared. Without this an adversary could set is_rec=0 on a recursive 1-ctor inductive to enable struct eta, which is unsound. Mirror src/ix/kernel/inductive.rs:309-315.
• Param-domain agreement (A1) wired into the Ctor arm at point of use, in addition to the existing mutual-peer S3b path.
• S3 universe agreement uses n_params + n_indices for self_lvl (was previously self_n_params only, mismatching peer_lvl).
• Canonical block-sort filters to Indc-only, mirroring the Rust ingress rule that excludes Recr/Defn/Ctor entries from the sorted partition.
• Ctor block_addr derivation: Rec returns its own ba (added 10th field to KConstantInfo.Rec); Ctor inherits parent's ba; non-Indc/non-Ctor constants return [0;32] so they don't fold into a block.

Completeness

• Five Prop-guard sites switched from syntactic level_eq(L, KLevel.Zero) to semantic level_equal. Rust uses the equivalent univ_eq in all of these locations; the syntactic check rejects valid universe-poly Mathlib terms whose levels reach the guard as Max(0, 0) or IMax(_, 0) after substitution. Sites: Theorem Prop guard, Prop inductive check, Prop-projection field guard, dependent-data-field guard, large-eliminator data-field check.

• cleanup_nat_offset_major ported. When the Nat.rec major has shape base + k_lit with k_lit > 0, expose one Nat.succ layer so iota fires without delta-unfolding Nat.add and allocating O(k) intermediates. Mirror whnf.rs:1113-1143.

• Multi-member recursor synthesis (mutual blocks). flat block with per-member (ind_idx, is_aux, spec_params, occurrence_us) threading; peer_recs resolved within the recursor's block_addr; cross-member IH calls dispatched to peer recursors; ctor params peeled with appropriate substitution (recursor-param BVars for non-aux, spec_params for aux); per-target own_params used for idx_args = drop(spine, target_n_params).

• Nested-aux recursor synthesis (Tree.rec over Tree.mk : List Tree → Tree). gather_block_nested walks ctor field doms collecting external occurrences with (ext_idx, spec_params, occurrence_us); build_flat_block concatenates originals + auxes; resolve_primary_ind_for_rec walks the recursor block to find the canonical-block-source inductive (the one with nested > 0), so aux recursors (e.g. Tree.rec_1) build their canonical form against the original block (Tree's), not the aux's external Indc block (List's).

Ingress / Convert

• extract_member_ctor_idxs returns this recursor's own ctor positions (slicing members[member_idx] instead of returning all block ctors), so each mutual recursor's rules align with its own ctors.
• build_recur_idxs / build_rule_ctor_idxs rewritten as running-position walkers; the prior versions threaded both a shortened members and an incremented member_idx, which double-counted offsets and pointed Const refs at wrong kernel positions in mutual blocks.
• Constant.Mk-keyed Muts dedup (was Indc.Mk-keyed) so distinct String.Internal.append width-paramaterized wrappers no longer alias via shared blob-ref index. Resolves the previously-flaky String.Internal.append and extractMainModule cases.

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.

Tests

• Tests/Ix/IxVM.lean: new IxVMPrim namespace exercises Nat / Bitwise / Decidable / String / BitVec primitive reduction via rfl theorems.
• New IxVMInd namespace adds mutual { Even, Odd } (mutual block, multi-member recursor) and Tree { mk : List Tree → Tree } (nested inductive, aux recursor).
• kernelChecks expanded to cover all of the above plus the previously flaky String.Internal.append / extractMainModule cases.
• Tests/Main.lean: ixvm test re-enabled (was commented-out for the duration of the port).

Speed (preserves soundness/completeness)

• walk_fields_classify, peel_leading_foralls_acc, collect_n_doms_acc accumulate via O(1) cons + final reverse instead of O(F²) snoc.
• lazy_delta_loop hoists head extraction once per iteration, dispatching to const-app congruence only when both heads are Const.
• Dead helpers removed: peel_n_subst_recparam_bvars, aggregate_ctor_indices.

Outstanding TODOs

These were left in place during the port and are tracked inline:

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

Provenance

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