M4.5 - Decode Attention Kernels, Mask Programs, and Backend Boundaries

0x00 Historical Introduction And Owner Contract

The owner question is:

When query length collapses to one, which axis can a kernel parallelize, how are partial softmax states recombined exactly, and how do masks, K/V layout, GQA, and framework dispatch constrain the implementation that actually runs?

This is not a minor epilogue to FlashAttention-2. It is the point where the shape of autoregressive inference invalidates the most abundant work axis used by prefill and training kernels.

prefill or training attention:
    Q [B, S_q, H_q, d_h], S_q >> 1
    many query tiles can own independent output rows

ordinary one-token decode:
    Q       [B, 1, H_q, d_h]
    K_cache [B_cache, T_capacity, H_kv, d_h] or paged equivalent
    V_cache [B_cache, T_capacity, H_kv, d_h] or paged equivalent
    one new row attends over T visible historical positions

The logical attention equation has not changed. The materialized schedule, available parallel axes, persistent state, and runtime admission contract have. That distinction is the historical thread of this article.

0x00A From IO-Aware Attention To A Decode-Specific Schedule

The attention-kernel sequence is best read as a sequence of bottleneck discoveries, not as one universal upgrade ladder:

Stage	Problem made explicit	Durable mechanism	What remains unresolved here
Online softmax	a stable denominator need not require separate maximum and normalization passes	carry a running maximum and rescaled denominator	does not choose GPU work owners
FlashAttention-1	materializing S = QK^T and P = softmax(S) creates avoidable HBM traffic	tile attention and carry exact row state on chip	the paper schedule is not automatically optimal for every shape
FlashAttention-2	non-matmul work and output ownership can leave hardware underused	expose query-block parallelism and remove a cross-warp output reduction	query-block parallelism collapses when S_q becomes one or a few
Flash-Decoding	one short query still reads a long K/V history	partition the K/V sequence, emit partial row states, then reduce them	split count, temporary state, reduction cost, cache layout, and masks become runtime contracts
FlashMask and programmable-mask systems	a dense mask can erase the IO benefit of tiled attention	encode legal score regions compactly and classify tiles	representability and phase-specific backend support must be proven
Serving attention engines	one mathematical call maps to many cache and kernel implementations	plan by shape, cache ABI, hardware, and feature set	an API name does not prove which backend executed

The first three stages are derived in M4.3 and M4.4. This article starts at the fourth stage. The 2023 Flash-Decoding design exposed cached-sequence partitions as new workers and added a reduction that preserves the global softmax. Later work did not merely make that one schedule faster: FlashDecoding++ changed softmax and flat-GEMM scheduling, LeanAttention treated online-softmax combination as a stream-K-style reduction, FlashInfer made ragged and paged serving plans explicit, and FlexDecoding compiled score modifications into a short-query backend. Their benchmark numbers are source-reported coordinates, not a timeless ranking.

FlashMask is another branch, not “Flash-Decoding with masks.” It asks whether a mask can be encoded compactly enough to classify an attention tile as fully allowed, fully masked, or partial. Its primary paper evaluates long-context training and post-training workloads. This article therefore owns the mask representation and kernel-classification contract while refusing to treat that evidence as proof of one-token decode acceleration.

0x00B Thesis: Decode Attention Is A Contract Stack

“FlashAttention is enabled” is not a complete claim. A decode result crosses six separately auditable contracts:

semantic contract:
    visible positions, causal alignment, score modifiers, and all-masked rows
    define the intended output

state contract:
    every split exports enough information to reconstruct one global softmax

ownership contract:
    query heads, K/V heads, sequence partitions, and reduction workers have
    explicit producer and consumer sets

address contract:
    logical token positions map to valid contiguous rows or physical pages

launch contract:
    split count, workspace, resources, waves, and reduction overhead fit the
    actual batch and context distribution

dispatch contract:
    the loaded framework build admits the call to a compatible kernel, and a
    diagnostic or profiler trace proves the path that ran

The unit of analysis is therefore not a method name. It is one complete decode coordinate:

(implementation revision, device, dtype,
 B, S_q, visible S_k, H_q, H_kv, d_h,
 mask program, cache layout, append mode,
 split policy, workspace policy, graph mode,
 selected backend and kernel symbol)

Changing any coordinate may preserve mathematical attention while selecting a different schedule, allocating different temporary state, or rejecting the requested backend.

0x00C Consumes, Owns, And Defers

Relationship	Contract
Consumes from M4.1	FLOP, byte, arithmetic-intensity, numerator, duration, and evidence-coordinate accounting.
Consumes from M4.2	grid, CTA, occupancy, wave, synchronization, launch-overhead, and profiler vocabulary.
Consumes from M4.3	safe/online softmax, exact row-state coordinates, tiled attention, and logical-versus-measured traffic.
Consumes from M4.4	FA2 query-row ownership, GQA head mapping, causal alignment, and the measured boundary where query parallelism collapses.
Owns in M4.5	one/few-query decode geometry; K/V-axis splitting; exact partial-state reduction including empty partitions; split temporary-state and reduction traffic; decode-specific GQA work sharing; read-side contiguous, ragged, and paged cache addressing; mask-program representation and tile classification; backend admission and runtime proof.
Defers to M4.6	FA3/FA4 producer-consumer pipelines, TMA/WGMMA/TMEM details, precision modes, and architecture-specific pipeline schedules.
Defers to M5.1-M5.3	request lifecycle, cache reservation, scheduler policy, block allocation, page-table mutation, prefix ownership, eviction, and offload. M5.2 owns repeated work selection; M4.5 consumes the resulting frozen microbatch and read-side cache ABI.
Defers to M5.7-M5.8	model-level MQA/GQA conversion, quality trade-offs, tensor-parallel cache placement, MLA projection absorption, and latent-cache architecture.
Defers to M8.6, M8.9, and M8.10	KV quantization, deployment-wide kernel packaging, compatibility qualification, release, and rollback policy.

This boundary prevents two common forms of duplication. M4.5 may derive how a decode kernel reads a block table, but it does not redesign the allocator that produced it. It may map query heads to shared K/V heads, but it does not repeat the model-conversion and quality analysis owned by M5.7.

0x00D Phase Contract

Phase	Query surface	State interaction	M4.5 treatment
Training forward/backward	many query rows	saved or recomputed differentiation state	comparison boundary only; M4.3-M4.4 own the main derivation
Prefill	many prompt rows	constructs prompt K/V state	used when a mask or backend contract is primarily prefill-facing
Chunked verification	a few query rows	reads history and may stage several new rows	included as a few-query sensitivity, not silently relabeled one-token decode
One-token decode	one query row per active sequence	reads visible K/V and may append one new row	primary kernel owner

Claim Status And Source Discipline

Status	Meaning
Source-local	Preserved from A19, especially its Flash-Decoding and FlashMask explanatory sequence or figure inventory. Source-local does not mean externally correct.
Externally verified	Checked against a versioned primary paper, author engineering note, official repository, or official framework documentation.
Version-scoped implementation	A claim about named files or behavior at one pinned repository commit. It is not projected onto historical or future releases.
Synthetic contract test	An executable oracle or estimator validates algebra, indexing, or accounting on declared fixtures. It is not GPU performance evidence.
Source-reported measurement	A benchmark is preserved with the source’s hardware, software, shapes, numerator, and baseline. It is not a current ranking.
Rewrite interpretation	A derived systems explanation connecting tensor shape, work ownership, masks, cache layout, and backend dispatch.
Unmeasured	No local build, dispatch diagnostic, profiler capture, or timing distribution supports the claim yet.

The immutable source and figure coordinates live in:

docs/numinens-evidence/m4-5-decode-kernel-boundaries/source_manifest.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/figure_manifest.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/article_contracts.json

Those manifests separate four objects that prose often conflates:

paper claim
historical or current source observation
repository-authored reconstruction
local runtime measurement

No local GPU build, selected-kernel trace, or timing sample is claimed in this loop. The source pins are study coordinates only.

0x00E Background Knowledge: Decode Trades Query Parallelism For Persistent History

During prefill, a request contributes many query rows. During ordinary autoregressive decode, it contributes one new query row while retaining a long K/V history. The computation remains exact attention, but the useful work axes change.

Splitting the key sequence can recover parallelism. Each worker computes a partial online-softmax state:

local maximum:
    stabilizes scores in one allowed key partition

local exponential sum:
    records that partition's softmax denominator

local weighted value sum:
    records its unnormalized output contribution

validity or empty-state marker:
    distinguishes a partition with no allowed scores from an ordinary finite
    partition before any -inf - -inf arithmetic occurs

Those states must be merged with an exact common-reference rule before final normalization. Section 0x02 derives the identity, closure, commutativity, and associativity contracts and will state the all-masked-row output policy. Later loops then bind the algebra to K/V addresses, GQA ownership, mask programs, launch geometry, and the backend that actually executes.

0x01 Why The Query Axis Collapses

For prefill, a common conceptual work grid is:

grid_prefill ~= B * H_q * ceil(S_q / B_q)

where B_q is the number of query rows owned by one work unit.

At decode, S_q = 1:

grid_decode_without_split ~= B * H_q

The arithmetic has not disappeared. Each query head still reads a long K/V history and computes:

$$s_t = \frac{q_tK_{1:T}^{\mathsf T}}{\sqrt{d_h}}, \qquad o_t = \operatorname{softmax}(s_t)V_{1:T}.$$

Renderer-safe form:

scores [B, H_q, 1, T] = q @ K_cache^T / sqrt(d_h)
output [B, H_q, 1, d_h] = softmax(scores) @ V_cache

The shape has become asymmetric:

small side:
    one query row

large side:
    T cached key rows
    T cached value rows

If B * H_q is too small to occupy the device, the kernel needs another independent axis. The available large axis is the cached sequence:

grid_decode_with_kv_split
    ~= B * H_q * num_kv_splits

This creates more work units, but it also creates a new correctness problem. Every split sees only part of the softmax row, so no split owns the global denominator.

Source: PyTorch, Flash-Decoding for long-context inference, unnumbered official animation. The reduced-motion source is a repository-extracted static frame from the same animation. The split boundaries expose more parallel work; the final result still requires the log-sum-exp-aware reduction derived next. The figure does not identify a current kernel, split heuristic, local runtime path, or measured speedup, and no general reuse license is claimed.

0x02 Exact Split-State Algebra And Reduction Contract

M4.3 derived the generic online-attention state. Decode adds a specific partition contract: several workers summarize disjoint K/V index ranges for one query row, a mask can remove every logical position from a physical range, and a later operation must recover the same row that unsplit attention would produce.

The reduction proof therefore starts from sets, not kernel names.

0x02A One K/V Partition Has A Canonical Allowed-Set Summary

Let C_c be the physical indices owned by split c, and let A_c be the indices in that split that remain visible after causal, padding, window, or application masking:

$$A_c = \{j \in C_c : j\text{ is allowed for this query row}\}.$$

For a non-empty allowed set, define:

$$m(A_c) = \max_{j \in A_c} s_j,$$ $$l(A_c) = \sum_{j \in A_c} e^{s_j-m(A_c)},$$ $$u(A_c) = \sum_{j \in A_c} e^{s_j-m(A_c)}v_j.$$

The canonical split summary is:

$$\Sigma(A_c) = (\nu_c,m_c,l_c,u_c),$$

where valid = nu_c records whether A_c is non-empty. u_c is a vector with width d_h; it is not yet divided by l_c.

Renderer-safe state contract:

A_c = physical split indices that survive the row mask

if A_c is non-empty:
    state(A_c) = (valid=true, m_c, l_c, u_c)
    m_c = max_{j in A_c} score[j]
    l_c = sum_{j in A_c} exp(score[j] - m_c)
    u_c = sum_{j in A_c} exp(score[j] - m_c) * value[j]

The executable oracle also carries count_c = |A_c| as test metadata. A production kernel does not need that field if validity and all other ownership invariants are available.

Three distinctions matter:

physical split:
    address range assigned to one work unit

allowed set:
    positions in that range that survive the mask

split state:
    sufficient statistic of the allowed scores and values

An overlapping partition violates the contract because a K/V position would be counted twice. An uneven or empty partition does not violate it.

0x02B The Binary Merge Moves Both States Into One Exponential Frame

Take two disjoint, non-empty allowed sets A and B. Their local maxima need not match. Choose the merged maximum:

$$m = \max(m_A,m_B).$$

For a score in A, factor its globally shifted exponential through m_A:

$$e^{s_j-m} = e^{s_j-m_A}e^{m_A-m}.$$

The same factorization holds for B. Define the frame-conversion factors:

$$\alpha = e^{m_A-m}, \qquad \beta = e^{m_B-m}.$$

Then the denominator over the union is:

$$l = \sum_{j\in A\cup B}e^{s_j-m} = \alpha l_A + \beta l_B,$$

and the unnormalized value accumulator is:

$$u = \sum_{j\in A\cup B}e^{s_j-m}v_j = \alpha u_A + \beta u_B.$$

The non-empty merge is therefore:

$$(\nu_A,m_A,l_A,u_A)\oplus(\nu_B,m_B,l_B,u_B) = (\text{true},m,\alpha l_A+\beta l_B,\alpha u_A+\beta u_B).$$

The final row is obtained only after all split states have been merged:

$$O = \frac{u}{l}, \qquad \operatorname{LSE}=m+\log l.$$

Renderer-safe non-empty merge:

m = max(m_A, m_B)
alpha = exp(m_A - m)
beta  = exp(m_B - m)
l = alpha * l_A + beta * l_B
u = alpha * u_A + beta * u_B
O = u / l
LSE = m + log(l)

This is why a split kernel cannot return only its normalized output. The reducer must know each split’s relative partition mass.

0x02C Empty And Fully Masked Splits Need An Executable Identity

A physical split can have no valid logical position. Common causes include:

num_splits exceeds the visible tail length
a ragged request ends before this split
a causal or local window masks the entire split
an application mask removes every position in the tile

The canonical empty summary is:

$$\mathbf{e}=(\text{false},-\infty,0,\mathbf{0}).$$

But the tuple alone is not sufficient implementation guidance. Directly applying the non-empty formula to two empty states forms -inf - -inf, which is NaN. The reducer must branch on validity before exponential arithmetic:

EMPTY = (False, -inf, 0.0, zeros(d_h))

def merge_state(a, b):
    if not a.valid:
        return b
    if not b.valid:
        return a

    m = max(a.m, b.m)
    alpha = exp(a.m - m)
    beta = exp(b.m - m)
    return State(
        valid=True,
        m=m,
        l=alpha * a.l + beta * b.l,
        u=alpha * a.u + beta * b.u,
    )

This makes the identity laws executable:

$$\mathbf{e}\oplus\Sigma(A)=\Sigma(A), \qquad \Sigma(A)\oplus\mathbf{e}=\Sigma(A), \qquad \mathbf{e}\oplus\mathbf{e}=\mathbf{e}.$$

If every split is empty, the row is all-masked. This article and its oracle declare the following output policy:

all-masked row:
    O = zero_vector(d_h)
    LSE = -inf

The observed FlashAttention interface documents a zero output for all-masked rows. That does not make this policy universal across every framework or backend; an integration must record the selected API’s all-masked-row contract.

0x02D Closure, Commutativity, And Associativity Follow From Set Union

The shortest reliable proof is to show that the merge recovers the canonical summary of a union.

For disjoint allowed sets A and B, Section 0x02B established:

$$\Sigma(A)\oplus\Sigma(B)=\Sigma(A\cup B).$$

That equality gives four properties in exact arithmetic.

Closure. The merge result has the same state type and summarizes another allowed set:

$$\Sigma(A)\oplus\Sigma(B)\in\mathcal{S}.$$

Identity. The empty state summarizes the empty set:

$$\Sigma(\varnothing)=\mathbf{e}.$$

Because A union empty = A, the explicit empty branches implement both identity directions.

Commutativity. Set union and the denominator/numerator sums do not depend on operand order:

$$\Sigma(A)\oplus\Sigma(B) = \Sigma(A\cup B) = \Sigma(B\cup A) = \Sigma(B)\oplus\Sigma(A).$$

Associativity. Both parenthesizations summarize the same union:

$$(\Sigma(A)\oplus\Sigma(B))\oplus\Sigma(C) = \Sigma(A\cup B\cup C) = \Sigma(A)\oplus(\Sigma(B)\oplus\Sigma(C)).$$

These are statements about the mathematical reduction target. Floating-point addition is not associative, so a concrete kernel can produce small tree-dependent differences. Section 0x02H makes that boundary explicit.

0x02E Partition Invariance Is The Decode Correctness Contract

Let the visible K/V indices for one query row be A, partitioned into pairwise-disjoint sets:

$$A=\biguplus_{c=1}^{n} A_c.$$

Repeated closure and associativity give:

$$\bigoplus_{c=1}^{n}\Sigma(A_c)=\Sigma(A).$$

Therefore, in exact arithmetic, the result is independent of:

where physical split boundaries fall
whether the tail split is shorter
how many mask-created empty states occur
the order in which split states are reduced
whether the reduction tree is sequential or balanced

This is the correctness permission that allows decode kernels to expose the cached-sequence axis for parallelism. It does not say every split count has the same performance, temporary traffic, or numerical error.

The proof has one important precondition: the A_c sets must be disjoint and cover A exactly. Missing positions lose probability mass; duplicated positions count probability mass twice.

0x02F A Normalized Partial Output Needs LSE, Not Averaging

Some implementations store (m,l,u). Others normalize each partial numerator and store:

$$O_A=\frac{u_A}{l_A}, \qquad L_A=m_A+\log l_A.$$

For two valid output states, choose a stable pivot:

$$p=\max(L_A,L_B),$$

and recover the union log-partition:

$$L = p+\log\left(e^{L_A-p}+e^{L_B-p}\right).$$

The normalized output is then:

$$O=e^{L_A-L}O_A+e^{L_B-L}O_B.$$

The two coefficients sum to one in exact arithmetic because L is the log of the combined partition function. Empty output states still require explicit validity branches.

Renderer-safe (LSE, O) merge:

if A is empty: return B
if B is empty: return A

p = max(LSE_A, LSE_B)
LSE = p + log(exp(LSE_A - p) + exp(LSE_B - p))
O = exp(LSE_A - LSE) * O_A + exp(LSE_B - LSE) * O_B

Why Averaging Partial Outputs Fails

Use two scalar-value splits:

split A scores: [10, 10]
split A values: [1, 1]

split B scores: [0, 0]
split B values: [100, 100]

Each local softmax is uniform, so:

O_A = 1
O_B = 100
naive average = 50.5

But LSE_A = 10 + log(2) and LSE_B = log(2). The exact global output is:

O = 1.0044943890

Almost all probability mass belongs to split A. The normalized vectors alone discarded the evidence needed to know that.

0x02G Worked Three-Split Trace With An Empty Middle Split

The executable fixture worked_empty_middle uses a two-dimensional value vector:

scores:
    [4, -1 | masked, masked | 3, -2, 1]

values:
    [[1, 0], [0, 2]
     [99, 99], [-99, -99]
     [2, 3], [-1, 4], [4, -2]]

The masked values are deliberately large. They must have no effect because the middle allowed set is empty.

The float64 oracle summarizes the three splits as:

split 0:
    valid = true
    m_0 = 4
    l_0 = 1.0067379469990854
    u_0 = [1.0, 0.013475893998170934]

split 1:
    valid = false
    m_1 = -inf
    l_1 = 0
    u_1 = [0, 0]

split 2:
    valid = true
    m_2 = 3
    l_2 = 1.142073230235698
    u_2 = [2.5346031859473657, 2.7562812215231167]

Merging split 0 with the empty identity leaves split 0 unchanged. Merging split 2 moves it from maximum 3 into the global maximum frame 4, so its scale is exp(-1):

m = 4
l = 1.4268832087150578
u = [1.9324284036376742, 1.0274550894834356]
O = [1.3543003322450418, 0.7200695075868776]
LSE = 4.355492491217523

The unsplit dense reference gives the same output to floating-point tolerance. Sequential, balanced, and permuted float64 split reductions also agree to at most 3.34e-16 in the fixture report.

0x02H Finite Precision Changes Reduction Order, Not The Target

The algebra above uses exact real arithmetic. A kernel uses finite accumulators, approximate exponentials, and a concrete reduction topology. Consequently:

mathematical contract:
    all legal partitions and trees summarize the same visible set

implementation result:
    different legal trees may round differently

The synthetic sensitivity fixture uses four equal scores with scalar values:

[2048, 1, -2048, 1]

The exact numerator is 2 and the exact output is 0.5. In the oracle’s round-after-operation float16 model:

sequential original order -> output 0.25
balanced original order   -> output 0.25
permuted order            -> output 0.50
order spread              -> 0.25

This deliberately adversarial fixture proves that exact-arithmetic associativity cannot be promoted into a bitwise floating-point guarantee. It is not a claim about a measured CUDA kernel.

A runtime contract must decide which promise it makes:

accuracy contract:
    compare against an unsplit reference under declared dtype-specific tolerances

determinism contract:
    freeze split count, reduction tree, kernel family, and relevant runtime controls

performance contract:
    tune split count and tree shape under the same semantic and accuracy gates

0x02I Executable Oracle And Failure Closure

The article’s algebra is bound to standard-library evidence:

fixture:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/split_state_fixture.json

oracle:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/split_state_oracle.py

generated report:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/split_state_report.json

tests:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_split_state_oracle.py

The fixtures cover empty identity, all-masked rows, ragged empty tails, uneven tails, extreme scores, (m,l,u) versus (LSE,O), local-output averaging failure, and reduction-order sensitivity. They are Synthetic contract tests, not profiler or throughput evidence.

Failure	Invalid implementation	Observable consequence	Required closure
Empty-state arithmetic	Evaluate exp(-inf - -inf)	NaN state	Branch on validity before arithmetic
Missing visible position	Split union does not cover the allowed set	Lost probability mass	Validate exact coverage
Overlapping splits	Same K/V index appears in two states	Duplicated probability mass	Require disjoint ownership
Average local outputs	Reduce O_c without LSE_c	Wrong cross-split weighting	Carry (m,l,u) or (LSE,O)
Commit arbitrary tree as bitwise truth	Treat exact associativity as floating associativity	Backend- or split-dependent drift	Declare tolerance and determinism contracts
Unspecified all-masked behavior	Divide an empty numerator by an empty denominator	NaN or backend mismatch	Declare output and LSE policy

0x03 Split Tensor Shapes, Storage, Traffic, Tails, Dtypes, And Launch Ownership

Section 0x02 proved what every split must summarize. This section asks what that proof costs once states become tensors in a two-stage decode schedule.

The official Flash-Decoding explanation describes separate partial-attention and reduction kernels. That is the historical contract used here. Current backends may fuse work, use persistent execution, or choose a different workspace ABI, so every grid below is labeled a teaching launch model, not a claim about a selected runtime kernel.

0x03A Start With A Ragged GQA Decode Call

Use two requests whose visible context lengths differ:

B = 2
H_q = 8
H_kv = 2
T_b = [4096, 3587]
d_h = d_v = 128
S = num_splits = 8
S_capacity = 8

