Function resolve_lean_name_addr

crates/kernel/src/ingress.rs:2151–2167

Resolve a Lean Name to an Address, using real Ixon address if available. Checks `name_to_ixon_addr` first (real compiled address), falls back to `Address::from_blake3_hash(*name.get_hash())` for constants not yet compiled.

(
  name: &Name,
  name_to_ixon_addr: Option<&DashMap<Name, Address>>,
  aux_n2a: Option<&DashMap<Name, Address>>,
)

  name_to_addr: &FxHashMap<Name, Address>,
  intern: &mut InternTable<M>,
  stats: &mut ConvertStats,
) -> Result<Vec<(KId<M>, KConst<M>)>, String> {
  let block_id: KId<M> =
    KId::new(entry_addr.clone(), M::meta_field(entry_name.clone()));

  let block_constant = ixon_env.get_const(entry_addr).ok_or_else(|| {
    format!("missing Muts block constant {}", entry_addr.hex())
  })?;
  let members = match &block_constant.info {
    IxonCI::Muts(m) => m,
    _ => return Err(format!("constant at {} is not Muts", entry_addr.hex())),
  };

  let mut results: Vec<(KId<M>, KConst<M>)> = Vec::new();

  for (i, member) in members.iter().enumerate() {
    // `all[i][0]` is the name-hash address of this member's canonical Lean
    // name; we read the per-member metadata (arena, type_root, etc.) from
    // that Named entry. Note the address distinction: `primary_name_addr`
    // is a *name-content* hash (Blake3 of the Lean name components),