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

Ix/IxVM/Kernel/Check.lean

@@ -2339,6 +2339,22 @@ def check := ⟦
           univ_offset, flat, flat_own_params, self_pos);
         assert_eq!(k_is_def_eq(ty, canonical_ty, store(ListNode.Nil)), 1,
           "recursor's declared type is not def-eq to the canonical reconstruction");
+        -- The type check pins the SUM of the motive and minor binders, but
+        -- not the SPLIT between them: a def-eq between two Pi telescopes
+        -- cannot tell where the motives end and the minors begin. Yet
+        -- `minor_var` (`populate_rules`) reads the declared `n_min` ALONE
+        -- to pick which binder each canonical rule body points at, so a
+        -- prover who moves mass between the two fields (sum preserved)
+        -- retargets every rule while the type stays honest. Pin both
+        -- against the reconstruction, as the reference does (`inductive.rs`
+        -- check_recursor "arity metadata mismatch").
+        let canon_n_motives = list_length(flat);
+        let canon_n_minors = list_length(build_all_minors(flat,
+          flat_own_params, n_p, canon_n_motives, n_p));
+        assert_eq!(n_mot, canon_n_motives,
+          "recursor motive count disagrees with the canonical reconstruction");
+        assert_eq!(n_min, canon_n_minors,
+          "recursor minor count disagrees with the canonical reconstruction");
         let self_ctors_offset = ctors_before_pos(flat, self_pos, 0);
         let canonical = populate_rules(num_ctors, self_ctors_offset,
           parent_block_addr, parent_ind_idx, n_p, n_mot, n_min, occ_us,

Ix/IxVM/Kernel/DefEq.lean

@@ -877,35 +877,28 @@ def defEq := ⟦
     }
   }
 
-  -- 1 iff `whnf(infer_only(ty))` is `Sort 0`.
+  -- 1 iff `whnf(infer_only(ty))` is a `Sort` whose level is SEMANTICALLY
+  -- zero (i.e. `Prop`).
   --
-  -- STRUCTURAL on purpose — do not swap this for `level_equal`. All three
-  -- references gate struct-eta and proof irrelevance on the level being
-  -- literally `Zero`: Rust `KUniv::is_zero` (`level.rs:112-114`, a
-  -- `matches!` on `UnivData::Zero`), `Ix/Tc` `KUniv.isZero`
-  -- (`Level.lean:64-66`), and lean4lean's `isProp`
-  -- (`TypeChecker.lean:192-193`), which compares against `.prop` with
-  -- structural `==`.
+  -- SEMANTIC on purpose — `level_equal`, matching `is_inductive_prop`
+  -- (`Infer.lean:260`) and all three references: Rust gates both struct-
+  -- eta (`whnf.rs:1884`) and proof irrelevance (`def_eq.rs:878`) on
+  -- `KUniv::is_semantic_zero`, `Ix/Tc` on `isSemanticZero`
+  -- (`Whnf.lean:1139`, `DefEq.lean:817`), and lean4lean's `isProp` on
+  -- `Level.isAlwaysZero` (`TypeChecker.lean:230`), all of which normalize.
   --