Q       [2, 8, 1, 128]       bf16
K_cache ragged logical rows   bf16
V_cache ragged logical rows   bf16
O       [2, 8, 1, 128]       bf16

Four query heads share one K/V head:

$$g = \frac{H_q}{H_{kv}} = 4, \qquad h_{kv}(h_q)=\left\lfloor\frac{h_q}{g}\right\rfloor.$$

Renderer-safe GQA ownership:

group_size = H_q / H_kv = 4
kv_head(q_head) = floor(q_head / 4)

query heads 0..3 -> K/V head 0
query heads 4..7 -> K/V head 1

The query head remains the output owner. Sharing a K/V head does not mean the four query heads have the same scores or partial states.

0x03B Split Bounds Must Be Derived Per Request

A single global T / S is insufficient for ragged requests. The split-launch fixture uses a balanced quotient/remainder policy for each request b:

$$q_b=\left\lfloor\frac{T_b}{S}\right\rfloor, \qquad r_b=T_b\bmod S.$$

Split s receives:

$$n_{b,s}=q_b+\mathbf{1}[s<r_b].$$

Its half-open bounds are:

$$\operatorname{start}_{b,s}=s q_b+\min(s,r_b),$$ $$\operatorname{end}_{b,s}=\operatorname{start}_{b,s}+n_{b,s}.$$

This gives disjoint exact coverage:

$$[0,T_b)=\biguplus_{s=0}^{S-1} [\operatorname{start}_{b,s},\operatorname{end}_{b,s}).$$

For the fixture:

request 0, T_0 = 4096:
    split lengths = [512, 512, 512, 512, 512, 512, 512, 512]

request 1, T_1 = 3587:
    q_1 = 448
    r_1 = 3
    split lengths = [449, 449, 449, 448, 448, 448, 448, 448]

Two other policies are valid design choices:

Policy	Configuration	Tail behavior	Runtime consequence
Balanced split count	choose S, derive quotient/remainder	lengths differ by at most one	stable owner count; per-request bounds
Fixed chunk width	choose C, derive ceil(T_b/C)	final chunk is shorter	owner count varies with context
Capacity envelope	allocate/launch S_capacity >= S	inactive ids produce identity states	graph-stable shapes; extra initialization and reduction slots

The article uses the first policy for ordinary ragged rows and the third for its fixed-capacity failure case. A backend may choose another policy, but it must still satisfy the coverage and disjointness preconditions from Section 0x02E.

0x03C Producer And Reducer Ownership Are Different Grids

The conceptual producer owner is:

(batch b, query head h_q, launch split id s)

The conceptual reducer owner is:

(batch b, query head h_q)

With split capacity S_capacity, their teaching-grid sizes are:

$$G_{producer}=B H_q S_{capacity},$$ $$G_{reducer}=B H_q.$$

For the main fixture:

producer grid = [2, 8, 8] -> 128 conceptual owners
reducer grid  = [2, 8]    -> 16 conceptual owners

each reducer consumes 8 split states
non-empty binary merges = 16 * (8 - 1) = 112

The producer’s K/V address path is:

(b, q_head, split_id)
    -> kv_head(q_head)
    -> request-local [start, end)
    -> cache layout address mapping
    -> K/V rows

The final physical cache mapping is deferred to Section 0x04 and M5.3. Section 0x03 owns the logical owner and range before that address translation.

One conceptual owner is not necessarily one CUDA CTA in every implementation. Alternatives include:

one CTA per split state
multiple CTAs cooperating on one split
one persistent CTA processing several split tasks
a fused or cooperative reduction
a planned serving kernel that assigns work dynamically

The invariant is ownership of one disjoint score/value subset and one destination state slot, not a universal launch geometry.

0x03D The Algebra Determines The Workspace Tensor Shapes

For the (m,l,u) state from Section 0x02, a structure-of-arrays teaching layout is:

partial_u     [B, H_q, S, d_v]
partial_m     [B, H_q, S]
partial_l     [B, H_q, S]
partial_valid [B, H_q, S]

For the main call:

partial_u     [2, 8, 8, 128] fp32
partial_m     [2, 8, 8]      fp32
partial_l     [2, 8, 8]      fp32
partial_valid [2, 8, 8]      uint8

The normalized output-state alternative is:

partial_O     [B, H_q, S, d_v]
partial_LSE   [B, H_q, S]
partial_valid [B, H_q, S]

The official Flash-Decoding description uses partial attention values plus log-sum-exp. The (m,l,u) form remains useful because it mirrors the proof and avoids normalizing each split before storage. They are equivalent mathematical ABIs under Section 0x02F, but their stored dtypes and byte costs can differ.

An explicit validity byte is an article/oracle choice. A backend may encode emptiness through LSE = -inf or another sentinel. It still needs a control-flow path that prevents empty arithmetic.

Logical shape is not always allocation shape:

logical workspace:
    [B, H_q, S, d_v]

capacity workspace:
    [B, H_q, S_capacity, d_v_padded]

d_v_padded:
    round_up(d_v, vector_alignment_elements)

The estimator’s allocation envelope includes split capacity and vector-lane padding. It deliberately excludes allocator pages, tensor-base alignment, cache lines, and backend-private metadata.

0x03E Derive Temporary Storage From The ABI

Define:

N_cfg = B * H_q * S
N_cap = B * H_q * S_capacity

b_u     = bytes per stored partial numerator/output element
b_state = bytes per scalar maximum, denominator, or LSE
b_valid = bytes per explicit validity field

The configured logical (m,l,u) payload is:

$$M_{mlu}^{logical} = N_{cfg}\left(d_v b_u+2b_{state}+b_{valid}\right).$$

If the vector width is padded to d_v_padded, the capacity envelope is:

$$M_{mlu}^{capacity} = N_{cap}\left(d_v^{padded} b_u+2b_{state}+b_{valid}\right).$$

For (LSE,O):

$$M_{lse,o}^{logical} = N_{cfg}\left(d_v b_O+b_{state}+b_{valid}\right).$$

Apply the formulas to the main call, where N_cfg = 128:

Workspace ABI	Declared stored dtypes	Bytes per state	Configured payload
(m,l,u)	u,m,l FP32; validity uint8	128*4 + 2*4 + 1 = 521	66,688 B = 65.125 KiB
(LSE,O)	O BF16; LSE FP32; validity uint8	128*2 + 4 + 1 = 261	33,408 B = 32.625 KiB

The second row is smaller because the fixture stores normalized partial outputs in BF16. That is a storage/numerical design choice, not a theorem that (LSE,O) always uses fewer bytes. Storing O in FP32, omitting an explicit validity tensor, using array-of-structures packing, or aligning every state row changes the result.

0x03F Reduction Traffic Is A Workspace Round Trip

For a two-kernel design that writes every consumed state once and reads it once:

$$M_{workspace\ roundtrip}=M_{partial\ write}+M_{partial\ read}.$$

The reduction path also writes final output and optionally final LSE:

$$M_{reduction\ path} = 2M_{partial} + B H_q d_v b_O + \mathbf{1}_{write\ LSE}B H_q b_{state}.$$

For the main fixture:

Item	FP32 (m,l,u)	BF16 (LSE,O)
Producer workspace write	66,688 B	33,408 B
Reducer workspace read	66,688 B	33,408 B
Final BF16 output write	4,096 B	4,096 B
Final FP32 LSE write	64 B	64 B
Reduction path total	137,536 B	70,976 B

This is real logical work introduced by the split schedule. It replaces A19’s imprecise “almost no additional storage” description with an auditable contract.

It is still not measured HBM traffic.

M4.1 distinguished unique payload, logical demand, and profiler transactions. Applied to this decode call:

$$M_{KV}^{unique} = \sum_b T_b H_{kv}(d_h+d_v)b_{cache},$$ $$M_{KV}^{qhead\ demand} = \sum_b T_b H_q(d_h+d_v)b_{cache}.$$

Under the teaching owner schedule:

unique Q payload                         = 4,096 B
Q load demand if every split loads Q     = 32,768 B

unique K/V payload by K/V head           = 7,867,392 B
per-query-head K/V logical load demand   = 31,469,568 B

FP32 (m,l,u) full two-launch demand      = 31,639,872 B
BF16 (LSE,O) full two-launch demand      = 31,573,312 B

The fourfold K/V gap follows from H_q / H_kv = 4. It is a reuse opportunity, not a prediction that DRAM transfers four copies. Query heads can share cache lines, a kernel can group heads, and L2 can serve repeated loads. Conversely, padding, metadata, write allocation, cache misses, and retries can add physical transactions.

0x03G There Are Four Different Tails

“The tail” is not one condition.

Tail	Example	Required behavior
Request-length tail	T_1 = 3587 while another request has 4096	derive bounds from each T_b
Split-balance tail	[449,449,449,448,448,448,448,448]	predicate the shorter split extents
Empty/capacity tail	T=3, S=5, S_capacity=8	write identity for every state the reducer may consume
Head-width tail	logical d_v=80, allocated envelope d_v_padded=96	predicate invalid lanes and never expose them as output

The fixed-capacity fixture is deliberately severe:

B = 2
H_q = 4
T_b = [3, 0]
S = 5
S_capacity = 8

producer owners = 2 * 4 * 8 = 64
active owners = 12
empty or inactive owners = 52
reducer owners = 8
identity bypasses = 52

Its first request has split lengths:

[1, 1, 1, 0, 0 | inactive, inactive, inactive]

Its second request has eight empty slots. Because the fixture’s reducer reads the full capacity envelope, all 64 slots must be initialized. Leaving inactive slots uninitialized would turn shape stability into a correctness bug.

The head-width fixture separates logical payload from lane envelope:

d_v = 80
vector alignment = 32 elements
d_v_padded = 96

logical configured workspace = 10,528 B
capacity allocation envelope = 12,576 B
padding difference = 2,048 B

Predication can prevent invalid global loads or stores. It does not erase the fact that a kernel specialization may reserve registers, shared-memory fragments, or workspace lanes for the padded width.

0x03H Dtype Is A Field-Level Contract

The algebra uses real numbers. A concrete workspace needs a dtype for every field:

Field	Teaching baseline	Alternatives	Failure if omitted from the contract
Q storage	BF16/FP16	FP8 or other runtime formats	wrong byte ledger or unsupported dispatch
K/V cache storage	BF16/FP16	quantized cache plus scales	wrong load width and missing dequantization state
Score/max/sum compute	FP32 baseline	backend-specific mixed precision	overflow, drift, or false parity claim
Partial vector storage	FP32 u or BF16 O examples	FP16/BF16/FP32 or packed format	workspace and accuracy change together
Partial scalar storage	FP32	backend-specific	LSE/denominator precision changes
Validity	uint8 in the oracle	LSE sentinel, bitset, metadata	empty slots may be consumed as data
Final output	BF16/FP16	model/runtime output dtype	wrong downstream ABI

The estimator does not claim that every real Flash-Decoding kernel stores FP32 u, a uint8 validity tensor, or BF16 partial O. It makes those choices explicit so their consequences can be calculated.

Quantized K/V cache formats add scale/zero-point or codebook state and dequantization work. M8 owns those representations. M4.5 owns the fact that cache dtype and its metadata belong in the decode dispatch key and traffic ledger.

0x03I Empty-Aware Two-Launch Pseudocode

def summarize_allowed_split(scores, values, allowed):
    # The validity branch occurs before max or exponential arithmetic.
    if len(allowed) == 0:
        return EMPTY_STATE

    local_scores = scores[allowed]
    local_values = values[allowed]
    m_c = max(local_scores)
    weights = exp(local_scores - m_c)
    l_c = sum(weights)
    u_c = weights @ local_values
    return SplitState(valid=True, maximum=m_c, denominator=l_c, numerator=u_c)


def split_decode(q, cache, context_lengths, S, S_capacity, plan):
    # Logical Q: [B, H_q, 1, d_h]
    # Capacity workspace: [B, H_q, S_capacity, state_fields]
    partial = allocate_workspace(plan.workspace_abi, S_capacity)

    parallel_for b, q_head, split_id in grid(B, H_q, S_capacity):
        # Every slot that a reducer can read receives a defined state.
        if split_id >= S:
            partial[b, q_head, split_id] = EMPTY_STATE
            continue

        start, end = balanced_split_bounds(
            context_lengths[b], S, split_id
        )
        if start == end:
            partial[b, q_head, split_id] = EMPTY_STATE
            continue

        kv_head = q_head // (H_q // H_kv)
        q_row = load_q(q, b, q_head)
        k_rows, v_rows = load_logical_cache_range(
            cache, b, kv_head, start, end
        )

        scores = q_row @ k_rows.T * scale
        scores = apply_decode_mask(scores, b, q_head, start, end)
        allowed = logical_positions_surviving_mask(scores)
        partial[b, q_head, split_id] = summarize_allowed_split(
            scores, v_rows, allowed
        )

    parallel_for b, q_head in grid(B, H_q):
        state = EMPTY_STATE
        for split_id in plan.reducer_split_ids:
            state = merge_state(state, partial[b, q_head, split_id])
        O[b, q_head, 0, :], LSE[b, q_head] = finalize_row(state)

    return O, optional(LSE)

The pseudocode initializes inactive capacity slots because its plan may reduce them. A runtime that reduces only 0:S need not write S:S_capacity; producer and reducer contracts must agree.

The split count remains a tuning decision:

more splits:
    more producer owners
    shorter K/V ranges
    more state slots
    more reduction fan-in

fewer splits:
    less workspace and reduction work
    fewer independent owners
    possible under-occupancy when B * H_q is small

0x03J Executable Storage And Ownership Evidence

The split-launch/storage contract is bound to:

fixture:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/split_launch_storage_fixture.json

oracle:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/split_launch_storage_oracle.py

generated report:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/split_launch_storage_report.json

tests:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_split_launch_storage_oracle.py

The oracle checks disjoint coverage, ragged bounds, capacity initialization, launch owner counts, workspace ABIs, GQA reuse gaps, head-width padding, and one-split reduction closure. Its evidence class is Synthetic contract test and its runtime evidence is none.

Failure	Invalid assumption	Consequence	Closure
Use batch maximum T for every request	ragged rows share split bounds	out-of-range or unrelated K/V reads	derive bounds from each T_b
Allocate [B,H_q,S,d_v] but launch S_capacity	launch and workspace capacities differ	out-of-bounds state write	bind launch and allocation manifests
Reducer reads unwritten empty slots	inactive owner exits without identity write	nondeterministic output or NaN	initialize every consumed slot
Count only partial_u	scalar and validity state omitted	understated storage/traffic	ledger every ABI field and dtype
Treat logical bytes as DRAM bytes	cache reuse and transaction granularity ignored	unsupported performance claim	require profiler counters
Count unique GQA K/V payload as per-head demand	head sharing conflated with free reuse	understated load demand	report both ledgers
Treat padded width as valid output width	specialization lanes leak into semantics	shape or value corruption	predicate tails and crop final output

0x04 Contiguous, Ragged, And Paged K/V Address Translation

The split derivation in 0x03 assigns one owner a logical interval [start,end). That interval is not yet a load instruction. Before the owner can form one score, it must turn a logical coordinate into a valid byte address:

(active request b, logical token t, query head h_q, lane x, K or V)
    -> cache identity
    -> K/V head identity
    -> storage row or physical page
    -> layout-specific tensor coordinate
    -> element offset
    -> byte address relative to the K or V base

This section owns that read-side translation contract. It does not own the allocator, free list, reference counts, copy-on-write transition, prefix-cache policy, or page-table mutation that produced the metadata. Those lifecycle operations remain in M5.3. The distinction matters: a serving kernel may consume a perfectly valid page table and still read the wrong payload because it confuses active batch order, cache-row identity, K/V-head identity, or page-tail visibility.

0x04A One Logical Coordinate Has Several Identities

Let the logical input coordinate be:

$$\chi=(b,t,h_q,x,z),$$

where b indexes the current active batch, t is a request-local token position, h_q is a query head, x is a lane in the head dimension, and $z\in\{K,V\}$. Address translation first resolves two identities that need not equal their input indices.

Request identity. Continuous batching can reorder active requests while their cache storage remains stable. With a cache-row remap:

$$c=\operatorname{cache\_batch\_idx}[b].$$

The teaching fixture deliberately maps active request req-A from b=0 to c=2. Using b directly would produce an in-bounds address in the wrong request’s cache.

K/V-head identity. For regular grouped-query attention with divisible head groups:

$$g=\frac{H_q}{H_{kv}}, \qquad h_{kv}=\left\lfloor\frac{h_q}{g}\right\rfloor.$$

The fixture has $H_q=4$, $H_{kv}=2$, and therefore h_q=3 -> h_kv=1. This mapping is a model contract, not an optimization that a kernel may infer differently. More general trained mappings would need explicit metadata.

Only after resolving c and $h_{kv}$ may the implementation choose a contiguous stride calculation, a ragged row pointer, or a page-table lookup.

0x04B Contiguous Cache: Strides Are The Address Formula

Assume separate K and V tensors, element width $b_e$, cache-row capacity $B_c$, token capacity $T_c$, and head width $d_h$. A token-major or NHD cache has shape:

$$[B_c,T_c,H_{kv},d_h]$$

and contiguous element strides:

$$[T_cH_{kv}d_h,\ H_{kv}d_h,\ d_h,\ 1].$$

The scalar element offset is therefore derived by expanding the dot product of the coordinate and stride vectors:

$$o_{\text{NHD}} =c(T_cH_{kv}d_h)+t(H_{kv}d_h)+h_{kv}d_h+x =((cT_c+t)H_{kv}+h_{kv})d_h+x.$$

A head-major or HND cache instead has shape [B_c,H_kv,T_c,d_h], so:

$$o_{\text{HND}} =c(H_{kv}T_cd_h)+h_{kv}(T_cd_h)+td_h+x =((cH_{kv}+h_{kv})T_c+t)d_h+x.$$

For either layout:

$$\operatorname{addr}_z(\chi)=\operatorname{base}_z+b_eo, \qquad z\in\{K,V\}.$$

The formula assumes separate K and V bases. An interleaved K/V representation needs another axis and another stride; silently reusing this equation would be wrong.

The fixture uses B_c=4, T_c=12, H_kv=2, d_h=4, and b_e=2 bytes. For req-A, t=3, h_q=3, and x=2, the resolved coordinate is c=2, h_kv=1. Thus:

NHD coordinate = [2, 3, 1, 2]
NHD strides    = [96, 8, 4, 1] elements
offset         = 2*96 + 3*8 + 1*4 + 2 = 222 elements = 444 B

HND coordinate = [2, 1, 3, 2]
HND strides    = [96, 48, 4, 1] elements
offset         = 2*96 + 1*48 + 3*4 + 2 = 254 elements = 508 B

Different offsets do not imply different logical data. They prove that layout is part of the kernel ABI. The current FlashAttention repository documents a contiguous flash_attn_with_kvcache form with cache shape (batch_size_cache, seqlen_cache, nheads_k, headdim) and an optional cache_batch_idx; that is one version-scoped interface, not a universal cache layout. (official interface)

0x04C Packed Ragged Cache: indptr Replaces The Batch Stride

A packed ragged representation removes per-request token-capacity padding. Let requests appear in metadata order r=0..B-1, with monotone row pointers:

$$\operatorname{indptr}[0]=0, \qquad \operatorname{indptr}[r+1]-\operatorname{indptr}[r]=T_r.$$

The request-local token becomes packed row:

$$p=\operatorname{indptr}[r]+t, \qquad 0\le t<T_r.$$

For packed NHD data shaped [sum_r T_r,H_kv,d_h], the element offset is:

$$o_{\text{ragged}}=(pH_{kv}+h_{kv})d_h+x.$$

The fixture packs lengths [10,7,5] with indptr=[0,10,17,22]. Therefore req-B,t=6 maps to packed row 10+6=16; it does not use cache_row=0 as a packed row. FlashInfer’s layout documentation exposes this same distinction between ragged indptr metadata and NHD/HND tensor order. Its documented integer dtypes and exact wrapper fields are implementation contracts that must be pinned with the library version. (FlashInfer KV layouts)

Packed ragged storage reduces padding but changes append and relocation costs. It also does not by itself provide stable physical placement under continuous allocation. Those are design trade-offs, not reasons to conflate indptr with a page table.

0x04D Paged Cache: Logical Block And Physical Page Are Different Axes

Let page size be $P$. The request-local token decomposes as:

$$j=\left\lfloor\frac{t}{P}\right\rfloor, \qquad r_p=t\bmod P,$$

where j is a logical block number and $r_p$ is a row within that block. Neither value is a physical page id.

A dense block-table encoding resolves:

$$\pi=\operatorname{block\_table}[c,j].$$

A compressed sparse row encoding resolves the same logical block with:

$$i=\operatorname{request\_segment}(b), \qquad \pi=\operatorname{kv\_page\_indices} [\operatorname{kv\_page\_indptr}[i]+j].$$

The two encodings have different metadata shapes but must yield the same physical page $\pi$ for the same request and logical block. With paged NHD data [N_pages,P,H_kv,d_h]:

$$o_{\text{page,NHD}}=((\pi P+r_p)H_{kv}+h_{kv})d_h+x.$$

With paged HND data [N_pages,H_kv,P,d_h]:

$$o_{\text{page,HND}}=((\pi H_{kv}+h_{kv})P+r_p)d_h+x.$$

The fixture gives req-A the logical-to-physical table [7,3,9]. Hence tokens 0..3 live in physical page 7, tokens 4..7 in page 3, and tokens 8..9 in page 9. The sequence is logically contiguous while its page ids are not.

FlashInfer documents paged metadata as kv_page_indptr, kv_page_indices, and kv_last_page_lens; for a non-empty request its represented context length is:

$$T=P(n_{pages}-1)+\operatorname{last\_page\_len}, \qquad 1\le\operatorname{last\_page\_len}\le P.$$

The PagedAttention paper motivates this OS-style separation between logical K/V blocks and non-contiguous physical storage. (PagedAttention paper)

0x04E A Logical Split Becomes A Sequence Of Bounded Page Segments

A Flash-Decoding owner receives [a,e), not one physical pointer. For a non-empty interval, the number of pages touched is:

$$n_{seg}=1+ \left\lfloor\frac{e-1}{P}\right\rfloor- \left\lfloor\frac{a}{P}\right\rfloor.$$

The implementation should translate once per intersected page segment, then iterate contiguous rows within that page. It need not reload page metadata for every scalar or every head-dimension lane.

For req-A, P=4, and split [3,9), the exact trace is:

Logical range	Logical block	Physical page	First page row	Rows
[3,4)	0	7	3	1
[4,8)	1	3	0	4
[8,9)	2	9	0	1

The six logical rows require three page lookups. Split boundaries and page boundaries are independent; a planner that selects splits only for occupancy can create extra page fragments, while forcing every split to page boundaries can create load imbalance. That is a measured tuning problem, not a universal rule.

0x04F Allocated Tail Is Not Visible History

The final physical page is usually only partially visible. For T=10 and P=4, page 9 has two legal rows:

