dQ stored as the projection gradient's inverse-rotated bfloat16 Q slice
(sqRotatedEpilogue): a power-of-two sequence, the query heads within the
projection's width, its byte offsets within 32 bits
2217def streamingAttentionQueryFromScoresRotatedAdmitted =
2218 (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat .
2219 (lambda unrestricted keyValueHeads : Nat . (lambda unrestricted width : Nat .
2220 (naturalAnd (streamingAttentionGroupedSM86Admitted seq heads keyValueHeads)
2221 (naturalAnd (naturalEqual (naturalPowerOfTwo (sqrLog2 seq)) seq)
2222 (naturalAnd (naturalLessOrEqual (naturalMultiply heads saHeadWidth) width)
2223 (naturalLess (naturalMultiply seq (naturalMultiply width saHalfBytes)) (naturalPowerOfTwo 32)))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.