§1-C: memory-aware CI floor spawn_width — derived from measured VmHWM peak + live budget (not pinned 4)

dsl/gunbc/ci_floor_measurement.dag

@@ -0,0 +1,67 @@
+// gunbc/ci_floor_measurement.dag — the CI floor's MEASURED per-shard memory peak (§1-C).
+//
+// This is the committed half of the §1 measurement→plan loop (realization-measurement-loop.md
+// Phase 0/1). The spawn-width derivation (src/v2/workflow/ci_floor_plan.dag) divides the LIVE
+// host memory budget by the per-shard peak recorded HERE. Per DESIGN §3 (measured⇒peripheral):
+//   - the per-shard peak is OUR measurement → we COMMIT it, provenance-stamped (this file);
+//   - the cgroup budget is authored by an EXTERNAL system (the host/scheduler) → the host
+//     realizer READS it live (claim_executor), never committed.
+// This file is the peripheral measured realization; the v2 plan stays pure topology.
+//
+// NOT a hand-grounded literal: the number below is claim_executor's MEASURED VmHWM emit
+// ("[measurement] floor peak RSS: <bytes> (VmHWM) at spawn_width=N", added in #5431). It
+// replaces — does not re-add — the ~14GB hand-grounded literal #5419 deleted as unwired.
+//
+// ── PROVENANCE (re-stamp on every re-measure) ────────────────────────────────
+//   source emit : "[measurement] floor peak RSS: 8400113664 bytes (VmHWM) at spawn_width=4"
+//   run         : GitHub Actions run 27893441091 (#5431 PR CI, job 82540829121)
+//   commit      : cb71163cf2 (the #5431 merge that landed the VmHWM emit)
+//   corpus      : 616 discovery witnesses (0 skipped)
+//   date        : 2026-06-21
+// Each DiscoveryBatch shard does a WHOLE-TREE resolve, so the per-shard peak ≈ the whole-floor
+// VmHWM ÷ the spawn_width it was measured at (the concurrency). It scales with TREE size, not
+// witnesses-per-shard — which is why a larger tree (the old ~2900-row era) peaked far higher.
+//
+// 🟡 SCAFFOLD — feature:measured-peak-drift-gate —
+// consumer: ci_floor_plan.gunbc_ci_floor_spawn_width (via std.realization_width).
+// RESIDUE (DESIGN §6, legit unstructurable-before-execution): the committed peak is stale in
+// exactly ONE dangerous direction — the tree grows un-re-stamped → committed peak too LOW →
+// ⌊budget ÷ peak⌋ too HIGH → OOM. A peak is fundamentally a runtime OUTPUT (you cannot know a
+// run's peak before running it), so a committed-prior-measurement + a drift-check is the legit
+// §6 residue, not a construction wall. The #5431 emit each run is the drift MONITOR but nothing
+// GATES on it yet (observe-by-eyeball = validation, not construction).
+// dissolve-on: a cheap CI gate compares this committed peak against the live emit's VmHWM÷width
+// and fails closed when committed is stale-LOW beyond a margin (re-stamp required). Out of scope
+// for the §1-C width PR; this marker keeps the committed fact from being a silent staleness trap.
+
+module gunbc.ci_floor_measurement
+
+import std.measure { ByteSize, byte_size }
+import std.types { Int }
+import std.realization_measurement {
+  ConcurrentMemoryPeakSample,
+  concurrent_memory_peak_per_share,
+}
+
+// The measured whole-floor concurrent peak (VmHWM) bundled with the concurrency it was sampled
+// at — ONE fact (a ConcurrentMemoryPeakSample), the single authority for the §1-C derivation.
+// Peak and concurrency are only meaningful together (per-share = peak ÷ concurrency), so they
+// live in one carrier rather than as two loose rows that could drift apart. Re-stamp the pair
+// here on every re-measure (provenance above).
+data gunbc_ci_floor_measured_peak: ConcurrentMemoryPeakSample = ConcurrentMemoryPeakSample {
+  peak: byte_size(8400113664)
+  concurrency: 4
+}
+
+// Per-shard peak: each DiscoveryBatch shard does a whole-tree resolve, so the per-shard peak is
+// the measured concurrent peak distributed across its sample concurrency. Delegates to the std
+// measure-algebra derivation (std.realization_measurement) — no inline unwrap/divide/re-ground
+// here; the division is a grounded measure operation, not a one-off expression.
+fn gunbc_ci_floor_per_shard_peak_rss_bytes() -> ByteSize {
+  concurrent_memory_peak_per_share(sample: gunbc_ci_floor_measured_peak)
+}
+
+// Fail-closed fallback width when the host cannot read a live memory budget: the last
+// known-safe MEASURED width (the run above passed at width 4 = 8.40 GB concurrent on the real
+// fleet). A bounded, grounded fallback — never fabricated, never an unbounded memory-blind width.
+data gunbc_ci_floor_conservative_fallback_width: Int = 4

