IxVM soundness audit: three kernel holes closed, pinned as regressions

[arthurpaulino]

Summary

A deep soundness audit of the IxVM kernel (Codex lead + a four-agent
review against the Rust, Ix/Tc and lean4lean references) surfaced three
genuinely exploitable soundness holes and one non-weaponizable bug. Each
exploitable hole is first reproduced as an adversarial Ixon fixture that
the kernel wrongly accepts, then fixed so the fixture flips to a correct
rejection. Codegen is regenerated and the FFT pins repinned. A dedicated
regression constant guards the one fix whose reduction path the test
corpus did not otherwise exercise.

Holes found and fixed

Hole	What the kernel wrongly did	Fix
SizeOf ignores instance	try_reduce_size_of_unit folded @SizeOf.sizeOf Unit _ () → 1 reading only the type argument, so @SizeOf.sizeOf Unit ⟨fun _ => 5⟩ () = 1 typechecked by rfl (it is 5 in Lean).	Drop the native fold; reduce honestly through the instance projection, as lean4lean does (NatPrim.lean).
Recursor arity metadata unvalidated	The declared motives/minors split was never checked against the reconstruction. The type check pins only their sum, but minor_var reads minors alone, so a forged split (sum preserved) retargets every iota rule — R mo m0 m1 c0 ↝ mo, i.e. (I → Type) : Type → Girard.	Assert the declared motives/minors counts equal the canonical reconstruction, matching inductive.rs (Check.lean).
is_prop_type structural vs semantic zero	Prop was tested against the structural node KLevelNode.Zero; all three references test semantic zero. A prover-authored Sort (max 0 0) then fired struct-eta on a Prop-typed major (the lean4#14613 guard).	Test semantic zero via level_equal(l, Zero), matching is_inductive_prop and every reference (DefEq.lean).
Denormalized codepoint (not fixturable)	klimbs_from_g(0) returned the denormalized [[0;8]] rather than the canonical empty list; klimbs_eq (behind Nat.beq/decEq) compares limbs without normalizing, so a codepoint 0 from String.back/build_char_list compared unequal to 0.	Normalize inside klimbs_from_g so all callers are covered (NatPrim.lean). Not fixturable — the only reach-path forces Char.ofNat's validity dite and cascades rather than settling to a false accept.

The audit also cleared as faithful to the references: large elimination
of Prop, level construction/comparison, quotient reduction, proof
irrelevance, the projection def-eq, function/struct eta, lazy delta,
Nat-literal ingress, and the Int primitives.

Fixtures (Tests/Ix/IxVM/Exploits.lean)

Each exploit is paired with a control that differs minimally, so a green
suite cannot mean the fixture stopped reaching its target.

• sizeof-unit-ignores-instance + control-sizeof-unit-canonical-value
• recursor-motives-minors-split-forged + control-swapped-recursor-rules, recursor-rule-rhs-doctored-binder-domains
• struct-eta-fires-on-semantic-prop + control-struct-eta-syntactic-prop-declines

Regression guard (Tests/Ix/IxVM.lean)

IxVMPrim.sizeof_unit (sizeOf () = 1) forces the honest reduction of
the SizeOf.sizeOf class projection through the canonical Const
instance — the path the removed fold used to short-circuit, and the one
the exploit control (a literal SizeOf.mk) did not cover. If that
projection path regresses, the constant goes stuck and the pin fails.

Validation

• Exploit suite: all cases green — the three exploits reject, every
  control behaves as specified.
• ixvm kernel-check suite: the fixes shifted 76 FFT costs and the
  shard-pipeline cost; codegen (aiur_ixvm.rs) regenerated and all pins
  repinned. The codegen ↔ bytecode parity gate passes, and every real
  recursor still checks — the new arity assert rejects only the forged
  fixture, not HEq.rec/Eq.rec/the IxVMInd.*.recs (main, mutual,
  aux, nested and indexed).
• Full environment sweep: 648/648 shards passed, zero timeouts or
  errors, across all six environments.

Disclosure — sharding configuration. This sweep was run with a
slightly different sharding configuration from the repo's committed
shard layout. The FFT figures below are therefore not directly
comparable to the committed kernelCheckEntries / shard-pipeline pin
or to prior sweep baselines — per-shard FFT depends on how constants
are grouped. The meaningful result is the all-pass: every constant
across Init, InitStd, Batteries, Lean, Mathlib and FLT still checks
successfully under the fixes.

Environment	Shards	Total FFT	Most expensive shard	Peak RSS
Init	8	5.054T	5: 659.223B	18.09 GiB
InitStd	32	9.380T	2: 355.124B	12.80 GiB
Batteries	32	9.112T	17: 492.722B	15.65 GiB
Lean	64	13.271T	9: 276.358B	11.69 GiB
Mathlib	256	148.156T	212: 1.685T	35.15 GiB
FLT	256	154.146T	164: 1.247T	31.79 GiB

Total FFT cost: 339,118,996,450,290

Safety of the fixes

Each fix was analyzed for the two non-soundness failure modes and the
sweep is consistent with the analysis:

• Hang / cascade: none introduce unbounded recursion. level_equal
  and the recursor recompute are bounded; the honest SizeOf path is the
  same reduction Lean performs (stuck stays stuck, no loop); klimbs
  adds one bounded normalize.
• Wrong rejection: is_prop_type is byte-identical on canonical
  levels (real constants), diverging only on adversarial non-canonical
  ones, where it matches Lean. The recursor assert is implied by the
  existing type-check invariant, so it cannot reject a recursor the type
  check accepts. klimbs_from_g is strictly more canonical. The SizeOf
  removal was the one path needing empirical confirmation that honest
  reduction fires through the real Const instance — now pinned by
  IxVMPrim.sizeof_unit and confirmed by the full sweep.

Commits

1. test(ixvm): pin three soundness holes as exploit fixtures
2. fix(ixvm): close three kernel soundness holes
3. fix(ixvm): normalize klimbs_from_g output at the source
4. chore(ixvm): regen codegen and repin FFT after kernel fixes
5. test(ixvm): pin SizeOf.sizeOf Unit reduction as a regression fixture