-  -- It is sound because levels are built by SIMPLIFYING constructors —
-  -- `level_imax` collapses `imax u 0` to `Zero` at construction, as
-  -- Rust's `KUniv::imax` and lean4lean's `mkLevelIMax'` do — and because
-  -- the test runs after `whnf`. So a Prop cannot reach here spelled any
-  -- other way.
-  --
-  -- Note this is NOT the rule everywhere: the projection-field Prop test
-  -- normalizes in Rust (`univ_eq`, `infer.rs:516`) and in `Ix/Tc`
-  -- (`Infer.lean:315`), which is why `is_inductive_prop` uses
-  -- `level_equal`. Those two tests are deliberately different.
+  -- A structural `KLevelNode.Zero` test is UNSOUND here: `convert_univ`
+  -- (`Convert.lean:87`) is a raw conversion, so a prover can author
+  -- `Sort (max 0 0)` / `Sort (imax 1 0)` — semantically zero, structurally
+  -- not — and `whnf` is the identity on `Srt`. Reading such a Prop as
+  -- "not Prop" fires `try_struct_eta_iota` on a proof, the reduction
+  -- lean4#14613 fixed (see `Tests/Ix/IxVM/Exploits.lean`
+  -- `struct-eta-fires-on-semantic-prop`).
   fn is_prop_type(ty: KExpr, types: List‹KExpr›) -> G {
     let sort = k_infer_only(ty, types);
     let sort_w = whnf(sort, types);
     match load(sort_w) {
-      KExprNode.Srt(l) =>
-        match load(l) {
-          KLevelNode.Zero => 1,
-          _ => 0,
-        },
+      KExprNode.Srt(l) => level_equal(l, store(KLevelNode.Zero)),
       _ => 0,
     }
   }

Ix/IxVM/Kernel/NatPrim.lean

@@ -229,26 +229,6 @@ def natPrim := ⟦
      0x11u8, 0x9bu8, 0xcau8, 0x51u8, 0xd7u8, 0xb0u8, 0xbdu8, 0xd5u8])
   }
 
-  fn size_of_size_of_addr() -> Addr {
-    store([0xa3u8, 0x43u8, 0xa6u8, 0x51u8, 0xbfu8, 0xf4u8, 0x08u8, 0xc3u8,
-     0xa2u8, 0x9fu8, 0xf2u8, 0x7bu8, 0x2bu8, 0x62u8, 0xe3u8, 0x4bu8,
-     0x54u8, 0xb2u8, 0xabu8, 0x38u8, 0x1cu8, 0xf6u8, 0xf3u8, 0xadu8,
-     0x87u8, 0xc5u8, 0x40u8, 0xc9u8, 0x77u8, 0xdcu8, 0x3cu8, 0x4au8])
-  }
-
-  fn punit_addr() -> Addr {
-    store([0x2du8, 0xfcu8, 0x16u8, 0xafu8, 0x01u8, 0xb8u8, 0x2bu8, 0x3bu8,
-     0x91u8, 0xc2u8, 0xffu8, 0x70u8, 0x44u8, 0x09u8, 0xd7u8, 0x62u8,
-     0x36u8, 0xa8u8, 0x3fu8, 0x95u8, 0x6cu8, 0x0cu8, 0x6eu8, 0x66u8,
-     0x59u8, 0xa6u8, 0x4fu8, 0xe2u8, 0x1du8, 0x76u8, 0x69u8, 0x5bu8])
-  }
-
-  fn unit_addr() -> Addr {
-    store([0x92u8, 0x32u8, 0x49u8, 0x86u8, 0x67u8, 0xf7u8, 0x65u8, 0xf4u8,
-     0x37u8, 0xdeu8, 0xdau8, 0xacu8, 0x82u8, 0x8eu8, 0x55u8, 0x5fu8,
-     0x6cu8, 0xc6u8, 0x7au8, 0x20u8, 0xe6u8, 0xdbu8, 0x28u8, 0xf6u8,
-     0x14u8, 0xfdu8, 0xf3u8, 0xc2u8, 0x62u8, 0x71u8, 0x0fu8, 0xebu8])
-  }
 
   fn is_native_prim_addr(a: Addr) -> G {
     match address_eq(a, system_platform_num_bits_addr()) {
@@ -265,11 +245,7 @@ def natPrim := ⟦
             _ =>
             match address_eq(a, subtype_val_addr()) {
               1 => 1,
-              _ =>
-              match address_eq(a, size_of_size_of_addr()) {
-                1 => 1,
-                _ => 0,
-              },
+              _ => 0,
             },
           },
         },
