From a5e0b5ae9671fe8a87121b6af42bd061ed03c587 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 19:08:35 +0000 Subject: [PATCH 01/11] Spark serving route: the operator's site allocation, and a first-party self-use posture behind it Two deliberate walls stood between a dashboard dispatch and a placed serving turn, and either alone unblocks nothing, so they land together. WALL 1 -- THE ROUTE HAD NO REGION. gunbc.spark.serving_offer refused every offer because a ProviderRoute needs a region and nothing observes which region a serving host sits in (withdrawn by operator ruling 2026-09-09). That refusal was right for a rented route. For a unit the operator owns and physically holds, no observer can ever exist -- the site is what the operator says it is -- so the fix is not an observer but an ATTRIBUTABLE ALLOCATION, and SparkServingRoute grows a third arm, ServingRouteOperatorAsserted, so the two kinds of fact are told apart by matching rather than by prose. The allocation is the operator's 2026-09-11 assertion that every Spark unit sits at his NYC home, outside the rack, carried in the OperatorAllocation carrier gunbc.spark.dgx_procurement already uses for the slot join. "Right now" is carried by decided_on: a move into the rack is a NEW row, never an edit. THE SITE IS NOT MINTED. gunbc.fleet_physical_inventory operator_site already IS the operator's premises and gunbc.fleet_site_locale records that minting a second SiteIdentity for this exact place was already done once and reverted as the section 3 nickname failure. "Outside the rack" is a per-asset RackResidence fact, not a site fact. WALL 2 -- PROVIDER USE. gunbc.spark.first_party_serving declares the posture the route is used under: gunbc serving gunbc, our own material, on operator-owned hardware, with no third party and no border crossed. The provider anchor is declared in OUR layer because for self-hosted serving the provider is us; vLLM and the weights stay upstream facts in extdeps and are what the service runs, not who provides it. "FOR NOW" IS ENFORCED BY EXECUTION, NOT WRITTEN DOWN. The single sanction row is bound to this posture revision, so another customer profile refuses as CustomerScopeUnsupported and a superseded posture refuses as PostureRevisionStale -- both are reds in the new witness. NO FABRICATED LEGAL FINDINGS. The three use dispositions are required to be DispositionCleared before a permit mints, and each one's evidence names a declaration stating the program is NOT ENGAGED under first-party self-use -- no screening was run and no determination is claimed. A witness asserts the permit carries exactly those references, so swapping one for a clearance goes red. WHAT STILL DOES NOT PLACE A TURN, stated rather than implied: a CandidateOffer needs a demand and a work identity, a WorkKey comes only from product.fabric.work derive_work_key, and gunbc.serving.turn_demand refuses to bind a source manifest because nothing observes the weights, tokenizer and runtime closure a launch loaded. harness_seat's refusal note is repointed from "no provider-use admission producer exists" -- which stops being true here -- to that obligation, and the admission producer carries it as a declared frontier (DESIGN 3c) with the receipt that retires it as its trigger. The witness that asserted the standing refuses flips to a regression control per DESIGN 4b(4) rather than being deleted. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/harness/harness_seat.dag | 30 +- dag/gunbc/spark/first_party_serving.dag | 367 ++++++++++++++++++ dag/gunbc/spark/serving_offer.dag | 71 +++- ...spark_first_party_serving_witness_test.dag | 133 +++++++ ...spark_serving_offer_route_witness_test.dag | 31 +- 5 files changed, 602 insertions(+), 30 deletions(-) create mode 100644 dag/gunbc/spark/first_party_serving.dag create mode 100644 dag/test/claim/spark/spark_first_party_serving_witness_test.dag diff --git a/dag/gunbc/harness/harness_seat.dag b/dag/gunbc/harness/harness_seat.dag index 997d48756ba..99bdb615b95 100644 --- a/dag/gunbc/harness/harness_seat.dag +++ b/dag/gunbc/harness/harness_seat.dag @@ -271,19 +271,25 @@ fn harness_no_candidate(acc: HarnessCandidates, note: String, retryable: Bool) - HarnessCandidates { candidates: acc.candidates, notes: concat(acc.notes, [note]), retryable: acc.retryable || retryable } } -// NO CANDIDATE IS PRODUCED FROM A BOUND OFFER ANY MORE, AND THE MISSING PIECE IS ADMISSION RATHER -// THAN BINDING. A CandidateOffer now seals a ProviderUsePermit, so bind_candidate needs a -// ProviderUseAdmission over the offer's route -- and producing one through admit_provider_use -// requires a ProviderUseScope carrying a customer profile, a data-handling profile, an agreement -// and three cleared dispositions. Those are compliance claims about us; there is no producer for -// them, and writing plausible ones so the call typechecks is the fail-open this wall exists to -// close. So the SparkOfferBound arm reports what is missing and seats nobody. +// NO CANDIDATE IS PRODUCED FROM A BOUND OFFER YET, AND THE MISSING PIECE HAS MOVED ONE WALL BACK. +// Two of the three obstacles are now gone: spark_serving_route_standing carries the operator's +// dated site allocation rather than refusing, and gunbc.spark.first_party_serving +// spark_first_party_admission is the provider-use admission producer this note used to say did not +// exist. What remains is the offer's OTHER seal. // -// That arm is unreachable today for a second, independent reason -- spark_serving_route_standing -// refuses above it -- and the two are deliberately separate: landing a region observer alone must -// not silently resume seating through a path nothing admitted. +// A CandidateOffer is sole_constructor through product.fabric.selection bind_candidate, which takes +// a DEMAND IDENTITY and a WORK IDENTITY and compares the permit against both. A WorkKey comes from +// exactly one place -- product.fabric.work derive_work_key, through work_for -- which needs a +// WorkContract, which needs a SourceManifestRef; and gunbc.serving.turn_demand refuses to produce +// one, because nothing in this repository observes the exact weights, tokenizer and runtime closure +// a launch loaded (serving_turn_source_obligation). Minting a key beside derive_work_key would +// fabricate the identity the fabric's deduplication and receipts are keyed on, so this arm reports +// what is missing and seats nobody rather than inventing it. // -// Restoration trigger: a provider-use admission producer for the spark serving route. +// Restoration trigger: a launch receipt that reads the weights, tokenizer and runtime closure off a +// running engine, SUFFICIENT FOR gunbc.serving.turn_demand serving_turn_work to return TurnWorkBound +// for a harness turn -- at which point the demand and work identities exist, the admission producer +// above is called with them, and bind_candidate has everything it compares. fn harness_bind_candidate(acc: HarnessCandidates, group: FabricGroup, address: String, launch: VllmEndpointProcessLaunch, now: EpochSecs) -> HarnessCandidates { match bind_spark_serving_offer( principal: "gunbc" as NonEmptyStr, @@ -303,7 +309,7 @@ fn harness_bind_candidate(acc: HarnessCandidates, group: FabricGroup, address: S acc: acc, note: seat_bind_detail( group: group, - text: "the serving offer bound but no provider-use admission producer exists for its route, so it cannot become a candidate", + text: "the serving offer bound and its route is admissible, but a serving turn has no Work identity: nothing observes the weights, tokenizer and runtime closure a launch loaded, so gunbc.serving.turn_demand cannot bind a source manifest and product.fabric.selection bind_candidate has no work to compare the permit against", ), retryable: false, ) diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag new file mode 100644 index 00000000000..20867f6aab3 --- /dev/null +++ b/dag/gunbc/spark/first_party_serving.dag @@ -0,0 +1,367 @@ +module gunbc.spark.first_party_serving + +import std.types { NonEmptyStr, List } +import std.decl_ref { DeclarationRef, decl_ref } +import std.content_hash { as_content_hash_structural, content_hash_atom } +import product.placement_supply { SiteIdentity, HostIdentity } +import product.fabric.identity { FabricIdentity, DemandKey, WorkKey, OfferKey } +import product.fabric.provider_route { + ProviderRoute, CompliancePostureRevision, ProviderRouteFacts, + ProviderDataPathClosure, ProviderPathStanding, ProviderPathLocated, + DownstreamProviderPopulation, NoDownstreamProviders, +} +import product.fabric.provider_admission { + RouteScopeSanction, ProviderUseScope, ProviderUseAdmission, + DispositionStanding, DispositionCleared, admit_provider_use, +} +import gunbc.spark.dgx_procurement { OperatorAllocation } +import gunbc.fleet_physical_inventory { operator_site } +import gunbc.fleet_intent_network { + operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8, + operator_host_srv9, operator_host_srv10, operator_host_srv11, operator_host_srv12, +} + +// ── WHY A SERVING ROUTE EXISTS AT ALL NOW, AND WHAT KIND OF FACT IT RESTS ON ────────────────── +// +// gunbc.spark.serving_offer refused every offer because its ProviderRoute needs a region and +// nothing OBSERVES which region a serving host sits in. That refusal was correct for a rented +// route: where someone else's machine sits is a fact about someone else's estate, and inventing it +// is the fabricated placement the fabric exists to prevent. +// +// A SELF-HOSTED UNIT IS THE CASE WHERE NO OBSERVER CAN EXIST, AND THAT IS A STATED DIVERGENCE +// (DESIGN section 3b) RATHER THAN A REGION SOMEBODY MEASURED. There is no third party to ask and no +// vendor API to read: the site of a machine the operator owns and physically holds is what the +// operator says it is. So the standing this module supplies is an ATTRIBUTABLE ALLOCATION -- a +// decider, a date and a basis -- carried in the same OperatorAllocation gunbc.spark.dgx_procurement +// already uses for the slot join, and for the same reason it gives there: recording a commitment as +// an observation would present it as recoverable evidence rather than as something someone said. +// gunbc.spark.serving_offer keeps the two APART STRUCTURALLY, in two arms of SparkServingRoute, so +// no reader has to take this paragraph's word for which one they are holding. +// +// THE SITE IS NOT MINTED HERE, AND THAT IS THE SECOND HALF OF THE POINT. The operator's premises +// already have one authority -- gunbc.fleet_physical_inventory operator_site -- and +// gunbc.fleet_site_locale records that minting a second SiteIdentity for this exact place was +// already done once and reverted as the section 3 nickname failure. The operator's 2026-09-11 +// assertion NAMES that site (his NYC home) and scopes every Spark unit to it; it does not introduce +// a place the corpus did not already carry. The NEARBY NAME THAT IS NOT THIS ONE: +// gunbc.spark.serving_deployment_selection serving_topology_region is a Pareto DecisionRegion -- a +// region of a decision field, not a place a machine sits. + +// SCOPED TO THE UNITS, NOT TO THE RACK. "Outside the rack" is a per-asset residence fact that +// product.placement_supply RackResidence owns; what this row states is the SITE, which is the fact +// a route needs. The units are listed rather than summarized as "all sparks" because a roster that +// names itself cannot be checked, and a unit added later must be an edit someone makes deliberately. +type SparkFleetSiteAllocation { + site: SiteIdentity + units: List + allocation: OperatorAllocation +} + +// "RIGHT NOW" IS LOAD-BEARING AND IS CARRIED BY decided_on RATHER THAN BY A CAVEAT. When the units +// move into the rack that is a NEW allocation row with a later date, never an edit to this one -- +// the same discipline dgx_procurement's superseded-address note states: a dated row that disagrees +// with the present is a dated row, not a stale one, and rewriting it would present a 2026-09-11 +// decision as though it had been taken on facts that did not exist yet. +data spark_fleet_site_allocation: SparkFleetSiteAllocation = SparkFleetSiteAllocation { + site: operator_site, + units: [ + operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8, + operator_host_srv9, operator_host_srv10, operator_host_srv11, operator_host_srv12, + ], + allocation: OperatorAllocation { + decided_by: "operator (2026-09-11): 'srv5, 6, and all the sparks sit outside the rack right now, but in my NYC home'", + decided_on: "2026-09-11", + basis: "The operator asserts that every Spark unit sits at his NYC home, outside the rack, as of this date. This is an ATTRIBUTABLE ASSERTION and not a measurement: for hardware the operator owns and holds there is no third party to observe the site, so no observer can exist and none is claimed. It names the site the corpus already carries as gunbc.fleet_physical_inventory operator_site, whose civil zone gunbc.fleet_site_locale already records as America/New_York, rather than introducing a second name for one place. It is explicitly NOT a colocation facility: no row of extdeps.colo.interserver or any other extdeps.colo operator describes where these units sit. RIGHT NOW is part of the assertion -- the units are expected to move into the rack later, and that move is a NEW allocation row carrying its own date, never an edit to this one.", + }, +} + +// ── THE PROVIDER IS US, WHICH IS THE ONE MODELING CALL THIS MODULE MAKES ────────────────────── +// +// A ProviderRoute is provider x service x region and all three are cited declarations. For a rented +// route the provider anchor lives in extdeps, because an independently governed upstream owns its +// own facts. Self-hosted serving has no such upstream: the hardware is the operator's, the engine +// runs on our own site, and the turn is served by us to us. vLLM and the served weights remain +// upstream facts and keep their extdeps homes -- they are what the service RUNS, not who provides +// it -- and borrowing one of their vendor anchors as the provider would invert the layering that +// product.fabric.provider_route fixes deliberately: extdeps carries facts about the provider, and +// whether we are willing and authorised to use them is a fact about US (operator ruling 2026-09-11). +// +// So the provider anchor is declared here, in our layer, and it is the principal the harness +// already places work under. +type FirstPartyServingAuthority { + principal: NonEmptyStr + basis: NonEmptyStr +} + +data gunbc_first_party_serving_provider: FirstPartyServingAuthority = FirstPartyServingAuthority { + principal: "gunbc", + basis: "For self-hosted Spark serving the provider is gunbc itself: the units are operator-owned, they sit at the operator's own site, and the engine is run by us. This is the same principal gunbc.harness.harness_seat already passes as the fabric principal, so the route names the party that is actually serving rather than an upstream vendor whose software happens to be running.", +} + +// THE SERVICE IS THE DEPLOYMENT WE ALREADY DECLARE, cited rather than re-coined: the thing being +// offered on this route is the Spark pair serving deployment, whose single authority is +// gunbc.spark.pair_serving_desired. A fresh service anchor beside it would be a second name for it. +fn spark_first_party_service_ref() -> DeclarationRef { + decl_ref(module_path: "gunbc.spark.pair_serving_desired", decl_name: "spark_pair_serving_desired") +} + +fn spark_first_party_provider_ref() -> DeclarationRef { + decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "gunbc_first_party_serving_provider") +} + +// THE REGION IS THE ALLOCATION, NOT THE SITE ROW, and that is deliberate. Citing operator_site alone +// would name a place while dropping the only thing that makes the claim honest -- who said the units +// are there, and when. A route's region reference is read by auditors reconstructing why a turn was +// admitted, and this one leads them straight to the assertion it rests on. +fn spark_first_party_region_ref() -> DeclarationRef { + decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_fleet_site_allocation") +} + +fn spark_first_party_route() -> ProviderRoute { + ProviderRoute { + provider: spark_first_party_provider_ref(), + service: spark_first_party_service_ref(), + region: spark_first_party_region_ref(), + } +} + +// ── THE POSTURE: FIRST-PARTY SELF-USE, AND WHAT ENDS IT ─────────────────────────────────────── +// +// "FOR NOW" IS LOAD-BEARING AND IS NOT MODELED HERE, because it is already modeled: a sanction is +// per posture revision by construction, and product.fabric.provider_admission refuses a sanction +// evaluated under a superseded revision as PostureRevisionStale. Serving anybody else is a +// materially different contract subject, so it is a NEW posture revision that makes every sanction +// under this one stale -- not an extra profile quietly added to the roster below. That is why the +// staleness_condition field is a field of the posture rather than a sentence in an annotation: no +// Accepted program reads an annotation (DESIGN 4c), and every consumer of this row reads this. +type FirstPartySelfUsePosture { + assertion: OperatorAllocation + serves: NonEmptyStr + data_subject: NonEmptyStr + hardware_custody: NonEmptyStr + staleness_condition: NonEmptyStr +} + +data spark_first_party_use_posture: FirstPartySelfUsePosture = FirstPartySelfUsePosture { + assertion: OperatorAllocation { + decided_by: "operator (2026-09-11): 'it is just serving us for now'", + decided_on: "2026-09-11", + basis: "The operator asserts that the Spark serving groups serve gunbc itself and nobody else as of this date. Attributable assertion, not a measurement: who the served turns are for is a fact about our intent, which no probe can read off a running engine.", + }, + serves: "gunbc itself. Every turn placed on this route originates inside this repository's own harness and control plane; no turn is served to any party outside gunbc and none crosses an organisational or national boundary.", + data_subject: "our own material. The prompts and responses on this route are gunbc's, held on operator-owned hardware at the operator's own site; no customer data and no third-party data is processed on it.", + hardware_custody: "operator-owned and operator-held. There is no third-party agreement governing this route because there is no third party: no hosting contract, no processor, and no service terms stand between us and the hardware.", + staleness_condition: "SERVING ANYONE ELSE ENDS THIS POSTURE. A turn served to a party outside gunbc, or any third-party material processed on this route, is a materially different contract subject and requires a NEW CompliancePostureRevision; every RouteScopeSanction below is bound to THIS revision, so it goes stale through product.fabric.provider_admission PostureRevisionStale rather than silently carrying over. Nothing here may be widened to cover another customer profile by adding a roster row under this revision.", +} + +// The revision is the hash of the statement's identity as a named revision, not of the row's bytes. +// A statement change that does not move this tag is the hazard, and it is the reason the posture's +// own staleness_condition names re-posturing rather than editing: the authority reference below +// points at the row, so an auditor re-derives what was evaluated by reading it. +data spark_first_party_posture: CompliancePostureRevision = CompliancePostureRevision { + authority: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture"), + revision: as_content_hash_structural(structural: content_hash_atom(value: "gunbc.spark.first-party-self-use.2026-09-11" as NonEmptyStr)), +} + +// ── THE PROFILES THE SANCTION IS WRITTEN OVER ───────────────────────────────────────────────── +// +// Each is a declared row because RouteScopeSanction and ProviderUseScope compare them by +// declaration reference: a profile spelled as a branded string would let a scope and a sanction +// agree by spelling while meaning different things, which is exactly the magic-string failure the +// route type was built to remove. +type FirstPartyUseProfile { + label: NonEmptyStr + basis: NonEmptyStr +} + +data spark_first_party_customer_profile: FirstPartyUseProfile = FirstPartyUseProfile { + label: "first-party-self", + basis: "The customer is gunbc. The only consumer of turns placed on this route is this repository's own harness and control plane, so there is no customer relationship on this route at all.", +} + +data spark_own_data_handling_profile: FirstPartyUseProfile = FirstPartyUseProfile { + label: "own-data", + basis: "Our own material only, on operator-owned hardware at the operator's own site. No customer data, no third-party data, and no transfer to any other party.", +} + +data spark_operator_owned_hardware_agreement: FirstPartyUseProfile = FirstPartyUseProfile { + label: "operator-owned-hardware", + basis: "The agreement authority for this route is the operator's ownership of the hardware. There is no third-party contract to present because there is no third party; this row is what the scope names so that an agreement is a cited authority rather than an empty field.", +} + +// ── THE THREE USE PROGRAMS, AND WHY EACH READS 'NOT ENGAGED' RATHER THAN 'CLEARED' ──────────── +// +// This is the point the whole wall exists to protect, so it is stated in the VALUES and not only +// here. admit_provider_use requires the prohibited-use, sanctions and export dispositions to be +// DispositionCleared before a permit mints, and the tempting way to satisfy that is to write three +// clearances -- which would be fabricated legal findings, the fail-open this gate closes. Nobody has +// run a screening, no determination has been made, and none is claimed. +// +// WHAT IS ACTUALLY TRUE is narrower and is what each row below says: under first-party self-use +// these programs have NO SUBJECT. Nothing is supplied to any party, nothing is exported, and nothing +// crosses a border, because the turn begins and ends inside gunbc on hardware gunbc's operator owns +// at a site in the operator's own home. The evidence each disposition carries is THIS POSTURE +// DECLARATION and nothing else, so a reader following the reference arrives at the statement "not +// engaged, because first-party self-use" rather than at a clearance somebody appears to have issued. +// The moment the posture changes -- the moment a turn is served to anyone else -- these rows stop +// describing the route, which is why they cite the posture that goes stale rather than standing on +// their own. +type UseProgramStanding { + program: NonEmptyStr + engagement: NonEmptyStr + basis: NonEmptyStr +} + +data spark_prohibited_use_not_engaged: UseProgramStanding = UseProgramStanding { + program: "prohibited use", + engagement: "NOT ENGAGED under first-party self-use. This is not a review or a determination; no prohibited-use assessment has been performed.", + basis: "The route serves gunbc's own turns to gunbc. There is no user, customer or counterparty whose use could be governed, so the program has no subject here. It acquires one the moment gunbc.spark.first_party_serving spark_first_party_use_posture is superseded by serving anyone else, at which point this row no longer describes the route.", +} + +data spark_sanctions_not_engaged: UseProgramStanding = UseProgramStanding { + program: "sanctions", + engagement: "NOT ENGAGED under first-party self-use. This is NOT a sanctions determination and no screening was performed against any list.", + basis: "Nothing is supplied, sold or made available to any party outside gunbc on this route: the turn is served on operator-owned hardware at the operator's own site to gunbc itself. With no counterparty there is no party to screen, so the program has no subject here. It acquires one the moment gunbc.spark.first_party_serving spark_first_party_use_posture is superseded by serving anyone else, at which point this row no longer describes the route.", +} + +data spark_export_not_engaged: UseProgramStanding = UseProgramStanding { + program: "export control", + engagement: "NOT ENGAGED under first-party self-use. This is NOT an export determination, classification or licence finding.", + basis: "Nothing leaves gunbc and nothing crosses a national boundary on this route: the units sit at one site, the operator's NYC home (gunbc.spark.first_party_serving spark_fleet_site_allocation), and the turns begin and end inside gunbc. With no transfer and no recipient there is no export to classify, so the program has no subject here. It acquires one the moment the posture is superseded by serving anyone else or by placing a unit outside that site.", +} + +fn spark_prohibited_use_disposition() -> DispositionStanding { + DispositionCleared { + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_prohibited_use_not_engaged"), + } +} + +fn spark_sanctions_disposition() -> DispositionStanding { + DispositionCleared { + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_sanctions_not_engaged"), + } +} + +fn spark_export_disposition() -> DispositionStanding { + DispositionCleared { + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_export_not_engaged"), + } +} + +// ── THE SANCTION ROSTER: ONE ROW, AND ONE IS THE POINT ──────────────────────────────────────── +// +// A roster row admits a (route, posture, customer profile, data class) tuple. There is exactly one, +// so any other customer profile or data class on this route has no matching row and refuses as +// CustomerScopeUnsupported or DataHandlingUnsupported -- which is how "it is just serving us for +// now" is enforced by execution rather than by this sentence. Adding a second row to widen it is +// the move the posture's staleness_condition forbids. +fn spark_first_party_sanction_roster() -> List { + [ + RouteScopeSanction { + route: spark_first_party_route(), + posture: spark_first_party_posture, + customer_profile: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_customer_profile"), + data_handling_profile: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_own_data_handling_profile"), + requires_agreement: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_operator_owned_hardware_agreement"), + }, + ] +} + +// ── THE ROUTE FACTS: NINE PATHS, ALL LOCATED, NONE ABSENT ───────────────────────────────────── +// +// EVERY PATH IS LOCATED AT THE SAME SITE BY THE SAME ASSERTION, and no path is claimed ABSENT. The +// tempting shortcut is to write backups or spill as ProviderPathAbsent -- "we do not back the +// serving host up" -- and that would be a claim about our own machines that nobody has made and no +// probe has read. What the operator's assertion DOES establish is location: whatever these paths +// are, they terminate on operator-owned hardware at the operator's own site, because there is no +// other estate for them to reach. So every path takes the located arm, with the site allocation as +// its jurisdiction and the posture as its evidence, and the honest weakness of the row is that its +// operator and jurisdiction are an allocation rather than a measurement -- which is the same stated +// divergence the route itself carries, not a second one. +fn spark_first_party_path() -> ProviderPathStanding { + ProviderPathLocated { + operator: spark_first_party_provider_ref(), + jurisdiction: spark_first_party_region_ref(), + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture"), + } +} + +// NO DOWNSTREAM PROVIDERS, and this is the one place the arm is straightforwardly true rather than +// asserted: a downstream provider is a party that processes our material on the provider's behalf, +// and a machine we own, in a room the operator holds, has none. The evidence is the posture, because +// that is the declaration stating the custody the claim rests on. +fn spark_first_party_downstream() -> DownstreamProviderPopulation { + NoDownstreamProviders { + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture"), + } +} + +fn spark_first_party_route_facts() -> ProviderRouteFacts { + ProviderRouteFacts { + route: spark_first_party_route(), + contract_terms: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_operator_owned_hardware_agreement"), + data_paths: ProviderDataPathClosure { + execution: spark_first_party_path(), + durable_storage: spark_first_party_path(), + backups: spark_first_party_path(), + logs: spark_first_party_path(), + telemetry: spark_first_party_path(), + control_plane: spark_first_party_path(), + support_access: spark_first_party_path(), + administrative_access: spark_first_party_path(), + spill: spark_first_party_path(), + }, + downstream: spark_first_party_downstream(), + observed_at: "2026-09-11T00:00:00Z", + facts_revision: as_content_hash_structural(structural: content_hash_atom(value: "gunbc.spark.first-party-route-facts.2026-09-11" as NonEmptyStr)), + } +} + +// ── THE SCOPE AND THE ADMISSION ─────────────────────────────────────────────────────────────── +// +// The demand and the work are PARAMETERS, never literals here. admit_provider_use seals them into +// the permit and product.fabric.selection compares the permit against the demand and work the +// candidate is being bound for, so a work key transcribed beside the call would refuse every real +// placement -- and, worse, would be a work identity this module invented. +fn spark_first_party_use_scope

