Budget-tree consumer-0 + Track A: instantiate the real srv1 fleet BudgetNode tree from measured numbers + DERIVE the .dag-floor spawn-width from it (construction, not a Bool check)

dsl/gunbc/ci_budget_tree.dag

@@ -0,0 +1,153 @@
+module gunbc.ci_budget_tree
+
+import std.measure { ByteSize, byte_size, byte_size_count, Memory, One }
+import std.types { Int, List }
+import std.realization_width { memory_effective_budget }
+import extdeps.accounting.budget { Appropriation, LineItem }
+import product.budget_tree {
+  BudgetNode, BudgetClaim, BudgetPriority, Guaranteed, Burstable,
+  node_conserves_local, node_balance, admit_claims, claim_items
+}
+import product.compute_fabric { compute_host_ram_bytes_total }
+import gunbc.operator_fleet { srv1_host }
+import gunbc.ci_floor_measurement {
+  CiJobPeak,
+  HostFixedOverhead, HostFixedOverheadMeasured, HostFixedOverheadUnmeasured,
+  gunbc_ci_job_peaks,
+  gunbc_ci_host_fixed_overhead,
+  gunbc_ci_concurrent_runs_conservative_high,
+}
+import gunbc.ci_runner_placement {
+  JobPeakResolution, JobPeaksResolved, JobPeaksUnresolved,
+  resolve_run_unit_peak,
+}
+
+// The srv1 fleet memory budget as a BudgetNode tree, instantiated entirely from the
+// measured single-authority carriers (no fresh magic numbers): host RAM from the modeled
+// srv1 ComputeHost, fixed overhead + per-run peak + conservative-high R from
+// gunbc.ci_floor_measurement, reduced through the same helpers ci_runner_placement uses
+// (resolve_run_unit_peak, memory_effective_budget) so the tree does not fork their numbers.
+//
+// Divide-once: the root is host RAM; the run-pool's appropriation is the placement-effective
+// budget (0.8 safety fraction minus fixed overhead), so the unallocated remainder at the root
+// is exactly the safety headroom (Surplus, by construction). The floor consumer imports one
+// run slot (per-run peak); it never re-divides host RAM.
+
+fn srv1_host_ram() -> ByteSize {
+  compute_host_ram_bytes_total(host: srv1_host)
+}
+
+// Fail-closed: an unmeasured overhead cannot price the reserve, so reserve nothing usable
+// (byte_size(0) collapses the run-pool to the safety fraction alone — conservative, never
+// an over-commit). The live carrier is HostFixedOverheadMeasured, so this is the §5 backstop.
+fn gunbc_ci_fixed_overhead_bytes() -> ByteSize {
+  match gunbc_ci_host_fixed_overhead {
+    HostFixedOverheadMeasured { bytes: b } => b
+    HostFixedOverheadUnmeasured => byte_size(0)
+  }
+}
+
+// Single authority for the per-run peak: the same reduction ci_runner_placement applies to
+// gunbc_ci_job_peaks. Fail-closed to byte_size(0) when unresolved (a zero per-run peak makes
+// every fit/admission back off rather than divide by a fabricated number).
+fn gunbc_ci_per_run_peak() -> ByteSize {
+  match resolve_run_unit_peak(job_peaks: gunbc_ci_job_peaks) {
+    JobPeaksResolved { run_unit_peak: p } => p
+    JobPeaksUnresolved { reason: _ } => byte_size(0)
+  }
+}
+
+// The placement-effective budget for runs: 0.8 safety fraction of host RAM minus fixed
+// overhead. Reused verbatim from std.realization_width so the budget tree and
+// ci_runner_placement read the SAME usable-for-runs number (§3 single authority).
+fn gunbc_ci_run_pool_budget() -> ByteSize {
+  memory_effective_budget(budget: srv1_host_ram(), reserved: gunbc_ci_fixed_overhead_bytes())
+}
+
+fn run_claim(peak: ByteSize) -> BudgetClaim {
+  BudgetClaim {
+    item: LineItem { purpose: "concurrent-run", amount: peak },
+    priority: Burstable
+  }
+}
+
+fn run_claims_loop(acc: List<BudgetClaim>, peak: ByteSize, remaining: Int) -> List<BudgetClaim> {
+  if remaining <= 0 {
+    acc
+  } else {
+    run_claims_loop(acc: concat(acc, [run_claim(peak: peak)]), peak: peak, remaining: remaining - 1)
+  }
+}
+
+// R candidate runs at the conservative-high ceiling, each appropriated the per-run peak.
+fn gunbc_ci_run_candidates() -> List<BudgetClaim> {
+  run_claims_loop(
+    acc: [],
+    peak: gunbc_ci_per_run_peak(),
+    remaining: gunbc_ci_concurrent_runs_conservative_high
+  )
+}
+
+// L1 — the concurrent-run pool. Appropriation = placement-effective budget; claims = the
+// conservative-high R candidate runs. node_conserves_local is HONESTLY false here whenever
+// R exceeds what the pool can admit: that is the §5 over-commit the OOM-killer enforces today,
+// not a wall. The wall is admit_claims below (admission is construction).
+fn gunbc_ci_run_pool_node() -> BudgetNode {
+  BudgetNode {
+    name: "concurrent-runs",
+    appropriation: Appropriation { ceiling: gunbc_ci_run_pool_budget() },
+    claims: gunbc_ci_run_candidates(),
+    children: []
+  }
+}
+
+// L0 — srv1 host RAM. Claim = fixed overhead (Guaranteed). Child = the run pool. The root
+// conserves with a Surplus equal to the 0.8 safety headroom (reserved by construction, not a
+// flag): overhead + run-pool-budget = overhead + (0.8 host - overhead) = 0.8 host < host.
+fn gunbc_srv1_budget_tree() -> BudgetNode {
+  BudgetNode {
+    name: "srv1",
+    appropriation: Appropriation { ceiling: srv1_host_ram() },
+    claims: [
+      BudgetClaim {
+        item: LineItem { purpose: "host-fixed-overhead", amount: gunbc_ci_fixed_overhead_bytes() },
+        priority: Guaranteed
+      }
+    ],
+    children: [gunbc_ci_run_pool_node()]
+  }
+}
+
+// L2 — the .dag CI floor run. One run slot: appropriation = per-run peak. This is the
+// allocation the floor spawn-width derives its memory budget from (Track A); the floor never
+// divides host RAM, it imports this single slot from its parent run pool (divide-once).
+fn gunbc_ci_floor_run_node() -> BudgetNode {
+  BudgetNode {
+    name: "ci-floor-run",
+    appropriation: Appropriation { ceiling: gunbc_ci_per_run_peak() },
+    claims: [],
+    children: []
+  }
+}
+
+// The floor's L2 memory budget in bytes — the single value Track A wires into
+// gunbc_ci_floor_spawn_width in place of an independently-divided host budget.
+fn gunbc_ci_floor_run_appropriation_bytes() -> Int {
+  byte_size_count(b: gunbc_ci_floor_run_node().appropriation.ceiling)
+}
+
+// Byte accessors for downstream consumers (the floor) that need the raw magnitude.
+fn gunbc_ci_per_run_peak_bytes() -> Int {
+  byte_size_count(b: gunbc_ci_per_run_peak())
+}
+
+fn gunbc_ci_srv1_host_ram_bytes() -> Int {
+  byte_size_count(b: srv1_host_ram())
+}
+
+// Construction: the admitted run set is provably within the run-pool appropriation. The
+// count of admitted runs is the safe concurrent-run count derived by zero-based admission —
+// over-commit is unwritable on this path (it lands in `refused`, not `committed`).
+fn gunbc_ci_admitted_run_count() -> Int {
+  admit_claims(node: gunbc_ci_run_pool_node()).committed.length()
+}

