ci-floor: memory-aware spawn_width — bound batch-2 fan-out by memory budget, not CPU only

dsl/gunbc/ci_fleet.dag

@@ -24,13 +24,15 @@ import product.compute_fabric {
   Dram,
   WorkDemand,
   ResourceEnvelope,
+  MemoryRequirement,
   IsolationRequirement,
   IndependentShards,
   offer_placement_supply_row,
   placement_spawn_width,
+  placement_floor_memory_budget_bytes,
 }
 import extdeps.cpu.types { CpuFacts, CpuDeploymentFacts }
-import std.measure { byte_size, hertz, hardware_thread_count, HardwareThreadCount }
+import std.measure { byte_size, byte_size_count, hertz, hardware_thread_count, hardware_thread_count_value, HardwareThreadCount }
 import std.os.types {
   OperatingSystemSurface,
   Linux,
@@ -58,7 +60,12 @@ data gunbc_ci_host: ComputeHost = ComputeHost {
   identity: gunbc_ci_host_identity,
   baseboard: none,
   processors: [CpuProcessor { cpu: gunbc_ci_cpu }],
-  memory: [MemoryDevice { capacity: byte_size(274877906944), memory_kind: Dram, bandwidth: none }],
+  // 125 GiB measured on the real fleet host (Ampere Altra Max M128, 1 NUMA node). The prior
+  // 256 GiB was a stub; the memory-aware spawn-width bound (placement_spawn_width) needs a
+  // real RAM figure or it cannot back fan-out off before the cgroup OOM. CPU thread count
+  // (catalog) is still the 64-thread stub — corrected with the ctrl fleet grounding; the
+  // memory bound dominates the floor width regardless, so it is not load-bearing here.
+  memory: [MemoryDevice { capacity: byte_size(134217728000), memory_kind: Dram, bandwidth: none }],
   storage: [],
   network_interfaces: [],
 }
@@ -100,7 +107,13 @@ fn gunbc_ci_floor_corpus_work_demand(corpus_shard_count: Int) -> WorkDemand {
     resources: ResourceEnvelope {
       cpu: none,
       gpu: none,
-      memory: none,
+      // Per-shard peak resolve memory. Grounded in the deterministic floor-OOM evidence
+      // (eager-boar-790, 3 runs of a grown corpus at width=7): srv2's ~87.6 GiB cgroup cap
+      // passes 7 concurrent ~2900-item resolves only by a thin margin (~12.5 GiB/unit), and
+      // srv1's ~65.6 GiB cap OOM-kills (exit 137). 14 GiB/unit carries headroom for corpus
+      // growth; the memory-aware width then floors batch-2 below the OOM ceiling on both
+      // hosts. Grounds-tighter when a peak-RSS probe per resolve lands.
+      memory: Present { value: MemoryRequirement { min_bytes: byte_size(15032385536) } },
       storage: none,
       network: none,
     },
@@ -117,13 +130,34 @@ fn gunbc_ci_floor_placement_supply() -> PlacementSupplyRow? {
   offer_placement_supply_row(offer: gunbc_ci_fleet_offer)
 }
 
-// Host spawn-width = min(caller's corpus breadth, this fleet's hardware threads).
-// No hand-tuned width: add a gate to the spec → breadth re-derives; change the host →
-// supply re-derives; spawn_width follows from both with zero edits here.
+// Host spawn-width = min(corpus breadth, hardware threads, memory_budget / per-shard peak).
+// No hand-tuned width: add a gate to the spec → breadth re-derives; change the host → supply
+// re-derives; raise the per-shard memory → the memory bound re-derives; spawn_width follows
+// from all three via placement_spawn_width with zero edits here. The memory term is what
+// keeps batch-2 from OOM-killing as the corpus grows (the CPU-only bound was memory-blind).
 fn ci_fleet_floor_spawn_width(corpus_shard_count: Int) -> HardwareThreadCount {
   match gunbc_ci_floor_placement_supply() {
     Absent => hardware_thread_count(1)
     Present { value: row } =>
       placement_spawn_width(supply: row, demand: gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count))
   }
 }
+
+// §5 OOM oracle: the chosen floor width times the per-shard peak memory must fit the
+// conservative memory budget — i.e. batch-2's concurrent memory peak stays under the cgroup
+// MemoryMax. Discriminating: a memory-blind width (= min(breadth, threads), ignoring the
+// memory term) would exceed the budget and flip this false. Absent supply / Absent memory
+// demand are vacuously safe (no concurrent memory pressure to bound).
+fn ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: Int) -> Bool {
+  match gunbc_ci_floor_placement_supply() {
+    Absent => true
+    Present { value: row } =>
+      match gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count).resources.memory {
+        Absent => true
+        Present { value: req } => {
+          let width = hardware_thread_count_value(t: ci_fleet_floor_spawn_width(corpus_shard_count: corpus_shard_count))
+          width * byte_size_count(req.min_bytes) <= placement_floor_memory_budget_bytes(supply: row)
+        }
+      }
+  }
+}

