Function rs_kernel_check_anon

crates/ffi/src/kernel.rs:1516–1624

(
  env_path: LeanString<LeanBorrowed<'_>>,
  quiet: LeanBool<LeanBorrowed<'_>>,
  fail_out: LeanString<LeanBorrowed<'_>>,
)

          for &result_idx in &result_idxs {
            // Each result slot is written exactly once across the
            // entire run. `build_anon_work` assigns disjoint
            // `result_idxs` per work item; if this assertion fires,
            // that invariant has been broken (likely by a future
            // dedup refactor) and we'd silently drop the second
            // write rather than expose the bug.
            if results[result_idx].set(result.clone()).is_err() {
              debug_assert!(
                false,
                "anon work-item dedup invariant: result slot {result_idx} set twice"
              );
            }
            if let (Some(log), Err((_, msg))) =
              (failure_log_worker.as_ref(), result.as_ref())
            {
              let label = format!("#{}", addrs[result_idx].hex());
              log.record(&label, msg);
            }
          }
          checks_since_clear += 1;
        }
      }) {
      Ok(h) => h,
      Err(e) => {
        progress.stop_reporter();
        if let Some(r) = reporter.take() {
          let _ = r.join();
        }
        for h in handles {
          let _ = h.join();
        }
        return Err(format!("spawn anon worker: {e}"));
      },
    };
    handles.push(handle);
  }

  let mut panicked = false;
  for h in handles {
    if h.join().is_err() {
      panicked = true;
    }
  }
  progress.stop_reporter();
  if let Some(r) = reporter {
    let _ = r.join();
  }
  progress.log_mem_summary();
  if panicked {
    return Err("anon worker panicked".to_string());
  }

  if let Some(path) = &per_const_out {
    let rows = per_const_rows
      .lock()
      .map_err(|e| format!("per-const entries poisoned: {e}"))?;
    let mut out = String::with_capacity(rows.len() * 96 + 96);
    out.push_str(