page 9 offset 0 -> logical token 8  visible
page 9 offset 1 -> logical token 9  visible
page 9 offset 2 -> poison/stale/uninitialized, not visible
page 9 offset 3 -> poison/stale/uninitialized, not visible

A page id proves allocation, not token visibility. Every load path needs the request’s exact context length or an equivalent last-page-length contract. A kernel that rounds the loop bound up to page capacity can ingest stale values into the maximum, denominator, or numerator while remaining memory-safe.

This is also why appending and reading are distinct state transitions. A runtime may reserve a page before all rows are initialized. The decode reader must consume only committed logical positions. M5.1 owns when a token becomes committed request state; M5.3 owns allocation and page-table mutation.

0x04G Layout Alternatives Change Different Costs

Representation	Read-side translation	Principal benefit	Principal cost or risk
padded contiguous NHD	cache-row remap plus strides	simple token-major traversal	unused token capacity and relocation/reservation pressure
padded contiguous HND	cache-row remap plus different strides	head-major traversal can suit some kernels	same capacity issue; incompatible stride assumptions
packed ragged	request segment plus indptr[r]+t	no per-request token padding in packed view	append/compaction and metadata-order contract
explicit paged dense table	block_table[c,j]	stable non-contiguous physical pages and constant-width rows	sentinel/capacity entries and table footprint
explicit paged CSR table	indices[indptr[r]+j] plus last-page length	metadata proportional to assigned pages	another indirection and ragged page-list boundaries
contiguous virtual K/V	ordinary virtual address arithmetic; VM maps backing pages	removes explicit block-table lookup from the kernel	virtual-memory setup, platform constraints, and page mapping remain
gathered compact view	pre-kernel gather creates contiguous rows	simpler attention inner loop	extra materialization, traffic, storage, and launch synchronization
specialized vectorized K/V layout	backend-specific strides or packing	aligns loads and kernels to hardware	K and V may use different physical layouts; generic formulas fail

vAttention is a primary example of the contiguous-virtual alternative: it keeps a contiguous virtual address contract while mapping physical pages on demand, rather than exposing a user-space block table to the attention kernel. (vAttention paper) Historical vLLM PagedAttention documentation also illustrates a specialized alternative in which K and V use different vectorized block layouts. Such layouts must be treated as version-scoped ABIs, not generalized into the NHD/HND equations. The document itself warns that it is historical and no longer describes current vLLM code. (historical kernel note)

These methods preserve logical attention only if their address translator recovers the same (request,t,h_kv,x,K/V) payload. They are not interchangeable performance labels: metadata cache behavior, vectorization, page size, gather traffic, and append path differ.

0x04H Read-Side Translation And Segment Iteration

def resolve_kv_identity(active_b, q_head, plan):
    cache_row = plan.cache_batch_idx[active_b]
    kv_head = q_head // (plan.H_q // plan.H_kv)
    return cache_row, kv_head


def paged_segments(active_b, start, end, plan):
    cache_row, _ = resolve_kv_identity(active_b, q_head=0, plan=plan)
    position = start
    while position < end:
        logical_block = position // plan.page_size
        page_offset = position % plan.page_size
        physical_page = plan.block_table[cache_row, logical_block]

        segment_end = min(end, (logical_block + 1) * plan.page_size)
        yield physical_page, page_offset, segment_end - position
        position = segment_end


def load_paged_nhd(base, active_b, q_head, lane, start, end, plan):
    _, kv_head = resolve_kv_identity(active_b, q_head, plan)
    assert 0 <= start <= end <= plan.context_lengths[active_b]

    rows = []
    for page, page_offset, count in paged_segments(
        active_b, start, end, plan
    ):
        assert 0 <= page < plan.num_physical_pages
        rows.append(
            base[page, page_offset:page_offset + count, kv_head, lane]
        )
    return concatenate(rows, axis=0)

This is reference pseudocode, not a claim about one production kernel’s loop nest. A real implementation may hoist metadata, vectorize lanes, share page ids across grouped query heads, stage rows in shared memory, or fuse append and attention. Those transformations must preserve four invariants:

request invariant:
    active batch order is translated through the declared cache identity map

head invariant:
    each query head reads its trained K/V head group

visibility invariant:
    every logical token satisfies 0 <= t < context_length[b]

address invariant:
    each translated coordinate is in-bounds for the selected physical ABI

0x04I Metadata Bytes Are Not Measured Metadata Traffic

The fixture’s dense table has 4 cache rows * 3 slots = 12 int32 entries, or 48 resident bytes. Its CSR metadata has four row pointers, seven page ids, and three last-page lengths: 14 int32 entries, or 56 resident bytes.

Those totals do not prove 48 or 56 DRAM bytes per decode call. A page id may be cached, loaded once per segment, shared across heads, redundantly loaded by several CTAs, widened into a transaction, or fused into a planner workspace. The traffic ledger must remain:

resident metadata payload:
    shape * dtype bytes

logical lookup demand:
    page-list and row-pointer entries required by the algorithm

measured memory traffic:
    profiler counters at one declared runtime coordinate

Page size changes the number of lookups and tail waste at the same time. The allocator-level trade-off and fragmentation policy belong to M5.3; M4.5 owns how the selected value changes one kernel’s segmentation and address work.

0x04J Executable Address Evidence And Failure Closure

The address-translation contract is bound to:

valid fixture:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/kv_address_translation_fixture.json

invalid fixtures:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_kv_address_translation_fixtures.json

oracle:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/kv_address_translation_oracle.py

generated report:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/kv_address_translation_report.json

tests:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_kv_address_translation_oracle.py

The synthetic oracle writes unique payload ids into contiguous NHD, contiguous HND, packed-ragged NHD, dense-table paged NHD/HND, and CSR-table paged NHD stores. It then reads every visible coordinate through the same translator. Across three requests it checks 176 scalar elements per K or V, 352 across both, with zero address collisions, zero recovery mismatches, and zero dense-versus-CSR page disagreements. It poisons 96 K/V tail elements and proves that no visible gather reaches them. This is executable indexing evidence, not a GPU trace or bandwidth measurement.

Failure	Invalid assumption	Consequence	Closure
use active b as stable cache row	active batch order equals storage order	another request’s valid K/V is read	apply and test cache_batch_idx
use h_q as h_kv	query and K/V head spaces are identical	out-of-range or wrong trained group	bind explicit GQA mapping
use NHD strides on HND data	shape names imply the same address order	in-bounds payload permutation	derive offsets from the declared layout
treat ragged indptr as a page table	packed row and physical page are the same identity	unrelated rows or invalid pages	type metadata by representation
use logical block j as physical page	logical and physical page order match	wrong non-contiguous K/V	follow the block/page table
accept a visible-page sentinel or out-of-pool id	table capacity entries are initialized mappings	invalid address	validate all visible logical blocks
round T to allocated page capacity	allocated tail is visible history	stale tail changes softmax state	predicate exact context or last-page length
assume dense and CSR tables agree	two metadata views are equivalent by construction	planner/kernel ABI drift	compare every visible mapping in tests
report resident metadata as HBM traffic	bytes stored equal bytes transferred	unsupported roofline conclusion	preserve resident, logical, and measured ledgers

0x05 A Mask Is A Program Over Logical Score Coordinates

Section 0x04 answered where a visible K/V row lives. A mask answers a prior question:

For query row q, is logical key position k allowed to contribute at all?

Those contracts must not be collapsed. A physical page can exist while its token is outside the committed context, and a committed token can be logically hidden by a window, document boundary, or structured mask. Address translation therefore cannot decide attention visibility by itself.

0x05A Visibility, Representation, And Dispatch Are Different Contracts

Let one logical score be

$$S_{qk}=\frac{Q_qK_k^\top}{\sqrt{d_h}}.$$

Define the allowed set for row $q$ as

$$\mathcal A_q=\{k\mid V(q,k)=\text{true}\}.$$

The additive mask is then derived from visibility, not the other way around:

$$M_{qk}= \begin{cases} 0,&k\in\mathcal A_q,\\ -\infty,&k\notin\mathcal A_q. \end{cases}$$

Three implementation objects follow from this one semantic object:

semantic visibility:
    V(batch, head, q_position, kv_position) -> bool

stored representation:
    dense values, lengths, intervals, block indices, or a compiled predicate

kernel dispatch program:
    SKIP, FULL, or PARTIAL for one score tile

They are not interchangeable. A representation may be exact but expensive to read. A compact representation may not express the requested pattern. A backend may understand the semantics but reject the representation supplied by the caller.

0x05B Polarity And Position Space Must Be Bound Before The Kernel

Mask APIs disagree about polarity. A boolean can mean either allowed or masked, while additive masks usually use 0 and -inf. Position indices can be local packed rows, absolute sequence positions, or per-request offsets. The call contract must therefore bind:

mask polarity
query and K/V position coordinate systems
batch/head broadcast rules
exact query and context lengths
all-masked-row policy
representation dtype and sentinel rules

The mask-program fixture uses true_means_masked, int32 interval endpoints, and the same all-masked policy as Section 0x02:

output = zero_vector(d_v)
LSE    = -inf

Changing polarity while preserving tensor shape is a dangerous failure: the program remains addressable and often finite, but computes the complement of the intended attention graph.

0x05C Tile Classes Follow From Set Relations

For a score tile

$$\mathcal T=[q_0,q_1)\times[k_0,k_1),$$

let $\mathcal M$ be the set of masked score coordinates. The exact tile class is

$$\operatorname{class}(\mathcal T)= \begin{cases} \text{SKIP},&\mathcal T\subseteq\mathcal M,\\ \text{FULL},&\mathcal T\cap\mathcal M=\varnothing,\\ \text{PARTIAL},&\text{otherwise}. \end{cases}$$

Each class changes the inner loop:

Class	Load K/V?	Form QK^T?	Load element mask?	Softmax-state effect
SKIP	No	No	No	merge the empty identity
FULL	Yes	Yes	No	ordinary online update
PARTIAL	Yes	Yes	Yes or evaluate predicate	set hidden scores to -inf before max/sum

The third row is the correctness boundary. Applying the mask after the local maximum or denominator lets hidden scores change the exponential frame even if their final probabilities are later zeroed.

0x05D Visibility Composes With Address Translation

The logical order is:

for logical_k_tile in visible_context:
    tile_class = mask_program.classify(q_tile, logical_k_tile)
    if tile_class == SKIP:
        continue

    # Section 0x04 translates only the logical rows that this tile may consume.
    physical_segments = kv_address_program.translate(logical_k_tile)
    K_tile, V_tile = load_segments(physical_segments)

    scores = Q_tile @ K_tile.T * scale    # scale = 1 / sqrt(d_h), as in 0x05A
    if tile_class == PARTIAL:
        scores = apply_element_visibility(scores, q_tile, logical_k_tile)
    online_state.update(scores, V_tile)

An implementation may fuse classification, address generation, and loads, but the proof obligations remain separate. SKIP can avoid K/V address work; FULL and PARTIAL still require the contiguous, ragged, paged, or virtual translation derived in 0x04.

0x05E Decode Changes Which Mask Optimizations Matter

For standard one-token causal decode, the new query is after every committed key. Once exact context length has excluded the page tail, the causal predicate often marks the whole historical row visible. There is no square S_q x S_k mask to compress when S_q = 1.

Masks remain operationally important for:

• sliding-window or sink policies;
• document or segment isolation;
• explicit cache eviction/retention patterns;
• chunked prefill and verification calls with several query rows;
• speculative trees or packed candidate branches;
• training and post-training with long structured sequences.

This phase distinction prevents a training/prefill mask result from becoming an unsupported one-token decode claim.

0x06 FlashMask: Two Intervals Per Column And Three Tile Paths

FlashMask starts from an empirical structure in practical training masks: from one key column, hidden query rows often form one continuous run on each side of the diagonal. It encodes those runs directly, then summarizes each K/V column block so the attention kernel can classify tiles before loading full interval vectors.

0x06A The Column Observation Narrows The Representation

For key column $j$, a single generic interval would be

$$\mathcal I_j=[start_j,end_j).$$

One interval cannot encode separated hidden regions above and below the diagonal. FlashMask therefore splits the score column into two half-open masked intervals:

$$\mathcal U_j=[UTS_j,UTE_j),\qquad \mathcal L_j=[LTS_j,LTE_j).$$

Its represented dense-mask semantics are

$$M_{qj}=-\infty \quad\Longleftrightarrow\quad q\in\mathcal U_j\cup\mathcal L_j.$$

The four int32 vectors have shape [S_k] or a batched/head-broadcast extension of that logical shape. Paddle’s current API contract exposes startend_row_indices [B, H_kv_or_1, S_k, {1,2,4}], showing that the paper’s four-vector object can be packed into one last dimension. That API is a versioned implementation surface, not proof that a local Paddle kernel ran.

0x06B One Worked Column Makes Half-Open Semantics Auditable

The fixture reconstructs the paper’s illustrative column contract at j = 5:

UT interval = [2, 4)  -> masked query rows 2, 3
LT interval = [7, 10) -> masked query rows 7, 8, 9

masked rows = {2, 3, 7, 8, 9}

Rows 4, 5, and 6 remain visible. Treating either end as inclusive would hide rows 4 or 10 and change the model’s attention graph.

0x06C Eight Block Summaries Avoid Reading Four Vectors For Every Tile

Partition K/V columns into blocks of width $B_c$. For one block $J$, FlashMask precomputes min and max values for every start/end vector:

$$UTS_J^{min}=\min_{j\in J}UTS_j,\qquad UTS_J^{max}=\max_{j\in J}UTS_j,$$

with the same pair for UTE, LTS, and LTE. This creates eight summary values per K/V block:

UTS_min, UTS_max, UTE_min, UTE_max
LTS_min, LTS_max, LTE_min, LTE_max

The summary does not replace the original endpoints. It is a coarse proof that a Q tile is wholly covered, wholly disjoint, or may overlap an interval family. Only the last case needs the per-column vectors.

0x06D The Tile Predicates Follow From Interval Intersection

For query rows $Q=[q_0,q_1)$ and one interval family with per-column starts $s_j$ and ends $e_j$, every score in the tile is masked when

$$q_0\ge \max_j s_j \quad\land\quad q_1\le \min_j e_j.$$

The first inequality puts the tile after every interval start. The second puts its exclusive end before every interval end. The tile may overlap at least one interval when

$$q_1>\min_j s_j \quad\land\quad q_0<\max_j e_j.$$

Applying those tests independently to the upper and lower families gives a safe three-way classifier:

def classify_flashmask_tile(q0, q1, summary):
    upper = interval_family_relation(q0, q1, summary.upper)
    lower = interval_family_relation(q0, q1, summary.lower)

    if upper == COVERS or lower == COVERS:
        return SKIP
    if upper == DISJOINT and lower == DISJOINT:
        return FULL
    return PARTIAL

Min/max summaries can conservatively return PARTIAL; they must never return SKIP for a visible cell or FULL for a hidden cell. The elementwise interval test closes any uncertainty on the partial path.

0x06E The Forward Trace Adds Control Around The Existing Attention State

The paper extends an FA2-style query-tile loop. In contract-level pseudocode:

for q_tile in query_tiles:
    Q = load_q(q_tile)
    state = EMPTY

    for kv_tile in kv_tiles:
        summary = load_eight_bounds(kv_tile)
        tile_class = classify_flashmask_tile(q_tile, summary)

        if tile_class == SKIP:
            continue

        K, V = load_kv(kv_tile)
        S = Q @ K.T * scale    # scale = 1 / sqrt(d_h)

        if tile_class == PARTIAL:
            UTS, UTE, LTS, LTE = load_column_intervals(kv_tile)
            S = set_hidden_scores_to_negative_infinity(
                S, q_tile, UTS, UTE, LTS, LTE
            )

        state = online_attention_update(state, S, V)

    output[q_tile], lse[q_tile] = finalize_or_all_masked(state)

This is not a literal Paddle, CUDA, or Triton source trace. It transcribes tensor and loop semantics. The existing online state remains owned by M4.3; Section 0x06 owns the control path that decides whether and how one score tile enters that state.

0x06F Skipping A Fully Masked Tile Is Exact

For every hidden score,

$$\exp(S_{qk}+M_{qk})=\exp(-\infty)=0.$$

Therefore a fully masked tile contributes neither denominator mass nor value-weighted numerator. Its canonical partial state is the empty identity from 0x02, so skipping it is algebraically identical to forming and masking the scores. A FULL tile is exact because its mask is identically zero. A PARTIAL tile is exact only if hidden scores become -inf before row max, denominator, and numerator updates.

The FlashMask paper reports bit-level convergence agreement at its experimental coordinates. That source-reported observation is narrower than a universal bitwise theorem across dtypes, reduction trees, library versions, and backends. The article’s executable claim is only parity for the declared float64 fixture.

0x06G Storage, Logical Reads, And Omitted Work Need Separate Ledgers

For square length $N$, four-byte endpoints, and one-byte dense-mask elements:

$$M_{dense}=N^2\ \text{bytes},$$ $$M_{interval}=4N\cdot4\ \text{bytes},$$ $$M_{summary}=8\left\lceil\frac{N}{B_c}\right\rceil\cdot4\ \text{bytes}.$$

At N = 131,072 and B_c = 64, the synthetic resident-payload ledger is:

one-byte dense mask       = 17,179,869,184 B = 16,384 MiB
four int32 vectors        =      2,097,152 B =      2 MiB
eight int32 summaries     =         65,536 B =     64 KiB

These are stored-object sizes, not measured HBM traffic. The paper’s logical access analysis and a profiler’s transactions are different evidence classes. Similarly, block sparsity

$$\rho=\frac{N_{skip}}{T_rT_c}$$

counts wholly skipped tiles, not masked scalar cells. Partial tiles still form QK^T and then mask individual entries.

0x06H The Representation Boundary Is Structural, Not Numerical

Two intervals can encode at most two contiguous masked runs in one column. The fixture’s alternating hidden rows

{0, 2, 4, 6, 8}

form five runs and are not representable by one upper plus one lower interval. No endpoint precision increase repairs that mismatch; the caller needs another representation or a dense/compiled fallback.

Design	Semantic surface	Stored object	Kernel consequence	Boundary
causal/window flags	fixed coordinate rule	a few scalars	specialized tile bounds	narrowest, cheapest
packed cu_seqlens/document extents	segment isolation	row pointers/lengths	ragged tile limits	only segment-shaped masks
dense additive/boolean mask	per score cell	O(S_qS_k) values	element mask or fallback	broad semantics, high payload
BSR/BlockMask	block-level traversal plus optional predicate	block indices and counts	skip absent blocks; predicate partial blocks	granularity and preprocessing costs
FlashMask	two masked intervals per K/V column	four vectors plus eight summaries per column block	FULL/SKIP/PARTIAL routing	at most two represented runs per column
FlexAttention	callable score/mask program plus compiled block metadata	generated BlockMask and code	compiler specializes score and mask paths	compilation, support, and block metadata contract

PyTorch’s current FlexAttention documentation separates full blocks so the kernel can bypass mask_mod, mirroring the same general lesson: semantic programmability is useful only when the representation also exposes hardware-relevant tile classes.

0x06I Training, Prefill, And Cached Decode Are Different Evidence Coordinates

FlashMask’s main paper evaluates training and post-training workloads and gives a backward algorithm. Its Appendix B labels an inference comparison, but the reported API coordinate uses FlashInfer’s single_prefill_with_kv_cache and BlockSparseAttentionWrapper with long query sequences. That is prefill-style attention, not proof of a one-token paged-cache decode speedup.

paper main body:
    structured-mask training/post-training forward and backward

paper inference appendix:
    batch 1, long-sequence prefill-style mask comparison

this M4.5 local claim:
    mask representation and tile-dispatch correctness contract

not claimed:
    current local backend, one-token decode speedup, or profiler traffic

Column orientation also aligns naturally with dK/dV ownership in backward, as the paper notes, but detailed FlashMask backward scheduling is not derived in this decode-focused loop.

0x06J Executable Mask Evidence And Failure Closure

The mask-program evidence bundle is:

fixture:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/mask_program_fixture.json

invalid fixtures:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_mask_program_fixtures.json

oracle:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/mask_program_oracle.py

generated report:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/mask_program_report.json

tests:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_mask_program_oracle.py

The 10 x 8 mask uses 2 x 2 tiles. Its 20 tiles classify as six FULL, three SKIP, and eleven PARTIAL. The skipped path omits 12 score cells. No summary makes an unsafe FULL or SKIP decision, and tiled execution matches the dense float64 reference with zero observed output and LSE error. This is a synthetic contract test, not GPU-runtime evidence.

Failure	Invalid assumption	Consequence	Closure
invert mask polarity	true has universal meaning	compute the complement attention graph	bind and test polarity
use inclusive interval ends	index pairs are closed ranges	boundary rows are hidden incorrectly	use and test half-open ranges
accept malformed triangle intervals	any ordered endpoints are FlashMask-compatible	representation no longer matches the declared two-side contract	validate diagonal, order, and disjointness
treat min/max overlap as exact membership	summary resolves every scalar	visible or hidden cells are misclassified	route uncertain tiles to PARTIAL
apply partial mask after softmax update	zeroing output is sufficient	hidden scores alter max and denominator	mask scores before online state
represent five runs with two intervals	compactness is universal	silent semantic loss	run-count/representability gate or fallback
use resident metadata as traffic	object size equals DRAM transactions	unsupported bandwidth conclusion	preserve logical and measured ledgers
quote Appendix B as decode proof	all inference shapes are one-token decode	wrong phase/performance conclusion	preserve API and shape coordinate

0x07 Backend Admission, Selection, Plan State, And Runtime Evidence

The call site still does not name the implementation that performs attention:

F.scaled_dot_product_attention(
    q,
    k,
    v,
    attn_mask=mask,
    dropout_p=p,
    is_causal=is_causal,
    enable_gqa=enable_gqa,
)

This API supplies an attention request. A runtime must first decide which backend families belong to the request’s phase and platform, then evaluate their capability predicates, apply a selection policy, prepare any persistent plan state, and finally launch one or more kernels. Those are different events.

PyTorch documents SDPA as a semantic function that may select among several implementations. Its sdpa_kernel context manager restricts allowed backends and can interpret a supplied order as priority; the SDPA documentation also says that fused kernels have input limitations and can emit reasons when a requested fused implementation cannot run. vLLM’s backend-support documentation makes the policy distinction explicit: forced selection is validated and fails with reasons, whereas automatic selection walks a platform-specific priority list and chooses the first compatible backend. These are version-scoped runtime contracts, not universal laws for every framework.

0x07A Freeze The Dispatch Key Before Asking Which Backend Wins

Let one immutable dispatch key be

$$\mathcal D=(\mathcal E,\mathcal O,\mathcal T,\mathcal S,\mathcal R),$$

where:

Coordinate	Required content	Why it can change the path
environment $\mathcal E$	framework build, extension build, device, compute capability, driver/runtime	determines which code objects can exist and execute
operation $\mathcal O$	training forward/backward, prefill, append, decode, mixed batch	determines the available parallel axes and state lifecycle
tensors $\mathcal T$	$B,S_q,S_k,H_q,H_{kv},d_{qk},d_v$, dtypes, strides, alignment	constrains tile shapes, vector loads, GQA mapping, and precision paths
semantics $\mathcal S$	causal/custom mask, position convention, dropout, soft cap, window, bias	determines whether a backend computes the requested function
runtime controls $\mathcal R$	allowed/forced backend, determinism, graph capture, cache layout, workspace	constrains policy, state reuse, and launch legality

The dispatch fixture serializes the teaching key as:

phase, device_type, compute_capability
dtype, kv_dtype
q_len, kv_len
num_q_heads, num_kv_heads
head_dim_qk, head_dim_vo
cache_layout, page_size
mask_kind, dropout_p, training
requires_deterministic, cuda_graph
last_dim_contiguous, backend_request

This list is not a claim that every runtime hashes these exact fields. It is a minimum reproducibility record for this article. A framework may have more coordinates: attention sinks, quantization scales, RoPE mode, MLA dimensions, compile flags, environment variables, or a model-specific backend class.

The semantic checks precede backend checks. For example:

assert q_len > 0 and kv_len > 0
assert num_q_heads % num_kv_heads == 0
assert 0.0 <= dropout_p <= 1.0

if cache_layout.startswith("paged_"):
    assert page_size is not None and page_size > 0
else:
    assert page_size is None

An invalid GQA ratio is not “unsupported by the fast kernel”; it is a malformed call contract. Keeping malformed calls out of the capability matrix prevents a slow fallback from appearing to repair undefined semantics.

0x07B Admission Is A Conjunction, And Rejection Is A Vector

For backend $b$, define one admission predicate:

$$\begin{aligned} A_b(\mathcal D)= &I_b\land E_b\land P_b\land H_b\land D_b\land K_b\\ &\land Q_b\land G_b\land L_b\land M_b\land N_b\land C_b, \end{aligned}$$

with the factors interpreted as:

I_b: backend package/code object is installed
E_b: backend is enabled by runtime policy
P_b: phase/operation is supported
H_b: hardware and compute capability are supported
D_b: query/output dtype is supported
K_b: K/V dtype and cache representation are supported
Q_b: query length and head dimensions are supported
G_b: MHA/MQA/GQA head relationship is supported
L_b: layout, strides, alignment, and page size are supported
M_b: mask, window, bias, and position semantics are supported
N_b: numerical and determinism controls are supported
C_b: graph-capture, workspace, and lifecycle constraints are supported

The final result is Boolean, but diagnostics should retain every failed factor:

$$R_b(\mathcal D)=\{r_i\mid A_{b,i}(\mathcal D)=\text{false}\}.$$

This reason vector matters operationally. “Backend not selected” does not say whether the cause was a missing extension, unsupported head dimension, dense mask, paged-cache layout, graph mode, or a disabled policy. Those causes have different fixes and different regression risks.

The admission order also matters. The backend should reject unsupported semantics before dereferencing Section 0x04 page metadata or entering the Section 0x06 mask program. Admission is the guard around those lower-level contracts, not a replacement for their assertions.

0x07C Registry, Candidate Domain, Eligibility, And Priority Are Four Stages

Let $\mathcal B$ be every registered backend. A runtime usually narrows this registry by platform and attention family before applying detailed capability checks:

$$\mathcal C(\mathcal D)= \{b\in\mathcal B\mid \operatorname{platform}(b)=\mathcal E \land\operatorname{phase}(b)\ni\mathcal O\}.$$

The eligible set is then

$$\mathcal G(\mathcal D)= \{b\in\mathcal C(\mathcal D)\mid A_b(\mathcal D)=\text{true}\}.$$

This separation prevents a prefill-only CUDA kernel from being reported as a decode fallback, or a CUDA backend from being counted as a rejected CPU candidate. vLLM’s documentation explicitly notes separate selection behavior and priority tables for platforms and attention families; its current table is a versioned implementation surface, not a priority order to copy permanently into an article.

Two common policies follow.

forced_fail_closed:
    a requested backend either admits the complete key or returns its reasons

ordered_first_eligible:
    automatic policy selects the first eligible in-domain backend by priority

Forced backend $b_f$:

$$\operatorname{select}_{forced}(\mathcal D,b_f)= \begin{cases} b_f,&A_{b_f}(\mathcal D)=\text{true},\\ \operatorname{error}(R_{b_f}),&\text{otherwise}. \end{cases}$$

There is no silent fallback in this contract. A forced backend is useful for testing precisely because failure exposes incompatibility instead of hiding it.

Automatic ordered selection with priority $\pi(b)$:

$$b^*=\underset{b\in\mathcal G(\mathcal D)}{\arg\min}\;\pi(b).$$

If $\mathcal G$ is empty, the runtime either errors or invokes an explicitly declared outer fallback. A math path is not magically available for paged K/V: someone must define how the page table is consumed or how K/V is gathered, and that transformation has its own memory and synchronization cost.

A backend fallback event occurs when a higher-priority member of the same candidate domain is rejected and a lower-priority eligible backend is chosen. Do not conflate it with:

algorithmic fallback:
    one selected backend changes its internal schedule or split count

semantic fallback:
    the system materializes/gathers another representation to preserve meaning

failure:
    no legal implementation exists under the current policy

0x07D A Seven-Case Teaching Matrix Makes Selection Auditable

The executable fixture uses four deliberately generic teaching backends. Their names do not describe literal PyTorch, vLLM, FlashInfer, or FlashAttention implementations:

Teaching backend	Candidate role	Deliberately narrow property
decode_paged_fast	CUDA paged decode	$1\le S_q\le4$, selected dimensions, causal/window masks
prefill_contiguous_fast	CUDA contiguous prefill	$S_q\ge2$, no paged cache
paged_reference	semantic fallback for paged K/V	wider dimensions/masks, no graph mode
math_reference	contiguous CPU/CUDA reference	broad semantics, no paged-cache address program

For the base decode call:

device       = CUDA, compute capability 90
phase        = decode
S_q, S_k     = 1, 4096
H_q, H_kv    = 32, 8
d_qk, d_v    = 128, 128
dtype        = fp16 Q/O and fp16 K/V
cache        = paged NHD, page_size 16
mask         = causal
graph mode   = true
policy       = auto

the selected teaching backend is decode_paged_fast. Changing one coordinate can change the outcome:

Case	Changed coordinate	Result	Preserved diagnostic
paged decode	none	select decode_paged_fast	no rejection above winner
custom mask	mask_kind=dense_custom, graph off	select paged_reference	fast path rejects mask
head dimension	$d_{qk}=d_v=80$, graph off	select paged_reference	fast path rejects both dimensions
forced custom-mask fast path	force decode_paged_fast	error	forced path rejects mask; no fallback
prefill	$S_q=128$, contiguous K/V	select prefill_contiguous_fast	candidate domain changes
CPU decode	CPU, contiguous K/V	select math_reference	CUDA backends leave the domain
custom mask under graph mode	dense mask plus graph capture	error	every in-domain candidate has reasons

The head-dimension fallback retains both failed predicates:

head_dim_qk=80 unsupported
head_dim_vo=80 unsupported

The seven cases produce five selections, two errors, and two true backend fallbacks. The fixture deliberately records the complete rejection vector even after a winner is found. That turns a latency regression from “the API got slower” into “the fast path rejected mask_kind=dense_custom.”

The base call’s canonical teaching-key digest is:

f4813d5b08179c23e85c587f0da636b380caeb8338e74c0c4a5faa87cd66d2eb

Changing only $d_{qk}$ changes the digest. The digest is an identity aid, not a substitute for storing the human-readable fields or the capability reasons.

0x07E Framework APIs Expose Different Parts Of The Contract

The generic algebra maps to current official surfaces in different ways:

Runtime surface	What it exposes	What it still does not prove
PyTorch SDPA	semantic call, allowed backends, priority option, eligibility diagnostics	exact kernel symbol, launch geometry, measured traffic
vLLM backend registry	configuration validation, platform/family candidate lists, automatic/forced policy, incompatibility reasons	that a locally deployed revision matches the latest docs or that one request retained the startup path
FlashAttention flash_attn_with_kvcache	explicit cache layout/state, append, GQA, paged table, windows and inference surface	that another framework’s SDPA call dispatched to this interface
FlashInfer decode wrappers	explicit NHD/HND or paged metadata, workspace, backend option, plan()/run() lifecycle	that an auto choice or planned module corresponds to a profiler-observed symbol without runtime evidence

PyTorch also exposes can_use_flash_attention(params, debug=True) and related capability helpers. Such a result is an eligibility observation for one build and one parameter object. It is stronger than guessing from the API name but weaker than a profiler trace proving which kernel executed.

FlashInfer’s current single_decode_with_kv_cache surface makes several dispatch coordinates explicit: NHD/HND layout, GQA head ratio, Tensor-Core choice, position mode, window, soft cap, scales, and whether LSE is returned. Its paged decode wrappers add page metadata, workspace, graph mode, and a backend="auto" control. This variety is precisely why “FlashInfer ran” is not a sufficient benchmark coordinate.

0x07F A Planned Wrapper Adds A Second Immutable Key

Stateful runtimes can separate preparation from execution:

construct -> plan(shape/layout/static policy) -> run(tensors/dynamic state)

FlashInfer’s current attention documentation says BatchAttention.plan() must precede run() and that the plan is cached for subsequent calls with the same layout. The decode wrapper owns or receives workspace and paged metadata. This creates a second consistency condition beyond backend admission.

Let $P$ project a runtime call onto the fields frozen by its plan:

$$K_{plan}=P(\mathcal D_{plan}).$$

A later run may reuse the plan only if

$$P(\mathcal D_{run})=K_{plan}.$$

Which fields belong to $P$ is API- and version-specific. The dispatch teaching wrapper freezes:

device and workspace_device
K/V layout and page size
H_q, H_kv, d_qk, d_v
Q dtype and K/V dtype
CUDA Graph mode

It declares K/V lengths and page-list contents dynamic only under an explicit pre-bound-buffer update protocol. This is a synthetic lifecycle contract, not permission to mutate actual FlashInfer plan inputs arbitrarily. For a real wrapper, use the loaded version’s documentation and source to determine whether changed indptr, indices, lengths, batch capacity, or pointers require another plan() call or an in-place update to preallocated graph buffers.

The fixture’s plan-key digest is:

2a378ec0dc32475c6b2cf67212cd405d9184e23d54d27eeb1c57471ad470c3a8

Its lifecycle tests show:

Run change	Reuse teaching plan?	Reason
declared dynamic lengths/page list	yes	static projection unchanged
$d_{qk},d_v:128\to256$	no	kernel/layout specialization changes
workspace cuda:0 to cuda:1	no	workspace ownership changes
graph mode true to false	no	capture/lifecycle contract changes

A stale plan is not merely a performance problem. It can mean wrong workspace sizes, incompatible launch metadata, or pointers captured for another graph.

0x07G Determinism And Numerical Policy Belong In The Key

All eligible backends may target the same exact attention equation while using different reduction trees, accumulator widths, split counts, or precision modes. Section 0x02 already established that exact partition invariance does not imply bitwise floating-point identity.

PyTorch’s current reproducibility documentation lists different determinism characteristics for SDPA backends and notes that backend accumulation order can change numerical results. That table is version-scoped. The durable contract is to record:

forward or backward
requested deterministic policy
selected backend
input and accumulation dtypes where observable
split/reduction policy where observable
reference backend and tolerance
NaN/Inf and all-masked-row policy

For one-token inference there is no attention backward, but deterministic forward, precision mode, and graph replay are still reproducibility coordinates. Training calls add dropout RNG state and backward atomics/reduction order. A training benchmark and a decode benchmark therefore cannot share one numerical evidence row merely because both entered an API named SDPA.

Reference comparison should be field-aware:

assert same_shape(candidate, reference)
assert finite_policy_matches(candidate, reference)
assert max_abs_error <= atol + rtol * max_abs_reference

if return_lse:
    assert lse_policy_matches(candidate_lse, reference_lse)

if cache_append:
    assert committed_kv_rows_match_expected_tokens()

Output agreement alone does not validate Section 0x04 address metadata or in-place K/V append state if the call also mutates a cache.

0x07H Selection Evidence Is Not Execution Evidence

The evidence chain has strict claim ceilings:

1. API requested
2. backend package/build available
3. backend eligible for the frozen key
4. backend selected by policy
5. kernel symbol observed in a profiler trace
6. correctness comparison captured
7. raw timing distribution and profiler counters captured

No lower level proves a higher one. In particular:

$$\text{eligible}\not\Rightarrow\text{selected},\qquad \text{selected}\not\Rightarrow\text{kernel observed},\qquad \text{observed}\not\Rightarrow\text{performance measured}.$$

A selection log can identify a backend class while that backend internally launches different kernels by $S_q$, $S_k$, split count, dtype, or architecture. A profiler symbol can prove execution but says nothing about steady-state latency unless warmup, synchronization, graph replay, allocations, and timing samples are controlled.

FlashInfer’s logging and replay documentation illustrates another state boundary: API records and tensor dumps can be captured for a stateful wrapper, while CUDA Graph capture/replay requires deferred flush handling. Debug logging itself can add synchronization and disk I/O, so a correctness/replay trace must not be reused as an uninstrumented performance sample.

0x07I One Evidence Row Binds One Key To One Observation

M4.2’s executable evidence-bundle schema remains the measurement handoff:

docs/numinens-evidence/m4-m5-p1/kernel_bundle_template.json
docs/numinens-evidence/m4-m5-p1/validate_kernel_bundle.py

For M4.5, one measured row must bind:

environment:
    loaded framework and extension versions
    package/build hashes where available
    GPU model, compute capability, driver, runtime

dispatch:
    complete human-readable key and canonical digest
    candidate domain and ordered policy
    eligibility/rejection diagnostics
    selected backend and internal mode if reported
    plan key and replan event if stateful

execution:
    profiler trace path
    exact kernel symbols and launch counts
    temporary allocations and graph mode

correctness:
    reference path and tolerance
    output/LSE/cache-state comparison

measurement:
    warmup policy
    raw synchronized timing samples
    profiler counters with numerator/denominator definitions

Changing $S_q=1$ to an MTP chunk, fp16 K/V to FP8 K/V, dense K/V to a block table, page size, mask kind, $H_{kv}$, head dimension, graph mode, or tensor stride creates a new dispatch key and therefore a new evidence row. Aggregating those paths into one latency number destroys the relationship between admission and measurement.

The source manifest records repository HEADs observed on 2026-07-28. An observed source revision does not prove that a loaded wheel contains it. A real run must preserve the loaded package/build revision and the profiler artifact from that run.

0x07J Executable Dispatch Evidence And Failure Closure

The dispatch evidence bundle adds:

fixture:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/dispatch_admission_fixture.json

invalid fixtures:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_dispatch_admission_fixtures.json

oracle:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/dispatch_admission_oracle.py

generated report:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/dispatch_admission_report.json

tests:
    docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_dispatch_admission_oracle.py

The report contains no profiler kernel symbol and zero timing samples. Its machine-readable claim ceiling is therefore:

backend_selection_only_not_kernel_execution_or_performance

Even that selected backend is synthetic: the report proves the article’s admission algebra and evidence policy, not a local GPU dispatch.

Failure	Invalid assumption	Consequence	Closure
infer kernel from API name	semantic function names implementation	false performance explanation	capture eligibility, selection, and profiler symbol separately
count wrong-phase backend as fallback	registry equals candidate domain	misleading fallback telemetry	construct platform/phase domain first
keep only first rejection	one failed predicate explains call	secondary incompatibility is hidden	preserve complete reason vector
force backend then silently fall back	request is only a preference	test passes on unintended path	forced policy fails closed
assume math handles paged K/V	reference path accepts every layout	undefined address semantics or hidden gather cost	require explicit address/gather contract
reuse stale plan	run() tensors determine everything	wrong workspace, metadata, or graph state	hash declared static plan projection
omit determinism from key	all correct kernels are bitwise equal	irreproducible comparisons	record backend, precision, and reduction policy
treat selection log as profiler proof	backend class names one kernel	wrong launch/traffic attribution	preserve profiler trace and symbols
benchmark with debug dumping	observability has zero overhead	synchronization/I/O contaminates latency	separate debug and performance runs
average different keys	all decode calls are one population	regressions and fallbacks disappear in aggregate	one evidence row per immutable key

0x08 Phase Integration: Training, Prefill, Append, Mixed Batches, And Decode

The attention equation is shared across phases, but the state machine around the equation is not. A training call owns backward state and usually no persistent serving cache. A prefill constructs cache state. An append call must read an old cache while adding several ordered rows. A one-token decode is the boundary case with one new row. A mixed serving batch contains several of those contracts at once.

The scheduler policy that chose those requests belongs to M5.2, working over the request state that M5.1 defines. This section starts later: it consumes an immutable microbatch manifest and asks what attention is allowed to read, what it may write, and which launch composition preserves those facts.

0x08A One Equation Sits Inside Five Different State Machines

Contract	Query rows	K/V source	Persistent mutation	State required after forward	Backward
causal training	$S$ per sequence	current training tensors	none in the serving cache	output plus LSE/recompute state; RNG state if dropout	$dQ,dK,dV$
prefill	$C>0$, old length $T=0$	new prompt K/V	construct $C$ cache rows	committed prompt cache	no
append/chunked prefill	$C>1$, $T>0$	old cache plus $C$ staged K/V rows	extend cache from $T$ to $T+C$	committed appended rows	no
one-token decode	$C=1$, $T>0$	old cache plus one staged K/V row	extend cache from $T$ to $T+1$	one committed row	no
mixed serving batch	request-specific $(T_b,C_b)$	request-specific cache rows/pages	several independent extensions	packed outputs and per-request commits	no

The differences are not naming conventions. They change:

semantic state:   causal positions and visible keys
storage state:    temporary tensors versus persistent K/V
mutation state:   no write, initial construction, or append
launch state:     query tiles, K/V splits, or mixed phase owners
autograd state:   saved LSE/RNG and backward versus inference-only

PyTorch’s SDPA is a stateless semantic interface from the caller’s point of view; the caller still owns any persistent cache. It also always applies the specified dropout_p, so evaluation code must pass 0.0 explicitly. (PyTorch SDPA documentation) By contrast, FlashAttention’s documented flash_attn_with_kvcache interface can update supplied K/V caches in place and explicitly does not support a backward pass. These are different APIs because they own different state. (FlashAttention repository interface)

0x08B Bottom-Right Causality Follows From Old Length $T$ And New Length $C$

For one serving request, freeze:

T = number of committed K/V rows before this operation
C = number of new query rows and staged K/V rows
i = local new-row index, 0 <= i < C

This $T$ is narrower than the $T$ of the opening and Sections 0x01-0x04, which counted every key row visible to the decode query. Here $T$ excludes the rows staged by this call, so a one-token decode reads $T+1$ keys (Section 0x08D): the earlier visible width $T$ is this section’s $T+1$.

New query row $i$ has absolute sequence position $T+i$. Under ordinary causal self-attention it may read every old row and new rows through itself, but not a later row in the same append chunk:

$$p_i=T+i, \qquad \mathcal A_i=\{0,1,\ldots,T+i\}=[0,T+i+1).$$

This is the bottom-right alignment required when query and K/V lengths differ. The full logical score rectangle has $C$ rows and $T+C$ columns:

$$N_{\mathrm{rect}}(T,C)=C(T+C).$$

Summing the allowed prefix length over query rows gives the visible cells:

$$\begin{aligned} N_{\mathrm{visible}}(T,C) &=\sum_{i=0}^{C-1}(T+i+1)\\ &=CT+\sum_{j=1}^{C}j\\ &=CT+\frac{C(C+1)}{2}. \end{aligned}$$

The difference is exactly the future part of the new chunk:

$$N_{\mathrm{causal\ masked}} =N_{\mathrm{rect}}-N_{\mathrm{visible}} =\frac{C(C-1)}{2}.$$

That last quantity does not depend on $T$: every old row is visible, while only future rows inside the new chunk are causally hidden. These are logical score cells, not measured FLOPs, tile count, or DRAM transactions. Tile rounding, page segmentation, split reduction, and backend fusion belong to separate ledgers.

The phase names are specializations of the same coordinates:

prefill:    T = 0, C > 0
append:     T > 0, C > 1
decode:     T > 0, C = 1
post state: T_post = T + C, after a valid commit

0x08C Prefill, Append, And Decode Share Algebra But Not Cache History

The phase-integration fixture makes the boundary concrete:

Case	$(T,C)$	Rectangle	Visible	Causally masked	Post-commit length
prefill	$(0,5)$	$25$	$15$	$10$	$5$
append	$(5,3)$	$24$	$21$	$3$	$8$
decode	$(8,1)$	$9$	$9$	$0$	$9$

For the append row trace, the old cache is [a0,a1,a2,a3,a4] and the staged rows are [a5,a6,a7]:

query a5 at absolute position 5 -> visible [a0..a5]
query a6 at absolute position 6 -> visible [a0..a6]
query a7 at absolute position 7 -> visible [a0..a7]

An upper-left triangular mask would be wrong for this non-square call: it would align query row zero with key row zero instead of absolute position five. FlashAttention’s documented K/V-cache API states bottom-right causal alignment for unequal query and K/V lengths and shows the same two-row/five-key pattern.

Cache append should be reasoned about as a logical transaction:

def append_attention(request):
    T = request.committed_kv_length
    C = len(request.new_tokens)
    assert request.cache_capacity >= T + C

    new_k, new_v = project_kv(request.new_hidden)     # C rows
    staged = stage_rows(request.cache_row_id, T, new_k, new_v)

    # Query i may read old rows [0:T) and staged rows [T:T+i+1).
    out = attention_bottom_right_causal(
        q=request.q,
        old_cache=request.cache[0:T],
        staged_rows=staged,
        absolute_q_positions=range(T, T + C),
    )

    validate_output_and_metadata(out, request)
    commit_staged_rows(request.cache_row_id, T, staged)
    request.committed_kv_length = T + C
    return out

“Transaction” here specifies visibility and commit semantics, not that every library supplies rollback. A fused in-place API may require all capacity, identity, and metadata validation before launch because the operation itself mutates cache storage. The FlashAttention interface, for example, requires the cache to be large enough before optional K/V rows are appended in place.

0x08D One-Token Decode Is The $C=1$ Boundary, Not A Small Prefill Schedule

Substituting $C=1$ gives:

$$N_{\mathrm{visible}}(T,1)=T+1, \qquad N_{\mathrm{causal\ masked}}(1)=0.$$

There is no future row inside a one-token chunk. Semantically, decode is the smallest append. Computationally, it is the boundary where the query-row axis collapses. That is why Sections 0x01-0x04 introduced K/V-axis splitting, partial-state workspaces, paged address translation, and exact reduction.

Calling the same broad API for prefill and decode does not imply that one implementation or launch geometry handled both. The immutable dispatch key from 0x07 must include phase and shape, while a profiler trace is still required to identify the selected kernel.