dsl/product/compute_fabric.dag

@@ -80,7 +80,7 @@ import extdeps.toolchain.types {
 }
 import product.placement_supply { HostIdentity, PlacementSupplyRow }
 import std.baseboard { ServerBaseboard }
-import std.realization_width { bounded_host_spawn_width }
+import std.realization_width { bounded_host_spawn_width, int_min }
 
 // 🟡 forward — v2.std.witness / v2.std.diagnostic at harness (P-CF-WITNESS).
 // Kept intentionally distinct from the kernel `Witness<T>` container.
@@ -505,14 +505,53 @@ fn work_demand_shard_count(demand: WorkDemand) -> Int {
   }
 }
 
-// Width projection: min(shard_count, PlacementSupplyRow.hardware_threads) — single authority.
-// Eligibility is NOT rejected when demand exceeds supply — the peripheral host fold caps
-// fan-out; satisfies records DemandParallelism as proven when IndependentShards is present.
+// Conservative memory budget for concurrent fan-out on a host. A floor batch is killed by
+// its runner-slice cgroup MemoryMax (NOT total RAM), which on the tightest fleet host caps
+// near half of RAM. Until ctrl/BMC grounds the exact per-host MemoryMax bytes, approximate
+// the budget as 0.50×RAM so a single fleet-wide spawn width stays safe on the TIGHTEST host
+// (the floor lands on either host). Grounds-later: replace 0.50×RAM with measured MemoryMax.
+fn placement_floor_memory_budget_bytes(supply: PlacementSupplyRow) -> Int {
+  byte_size_count(supply.ram_bytes) / 2
+}
+
+// Memory width BOUND: how many concurrent units fit under the memory budget, each peaking at
+// the demand's per-unit memory requirement. `none` = no memory bound (Absent demand, or a
+// degenerate non-positive per-unit guarded against divide-by-zero). A budget under one unit
+// still admits 1 (fail-closed forward progress, never 0 width). Returned as `Int?` so the
+// "no bound" case never has to unify with the Int division result.
+fn placement_memory_width_bound(supply: PlacementSupplyRow, demand: WorkDemand) -> Int? {
+  match demand.resources.memory {
+    Absent => none
+    Present { value: req } => {
+      let per_unit = byte_size_count(req.min_bytes)
+      if per_unit <= 0 { none } else {
+        let fits = placement_floor_memory_budget_bytes(supply: supply) / per_unit
+        Present { value: if fits < 1 { 1 } else { fits } }
+      }
+    }
+  }
+}
+
+// Width projection: min(shard_count, hardware_threads, memory_budget / per_unit_peak) —
+// single authority, MEMORY-AWARE. The CPU bound (bounded_host_spawn_width) alone is
+// memory-blind: N concurrent resolves each peak at the demand's per-unit memory, and N×peak
+// must stay under the floor's cgroup MemoryMax or the batch is OOM-killed (exit 137). The
+// memory term backs fan-out off BEFORE the kill — §1's safety axis made structural, and the
+// connected model §6 ('fix related systems together') requires: CPU and memory are ONE width
+// relationship, not a CPU bound patched after an OOM. Eligibility is NOT rejected when demand
+// exceeds supply — the peripheral host fold caps fan-out; satisfies records DemandParallelism
+// as proven when IndependentShards is present.
 fn placement_spawn_width(supply: PlacementSupplyRow, demand: WorkDemand) -> HardwareThreadCount {
-  bounded_host_spawn_width(
-    shard_count: work_demand_shard_count(demand: demand),
-    hardware_threads: supply.hardware_threads
+  let cpu_width = hardware_thread_count_value(
+    t: bounded_host_spawn_width(
+      shard_count: work_demand_shard_count(demand: demand),
+      hardware_threads: supply.hardware_threads
+    )
   )
+  match placement_memory_width_bound(supply: supply, demand: demand) {
+    Absent => hardware_thread_count(count: cpu_width)
+    Present { value: mem_width } => hardware_thread_count(count: int_min(a: cpu_width, b: mem_width))
+  }
 }
 
 // --- §1.2 demand -------------------------------------------------------------

src/v2/test/claim/ci_floor_plan_witness_test.dag

@@ -15,7 +15,8 @@ import std.realization {
 }
 import v2.workflow.ci_floor_plan {
   gunbc_ci_floor_batches, corpus_runnable,
-  gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width
+  gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width,
+  gunbc_ci_floor_spawn_fits_memory_budget
 }
 import std.measure { hardware_thread_count_value }
 import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots }
