diff --git a/dag/gunbc/runner/runner_slot_population_census.dag b/dag/gunbc/runner/runner_slot_population_census.dag index 2b20409e434..e8a70c8736f 100644 --- a/dag/gunbc/runner/runner_slot_population_census.dag +++ b/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 List { + host_committed_identities_at(host: host, committed: committed) + |> map(id => runner_slot_unit_name(slot: id) as String) +} + fn observed_unit_names(observed: List) -> List { observed |> map(o => o.unit) } @@ -140,7 +152,7 @@ fn slot_population_census(host: HostIdentity, observed: List 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, ) } diff --git a/dag/gunbc/runner/runner_width_transition.dag b/dag/gunbc/runner/runner_width_transition.dag index c04ef06890c..fe244884c68 100644 --- a/dag/gunbc/runner/runner_width_transition.dag +++ b/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, committed: List) -> List { + 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)) } diff --git a/dag/gunbc/spark/training_ready.dag b/dag/gunbc/spark/training_ready.dag index 744054f086c..e536e13d8cb 100644 --- a/dag/gunbc/spark/training_ready.dag +++ b/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, ) -> 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, diff --git a/dag/test/claim/runner/runner_host_file_converge_witness_test.dag b/dag/test/claim/runner/runner_host_file_converge_witness_test.dag index a1ccb5a5a75..138433059cc 100644 --- a/dag/test/claim/runner/runner_host_file_converge_witness_test.dag +++ b/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 { - 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 { - 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 { - 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 { - 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, wire: String) -> Bool { diff --git a/dag/test/claim/runner/runner_slot_retirement_witness_test.dag b/dag/test/claim/runner/runner_slot_retirement_witness_test.dag index 4562224d2e5..b0f7262f386 100644 --- a/dag/test/claim/runner/runner_slot_retirement_witness_test.dag +++ b/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. diff --git a/dag/test/claim/spark/spark_training_ready_witness_test.dag b/dag/test/claim/spark/spark_training_ready_witness_test.dag index 32900799157..8e4da5c1f2a 100644 --- a/dag/test/claim/spark/spark_training_ready_witness_test.dag +++ b/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,6 +135,16 @@ 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 { host: operator_host_srv5, role: SparkServingCell }, + SparkCellRoleAssignment { host: operator_host_srv6, role: SparkTrainingCell }, +] + fn w_readiness( retirement: SparkServingRetirementObservation, meminfo_stdout: String, @@ -140,7 +152,7 @@ fn w_readiness( 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