(total: usize, worker_count: usize, quiet: bool)
| 2520 | balance, |
| 2521 | parallelism, |
| 2522 | out_opt, |
| 2523 | ) { |
| 2524 | Ok(report) => { |
| 2525 | eprintln!("[rs_shard]\n{report}"); |
| 2526 | LeanIOResult::ok(LeanOwned::box_usize(0)) |
| 2527 | }, |
| 2528 | Err(e) => LeanIOResult::error_string(&format!("rs_shard_esp: {e}")), |
| 2529 | } |
| 2530 | } |
| 2531 | |
| 2532 | /// Total system RAM in GiB from `/proc/meminfo` (Linux); `None` if unreadable. |
| 2533 | fn system_ram_gib() -> Option<f64> { |
| 2534 | let s = std::fs::read_to_string("/proc/meminfo").ok()?; |
| 2535 | let rest = s.lines().find_map(|l| l.strip_prefix("MemTotal:"))?; |
| 2536 | let kib: f64 = rest.trim().trim_end_matches("kB").trim().parse().ok()?; |
| 2537 | Some(kib / 1024.0 / 1024.0) // KiB → GiB |
| 2538 | } |
| 2539 | |
| 2540 | /// FFI: partition a `.ixprof` to a per-shard cycle/RAM budget and write a |
| 2541 | /// `.ixes` manifest. `max_cycles` is a guest-STEP cap; if `ram_gb` > 0 it is |
| 2542 | /// converted via the measured prover RAM model and overrides `max_cycles`. Pass |
| 2543 | /// "0" for both to default the budget to detected system RAM. |
| 2544 | #[allow(clippy::cast_precision_loss)] |
| 2545 | #[unsafe(no_mangle)] |
| 2546 | pub extern "C" fn rs_shard_esp_cap( |
| 2547 | esp_path: LeanString<LeanBorrowed<'_>>, |
| 2548 | max_cycles: LeanString<LeanBorrowed<'_>>, |
| 2549 | ram_gb: LeanString<LeanBorrowed<'_>>, |
| 2550 | balance_pct: LeanString<LeanBorrowed<'_>>, |
nothing calls this directly
no test coverage detected