dsl/test/claim/ci_budget_tree_witness_test.dag

@@ -0,0 +1,66 @@
+module test.claim.ci_budget_tree_witness
+
+import std.logic { Bool }
+import std.measure { byte_size_count, measure_le }
+import extdeps.accounting.budget {
+  BudgetBalance, Surplus, within_appropriation
+}
+import product.budget_tree {
+  node_conserves_local, node_balance, admit_claims
+}
+import gunbc.ci_budget_tree {
+  gunbc_srv1_budget_tree,
+  gunbc_ci_run_pool_node,
+  gunbc_ci_floor_run_node,
+  gunbc_ci_per_run_peak,
+  gunbc_ci_run_pool_budget,
+  gunbc_ci_admitted_run_count,
+}
+import gunbc.ci_runner_placement { effective_runners_per_host }
+
+// The root conserves and the unallocated remainder is a Surplus — the 0.8 safety headroom,
+// reserved by construction (overhead claim + run-pool budget = 0.8 host < host).
+fn witness_root_conserves_with_safety_surplus() -> Bool {
+  node_conserves_local(node: gunbc_srv1_budget_tree())
+    && (node_balance(node: gunbc_srv1_budget_tree()) == Surplus)
+}
+
+// Honest §5 boundary: at the conservative-high R the run pool does NOT locally conserve —
+// the over-commit the kernel OOM-killer enforces today. This is the residue lens, not a wall.
+fn witness_runpool_overcommits_at_conservative_high() -> Bool {
+  !node_conserves_local(node: gunbc_ci_run_pool_node())
+}
+
+// The wall: admission is construction. The committed set is provably within appropriation and
+// the excess candidates are refused (not silently dropped). Admitted count = the safe R (3).
+fn witness_admission_constructs_safe_run_count() -> Bool {
+  let admitted = admit_claims(node: gunbc_ci_run_pool_node())
+  return within_appropriation(
+      appropriation: gunbc_ci_run_pool_node().appropriation,
+      items: admitted.committed
+    )
+    && (admitted.refused.length() > 0)
+    && (admitted.committed.length() == 3)
+}
+
+// §3 convergence: the budget-tree admission reproduces the existing placement authority's
+// per-host run count from the same measured numbers — the two are not forked.
+fn witness_admission_matches_placement() -> Bool {
+  gunbc_ci_admitted_run_count() == effective_runners_per_host(cap_enforced: true)
+}
+
+// Divide-once: the floor imports exactly one run slot (per-run peak) and that slot fits inside
+// the parent run-pool budget. The floor never re-divides host RAM.
+fn witness_floor_run_imports_one_slot() -> Bool {
+  let slot_is_peak = byte_size_count(b: gunbc_ci_floor_run_node().appropriation.ceiling) == byte_size_count(b: gunbc_ci_per_run_peak())
+  let fits = measure_le(a: gunbc_ci_floor_run_node().appropriation.ceiling, b: gunbc_ci_run_pool_budget())
+  return slot_is_peak && fits
+}
+
+test fn ci_budget_tree_holds() -> Bool {
+  witness_root_conserves_with_safety_surplus()
+    && witness_runpool_overcommits_at_conservative_high()
+    && witness_admission_constructs_safe_run_count()
+    && witness_admission_matches_placement()
+    && witness_floor_run_imports_one_slot()
+}

