Function build_lean_io_buffer

crates/ffi/src/aiur/protocol.rs:683–711

Build a Lean `Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)` from an `IOBuffer`. The first array enumerates per-channel data arenas; the second is the channel-keyed info map.

(io_buffer: &IOBuffer)

/// pure ratio calibrated on large shards under-reserves small ones
/// (measured: 151 ISLB shards at 1.1-4.8 GiB estimated ran to 175 GB
/// actual against a 110 GiB budget — an OOM on a real 128 GB box).
/// Fit on the two ISLB partitions (2026-08-22, measured in-flight
/// RSS): 5.7 MB owned -> ~9.6 GB and 1.4 MB -> ~5.5 GB, giving
/// ~4 GiB + ~1000x; both terms rounded up for cross-shard spread.
const EXEC_RSS_FIXED_BYTES: usize = 9 * (1 << 29); // 4.5 GiB
// Two calibrations, each accurate in its own regime, combined as a MAX
// in `exec_rss_estimate` because the per-owned-byte execution footprint
// is env-dependent and the gate's contract is NEVER OOM:
// - The affine fit (4.5 GiB + 1100x) measured on ISLB's small shards
//   (1.4-5.7 MB owned; a pure ratio under-reserved them and OOM'd a
//   128 GB box).
// - The pure ratio (2500x, ~2300x measured + margin) validated on
//   Mathlib's full-width 233-shard batch at +2% of estimate; the
//   affine slope alone under-reserved Mathlib-class shards and
//   over-admitted a 132-shard full-width batch to 486/495 GB
//   (OOM, 2026-08-29 — the first Mathlib full-width run under the
//   affine constant).
// The max reproduces each fit where it was measured: small shards take
// the affine branch (ISLB bench reservations unchanged), large shards
// the ratio branch.
const EXEC_RSS_PER_OWNED_BYTE: usize = 1100;
const EXEC_RSS_RATIO_PER_OWNED_BYTE: usize = 2500;

/// Per-shard execution-RSS reserve: the max of the two measured fits
/// (see the constants above).
fn exec_rss_estimate(owned_bytes: usize) -> usize {
  EXEC_RSS_FIXED_BYTES
    .saturating_add(owned_bytes.saturating_mul(EXEC_RSS_PER_OWNED_BYTE))
    .max(owned_bytes.saturating_mul(EXEC_RSS_RATIO_PER_OWNED_BYTE))
}

/// FFI: the detected prover/execution RAM budget in bytes