dsl/std/realization.dag

@@ -63,6 +63,15 @@ import std.realization_width {
   witness_width_fold_preserves_schedule_topology,
   witness_budget_ignoring_fold_fails,
   witness_measured_cost_affects_shard_balance,
+  memory_aware_spawn_width,
+  memory_bounded_shard_count,
+  budget_safety_fraction_apply,
+  memory_aware_width_value,
+  witness_memory_term_non_binding_uses_shard_count,
+  witness_tight_budget_backs_off_below_shard_count,
+  witness_unreadable_budget_falls_back_conservative,
+  witness_safety_fraction_is_load_bearing,
+  witness_subunit_budget_admits_one,
 }
 
 // --- Independence classifier (fail-closed) ------------------------------------

dsl/std/realization_measurement.dag

@@ -12,13 +12,15 @@
 
 module std.realization_measurement
 
-import std.types { ContentHash, Bool, String, List }
+import std.types { ContentHash, Bool, String, List, Int }
 import std.nat { Nat, nat_max }
 import std.measure {
   Measure,
   Time,
   time_measure,
   measure_count,
+  ByteSize,
+  byte_size,
 }
 import std.realization_schedule {
   CostAccount,
@@ -55,6 +57,44 @@ fn time_measure_list_total<S>(times: List<Measure<Time, S, Nat>>) -> Measure<Tim
   )
 }
 
+// --- Concurrent memory-peak sample → per-share peak (§1-C) ------------------
+//
+// A whole-system peak resident-memory observation (VmHWM) is only meaningful paired with the
+// concurrency it was sampled at: each concurrent share does a whole-tree pass, so the observed
+// concurrent peak ≈ per-share peak × concurrency. Bundling (peak, concurrency) into ONE carrier
+// keeps the observation and the divisor it derives against as a single fact (§2/§3) — a loose
+// peak with the concurrency stored elsewhere is anemic (the two can drift apart, and neither
+// reads as "a measurement"). This is the agnostic SHAPE; the measured VALUES live peripherally
+// at the consumer (gunbc.ci_floor_measurement, §3 measured⇒peripheral).
+type ConcurrentMemoryPeakSample {
+  peak: ByteSize
+  concurrency: Int
+}
+
+// Per-share peak: distribute the observed concurrent peak across the concurrency it was sampled
+// at, re-grounding the Memory magnitude at the same carrier — the measure-algebra idiom
+// (project via measure_count → magnitude arithmetic → reconstruct via byte_size, exactly as
+// time_measure_seq/_par above project→arithmetic→reconstruct over Time). Fail-closed (§5): a
+// non-positive concurrency is degenerate, so the whole peak stands (a share count of 1) rather
+// than a divide-by-zero or a fabricated share.
+fn concurrent_memory_peak_per_share(sample: ConcurrentMemoryPeakSample) -> ByteSize {
+  if sample.concurrency <= 0 {
+    sample.peak
+  } else {
+    byte_size(count: measure_count(m: sample.peak) / sample.concurrency)
+  }
+}
+
+// Discriminating witness (§5): the per-share peak of an N-way sample is the whole peak ÷ N, and
+// re-grounds at the same Memory carrier — goes red if the derivation drops the concurrency, aliases
+// the whole peak, or loses the magnitude. Degenerate concurrency falls closed to the whole peak.
+fn witness_concurrent_memory_peak_per_share_divides() -> Bool {
+  let sample = ConcurrentMemoryPeakSample { peak: byte_size(8400113664), concurrency: 4 }
+  let degenerate = ConcurrentMemoryPeakSample { peak: byte_size(2100028416), concurrency: 0 }
+  measure_count(m: concurrent_memory_peak_per_share(sample: sample)) == 2100028416
+    && measure_count(m: concurrent_memory_peak_per_share(sample: degenerate)) == 2100028416
+}
+
 // --- Critical-path span roll-up (Phase 1.5b) --------------------------------
 //
 // Authority: v1.compiler.complexity — `span` is critical-path length under DAG

