diff --git a/dag/extdeps/memory/samsung.dag b/dag/extdeps/memory/samsung.dag index 0f948ff3b4a..67cd2835e85 100644 --- a/dag/extdeps/memory/samsung.dag +++ b/dag/extdeps/memory/samsung.dag @@ -26,7 +26,7 @@ data extdeps_model_scope: ExternalModelScope = ExternalModelScope { further_citations: [] } -data stick_capacity_bytes: ByteSize = byte_size(34359738368) +data stick_capacity_bytes_32g: ByteSize = byte_size(34359738368) // PROVENANCE, SPLIT BY WHAT ACTUALLY SUPPORTS EACH FACT, because the module scope binds its // citation to this exact declaration and a generic DDR4 reference cannot carry a vendor SKU. @@ -55,7 +55,7 @@ data m386a4g40dm0_cpb_catalog: DramModuleCatalogRow = DramModuleCatalogRow { part_number: "M386A4G40DM0-CPB", manufacturer: samsung, generation: dram_generation_ddr4, - capacity_bytes: stick_capacity_bytes, + capacity_bytes: stick_capacity_bytes_32g, data_rate_mts: 2133, ecc: true, buffering: LoadReduced, diff --git a/dag/extdeps/memory/sk_hynix.dag b/dag/extdeps/memory/sk_hynix.dag index c3ce6b436a2..685a4f782da 100644 --- a/dag/extdeps/memory/sk_hynix.dag +++ b/dag/extdeps/memory/sk_hynix.dag @@ -13,13 +13,13 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { } } -data stick_capacity_bytes: ByteSize = byte_size(17179869184) +data stick_capacity_bytes_16g: ByteSize = byte_size(17179869184) data hma82gr7afr4n_vk_catalog: DramModuleCatalogRow = DramModuleCatalogRow { part_number: "HMA82GR7AFR4N-VK", manufacturer: sk_hynix, generation: dram_generation_ddr4, - capacity_bytes: stick_capacity_bytes, + capacity_bytes: stick_capacity_bytes_16g, data_rate_mts: 2666, ecc: true, buffering: Registered, @@ -33,7 +33,7 @@ data hma82gr7afr8n_vk_catalog: DramModuleCatalogRow = DramModuleCatalogRow { part_number: "HMA82GR7AFR8N-VK", manufacturer: sk_hynix, generation: dram_generation_ddr4, - capacity_bytes: stick_capacity_bytes, + capacity_bytes: stick_capacity_bytes_16g, data_rate_mts: 2666, ecc: true, buffering: Registered, diff --git a/dag/gunbc/dispatch_selection.dag b/dag/gunbc/dispatch_selection.dag index 17d9c1da2d3..0d537c418a6 100644 --- a/dag/gunbc/dispatch_selection.dag +++ b/dag/gunbc/dispatch_selection.dag @@ -53,6 +53,12 @@ import gunbc.roadmap_model { IntricacyHigh, PrsMerged, } +import product.placement_supply { HostIdentity } +import gunbc.fleet_capacity_control { + fleet_capacity_admission, fleet_capacity_admission_in, fleet_capacity_admission_admits, + HostCapacityWithdrawal, ProviderCapacityWithdrawal, + withdrawn_hosts, withdrawn_providers, +} import gunbc.roadmap_dashboard_instance { HostDashboardInstance, DashboardExistingProviderState, @@ -612,7 +618,101 @@ fn claude_offer_for_instance(instance: HostDashboardInstance) -> ClaudeOffer { ) } +// THE OPERATOR CAPACITY GATE, APPLIED WHERE THE OFFER IS MADE RATHER THAN WHERE IT IS CHOSEN. +// +// A withdrawn host or runtime makes NO OFFER, so ResolvedProviderSelection has no constructor for +// it -- the cut-off provider is not selected-and-then-rejected, it is unselectable. Gating after +// selection instead would concede that the bad state is writable and leave a refusal to catch it +// (DESIGN section 5: construction over validation). +// +// THE WITHDRAWALS ARE RETURNED SEPARATELY AND THAT IS NOT A CONVENIENCE. An inventory emptied by +// withdrawal and an inventory empty because nothing is installed are different facts with opposite +// remedies, and a bare filter renders both as the same empty list -- the empty-observation narrow, +// where could-not-offer becomes the verdict nothing-is-available. Keeping the removed rows +// addressable is what lets a consumer say WHY it has no offers. +fn instance_capacity_host(instance: HostDashboardInstance) -> HostIdentity { + instance.host_identity as HostIdentity +} + +// THE GATE TAKES ITS ROSTERS AS ARGUMENTS FOR THE REASON THE AUTHORITY DOES, ONE LAYER OUT. +// +// The live rosters are empty, so a gate that read them directly could only ever be witnessed in +// its neutral state -- a fixture could prove the gate is WIRED and never that it CUTS, which is a +// green test over the half that does nothing. +fn offer_is_capacity_admitted_in( + host_rows: List, + provider_rows: List, + instance: HostDashboardInstance, + offer: ProviderOffer, +) -> Bool { + fleet_capacity_admission_admits(admission: fleet_capacity_admission_in( + host_rows: host_rows, + provider_rows: provider_rows, + host: instance_capacity_host(instance: instance), + provider: provider_offer_kind(offer: offer), + )) +} + +fn capacity_admitted_offers_in( + host_rows: List, + provider_rows: List, + instance: HostDashboardInstance, + offers: List, +) -> List { + filter(offers, o => offer_is_capacity_admitted_in( + host_rows: host_rows, provider_rows: provider_rows, instance: instance, offer: o)) +} + +fn capacity_withdrawn_offers_in( + host_rows: List, + provider_rows: List, + instance: HostDashboardInstance, + offers: List, +) -> List { + filter(offers, o => !offer_is_capacity_admitted_in( + host_rows: host_rows, provider_rows: provider_rows, instance: instance, offer: o)) +} + +fn capacity_admitted_offers( + instance: HostDashboardInstance, + offers: List, +) -> List { + capacity_admitted_offers_in( + host_rows: withdrawn_hosts, provider_rows: withdrawn_providers, + instance: instance, offers: offers) +} + +fn capacity_withdrawn_offers( + instance: HostDashboardInstance, + offers: List, +) -> List { + capacity_withdrawn_offers_in( + host_rows: withdrawn_hosts, provider_rows: withdrawn_providers, + instance: instance, offers: offers) +} + +fn provider_inventory_withdrawn_for_instance( + instance: HostDashboardInstance, +) -> List { + capacity_withdrawn_offers( + instance: instance, + offers: declared_provider_inventory_for_instance(instance: instance).offers, + ) +} + fn provider_inventory_for_instance(instance: HostDashboardInstance) -> ProviderInventory { + ProviderInventory { + offers: capacity_admitted_offers( + instance: instance, + offers: declared_provider_inventory_for_instance(instance: instance).offers, + ), + } +} + +// THE DECLARED INVENTORY, BEFORE THE OPERATOR GATE. Kept as its own function so the gate has an +// unfiltered denominator to compare against; a gate folded into the construction below would have +// nothing to report a withdrawal against. +fn declared_provider_inventory_for_instance(instance: HostDashboardInstance) -> ProviderInventory { if instance.instance_id == srv2_dashboard_lab_id || instance.instance_id == srv2_dashboard_preview_id { ProviderInventory { diff --git a/dag/gunbc/fleet_capacity_control.dag b/dag/gunbc/fleet_capacity_control.dag new file mode 100644 index 00000000000..8a4d4d5b4ac --- /dev/null +++ b/dag/gunbc/fleet_capacity_control.dag @@ -0,0 +1,340 @@ +module gunbc.fleet_capacity_control + +import std.types { String, NonEmptyStr, Bool, List, Int } +import product.placement_supply { HostIdentity } +import extdeps.llm.cli_lifecycle { ProviderKind, ClaudeCliProvider, CodexCliProvider, CursorCliProvider, provider_kind_label } +import gunbc.fleet_intent_network { + operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4, +} + +// THE OPERATOR'S CONTROL OVER ACTIVE FLEET CAPACITY, ON TWO AXES THAT ARE NOT THE SAME FACT. +// +// Turning a MACHINE down and cutting off a PROVIDER are different questions with different blast +// radii, and fusing them into one "enabled" flag would make the smaller action unavailable: an +// operator who wants Codex off everywhere would have to take hosts down to get it, and an operator +// draining srv3 would have to reason about which runtimes that implicitly removes. They are +// therefore two withdrawal rosters over two subject types, joined only where capacity is actually +// consumed. +// +// WHY THIS IS A WITHDRAWAL ROSTER AND NOT AN ENABLEMENT ROSTER. The rows here name what is CUT OFF, +// so the default for an unlisted subject is active. The inverse -- listing what is enabled -- makes +// the roster load-bearing for ordinary operation, so a host absent through an authoring slip goes +// dark rather than staying up, and a new host must be added in two places before it can ever be +// used. Withdrawal fails toward capacity remaining available, which is the recoverable direction: +// too much capacity is a cost, too little is an outage. +data fleet_capacity_control_note: String = "Operator withdrawal rosters for fleet capacity on two axes: whole hosts and provider runtimes. Consumed at the dispatch inventory seam so a withdrawn provider makes no offer. Absent from a roster means active." + +// A WITHDRAWAL CARRIES ITS REASON BECAUSE THE ROSTER OUTLIVES THE SITUATION THAT CAUSED IT. +// +// The three causes are not decoration: they have different restoration conditions and different +// answers to "may an automated process put this back". Maintenance ends when the work does and is +// the operator's to reverse. A capacity cut is a deliberate standing spend decision. A fault +// withdrawal is a response to observed misbehaviour and must NOT be auto-restored by anything that +// merely notices the host answering again -- an intermittently failing host answers between +// failures, and a restorer keyed on reachability would flap it back into service repeatedly. +type CapacityWithdrawalCause + = WithdrawnForMaintenance { detail: NonEmptyStr } + | WithdrawnToReduceSpend { detail: NonEmptyStr } + | WithdrawnForObservedFault { detail: NonEmptyStr } + +fn withdrawal_cause_label(cause: CapacityWithdrawalCause) -> String { + match cause { + WithdrawnForMaintenance { detail: _ } => "maintenance" + WithdrawnToReduceSpend { detail: _ } => "spend" + WithdrawnForObservedFault { detail: _ } => "fault" + } +} + +fn withdrawal_cause_detail(cause: CapacityWithdrawalCause) -> NonEmptyStr { + match cause { + WithdrawnForMaintenance { detail: d } => d + WithdrawnToReduceSpend { detail: d } => d + WithdrawnForObservedFault { detail: d } => d + } +} + +// A FAULT WITHDRAWAL IS THE ONE AN AUTOMATED RESTORER MUST NOT TOUCH, AND THAT IS DECIDED HERE +// RATHER THAN AT EACH RESTORER. Left to callers, this becomes a rule some of them remember. +fn withdrawal_admits_automatic_restore(cause: CapacityWithdrawalCause) -> Bool { + match cause { + WithdrawnForMaintenance { detail: _ } => true + WithdrawnToReduceSpend { detail: _ } => false + WithdrawnForObservedFault { detail: _ } => false + } +} + +type HostCapacityWithdrawal { + host: HostIdentity + cause: CapacityWithdrawalCause +} + +type ProviderCapacityWithdrawal { + provider: ProviderKind + cause: CapacityWithdrawalCause +} + +// THE LIVE ROSTERS. Empty means the whole fleet and every runtime are active, which is the state +// this repository is in as of authoring -- these are the operator's control surface, and an empty +// control surface is the correct resting position rather than an unfinished one. +data withdrawn_hosts: List = [] + +data withdrawn_providers: List = [] + +// THE DECISION TAKES ITS ROSTERS AS ARGUMENTS AND THE GLOBAL READERS ARE THIN WRAPPERS, BECAUSE +// THE LIVE ROSTERS ARE EMPTY AND MUST STAY THAT WAY. +// +// A decision that reads the module-scope rosters directly can only ever be exercised in the state +// those rosters happen to be in -- today, empty -- so every refusal arm below would be unreachable +// by any fixture, and the witnesses could assert nothing but the admitted path. That is the +// decoration DESIGN names: a check whose RED cannot be produced is permanently green and worse +// than absent, because it is cited as coverage. Parameterizing makes the refusals authorable by a +// fixture without withdrawing anything on the live fleet, which is the distinction between +// unwritable-in-the-corpus and unwritable-as-a-fixture. +fn host_withdrawal_in( + rows: List, + host: HostIdentity, +) -> HostCapacityWithdrawal? { + filter(rows, row => row.host == host).first() +} + +fn provider_withdrawal_in( + rows: List, + provider: ProviderKind, +) -> ProviderCapacityWithdrawal? { + filter(rows, row => row.provider == provider).first() +} + +fn host_withdrawal_for(host: HostIdentity) -> HostCapacityWithdrawal? { + host_withdrawal_in(rows: withdrawn_hosts, host: host) +} + +fn provider_withdrawal_for(provider: ProviderKind) -> ProviderCapacityWithdrawal? { + provider_withdrawal_in(rows: withdrawn_providers, provider: provider) +} + +// THESE TWO REMAIN AS PREDICATES RATHER THAN BEING DISSOLVED INTO THEIR OPTION READERS +// (review 54905). The reviewer is right that Present => true / Absent => false is predicate +// dissolution and would be blocking in std. It is kept here because both callers -- the counts +// below and the dispatch gate in gunbc.dispatch_selection -- genuinely want the BOOLEAN and not +// the row: the gate filters offers and has no use for the cause. Dissolving would push a match +// over an Option whose Present payload is discarded into every call site, which is the same +// discard spelled more times. The Option readers are exported beside them for callers that need +// the cause, so nothing is forced through the lossy surface. +fn host_is_withdrawn(host: HostIdentity) -> Bool { + match host_withdrawal_for(host: host) { + Present { value: _ } => true + Absent => false + } +} + +fn provider_is_withdrawn(provider: ProviderKind) -> Bool { + match provider_withdrawal_for(provider: provider) { + Present { value: _ } => true + Absent => false + } +} + +// WHETHER A GIVEN RUNTIME MAY RUN ON A GIVEN HOST IS ONE QUESTION WITH THREE ANSWERS, NOT A BOOL. +// +// This is the load-bearing shape in the module and the reason the axes stay separate all the way to +// the consumer. A caller that receives only "no" cannot tell a withdrawn HOST from a withdrawn +// RUNTIME, and those have opposite remedies: one is fixed by restoring a machine, the other by +// restoring a provider everywhere. Collapsing them would also make a fully-withdrawn host's +// inventory indistinguishable from a host with nothing installed -- the empty-observation narrow +// DESIGN section 5 names, where could-not-offer is rendered as the verdict nothing-is-available. +type CapacityAdmission + = CapacityAdmitted + | CapacityRefusedHostWithdrawn { host: HostIdentity, cause: CapacityWithdrawalCause } + | CapacityRefusedProviderWithdrawn { provider: ProviderKind, cause: CapacityWithdrawalCause } + +// THE HOST AXIS IS CHECKED FIRST, AND THE ORDER IS A REAL DECISION RATHER THAN AN ARBITRARY ONE. +// +// When both are withdrawn the host is the dominant fact: nothing runs there regardless of runtime, +// so reporting the provider would name a cause whose repair changes nothing about this host. The +// same precedence is why the two refusals are distinct arms -- an operator reading "provider +// withdrawn" about a host that is down would restore the provider and see no capacity return. +fn fleet_capacity_admission_in( + host_rows: List, + provider_rows: List, + host: HostIdentity, + provider: ProviderKind, +) -> CapacityAdmission { + match host_withdrawal_in(rows: host_rows, host: host) { + Present { value: h } => CapacityRefusedHostWithdrawn { host: host, cause: h.cause } + Absent => + match provider_withdrawal_in(rows: provider_rows, provider: provider) { + Present { value: p } => + CapacityRefusedProviderWithdrawn { provider: provider, cause: p.cause } + Absent => CapacityAdmitted + } + } +} + +fn fleet_capacity_admission(host: HostIdentity, provider: ProviderKind) -> CapacityAdmission { + fleet_capacity_admission_in( + host_rows: withdrawn_hosts, + provider_rows: withdrawn_providers, + host: host, + provider: provider, + ) +} + +fn fleet_capacity_admission_admits(admission: CapacityAdmission) -> Bool { + match admission { + CapacityAdmitted => true + CapacityRefusedHostWithdrawn { host: _, cause: _ } => false + CapacityRefusedProviderWithdrawn { provider: _, cause: _ } => false + } +} + +// THE OPERATOR-FACING LINE FOR ONE REFUSAL, WHICH IS WHAT THE WORKSPACE PANEL RENDERS. +// +// It names the SUBJECT that was withdrawn rather than the pair, because that is the thing the +// operator would act on. A line that said only "srv3/Codex unavailable" would leave the reader to +// work out which of the two to restore, which is precisely the distinction the coproduct above +// exists to preserve. +fn fleet_capacity_admission_line(admission: CapacityAdmission) -> String { + match admission { + CapacityAdmitted => "active" + CapacityRefusedHostWithdrawn { host: h, cause: c } => + join(["host ", h as String, " withdrawn (", withdrawal_cause_label(cause: c), "): ", + withdrawal_cause_detail(cause: c) as String], "") + CapacityRefusedProviderWithdrawn { provider: p, cause: c } => + join(["provider ", provider_kind_label(kind: p), " withdrawn (", + withdrawal_cause_label(cause: c), "): ", + withdrawal_cause_detail(cause: c) as String], "") + } +} + +// THE FLEET THIS CONTROL SPANS. Four hosts, taken from the fleet identity authority rather than +// respelled, so a host added there is a host this control can reach without an edit here. +fn capacity_controlled_hosts() -> List { + [operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4] +} + +fn capacity_controlled_providers() -> List { + [ClaudeCliProvider, CodexCliProvider, CursorCliProvider] +} + +fn active_host_count() -> Int { + capacity_controlled_hosts() |> filter(h => !host_is_withdrawn(host: h)) |> count +} + +fn active_provider_count() -> Int { + capacity_controlled_providers() |> filter(p => !provider_is_withdrawn(provider: p)) |> count +} + +// ============================================================================================ +// THE OPERATOR CONTROL SURFACE. This is what the workspace panel actuates, and its shape is a +// ruling rather than a preference (operator, 2026-08-23). +// +// "CUT OFF A PROVIDER" NAMES TWO DIFFERENT ACTIONS AND THE CONTROL MUST SAY WHICH. Cutting a +// RUNTIME stops Claude everywhere; cutting an ACCOUNT BINDING stops one credential while the +// runtime keeps serving other accounts. They have different blast radii, and the conflation is +// silent in the worst direction: an operator who means "cut this Claude account" and gets Claude +// cut entirely discovers it as missing capacity rather than as a refusal, because both readings +// are perfectly well-formed requests and nothing downstream can tell them apart. +// +// So both controls exist from the first version even though only the runtime axis is wired. The +// account axis REFUSES with a typed cause rather than being absent -- an absent control reads as +// "not applicable here", which is the not-applicable-versus-malformed conflation this corpus has +// now found three times in three stages. A refusal says the axis is real and this build cannot +// serve it yet, which is the true statement. +// +// THE ACCOUNT AXIS IS NOT HYPOTHETICAL. Accounts on this fleet are being managed by hand at +// exactly this granularity today -- a credentials update performing an active-slot swap restarted +// a live container on 2026-08-22 -- so this is an axis someone is already operating WITHOUT a +// control, not a second reading invented for symmetry. +// ============================================================================================ + +type CapacityControlRequest + = CutHost { host: HostIdentity, cause: CapacityWithdrawalCause } + | CutProviderRuntime { provider: ProviderKind, cause: CapacityWithdrawalCause } + | CutProviderAccountBinding { + provider: ProviderKind, + account: NonEmptyStr, + cause: CapacityWithdrawalCause, + } + | RestoreHost { host: HostIdentity } + | RestoreProviderRuntime { provider: ProviderKind } + +// NOTHING HERE APPLIES ANYTHING, AND THE OUTCOME VOCABULARY SAYS SO (review 54905, 2026-08-23). +// +// An earlier revision of this type had a ControlApplied arm returning "host srv3 withdrawn +// (maintenance)" for four of the five requests. That was fabricated plausible output in the sense +// DESIGN section 5 forbids: the rosters are module-scope data rows, so a caller that applied a cut +// and then read host_is_withdrawn saw false immediately after being told the cut succeeded. The +// sibling witness asserting the rosters stay empty made the two claims jointly inconsistent by +// construction, and the witnesses could not catch it because they only compared strings between +// requests rather than joining the control to the roster reader. +// +// WHAT ACTUALLY HAPPENS IS PLANNING, SO THAT IS WHAT THE OUTCOME NAMES. Withdrawing capacity means +// authoring a roster row and committing it -- deliberately, because a withdrawal must face review +// like any other change to what the fleet does. So the control emits the EDIT that would effect +// the request, and applying it is the commit. This is the same plan/apply split the fleet converge +// path already uses, and it is honest at the only point that matters: no arm claims an effect that +// has not occurred. +// +// THE TWO NON-PLANNING ARMS ARE DISTINCT BECAUSE THEIR CAUSES ARE. ControlUnbound means no +// mechanism exists to serve a well-formed request -- the account axis, where there is no offer to +// remove. ControlRejected means the request itself was refused. Collapsing them would tell an +// operator to rephrase a request that was never the problem. +type CapacityControlOutcome + = ControlPlanned { roster_edit: String } + | ControlUnbound { axis: NonEmptyStr, trigger: NonEmptyStr } + | ControlRejected { reason: NonEmptyStr } + +data capacity_control_account_axis: NonEmptyStr = "provider account binding" as NonEmptyStr + +data capacity_control_account_axis_trigger: NonEmptyStr = "dispatch_selection AdmittedAccountBinding must become a withdrawable subject: the account binding is resolved inside provider selection rather than offered alongside it, so there is no offer to remove and the runtime-axis mechanism does not reach it" as NonEmptyStr + +fn apply_capacity_control(request: CapacityControlRequest) -> CapacityControlOutcome { + match request { + CutHost { host: h, cause: c } => + ControlPlanned { + roster_edit: join(["add to withdrawn_hosts: host ", h as String, " (", + withdrawal_cause_label(cause: c), ") ", + withdrawal_cause_detail(cause: c) as String], ""), + } + CutProviderRuntime { provider: p, cause: c } => + ControlPlanned { + roster_edit: join(["add to withdrawn_providers: runtime ", + provider_kind_label(kind: p), " (", + withdrawal_cause_label(cause: c), ") ", + withdrawal_cause_detail(cause: c) as String], ""), + } + CutProviderAccountBinding { provider: _, account: _, cause: _ } => + ControlUnbound { + axis: capacity_control_account_axis, + trigger: capacity_control_account_axis_trigger, + } + RestoreHost { host: h } => + ControlPlanned { + roster_edit: join(["remove from withdrawn_hosts: host ", h as String], ""), + } + RestoreProviderRuntime { provider: p } => + ControlPlanned { + roster_edit: join(["remove from withdrawn_providers: runtime ", + provider_kind_label(kind: p)], ""), + } + } +} + +// NAMED FOR PLANNING RATHER THAN ACTUATION, BECAUSE THAT IS WHAT IT DECIDES. A predicate called +// is_actuated over a function that actuates nothing is the same fabrication one layer out. +fn capacity_control_is_planned(outcome: CapacityControlOutcome) -> Bool { + match outcome { + ControlPlanned { roster_edit: _ } => true + ControlUnbound { axis: _, trigger: _ } => false + ControlRejected { reason: _ } => false + } +} + +fn capacity_control_outcome_line(outcome: CapacityControlOutcome) -> String { + match outcome { + ControlPlanned { roster_edit: e } => join(["plan: ", e], "") + ControlUnbound { axis: a, trigger: t } => + join(["not wired on this build -- axis: ", a as String, "; needs: ", t as String], "") + ControlRejected { reason: r } => join(["rejected: ", r as String], "") + } +} diff --git a/dag/gunbc/fleet_capacity_panel.dag b/dag/gunbc/fleet_capacity_panel.dag new file mode 100644 index 00000000000..3d3613affef --- /dev/null +++ b/dag/gunbc/fleet_capacity_panel.dag @@ -0,0 +1,223 @@ +module gunbc.fleet_capacity_panel + +import std.types { String, NonEmptyStr, Bool, List, Int } +import std.markup { Fragment } +import std.measure { ByteSize, byte_size_count } +import gunbc.site.markup { txt, el_class } +import extdeps.languages.css.values { css_ch, css_length_wire } +import product.placement_supply { HostIdentity } +import extdeps.llm.cli_lifecycle { ProviderKind, provider_kind_label } +import gunbc.runner_slot_allocation { + gunbc_runner_slots_per_host, gunbc_runner_slot_desired, host_width_binding_label, +} +import gunbc.fleet_capacity_control { + capacity_controlled_hosts, capacity_controlled_providers, + host_withdrawal_for, provider_withdrawal_for, + withdrawal_cause_label, withdrawal_cause_detail, + active_host_count, active_provider_count, +} + +// THE FLEET CAPACITY PANEL ON THE DAILY WORKSPACE. +// +// It reads gunbc.fleet_capacity_control -- the SAME roster the dispatch gate reads -- rather than +// a display copy. That is the whole difference between a control and a cockpit: a panel with its +// own roster drifts from the thing it claims to steer, and the drift is invisible because both +// sides look internally consistent. +data fleet_capacity_panel_note: String = "Daily-workspace panel over declared fleet capacity. Reads gunbc.fleet_capacity_control directly so the panel and the dispatch gate cannot disagree." + +// EVERY NUMBER HERE IS DECLARED, NOT OBSERVED, AND THE PANEL SAYS SO IN THE RENDERED OUTPUT. +// +// This is not caution, it is the difference between two facts that look identical on a screen. +// gunbc.runner_slot_allocation states plainly that srv3 and srv4's committed width of 6 is a +// PROVISIONING TARGET -- two slots that do not exist yet -- while srv1 and srv2's 5 matches live. +// A panel rendering "6 slots" beside "5 slots" with no qualifier invites the reader to conclude the +// fleet is running 22, and a capacity decision made on that number would be wrong on the only axis +// the panel exists to inform. Labelling the column "committed" costs one word and removes the +// class of error entirely. +data fleet_capacity_panel_declared_note: String = "Widths are committed allocations, not observed incarnations. srv3/srv4 commit 6 while running 5 (runner_slot_allocation gunbc_runner_slot_width_ruling_note): the model leads the fleet on that axis." + +// THE PANEL NAMES WHICH AXIS BOUND EACH HOST, BECAUSE THE TOTAL CANNOT SAY IT AND THE REMEDIES +// DIFFER. A committed width is a minimum over axes, and the number that survives says nothing +// about what would buy more. The axes are not interchangeable purchases: where memory binds the +// answer is DIMMs, where cores bind it is a different machine entirely, and a reader given only a +// fleet total assumes one story across four hosts. +// +// THIS IS ABOUT TO MATTER MUCH MORE THAN IT DOES TODAY. Measured now, memory binds everywhere and +// the rows agree, so the column looks redundant. Once the CPU axis lands (gunbc#8976) srv1/srv3/ +// srv4 become core-bound at 21 while srv2 stays memory-bound at 5 -- its 64 GiB DIMM install +// failed training and was reverted, so it holds 8x16 GiB where the others hold 8x64 -- and the +// single total becomes two unrelated stories. The column is authored before that lands rather than +// after someone reads the total wrong. +data fleet_capacity_panel_binding_axis_note: String = "Each host row names its binding axis. A committed width is a minimum over axes and the surviving number cannot say which one bound it; the remedies differ per axis and per host." + +fn gib_label(bytes: ByteSize) -> String { + join([to_string(byte_size_count(b: bytes) / 1073741824), " GiB"], "") +} + +fn host_standing_label(host: HostIdentity) -> String { + match host_withdrawal_for(host: host) { + Present { value: w } => + join(["withdrawn · ", withdrawal_cause_label(cause: w.cause), " · ", + withdrawal_cause_detail(cause: w.cause) as String], "") + Absent => "active" + } +} + +fn provider_standing_label(provider: ProviderKind) -> String { + match provider_withdrawal_for(provider: provider) { + Present { value: w } => + join(["withdrawn · ", withdrawal_cause_label(cause: w.cause), " · ", + withdrawal_cause_detail(cause: w.cause) as String], "") + Absent => "active" + } +} + +fn host_standing_class(host: HostIdentity) -> String { + match host_withdrawal_for(host: host) { + Present { value: _ } => "capacity-row capacity-withdrawn" + Absent => "capacity-row capacity-active" + } +} + +fn provider_standing_class(provider: ProviderKind) -> String { + match provider_withdrawal_for(provider: provider) { + Present { value: _ } => "capacity-row capacity-withdrawn" + Absent => "capacity-row capacity-active" + } +} + +fn fleet_committed_slot_total() -> Int { + fold(capacity_controlled_hosts(), init: 0, f: (acc, h) => { + match host_withdrawal_for(host: h) { + Present { value: _ } => acc + Absent => acc + gunbc_runner_slots_per_host(host: h) + } + }) +} + +// A WITHDRAWN HOST CONTRIBUTES ZERO TO THE ACTIVE TOTAL, WHICH IS THE POINT OF THE TOTAL. +// Summing every host's committed width regardless of standing would report capacity the operator +// has explicitly taken out of service, which is the number they turned the control to change. +fn fleet_committed_slot_total_ignoring_withdrawals() -> Int { + fold(capacity_controlled_hosts(), init: 0, f: (acc, h) => { + acc + gunbc_runner_slots_per_host(host: h) + }) +} + +fn host_capacity_row(host: HostIdentity) -> Fragment { + el_class("div", host_standing_class(host: host), [ + el_class("span", "capacity-subject", [txt(host as String)]), + el_class("span", "capacity-metric", [ + txt(join([to_string(gunbc_runner_slots_per_host(host: host)), + " slots committed"], "")), + ]), + el_class("span", "capacity-metric", [ + txt(join([gib_label(bytes: gunbc_runner_slot_desired().memory_max), "/slot"], "")), + ]), + el_class("span", "capacity-metric", [txt(host_width_binding_label(host: host))]), + el_class("span", "capacity-standing", [txt(host_standing_label(host: host))]), + ]) +} + +fn provider_capacity_row(provider: ProviderKind) -> Fragment { + el_class("div", provider_standing_class(provider: provider), [ + el_class("span", "capacity-subject", [txt(provider_kind_label(kind: provider))]), + el_class("span", "capacity-metric", [txt("runtime")]), + el_class("span", "capacity-standing", [txt(provider_standing_label(provider: provider))]), + ]) +} + +fn fleet_capacity_summary_line() -> String { + join([ + to_string(active_host_count()), " of ", + to_string(capacity_controlled_hosts() |> count), " hosts · ", + to_string(active_provider_count()), " of ", + to_string(capacity_controlled_providers() |> count), " runtimes · ", + to_string(fleet_committed_slot_total()), " slots committed", + ], "") +} + +// THE SUMMARY REPORTS WITHDRAWN CAPACITY ONLY WHEN THERE IS SOME. +// +// A standing "0 withdrawn" line is noise on every ordinary day and trains the reader to skip the +// row where the number finally matters. Absent means nothing is withdrawn, which is the same thing +// the per-host rows already say -- this line exists to make a NON-ZERO state impossible to miss. +fn fleet_capacity_withdrawn_line() -> String? { + let withdrawn = fleet_committed_slot_total_ignoring_withdrawals() - fleet_committed_slot_total() + if withdrawn > 0 { + Present { + value: join([to_string(withdrawn), " slots withdrawn by operator control"], ""), + } + } else { + none + } +} + +fn fleet_capacity_withdrawn_nodes() -> List { + match fleet_capacity_withdrawn_line() { + Present { value: line } => [el_class("div", "capacity-withdrawn-total", [txt(line)])] + Absent => [] + } +} + +// THE TWO COLUMN RESERVATIONS ARE DERIVED FROM THE LABELS THEY MUST HOLD, NOT PICKED. +// +// An earlier revision wrote min-width: 5rem and 9rem, which were the only untokened lengths in the +// stylesheet and would have needed re-tuning by eye every time a host name or a metric phrase grew. +// This follows roadmap_component dispatch_reserved_width exactly: reserve the longest string the +// column can actually wear, plus a gutter, so a new host or a longer binding-axis phrase moves the +// reservation by derivation and there is no pixel to maintain. +data capacity_column_ch_gutter: Int = 2 + +fn capacity_longest_len(labels: List) -> Int { + fold(labels, init: 0, f: (acc, l) => + if string_length(s: l) > acc { string_length(s: l) } else { acc }) +} + +fn capacity_subject_labels() -> List { + concat( + map(capacity_controlled_hosts(), h => h as String), + map(capacity_controlled_providers(), p => provider_kind_label(kind: p)), + ) +} + +fn capacity_metric_labels() -> List { + concat( + map(capacity_controlled_hosts(), h => + join([to_string(gunbc_runner_slots_per_host(host: h)), " slots committed"], "")), + map(capacity_controlled_hosts(), h => host_width_binding_label(host: h)), + ) +} + +fn capacity_subject_reserved_width() -> String { + css_length_wire(l: css_ch(n: capacity_longest_len(labels: capacity_subject_labels()) + + capacity_column_ch_gutter)) +} + +fn capacity_metric_reserved_width() -> String { + css_length_wire(l: css_ch(n: capacity_longest_len(labels: capacity_metric_labels()) + + capacity_column_ch_gutter)) +} + +fn fleet_capacity_panel() -> Fragment { + el_class("section", "fleet-capacity-panel", concat( + [ + el_class("h2", "capacity-title", [txt("fleet capacity")]), + el_class("div", "capacity-summary", [txt(fleet_capacity_summary_line())]), + ], + concat( + fleet_capacity_withdrawn_nodes(), + concat( + map(capacity_controlled_hosts(), h => host_capacity_row(host: h)), + concat( + map(capacity_controlled_providers(), p => provider_capacity_row(provider: p)), + [ + el_class("div", "capacity-declared-note", [ + txt("committed allocations, not observed incarnations — srv3/srv4 commit 6 while running 5"), + ]), + ], + ), + ), + ), + )) +} diff --git a/dag/gunbc/fleet_converge_plan.dag b/dag/gunbc/fleet_converge_plan.dag index 4dc9e641499..1bcb9ff22f5 100644 --- a/dag/gunbc/fleet_converge_plan.dag +++ b/dag/gunbc/fleet_converge_plan.dag @@ -49,6 +49,7 @@ import gunbc.membership_reconcile { membership_reconcile, membership_plan_admitting_outcome, membership_refusal_count, + membership_added_count, } import gunbc.ownership { Ownership, Owned } import gunbc.spark.serving_execution_schedule { ScheduledRows, scheduled_rows_empty, scheduled_rows_list } @@ -79,6 +80,24 @@ import gunbc.host_converge { systemd_tasks_max_property, } import gunbc.runner_slot_allocation { gunbc_runner_slot_desired } +import gunbc.runner_slot_provision { + RunnerSlotMember, + RunnerSlotMemberAt, + runner_slot_member_key, + runner_slot_provision_plan, + RunnerSlotProvisionPlan, +} +import extdeps.github.actions_runner { + actions_runner_release_2_334_0, + actions_runner_binary_artifact_for_arch, +} +import extdeps.cpu.ampere { altra_max_m12830_catalog } +import product.placement_supply { HostIdentity } +import gunbc.runner_host_deploy { + RunnerHostDeployFound, + RunnerHostDeployUnmodeled, + runner_host_deploy_for, +} import gunbc.spark.serving_membership { SparkServingMember, SparkServingMemberAt, @@ -117,6 +136,7 @@ fn fleet_converge_plan_subject( observed_timers: List, observed_caps: List, observed_spark: List, + observed_slots: List, ) -> FleetConvergePlanSubject { FleetConvergePlanSubject { host: host, @@ -125,6 +145,7 @@ fn fleet_converge_plan_subject( observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ), } } @@ -134,6 +155,7 @@ fn fleet_converge_member_set_fingerprint( observed_timers: List, observed_caps: List, observed_spark: List, + observed_slots: List, ) -> ContentHash { content_hash_of_value( value: observed_baseline_text( @@ -141,6 +163,7 @@ fn fleet_converge_member_set_fingerprint( observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ) as NonEmptyStr, ) } @@ -155,6 +178,7 @@ fn fleet_converge_apply_subject_admits( observed_timers: List, observed_caps: List, observed_spark: List, + observed_slots: List, ) -> Bool { fleet_converge_apply_subject_host_matches(planned_host: planned_subject.host, observed_host: observed_host) && compare_content_hash( @@ -164,6 +188,7 @@ fn fleet_converge_apply_subject_admits( observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ), ) == ContentHashEqual } @@ -198,6 +223,7 @@ fn fleet_converge_member_set_fingerprint_matches( observed_timers: List, observed_caps: List, observed_spark: List, + observed_slots: List, ) -> Bool { trim(s: planned_fingerprint_text) == ( serialize_content_hash( @@ -206,6 +232,7 @@ fn fleet_converge_member_set_fingerprint_matches( observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ), ) as String ) @@ -308,6 +335,133 @@ fn membership_plan_lines_cap(plan: MembershipPlan) -> Li map(plan.actions, a => cap_action_line(action: a)) } +data slot_family_is_the_third_member_family_note: String = "THE SLOT ROSTER IS RECONCILED HERE RATHER THAN STOOD UP BY A SEPARATE SCRIPT, which is the whole point of the consolidation (operator directive 2026-08-22: this all belongs in fleet convergence). Timers and caps already flowed through membership_reconcile and slot standup did not, so the fleet had two ways to change a host: a reviewed plan artifact with a lease, a member-set fingerprint and a CAS against the observed baseline, and a hand-run provisioning path with none of those. A width change landing through the second one is unreviewed by construction.\n\nDESIRED COMES FROM THE DEPLOY ROW AND THE DEPLOY ROW DERIVES ITS WIDTH, so the roster this plan proposes is the width the admission axes committed -- not a number authored beside them. An unmodeled host emits a REFUSED line and no actions; it does not fall through to zero desired members, because zero desired against a populated host reconciles to REMOVE EVERY SLOT, which is the absorbing failure arm pointed the destructive direction.\n\nOBSERVATION REFUSAL IS UPSTREAM. gunbc.runner_slot_provision RunnerSlotsUnobserved is resolved by the caller before it reaches this module; a List arriving here has already been established to be a genuine reading of the host rather than an unread one rendered as empty." + +fn slot_action_line(action: MemberAction) -> String { + match action { + MemberAdded { at: _, to: m } => concat("ADD runner-slot ", runner_slot_member_key(m: m) as String) + MemberChanged { at: _, from: f, to: t } => + concat( + concat("CHANGE runner-slot ", runner_slot_member_key(m: f) as String), + concat(" -> ", runner_slot_member_key(m: t) as String), + ) + MemberRemoved { at: _, from: m } => concat("REMOVE runner-slot ", runner_slot_member_key(m: m) as String) + MemberRemovalRefused { from: m, cause: c } => + concat( + concat("REFUSED-REMOVAL runner-slot ", runner_slot_member_key(m: m) as String), + concat(" cause=", teardown_refusal_cause_label(cause: c)), + ) + MemberRosterDuplicateKeyRefused { roster: _, first: _, duplicate: _ } => "REFUSED-DUPLICATE-KEY" + } +} + +type FleetConvergeSlotFamily + = SlotFamilyPlanned { plan: RunnerSlotProvisionPlan } + | SlotFamilyUnmodeledHost { host: HostIdentity } + | SlotFamilyArtifactUnpublished { host: HostIdentity } + +// ONE RESOLUTION FEEDS BOTH THE REVIEW LINES AND THE APPLY SCRIPT, which is not tidiness -- it is +// the property the whole plan/apply split rests on. If the renderer and the actuator each resolved +// the host and reconciled the roster on their own, the reviewer could approve one membership and +// apply could execute a different one, and the bundle hash would not catch it because both halves +// would be internally consistent. Resolving once and deriving both projections makes that +// disagreement unrepresentable rather than checked. +fn fleet_converge_slot_family( + host: NonEmptyStr, + observed_slots: List, +) -> FleetConvergeSlotFamily { + match runner_host_deploy_for(host: host as HostIdentity) { + RunnerHostDeployUnmodeled { host: h } => SlotFamilyUnmodeledHost { host: h } + RunnerHostDeployFound { deploy: d } => + match actions_runner_binary_artifact_for_arch( + binary_release: actions_runner_release_2_334_0, + arch: altra_max_m12830_catalog.architecture, + ) { + Absent => SlotFamilyArtifactUnpublished { host: host as HostIdentity } + Present { value: a } => + SlotFamilyPlanned { + plan: runner_slot_provision_plan(deploy: d, artifact: a, observed: observed_slots), + } + } + } +} + +fn fleet_converge_slot_lines( + host: NonEmptyStr, + observed_slots: List, +) -> List { + match fleet_converge_slot_family(host: host, observed_slots: observed_slots) { + SlotFamilyUnmodeledHost { host: h } => + [concat("REFUSED-UNMODELED-HOST runner-slot host=", h as String)] + SlotFamilyArtifactUnpublished { host: h } => + [concat("REFUSED-NO-PUBLISHED-RUNNER-BINARY runner-slot host=", h as String)] + SlotFamilyPlanned { plan: p } => map(p.membership.actions, a => slot_action_line(action: a)) + } +} + +// SLOT ADD IS THE ONE MEMBER FAMILY THIS SCRIPT ACTUALLY EXECUTES BESIDE TIMER TEARDOWN, and the +// reason is principal, not appetite. Cap drop-ins live under /etc/systemd and belong to the +// deploy principal (fleet_converge_cap_apply_shell_note); slot directories live under the runner +// user's own /opt/actions-runner, which is exactly the principal converge already runs as. So +// emitting ADD here is converge acting within its own authority rather than reaching outside it. +// +// REMOVE AND CHANGE EMIT NOTHING, AND THAT IS THE FAIL-CLOSED ARM RATHER THAN AN OVERSIGHT. +// gunbc.runner_slot_provision runner_slot_member_ownership returns Absent for every observed slot +// because no provenance signal exists yet to tell a gunbc-managed directory from one somebody put +// there by hand. Reconcile therefore yields MemberRemovalRefused rather than MemberRemoved, those +// refusals ARE rendered into plan.txt for the reviewer, and nothing deletes a directory whose +// ownership was never established. Teardown becomes emittable when the provenance signal lands, +// not before. +// +// AN UNMODELED HOST STOPS THE SCRIPT RATHER THAN CONTRIBUTING NO LINES. Silence here would be +// indistinguishable from "this host had nothing to do", so apply would report success for a host it +// could not identify -- the fabricated plausible output at the actuation seam. The emitted exit is +// the line-stop. +// AN UNMODELED HOST COUNTS AS A REFUSAL RATHER THAN AS ZERO REFUSALS. Zero is what a reviewer reads +// as "nothing was refused on this axis", and a host nobody modeled is the largest refusal the slot +// family can produce -- so reporting it as zero would make the most severe state look like the +// cleanest one. +fn fleet_converge_slot_refusal_count( + host: NonEmptyStr, + observed_slots: List, +) -> Int { + match fleet_converge_slot_family(host: host, observed_slots: observed_slots) { + SlotFamilyUnmodeledHost { host: _ } => 1 + SlotFamilyArtifactUnpublished { host: _ } => 1 + SlotFamilyPlanned { plan: p } => membership_refusal_count(plan: p.membership) + } +} + +fn slot_apply_lines( + host: NonEmptyStr, + observed_slots: List, +) -> List { + match fleet_converge_slot_family(host: host, observed_slots: observed_slots) { + SlotFamilyUnmodeledHost { host: h } => + [ + concat( + "echo 'fleet_converge_apply: REFUSED-UNMODELED-HOST runner-slot host=", + concat(h as String, "' >&2"), + ), + "exit 1", + ] + SlotFamilyArtifactUnpublished { host: h } => + [ + concat( + "echo 'fleet_converge_apply: REFUSED-NO-PUBLISHED-RUNNER-BINARY runner-slot host=", + concat(h as String, "' >&2"), + ), + "exit 1", + ] + SlotFamilyPlanned { plan: p } => + if membership_added_count(plan: p.membership) == 0 { + ["# runner-slot: no slots to add"] + } else { + concat([p.base_dir_script], p.upsert_extract_scripts) + } + } +} + fn fleet_converge_desired_caps() -> List { let slot = gunbc_runner_slot_desired() [ @@ -351,6 +505,7 @@ fn observed_baseline_text( observed_timers: List, observed_caps: List, observed_spark: List, + observed_slots: List, ) -> String { join( concat( @@ -359,10 +514,13 @@ fn observed_baseline_text( map(observed_timers, m => concat("timer:", m.unit_name as String)), ), concat( - map(observed_caps, c => concat("cap:", c.dropin_path as String, "=", c.content)), - map(observed_spark, m => concat( - "spark:", spark_serving_member_key(member: m), "=", m.state_digest as String, - )), + concat( + map(observed_caps, c => concat("cap:", c.dropin_path as String, "=", c.content)), + map(observed_spark, m => concat( + "spark:", spark_serving_member_key(member: m), "=", m.state_digest as String, + )), + ), + map(observed_slots, m => concat("slot:", runner_slot_member_key(m: m) as String)), ), ), "\n", @@ -1022,18 +1180,24 @@ fn fleet_converge_locked_apply_script( ]) } -fn fleet_converge_apply_shell(timer_plan: MembershipPlan) -> String { +fn fleet_converge_apply_shell( + timer_plan: MembershipPlan, + host: NonEmptyStr, + observed_slots: List, +) -> String { join( concat( [ concat("# ", dissolution_description(condition: fleet_converge_apply_shell_emit_dissolution_trigger)), concat("# ", fleet_converge_cap_apply_shell_note), - "# Admission gates enforced in fleet_converge_apply_wet before bash — this script runs timer teardown only", + "# Admission gates enforced in fleet_converge_apply_wet before bash — this script runs timer teardown and runner-slot ADD", "set -euo pipefail", ], ["# generated at plan time — apply MUST NOT recompute membership_reconcile"], timer_apply_lines(plan: timer_plan), ["sudo -n systemctl daemon-reload"], + ["# runner-slot membership (gunbc.runner_slot_provision) — ADD only; see slot_apply_lines"], + slot_apply_lines(host: host, observed_slots: observed_slots), ), "\n", ) @@ -1045,12 +1209,14 @@ fn fleet_converge_plan_artifact( observed_timers: List, observed_caps: List, observed_spark: List, + observed_slots: List, ) -> FleetConvergePlanArtifact? { let subject = fleet_converge_plan_subject( host: host, observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ) let timer_plan = timer_retirement_plan(observed: observed_timers) let cap_plan = caps_reconcile(desired: fleet_converge_desired_caps(), observed: observed_caps) @@ -1061,6 +1227,7 @@ fn fleet_converge_plan_artifact( observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ) let planned_generation = prior_generation + 1 let body = join( @@ -1081,7 +1248,10 @@ fn fleet_converge_plan_artifact( timer_lines, ["# cap-axis"], cap_lines, + ["# runner-slot"], + fleet_converge_slot_lines(host: host, observed_slots: observed_slots), [ + concat("# slot-refusals=", to_string(fleet_converge_slot_refusal_count(host: host, observed_slots: observed_slots))), concat("# cap-refusals=", to_string(membership_refusal_count(plan: cap_plan))), concat("# timer-refusals=", to_string(membership_refusal_count(plan: timer_plan))), ], @@ -1094,7 +1264,11 @@ fn fleet_converge_plan_artifact( prior_generation: prior_generation, owner_fingerprint: owner_fp, ) - let apply_shell = fleet_converge_apply_shell(timer_plan: timer_plan) + let apply_shell = fleet_converge_apply_shell( + timer_plan: timer_plan, + host: host, + observed_slots: observed_slots, + ) match content_hash_of_value(value: baseline as NonEmptyStr) { Fnv1a64(structural) => Present { @@ -1136,12 +1310,14 @@ fn fleet_converge_observed_baseline_matches( observed_timers: List, observed_caps: List, observed_spark: List, + observed_slots: List, ) -> Bool { let baseline = observed_baseline_text( host: host, observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ) match content_hash_of_value(value: baseline as NonEmptyStr) { Fnv1a64(structural) => structural.digest == observed_baseline_hex diff --git a/dag/gunbc/fleet_converge_plan_cli.dag b/dag/gunbc/fleet_converge_plan_cli.dag index 857e6accabf..6e225ead480 100644 --- a/dag/gunbc/fleet_converge_plan_cli.dag +++ b/dag/gunbc/fleet_converge_plan_cli.dag @@ -10,6 +10,11 @@ import extdeps.filesystem.filesystem_io { Filesystem } import extdeps.exec.command { ArgvCommand, LocalExec } import gunbc.command_runner { run_shell_command_capture, run_shell_commands, process_outcome_admitted } import gunbc.host_axis_caps { CapMember, caps_managed_dropin_paths } +import gunbc.runner_slot_provision { + RunnerSlotsObserved, + RunnerSlotsUnobserved, + observe_runner_slot_members_wet, +} import gunbc.fleet_converge_plan { TimerRetirementMember, fleet_converge_plan_artifact, @@ -131,12 +136,19 @@ func fleet_converge_plan_wet() -> ProcessExit GenerationAdmitted { generation: prior_generation } => { let observed_timers = observe_timer_members_wet() let observed_caps = observe_cap_members_wet() + match observe_runner_slot_members_wet() { + RunnerSlotsUnobserved { reason: why } => + exit_failure( + reason: concat("fleet_converge_plan: RunnerSlotsUnobserved — ", why as String), + ) + RunnerSlotsObserved { members: observed_slots } => match fleet_converge_plan_artifact( host: host, prior_generation: prior_generation, observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: [], + observed_slots: observed_slots, ) { Absent => exit_failure(reason: "fleet_converge_plan: observed baseline is not Fnv1a64Structural — plan refused") @@ -216,6 +228,7 @@ func fleet_converge_plan_wet() -> ProcessExit } } } + } } func fleet_converge_apply_wet() -> ProcessExit @@ -265,12 +278,19 @@ func fleet_converge_apply_wet() -> ProcessExit } else { let observed_timers = observe_timer_members_wet() let observed_caps = observe_cap_members_wet() + match observe_runner_slot_members_wet() { + RunnerSlotsUnobserved { reason: why } => + exit_failure( + reason: concat("fleet_converge_apply: RunnerSlotsUnobserved — ", why as String), + ) + RunnerSlotsObserved { members: observed_slots } => if !fleet_converge_member_set_fingerprint_matches( planned_fingerprint_text: read_member_fp.content, host: observed_host, observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: [], + observed_slots: observed_slots, ) { exit_failure(reason: "fleet_converge_apply: SubjectIdentityMismatch — member set drifted since plan") } else if !fleet_converge_observed_baseline_matches( @@ -279,6 +299,7 @@ func fleet_converge_apply_wet() -> ProcessExit observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: [], + observed_slots: observed_slots, ) { exit_failure(reason: "fleet_converge_apply: ObservedBaselineMismatch — host drifted since plan; rerun plan and review") } else if !fleet_converge_plan_bundle_matches( @@ -315,4 +336,5 @@ func fleet_converge_apply_wet() -> ProcessExit } } } + } } diff --git a/dag/gunbc/roadmap_page.dag b/dag/gunbc/roadmap_page.dag index 7815abfbe60..a4334112125 100644 --- a/dag/gunbc/roadmap_page.dag +++ b/dag/gunbc/roadmap_page.dag @@ -6,6 +6,7 @@ import gunbc.site.markup { txt, el, el_class, el_attrs } import std.markdown { markdown_inlines_to_fragments } import extdeps.languages.markdown { parse_inline_markdown_minimal } import gunbc.roadmap_style { roadmap_css } +import gunbc.fleet_capacity_panel { fleet_capacity_panel } import gunbc.roadmap_model { RoadmapNode, RoadmapEdge, RoadmapNodeId, RoadmapParent, TopLevel, UnderParent, roadmap_primary_parent, is_top_level, @@ -850,9 +851,9 @@ fn roadmap_daily_workspace_page_impl_for_accepted( ]), el("body", [ roadmap_header(page: "daily workspace"), - el_class("main", "daily-workspace", concat(main_prefix, concat(program_strip, concat( + el_class("main", "daily-workspace", concat(main_prefix, concat([fleet_capacity_panel()], concat(program_strip, concat( workspace_observation_banner(observation: ws.observation), - [ workspace_markup(ws: ws) ])))), + [ workspace_markup(ws: ws) ]))))), dispatch_client_script(), ]), ], diff --git a/dag/gunbc/roadmap_style.dag b/dag/gunbc/roadmap_style.dag index d72e10ecc92..1cbc5785dd2 100644 --- a/dag/gunbc/roadmap_style.dag +++ b/dag/gunbc/roadmap_style.dag @@ -28,6 +28,9 @@ import gunbc.design.state_response { state_var_name, state_var_ref, state_rest_decl, state_paint_rules, RestBinding, StateClassBinding, } +import gunbc.fleet_capacity_panel { + capacity_subject_reserved_width, capacity_metric_reserved_width, +} import gunbc.roadmap_component { dispatch_reserved_width, theme_toggle_class, theme_toggle_reserved_width, sound_toggle_class, sound_toggle_reserved_width, @@ -486,6 +489,59 @@ fn roadmap_instance_rules_head() -> List { decl(prop: FontStyle, value: "italic"), decl(prop: FontSize, value: scale_var(t: text_12)), ] }, + StaticRule { selector: ClassSelector { name: "fleet-capacity-panel" }, decls: [ + role_decl(prop: Background, r: SurfaceRole), + decl(prop: Border, value: scale_border(w: border_1, color_var: "var(--border)")), + decl(prop: BorderRadius, value: scale_var(t: radius_3)), + decl(prop: Padding, value: scale_pair(a: space_12, b: space_16)), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-title" }, decls: [ + role_decl(prop: Color, r: TextRole), + decl(prop: FontSize, value: scale_var(t: text_13)), + decl(prop: FontWeight, value: "600"), + decl(prop: MarginBottom, value: scale_var(t: space_8)), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-summary" }, decls: [ + role_decl(prop: Color, r: TextRole), + decl(prop: FontSize, value: scale_var(t: text_13)), + decl(prop: FontFamily, value: scale_var(t: font_mono)), + decl(prop: MarginBottom, value: scale_var(t: space_8)), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-row" }, decls: [ + decl(prop: Display, value: "flex"), + decl(prop: AlignItems, value: "center"), + decl(prop: Gap, value: scale_var(t: space_12)), + decl(prop: FontSize, value: scale_var(t: text_12)), + decl(prop: FontFamily, value: scale_var(t: font_mono)), + decl(prop: Padding, value: scale_pair(a: space_1, b: space_4)), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-subject" }, decls: [ + role_decl(prop: Color, r: TextRole), + decl(prop: FontWeight, value: "600"), + decl(prop: MinWidth, value: capacity_subject_reserved_width()), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-metric" }, decls: [ + role_decl(prop: Color, r: TextDimRole), + decl(prop: MinWidth, value: capacity_metric_reserved_width()), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-standing" }, decls: [ + role_decl(prop: Color, r: TextDimRole), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-withdrawn" }, decls: [ + decl(prop: Opacity, value: "0.6"), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-withdrawn-total" }, decls: [ + role_decl(prop: Color, r: TextRole), + decl(prop: FontSize, value: scale_var(t: text_12)), + decl(prop: FontWeight, value: "600"), + decl(prop: MarginBottom, value: scale_var(t: space_8)), + ] }, + StaticRule { selector: ClassSelector { name: "capacity-declared-note" }, decls: [ + role_decl(prop: Color, r: TextDimRole), + decl(prop: FontSize, value: scale_var(t: text_12)), + decl(prop: FontStyle, value: "italic"), + decl(prop: MarginTop, value: scale_var(t: space_8)), + ] }, StaticRule { selector: ClassSelector { name: "daily-workspace" }, decls: [ decl(prop: Padding, value: scale_pair(a: space_16, b: space_24)), decl(prop: MaxWidth, value: scale_var(t: measure_page)), diff --git a/dag/gunbc/runner_host_deploy.dag b/dag/gunbc/runner_host_deploy.dag index c9c930f651e..9ff78ac1cff 100644 --- a/dag/gunbc/runner_host_deploy.dag +++ b/dag/gunbc/runner_host_deploy.dag @@ -18,7 +18,7 @@ import gunbc.fleet_intent { fleet_intent_known_hosts } import product.placement_supply { HostIdentity } import gunbc.build_cache_instance { runner_slot_index_suffix } import gunbc.runner_slot_allocation { gunbc_runner_slots_per_host } -import gunbc.fleet_intent_network { operator_host_srv3, operator_host_srv4 } +import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4 } data runner_host_deploy_citation: String = "VOID CITATION RETIRED (operator ruling 2026-08-06): ctrl:scripts/session-dashboard/host/* path literals and void_note twins were deleted — ctrl is a dead repo, not a live upstream. Runner slot materialization is owned in gunbc.runner_slot_provision / gunbc.runner_lifecycle on host_effect_apply. runner_host_installer_command_argv remains a legacy argv builder taking installer_path as a parameter; it is not an authority row citing ctrl." @@ -49,7 +49,27 @@ type RunnerHostDeploy { data srv4_runner_count_disk_cap_note: String = "srv4's historical five-slot pin is RETIRED (operator ruling 2026-08-06). runner_count on srv4_runner_host_deploy now names the materialization target width (6 after the 2026-08-17 16GiB ruling, matching srv3), and disk binding moves to APPLY-TIME preflight in gunbc.runner_lifecycle runner_width_disk_preflight — not a silent row pin and never an absorbing fallback to 5 when disk is unobservable.\n\nFACT unchanged: NVMe is a Samsung 970 EVO 500GB against 2TB on srv1-3; every ephemeral runner keeps a _work tree plus caches. gunbc.runner_lifecycle runner_slot_disk_budget_per_slot (~38GB per slot; the charge is per-slot, so the total demanded at apply falls with the 2026-08-17 move from width 7 to 6) is the conservative charge used at apply; sufficient observed headroom proceeds, insufficient REFUSES, unobservable REFUSES.\n\ngunbc.ci_runner_placement still models RAM only for solver admission; memory admits 6 for srv4 at the 16GiB slot (7 at the superseded 14GiB slot). The disk gate is no longer this note or host_disk_admitted_width reading runner_count as a cap — it is the observed preflight arm vivid-eagle-131's apply_wet path must invoke before slot ADD." -data runner_count_derives_from_committed_width_note: String = "runner_count IS DERIVED, NOT AUTHORED, AND THAT CLOSES A FORK THAT WOULD HAVE SILENTLY EATEN A WIDTH CHANGE. These rows carried a literal 6 while gunbc.runner_slot_allocation gunbc_runner_slots_per_host independently answered the same question -- how many slots does this host carry -- so one concept had two authorings and the deploy side was the one nobody re-derived. The cost was not hypothetical: the 2026-08-23 CPU-axis change moved committed width to 21 on srv3 and srv4, and with the literal in place PROVISIONING WOULD STILL HAVE STOOD UP SIX. The allocation model and the materialization path would have disagreed about the fleet with no diagnostic anywhere, which is exactly the roster-versus-prose failure gunbc.runner_slot_allocation width_is_a_minimum_over_axes_note records for srv4.\n\nTHE DIRECTION IS DELIBERATE. Width is decided by the conservation and admission axes and materialization CONSUMES that decision; a deploy row is not a place to re-decide it. The disk question that the old srv4 note worried about is unaffected and still lives where it belongs -- apply-time gunbc.runner_lifecycle runner_width_disk_preflight refuses on insufficient or unobservable headroom rather than lowering the count here.\n\nsrv1 AND srv2 STILL HAVE NO DEPLOY ROW AT ALL. That is pre-existing and is NOT closed by this change: only srv3 and srv4 are modeled for materialization, so srv1's move from five slots to twenty-one has no provisioning path in this module even after this correction. Recorded here rather than left to be discovered, because a reader seeing two derived rows may reasonably assume the fleet is covered." +data runner_count_derives_from_committed_width_note: String = "runner_count IS DERIVED, NOT AUTHORED, AND THAT CLOSES A FORK THAT WOULD HAVE SILENTLY EATEN A WIDTH CHANGE. These rows carried a literal 6 while gunbc.runner_slot_allocation gunbc_runner_slots_per_host independently answered the same question -- how many slots does this host carry -- so one concept had two authorings and the deploy side was the one nobody re-derived. The cost was not hypothetical: the 2026-08-23 CPU-axis change moved committed width to 21 on srv3 and srv4, and with the literal in place PROVISIONING WOULD STILL HAVE STOOD UP SIX. The allocation model and the materialization path would have disagreed about the fleet with no diagnostic anywhere, which is exactly the roster-versus-prose failure gunbc.runner_slot_allocation width_is_a_minimum_over_axes_note records for srv4.\n\nTHE DIRECTION IS DELIBERATE. Width is decided by the conservation and admission axes and materialization CONSUMES that decision; a deploy row is not a place to re-decide it. The disk question that the old srv4 note worried about is unaffected and still lives where it belongs -- apply-time gunbc.runner_lifecycle runner_width_disk_preflight refuses on insufficient or unobservable headroom rather than lowering the count here.\n\nsrv1 AND srv2 NOW HAVE ROWS, closing the gap this note declared on 2026-08-23. All four hosts are modeled for materialization and every row derives its width from the same authority, so the fleet is covered rather than partially covered." + +data legacy_pair_deploy_rows_note: String = "srv1 AND srv2 ARE MODELED FOR MATERIALIZATION AS OF 2026-08-23, closing a gap that made the width authority unactionable on half the fleet. Until this row pair existed only srv3 and srv4 had deploy rows, so gunbc_runner_slots_per_host could say srv1 carries twenty-one slots and NOTHING COULD ACT ON IT -- the number was real and there was no provisioning target to hand it to.\n\nTHE ADDRESSES ARE MEASURED, NOT ASSUMED. Both were read over SSH on 2026-08-23 by connecting and asking the host its own name: srv1 answers at 192.168.1.185 and srv2 at 192.168.1.188. That matters because this lane started the night with 192.168.1.183 and .184 for these two, which are their BMC addresses rather than their host addresses, and an ssh_target pointing at a management controller would fail in a way that looks like an unreachable host rather than a wrong row.\n\nBOTH CARRY INTERACTIVE SESSIONS AND THAT IS ALREADY PRICED. gunbc.session_residency places session containers on exactly these two hosts, and the conservation wall charges each of them a sessions slice out of the same RAM before any width is admitted -- which is why srv2 commits five where srv3 and srv4 commit twenty-one. Nothing here re-decides that; the row consumes the width the admission axes produced.\n\nsrv1 AND srv2 DIFFER FROM EACH OTHER FOR A HARDWARE REASON, not a policy one: srv1 took the 64 GiB DIMM upgrade and srv2's failed memory training and was reverted, so srv1 is bound by cores at twenty-one and srv2 by memory at five. Two rows that look identical here resolve to very different widths, and that is the derivation working rather than an inconsistency." + +data srv1_runner_host_deploy: RunnerHostDeploy = RunnerHostDeploy { + host_label: "srv1", + ssh_target: "briansrls@192.168.1.185", + runner_user: "briansrls", + job_user: "ghrunner", + app: gunbc_ci_github_app, + runner_count: gunbc_runner_slots_per_host(host: operator_host_srv1), +} + +data srv2_runner_host_deploy: RunnerHostDeploy = RunnerHostDeploy { + host_label: "srv2", + ssh_target: "briansrls@192.168.1.188", + runner_user: "briansrls", + job_user: "ghrunner", + app: gunbc_ci_github_app, + runner_count: gunbc_runner_slots_per_host(host: operator_host_srv2), +} data srv3_runner_host_deploy: RunnerHostDeploy = RunnerHostDeploy { host_label: "srv3", @@ -69,6 +89,33 @@ data srv4_runner_host_deploy: RunnerHostDeploy = RunnerHostDeploy { runner_count: gunbc_runner_slots_per_host(host: operator_host_srv4), } +type RunnerHostDeployResolution + = RunnerHostDeployFound { deploy: RunnerHostDeploy } + | RunnerHostDeployUnmodeled { host: HostIdentity } + +data runner_host_deploy_for_refuses_note: String = "AN UNMODELED HOST REFUSES RATHER THAN BORROWING A NEIGHBOUR'S ROW. This dispatch is the seam where a width becomes a provisioning target, and the tempting failure arm is to hand an unclassified host whichever row is nearest -- which would provision it against another machine's ssh_target, runner user and slot count. RunnerHostDeployUnmodeled names the host and carries no deploy, so a caller cannot proceed by accident; the four enrolled hosts are the whole population and a fifth is a row someone must author, not a default someone inherits.\n\nThis mirrors gunbc.runner_slot_allocation gunbc_runner_slots_per_host_unknown_note, which answers zero slots for an unknown host on the same reasoning: an unclassified machine is unknown, not typical." + +fn runner_host_deploy_for(host: HostIdentity) -> RunnerHostDeployResolution { + if (host as String) == (operator_host_srv1 as String) { + RunnerHostDeployFound { deploy: srv1_runner_host_deploy } + } else if (host as String) == (operator_host_srv2 as String) { + RunnerHostDeployFound { deploy: srv2_runner_host_deploy } + } else if (host as String) == (operator_host_srv3 as String) { + RunnerHostDeployFound { deploy: srv3_runner_host_deploy } + } else if (host as String) == (operator_host_srv4 as String) { + RunnerHostDeployFound { deploy: srv4_runner_host_deploy } + } else { + RunnerHostDeployUnmodeled { host: host } + } +} + +data fleet_runner_host_deploys: List = [ + srv1_runner_host_deploy, + srv2_runner_host_deploy, + srv3_runner_host_deploy, + srv4_runner_host_deploy, +] + // runner_count names slots via runner_instance_names / runner_index_seq but does NOT reach // runner_host_installer_command_argv — install-actions-runner.sh has no slot-count parameter // (per-host handler only). Width realization lives in gunbc.runner_slot_provision. diff --git a/dag/gunbc/runner_slot_allocation.dag b/dag/gunbc/runner_slot_allocation.dag index 8852235a90d..7c136aa2e10 100644 --- a/dag/gunbc/runner_slot_allocation.dag +++ b/dag/gunbc/runner_slot_allocation.dag @@ -109,6 +109,95 @@ fn host_cpu_admitted_width(host: HostIdentity) -> Int { data width_minimum_now_spans_three_axes_note: String = "THE MINIMUM IS OVER THREE AXES AND THE THIRD ONE IS WHY THIS CHANGE IS SAFE. Memory admits 29 on the upgraded hosts, CPU admits 21, disk admits nothing numeric, so the commitment is 21 -- and the two answers coexist under their own names instead of one of them being suppressed to keep the other honest. width_is_a_minimum_over_axes_note records what happens when they are collapsed: gunbc_runner_slots_per_host once returned the memory verdict under a name that read as the full commitment, and srv4's roster and its prose disagreed as a result.\n\nSo host_memory_admitted_width saying 29 is not a claim that 29 runners may exist. It is the true answer to the question that function asks, and it is the minimum's job -- not the literal's -- to keep the fleet from acting on it." +// WHICH AXIS ACTUALLY BOUND THE WIDTH, WHICH THE MINIMUM DISCARDS. +// +// gunbc_runner_slots_per_host takes a minimum over three axes and returns a number. That number +// cannot say what would unblock more capacity, and the answer differs per host: where memory binds +// the remedy is DIMMs, where cores bind it is a different machine, and the two are unrelated +// purchases. A reader given only the total assumes one binding axis across the fleet and plans +// against the wrong one -- which is now the live situation rather than a future one, since the CPU +// axis above makes srv1/srv3/srv4 core-bound while srv2 stays memory-bound on its reverted DIMMs. +// +// THE UNMEASURED AXIS IS REPORTED AS UNMEASURED, NOT AS ADMITTING EVERYTHING. Disk currently +// returns DiskWidthUnconstrained on every host, and this module's own reason string is explicit +// that this is "an unmeasured axis, not a measured all-clear". Rendering that as "disk admits any +// width" would turn an absence of observation into a positive clearance -- the state-space +// conflation this corpus keeps finding, where not-applicable and not-observed wear one symbol. +type WidthAxisStanding + = AxisAdmits { axis: NonEmptyStr, slots: Int } + | AxisUnmeasured { axis: NonEmptyStr, reason: NonEmptyStr } + +fn width_axis_standing_label(standing: WidthAxisStanding) -> String { + match standing { + AxisAdmits { axis: a, slots: n } => + join([a as String, " admits ", to_string(n)], "") + AxisUnmeasured { axis: a, reason: _ } => + join([a as String, " unmeasured"], "") + } +} + +fn host_width_axes(host: HostIdentity) -> List { + let memory = AxisAdmits { + axis: "memory" as NonEmptyStr, + slots: host_memory_admitted_width(host: host), + } + let cpu = AxisAdmits { + axis: "cores" as NonEmptyStr, + slots: host_cpu_admitted_width(host: host), + } + let disk = match host_disk_admitted_width(host: host) { + DiskAdmitsWidth { slots: d, provenance: _ } => + AxisAdmits { axis: "disk" as NonEmptyStr, slots: d } + DiskWidthUnconstrained { reason: r } => + AxisUnmeasured { axis: "disk" as NonEmptyStr, reason: r as NonEmptyStr } + } + [memory, cpu, disk] +} + +fn width_axis_binds_at(standing: WidthAxisStanding, committed: Int) -> Bool { + match standing { + AxisAdmits { axis: _, slots: n } => n == committed + AxisUnmeasured { axis: _, reason: _ } => false + } +} + +// THE BINDING AXES ARE THOSE SITTING AT THE COMMITTED WIDTH, AND THERE MAY BE MORE THAN ONE. +// +// Returning a single winner would have to break ties arbitrarily, and a tie is real information: +// two axes at the same number means relieving either one alone buys nothing. An unmeasured axis is +// never binding -- it cannot be, since it states no width -- which is why the predicate above +// answers false for it rather than treating absence as a bound. +fn host_binding_width_axes(host: HostIdentity) -> List { + let committed = gunbc_runner_slots_per_host(host: host) + filter(host_width_axes(host: host), a => width_axis_binds_at(standing: a, committed: committed)) +} + +fn host_width_binding_label(host: HostIdentity) -> String { + let binding = host_binding_width_axes(host: host) + let unmeasured = filter(host_width_axes(host: host), a => + match a { + AxisAdmits { axis: _, slots: _ } => false + AxisUnmeasured { axis: _, reason: _ } => true + }) + join([ + "bound by ", + join(map(binding, a => + match a { + AxisAdmits { axis: x, slots: _ } => x as String + AxisUnmeasured { axis: x, reason: _ } => x as String + }), "+"), + if (unmeasured |> count) > 0 { + join([" · ", join(map(unmeasured, a => + match a { + AxisAdmits { axis: x, slots: _ } => x as String + AxisUnmeasured { axis: x, reason: _ } => x as String + }), "+"), " unmeasured"], "") + } else { + "" + }, + ], "") +} + fn gunbc_runner_slots_per_host(host: HostIdentity) -> Int { let by_memory = host_memory_admitted_width(host: host) let by_cpu = host_cpu_admitted_width(host: host) diff --git a/dag/gunbc/runner_slot_provision.dag b/dag/gunbc/runner_slot_provision.dag index af86340e6e1..85c8d06ec31 100644 --- a/dag/gunbc/runner_slot_provision.dag +++ b/dag/gunbc/runner_slot_provision.dag @@ -1,6 +1,7 @@ module gunbc.runner_slot_provision import std.types { NonEmptyStr, String, List, Bool, Int } +import std.algebra { trim } import std.disposition { Disposition, Scaffold, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } import gunbc.membership_reconcile { @@ -16,7 +17,7 @@ import gunbc.membership_reconcile { import gunbc.ownership { Ownership } import gunbc.runner_host_deploy { RunnerHostDeploy, - runner_instance_names, + runner_index_seq, } import extdeps.github.actions_runner { ActionsRunnerBinaryArtifact, @@ -26,7 +27,18 @@ import extdeps.github.actions_runner { actions_runner_slot_extract_script, } import product.placement_supply { HostIdentity } +import gunbc.build_cache_instance { RunnerSlotIdentity, runner_slot_instance_name } +import gunbc.runner_slot_allocation { identity_is_fabric_execution_member } import gunbc.fleet_host_budget { declared_runner_count_for } +import gunbc.command_runner { + ProcessOutcome, + ProcessOutputPresent, + ProcessOutputAbsent, + ProcessRefused, + run_shell_command_capture, + LocalExec, +} +import extdeps.exec.command { ArgvCommand } // RunnerSlotProvision owns runner installation end-to-end in gunbc (operator ruling 2026-08-06: // ctrl is a dead repo; prior ctrl:install-actions-runner citations are void legacy pointers). @@ -52,7 +64,7 @@ type RunnerSlotMember { type RunnerSlotObservation = RunnerSlotsObserved { members: List } - | RunnerSlotsUnobserved { host: HostIdentity, reason: NonEmptyStr } + | RunnerSlotsUnobserved { reason: NonEmptyStr } fn runner_slot_instance_dir(instance_name: NonEmptyStr) -> NonEmptyStr { join([actions_runner_base_dir, "/", instance_name as String], "") as NonEmptyStr @@ -66,10 +78,54 @@ fn runner_slot_member_from_instance_name(instance_name: String) -> RunnerSlotMem } } +// THE FABRIC SLOT IS NOT A PROVISIONING TARGET, AND UNTIL 2026-08-23 IT WAS ONE. +// +// This mapped runner_instance_names straight through, so desired was 1..runner_count and nothing +// asked what any of those slots was FOR. gunbc.runner_slot_allocation authors srv3-06 as +// SlotServesFabricExecution, so the desired set proposed installing a GitHub Actions runner ON TOP +// OF THE FABRIC EXECUTION SLOT -- and reconcile would have seen it as an ordinary missing member, +// so apply would have done it with no refusal anywhere. +// +// That is the count-as-authority failure runner_slot_allocation exists to prevent, reintroduced one +// layer above it. Its own note records the first occurrence: purpose was derived by comparing index +// against count, so the fabric slot MOVED WITH THE WIDTH -- at width 7, srv3-07 would have become +// fabric and srv3-06 would have been silently handed back to Actions, relabelling a slot that may be +// running work. The carve was made an AUTHORED identity so a width change could not do that. This +// module then consumed the width and ignored the carve, reaching the same outcome by the other road. +// +// THE FILTER IS ON THE FABRIC ROLE, NOT ON COMMITTED MEMBERSHIP, and that choice is load-bearing. +// Filtering on runner_slot_membership would ask the allocation authority whether each index is +// within the host's committed width -- which is the same question runner_count already answered, and +// which yields ZERO desired members for any host the fleet model does not know. The reconcile +// fixtures deliberately plant their own synthetic deploy row (host_label "wfix") precisely so their +// expected counts are literals authored beside a known input rather than a restatement of the live +// fleet; routing desired through the global width authority would have silently emptied them and +// turned four exact-count fixtures green-by-vacuity. +// +// So the width still comes from the deploy row, which already derives it from +// gunbc_runner_slots_per_host, and this function removes exactly the identities that are spoken for. +// Two questions, two answers: how many slots does this host carry, and which of them are Actions +// runners. +// +// It works on INDICES rather than on rendered names, so the fabric identity is compared as an +// identity and never by parsing a slot number back out of a string it was just formatted into. +// +// CONSEQUENCE ON THE FLEET: srv3 desires twenty against a committed width of twenty-one. srv1, srv2 +// and srv4 carry no fabric member and are unchanged. fn desired_runner_slot_members(deploy: RunnerHostDeploy) -> List { + let host = deploy.host_label as HostIdentity map( - runner_instance_names(deploy: deploy), - n => runner_slot_member_from_instance_name(instance_name: n), + filter( + runner_index_seq(n: deploy.runner_count), + i => !identity_is_fabric_execution_member( + identity: RunnerSlotIdentity { host: host, slot_index: i }, + ), + ), + i => runner_slot_member_from_instance_name( + instance_name: runner_slot_instance_name( + slot: RunnerSlotIdentity { host: host, slot_index: i }, + ), + ), ) } @@ -172,3 +228,61 @@ fn runner_slot_provision_plan( fn runner_slot_provision_has_width_increase(plan: RunnerSlotProvisionPlan) -> Bool { membership_added_count(plan: plan.membership) > 0 } + +// --- observation: the third converge member family ------------------------------------------- + +data runner_slot_observation_refuses_note: String = "AN UNREADABLE HOST REFUSES; AN EMPTY HOST DOES NOT. These are different states and collapsing them is the empty-observation narrow: rendering 'I could not enumerate the slots' as 'this host has no slots' makes the reconcile propose ADDING every desired slot to a machine whose real population was never read, which on apply means installing over a live fleet. RunnerSlotsUnobserved carries the CAUSE AND NOT THE HOST, which is a correction rather than an omission: this observer runs LocalExec against whatever machine it is on and has no way to name that machine, so a host field here could only ever be fabricated. It was, briefly -- as the empty string -- and the empty string is not even a HostIdentity, so the fabrication refused to typecheck, which is the carrier shape doing the work a review would otherwise have had to do. The caller knows which host it is converging and supplies it; the observation reports only what it actually established. RunnerSlotsObserved with an empty list is a genuine answer about a genuinely empty host.\n\nTHE SIBLING FAMILIES DO NOT DRAW THIS LINE AND THAT IS THE DEFECT NOT TO COPY. gunbc.fleet_converge_plan_cli observe_cap_members_wet yields [] both when a drop-in is absent and when it cannot be read, and observe_timer_members_wet filters on a test that cannot distinguish 'no such unit' from 'could not run the test'. Those are tolerable for caps because an absent drop-in is the common real state; they are not tolerable for slots, where absent means 'provision it'.\n\nENUMERATION IS BY DIRECTORY, NOT BY PROBING THE DESIRED NAMES. Asking 'does each name I expect exist' can only ever return a subset of what I already intended, so an out-of-band slot -- one nobody desired -- would be invisible and could never be reported as MemberRemoved. Listing the base directory is what makes the observed population independent of the desired one, which is the whole point of a reconcile." + +func observe_runner_slot_members_wet() -> RunnerSlotObservation + uses net: Network +{ + match run_shell_command_capture( + command: ArgvCommand { argv: ["ls", "-1", actions_runner_base_dir] }, + transport: LocalExec, + ) { + ProcessRefused { exit_code: code, stderr: err } => + RunnerSlotsUnobserved { + reason: concat( + concat("could not enumerate ", actions_runner_base_dir), + concat(": the listing refused rather than returning an empty directory, so this host's slot population is UNKNOWN and must not be read as empty. stderr: ", err) + ) as NonEmptyStr, + } + ProcessOutputAbsent => + RunnerSlotsUnobserved { + reason: concat( + concat("enumerating ", actions_runner_base_dir), + " produced no output at all -- not an empty listing, which would be an empty string. A command that yields nothing has not answered the question, and treating it as 'no slots' would propose installing every desired slot onto a host whose population was never read." + ) as NonEmptyStr, + } + ProcessOutputPresent { text: t } => + RunnerSlotsObserved { + members: map( + filter(t.split("\n"), l => trim(s: l) != ""), + l => runner_slot_member_from_instance_name(instance_name: trim(s: l)), + ), + } + } +} + +type RunnerSlotConvergeVerdict + = RunnerSlotConvergePlanned { host: HostIdentity, plan: RunnerSlotProvisionPlan } + | RunnerSlotConvergeRefused { host: HostIdentity, reason: NonEmptyStr } + +data runner_slot_converge_verdict_note: String = "THE REFUSAL ARM IS THE REASON THIS FUNCTION EXISTS RATHER THAN CALLERS COMPOSING THE TWO HALVES THEMSELVES. A caller holding an observation and a deploy row can always pass the observed members straight into runner_slot_provision_plan, and the unobserved case would then be a list nobody looked at. Routing both through one verdict means the only way to reach a plan is to have actually read the host, and an unmodeled host or an unreadable directory produces a refusal that names which it was." + +fn runner_slot_converge_verdict( + host: HostIdentity, + deploy: RunnerHostDeploy, + artifact: ActionsRunnerBinaryArtifact, + observation: RunnerSlotObservation, +) -> RunnerSlotConvergeVerdict { + match observation { + RunnerSlotsUnobserved { reason: r } => + RunnerSlotConvergeRefused { host: host, reason: r } + RunnerSlotsObserved { members: obs } => + RunnerSlotConvergePlanned { + host: host, + plan: runner_slot_provision_plan(deploy: deploy, artifact: artifact, observed: obs), + } + } +} diff --git a/dag/gunbc/spark/serving_converge_plan.dag b/dag/gunbc/spark/serving_converge_plan.dag index 41da81d8dfd..600d2b0cef7 100644 --- a/dag/gunbc/spark/serving_converge_plan.dag +++ b/dag/gunbc/spark/serving_converge_plan.dag @@ -59,6 +59,7 @@ import gunbc.spark.serving_member_realization { spark_serving_install_effects_include, } import gunbc.spark.serving_realization { ServingInstallEffect, EnableLingerForOwnAccount } +import gunbc.runner_slot_provision { RunnerSlotMember } import gunbc.fleet_converge_plan { FleetConvergePlanArtifact, FleetConvergeSparkServingTypedAction, @@ -288,8 +289,14 @@ fn fleet_converge_spark_serving_typed_actions_in_order( fn spark_serving_fleet_converge_apply_shell( timer_plan: MembershipPlan, + host: NonEmptyStr, + observed_slots: List, ) -> String { - fleet_converge_apply_shell(timer_plan: timer_plan) + fleet_converge_apply_shell( + timer_plan: timer_plan, + host: host, + observed_slots: observed_slots, + ) } // THE FULL-POPULATION CUTOVER. This function planned a single-element linger desired list, so three @@ -408,6 +415,7 @@ fn spark_serving_fleet_converge_plan_artifact_for_release( spark_plan: full_plan, spark_rows: spark_rows, observed_spark: observed_members, + observed_slots: [], ), } } @@ -440,12 +448,14 @@ fn spark_serving_fleet_converge_plan_artifact_from_rows( spark_plan: MembershipPlan, spark_rows: ScheduledRows, observed_spark: List, + observed_slots: List, ) -> FleetConvergePlanArtifact { let subject = fleet_converge_plan_subject( host: host, observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ) let timer_plan = timer_retirement_plan(observed: observed_timers) let cap_plan = caps_reconcile(desired: fleet_converge_desired_caps(), observed: observed_caps) @@ -457,10 +467,15 @@ fn spark_serving_fleet_converge_plan_artifact_from_rows( observed_timers: observed_timers, observed_caps: observed_caps, observed_spark: observed_spark, + observed_slots: observed_slots, ) let planned_generation = prior_generation + 1 let spark_wire = fleet_converge_spark_serving_typed_actions_wire(rows: scheduled_rows_list(scheduled: spark_rows)) - let apply_shell = spark_serving_fleet_converge_apply_shell(timer_plan: timer_plan) + let apply_shell = spark_serving_fleet_converge_apply_shell( + timer_plan: timer_plan, + host: host, + observed_slots: observed_slots, + ) let body = join( concat( [ diff --git a/dag/test/claim/design_register_lift_parity_witness_test.dag b/dag/test/claim/design_register_lift_parity_witness_test.dag index 58665b89fe5..0f530a0542a 100644 --- a/dag/test/claim/design_register_lift_parity_witness_test.dag +++ b/dag/test/claim/design_register_lift_parity_witness_test.dag @@ -64,7 +64,9 @@ data roadmap_css_repin_a2_hierarchy_note: String = "Re-pinned 2026-08-02 for the data lift_parity_merge_resolution_note: String = "MERGE RESOLUTION, RE-DERIVED NOT RECONCILED (S1 x A2-hierarchy, 2026-08-03). Both branches edited this row block and each moved a DIFFERENT digest: #7701 (A2 hierarchy closeout) moved roadmap_css because it changed the stylesheet, and S1 moved moodboard_thesis_themes because it revised register_thesis. Neither touched the other's surface, so the semantic union is the resolution and no value is a compromise between two claims. The union was nonetheless not TRUSTED: both digests were re-run by execution on the merged tree, because a digest pins emitted bytes and a merge is the one moment when the bytes belong to a tree neither side ever built — picking a side by reasoning about scope is exactly the copied-measurement-as-oracle failure this file's own repin notes disclaim ('derived by execution, never chosen'). The re-run is the oracle; the reasoning above only explains why the re-run was expected to agree." -data roadmap_css_lift_parity_digest: String = "25d65c956b7578ca" +data roadmap_css_repin_fleet_capacity_panel_note: String = "Re-pinned 2026-08-23 for the daily-workspace fleet capacity panel (operator request: live fleet info on the workspace): the roadmap bytes move intentionally — the .fleet-capacity-panel family lands (panel surface, .capacity-title, .capacity-summary, .capacity-row with its active/withdrawn variants, .capacity-subject, .capacity-metric, .capacity-standing, .capacity-withdrawn-total, .capacity-declared-note), all role-routed and tokened. The two column reservations are NOT pixels: .capacity-subject and .capacity-metric take min-width from gunbc.fleet_capacity_panel capacity_subject_reserved_width and capacity_metric_reserved_width, which derive the longest label each column can wear plus a gutter — the same projection discipline roadmap_component dispatch_reserved_width uses, so a new host or a longer binding-axis phrase moves the reservation by derivation. An earlier revision of this change wrote raw 5rem/9rem, which would have been the only untokened lengths in the stylesheet. Behavioral receipts: test.claim.fleet_capacity_panel_witness_test — the panel reaches the serialized daily workspace, its widths are labelled committed rather than observed, the slot total sums the allocation authority as a relation, an unmeasured axis is not reported as binding, and the withdrawn line is absent when nothing is withdrawn. Derived by execution from this tree (roadmap_css_derived_digest run 2026-08-23); this digest only pins bytes, never chosen." + +data roadmap_css_lift_parity_digest: String = "b6df98adc93f7077" data moodboard_thesis_themes_lift_parity_digest: String = "98f0513aebb0dcb3" fn emission_content_digest(s: String) -> String { diff --git a/dag/test/claim/fleet_capacity_control_witness_test.dag b/dag/test/claim/fleet_capacity_control_witness_test.dag new file mode 100644 index 00000000000..023496bddbb --- /dev/null +++ b/dag/test/claim/fleet_capacity_control_witness_test.dag @@ -0,0 +1,184 @@ +module test.claim.fleet_capacity_control_witness_test + +import std.types { Bool, NonEmptyStr, List, String } +import extdeps.llm.cli_lifecycle { ProviderKind, ClaudeCliProvider, CodexCliProvider, CursorCliProvider } +import product.placement_supply { HostIdentity } +import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv3 } +import gunbc.fleet_capacity_control { + HostCapacityWithdrawal, ProviderCapacityWithdrawal, + WithdrawnForMaintenance, WithdrawnToReduceSpend, WithdrawnForObservedFault, + withdrawal_admits_automatic_restore, + fleet_capacity_admission_in, fleet_capacity_admission_admits, fleet_capacity_admission_line, + CapacityAdmitted, CapacityRefusedHostWithdrawn, CapacityRefusedProviderWithdrawn, + withdrawn_hosts, withdrawn_providers, + CapacityControlRequest, CutHost, CutProviderRuntime, CutProviderAccountBinding, + RestoreHost, RestoreProviderRuntime, + apply_capacity_control, capacity_control_is_planned, capacity_control_outcome_line, + ControlPlanned, ControlUnbound, ControlRejected, + host_is_withdrawn, provider_is_withdrawn, + active_host_count, active_provider_count, +} + +fn host_rows_srv3_down() -> List { + [HostCapacityWithdrawal { + host: operator_host_srv3, + cause: WithdrawnForMaintenance { detail: "memory upgrade" as NonEmptyStr }, + }] +} + +fn provider_rows_codex_down() -> List { + [ProviderCapacityWithdrawal { + provider: CodexCliProvider, + cause: WithdrawnToReduceSpend { detail: "quota exhausted" as NonEmptyStr }, + }] +} + +fn admission_label( + hosts: List, + providers: List, + host: HostIdentity, + provider: ProviderKind, +) -> String { + match fleet_capacity_admission_in( + host_rows: hosts, provider_rows: providers, host: host, provider: provider, + ) { + CapacityAdmitted => "admitted" + CapacityRefusedHostWithdrawn { host: _, cause: _ } => "refused-host" + CapacityRefusedProviderWithdrawn { provider: _, cause: _ } => "refused-provider" + } +} + +// THE TWO REFUSALS DO NOT COLLAPSE, WHICH IS THE WHOLE REASON THEY ARE SEPARATE ARMS. +// +// This is the discriminating control. An operator told only "unavailable" cannot tell a downed +// MACHINE from a cut RUNTIME, and the two have opposite repairs -- restoring the provider on a +// host that is down returns no capacity at all. If the coproduct were collapsed to a Bool this +// witness goes red while every admitted-path assertion stays green. +test fn a_downed_host_and_a_cut_runtime_do_not_share_one_answer() -> Bool { + let host_down = admission_label( + hosts: host_rows_srv3_down(), providers: [], + host: operator_host_srv3, provider: ClaudeCliProvider, + ) + let runtime_down = admission_label( + hosts: [], providers: provider_rows_codex_down(), + host: operator_host_srv3, provider: CodexCliProvider, + ) + host_down != runtime_down + && host_down == "refused-host" + && runtime_down == "refused-provider" +} + +// WHEN BOTH ARE WITHDRAWN THE HOST WINS, AND THAT PRECEDENCE IS LOAD-BEARING RATHER THAN TIDY. +// Reporting the provider for a host that is down names a cause whose repair changes nothing. +test fn a_downed_host_dominates_a_cut_runtime() -> Bool { + admission_label( + hosts: host_rows_srv3_down(), providers: provider_rows_codex_down(), + host: operator_host_srv3, provider: CodexCliProvider, + ) == "refused-host" +} + +// WITHDRAWAL IS SCOPED TO ITS SUBJECT AND DOES NOT LEAK ACROSS THE AXIS. +// srv3 being down must not withdraw srv1, and Codex being cut must not cut Claude. +test fn a_withdrawal_does_not_leak_to_its_siblings() -> Bool { + admission_label( + hosts: host_rows_srv3_down(), providers: provider_rows_codex_down(), + host: operator_host_srv1, provider: ClaudeCliProvider, + ) == "admitted" +} + +// A FAULT WITHDRAWAL IS NOT AUTO-RESTORABLE AND A MAINTENANCE ONE IS. +// +// The discriminating half is that these three answers are not all the same: a restorer keyed on +// reachability would flap an intermittently-failing host back into service between its failures, +// which is exactly why the cause is carried rather than being a bare withdrawn flag. +test fn only_maintenance_withdrawals_admit_automatic_restore() -> Bool { + withdrawal_admits_automatic_restore( + cause: WithdrawnForMaintenance { detail: "d" as NonEmptyStr }) + && !withdrawal_admits_automatic_restore( + cause: WithdrawnForObservedFault { detail: "d" as NonEmptyStr }) + && !withdrawal_admits_automatic_restore( + cause: WithdrawnToReduceSpend { detail: "d" as NonEmptyStr }) +} + +// THE ACCOUNT AXIS REFUSES RATHER THAN BEING ABSENT (operator ruling 2026-08-23). +// +// The control names both readings of "cut off a provider", and the unwired one answers with a +// typed not-yet-bound carrying the axis it needs. An absent control would read as "not applicable +// here" -- the not-applicable-versus-malformed conflation -- and would let an ambiguous request be +// answered by whichever reading happened to get built. +test fn the_account_axis_refuses_by_name_instead_of_being_absent() -> Bool { + let account = apply_capacity_control(request: CutProviderAccountBinding { + provider: ClaudeCliProvider, + account: "work-account" as NonEmptyStr, + cause: WithdrawnToReduceSpend { detail: "rotating" as NonEmptyStr }, + }) + let runtime = apply_capacity_control(request: CutProviderRuntime { + provider: ClaudeCliProvider, + cause: WithdrawnToReduceSpend { detail: "rotating" as NonEmptyStr }, + }) + !capacity_control_is_planned(outcome: account) + && capacity_control_is_planned(outcome: runtime) + && string_contains(s: capacity_control_outcome_line(outcome: account), pattern: "account binding") +} + +// THE CONTROL PLANS AND DOES NOT APPLY, AND THIS IS THE WITNESS THAT JOINS THE TWO (review 54905). +// +// This is the shape the reviewer named, and it is the one that catches the failure the earlier +// revision shipped: call the control, then READ THE ROSTER. An arm reporting "applied" while the +// roster reader still answers false is fabricated plausible output, and no amount of comparing +// outcome strings to each other can see it -- the previous witnesses compared requests against +// each other and were all green while the control lied. +// +// The assertion is deliberately that the host is STILL NOT withdrawn. Planning is what happened; +// withdrawal takes authoring a roster row and committing it, so a green here means the control is +// honest about the boundary rather than that it failed. +test fn planning_a_cut_does_not_withdraw_anything_by_itself() -> Bool { + let outcome = apply_capacity_control(request: CutHost { + host: operator_host_srv3, + cause: WithdrawnForMaintenance { detail: "memory upgrade" as NonEmptyStr }, + }) + capacity_control_is_planned(outcome: outcome) + && !host_is_withdrawn(host: operator_host_srv3) + && string_contains(s: capacity_control_outcome_line(outcome: outcome), pattern: "plan:") + && string_contains(s: capacity_control_outcome_line(outcome: outcome), + pattern: "add to withdrawn_hosts") +} + +test fn planning_a_runtime_cut_does_not_withdraw_it_by_itself() -> Bool { + let outcome = apply_capacity_control(request: CutProviderRuntime { + provider: CodexCliProvider, + cause: WithdrawnToReduceSpend { detail: "quota" as NonEmptyStr }, + }) + capacity_control_is_planned(outcome: outcome) + && !provider_is_withdrawn(provider: CodexCliProvider) +} + +// CUTTING A RUNTIME AND CUTTING A HOST ARE DIFFERENT PLANS, NOT ONE CONTROL WITH AN ARGUMENT. +test fn the_two_cut_controls_actuate_distinctly() -> Bool { + let cut_host = capacity_control_outcome_line(outcome: apply_capacity_control( + request: CutHost { + host: operator_host_srv3, + cause: WithdrawnForMaintenance { detail: "ram" as NonEmptyStr }, + })) + let cut_runtime = capacity_control_outcome_line(outcome: apply_capacity_control( + request: CutProviderRuntime { + provider: CursorCliProvider, + cause: WithdrawnForMaintenance { detail: "ram" as NonEmptyStr }, + })) + cut_host != cut_runtime + && string_contains(s: cut_host, pattern: "srv3") + && string_contains(s: cut_runtime, pattern: "Cursor") +} + +// THE LIVE FLEET IS FULLY ACTIVE, AND THIS IS THE ASSERTION THAT A ROSTER EDIT IS DELIBERATE. +// +// The rosters are the operator's control surface; empty is the correct resting position. This +// witness goes red the moment capacity is withdrawn in a commit, which is the point -- taking a +// machine or a runtime out of service should require an author to face a red test and say so, +// rather than riding in as a data row nobody reads. +test fn the_live_rosters_withdraw_nothing() -> Bool { + active_host_count() == 4 + && active_provider_count() == 3 + && (withdrawn_hosts |> count) == 0 + && (withdrawn_providers |> count) == 0 +} diff --git a/dag/test/claim/fleet_capacity_gate_witness_test.dag b/dag/test/claim/fleet_capacity_gate_witness_test.dag new file mode 100644 index 00000000000..1f33adf2709 --- /dev/null +++ b/dag/test/claim/fleet_capacity_gate_witness_test.dag @@ -0,0 +1,109 @@ +module test.claim.fleet_capacity_gate_witness_test + +import std.types { Bool, NonEmptyStr, List } +import extdeps.llm.cli_lifecycle { ProviderKind, CodexCliProvider, ClaudeCliProvider } +import product.placement_supply { HostIdentity } +import gunbc.fleet_capacity_control { + HostCapacityWithdrawal, ProviderCapacityWithdrawal, + WithdrawnForMaintenance, WithdrawnToReduceSpend, +} +import gunbc.roadmap_dashboard_instance { HostDashboardInstance, srv1_live_dashboard_instance } +import gunbc.dispatch_selection { + ProviderOffer, ProviderInventory, + declared_provider_inventory_for_instance, + provider_inventory_for_instance, + provider_inventory_withdrawn_for_instance, + capacity_admitted_offers_in, capacity_withdrawn_offers_in, +} + + +fn live_instance() -> HostDashboardInstance { + srv1_live_dashboard_instance() +} + +fn declared_offers() -> List { + declared_provider_inventory_for_instance(instance: live_instance()).offers +} + +fn withdraw_this_host() -> List { + [HostCapacityWithdrawal { + host: live_instance().host_identity as HostIdentity, + cause: WithdrawnForMaintenance { detail: "memory upgrade" as NonEmptyStr }, + }] +} + +fn withdraw_codex() -> List { + [ProviderCapacityWithdrawal { + provider: CodexCliProvider, + cause: WithdrawnToReduceSpend { detail: "quota exhausted" as NonEmptyStr }, + }] +} + +// THE GATE ACTUALLY CUTS, WHICH IS THE CLAIM A NEUTRAL LIVE ROSTER CANNOT MAKE. +// +// The live rosters are empty, so the production inventory is unchanged by this wiring. That is +// correct and it is also why this witness authors its own withdrawal: without it every assertion +// here would be about the half of the gate that does nothing, and a wiring that silently failed to +// filter would stay green forever. +test fn withdrawing_this_host_removes_every_offer_it_had() -> Bool { + let before = declared_offers() + let after = capacity_admitted_offers_in( + host_rows: withdraw_this_host(), provider_rows: [], + instance: live_instance(), offers: before, + ) + (before |> count) > 0 && (after |> count) == 0 +} + +// AN INVENTORY EMPTIED BY WITHDRAWAL IS DISTINGUISHABLE FROM ONE THAT WAS NEVER FILLED. +// +// This is the empty-observation narrow, guarded. A bare filter renders both as the same empty +// list, and the two have opposite remedies -- restore the host, versus install a provider. The +// withdrawn list is what carries the distinguishing fact, so it must be NON-EMPTY exactly when the +// offers went away because someone cut them. +test fn a_withdrawn_empty_inventory_is_not_an_unfilled_one() -> Bool { + let offers = declared_offers() + let admitted = capacity_admitted_offers_in( + host_rows: withdraw_this_host(), provider_rows: [], + instance: live_instance(), offers: offers, + ) + let withdrawn = capacity_withdrawn_offers_in( + host_rows: withdraw_this_host(), provider_rows: [], + instance: live_instance(), offers: offers, + ) + (admitted |> count) == 0 + && (withdrawn |> count) == (offers |> count) + && (withdrawn |> count) > 0 +} + +// CUTTING ONE RUNTIME IS NOT CUTTING THE HOST: THE PARTITION IS EXACT AND LOSES NOTHING. +// +// Every declared offer lands in exactly one of the two lists. A gate that dropped an offer from +// both -- or double-counted one -- would still look plausible on the admitted side alone, which is +// why this asserts the sum against the denominator rather than just that something was removed. +test fn the_gate_partitions_offers_without_losing_any() -> Bool { + let offers = declared_offers() + let admitted = capacity_admitted_offers_in( + host_rows: [], provider_rows: withdraw_codex(), + instance: live_instance(), offers: offers, + ) + let withdrawn = capacity_withdrawn_offers_in( + host_rows: [], provider_rows: withdraw_codex(), + instance: live_instance(), offers: offers, + ) + (admitted |> count) + (withdrawn |> count) == (offers |> count) + && (offers |> count) > 0 +} + +// THE LIVE PRODUCTION INVENTORY IS UNCHANGED BY THIS WIRING. +// +// With empty rosters the gate is exactly the identity, and nothing is withdrawn. This is the +// no-op control: it goes red if the gate ever starts removing production capacity that no operator +// asked to remove, which is the failure this change could plausibly introduce. +test fn the_live_inventory_loses_nothing_to_the_gate() -> Bool { + let declared = declared_provider_inventory_for_instance(instance: live_instance()) + let gated = provider_inventory_for_instance(instance: live_instance()) + let withdrawn = provider_inventory_withdrawn_for_instance(instance: live_instance()) + (gated.offers |> count) == (declared.offers |> count) + && (withdrawn |> count) == 0 + && (declared.offers |> count) > 0 +} diff --git a/dag/test/claim/fleet_capacity_panel_witness_test.dag b/dag/test/claim/fleet_capacity_panel_witness_test.dag new file mode 100644 index 00000000000..6f6ff4d9f6d --- /dev/null +++ b/dag/test/claim/fleet_capacity_panel_witness_test.dag @@ -0,0 +1,184 @@ +module test.claim.fleet_capacity_panel_witness_test + +import std.types { Bool, String, List } +import extdeps.languages.html { EmitOk, EmitRejected, HtmlEmitResult, try_serialize_html_source } +import gunbc.roadmap_document { RoadmapDocument } +import gunbc.roadmap_page { roadmap_daily_workspace_page } +import gunbc.fleet_capacity_panel { + fleet_capacity_summary_line, + fleet_committed_slot_total, + fleet_committed_slot_total_ignoring_withdrawals, + fleet_capacity_withdrawn_line, +} +import gunbc.runner_slot_allocation { + gunbc_runner_slots_per_host, host_binding_width_axes, host_width_binding_label, + width_axis_binds_at, +} +import gunbc.fleet_intent_network { + operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4, +} + +fn workspace_emission() -> HtmlEmitResult { + try_serialize_html_source(node: roadmap_daily_workspace_page( + doc: RoadmapDocument { preamble: [], lead_lanes: [], sections: [] }, + merged: [], + )) +} + +// A REFUSED SERIALIZATION MUST NOT ANSWER AS AN EMPTY PAGE (review 55040, DESIGN §5). +// +// This arm returned "" on EmitRejected, which is the absorbing fallback in the direction that +// costs the most here: every !string_contains assertion in this file is SATISFIED by the empty +// string, so a total serialization failure would have rendered the negative rows green and left +// the positive rows unable to distinguish "the panel is missing" from "nothing serialized at all". +// Two states with opposite remedies, one answer. +// +// The rejected arm now carries the reason, so a positive assertion fails on it and the text names +// what happened rather than vanishing. The reason is prefixed with a marker no assertion in this +// file searches for, so it cannot accidentally satisfy one either. +fn empty_workspace_html() -> String { + match workspace_emission() { + EmitOk { html: h } => h + EmitRejected { reason: r } => join(["EMISSION-REFUSED: ", r as String], "") + } +} + +fn workspace_emission_is_ok() -> Bool { + match workspace_emission() { + EmitOk { html: _ } => true + EmitRejected { reason: _ } => false + } +} + +// THE REFUSAL IS ITS OWN RED, NOT A CONDITION ATTACHED TO OTHER ROWS. +// +// Without this, a serialization refusal is only ever observed indirectly, through whichever +// assertion happens to notice the page is not what it expected. This makes it a finding in its own +// right with its own name, so the ledger says "emission refused" rather than "the panel is absent". +test fn the_workspace_actually_serializes() -> Bool { + workspace_emission_is_ok() +} + +// THE PANEL REACHES THE RENDERED PAGE, WHICH IS THE ONLY SURFACE THE OPERATOR SEES. +// +// A witness over fleet_capacity_panel() alone would prove the fragment builds and say nothing +// about whether it is composed into the workspace -- the specification-without-execution failure, +// where a green test sits beside a page that never shows the thing. This serializes the actual +// daily workspace document and looks for the panel in the HTML. +test fn the_capacity_panel_reaches_the_rendered_workspace() -> Bool { + let h = empty_workspace_html() + string_contains(s: h, pattern: "fleet-capacity-panel") + && string_contains(s: h, pattern: "fleet capacity") + && string_contains(s: h, pattern: "srv1") + && string_contains(s: h, pattern: "srv4") + && string_contains(s: h, pattern: "slots committed") +} + +// THE PANEL SAYS ITS NUMBERS ARE COMMITTED RATHER THAN OBSERVED, IN THE OUTPUT AND NOT ONLY IN A +// COMMENT. runner_slot_allocation states that srv3/srv4's width of 6 is a provisioning target -- +// two slots that do not exist yet -- so a reader summing the column gets 22 for a fleet running +// 20. The qualifier is the difference between a number and a misleading number, and an annotation +// cannot carry it because no operator reads the source. +test fn the_panel_labels_its_widths_as_committed_not_observed() -> Bool { + let h = empty_workspace_html() + workspace_emission_is_ok() && + string_contains(s: h, pattern: "committed allocations, not observed incarnations") + && !string_contains(s: h, pattern: "slots running") +} + +// THE SUMMARY IS DERIVED FROM THE ALLOCATION AUTHORITY, NOT TRANSCRIBED. +// +// Asserted as the relation against gunbc_runner_slots_per_host rather than against the literal 22. +// A literal would be a change detector that goes red on a correct width ruling and stays green if +// the panel silently stopped reading the authority at all. +// THE TOTAL JOINS TO THE ALLOCATION AUTHORITY PER HOST, AND NAMES EVERY HOST TO DO IT. +// +// An earlier revision asserted srv1 * 2 + srv3 * 2, which was true only while the fleet was two +// symmetric pairs. #8976 made CPU an admission axis and the symmetry ended: srv1/srv3/srv4 became +// core-bound while srv2 stayed memory-bound on 8x16 GiB, because its 64 GiB upgrade failed training +// and was reverted. The doubling was never the property under test -- it was a shortcut that +// happened to hold -- and it turned a real fleet asymmetry into a red on a witness about summing. +// +// Naming all four hosts keeps the join (the panel's total must equal the allocation authority's +// per-host widths) while carrying no assumption about which hosts resemble each other. It also +// stays a genuine oracle rather than measure() == measure(): the right side reads +// gunbc_runner_slot_allocation, a different authority from the panel fold on the left. +test fn the_slot_total_sums_the_allocation_authority() -> Bool { + fleet_committed_slot_total_ignoring_withdrawals() + == gunbc_runner_slots_per_host(host: operator_host_srv1) + + gunbc_runner_slots_per_host(host: operator_host_srv2) + + gunbc_runner_slots_per_host(host: operator_host_srv3) + + gunbc_runner_slots_per_host(host: operator_host_srv4) + && fleet_committed_slot_total() > 0 +} + +// WITH NOTHING WITHDRAWN THE TWO TOTALS AGREE AND THE WITHDRAWN LINE IS ABSENT. +// +// The absent line is the point: a standing "0 withdrawn" row is noise on every ordinary day and +// trains the reader to skip the row where a non-zero number finally matters. +test fn nothing_withdrawn_means_no_withdrawn_line() -> Bool { + let line_absent = match fleet_capacity_withdrawn_line() { + Present { value: _ } => false + Absent => true + } + fleet_committed_slot_total() == fleet_committed_slot_total_ignoring_withdrawals() + && line_absent +} + +test fn the_summary_line_names_both_axes() -> Bool { + let line = fleet_capacity_summary_line() + string_contains(s: line, pattern: "hosts") + && string_contains(s: line, pattern: "runtimes") + && string_contains(s: line, pattern: "slots committed") +} + +// AN UNMEASURED AXIS IS NEVER REPORTED AS BINDING, AND NEVER AS ADMITTING EITHER. +// +// Disk returns DiskWidthUnconstrained on every host today, and runner_slot_allocation's own reason +// string is explicit that this is "an unmeasured axis, not a measured all-clear". Rendering it as +// "disk admits any width" would turn an absence of observation into a positive clearance -- the +// conflation where not-applicable and not-observed wear one symbol. The discriminating half is +// that disk is excluded from the BINDING set: a fold that treated an unstated width as +// satisfying the minimum would list disk beside memory and read as two independent confirmations +// of a width only one axis actually measured. +test fn an_unmeasured_axis_is_not_reported_as_binding() -> Bool { + let binding = host_binding_width_axes(host: operator_host_srv1) + let label = host_width_binding_label(host: operator_host_srv1) + (binding |> count) == 1 + && string_contains(s: label, pattern: "disk unmeasured") + && !string_contains(s: label, pattern: "disk admits") +} + +// TWO HOSTS, TWO DIFFERENT BINDING AXES -- THE WHOLE REASON THE COLUMN EXISTS. +// +// srv1 is core-bound at 21 and srv2 is memory-bound at 5, because srv2's 64 GiB DIMM install +// failed training and was reverted while the other three carry 8x64. So the fleet total is two +// unrelated stories, and an operator reading only the total would go buy the wrong thing for one +// of these hosts. This is the discriminating witness: a label function that named one axis for the +// whole fleet passes every other assertion here and fails this one. +test fn srv1_and_srv2_are_bound_by_different_axes() -> Bool { + let one = host_width_binding_label(host: operator_host_srv1) + let two = host_width_binding_label(host: operator_host_srv2) + one != two + && string_contains(s: one, pattern: "bound by cores") + && string_contains(s: two, pattern: "bound by memory") +} + +// THE BINDING AXIS IS DERIVED FROM THE COMMITTED WIDTH RATHER THAN ASSERTED BESIDE IT. +// +// Asserted as the relation: whatever axis is named as binding must actually sit at the committed +// width. A label authored independently of the arithmetic could name memory while the minimum came +// from somewhere else, and nothing downstream would catch it -- the panel would explain a number +// using a cause that did not produce it. +test fn the_binding_axis_sits_at_the_committed_width() -> Bool { + all([operator_host_srv1, operator_host_srv3], h => + all(host_binding_width_axes(host: h), a => + width_axis_binds_at(standing: a, committed: gunbc_runner_slots_per_host(host: h)))) +} + +test fn the_panel_renders_the_binding_axis_for_every_host() -> Bool { + let h = empty_workspace_html() + string_contains(s: h, pattern: "bound by cores") + && string_contains(s: h, pattern: "bound by memory") + && string_contains(s: h, pattern: "unmeasured") +} diff --git a/dag/test/claim/fleet_converge_plan_witness_test.dag b/dag/test/claim/fleet_converge_plan_witness_test.dag index 8d328254f10..4dffd810eda 100644 --- a/dag/test/claim/fleet_converge_plan_witness_test.dag +++ b/dag/test/claim/fleet_converge_plan_witness_test.dag @@ -33,7 +33,10 @@ import gunbc.fleet_converge_plan { fleet_converge_plan_content_hash_path, fleet_converge_plan_bundle_digest_hex, fleet_converge_plan_bundle_matches, + fleet_converge_slot_lines, + fleet_converge_slot_refusal_count, } +import gunbc.runner_slot_provision { runner_slot_member_from_instance_name } import extdeps.posix.shell_command_language { posix_single_quote } import gunbc.fleet_converge_plan_cli { fleet_converge_plan_cli_note } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -55,6 +58,7 @@ test fn timer_retirement_plan_shows_refused_removal_for_foreign_cap() -> Bool { observed_timers: [], observed_caps: [foreign], observed_spark: [], + observed_slots: [], ) { Present { value: artifact } => string_contains(s: artifact.plan_body, pattern: "REFUSED-REMOVAL cap ") @@ -82,6 +86,7 @@ test fn plan_artifact_hash_is_stable_for_fixed_observation() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) { Present { value: a1 } => match fleet_converge_plan_artifact( @@ -90,6 +95,7 @@ test fn plan_artifact_hash_is_stable_for_fixed_observation() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) { Present { value: a2 } => match fleet_converge_plan_artifact_hash(artifact: a1) { @@ -117,6 +123,7 @@ test fn observed_baseline_cas_refuses_after_drift() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) { Present { value: artifact } => { let drifted = CapMember { @@ -129,6 +136,7 @@ test fn observed_baseline_cas_refuses_after_drift() -> Bool { observed_timers: [], observed_caps: [drifted], observed_spark: [], + observed_slots: [], ) } Absent => false @@ -142,6 +150,7 @@ test fn plan_body_names_subject_host_and_generation() -> Bool { observed_timers: [], observed_caps: [], observed_spark: [], + observed_slots: [], ) { Present { value: artifact } => string_contains(s: artifact.plan_body, pattern: "subject_host:srv1") @@ -164,6 +173,7 @@ test fn cross_host_apply_refuses_subject_identity() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) { Present { value: artifact } => !fleet_converge_apply_subject_admits( @@ -172,6 +182,7 @@ test fn cross_host_apply_refuses_subject_identity() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) Absent => false } @@ -188,6 +199,7 @@ test fn same_host_different_generation_changes_plan_hash() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) { Present { value: gen0 } => match fleet_converge_plan_artifact( @@ -196,6 +208,7 @@ test fn same_host_different_generation_changes_plan_hash() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) { Present { value: gen1 } => match fleet_converge_plan_artifact_hash(artifact: gen0) { @@ -231,6 +244,7 @@ test fn member_set_fingerprint_mismatch_refuses_identity() -> Bool { observed_timers: [], observed_caps: [observed_cap], observed_spark: [], + observed_slots: [], ) { Present { value: artifact } => { let drifted = CapMember { @@ -243,6 +257,7 @@ test fn member_set_fingerprint_mismatch_refuses_identity() -> Bool { observed_timers: [], observed_caps: [drifted], observed_spark: [], + observed_slots: [], ) } Absent => false @@ -266,6 +281,7 @@ test fn bundle_hash_binds_apply_shell_not_plan_body_only() -> Bool { observed_timers: [], observed_caps: [], observed_spark: [], + observed_slots: [], ) { Present { value: artifact } => match fleet_converge_plan_bundle_digest_hex( @@ -437,6 +453,7 @@ test fn apply_shell_carries_dissolve_on_marker_not_host_gate() -> Bool { observed_timers: [], observed_caps: [], observed_spark: [], + observed_slots: [], ) { Present { value: artifact } => string_contains(s: artifact.apply_shell, pattern: "dissolve-on: fleet_converge_apply_shell") @@ -461,3 +478,97 @@ test fn locked_apply_stale_diagnostic_keeps_observed_value_in_one_word() -> Bool !string_contains(s: inner, pattern: "observed= ") && string_contains(s: inner, pattern: "observed=") } + + +// --- the slot family: the third member family joins plan and apply ----------------------------- + +// A HOST NOBODY MODELED PRODUCES A REFUSAL LINE IN THE PLAN, not an empty slot section. This is the +// discriminating RED for the arm: an empty section reads to a reviewer as "this axis is converged", +// which is the exact opposite of what an unresolvable host means. +test fn an_unmodeled_host_refuses_in_the_slot_section() -> Bool { + let lines = fleet_converge_slot_lines( + host: "srv-nonexistent" as NonEmptyStr, + observed_slots: [], + ) + any(lines, l => string_contains(s: l, pattern: "REFUSED-UNMODELED-HOST runner-slot")) + && fleet_converge_slot_refusal_count( + host: "srv-nonexistent" as NonEmptyStr, + observed_slots: [], + ) == 1 +} + +// THE POSITIVE CONTROL, without which the row above is satisfied by a family that refuses always. +// srv1 is modeled and carries a committed width, so an empty observation must propose ADDs. +test fn a_modeled_host_proposes_the_slots_it_is_missing() -> Bool { + let lines = fleet_converge_slot_lines(host: witness_host_srv1, observed_slots: []) + any(lines, l => string_contains(s: l, pattern: "ADD runner-slot srv1-01")) + && (any(lines, l => string_contains(s: l, pattern: "REFUSED-UNMODELED-HOST")) == false) +} + +// AN OUT-OF-BAND SLOT IS REFUSED REMOVAL RATHER THAN DELETED. gunbc.runner_slot_provision cannot yet +// establish that a directory under /opt/actions-runner was placed there by gunbc, so ownership is +// Absent and reconcile must produce MemberRemovalRefused. A plan that silently emitted REMOVE here +// would delete a stranger's directory on apply. +test fn an_unowned_observed_slot_is_refused_removal_not_removed() -> Bool { + let lines = fleet_converge_slot_lines( + host: witness_host_srv1, + observed_slots: [runner_slot_member_from_instance_name(instance_name: "srv1-99")], + ) + any(lines, l => string_contains(s: l, pattern: "REFUSED-REMOVAL runner-slot srv1-99")) + && (any(lines, l => string_contains(s: l, pattern: "REMOVE runner-slot srv1-99")) == false) +} + +// THE SLOT FAMILY REACHES apply.sh, WHICH IS THE HALF THAT MAKES THIS A CONVERGENCE RATHER THAN A +// REPORT. Timer teardown was the only thing the emitted script executed; a slot ADD must now appear +// in it, and the plan body must name the same axis, so a reviewer approving plan.txt is approving +// what apply runs. +test fn a_slot_add_reaches_the_emitted_apply_script() -> Bool { + match fleet_converge_plan_artifact( + host: witness_host_srv1, + prior_generation: 0, + observed_timers: [], + observed_caps: [], + observed_spark: [], + observed_slots: [], + ) { + Present { value: artifact } => + string_contains(s: artifact.plan_body, pattern: "ADD runner-slot srv1-01") + && string_contains(s: artifact.plan_body, pattern: "# slot-refusals=0") + && string_contains(s: artifact.apply_shell, pattern: "actions-runner") + && (string_contains(s: artifact.apply_shell, pattern: "no slots to add") == false) + Absent => false + } +} + +// AND THE SLOT POPULATION IS PART OF THE SUBJECT IDENTITY, so a host whose slot roster drifted +// between plan and apply fails the member-set gate instead of applying a stale plan. Without this +// the slot family would be rendered in the plan and unprotected by the CAS that guards the others. +test fn slot_drift_breaks_the_member_set_fingerprint() -> Bool { + match fleet_converge_plan_artifact( + host: witness_host_srv1, + prior_generation: 0, + observed_timers: [], + observed_caps: [], + observed_spark: [], + observed_slots: [], + ) { + Present { value: artifact } => + fleet_converge_member_set_fingerprint_matches( + planned_fingerprint_text: serialize_content_hash(hash: artifact.subject.member_set_fingerprint) as String, + host: witness_host_srv1, + observed_timers: [], + observed_caps: [], + observed_spark: [], + observed_slots: [], + ) + && (fleet_converge_member_set_fingerprint_matches( + planned_fingerprint_text: serialize_content_hash(hash: artifact.subject.member_set_fingerprint) as String, + host: witness_host_srv1, + observed_timers: [], + observed_caps: [], + observed_spark: [], + observed_slots: [runner_slot_member_from_instance_name(instance_name: "srv1-01")], + ) == false) + Absent => false + } +} diff --git a/dag/test/claim/runner_capacity_plan_witness_test.dag b/dag/test/claim/runner_capacity_plan_witness_test.dag index c629fe46e2c..2f299a319c0 100644 --- a/dag/test/claim/runner_capacity_plan_witness_test.dag +++ b/dag/test/claim/runner_capacity_plan_witness_test.dag @@ -13,7 +13,7 @@ import gunbc.runner_capacity_plan { } import gunbc.fleet_intent_network { operator_host_srv1 } import gunbc.build_cache_instance { RunnerSlotIdentity } -import gunbc.runner_slot_allocation { committed_slot_identities } +import gunbc.runner_slot_allocation { committed_slot_identities, gunbc_runner_slots_per_host } import gunbc.runner_capacity_plan { runner_capacity_plan, runner_capacity_add_count, @@ -63,10 +63,20 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // to carry stops at the wall with a typed cause rather than being admitted and then producing // nothing. Both hosts plan zero actions and both carry a WidthRefused admission -- the difference // from the old behaviour is that the refusal is now VISIBLE in the plan. +// THE REQUESTED WIDTH IS DERIVED FROM THE CEILING, BECAUSE A LITERAL SEVEN STOPPED BEING ABOVE IT. +// +// This row asked for width 7 when the committed ceiling was 6, so the plan refused to add and +// add_count was 0. The 2026-08-23 CPU-axis change moved srv3 and srv4 to twenty-one, and 7 became +// an ordinary in-range request that the plan quite correctly fulfils -- so the row went red without +// the ceiling behaviour it names having changed at all. +// +// Retyping 7 as 22 puts the same landmine one width further out. Asking for committed + 1 keeps the +// request above the ceiling by construction, so this stays a check on the refusal arm rather than +// on whatever number the fleet happened to commit the day it was written. test fn a_width_above_the_committed_ceiling_is_refused_not_silently_unfulfilled() -> Bool { let plan = runner_capacity_plan( - srv3_width: 7, - srv4_width: 7, + srv3_width: gunbc_runner_slots_per_host(host: operator_host_srv3) + 1, + srv4_width: gunbc_runner_slots_per_host(host: operator_host_srv4) + 1, roster: organization_runner_roster_evidence() ) match plan { @@ -269,6 +279,16 @@ test fn an_identity_from_another_host_cannot_answer_for_this_one() -> Bool { )) } +// THE srv1 CLAUSE NOW DERIVES ITS OUT-OF-RANGE INDEX; THE srv3 CLAUSES NEEDED NOTHING. +// +// The last clause observed srv1 slots [1, 6] and required a refusal. Six was outside srv1's +// five-wide population when this was written; at twenty-one it is an ordinary committed member, so +// the refusal correctly did not fire and only this fixture was wrong. It now asks for committed + 1. +// +// Every srv3 clause is untouched and that is the informative half: srv3-06 refuses because it is +// the AUTHORED fabric identity, not because of where it sits relative to a width. The width moved +// from six to twenty-one underneath these clauses and they did not notice -- which is the property +// runner_slot_allocation was built to have, observed rather than asserted. test fn a_github_runner_in_a_fabric_slot_refuses_instead_of_reading_converged() -> Bool { population_is_refused(v: validate_observed_github_slot_members( host: operator_host_srv3, @@ -288,7 +308,7 @@ test fn a_github_runner_in_a_fabric_slot_refuses_instead_of_reading_converged() )) && population_is_refused(v: validate_observed_github_slot_members( host: operator_host_srv1, - observed: [srv1_slot(i: 1), srv1_slot(i: 6)], + observed: [srv1_slot(i: 1), srv1_slot(i: gunbc_runner_slots_per_host(host: operator_host_srv1) + 1)], )) } diff --git a/dag/test/claim/runner_host_deploy_witness_test.dag b/dag/test/claim/runner_host_deploy_witness_test.dag index 260718557e8..ee02ec2f825 100644 --- a/dag/test/claim/runner_host_deploy_witness_test.dag +++ b/dag/test/claim/runner_host_deploy_witness_test.dag @@ -27,7 +27,7 @@ import gunbc.runner_activation { BuildCacheInstanceReady, HostCompilePoolReady, admit_runner_activation, runner_activate_command, } -import gunbc.build_cache_instance { BuildCacheInstance, ProcessIdentity, ci_cache_instance } +import gunbc.build_cache_instance { BuildCacheInstance, ProcessIdentity, ci_cache_instance, runner_slot_index_suffix } import gunbc.host_layout { gunbc_managed_compile_pool_slice } import product.placement_supply { HostIdentity } import std.types { NonEmptyStr, String } @@ -76,17 +76,31 @@ test fn srv4_runner_app_from_secret_manager() -> Bool { && gunbc_ci_github_app.installation_id.value == 104134109 } -test fn srv4_enables_six_named_runner_instances() -> Bool { +// THE ROSTER AND THE ENABLE COMMAND MUST AGREE WITH THE DECLARED COUNT, WHATEVER THAT COUNT IS. +// +// This row pinned six twice over: the roster length, and an assertion that srv4-07 does NOT appear. +// Both were measurements of the tree the day it was written, and the 2026-08-23 CPU-axis change +// falsified both at once -- srv4 commits twenty-one, so the roster is twenty-one long and srv4-07 +// is a perfectly ordinary member of it. +// +// What the row is actually for is the JOIN: the systemd units the enable command names are exactly +// the instances the roster names, one per slot, zero-padded and one-based. That relation is what +// would break if the two ever diverged, and it holds at any width. The name changes with it, since +// a row called _six_ that no longer asserts six is worse than either. +test fn srv4_enables_its_declared_runner_instances() -> Bool { let names = runner_instance_names(deploy: srv4_runner_host_deploy) let enable = match runner_activate_command(admission: admit_runner_activation(host_admission: admit_runner_host(deploy: srv4_runner_host_deploy), cache_ready: witness_ready_receipt(), pool_ready: witness_ready_pool())) { RunnerCommandReady { command: cmd } => shell_command_render(command: cmd) RunnerCommandRefused { host_label: _, reason: _ } => "" } - list_length(items: names) == 6 + list_length(items: names) == srv4_runner_host_deploy.runner_count && string_contains(s: enable, pattern: "'actions-runner@srv4-01.service'") && string_contains(s: enable, pattern: "'actions-runner@srv4-05.service'") - && string_contains(s: enable, pattern: "srv4-06") - && !string_contains(s: enable, pattern: "srv4-07") + && all(names, n => string_contains(s: enable, pattern: n)) + && !string_contains( + s: enable, + pattern: concat("srv4-", runner_slot_index_suffix(index: srv4_runner_host_deploy.runner_count + 1)), + ) && string_contains(s: enable, pattern: "'sudo' 'systemctl' 'enable' '--now'") } diff --git a/dag/test/claim/runner_slot_allocation_witness_test.dag b/dag/test/claim/runner_slot_allocation_witness_test.dag index 7af87b66189..e4512af96e7 100644 --- a/dag/test/claim/runner_slot_allocation_witness_test.dag +++ b/dag/test/claim/runner_slot_allocation_witness_test.dag @@ -241,12 +241,32 @@ test fn slot_purposes_partition_every_host_committed_width() -> Bool { // index above the GitHub ceiling answered "fabric" -- measured, srv1-06 and srv3-99 both did, though // srv1 is five wide and neither is a member of anything. Membership now precedes purpose and those // identities are refused with the width they were measured against. +// THE OUT-OF-RANGE INDEX IS DERIVED, BECAUSE WRITING ONE DOWN IS HOW THIS ROW STOPPED CHECKING. +// +// It read slot 6 on srv1 and slot 7 on srv3. Both WERE outside the committed population -- at the +// widths of the day, five and six. The 2026-08-23 CPU-axis change moved both hosts to twenty-one, +// so both indices became ordinary committed members, the refusal correctly did not fire, and the +// row went red. Nothing about the property it names had changed. +// +// Retyping 7 as 22 would re-arm exactly the same landmine one width later. A fixture that picks an +// out-of-range index by writing down a number that happens to be out of range TODAY is a change +// detector wearing a property's name (DESIGN section 5: a measurement copied from the same current +// tree is not an oracle). Deriving committed + 1 makes the fixture discriminating at ANY width, +// which is what it was always trying to say. +// +// The two clauses that did NOT need touching are the informative ones. srv3-99 stays outside at any +// plausible width, and srv3-06 stays INSIDE and stays fabric, because runner_slot_allocation +// AUTHORS that identity rather than deriving it from a count -- the defence in +// the_fabric_member_is_an_authored_identity_not_a_top_index_rule, observed working through a real +// width change rather than only asserted. test fn an_identity_outside_the_committed_population_is_refused_not_classified() -> Bool { - membership_is_outside(m: runner_slot_membership(host: operator_host_srv1, slot_index: 6)) + let srv1_past_end = gunbc_runner_slots_per_host(host: operator_host_srv1) + 1 + let srv3_past_end = gunbc_runner_slots_per_host(host: operator_host_srv3) + 1 + membership_is_outside(m: runner_slot_membership(host: operator_host_srv1, slot_index: srv1_past_end)) && membership_is_outside(m: runner_slot_membership(host: operator_host_srv3, slot_index: 99)) - && membership_is_outside(m: runner_slot_membership(host: operator_host_srv3, slot_index: 7)) + && membership_is_outside(m: runner_slot_membership(host: operator_host_srv3, slot_index: srv3_past_end)) && !membership_is_outside(m: runner_slot_membership(host: operator_host_srv3, slot_index: 6)) - && !membership_is_fabric(m: runner_slot_membership(host: operator_host_srv1, slot_index: 6)) + && !membership_is_fabric(m: runner_slot_membership(host: operator_host_srv1, slot_index: srv1_past_end)) } // THE FABRIC MEMBER IS AN EXACT IDENTITY AND DOES NOT MOVE WITH THE WIDTH. The carve is authored as @@ -273,11 +293,29 @@ test fn srv3_slot_six_is_the_only_fabric_slot_in_the_fleet() -> Bool { // GitHub slots and none is renamed or deregistered to pay for the canary. Taking the fabric slot // from the bottom would have renumbered every live runner on the host, and this row goes red if // anyone reverses that direction. +// THE GITHUB COUNT IS THE COMMITTED WIDTH LESS THE FABRIC MEMBERS, NOT THE NUMBER FIVE. +// +// This row pinned 5, which was srv3's six committed slots less its one fabric member. At width +// twenty-one the same relation yields twenty, so the literal went red while the property -- that +// carving out srv3-06 costs GitHub exactly one slot and takes none of the five that were live -- +// held throughout. +// +// Stated as the relation it survives any width, and it still fails if the carve ever starts +// deregistering a live runner: slots one through five are asserted individually, so a fabric role +// that slid onto one of them would be caught here rather than absorbed into a count. +// +// The minus-one is deliberate rather than minus host_fabric_slot_count. Subtracting the measured +// fabric count would make this row true for ANY number of fabric members, including zero, which is +// the general conservation already asserted by +// slot_purposes_partition_every_host_committed_width. THIS row is about the specific +// carve: srv3 gives up exactly one slot to the fabric. Writing it as the general identity would +// leave that claim asserted nowhere. test fn introducing_the_fabric_slot_deregisters_no_live_runner() -> Bool { !membership_is_fabric(m: runner_slot_membership(host: operator_host_srv3, slot_index: 1)) && !membership_is_fabric(m: runner_slot_membership(host: operator_host_srv3, slot_index: 2)) && !membership_is_fabric(m: runner_slot_membership(host: operator_host_srv3, slot_index: 3)) && !membership_is_fabric(m: runner_slot_membership(host: operator_host_srv3, slot_index: 4)) && !membership_is_fabric(m: runner_slot_membership(host: operator_host_srv3, slot_index: 5)) - && host_github_slot_count(host: operator_host_srv3) == 5 + && host_github_slot_count(host: operator_host_srv3) + == gunbc_runner_slots_per_host(host: operator_host_srv3) - 1 } diff --git a/dag/test/claim/runner_slot_provision_witness_test.dag b/dag/test/claim/runner_slot_provision_witness_test.dag index 9d911d82a45..beec1eb9d8a 100644 --- a/dag/test/claim/runner_slot_provision_witness_test.dag +++ b/dag/test/claim/runner_slot_provision_witness_test.dag @@ -1,7 +1,7 @@ module test.claim.runner_slot_provision import std.logic { Bool } -import std.types { list_length, NonEmptyStr, List } +import std.types { list_length, NonEmptyStr, List, String } import extdeps.toolchain.types { Aarch64 } import extdeps.github.actions_runner { actions_runner_release_2_334_0, @@ -9,8 +9,14 @@ import extdeps.github.actions_runner { actions_runner_download_url, } import gunbc.runner_host_deploy { + srv1_runner_host_deploy, + srv2_runner_host_deploy, srv3_runner_host_deploy, srv4_runner_host_deploy, + runner_host_deploy_for, + RunnerHostDeployFound, + RunnerHostDeployUnmodeled, + fleet_runner_host_deploys, runner_host_installer_command_argv, runner_instance_names, gunbc_ci_github_app, @@ -25,10 +31,19 @@ import gunbc.runner_slot_provision { RunnerSlotEnumerationMismatch, RunnerSlotMember, runner_slot_provision_has_width_increase, + RunnerSlotObservation, + RunnerSlotsObserved, + RunnerSlotsUnobserved, + RunnerSlotConvergeVerdict, + RunnerSlotConvergePlanned, + RunnerSlotConvergeRefused, + runner_slot_converge_verdict, + runner_slot_member_from_instance_name, } import gunbc.membership_reconcile { membership_added_count } +import gunbc.runner_slot_allocation { gunbc_runner_slots_per_host, host_fabric_slot_count } import gunbc.fleet_host_budget { declared_runner_count_for } -import gunbc.fleet_intent_network { operator_host_srv3 } +import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4 } import extdeps.exec.command { shell_command_render } test fn witness_actions_runner_release_cites_github_digest() -> Bool { @@ -55,17 +70,30 @@ test fn witness_runner_count_not_in_installer_argv() -> Bool { && (string_contains(s: rendered, pattern: "CTRL_RUNNER_SLOT") == false) } -test fn witness_srv3_deploy_row_names_six_slots() -> Bool { - list_length(items: runner_instance_names(deploy: srv3_runner_host_deploy)) == 6 - && string_contains(s: runner_instance_names(deploy: srv3_runner_host_deploy).first(), pattern: "srv3-01") - && string_contains(s: runner_instance_names(deploy: srv3_runner_host_deploy).skip(n: 5).first(), pattern: "srv3-06") +// THE NAMING IS WHAT THIS ROW CHECKS; THE WIDTH LITERAL IT USED TO CARRY IS GONE. +// +// It read `== 6` on both the count and the last instance name, which was a measurement copied from +// the tree the day it was written. The 2026-08-23 CPU-axis change moved srv3 to twenty-one and the +// row went red without a single thing about instance NAMING having changed -- which is the tell that +// the literal was never the claim (DESIGN section 5: a measurement copied from the same current tree +// is not an oracle). +// +// What survives is the part a fixture can falsify independently of width: the roster is exactly as +// long as the row says it is, it is one-based, and it is zero-padded. Width itself is asserted where +// width is decided, not restated here. +test fn witness_srv3_deploy_row_names_its_declared_slots() -> Bool { + let names = runner_instance_names(deploy: srv3_runner_host_deploy) + list_length(items: names) == srv3_runner_host_deploy.runner_count + && string_contains(s: names.first(), pattern: "srv3-01") + && list_length(items: names) > 1 + && roster_names_are_distinct(names: names) } // The reconcile fixtures plant their OWN five-slot deploy row rather than // reading the live fleet, so the expected counts below are exact literals // authored beside a known input — not a restatement of whatever width the // fleet happens to declare. srv3's real width is asserted separately, by -// witness_srv3_deploy_row_names_six_slots. +// witness_srv3_deploy_row_names_its_declared_slots. fn fixture_five_slot_deploy() -> RunnerHostDeploy { RunnerHostDeploy { host_label: "wfix", @@ -134,7 +162,188 @@ test fn witness_enumeration_postcondition_red_on_under_count() -> Bool { } } -test fn witness_srv4_runner_count_six_materialization_target() -> Bool { - srv4_runner_host_deploy.runner_count == 6 - && list_length(items: runner_instance_names(deploy: srv4_runner_host_deploy)) == 6 +// SAME CORRECTION AS srv3 ABOVE, and the same reason: this row pinned six on both sides of an `&&`, +// so it measured the tree rather than checking a relation. The relation it was reaching for is that +// the instance roster and the declared count cannot disagree, which holds at any width. +test fn witness_srv4_instance_roster_matches_its_declared_count() -> Bool { + let names = runner_instance_names(deploy: srv4_runner_host_deploy) + list_length(items: names) == srv4_runner_host_deploy.runner_count + && roster_names_are_distinct(names: names) +} + +// A LENGTH IS NOT A ROSTER, AND EVERY PURE LENGTH ASSERTION IN THIS FILE HAD THIS HOLE. +// +// A generator emitting ONE name N times satisfies `list_length(names) == count` perfectly while +// deploying a single runner N ways -- N units all pointing at one slot directory, one registration +// name contending with itself. The count check cannot see it because the count is right. +// +// Found by silent-bear-842, who independently rewrote these rows and asked what a length assertion +// does NOT cover before shipping. Kept as a named function rather than inlined because it belongs +// beside every length claim, not just this one. +fn roster_names_are_distinct(names: List) -> Bool { + !any(names, a => list_length(items: filter(names, b => b == a)) > 1) +} + +// THE INDEXING CONTRACT, PINNED ON GROUND THAT CANNOT MOVE. +// +// The rows this file used to carry asserted srv3-01 and srv3-06 by name -- one-based, zero-padded, +// last index equals count. Those were real claims and they were deleted along with the width +// literals they were entangled with, because every index expectation was a function of a width the +// CPU axis then moved. Deriving the expectation from the width would have made it vacuous: the +// enumerator would be checked against itself. +// +// An AUTHORED runner_count breaks that circle. Three is a number the allocation authority never +// produced and never will, so this row pins one-basedness, zero-padding and the count-to-last-index +// relation without consulting the fleet at all. That is the planted-fixture side of the +// authority-witness / boundary-probe split: a fixture that authors its own input SHOULD carry +// literals, and only a probe aimed at a live authority must derive its discriminator. +// +// Measured discriminating rather than assumed: under a planted one-off in runner_instance_names +// (mapping over runner_count - 1) this row returns false, as do the two length rows above +// (silent-bear-842). +data authored_three_slot_deploy: RunnerHostDeploy = RunnerHostDeploy { + host_label: "fixture-host", + ssh_target: "fixture@203.0.113.1", + runner_user: "fixture", + job_user: "fixturejob", + app: gunbc_ci_github_app, + runner_count: 3, +} + +test fn an_authored_count_enumerates_exactly_that_many_indexed_names() -> Bool { + let names = runner_instance_names(deploy: authored_three_slot_deploy) + list_length(items: names) == 3 + && string_contains(s: names.first(), pattern: "fixture-host-01") + && string_contains(s: names.skip(n: 2).first(), pattern: "fixture-host-03") + && roster_names_are_distinct(names: names) +} + +// --- converge seam: the refusal must be real, not decorative ---------------------------------- + +data converge_seam_witness_note: String = "THESE FOUR ROWS EXIST BECAUSE THE REFUSAL ARM IS THE ENTIRE POINT OF THE SEAM. An observation type with an Unobserved arm that nothing can drive is a decoration -- permanently green by construction and worse than absent, because it gets cited as coverage. The fixture below authors the unobserved state directly, so the arm has a RED that a fixture may produce, and the planned control beside it stops the refusal being satisfied by refusing always." + +data unobserved_fixture: RunnerSlotObservation = RunnerSlotsUnobserved { + reason: "FIXTURE: the base-directory listing refused" as NonEmptyStr, +} + +data observed_two_fixture: RunnerSlotObservation = RunnerSlotsObserved { + members: [ + runner_slot_member_from_instance_name(instance_name: "srv1-01"), + runner_slot_member_from_instance_name(instance_name: "srv1-02"), + ], +} + +// THE DISCRIMINATING RED. An unreadable host must not produce a plan, because a plan built on an +// unread population proposes installing every desired slot onto a machine whose real state nobody +// saw. This is the arm that turns a silent overwrite into a stop. +test fn an_unobserved_host_refuses_instead_of_planning() -> Bool { + match actions_runner_binary_artifact_for_arch(binary_release: actions_runner_release_2_334_0, arch: Aarch64) { + Absent => false + Present { value: artifact } => + match runner_slot_converge_verdict( + host: operator_host_srv1, + deploy: srv1_runner_host_deploy, + artifact: artifact, + observation: unobserved_fixture, + ) { + RunnerSlotConvergeRefused { host: h, reason: _ } => (h as String) == (operator_host_srv1 as String) + RunnerSlotConvergePlanned { host: _, plan: _ } => false + } + } +} + +// THE POSITIVE CONTROL, without which the row above is satisfied by a seam that refuses everything. +// srv1 commits twenty-one and two slots are observed, so a plan must be produced AND must propose +// adding the nineteen that are missing. +test fn an_observed_host_plans_the_missing_slots() -> Bool { + match actions_runner_binary_artifact_for_arch(binary_release: actions_runner_release_2_334_0, arch: Aarch64) { + Absent => false + Present { value: artifact } => + match runner_slot_converge_verdict( + host: operator_host_srv1, + deploy: srv1_runner_host_deploy, + artifact: artifact, + observation: observed_two_fixture, + ) { + RunnerSlotConvergePlanned { host: _, plan: p } => + runner_slot_provision_has_width_increase(plan: p) + && membership_added_count(plan: p.membership) == (srv1_runner_host_deploy.runner_count - 2) + RunnerSlotConvergeRefused { host: _, reason: _ } => false + } + } +} + +// EVERY ENROLLED HOST RESOLVES TO A DEPLOY ROW, which is the gap this change closed. Before it, +// srv1 and srv2 had no row at all, so the width authority could say twenty-one and nothing could +// act on it. +test fn every_enrolled_host_has_a_deploy_row() -> Bool { + all( + [operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4], + h => match runner_host_deploy_for(host: h) { + RunnerHostDeployFound { deploy: d } => (d.host_label as String) == (h as String) + RunnerHostDeployUnmodeled { host: _ } => false + } + ) +} + +// AND AN UNMODELED HOST REFUSES RATHER THAN BORROWING A NEIGHBOUR'S ROW -- the arm that stops a +// fifth machine being provisioned against srv4's ssh_target and slot count. +test fn an_unmodeled_host_has_no_deploy_row() -> Bool { + match runner_host_deploy_for(host: "srv-does-not-exist" as HostIdentity) { + RunnerHostDeployUnmodeled { host: h } => (h as String) == "srv-does-not-exist" + RunnerHostDeployFound { deploy: _ } => false + } +} + +// NO DEPLOY ROW OUT-COMMITS THE MEMORY BUDGET, and this is a join between two authorities rather +// than a restatement of one. +// +// runner_count derives from gunbc.runner_slot_allocation gunbc_runner_slots_per_host, which is the +// MINIMUM over the memory, CPU and disk axes. gunbc.fleet_host_budget declared_runner_count_for is +// the memory axis alone, computed from the pool budget and the per-runner cgroup cap by a different +// route. Asserting equality between them would be wrong as well as vacuous -- since the 2026-08-23 +// CPU-axis change the CPU axis binds first on srv1, srv3 and srv4, so the two numbers legitimately +// differ (twenty-one committed against a memory admission of twenty-seven or twenty-nine). +// +// The relation that must hold in every case is the inequality: materialization may commit fewer +// slots than memory would admit, never more. That is falsifiable -- a deploy row raised past its +// memory admission fails here -- and it does not collapse into f(x) == f(x). +test fn no_deploy_row_out_commits_the_memory_budget() -> Bool { + all( + fleet_runner_host_deploys, + d => d.runner_count <= declared_runner_count_for(host: d.host_label as HostIdentity) + && d.runner_count > 0 + ) +} + + +// --- the fabric carve reaches the provisioning target -------------------------------------------- + +// THE DESIRED SET MUST NOT CONTAIN srv3-06, AND THIS IS THE ROW THAT SAYS SO. +// +// desired_runner_slot_members built 1..runner_count until 2026-08-23, which meant converge would +// have proposed installing a GitHub Actions runner over srv3's fabric execution slot -- and +// reconcile would have seen it as an ordinary missing member, so apply would have done it with no +// refusal anywhere. The width says how many slots exist; it does not say what they are for. +test fn the_fabric_slot_is_not_a_provisioning_target() -> Bool { + let names = map( + desired_runner_slot_members(deploy: srv3_runner_host_deploy), + m => runner_slot_member_key(m: m) as String, + ) + (any(names, n => n == "srv3-06") == false) + && any(names, n => n == "srv3-05") + && any(names, n => n == "srv3-07") +} + +// THE POSITIVE CONTROL AND THE ARITHMETIC, without which the row above is satisfied by a desired set +// that is simply too small. srv3 gives up exactly one slot to the fabric; every other host carries +// no fabric member and loses nothing. +test fn only_the_fabric_host_loses_a_provisioning_target() -> Bool { + list_length(items: desired_runner_slot_members(deploy: srv3_runner_host_deploy)) + == gunbc_runner_slots_per_host(host: operator_host_srv3) - 1 + && host_fabric_slot_count(host: operator_host_srv3) == 1 + && list_length(items: desired_runner_slot_members(deploy: srv4_runner_host_deploy)) + == gunbc_runner_slots_per_host(host: operator_host_srv4) + && list_length(items: desired_runner_slot_members(deploy: srv1_runner_host_deploy)) + == gunbc_runner_slots_per_host(host: operator_host_srv1) }