The KV pool is read back, and a computed one needs a log line beside it

[gunbai-bot]

What this lands

Two extdeps/vllm/ modules and one witness module, for the pool-as-observed parse.

extdeps.vllm.log_lines cites three vLLM startup lines by prefix, not by position, each carrying the revision it was read at. extdeps.vllm.kv_cache carries the KV pool as an observation, refuses both arithmetic reconstructions of it, and binds the pool to the line class it is read from.

Why the pool is observed and never computed

The pool is a residual of large numbers — the memory budget minus the weights minus a profiled activation peak minus a cudagraph reservation. Every term but the first is measured by the engine after it loads, so small argument changes move the result by multiples rather than percentages: a utilization step of a few points moved it several-fold, and adding one batching argument cut it by two thirds. A quantity with that shape cannot be predicted from the arguments.

So VllmPoolReconstruction has two arms — BlockCountTimesBlockSize and UtilizationTimesTotalMemory — and vllm_pool_reconstruction_is_authoritative answers false for both. num_gpu_blocks * block_size is wrong under MLA with the DeepSeek fp8 layout by roughly an order of magnitude, in the direction that looks plausible. It is a typed refusal rather than a warning because it was computed twice, the second time by someone who knew better: the failure isn't ignorance of the rule, it's that the arithmetic is available and reads like a derivation.

There is no interpolation function anywhere. Two points do not establish a shape.

The line class is bound by construction

An earlier head of this PR had a real defect, found by exact-head review 5117692079: VllmObservedKvPool required a captured_line, but it was any NonEmptyStr, and a separate zero-argument helper returned GpuKvCacheSize. The two never met, so this typechecked:

vllm_observed_kv_pool(tokens: …, captured_line: "Maximum concurrency for 262,144 tokens: 9.81x")

The pool carried a line without carrying the KV-cache-size line — and the witness that appeared to cover it proved only that the disconnected helper returned the enum value it was written to return. Permanently green, and cited as coverage.

Pool construction now consumes a typed reading:

vllm_observed_kv_pool_from_reading(tokens, reading: VllmStartupReading) -> VllmKvPoolAdmission

  GpuKvCacheSize        -> KvPoolAdmitted, carrying the reading's own captured_text and revision
  MaximumConcurrency    -> KvPoolRefused { ReadingIsNotTheKvCacheSizeLine { line } }
  ResolvedKvCacheFormat -> KvPoolRefused { ReadingIsNotTheKvCacheSizeLine { line } }

The revision travels from the reading rather than being re-stamped at the call, because re-stamping would launder a stale observation as current. Both older functions are deleted, not kept beside this one — an unchecked constructor next to a checking one makes the refusal satisfiable by calling the other function.

What is guaranteed, and what is not

STRUCTURAL   no pool without a VllmStartupReading, and none from either non-KV line class
MITIGATABLE  agreement between the authored TokenCount and the count the captured text reports

A genuine KV-cache-size line paired with a wrong number is admitted and this module does not detect it. That is stated in the module itself rather than softened, because no row in the battery goes red for a mismatched number. The next-rung trigger is named: a parser under gunbc.spark.serving_readback_parse producing both halves, so neither is authorable independently.

Evidence, executed

8 property rows plus the aggregate — 9/9 PASS. Two of the rows could not exist against the previous shape:

w_the_concurrency_line_refuses_rather_than_becoming_a_pool     the case that used to typecheck
w_the_resolved_format_line_refuses_rather_than_becoming_a_pool  so admission is keyed on BEING the
                                                                kv-cache-size line, not on not being
                                                                the concurrency line

The positive row asserts the reading's text survives into the pool; without that conjunct it would be satisfied by a constructor that accepted the reading and dropped it, which is what the deleted one effectively did. The cap/pool row consumes an admitted pool and returns false on Absent rather than substituting a placeholder.

🤖 Generated with Claude Code

https://claude.ai/code/session_01U397y4s3dSBof7vGPAX87G

[briansrls]

REQUEST_CHANGES on exact head a11eb53.