dsl/std/realization_width.dag

@@ -24,9 +24,12 @@ import std.types { Int, List }
 import std.nat { Nat }
 import std.measure {
   HardwareThreadCount,
+  ByteSize,
   Measure,
   Time,
   Nano,
+  byte_size,
+  byte_size_count,
   hardware_thread_count,
   hardware_thread_count_value,
   time_measure,
@@ -77,6 +80,83 @@ fn bounded_host_spawn_width(shard_count: Int, hardware_threads: HardwareThreadCo
   hardware_thread_count(count: width)
 }
 
+// ── memory-aware width (§1-C): the third term — fail-closed against OOM ───────
+// The CPU/topology bound above is memory-BLIND: N concurrent whole-tree-resolve shards
+// each peak at the MEASURED per-shard RSS, and N×peak must stay under the host's cgroup
+// budget or the batch is OOM-killed (exit 137). The memory term backs fan-out off BEFORE
+// the kill — §1's safety axis made structural, CPU and memory ONE width relationship (a
+// CPU bound patched after an OOM is the §6 forked-logic trap). The per-shard peak is sourced
+// from the §1 measurement keystone (claim_executor's VmHWM emit), NOT a hand-grounded literal
+// (the literal #5419 deleted as unwired); the live budget is read by the host realizer and
+// threaded in — §3 measured⇒peripheral: WE author+commit the measurement, an EXTERNAL system
+// (the host/cgroup) authors the budget so the host READS it live.
+
+// Conservative fraction applied to the LIVE budget before dividing by the measured per-shard
+// peak: floor(budget × 4/5) = 0.80×budget. memory.max is the HARD OOM-kill ceiling and the
+// per-shard peak is a division-derived ESTIMATE (whole-floor VmHWM ÷ width) with non-shard
+// overhead around it (parent process, allocator slop, page-cache pressure, the in-shard gunbc
+// compile). 0.80 = a 20% margin: it costs nothing while memory is non-binding (width capped by
+// shard_count today) and is precisely the lean (DESIGN §5) that protects the one failure mode
+// §1-C exists to prevent — OOM — in the future stale-low-peak case. Integer ×4/5 (no floats).
+// Stays in the ByteSize domain (a fractioned budget is still a budget): scale the underlying Nat
+// magnitude and re-ground via byte_size() — the dimension stays attached at the public seam.
+fn budget_safety_fraction_apply(budget: ByteSize) -> ByteSize {
+  byte_size(count: (byte_size_count(b: budget) * 4) / 5)
+}
+
+// Nat→Int projection of a ByteSize count. The byte magnitude is a Nat (byte_size_count), but the
+// fold's shard-count arithmetic and the host's 0-byte sentinel live in Int (cf.
+// bounded_host_spawn_width's int_min over hardware_thread_count_value). Nat ⊂ Int, so this is the
+// widening at a typed boundary — the public ByteSize fields stay the canonical carrier, the inner
+// dimensionless shard-count plumbing is Int.
+fn byte_size_count_int(b: ByteSize) -> Int {
+  byte_size_count(b: b)
+}
+
+// How many concurrent shards fit under the safety-fractioned budget, each peaking at the MEASURED
+// per-shard RSS. ByteSize in (the canonical carrier); the dimensionless shard count comes out as
+// Int (ByteSize ÷ ByteSize) via the projection above. Fail-closed forward progress: a non-positive
+// peak (unknown measurement) or a budget under one shard still admits 1, never 0.
+fn memory_bounded_shard_count(memory_budget: ByteSize, per_shard_peak: ByteSize) -> Int {
+  let peak_bytes = byte_size_count_int(b: per_shard_peak)
+  if peak_bytes <= 0 {
+    1
+  } else {
+    let safe_budget = byte_size_count_int(b: budget_safety_fraction_apply(budget: memory_budget))
+    let fits = safe_budget / peak_bytes
+    if fits < 1 { 1 } else { fits }
+  }
+}
+
+// Memory-aware spawn width: min(shard_count, hardware_threads, ⌊0.8·budget ÷ measured_peak⌋).
+// Byte quantities are std.measure ByteSize (the canonical Memory carrier), not flat Int — the
+// dimension is attached at the authority-layer API; the counts are projected to Int (the fold's
+// arithmetic domain) at the boundary. A zero budget means the host could NOT read a live budget —
+// fall back to the caller's conservative committed width so a missing measurement never OOMs and
+// is never fabricated here (DESIGN §5; the host supplies the fallback). The heavy-resolve topology
+// serialization stays the independent backstop either way.
+fn memory_aware_spawn_width(
+  shard_count: Int,
+  hardware_threads: HardwareThreadCount,
+  memory_budget: ByteSize,
+  per_shard_peak: ByteSize,
+  conservative_fallback_width: Int
+) -> HardwareThreadCount {
+  let budget_bytes = byte_size_count_int(b: memory_budget)
+  if budget_bytes <= 0 {
+    hardware_thread_count(count: conservative_fallback_width)
+  } else {
+    let cpu_width = hardware_thread_count_value(
+      t: bounded_host_spawn_width(shard_count: shard_count, hardware_threads: hardware_threads)
+    )
+    let mem_width = memory_bounded_shard_count(
+      memory_budget: memory_budget,
+      per_shard_peak: per_shard_peak
+    )
+    hardware_thread_count(count: int_min(a: cpu_width, b: mem_width))
+  }
+}
+
 // Pareto goals for width trade-off (wall-time ↓, peak-memory ↓) — reuse std.pareto vocabulary.
 fn width_fold_objective_goals() -> List<AxisGoal> {
   [LowerIsBetter, LowerIsBetter]
@@ -150,3 +230,86 @@ fn witness_measured_cost_affects_shard_balance() -> Bool {
   let right = shard_balance_slot_for_cost(cost: low, baseline: baseline)
   left != right
 }
+
+// ── §1-C memory-aware width witnesses ────────────────────────────────────────
+// Helper: derived width value given the four inputs (shard/threads/budget/peak) + fallback.
+fn memory_aware_width_value(
+  shard_count: Int,
+  hardware_threads: HardwareThreadCount,
+  memory_budget: ByteSize,
+  per_shard_peak: ByteSize,
+  conservative_fallback_width: Int
+) -> Int {
+  hardware_thread_count_value(
+    t: memory_aware_spawn_width(
+      shard_count: shard_count,
+      hardware_threads: hardware_threads,
+      memory_budget: memory_budget,
+      per_shard_peak: per_shard_peak,
+      conservative_fallback_width: conservative_fallback_width
+    )
+  )
+}
+
+// Non-binding case: budget admits far more than shard_count, so width = shard_count (the
+// 4→7 reality — 0.8×62.5GiB ÷ 2.1GB ≈ 23 ≫ 7, so memory does not bind).
+fn witness_memory_term_non_binding_uses_shard_count(
+  shard_count: Int,
+  hardware_threads: HardwareThreadCount
+) -> Bool {
+  memory_aware_width_value(
+    shard_count: shard_count,
+    hardware_threads: hardware_threads,
+    memory_budget: byte_size(67108864000),
+    per_shard_peak: byte_size(2100028416),
+    conservative_fallback_width: 4
+  ) == shard_count
+}
+
+// Binding case: a tight budget backs width BELOW the topology cap — the fail-closed floor.
+// budget 6 GiB × 0.8 = 4.8 GiB ÷ 2.1 GB = 2 shards < shard_count 7 → width 2.
+fn witness_tight_budget_backs_off_below_shard_count() -> Bool {
+  memory_aware_width_value(
+    shard_count: 7,
+    hardware_threads: hardware_thread_count(128),
+    memory_budget: byte_size(6442450944),
+    per_shard_peak: byte_size(2100028416),
+    conservative_fallback_width: 4
+  ) == 2
+}
+
+// Fail-closed: an unreadable budget (0-byte sentinel from the host) → the conservative fallback,
+// never an unbounded width and never an OOM. RED if a memory-blind fold ignored the sentinel.
+fn witness_unreadable_budget_falls_back_conservative() -> Bool {
+  memory_aware_width_value(
+    shard_count: 7,
+    hardware_threads: hardware_thread_count(128),
+    memory_budget: byte_size(0),
+    per_shard_peak: byte_size(2100028416),
+    conservative_fallback_width: 4
+  ) == 4
+}
+
+// Fraction is load-bearing: 0.8×budget changes the bound. budget exactly 2×peak admits 2 raw
+// but 0.8×(2×peak)=1.6×peak admits only 1 — the safety margin demoted it. RED without ×4/5.
+fn witness_safety_fraction_is_load_bearing() -> Bool {
+  let peak = 2100028416
+  memory_aware_width_value(
+    shard_count: 7,
+    hardware_threads: hardware_thread_count(128),
+    memory_budget: byte_size(peak * 2),
+    per_shard_peak: byte_size(peak),
+    conservative_fallback_width: 4
+  ) == 1
+}
+
+// Fail-closed forward progress: a budget under one shard still admits width 1 (never 0).
+fn witness_subunit_budget_admits_one() -> Bool {
+  memory_aware_width_value(
+    shard_count: 7,
+    hardware_threads: hardware_thread_count(128),
+    memory_budget: byte_size(1000000000),
+    per_shard_peak: byte_size(2100028416),
+    conservative_fallback_width: 4
+  ) == 1
+}

dsl/test/claim/realization_measurement_keystone_test.dag

@@ -17,6 +17,7 @@ import std.realization_schedule {
 import std.realization_measurement {
   RealizationMeasureEffect,
   witness_measured_rollup_differs_from_predicted_zero,
+  witness_concurrent_memory_peak_per_share_divides,
 }
 import extdeps.realization.v1_handler { v1_eval_expr_measure_handler_id }
 import product.compute_fabric {
@@ -73,4 +74,5 @@ test fn realization_measurement_keystone_witnesses() -> Bool {
     && witness_measured_receipt_rollup_uses_lens()
     && witness_measured_rollup_red_on_predicted_zero()
     && witness_v1_handler_id_declared()
+    && witness_concurrent_memory_peak_per_share_divides()
 }

dsl/test/claim/realization_width_witness_test.dag

@@ -23,6 +23,11 @@ import std.realization {
   witness_width_fold_preserves_schedule_topology,
   witness_budget_ignoring_fold_fails,
   witness_measured_cost_affects_shard_balance,
+  witness_memory_term_non_binding_uses_shard_count,
+  witness_tight_budget_backs_off_below_shard_count,
+  witness_unreadable_budget_falls_back_conservative,
+  witness_safety_fraction_is_load_bearing,
+  witness_subunit_budget_admits_one,
 }
 
 fn synthetic_plan_total() -> CostAccount<Nano> {
@@ -106,6 +111,14 @@ fn witness_measured_balance_discriminator() -> Bool {
   witness_measured_cost_affects_shard_balance()
 }
 
+// §1-C memory-aware width: budget non-binding → width = shard_count (the 4→7 reality).
+fn witness_memory_non_binding_at_7() -> Bool {
+  witness_memory_term_non_binding_uses_shard_count(
+    shard_count: 7,
+    hardware_threads: witness_threads_64()
+  )
+}
+
 test fn realization_width_witnesses() -> Bool {
   witness_under_cap_uses_shard_count()
     && witness_over_cap_uses_hardware_threads()
@@ -114,4 +127,9 @@ test fn realization_width_witnesses() -> Bool {
     && witness_degenerate_shard_count_fail_closed_serial()
     && witness_budget_ignoring_fold_red_on_8_4()
     && witness_measured_balance_discriminator()
+    && witness_memory_non_binding_at_7()
+    && witness_tight_budget_backs_off_below_shard_count()
+    && witness_unreadable_budget_falls_back_conservative()
+    && witness_safety_fraction_is_load_bearing()
+    && witness_subunit_budget_admits_one()
 }