Aux-recursor block reconstruction gap for fresh-aux nested inductives

[arthurpaulino]

Summary

Aiur's kernel rejects Lean-generated aux recursors (X.rec_N) whose underlying nested-aux inductive is a fresh, solo, Lean-synthesised ind rather than an existing external one (like Array / List). The gap surfaces on nested-inductive shapes that Ix's mutual compile path splits into separate blocks rather than one shared block.

Root cause is out-of-circuit: Ixon's canonical Recursor main-data type does not carry Lean's RecursorVal.all field, so Aiur cannot reconstruct the block-member set the aux rec was generated over. The Rust kernel exhibits the same failure on the same fixture — this is not an Aiur-specific bug, it is an out-of-circuit modelling gap that both kernels inherit from Ixon.

Minimal repro fixture

namespace IxVMInd

mutual
 inductive AuxDedupA : Type where
 | mk : List AuxDedupB → List AuxDedupC → AuxDedupA
 inductive AuxDedupB : Type where
 | leaf : AuxDedupB
 inductive AuxDedupC : Type where
 | leaf : AuxDedupC
end

end IxVMInd

Ix compiles A, B, C into three separate Ixon blocks (Rust kernel probe confirms n_block_members=1 per const, nested=2 on A/B/C).

Failure

$ ix check --interp bytecode IxVMInd.AuxDedupA.rec_1
IxVMInd.AuxDedupA.rec_1: IxVM-native Aiur execution error: execute (bytecode): assert_eq mismatch: 0 != 1

Fires at check_recursor_member line 1825, assert_eq!(ty_eq, 1) — Aiur's canonical rec type differs from the declared one on k_is_def_eq. Same shape for AuxDedupA.rec_2. The primary AuxDedupA.rec and the inductives themselves have their own separate failures documented in the H1 block-collective / num_nested notes at the bottom of this issue.

Diagnosis

Instrumented check_recursor_member on AuxDedupA.rec_1:

probe	value	interpretation
n_p / n_mot / n_min / n_i	0 / 5 / 7 / 0	Lean declares a 5-member block
total_foralls in ty	13	matches n_p + n_mot + n_min + n_i + 1; peel count correct
self_major (peel-derived)	3	idx of a fresh solo aux ind, not A/B/C
self_ind (idx 3): n_params / n_ctors / is_rec / nested	1 / 2 / 1 / 0	List-clone shape (nil + cons), nested = 0
self_ind block_addr	non-zero, unique	no other Induct in top shares it
rec_block scan	1 rec found (rec_1 itself)	no siblings in same rec block
rule 0	ctor_idx=4, owning_ind=3, n_fields=0	aux ind's nil
rule 1	ctor_idx=5, owning_ind=3, n_fields=2	aux ind's cons
resolve_primary_ind_for_rec	3 (aux itself)	scans rec_block for a rec whose major has ne > 0; finds none → falls back to self_major
derive_block_member_idxs(3)	[3]	block_addr solo → 1 member
queue-based build_flat_block([3])	[3]	aux's cons field spine head = self (BVar / Const → aux), no external block members reachable
canonical n_motives	1	vs declared 5 → mismatch → assert fires

Cons ctor field types were also dumped:

• field 0: head_kind = BVar(0) — the α param.
• field 1: head_kind = Const(3) applied to 1 arg — self-recursive tail (aux α).

The aux ind is structurally a plain solo parametric List α clone whose ctors carry no reference to A / B / C in their field types. There is no in-top breadcrumb Aiur can follow from the aux ind back to the original mutual block.

Root cause

Lean's Lean.RecursorVal (see src/lean/Lean/Declaration.lean) carries all : List Name — the canonical list of every inductive in the mutual declaration the recursor was generated over. For nested-aux recs, all names the primary + all peers + all synthesised aux inds (5 names for AuxDedupA.rec_1).

Ix/CompileM.lean:compileRecursor (line 1013+) reads r.all, but writes it into Ixon.ConstantMeta.recr (metadata side channel), not into Ixon.Recursor (canonical main data):

let allAddrs := r.all.map (·.getHash)
...
let constMeta := Ixon.ConstantMeta.recr nameAddr lvlAddrs ruleAddrs allAddrs ctxAddrs arena typeRoot ruleRoots

Aiur's KConstantInfo.Rec (10 fields, Ix/IxVM/KernelTypes.lean:146) mirrors the canonical Ixon.Recursor:

Rec(G, KExpr, G, G, G, G, List‹KRecRule›, G, G, Addr)
 lvls, ty, n_p, n_i, n_m, n_min, rules, k_flag, is_unsafe, rec_block

No all field. Aiur has no way to see Lean's canonical block membership.

For Lean.Syntax.rec_1 this doesn't bite because its aux ind IS the external Array — already in top with its own well-formed block, and resolve_primary_ind_for_rec walks rec_block (which contains rec, rec_1, rec_2 — 3 recs sharing a block) and picks Syntax (ne = 2) as primary. The queue-based flat build (from the shard 53 fix) then correctly reconstructs [Syntax, Array, List] from Syntax's ctor field occurrences. AuxDedupA breaks this: no external ind to reuse, no shared rec_block sibling to pivot off of.

Proposed principled fix (cross-cutting, out-of-circuit)

Promote all from Ixon.ConstantMeta.recr metadata to Ixon.Recursor canonical main data:

1. Ixon type (Ix.Ixon): add all : Array Address (or List Address) to Ixon.Recursor.
2. Ixon serialize / deserialize (Anon codec): extend to write and read the new field.
3. Ix/CompileM.lean:compileRecursor: write allAddrs into the Ixon.Recursor main data, not (only) into ConstantMeta.recr.
4. Aiur type (Ix/IxVM/KernelTypes.lean): extend KConstantInfo.Rec with all_idxs : List‹G›.
5. Ixon → KConstantInfo ingest (Ix/IxVM/Convert.lean or equivalent): translate all addresses to positional idxs in top.
6. Aiur kernel logic:
   • derive_block_members_for_rec(rec_ci) := rec.all_idxs — replaces the current derive_block_member_idxs(primary_ind_idx) in check_recursor_member when checking a Rec.
   • resolve_primary_ind_for_rec picks the primary as the first all_idxs member whose Induct has ne > 0 (falls back to all_idxs[0] if none — matches Lean's block ordering convention).
   • Queue-based build_flat_block seeds from all_idxs instead of derive_block_member_idxs(primary); for AuxDedupA.rec_1 this seeds [A, B, C, aux_1, aux_2], then the queue-scan proceeds as it does today.

Side effects to expect

• Every existing pinned FFT cost in Tests/Ix/IxVM.lean:kernelCheckEntries bumps once (Ixon Recursor changes → new content addresses → different arena → different circuit widths). All ~50 pins need re-pin.
• Codegen kernel (crates/ix/src/aiur_ixvm.rs) regenerates.
• Ixon on-disk format shifts — any pre-serialised .ixe becomes stale (mitigated by content-addressing; ix compile from source regenerates).

Narrower alternate: metadata-side channel

Keep Ixon.Recursor untouched; extend Aiur's Ixon deserialiser to also load ConstantMeta.recr.allAddrs into a parallel table Aiur can query by rec position. Still out-of-circuit (ingest + Aiur Ixon reader changes), but no Ixon spec churn and existing pinned costs stay stable except where the new path fires.

Trade-off: metadata is not part of the security-critical canonical form. Trusting it changes the trust boundary; either accept that or bind allAddrs into the Recursor's content address via a hash commitment.

Non-fix alternates (unsound)

• Cross-scan top for Inducts that appear as spec_params of any nested aux and treat them as a virtual block. Fragile (misses members whose ctors don't yet appear in the current closure), order-dependent, and cannot recover Lean's block ordering (breaks BVar depth math).
• num_nested > 0 ⟹ is_rec = 1 as an H1 shortcut. Fixes the is_rec mismatch that surfaces on the ind check, but doesn't touch the check_recursor_member failure and diverges from the Rust kernel's H1 policy. Not landable on its own.

Pinned fixture status

The fixture lives in Ix/Cli/CheckCmd.lean (visible to both the ix check CLI and the test-suite Lean env). Tests/Ix/IxVM.lean:kernelCheckEntries holds six placeholder pins with cost 0:

• IxVMInd.AuxDedupA
• IxVMInd.AuxDedupB
• IxVMInd.AuxDedupC
• IxVMInd.AuxDedupA.rec
• IxVMInd.AuxDedupA.rec_1
• IxVMInd.AuxDedupA.rec_2

All six fail today; they become PASS + re-pinnable once the fix above lands.