src/v2/test/claim/ci_floor_plan_witness_test.dag

@@ -10,6 +10,8 @@ import v2.workflow.ci_floor_plan {
   witness_floor_tight_budget_backs_off_envelope,
   witness_floor_fail_open_would_exceed_budget,
   witness_floor_unreadable_budget_uses_conservative_envelope,
+  witness_floor_budget_is_l2_run_slot_not_host,
+  witness_floor_spawn_width_fits_l2_budget,
 }
 import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots }
 import v2.std.algebra { length, list_snoc_item }

src/v2/workflow/ci_floor_plan.dag

@@ -13,7 +13,12 @@ import v2.std.dependency { DataDependsOn, ResourceDependsOn, DependencyView }
 import v2.std.node { Atom, Node, TypeNode }
 import v2.std.text { String }
 import std.types { ContentHash, Int }
-import std.measure { HardwareThreadCount, hardware_thread_count, byte_size }
+import std.measure { HardwareThreadCount, hardware_thread_count, hardware_thread_count_value, byte_size }
+import gunbc.ci_budget_tree {
+  gunbc_ci_floor_run_appropriation_bytes,
+  gunbc_ci_per_run_peak_bytes,
+  gunbc_ci_srv1_host_ram_bytes,
+}
 import std.realization_width { width_fold_objective_goals, memory_aware_spawn_width, bounded_host_spawn_width }
 import product.compute_fabric {
   ResourceEnvelope,
@@ -242,7 +247,7 @@ fn gunbc_ci_floor_hardware_threads() -> HardwareThreadCount {
   altra_max_m12830_catalog.threads
 }
 
-fn gunbc_ci_floor_spawn_width(memory_budget_bytes: Int) -> HardwareThreadCount {
+fn gunbc_ci_floor_spawn_width_at_budget(memory_budget_bytes: Int) -> HardwareThreadCount {
   memory_aware_spawn_width(
     shard_count: gunbc_ci_floor_breadth(),
     hardware_threads: gunbc_ci_floor_hardware_threads(),
@@ -252,6 +257,15 @@ fn gunbc_ci_floor_spawn_width(memory_budget_bytes: Int) -> HardwareThreadCount {
   )
 }
 
+// Track A — the floor spawn-width is CONSTRUCTED from the budget tree's L2 run allocation
+// (the one run slot the floor imports), not from a free-Int host budget. There is no longer a
+// knob to set the budget too high: the only budget available is the divide-once L2 slot, so a
+// spawn that would over-commit the floor is unwritable. This dissolves the realization_width
+// independent-host-division fork onto extdeps.accounting.budget (§3 single authority).
+fn gunbc_ci_floor_spawn_width() -> HardwareThreadCount {
+  gunbc_ci_floor_spawn_width_at_budget(memory_budget_bytes: gunbc_ci_floor_run_appropriation_bytes())
+}
+
 fn gunbc_ci_floor_run_envelope(memory_budget_bytes: Int) -> ResourceEnvelope {
   parallel_run_demand_envelope_from_budget(
     shard_count: gunbc_ci_floor_breadth(),
@@ -287,6 +301,26 @@ fn witness_floor_unreadable_budget_uses_conservative_envelope() -> Bool {
   demand_envelope_thread_count(envelope: envelope) == gunbc_ci_floor_conservative_fallback_width
 }
 
+// Track A construction: the floor's budget is the L2 run slot (the per-run peak), NOT a
+// host-wide budget — the divide-once boundary made concrete. The discriminating control is
+// that the budget differs from host RAM: an independently-divided host budget is no longer
+// reachable through the floor entrypoint.
+fn witness_floor_budget_is_l2_run_slot_not_host() -> Bool {
+  let budget = gunbc_ci_floor_run_appropriation_bytes()
+  budget == gunbc_ci_per_run_peak_bytes() && budget != gunbc_ci_srv1_host_ram_bytes()
+}
+
+// The tree-derived spawn-width fits inside the L2 budget it was constructed from, and is a
+// genuine memory-bounded width (> 0, not the unreadable-budget fallback) — the construction
+// produces a usable, conserving width by execution.
+fn witness_floor_spawn_width_fits_l2_budget() -> Bool {
+  let budget = gunbc_ci_floor_run_appropriation_bytes()
+  let envelope = gunbc_ci_floor_run_envelope(memory_budget_bytes: budget)
+  demand_envelope_fits_budget(envelope: envelope, budget: byte_size(budget))
+    && demand_envelope_thread_count(envelope: envelope) > 0
+    && hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) > 0
+}
+
 fn floor_layer_heavy_resolve_count(batch: ExecutorBatch, spec: CiSpec) -> Int {
   fold(batch.jobs, init: 0, f: fn(acc, job) {
     if floor_node_is_heavy_resolve(node: job.node, spec: spec) { acc + 1 } else { acc }