Runner obligation and census read committed identities; Spark training readiness takes its roster

dag/gunbc/runner/runner_slot_population_census.dag

@@ -9,6 +9,7 @@ import gunbc.runner_slot_allocation {
   gunbc_runner_committed_width,
   RunnerWidthResolution, RunnerWidthDerived, RunnerWidthUnresolved,
   runner_width_unresolved_cause_text,
+  host_committed_identities_at,
 }
 import gunbc.host_axis_caps { SurplusSlotObservation, SurplusSlotsObserved, SurplusSlotsUnobserved }
 import gunbc.fleet_known_hosts_anchor { FleetSshExecutionContext, SshTarget }
@@ -78,6 +79,17 @@ fn desired_unit_names_range(host: HostIdentity, slot: Int, limit: Int) -> List<S
   }
 }
 
+// THE COMMITTED POPULATION AS UNIT NAMES, AT IDENTITY GRAIN. Since #12339 a host's committed members
+// are not 1..width: on srv1 the microVM shakedown slot is a member by its authored index (13) and the
+// fleet range beneath it is 1..(width - 1) -- gunbc.runner_slot_allocation
+// host_committed_identities_at. A consumer that enumerated 1..width named a fleet slot the width never
+// charged for and dropped srv1-13, so the census classified the shakedown slot as retiring and the
+// transition obligation required it. Every desired-set reader goes through this one derivation.
+fn committed_unit_names_at(host: HostIdentity, committed: Int) -> List<String> {
+  host_committed_identities_at(host: host, committed: committed)
+    |> map(id => runner_slot_unit_name(slot: id) as String)
+}
+
 fn observed_unit_names(observed: List<ObservedRunnerUnit>) -> List<String> {
   observed |> map(o => o.unit)
 }
@@ -140,7 +152,7 @@ fn slot_population_census(host: HostIdentity, observed: List<ObservedRunnerUnit>
     RunnerWidthDerived { slots: slots } =>
       slot_population_census_against_desired(
         host: host,
-        desired: desired_unit_names_range(host: host, slot: 1, limit: slots),
+        desired: committed_unit_names_at(host: host, committed: slots),
         observed: observed,
       )
   }

dag/gunbc/runner/runner_width_transition.dag

@@ -3,7 +3,7 @@ module gunbc.runner_width_transition
 import std.types { Bool, List, String, NonEmptyStr, Int, list_length }
 import product.host_identity { HostIdentity }
 import gunbc.fleet_host_identity { operator_host_srv1, operator_host_srv3, operator_host_srv4 }
