(
&mut self,
ind_block_id: &KId<M>,
rec_block_id: &KId<M>,
generated_snapshot: &[GeneratedRecursor<M>],
flat: &[FlatBlockMember<M>],
rec_ids: &[KId<M>],
prefix_base: u64,
| 1519 | let mut marker_ty = self |
| 1520 | .intern(KExpr::cnst(member.id.clone(), member.occurrence_us.clone())); |
| 1521 | for sp in member.spec_params.iter() { |
| 1522 | marker_ty = self.intern(KExpr::app(marker_ty, sp.clone())); |
| 1523 | } |
| 1524 | let mut mh = blake3::Hasher::new(); |
| 1525 | mh.update(b"AUX_MARKER_VIEW"); |
| 1526 | mh.update(aux_addr.as_bytes()); |
| 1527 | let marker_addr = Address::from_blake3_hash(mh.finalize()); |
| 1528 | let marker_kid = |
| 1529 | KId::new(marker_addr.clone(), M::meta_field(Name::anon())); |
| 1530 | let marker_ctor = KConst::Ctor { |
| 1531 | name: M::meta_field(Name::anon()), |
| 1532 | level_params: M::meta_field(vec![]), |
| 1533 | is_unsafe: false, |
| 1534 | lvls: block_us.len() as u64, |
| 1535 | induct: aux_id.clone(), |
| 1536 | cidx: aux_ctor_kids.len() as u64, |
| 1537 | params: n_block_params, |
| 1538 | fields: 0, |
| 1539 | ty: marker_ty, |
| 1540 | }; |
| 1541 | all_ctor_lookup.insert(marker_addr, marker_ctor); |
| 1542 | aux_ctor_kids.push(marker_kid); |
| 1543 | } |
| 1544 | |
| 1545 | let aux_indc = KConst::Indc { |
| 1546 | name: M::meta_field(seed_name), |
| 1547 | level_params: M::meta_field(vec![]), |
| 1548 | lvls: block_us.len() as u64, |
| 1549 | params: n_block_params, |
| 1550 | indices: ext_n_indices, |
| 1551 | is_unsafe: false, |
| 1552 | block: KId::new( |
| 1553 | Address::hash(b"synthetic-aux-block"), |
| 1554 | M::meta_field(Name::anon()), |
| 1555 | ), |
| 1556 | member_idx: 0, |
| 1557 | ty: typ, |
| 1558 | ctors: aux_ctor_kids, |
| 1559 | lean_all: M::meta_field(vec![]), |
| 1560 | }; |
| 1561 | |
| 1562 | aux_indcs.push((aux_id, aux_indc)); |
| 1563 | } |
| 1564 | |
| 1565 | // Build (KId, &KConst) pairs for sorting. |
| 1566 | let pairs: Vec<(KId<M>, &KConst<M>)> = |
| 1567 | aux_indcs.iter().map(|(id, c)| (id.clone(), c)).collect(); |
| 1568 | |
| 1569 | // resolve_ctor: synthetic ctors → synthetic KConst::Ctor. |
| 1570 | let resolve_ctor = |cid: &KId<M>| -> Option<KConst<M>> { |
| 1571 | all_ctor_lookup.get(&cid.addr).cloned() |
| 1572 | }; |
| 1573 | |
| 1574 | // Optional canonical-sort dump for debugging the kernel/compile |
| 1575 | // partition-refinement divergence. Triggered when `IX_RECURSOR_DUMP` |
| 1576 | // matches the block's `all0_name` prefix. Dumps each synthetic aux's |
| 1577 | // pre-sort `(seed_name, addr, typ, ctor.ty)`, then the post-sort |
| 1578 | // class structure. Use to compare against compile-side |
no test coverage detected