0x08E Training Reuses The Visibility Algebra But Owns Different State

For causal training with sequence length $S$, setting $T=0,C=S$ recovers the same $S(S+1)/2$ visible-cell count. That algebraic reuse does not turn training into cache construction:

training forward:
    consume current Q/K/V tensors
    produce O and compact softmax state such as LSE
    preserve dropout RNG state or an equivalent reproducible contract

training backward:
    consume dO plus saved/recomputed forward state
    recompute score/probability tiles as required
    produce dQ, dK, dV

serving prefill:
    consume prompt Q/K/V
    produce O and persistent prompt K/V rows
    do not retain an autograd graph for decode

The phase-integration training fixture uses $S=4$: a $16$-cell rectangle, $10$ visible causal cells, and $6$ masked cells. It requires backward, LSE, and RNG state for nonzero dropout, while explicitly forbidding persistent serving-cache mutation. The fixture does not prescribe one backward kernel or checkpointing policy; those implementation alternatives remain version and framework dependent.

0x08F A Mixed Batch Needs A Per-Request Manifest, Not One Global Phase Label

For request $b$, retain $(T_b,C_b)$ and a stable cache-row identity. Packed query offsets are a prefix sum:

$$\mathrm{qo\_indptr}[b+1] =\mathrm{qo\_indptr}[b]+C_b.$$

The mixed-batch visible-cell ledger is:

$$N_{\mathrm{visible}}^{\mathrm{batch}} =\sum_b\left(C_bT_b+\frac{C_b(C_b+1)}{2}\right).$$

The fixture combines three requests:

Request	Phase	$(T_b,C_b)$	Query slice	Visible / rectangle	Cache length transition
mix_prefill	prefill	$(0,4)$	[0:4)	$10/16$	$0\to4$
mix_append	append	$(6,2)$	[4:6)	$15/16$	$6\to8$
mix_decode	decode	$(9,1)$	[6:7)	$10/10$	$9\to10$
total	mixed	-	qo_indptr=[0,4,6,7]	$35/42$	7 rows appended

A naive common envelope with batch $3$, maximum query length $4$, and maximum post-append K/V length $10$ contains $3\times4\times10=120$ cells. Of these, $78$ lie beyond even the three request-local rectangles. That number describes a padding envelope only. It is not a claim that a fused or masked backend executes 120 score operations.

Every packed output row must scatter back to the same request that supplied its query, and every appended K/V row must commit to that request’s cache_row_id, not its transient position in the active batch. This reuses the identity distinction derived in 0x04.

0x08G Four Integration Strategies Preserve The Same Per-Request Contract

Strategy	Composition	Strength	Cost or restriction
partition by phase	gather phase groups, launch specialized owners, scatter outputs	simple specialization boundary	more launches and gather/scatter metadata; performance is runtime dependent
unified mixed wrapper	one packed manifest, per-request prefill/decode dispatch inside the wrapper	avoids one global phase label	wrapper layout, plan, mask, and backend support must match every request
prefill/decode overlap	co-schedule supported prefill-side and batch-decode work	can exploit complementary resource profiles	not a universal interface for arbitrary prefill/append/decode mixtures
padded fallback	common tensor envelopes plus explicit masks	broad semantic escape path	extra materialization and padding envelope; measured cost requires profiling

FlashInfer’s current BatchAttention documentation exposes the unified option: qo_indptr, paged K/V offsets, and per-request K/V lengths are passed to plan(), and the wrapper dispatches prefill-style versus decode-style work per request. (FlashInfer attention API) Its K/V-layout documentation separately identifies paged-prefill wrappers for prefill/append attention, decode wrappers, and an append API whose pages must already be allocated. (FlashInfer K/V layout)

POD-Attention is a different composition. The paper motivates concurrent prefill and decode because the phases stress different resources; the current FlashInfer POD wrapper documents a single-request prefill side and a paged batch-decode side in one launch. This is a concrete interface, not permission to assume every append layout or mixed mask is accepted. (POD-Attention paper, FlashInfer POD API)

The alternatives therefore belong in a design comparison, not a winner table. Correctness is the invariant $(T_b,C_b)$ visibility and cache identity; selection requires the 0x07 admission contract; performance requires a phase-keyed runtime measurement.

0x08H Phase-Aware Planning And Cache Mutation Must Be Separate Decisions

def freeze_microbatch(active_requests):
    manifest = []
    for request in active_requests:
        T = request.committed_kv_length
        C = len(request.new_tokens)
        phase = (
            "prefill" if T == 0 and C > 0 else
            "decode"  if T > 0 and C == 1 else
            "append"  if T > 0 and C > 1 else
            fail("invalid active request")
        )
        manifest.append({
            "request_id": request.id,
            "cache_row_id": request.cache_row_id,
            "T": T,
            "C": C,
            "q_range": None,              # assigned by packing
            "post_length": T + C,
            "phase": phase,
        })
    assert_unique(entry["request_id"] for entry in manifest)
    assert_unique(entry["cache_row_id"] for entry in manifest)
    return assign_qo_indptr(manifest)


def execute_manifest(manifest, policy):
    validate_capacity_pages_masks_and_plan(manifest)
    if policy == "partition_by_phase":
        outputs = run_specialized_groups(group_by_phase(manifest))
    elif policy == "unified_mixed":
        outputs = run_per_request_mixed_wrapper(manifest)
    elif policy == "prefill_decode_overlap":
        require_supported_overlap_shape(manifest)
        outputs = run_overlap_wrapper(manifest)
    else:
        outputs = run_explicitly_masked_fallback(manifest)

    validate_output_row_identity(outputs, manifest)
    commit_each_request_to_its_cache_row(manifest)
    return scatter_to_request_order(outputs, manifest)

The manifest is immutable during one operation. Scheduling another token, allocating or evicting pages, changing active order, or admitting a new request creates a new manifest. The lifecycle and page-allocation policies remain in M5.1 through M5.3; M4.5 owns only the kernel integration contract once those decisions are frozen. Speculative branch verification adds another state machine and remains in M7.1.

0x08I Executable Phase Evidence And Failure Closure

The synthetic evidence bundle is:

docs/numinens-evidence/m4-5-decode-kernel-boundaries/phase_integration_fixture.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_phase_integration_fixtures.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/phase_integration_oracle.py
docs/numinens-evidence/m4-5-decode-kernel-boundaries/phase_integration_report.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_phase_integration_oracle.py

The oracle reconstructs every visible cache prefix, verifies staged and committed token identity, derives packed offsets and work ledgers, and rejects future-row leakage, stale lengths, duplicate cache identities, and invalid training state. It has no local GPU build, selected-kernel symbol, timing sample, hardware counter, or performance claim.

Failure	Invalid assumption	Consequence	Closure
align causal mask upper-left for append	local query row zero is absolute position zero	old history is hidden or wrong rows are visible	derive absolute positions from $T+i$
expose all staged rows to every append query	staged means causally committed	earlier queries attend to future tokens	enforce visible prefix [0,T+i+1)
classify a mixed batch from global query length	every request has one phase	wrong backend or mask for some requests	retain $(T_b,C_b)$ and packed offsets
use active batch index as cache row	active order is persistent identity	K/V corruption across requests	freeze cache_row_id separately
mutate cache before validating capacity/pages	in-place append is rollback-safe	partial or out-of-bounds state	prevalidate the complete mutation contract
reuse training dropout in evaluation	module mode disables functional dropout	stochastic inference	pass dropout_p=0.0 explicitly
treat wrapper capability as kernel evidence	supported API proves selected launch	unsupported performance narrative	retain dispatch and profiler evidence separately
call padded envelope measured work	shape allocation equals executed operations	false FLOP/traffic ledger	label logical, materialized, and measured ledgers separately

0x09 Paper-By-Contract Comparison: Fixed Splits, Work-Centric Reduction, And Planned Serving

A paper name is not a backend contract. Two methods can both say “parallelize decode attention over K/V” while disagreeing about all of the following:

what one worker owns;
whether split size is fixed per output or balanced globally;
which partial state crosses worker boundaries;
where reduction happens;
whether the plan is static, heuristic, or rebuilt from ragged lengths;
which cache-address program feeds the kernel;
what numerical guard preserves the softmax contract;
which benchmark coordinate supports the performance claim.

The comparison must therefore begin from contracts, not reported speedup.

0x09A Nine Axes Prevent A False Ranking

This section freezes nine comparison axes:

Axis	Question that must be answered
problem phase	training, prefill, append, one-token decode, or a mixed batch?
parallel axis	query tiles, fixed K/V splits, global work tiles, or planned ragged chunks?
work granularity	one output owner, one partial output, one LeanTile, or one queue item?
partial-state ABI	(m,l,u), (LSE,O), shared-shift numerator/denominator, or another sufficient state?
reduction topology	owner-local recurrence, second kernel, cross-CTA reduction, or persistent contraction?
planning locus	compile/launch configuration, paper heuristic, CPU plan(), or serving scheduler?
cache-address contract	dense views, ragged pointers, explicit pages, virtual continuity, or composable sparse formats?
numerical policy	exact merge, shared-shift guard and fallback, reduction order, dtype, determinism?
measurement coordinate	which model, shape distribution, hardware, engine, baseline, and metric?

The matrix is deliberately asymmetric. FlashDecoding++ is an inference engine with attention, flat-GEMM, buffering, and hardware-adaptive dataflow changes; it is not merely another split-reduction kernel. FlashInfer is a serving attention engine with a planner, composable cache formats, JIT templates, and persistent execution; it is not merely a paper formula. PagedAttention, vAttention, FlashMask, and POD-Attention operate on orthogonal axes and are handled separately in 0x09F.

0x09B Flash-Decoding Adds A Fixed Per-Output Split And A Second Reduction Level

Flash-Decoding’s author note defines three logical steps:

1. partition one K/V sequence into views;
2. compute one FlashAttention result and one LSE scalar for every query row and split;
3. reduce split outputs using those LSE values.

Only the second and third steps require kernels. The key distinction from FA2 is not the attention equation. It is the new owner axis:

$$(b,h_q,q_{tile}) \quad\longrightarrow\quad (b,h_q,q_{tile},s_{kv}).$$

For split $j$, define normalized partial output $O_j$ and

$$L_j=\log\sum_{i\in I_j}e^{s_i}.$$

The global reference is

$$L=\operatorname{logsumexp}(L_1,\ldots,L_S),$$

and the exact output target is

$$O=\sum_{j=1}^{S}e^{L_j-L}O_j.$$

This explains why normalized outputs alone cannot be averaged and why one extra scalar per row and split is sufficient. Section 0x02 derives the same composition from canonical allowed-set summaries; the paper comparison only binds that algebra to a two-kernel topology.

partials = parallel_for(fixed_kv_splits, lambda split:
    flash_attention_partial(q, kv_view(split), return_lse=True)
)

# A separate owner sees every partial for the same output identity.
output = lse_weighted_reduce(partials)

The fixed split count is a launch policy, not a theorem. Too few splits leave SMs idle; too many increase partial-state writes, launch work, and reduction cost. Equal split count per output also does not imply equal work when request lengths are ragged.

0x09C FlashDecoding++ Changes The Numerical Coordinate, Then Adds Engine-Wide Choices

The original local A19 article describes FlashDecoding++ as approximating the global maximum. That wording is incomplete. A common shift does not alter the exact real-arithmetic softmax ratio. For any finite shared shift $\phi$,

$$O= \frac{\sum_i e^{s_i-\phi}v_i} {\sum_i e^{s_i-\phi}}.$$

Partition the row into disjoint sets $I_j$ and define

$$n_j(\phi)=\sum_{i\in I_j}e^{s_i-\phi}v_i, \qquad l_j(\phi)=\sum_{i\in I_j}e^{s_i-\phi}.$$

Because every partition uses the same frame,

$$O= \frac{\sum_j n_j(\phi)} {\sum_j l_j(\phi)}.$$

No cross-partition exponential rescaling is needed. That is the attraction. The danger is finite representation:

phi too small:
    some exp(score - phi) overflows

phi too large:
    useful terms underflow toward zero

different phi per partition:
    raw numerator/denominator sums no longer share one frame

The FlashDecoding++ paper therefore pairs its profiled shared shift with a range check and falls back to synchronized partial softmax recomputation when the guard fails. Its $[-3,3]$ interval and $\phi=6$ trace are a paper illustration, not a universal runtime default.

def guarded_shared_shift_partial(scores, values, phi, lower, upper):
    delta = scores - phi
    if any(delta <= lower) or any(delta >= upper):
        return FALLBACK_REQUIRED
    return sum(exp(delta) * values), sum(exp(delta))

partials = parallel_map(partitions, guarded_shared_shift_partial)
if any(partial is FALLBACK_REQUIRED for partial in partials):
    return recompute_with_synchronized_partial_softmax()
return sum(p.numerator for p in partials) / sum(p.denominator for p in partials)

This numerical path is only one part of FlashDecoding++. The paper also owns flat-GEMM padding/tiling, double buffering, and hardware-adaptive dataflow. Consequently, its end-to-end measurements cannot be attributed solely to the shared-shift attention path.

0x09D LeanAttention Moves From Equal Splits Per Output To Equalized Global Work

LeanAttention starts from the same associative softmax-rescaling property derived in 0x02, but changes the work unit. Instead of assigning an equal number of K/V chunks to every output, it defines LeanTiles and distributes attention work in a Stream-K-style global order.

Let output $r$ own $W_r$ K/V work units. A fixed split policy with $S$ splits creates approximately

$$w_{r,j}\approx\left\lceil\frac{W_r}{S}\right\rceil.$$

If request lengths differ, the worker loads differ even when every output has the same split count. A work-centric policy instead flattens the work volume:

$$W_{total}=\sum_r W_r, \qquad \bar{W}=\frac{W_{total}}{P},$$

then assigns approximately $\bar{W}$ units to each of $P$ workers. A worker can finish one output and continue into another. That creates two obligations:

1. it must keep partial states separated by output identity;
2. every output with multiple contributors needs an exact reduction path.

The work partition is allowed to cross an output boundary; the softmax state is not.

for cta in global_work_partitions:
    for output_fragment in cta.fragments:
        state[output_fragment.output_id] = summarize(output_fragment)
        publish_for_exact_rescaling_reduction(state[output_fragment.output_id])

LeanAttention presents this as a single fused, work-centric kernel rather than Flash-Decoding’s fixed first-stage grid followed by a separate reducer launch. That is a topology difference, not a change to the target attention row.

0x09E FlashInfer Turns Ragged Work Assignment Into A Plan/Run ABI

FlashInfer generalizes load balancing to dynamic serving lengths. Its paper planner receives query/output and K/V lengths. For query tile size $T_q$, it uses the aggregate work estimate

$$L_{kv}^{plan} \approx \frac{ \sum_i \left\lceil l_{qo}(i)/T_q\right\rceil l_{kv}(i) }{N_{CTA}}$$

to bound K/V chunks, sorts chunks by size, and greedily assigns them to the least-loaded CTA under a cost model

$$cost(l_q,l_{kv})=\alpha l_q+\beta l_{kv}.$$

Those equations describe a paper algorithm, not the exact implementation of every FlashInfer release. The paper-contract oracle integerizes the first equation with ceil and sets $\alpha=0,\beta=1$ only to expose the work-assignment contract.

FlashInfer’s deeper difference is runtime integration:

CPU plan:
    consume ragged length manifest
    build deterministic CTA work queues
    build partial-to-final output mapping
    copy plan into fixed workspace regions

GPU run:
    reuse a fixed compiled grid
    execute persistent attention/composition work
    retain fixed pointers for CUDA Graph replay

The paper explicitly avoids Stream-K atomic aggregation so identical length manifests have a deterministic aggregation order. Planning may run every generation step, but one plan can be amortized across layers with matching lengths. This is more than “choose a split count.” It is an inspector/executor ABI between ragged serving state and a graph-compatible GPU schedule.

0x09F Cache Layout, Mask Compression, And Phase Overlap Are Orthogonal Axes

Several important methods should not be inserted into a one-dimensional “decode kernel ranking”:

Method	Axis it changes	Contract it does not replace
PagedAttention	logical blocks, physical pages, allocator and block-table addressing	K/V work partition and partial-softmax reduction
vAttention	contiguous virtual addresses backed by physical-page mapping	K/V work partition and partial-softmax reduction
FlashMask	mask representation and SKIP/FULL/PARTIAL tile classification	ragged decode scheduling and cache allocation
POD-Attention	concurrent prefill/decode resource allocation	each request’s attention and cache-commit semantics
FA3/FA4	Hopper/Blackwell pipeline, memory movement, and precision mechanisms	serving scheduler and request lifecycle

These axes compose only when their interfaces compose. A K/V split still needs the Section 0x04 address translator for paged storage. A planned ragged chunk still needs the mask and dispatch contracts from Sections 0x05-0x07. A POD launch still needs the phase-integration phase manifest. FA3/FA4 hardware pipelines remain M4.6’s owner.

0x09G One Ragged Workload Exposes The Scheduling Difference

Collapse batch/head identity into two output groups solely for this teaching trace:

long output:   4096 visible K/V work units
short output:  1024 visible K/V work units
workers:       8 CTAs
fixed splits:  4 per output

The total and ideal mean are

$$W=4096+1024=5120, \qquad \bar{W}=5120/8=640.$$

Fixed per-output splits. Four chunks for each output produce

CTA loads = [1024,1024,1024,1024,256,256,256,256]

The logical max-to-mean ratio and idealized work efficiency are

$$\rho=\frac{1024}{640}=1.6, \qquad \eta_{work}=\frac{5120}{8\cdot1024}=0.625.$$

Global work partition. Flattening 5120 units into eight intervals gives [640 x 8]. CTA 6 owns 256 units from the long output and 384 from the short output. Work is equalized, but CTA 6 must publish two output-specific states.

FlashInfer-style teaching plan. The integer chunk limit is 640. Splitting each output independently yields sorted lengths

[640,640,640,640,640,640,640,384,256].

A deterministic least-loaded queue assignment puts the final 384 and 256 chunks on the same CTA, again producing [640 x 8] without making one chunk cross an output identity.

Strategy	Work balance in this fixture	Extra obligation
fixed four-way split	max/mean 1.6	simple per-output mapping; idle tail in the teaching schedule
global equal work	max/mean 1.0	one CTA may own fragments from multiple outputs
planned variable chunks	max/mean 1.0	planner, queue metadata, partial-to-final map, deterministic reduction order

These are logical work-unit ratios. Equal K/V-token counts do not prove equal cycles, occupancy, bandwidth, or latency because address layout, tile tails, head grouping, cache hits, resource limits, and reduction overhead remain unmeasured.

0x09H Paper Benchmarks Stay Attached To Their Coordinates

The papers do not evaluate one interchangeable kernel under one shared manifest:

Source	What its measurement can support	What it cannot establish here
Flash-Decoding author note	source-reported CodeLlama-34B batch-1 decode over stated context lengths	current library behavior or another model/batch/backend
FlashDecoding++	source-reported engine results combining attention, flat GEMM, buffering, and adaptive dataflow	isolated shared-shift speedup in this repository
LeanAttention	source-reported kernel sweeps and OPT end-to-end coordinates on the paper’s hardware/configurations	universal win over fixed splits; the paper includes at least one near-tie coordinate
FlashInfer	source-reported kernel and serving results with named engines, distributions, GPUs, software, and formats	behavior of an unpinned installed package or selected local backend

Therefore this comparison records each paper’s measurement coordinate but imports no number as a local expectation. Runtime comparison needs a benchmark manifest, selected-kernel evidence, synchronized timings, output tolerances, warmup, and environment pinning.

0x09I Executable Paper Contract And Failure Closure

The machine-readable artifacts are:

docs/numinens-evidence/m4-5-decode-kernel-boundaries/paper_contract_fixture.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_paper_contract_fixtures.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/paper_contract_oracle.py
docs/numinens-evidence/m4-5-decode-kernel-boundaries/paper_contract_report.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_paper_contract_oracle.py

The oracle checks frozen paper versions, sufficient split state, the FlashDecoding++ guard/fallback, deterministic FlashInfer aggregation, orthogonal method classification, all three work schedules, and the unmeasured evidence ceiling. It does not implement any paper kernel.

Failure	Invalid inference	Closure
call every method “Split-K attention”	planning and reduction topology are interchangeable	compare all nine contract axes
average Flash-Decoding outputs	normalized partials carry equal mass	retain and merge LSE
sum shared-shift states with different $\phi$	partials share one exponential frame	freeze one shift or rescale before composition
omit FlashDecoding++ fallback	profiled score range is a proof for every row	guard every row and fail to synchronized recomputation
let global work cross output identity silently	work interval and softmax row identity are the same axis	publish separate state per output fragment
use atomics while claiming deterministic FlashInfer order	mathematical associativity implies bitwise determinism	freeze reduction order and runtime policy
call PagedAttention a reduction strategy	cache layout chooses work ownership	keep address and schedule contracts separate
report [640 x 8] as measured occupancy	equal logical work means equal GPU duration	require profiler and timing evidence

0x0A Version-Pinned Source Traces: From Public API To Kernel Surface

The paper contracts in 0x09 answer what an algorithm proposes. They do not answer what a particular repository revision implements. Names such as “FlashAttention,” “FlashInfer,” or “SDPA” are too broad for that job: each repository contains several generations, backends, feature branches, and fallbacks. The version-pinned source trace therefore changes coordinates again:

paper coordinate:
    named algorithm + paper version + stated workload

source coordinate:
    repository commit + path + content hash + symbol span + call-chain layer

runtime coordinate:
    installed package + loaded binary + build flags + immutable call key

execution coordinate:
    dispatch observation + profiler symbol + device trace

This section owns only the second coordinate. It can establish that one frozen source graph contains an API-to-kernel path. It cannot establish that the path was built, loaded, selected, executed, correct for a local call, or fast.

0x0AA A Source Name Is Not An Immutable Coordinate

The evidence fixture pins 14 files and 34 symbol probes across four repositories:

Repository coordinate	Files / probes	Exact path under examination	Maximum source conclusion
FlashAttention 14c377950125c70b7a9dabf9c561fca53715ac7d	3 / 8	CUDA cache-aware forward and split-K/V launch	a split-capable path, partial workspace, and combine kernel exist
FlashInfer 2deed6c15e8c8410763d6e8adedc8ca69597e957	4 / 10	CUDA-core paged batch decode with use_tensor_cores=false	occupancy-aware partition planning and conditional merge exist
vLLM 88402a41c4ab272ebbbd33f4a77fbbac0431cbb9	4 / 10	CUDA backend admission through FlashAttention call surface	registry, rejection, selection, metadata, and call surface exist
PyTorch a57db29aa6d98118fdd27a7d509ab3525a750669	3 / 6	stateless CUDA SDPA policy and operator dispatch	enablement, ordered admission, selection, and operator switch exist

The full 40-character commit is necessary but not sufficient. A valid source claim also binds the repository-relative path, SHA-256 of the retrieved bytes, symbol name, line span, and the contract attributed to that span. The content hash catches a mismatched download; the symbol span prevents a nearby comment or unrelated branch from becoming evidence for the claim.