@@ -305,9 +281,6 @@ def natPrim := ⟦
         match address_eq(head_addr, subtype_val_addr()) {
           1 => try_reduce_subtype_val(spine),
           _ =>
-          match address_eq(head_addr, size_of_size_of_addr()) {
-            1 => try_reduce_size_of_unit(spine),
-            _ =>
               let is_rb = address_eq(head_addr, reduce_bool_addr());
               let is_rn = address_eq(head_addr, reduce_nat_addr());
               match is_rb + is_rn {
@@ -324,7 +297,6 @@ def natPrim := ⟦
                       },
                   },
               },
-          },
         },
       },
     }
@@ -350,29 +322,6 @@ def natPrim := ⟦
     }
   }
 
-  -- SizeOf.sizeOf.{u} Unit/PUnit ... → 1. First arg = type.
-  fn try_reduce_size_of_unit(spine: List‹KExpr›) -> (G, KExpr) {
-    match u32_less_than(list_length(spine), 1) {
-      1 => (0, store(KExprNode.BVar(0))),
-      _ =>
-        match collect_spine(list_lookup(spine, 0)) {
-          (head, _) =>
-            match load(head) {
-              KExprNode.Const(caddr, _) =>
-                match address_eq(caddr, unit_addr()) {
-                  1 => (1, mk_nat_one()),
-                  _ =>
-                    match address_eq(caddr, punit_addr()) {
-                      1 => (1, mk_nat_one()),
-                      _ => (0, store(KExprNode.BVar(0))),
-                    },
-                },
-              _ => (0, store(KExprNode.BVar(0))),
-            },
-        },
-    }
-  }
-
   fn check_native_bool(e: KExpr) -> (G, KExpr) {
     match load(e) {
       KExprNode.Const(caddr, _) =>
@@ -800,17 +749,12 @@ def natPrim := ⟦
               KExprNode.Lit(lit) =>
                 match lit {
                   KLiteral.Str(bs) =>
-                    -- The length must be a CANONICAL `KLimbs`, because
-                    -- `klimbs_eq` — behind `Nat.beq`/`Nat.decEq`/
-                    -- `literal_eq` — compares limbs without normalizing.
-                    -- `klimbs_from_g` range-checks and pins its byte
-                    -- decomposition (so a length >= 256 lands in the right
-                    -- limb instead of an out-of-range digit), and
-                    -- `klimbs_normalize` strips the all-zero limb so the
-                    -- empty string yields the canonical zero rather than
-                    -- `[[0;8]]`.
-                    let limbs =
-                      klimbs_normalize(klimbs_from_g(list_length(bs)));
+                    -- `klimbs_from_g` range-checks its byte decomposition
+                    -- (so a length >= 256 lands in the right limb) and
+                    -- returns a canonical `KLimbs` — required because
+                    -- `klimbs_eq` (behind `Nat.beq`/`Nat.decEq`/
+                    -- `literal_eq`) compares limbs without normalizing.
+                    let limbs = klimbs_from_g(list_length(bs));
                     (1, store(KExprNode.Lit(KLiteral.Nat(limbs)))),
                   _ => (0, store(KExprNode.BVar(0))),
                 },
@@ -1153,8 +1097,14 @@ def natPrim := ⟦
         assert_eq!(x, to_field(b0) + 256 * to_field(b1)
                    + 65536 * to_field(b2) + 16777216 * to_field(b3),
           "u32 byte split does not recompose to the original value");
-        store(ListNode.Cons([b0, b1, b2, b3, 0u8, 0u8, 0u8, 0u8],
-                            store(ListNode.Nil))),
+        -- Normalize HERE, not at each caller: `x == 0` gives the all-zero
+        -- limb, which is the denormalized `[[0;8]]`. `klimbs_eq` (behind
+        -- `Nat.beq`/`decEq`) compares limbs without normalizing, so an
+        -- unnormalized zero disagrees with the canonical empty list and
+        -- makes a reducer's literal wrong. Callers used to normalize
+        -- individually and one (`String.back`) was missed.
+        klimbs_normalize(store(ListNode.Cons(
+          [b0, b1, b2, b3, 0u8, 0u8, 0u8, 0u8], store(ListNode.Nil)))),
     }
   }