The central cut is accepted. VllmObservedKvPool requires a token count, captured text, and revision; both arithmetic reconstructions are explicitly non-authoritative; the two reconstruction arms are witnessed separately; cap/pool observations carry utilization and expose no interpolation function; and the startup vocabulary is keyed by stable prefixes rather than stream positions. Exact-head run 33913757864 is terminal success, all required lanes are green, and GitHub reports the PR mergeable/clean.

One structural connection is missing, and the current witness overclaims it. VllmObservedKvPool carries only captured_line: NonEmptyStr; neither the carrier nor vllm_observed_kv_pool carries/consumes a VllmStartupLine or VllmStartupReading. vllm_observed_kv_pool_line() is a free zero-argument helper returning GpuKvCacheSize, disconnected from every pool construction. Therefore a caller can construct a pool from the MaximumConcurrency or resolved-format captured text and the program still typechecks. w_the_pool_is_read_from_the_kv_cache_size_line proves only that the free helper returns the desired enum; it remains green if every real pool is built from the wrong startup line. Its annotation's claim that a future parser cannot bind the concurrency line and still typecheck is false on this head.

The final property row has the same seam in miniature: w_a_cap_pool_pair_carries_its_utilization_and_its_source_line checks only utilization and max_model_len; it never inspects the pool's captured text or source-line class.

Repair at the source/observation seam, not by strengthening prose. Acceptable narrow shapes include: (1) make the pool consume a typed VllmStartupReading and narrow/refuse unless its line is GpuKvCacheSize; or (2) introduce a specialized KV-cache-size reading minted by that narrowing and make the pool consume it. Then make the witnesses construct a pool, prove a KV-cache-size reading admits, prove the other startup-line classes refuse, and inspect the source carried by the cap/pool observation. The token/text agreement may honestly remain authorable until the named stdout parser exists; this finding is only that the line class currently is not connected at all.

No objection to the observed-not-derived policy, reconstruction refusals, absence of interpolation, three-file scope, or current CI. No merge authorization on this head.

Superseded by source and witness changes on exact head c3a9dc0; replacing with an exact-head review.

[briansrls]

REQUEST_CHANGES on exact head c3a9dc0.

The implementation blocker from review 5117692079 is discharged. vllm_observed_kv_pool_from_reading now consumes VllmStartupReading, admits only GpuKvCacheSize, and returns a typed refusal carrying the supplied line class for both MaximumConcurrency and ResolvedKvCacheFormat. The admitted arm carries the reading's own captured_text and observed_at_revision; it does not re-stamp the revision at pool conversion. Both former escape hatches—the free (TokenCount, NonEmptyStr) constructor and the disconnected zero-argument line helper—are gone. The positive witness inspects the surviving source text, both non-KV line classes have refusing rows, the cap/pool row follows the admitted arm rather than fabricating an Absent placeholder, and the explicit aggregate calls all eight property rows. No behavioral change remains requested.

Two evidence-prose blockers remain.

1. The source still opens this section with THE POOL IS OBSERVED, AND THE CARRIER IS SHAPED SO THAT A COMPUTED ONE CANNOT BE WRITTEN, and the following paragraph calls that MECHANICALLY PREVENTABLE. That is broader than the graph. The constructor still accepts an independently authored TokenCount, and the same file correctly says an author can pair a real KV-cache-size reading with a wrong number. What is mechanically prevented here is construction from no typed reading or from a reading classified as either non-KV line; numerical agreement between tokens and captured_text remains mitigatable until the named stdout parser exists. Narrow the heading/rung sentence to that exact line-class guarantee. No parser or logic expansion is requested.

2. The canonical PR body still reports 6 property rows plus the aggregate PASS. This head carries eight property rows plus the aggregate, 9/9 in the reported local run, including the two new non-KV-line refusals. Update the body to describe the typed-reading admission and the current 8+aggregate evidence; once CI terminates, bind the exact-head result to this SHA/run rather than retaining the prior head's evidence count.

Exact-head run 33918777721 names c3a9dc0 and is nonterminal. GitHub currently reports the PR open and mergeable. No merge authorization until the source claim is scoped truthfully, the body is current, a replacement exact-head review is filed, and terminal exact-head CI succeeds.