-import gunbc.runner_slot_population_census { desired_unit_names_range, unit_is_owned_by_host }
+import gunbc.runner_slot_population_census { desired_unit_names_range, unit_is_owned_by_host, committed_unit_names_at }
 import gunbc.runner_slot_allocation {
   gunbc_runner_committed_width,
   RunnerWidthResolution, RunnerWidthDerived, RunnerWidthUnresolved,
@@ -121,15 +121,22 @@ fn transition_required_retirees_at(t: RunnerWidthTransition, target_width: Runne
       RetireesUnresolved { host: t.host, cause: runner_width_unresolved_cause_text(cause: c) }
     RunnerWidthDerived { slots: target } =>
       RetireesKnown {
-        units: desired_unit_names_range(
-          host: t.host,
-          slot: target + 1,
-          limit: t.prior_width,
+        units: prior_minus_committed(
+          prior: desired_unit_names_range(host: t.host, slot: 1, limit: t.prior_width),
+          committed: committed_unit_names_at(host: t.host, committed: target),
         ) |> map(u => u as NonEmptyStr),
       }
   }
 }
 
+// PRIOR MINUS COMMITTED IS A SET DIFFERENCE OVER IDENTITIES, NOT `target + 1 .. prior`. The index
+// range was exact only while the committed population was 1..width; since #12339 srv1's committed
+// population is 1..(width - 1) plus the shakedown slot srv1-13, so the range both required srv1-13 --
+// a committed fabric member -- and left out the fleet slot the width stopped charging for.
+fn prior_minus_committed(prior: List<String>, committed: List<String>) -> List<String> {
+  prior |> filter(u => !any(committed, c => c == u))
+}
+
 fn transition_required_retirees(t: RunnerWidthTransition) -> RequiredRetirees {
   transition_required_retirees_at(t: t, target_width: gunbc_runner_committed_width(host: t.host))
 }

dag/gunbc/spark/training_ready.dag

@@ -8,7 +8,9 @@ import gunbc.spark.cell_role {
   SparkCellRole,
   SparkServingCell,
   SparkTrainingCell,
-  spark_cell_role_of,
+  SparkCellRoleAssignment,
+  spark_cell_role_assignments,
+  spark_cell_role_in,
   spark_cell_role_eq,
   SparkCellRoleLookup,
   SparkCellRoleAbsent,
@@ -443,9 +445,21 @@ fn spark_serving_retirement_refusals(retirement: SparkServingRetirementObservati
 // is where the refusal now lives.
 fn spark_training_readiness(
   pool: SparkUnifiedPoolObservation,
+) -> SparkTrainingReadiness {
+  spark_training_readiness_in(pool: pool, assignments: spark_cell_role_assignments)
+}
+
+// THE ROSTER IS A PARAMETER, FOR THE REASON gunbc.spark.cell_role spark_cell_role_in GIVES: a
+// capability's evidence must not depend on which machines are currently assigned what. Reading the
+// production roster here left the training arm with no subject once the 2026-09-02 operator decision
+// (#10009) made srv6 a serving cell -- the positive control went red, and every refusal claim over
+// srv6 passed on role alone instead of on the axis it exists to discriminate.
+fn spark_training_readiness_in(
+  pool: SparkUnifiedPoolObservation,
+  assignments: List<SparkCellRoleAssignment>,
 ) -> SparkTrainingReadiness {
   let retirement = pool.after
-  match spark_cell_role_of(host: retirement.host) {
+  match spark_cell_role_in(assignments: assignments, host: retirement.host) {
     SparkCellRoleAbsent =>
       SparkTrainingNotReady {
         cause: "spark_training_ready: the host holds no Spark cell role, so nothing assigned it to training" as NonEmptyStr,

dag/test/claim/runner/runner_host_file_converge_witness_test.dag

@@ -10,7 +10,7 @@ import extdeps.needrestart {
   needrestart_unit_name_prefix_regex,
 }
 import product.host_identity { HostIdentity }
-import gunbc.runner_slot_population_census { desired_unit_names_range }
+import gunbc.runner_slot_population_census { desired_unit_names_range, committed_unit_names_at }
 import gunbc.runner_slot_allocation { gunbc_runner_committed_width, RunnerWidthDerived, RunnerWidthUnresolved }
 import gunbc.runner_width_transition { transition_population_agreement, TransitionPopulationAgrees, TransitionPopulationDisagrees, TransitionPopulationUndecidable }
 import gunbc.fleet_host_identity { operator_host_srv1 }
@@ -728,22 +728,29 @@ fn srv1_width() -> Int? {
   }
 }
 
+// THE LIVE SET IS THE COMMITTED IDENTITIES, NOT 1..width. Since #12339 srv1's committed population
+// is srv1-01..(width - 1) plus the shakedown slot srv1-13 (gunbc.runner_slot_allocation
+// host_committed_identities_at), so cutting the listing at the width named a slot the width no longer
+// charges as live and masked srv1-13. The live set comes from the census authority's one derivation;
+// the retiring set is the rest of the listing.
 fn srv1_live_names() -> List<String> {
-  match srv1_width() { Absent => [] Present { value: w } => srv1_unit_names(slot: 1, limit: w) }
+  match srv1_width() { Absent => [] Present { value: w } => committed_unit_names_at(host: "srv1" as HostIdentity, committed: w) }
 }
 
 fn srv1_retiring_names(limit: Int) -> List<String> {
-  match srv1_width() { Absent => [] Present { value: w } => srv1_unit_names(slot: w + 1, limit: limit) }
+  let live = srv1_live_names()
+  match srv1_width() { Absent => [] Present { value: _ } => srv1_unit_names(slot: 1, limit: limit) |> filter(u => !any(live, l => l == u)) }
 }
 
 // The last declared-live slot: the one the REDs below mask or lose to show that retirement never
 // excuses a live slot.
 fn srv1_last_live_names() -> List<String> {
-  match srv1_width() { Absent => [] Present { value: w } => srv1_unit_names(slot: w, limit: w) }
+  fold(srv1_live_names(), init: [], f: (acc, u) => [u])
 }
 
 fn srv1_all_but_last_live_names() -> List<String> {
-  match srv1_width() { Absent => [] Present { value: w } => srv1_unit_names(slot: 1, limit: w - 1) }
+  let last = srv1_last_live_names()
+  srv1_live_names() |> filter(u => !any(last, l => l == u))
 }
 
 fn every_unit_holds(pop: RunnerSlotPopulation, units: List<String>, wire: String) -> Bool {

dag/test/claim/runner/runner_slot_retirement_witness_test.dag

@@ -1085,6 +1085,27 @@ test fn a_derived_target_width_yields_the_prior_minus_target_obligation() -> Boo
   }
 }
 
+// THE OBLIGATION IS PRIOR MINUS THE COMMITTED IDENTITIES, NOT `target + 1 .. prior`. On srv1 the
+// committed population at width 11 is srv1-01..10 plus the shakedown slot srv1-13 (#12339), so the
+// obligation must name srv1-11 and srv1-12 -- the fleet slots the width stopped charging for -- and
+// must NOT name srv1-13. The index-range derivation got both wrong with the same count (39), which
+// is why this asserts membership rather than length alone.
+test fn the_obligation_excludes_a_committed_member_above_the_fleet_range() -> Bool {
+  match transition_row_for_host(host: operator_host_srv1).first() {
+    Absent => false
+    Present { value: t } =>
+      match transition_required_retirees_at(t: t, target_width: RunnerWidthDerived { slots: 11 }) {
+        RetireesKnown { units: units } =>
+          list_length(items: units) == 39
+            && any(units, u => (u as String) == "actions-runner@srv1-11.service")
+            && any(units, u => (u as String) == "actions-runner@srv1-12.service")
+            && !any(units, u => (u as String) == "actions-runner@srv1-13.service")
+            && !any(units, u => (u as String) == "actions-runner@srv1-10.service")
+        RetireesUnresolved { host: _, cause: _ } => false
+      }
+  }
+}
+
 // AND THE WRAPPER REACHES THE DECISION ON THE REAL PATH, which is what keeps the two supplied-input
 // rows above from being claims about a function nothing calls: srv4's width resolves today, so the
 // production read yields the same derived obligation the decision produces for that width.

dag/test/claim/spark/spark_training_ready_witness_test.dag

@@ -3,6 +3,7 @@ module test.claim.spark.spark_training_ready_witness_test
 import std.types { String, Bool, List, NonEmptyStr, Int }
 import product.host_identity { HostIdentity }
 import gunbc.fleet_host_identity { operator_host_srv5, operator_host_srv6 }
+import gunbc.spark.cell_role { SparkCellRoleAssignment, SparkServingCell, SparkTrainingCell }
 import gunbc.spark.training_ready {
   SparkServingProbeCapture,
   ProbeNeverRan,
@@ -18,6 +19,7 @@ import gunbc.spark.training_ready {
   SparkTrainingReady,
   SparkTrainingNotReady,
   spark_training_readiness,
+  spark_training_readiness_in,
   spark_serving_absence_from_probe,
   spark_serving_absence_refusal,
   SparkServingAbsenceEvidence,
@@ -133,14 +135,24 @@ fn w_pool_or_refused(
   }
 }
 
+// THE ROSTER IS SUPPLIED, NOT READ FROM PRODUCTION. The 2026-09-02 operator decision (#10009) made
+// srv6 a serving cell, so against the production roster the positive control below had no subject
+// and every refusal claim over srv6 passed on role alone rather than on the axis it names. srv6
+// trains and srv5 serves in this authored roster; the production wrapper is exercised by
+// w_the_production_roster_holds_no_training_cell.
+data w_roster: List<SparkCellRoleAssignment> = [
+  SparkCellRoleAssignment { host: operator_host_srv5, role: SparkServingCell },
+  SparkCellRoleAssignment { host: operator_host_srv6, role: SparkTrainingCell },
+]
+
 fn w_readiness(
   retirement: SparkServingRetirementObservation,
   meminfo_stdout: String,
 ) -> Bool {
   match w_pool_or_refused(meminfo_stdout: meminfo_stdout, after: retirement) {
     Absent => false
     Present { value: pool } =>
-      match spark_training_readiness(pool: pool) {
+      match spark_training_readiness_in(pool: pool, assignments: w_roster) {
         SparkTrainingReady { proof: _ } => true
         SparkTrainingNotReady { cause: _ } => false
       }
@@ -151,6 +163,19 @@ test fn w_a_fully_retired_training_cell_is_ready() -> Bool {
   w_readiness(retirement: w_retired_srv6(), meminfo_stdout: "97656250")
 }
 
+// THE PRODUCTION WRAPPER READS THE PRODUCTION ROSTER, where srv6 serves since #10009: the same
+// observation the positive control admits is refused there, on role.
+test fn w_the_production_roster_holds_no_training_cell() -> Bool {
+  match w_pool_or_refused(meminfo_stdout: "97656250", after: w_retired_srv6()) {
+    Absent => false
+    Present { value: pool } =>
+      match spark_training_readiness(pool: pool) {
+        SparkTrainingReady { proof: _ } => false
+        SparkTrainingNotReady { cause: _ } => true
+      }
+  }
+}
+
 // THE POSITIVE CONTROL'S MIRROR: THE SERVING CELL IS NEVER READY.
 //
 // srv5's retirement observation is deliberately WELL-FORMED and fully absent here. If role were not