Stage 1 of the serving extraction: what the observer may read from vLLM, and when it must refuse

dag/extdeps/vllm/engine_args.dag

@@ -76,10 +76,25 @@ fn vllm_distributed_executor_backend_wire(backend: VllmDistributedExecutorBacken
   }
 }
 
-// THE ARGUMENTS A LAUNCH ACTUALLY CARRIES. `max_num_batched_tokens` is deliberately ABSENT from this
-// record rather than present-and-optional: see the do-not-set row below, which is a typed refusal
-// subject and not a comment.
+// THE PREFILL SCHEDULING AXIS, WHICH IS A REQUEST AND NOT AN EFFECTIVE VALUE.
+//
+// A launch that omits `--max-num-batched-tokens` has NOT thereby chosen a value. This build resolves
+// the default from device memory, usage context, parallel configuration and performance mode, and
+// then adjusts it again when chunked prefill is off -- so the absence of the flag determines nothing
+// a consumer may read. `none` below means UNREQUESTED, and the effective budget is knowable only by
+// reading it back off the running engine.
+type ChunkedPrefillRequest
+  = ChunkedPrefillRequested
+  | ChunkedPrefillNotRequested
+
+type VllmPrefillSchedulingPolicy {
+  max_num_batched_tokens: TokenCount
+  chunked_prefill: ChunkedPrefillRequest
+}
+
+// THE ARGUMENTS A LAUNCH ACTUALLY CARRIES.
 type VllmEngineArgs {
+  prefill_scheduling: VllmPrefillSchedulingPolicy?
   tensor_parallel_size: Nat
   gpu_memory_utilization: VllmMemoryUtilization
   max_model_len: TokenCount
@@ -127,16 +142,28 @@ type VllmDiscouragedArg {
   ground: NonEmptyStr
 }
 
-data vllm_discouraged_max_num_batched_tokens: VllmDiscouragedArg = VllmDiscouragedArg {
-  arg: "--max-num-batched-tokens" as NonEmptyStr,
-  ground: "on a unified-memory GB10 this only reduces the KV pool; prefill is compute-bound so a larger batch buys no throughput" as NonEmptyStr
-}
+// WITHDRAWN 2026-09-07. This row said `--max-num-batched-tokens` "only reduces the KV pool; prefill
+// is compute-bound so a larger batch buys no throughput", and both halves are now unsupported.
+//
+// The batch budget is the per-iteration token budget the scheduler divides between decode and
+// prefill, so it participates in a LATENCY/FAIRNESS tradeoff whatever it does to aggregate
+// throughput: a co-tenant's next decode token cannot appear until the current mixed step finishes.
+// A measured comparison on this fleet -- the same decode taking 3.8s alone and 63.5s beside a cold
+// prefill -- is a serving result the old ground did not account for.
+//
+// And "prefill is compute-bound" was never established here. It was inferred from average link
+// utilisation (~7.9 Gb/s of 50 Gb/s during a cold prefill), and low AVERAGE bandwidth is equally
+// consistent with latency-bound collectives, one-rank stragglers, or host gaps between kernels.
+// Bulk transfer time is a lower bound on communication cost, not a share of the critical path.
+//
+// It is deliberately NOT replaced with a recommended value. The honest state is an unresolved policy
+// axis whose selection needs a step-level trace this repository does not yet capture, and encoding a
+// number here would be the same mistake in the other direction.
 
 data vllm_verified_negatives: List<VllmVerifiedNegative> = [
   vllm_negative_nvfp4_kv_for_mla,
   vllm_negative_dcp_with_sliding_window,
 ]
 
 data vllm_discouraged_args: List<VllmDiscouragedArg> = [
-  vllm_discouraged_max_num_batched_tokens,
 ]

dag/extdeps/vllm/log_lines.dag

@@ -71,13 +71,23 @@ type VllmStartupReading sole_constructor {
   observed_at_revision: VllmSourceRevision
 }
 
+// THE REVISION IS OBSERVED, NOT STAMPED. This constructor used to fill observed_at_revision from
+// vllm_source_revision_read, the constant naming the revision the LAWS were read from -- so every
+// reading asserted it had been taken at the modelled revision no matter which build produced it,
+// and the field the carrier's own note calls load-bearing could not disagree with the model. Every
+// downstream revision comparison was therefore permanently green: not a weak wall, a decoration.
+//
+// A reading is evidence about the build that emitted it, so the caller that captured the text
+// supplies the revision it captured it from. Agreeing with the modelled revision is then a real
+// question a consumer can ask and get "no" to.
 fn vllm_startup_reading(
   line: VllmStartupLine,
   captured_text: NonEmptyStr,
+  observed_at_revision: VllmSourceRevision,
 ) -> VllmStartupReading {
   VllmStartupReading {
     line: line,
     captured_text: captured_text,
-    observed_at_revision: vllm_source_revision_read
+    observed_at_revision: observed_at_revision
   }
 }

dag/gunbc/guarantee_stall/probe_program_assembled_from_string_literals_stall.dag

@@ -0,0 +1,36 @@
+module gunbc.guarantee_stall.probe_program_assembled_from_string_literals_stall
+
+import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed }
+import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation, climbs_when }
+
+// gunbc.instruments.fabric_capacity_standing capacity_probe_script builds an eleven-field bash
+// program by joining String literals -- command substitutions, pipelines, sed and grep -oE scripts,
+// and a per-field default -- and group_report ships it to `ssh ... bash -s` as a stdin payload.
+//
+// THE DEFECT IS NOT THAT IT IS SHELL. docs/plans/shell-to-dag-residual-census-and-arc-completion.md
+// splits the remaining arc in two, and a probe executed on a foreign host over SSH falls in its
+// LEGITIMATE SHELL bucket: foreign executors stay shell. But that same finding says legitimate shell
+// is "emitted through the v2 bash rows (grammar-owned), and is bounded", and this program is neither
+// -- it is assembled by string concatenation, so no grammar row describes it and nothing in the
+// substrate can read it. ROADMAP's translator row names exactly this population as what it deletes:
+// "the scripts assembled by gluing strings together".
+//
+// WHY IT IS A LADDER ROW AND NOT ONLY UNTIDINESS. Every field this probe returns is an input to a
+// capacity standing, and the program that produces them is opaque to the compiler: a quoting defect,
+// a pipeline that silently yields empty, or a sed expression that stops matching after an upstream
+// format change all reduce to the field's `-` default. The instrument then reports an unestablished
+// standing rather than a wrong number, which is the correct failure -- so this sits at mitigatable
+// rather than lower -- but the class of defect is invisible to every check the substrate can run,
+// and it stays invisible until the program has a grammar.
+//
+// It is declared here because the census that owns the class does not name this instance: the
+// document is dated 2026-07-12 against #6507 and predates this module, so without a row the
+// instance is an untracked member of a known population.
+data probe_program_assembled_from_string_literals_stall: GuaranteeStall = GuaranteeStall {
+  subject: "gunbc.instruments.fabric_capacity_standing capacity_probe_script assembles an eleven-field bash program from String literals and ships it to ssh bash -s, so no grammar row describes the program and no substrate check can read it",
+  current: Mitigatable,
+  ceiling: StructurallyGuaranteed,
+  blocker: AwaitsOneGrounding { grounding: "docs/plans/shell-to-dag-residual-census-and-arc-completion.md" },
+  population: BoundedPopulation { members: ["gunbc.instruments.fabric_capacity_standing"] },
+  next_rung_trigger: climbs_when(capability: "one translator that turns a described plan into a shell program while preserving order, captured output and failure behaviour, sufficient to express this probe's command substitutions, pipelines, per-field default and remote stdin delivery, so that the program is grammar-owned and no consumer assembles one by joining String literals")
+}

