Function build_perm_ctx_1b

crates/ffi/src/lean_env.rs:1165–1347

Build per-block PermCtx for the permutation-aware comparator. Mirrors `build_perm_ctx` in `rs_compile_validate_aux` below; kept as a local fn here so the `#[cfg(feature = "test-ffi")]` path doesn't escape its scope.

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

/// `LeanBorrowed` accessors are refcount-silent, and each element's
/// owned handle keeps its Lean objects alive for the `Env`'s lifetime
/// regardless of what the Lean side does after the FFI call.
pub fn decode_env_lazy(
  list: LeanList<LeanBorrowed<'_>>,
  cache_entries: usize,
) -> Env {
  let shared_list = LeanShared::new(list.inner().to_owned_ref());
  let objs = collect_list_shared(shared_list.borrow().as_list());
  let global = Arc::new(GlobalCache::with_capacity(objs.len() * 3));

  // Name index (parallel; bodies untouched). Each element is a
  // `Prod (Name × ConstantInfo)` ctor — field 0 is the name.
  let named: Vec<(Name, LeanShared)> = objs
    .into_par_iter()
    .map(|o| {
      let name = decode_name(o.borrow().as_ctor().get(0), &global);
      (name, o)
    })
    .collect();
  let names: Vec<Name> = named.iter().map(|(n, _)| n.clone()).collect();
  let handles: FxHashMap<Name, LeanShared> = named.into_iter().collect();

  let fetch = move |name: &Name| {
    let obj = handles.get(name)?;
    let mut cache = Cache::new(&global);
    Some(decode_constant_info(obj.borrow().as_ctor().get(1), &mut cache))
  };
  Env::new_lazy(names, Box::new(fetch), cache_entries)
}

// Decode a Lean environment in parallel with hybrid caching.
pub fn decode_env(list: LeanList<LeanBorrowed<'_>>) -> Env {
  // Phase 1: Mark entire list graph as MT, then collect elements as LeanShared.
  // lean_mark_mt recursively marks all reachable objects. Subsequent
  // LeanShared::new calls on elements are a fast no-op (single is_st check).
  let shared_list = LeanShared::new(list.inner().to_owned_ref());
  let objs = collect_list_shared(shared_list.borrow().as_list());

  if objs.len() < PARALLEL_THRESHOLD {
    // Sequential fallback for small environments — no MT overhead needed,
    // but objects are already marked. Just borrow directly.
    let global = GlobalCache::new();
    let mut env = Env::default();
    for o in &objs {
      let (name, constant_info) =
        decode_name_constant_info(o.borrow(), &global);
      env.insert(name, constant_info);
    }
    return env;
  }

  // Estimate: ~3 unique names per constant on average
  let global = GlobalCache::with_capacity(objs.len() * 3);

  // Phase 2: Decode in parallel with shared global name cache
  let pairs: Vec<(Name, ConstantInfo)> = objs
    .into_par_iter()
    .map(|shared| decode_name_constant_info(shared.borrow(), &global))
    .collect();