Compiler fixes for auxiliary constant generation (#473)

* Ixon: drop recr/refl/nested flags from Inductive

Remove the `recr`/`refl` bools and the `nested` count from the Ixon
`Inductive` constant and its serialization (Rust and Lean), and from
the `Indc` reveal-proof variant, renumbering the field-presence mask
bits. These flags are derivable from constructor structure, so storing
them was redundant and trusting declared values was an adversarial
surface (e.g. is_rec = false on a recursive inductive enables improper
struct-eta).

- kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now
  computed on demand (computed_is_rec), memoized in the new env
  is_rec_cache with a provisional entry to break the whnf ->
  try_struct_eta_iota -> is_struct_like cycle. This replaces the
  declared-vs-computed H1 verification in check_inductive.
- compile: new compute_lean_ind_flags recomputes Lean's block-wide
  isRec/isReflexive/numNested wherever an InductiveVal is reconstructed
  without a source Lean env (kernel egress, decompile), since Ixon no
  longer stores the flags; validate_lean_ind_flags checks a whole env
  against the recomputation.
- tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising
  aux-constant dedup across blocks (fix forthcoming); add a
  CompileMutualFixtures benchmark lib building the mutual test
  fixtures; ignore *.ixe.

* Compile: evaporated-aux canonicalization and byte-exact aux roundtrip

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a
nested aux's spec-param inductives outside the owner's SCC, no SCC holds
the joint family, and dropping the irrelevant over-merged motives leaves
exactly the external inductive's generic recursor. Canonical treatment:
`rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are
rebuilt onto the external telescope via head-rewrite CallSitePlans
(owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile
as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check
failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to
AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a
perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner.
Documented in docs/ix_canonicity.md 6.5.

Call-site surgery guard is now durable across serialization: aux-regen
detection accepts `Named.original.is_some()` in addition to the
in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles
no longer misapply surgery. Shift-aware `instantiate_rev` replaces
unshifted substitution in the type-walking helpers (fixes fvar leaks in
`.brecOn.go` bodies).

Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the
ref/univ tables (`preseed_expr_tables`) like every production compile
path. The serialized constant embeds those tables in sorted order;
compiling without the preseed filled them in traversal order instead,
permuting every `Ref`/univ index — byte-different but semantically
identical constants (decode resolves through the embedded table). This
silently failed the Phase-A address comparison against
`Named.original.0` for 1529 of 1545 aux constants (including plain
stdlib like `Nat.casesOn`); a debug probe proved
compile(original) == compile(regen) in every case, i.e. the
regeneration itself was always faithful.

With the invariant holding corpus-wide, the Phase-A recompile-hash
mismatch is now a hard error with no aux exemption, and every roundtrip
arm records failures in `aux_gen_errors` (recovery keeps the
Lean-facing env populated for diagnosis but is never silent). Pass-2
scope hygiene: the below-def roundtrip loop filters by the
original-gated `aux_members` like its sibling loops, so evaporated
`below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now
dumps hashed component scalars/hashes and runs an original-form
recompile probe for any mismatch.

Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry
recomputation-honest flags so compile-side `validate_ind_flags` no
longer poisons the shared tutorial env (73/335 -> 335/335, with the
kernel rejecting each bad fixture as designed); validate-aux seeds
match module-private fixture names via `privateToUserName?` and enable
the Canonicity prefix; Phase 4b gains per-module markers so a fully
absent identity group fails loudly when its fixture module is loaded
(previously vacuous at 0 pass / 0 fail, now 109 pass).

Gates: kernel-check-env 201296/201296; rust-compile all phases with 0
aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the
full 213k env (live and deserialized); validate-aux 0 failures at
4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip
143694/0; kernel-tutorial 335/335; cargo test and lake test green.

* chore: fix clippy warnings and fmt drift

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`:
map_or over map+unwrap_or and slice::contains in surgery.rs, an
enumerate loop for the motive-peeling walk in aux_motive_sigs, and
let-chain collapses for the inductive-flags fixup loops in decompile.rs
and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over
from the previous commit.

* IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen

Three interlocking bugs in the Aiur block-flattening / recursor-type
builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with
`assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality:

- `build_flat_block` traversed originals once; nested-aux members
  (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so
  `flat` had 2 motives when Lean's recursor declares 3. Replaced with a
  queue-based fixed point mirroring `crates/kernel/src/inductive.rs:
  build_flat_block:531-599`.

- `is_rec_field` classified any ctor field as recursive when its spine
  head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`,
  the field `preresolved : List Preresolved` shares the base List const
  idx with the block's `List Lean.Syntax` aux and got a spurious
  `motive_2 preresolved` IH binder. Match key is now (head_idx,
  spine-arg prefix ≡ member.spec_params) — direct members carry
  `spec_params = []` and match on idx alone, auxes require the concrete
  occurrence.

- `build_all_minors` was iterating `flat` and passing the shrinking
  suffix into `build_minor_doms`, so field classification for later
  members was blind to earlier members. Split into a wrapper +
  `build_all_minors_walk` that pins the caller's full flat while the
  iteration state shrinks.

Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost
shifted by the codegen refresh (`ix codegen`).

* IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel

Port of the two Rust kernel fixes on this branch:

- Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct
  drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand
  (computed_is_rec_ind), nested detection is structural (member_has_nested /
  ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten
  member-scoped without the declared nested count. Serialization packs one
  bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive
  addresses re-pinned.

- collectDependencies (Ix/Common.lean) now closes over a declaration's full
  recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference
  in rule RHSs) plus each rule ctor's owning external recursor (List.rec).
  Without these the per-name compile either failed (MissingConstant
  AuxDedup1.C.rec from A.rec_1's block) or silently skipped the
  evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2
  in original form, which the kernel rejects.

AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join
kernelCheckEntries; the four evaporated rec_N entries pin the identical
3_073_003 FFT cost (their claims are byte-exact List.rec:
lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2).
All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop
shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

---------

Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com>

Author: johnchandlerburnham

.gitignore

@@ -7,3 +7,7 @@
 # Nix
 result*
 .direnv/
+
+#Ix
+*.ixe
+plans

Benchmarks/Compile/CompileMutualFixtures.lean

@@ -0,0 +1 @@
+import Tests.Ix.Compile.Mutual

Benchmarks/Compile/lake-manifest.json

@@ -21,6 +21,13 @@
    "inputRev": "v4.29.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "ix",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../..",
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -110,6 +117,26 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": true,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/argumentcomputer/Blake3.lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "name": "Blake3",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/argumentcomputer/LSpec",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "Compile",
  "lakeDir": ".lake"}

Benchmarks/Compile/lakefile.toml

@@ -17,6 +17,13 @@ name = "CompileMathlib"
 [[lean_lib]]
 name = "CompileFLT"
 
+[[lean_lib]]
+name = "CompileMutualFixtures"
+
+[[require]]
+name = "ix"
+path = "../.."
+
 [[require]]
 name = "flt"
 git = "https://github.com/ImperialCollegeLondon/FLT"

Ix/Claim.lean

@@ -94,10 +94,9 @@ structure RevealRecursorRule where
 inductive RevealMutConstInfo where
   | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
          (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
-  | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
-         (lvls : Option UInt64) (params : Option UInt64)
-         (indices : Option UInt64) (nested : Option UInt64)
-         (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
+  | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
+         (indices : Option UInt64) (typ : Option Address)
+         (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
   | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
          (params : Option UInt64) (indices : Option UInt64)
          (motives : Option UInt64) (minors : Option UInt64)
@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
     match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
     match typ with | some a => Serialize.put a | none => pure ()
     match value with | some a => Serialize.put a | none => pure ()
-  | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
+  | .indc isUnsafe lvls params indices typ ctors => do
     putU8 1
-    let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
-                             lvls.isSome, params.isSome, indices.isSome,
-                             nested.isSome, typ.isSome, ctors.isSome]
+    let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
+      indices.isSome, typ.isSome, ctors.isSome]
     putTag0 ⟨mask⟩
-    match isRecr with | some b => putBoolField b | none => pure ()
-    match refl with | some b => putBoolField b | none => pure ()
     match isUnsafe with | some b => putBoolField b | none => pure ()
     match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
     match params with | some n => putTag0 ⟨n⟩ | none => pure ()
     match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
-    match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
     match typ with | some a => Serialize.put a | none => pure ()
     match ctors with | some c => putCtors c | none => pure ()
   | .recr k isUnsafe lvls params indices motives minors typ rules => do
@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
     let value ← getOpt mask 16 Serialize.get
     return .defn kind safety lvls typ value
   | 1 => do -- Indc
-    let isRecr ← getOpt mask 1 getBoolField
-    let refl ← getOpt mask 2 getBoolField
-    let isUnsafe ← getOpt mask 4 getBoolField
-    let lvls ← getOpt mask 8 getTag0Size
-    let params ← getOpt mask 16 getTag0Size
-    let indices ← getOpt mask 32 getTag0Size
-    let nested ← getOpt mask 64 getTag0Size
-    let typ ← getOpt mask 128 Serialize.get
-    let ctors ← getOpt mask 256 getCtors
-    return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
+    let isUnsafe ← getOpt mask 1 getBoolField
+    let lvls ← getOpt mask 2 getTag0Size
+    let params ← getOpt mask 4 getTag0Size
+    let indices ← getOpt mask 8 getTag0Size
+    let typ ← getOpt mask 16 Serialize.get
+    let ctors ← getOpt mask 32 getCtors
+    return .indc isUnsafe lvls params indices typ ctors
   | 2 => do -- Recr
     let k ← getOpt mask 1 getBoolField
     let isUnsafe ← getOpt mask 2 getBoolField

Ix/Commit.lean

@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
       for j in [:i.ctors.size] do
         arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
       return arr
-    .indc (some i.recr) (some i.refl) (some i.isUnsafe)
-      (some i.lvls) (some i.params) (some i.indices) (some i.nested)
+    .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
       (some (exprAddr i.typ)) (some ctors)
   | .recr r =>
     let rules := Id.run do

Ix/Common.lean

@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
     goExpr consts acc val.value
   | .recInfo val =>
     let acc ← collectNames val.all acc
+    -- The compiler processes a declaration's recursors as one block, and
+    -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
+    -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
+    -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
+    let siblings := val.all.filterMap fun ind =>
+      let n := Lean.mkRecName ind
+      if consts.contains n then some n else none
+    let auxSiblings : List Lean.Name := Id.run do
+      let mut out := []
+      let mut i := 1
+      repeat
+        match val.all.head? with
+        | none => break
+        | some base =>
+          let n := Lean.Name.mkStr base s!"rec_{i}"
+          if consts.contains n then
+            out := n :: out
+            i := i + 1
+          else break
+      return out
+    let acc ← collectNames (siblings ++ auxSiblings) acc
+    -- A nested-aux recursor's rules recurse via the external container's
+    -- ctors; its evaporated form aliases that container's recursor
+    -- (`List.rec`), which no collected expr mentions — pull it via each
+    -- rule ctor's owning inductive.
+    let extRecs := val.rules.filterMap fun rule =>
+      match consts.find? rule.ctor with
+      | some (.ctorInfo cv) =>
+        if val.all.contains cv.induct then none
+        else
+          let n := Lean.mkRecName cv.induct
+          if consts.contains n then some n else none
+      | _ => none
+    let acc ← collectNames extRecs acc
     let acc ← goExpr consts acc val.type
     val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
 where

Ix/CompileM.lean

@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
     let ctxAddrs ← getMutCtxAddrs
 
     let ind : Ixon.Inductive := {
-      recr := i.isRec
-      refl := i.isReflexive
       isUnsafe := i.isUnsafe
       lvls := i.cnst.levelParams.size.toUInt64
       params := i.numParams.toUInt64
       indices := i.numIndices.toUInt64
-      nested := i.numNested.toUInt64
       typ := typeExpr
       ctors := ctors
     }
@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
     let ctxAddrs ← getMutCtxAddrs
 
     let ind : Ixon.Inductive := {
-      recr := i.isRec
-      refl := i.isReflexive
       isUnsafe := i.isUnsafe
       lvls := i.levelParams.size.toUInt64
       params := i.numParams.toUInt64
       indices := i.numIndices.toUInt64
-      nested := i.numNested.toUInt64
       typ := typeExpr
       ctors := ctors
     }

Ix/DecompileM.lean

@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
     cnst := { name, levelParams := univParams, type := typeExpr },
     numParams := ind.params.toNat, numIndices := ind.indices.toNat,
     all := allNames, ctors := ctorNames,
-    numNested := ind.nested.toNat, isRec := ind.recr,
-    isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
+    -- temporary stub until we update the Lean compiler and decompiler semantics
+    numNested := 0, isRec := false
+    isUnsafe := ind.isUnsafe, isReflexive := false }
   pure (indVal, ctors)
 
 /-! ## Projection Handling -/

Ix/IxVM/Convert.lean

@@ -314,11 +314,11 @@ def convert := ⟦
     match ctx {
       ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
         match ind {
-          Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
+          Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
             let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
             KConstantInfo.Induct(
               flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
-              ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
+              ctor_idxs, is_unsafe, block_addr),
         },
     }
   }