H1: Compute `is_rec` constructively by scanning constructor fields for references to any inductive in the mutual block. This verifies the declared `is_rec` flag rather than trusting it from Ixon input. An inductive is recursive if any constructor field (after parameters) mentions any inductive in the mutual block.
(
&mut self,
ctors: &[KId<M>],
n_params: usize,
block_addrs: &[Address],
)
| 447 | // A4: Universe constraints |
| 448 | self.check_field_universes(&ctor_ty, ind_params, &ind_level)?; |
| 449 | |
| 450 | // A2: Constructor return type |
| 451 | self.check_ctor_return_type( |
| 452 | &ctor_ty, |
| 453 | ind_params, |
| 454 | u64_to_usize(indices)?, |
| 455 | ctor_fields, |
| 456 | &id.addr, |
| 457 | lvls, |
| 458 | &block_addrs, |
| 459 | )?; |
| 460 | } |
| 461 | |
| 462 | // Trigger recursor generation for the block (fatal — ZK context cannot tolerate silent failure) |
| 463 | if !self.env.recursor_cache.contains_key(&block) { |
| 464 | self.generate_block_recursors(&block)?; |
| 465 | } |
| 466 | |
| 467 | Ok(()) |
| 468 | } |
| 469 | |
| 470 | /// Validate a standalone constructor by checking its parent inductive block. |
| 471 | pub fn check_ctor_against_inductive( |
| 472 | &mut self, |
| 473 | ctor_id: &KId<M>, |
| 474 | induct_id: &KId<M>, |
| 475 | ) -> Result<(), TcError<M>> { |
| 476 | let block = match self.try_get_const(induct_id)? { |
| 477 | Some(KConst::Indc { block, .. }) => block.clone(), |
| 478 | _ => { |
| 479 | return self.check_ctor_against_inductive_member(ctor_id, induct_id); |
| 480 | }, |
| 481 | }; |
| 482 | let Some(members) = self.try_get_block(&block)? else { |
| 483 | return self.check_ctor_against_inductive_member(ctor_id, induct_id); |
| 484 | }; |
| 485 | for member in &members { |
| 486 | if !matches!( |
| 487 | self.try_get_const(member)?, |
no test coverage detected