( + demand: FabricIdentity, + work: FabricIdentity, +) -> ProviderUseScope

{ + ProviderUseScope { + demand: demand, + work: work, + customer_profile: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_customer_profile"), + data_handling_profile: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_own_data_handling_profile"), + agreement: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_operator_owned_hardware_agreement"), + prohibited_use_disposition: spark_prohibited_use_disposition(), + sanctions_disposition: spark_sanctions_disposition(), + export_disposition: spark_export_disposition(), + } +} + +// THE SCOPE IS A PARAMETER RATHER THAN BUILT INSIDE, which is what makes the refusal path +// executable: a caller bringing a scope this posture does not sanction -- another customer profile, +// another data class -- reaches the same producer and is refused by it, instead of the refusal being +// a state only a fixture could construct. +// +// DECLARED FRONTIER (DESIGN section 3c). The production consumer of this function is +// gunbc.harness.harness_seat, which cannot call it yet: product.fabric.selection bind_candidate +// needs a demand identity and a work identity, a WorkKey comes only from product.fabric.work +// derive_work_key, and gunbc.serving.turn_demand serving_turn_source_obligation refuses to produce +// the source manifest that would feed it. TRIGGER: a launch receipt that reads the exact weights, +// tokenizer and runtime closure off a running engine, SUFFICIENT FOR gunbc.serving.turn_demand +// serving_turn_work to return TurnWorkBound for a harness turn. Until then this producer is executed +// by test.claim.spark.spark_first_party_serving_witness_test, which exercises both arms. +fn spark_first_party_admission

( + scope: ProviderUseScope

, + offer: FabricIdentity, +) -> ProviderUseAdmission

{ + admit_provider_use( + roster: spark_first_party_sanction_roster(), + facts: spark_first_party_route_facts(), + active: spark_first_party_posture, + scope: scope, + offer: offer, + decision_receipt: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture"), + ) +} diff --git a/dag/gunbc/spark/serving_offer.dag b/dag/gunbc/spark/serving_offer.dag index 9a5fcb59de9..4da44a93a7b 100644 --- a/dag/gunbc/spark/serving_offer.dag +++ b/dag/gunbc/spark/serving_offer.dag @@ -11,6 +11,8 @@ import product.fabric.provider_route { ProviderRoute } import std.measure { Second, second, MoneyRate, money_amount_micro, hardware_thread_count } import extdeps.currency.currency { Usd } import gunbc.spark.fabric_switch_observed { fabric_group_wire } +import gunbc.spark.dgx_procurement { OperatorAllocation } +import gunbc.spark.first_party_serving { spark_first_party_route, spark_fleet_site_allocation } import gunbc.spark.vllm_endpoint_process_launch { VllmEndpointProcessLaunch, vllm_endpoint_process_launch_key, } @@ -109,18 +111,42 @@ type SparkServingReadiness // THE NEARBY NAME THAT IS NOT THIS ONE: gunbc.spark.serving_deployment_selection // serving_topology_region is a DecisionRegion from the Pareto vocabulary -- a region of a decision // field, not a place a machine sits. Reusing it here would be one name for two concepts. +// THE THIRD ARM IS WHERE THE SPARKS ACTUALLY SIT, AND IT IS A SEPARATE ARM PRECISELY SO THAT +// NOBODY HAS TO TRUST AN ANNOTATION. A unit the operator owns and physically holds has no possible +// observer of its site: there is no vendor to ask and no API to read, because the site is what the +// operator says it is. The honest carrier for that is an ATTRIBUTABLE ALLOCATION -- decider, date, +// basis -- which is what gunbc.spark.dgx_procurement OperatorAllocation already is, and which +// gunbc.spark.first_party_serving fills for every Spark unit from the operator's 2026-09-11 +// assertion. Putting it in the observed arm would have relabelled an allocation as a measurement, +// and the divergence (DESIGN section 3b) would then have been readable only in prose; as its own +// arm, every consumer that cares can tell the two apart by matching, and the offer records which +// kind of fact its region rests on. type SparkServingRoute = ServingRouteObserved { route: ProviderRoute } + | ServingRouteOperatorAsserted { route: ProviderRoute, allocation: OperatorAllocation } | ServingRouteRegionUnobserved { obligation: NonEmptyStr } -// THE SINGLE PLACE THE STALL IS RECORDED, so the observer replaces one declaration rather than -// every call site. Restoration trigger: a producer that OBSERVES which site a serving host sits in -// and returns ServingRouteObserved. Until then every spark serving offer refuses to bind, which is -// a live capability withdrawn deliberately (operator ruling, 2026-09-09) rather than a defect. +// THE SINGLE PLACE THE STANDING IS RECORDED, which is why the 2026-09-11 restoration replaced one +// declaration rather than every call site -- the same property that made the withdrawal cheap. +// +// THE OBLIGATION ROW SURVIVES THE RESTORATION AND IS NOT DEAD. It is the refusal a caller reaches +// when it has no allocation and no observation to offer, it is what the binder reports for that +// arm, and test.claim.spark.spark_serving_offer_route_witness_test still drives the binder with it. +// Deleting it would delete the only spelling of "this route's region rests on nothing". data spark_serving_route_region_obligation: NonEmptyStr = "gunbc.spark.serving_offer: no producer observes which region a serving host sits in, so the offer's ProviderRoute cannot be constructed and the offer does not bind" +// WITHDRAWN 2026-09-09, RESTORED 2026-09-11 ON AN ASSERTION RATHER THAN AN OBSERVATION. The +// withdrawal was right: what it refused was a region nobody had established. What changed is not +// that somebody measured one -- for self-hosted units nobody ever can -- but that the operator +// stated where the units are, dated and attributable, and gunbc.spark.first_party_serving carries +// that statement as an OperatorAllocation over every Spark unit. The standing therefore selects the +// asserted arm, and the route it carries is the first-party one: provider us, service the pair +// serving deployment, region the allocation itself. fn spark_serving_route_standing() -> SparkServingRoute { - ServingRouteRegionUnobserved { obligation: spark_serving_route_region_obligation } + ServingRouteOperatorAsserted { + route: spark_first_party_route(), + allocation: spark_fleet_site_allocation.allocation, + } } type SparkOfferBinding

@@ -159,8 +185,38 @@ fn bind_spark_serving_offer

( match route { ServingRouteRegionUnobserved { obligation: why } => SparkOfferBindingRefused { group_wire: fabric_group_wire(g: launch.group), cause: why } + ServingRouteOperatorAsserted { route: asserted, allocation: _ } => + bind_spark_serving_offer_on_route( + principal: principal, executor: executor, launch: launch, model: model, + trust_domain: trust_domain, isolation: isolation, seats: seats, + readiness: readiness, route: asserted, + ) ServingRouteObserved { route: r0 } => - match readiness { + bind_spark_serving_offer_on_route( + principal: principal, executor: executor, launch: launch, model: model, + trust_domain: trust_domain, isolation: isolation, seats: seats, + readiness: readiness, route: r0, + ) + } +} + +// THE TWO ROUTE-BEARING ARMS BIND THROUGH ONE BODY, so an offer built from an asserted site and one +// built from an observed site cannot drift apart. What distinguishes them is entirely upstream -- +// which arm a producer could honestly construct -- and nothing downstream of the route treats them +// differently, because a ProviderRoute is a ProviderRoute once it exists. Duplicating the binder +// per arm would have been the fork that lets exactly that stop being true. +fn bind_spark_serving_offer_on_route

( + principal: P, + executor: P, + launch: VllmEndpointProcessLaunch, + model: NonEmptyStr, + trust_domain: TrustDomainRef, + isolation: IsolationProfile, + seats: Int, + readiness: SparkServingReadiness, + route: ProviderRoute, +) -> SparkOfferBinding

{ + match readiness { ServingUnobserved { obligation: why } => SparkOfferBindingRefused { group_wire: fabric_group_wire(g: launch.group), cause: why } ServingObserved { ready_at: at, receipt: r } => @@ -168,7 +224,7 @@ fn bind_spark_serving_offer

( bound: SparkOfferProjection { offer: SupplierOffer { id: FabricIdentity { principal: principal, key: spark_serving_offer_key(launch: launch) }, - route: r0, + route: route, executor: executor, shape: spark_serving_shape(), capabilities: spark_serving_capability(model: model), @@ -183,6 +239,5 @@ fn bind_spark_serving_offer

( launch: launch, }, } - } } } diff --git a/dag/test/claim/spark/spark_first_party_serving_witness_test.dag b/dag/test/claim/spark/spark_first_party_serving_witness_test.dag new file mode 100644 index 00000000000..aa0258ea11a --- /dev/null +++ b/dag/test/claim/spark/spark_first_party_serving_witness_test.dag @@ -0,0 +1,133 @@ +module test.claim.spark.spark_first_party_serving_witness_test + +import std.types { Bool, NonEmptyStr, String } +import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq } +import std.content_hash { as_content_hash_structural, content_hash_atom } +import product.fabric.identity { FabricIdentity, DemandKey, WorkKey, OfferKey } +import product.fabric.provider_route { CompliancePostureRevision } +import product.fabric.provider_admission { + ProviderUseScope, ProviderUseAdmission, ProviderUseAdmitted, ProviderUseDenied, + refusal_reason, admit_provider_use, +} +import gunbc.spark.first_party_serving { + spark_first_party_use_scope, spark_first_party_admission, + spark_first_party_sanction_roster, spark_first_party_route_facts, spark_first_party_posture, + spark_sanctions_disposition, spark_export_disposition, spark_prohibited_use_disposition, +} + +// WHAT THESE ROWS ARE FOR. gunbc.spark.first_party_serving admits exactly one use of the Spark +// serving route -- gunbc serving gunbc, on our own material, on operator-owned hardware -- and the +// operator's assertion behind it is explicitly "for now". "For now" is only worth writing down if +// something EXECUTES it, so the refusal rows below are the substance of this file and the admitted +// row is the control that stops them from being satisfied by a producer that refuses everything. + +fn t_demand() -> FabricIdentity { + FabricIdentity { principal: "gunbc" as NonEmptyStr, key: "harness-turn-demand-1" as DemandKey } +} + +fn t_work() -> FabricIdentity { + FabricIdentity { principal: "gunbc" as NonEmptyStr, key: "harness-turn-work-1" as WorkKey } +} + +fn t_offer() -> FabricIdentity { + FabricIdentity { principal: "gunbc" as NonEmptyStr, key: "group-a@http://192.168.1.225:30000@1" as OfferKey } +} + +// THE THIRD-PARTY SCOPE IS THE SAME SCOPE WITH ONE FIELD CHANGED, which is what makes the refusal +// below discriminating: it differs from the admitted scope ONLY in who the customer is, so a +// producer that admitted it would be admitting a customer profile no posture sanctions. +fn t_third_party_profile() -> DeclarationRef { + decl_ref(module_path: "test.claim.spark.spark_first_party_serving_witness_test", decl_name: "t_third_party_profile") +} + +fn t_third_party_scope() -> ProviderUseScope { + ProviderUseScope { + demand: t_demand(), + work: t_work(), + customer_profile: t_third_party_profile(), + data_handling_profile: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_own_data_handling_profile"), + agreement: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_operator_owned_hardware_agreement"), + prohibited_use_disposition: spark_prohibited_use_disposition(), + sanctions_disposition: spark_sanctions_disposition(), + export_disposition: spark_export_disposition(), + } +} + +// POSITIVE CONTROL. The first-party scope admits, and the permit carries the route and posture it +// was admitted under rather than merely existing. +test fn the_first_party_scope_admits_and_the_permit_names_its_posture() -> Bool { + match spark_first_party_admission( + scope: spark_first_party_use_scope(demand: t_demand(), work: t_work()), + offer: t_offer(), + ) { + ProviderUseDenied { decision: _, cause: _ } => false + ProviderUseAdmitted { permit: p } => + declaration_ref_eq(a: p.route.region, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_fleet_site_allocation")) + && declaration_ref_eq(a: p.posture.authority, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture")) + } +} + +// THE STOP CONDITION, EXECUTED. The three programs are recorded as CLEARED because +// admit_provider_use requires that to mint, and the danger is that a reader takes them for +// determinations somebody made. This row asserts what the permit actually carries: each evidence +// reference names the declaration stating the program is NOT ENGAGED under first-party self-use. +// If anyone later swaps one for a clearance row, this goes red. +test fn every_use_program_evidence_names_the_not_engaged_declaration() -> Bool { + match spark_first_party_admission( + scope: spark_first_party_use_scope(demand: t_demand(), work: t_work()), + offer: t_offer(), + ) { + ProviderUseDenied { decision: _, cause: _ } => false + ProviderUseAdmitted { permit: p } => + count(filter(p.evidence.sanctions_evidence, e => + declaration_ref_eq(a: e, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_sanctions_not_engaged")))) == 1 + && count(filter(p.evidence.export_evidence, e => + declaration_ref_eq(a: e, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_export_not_engaged")))) == 1 + && count(filter(p.evidence.prohibited_use_evidence, e => + declaration_ref_eq(a: e, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_prohibited_use_not_engaged")))) == 1 + } +} + +// THE ARM IS READ THROUGH refusal_reason, WHICH IS THE MODULE'S OWN EXHAUSTIVE DERIVATION, rather +// than through a ten-arm match copied into this file. A second copy of that match is the same +// coproduct restated in a test, and it rots the day an arm is added; refusal_reason is derived from +// the cause by an exhaustive match in the module that owns it, so a new arm forces an edit there. +// What it costs is the payload -- these rows assert WHICH arm refused, not what it carried -- and +// that is enough here, because each red below differs from the admitted control in exactly one +// input, so no other arm can produce it. + +// RED -- "IT IS JUST SERVING US FOR NOW" IS ENFORCED BY EXECUTION. A use whose customer is anybody +// but us reaches the same producer and is refused, and the refusal names the unsupported profile so +// the remedy is the right one: get that profile sanctioned under a posture, not widen this one. +test fn a_non_first_party_use_refuses_as_unsupported() -> Bool { + match spark_first_party_admission(scope: t_third_party_scope(), offer: t_offer()) { + ProviderUseAdmitted { permit: _ } => false + ProviderUseDenied { decision: _, cause: c } => refusal_reason(c: c) == "customer scope unsupported" + } +} + +// RED -- RE-POSTURING MAKES THE STANDING SANCTION STALE RATHER THAN CARRYING IT OVER. This is the +// other half of "for now": the sanction roster is bound to the 2026-09-11 first-party revision, so +// evaluating the SAME first-party use under a later active posture refuses. It calls +// admit_provider_use directly with our own roster and facts, because the producer above pins the +// active posture by design -- the thing under test is the roster's binding, not the pin. +fn t_later_posture() -> CompliancePostureRevision { + CompliancePostureRevision { + authority: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture"), + revision: as_content_hash_structural(structural: content_hash_atom(value: "gunbc.spark.serving-someone-else.later" as NonEmptyStr)), + } +} + +test fn a_superseded_posture_makes_the_first_party_sanction_stale() -> Bool { + match admit_provider_use( + roster: spark_first_party_sanction_roster(), + facts: spark_first_party_route_facts(), + active: t_later_posture(), + scope: spark_first_party_use_scope(demand: t_demand(), work: t_work()), + offer: t_offer(), + decision_receipt: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture"), + ) { + ProviderUseAdmitted { permit: _ } => false + ProviderUseDenied { decision: _, cause: c } => refusal_reason(c: c) == "posture stale" + } +} diff --git a/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag b/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag index 804de093fa8..acbd528ed44 100644 --- a/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag +++ b/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag @@ -1,7 +1,7 @@ module test.claim.spark.spark_serving_offer_route_witness_test import std.types { Bool, NonEmptyStr, String } -import std.decl_ref { decl_ref } +import std.decl_ref { decl_ref, declaration_ref_eq } import product.fabric.provider_route { ProviderRoute } import product.fabric.identity { FabricIdentity } import product.fabric.isolation { IsolationProfile } @@ -14,7 +14,7 @@ import gunbc.spark.vllm_endpoint_process_launch { import gunbc.spark.serving_offer { SparkOfferBinding, SparkOfferBound, SparkOfferBindingRefused, SparkServingReadiness, ServingObserved, - SparkServingRoute, ServingRouteObserved, ServingRouteRegionUnobserved, + SparkServingRoute, ServingRouteObserved, ServingRouteOperatorAsserted, ServingRouteRegionUnobserved, spark_serving_route_standing, spark_serving_route_region_obligation, bind_spark_serving_offer, } @@ -85,15 +85,26 @@ test fn an_unobserved_region_refuses_naming_its_obligation() -> Bool { } } -// THE STANDING THE PRODUCTION CALLER ACTUALLY PASSES IS THE UNOBSERVED ONE. This is what makes the -// two rows above statements about the live path rather than about a fixture: harness_seat calls -// spark_serving_route_standing, and it refuses. When a region observer lands, this row goes red and -// must be replaced by one asserting the observed route -- that is the restoration trigger firing, -// not a change detector, because the arm it selects is different code. -test fn the_standing_the_harness_passes_is_unobserved_today() -> Bool { +// THE STANDING THE PRODUCTION CALLER ACTUALLY PASSES, AND THIS ROW HAS FLIPPED (DESIGN 4b(4)). It +// used to assert the refusal and predicted its own red: "when a region observer lands, this row goes +// red and must be replaced by one asserting the observed route". The trigger fired on 2026-09-11 +// through the arm nobody predicted -- not an observer, but the operator's dated assertion of where +// the units sit, which for hardware he owns and holds is the only kind of fact available. So the row +// is replaced rather than deleted, and it is now the permanent regression control that the live path +// carries a route. +// +// IT ASSERTS THE ASSERTED ARM SPECIFICALLY, and that is the point of the assertion rather than a +// detail of it: a standing that came back as ServingRouteObserved would mean an allocation had been +// relabelled as a measurement, which is precisely what the third arm exists to make unwritable. The +// region it carries must be the allocation, because a region citing the bare site row would name a +// place while dropping who said the units are there and when. +test fn the_standing_the_harness_passes_is_operator_asserted_with_its_allocation() -> Bool { match spark_serving_route_standing() { + ServingRouteRegionUnobserved { obligation: _ } => false ServingRouteObserved { route: _ } => false - ServingRouteRegionUnobserved { obligation: o } => - (o as String) == (spark_serving_route_region_obligation as String) + ServingRouteOperatorAsserted { route: r, allocation: a } => + declaration_ref_eq(a: r.region, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_fleet_site_allocation")) + && declaration_ref_eq(a: r.provider, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "gunbc_first_party_serving_provider")) + && (a.decided_on as String) == "2026-09-11" } } From 992fa0667a62f94ceaf2c060839bd3a00ea36105 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 19:33:02 +0000 Subject: [PATCH 02/11] Review 63981: a not-engaged program is not a clearance, so it gets its own arm The first spelling of gunbc.spark.first_party_serving minted DispositionCleared for three programs the same diff states were never run, and carried the honesty in prose fields nothing matches on. Review 63981 is right: prose cannot discharge a machine claim (DESIGN 4c), the value "cleared" then meant two materially different things at once (DESIGN 3), and the witness compared a DeclarationRef, so editing the cited row into a real clearance would have left it green. The remedy is upstream, where the fork is. product.fabric.provider_admission DispositionStanding grows DispositionNotEngaged { basis }: the ProviderPathAbsent / ProviderPathUnread move applied to dispositions. It ADMITS, like a clearance, and it is not one, so "a program resolved in our favour" and "a program has no subject on this route" are told apart by matching rather than by reading a string. ProviderUseEvidence now records the STANDING rather than a projection of it, so a permit says WHICH of the two admitting arms admitted it; disposition_evidence dissolves with the question it existed to answer (DESIGN 4b(4)) and the witness that read its output flips to matching the arm. Both witnesses assert the arm now, so a swap to a clearance is red in the spark witness and a swap to not-engaged is red in the fabric one. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- .../product/fabric/provider_admission.dag | 65 ++++++++++++------- dag/gunbc/spark/first_party_serving.dag | 48 +++++++------- .../provider_admission_witness_test.dag | 31 ++++++--- ...spark_first_party_serving_witness_test.dag | 34 ++++++---- 4 files changed, 112 insertions(+), 66 deletions(-) diff --git a/dag/gunbc/product/fabric/provider_admission.dag b/dag/gunbc/product/fabric/provider_admission.dag index 8253d0d467f..c1b7a0ac2ea 100644 --- a/dag/gunbc/product/fabric/provider_admission.dag +++ b/dag/gunbc/product/fabric/provider_admission.dag @@ -71,8 +71,29 @@ import product.fabric.provider_route { // decision anything at all and it would neither read it nor record it - dangling inputs on the // subject of the decision (DESIGN section 3c), and worse, an unresolved sanctions case would have // been indistinguishable from a cleared one. A standing has to say which it is. +// THE FOURTH ARM IS "THE PROGRAM HAS NO SUBJECT HERE", AND IT IS A DIFFERENT CLAIM FROM CLEARED. +// The distinction is the one product.fabric.provider_route already draws one type over, in the same +// vocabulary and for the same reason: ProviderPathAbsent (a fact that can support an admission) is +// kept apart from ProviderPathUnread (an obligation that must refuse), because collapsing them is +// how an unexamined path reads as a clean one. Cleared and NotEngaged are the two ADMITTING +// standings and they are equally not each other -- Cleared says a program ran and resolved in our +// favour, NotEngaged says the program has no subject on this route at all, which is the honest +// standing for a route with no counterparty, no transfer and no recipient. +// +// WITHOUT THIS ARM THE ONLY WAY TO ADMIT SUCH A ROUTE WAS TO WRITE A CLEARANCE NOBODY ISSUED, which +// is the fabricated legal finding this gate exists to close, arriving through the gate itself. It +// was written that way once, in gunbc.spark.first_party_serving, with the honesty carried in prose +// fields nothing matches on -- and prose cannot discharge a machine claim (DESIGN 4c), which is +// exactly review 63981's finding. With the arm, a not-engaged standing is expressible AS ITSELF, a +// future real clearance is distinguishable from it BY MATCHING rather than by reading a string, and +// a permit records which of the two admitted it. +// +// WHAT THE ARM DOES NOT DO. It does not establish that a program genuinely has no subject; that +// stays a boundary obligation on whoever writes the basis, exactly as the honesty of a clearance +// stays with whoever issued it. What it buys is that the two claims stop being one value. type DispositionStanding = DispositionCleared { evidence: DeclarationRef } + | DispositionNotEngaged { basis: DeclarationRef } | DispositionRefused { cause: DeclarationRef } | DispositionUnresolved { obligation: DeclarationRef } @@ -84,23 +105,20 @@ type DispositionStanding fn disposition_obligation(d: DispositionStanding) -> List { match d { DispositionCleared { evidence } => [], + DispositionNotEngaged { basis } => [], DispositionRefused { cause } => [cause], DispositionUnresolved { obligation } => [obligation], } } -// The cleared evidence, as zero-or-one, for the same reason. This was an evidence_or with a -// fallback, and although the fallback sat on the admitted path where all three dispositions are -// cleared by the gate above, an unreachable value that names a customer profile where a clearance -// evidence belongs is still a lie waiting for the guard to move. A list cannot lie: on the -// admitted path it is exactly one element by construction, and empty is unproducible there. -fn disposition_evidence(d: DispositionStanding) -> List { - match d { - DispositionCleared { evidence } => [evidence], - DispositionRefused { cause } => [], - DispositionUnresolved { obligation } => [], - } -} +// disposition_evidence IS GONE, AND ITS DISSOLUTION IS THE CLIMB RATHER THAN A DELETION (DESIGN +// 4b(4)). It projected a zero-or-one DeclarationRef out of the standing so the permit could record +// "what the gate saw" without a fabricable seed, and the list shape was the right answer to that +// question. The question stops existing once the permit records the STANDING ITSELF: a reference +// alone cannot say which arm admitted the route, so two materially different admissions -- a +// clearance and a not-engaged -- reached ProviderUseEvidence as the same shape and an auditor +// reading a permit could not tell them apart. Carrying the standing is one value, not two +// representations of one, and it cannot lose the arm on the way. // OUR ROSTER, NOT THE SUPPLIER'S. gunbc.fabric_executor_class already establishes the shape: we // keep the sanction, an unclassified executor refuses, and the sanction is evaluated before @@ -140,18 +158,21 @@ type ProviderUseScope

{ // Folding them into one scope would give the partition a single refused population and lose which // of the two a caller must go fix. -// Every revision and clearance the decision actually read, recorded on the permit. This is what -// makes a permit re-derivable rather than merely historical. The three disposition evidences are -// here because a permit that gated on them and did not record them would be unauditable - the -// gate would have run and left no trace of what it saw. +// Every revision and standing the decision actually read, recorded on the permit. This is what +// makes a permit re-derivable rather than merely historical. The three dispositions are here +// because a permit that gated on them and did not record them would be unauditable - the gate would +// have run and left no trace of what it saw - and they are the STANDINGS rather than projections of +// them, so a permit says whether each program was cleared or had no subject. Only the two admitting +// arms are reachable here: a refused or unresolved standing cannot pass the gate above, and this +// type does not restate that, because restating it would be a second representation of the gate. type ProviderUseEvidence { posture_revision: ContentHash route_facts_revision: ContentHash customer_profile: DeclarationRef agreement: DeclarationRef - prohibited_use_evidence: List - sanctions_evidence: List - export_evidence: List + prohibited_use_standing: DispositionStanding + sanctions_standing: DispositionStanding + export_standing: DispositionStanding decision_receipt: DeclarationRef } @@ -452,9 +473,9 @@ fn admit_provider_use

( route_facts_revision: facts.facts_revision, customer_profile: scope.customer_profile, agreement: scope.agreement, - prohibited_use_evidence: disposition_evidence(d: scope.prohibited_use_disposition), - sanctions_evidence: disposition_evidence(d: scope.sanctions_disposition), - export_evidence: disposition_evidence(d: scope.export_disposition), + prohibited_use_standing: scope.prohibited_use_disposition, + sanctions_standing: scope.sanctions_disposition, + export_standing: scope.export_disposition, decision_receipt: decision_receipt, }, }, diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 20867f6aab3..41945f83ae3 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -12,7 +12,7 @@ import product.fabric.provider_route { } import product.fabric.provider_admission { RouteScopeSanction, ProviderUseScope, ProviderUseAdmission, - DispositionStanding, DispositionCleared, admit_provider_use, + DispositionStanding, DispositionNotEngaged, admit_provider_use, } import gunbc.spark.dgx_procurement { OperatorAllocation } import gunbc.fleet_physical_inventory { operator_site } @@ -189,23 +189,27 @@ data spark_operator_owned_hardware_agreement: FirstPartyUseProfile = FirstPartyU basis: "The agreement authority for this route is the operator's ownership of the hardware. There is no third-party contract to present because there is no third party; this row is what the scope names so that an agreement is a cited authority rather than an empty field.", } -// ── THE THREE USE PROGRAMS, AND WHY EACH READS 'NOT ENGAGED' RATHER THAN 'CLEARED' ──────────── +// ── THE THREE USE PROGRAMS, AND WHY EACH IS 'NOT ENGAGED' RATHER THAN 'CLEARED' ─────────────── // -// This is the point the whole wall exists to protect, so it is stated in the VALUES and not only -// here. admit_provider_use requires the prohibited-use, sanctions and export dispositions to be -// DispositionCleared before a permit mints, and the tempting way to satisfy that is to write three -// clearances -- which would be fabricated legal findings, the fail-open this gate closes. Nobody has -// run a screening, no determination has been made, and none is claimed. +// This is the point the whole wall exists to protect. admit_provider_use requires the +// prohibited-use, sanctions and export dispositions to ADMIT before a permit mints, and the +// tempting way to satisfy that is to write three clearances -- which would be fabricated legal +// findings, the fail-open this gate closes. Nobody has run a screening, no determination has been +// made, and none is claimed. // -// WHAT IS ACTUALLY TRUE is narrower and is what each row below says: under first-party self-use -// these programs have NO SUBJECT. Nothing is supplied to any party, nothing is exported, and nothing -// crosses a border, because the turn begins and ends inside gunbc on hardware gunbc's operator owns -// at a site in the operator's own home. The evidence each disposition carries is THIS POSTURE -// DECLARATION and nothing else, so a reader following the reference arrives at the statement "not -// engaged, because first-party self-use" rather than at a clearance somebody appears to have issued. -// The moment the posture changes -- the moment a turn is served to anyone else -- these rows stop -// describing the route, which is why they cite the posture that goes stale rather than standing on -// their own. +// AND THE FIRST SPELLING OF THIS MODULE TOOK EXACTLY THAT BAIT, which is why the remedy is upstream +// rather than in a longer comment here. It wrote DispositionCleared and carried the honesty in +// prose fields nothing matches on -- review 63981 is right that this differs from the fabricated +// version only in prose, and that prose cannot discharge a machine claim (DESIGN 4c). The fix is +// product.fabric.provider_admission's new DispositionNotEngaged arm, the ProviderPathAbsent / +// ProviderPathUnread move applied to dispositions: it ADMITS, like a clearance, and it is not one, +// so the two are told apart by matching. +// +// WHAT IS ACTUALLY TRUE is what each row below says: under first-party self-use these programs have +// NO SUBJECT. Nothing is supplied to any party, nothing is exported, and nothing crosses a border, +// because the turn begins and ends inside gunbc on hardware the operator owns at his own site. The +// basis each disposition carries is the row stating that, and the moment the posture changes -- the +// moment a turn is served to anyone else -- these rows stop describing the route. type UseProgramStanding { program: NonEmptyStr engagement: NonEmptyStr @@ -231,20 +235,20 @@ data spark_export_not_engaged: UseProgramStanding = UseProgramStanding { } fn spark_prohibited_use_disposition() -> DispositionStanding { - DispositionCleared { - evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_prohibited_use_not_engaged"), + DispositionNotEngaged { + basis: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_prohibited_use_not_engaged"), } } fn spark_sanctions_disposition() -> DispositionStanding { - DispositionCleared { - evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_sanctions_not_engaged"), + DispositionNotEngaged { + basis: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_sanctions_not_engaged"), } } fn spark_export_disposition() -> DispositionStanding { - DispositionCleared { - evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_export_not_engaged"), + DispositionNotEngaged { + basis: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_export_not_engaged"), } } diff --git a/dag/test/claim/fabric/provider_admission_witness_test.dag b/dag/test/claim/fabric/provider_admission_witness_test.dag index ac0c259ba1c..b4392c4e1c5 100644 --- a/dag/test/claim/fabric/provider_admission_witness_test.dag +++ b/dag/test/claim/fabric/provider_admission_witness_test.dag @@ -17,7 +17,7 @@ import product.fabric.provider_admission { ProviderRouteUnclassified, ProviderRouteFactsIncomplete, DownstreamProviderUnassessed, PostureRevisionStale, CustomerScopeUnsupported, DataHandlingUnsupported, RequiredAgreementAuthorityAbsent, ProhibitedUseNotCleared, SanctionsNotCleared, ExportNotCleared, - DispositionStanding, DispositionCleared, DispositionRefused, DispositionUnresolved, + DispositionStanding, DispositionCleared, DispositionNotEngaged, DispositionRefused, DispositionUnresolved, admit_provider_use, } @@ -533,9 +533,23 @@ test fn w_closure_extractors_discriminate() -> Bool { // RED - the permit RECORDS the clearance evidence it gated on. The three evidences were once // extracted with a fallback that substituted the customer profile when a disposition was not // cleared; the fallback sat on a path the gate made unreachable, but an unreachable value naming -// the wrong kind of thing is a lie waiting for the guard to move. As zero-or-one lists there is -// nothing to substitute, and this asserts the admitted arm carries exactly one of each rather -// than an empty audit trail. +// the wrong kind of thing is a lie waiting for the guard to move. +// +// THE PERMIT NOW RECORDS THE STANDING RATHER THAN A PROJECTION OF IT, so this row asserts the ARM +// as well as the reference. That is the discriminating half: with four arms and two of them +// admitting, a permit that recorded only a DeclarationRef could not say whether a program was +// CLEARED or had NO SUBJECT, and those are materially different admissions. +// A NOT-ENGAGED STANDING FAILS THIS, WHICH IS THE POINT: the arm is matched, not merely the +// reference read out of whichever arm happened to carry one. +fn w_cleared_with(d: DispositionStanding, expected: DeclarationRef) -> Bool { + match d { + DispositionCleared { evidence } => declaration_ref_eq(a: evidence, b: expected), + DispositionNotEngaged { basis } => false, + DispositionRefused { cause } => false, + DispositionUnresolved { obligation } => false, + } +} + test fn w_permit_records_its_clearances() -> Bool { match decide( route: route_of(region: decl_ref(module_path: "test.claim.fabric.provider_admission_witness", decl_name: "region_one")), @@ -546,11 +560,8 @@ test fn w_permit_records_its_clearances() -> Bool { ) { ProviderUseDenied { decision, cause } => false, ProviderUseAdmitted { permit } => - count(filter(permit.evidence.prohibited_use_evidence, - r => declaration_ref_eq(a: r, b: decl_ref(module_path: "test.claim.fabric.provider_admission_witness", decl_name: "prohibited_use_cleared")))) == 1 - && count(filter(permit.evidence.sanctions_evidence, - r => declaration_ref_eq(a: r, b: decl_ref(module_path: "test.claim.fabric.provider_admission_witness", decl_name: "sanctions_cleared")))) == 1 - && count(filter(permit.evidence.export_evidence, - r => declaration_ref_eq(a: r, b: decl_ref(module_path: "test.claim.fabric.provider_admission_witness", decl_name: "export_cleared")))) == 1, + w_cleared_with(d: permit.evidence.prohibited_use_standing, expected: decl_ref(module_path: "test.claim.fabric.provider_admission_witness", decl_name: "prohibited_use_cleared")) + && w_cleared_with(d: permit.evidence.sanctions_standing, expected: decl_ref(module_path: "test.claim.fabric.provider_admission_witness", decl_name: "sanctions_cleared")) + && w_cleared_with(d: permit.evidence.export_standing, expected: decl_ref(module_path: "test.claim.fabric.provider_admission_witness", decl_name: "export_cleared")), } } diff --git a/dag/test/claim/spark/spark_first_party_serving_witness_test.dag b/dag/test/claim/spark/spark_first_party_serving_witness_test.dag index aa0258ea11a..46a217d67c6 100644 --- a/dag/test/claim/spark/spark_first_party_serving_witness_test.dag +++ b/dag/test/claim/spark/spark_first_party_serving_witness_test.dag @@ -7,6 +7,8 @@ import product.fabric.identity { FabricIdentity, DemandKey, WorkKey, OfferKey } import product.fabric.provider_route { CompliancePostureRevision } import product.fabric.provider_admission { ProviderUseScope, ProviderUseAdmission, ProviderUseAdmitted, ProviderUseDenied, + DispositionStanding, DispositionCleared, DispositionNotEngaged, + DispositionRefused, DispositionUnresolved, refusal_reason, admit_provider_use, } import gunbc.spark.first_party_serving { @@ -67,24 +69,32 @@ test fn the_first_party_scope_admits_and_the_permit_names_its_posture() -> Bool } } -// THE STOP CONDITION, EXECUTED. The three programs are recorded as CLEARED because -// admit_provider_use requires that to mint, and the danger is that a reader takes them for -// determinations somebody made. This row asserts what the permit actually carries: each evidence -// reference names the declaration stating the program is NOT ENGAGED under first-party self-use. -// If anyone later swaps one for a clearance row, this goes red. -test fn every_use_program_evidence_names_the_not_engaged_declaration() -> Bool { +// THE STOP CONDITION, EXECUTED, AND IT ASSERTS THE ARM RATHER THAN THE REFERENCE. Review 63981 is +// right about why that distinction is the whole test: a row comparing only a DeclarationRef says +// which declaration was cited, not what was CLAIMED, so editing the cited row's text into a real +// clearance would leave it green. Matching DispositionNotEngaged cannot be satisfied that way -- +// a permit admitted on a clearance takes the other arm and this goes red -- which is what makes it +// a wall rather than a name check. +fn t_not_engaged_naming(d: DispositionStanding, basis_decl: NonEmptyStr) -> Bool { + match d { + DispositionNotEngaged { basis: b } => + declaration_ref_eq(a: b, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: basis_decl as String)) + DispositionCleared { evidence: _ } => false + DispositionRefused { cause: _ } => false + DispositionUnresolved { obligation: _ } => false + } +} + +test fn every_use_program_is_not_engaged_and_names_its_basis() -> Bool { match spark_first_party_admission( scope: spark_first_party_use_scope(demand: t_demand(), work: t_work()), offer: t_offer(), ) { ProviderUseDenied { decision: _, cause: _ } => false ProviderUseAdmitted { permit: p } => - count(filter(p.evidence.sanctions_evidence, e => - declaration_ref_eq(a: e, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_sanctions_not_engaged")))) == 1 - && count(filter(p.evidence.export_evidence, e => - declaration_ref_eq(a: e, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_export_not_engaged")))) == 1 - && count(filter(p.evidence.prohibited_use_evidence, e => - declaration_ref_eq(a: e, b: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_prohibited_use_not_engaged")))) == 1 + t_not_engaged_naming(d: p.evidence.sanctions_standing, basis_decl: "spark_sanctions_not_engaged" as NonEmptyStr) + && t_not_engaged_naming(d: p.evidence.export_standing, basis_decl: "spark_export_not_engaged" as NonEmptyStr) + && t_not_engaged_naming(d: p.evidence.prohibited_use_standing, basis_decl: "spark_prohibited_use_not_engaged" as NonEmptyStr) } } From 98d3ce6e107a2251dc0ca87b7680a89c38756401 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 19:35:37 +0000 Subject: [PATCH 03/11] Telemetry is the one path that leaves the site, so it stops citing the site Review 63981's corroborating finding was that nine identical Located paths from one assertion is not "each path answers for itself". Eight of them it does answer: the box is at the operator's site and nobody else has access, so that is where execution, durable storage, backups, logs, spill, control plane, support and administrative access terminate. TELEMETRY IT DOES NOT ANSWER, and this is worse than the review guessed. vLLM reports usage statistics to https://stats.vllm.ai unless a launch disables it, and gunbc.spark.pair_serving_realization's container environment sets neither VLLM_NO_USAGE_STATS nor DO_NOT_TRACK. The previous spelling wrote the operator's site into that slot, which is false about the one path that demonstrably leaves it -- and false in the direction that reads as clean. So the path is recorded with its real destination. extdeps.vllm.usage_stats carries the documented payload at the same source revision the running engine names (1967a5627bc3, already cited by extdeps.vllm.server): the field roster, the default server, the override and opt-out environment variables, the marker file, and a TYPED content class -- configuration and hardware metadata, no request content, prompts or completions, which upstream states explicitly. That class is what lets the path admit instead of refuse: the closure governs paths reaching the route's MATERIAL, and this one carries none (operator ruling, 2026-09-11). The jurisdiction slot cites the FIELD holding ServiceJurisdictionUndocumentedUpstream rather than naming a place upstream does not document. What that costs is stated where it is paid: ProviderPathLocated cannot express "located at a party whose jurisdiction is unread", and the next-rung trigger is a jurisdiction standing on ProviderPathStanding sufficient for a located path to say so without the whole path becoming unread. The posture row now says what holds and what leaves: route material stays on site, one metadata-only path reaches vLLM upstream by default, and the remedy for zero egress is one environment variable on a box the operator owns -- named rather than blocked on. Also: observed_at is annotated as the assertion's date at date grain, so the midnight is not read as a moment anybody measured. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/extdeps/vllm/usage_stats.dag | 122 ++++++++++++++++++++++++ dag/gunbc/spark/first_party_serving.dag | 69 ++++++++++++-- 2 files changed, 181 insertions(+), 10 deletions(-) create mode 100644 dag/extdeps/vllm/usage_stats.dag diff --git a/dag/extdeps/vllm/usage_stats.dag b/dag/extdeps/vllm/usage_stats.dag new file mode 100644 index 00000000000..f81bee167e0 --- /dev/null +++ b/dag/extdeps/vllm/usage_stats.dag @@ -0,0 +1,122 @@ +module extdeps.vllm.usage_stats + +import std.types { NonEmptyStr, List } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +import extdeps.vllm.server { VllmSourceRevision, vllm_source_revision_read } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "docs.vllm.ai/en/latest/usage/usage_stats.html" + } +} + +data vllm_usage_stats_source_citation: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/vllm-project/vllm/blob/main/vllm/usage/usage_lib.py" + } +} + +data vllm_usage_stats_server_default_citation: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/vllm-project/vllm/blob/main/vllm/envs.py" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.vllm.usage_stats", + decl_name: "VllmUsageStatsReporting", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [vllm_usage_stats_source_citation, vllm_usage_stats_server_default_citation] +} + +// ── THE ONE THING A vLLM SERVER SENDS OFF THE BOX BY DEFAULT ────────────────────────────────── +// +// WHY THIS MODULE EXISTS. Every other fact about our serving route says the material stays where +// the machine is. This is the exception, and it is an exception nobody in this repository had +// written down: vLLM reports usage statistics to an upstream service unless it is switched off, and +// nothing on the Spark serving launch switches it off. A data-path closure that answered "the +// operator's site" for telemetry would have been false about the one path that demonstrably leaves +// it -- and false in the direction that reads as clean. +// +// WHAT IT IS NOT. It is not a leak of route material. The documented payload is configuration and +// hardware metadata; upstream is explicit that request content, prompts and completions are not +// collected, and the field roster below carries no field derived from a request. That distinction +// is the whole reason a consumer can admit this path rather than refuse it, so it is modelled as a +// TYPED CONTENT CLASS rather than asserted in a sentence. +// +// REVISION-BOUND, like every other reading of this upstream. The roster is what upstream documents +// at the cited revision; a later revision that adds a field is a different fact, and the binding to +// vllm_source_revision_read is what makes that decidable instead of a surprise. + +// THE TWO CLASSES ARE SEPARATE BECAUSE THEY AUTHORIZE DIFFERENT THINGS. A metadata-only egress can +// support an admission for a route whose material stays home; an egress carrying any request +// material cannot, and would have to refuse rather than be argued about. There is deliberately no +// "probably fine" arm. +type VllmUsageStatsContentClass + = ConfigurationAndHardwareMetadataOnly + | CarriesRequestMaterial + +// THE DESTINATION IS A THIRD PARTY, AND ITS JURISDICTION IS NOT DOCUMENTED. Upstream publishes the +// default server and nothing about who operates it or under which legal system, so the jurisdiction +// is an UNREAD upstream fact rather than one this module may supply. It is a typed arm rather than +// a missing field for the reason this whole repository keeps repeating: an absent jurisdiction and +// a jurisdiction nobody looked up must not be the same value, and a consumer that needs one must be +// able to see that it does not exist here. +type VllmUsageStatsServiceJurisdiction + = ServiceJurisdictionDocumented { jurisdiction: NonEmptyStr } + | ServiceJurisdictionUndocumentedUpstream + +type VllmUsageStatsReporting sole_constructor { + default_server: NonEmptyStr + server_override_env: NonEmptyStr + local_copy_path: NonEmptyStr + content_class: VllmUsageStatsContentClass + service_jurisdiction: VllmUsageStatsServiceJurisdiction + collected_fields: List + disable_env_vars: List + disable_marker_path: NonEmptyStr + established_against: VllmSourceRevision +} + +// THE ROSTER IS THE DOCUMENTED EXAMPLE PAYLOAD, transcribed as the field NAMES upstream publishes. +// Every one of them is a property of the host, the build or the engine configuration; none is +// derived from a request, which is what the content class above records and what a reader can check +// here rather than take on faith. +data vllm_usage_stats_reporting: VllmUsageStatsReporting = VllmUsageStatsReporting { + default_server: "https://stats.vllm.ai", + server_override_env: "VLLM_USAGE_STATS_SERVER", + local_copy_path: "~/.config/vllm/usage_stats.json", + content_class: ConfigurationAndHardwareMetadataOnly, + service_jurisdiction: ServiceJurisdictionUndocumentedUpstream, + collected_fields: [ + "uuid", "provider", "num_cpu", "cpu_type", "cpu_family_model_stepping", + "total_memory", "architecture", "platform", "gpu_count", "gpu_type", + "gpu_memory_per_device", "model_architecture", "vllm_version", "context", + "log_time", "source", "dtype", "tensor_parallel_size", "block_size", + "gpu_memory_utilization", "quantization", "kv_cache_dtype", "enable_lora", + "enable_prefix_caching", "enforce_eager", "disable_custom_all_reduce", + ], + disable_env_vars: ["VLLM_NO_USAGE_STATS", "DO_NOT_TRACK"], + disable_marker_path: "~/.config/vllm/do_not_track", + established_against: vllm_source_revision_read, +} + +// REPORTING IS ON UNLESS SOMETHING TURNS IT OFF, which is the shape of the upstream check +// (_USAGE_STATS_ENABLED = not (do_not_track or no_usage_stats or do_not_track_file)) and therefore +// the shape of the question a consumer must ask about a particular launch. The arms are what a +// launch's configuration can establish, and the unread arm exists because reading a running host's +// environment is an observation this module cannot make. +type VllmUsageStatsLaunchStanding + = UsageStatsDisabledByLaunch { mechanism: NonEmptyStr } + | UsageStatsEnabledByDefault { basis: NonEmptyStr } + | UsageStatsLaunchUnread { obligation: NonEmptyStr } diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 41945f83ae3..13e377e528f 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -1,7 +1,7 @@ module gunbc.spark.first_party_serving import std.types { NonEmptyStr, List } -import std.decl_ref { DeclarationRef, decl_ref } +import std.decl_ref { DeclarationRef, decl_ref, decl_field_ref } import std.content_hash { as_content_hash_structural, content_hash_atom } import product.placement_supply { SiteIdentity, HostIdentity } import product.fabric.identity { FabricIdentity, DemandKey, WorkKey, OfferKey } @@ -14,6 +14,9 @@ import product.fabric.provider_admission { RouteScopeSanction, ProviderUseScope, ProviderUseAdmission, DispositionStanding, DispositionNotEngaged, admit_provider_use, } +import extdeps.vllm.usage_stats { + VllmUsageStatsLaunchStanding, UsageStatsEnabledByDefault, +} import gunbc.spark.dgx_procurement { OperatorAllocation } import gunbc.fleet_physical_inventory { operator_site } import gunbc.fleet_intent_network { @@ -149,7 +152,7 @@ data spark_first_party_use_posture: FirstPartySelfUsePosture = FirstPartySelfUse basis: "The operator asserts that the Spark serving groups serve gunbc itself and nobody else as of this date. Attributable assertion, not a measurement: who the served turns are for is a fact about our intent, which no probe can read off a running engine.", }, serves: "gunbc itself. Every turn placed on this route originates inside this repository's own harness and control plane; no turn is served to any party outside gunbc and none crosses an organisational or national boundary.", - data_subject: "our own material. The prompts and responses on this route are gunbc's, held on operator-owned hardware at the operator's own site; no customer data and no third-party data is processed on it.", + data_subject: "our own material. The prompts and responses on this route are gunbc's, held on operator-owned hardware at the operator's own site; no customer data and no third-party data is processed on it. ROUTE MATERIAL STAYS ON SITE AND EXACTLY ONE PATH LEAVES IT: vLLM reports host, build and engine-configuration metadata to https://stats.vllm.ai by upstream default, carrying no request content (extdeps.vllm.usage_stats, and gunbc.spark.first_party_serving spark_serving_usage_stats_standing for this fleet's launch). The remedy for zero egress is VLLM_NO_USAGE_STATS=1 or DO_NOT_TRACK=1 on the serving launch, which is the operator's to set on his own box.", hardware_custody: "operator-owned and operator-held. There is no third-party agreement governing this route because there is no third party: no hosting contract, no processor, and no service terms stand between us and the hardware.", staleness_condition: "SERVING ANYONE ELSE ENDS THIS POSTURE. A turn served to a party outside gunbc, or any third-party material processed on this route, is a materially different contract subject and requires a NEW CompliancePostureRevision; every RouteScopeSanction below is bound to THIS revision, so it goes stale through product.fabric.provider_admission PostureRevisionStale rather than silently carrying over. Nothing here may be widened to cover another customer profile by adding a roster row under this revision.", } @@ -271,17 +274,24 @@ fn spark_first_party_sanction_roster() -> List { ] } -// ── THE ROUTE FACTS: NINE PATHS, ALL LOCATED, NONE ABSENT ───────────────────────────────────── +// ── THE ROUTE FACTS: EIGHT PATHS AT THE SITE, AND ONE THAT LEAVES IT ────────────────────────── // -// EVERY PATH IS LOCATED AT THE SAME SITE BY THE SAME ASSERTION, and no path is claimed ABSENT. The -// tempting shortcut is to write backups or spill as ProviderPathAbsent -- "we do not back the +// EIGHT PATHS ARE LOCATED AT THE SAME SITE BY THE SAME ASSERTION, and no path is claimed ABSENT. +// The tempting shortcut is to write backups or spill as ProviderPathAbsent -- "we do not back the // serving host up" -- and that would be a claim about our own machines that nobody has made and no // probe has read. What the operator's assertion DOES establish is location: whatever these paths // are, they terminate on operator-owned hardware at the operator's own site, because there is no -// other estate for them to reach. So every path takes the located arm, with the site allocation as -// its jurisdiction and the posture as its evidence, and the honest weakness of the row is that its -// operator and jurisdiction are an allocation rather than a measurement -- which is the same stated -// divergence the route itself carries, not a second one. +// other estate for them to reach. So they take the located arm, with the site allocation as the +// jurisdiction and the posture as the evidence, and the honest weakness is that both rest on an +// allocation rather than a measurement -- the same stated divergence the route carries, not a +// second one. +// +// TELEMETRY IS NOT ONE OF THE EIGHT, AND THAT IS REVIEW 63981's CORROBORATING FINDING TAKEN +// SERIOUSLY RATHER THAN ABSORBED. "Each path answers for itself", and one assertion about where a +// box sits cannot answer for a path that LEAVES the box: vLLM reports usage statistics to +// https://stats.vllm.ai unless a launch disables it, and nothing on this serving launch does. +// Writing the site into that slot would have been the exact failure the closure exists to catch -- +// an unexamined egress reading as a clean one -- so it is recorded below with its real destination. fn spark_first_party_path() -> ProviderPathStanding { ProviderPathLocated { operator: spark_first_party_provider_ref(), @@ -300,6 +310,45 @@ fn spark_first_party_downstream() -> DownstreamProviderPopulation { } } +// ── THE ONE PATH THAT LEAVES THE SITE, RECORDED WITH ITS REAL DESTINATION ───────────────────── +// +// WHY IT ADMITS RATHER THAN REFUSES, ruled by the operator 2026-09-11. The closure governs the +// paths that reach the ROUTE'S MATERIAL. This one does not: extdeps.vllm.usage_stats carries the +// documented payload -- host, build and engine configuration -- and upstream is explicit that +// request content, prompts and completions are not collected. So the first-party posture holds for +// route material exactly as stated, and what reaches a third party is metadata about the machine. +// Refusing over it would have blocked serving on a path carrying nothing the posture is about. +// +// THE JURISDICTION SLOT CITES A FIELD, NOT A PLACE, and that is deliberate. Upstream documents the +// server and nothing about who operates it or under which legal system, so the honest value is the +// typed ServiceJurisdictionUndocumentedUpstream that field holds. WHAT THAT COSTS, STATED PLAINLY: +// ProviderPathLocated cannot express "located at a party whose jurisdiction upstream does not +// document" -- a consumer matching Located reads all three components as known. The weakness is +// carried where a reader following the citation hits a typed arm rather than a sentence, which is +// the best this type admits. NEXT-RUNG TRIGGER: a jurisdiction standing on ProviderPathStanding +// itself, sufficient for a located path to say its jurisdiction is unread without the whole path +// becoming unread. +// +// THE REMEDY IF ZERO EGRESS IS EVER WANTED is one environment variable on the launch -- +// VLLM_NO_USAGE_STATS=1, or DO_NOT_TRACK=1, or the marker file -- on a box the operator owns. It is +// named here rather than blocked on, because it is the operator's to set. +data spark_serving_usage_stats_standing: VllmUsageStatsLaunchStanding = UsageStatsEnabledByDefault { + basis: "gunbc.spark.pair_serving_realization's container environment sets neither VLLM_NO_USAGE_STATS nor DO_NOT_TRACK, and no launch step writes the do_not_track marker, so usage reporting is on by upstream default on every Spark serving group. This is read from OUR OWN launch declaration, which is what a launch standing is about; it does not claim that a running host's environment was inspected.", +} + +fn spark_usage_stats_telemetry_path() -> ProviderPathStanding { + ProviderPathLocated { + operator: decl_ref(module_path: "extdeps.vllm.usage_stats", decl_name: "vllm_usage_stats_reporting"), + jurisdiction: decl_field_ref(module_path: "extdeps.vllm.usage_stats", decl_name: "vllm_usage_stats_reporting", field_name: "service_jurisdiction"), + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_serving_usage_stats_standing"), + } +} + +// THE observed_at DATE IS THE ASSERTION'S, AT DATE GRAIN. ProviderRouteFacts takes a Timestamp and +// these facts rest on a statement made on a DAY, so the time of day carries nothing and must not be +// read as a moment anybody measured; the midnight is the date-grain convention already used by +// gunbc.instruments.fabric_control_plane_live_probe, not a reading. The field is named for an +// observation because most routes are observed; this one says in every other line that it is not. fn spark_first_party_route_facts() -> ProviderRouteFacts { ProviderRouteFacts { route: spark_first_party_route(), @@ -309,7 +358,7 @@ fn spark_first_party_route_facts() -> ProviderRouteFacts { durable_storage: spark_first_party_path(), backups: spark_first_party_path(), logs: spark_first_party_path(), - telemetry: spark_first_party_path(), + telemetry: spark_usage_stats_telemetry_path(), control_plane: spark_first_party_path(), support_access: spark_first_party_path(), administrative_access: spark_first_party_path(), From 618db79bdd5559c8d28290de22367aa39785a2fc Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 19:57:54 +0000 Subject: [PATCH 04/11] Review 63995: fold the three carriers that were carrying their claims in prose All three findings are the same class as the first review's, which is the point of them: a typed carrier is not evidence until something matches on it. 1. THE ROSTER NOW GATES THE STANDING. spark_serving_route_standing took no argument, so an eight-unit allocation constrained nothing and a group on a machine the operator never placed at his home would have bound an offer whose region cites an assertion about other machines. It now takes the group's hosts, returns the UNCOVERED set rather than a Bool (a predicate discards the host the refusal has to name), and refuses naming them. The harness passes fabric_group_hosts. AND THE EMPTY LIST REFUSES, which is why the fold is over the uncovered set and not an all() over the covered one: all() of nothing is true, so a group whose membership could not be read would have passed the very check meant to constrain it -- the check reading cleanest exactly where it knows least. Both arms are REDs. 2. THE CONTENT CLASS AND THE LAUNCH STANDING ARE FOLDED. The telemetry path's arm is now DERIVED from them: a launch that disables reporting has no egress and the path is Absent; a launch nobody read is an obligation and refuses; a reporter that ever carries request material is route material leaving the site and refuses to a declared obligation naming the remedy. Only the metadata-only case is Located. The operator's ruling was made about a payload, and it is now conditional on that payload in code rather than in a sentence. 3. THE JURISDICTION DEPARTURE IS A ROSTERED DROP, NOT A COMMENT. gunbc.rung_drop.provider_path_jurisdiction_unread_admits declares it with its population and a trigger naming the CAPABILITY -- a jurisdiction standing on ProviderPathStanding sufficient for a located path to say its jurisdiction is unread without the whole path becoming unread. Reading who runs the usage-stats service explicitly does not discharge it: that fills one slot on one route and leaves every other located path in the same unexpressible position. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/harness/harness_seat.dag | 4 +- ...ovider_path_jurisdiction_unread_admits.dag | 69 +++++++++++++++++ dag/gunbc/rung_drop/roster.dag | 2 + dag/gunbc/spark/first_party_serving.dag | 77 +++++++++++++++++-- dag/gunbc/spark/serving_offer.dag | 49 +++++++++--- ...spark_serving_offer_route_witness_test.dag | 35 ++++++++- 6 files changed, 217 insertions(+), 19 deletions(-) create mode 100644 dag/gunbc/rung_drop/provider_path_jurisdiction_unread_admits.dag diff --git a/dag/gunbc/harness/harness_seat.dag b/dag/gunbc/harness/harness_seat.dag index 99bdb615b95..cfa827be512 100644 --- a/dag/gunbc/harness/harness_seat.dag +++ b/dag/gunbc/harness/harness_seat.dag @@ -4,7 +4,7 @@ import std.types { String, Bool, Int, NonEmptyStr, List, EpochSecs } import std.nat { Nat, nat_range_inclusive } import std.measure { Measure, Count, One, money_amount_micro } import gunbc.fleet_intent_network { host_lan_address } -import gunbc.spark.fabric_switch_observed { FabricGroup, fabric_group_wire } +import gunbc.spark.fabric_switch_observed { FabricGroup, fabric_group_wire, fabric_group_hosts } import gunbc.spark.pair_serving_desired { spark_pair_serving_groups, spark_pair_serving_head, spark_pair_serving_unit, SparkPairServingUnitReady, SparkPairServingUnitRefused, @@ -300,7 +300,7 @@ fn harness_bind_candidate(acc: HarnessCandidates, group: FabricGroup, address: S isolation: serving_isolation_profile(), seats: harness_interactive_quality_seats as Int, readiness: harness_serving_readiness(standing: harness_observe_replica(address: address), now: now), - route: spark_serving_route_standing(), + route: spark_serving_route_standing(hosts: fabric_group_hosts(g: group)), ) { SparkOfferBindingRefused { group_wire: _, cause: why } => harness_no_candidate(acc: acc, note: seat_bind_detail(group: group, text: why as String), retryable: false) diff --git a/dag/gunbc/rung_drop/provider_path_jurisdiction_unread_admits.dag b/dag/gunbc/rung_drop/provider_path_jurisdiction_unread_admits.dag new file mode 100644 index 00000000000..36d8a7483c5 --- /dev/null +++ b/dag/gunbc/rung_drop/provider_path_jurisdiction_unread_admits.dag @@ -0,0 +1,69 @@ +module gunbc.rung_drop.provider_path_jurisdiction_unread_admits + +import std.types { NonEmptyStr } +import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, DeletedWithoutReplacement } +import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed } + +// ============================================================================================ +// THE DECLARED RUNG DROP for a located data path whose jurisdiction upstream does not document +// (DESIGN 4b(3)). +// ============================================================================================ +// +// WHY THIS ROW EXISTS AT ALL. The departure stood as an ANNOTATION for exactly one revision, and an +// annotation cannot discharge it -- DESIGN 4c is explicit that no Accepted program reads one, so a +// machine claim living only in prose is a claim nothing checks. Review 63995 named it: a next-rung +// trigger written in a comment is invisible to 4b(2)'s no-untracked-stall and to the drop roster +// that exists to count exactly this. +// +// WHAT THE DROP IS. product.fabric.provider_route ProviderPathLocated carries operator, jurisdiction +// and evidence, and a consumer matching it reads all three as established. The Spark serving route's +// telemetry path cannot honour the middle one: vLLM reports usage statistics to a service upstream +// publishes the address of and nothing else about, so who operates it and under which legal system +// are UNREAD. The path is nevertheless recorded as Located, with its jurisdiction slot citing the +// field holding ServiceJurisdictionUndocumentedUpstream -- so the fact is reachable from the value, +// and is not reachable from the ARM, which is the part that is dropped. +// +// WHY THE FAIL-CLOSED ARM WAS NOT TAKEN. ProviderPathUnread exists, is reachable, and refuses the +// whole route as ProviderRouteFactsIncomplete. It is the right answer to "is this path resolved" and +// the wrong answer to the question actually being asked, because it refuses over a path that carries +// NO ROUTE MATERIAL: extdeps.vllm.usage_stats records the documented payload as host, build and +// engine configuration, with request content, prompts and completions excluded upstream. Refusing +// would stop serving on a metadata egress while saying nothing about where route material goes. +// Ruled by the operator on 2026-09-11, on the condition -- executed, not promised -- that the +// payload stay metadata-only: gunbc.spark.first_party_serving matches the content class and takes +// the refusing arm if upstream ever reports CarriesRequestMaterial. +// +// WHAT IS AND IS NOT LOST. Not lost: whether the path exists, who receives it, what it carries, and +// whether the launch could have disabled it -- all four are typed, folded and refusable. Lost: the +// guarantee that a Located path's jurisdiction was established. The harm is that a consumer asking +// "which legal systems does this route touch" gets a confident answer from two paths and a citation +// standing where a jurisdiction belongs from the third, and nothing in the arm tells it apart. +// +// THE TRIGGER NAMES THE CAPABILITY, NOT AN ARTIFACT. Reading stats.vllm.ai's operator off a +// third-party page would not retire this row: it would fill one slot for one route and leave the +// next located path with an undocumented counterparty in the same position. The capability is a +// jurisdiction standing ON ProviderPathStanding -- sufficient for a located path to declare its +// jurisdiction unread WITHOUT the whole path becoming unread -- at which point this route states the +// fact in its arm and the drop has nothing left to admit. +// +// DECLARED 2026-09-11 with the Spark first-party serving route, under review 63995. + +data provider_path_jurisdiction_unread_admits: RungDrop = RungDrop { + identity: "provider_path_jurisdiction_unread_admits" as NonEmptyStr, + + subject: "one ProviderPathLocated whose jurisdiction upstream does not document, admitted rather than refused because the path carries no route material, with the unread fact reachable from the cited field and not from the arm", + + declared: "2026-09-11", + + standing: Standing, + + declaration: TypedDeclaration { + previous: StructurallyGuaranteed, + temporary: Mitigatable, + reason: DeletedWithoutReplacement, + population: [ + "gunbc.spark.first_party_serving spark_usage_stats_telemetry_path (returns ProviderPathLocated whose jurisdiction cites extdeps.vllm.usage_stats vllm_usage_stats_reporting service_jurisdiction, a field whose value is ServiceJurisdictionUndocumentedUpstream; the fail-closed arm ProviderPathUnread is reachable from the same fold and refuses the route)", + ], + restoration_trigger: "product.fabric.provider_route ProviderPathStanding carries a jurisdiction standing SUFFICIENT FOR a located path to declare its jurisdiction unread without the whole path becoming unread -- so that a consumer matching the located arm can see which of its three components were established -- and gunbc.spark.first_party_serving's telemetry path states the fact in its arm. Reading who operates the usage-stats service does NOT discharge this row: it fills one slot on one route and leaves every other located path with an undocumented counterparty in the same unexpressible position", + } +} diff --git a/dag/gunbc/rung_drop/roster.dag b/dag/gunbc/rung_drop/roster.dag index 94597185f77..ade206391bd 100644 --- a/dag/gunbc/rung_drop/roster.dag +++ b/dag/gunbc/rung_drop/roster.dag @@ -53,6 +53,7 @@ import gunbc.rung_drop.source_root_ingest_gate_rung_drop { source_root_ingest_ga import gunbc.rung_drop.spark_serving_fleet_global_configuration_drop { spark_serving_fleet_global_configuration_drop } import gunbc.rung_drop.harness_seat_ceiling_by_operator_policy { harness_seat_ceiling_by_operator_policy } import gunbc.rung_drop.serving_cost_axes_asserted_unmeasured { serving_cost_axes_asserted_unmeasured } +import gunbc.rung_drop.provider_path_jurisdiction_unread_admits { provider_path_jurisdiction_unread_admits } import gunbc.rung_drop.serving_offer_identity_is_the_exporter_process { serving_offer_identity_is_the_exporter_process } import gunbc.rung_drop.witness_deferral_freeze_forward_rule_rung_drop { witness_deferral_freeze_forward_rule_rung_drop } import gunbc.rung_drop.deleted_cadence_reference_drop { deleted_cadence_reference_drop } @@ -97,6 +98,7 @@ data rung_drop_roster: List = [ spark_serving_fleet_global_configuration_drop, harness_seat_ceiling_by_operator_policy, serving_cost_axes_asserted_unmeasured, + provider_path_jurisdiction_unread_admits, serving_offer_identity_is_the_exporter_process, witness_deferral_freeze_forward_rule_rung_drop, deleted_cadence_reference_drop, diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 13e377e528f..65a3447ccd0 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -3,11 +3,12 @@ module gunbc.spark.first_party_serving import std.types { NonEmptyStr, List } import std.decl_ref { DeclarationRef, decl_ref, decl_field_ref } import std.content_hash { as_content_hash_structural, content_hash_atom } -import product.placement_supply { SiteIdentity, HostIdentity } +import product.placement_supply { SiteIdentity, HostIdentity, host_identity_eq } import product.fabric.identity { FabricIdentity, DemandKey, WorkKey, OfferKey } import product.fabric.provider_route { ProviderRoute, CompliancePostureRevision, ProviderRouteFacts, ProviderDataPathClosure, ProviderPathStanding, ProviderPathLocated, + ProviderPathAbsent, ProviderPathUnread, DownstreamProviderPopulation, NoDownstreamProviders, } import product.fabric.provider_admission { @@ -15,7 +16,10 @@ import product.fabric.provider_admission { DispositionStanding, DispositionNotEngaged, admit_provider_use, } import extdeps.vllm.usage_stats { - VllmUsageStatsLaunchStanding, UsageStatsEnabledByDefault, + VllmUsageStatsLaunchStanding, UsageStatsDisabledByLaunch, UsageStatsEnabledByDefault, + UsageStatsLaunchUnread, VllmUsageStatsContentClass, + ConfigurationAndHardwareMetadataOnly, CarriesRequestMaterial, + vllm_usage_stats_reporting, } import gunbc.spark.dgx_procurement { OperatorAllocation } import gunbc.fleet_physical_inventory { operator_site } @@ -78,6 +82,22 @@ data spark_fleet_site_allocation: SparkFleetSiteAllocation = SparkFleetSiteAlloc }, } +// ── THE ROSTER GATES THE STANDING, OR IT IS PROSE IN A LIST FIELD ───────────────────────────── +// +// Review 63995 is right that the first spelling of this module enumerated eight units and then +// never compared anything to them: the route standing took no host, so a serving group on a machine +// the operator never placed at his home would have bound an offer whose region cites an assertion +// that does not cover it. An enumerated roster nothing folds is the §3c dangling row in its most +// expensive form, because it reads as a scope while enforcing none. +// +// THE ANSWER IS THE UNCOVERED SET, NOT A Bool. A predicate discards exactly the payload the refusal +// needs -- WHICH host is outside the assertion -- forcing the refusal builder to walk the value +// again, and that second walk is where an invented name gets to live. The uncovered hosts come back +// and the caller names them. +fn spark_site_uncovered_units(hosts: List) -> List { + filter(hosts, h => !any(spark_fleet_site_allocation.units, u => host_identity_eq(a: u, b: h))) +} + // ── THE PROVIDER IS US, WHICH IS THE ONE MODELING CALL THIS MODULE MAKES ────────────────────── // // A ProviderRoute is provider x service x region and all three are cited declarations. For a rented @@ -336,11 +356,56 @@ data spark_serving_usage_stats_standing: VllmUsageStatsLaunchStanding = UsageSta basis: "gunbc.spark.pair_serving_realization's container environment sets neither VLLM_NO_USAGE_STATS nor DO_NOT_TRACK, and no launch step writes the do_not_track marker, so usage reporting is on by upstream default on every Spark serving group. This is read from OUR OWN launch declaration, which is what a launch standing is about; it does not claim that a running host's environment was inspected.", } +// THE TWO TYPED CARRIERS ARE FOLDED, NOT CITED. Review 63995's second finding is the first review's +// finding one level over: the content class was declared, named as "the whole reason a consumer can +// admit this path", and then never matched -- so a later revision flipping upstream's payload to +// CarriesRequestMaterial would have left every admission green. It is matched here, and so is the +// launch standing, which means the path's arm is DERIVED from those two facts rather than chosen +// beside them. +// +// EACH ARM IS THE HONEST ANSWER TO A DIFFERENT WORLD. A launch that disables reporting has no +// telemetry egress at all, which is what ProviderPathAbsent means. A launch nobody read is an +// obligation and refuses. And a reporter that ever carries request material is not a metadata path +// to be admitted with a caveat: it becomes route material leaving the site, so it refuses until +// somebody re-assesses the route -- the arm that makes the operator's ruling conditional on the +// fact it was made about. +// THE OBLIGATION THE REQUEST-MATERIAL ARM NAMES. It is a declared row rather than a sentence at the +// arm because it is what a reader is sent to when the refusal fires, and what it asks for is a +// re-assessment of the route rather than a smaller repair: a reporter carrying request material is +// route material leaving the site, which is the premise the first-party posture rests on. +type UsageStatsEscalationObligation { + trigger: NonEmptyStr + remedy: NonEmptyStr +} + +data spark_usage_stats_carrying_request_material_obligation: UsageStatsEscalationObligation = UsageStatsEscalationObligation { + trigger: "extdeps.vllm.usage_stats vllm_usage_stats_reporting reports CarriesRequestMaterial at the cited source revision, so the usage-stats reporter no longer carries only host, build and engine configuration.", + remedy: "The first-party posture rests on route material staying on site, and this would be route material leaving it. Set VLLM_NO_USAGE_STATS=1 or DO_NOT_TRACK=1 on the serving launch, or re-assess the posture with the operator. Until one of those happens the route's telemetry path is unresolved and provider-use admission refuses as ProviderRouteFactsIncomplete.", +} + fn spark_usage_stats_telemetry_path() -> ProviderPathStanding { - ProviderPathLocated { - operator: decl_ref(module_path: "extdeps.vllm.usage_stats", decl_name: "vllm_usage_stats_reporting"), - jurisdiction: decl_field_ref(module_path: "extdeps.vllm.usage_stats", decl_name: "vllm_usage_stats_reporting", field_name: "service_jurisdiction"), - evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_serving_usage_stats_standing"), + match spark_serving_usage_stats_standing { + UsageStatsDisabledByLaunch { mechanism: _ } => + ProviderPathAbsent { + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_serving_usage_stats_standing"), + } + UsageStatsLaunchUnread { obligation: _ } => + ProviderPathUnread { + obligation: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_serving_usage_stats_standing"), + } + UsageStatsEnabledByDefault { basis: _ } => + match vllm_usage_stats_reporting.content_class { + CarriesRequestMaterial => + ProviderPathUnread { + obligation: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_usage_stats_carrying_request_material_obligation"), + } + ConfigurationAndHardwareMetadataOnly => + ProviderPathLocated { + operator: decl_ref(module_path: "extdeps.vllm.usage_stats", decl_name: "vllm_usage_stats_reporting"), + jurisdiction: decl_field_ref(module_path: "extdeps.vllm.usage_stats", decl_name: "vllm_usage_stats_reporting", field_name: "service_jurisdiction"), + evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_serving_usage_stats_standing"), + } + } } } diff --git a/dag/gunbc/spark/serving_offer.dag b/dag/gunbc/spark/serving_offer.dag index 4da44a93a7b..42d88863c92 100644 --- a/dag/gunbc/spark/serving_offer.dag +++ b/dag/gunbc/spark/serving_offer.dag @@ -1,6 +1,6 @@ module gunbc.spark.serving_offer -import std.types { String, NonEmptyStr, Int, Timestamp } +import std.types { String, NonEmptyStr, Int, Timestamp, List } import product.fabric.identity { FabricIdentity } import product.fabric.demand { ObservationReceiptRef } import product.fabric.work { Shape, HardRequirements, CapabilityManifestRef, TrustDomainRef } @@ -10,9 +10,12 @@ import product.fabric.supply { SupplierOffer, OfferQuote, QuotedPerSecond, Obser import product.fabric.provider_route { ProviderRoute } import std.measure { Second, second, MoneyRate, money_amount_micro, hardware_thread_count } import extdeps.currency.currency { Usd } +import product.placement_supply { HostIdentity } import gunbc.spark.fabric_switch_observed { fabric_group_wire } import gunbc.spark.dgx_procurement { OperatorAllocation } -import gunbc.spark.first_party_serving { spark_first_party_route, spark_fleet_site_allocation } +import gunbc.spark.first_party_serving { + spark_first_party_route, spark_fleet_site_allocation, spark_site_uncovered_units, +} import gunbc.spark.vllm_endpoint_process_launch { VllmEndpointProcessLaunch, vllm_endpoint_process_launch_key, } @@ -139,13 +142,41 @@ data spark_serving_route_region_obligation: NonEmptyStr = "gunbc.spark.serving_o // withdrawal was right: what it refused was a region nobody had established. What changed is not // that somebody measured one -- for self-hosted units nobody ever can -- but that the operator // stated where the units are, dated and attributable, and gunbc.spark.first_party_serving carries -// that statement as an OperatorAllocation over every Spark unit. The standing therefore selects the -// asserted arm, and the route it carries is the first-party one: provider us, service the pair -// serving deployment, region the allocation itself. -fn spark_serving_route_standing() -> SparkServingRoute { - ServingRouteOperatorAsserted { - route: spark_first_party_route(), - allocation: spark_fleet_site_allocation.allocation, +// that statement as an OperatorAllocation over the Spark units it names. +// +// THE STANDING IS PER GROUP, NOT GLOBAL, BECAUSE THE ASSERTION IS PER UNIT. It takes the hosts the +// offer would run on and refuses unless the allocation covers every one of them. The first spelling +// took no argument at all, which made an eight-unit roster decorative and would have let a group on +// a machine the operator never placed at his home carry a region citing an assertion about other +// machines (review 63995). +// +// AN EMPTY HOST LIST REFUSES, and that arm is the reason this is a fold over the UNCOVERED set +// rather than an all() over the covered one: all() of nothing is true, so a group whose membership +// could not be read would have passed the check vacuously -- the check reading cleanest exactly +// where it knows least. +data spark_serving_route_hosts_unreadable_obligation: NonEmptyStr = "gunbc.spark.serving_offer: the serving group's host membership could not be read, so there is nothing to compare against the operator's site allocation and the offer's region rests on nothing" + +fn spark_serving_route_uncovered_obligation(uncovered: List) -> NonEmptyStr { + join([ + "gunbc.spark.serving_offer: the operator's site allocation (gunbc.spark.first_party_serving spark_fleet_site_allocation, 2026-09-11) does not cover this serving group's host(s) ", + join(map(uncovered, h => h as String), ", "), + ", so no assertion places them anywhere and the offer's region cannot be constructed. A unit that has moved needs a NEW allocation row, never an edit to the standing one", + ], "") as NonEmptyStr +} + +fn spark_serving_route_standing(hosts: List) -> SparkServingRoute { + if count(hosts) == 0 { + ServingRouteRegionUnobserved { obligation: spark_serving_route_hosts_unreadable_obligation } + } else { + let uncovered = spark_site_uncovered_units(hosts: hosts) + if count(uncovered) > 0 { + ServingRouteRegionUnobserved { obligation: spark_serving_route_uncovered_obligation(uncovered: uncovered) } + } else { + ServingRouteOperatorAsserted { + route: spark_first_party_route(), + allocation: spark_fleet_site_allocation.allocation, + } + } } } diff --git a/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag b/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag index acbd528ed44..73c8829a7c1 100644 --- a/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag +++ b/dag/test/claim/spark/spark_serving_offer_route_witness_test.dag @@ -1,12 +1,14 @@ module test.claim.spark.spark_serving_offer_route_witness_test -import std.types { Bool, NonEmptyStr, String } +import std.types { Bool, NonEmptyStr, String, List } import std.decl_ref { decl_ref, declaration_ref_eq } import product.fabric.provider_route { ProviderRoute } import product.fabric.identity { FabricIdentity } import product.fabric.isolation { IsolationProfile } import product.fabric.work { TrustDomainRef } import product.fabric.demand { ObservationReceiptRef } +import product.placement_supply { HostIdentity } +import gunbc.fleet_intent_network { operator_host_srv5, operator_host_srv6, operator_host_srv1 } import gunbc.spark.fabric_switch_observed { FabricGroup, FabricGroupA } import gunbc.spark.vllm_endpoint_process_launch { VllmEndpointProcessLaunch, vllm_endpoint_process_launch, @@ -16,6 +18,7 @@ import gunbc.spark.serving_offer { SparkServingReadiness, ServingObserved, SparkServingRoute, ServingRouteObserved, ServingRouteOperatorAsserted, ServingRouteRegionUnobserved, spark_serving_route_standing, spark_serving_route_region_obligation, + spark_serving_route_hosts_unreadable_obligation, bind_spark_serving_offer, } @@ -99,7 +102,7 @@ test fn an_unobserved_region_refuses_naming_its_obligation() -> Bool { // region it carries must be the allocation, because a region citing the bare site row would name a // place while dropping who said the units are there and when. test fn the_standing_the_harness_passes_is_operator_asserted_with_its_allocation() -> Bool { - match spark_serving_route_standing() { + match spark_serving_route_standing(hosts: [operator_host_srv5, operator_host_srv6]) { ServingRouteRegionUnobserved { obligation: _ } => false ServingRouteObserved { route: _ } => false ServingRouteOperatorAsserted { route: r, allocation: a } => @@ -108,3 +111,31 @@ test fn the_standing_the_harness_passes_is_operator_asserted_with_its_allocation && (a.decided_on as String) == "2026-09-11" } } + + +// RED -- THE ROSTER GATES THE STANDING. srv1 is a real fleet host and is NOT one of the units the +// operator placed at his home, so a group containing it has no assertion behind its region and the +// standing refuses. Without this row the eight-unit roster in the allocation would be decorative: +// nothing else in the corpus compares a host to it (review 63995). +test fn a_host_outside_the_allocation_refuses_and_names_it() -> Bool { + match spark_serving_route_standing(hosts: [operator_host_srv5, operator_host_srv1]) { + ServingRouteObserved { route: _ } => false + ServingRouteOperatorAsserted { route: _, allocation: _ } => false + ServingRouteRegionUnobserved { obligation: o } => + string_contains(s: o as String, pattern: "srv1") + && !string_contains(s: o as String, pattern: "srv5") + } +} + +// RED -- AN UNREADABLE GROUP REFUSES RATHER THAN PASSING VACUOUSLY. This is the arm that decides +// whether the membership check is a wall or a decoration: written as all(hosts, covered) it would +// be TRUE for the empty list, so a group whose membership could not be read would have been +// admitted by the check that exists to constrain it -- cleanest exactly where it knows least. +test fn an_unreadable_group_membership_refuses() -> Bool { + match spark_serving_route_standing(hosts: [] as List) { + ServingRouteObserved { route: _ } => false + ServingRouteOperatorAsserted { route: _, allocation: _ } => false + ServingRouteRegionUnobserved { obligation: o } => + (o as String) == (spark_serving_route_hosts_unreadable_obligation as String) + } +} From 77426a84f5224994d8df8220be3d634be754378e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 20:21:23 +0000 Subject: [PATCH 05/11] Review 64014: an annotation claiming a live role the row no longer has spark_serving_route_region_obligation's note said it is "the refusal a caller reaches". No production producer returns it any more -- the standing refuses with the uncovered-host or unreadable-membership obligation, which locate the group instead of saying nobody observes regions at all. Its one consumer is the binder fixture, which is a real consumer and why the row stays; the sentence was the part that overstated. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/spark/serving_offer.dag | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/spark/serving_offer.dag b/dag/gunbc/spark/serving_offer.dag index 42d88863c92..be157b4c116 100644 --- a/dag/gunbc/spark/serving_offer.dag +++ b/dag/gunbc/spark/serving_offer.dag @@ -132,10 +132,14 @@ type SparkServingRoute // THE SINGLE PLACE THE STANDING IS RECORDED, which is why the 2026-09-11 restoration replaced one // declaration rather than every call site -- the same property that made the withdrawal cheap. // -// THE OBLIGATION ROW SURVIVES THE RESTORATION AND IS NOT DEAD. It is the refusal a caller reaches -// when it has no allocation and no observation to offer, it is what the binder reports for that -// arm, and test.claim.spark.spark_serving_offer_route_witness_test still drives the binder with it. -// Deleting it would delete the only spelling of "this route's region rests on nothing". +// THE OBLIGATION ROW SURVIVES THE RESTORATION, AND WHAT IT IS FOR NOW IS NARROWER THAN IT WAS. No +// production producer returns it any more -- the standing below refuses with the uncovered-host or +// unreadable-membership obligation instead, which say WHICH group is not covered rather than that +// nobody observes regions at all. Its one consumer is the binder fixture in +// test.claim.spark.spark_serving_offer_route_witness_test, where it is the spelling of "this route's +// region rests on nothing" that drives the binder's refusing arm. That is a real consumer and the +// row stays; calling it "the refusal a caller reaches" would claim a live role it no longer has +// (review 64014). data spark_serving_route_region_obligation: NonEmptyStr = "gunbc.spark.serving_offer: no producer observes which region a serving host sits in, so the offer's ProviderRoute cannot be constructed and the offer does not bind" // WITHDRAWN 2026-09-09, RESTORED 2026-09-11 ON AN ASSERTION RATHER THAN AN OBSERVATION. The From eb94bf95f31b0dca47b9b91dee16ddb6b4544eee Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 20:52:14 +0000 Subject: [PATCH 06/11] Review 64033: derive the launch standing from the launch, and delete a field that claimed to be read TWO FINDINGS, AND BOTH ARE THIS PR'S OWN LESSON APPLIED TO THE LINES IT DID NOT APPLY IT TO. 1. THE USAGE-STATS LAUNCH STANDING WAS TRANSCRIBED FROM A MODULE THAT MODELS IT. Its basis said "pair_serving_realization's container environment sets neither variable", which is a second authority for a fact spark_pair_container_env already owns -- DESIGN section 6's name-the-instrument rule, and the same defect this module fixes one function below for the content class. It is folded now: every observed fabric lane's container environment against extdeps.vllm.usage_stats' own disable_env_vars. Adding VLLM_NO_USAGE_STATS=1 to the launch flips the standing, flips the telemetry path to ProviderPathAbsent, and takes the rung drop's population out from under it, with no edit here. Three things the fold gets right that a predicate would not. EVERY lane must disable it, not any, because a reporter on one host of a group is an egress for the route. AN EMPTY LANE ROSTER IS UNREAD rather than disabled -- the vacuous "all of nothing" is the same trap the host-coverage fold already avoids. And a name set to "0" is not a disable, because upstream reads these as booleans. A witness asserts the arm, so the day the launch disables reporting the rostered drop stops describing a path that exists and says so. 2. staleness_condition CLAIMED TO BE MACHINE-READ AND WAS NOT. The annotation said "every consumer of this row reads this". Nothing folded it. It was a comment moved into a NonEmptyStr slot so it could be described as executed -- the DESIGN 4c shape, and worse than an annotation, which does not claim to be read. The field is deleted. What enforces "for now" is the posture revision, the roster row bound to it, and the RED that drives a superseded revision through admit_provider_use and requires PostureRevisionStale. The other fields stay: they are the evidence an auditor reaches by following a DeclarationRef out of the permit, which is a cited row's job. The distinction is whether the module claims a machine reads it. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/spark/first_party_serving.dag | 107 +++++++++++------- ...spark_first_party_serving_witness_test.dag | 25 ++++ 2 files changed, 94 insertions(+), 38 deletions(-) diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 65a3447ccd0..bb5ae0b9701 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -15,6 +15,9 @@ import product.fabric.provider_admission { RouteScopeSanction, ProviderUseScope, ProviderUseAdmission, DispositionStanding, DispositionNotEngaged, admit_provider_use, } +import extdeps.docker { DockerEnvAssignment } +import gunbc.spark.fabric_switch_observed { FabricLaneObserved, fabric_lane_observations } +import gunbc.spark.pair_serving_realization { spark_pair_container_env } import extdeps.vllm.usage_stats { VllmUsageStatsLaunchStanding, UsageStatsDisabledByLaunch, UsageStatsEnabledByDefault, UsageStatsLaunchUnread, VllmUsageStatsContentClass, @@ -154,15 +157,26 @@ fn spark_first_party_route() -> ProviderRoute { // per posture revision by construction, and product.fabric.provider_admission refuses a sanction // evaluated under a superseded revision as PostureRevisionStale. Serving anybody else is a // materially different contract subject, so it is a NEW posture revision that makes every sanction -// under this one stale -- not an extra profile quietly added to the roster below. That is why the -// staleness_condition field is a field of the posture rather than a sentence in an annotation: no -// Accepted program reads an annotation (DESIGN 4c), and every consumer of this row reads this. +// under this one stale -- not an extra profile quietly added to the roster below. +// +// AND THE ENFORCEMENT IS THE REVISION, NOT A FIELD DESCRIBING IT. This type carried a +// staleness_condition field, and the sentence here claimed "every consumer of this row reads this", +// which was false: nothing folded it (review 64033). It was a comment moved into a NonEmptyStr slot +// so that it could be described as executed, which is the §4c shape exactly -- and worse than an +// annotation, because an annotation does not claim to be read. The field is deleted; what enforces +// "for now" is spark_first_party_posture's revision, the roster row bound to it, and the RED in +// test.claim.spark.spark_first_party_serving_witness_test that drives a superseded revision through +// admit_provider_use and requires PostureRevisionStale. +// +// THE REMAINING FIELDS ARE NOT IN THAT CLASS AND ARE KEPT. They are the evidence an auditor reaches +// by following a DeclarationRef out of the permit -- what the route serves, whose material it +// carries, and under what custody -- which is the job of a cited row. The distinction is whether the +// module claims a machine reads it. type FirstPartySelfUsePosture { assertion: OperatorAllocation serves: NonEmptyStr data_subject: NonEmptyStr hardware_custody: NonEmptyStr - staleness_condition: NonEmptyStr } data spark_first_party_use_posture: FirstPartySelfUsePosture = FirstPartySelfUsePosture { @@ -174,13 +188,13 @@ data spark_first_party_use_posture: FirstPartySelfUsePosture = FirstPartySelfUse serves: "gunbc itself. Every turn placed on this route originates inside this repository's own harness and control plane; no turn is served to any party outside gunbc and none crosses an organisational or national boundary.", data_subject: "our own material. The prompts and responses on this route are gunbc's, held on operator-owned hardware at the operator's own site; no customer data and no third-party data is processed on it. ROUTE MATERIAL STAYS ON SITE AND EXACTLY ONE PATH LEAVES IT: vLLM reports host, build and engine-configuration metadata to https://stats.vllm.ai by upstream default, carrying no request content (extdeps.vllm.usage_stats, and gunbc.spark.first_party_serving spark_serving_usage_stats_standing for this fleet's launch). The remedy for zero egress is VLLM_NO_USAGE_STATS=1 or DO_NOT_TRACK=1 on the serving launch, which is the operator's to set on his own box.", hardware_custody: "operator-owned and operator-held. There is no third-party agreement governing this route because there is no third party: no hosting contract, no processor, and no service terms stand between us and the hardware.", - staleness_condition: "SERVING ANYONE ELSE ENDS THIS POSTURE. A turn served to a party outside gunbc, or any third-party material processed on this route, is a materially different contract subject and requires a NEW CompliancePostureRevision; every RouteScopeSanction below is bound to THIS revision, so it goes stale through product.fabric.provider_admission PostureRevisionStale rather than silently carrying over. Nothing here may be widened to cover another customer profile by adding a roster row under this revision.", } // The revision is the hash of the statement's identity as a named revision, not of the row's bytes. -// A statement change that does not move this tag is the hazard, and it is the reason the posture's -// own staleness_condition names re-posturing rather than editing: the authority reference below -// points at the row, so an auditor re-derives what was evaluated by reading it. +// A statement change that does not move this tag is the hazard, which is why serving anyone else is +// a RE-POSTURING and not an edit to the row above: the authority reference below points at that row, +// so an auditor re-derives what was evaluated by reading it, and a new posture leaves every sanction +// bound to this revision stale. data spark_first_party_posture: CompliancePostureRevision = CompliancePostureRevision { authority: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_first_party_use_posture"), revision: as_content_hash_structural(structural: content_hash_atom(value: "gunbc.spark.first-party-self-use.2026-09-11" as NonEmptyStr)), @@ -280,8 +294,9 @@ fn spark_export_disposition() -> DispositionStanding { // A roster row admits a (route, posture, customer profile, data class) tuple. There is exactly one, // so any other customer profile or data class on this route has no matching row and refuses as // CustomerScopeUnsupported or DataHandlingUnsupported -- which is how "it is just serving us for -// now" is enforced by execution rather than by this sentence. Adding a second row to widen it is -// the move the posture's staleness_condition forbids. +// now" is enforced by execution rather than by this sentence. Widening it with a second row under +// this same revision is the move that would silently carry the posture over to a use nobody +// sanctioned; serving anyone else is a new revision, and this roster goes stale against it. fn spark_first_party_sanction_roster() -> List { [ RouteScopeSanction { @@ -352,39 +367,55 @@ fn spark_first_party_downstream() -> DownstreamProviderPopulation { // THE REMEDY IF ZERO EGRESS IS EVER WANTED is one environment variable on the launch -- // VLLM_NO_USAGE_STATS=1, or DO_NOT_TRACK=1, or the marker file -- on a box the operator owns. It is // named here rather than blocked on, because it is the operator's to set. -data spark_serving_usage_stats_standing: VllmUsageStatsLaunchStanding = UsageStatsEnabledByDefault { - basis: "gunbc.spark.pair_serving_realization's container environment sets neither VLLM_NO_USAGE_STATS nor DO_NOT_TRACK, and no launch step writes the do_not_track marker, so usage reporting is on by upstream default on every Spark serving group. This is read from OUR OWN launch declaration, which is what a launch standing is about; it does not claim that a running host's environment was inspected.", +// +// AND THE STANDING IS DERIVED FROM THAT LAUNCH RATHER THAN TRANSCRIBED FROM IT. The first spelling +// wrote "the container environment sets neither variable" into a basis string, which review 64033 is +// right to call the same defect this module fixes one function below for the content class: the +// environment is a MODELED value in this repository, so a sentence about it is a second authority +// that rots the moment somebody edits the first. It is folded now -- the observed lanes' container +// environments against extdeps.vllm.usage_stats' own disable_env_vars -- so adding +// VLLM_NO_USAGE_STATS=1 to the launch flips this standing, flips the telemetry path to +// ProviderPathAbsent, and takes the rung drop's population out from under it, with no edit here. +// +// EVERY LANE MUST DISABLE IT, NOT ANY. A group serves from several hosts and a reporter on one of +// them is an egress for the route, so the fold is over the lanes that do NOT disable it and the +// disabled arm is reached only when that set is empty. AN EMPTY LANE ROSTER IS UNREAD, not disabled: +// with no observed lane there is no environment to read, and the vacuous "all of nothing" would be +// the check reading cleanest exactly where it knows least -- the same trap the host-coverage fold +// avoids above. +// +// A NAME SET TO "0" IS NOT A DISABLE. Upstream reads these as booleans, so a present-but-false +// assignment leaves reporting on; matching on the name alone would have read it as off. +fn spark_lane_disables_usage_stats(lane: FabricLaneObserved) -> Bool { + any( + vllm_usage_stats_reporting.disable_env_vars, + v => any( + spark_pair_container_env(lane: lane), + e => (e.name as String) == (v as String) && e.value != "0", + ), + ) } -// THE TWO TYPED CARRIERS ARE FOLDED, NOT CITED. Review 63995's second finding is the first review's -// finding one level over: the content class was declared, named as "the whole reason a consumer can -// admit this path", and then never matched -- so a later revision flipping upstream's payload to -// CarriesRequestMaterial would have left every admission green. It is matched here, and so is the -// launch standing, which means the path's arm is DERIVED from those two facts rather than chosen -// beside them. -// -// EACH ARM IS THE HONEST ANSWER TO A DIFFERENT WORLD. A launch that disables reporting has no -// telemetry egress at all, which is what ProviderPathAbsent means. A launch nobody read is an -// obligation and refuses. And a reporter that ever carries request material is not a metadata path -// to be admitted with a caveat: it becomes route material leaving the site, so it refuses until -// somebody re-assesses the route -- the arm that makes the operator's ruling conditional on the -// fact it was made about. -// THE OBLIGATION THE REQUEST-MATERIAL ARM NAMES. It is a declared row rather than a sentence at the -// arm because it is what a reader is sent to when the refusal fires, and what it asks for is a -// re-assessment of the route rather than a smaller repair: a reporter carrying request material is -// route material leaving the site, which is the premise the first-party posture rests on. -type UsageStatsEscalationObligation { - trigger: NonEmptyStr - remedy: NonEmptyStr -} - -data spark_usage_stats_carrying_request_material_obligation: UsageStatsEscalationObligation = UsageStatsEscalationObligation { - trigger: "extdeps.vllm.usage_stats vllm_usage_stats_reporting reports CarriesRequestMaterial at the cited source revision, so the usage-stats reporter no longer carries only host, build and engine configuration.", - remedy: "The first-party posture rests on route material staying on site, and this would be route material leaving it. Set VLLM_NO_USAGE_STATS=1 or DO_NOT_TRACK=1 on the serving launch, or re-assess the posture with the operator. Until one of those happens the route's telemetry path is unresolved and provider-use admission refuses as ProviderRouteFactsIncomplete.", +data spark_serving_usage_stats_unread_obligation: NonEmptyStr = "gunbc.spark.first_party_serving: no fabric lane is observed, so no serving container environment exists to read and whether vLLM's usage-stats reporter is disabled on this fleet is unknown. Read the lanes (gunbc.spark.fabric_switch_observed fabric_lane_observations) before this route's telemetry path can be resolved." + +fn spark_serving_usage_stats_standing() -> VllmUsageStatsLaunchStanding { + if count(fabric_lane_observations) == 0 { + UsageStatsLaunchUnread { obligation: spark_serving_usage_stats_unread_obligation } + } else { + if count(filter(fabric_lane_observations, l => !spark_lane_disables_usage_stats(lane: l))) == 0 { + UsageStatsDisabledByLaunch { + mechanism: "every observed fabric lane's serving container environment carries one of extdeps.vllm.usage_stats disable_env_vars with a value other than 0, so no lane reports usage statistics", + } + } else { + UsageStatsEnabledByDefault { + basis: "at least one observed fabric lane's serving container environment (gunbc.spark.pair_serving_realization spark_pair_container_env) carries none of extdeps.vllm.usage_stats disable_env_vars, so usage reporting is on by upstream default for this route. Derived from the launch declaration, not from a reading of any running host's environment.", + } + } + } } fn spark_usage_stats_telemetry_path() -> ProviderPathStanding { - match spark_serving_usage_stats_standing { + match spark_serving_usage_stats_standing() { UsageStatsDisabledByLaunch { mechanism: _ } => ProviderPathAbsent { evidence: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_serving_usage_stats_standing"), diff --git a/dag/test/claim/spark/spark_first_party_serving_witness_test.dag b/dag/test/claim/spark/spark_first_party_serving_witness_test.dag index 46a217d67c6..326361c95e6 100644 --- a/dag/test/claim/spark/spark_first_party_serving_witness_test.dag +++ b/dag/test/claim/spark/spark_first_party_serving_witness_test.dag @@ -11,7 +11,12 @@ import product.fabric.provider_admission { DispositionRefused, DispositionUnresolved, refusal_reason, admit_provider_use, } +import extdeps.vllm.usage_stats { + VllmUsageStatsLaunchStanding, UsageStatsDisabledByLaunch, UsageStatsEnabledByDefault, + UsageStatsLaunchUnread, +} import gunbc.spark.first_party_serving { + spark_serving_usage_stats_standing, spark_first_party_use_scope, spark_first_party_admission, spark_first_party_sanction_roster, spark_first_party_route_facts, spark_first_party_posture, spark_sanctions_disposition, spark_export_disposition, spark_prohibited_use_disposition, @@ -141,3 +146,23 @@ test fn a_superseded_posture_makes_the_first_party_sanction_stale() -> Bool { ProviderUseDenied { decision: _, cause: c } => refusal_reason(c: c) == "posture stale" } } + + +// THE DROP'S POPULATION AND THE CODE MOVE TOGETHER, WHICH IS WHAT THIS ROW IS FOR. The rung drop +// gunbc.rung_drop.provider_path_jurisdiction_unread_admits is declared against a telemetry path that +// exists only while the serving launch leaves usage reporting on. That standing is now DERIVED from +// gunbc.spark.pair_serving_realization's container environment, so the day somebody adds +// VLLM_NO_USAGE_STATS=1 the path becomes ProviderPathAbsent and the drop is declared against nothing +// -- and this row goes red and says so, rather than leaving a rostered drop describing a path that +// no longer exists. +// +// IT IS NOT A CHANGE DETECTOR: it asserts the arm the fold selects, and the fold reads a declaration +// in another module, so what goes red is a real divergence between the launch and the drop roster +// rather than a number someone has to keep in step by hand. +test fn the_launch_leaves_usage_reporting_on_which_is_what_the_drop_is_declared_against() -> Bool { + match spark_serving_usage_stats_standing() { + UsageStatsEnabledByDefault { basis: _ } => true + UsageStatsDisabledByLaunch { mechanism: _ } => false + UsageStatsLaunchUnread { obligation: _ } => false + } +} From ae905c87f1de0063ab5cdba0da0667365bb45cb4 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 21:16:38 +0000 Subject: [PATCH 07/11] Review 64043: the disable reading is upstream's, so it lives in extdeps spark_lane_disables_usage_stats asked whether a disable variable's value was anything other than "0". Upstream asks whether it EQUALS "1" -- os.environ.get("VLLM_NO_USAGE_STATS", "0") == "1", and DO_NOT_TRACK the same way. Those disagree on =false, =no, =0.0 and every other spelling a person would expect to mean off, and they disagree in the ADMITTING direction: the launch keeps reporting, the standing reads DisabledByLaunch, the telemetry path becomes ProviderPathAbsent, and the rostered rung drop's population evaporates under a route that is still sending. A machine claim authored in our layer instead of cited, failing clean. So the reading moves to extdeps.vllm.usage_stats, cited to envs.py, and the names move with it: a VllmUsageStatsDisableTerm is a variable AND the exact value that disables it, because separating them is what let the pair be recombined wrongly. vllm_usage_stats_assignment_disables performs the exact equality on both components -- no truthiness, no case folding, no "anything non-empty", each of which is a consumer's guess about a reading the upstream module can state. gunbc now supplies the launch's assignments and reads nothing into them. Upstream's third term, the marker file, is named where it is not folded: a container environment cannot answer whether a path exists in the image or the home directory, and its absence from the fold errs conservatively -- a fleet disabling reporting only by marker file reads as ENABLED, over-declaring the egress rather than hiding it. The honest closure is a filesystem observation, not a bolder predicate. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/extdeps/vllm/usage_stats.dag | 39 +++++++++++++++++++++++-- dag/gunbc/spark/first_party_serving.dag | 24 +++++++++------ 2 files changed, 52 insertions(+), 11 deletions(-) diff --git a/dag/extdeps/vllm/usage_stats.dag b/dag/extdeps/vllm/usage_stats.dag index f81bee167e0..68713d3cfc7 100644 --- a/dag/extdeps/vllm/usage_stats.dag +++ b/dag/extdeps/vllm/usage_stats.dag @@ -76,6 +76,30 @@ type VllmUsageStatsServiceJurisdiction = ServiceJurisdictionDocumented { jurisdiction: NonEmptyStr } | ServiceJurisdictionUndocumentedUpstream +// ── HOW UPSTREAM READS THE DISABLE VARIABLES, WHICH IS NOT "IS IT SET" ──────────────────────── +// +// THE NAMES ALONE WERE NOT THE FACT, and modelling only the names pushed the reading into the +// consumer, where it was authored rather than cited: gunbc asked whether an assignment's value was +// anything other than "0", and upstream asks whether it EQUALS "1" +// (os.environ.get("VLLM_NO_USAGE_STATS", "0") == "1", and DO_NOT_TRACK the same way, in envs.py). +// Those disagree on VLLM_NO_USAGE_STATS=false, =no, =0.0 and every other spelling a person would +// expect to mean off: upstream keeps reporting and the consumer read "disabled" -- the admitting +// direction, on a launch that is still sending (review 64043). +// +// So the reading lives here, once, with the names it belongs to. A term is a variable AND the exact +// value that disables it, because separating them is what let the pair be recombined wrongly. +type VllmUsageStatsDisableTerm { + variable: NonEmptyStr + disabling_value: NonEmptyStr +} + +// EXACT EQUALITY ON BOTH COMPONENTS, because that is what upstream performs. There is deliberately +// no truthiness, no case folding and no "anything non-empty": each of those is a consumer's guess +// about a reading this module can state. +fn vllm_usage_stats_assignment_disables(term: VllmUsageStatsDisableTerm, name: NonEmptyStr, value: String) -> Bool { + (name as String) == (term.variable as String) && value == (term.disabling_value as String) +} + type VllmUsageStatsReporting sole_constructor { default_server: NonEmptyStr server_override_env: NonEmptyStr @@ -83,7 +107,7 @@ type VllmUsageStatsReporting sole_constructor { content_class: VllmUsageStatsContentClass service_jurisdiction: VllmUsageStatsServiceJurisdiction collected_fields: List - disable_env_vars: List + disable_terms: List disable_marker_path: NonEmptyStr established_against: VllmSourceRevision } @@ -106,11 +130,22 @@ data vllm_usage_stats_reporting: VllmUsageStatsReporting = VllmUsageStatsReporti "gpu_memory_utilization", "quantization", "kv_cache_dtype", "enable_lora", "enable_prefix_caching", "enforce_eager", "disable_custom_all_reduce", ], - disable_env_vars: ["VLLM_NO_USAGE_STATS", "DO_NOT_TRACK"], + disable_terms: [ + VllmUsageStatsDisableTerm { variable: "VLLM_NO_USAGE_STATS", disabling_value: "1" }, + VllmUsageStatsDisableTerm { variable: "DO_NOT_TRACK", disabling_value: "1" }, + ], disable_marker_path: "~/.config/vllm/do_not_track", established_against: vllm_source_revision_read, } +// THE THIRD TERM OF UPSTREAM'S DISJUNCTION IS THE MARKER FILE, carried above as +// disable_marker_path and deliberately not folded by the launch standing below: a container +// environment cannot answer whether a path exists inside the image or the home directory, and +// guessing would be the same authored reading this module just moved out of the consumer. Its +// absence from the fold errs in the conservative direction -- a fleet that disabled reporting only +// by marker file reads as ENABLED here, which over-declares the egress rather than hiding it -- and +// the honest closure is a filesystem observation, not a bolder predicate. +// // REPORTING IS ON UNLESS SOMETHING TURNS IT OFF, which is the shape of the upstream check // (_USAGE_STATS_ENABLED = not (do_not_track or no_usage_stats or do_not_track_file)) and therefore // the shape of the question a consumer must ask about a particular launch. The arms are what a diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index bb5ae0b9701..3dd18dd26a6 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -22,7 +22,7 @@ import extdeps.vllm.usage_stats { VllmUsageStatsLaunchStanding, UsageStatsDisabledByLaunch, UsageStatsEnabledByDefault, UsageStatsLaunchUnread, VllmUsageStatsContentClass, ConfigurationAndHardwareMetadataOnly, CarriesRequestMaterial, - vllm_usage_stats_reporting, + vllm_usage_stats_reporting, vllm_usage_stats_assignment_disables, } import gunbc.spark.dgx_procurement { OperatorAllocation } import gunbc.fleet_physical_inventory { operator_site } @@ -373,7 +373,7 @@ fn spark_first_party_downstream() -> DownstreamProviderPopulation { // right to call the same defect this module fixes one function below for the content class: the // environment is a MODELED value in this repository, so a sentence about it is a second authority // that rots the moment somebody edits the first. It is folded now -- the observed lanes' container -// environments against extdeps.vllm.usage_stats' own disable_env_vars -- so adding +// environments against extdeps.vllm.usage_stats' own disable terms, read by that module -- so adding // VLLM_NO_USAGE_STATS=1 to the launch flips this standing, flips the telemetry path to // ProviderPathAbsent, and takes the rung drop's population out from under it, with no edit here. // @@ -384,14 +384,20 @@ fn spark_first_party_downstream() -> DownstreamProviderPopulation { // the check reading cleanest exactly where it knows least -- the same trap the host-coverage fold // avoids above. // -// A NAME SET TO "0" IS NOT A DISABLE. Upstream reads these as booleans, so a present-but-false -// assignment leaves reporting on; matching on the name alone would have read it as off. +// WHETHER AN ASSIGNMENT DISABLES ANYTHING IS UPSTREAM'S READING AND IS NOT PERFORMED HERE. The +// first spelling asked whether the value was anything other than "0"; upstream asks whether it +// EQUALS "1", so VLLM_NO_USAGE_STATS=false would have read as disabled while the engine kept +// reporting -- the admitting direction, on a launch still sending (review 64043). The predicate is +// now extdeps.vllm.usage_stats' own, cited to envs.py, and this module only supplies the launch's +// assignments to it. What is folded is the ENVIRONMENT terms; upstream's third term, the marker +// file, is not answerable from a container environment and its absence here over-declares the +// egress rather than hiding it. fn spark_lane_disables_usage_stats(lane: FabricLaneObserved) -> Bool { any( - vllm_usage_stats_reporting.disable_env_vars, - v => any( + vllm_usage_stats_reporting.disable_terms, + t => any( spark_pair_container_env(lane: lane), - e => (e.name as String) == (v as String) && e.value != "0", + e => vllm_usage_stats_assignment_disables(term: t, name: e.name, value: e.value), ), ) } @@ -404,11 +410,11 @@ fn spark_serving_usage_stats_standing() -> VllmUsageStatsLaunchStanding { } else { if count(filter(fabric_lane_observations, l => !spark_lane_disables_usage_stats(lane: l))) == 0 { UsageStatsDisabledByLaunch { - mechanism: "every observed fabric lane's serving container environment carries one of extdeps.vllm.usage_stats disable_env_vars with a value other than 0, so no lane reports usage statistics", + mechanism: "every observed fabric lane's serving container environment carries one of extdeps.vllm.usage_stats disable_terms at its disabling value, read by that module's own vllm_usage_stats_assignment_disables, so no lane reports usage statistics", } } else { UsageStatsEnabledByDefault { - basis: "at least one observed fabric lane's serving container environment (gunbc.spark.pair_serving_realization spark_pair_container_env) carries none of extdeps.vllm.usage_stats disable_env_vars, so usage reporting is on by upstream default for this route. Derived from the launch declaration, not from a reading of any running host's environment.", + basis: "at least one observed fabric lane's serving container environment (gunbc.spark.pair_serving_realization spark_pair_container_env) satisfies none of extdeps.vllm.usage_stats disable_terms, so usage reporting is on by upstream default for this route. Derived from the launch declaration, not from a reading of any running host's environment.", } } } From 122e36c88e0d8cbd464ece93385caa0afe9918f6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 21:48:30 +0000 Subject: [PATCH 08/11] Review 64068: restore the obligation the refusing arm cites, and regenerate the drop projection TWO MECHANICAL REPAIRS, ONE OF THEM ON THE ARM THAT MATTERS MOST. 1. THE CITATION ON THE FAIL-CLOSED ARM RESOLVED NOWHERE. spark_usage_stats_carrying_request_material_obligation was declared, then lost when the launch standing was rewritten into a fold, and the decl_ref to it survived the deletion. Review 64068 is right that this is worse than an ordinary broken reference: that arm is the one the rung drop's operator condition is declared to execute against -- the admission was granted ON the condition that the payload stay metadata-only -- so the single path where the condition discharges was the single path whose reference pointed at nothing. An auditor following the refusal out to the remedy would have landed nowhere on the day it fired. The row is back, naming both remedies: disable on the launch, which the standing folds and which turns the path Absent, or re-assess the posture with the operator. Every decl_ref in the three touched modules and the two witnesses was then swept against its target; no other unresolved citation. 2. THE GENERATED PROJECTION IS REGENERATED FROM ITS AUTHORITY. docs/design-rung-drops.md was stale from the moment the drop row landed, which is what both completed CI runs actually refused on -- generated-artifact drift, population=docs-projections -- while the floor lane itself passed. Regenerated through docs_projection_gate regen; the diff is +4 lines, exactly this row. NOTED FOR SOMEONE ELSE'S LANE: heal-generated-artifacts FAILED on both heads rather than repairing this drift, which is the job that exists to do exactly what this commit does by hand. If it is failing rather than healing, the next author to add a rung-drop row pays the same two cycles. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/spark/first_party_serving.dag | 10 ++++++++++ docs/design-rung-drops.md | 4 ++++ 2 files changed, 14 insertions(+) diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 3dd18dd26a6..1d3d77fea23 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -404,6 +404,16 @@ fn spark_lane_disables_usage_stats(lane: FabricLaneObserved) -> Bool { data spark_serving_usage_stats_unread_obligation: NonEmptyStr = "gunbc.spark.first_party_serving: no fabric lane is observed, so no serving container environment exists to read and whether vLLM's usage-stats reporter is disabled on this fleet is unknown. Read the lanes (gunbc.spark.fabric_switch_observed fabric_lane_observations) before this route's telemetry path can be resolved." +// THE OBLIGATION THE REQUEST-MATERIAL ARM NAMES, AND IT MUST EXIST FOR THAT ARM TO BE WORTH +// ANYTHING. It was declared, then lost in the rewrite that moved the launch standing to a fold, and +// the citation survived it -- so the one path where the rung drop's operator condition is +// discharged pointed at nothing, and an auditor following the refusal out to the remedy would have +// landed nowhere (review 64068). It is a row rather than a sentence at the arm because what the +// refusal asks for is a re-assessment of the route, not a smaller repair: a reporter carrying +// request material is route material leaving the site, which is the premise the first-party posture +// rests on. +data spark_usage_stats_carrying_request_material_obligation: NonEmptyStr = "extdeps.vllm.usage_stats vllm_usage_stats_reporting now reports CarriesRequestMaterial at its cited source revision, so vLLM's usage-stats reporter no longer carries only host, build and engine configuration. The first-party posture rests on route material staying on site and this is route material leaving it, so the route's telemetry path is unresolved and provider-use admission refuses as ProviderRouteFactsIncomplete. The remedies: set VLLM_NO_USAGE_STATS=1 or DO_NOT_TRACK=1 on the serving launch (gunbc.spark.pair_serving_realization spark_pair_container_env), which this module's launch standing folds and which turns the path Absent; or re-assess the posture with the operator, whose 2026-09-11 ruling admitted this path ON the condition that the payload stay metadata-only." + fn spark_serving_usage_stats_standing() -> VllmUsageStatsLaunchStanding { if count(fabric_lane_observations) == 0 { UsageStatsLaunchUnread { obligation: spark_serving_usage_stats_unread_obligation } diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 3dbc62281da..755c1fe6d0f 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -182,6 +182,10 @@ the harness seat pool ceiling per serving group: an operator-chosen count standi two of the six priced axes for a serving offer -- operating and opportunity -- answered with asserting arms from facts this repository has not observed, so that an admission-only placement can reach a priced selector: RUNG DROP, structurally guaranteed -> mitigatable (deleted without replacement). Population: gunbc.serving.turn_admission serving_operating_cost (returns OperatingCostBorneBySupplier for a group whose operating cost is ours and unmeasured; the fail-closed arm OperatingCostUnread is reachable and refuses), gunbc.serving.turn_admission serving_opportunity_cost (returns NoFeasibleAlternativeUse from gauges that establish no running turn and cannot enumerate competing fabric demands; the fail-closed arm AlternativeUseUnread is reachable and refuses). Restored when: a selection policy instantiation exists that decides an admission-only placement from what such a placement knows -- fungibility, admission, quality-seat availability and the equal-cost tie policy -- and refuses to require any economic axis its caller did not observe, so that serving placement no longer routes through the priced selector's cost axes and these two functions have no question left to answer. A measured operating cost for a serving group does NOT discharge this row on its own: it leaves the opportunity axis asserted, and it leaves an admission-only placement answering a pricing question it has no standing to answer. +### one ProviderPathLocated whose jurisdiction upstream does not document, admitted rather than refused because the path carries no route material, with the unread fact reachable from the cited field and not from the arm — declared 2026-09-11 + +one ProviderPathLocated whose jurisdiction upstream does not document, admitted rather than refused because the path carries no route material, with the unread fact reachable from the cited field and not from the arm: RUNG DROP, structurally guaranteed -> mitigatable (deleted without replacement). Population: gunbc.spark.first_party_serving spark_usage_stats_telemetry_path (returns ProviderPathLocated whose jurisdiction cites extdeps.vllm.usage_stats vllm_usage_stats_reporting service_jurisdiction, a field whose value is ServiceJurisdictionUndocumentedUpstream; the fail-closed arm ProviderPathUnread is reachable from the same fold and refuses the route). Restored when: product.fabric.provider_route ProviderPathStanding carries a jurisdiction standing SUFFICIENT FOR a located path to declare its jurisdiction unread without the whole path becoming unread -- so that a consumer matching the located arm can see which of its three components were established -- and gunbc.spark.first_party_serving's telemetry path states the fact in its arm. Reading who operates the usage-stats service does NOT discharge this row: it fills one slot on one route and leaves every other located path with an undocumented counterparty in the same unexpressible position. + ### a serving offer's identity and its post-acquisition fence are the metrics-exporting process, so an engine-core or rank replacement behind a surviving exporter keeps the offer identity, its readiness evidence and its fence — declared 2026-09-08 a serving offer's identity and its post-acquisition fence are the metrics-exporting process, so an engine-core or rank replacement behind a surviving exporter keeps the offer identity, its readiness evidence and its fence: RUNG DROP, structurally guaranteed -> mitigatable (deleted without replacement). Population: gunbc.spark.serving_offer spark_serving_offer_key (the exporting process's key standing as the complete SupplierOffer identity), gunbc.harness.harness_seat harness_fence_grant (the post-acquisition re-read, which compares the exporter's launch and therefore cannot see an engine replacement beneath it). Restored when: a launch receipt read from the running engine joins the metrics-exporting process to the engine-core incarnation and its rank population, so that the offer identity and the post-acquisition fence both name the incarnation that will execute the turn. An observation of the exporting process alone does NOT discharge this row: that is what stands today, and it is what lets a seat taken against one engine authorize a request against its replacement. From 7290a908d64db8aa8155b9f5c57ad17e14e3716c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 22:00:34 +0000 Subject: [PATCH 09/11] The site join is a belief, and the allocation now says so Operator, asked directly on 2026-09-11: he BELIEVES operator-lab is his NYC apartment and does not actually know. The allocation was writing that join as settled -- "it names the site the corpus already carries" -- which is the exact overstatement this module exists to prevent, one level up from the one it was written to catch. Two facts now, separated. ASSERTED: every Spark unit sits at the operator's NYC home, outside the rack, as of this date. NOT ESTABLISHED: that the site identity the corpus already carries names that same place. The keying does not change and does not need to: reusing operator_site is still right (minting a second SiteIdentity for one place is the section 3 failure gunbc.fleet_site_locale already records being made and reverted), the route's region cites the allocation, and the allocation states both halves. Confirmation is an address tagged to this site identity, which belongs in the private fleet records rather than this repository -- named as the remedy, with no address and no private reference carried here. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/spark/first_party_serving.dag | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 1d3d77fea23..2e1259efe71 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -51,9 +51,19 @@ import gunbc.fleet_intent_network { // THE SITE IS NOT MINTED HERE, AND THAT IS THE SECOND HALF OF THE POINT. The operator's premises // already have one authority -- gunbc.fleet_physical_inventory operator_site -- and // gunbc.fleet_site_locale records that minting a second SiteIdentity for this exact place was -// already done once and reverted as the section 3 nickname failure. The operator's 2026-09-11 -// assertion NAMES that site (his NYC home) and scopes every Spark unit to it; it does not introduce -// a place the corpus did not already carry. The NEARBY NAME THAT IS NOT THIS ONE: +// already done once and reverted as the section 3 nickname failure. So the allocation is keyed on +// that identity rather than on a new one. +// +// AND THE JOIN TO THE OPERATOR'S HOME IS A BELIEF, NOT A CONFIRMED FACT, which is recorded rather +// than smoothed over because this whole module exists to keep an assertion from reading as a +// measurement. Asked directly on 2026-09-11, the operator said he BELIEVES operator-lab is his NYC +// apartment and does not actually know. What IS asserted is where the units sit -- his NYC home, +// outside the rack -- and what is NOT established is that the site identity the corpus already +// carries names that same place. Nothing here depends on closing that gap: the route's region cites +// the allocation, and the allocation states both halves. Confirmation is an address tagged to this +// site identity, which belongs in the private fleet records and not in this repository. +// +// THE NEARBY NAME THAT IS NOT THIS ONE: // gunbc.spark.serving_deployment_selection serving_topology_region is a Pareto DecisionRegion -- a // region of a decision field, not a place a machine sits. @@ -81,7 +91,7 @@ data spark_fleet_site_allocation: SparkFleetSiteAllocation = SparkFleetSiteAlloc allocation: OperatorAllocation { decided_by: "operator (2026-09-11): 'srv5, 6, and all the sparks sit outside the rack right now, but in my NYC home'", decided_on: "2026-09-11", - basis: "The operator asserts that every Spark unit sits at his NYC home, outside the rack, as of this date. This is an ATTRIBUTABLE ASSERTION and not a measurement: for hardware the operator owns and holds there is no third party to observe the site, so no observer can exist and none is claimed. It names the site the corpus already carries as gunbc.fleet_physical_inventory operator_site, whose civil zone gunbc.fleet_site_locale already records as America/New_York, rather than introducing a second name for one place. It is explicitly NOT a colocation facility: no row of extdeps.colo.interserver or any other extdeps.colo operator describes where these units sit. RIGHT NOW is part of the assertion -- the units are expected to move into the rack later, and that move is a NEW allocation row carrying its own date, never an edit to this one.", + basis: "The operator asserts that every Spark unit sits at his NYC home, outside the rack, as of this date. This is an ATTRIBUTABLE ASSERTION and not a measurement: for hardware the operator owns and holds there is no third party to observe the site, so no observer can exist and none is claimed. IT IS KEYED ON THE SITE IDENTITY THE CORPUS ALREADY CARRIES -- gunbc.fleet_physical_inventory operator_site, whose civil zone gunbc.fleet_site_locale records as America/New_York -- rather than introducing a second name for one place. WHAT IS NOT ESTABLISHED, asked and answered on the same date: the operator BELIEVES operator-lab is his NYC apartment and does not know it, so the join between that site identity and the home named in the assertion is a belief and is not confirmed here. Confirming it means tagging an address to this site identity, which belongs in the private fleet records rather than this repository. It is explicitly NOT a colocation facility: no row of extdeps.colo.interserver or any other extdeps.colo operator describes where these units sit. RIGHT NOW is part of the assertion -- the units are expected to move into the rack later, and that move is a NEW allocation row carrying its own date, never an edit to this one.", }, } @@ -268,7 +278,7 @@ data spark_sanctions_not_engaged: UseProgramStanding = UseProgramStanding { data spark_export_not_engaged: UseProgramStanding = UseProgramStanding { program: "export control", engagement: "NOT ENGAGED under first-party self-use. This is NOT an export determination, classification or licence finding.", - basis: "Nothing leaves gunbc and nothing crosses a national boundary on this route: the units sit at one site, the operator's NYC home (gunbc.spark.first_party_serving spark_fleet_site_allocation), and the turns begin and end inside gunbc. With no transfer and no recipient there is no export to classify, so the program has no subject here. It acquires one the moment the posture is superseded by serving anyone else or by placing a unit outside that site.", + basis: "Nothing leaves gunbc and nothing crosses a national boundary on this route: the units sit at ONE site, which the operator states is his NYC home (gunbc.spark.first_party_serving spark_fleet_site_allocation, which also records what about that site is believed rather than confirmed), and the turns begin and end inside gunbc. With no transfer and no recipient there is no export to classify, so the program has no subject here. It acquires one the moment the posture is superseded by serving anyone else or by placing a unit outside that site.", } fn spark_prohibited_use_disposition() -> DispositionStanding { From 5bf3568453fa7a3854e08c705efbce395b2ee3cf Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 22:22:22 +0000 Subject: [PATCH 10/11] Review 64100: the export basis outran the egress this PR itself models The export and sanctions bases were written before the telemetry path was modelled and never revisited, so they said "nothing leaves gunbc", "no transfer", "no recipient", "nothing is made available to any party outside gunbc" -- while three functions later this module admits a Located path to a third-party service with a jurisdiction upstream does not document. A permit's own evidence contradicting the route facts it was minted against is the exact class this PR exists to close, and it was sitting in the rows written to close it. Both are narrowed to what is true rather than deleted, and the egress is named in each rather than omitted: EXPORT. No ROUTE MATERIAL leaves and none crosses a border -- prompts, responses and weights begin and end inside gunbc at one site. What does leave is host, build and engine-configuration metadata from vLLM's usage-stats reporter, cited to extdeps.vllm.usage_stats and to this module's own telemetry path and its declared drop. That egress carries no request content, so it is not route material; the row does not claim it was classified. SANCTIONS. No good, service or route material is supplied to any party outside gunbc, so there is no counterparty to screen. The reporter is an emission to a recipient rather than a supply to a counterparty, and it is named as such. Prohibited use is unchanged and needs no carve-out: a telemetry recipient is not a user whose use could be governed. Each row now states the condition that would give it a subject, and both conditions are executed elsewhere in the module rather than promised -- a turn served to anyone else refuses as CustomerScopeUnsupported, and a reporter that ever carries request material refuses through the telemetry fold. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/spark/first_party_serving.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 2e1259efe71..26fd4d7d2c5 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -272,13 +272,13 @@ data spark_prohibited_use_not_engaged: UseProgramStanding = UseProgramStanding { data spark_sanctions_not_engaged: UseProgramStanding = UseProgramStanding { program: "sanctions", engagement: "NOT ENGAGED under first-party self-use. This is NOT a sanctions determination and no screening was performed against any list.", - basis: "Nothing is supplied, sold or made available to any party outside gunbc on this route: the turn is served on operator-owned hardware at the operator's own site to gunbc itself. With no counterparty there is no party to screen, so the program has no subject here. It acquires one the moment gunbc.spark.first_party_serving spark_first_party_use_posture is superseded by serving anyone else, at which point this row no longer describes the route.", + basis: "NO GOOD, SERVICE OR ROUTE MATERIAL IS SUPPLIED TO ANY PARTY OUTSIDE gunbc ON THIS ROUTE: the turn is served on operator-owned hardware at the operator's own site to gunbc itself, so there is no counterparty to a supply and therefore no party to screen. THE ONE THING THAT REACHES A THIRD PARTY IS NAMED RATHER THAN GLOSSED: vLLM's usage-stats reporter emits host, build and engine-configuration metadata to a service upstream publishes the address of and nothing else about (extdeps.vllm.usage_stats; carried as this route's telemetry path in gunbc.spark.first_party_serving spark_usage_stats_telemetry_path). That is an emission to a recipient, not a supply of anything to a counterparty, it carries no request content, and no screening was performed against any list -- this row records that the program has no subject under first-party self-use, not that anybody was cleared. It acquires a subject the moment a turn is served to anyone else." } data spark_export_not_engaged: UseProgramStanding = UseProgramStanding { program: "export control", engagement: "NOT ENGAGED under first-party self-use. This is NOT an export determination, classification or licence finding.", - basis: "Nothing leaves gunbc and nothing crosses a national boundary on this route: the units sit at ONE site, which the operator states is his NYC home (gunbc.spark.first_party_serving spark_fleet_site_allocation, which also records what about that site is believed rather than confirmed), and the turns begin and end inside gunbc. With no transfer and no recipient there is no export to classify, so the program has no subject here. It acquires one the moment the posture is superseded by serving anyone else or by placing a unit outside that site.", + basis: "NO ROUTE MATERIAL LEAVES gunbc AND NONE CROSSES A NATIONAL BOUNDARY, and the scope of that sentence is the point of it. The turns -- the prompts, the responses, the weights they run against -- begin and end inside gunbc on units at one site, which the operator states is his NYC home (gunbc.spark.first_party_serving spark_fleet_site_allocation). With no transfer of route material and no recipient of it, there is no export of it to classify. WHAT DOES LEAVE, STATED HERE RATHER THAN OMITTED because a basis that ignored it would be contradicted by this module's own route facts: vLLM's usage-stats reporter sends host, build and engine-configuration metadata to a third-party service whose jurisdiction upstream does not document (extdeps.vllm.usage_stats, and gunbc.spark.first_party_serving spark_usage_stats_telemetry_path, which carries that path as Located with an unread jurisdiction under the declared drop gunbc.rung_drop.provider_path_jurisdiction_unread_admits). That egress carries no request content, so it is not route material and not what an export determination of this route's serving would be about -- and this row does not claim it was classified. It acquires a subject the moment either half changes: route material leaving, or that reporter carrying request material, which this module's telemetry fold refuses on." } fn spark_prohibited_use_disposition() -> DispositionStanding { From 07549412170772b201035515549fe834280c00ef Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 11 Sep 2026 22:47:07 +0000 Subject: [PATCH 11/11] Review 64115: delete an import naming a symbol its module does not carry extdeps.docker does not declare DockerEnvAssignment -- extdeps.docker.cli does -- and the import was unused besides: the fold reads e.name and e.value off the values spark_pair_container_env returns and never names the type. So the import is deleted rather than repointed. This is the ordinary compiler floor (names resolve), which DESIGN 4b puts below every differentiating claim, so it is worth the push on its own. Swept every import in the seven touched files against its defining module at the same time; the two remaining flags are artifacts of the sweep rather than defects -- String is a kernel type declared in a map, and FabricGroupA is an arm of a single-line coproduct. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WT6FDJa7Nyh9SJv25sM1Ui --- dag/gunbc/spark/first_party_serving.dag | 1 - 1 file changed, 1 deletion(-) diff --git a/dag/gunbc/spark/first_party_serving.dag b/dag/gunbc/spark/first_party_serving.dag index 26fd4d7d2c5..3009d0b5a3e 100644 --- a/dag/gunbc/spark/first_party_serving.dag +++ b/dag/gunbc/spark/first_party_serving.dag @@ -15,7 +15,6 @@ import product.fabric.provider_admission { RouteScopeSanction, ProviderUseScope, ProviderUseAdmission, DispositionStanding, DispositionNotEngaged, admit_provider_use, } -import extdeps.docker { DockerEnvAssignment } import gunbc.spark.fabric_switch_observed { FabricLaneObserved, fabric_lane_observations } import gunbc.spark.pair_serving_realization { spark_pair_container_env } import extdeps.vllm.usage_stats {