diff --git a/dag/extdeps/vllm/usage_stats.dag b/dag/extdeps/vllm/usage_stats.dag new file mode 100644 index 00000000000..68713d3cfc7 --- /dev/null +++ b/dag/extdeps/vllm/usage_stats.dag @@ -0,0 +1,157 @@ +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 + +// ── 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 + local_copy_path: NonEmptyStr + content_class: VllmUsageStatsContentClass + service_jurisdiction: VllmUsageStatsServiceJurisdiction + collected_fields: List + disable_terms: 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_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 +// 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/harness/harness_seat.dag b/dag/gunbc/harness/harness_seat.dag index 4627078c021..69afe82fcb9 100644 --- a/dag/gunbc/harness/harness_seat.dag +++ b/dag/gunbc/harness/harness_seat.dag @@ -3,7 +3,7 @@ module gunbc.harness.harness_seat import std.types { String, Bool, Int, NonEmptyStr, List, EpochSecs } import std.nat { Nat, nat_range_inclusive, nat_min } import std.measure { Measure, Count, One, money_amount_micro } -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.serving.serving_enrollment { ServingRoute, ServingRouteResolved, ServingRouteUnresolved, ServingRouteEndpoint, ServingRouteTurnCeiling, serving_enrolled_routes, serving_route_turn_ceiling_count, @@ -434,17 +434,20 @@ 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. // // THE CAPABILITY IS THE REQUIREMENT'S, NOT THE OBSERVED MODEL'S, and the two are reconciled before // this is reached rather than here: the observed unit has already been checked against the @@ -452,7 +455,10 @@ fn harness_no_candidate(acc: HarnessCandidates, note: String, retryable: Bool) - // route satisfies what the demand asked for -- and keeps the offer and the demand comparable by the // equality the fabric uses. // -// 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, endpoint: ServingRouteEndpoint, launch: VllmEndpointProcessLaunch, standing: HarnessBackendStanding, requirement: ServingModelRequirement, seats: Nat, now: EpochSecs) -> HarnessCandidates { match bind_spark_serving_offer( principal: "gunbc" as NonEmptyStr, @@ -463,7 +469,7 @@ fn harness_bind_candidate(acc: HarnessCandidates, group: FabricGroup, endpoint: isolation: serving_isolation_profile(), seats: seats as Int, readiness: harness_serving_readiness(standing: standing, 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) @@ -472,7 +478,7 @@ fn harness_bind_candidate(acc: HarnessCandidates, group: FabricGroup, endpoint: 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/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/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 new file mode 100644 index 00000000000..3009d0b5a3e --- /dev/null +++ b/dag/gunbc/spark/first_party_serving.dag @@ -0,0 +1,541 @@ +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, 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 { + RouteScopeSanction, ProviderUseScope, ProviderUseAdmission, + DispositionStanding, DispositionNotEngaged, admit_provider_use, +} +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, + ConfigurationAndHardwareMetadataOnly, CarriesRequestMaterial, + vllm_usage_stats_reporting, vllm_usage_stats_assignment_disables, +} +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. 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. + +// 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 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.", + }, +} + +// ── 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 +// 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. +// +// 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 +} + +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. 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.", +} + +// 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, 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)), +} + +// ── 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 IS 'NOT ENGAGED' RATHER THAN 'CLEARED' ─────────────── +// +// 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. +// +// 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 + 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: "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: "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 { + DispositionNotEngaged { + basis: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_prohibited_use_not_engaged"), + } +} + +fn spark_sanctions_disposition() -> DispositionStanding { + DispositionNotEngaged { + basis: decl_ref(module_path: "gunbc.spark.first_party_serving", decl_name: "spark_sanctions_not_engaged"), + } +} + +fn spark_export_disposition() -> DispositionStanding { + DispositionNotEngaged { + basis: 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. 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 { + 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: EIGHT PATHS AT THE SITE, AND ONE THAT LEAVES IT ────────────────────────── +// +// 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 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(), + 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"), + } +} + +// ── 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. +// +// 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 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. +// +// 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. +// +// 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_terms, + t => any( + spark_pair_container_env(lane: lane), + e => vllm_usage_stats_assignment_disables(term: t, name: e.name, value: e.value), + ), + ) +} + +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 } + } 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_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) 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.", + } + } + } +} + +fn spark_usage_stats_telemetry_path() -> ProviderPathStanding { + 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"), + } + } + } +} + +// 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(), + 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_usage_stats_telemetry_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..be157b4c116 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,7 +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, spark_site_uncovered_units, +} import gunbc.spark.vllm_endpoint_process_launch { VllmEndpointProcessLaunch, vllm_endpoint_process_launch_key, } @@ -109,18 +114,74 @@ 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 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" -fn spark_serving_route_standing() -> SparkServingRoute { - ServingRouteRegionUnobserved { obligation: spark_serving_route_region_obligation } +// 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 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, + } + } + } } type SparkOfferBinding

@@ -159,8 +220,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 +259,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 +274,5 @@ fn bind_spark_serving_offer

( launch: launch, }, } - } } } 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 new file mode 100644 index 00000000000..326361c95e6 --- /dev/null +++ b/dag/test/claim/spark/spark_first_party_serving_witness_test.dag @@ -0,0 +1,168 @@ +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, + DispositionStanding, DispositionCleared, DispositionNotEngaged, + 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, +} + +// 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, 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 } => + 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) + } +} + +// 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" + } +} + + +// 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 + } +} 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..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.decl_ref { decl_ref } +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, @@ -14,8 +16,9 @@ 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, + spark_serving_route_hosts_unreadable_obligation, bind_spark_serving_offer, } @@ -85,15 +88,54 @@ 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 { - match spark_serving_route_standing() { +// 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(hosts: [operator_host_srv5, operator_host_srv6]) { + ServingRouteRegionUnobserved { obligation: _ } => false ServingRouteObserved { route: _ } => false + 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" + } +} + + +// 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_region_obligation as String) + (o as String) == (spark_serving_route_hosts_unreadable_obligation as String) } } 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.