diff --git a/DESIGN.md b/DESIGN.md index 68c5b72aeaf..5a73f4ebc94 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -131,6 +131,7 @@ Every newly discovered error class — incident, review finding, runtime excepti - **Required gate reduced to the compiler floor** — declared 2026-08-29 - **Non-literal kernel-String refusal at the structural text boundary** — declared 2026-08-30 - **Fabric CI evidence lane as a required merge block** — declared 2026-08-31 +- **Spark serving role-scoped retirement evidence at the production plan root** — declared 2026-09-02 - **Arity agreement between a declared builtin parameter name and its derived algebra template** — declared 2026-09-01 - **n-ary concat call sites judged against concat's binary declared signature** — declared 2026-09-01 diff --git a/dag/extdeps/deepseek/deepspec.dag b/dag/extdeps/deepseek/deepspec.dag new file mode 100644 index 00000000000..06ce8f791f5 --- /dev/null +++ b/dag/extdeps/deepseek/deepspec.dag @@ -0,0 +1,254 @@ +module extdeps.deepseek.deepspec + +import std.types { String, Bool, List, Int, NonEmptyStr } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +import std.decl_ref { DeclarationRef, WholeDeclaration } + +// DEEPSPEC, DEEPSEEK'S SPECULATIVE-DECODING CODEBASE, AND THE THREE DRAFT ALGORITHMS IT SHIPS. +// +// THIS MODULE EXISTS BECAUSE OF A NAME COLLISION THAT COST REAL WORK. "dspark" was used across two +// sessions and an operator conversation to mean NVIDIA's `dgx-spark-playbooks` -- the DGX Spark +// hardware recipes, `connect-two-sparks` and its vLLM multi-node section. The operator meant DSpark, +// DeepSeek's speculative-decoding algorithm. One spelling, two independently governed upstreams, +// nothing in common: the §3 meaning fork, discovered only when the operator asked directly whether +// we were on the same page. A fabric, a Ray topology and a privileged-container decision were all +// pursued under the wrong referent. +// +// So the two subjects are named apart and neither is ever spelled "dspark" bare in this repository. +// This module is the DeepSeek one. NVIDIA's playbooks are a different authority and belong under +// their own vendor path. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/deepseek-ai/DeepSpec" + } +} + +data dspark_paper_citation: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "arxiv.org/abs/2607.05147" + } +} + +data dflash_paper_citation: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "arxiv.org/abs/2602.06036" + } +} + +data eagle3_paper_citation: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "arxiv.org/abs/2503.01840" + } +} + +// ONE SUBJECT, SEVERAL CITATIONS. The subject is the DeepSpec codebase, which is what governs the +// roster below: the three algorithms are ITS enumeration, carried in its own `config/` tree, and a +// fourth would arrive as a commit to that repository. The per-algorithm papers are further +// citations rather than separate subjects for the same reason -- Eagle3 is not DeepSeek's work at +// all, and modelling it as its own upstream product here would claim an authority this module does +// not have. +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.deepseek.deepspec", + decl_name: "SpeculativeDraftAlgorithm", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [dspark_paper_citation, dflash_paper_citation, eagle3_paper_citation], +} + +// The three draft algorithms DeepSpec implements. Closed, because the roster is the upstream's own +// and an unmodeled fourth should be absent rather than approximated. +type SpeculativeDraftAlgorithm + = DSpark + | DFlash + | Eagle3 + +fn speculative_draft_algorithm_wire(a: SpeculativeDraftAlgorithm) -> NonEmptyStr { + match a { + DSpark => "dspark" as NonEmptyStr + DFlash => "dflash" as NonEmptyStr + Eagle3 => "eagle3" as NonEmptyStr + } +} + +fn speculative_draft_algorithm_eq(a: SpeculativeDraftAlgorithm, b: SpeculativeDraftAlgorithm) -> Bool { + (speculative_draft_algorithm_wire(a: a) as String) + == (speculative_draft_algorithm_wire(a: b) as String) +} + +// HOW THE DRAFT REACHES THE HOST, WHICH IS TWO DIFFERENT FACTS AND WAS FIRST MODELLED AS ONE. +// +// A speculative draft is published in one of two shapes, and this repository has a live example of +// each for the SAME base model: +// +// - SEPARATE ARTIFACT. The draft is its own file beside the base weights. DeepSpec's released +// checkpoints are this shape, and so are the three `DeepSeek-V4-Flash-DSpark-support.gguf` +// files in the antirez GGUF distribution. Here "base" and "base plus draft" are two totals you +// can choose between, because they are two downloads. +// +// - FUSED INTO THE CHECKPOINT. The draft ships INSIDE the weights as extra layers. +// deepseek-ai/DeepSeek-V4-Flash-DSpark is this shape: 48 shards against the plain repo's 46, +// same DeepseekV4ForCausalLM architecture and same fp8/e4m3/ue8m0 quantization, plus +// num_nextn_predict_layers 1 and the dspark_* configuration. DeepSeek's own model card states +// it: "not a new model. It is the same checkpoint with an additional speculative decoding +// module attached." +// +// THE DISTINCTION IS LOAD-BEARING FOR FIT, WHICH IS WHY IT IS A TYPE. In the fused shape there is no +// download that gets you the base alone -- that is a DIFFERENT REPOSITORY -- so a consumer that +// reasons about "base_total, plus the draft if enabled" computes a residency figure no disk will +// ever hold. Measured: the plain repo is 159.6 GB over 46 shards, the DSpark repo 166.9 GB over 48. +// 166.9 is the only number that predicts the disk and the memory for the artifact actually being +// deployed; 159.6 names a repository deliberately not in use. +type SpeculativeDraftAttachment + = DraftAsSeparateArtifact + | DraftFusedIntoCheckpoint + +fn speculative_draft_attachment_wire(a: SpeculativeDraftAttachment) -> NonEmptyStr { + match a { + DraftAsSeparateArtifact => "separate-artifact" as NonEmptyStr + DraftFusedIntoCheckpoint => "fused-into-checkpoint" as NonEmptyStr + } +} + +// Whether the base weights are separately obtainable from this publication. Only the separate shape +// admits it, and a consumer sizing a deployment must ask THIS rather than subtracting. +fn base_weights_separately_obtainable(a: SpeculativeDraftAttachment) -> Bool { + match a { + DraftAsSeparateArtifact => true + DraftFusedIntoCheckpoint => false + } +} + +// A DRAFT IS BOUND TO ONE TARGET, AND THAT IS THE WHOLE SAFETY CONTENT OF THIS MODULE. +// +// DeepSpec's released checkpoints are a grid of (algorithm x target): dspark_qwen3_4b_block7 exists +// because it was TRAINED AGAINST Qwen/Qwen3-4B, on answers that model generated. The README states +// the binding directly -- `target_name_or_path` is a required evaluation input beside +// `draft_name_or_path`, and it warns that a comparison whose setup differs from the training +// settings "is not meaningful". +// +// The failure this prevents is quiet rather than loud. Speculative decoding is designed to be +// output-equivalent to the target: the draft proposes, the target verifies, and rejected tokens are +// discarded. So a draft paired with the WRONG target does not produce wrong text -- it produces the +// same text, more slowly, while every acceptance-rate and throughput number measured from it +// describes a configuration nobody intended. It is a performance claim that silently detaches from +// its subject, which is precisely the class this repository refuses to leave to review. +// +// Hence: a draft binding carries its target, and equality of the pair is what a consumer joins on. +// There is no constructor for an unbound draft. +type SpeculativeDraftBinding sole_constructor { + algorithm: SpeculativeDraftAlgorithm + attachment: SpeculativeDraftAttachment + draft_repository: NonEmptyStr + target_repository: NonEmptyStr + draft_block_size: Int +} + +fn speculative_draft_binding( + algorithm: SpeculativeDraftAlgorithm, + attachment: SpeculativeDraftAttachment, + draft_repository: NonEmptyStr, + target_repository: NonEmptyStr, + draft_block_size: Int, +) -> SpeculativeDraftBinding? { + if draft_block_size < 1 { + none + } else if (draft_repository as String) == (target_repository as String) { + none + } else { + Present { value: SpeculativeDraftBinding { + algorithm: algorithm, + attachment: attachment, + draft_repository: draft_repository, + target_repository: target_repository, + draft_block_size: draft_block_size, + } } + } +} + +// Whether a draft may be used to accelerate a given target. It is an identity join on the repository +// the draft was trained against, never a similarity judgement about names. +fn draft_serves_target(binding: SpeculativeDraftBinding, target_repository: NonEmptyStr) -> Bool { + (binding.target_repository as String) == (target_repository as String) +} + +// ============ THE PUBLISHED CHECKPOINTS THIS REPOSITORY HAS GROUNDED ============ +// +// The Table 1 grid from the DeepSpec README, read from the repository rather than recalled. Block +// size 7 is carried because it is in the checkpoint name and is a real parameter of the algorithm -- +// DSpark drafts a BLOCK per forward pass, so the block size bounds how many tokens one draft step +// can propose. +data dspark_qwen3_4b_block7: SpeculativeDraftBinding? = speculative_draft_binding( + algorithm: DSpark, + attachment: DraftAsSeparateArtifact, + draft_repository: "deepseek-ai/dspark_qwen3_4b_block7" as NonEmptyStr, + target_repository: "Qwen/Qwen3-4B" as NonEmptyStr, + draft_block_size: 7) + +data dspark_qwen3_8b_block7: SpeculativeDraftBinding? = speculative_draft_binding( + algorithm: DSpark, + attachment: DraftAsSeparateArtifact, + draft_repository: "deepseek-ai/dspark_qwen3_8b_block7" as NonEmptyStr, + target_repository: "Qwen/Qwen3-8B" as NonEmptyStr, + draft_block_size: 7) + +data dspark_qwen3_14b_block7: SpeculativeDraftBinding? = speculative_draft_binding( + algorithm: DSpark, + attachment: DraftAsSeparateArtifact, + draft_repository: "deepseek-ai/dspark_qwen3_14b_block7" as NonEmptyStr, + target_repository: "Qwen/Qwen3-14B" as NonEmptyStr, + draft_block_size: 7) + +// THE V4-FLASH RELEASE, WHICH IS THE ONE THIS FLEET DEPLOYS, AND A CORRECTION. +// +// An earlier revision of this module stated that no published DeepSpec checkpoint existed for +// DeepSeek-V4-Flash and that the only DSpark artifacts for it were a distributor's packaging. That +// was wrong, and it was wrong in the direction that matters: deepseek-ai/DeepSeek-V4-Flash-DSpark is +// a first-party DeepSeek release. Verified from the Hub rather than recalled -- 48 shards against +// the plain repository's 46, DeepseekV4ForCausalLM, dspark_block_size 5, +// dspark_target_layer_ids [40, 41, 42], dspark_markov_rank 256, num_nextn_predict_layers 1. +// +// Note the block size is FIVE here, not the 7 of the Qwen grid above. The block size is a property +// of the trained draft, not of the algorithm, which is exactly why it is a field on the binding. +data dspark_deepseek_v4_flash: SpeculativeDraftBinding? = speculative_draft_binding( + algorithm: DSpark, + attachment: DraftFusedIntoCheckpoint, + draft_repository: "deepseek-ai/DeepSeek-V4-Flash-DSpark" as NonEmptyStr, + target_repository: "deepseek-ai/DeepSeek-V4-Flash" as NonEmptyStr, + draft_block_size: 5) + +// THE SERVING FLAG, CARRIED HERE BECAUSE THE UPSTREAM SPELLS IT. +// +// DeepSeek's model card gives the exact vLLM enablement: +// --speculative-config '{"method":"dspark","num_speculative_tokens":7,"draft_sample_method":"greedy"}' +// It is modeled as the method NAME the engine expects rather than as the whole argv, because the +// token count and sampling method are deployment policy and belong to the workflow layer, not to +// this dependency (DESIGN §3: interface, realization and policy are three facts). +// +// This also settles a question that was open and being treated as a project risk: vLLM DOES +// implement DSpark as a speculative method. What remains genuinely unverified is whether the +// specific engine BUILD a deployment pins carries it, and that is an observation about that build, +// not a fact about this upstream. +fn vllm_speculative_method_name(a: SpeculativeDraftAlgorithm) -> NonEmptyStr { + speculative_draft_algorithm_wire(a: a) +} + +// The GGUF distribution's `*-DSpark-support.gguf` files are NOT modeled here. They are a +// distributor's repackaging, and a distributor's artifact is a receipt in the observing layer +// (gunbc.model.publication), never a property authored inside this upstream. Whether one of them is +// a DSpark draft bound to a V4-Flash build is an OBSERVATION somebody must make. +fn deepspec_released_dspark_bindings() -> List { + flat_map([dspark_qwen3_4b_block7, dspark_qwen3_8b_block7, dspark_qwen3_14b_block7, dspark_deepseek_v4_flash], b => + match b { + Present { value: v } => [v] + Absent => [] + }) +} diff --git a/dag/extdeps/network/ipv4.dag b/dag/extdeps/network/ipv4.dag index d7361ec37ba..91e1bd6626a 100644 --- a/dag/extdeps/network/ipv4.dag +++ b/dag/extdeps/network/ipv4.dag @@ -66,6 +66,42 @@ fn render_ipv4_address(addr: Ipv4Address) -> NonEmptyStr { ], ".") as NonEmptyStr } +// A PREFIX LENGTH IS PART OF THE ADDRESS AUTHORITY, not a bare Int at each consumer. It uses the +// same `Int where range` idiom Octet above uses, for the same reason: /33 has no constructor rather +// than a validator. The upper bound is 32 because this is the IPv4 module; IPv6 prefixes are a +// different authority's concern. +type PrefixLength = Int where range(min: 0, max: 32) + +// The CIDR spelling, which is what /etc/netplan, `ip addr` and every router table write. It is a +// rendering of two facts this module already owns, not a third representation of an address. +fn render_ipv4_cidr(addr: Ipv4Address, prefix: PrefixLength) -> NonEmptyStr { + join([render_ipv4_address(addr: addr) as String, to_string(prefix)], "/") as NonEmptyStr +} + +// Whether two addresses share a network at a given prefix. Written as an octet-wise comparison over +// the four whole octets a /8, /16, /24 or /32 fixes, plus the partial octet a /30 splits -- so it is +// exact for the prefixes this repository actually uses and REFUSES to answer for the rest, rather +// than approximating. A /30 is the point-to-point case every fabric link here is built from. +fn ipv4_same_network(a: Ipv4Address, b: Ipv4Address, prefix: PrefixLength) -> Bool? { + if prefix == 30 { + Present { value: a.octet1 == b.octet1 && a.octet2 == b.octet2 && a.octet3 == b.octet3 && (a.octet4 / 4) == (b.octet4 / 4) } + } else if prefix == 24 { + Present { value: a.octet1 == b.octet1 && a.octet2 == b.octet2 && a.octet3 == b.octet3 } + } else if prefix == 16 { + Present { value: a.octet1 == b.octet1 && a.octet2 == b.octet2 } + } else if prefix == 8 { + Present { value: a.octet1 == b.octet1 } + } else if prefix == 32 { + Present { value: ipv4_address_eq(a: a, b: b) } + } else { + none + } +} + +fn ipv4_address_eq(a: Ipv4Address, b: Ipv4Address) -> Bool { + a.octet1 == b.octet1 && a.octet2 == b.octet2 && a.octet3 == b.octet3 && a.octet4 == b.octet4 +} + type OctetResult = OctetOk { value: Octet } | OctetErr { error: Ipv4ParseError } diff --git a/dag/gunbc/fleet/fleet_intent_network.dag b/dag/gunbc/fleet/fleet_intent_network.dag index 093648ff25b..0390d9fe1df 100644 --- a/dag/gunbc/fleet/fleet_intent_network.dag +++ b/dag/gunbc/fleet/fleet_intent_network.dag @@ -23,6 +23,24 @@ data operator_host_srv3: HostIdentity = "srv3" data operator_host_srv4: HostIdentity = "srv4" // SPARK-LANE-A (2026-08-06). srv5/srv6 are the operator's HostIdentity slots for the two ordered NVIDIA DGX Spark units (gunbc.spark.dgx_procurement). They live here because HostIdentity naming is this module's single authority — SPARK-0 minted `srv5_reserved`/`srv6_reserved` privately inside the procurement module only because this file was mid-refactor and out of scope, which was a §3 fork of one concept (a host's fleet identity) across two homes; those private rows are deleted and the procurement module imports these. NAMING AN IDENTITY IS NOT ENROLLMENT, and that distinction is carried structurally rather than by this prose: enrollment is membership in `fleet_intent_network.endpoints` (and in gunbc.fleet_intent's ComputeHost list), and srv5/srv6 appear in neither. Updated 2026-08-07 for the arrived state: both units are now live on the LAN and the operator has authored two static reservations for them (spark-a3ee 192.168.1.222 and spark-3bd5 192.168.1.223, both MACs ARP-confirmed — SUPERSEDED, see the SPARK-WIFI-0 clause at the end of this note), so the missing fact is no longer the addresses. CORRECTED 2026-08-23: THE SLOT ASSIGNMENT IS ALSO NO LONGER MISSING, AND THIS NOTE WENT ON ASSERTING THAT IT WAS. It read that the operator "supplied the router table but never stated the assignment", so authoring an address here would be a 50/50 guess and thus the fabricated-plausible-output failure DESIGN §5 forbids. The decision exists and is one import away: gunbc.spark.dgx_procurement `dgx_spark_router_binding_operator_allocation` records srv5 taking spark-a3ee and srv6 taking spark-3bd5, decided 2026-08-07 under an explicit operator delegation, on an ascending-address-order basis kept precisely so the tie-break is attributable rather than looking like a measurement; `srv5_router_binding` and `srv6_router_binding` are both SlotAssigned carrying it. The two notes are the same date — the stated blocker was resolved the day it was written. THE DOCTRINE WAS INVOKED AGAINST THE WRONG TARGET, which is why this is a correction and not a refresh: §5 forbids fabricating an OBSERVATION, and an attributable ALLOCATION with a decider, a date and a basis is not one. This is the stale-citation class in its expensive form — a rotted REASON rather than a rotted line number — and it propagated: a lane read it, believed Spark work was blocked on an operator fact, and reported that upward before anyone opened the procurement carrier. WHAT IS STILL TRUE, and is why no endpoint row is added here: srv5/srv6 remain absent from `endpoints` and from gunbc.fleet_intent's ComputeHost list, because in this module that membership IS enrollment — authoring the rows would enroll them, not merely describe them — and there is nothing to enroll into while the units are unplugged and the converge timer is retired. A PROJECTED ENDPOINT ALSO CANNOT LIVE HERE, and that is structural rather than a preference: gunbc.spark.dgx_procurement imports THIS module for operator_host_srv5/srv6, so the reverse import is refused by the import graph's one law — measured, not inferred, by adding it and compiling: `circular dependency detected: gunbc.fleet_intent_network -> gunbc.spark.dgx_procurement`. Anyone who later wants the endpoints projected from the binding starts from that constraint. Until enrollment genuinely happens, the address authority stays single because there is only ever one — the reservation rows in the procurement module. SPARK-WIFI-0 (2026-08-27): TWO THINGS IN THIS NOTE WENT STALE AT ONCE, and both are corrected in the procurement module rather than here, because that is where the address authority lives. First, the addresses: the operator moved both units onto the LAN's wireless SSID, unplugged both ethernet cables, and authored fresh CR1000A reservations keyed to the RADIO MACs — spark-a3ee is now 192.168.1.226 (F0:68:E3:B3:1A:40) and spark-3bd5 is now 192.168.1.225 (F0:68:E3:31:AB:E6). A DHCP reservation binds a MAC, and a radio has its own, so the ethernet-keyed rows could not follow the units across the medium change. Second, and more consequentially for anyone reading this note for a reason: THE UNITS ARE NO LONGER UNPLUGGED. The clause above gives "the units are unplugged and the converge timer is retired" as the standing reason there is nothing to enroll into, and the first half of that is now false — both boxes are live, reachable, and answering SSH on their enrolled host keys, which were re-scanned at the new addresses and matched exactly. Enrollment is still NOT performed here, and that is deliberate rather than leftover: membership in `endpoints` IS enrollment in this module, so authoring the rows is the act itself and belongs to the roadmap node that owns it, not to an address correction. What changed is the REASON — from "there is nothing to enroll" to "enrolling is a decision nobody has taken yet" — and that distinction is exactly the rotted-reason class this note already documents itself falling into once. +// SPARK-PAIR-1 (2026-09-02). srv7/srv8 are the operator's HostIdentity slots for the SECOND DGX +// Spark pair -- spark-c2b1 at 192.168.1.232 and spark-ac79 at 192.168.1.233 on the wireless LAN, +// cross-cabled to each other on dual direct-attach 200G ports. They are NAMED here and, exactly as +// the srv5/srv6 note above sets out, naming is not enrollment: neither appears in `endpoints` or in +// gunbc.fleet_intent's ComputeHost list, so this row describes them without admitting them. +// +// They are named now because the fabric addressing between them is real, durable and modeled -- +// gunbc.spark.fabric_link_desired reads it back from /etc/netplan on both hosts -- and that module +// needs an identity for each end. An address-carrying model keyed on a raw hostname string would be +// the §3 fork this note already documents once. +// +// WHAT IS STILL MISSING, stated as the remaining acts rather than as a blocker: adoption is five +// separable things -- physical adoption, host and network identity, fleet enrollment, cell-role +// assignment, assembly membership -- and this row is the second alone. Convergence cannot manage +// these hosts until enrollment happens, which is why the fabric on them was configured by hand. +data operator_host_srv7: HostIdentity = "srv7" +data operator_host_srv8: HostIdentity = "srv8" + data operator_host_srv5: HostIdentity = "srv5" data operator_host_srv6: HostIdentity = "srv6" diff --git a/dag/gunbc/rung_drop.dag b/dag/gunbc/rung_drop.dag index 161f7d53d26..312cea07168 100644 --- a/dag/gunbc/rung_drop.dag +++ b/dag/gunbc/rung_drop.dag @@ -101,6 +101,7 @@ data direct_call_arg_seam_v2_exemption: RungDrop = RungDrop { } data floor_cost_contention_verdict: RungDrop = RungDrop { identity: "floor_cost_contention_verdict" as NonEmptyStr, subject: "Stable per-claim cost qualification under a shared execution envelope", declared: "2026-09-01", standing: Standing, authored: "Required floor cost — **RUNG DROP, DECLARED (2026-09-01).** SUBJECT: stable per-claim cost qualification under a shared execution envelope. WHAT IS LOST: an attempt's CPU duration cannot be read as an invariant property of the witness, nor as proof of a witness-owned regression. `required_floor_claim_cpu_safety_limit_ms` is a cpu-ms literal compared against a measurement taken on a shared runner, so a row that exceeds it may have done nothing but run beside somebody else's build. THE MEASUREMENT IS NOT WRONG AND THIS ROW DOES NOT SAY SO: it is a VALID observation of THIS EXECUTION ATTEMPT. What it is not is a stable observation of the claim as an isolated subject, and only the second reading is what a cost verdict needs. WHAT REMAINS, AND STAYS REQUIRED: the 500ms attempt-safety stop, and fail-closed treatment of a required claim that produced no verdict. Contention disqualifies the deadline as an INTRINSIC CLAIM-COST VERDICT; it does not disqualify it as a REQUIRED ATTEMPT-SAFETY AND VERDICT-AVAILABILITY criterion. Both terminal arms stay required reds and are distinct: an interrupted attempt means the required claim never produced a semantic verdict, and a completed-past-limit attempt means it crossed the declared safety envelope. Neither proves the witness intrinsically costs more than the limit, that it regressed, that it owns the observed excess, or that it belongs in permanent cost debt. A shared runner producing false refusals is an AVAILABILITY loss that fails closed, and removing the deadline would let genuinely runaway evaluation consume the executor without bound. PREVIOUS RUNG: none for environment-independent claim-cost qualification -- that guarantee was never held, and saying it was would be inventing a rung to drop from. Mechanically preventable remains TRUE and undropped for attempt safety. TEMPORARY RUNG: claim-cost qualification UNAVAILABLE; verdict availability environment-sensitive; acceptance still fail-closed. REASON, and the three negative results that make this a capability claim rather than a shrug. (1) THE BASIS IS ALREADY CPU BY DECLARATION: `required_floor_cost_basis` returns `CpuCost` because these claims execute Hermetic, so 'judge cpu rather than wall' is DONE and what remains is cpu-time variance itself. (2) THE OBVIOUS CALIBRATOR IS REFUTED BY MEASUREMENT, and this is the sentence that stops the trigger being discharged by pointing at what we already measure: THE PREPARATION WARM PHASES ARE NOT A CALIBRATOR. Across main and two attempts of one identical tree, `pool-root-index-warm` measured 693 / 727 / 596 cpu-ms and `languages-consumer-census-warm` measured 858 / 606 / 531, so on the attempt whose CLAIMS ran hottest the census phase ran COLDER than main's. They do not track claim inflation. (3) NO CALIBRATION CONCEPT EXISTS IN THE REPOSITORY AT ALL. Normalizing by a quantity that does not track the machine would produce a threshold that LOOKS principled and is not, which is strictly worse than the honest literal. POPULATION -- THE CLOSED SUBJECT UNIVERSE IS NOT A THRESHOLD-SELECTED SET, AND THIS ROW SAID OTHERWISE FOR TWO REVISIONS. The universe is EVERY REQUIRED IDENTITY FOR WHICH THE CPU DEADLINE IS ARMED WHILE IT EXECUTES UNDER THE UNCONTROLLED SHARED-RUNNER ENVELOPE. That is closed, decidable from the run's own plan, and it does not move with anyone's measurement. WHY THE THRESHOLD SET IS NOT THAT UNIVERSE: the contention term is unbounded, so NO lower threshold can prove the rows beneath it unaffected. A set selected by 'measured cpu at or above N' is a VIEW whose membership is a property of the MEASUREMENT rather than of the subject, and letting a decidable admission predicate's output stand in for the class's population joins two different objects by an assumption. The predicate was the right answer to a censored-parameter refusal and the wrong answer to 'what is the population'. THE THRESHOLD SET SURVIVES AS AN EXPOSED ATTENTION SUBSET, which is what it is good for: prioritising optimisation and isolation work. Admission is measured cpu at or above the attention constant -- 280ms against the 500ms ceiling, the ceiling over the largest inflation floor observed to date -- and the constant is spelled ONCE here, with every later reference in this row naming it rather than repeating the digits, because a constant that has already moved twice in one day reforks the row on its next revision if it is spelled in three places. THAT SINGLE-SPELLING DISCIPLINE IS PROSE AND NOT STRUCTURE: `RungDrop` carries no numeric field, so nothing refuses a future revision that updates one mention and not another. That missing field is this discipline's next rung. THE ATTENTION CONSTANT'S OWN DERIVATION AND REVISION CONDITION: it is the ceiling over an inflation FLOOR of 1.777, measured by identity join -- `v2.test.execution.emit_host_meet_join_equals_eval.emit_host_meet_wrong_fixture_refuses_holds` measured 501 cpu-ms on one attempt and 282 on a re-run of THE SAME TREE with nothing changed. A floor is not the inflation, so the constant MUST BE RE-DERIVED THE MOMENT A LARGER FLOOR IS MEASURED. Its predecessor was falsified within the hour for exactly this reason: sized at 400 against a floor of 1.196, it EXCLUDED the one row this class has been observed to trip on the completed-past-limit arm, and an admission rule that omits a known member is wrong at its own grain. TWO OBJECTS, ONE MONOTONE AND ONE NOT, AND THIS ROW PREVIOUSLY CONFLATED THEM: the EVIDENCE FLOOR is monotone -- the largest observed inflation floor can only rise, so the constant derived from it can only fall. THE MEMBERSHIP SET IS NOT MONOTONE: individual identities enter and leave the attention subset as their measured attempt costs vary, which is exactly what makes it a view rather than a population. Monotonicity of the first gives nothing about the second. ON THE NAMED RUN (gunbc#9840 head 85c4a307, required-witnesses-floor, second attempt, 3381 executed rows) the attention subset holds 53 identities across 21 modules, the largest groups being `test.claim.compiler_frontend_program_status_witness` (9), `v2.test.execution.emit_host_meet_join_equals_eval` (4), `v2.test.emit.rust_body_add_emit` (4) and `v2.test.emit.rust_binop_emit` (4). THE SUBSET IS A MANUAL DERIVATION AND NOT AN EXPOSED RUN PRODUCT, AND AN EARLIER REVISION OF THIS ROW OVERCLAIMED IT. The enumeration above was computed BY HAND by reading a run's uploaded `required_floor_claim_cost.tsv` and filtering on the attention constant. NO MODELED FIELD, FUNCTION OR REPORT PRODUCES IT: the constant lives only in this prose, `RungDrop` carries no numeric field to hold it, and nothing consumes it -- so saying the artifact 'reports the subset' asserted an executable relationship that does not exist. WHAT WOULD MAKE IT A PRODUCER, and it is a carrier gap rather than a missing script: the constant modeled as a declaration, and the per-claim cost artifact modeled as data a function can read, at which point the subset is a fold and this paragraph becomes its projection. Neither exists today, and a hand-run filter described as a run product is the specification-without-execution DESIGN section 5 names -- which is why this row now says which of the two it is. THE CONSTANT SITS ON THE STEEPEST PART OF THE COST CURVE and must not be read as a measured threshold: 12 rows reach 400, 16 reach 350, 43 reach 300, 50 reach 290 and 53 reach 280 -- seven rows arrive in a 10ms interval, and 1388 rows measure zero. RESTORATION TRIGGER, A CAPABILITY AND NOTHING SHORT OF IT: A CLAIM-OWNED COST BASIS WHOSE VALUE IS INVARIANT, OR BOUNDED BY CONSTRUCTION, ACROSS THE ADMITTED EXECUTION ENVELOPES. Three arms satisfy it: an adequately isolated envelope; a deterministic work measure such as evaluator steps; or a calibrated relative basis WHOSE TRACKING HAS ITSELF BEEN PROVEN over the relevant workload classes. It is deliberately wider than 'one in-run reference workload': the warm phases already failed to track claim inflation, and heterogeneous claims respond differently to cache, memory, frequency and co-tenant pressure, so a single reference workload is one candidate arm and not the capability. A SEPARATE CAPABILITY BOUND, RECORDED HERE AND EXPLICITLY NOT THIS ROW'S CAUSE: a shared artifact fill paid inside a claim's measured window before preemption bounds what any deadline mechanism can promise about attribution. PAYER TRANSFER IS REFUTED FOR THIS INCIDENT -- the red run's own `[floor-shared-fill]` ledger carries no `paid_by` line naming the module that tripped, the whole module shifted uniformly by 8 to 11 percent rather than one row taking a lump, and the rows that crossed sat mid-pack on the green attempt. It is a bound on the mechanism, not an explanation of these observations, and it is not this row's population producer. RAISING THE CEILING DOES NOT RETIRE THIS ROW AND IS NOT PROPOSED: 'the comparison does not qualify the claim' and 'the threshold is too low' are different claims, and only the first is recorded here. NOT PROPOSED EITHER: re-running an undecided row until it answers is retry-until-green -- fail-open wearing a fail-closed label -- admissible only as a counted, visible mitigation carrying this row's trigger as its dissolution condition. RECEIPT, 2026-09-02, AND THE MITIGATION THE SENTENCE ABOVE ADMITS CONDITIONALLY IS HEREBY MADE VISIBLE RATHER THAN LEFT IMPLICIT. Rerolling a refused required floor job has been in continuous informal use across this board today under a bounded rule -- at most one reroll per head per signature, and only where the run reported `failed=0` with the refusal carried entirely by this row's two arms. Bounded is better than retry-until-green, and it was still NOT the admitted arm, because nothing enumerated the instances and nothing carried this row's trigger as their dissolution condition. This paragraph is that enumeration. DISSOLUTION CONDITION: this row's own RESTORATION TRIGGER and nothing short of it -- a claim-owned cost basis whose value is invariant, or bounded by construction, across the admitted execution envelopes. When that lands, the reroll has no subject and this paragraph goes with it. INSTANCES, CITED BY RUN ID SO EACH IS REACHABLE AND FALSIFIABLE RATHER THAN TALLIED: gunbc#9984 run 33604337589 attempts 1 and 2 on head 9b00e24f592 (refuse then pass; `interrupted_before_verdict` 4 then 0, `completed_over_cost_requirement` 3 then 0, `planned=executed=3486` and `failed=0` on both); gunbc#10022 run 33615900632 attempts 1 and 2 on head c2c1db141a (refuse then pass, two undecided rows in `test.claim.self_host_compile_phase_live_gate_witness`); gunbc#9954 commit 53088562e30 (`interrupted_before_verdict=15`, `completed_over_cost_requirement=0`, `failed=0` -- the largest single observation, and purely the non-verdict arm); gunbc#10044 run 33618811753 attempts 1 and 2 on head 2d42cca4b94 by session eager-ferret-714's lane (refuse THEN REFUSE on one tree with different accounting -- `interrupted` 2 then 4, `over_cost` 0 then 2); and gunbc#10044 run 33619277245 attempts 1 and 2 on head 0e9b1518b7b (refuse then refuse; `interrupted` 5 then 2, `over_cost` 4 then 0, `planned=executed=3477` and `failed=0` on both); gunbc#10047 run 33622971872 attempt 2 on head 1aa6d8f41dc (attempt 1 refused at 502ms on `v2.test.emit.rust_binop_emit.rust_binop_producer_emit_sub_holds`, a module carrying four identities in this row's own attention subset -- so the roster PREDICTED the row that blocked that PR, which is a stronger receipt than a fresh observation); gunbc#9986 at f5fca17678f (`planned=executed=3503`, `failed=0`, `interrupted_before_verdict=2` in `test.claim.compiler_frontend_program_status_witness` and `test.claim.self_host_compile_phase_frontier_witness` -- NEITHER in the live-gate family, on a head that had ALREADY taken 2d76d9ccb33, which is what establishes the arm is not confined to a repairable family); and gunbc#10044 run 33628404336 attempts 1 and 2 on head 03780b8c76c, floor jobs 100219422472 and 100256793010 (REFUSE THEN REFUSE at ONE ROW EACH, `failed=0` and `planned=executed=3486` on both, `interrupted_cpu_deadline=1` -- but attempt 1's row was `v2.test.emit.produced_decl_two_target` and attempt 2's was `v2.test.execution.emit_host_module_equals_eval`, a DIFFERENT identity at the same count). THAT LAST PAIR IS SUGGESTIVE AND DOES NOT SETTLE IT ALONE, WHICH IS WORTH SAYING BECAUSE THE OVERSTATED VERSION WAS WRITTEN HERE FIRST: two draws showing DIFFERENT identities at n=1 per side are equally consistent with a FIXED set of marginal rows sitting so close to the deadline that ordering decides which one crosses. Identity change alone does not discriminate those two explanations. WHAT DISCRIMINATES IS THAT THE COUNT MOVES AS WELL AS THE MEMBERSHIP, across the instances above taken jointly: 4 then 0, 5 then 2, 1 then 1, 2 then 4, and 15. A fixed marginal set would have to explain a count ranging over 0, 1, 2, 4, 5 and 15 AND the membership changing; a population redrawn per attempt explains both, and near-threshold ordering explains only the second. So the redraw reading is CORROBORATED BY THE INSTANCES JOINTLY rather than established by any one pair -- and the load-bearing consequence survives either way, because on both readings no enumeration of the expensive claims can be the population, family-by-family cost repair lowers incidence without bounding the class, and a green reroll is not evidence the refused row was wrong. RE-DERIVE ANY OF THESE WITH `gh api repos/OWNER/REPO/actions/jobs/JOB/logs --allow-escape-sequences` AND WITH NOTHING ELSE. Measured on the first pair above: `gh run view --job --log` answers an ATTEMPT-1 job id with ATTEMPT 2's CONTENT -- banner timestamp and counters both attempt 2's -- so an auditor re-deriving a two-attempt specimen with it obtains IDENTICAL content on both sides, observes no disagreement, and reports these enumerated instances as fabricated. The instrument fails in the direction that discredits a true finding, and without the escape-sequences flag the same endpoint writes zero bytes instead. Anyone checking these numbers must be holding the right instrument before disagreeing with them. NO MODELED PRODUCER COUNTS THESE, AND THAT MISSING COUNTER IS THIS PARAGRAPH'S OWN GAP: `RungDrop` carries no field for a mitigation instance, nothing folds the run ids, and a hand-kept TALLY is deliberately absent here because this row has already had to retract one hand-derivation described as a run product. A count with no producer is stale at the next roll and re-derivable by nobody; a run id is reachable by anyone. Whoever wants the number counts the citations. WHAT THE INSTANCES ESTABLISH BEYOND THE MITIGATION ITSELF: the two arms vary INDEPENDENTLY and in both directions on fixed bytes, and a refusal can repeat while disagreeing with itself about which rows were undecided -- so a reroll is not a coin flip against a fixed population but a fresh draw of the population. ONE FINER OBSERVATION THAN THIS ROW PREVIOUSLY SUPPORTED, from the last instance: after the live-gate cost repairs in 2d76d9ccb33 (gunbc#10038), `test.claim.self_host_compile_phase_live_gate_witness` was ABSENT from attempt 1 and BACK in attempt 2 of ONE head. A cost repair lowering a family's incidence is the expected reading; that the family is intermittent WITHIN a single head's attempts is stronger, and it is the sharpest available statement that a cost repair moves incidence without touching the mechanism at the boundary. The conflation of a computed non-verdict with a refusal at the AGGREGATE boundary is a separate class and is filed as `gunbc.recurring_failure_mode` `non_verdict_disposition_surfaces_as_refusal`, which cites this row for the cost half rather than re-deriving it." } +data spark_role_scoped_retirement_production_root: RungDrop = RungDrop { identity: "spark_role_scoped_retirement_production_root" as NonEmptyStr, subject: "Spark serving role-scoped retirement evidence at the production plan root", declared: "2026-09-02", standing: Standing, authored: "**AN OPERATOR DECISION REMOVED A BEHAVIOUR'S ONLY SUBJECT, AND THIS ROW IS THAT DECLARATION (2026-09-02).** `gunbc.spark.cell_role` assigned srv6 to `SparkTrainingCell`, and the operator withdrew that dedication as premature -- 'i wouldn't dedicate a whole node for any task - just have it converge and serve whatever task we converge it to' -- so the production roster now holds ZERO training cells. Three claims in `test.claim.spark.spark_cell_role_retirement_witness_test` entered through `fleet_converge_plan_artifact`, the root the converge actuator itself walks, and each needed a production host holding that role to have a subject at all: `w_the_production_artifact_plans_four_retirements_for_the_training_cell`, `w_the_production_artifact_plans_no_rows_for_the_converged_serving_cell`, and `w_the_production_retirement_touches_no_baseline_address`. They are DELETED rather than left silently red, because a claim whose subject no longer exists is not a failing test, and leaving it to fail would have made an operator's decision look like a regression. **PREVIOUS RUNG: mechanically preventable** -- the training arm's four retirement rows and the serving arm's zero rows were both exercised through the production root, so a planner regression that pointed `spark_serving_full_membership_plan` back at the unscoped desired members went red there. **TEMPORARY RUNG: mitigatable** -- both arms are still exercised, but only at `spark_serving_role_scoped_desired_members_in` over an authored fixture roster (`w_the_planner_scopes_desired_state_by_role`), which is a real production function and is NOT the path the converge actuator calls; the same PR added `spark_cell_role_in` and that `_in` planner variant precisely so an arm's evidence stops depending on which machines are currently assigned what. **REASON:** operator decision, recorded with its basis at `gunbc.spark.cell_role` `spark_cell_role_assignment_basis`; role is converged desired state rather than a node dedication. **POPULATION, BOUNDED:** the training arm of Spark serving role scoping and the retirement rows it produces, AS REACHED THROUGH `fleet_converge_plan_artifact`. The serving arm, the no-role refusal, the reconcile, the freeze and the apply are unaffected and their production-root claims remain enrolled. **RESTORATION TRIGGER, NAMING THE CAPABILITY:** a roster-parameterized plan artifact -- the assignment roster threaded from `fleet_converge_plan_artifact` down to `spark_serving_role_scoped_desired_members_in` -- SUFFICIENT FOR a witness to drive the production root over an authored roster and read back the four retirement rows with no production host holding `SparkTrainingCell`. Half that capability exists today: both `_in` functions take the roster; what is missing is the threading through the generic artifact entry point. **RESTORING A TRAINING CELL TO THE PRODUCTION ROSTER DOES NOT RETIRE THIS DROP** -- that would re-create the coupling between an arm's evidence and the current assignment, which is the defect this row exists to record, and it is exactly the trigger-names-less-than-the-capability failure §4b(3) warns about." } data floor_cut_heal: RungDrop = RungDrop { identity: "floor_cut_heal" as NonEmptyStr, subject: "Heal job for generated artifacts", declared: "2026-09-01", standing: Standing, authored: "**HEAL IS GONE AND ITS AUTHORITY MODULE IS GONE WITH IT, AND THIS ROW DECLARES THAT RUNG (2026-09-01).** Split out of `floor_cut`, whose single trigger could not retire it. PREVIOUS RUNG: 2 (mechanically preventable) -- a required job regenerated drifted generated artifacts and pushed the repair onto the branch head, so the class `a committed generated artifact diverges from its authority` was caught and CORRECTED without an author. TEMPORARY RUNG: 1 (mitigatable) -- drift is still CAUGHT, by the `generated-artifact` required phase, but nothing repairs it, so every divergence is now a human round trip. REASON: the 2026-08-15 floor cut deleted the job with the workflow authority that carried it. BOUNDED POPULATION: one capability -- automatic repair of drifted generated artifacts on a branch head. MEASURED FROM THE TREE RATHER THAN FROM THE PARAGRAPH UNDER SUSPICION (2026-09-01): `gunbc.ci_heal_credential` survives in full and still carries `ci_heal_job_ref` and `ci_heal_workflow_ref` as DeclarationRefs to `gunbc.ci_workflow` `ci_heal_generated_artifacts_job` and `gunbc.ci_workflow` `ci_workflow` -- and `gunbc.ci_workflow` DOES NOT EXIST in this tree; the only module of that stem is `gunbc.ci_workflow_expressions`, and the decl name resolves nowhere. So heal's credential model is live and its job and workflow are deleted, which also means a typed citation to a deleted module is sitting unrefused; that second fact is recorded here as an observation and is NOT this row's subject. RESTORATION TRIGGER, A CAPABILITY: a required-run consumer that, on a branch head whose committed generated artifacts diverge from their authorities, WRITES the regenerated bytes back and pushes them under a credential the repository already models -- observed doing so on a real divergence, not merely emitted. WHAT DOES NOT RETIRE THIS ROW: restoring `gunbc.ci_workflow` or re-pointing `ci_heal_credential`'s dangling citations, which repairs the MODEL and heals nothing; nor a job that only reports drift, which is the phase we already have. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } data floor_cut_effect_gates: RungDrop = RungDrop { identity: "floor_cut_effect_gates" as NonEmptyStr, subject: "Six of the seven effect gates (one restored)", declared: "2026-09-01", standing: Standing, authored: "**SIX OF THE SEVEN EFFECT GATES ARE UNGUARDED AND THE SEVENTH IS BACK, AND THE FRACTION IS STATED BECAUSE SAYING `THE EFFECT GATES` WHERE ONE OF SEVEN IS LIVE IS THE OVERSTATEMENT THIS LEDGER KEEPS PAYING FOR (2026-09-01).** Split out of `floor_cut`. THE SEVEN, from that row's own loss clause: compile-clean, generated-artifact drift, emit-host, extdeps citation, extdeps placement, prose-row, cheap-claim pool. DISCHARGED, 1 of 7: generated-artifact drift, restored by gunbc#9415 as the required `generated-artifact` phase adjudicating every member of `committed_generated_artifacts` through `gunbc.generated_artifact_emit` `generated_artifact_body_for_path`. It is named here as DONE rather than deleted from the list, because a population that shrinks silently cannot be checked. OUTSTANDING, 6 of 7: compile-clean, emit-host, extdeps citation, extdeps placement, prose-row, cheap-claim pool. PREVIOUS RUNG: 2 (mechanically preventable) for each -- a required gate blocked the merge. TEMPORARY RUNG: 0 for the six; not `1`, because these are not mitigated failures but UNOBSERVED ones -- the class is outside the modeled guarantee at the merge boundary until its gate returns. REASON: the 2026-08-15 floor cut deleted the wrapper carrying all seven obligations. BOUNDED POPULATION: the six named gates, enumerated above; the roster is closed and is not `whatever the plan lists`. RESTORATION TRIGGER, PER GATE AND NOT FOR THE SET: this row retires only when EACH of the six has a required-run consumer that refuses a merge on its own violation, each with a discriminating RED executed on the real acceptance path. Six retirements, one row, and the row states its own remaining fraction whenever it is read. WHAT DOES NOT RETIRE THIS ROW: the `generated-artifact` phase being live, which is the one already discharged; a lens that computes any of the six without gating, which is the inert tier DESIGN section 6 names; or a gate landed with no authored RED, which is a wall nobody has seen fire. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } @@ -134,6 +135,7 @@ data rung_drop_roster: List = [ required_gate_bankruptcy, text_boundary_identity_wall, fabric_evidence_gating, + spark_role_scoped_retirement_production_root, builtin_signature_arity_pairing_fabricates, concat_binary_signature_exempt_from_arg_binding, namespace_admission_consumed_row_deletion, diff --git a/dag/gunbc/spark/cell_role.dag b/dag/gunbc/spark/cell_role.dag index b2992c3d525..d9b611b307d 100644 --- a/dag/gunbc/spark/cell_role.dag +++ b/dag/gunbc/spark/cell_role.dag @@ -23,10 +23,30 @@ import gunbc.fleet_intent_network { operator_host_srv5, operator_host_srv6 } // that is not assigned here is not a Spark cell, which the assignment lookup answers as Absent rather // than as a third role. // -// DYNAMIC ROLE SWITCHING IS DELIBERATELY NOT MODELLED. Nothing here represents a cell in transition, -// and that is scope rather than omission: SPARK-PAIR-0 excludes serve/train switching, so the only -// transition this project performs is the one-way retirement of serving from srv6, carried by the -// retirement plan and its readiness proof rather than by a role value that means "mid-flight". +// A ROLE IS CONVERGED DESIRED STATE, NOT A DEDICATION. +// +// CORRECTED 2026-09-02 BY OPERATOR DECISION, and the correction is to the FRAME rather than to one +// row. The predecessor note said dynamic role switching was deliberately not modelled and that the +// only transition this project performs is a ONE-WAY retirement of serving from srv6. The operator's +// instruction is the opposite of both halves: "i wouldn't dedicate a whole node for any task - just +// have it converge and serve whatever task we converge it to." Training remains a modelled +// capability -- gunbc.spark.training_ready still carries retirement, its readiness proof and its +// remedies -- but it stops being a NODE RESERVATION, and the reservation was the premature part. +// +// So a row here is desired state that convergence actuates, and editing one is the ordinary way a +// cell changes what it is for. What survives unchanged is everything that made the sum the right +// shape: a cell still holds exactly ONE role at a time, because the contention that motivated it is +// physical and did not go away -- two roles on one unified memory pool have no arbiter. The closed +// sum is what makes that a construction fact rather than a checked one, and there is still no +// `SparkDualRoleCell` and no absent arm. +// +// WHAT IS STILL NOT MODELLED, stated as a gap rather than as scope: a cell IN TRANSITION. Nothing +// here represents mid-flight, so a role edit is a discrete change of desired state and the +// convergence that follows it is what makes it real on the host. A bounded temporary-role +// authority -- a probe that borrows a cell and whose teardown restores the prior role -- is the +// next rung and does not exist yet. Until it does, a serving deployment that wants a training cell +// must change the assignment, not run beside it. + type SparkCellRole = SparkServingCell | SparkTrainingCell @@ -46,7 +66,7 @@ type SparkCellRoleAssignment { // The basis is that srv5 already carries the live serving occurrence. Assigning serving to the host // that already serves makes the serving half of this project a model upgrade on a converged host, // and confines the retirement -- the part with no existing vocabulary -- to one machine. -data spark_cell_role_assignment_basis: NonEmptyStr = "OPERATOR DECISION (SPARK-PAIR-0, 2026-08-29): srv5 serves, srv6 trains. The units are identical, so the assignment is a tie-break rather than a measurement. Basis: srv5 already holds the live serving occurrence, so serving stays where it converged and the retirement -- the operation this corpus had no vocabulary for -- is confined to srv6." as NonEmptyStr +data spark_cell_role_assignment_basis: NonEmptyStr = "OPERATOR DECISION (SPARK-PAIR-0, 2026-09-02): srv5 and srv6 both serve. This SUPERSEDES the 2026-08-29 decision that assigned srv6 to training; the operator withdrew it as premature -- 'i wouldn't dedicate a whole node for any task - just have it converge and serve whatever task we converge it to' -- and moved training to its own lane. The units are identical, so neither assignment was ever a measurement. Consequence in gunbc.spark.serving_converge_plan: srv6 now receives full serving desired members rather than the baseline-only members a training cell receives." as NonEmptyStr data srv5_cell_role: SparkCellRoleAssignment = SparkCellRoleAssignment { host: operator_host_srv5, @@ -55,7 +75,7 @@ data srv5_cell_role: SparkCellRoleAssignment = SparkCellRoleAssignment { data srv6_cell_role: SparkCellRoleAssignment = SparkCellRoleAssignment { host: operator_host_srv6, - role: SparkTrainingCell, + role: SparkServingCell, } data spark_cell_role_assignments: List = [ @@ -103,8 +123,19 @@ type SparkCellRoleLookup | SparkCellRoleUnique { role: SparkCellRole } | SparkCellRoleAmbiguous { assignments: List } -fn spark_cell_role_of(host: HostIdentity) -> SparkCellRoleLookup { - let matched = filter(spark_cell_role_assignments, a => host_identity_eq(a: a.host, b: host)) +// THE LOOKUP IS OVER A ROSTER, AND THE PRODUCTION ROSTER IS ONE APPLICATION OF IT. +// +// Split out 2026-09-02 for a reason the roster change exposed: every claim about role SCOPING read +// the production assignments, so the evidence for the training arm existed only while a production +// host happened to hold that role. The operator withdrawing srv6's dedication would then have +// silently retired a behaviour's only witness -- the arm still exists and still decides desired +// state, and nothing would have exercised it. A capability's evidence must not depend on which +// machines are currently assigned what. +fn spark_cell_role_in( + assignments: List, + host: HostIdentity, +) -> SparkCellRoleLookup { + let matched = filter(assignments, a => host_identity_eq(a: a.host, b: host)) if length(matched) > 1 { SparkCellRoleAmbiguous { assignments: matched } } else { @@ -112,9 +143,25 @@ fn spark_cell_role_of(host: HostIdentity) -> SparkCellRoleLookup { } } -fn spark_hosts_with_role(role: SparkCellRole) -> List { - flat_map(spark_cell_role_assignments, a => - match spark_cell_role_of(host: a.host) { +fn spark_cell_role_of(host: HostIdentity) -> SparkCellRoleLookup { + spark_cell_role_in(assignments: spark_cell_role_assignments, host: host) +} + +// THE ROSTER-PARAMETERISED FORM, AND IT IS THE SAME ARGUMENT ONE LEVEL UP. +// +// `spark_cell_role_in` exists because a capability's evidence must not depend on which machines are +// currently assigned what. That argument does not stop at a single host's lookup: every claim about +// a ROLE POPULATION -- how many cells hold a role, whether two role rosters partition a scope -- +// had the same dependency, and the operator withdrawing srv6's training dedication took the only +// training cell with it. Four claims in `v2.test.claim.spark_observation_scope` went red on that +// change alone, having asserted `length(training) == 1` against the production roster. The +// behaviour they describe did not change; the machines did. +fn spark_hosts_with_role_in( + assignments: List, + role: SparkCellRole, +) -> List { + flat_map(assignments, a => + match spark_cell_role_in(assignments: assignments, host: a.host) { SparkCellRoleUnique { role: r } => if spark_cell_role_eq(a: r, b: role) { [a.host] } else { [] } SparkCellRoleAmbiguous { assignments: _ } => [] @@ -122,6 +169,10 @@ fn spark_hosts_with_role(role: SparkCellRole) -> List { }) } +fn spark_hosts_with_role(role: SparkCellRole) -> List { + spark_hosts_with_role_in(assignments: spark_cell_role_assignments, role: role) +} + fn spark_serving_cell_hosts() -> List { spark_hosts_with_role(role: SparkServingCell) } diff --git a/dag/gunbc/spark/fabric_link_desired.dag b/dag/gunbc/spark/fabric_link_desired.dag new file mode 100644 index 00000000000..ce69ce86633 --- /dev/null +++ b/dag/gunbc/spark/fabric_link_desired.dag @@ -0,0 +1,186 @@ +module gunbc.spark.fabric_link_desired + +import std.types { String, Bool, List, Int, NonEmptyStr } +import std.measure { ByteSize, byte_size, byte_size_count } +import product.placement_supply { HostIdentity, host_identity_eq } +import extdeps.network.ipv4 { + Ipv4Address, ipv4_address, render_ipv4_address, render_ipv4_cidr, + PrefixLength, ipv4_same_network, ipv4_address_eq, +} +import gunbc.fleet_intent_network { operator_host_srv7, operator_host_srv8 } + +// THE DESIRED STATE OF THE SPARK FABRIC, AND WHY IT IS DESIRED STATE RATHER THAN A RUNBOOK. +// +// This module exists because of a measured loss, not a preference. The 200 Gb/s RoCE addressing on +// srv5/srv6 was applied at RUNTIME -- `ip` and `nmcli` calls made by hand -- verified working at +// MTU 9000 with a clean 8972-byte jumbo ping, reported as configured, and then destroyed entirely by +// one power cycle. Nothing was on disk to survive it. +// +// The mechanism is specific and is the whole reason the file path below is the subject. These hosts +// run netplan with `renderer: NetworkManager`, and NetworkManager had the fabric NICs as "connected +// (externally)" -- observed, not managed. An `nmcli` write is intercepted by the netplan-NM +// integration and lands a keyfile in /run/NetworkManager/system-connections/, which is TMPFS. The +// durable artifact is the GENERATED /etc/netplan/90-NM-.yaml, and only that. So a convergence +// that actuates `nmcli` converges a host into a state that does not survive its next boot, while +// reporting success -- the runtime-observation-read-as-durable-state failure, at the layer that +// makes every serving fact above it unreachable after a reboot. +// +// A RAIL IS THE SUBJECT, NOT AN INTERFACE, and the rail's identity is the interface NAME -- which is +// the SAME on both hosts. This is the NVIDIA connect-two-sparks convention and it is load-bearing +// rather than cosmetic: NCCL selects a rail by matching interface to subnet, so the pairing that +// works for `ping` is not the pairing that works for collective traffic. +// +// This module first shipped the opposite rule, on a peer session's report that the names were +// CROSSED between hosts, and both of us then read it back off the durable files and found they are +// not: enp1s0f0np0 carries 192.168.100.x on both, enP2p1s0f0np0 carries 192.168.101.x on both. The +// crossed configuration had been applied by hand, passed a jumbo ping, and was wrong anyway -- which +// is exactly why the same-name rule is a CONSTRUCTOR condition here and not a comment. A rail whose +// two ends name different interfaces cannot be built. +// +// The two rails are two RoCE devices -- rocep1s0f0 and roceP2p1s0f0, both reported Up by +// ibdev2netdev on both hosts, with their f1 siblings Down. WHAT IS NOT ESTABLISHED, and is recorded +// here rather than assumed either way: whether those are two physical cables or two logical views of +// one QSFP port. A jumbo ping on each rail passes in both cases, so the reachability evidence cannot +// distinguish them. It does not affect addressing, which is what this module owns; it does bound any +// future claim about aggregate fabric bandwidth, and such a claim needs its own instrument. +type FabricEndpoint sole_constructor { + host: HostIdentity + interface: NonEmptyStr + address: Ipv4Address + prefix: PrefixLength + mtu: ByteSize +} + +// A RAIL THAT COULD NOT CARRY COLLECTIVE TRAFFIC HAS NO CONSTRUCTOR. Five conditions decide it, and +// every one of them was a real way to get this wrong by hand on these two hosts: +// +// - the endpoints must be on DIFFERENT HOSTS. A rail from a host to itself is a typo that reads as +// a configured fabric. +// - they must name the SAME INTERFACE. Crossing them survives a ping and breaks rail selection, +// which is the failure that is expensive precisely because it tests green. +// - they must share a NETWORK at the declared prefix. Two ends on unrelated subnets are up, +// carrier-present and unreachable, which gets diagnosed as a cabling fault. +// - they must be DIFFERENT ADDRESSES. Identical ends is the copy-paste error. +// - they must agree on MTU. A 9000/1500 mismatch does not fail until a jumbo frame meets the small +// end and is silently dropped -- no error anywhere, just collectives that stall. +// +// The prefix must also be one `ipv4_same_network` can answer for; an unanswerable prefix refuses +// rather than being assumed to match, because "I could not check" is not "it is fine". +type FabricLink sole_constructor { + name: NonEmptyStr + endpoint_a: FabricEndpoint + endpoint_b: FabricEndpoint +} + +fn fabric_link( + name: NonEmptyStr, + endpoint_a: FabricEndpoint, + endpoint_b: FabricEndpoint, +) -> FabricLink? { + if host_identity_eq(a: endpoint_a.host, b: endpoint_b.host) { + none + } else if (endpoint_a.interface as String) != (endpoint_b.interface as String) { + none + } else if ipv4_address_eq(a: endpoint_a.address, b: endpoint_b.address) { + none + } else if endpoint_a.prefix != endpoint_b.prefix { + none + } else if byte_size_count(b: endpoint_a.mtu) != byte_size_count(b: endpoint_b.mtu) { + none + } else { + match ipv4_same_network( + a: endpoint_a.address, b: endpoint_b.address, prefix: endpoint_a.prefix) { + Absent => none + Present { value: shared } => + if shared { + Present { value: FabricLink { + name: name, endpoint_a: endpoint_a, endpoint_b: endpoint_b } } + } else { + none + } + } + } +} + +fn fabric_endpoint( + host: HostIdentity, + interface: NonEmptyStr, + address: Ipv4Address, + prefix: PrefixLength, + mtu: ByteSize, +) -> FabricEndpoint { + FabricEndpoint { + host: host, interface: interface, address: address, prefix: prefix, mtu: mtu } +} + +// The endpoint this host owns on this link, or Absent when the link does not touch it. A host that +// is not an end of the link gets no configuration from it -- never a defaulted one. +fn fabric_endpoint_on(link: FabricLink, host: HostIdentity) -> FabricEndpoint? { + if host_identity_eq(a: link.endpoint_a.host, b: host) { + Present { value: link.endpoint_a } + } else if host_identity_eq(a: link.endpoint_b.host, b: host) { + Present { value: link.endpoint_b } + } else { + none + } +} + +// ================= THE MEASURED FABRIC ================= +// +// Read back from the durable /etc/netplan/90-NM-*.yaml on BOTH hosts on 2026-09-02 and cross-checked +// against `ip -br -4 addr` and `ibdev2netdev` on each -- not authored from intent, and not taken on +// report. The first version of these rows was authored from a peer session's summary and had the +// subnets crossed and the prefix wrong; re-derive from the files rather than trusting this block. +// +// The addressing follows the NVIDIA connect-two-sparks playbook: rail0 on 192.168.100.0/24, rail1 on +// 192.168.101.0/24, same interface name at both ends of each rail, MTU 9000, IPv6 disabled. The NM +// profile names on the hosts are cx7-rail0 and cx7-rail1. +data fabric_prefix: PrefixLength = 24 +// AN MTU IS A BYTE COUNT, so it carries std.measure's ByteSize rather than a bare Int. The scale is +// exactly what a 9000-vs-1500 mismatch turns on, and a bare number leaves it to the reader -- the +// same defect PrefixLength above exists to close for the network half of this record. +data fabric_mtu_bytes: ByteSize = byte_size(count: 9000) + +data fabric_rail0: FabricLink? = fabric_link( + name: "cx7-rail0" as NonEmptyStr, + endpoint_a: fabric_endpoint( + host: operator_host_srv7, + interface: "enp1s0f0np0" as NonEmptyStr, + address: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 10), + prefix: fabric_prefix, mtu: fabric_mtu_bytes), + endpoint_b: fabric_endpoint( + host: operator_host_srv8, + interface: "enp1s0f0np0" as NonEmptyStr, + address: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 11), + prefix: fabric_prefix, mtu: fabric_mtu_bytes)) + +data fabric_rail1: FabricLink? = fabric_link( + name: "cx7-rail1" as NonEmptyStr, + endpoint_a: fabric_endpoint( + host: operator_host_srv7, + interface: "enP2p1s0f0np0" as NonEmptyStr, + address: ipv4_address(octet1: 192, octet2: 168, octet3: 101, octet4: 10), + prefix: fabric_prefix, mtu: fabric_mtu_bytes), + endpoint_b: fabric_endpoint( + host: operator_host_srv8, + interface: "enP2p1s0f0np0" as NonEmptyStr, + address: ipv4_address(octet1: 192, octet2: 168, octet3: 101, octet4: 11), + prefix: fabric_prefix, mtu: fabric_mtu_bytes)) + +// The roster is the PRESENT links only. A link whose constructor refused is not a link with a +// problem to be reported later -- it never existed, so nothing downstream can plan from it. +fn spark_fabric_links() -> List { + flat_map([fabric_rail0, fabric_rail1], l => + match l { + Present { value: v } => [v] + Absent => [] + }) +} + +fn spark_fabric_endpoints_on(host: HostIdentity) -> List { + flat_map(spark_fabric_links(), l => + match fabric_endpoint_on(link: l, host: host) { + Present { value: e } => [e] + Absent => [] + }) +} diff --git a/dag/gunbc/spark/serving_converge_plan.dag b/dag/gunbc/spark/serving_converge_plan.dag index 685531cc12c..43cf9d149c7 100644 --- a/dag/gunbc/spark/serving_converge_plan.dag +++ b/dag/gunbc/spark/serving_converge_plan.dag @@ -75,6 +75,7 @@ import gunbc.spark.serving_member_realization { } import gunbc.spark.cell_role { SparkCellRole, SparkServingCell, SparkTrainingCell, spark_cell_role_of, + SparkCellRoleAssignment, spark_cell_role_in, spark_cell_role_assignments, SparkCellRoleLookup, SparkCellRoleAbsent, SparkCellRoleUnique, SparkCellRoleAmbiguous, } import gunbc.spark.serving_realization { @@ -641,7 +642,20 @@ fn spark_serving_role_scoped_desired_members( occurrence: SparkServingOccurrence, serving_release: SparkServingRelease, ) -> SparkServingRoleScopedDesired { - match spark_cell_role_of(host: occurrence.host) { + spark_serving_role_scoped_desired_members_in( + assignments: spark_cell_role_assignments, + occurrence: occurrence, + serving_release: serving_release) +} + +// The roster is a parameter so the training arm below stays exercisable by evidence regardless of +// which hosts currently hold which role -- see gunbc.spark.cell_role spark_cell_role_in. +fn spark_serving_role_scoped_desired_members_in( + assignments: List, + occurrence: SparkServingOccurrence, + serving_release: SparkServingRelease, +) -> SparkServingRoleScopedDesired { + match spark_cell_role_in(assignments: assignments, host: occurrence.host) { SparkCellRoleAbsent => SparkServingRoleScopedDesiredRefused { cause: "spark serving plan refused: the host holds no Spark cell role, and a machine nobody assigned must not receive serving desired state by default", diff --git a/dag/test/claim/spark/spark_cell_role_retirement_witness_test.dag b/dag/test/claim/spark/spark_cell_role_retirement_witness_test.dag index b210905850c..43975876b46 100644 --- a/dag/test/claim/spark/spark_cell_role_retirement_witness_test.dag +++ b/dag/test/claim/spark/spark_cell_role_retirement_witness_test.dag @@ -15,6 +15,7 @@ import gunbc.spark.cell_role { spark_cell_role_eq, spark_serving_cell_hosts, spark_training_cell_hosts, + SparkCellRoleAssignment, } import gunbc.spark.serving_desired { SparkServingDesiredAdmitted, @@ -35,6 +36,7 @@ import gunbc.spark.serving_converge_plan { SparkServingRoleScopedDesiredReady, SparkServingRoleScopedDesiredRefused, spark_serving_role_scoped_desired_members, + spark_serving_role_scoped_desired_members_in, spark_serving_axis_for_observation, fleet_converge_spark_serving_action_at, } @@ -159,18 +161,21 @@ fn w_retirement_effects(address: SparkServingResourceAddress) -> List Bool { - length(spark_serving_cell_hosts()) == 1 - && length(spark_training_cell_hosts()) == 1 - && any(spark_serving_cell_hosts(), h => h as String == operator_host_srv5 as String) - && any(spark_training_cell_hosts(), h => h as String == operator_host_srv6 as String) - && !any(spark_serving_cell_hosts(), h => h as String == operator_host_srv6 as String) - && !any(spark_training_cell_hosts(), h => h as String == operator_host_srv5 as String) + !any(spark_serving_cell_hosts(), h => + any(spark_training_cell_hosts(), t => h as String == t as String)) } // A HOST NOBODY ASSIGNED HAS NO ROLE, WHICH IS NOT A ROLE. @@ -185,29 +190,27 @@ test fn w_unassigned_host_has_no_spark_role() -> Bool { } } -// SERVING DESIRED STATE IS SRV5 ALONE, AND IT GOT THERE BY PROJECTION. +// SERVING DESIRED STATE IS EXACTLY THE SERVING CELLS, IN BOTH DIRECTIONS. // -// This is the claim that goes red the moment srv6's role is reverted to SparkServingCell -- which is -// the point. Nothing here names srv6 as excluded; the roster simply is what the role authority says, -// so a role change moves it without this file being touched. +// The projection claim, stated as the bijection it is rather than as the roster it currently +// produces. Every serving cell reaches desired state and nothing else does, so a role change moves +// the roster without this file being touched -- which is what the predecessor claimed to do and did +// not, because it named srv5 and srv6 directly. test fn w_serving_desired_hosts_are_the_serving_cells() -> Bool { - length(spark_serving_desired_hosts) == 1 - && any(spark_serving_desired_hosts, h => h as String == operator_host_srv5 as String) - && !any(spark_serving_desired_hosts, h => h as String == operator_host_srv6 as String) + all(spark_serving_cell_hosts(), c => + any(spark_serving_desired_hosts, h => h as String == c as String)) + && all(spark_serving_desired_hosts, h => + any(spark_serving_cell_hosts(), c => c as String == h as String)) } -// THE OFFER ROSTER EXCLUDES THE SERVING CELL, ASSERTED OVER THE ROSTER ITSELF. +// THE OFFER ROSTER EXCLUDES EVERY SERVING CELL, AND AN UNASSIGNED HOST IS IN NEITHER. // -// This asked a `spark_host_offerable_for_training` predicate, which existed only to be asked by this -// claim -- a claim whose whole subject is a function nothing else calls measures its own fixture. The -// subject that matters is the roster P3's supply module will consume, so the claim reads that: srv5 -// is absent from it because it serves, srv6 is present because it trains, and an unassigned host is -// in neither roster because it is not a Spark cell. +// The subject is the roster the training-supply module will consume. A serving cell must never +// appear in it -- that is the contention this role authority exists to prevent -- and a machine +// nobody assigned is in neither roster because it is not a Spark cell. test fn w_serving_cell_is_not_offerable_to_the_training_fabric() -> Bool { let trainable = spark_training_cell_hosts() - length(trainable) == 1 - && any(trainable, h => h as String == operator_host_srv6 as String) - && !any(trainable, h => h as String == operator_host_srv5 as String) + !any(trainable, t => any(spark_serving_cell_hosts(), c => c as String == t as String)) && !any(trainable, h => h as String == "srv1") && !any(spark_serving_cell_hosts(), h => h as String == "srv1") } @@ -498,8 +501,24 @@ fn w_occurrence(host: HostIdentity) -> SparkServingOccurrence { } } +// THE ROSTER IS A FIXTURE, NOT THE PRODUCTION ASSIGNMENT. +// +// These claims are about the role-SCOPING arms, and an arm's evidence must not depend on which +// machines are currently assigned what. Reading the production roster is exactly how the training +// arm nearly lost its only witness when the operator withdrew srv6's dedication on 2026-09-02: the +// arm still decides desired state and nothing would have exercised it. So the roster below is +// authored here and names two hosts that hold one role each. +data w_serving_cell_host: HostIdentity = "w-serving-cell" as HostIdentity +data w_training_cell_host: HostIdentity = "w-training-cell" as HostIdentity + +data w_fixture_roster: List = [ + SparkCellRoleAssignment { host: w_serving_cell_host, role: SparkServingCell }, + SparkCellRoleAssignment { host: w_training_cell_host, role: SparkTrainingCell }, +] + fn w_role_scoped_count(host: HostIdentity) -> Int { - match spark_serving_role_scoped_desired_members( + match spark_serving_role_scoped_desired_members_in( + assignments: w_fixture_roster, occurrence: w_occurrence(host: host), serving_release: w_release(), ) { @@ -512,10 +531,24 @@ fn w_role_scoped_count(host: HostIdentity) -> Int { // // Seven for the serving cell, three for the training cell, and the difference is the four service // members whose removal the teardown schedule orders. Both counts are asserted because a planner that -// returned baseline for EVERY host would satisfy a claim that only checked srv6. +// returned baseline for EVERY host would satisfy a claim that only checked the training cell. test fn w_the_planner_scopes_desired_state_by_role() -> Bool { - w_role_scoped_count(host: operator_host_srv5) == 7 - && w_role_scoped_count(host: operator_host_srv6) == 3 + w_role_scoped_count(host: w_serving_cell_host) == 7 + && w_role_scoped_count(host: w_training_cell_host) == 3 +} + +// AND THE PRODUCTION ROSTER AGREES WITH THE ARM IT SELECTS. Without this the fixture above could +// drift from what production actually asks: every production serving cell must reach the seven-member +// desired state through the real entry point. +test fn w_the_production_roster_reaches_the_serving_arm() -> Bool { + all(spark_serving_cell_hosts(), h => + match spark_serving_role_scoped_desired_members( + occurrence: w_occurrence(host: h), + serving_release: w_release(), + ) { + SparkServingRoleScopedDesiredReady { members: ms } => length(ms) == 7 + SparkServingRoleScopedDesiredRefused { cause: _ } => false + }) } // A HOST NOBODY ASSIGNED REFUSES RATHER THAN DEFAULTING TO SERVING. This planner is reachable with @@ -577,34 +610,18 @@ fn w_row_is_retirement(row: FleetConvergeSparkServingTypedAction) -> Bool { }) } -// A FULLY SERVING TRAINING CELL PLANS FOUR RETIREMENTS THROUGH THE PRODUCTION ROOT. +// ── THREE PRODUCTION-ROOT RETIREMENT CLAIMS ARE GONE, UNDER A DECLARED §4b(3) DROP ────────────── // -// The observation handed in is a host serving perfectly: runtime materialized, model held, unit -// present and enabled and RUNNING, linger on. Under the pre-role planner this input produced zero -// rows -- it is exactly the desired seven-member serving state -- so this claim is red on the old -// production path for the right reason, rather than red because the fixture was rebuilt. -test fn w_the_production_artifact_plans_four_retirements_for_the_training_cell() -> Bool { - let rows = w_artifact_rows(host: operator_host_srv6) - length(rows) == 4 && all(rows, r => w_row_is_retirement(row: r)) -} - -// AND THE SERVING CELL IN THE SAME STATE PLANS NOTHING. Without this, "four rows" could be true of a -// planner that retires every host it is handed. -test fn w_the_production_artifact_plans_no_rows_for_the_converged_serving_cell() -> Bool { - length(w_artifact_rows(host: operator_host_srv5)) == 0 -} - -// THE RETAINED CACHE IS ABSENT FROM THE PRODUCTION ROWS, not merely from the fixture reconcile. -test fn w_the_production_retirement_touches_no_baseline_address() -> Bool { - let rows = w_artifact_rows(host: operator_host_srv6) - length(rows) == 4 - && !any(rows, r => string_contains( - fleet_converge_spark_serving_action_at(action: r.action), - spark_serving_resource_address_wire(address: SparkServingRuntimeRootAddress))) - && !any(rows, r => string_contains( - fleet_converge_spark_serving_action_at(action: r.action), - spark_serving_resource_address_wire(address: SparkServingLingerAddress))) -} +// w_the_production_artifact_plans_four_retirements_for_the_training_cell, +// w_the_production_artifact_plans_no_rows_for_the_converged_serving_cell and +// w_the_production_retirement_touches_no_baseline_address each needed a PRODUCTION host holding +// SparkTrainingCell to have a subject, and after the operator's 2026-09-02 withdrawal of srv6's +// training dedication the roster holds none. +// +// The drop is rostered in full -- previous rung, temporary rung, reason, bounded population and +// restoration trigger -- at gunbc.rung_drop `spark_role_scoped_retirement_production_root`, which is +// where §4b says declared drops live so they stay countable and prioritizable. It is named here and +// not restated, because a second copy of a declaration is a second authority for it. // A HOST WITH NO ROLE REFUSES AT THE PRODUCTION ROOT. // diff --git a/dag/test/claim/spark/spark_fabric_link_witness_test.dag b/dag/test/claim/spark/spark_fabric_link_witness_test.dag new file mode 100644 index 00000000000..d570d11cc7d --- /dev/null +++ b/dag/test/claim/spark/spark_fabric_link_witness_test.dag @@ -0,0 +1,146 @@ +module test.claim.spark.spark_fabric_link_witness_test + +import std.types { String, Bool, List, Int, NonEmptyStr } +import std.measure { ByteSize, byte_size } +import product.placement_supply { HostIdentity } +import extdeps.network.ipv4 { + Ipv4Address, ipv4_address, render_ipv4_address, render_ipv4_cidr, + PrefixLength, ipv4_same_network, ipv4_address_eq, +} +import gunbc.fleet_intent_network { operator_host_srv7, operator_host_srv8 } +import gunbc.spark.fabric_link_desired { + FabricEndpoint, FabricLink, fabric_endpoint, fabric_link, fabric_endpoint_on, + spark_fabric_links, spark_fabric_endpoints_on, fabric_prefix, fabric_mtu_bytes, +} + +data w_mtu: ByteSize = byte_size(count: 9000) + +fn w_end(host: HostIdentity, iface: NonEmptyStr, o3: Int, o4: Int) -> FabricEndpoint { + fabric_endpoint( + host: host, interface: iface, + address: ipv4_address(octet1: 192, octet2: 168, octet3: o3, octet4: o4), + prefix: 24, mtu: w_mtu) +} + +fn w_built(a: FabricEndpoint, b: FabricEndpoint) -> Bool { + match fabric_link(name: "w-link" as NonEmptyStr, endpoint_a: a, endpoint_b: b) { + Present { value: _ } => true + Absent => false + } +} + +// THE POSITIVE CONTROL. A well-formed rail -- two hosts, one interface name, one subnet. +test fn w_a_wellformed_rail_constructs() -> Bool { + w_built( + a: w_end(host: operator_host_srv7, iface: "ifa" as NonEmptyStr, o3: 100, o4: 10), + b: w_end(host: operator_host_srv8, iface: "ifa" as NonEmptyStr, o3: 100, o4: 11)) +} + +// AND THE FIVE WAYS TO GET IT WRONG BY HAND, each of which produced a plausible-looking +// configuration rather than an error when this was done with `ip` and `nmcli` on these two hosts. +// +// The CROSSED-INTERFACE arm is the one that matters most and the one this repository actually got +// wrong: the fabric was first configured with enP2p1s0f0np0 on one host paired to enp1s0f0np0 on the +// other. It passed a jumbo ping. It is still wrong, because NCCL selects a rail by matching +// interface to subnet -- so this is a failure that TESTS GREEN, which is why it is a constructor +// condition rather than a diagnostic. +test fn w_a_rail_that_could_not_carry_collective_traffic_has_no_constructor() -> Bool { + !w_built( + a: w_end(host: operator_host_srv7, iface: "ifa" as NonEmptyStr, o3: 100, o4: 10), + b: w_end(host: operator_host_srv7, iface: "ifa" as NonEmptyStr, o3: 100, o4: 11)) + && !w_built( + a: w_end(host: operator_host_srv7, iface: "ifa" as NonEmptyStr, o3: 100, o4: 10), + b: w_end(host: operator_host_srv8, iface: "ifb" as NonEmptyStr, o3: 100, o4: 11)) + && !w_built( + a: w_end(host: operator_host_srv7, iface: "ifa" as NonEmptyStr, o3: 100, o4: 10), + b: w_end(host: operator_host_srv8, iface: "ifa" as NonEmptyStr, o3: 101, o4: 11)) + && !w_built( + a: w_end(host: operator_host_srv7, iface: "ifa" as NonEmptyStr, o3: 100, o4: 10), + b: w_end(host: operator_host_srv8, iface: "ifa" as NonEmptyStr, o3: 100, o4: 10)) + && !w_built( + a: w_end(host: operator_host_srv7, iface: "ifa" as NonEmptyStr, o3: 100, o4: 10), + b: fabric_endpoint( + host: operator_host_srv8, interface: "ifa" as NonEmptyStr, + address: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 11), + prefix: 24, mtu: byte_size(count: 1500))) +} + +// THE SUBNET BOUNDARY IS WHERE ADJACENCY STOPS. The two rails are 192.168.100.0/24 and +// 192.168.101.0/24 -- one octet apart and easy to conflate by eye, and on DIFFERENT networks. This +// is the discriminating case for the octet comparison rather than for the type. +test fn w_the_two_rails_are_not_one_network() -> Bool { + match ipv4_same_network( + a: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 10), + b: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 11), prefix: 24) { + Absent => false + Present { value: same_rail } => + same_rail && match ipv4_same_network( + a: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 10), + b: ipv4_address(octet1: 192, octet2: 168, octet3: 101, octet4: 10), prefix: 24) { + Absent => false + Present { value: cross_rail } => !cross_rail + } + } +} + +// AN UNANSWERABLE PREFIX REFUSES RATHER THAN ASSUMING A MATCH. "I could not check" is not "it is +// fine", and a link built on an unchecked prefix is the absorbing fallback in its network form. +test fn w_a_prefix_the_comparison_cannot_answer_refuses() -> Bool { + match ipv4_same_network( + a: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 10), + b: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 11), prefix: 27) { + Absent => true + Present { value: _ } => false + } +} + +// THE SHIPPED ROWS CARRY ONE INTERFACE NAME PER RAIL, ASSERTED OVER THE ROSTER. +// +// This claim replaces one that asserted the opposite. It was written from a peer session's report +// that the interface names were CROSSED between the hosts, and reading the durable /etc/netplan on +// both machines showed they are not -- the crossed state existed, had been applied by hand, and was +// a defect rather than the convention. The witness that encoded it would have locked the defect in. +// Two rails, each naming one interface at both ends, and the two rails naming different ones. +test fn w_each_rail_names_one_interface_at_both_ends() -> Bool { + length(spark_fabric_links()) == 2 + && all(spark_fabric_links(), l => + (l.endpoint_a.interface as String) == (l.endpoint_b.interface as String)) + && !any(spark_fabric_links(), x => + any(spark_fabric_links(), y => + (x.name as String) != (y.name as String) + && (x.endpoint_a.interface as String) == (y.endpoint_a.interface as String))) +} + +// AND EACH HOST OWNS ONE ENDPOINT ON EACH LINK -- two apiece, on different interfaces. A host that +// is not an end of a link gets nothing from it rather than a default. +test fn w_each_fabric_host_owns_one_endpoint_per_link() -> Bool { + length(spark_fabric_endpoints_on(host: operator_host_srv7)) == 2 + && length(spark_fabric_endpoints_on(host: operator_host_srv8)) == 2 + && length(spark_fabric_endpoints_on(host: "srv1" as HostIdentity)) == 0 + && all(spark_fabric_links(), l => + match fabric_endpoint_on(link: l, host: "srv1" as HostIdentity) { + Present { value: _ } => false + Absent => true + }) +} + +// THE CIDR RENDERING IS WHAT /etc/netplan CARRIES, so it is asserted against the exact spelling read +// back off the durable file on spark-c2b1 rather than against a re-derivation of itself. +test fn w_the_cidr_rendering_matches_the_durable_netplan_spelling() -> Bool { + (render_ipv4_cidr( + addr: ipv4_address(octet1: 192, octet2: 168, octet3: 100, octet4: 10), + prefix: 24) as String) == "192.168.100.10/24" + && (render_ipv4_cidr( + addr: ipv4_address(octet1: 192, octet2: 168, octet3: 101, octet4: 11), + prefix: 24) as String) == "192.168.101.11/24" +} + +test fn w_all_spark_fabric_claims_hold() -> Bool { + w_a_wellformed_rail_constructs() + && w_a_rail_that_could_not_carry_collective_traffic_has_no_constructor() + && w_the_two_rails_are_not_one_network() + && w_a_prefix_the_comparison_cannot_answer_refuses() + && w_each_rail_names_one_interface_at_both_ends() + && w_each_fabric_host_owns_one_endpoint_per_link() + && w_the_cidr_rendering_matches_the_durable_netplan_spelling() +} diff --git a/docs/design-ledgers.md b/docs/design-ledgers.md index 3d1d8a5e139..4d4dc27f593 100644 --- a/docs/design-ledgers.md +++ b/docs/design-ledgers.md @@ -174,6 +174,10 @@ CORRECTION NOTICE, recorded because the wrong version travelled: an earlier revi **THE FABRIC-CI EVIDENCE LANE STOPS BLOCKING MERGES AND KEEPS EXECUTING (2026-08-31).** #9704 added `fabric-evidence` as a fourth job and, in the same change, made it a `needs` of the aggregating `witnesses` job that the `passing CI` ruleset names as this repository's one required context. PREVIOUS RUNG: mechanically preventable — a defect in the FCI-EVIDENCE-0 run-boundary contract was exposed by an enrolled calibration and blocked the merge. TEMPORARY RUNG: mitigatable — the same calibration still runs on every push and pull request, still refuses loudly, and its log is still the record; what is gone is the block, so a red is now a signal a human must read rather than a wall. REASON, and it is wall clock rather than doubt about the evidence: the required context's wall is the MAX over its three lanes, and on run 33350499023 that max was `fabric-evidence` at 27 minutes against 20 for the floor lane and 10.5 for the build lane, having moved the required wall from ~13 minutes to ~28-40 within a day of #9704 landing. 1469 of those 1620 seconds are the calibration step, and its own logs put all ~18 of the plan's `gunbc run` host processes at 80-90 seconds each. That cost is not the evidence: the instrument's import closure is six modules, and per `cli_run.entry_resolve` an `--entry` run is scoped in what it EMITS but WHOLE-TREE in what it PARSES, so each process re-parses and re-censuses the entire 4414-module corpus to evaluate a handful of rows. The lane is paying eighteen whole-corpus censuses (DESIGN §2 duplicated work) for thirteen assertions. Batching them is NOT the repair and is not what this row defers: `gunbc.witness_floor_workflow` `fabric_ci_evidence_calibration_timeout_minutes` records that distinct host processes ARE the process-edge subject, so fewer processes would remove the boundary rather than observe it more cheaply. BOUNDED POPULATION: exactly one job, `fabric-evidence`, and exactly one lost edge — its `needs.fabric-evidence.result` binding into the aggregate's closed-vocabulary verdict fold. No other lane, phase, witness or claim changes rung; the build and floor lanes keep every edge they had, and the calibration keeps every assertion it had. The drop is countable from the emitted workflow: `test.claim.witness_floor_workflow_consolidation_witness_test` `w_RED_fabric_evidence_executes_without_gating` reds if the job stops executing, and reds again if either gating spelling returns while this row still stands. ONE OPERATIONAL CONSEQUENCE, recorded here because it is the kind of practice that quietly stops once the person who agreed to it moves on. With the needs edge withdrawn, a `fabric-evidence` failure no longer reaches the aggregate verdict, so any lane that was reading the required context as a proxy for that lane's health is now reading a context that cannot see it. The FABRIC-CI program (warm-seal-35) accepted the drop on that basis and will check `fabric-evidence` EXPLICITLY on every head rather than inferring it from `witnesses`. Anyone else joining on the required context owes the same explicit check for as long as this row stands; that obligation ends when the trigger below is met and not before. RESTORATION TRIGGER: the CAPABILITY of a single fabric evidence process resolving its entry against the source roots at a cost that fits the required wall budget — concretely, the whole-tree parse and name census being paid once per tree state rather than once per host process, so that the 13-row plan executes its full process-edge roster inside the lane's share of a ~10-minute required wall. THIS IS NOT RETIRED BY THE MEMO PR MERGING. It is retired by a measured `fabric-evidence` job wall that leaves the required context at or under its budget with the needs edge and the FABRIC_EVIDENCE binding restored, which is the only thing that makes the block affordable again. Reducing the plan's process count, relaxing what a row asserts, or moving the calibration to a cadence does not satisfy this trigger — the first removes the subject, and the other two are different drops that would need their own rows. +### Spark serving role-scoped retirement evidence at the production plan root — declared 2026-09-02 + +**AN OPERATOR DECISION REMOVED A BEHAVIOUR'S ONLY SUBJECT, AND THIS ROW IS THAT DECLARATION (2026-09-02).** `gunbc.spark.cell_role` assigned srv6 to `SparkTrainingCell`, and the operator withdrew that dedication as premature -- 'i wouldn't dedicate a whole node for any task - just have it converge and serve whatever task we converge it to' -- so the production roster now holds ZERO training cells. Three claims in `test.claim.spark.spark_cell_role_retirement_witness_test` entered through `fleet_converge_plan_artifact`, the root the converge actuator itself walks, and each needed a production host holding that role to have a subject at all: `w_the_production_artifact_plans_four_retirements_for_the_training_cell`, `w_the_production_artifact_plans_no_rows_for_the_converged_serving_cell`, and `w_the_production_retirement_touches_no_baseline_address`. They are DELETED rather than left silently red, because a claim whose subject no longer exists is not a failing test, and leaving it to fail would have made an operator's decision look like a regression. **PREVIOUS RUNG: mechanically preventable** -- the training arm's four retirement rows and the serving arm's zero rows were both exercised through the production root, so a planner regression that pointed `spark_serving_full_membership_plan` back at the unscoped desired members went red there. **TEMPORARY RUNG: mitigatable** -- both arms are still exercised, but only at `spark_serving_role_scoped_desired_members_in` over an authored fixture roster (`w_the_planner_scopes_desired_state_by_role`), which is a real production function and is NOT the path the converge actuator calls; the same PR added `spark_cell_role_in` and that `_in` planner variant precisely so an arm's evidence stops depending on which machines are currently assigned what. **REASON:** operator decision, recorded with its basis at `gunbc.spark.cell_role` `spark_cell_role_assignment_basis`; role is converged desired state rather than a node dedication. **POPULATION, BOUNDED:** the training arm of Spark serving role scoping and the retirement rows it produces, AS REACHED THROUGH `fleet_converge_plan_artifact`. The serving arm, the no-role refusal, the reconcile, the freeze and the apply are unaffected and their production-root claims remain enrolled. **RESTORATION TRIGGER, NAMING THE CAPABILITY:** a roster-parameterized plan artifact -- the assignment roster threaded from `fleet_converge_plan_artifact` down to `spark_serving_role_scoped_desired_members_in` -- SUFFICIENT FOR a witness to drive the production root over an authored roster and read back the four retirement rows with no production host holding `SparkTrainingCell`. Half that capability exists today: both `_in` functions take the roster; what is missing is the threading through the generic artifact entry point. **RESTORING A TRAINING CELL TO THE PRODUCTION ROSTER DOES NOT RETIRE THIS DROP** -- that would re-create the coupling between an arm's evidence and the current assignment, which is the defect this row exists to record, and it is exactly the trigger-names-less-than-the-capability failure §4b(3) warns about. + ### Arity agreement between a declared builtin parameter name and its derived algebra template — declared 2026-09-01 Builtin signature grounding -- **RUNG DROP, DECLARED (2026-09-01).** PREVIOUS RUNG: none to lower -- this declares that a class created by this change lands below its attainable ceiling rather than at it. v1.compiler.infer_method pairs each row's DECLARED parameter names with the parameter TYPES derived from std.algebra. When the two lists disagree in length, pair_declared_names yields AlgebraTypeVariable { id: "unpaired_declared_parameter" } for the unpaired position instead of refusing. That is a value standing where a refusal belongs -- DESIGN section 5's fabricated-plausible-output arm -- and it is declared here rather than left as a marker that reads like a wall. TEMPORARY RUNG: mitigatable. The marker is distinctive, greppable, and reaches src/v1/stage0/src/v1_compiler_infer_method.rs, so a mismatch is DISCOVERABLE by inspection of a generated artifact. It is not mechanically preventable, because NO CONSUMER ASSERTS ITS ABSENCE: an unchecked marker is an inert lens, and DESIGN is explicit that the tier where the machinery exists and nothing gates on it is itself a lie. REASON: builtin_function_registry is a `data` initializer and a .dag data initializer has no refusal channel -- there is nowhere at construction for a typed, located diagnostic to go, so the only arms available were a fabricated value or a silently shorter list, and a marked fabrication is the more honest of the two. POPULATION: bounded and closed at 20 rows -- exactly the registry names that std.algebra also declares and that therefore pair at all (count, to_int, substring, to_string, concat, map_insert, map_merge, with, map_contains_key, map_has, lookup, map_get, map_keys, map_values, get, reverse, list_push, length, starts_with, replace). The other 112 rows author their types directly and cannot reach this arm. Zero occurrences of the marker in the tree today, which is the state this row exists to keep observable. RESTORATION TRIGGER: construction-time refusal available inside a `data` initializer -- SUFFICIENT FOR a declared/derived arity disagreement to stop the line with a typed, located diagnostic at the row that causes it, rather than to produce a marked value that construction accepts. The trigger names that capability and not any artifact that would contribute to one; a witness asserting the marker's absence would raise this to mechanically preventable but would NOT retire the row, because the invalid state would still be writable. diff --git a/src/v2/test/claim/spark_observation_scope_test.dag b/src/v2/test/claim/spark_observation_scope_test.dag index ddaa350b4d1..f4827647927 100644 --- a/src/v2/test/claim/spark_observation_scope_test.dag +++ b/src/v2/test/claim/spark_observation_scope_test.dag @@ -3,8 +3,12 @@ module v2.test.claim.spark_observation_scope import std.types { Bool, List } import product.placement_supply { HostIdentity } import gunbc.fleet_intent_network { operator_host_srv5, operator_host_srv6 } -import gunbc.spark.serving_desired { spark_serving_desired_hosts } -import gunbc.spark.cell_role { spark_serving_cell_hosts, spark_training_cell_hosts } +import gunbc.spark.cell_role { + spark_hosts_with_role_in, + SparkCellRoleAssignment, + SparkServingCell, + SparkTrainingCell, +} import gunbc.spark.serving_observation_scope { spark_serving_observation_scope, spark_observation_coverage, @@ -27,8 +31,32 @@ fn w_covered(expected: List, observed: List) -> Bool // reds if anyone reinstates it. It is not a restatement of the scope claim below: that one says the // scope CONTAINS srv6, this one says the DESIRED roster does not, so the two rosters are different // facts and cannot be substituted for one another. +// THE FIXTURE ROSTER. Every claim below about a ROLE POPULATION reads this and not production. +// +// These four claims previously read the production assignments and asserted the live counts -- +// `length(training) == 1`, `length(spark_serving_cell_hosts()) == 1`. That made the evidence for a +// MODELLED CAPABILITY contingent on which machines happened to hold which role, and when the +// operator withdrew srv6's training dedication (SPARK-PAIR-0, 2026-09-02) all four went red without +// any behaviour changing. The arm they describe still exists and still decides desired state. +// +// The scope/roster partition is the subject; the production roster was only ever one instance of it. +data w_fixture_roster: List = [ + SparkCellRoleAssignment { host: operator_host_srv5, role: SparkServingCell }, + SparkCellRoleAssignment { host: operator_host_srv6, role: SparkTrainingCell }, +] + +fn w_fixture_serving() -> List { + spark_hosts_with_role_in(assignments: w_fixture_roster, role: SparkServingCell) +} + +fn w_fixture_training() -> List { + spark_hosts_with_role_in(assignments: w_fixture_roster, role: SparkTrainingCell) +} + +// THE DEFECT'S OWN CONTROL, now stated over the fixture: a ROLE-SCOPED roster is not the +// observation scope, so scoping observation by it loses whatever the other role holds. test fn w_scoping_observation_by_desired_state_loses_the_training_cell() -> Bool { - !w_covered(expected: spark_serving_observation_scope(), observed: spark_serving_desired_hosts) + !w_covered(expected: spark_serving_observation_scope(), observed: w_fixture_serving()) } test fn w_the_observation_scope_carries_both_spark_units() -> Bool { @@ -39,14 +67,14 @@ test fn w_the_observation_scope_carries_both_spark_units() -> Bool { // THE SCOPE IS WIDER THAN EITHER ROLE ROSTER, WHICH IS THE PARTITION THE RETIREMENT NEEDS. test fn w_the_scope_is_not_the_serving_roster() -> Bool { - length(spark_serving_cell_hosts()) == 1 + length(w_fixture_serving()) == 1 && length(spark_serving_observation_scope()) == 2 } test fn w_the_scope_covers_the_training_cell_the_serving_roster_omits() -> Bool { - let training = spark_training_cell_hosts() + let training = w_fixture_training() length(training) == 1 - && w_covered(expected: spark_serving_observation_scope(), observed: concat(spark_serving_cell_hosts(), training)) + && w_covered(expected: spark_serving_observation_scope(), observed: concat(w_fixture_serving(), training)) } // COVERAGE CONTROLS: each defect is a distinct arm, so each gets its own red. @@ -85,6 +113,6 @@ test fn w_a_duplicated_host_refuses() -> Bool { // A NON-EMPTY ROSTER IS NOT A COVERED ONE, WHICH IS THE GUARD THE OLD CHECK COULD NOT EXPRESS. test fn w_a_non_empty_but_narrowed_observation_is_still_refused() -> Bool { - let narrowed = spark_serving_desired_hosts + let narrowed = w_fixture_serving() length(narrowed) > 0 && !w_covered(expected: spark_serving_observation_scope(), observed: narrowed) }