Realization.Nvidia.SM86.StreamingAttentionSM86

Independent grid axes select the K/V head and within-group query head; the constant selects only the contiguous key-tile range. This composition keeps the mathematical body identical to the serial per-head schedule. The raw body overwrites a global-load address before its late read has retired (checked scoreboard ordinal 38 at 4096/9/3). Higher concurrency cannot rely on the serial launch's observed latency hiding. Reuse the target-owned read-barrier guard; full-kernel ordering is checked beside the indexing KATs. Physical correctness and its performance cost remain separate gates; this is not an established cause of the prior failures. Wide grids need separate physical qualification: the earlier unsplit grid did not retire on the 3090, and no occupancy/speed claim follows here.

3101def streamingAttentionKeyGroupedByGridAndTileSM86 =
3102  (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat .
3103    (lambda unrestricted keyValueHeads : Nat .
3104      (lambda erased admitted : (equal Nat (streamingAttentionGroupedSM86Admitted seq heads keyValueHeads) 1) .
3105        (sm86GuardLateReads
3106          (streamingAttentionKeyGroupedWithHeadSourceUncheckedSM86 seq heads keyValueHeads 0 1))))))