0x0AB FlashAttention Closes API, Heuristic, Workspace, And Reduction Layers

At the pinned FlashAttention coordinate, the chain is:

flash_attn_with_kvcache                         Python cache-aware API
    -> mha_fwd_kvcache                          C++ binding and validation
    -> num_splits_heuristic                     split planner
    -> set_params_splitkv                       partial-state workspace
    -> run_mha_fwd                              standard/split dispatch
    -> flash_fwd_splitkv_kernel                 partial producer
    -> flash_fwd_splitkv_combine_kernel         reduction

The source heuristic makes the split tradeoff concrete. Let $G=B H_q M_q$ be the unsplit producer-block count, $N_{SM}$ the effective SM count passed to the heuristic, $N_K$ the number of K/V blocks, and $s$ one eligible split count. The implementation evaluates

$$w(s)=\frac{Gs}{N_{SM}}, \qquad \eta(s)=\frac{w(s)}{\lceil w(s)\rceil}.$$

It caps $s$ by the requested maximum, $N_{SM}$, and $N_K$. It also rejects a candidate whose K/V blocks per split are unchanged from the preceding candidate:

$$\left\lceil\frac{N_K}{s}\right\rceil = \left\lceil\frac{N_K}{s-1}\right\rceil.$$

Among eligible candidates, the implementation returns the smallest $s$ whose efficiency reaches at least 85% of the best candidate efficiency. This is not simply argmax occupancy: the smallest near-best split limits the extra HBM round trip for partial state.

best = max(efficiency(s) for s in eligible_splits)
chosen = first(s for s in eligible_splits if efficiency(s) >= 0.85 * best)

If the chosen split count exceeds one, the binding allocates float partial LSE and output tensors with leading split dimensions. The launch path then exposes separate producer and combine kernels, matching the sufficient-state and workspace derivations in 0x02 and 0x03.

0x0AC Split-Capable Dispatch Does Not Mean More Than One Split Ran

The same pinned binding can force the split-capable dispatch family for cache append, cache-row remapping, or paged K/V. run_mha_fwd then distinguishes num_splits <= 1 && !force_split_kernel from the split-capable branch. Therefore these statements are different:

supported:
    the call requires the split-capable kernel family

not implied:
    num_splits > 1
    the partial workspaces are non-empty
    the combine kernel executed

This distinction prevents an API feature such as paged K/V from being reported as observed parallel K/V splitting. The actual split count belongs in runtime dispatch evidence.

0x0AD FlashInfer Materializes A Plan/Run ABI For This Decode Coordinate

The pinned FlashInfer trace deliberately narrows the repository to BatchDecodeWithPagedKVCache on the CUDA-core branch with use_tensor_cores=false:

BatchDecodeWithPagedKVCacheWrapper.plan
    -> BatchDecodeWithPagedKVCachePlan
    -> BatchDecodeWithPagedKVCacheWorkEstimationDispatched
    -> DecodePlanInfo + workspace offsets

BatchDecodeWithPagedKVCacheWrapper.run
    -> BatchDecodeWithPagedKVCacheRun
    -> BatchDecodeWithPagedKVCacheDispatched
    -> VariableLengthMergeStates, only when partitioned

The planner first queries active blocks per SM for the selected kernel and forms an occupancy-derived grid capacity:

$$G_{max}=N_{SM}\,B_{active/SM}.$$

With $H_{kv}=H_q/GQA\_group$, the unsplit producer grid is approximately $B H_{kv}$. If it already fills $G_{max}$, the plan remains unsplit. Otherwise, a binary search chooses a maximum page count per chunk that increases the partitioned batch toward the available grid. The resulting page chunks become three explicit index structures:

request_indices[j]    original request owning chunk j
kv_tile_indices[j]    chunk index within that request
o_indptr[b:b+2]       partial-state range reduced into output b

DecodePlanInfo stores offsets for those arrays, the K/V chunk size, graph padding, a validity mask, and optional float partial output/LSE buffers. run() reconstructs pointers from that plan. A direct output path is used when not partitioned; a partitioned path writes partial state and calls the variable-length merge by o_indptr.

This is a source-level realization of the same semantic obligations derived earlier: ragged chunk ownership, output identity, sufficient split state, and an exact reduction map.

0x0AE The FlashInfer Paper Planner Is Not This Pinned Batch-Decode Scheduler

Section 0x09E described the FlashInfer paper’s sorted-cost tasks, least-loaded CTA assignment, and persistent attention/contraction framing. Those remain valid paper-level claims. They are not the exact scheduler found in this pinned CUDA-core batch-decode path.

Coordinate	Planning mechanism	Materialized artifact	Reduction topology
FlashInfer paper contract	sorted costs and least-loaded assignment under the paper model	deterministic CTA queues and partial-to-final mapping	persistent attention/contraction framing
pinned CUDA-core batch decode	occupancy estimate plus binary-search page-chunk sizing	request indices, K/V tile indices, output indptr, workspace offsets	direct output or partitioned output plus variable-length merge

Other branches in the same Python wrapper include different backends and specializations. A repository-wide name cannot transfer one branch’s planner to another. This is why the version, API branch, and feature controls belong in the source coordinate.

0x0AF vLLM Adds Registry, Admission, Selection, And Plan Metadata Above The Kernel API

At its pinned coordinate, vLLM adds several layers above FlashAttention:

get_attn_backend
    -> AttentionBackendEnum
    -> CUDA _get_backend_priorities
    -> get_valid_backends
    -> get_attn_backend_cls
    -> FlashAttentionMetadataBuilder.build
    -> flash_attn_varlen_func

Registry membership only makes a backend discoverable. CUDA platform policy constructs a candidate order from device/model coordinates. Each candidate’s configuration check produces rejection reasons. A forced backend fails when invalid; automatic selection chooses the highest-priority valid candidate. The FlashAttention metadata builder then derives split-related metadata under CUDA Graph and batch-invariance policy before the call surface receives block tables, lengths, scheduler metadata, and split controls.

This chain connects the abstract Section 0x07 selector to concrete version-scoped source. Its ceiling is still a call surface. It does not identify the loaded FlashAttention binary or prove which compiled symbol ran.

0x0AG PyTorch SDPA Is A Stateless Policy And Operator Boundary

The pinned PyTorch chain is shorter because its owner contract is different:

sdpa_kernel context manager
    -> priority_order
    -> can_use_flash_attention and other capability predicates
    -> select_sdp_backend
    -> scaled_dot_product_attention operator switch

The context manager changes enabled backends and optional priority order, then restores prior state. The CUDA selector evaluates ordered capability predicates and returns the first passing backend; when none passes, diagnostic mode reruns the checks to surface rejection reasons. The operator dispatches according to that selected enum.

This source path owns stateless scaled-dot-product attention. It does not own page allocation, K/V append, transaction commit, or cache release. A serving engine can call SDPA inside a larger state machine, but cache ownership must be proven in that engine’s source and runtime trace, not inferred from the SDPA operator.

0x0AH Static Source Evidence Stops Two Levels Before Kernel Observation

The evidence ladder prevents source inspection from silently becoming a runtime claim:

Level	Evidence	Supported statement
1	commit, path, content hash, symbol	the exact source is present
2	valid acyclic chain with every required layer	the pinned source path closes
3	package version, binary hash, build flags	the loaded binary coordinate is identified
4	dispatch log bound to an immutable call key	runtime selection was observed
5	profiler symbol and device trace	one kernel execution was observed
6	synchronized samples, environment, correctness tolerance	performance was measured

The version-pinned source audit reaches level 2. A source-visible split heuristic is not an observed split count. A selected backend class is not a profiler symbol. A profiler symbol is not a latency distribution. Later runtime diagnostics must preserve the same commit/build/call key while adding evidence rather than replacing it.

0x0AI Executable Source Evidence And Failure Closure

The version-pinned evidence bundle is:

docs/numinens-evidence/m4-5-decode-kernel-boundaries/source_trace_fixture.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_source_trace_fixtures.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/source_trace_oracle.py
docs/numinens-evidence/m4-5-decode-kernel-boundaries/source_trace_report.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_source_trace_oracle.py

The oracle validates full commits, SHA-256 source identities, symbol probes, acyclic call graphs, required-layer closure, coordinate boundaries, and the level-2 evidence ceiling. Its invalid fixtures fail on floating revisions, missing hashes, duplicate file identities, missing nodes, cyclic chains, missing layers, paper/source conflation, selection/execution conflation, stateless-cache ownership, and invented profiler symbols.

Failure	Invalid inference	Closure
cite main or a package name	repository identity fixes implementation	pin commit, path, hash, symbol, and span
find a kernel symbol in source	source presence proves call-chain reachability	close API-to-kernel edges and every required layer
copy the paper planner onto one source branch	paper family and implementation coordinate are identical	compare pinned branch mechanics explicitly
equate split-capable dispatch with num_splits > 1	kernel family determines runtime split count	capture actual dispatch state later
equate selected vLLM backend with executed kernel	framework class identifies loaded device symbol	require binary and profiler evidence
assign K/V lifecycle to PyTorch SDPA	attention operator owns serving state	trace allocator/append/commit in the serving owner
report source heuristic as measured speedup	implementation intent predicts runtime outcome	require level-6 benchmark evidence

0x0B Runtime Evidence: Loaded Artifacts, Dispatch Diagnostics, And Measurement Closure

The version-pinned source trace closed source graphs. It did not identify an imported wheel, a loaded extension object, one runtime selection, or one CUDA launch. Those are different observations. This loop owns the protocol that joins them without promoting any missing link into evidence.

The owner question is narrower than “which backend is fastest?”:

For one immutable decode call, what must be preserved before a source-level kernel family can become a loaded-artifact, selected-backend, profiler-observed, correctness-checked, and measured runtime claim?

The answer is a monotone evidence bundle. Let $R_\ell$ be the set of required fields at evidence level $\ell$. The highest defensible claim is

$$L^*=\max\left\{\ell:\bigcup_{j=1}^{\ell}R_j \text{ is present and internally consistent}\right\}.$$

Evidence cannot skip a level. A trace cannot repair an unknown binary. Timing cannot repair an unknown call key. A passing latency run cannot repair a failed correctness comparison.

0x0BA A Distribution Version Is Not A Loaded Binary Identity

There are at least four identities that are often compressed into “the installed version”:

Identity	Example evidence	What it proves	What it does not prove
source coordinate	repository, 40-character commit, path, source SHA-256	the inspected implementation text	that a local wheel contains it
installed distribution	package metadata, version, wheel RECORD entries	files registered by the Python environment	that a compiled object was loaded by this process
import coordinate	module origin and extension import path	where Python resolved the module	every transitive shared object mapped by the loader
loaded-artifact coordinate	process loader map plus SHA-256 for each relevant .so	which compiled objects were mapped for this run	which symbol launched on the GPU

Python’s importlib.metadata can report distribution versions and registered files without importing the module. That makes it useful for preflight, but distribution metadata is not a process loader map. Editable installs, local rebuilds, extension caches, and transitive CUDA libraries can all make a package label insufficient.

Level 3 therefore requires a closure, not one version string:

distribution name and version
import origin
loaded compiled-object paths and SHA-256 digests
content-addressed process loader map
content-addressed build configuration
GPU name and architecture
driver and CUDA runtime versions

For PyTorch, torch.__config__.show() is one build-configuration input, while torch.cuda.get_device_properties provides the selected device properties. Neither replaces hashing the loaded attention extension.

0x0BB One Runtime Coordinate Is A Join, Not A Label

A measured row joins five state families:

$$K_{run}=H(K_{env},K_{artifact},K_{call},K_{dispatch},K_{measurement}),$$

where $H$ is a canonical content hash, not an informal concatenation. The families include:

K_env:
    host, GPU, architecture, driver, CUDA runtime, clocks/power policy

K_artifact:
    distribution, imported extension, loaded-object hashes, build flags

K_call:
    phase, B, S_q, per-request S_k, H_q, H_kv, d_qk, d_v,
    dtypes, layouts, strides, mask/window, page metadata, graph mode

K_dispatch:
    requested policy, candidate order, rejected predicates,
    selected backend, internal mode, split count, plan identity

K_measurement:
    warmup, synchronization, graph replay, allocation policy,
    raw samples, profiler tool/version, counter definitions

This derivation explains why framework=PyTorch or backend=FlashAttention cannot identify a result. A change in page size may preserve the API and alter address translation. A change in $S_q$ may switch decode to chunked prefill. A change in graph mode may reuse a plan and remove launches or allocations from the timed region. Each change creates a new $K_{run}$.

0x0BC Preflight Has A Valid Terminal State

The local capture for this repository was run on the current editing host:

Field	Observed value
operating system	Darwin 25.5.0
architecture	arm64
Python	3.9.6
nvidia-smi, nsys, ncu	unavailable
torch, flash_attn, flashinfer, vllm module specs	not found
extension import attempted	no
CUDA execution attempted	no
profiler or timing capture attempted	no
maximum local evidence level	2: source-chain closure

This is an Observed local preflight, not a failed benchmark. It proves that this Apple-Silicon host cannot supply the CUDA evidence required by levels 3–6. It does not prove that FlashAttention, FlashInfer, vLLM, or PyTorch CUDA paths are unavailable on supported systems.

Stopping is part of the protocol:

preflight = inspect_without_importing_extensions()

if not preflight.cuda_host_tool_visible:
    record_terminal_status("cuda_runtime_unavailable")
    preserve_absence_reasons()
    stop_before_import_or_execution()

Importing an extension merely to make a preflight look more complete would change process state and can initialize a CUDA context. The non-importing pass therefore records module discovery and distribution metadata separately from loaded-object evidence.

0x0BD Loaded-Artifact Closure Must Be Captured In The Running Process

On a compatible CUDA host, level 3 begins only after the target process imports the exact runtime path. A robust capture sequence is:

record_distribution_metadata()
import_target_runtime_and_extension()

record_import_origins()
record_process_loader_map()
hash_relevant_loaded_objects()
record_framework_build_configuration()
record_gpu_driver_and_runtime()

assert every claimed extension is present in the loader map
assert every recorded loaded object has a SHA-256 digest

Hashing a file named in wheel metadata before import is weaker: another object may be loaded. Hashing only the top-level extension is also incomplete when it dispatches through transitive libraries. Conversely, a loader map proves that an object is mapped, not that one of its CUDA kernels ran. That next claim belongs to profiler evidence.

Build configuration deserves its own artifact because architecture lists, compiler flags, deterministic modes, and optional backends can change the compiled kernel set without changing the Python API. The build report and loader map are content-addressed so the runtime bundle does not depend on a mutable path.

0x0BE Selection Evidence Must Bind One Human-Readable Call Key

Level 4 adds one observed dispatch record. It retains both a readable call key and its canonical digest:

call_key = {
    "phase": "decode",
    "B": B,
    "S_q": 1,
    "S_k_per_request": lengths,
    "H_q": H_q,
    "H_kv": H_kv,
    "d_qk": d_qk,
    "d_v": d_v,
    "q_dtype": str(q.dtype),
    "kv_dtype": str(k_cache.dtype),
    "cache_layout": cache_layout,
    "page_size": page_size,
    "mask": mask_policy,
    "graph_mode": graph_mode,
}

call_key_sha256 = canonical_hash(call_key)

The dispatch artifact must then preserve:

requested backend policy
ordered candidate set
eligibility result and rejection reason per candidate
selected backend
reported internal mode, split count, workspace, and plan key when exposed
diagnostic artifact path and SHA-256

The human-readable fields prevent a hash from becoming an opaque authority. The hash prevents silent drift. If the call changes while the digest remains old, the bundle fails. If a selected backend is absent from the observed eligible set, the bundle fails. A forced backend error is itself a valid diagnostic outcome, but not a kernel execution.

0x0BF A Profiler Trace Closes Execution, Not Performance

Level 5 requires a content-addressed device trace with exact kernel symbols and positive launch counts. NVIDIA’s Nsight Systems guide distinguishes CUDA API activity from GPU workload activity, including kernel executions and memory operations. This is the right level for questions such as:

Did a split producer launch?
Did a combine kernel launch?
How many launches occurred inside the marked call range?
Was the call replayed through a CUDA Graph?
Were unexpected copies or synchronizations present?

Use an NVTX range or an equivalently precise marker around the immutable call. Record profiler name/version, command, raw trace path and SHA-256, range name, kernel symbols, and launch counts. Do not infer the symbol from a selected backend class. Do not infer num_splits > 1 merely because a split-capable symbol family exists.

Nsight Systems establishes the timeline and executed symbols. NVIDIA Nsight Compute collects per-kernel metrics, often with replay and nontrivial overhead. A profiled metric run is therefore not automatically a latency sample. Preserve the metric set and replay mode, and run the uninstrumented timing protocol separately.

0x0BG Correctness Must Cover Output And Mutated Cache State

Level 6 begins with correctness, not timing. For a pure attention operator, compare output and optional LSE against a declared reference. For an append path, also compare the cache mutation and committed-token identities:

$$|O_{cand}-O_{ref}|\leq atol+rtol\,|O_{ref}|.$$

The bundle records the reference backend, tolerances, maximum absolute error, finite/all-masked policy, and pass/fail result. If the call appends K/V, it also records whether cache state was checked. Output agreement alone can miss a wrong append location whose effect appears only on the next decode step.

Alternative numerical policies require separate rows:

Design choice	Why it changes the contract
FP16/BF16 inputs with FP32 reduction	changes expected rounding envelope
FP8 K/V or output	changes quantization and accumulation error
deterministic reduction	may change topology or disable a faster path
shared-shift numerator	needs the finite-range guard derived in 0x09C
graph replay	freezes pointers and can change plan/reuse behavior

The tolerance is therefore a field of $K_{run}$, not a post-hoc adjustment made after observing an error.

0x0BH Raw Synchronized Samples And Counter Definitions Close Measurement

CUDA work is asynchronous. PyTorch’s torch.cuda.synchronize waits for kernels on the selected device, while CUDA events can measure elapsed device time within a stream. A timing protocol must state which mechanism it uses and what is inside the timed interval.

warm_up_same_call_key()
synchronize_device()

samples_us = []
for _ in range(N):
    start.record(stream)
    run_same_call_key()
    end.record(stream)
    end.synchronize()
    samples_us.append(1000.0 * start.elapsed_time(end))

persist_raw_samples_before_summarizing(samples_us)

The runtime evidence schema requires at least 20 positive raw samples, but that is a validation floor, not a claim that 20 samples are universally sufficient. Report count, minimum, median, p95, and maximum only after preserving the raw list. Allocation, plan construction, graph capture, cache append, and scheduler delay must be explicitly included or excluded.

Profiler counters also need semantics:

name
unit
numerator definition
denominator definition
kernel/range scope
profiler version and replay mode

“DRAM bytes” without read/write scope, launch scope, and profiler metric name cannot reconcile with the logical ledgers in 0x03–0x05. Metric collection can perturb execution, so counter runs and latency runs remain separate artifacts joined by the same $K_{run}$.

0x0BI Executable Runtime Contract And Failure Closure

The runtime evidence bundle adds:

docs/numinens-evidence/m4-5-decode-kernel-boundaries/runtime_evidence_fixture.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_runtime_evidence_fixtures.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/runtime_preflight.py
docs/numinens-evidence/m4-5-decode-kernel-boundaries/local_runtime_preflight.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/runtime_evidence_oracle.py
docs/numinens-evidence/m4-5-decode-kernel-boundaries/runtime_evidence_report.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_runtime_evidence_oracle.py

The oracle validates monotone levels, loaded-object hashes, loader/build artifacts, call-key digests, selected-set membership, trace hashes, positive launch counts, correctness, raw timing samples, synchronization, and counter definitions. Synthetic complete bundles exercise levels 2–6 only as schema tests; they are never emitted as local measurements.

Invalid fixtures close ten promotions:

Invalid promotion	Missing evidence
package version $\to$ loaded binary	loaded-object path, hash, loader map, build report
source commit $\to$ binary hash	SHA-256 of the mapped object
selected backend $\to$ observed selection	content-addressed diagnostic
kernel name $\to$ execution	profiler trace and launch count
latency summary $\to$ measurement	raw positive synchronized samples
timing $\to$ valid result	passing correctness comparison
profiler counter $\to$ traffic claim	unit, numerator, denominator, and scope
unsupported host $\to$ backend disproof	compatible CUDA coordinate

The generated report retains:

maximum local evidence level = 2
runtime evidence             = none
local kernel symbols         = []
local timing samples         = 0

That result is not empty. It is the truthful boundary between repository analysis and a future CUDA capture.

0x0C Benchmark Evidence: Source-Reported Results, Estimators, And Comparability

The paper-contract comparison kept benchmark headlines attached to their paper coordinates. The runtime evidence contract defined what a local CUDA measurement would require. A gap remains between those two contracts: a paper can report a number truthfully while still not publish enough fields to reconstruct, normalize, or compare that number with a result from another paper.

This loop owns that gap. Its owner question is:

What may this article infer from a source-reported benchmark once the source, denominator, workload, environment, metric, and aggregation rule are audited?

The answer is deliberately narrower than a leaderboard. A benchmark claim is the tuple

$$K_{bench}=H(K_{source},K_{workload},K_{environment},K_{baseline},K_{metric},K_{aggregation}),$$

where $H$ is a canonical identity over readable fields. If one field is unknown, the source-reported claim may still be quoted with that absence. The missing field does, however, block any inference that depends on it. A paper maximum with an unknown maximizing point is still a maximum reported by that paper; it is not a representative latency and not a portable speedup.

This section does not repeat the algorithm comparison in 0x09, and it does not fabricate the level-6 runtime bundle required by 0x0B. It derives the accounting rules between them.

0x0CA The Denominator Is Part Of The Result

An absolute latency is already coordinate-dependent. A relative result adds a second implementation coordinate:

$$S_L=\frac{T_{base}}{T_{candidate}}, \qquad S_\Theta=\frac{\Theta_{candidate}}{\Theta_{base}}.$$

$S_L$ is a latency speedup and $S_\Theta$ is a throughput speedup. They agree only when candidate and baseline perform the same counted work under the same steady-state protocol. Dynamic batching, request admission, generated-token count, graph capture, cache allocation, or different correctness policies can break that assumption.

The word “baseline” therefore expands into:

method and implementation owner
version or commit
supported/admitted backend path
compiler and build configuration
input and output precision
graph, workspace, allocation, and warmup policy
workload, request trace, and correctness contract

“Compared with Hugging Face” or “over FlashAttention-2” is useful provenance, but it is not a binary identity. When a source publishes only the family name, the row retains baseline_version = unknown. Replacing that absence with a modern release would silently change the denominator.

0x0CB Ratio And Reduction Units Must Be Derived, Not Renamed

For one identical workload point, latency reduction is

$$R_L=1-\frac{T_{candidate}}{T_{base}}.$$

Combining this definition with $S_L=T_{base}/T_{candidate}$ gives

$$S_L=\frac{1}{1-R_L}, \qquad R_L=1-\frac{1}{S_L}.$$

