Function rs_kernel_roundtrip

crates/ffi/src/kernel.rs:3063–3172

(
  env_consts: LeanList<LeanBorrowed<'_>>,
)

  kenv: &mut KEnv<M>,
  mut before_kernel_check: F,
) -> CheckOutcome
where
  F: FnMut(&str),
  M::MField<Vec<Name>>: CheckDupLevelParams,
{
  let name = &names[i];
  let should_pass = expect_pass.get(i).copied().unwrap_or(true);
  // In anon mode, surface the content address in the per-constant log
  // line — the kernel itself doesn't see names. We still accept names
  // as input (and resolve them via `ixon_env.named` at the FFI
  // scheduling layer), so the user's identifier is preserved in the
  // CLI surface; only the kernel-visible progress label switches to a
  // hash. Falls back to the name if the address lookup fails.
  let display = if M::HAS_META {
    name.pretty()
  } else {
    match ixon_env.lookup_name(name) {
      Some(named) => format!("#{}", named.addr.hex()),
      None => name.pretty(),
    }
  };

  if let Some(msg) = ungrounded.get(name) {
    return CheckOutcome {
      progress_index,
      progress_total,
      display,
      should_pass,
      result: Err((ErrKind::Compile, msg.clone())),
      status: CheckStatus::CompileFailed,
      elapsed: None,
      peak: None,
    };
  }

  let prefix =
    format!("  [{}/{}] {display}", progress_index + 1, progress_total);
  before_kernel_check(&prefix);

  let tc_start = Instant::now();
  let kid = match ingress_const_shallow_into_kenv_with_lookups(
    kenv, ixon_env, lookups, name,
  ) {
    Ok(kid) => kid,
    Err(msg) => {
      let elapsed = tc_start.elapsed();
      let status = if msg.contains("missing Named entry") {
        CheckStatus::NotFound
      } else {
        CheckStatus::Checked
      };
      return CheckOutcome {
        progress_index,
        progress_total,
        display,
        should_pass,
        result: Err((ErrKind::Kernel, msg)),
        status,