Function build_perm_ctx

crates/ffi/src/lean_env.rs:1920–2145

Build a `PermCtx` for the block: the congruence comparator uses it to walk gen vs orig in lockstep with permutation awareness. See `ix_compile::congruence::perm` for details. `n_primary = all.len()` because Phase 2 uses singleton classes (one class per original, no alpha-collapse at the primary level).

(
      all: &[Name],
      env: &Env,
      stt: &ix_compile::compile::CompileState,
      perm: &[usize],
    )

          .downcast_ref::<String>()
          .map(|s| s.as_str())
          .or_else(|| panic.downcast_ref::<&str>().copied())
          .unwrap_or("(non-string panic)");
        p1.record_fail(format!("compile_env PANICKED: {msg}"));
        p1.report();
        println!(
          "{VALIDATE_PREFIX} RESULT: {} total failures (aborted after Phase 1)",
          p1.fail
        );
        return p1.fail;
      },
    };
  println!("{VALIDATE_PREFIX} compiled in {:.2}s", t0.elapsed().as_secs_f32());

  // Parallel scan of all 707k+ constants against `stt`. Each check is an
  // independent pair of DashMap lookups (`ungrounded.contains_key` +
  // `resolve_addr`), so `env.par_iter()` over the FxHashMap is safe and
  // dramatically faster than a serial walk on Mathlib-scale inputs.
  {
    use std::sync::Mutex;
    use std::sync::atomic::{AtomicUsize, Ordering};

    let passes = AtomicUsize::new(0);
    let fails = AtomicUsize::new(0);
    let fail_msgs: Mutex<Vec<String>> = Mutex::new(Vec::new());

    let env_names: Vec<&Name> = env.keys().collect();
    env_names.par_iter().for_each(|&name| {
      if stt.ungrounded.contains_key(name) {
        return;
      }
      if stt.resolve_addr(name).is_some() {
        passes.fetch_add(1, Ordering::Relaxed);
      } else {
        fails.fetch_add(1, Ordering::Relaxed);
        let mut msgs = fail_msgs.lock().unwrap();
        if msgs.len() < 20 {
          msgs.push(format!("{}: not compiled", name.pretty()));
        }
      }
    });

    p1.pass = passes.load(Ordering::Relaxed);
    p1.fail = fails.load(Ordering::Relaxed);
    p1.failures = fail_msgs.into_inner().unwrap();
  }
  p1.report();

  // ══════════════════════════════════════════════════════════════════════
  // Phase 2: Aux_gen congruence (post-compilation, uses real CompileState)
  // ══════════════════════════════════════════════════════════════════════
  //
  // Structure: three passes.
  //   1. Serial — collect unique blocks (dedup by sorted `.all` names) and
  //      build `MutConst` values eagerly. Can't parallelize: the env iter
  //      is serial and the dedup set needs cross-iteration visibility.
  //   2. Serial — pre-ingress each block's transitive ctor-field deps into
  //      the shared `p2_kctx`. Serial because the visited set
  //      (`p2_ingressed`) is shared across blocks, and we want each name