@@ -102,11 +103,12 @@ fn witness_corpus_skip_node_frontier_enabled() -> Bool {
   }
 }
 
-// Connected relationship: spawn_width is DERIVED from the floor breadth, not tuned.
-// When breadth <= hardware threads (true on the real fleet), spawn_width == breadth —
-// so the host runs the independent layer concurrently, not one-at-a-time.
-fn witness_spawn_width_tracks_breadth() -> Bool {
-  hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) == gunbc_ci_floor_breadth()
+// Connected relationship: spawn_width is DERIVED (min of breadth, hardware threads, and the
+// memory budget / per-shard peak), never a tuned constant. It is positive and never exceeds
+// the work breadth — fanning out more workers than shards would be wasted concurrency.
+fn witness_spawn_width_bounded_by_breadth() -> Bool {
+  let width = hardware_thread_count_value(t: gunbc_ci_floor_spawn_width())
+  (width >= 1) && (width <= gunbc_ci_floor_breadth())
 }
 
 // Discriminating: the floor is NOT serial. A revert to a constant shard_count (=1) or a
@@ -116,6 +118,22 @@ fn witness_floor_not_serial() -> Bool {
     (hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) > 1)
 }
 
+// Connected memory relationship (the §5 OOM oracle): the scheduled width's concurrent memory
+// peak fits the fleet memory budget. DISCRIMINATING against the memory-blind regression — if
+// placement_spawn_width dropped its memory term, width would jump to min(breadth, threads)=7
+// and 7×(per-shard peak) would blow the budget, flipping this RED. This is the witness that
+// would have caught the deterministic floor-OOM (exit 137) at model time, not on the fleet.
+fn witness_floor_width_fits_memory_budget() -> Bool {
+  gunbc_ci_floor_spawn_fits_memory_budget()
+}
+
+// Discriminating: the memory term is ACTIVE — on the real fleet the per-shard peak caps the
+// width strictly below the CPU/breadth bound (mem budget admits fewer than `breadth` units).
+// A memory-blind width would equal breadth, flipping this RED.
+fn witness_floor_width_memory_bounded() -> Bool {
+  hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) < gunbc_ci_floor_breadth()
+}
+
 test fn ci_floor_plan_witnesses() -> Bool {
   witness_two_readiness_layers() &&
     witness_compile_root_runs_first() &&
@@ -125,6 +143,8 @@ test fn ci_floor_plan_witnesses() -> Bool {
     witness_scan_dirs_match_layer_authority() &&
     witness_corpus_has_no_explicit_entries() &&
     witness_corpus_skip_node_frontier_enabled() &&
-    witness_spawn_width_tracks_breadth() &&
-    witness_floor_not_serial()
+    witness_spawn_width_bounded_by_breadth() &&
+    witness_floor_not_serial() &&
+    witness_floor_width_fits_memory_budget() &&
+    witness_floor_width_memory_bounded()
 }

src/v2/workflow/ci_floor_plan.dag

@@ -37,7 +37,7 @@ import v2.std.collection { List }
 import v2.std.dependency { DataDependsOn, DependencyView }
 import v2.std.node { Atom, Node, TypeNode }
 import v2.std.text { String }
-import gunbc.ci_fleet { ci_fleet_floor_spawn_width }
+import gunbc.ci_fleet { ci_fleet_floor_spawn_width, ci_fleet_floor_spawn_fits_memory_budget }
 import std.types { ContentHash }
 import std.measure { HardwareThreadCount }
 import std.realization_width { width_fold_objective_goals }
@@ -222,8 +222,16 @@ fn gunbc_ci_floor_breadth() -> Int {
   length(xs: gunbc_ci_spec.gates)
 }
 
-// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads).
-// The relationship is the model; nothing here is hand-tuned per host or per gate.
+// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads, memory
+// budget / per-shard peak). The relationship is the model; nothing here is hand-tuned per
+// host or per gate — the memory term backs fan-out off before the cgroup OOM-kill.
 fn gunbc_ci_floor_spawn_width() -> HardwareThreadCount {
   ci_fleet_floor_spawn_width(corpus_shard_count: gunbc_ci_floor_breadth())
 }
+
+// §5 OOM oracle at the floor breadth: the scheduled width's concurrent memory peak fits the
+// fleet memory budget. A revert to a memory-blind width (= min(breadth, threads)) flips this
+// false on the real fleet (7×14 GiB > 0.50×125 GiB budget).
+fn gunbc_ci_floor_spawn_fits_memory_budget() -> Bool {
+  ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: gunbc_ci_floor_breadth())
+}