Validate every recursor in a recursor block.
(
&mut self,
block: &KId<M>,
members: &[KId<M>],
)
| 4035 | )?; |
| 4036 | |
| 4037 | // Position-by-position alignment. |
| 4038 | // |
| 4039 | // Both the kernel-side `flat` (rebuilt above with `canonical_aux_order` |
| 4040 | // when `RecursorAuxOrder::Canonical`) and `rec_ids` (the recursor block |
| 4041 | // members in their stored order) follow the same canonical permutation |
| 4042 | // by construction — see the rationale at the `canonical_aux_order` call |
| 4043 | // around line 2069 and `docs/ix_canonicity.md` §6.2. So generated peer |
| 4044 | // `gi` aligns with `rec_ids[gi]` directly: no search, no greedy match. |
| 4045 | // |
| 4046 | // We still verify the alignment by comparing extracted major-domain |
| 4047 | // signatures peer-by-peer. A mismatch means canonical order has in fact |
| 4048 | // diverged between the kernel's flat reconstruction and the stored |
| 4049 | // block — a real bug. Surface it loudly with a per-peer diagnostic so |
| 4050 | // the divergence is debuggable, then fail. |
| 4051 | if rec_ids.len() != flat.len() { |
| 4052 | return Err(TcError::Other(format!( |
| 4053 | "populate_recursor_rules_from_block: rec_ids/flat count mismatch: rec_ids={} flat={}", |
| 4054 | rec_ids.len(), |
| 4055 | flat.len() |
| 4056 | ))); |
| 4057 | } |
| 4058 | |
| 4059 | let mut peers: Vec<KId<M>> = Vec::with_capacity(flat.len()); |
| 4060 | for (gi, gen_rec) in generated_snapshot.iter().enumerate() { |
| 4061 | let target_addr = &gen_rec.ind_addr; |
| 4062 | let rid = &rec_ids[gi]; |
| 4063 | let (params, motives, minors, indices, ty) = match self.get_const(rid)? { |
| 4064 | KConst::Recr { params, motives, minors, indices, ty, .. } => { |
| 4065 | (params, motives, minors, indices, ty.clone()) |
| 4066 | }, |
| 4067 | _ => { |
| 4068 | return Err(TcError::Other(format!( |
| 4069 | "populate_recursor_rules_from_block: rec_ids[{gi}]={rid} is not a recursor" |
no test coverage detected