Check that decompiled environment matches the original. Counts and logs hash mismatches (which indicate metadata loss or decompilation errors).
( original: &LeanEnv, _stt: &CompileState, dstt: &DecompileState, )
| 4533 | _ => continue, |
| 4534 | }, |
| 4535 | }; |
| 4536 | if let Some(aux_def) = generate_rec_on(ro_name, &rec_val) { |
| 4537 | // Same safety propagation rule as `.casesOn`: if `.rec` is unsafe, |
| 4538 | // `.recOn` (which just reorders the rec's arguments) must be too. |
| 4539 | let safety = if rec_val.is_unsafe { |
| 4540 | DefinitionSafety::Unsafe |
| 4541 | } else { |
| 4542 | DefinitionSafety::Safe |
| 4543 | }; |
| 4544 | let as_defn = LeanConstantInfo::DefnInfo(DefinitionVal { |
| 4545 | cnst: ConstantVal { |
| 4546 | name: aux_def.name.clone(), |
| 4547 | level_params: aux_def.level_params.clone(), |
| 4548 | typ: aux_def.typ.clone(), |
| 4549 | }, |
| 4550 | value: aux_def.value.clone(), |
| 4551 | hints: ReducibilityHints::Abbrev, |
| 4552 | safety, |
| 4553 | all: vec![aux_def.name.clone()], |
| 4554 | }); |
| 4555 | generated_consts.insert(aux_def.name.clone(), as_defn); |
| 4556 | |
| 4557 | let mc = LeanMutConst::Defn(Def { |
| 4558 | name: aux_def.name.clone(), |
| 4559 | level_params: aux_def.level_params.clone(), |
| 4560 | typ: aux_def.typ.clone(), |
| 4561 | kind: DefKind::Definition, |
| 4562 | value: aux_def.value.clone(), |
| 4563 | hints: ReducibilityHints::Abbrev, |
| 4564 | safety, |
| 4565 | // Lean emits `.casesOn` / `.recOn` as standalone `defnDecl`s |
| 4566 | // (`refs/lean4/src/Lean/Elab/Inductive.lean:mkCasesOn` et al.), |
| 4567 | // each with `all = [self]`. `Named.original.0` captured that |
| 4568 | // exact shape; regenerating with `all = []` here makes the |
| 4569 | // Phase-A block hash match but leaves the Lean-level `all` |
| 4570 | // blank, so Phase B's `ConstantInfo::get_hash()` diverges |
| 4571 | // (type + value match but `all` differs). See |
| 4572 | // `docs/ix_canonicity.md` §9.2. |
| 4573 | all: vec![aux_def.name.clone()], |
| 4574 | }); |
| 4575 | match roundtrip_block(&[mc], &generated_consts, orig_env, stt, dstt) { |
| 4576 | Ok(roundtripped) if !roundtripped.is_empty() => { |
| 4577 | for (n, ci) in roundtripped { |
| 4578 | dstt.insert_interned(n, ci); |
| 4579 | } |
| 4580 | }, |
| 4581 | Ok(_) => { |
| 4582 | // Empty roundtrip result: prefer the source-faithful original |
| 4583 | // pair; fall back to the regenerated form otherwise. |
| 4584 | if !recover_aux_from_original(&aux_def.name, stt, dstt) |
| 4585 | && let Some(ci) = generated_consts.get(&aux_def.name) |
| 4586 | { |
| 4587 | dstt.insert_interned(aux_def.name.clone(), ci.clone()); |
| 4588 | } |
| 4589 | }, |
| 4590 | Err(e) => { |
| 4591 | // Recovery keeps the Lean-facing env populated for diagnosis, |
| 4592 | // but the failure is always recorded — post-preseed, the |