dag/gunbc/guarantee_stall/roster.dag

@@ -59,6 +59,8 @@ import gunbc.guarantee_stall.testgen_anchor_generator_totality_stall { testgen_a
 import gunbc.guarantee_stall.synthesis_established_bound_patch_stall { synthesis_established_bound_patch_stall }
 import gunbc.guarantee_stall.fn_index_depth_agreement_floor_enrollment_stall { fn_index_depth_agreement_floor_enrollment_stall }
 import gunbc.guarantee_stall.eval_steps_outside_the_reading_coproduct_stall { eval_steps_outside_the_reading_coproduct_stall }
+import gunbc.guarantee_stall.signed_and_ratio_measure_carrier_stall { signed_and_ratio_measure_carrier_stall }
+import gunbc.guarantee_stall.probe_program_assembled_from_string_literals_stall { probe_program_assembled_from_string_literals_stall }
 
 // THE COHORT PROVENANCE NOTES BELOW WERE AUTHORED WHEN EVERY ROW SAT IN ONE FILE, and they are
 // carried here verbatim rather than split across the row modules they describe. Their membership
@@ -213,6 +215,8 @@ data all_guarantee_stalls: List<GuaranteeStall> = [
   synthesis_established_bound_patch_stall,
   fn_index_depth_agreement_floor_enrollment_stall,
   eval_steps_outside_the_reading_coproduct_stall,
+  signed_and_ratio_measure_carrier_stall,
+  probe_program_assembled_from_string_literals_stall,
 ]
 
 // THE FOUR SUBJECTS RESTORED TO THE ROSTER, PINNED BY IDENTITY SO THEIR LOSS REFUSES.

dag/gunbc/guarantee_stall/signed_and_ratio_measure_carrier_stall.dag

@@ -0,0 +1,53 @@
+module gunbc.guarantee_stall.signed_and_ratio_measure_carrier_stall
+
+import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed }
+import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation, climbs_when }
+
+// WHY THIS ROW EXISTS RATHER THAN A FOURTH REVIEW ROUND. Three reviews in succession flagged the
+// unit-modeling class across gunbc.spark.serving_critical_path. Most of it was a real fork and is
+// now migrated: started_micros, elapsed_micros, four inter-iteration millis, wall_micros across
+// twenty-four sample rows, and two watt fields all consume std.measure.
+//
+// Three fields did not migrate, and leaving them as bare Int with no row is precisely what the
+// third review objected to -- not the Int, but the SILENCE. DESIGN 4b(2) says a class below its
+// ceiling must name its next-rung trigger, and 4b(3) says a rung may be lowered only by declaring
+// it. An undeclared Int beside a migrated Microsecond in the same record is an unstated divergence.
+//
+// WHAT ACTUALLY BLOCKS EACH ONE. Three different carrier gaps, not one:
+//
+//   intercept_micros             a fit intercept, computed by division, may be negative
+//   intercept_difference_micros  a difference of two intercepts, signed by construction
+//   micros_per_thousand_tokens   a RATE: microseconds per token
+//   milli_tokens_per_second      a rate at MILLI scale, in gunbc.spark.serving_step_cost
+//   gigabits_per_second_tenths   a link throughput reading
+//   link_gigabits                the link's rated throughput
+//
+// SIGNED. Microsecond is Measure<Time, Micro, Nat>, Nat-backed, so it cannot hold either of the two
+// signed values, and std.measure declares no signed duration alias.
+//
+// QUOTIENT. micros_per_thousand_tokens is a dimensional quotient. std.measure publishes
+// measure_add, measure_le, measure_count and two scale-fraction folds -- no product, no quotient,
+// and no composition on the Quantity type -- so a microseconds-per-token carrier cannot be spelled.
+//
+// SCALE. milli_tokens_per_second is a rate at milli scale. TokensPerSecond is Measure<Frequency,
+// One, Nat>, and its module states the reason the milli scaling exists: rounding a sub-unit rate to
+// an integer would report zero. Migrating to the One-scaled alias would erase the distinction the
+// field was created to preserve, so this needs Measure<Frequency, Milli, Nat> and no alias exists.
+//
+// AND ONE IS BLOCKED BY A FORK RATHER THAN AN ABSENCE, which is the worst of the four. The two RoCE
+// fields would take std.measure Bandwidth = Measure<DataRate, One, Nat>, and std.measure's own
+// comment beside MegatransfersPerSecond declares DataRate to be bits/s. Its live consumers do not
+// agree with that or with each other: extdeps.systems.nvidia records the GB10's 273 GB/s memory
+// bandwidth as bandwidth(count: 273000000000), which is bytes per second, while extdeps.colo
+// natcoweb records colo transit ports as bandwidth(count: 1000000) and bandwidth(count: 10000000),
+// which are neither. Three consumers, at least two mutually inconsistent readings of one carrier's
+// base unit. Joining that carrier would make these rows a THIRD reading and cement the fork, so they
+// stay declared here until the base unit has one answer.
+data signed_and_ratio_measure_carrier_stall: GuaranteeStall = GuaranteeStall {
+  subject: "unit fields across gunbc.spark.serving_critical_path and gunbc.spark.serving_step_cost carry bare Nat or Int beside migrated Watt, Hertz, Percent, Milliwatt and Microsecond fields in the same records, because std.measure has no signed duration alias, no dimensional quotient, no milli-scaled frequency alias, and no agreed base unit for Bandwidth",
+  current: Mitigatable,
+  ceiling: StructurallyGuaranteed,
+  blocker: AwaitsOneGrounding { grounding: "std.measure" },
+  population: BoundedPopulation { members: ["gunbc.spark.serving_critical_path", "gunbc.spark.serving_step_cost"] },
+  next_rung_trigger: climbs_when(capability: "std.measure carries a signed duration magnitude, a dimensional quotient with the arithmetic to inhabit it, a milli-scaled frequency alias, and one adjudicated base unit for DataRate that every live Bandwidth consumer is migrated onto, sufficient to express a fit intercept computed by division, a signed difference of two intercepts, a microseconds-per-token rate, a sub-unit token rate, and a link throughput without any consumer unwrapping to a bare scalar to do so")
+}