This is why a 50% latency reduction means $2\times$ speedup, while a 2x speedup means 50% reduction. A 69% reduction does not mean 1.69x:

$$\frac{1}{1-0.69}=3.226\times.$$

The FlashInfer paper reports 29–69% inter-token-latency reduction for its SGLang serving evaluation and 28–30% reduction for its optimized Streaming-LLM evaluation. Algebraically, those intervals become approximately 1.41–3.23x and 1.39–1.43x latency speedup, respectively. The transformation does not add a sample, reveal which setting produced an endpoint, or make the two experiments comparable. It only expresses the same reported ratios in a second unit. See the versioned FlashInfer v2 evaluation.

0x0CC Maximum, Mean, Range, And Ratio Of Sums Answer Different Questions

Let case $i$ have baseline latency $b_i$, candidate latency $c_i$, and per-case speedup $s_i=b_i/c_i$. At least three aggregate speedups are common:

$$\bar S_{arith}=\frac{1}{n}\sum_{i=1}^{n}s_i,$$ $$S_{sum}=\frac{\sum_i b_i}{\sum_i c_i},$$ $$\bar S_{geo}=\exp\left(\frac{1}{n}\sum_i\log s_i\right).$$

The first gives equal weight to every case’s ratio. The second weights cases by their contribution to total candidate time. The third is symmetric in multiplicative ratio space. None is universally “the average speedup.”

For two cases with baseline latencies $[10,100]$ ms and candidate latencies $[5,80]$ ms:

Estimator	Calculation	Result
arithmetic mean of per-case speedups	$(2+1.25)/2$	$1.625\times$
ratio of summed latencies	$110/85$	$1.294\times$
geometric mean of per-case speedups	$\sqrt{2\cdot1.25}$	$1.581\times$

An “average” without the sample manifest, weights, exclusions, and estimator cannot be reconstructed. An “up to” result is

$$S_{max}=\max_{i\in\mathcal{W}} s_i,$$

where the sweep $\mathcal{W}$ is part of the claim. Enlarging the sweep can increase $S_{max}$ without improving any old point. A range preserves only its endpoints unless the source also maps every endpoint to a configuration.

0x0CD Eight Source Rows Do Not Form One Leaderboard

The executable fixture transcribes eight claims from the primary sources. The values below are source-reported, not locally reproduced:

Source row	Scope and reported estimator	Coordinate retained	Why it is not cross-paper rankable
Flash-Decoding CodeLlama-34B	up to 8x generation throughput, batch 1, context 512–64k	model, batch, sweep, alternative baseline set	exact maximizing point, hardware, precision, and denominator version absent from prose
Flash-Decoding attention	up to 50x runtime speedup over pre-v2.2 FA2	A100, f16, $B=1$, $H_q=16$, $H_{kv}=2$, $d=128$, context to 64k	exact A100 SKU, baseline commit, maximizing point, and raw values absent
FlashDecoding++ vs Hugging Face	up to 4.86x decode speedup	A100/RTX3090 evaluation family and model sweep	framework baseline version, precision, and maximizing case unresolved
FlashDecoding++ vs FlashDecoding	reported 1.37x average on A100	accelerator and source evaluation section	baseline version, per-case values, weights, and average rule unresolved
LeanAttention vs FA2	reported 2.6x average over more than 500 attention cases	A100-80GB; varied batch, context, heads, and head width	baseline commit, sample manifest, precision, weights, and raw values absent
LeanAttention vs FA2	reported maximum 8.33x at 16 heads and 512k context	maximum point’s known head/context fields	batch, head dimension, baseline commit, precision, and absolute latencies absent
FlashInfer SGLang	29–69% ITL reduction across settings	FlashInfer 0.2, SGLang 0.3.4, Triton 3.0, H100 model coordinates, request-admission rule	endpoint mapping, trace manifest, absolute ITL, and raw values absent
FlashInfer Streaming-LLM	28–30% ITL reduction across recent-window settings	Vicuna-13B, MT-Bench, optimized implementation, f16 software coordinate	exact device, baseline commit, windows, endpoint mapping, and absolute ITL absent

The Flash-Decoding author note explicitly separates its end-to-end CodeLlama throughput sweep from its A100 f16 attention microbenchmark. The former reports up to 8x generation speedup; the latter reports attention up to 50x faster than FlashAttention. Combining those maxima or transferring the microbenchmark shape to the end-to-end row would alter the experiment. See the dated Flash-Decoding author note.

The LeanAttention v2 paper reports an average 2.6x attention speedup over FA2 and a maximum 8.33x at 16 heads and 512k context. Those are two estimators over the same broad study, not interchangeable descriptions of a typical point. See LeanAttention v2.

0x0CE Comparability Is An Equality Predicate Before It Is A Plot

For benchmark rows $i$ and $j$, define the strict teaching predicate

$$\mathcal{C}(i,j)= \prod_{f\in\mathcal{F}} \mathbf{1}\left[K_i^{(f)}=K_j^{(f)}\land K_i^{(f)}\neq\varnothing\right],$$

with

F = {
    scope, phase, metric quantity, direction,
    accelerator, precision, workload,
    baseline identity, statistic
}

This predicate is intentionally strict. It asks whether two rows answer the same measured question. If $\mathcal C=0$, both rows may be valid, but their ratio is not a performance conclusion. A kernel latency and an online-serving ITL differ in scope. A maximum and a mean differ in estimator. A100 and H100 results differ in machine. FlashAttention-2 and Triton differ in denominator. CodeLlama and a heterogeneous request trace differ in workload.

The eight source-reported rows produce zero admitted cross-paper pairs. This does not say the methods cannot be compared by a new experiment. It says the cited paper rows do not already supply that controlled experiment.

0x0CF Source Conflicts Must Survive Transcription

Version pinning does not guarantee that every statement inside one version is consistent. In FlashDecoding++ v4, the arXiv abstract reports an AMD headline of 2.18x, while the main-body contribution text reports 3.93x. Section 6.2 then reports 2.27x on RX7900XTX and 3.93x on MI210 against its Hugging Face baseline.

The manifest records this as an unresolved source-internal conflict:

source version: arXiv:2311.01282v4
locator A:      abstract                     -> 2.18x AMD headline
locator B:      contribution / Section 6.2   -> 3.93x headline
device rows:    RX7900XTX 2.27x; MI210 3.93x
policy:         do not average, silently substitute, or rank the conflict

Choosing the larger value because it is more impressive is invalid. Choosing the abstract because it appears first is also invalid. A publication can cite the exact Section 6.2 device rows with their locator while separately warning that the abstract conflicts. The conflict is evidence about the source, not a number to optimize away.

Figure digitization has a similar boundary. Reading an exact coordinate from pixels requires the figure version, axis transforms, pixel-to-data mapping, series identification, and uncertainty interval. The benchmark audit does not digitize plots. Fields visible only in a figure remain figure-dependent rather than being guessed from the nearest tick.

0x0CG Reported, Re-Expressed, And Reproduced Are Separate Verbs

The evidence progression is:

Evidence class	Permitted statement
source-reported	the pinned source states this value at this locator
transcription-audited	the value, unit, baseline, estimator, and known coordinate fields were checked
algebraically re-expressed	the same ratio was converted exactly into another unit
figure-digitized	pixels were converted under a declared uncertainty protocol
locally reproduced	runtime level-6 correctness and measurement bundle produced a compatible result
independently compared	candidate and baselines were rerun under one immutable benchmark manifest

The first three do not imply the last three. In particular, computing $1/(1-0.69)$ is an exact derivation from a paper’s percentage, but it does not reproduce the paper’s 69% endpoint. A local run with the same method name but a different call key is a new coordinate, not a reproduction.

0x0CH Executable Benchmark Manifest And Oracle

The benchmark evidence bundle adds:

docs/numinens-evidence/m4-5-decode-kernel-boundaries/source_reported_benchmark_fixture.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/invalid_source_reported_benchmark_fixtures.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/source_reported_benchmark_oracle.py
docs/numinens-evidence/m4-5-decode-kernel-boundaries/source_reported_benchmark_report.json
docs/numinens-evidence/m4-5-decode-kernel-boundaries/test_source_reported_benchmark_oracle.py

The fixture retains four primary-source coordinates, eight result rows, every known missing field, one source-internal conflict, and an empty local-runtime observation. The oracle validates units, baselines, claim classes, aggregation rules, range ordering, source versions, comparison keys, conflict policy, and the no-local-reproduction boundary. It also reproduces the two-case estimator example and the latency-reduction conversions.

The generated report is intentionally not a leaderboard:

source rows                      = 8
partial coordinates              = 8
cross-paper comparable pairs     = 0
source-internal conflicts        = 1
locally reproduced claims        = 0
local timing samples             = 0

0x0CI Benchmark Failure Closure

Twelve invalid fixtures fail closed:

Invalid promotion	Why it fails
floating source revision	result can drift without a new row identity
unknown source ID	value has no primary-source coordinate
relative result without baseline	denominator is missing
“up to” relabelled as average	estimator changed
latency reduction relabelled with x	unit and algebra changed
paper row marked locally reproduced	no runtime level-6 bundle exists
partial coordinate admitted to ranking	missing key fields are being ignored
aggregate without aggregation rule	published scalar cannot be reconstructed
reversed range endpoints	range is internally inconsistent
source conflict silently resolved	transcription discarded contrary evidence
local samples inserted into source-only bundle	evidence classes were conflated
null comparison field declared rankable	equality cannot be established

The closure rule is simple:

Preserve what the source reports, derive only what follows algebraically, expose every missing coordinate field, and rerun methods under one manifest before making a comparative performance claim.

0x0D Handoff To M4.6: FA3 And FA4 As Hardware Boundaries

FlashAttention-3 targets Hopper features such as asynchronous execution, warp specialization, Tensor Memory Accelerator transfers, newer matrix-multiply pipelines, and FP8 paths. The important continuity is:

as matmul gets faster,
softmax/reduction and data-movement scheduling become more visible;

as hardware exposes more asynchronous stages,
the kernel must overlap producer and consumer work explicitly.

FA3 should not be presented as a universal replacement independent of hardware. Its design is tied to Hopper capabilities, and FA4 changes the schedule again around Blackwell TMEM and 2-CTA MMA. M4.6 derives those two hardware pipelines, their on-chip capacity costs, their low-precision/numerical boundaries, and the benchmark evidence needed to distinguish them.

That comparison teaches a broader rule:

Kernel architecture follows the machine’s memory hierarchy, execution pipelines, and supported precision modes; an API-level attention equation does not determine the optimal schedule.

0x0E Failure Lab

Failure	Symptom	Root cause	Check
Average split outputs directly	wrong decode logits	local softmax outputs have different partition mass	compare exact LSE merge against unsplit reference
Omit m_c/LSE from partial state	overflow or wrong normalization	partial states cannot enter one exponential frame	assert split and unsplit numerical agreement
Run the non-empty merge on an empty split	NaN maximum frame or denominator	-inf - -inf reaches exponential arithmetic	branch on validity and test empty/all-masked rows
Launch S_capacity but allocate only S state slots	out-of-bounds writes or silent workspace corruption	launch capacity and allocation capacity were specified independently	bind producer grid, workspace envelope, and reducer range in one immutable plan
Reducer consumes an unwritten empty or inactive slot	nondeterministic output or NaN	a capacity owner exited without producing the merge identity	initialize every consumed slot or exclude it explicitly from the reducer plan
Report logical owner demand as HBM traffic	unsupported bandwidth and roofline conclusions	cache reuse, transaction granularity, and backend fusion were ignored	keep unique payload, logical demand, workspace traffic, and profiler counters separate
Use q_head as kv_head under GQA	wrong output or out-of-range access	query/KV head mapping ignored	test explicit group mapping
Use active batch index as cache row	another request’s plausible K/V is read	scheduler order and storage identity diverged	test cache_batch_idx remapping
Treat logical K/V as contiguous physical rows	invalid or unrelated cache reads	page/block table ignored	trace logical-to-physical addresses
Read the allocated final-page tail	softmax includes stale or uninitialized state	page capacity was treated as committed context	poison tail rows and predicate exact visibility
Report page-table size as DRAM traffic	unsupported memory claim	resident metadata and transactions were conflated	require profiler counters for measured traffic
Apply mask after local softmax	masked tokens affect denominator	mask missed max/sum recurrence	test fully masked and diagonal tiles
Assume SDPA means FlashAttention	unexpected latency or allocations	unsupported call fell back	inspect diagnostics and profiler
Maximize split count	slower short-context decode	reduction and partial-state overhead dominates	sweep split count by shape
Present FlashMask as arbitrary sparsity	unsupported pattern encoded incorrectly	interval representation overgeneralized	validate pattern representability
Cite a floating branch as implementation evidence	article drifts as upstream source changes	repository name was treated as an immutable coordinate	pin commit, path, hash, symbol, and span
Describe FlashInfer’s paper planner as the pinned batch-decode scheduler	wrong plan fields and launch topology	paper and branch coordinates were conflated	retain the paper/source comparison in 0x0AE
Treat a selected backend class as an executed kernel	unsupported runtime and performance claim	source-chain closure was promoted beyond its evidence level	require loaded-binary, dispatch, and profiler evidence
Treat a wheel version as loaded-object identity	irreproducible binary attribution	installed metadata and process loader state were conflated	preserve import origin, loader map, object hashes, and build report
Copy a source commit into the binary field	apparently immutable but false runtime coordinate	source identity was substituted for compiled bytes	hash every relevant loaded object with SHA-256
Infer execution from a dispatch log	wrong split/reduction narrative	selected class may launch several internal kernel paths	bind profiler symbols and launch counts to the call range
Time asynchronous launches without synchronization	implausibly small or unstable latency	host enqueue time was reported as completed device work	state event/device synchronization and persist raw samples
Tune tolerances after seeing the candidate error	correctness claim cannot be reproduced	numerical policy was not frozen before evaluation	bind reference, dtype policy, atol, and rtol in the run key
Reuse a metric profile as steady-state timing	profiler overhead contaminates latency	replay and counter collection changed execution	separate trace, metric, correctness, and uninstrumented timing artifacts
Relabel a 69% latency reduction as 1.69x	relative result is numerically wrong	percentage reduction was added to one instead of inverted	use $S=1/(1-R)$ on the identical workload point
Compare an “up to” result with an average	apparent winner depends on reporting convention	maximum and mean estimators were conflated	preserve claim class, sweep, weights, and aggregation rule
Rank kernel latency against online-serving ITL	cross-paper bar chart has no common measured scope	operator and scheduler/request metrics were conflated	require an identical strict comparison key before plotting
Replace an unknown baseline version with a current release	reconstructed result no longer belongs to the paper	missing denominator identity was silently imputed	retain unknown and mark the coordinate partial
Resolve conflicting source values by choosing one headline	citation looks precise but contrary source evidence disappears	locator-level conflict was treated as noise	preserve both locators and block normalization
Call an algebraic conversion a reproduction	derived ratio is presented as new experimental evidence	unit conversion and runtime measurement were conflated	require runtime level-6 artifacts for reproduction

0x0F What This Article Claims

1. One-token decode removes the query-row parallel axis used by FA2 prefill.
2. Splitting the K/V sequence exposes work but requires exact partial-softmax reduction.
3. The merge formula follows from moving every non-empty split into one exponential reference frame.
4. An explicit empty identity makes ragged, fully masked, and over-partitioned rows reducible without NaN arithmetic.
5. Exact closure, commutativity, associativity, and partition invariance follow because every merge recovers the canonical summary of a disjoint set union.
6. `(m,l,u)` and `(LSE,O)` are equivalent sufficient-state choices; normalized partial outputs alone are not.
7. Floating-point reduction trees target the same exact row but need not be bitwise identical.
8. Split bounds are per-request intervals; a ragged batch cannot reuse one global `T/S` partition.
9. Producer ownership `[B,H_q,S_capacity]` and reducer ownership `[B,H_q]` are different launch contracts, and neither universally implies one CUDA CTA per conceptual owner.
10. Temporary-state shape and traffic follow the selected sufficient-state ABI, its field dtypes, split capacity, and padded vector width.
11. Every split-capacity slot consumed by a reducer must contain a valid state or the explicit empty identity.
12. Unique payload, logical per-owner demand, workspace round-trip bytes, and measured DRAM transactions are different ledgers.
13. Active batch identity, cache-row identity, query-head identity, and K/V-head identity are distinct address coordinates.
14. Contiguous NHD/HND, packed ragged, dense-table paged, CSR-table paged, and contiguous-virtual caches can preserve one logical payload while requiring different address programs.
15. A Flash-Decoding split crossing page boundaries becomes a sequence of bounded physical segments; logical split count does not determine page-segment count.
16. Allocated final-page capacity is not visible K/V history, and every read must remain below the committed context length.
17. Resident metadata bytes, logical lookup demand, and measured metadata traffic are different ledgers.
18. Logical visibility, stored mask representation, tile dispatch, and physical K/V address translation are distinct contracts.
19. `SKIP`, `FULL`, and `PARTIAL` follow from the masked set's relation to one score tile; partial masking must happen before max, denominator, and numerator updates.
20. FlashMask represents at most one upper and one lower masked interval per K/V column with four endpoint vectors.
21. Eight min/max summaries per K/V column block can conservatively classify tiles without replacing the original endpoints needed by the partial path.
22. Skipping a fully masked tile is exact because it contributes the empty online-attention identity.
23. FlashMask's linear metadata claim applies only to representable interval-structured patterns; arbitrary multi-run sparsity needs another representation or fallback.
24. The paper's training and long-query inference coordinates do not prove one-token cached-decode speedup.
25. SDPA is a semantic and dispatch boundary, not proof that a specific kernel ran.
26. FA1, FA2, Flash-Decoding, FlashMask, and FA3 address different bottlenecks.
27. A reproducible dispatch key binds environment, operation, tensor, semantic, and runtime-control coordinates.
28. Backend admission is a conjunction of capability predicates; a complete rejection vector is more useful than a single eligible Boolean.
29. Registry discovery, phase/platform candidate construction, capability admission, and priority selection are distinct stages.
30. Forced backend selection fails closed under this article's contract, while automatic selection records every rejected candidate above its winner.
31. Stateful wrappers need a version-scoped plan projection; changing a frozen plan field requires replanning rather than silently reusing stale launch state.
32. Eligibility, selection, profiler-observed execution, correctness evidence, and performance measurement have strictly different claim ceilings.
33. Training, prefill, append, one-token decode, and mixed serving reuse attention algebra but own different backward, cache-mutation, and launch contracts.
34. For old committed length $T$ and new query length $C$, causal append row $i$ has absolute position $T+i$ and visible key interval `[0,T+i+1)`.
35. The visible-cell count $CT+C(C+1)/2$ follows by summing those row-prefix lengths; the $C(C-1)/2$ hidden cells are future rows inside the new chunk.
36. Prefill is the $T=0$ specialization, append has $T>0,C>1$, and one-token decode is the $T>0,C=1$ boundary where query-row parallelism collapses.
37. Persistent cache mutation is a logical transaction: validate identity, capacity, pages, positions, and masks before staging or committing rows.
38. Causal training may share the $S(S+1)/2$ visibility count while owning LSE/recompute, dropout RNG, and backward-gradient state rather than a serving cache.
39. A mixed batch requires per-request $(T_b,C_b)$ coordinates, packed query offsets, and stable cache-row identities; one global phase or query length is insufficient.
40. Visible cells, request-local rectangles, padded envelopes, tile work, measured FLOPs, and DRAM transactions are different ledgers.
41. Partitioned launches, unified per-request wrappers, prefill/decode overlap, and padded fallbacks are alternative integration strategies under the same per-request semantic contract.
42. A documented wrapper capability does not prove that a local runtime selected, executed, or benefited from one kernel.
43. M4.5 consumes a frozen microbatch manifest; request scheduling, admission, page allocation, and eviction remain M5 responsibilities.
44. The phase-integration oracle verifies phase, visibility, cache identity, packing, and logical-work invariants without claiming GPU execution or performance.
45. Decode-attention papers must be compared by phase, parallel axis, work granularity, state ABI, reduction topology, planning locus, cache contract, numerical policy, and measurement coordinate.
46. Flash-Decoding introduces fixed K/V splits per output and a second exact LSE-weighted reduction level; normalized partial outputs alone are insufficient.
47. A common finite softmax shift $\phi$ makes partition numerators and denominators directly summable in exact arithmetic because all partitions share one exponential frame.
48. FlashDecoding++'s shared-shift path still requires a per-row finite-range guard and synchronized recomputation fallback; a profiled score range is not a universal numerical proof.
49. FlashDecoding++ is an inference-engine design that also changes flat GEMM, buffering, and hardware-adaptive dataflow, so its end-to-end result cannot be assigned only to attention reduction.
50. LeanAttention replaces equal split count per output with work-centric LeanTile distribution and exact output-specific rescaling reduction; global work may cross output boundaries but softmax identity may not.
51. FlashInfer turns ragged lengths into deterministic CTA queues and partial-to-final mappings through a CPU-plan/GPU-run ABI with persistent graph-compatible execution.
52. The paper-derived FlashInfer planner and the integer teaching oracle are not source-code-equivalent implementations.
53. PagedAttention, vAttention, FlashMask, POD-Attention, and FA3/FA4 change address, mask, phase-overlap, or hardware-pipeline axes rather than replacing the decode reduction contract.
54. In the paper-contract fixture, fixed four-way per-output splitting has logical max-to-mean load $1.6$, while global and planned partitions reach $1.0$ by accepting different metadata and reduction obligations.
55. Equal logical K/V work does not prove equal runtime, occupancy, traffic, or latency.
56. Paper benchmark numbers remain attached to their model, shape, hardware, software, baseline, and metric coordinates and are not reproduced by the paper-contract oracle.
57. The paper-contract oracle validates classification and logical schedules without implementing a paper kernel or claiming local GPU evidence.
58. An implementation claim is frozen by repository commit, path, retrieved-byte hash, symbol span, branch coordinate, and call-chain layer rather than by repository name alone.
59. At the pinned FlashAttention coordinate, the cache-aware path closes from Python API through binding, split heuristic, partial workspace, dispatch, split producer, and combine kernel.
60. FlashAttention's source heuristic selects the smallest eligible split count reaching 85% of the best wave efficiency, which limits extra partial-state traffic rather than maximizing split count blindly.
61. A cache-aware call may require the split-capable kernel family while retaining one logical split; split-capable dispatch does not prove a combine launch.
62. At the pinned FlashInfer CUDA-core batch-decode coordinate, occupancy capacity and binary-search page chunking materialize request indices, K/V tile indices, output indptr, workspace offsets, and an optional merge path.
63. FlashInfer's paper-level sorted-cost persistent planner and the pinned CUDA-core paged batch-decode scheduler are different valid coordinates and must not be substituted for one another.
64. At the pinned vLLM coordinate, registry discovery, CUDA candidate order, capability rejection, backend selection, metadata construction, and the FlashAttention call surface form distinct source layers.
65. A source-selected vLLM backend class does not identify the loaded binary or prove a compiled kernel symbol executed.
66. At the pinned PyTorch coordinate, SDPA owns backend enablement, priority, admission, selection, and operator dispatch but not persistent K/V allocation or mutation.
67. The version-pinned source audit reaches source-chain evidence level 2; loaded-binary identity, runtime selection, profiler-observed execution, and synchronized performance require separate higher-level evidence.
68. The source-trace oracle closes 34 probes across four frozen repositories and fails closed on coordinate drift, broken source graphs, and claim-ceiling violations.
69. Runtime evidence is monotone: a claim at level $\ell$ requires every evidence field at levels $1$ through $\ell$ to be present and internally consistent.
70. Distribution metadata, import origin, loaded process objects, selected backend, and executed kernel are distinct identities.
71. Loaded-artifact evidence requires the imported distribution, content-addressed loader map, relevant compiled-object hashes, build configuration, GPU, driver, and CUDA runtime.
72. One runtime result is identified by a canonical join of environment, artifact, call, dispatch, and measurement coordinates rather than by a backend label.
73. A non-importing host preflight may terminate validly without initializing CUDA or promoting package discovery into loaded-object evidence.
74. The current Darwin arm64 host has no discovered target CUDA packages or NVIDIA runtime/profiler tools, so local evidence remains at source-chain level 2.
75. An unsupported local host does not disprove backend availability or behavior on a compatible CUDA coordinate.
76. Runtime selection evidence requires a readable immutable call key, matching digest, candidate/rejection diagnostic, selected backend, and content-addressed diagnostic artifact.
77. Kernel execution evidence requires a preserved profiler trace with exact symbols and positive launch counts for the marked call range.
78. Correctness for a cache-append path covers output, numerical policy, and mutated cache state rather than output alone.
79. Performance evidence preserves raw synchronized samples and separates uninstrumented timing from profiler trace and metric-replay runs.
80. The runtime evidence bundle supplies an executable schema and local preflight, but it claims no local CUDA kernel symbol, correctness result, profiler counter, or timing sample.
81. A benchmark result is identified by source, workload, environment, baseline, metric, and aggregation coordinates rather than by a method name and one scalar.
82. The denominator implementation and its version, admission path, precision, and runtime policy are part of every relative result.
83. Latency speedup and latency reduction obey $S_L=1/(1-R_L)$ only for the same workload point and counted work.
84. Algebraically re-expressing a source-reported percentage adds no timing sample and does not reproduce the source experiment.
85. Maximum, arithmetic mean of per-case ratios, ratio of summed latencies, and geometric mean are different estimators.
86. An “up to” result is a maximum over its declared sweep and is not a representative or portable speedup.
87. The eight audited primary-source benchmark rows remain partial because each lacks at least one field needed by the strict comparison key.
88. No pair among those eight rows is admitted to a cross-paper performance ranking.
89. Flash-Decoding's up-to-8x end-to-end generation result and up-to-50x attention microbenchmark are different scopes and coordinates.
90. LeanAttention's reported 2.6x average and 8.33x maximum are different estimators over its evaluation family.
91. FlashInfer's reported ITL-reduction ranges retain their serving/model/dataset coordinates when converted algebraically to speedup ranges.
92. FlashDecoding++ v4 contains conflicting AMD headline values between its abstract and main body; the benchmark audit preserves rather than resolves that conflict.
93. Plot digitization requires its own axis, transform, series, and uncertainty contract; the benchmark audit does not invent exact points from figures.
94. The benchmark evidence bundle transcribes and audits primary-source claims but reports no local reproduction, profiler trace, or timing sample.

0x0G Publish Gate

Gate	Status
Query-axis collapse is derived from tensor/grid shape	Covered in 0x01
Split softmax reduction is derived from allowed-set summaries, not only stated	Covered in 0x02A and 0x02B
Empty identity, all-masked policy, and merge laws are executable	Covered in 0x02C-0x02E and the split-state oracle
(m,l,u) and (LSE,O) ABIs are derived and tested	Covered in 0x02F and the split-state oracle
Worked values and finite-precision tree sensitivity are reproducible	Covered in 0x02G-0x02I and split_state_report.json
Ragged split ranges cover each request exactly without overlap	Covered in 0x03B and split_launch_storage_report.json
Producer, reducer, logical split, and capacity ownership are distinct	Covered in 0x03C, 0x03G, and the split-launch/storage oracle
(m,l,u) and (LSE,O) workspace shapes and bytes are derived field by field	Covered in 0x03D and 0x03E
Workspace round trip, final writes, logical demand, and measured traffic are not conflated	Covered in 0x03F and the traffic-ledger visual
Request, split, empty-capacity, and head-width tails have explicit behavior	Covered in 0x03G
Every temporary field has a declared dtype and alternative encoding boundary	Covered in 0x03H
The two-launch trace initializes every state its reducer may consume	Covered in 0x03I and test_split_launch_storage_oracle.py
Active request, cache row, query head, and K/V head have distinct tested identities	Covered in 0x04A and kv_address_translation_report.json
Contiguous NHD/HND and packed-ragged offsets are derived from declared strides or row pointers	Covered in 0x04B, 0x04C, and the address-translation oracle
Dense and CSR page tables recover the same visible logical payload	Covered in 0x04D and test_kv_address_translation_oracle.py
Logical split intervals become bounded physical page segments without overlap or gaps	Covered in 0x04E and the page-segment visual
Allocated final-page tail rows are excluded from visible history	Covered in 0x04F and the poisoned-tail tests
Explicit paging, virtual paging, gathering, and specialized layouts are compared without taking M5.3 allocator ownership	Covered in 0x04G and the M5.3 handoff
Resident metadata, logical lookups, and measured traffic are not conflated	Covered in 0x04I
The full read-side address contract is executable and reproducible	Covered in 0x04J, kv_address_translation_oracle.py, and test_loop4_contract.py
Visibility, representation, tile class, and physical address are separate contracts	Covered in 0x05A-0x05D
Mask polarity, position space, and all-masked behavior are explicit	Covered in 0x05B and the mask-program fixture
FlashMask’s four vectors and half-open column semantics are derived	Covered in 0x06A, 0x06B, and the column-contract visual
Eight block summaries and FULL/SKIP/PARTIAL predicates are derived	Covered in 0x06C, 0x06D, and the tile-classifier visual
Skipped, full, and partial paths reproduce dense-mask attention for the fixture	Covered in 0x06E, 0x06F, and mask_program_report.json
Dense payload, interval payload, summary payload, logical work, and measured traffic are not conflated	Covered in 0x06G
Non-representable multi-run patterns fail closed or use another backend	Covered in 0x06H and invalid-contract tests
Training, prefill-style inference, and one-token decode evidence are not conflated	Covered in 0x06I
Dispatch keys separate environment, operation, tensors, semantics, and runtime controls	Covered in 0x07A and dispatch_admission_fixture.json
Admission predicates produce complete backend rejection vectors	Covered in 0x07B, 0x07D, and the dispatch-admission oracle
Registry, candidate domain, eligibility, forced policy, and automatic priority are distinct	Covered in 0x07C and test_dispatch_admission_oracle.py
Plan-static and declared dynamic fields cannot drift silently between plan() and run()	Covered in 0x07F and dispatch_admission_report.json
Numerical and determinism policy remain part of the reproducibility key	Covered in 0x07G
Eligibility, selection, execution, correctness, and measurement have separate evidence ceilings	Covered in 0x07H-0x07J and the evidence-chain visual
Training, prefill, append, one-token decode, and mixed-batch state machines are separated	Covered in 0x08A and 0x08E
Bottom-right causal append visibility is derived from old length $T$ and new length $C$	Covered in 0x08B and phase_integration_report.json
Prefill, append, and decode ledgers reconcile rectangle, visible, masked, and post-commit lengths	Covered in 0x08C and the phase-integration oracle
Cache staging and commitment preserve token and cache-row identity	Covered in 0x08C, 0x08H, and invalid-contract tests
The one-token decode boundary is connected to K/V-axis splitting rather than treated as small prefill	Covered in 0x08D
Training backward/LSE/RNG state is not conflated with persistent serving cache state	Covered in 0x08E
Packed mixed batches retain per-request $(T_b,C_b)$, offsets, and cache identity	Covered in 0x08F and test_phase_integration_oracle.py
Visible, rectangular, padded, tile, and measured-work ledgers are not conflated	Covered in 0x08B, 0x08F, and the mixed-batch visual
Partitioned, unified, overlapped, and padded integration alternatives are compared by contract	Covered in 0x08G
M4.5 consumes a frozen microbatch while M5 retains scheduler and allocator ownership	Covered in 0x08H
Phase-integration evidence remains synthetic and unmeasured	Covered in 0x08I and phase_integration_report.json
Paper variants are compared across nine frozen contract axes rather than by name or headline speedup	Covered in 0x09A and paper_contract_fixture.json
Flash-Decoding’s fixed K/V split and LSE-weighted second reduction are connected to the split-state algebra	Covered in 0x09B
The shared-shift numerator/denominator derivation includes finite-range guard and fallback obligations	Covered in 0x09C and invalid-contract tests
FlashDecoding++ attention, flat-GEMM, buffering, and adaptive-dataflow changes are not conflated	Covered in 0x09C and 0x09H
LeanAttention work-centric partitioning preserves output-specific reduction identity	Covered in 0x09D and the global-work oracle trace
FlashInfer’s chunk formula, deterministic queue planning, fixed workspace, and plan/run boundary are separated	Covered in 0x09E and paper_contract_report.json
Cache layout, mask representation, phase overlap, and hardware pipelines remain orthogonal owner axes	Covered in 0x09F
Fixed-split, global-work, and planned-chunk schedules reconcile one immutable workload	Covered in 0x09G and test_paper_contract_oracle.py
Logical work balance is not reported as measured occupancy or performance	Covered in 0x09G-0x09I
Every paper measurement remains attached to its source coordinate	Covered in 0x09H
Paper-contract evidence remains synthetic, deterministic, reproducible, and unmeasured	Covered in 0x09I and paper_contract_report.json
Source claims bind commit, path, content hash, symbol span, and implementation coordinate	Covered in 0x0AA and source_trace_fixture.json
The FlashAttention cache API closes through split planning, partial workspace, producer, and combine source layers	Covered in 0x0AB and source_trace_report.json
Split-capable dispatch is not reported as an observed multi-split or combine launch	Covered in 0x0AC
FlashInfer’s pinned CUDA-core batch-decode planner is separated from the paper-level persistent planner	Covered in 0x0AD, 0x0AE, and invalid source fixtures
FlashInfer plan metadata and conditional variable-length merge are source-traced without claiming local execution	Covered in 0x0AD and source_trace_report.json
vLLM registry, admission, selection, metadata, and kernel call surface remain separate layers	Covered in 0x0AF
PyTorch SDPA policy and operator dispatch are not assigned persistent K/V cache ownership	Covered in 0x0AG and invalid source fixtures
Source presence, chain closure, loaded binary, runtime selection, execution, and measurement have separate evidence levels	Covered in 0x0AH and the evidence-ladder visual
Version-pinned source evidence stops at source-chain level 2	Covered in 0x0AH, 0x0AI, and source_trace_report.json
Installed distribution, import origin, and process-loaded compiled objects remain separate identities	Covered in 0x0BA and the loaded-artifact visual
Loaded-artifact level 3 requires object hashes, loader map, build report, and CUDA environment	Covered in 0x0BA, 0x0BD, and runtime_evidence_fixture.json
Runtime rows bind environment, artifact, call, dispatch, and measurement coordinates	Covered in 0x0BB
The local Darwin arm64 preflight stops without importing extensions or attempting CUDA execution	Covered in 0x0BC and local_runtime_preflight.json
Unsupported-host evidence is not promoted into backend disproof	Covered in 0x0BC, 0x0BI, and invalid runtime fixtures
Selection diagnostics retain a readable call key and matching canonical digest	Covered in 0x0BE and the runtime oracle
Kernel execution requires a content-addressed profiler trace, exact symbols, and positive launch counts	Covered in 0x0BF and invalid runtime fixtures
Correctness includes cache mutation where the call appends K/V	Covered in 0x0BG
Raw synchronized timing remains separate from trace and metric-replay artifacts	Covered in 0x0BH and the runtime-capture visual
Runtime evidence claims no local CUDA execution, correctness result, profiler counter, or timing sample	Covered in 0x0BC, 0x0BI, and runtime_evidence_report.json
Relative metrics retain the exact baseline as part of the benchmark coordinate	Covered in 0x0CA and source_reported_benchmark_fixture.json
Latency reduction and speedup are converted by derivation rather than relabelling	Covered in 0x0CB and source_reported_benchmark_report.json
Maximum, mean of ratios, ratio of sums, and geometric mean remain distinct estimators	Covered in 0x0CC and the metric-accounting visual
All eight source-reported rows expose their missing coordinate fields	Covered in 0x0CD and the benchmark fixture
No partial benchmark row enters a cross-paper ranking	Covered in 0x0CE and the benchmark-coordinate visual
The FlashDecoding++ v4 AMD headline conflict remains explicit	Covered in 0x0CF and the source-conflict manifest entry
Source reporting, algebraic re-expression, digitization, and local reproduction remain separate evidence classes	Covered in 0x0CG
The benchmark oracle rejects all twelve invalid promotions	Covered in 0x0CH, 0x0CI, and test_source_reported_benchmark_oracle.py
The benchmark audit claims no local reproduction, profiler trace, or timing sample	Covered in 0x0CH and source_reported_benchmark_report.json
Source-reported speedups are not used as universal claims	No universal speedup or cross-paper leaderboard claimed
Every registered formula family is present under one declared semantic, logical, source-reported, or measured coordinate	formula_contract.json and article_audit_report.json
Every local article and fragment link resolves to an existing owner	final article audit
Every responsive SVG has stable geometry, semantic alt text, title, description, and a pinned digest	visual_provenance_report.json
The official animation has direct attribution, an evidence limit, and a reduced-motion static fallback	visual provenance contract
Adjacent M4/M5/M8 owner boundaries are linked without exact long-paragraph duplication	boundary audit at a 240-character normalized threshold
No implementation-process label remains in reader-facing prose	final article audit

0x0H Final Formula, Source, Render, Accessibility, And Boundary Audit

Publication closure is a separate claim from mechanism depth. A long article can contain many equations and sources while still having an unbalanced math delimiter, a floating implementation claim, a broken local fragment, an inaccessible visual, or an ownership boundary that has drifted into a second derivation. The final audit therefore checks five contracts independently.

0x0HA Formula Contract

The formula audit classifies expressions before counting them:

exact semantic identities:
    decode attention, split summary, empty identity, exact merge, visibility

source-logical models:
    owner grids, workspace bytes, address offsets, tile classes, plan keys

source-reported accounting:
    paper comparison coordinates, relative metrics, estimator definitions

runtime measurement:
    synchronized durations, hardware counters, loaded artifacts, kernel traces

formula_contract.json registers the decode, split-state, launch/storage, address, mask, dispatch, phase, paper-variant, source/runtime, and benchmark families. The offline audit rejects unbalanced or empty display-math blocks and requires every registered expression to remain present. The publication snapshot contains 121 display-math blocks. That count is only a regression floor: formula presence does not replace the executable oracles, and a source-logical byte formula does not become measured DRAM traffic.

0x0HB Source And Evidence Contract

source_manifest.json separates local owners, versioned primary papers, official runtime documentation, immutable source traces, synthetic contract artifacts, observed unsupported-host preflight, source-reported benchmark rows, and unmeasured runtime fields. The audit verifies local source hashes, requires every primary or official source to retain a role and claim status, and keeps implementation commits in the article rather than accepting a floating repository name.

This article directly reuses one source visual: the unnumbered official Flash-Decoding animation from the PyTorch engineering note. Its source URL, digest, static-frame derivation, commentary purpose, rights boundary, and anti-claims are recorded separately from repository-authored reconstructions. It illustrates sequence partitioning; it does not prove a current launch, split heuristic, runtime path, or speedup. It is retained for attributed technical commentary, and no general reuse license is claimed.

The evidence classes remain non-interchangeable:

exact semantic identity != source-logical schedule
source-logical schedule != selected runtime path
selected runtime path    != profiler-observed execution
source-reported result   != local reproduction

0x0HC Render And Accessibility Contract

The reconstructed visual surface contains 23 responsive SVG pairs. Every desktop and mobile SVG must have fixed width, height, and viewBox, role="img", one non-empty <title>, one non-empty <desc>, and aria-labelledby="title desc". Every article image must have semantic alt text. The official animation adds a static PNG selected by prefers-reduced-motion: reduce; this fallback is an accessibility path, not a second source figure.

The complete surface is 24 semantic visuals and 48 image targets: 46 SVG targets plus the source GIF and its static fallback. Static provenance and browser behavior are separate gates. The browser acceptance matrix is:

desktop: 1440 x 1000, light and dark
mobile:   390 x  844, light and dark

required:
    MathJax completes without an article error
    the intended responsive or reduced-motion source is selected
    every image loads with positive natural dimensions
    no article-level horizontal overflow
    wide tables and code remain intentionally scrollable on mobile

0x0HD Boundary And Duplication Contract

M4.5 consumes accounting, execution, online-softmax, and FA2 work-partition contracts from M4.1-M4.4. It hands hardware-specific pipelines to M4.6, request and scheduler state to M5.1-M5.2, physical cache ownership to M5.3, model-level K/V representation to M5.7-M5.8, and quantized cache/runtime release policy to M8.6/M8.9/M8.10. The audit checks those outbound links and the established reciprocal M4.3-M4.6 and M5 handoffs.

An exact-prose comparison against A19 and adjacent M4/M5/M8 owners rejects duplicated long paragraphs at 240 normalized characters. This is a narrow mechanical guard, not proof that conceptual repetition is absent. The owner table and handoff sections remain the authoritative explanation of why an imported term is context rather than a competing derivation.

0x0HE Final Publication Closure

The reproducible closure commands are:

cd docs/numinens-evidence/m4-5-decode-kernel-boundaries
python3 audit_visual_provenance.py --output visual_provenance_report.json --fail-on-mismatch
python3 audit_article.py --output article_audit_report.json --fail-on-mismatch
python3 -m unittest discover -v

visual_coverage_contract.json, audit_visual_provenance.py, and visual_provenance_report.json close the image surface, with test_visual_provenance.py as the regression gate. formula_contract.json, audit_article.py, and article_audit_report.json close formulas, links, sources, artifacts, boundaries, and exact prose duplication, with test_article_audit.py as the release gate. These checks are joined by browser_acceptance_report.json, which records the five rendered desktop, mobile, theme, and reduced-motion states. They cannot manufacture the missing CUDA run. Local loaded-binary identity, selected kernel symbols, correctness on a compatible GPU, profiler counters, and raw synchronized timing remain explicitly unmeasured.

0xFF References

• Local source: Exploring the Transformer Series (19) - FlashAttention v2 and its upgrade
• M4.1 - Transformer Cost Model
• M4.2 - GPU Execution Model for Transformer Kernels
• M4.3 - IO-Aware Attention and FlashAttention-1
• M4.4 - FlashAttention-2 Work Partitioning and the Decode Boundary
• M4.6 - FlashAttention-3/4 Hardware Pipelines
• M5.1 - Autoregressive Serving State
• M5.2 - Continuous Batching and Scheduler Pressure
• M5.3 - KV Layout, Physical Allocation, and Exact Reuse
• M5.7 - MQA/GQA and KV-Head Sharing
• M5.8 - MLA, Latent Cache, and Absorbed Kernels
• M8.6 - Live-Data Quantization for Activations and KV Cache
• M8.9 - Quantized Artifacts and Runtime Integration
• M8.10 - Deployment Evaluation, Release, and Rollback
• Maxim Milakov and Natalia Gimelshein, Online Normalizer Calculation for Softmax
• Tri Dao, FlashAttention-2: Faster Attention with Better Parallelism and Work Partitioning
• Tri Dao et al., Flash-Decoding for long-context inference
• PyTorch, Flash-Decoding for long-context inference
• Ke Hong et al., FlashDecoding++: Faster Large Language Model Inference on GPUs
• Rya Sanovar et al., Lean Attention: Hardware-Aware Scalable Attention Mechanism for the Decode-Phase of Transformers
• Zihao Ye et al., FlashInfer: Efficient and Customizable Attention Engine for LLM Inference Serving
• FlashInfer, KV-Cache Layout Documentation
• Woosuk Kwon et al., Efficient Memory Management for Large Language Model Serving with PagedAttention
• Prabhu et al., vAttention: Dynamic Memory Management for Serving LLMs without PagedAttention
• Juechu Dong et al., Flex Attention: A Programming Model for Generating Optimized Attention Kernels
• PyTorch, FlexAttention and BlockMask API documentation
• Guoxia Wang et al., FlashMask: Efficient and Rich Mask Extension of FlashAttention
• PaddlePaddle, flashmask_attention API documentation
• Jay Shah et al., FlashAttention-3: Fast and Accurate Attention with Asynchrony and Low-precision
• Dao-AILab, FlashAttention repository and flash_attn_with_kvcache interface
• Dao-AILab, pinned flash_attn_with_kvcache interface
• Dao-AILab, pinned cache-aware binding, split heuristic, and workspace setup
• Dao-AILab, pinned split-K/V producer and combine launch template
• FlashInfer, Attention-kernel API and paged decode wrappers
• FlashInfer, pinned Python batch-decode plan/run wrapper
• FlashInfer, pinned batch-decode FFI plan/run binding
• FlashInfer, pinned occupancy-aware batch-decode scheduler
• FlashInfer, pinned direct/partitioned decode and merge launch
• FlashInfer, POD-Attention wrapper documentation
• Aditya K. Kamath et al., POD-Attention: Unlocking Full Prefill-Decode Overlap for Faster LLM Inference
• FlashInfer, single_decode_with_kv_cache API
• FlashInfer, API logging, flight recorder, and stateful replay documentation
• vLLM, Attention backend feature and admission matrix
• vLLM, pinned V1 attention selector
• vLLM, pinned attention backend registry
• vLLM, pinned CUDA backend admission and priority policy
• vLLM, pinned FlashAttention backend metadata and call surface
• vLLM, Historical PagedAttention kernel design note
• PyTorch, Scaled Dot Product Attention documentation
• PyTorch, sdpa_kernel backend-selection context manager
• PyTorch, pinned sdpa_kernel policy surface
• PyTorch, pinned CUDA SDPA capability and selection policy
• PyTorch, pinned scaled-dot-product-attention operator switch
• PyTorch, CUDA backend capability helpers
• PyTorch, Reproducibility and SDPA backend determinism
• Python, importlib.metadata distribution metadata
• PyTorch, torch.__config__.show() build configuration
• PyTorch, torch.cuda.get_device_properties
• PyTorch, torch.cuda.synchronize
• NVIDIA, Nsight Systems User Guide
• NVIDIA, Nsight Compute User Guide
• Joshua Ainslie et al., GQA: Training Generalized Multi-Query Transformer Models from Multi-Head Checkpoints