module Realization.Nvidia.SM86.AttentionHeadLayoutSM86 import Accelerator.SM86.Control import Accelerator.SM86.Immediate import Accelerator.SM86.Instruction import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.Program import Accelerator.SM86.Types import Data.SHA256Digest import Std.Natural -- coppelius S5 rung 4b (D24): the ATTENTION HEAD LAYOUT kernels at coppelius's -- geometry — sequence 1024, 8 heads of 64 (half width 32), model width 512, -- so the fused QKV projection is a 1024 × 1536 fp32 row-major matrix whose -- row is [Q heads 0..7 | K heads 0..7 | V heads 0..7], each head 64 wide. -- -- The tensor-core GEMM (Realization.Nvidia.SM86.GEMM.HMMA.*) computes C = A · Bᵀ -- with A (M × K) and B (N × K) both fp16 row-major. So per head h: -- scores_h = Q_h · K_hᵀ A = Q_h (1024 × 64), B = K_h (1024 × 64) -- out_h = P_h · V_h A = P_h (1024 × 1024), B = V_hᵀ (64 × 1024) -- and the layout kernels here produce exactly those operands: -- QK ROTARY: for every position p, head h and component c < 32 the HF -- half-split rotation (Llama): q'[c] = q[c]·cos − q[c+32]·sin, -- q'[c+32] = q[c+32]·cos + q[c]·sin, with cos/sin tables of 1024 × 32 fp32 -- (angle p · theta^(−2c/64)); the same for K; both written fp16 head-major -- [head][position][64]. Grid 1024 (one block per position), block 128: -- thread = head (tid >> 4) × component pair (tid & 15 → c = 2g, 2g+1), four -- fp32 loads per plane, two packed half2 stores per plane. -- VALUE TRANSPOSE: V written fp16 as [head][component][position]. Grid 512 -- (one block per PAIR of positions, so a thread packs two adjacent -- positions into one half2 store), block 512: thread = head (tid >> 6) × -- component (tid & 63). -- Constant bank 0 (64-bit pointers): 0x160 first output (Q or V), 0x168 second -- output (K; unused by the value kernel), 0x170 QKV input, 0x178 cosine table, -- 0x180 sine table. -- No host fallback: the image is emitted by the sovereign encoder or the -- build refuses with a stable code. family AttentionHeadLayoutSM86Kind : Type 0 constructor AttentionHeadLayoutQKRotary constructor AttentionHeadLayoutValueTranspose constructor AttentionHeadLayoutHeadToToken constructor AttentionHeadLayoutTokenToHead constructor AttentionHeadLayoutInverseRoPEQKVMerge end-family family AttentionHeadLayoutSM86FailureCode : Type 0 constructor AttentionHeadLayoutInstructionCountMismatch constructor AttentionHeadLayoutEncodingFailed constructor AttentionHeadLayoutIdentityInvalid end-family family AttentionHeadLayoutSM86Extents : Type 0 constructor AttentionHeadLayoutSM86ExtentsValue field unrestricted attentionHeadLayoutExtentSequence : Nat field unrestricted attentionHeadLayoutExtentHeads : Nat field unrestricted attentionHeadLayoutExtentHeadWidth : Nat field unrestricted attentionHeadLayoutExtentHalfWidth : Nat field unrestricted attentionHeadLayoutExtentModelWidth : Nat field unrestricted attentionHeadLayoutExtentQKVWidth : Nat end-family family AttentionHeadLayoutSM86Telemetry : Type 0 constructor AttentionHeadLayoutSM86TelemetryValue field unrestricted attentionHeadLayoutTelemetryKind : (family AttentionHeadLayoutSM86Kind) field unrestricted attentionHeadLayoutTelemetryExpectedInstructions : Nat field unrestricted attentionHeadLayoutTelemetryActualInstructions : Nat field unrestricted attentionHeadLayoutTelemetryRegisters : Nat field unrestricted attentionHeadLayoutTelemetryGridX : Nat field unrestricted attentionHeadLayoutTelemetryBlockX : Nat field unrestricted attentionHeadLayoutTelemetryExtents : (family AttentionHeadLayoutSM86Extents) field unrestricted attentionHeadLayoutTelemetryEncodedBytes : Nat field unrestricted attentionHeadLayoutTelemetryEncodedFields : Nat field unrestricted attentionHeadLayoutTelemetryEncodedBits : Nat end-family family AttentionHeadLayoutSM86ImageResult : Type 0 constructor AttentionHeadLayoutSM86ImageReady field unrestricted attentionHeadLayoutImageKind : (family AttentionHeadLayoutSM86Kind) field unrestricted attentionHeadLayoutImageBytes : Bytes field unrestricted attentionHeadLayoutImageSHA256 : Bytes field unrestricted attentionHeadLayoutImageTelemetry : (family AttentionHeadLayoutSM86Telemetry) constructor AttentionHeadLayoutSM86ImageFailed field unrestricted attentionHeadLayoutImageFailure : (family AttentionHeadLayoutSM86FailureCode) field unrestricted attentionHeadLayoutImageFailureInstruction : Nat field unrestricted attentionHeadLayoutImageFailureDetail : Bytes field unrestricted attentionHeadLayoutImageFailureTelemetry : (family AttentionHeadLayoutSM86Telemetry) end-family -- naturals def attentionHeadLayoutSM86N8 = (byte-to-nat (byte 8)) def attentionHeadLayoutSM86N23 = (byte-to-nat (byte 23)) def attentionHeadLayoutSM86N24 = (byte-to-nat (byte 24)) def attentionHeadLayoutSM86N31 = (byte-to-nat (byte 31)) def attentionHeadLayoutSM86N32 = (byte-to-nat (byte 32)) def attentionHeadLayoutSM86N48 = (byte-to-nat (byte 48)) def attentionHeadLayoutSM86N56 = (byte-to-nat (byte 56)) def attentionHeadLayoutSM86N63 = (byte-to-nat (byte 63)) def attentionHeadLayoutSM86N64 = (byte-to-nat (byte 64)) def attentionHeadLayoutSM86N72 = (byte-to-nat (byte 72)) def attentionHeadLayoutSM86N73 = (byte-to-nat (byte 73)) def attentionHeadLayoutSM86N77 = (byte-to-nat (byte 77)) def attentionHeadLayoutSM86N128 = (byte-to-nat (byte 128)) def attentionHeadLayoutSM86N256 = (nat-multiply (byte-to-nat (byte 16)) (byte-to-nat (byte 16))) def attentionHeadLayoutSM86N512 = (nat-multiply attentionHeadLayoutSM86N256 (byte-to-nat (byte 2))) def attentionHeadLayoutSM86N1024 = (nat-multiply attentionHeadLayoutSM86N256 (byte-to-nat (byte 4))) def attentionHeadLayoutSM86N1536 = (nat-multiply attentionHeadLayoutSM86N256 (byte-to-nat (byte 6))) def attentionHeadLayoutSM86Extents : (family AttentionHeadLayoutSM86Extents) = (constructor AttentionHeadLayoutSM86Extents AttentionHeadLayoutSM86ExtentsValue attentionHeadLayoutSM86N1024 attentionHeadLayoutSM86N8 attentionHeadLayoutSM86N64 attentionHeadLayoutSM86N32 attentionHeadLayoutSM86N512 attentionHeadLayoutSM86N1536) -- immediates def attentionHeadLayoutSM86U = (lambda unrestricted b0 : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (lambda unrestricted b3 : Byte . (sm86Unsigned32 b0 b1 b2 b3))))) def attentionHeadLayoutSM86U0 = (attentionHeadLayoutSM86U (byte 0) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U1 = (attentionHeadLayoutSM86U (byte 1) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U2 = (attentionHeadLayoutSM86U (byte 2) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U4 = (attentionHeadLayoutSM86U (byte 4) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U15 = (attentionHeadLayoutSM86U (byte 15) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U31 = (attentionHeadLayoutSM86U (byte 31) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U32 = (attentionHeadLayoutSM86U (byte 32) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U63 = (attentionHeadLayoutSM86U (byte 63) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U64 = (attentionHeadLayoutSM86U (byte 64) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U128 = (attentionHeadLayoutSM86U (byte 128) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U132 = (attentionHeadLayoutSM86U (byte 132) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86U512 = (attentionHeadLayoutSM86U (byte 0) (byte 2) (byte 0) (byte 0)) def attentionHeadLayoutSM86U1024 = (attentionHeadLayoutSM86U (byte 0) (byte 4) (byte 0) (byte 0)) def attentionHeadLayoutSM86U1088 = (attentionHeadLayoutSM86U (byte 64) (byte 4) (byte 0) (byte 0)) def attentionHeadLayoutSM86U1536 = (attentionHeadLayoutSM86U (byte 0) (byte 6) (byte 0) (byte 0)) def attentionHeadLayoutSM86U2048 = (attentionHeadLayoutSM86U (byte 0) (byte 8) (byte 0) (byte 0)) def attentionHeadLayoutSM86U2052 = (attentionHeadLayoutSM86U (byte 4) (byte 8) (byte 0) (byte 0)) def attentionHeadLayoutSM86U2112 = (attentionHeadLayoutSM86U (byte 64) (byte 8) (byte 0) (byte 0)) def attentionHeadLayoutSM86U2176 = (attentionHeadLayoutSM86U (byte 128) (byte 8) (byte 0) (byte 0)) def attentionHeadLayoutSM86U2180 = (attentionHeadLayoutSM86U (byte 132) (byte 8) (byte 0) (byte 0)) def attentionHeadLayoutSM86U3072 = (attentionHeadLayoutSM86U (byte 0) (byte 12) (byte 0) (byte 0)) def attentionHeadLayoutSM86U4096 = (attentionHeadLayoutSM86U (byte 0) (byte 16) (byte 0) (byte 0)) def attentionHeadLayoutSM86U6144 = (attentionHeadLayoutSM86U (byte 0) (byte 24) (byte 0) (byte 0)) def attentionHeadLayoutSM86U65536 = (attentionHeadLayoutSM86U (byte 0) (byte 0) (byte 1) (byte 0)) def attentionHeadLayoutSM86U131072 = (attentionHeadLayoutSM86U (byte 0) (byte 0) (byte 2) (byte 0)) def attentionHeadLayoutSM86U135168 = (attentionHeadLayoutSM86U (byte 0) (byte 16) (byte 2) (byte 0)) -- constant bank 0 offsets def attentionHeadLayoutSM86ConstantBase = (attentionHeadLayoutSM86U (byte 40) (byte 0) (byte 0) (byte 0)) def attentionHeadLayoutSM86FirstOutputPointer = (attentionHeadLayoutSM86U (byte 96) (byte 1) (byte 0) (byte 0)) -- Ordered launch arguments shared by the specialised Q, K and V layouts. -- V reads through the input pointer but has no table operands. def attentionHeadLayoutSM86FirstOutputArgument : Nat = 0 def attentionHeadLayoutSM86SecondOutputArgument : Nat = 1 def attentionHeadLayoutSM86InputArgument : Nat = 2 def attentionHeadLayoutSM86CosineArgument : Nat = 3 def attentionHeadLayoutSM86SineArgument : Nat = 4 def attentionHeadLayoutSM86SecondOutputPointer = (attentionHeadLayoutSM86U (byte 104) (byte 1) (byte 0) (byte 0)) def attentionHeadLayoutSM86InputPointer = (attentionHeadLayoutSM86U (byte 112) (byte 1) (byte 0) (byte 0)) def attentionHeadLayoutSM86CosinePointer = (attentionHeadLayoutSM86U (byte 120) (byte 1) (byte 0) (byte 0)) def attentionHeadLayoutSM86SinePointer = (attentionHeadLayoutSM86U (byte 128) (byte 1) (byte 0) (byte 0)) def attentionHeadLayoutSM86ValueGradientPointer = (attentionHeadLayoutSM86U (byte 136) (byte 1) (byte 0) (byte 0)) -- registers and program plumbing def attentionHeadLayoutSM86R = (lambda unrestricted value : Byte . (sm86Register value)) def attentionHeadLayoutSM86Next = (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext (constructor SM86Instruction SM86InstructionValue (constructor SM86InstructionGuard SM86InstructionAlways) body) tail))) def attentionHeadLayoutSM86End = (constructor SM86Program SM86ProgramEnd) def attentionHeadLayoutSM86SetSpecials = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0)) def attentionHeadLayoutSM86SetLoads = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1)) -- wait on barrier 0 (the special-register reads): mask bit 0 def attentionHeadLayoutSM86WaitSpecials : (family SM86Control) = (constructor SM86Control SM86ControlValue (byte 7) (constructor SM86YieldMode SM86Continue) (constructor SM86Barrier SM86BarrierNone) (constructor SM86Barrier SM86BarrierNone) (byte 1) (byte 0)) -- wait on barrier 1 (every global load): mask bit 1 def attentionHeadLayoutSM86WaitLoads : (family SM86Control) = (constructor SM86Control SM86ControlValue (byte 7) (constructor SM86YieldMode SM86Continue) (constructor SM86Barrier SM86BarrierNone) (constructor SM86Barrier SM86BarrierNone) (byte 2) (byte 0)) def attentionHeadLayoutSM86Move = (lambda unrestricted destination : Byte . (lambda unrestricted value : (family SM86Unsigned32) . (constructor SM86InstructionBody SM86MoveImmediate (attentionHeadLayoutSM86R destination) value sm86SafeControl))) def attentionHeadLayoutSM86IMAD = (lambda unrestricted destination : Byte . (lambda unrestricted left : Byte . (lambda unrestricted value : (family SM86Unsigned32) . (lambda unrestricted addend : Byte . (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate (attentionHeadLayoutSM86R destination) (attentionHeadLayoutSM86R left) value (attentionHeadLayoutSM86R addend) sm86SafeControl))))) def attentionHeadLayoutSM86Wide = (lambda unrestricted destination : Byte . (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (lambda unrestricted pointer : (family SM86Unsigned32) . (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant (attentionHeadLayoutSM86R destination) (attentionHeadLayoutSM86R left) (attentionHeadLayoutSM86R right) (byte 0) pointer sm86SafeControl))))) def attentionHeadLayoutSM86Load = (lambda unrestricted destination : Byte . (lambda unrestricted address : Byte . (lambda unrestricted offset : (family SM86Unsigned32) . (constructor SM86InstructionBody SM86LoadGlobal (attentionHeadLayoutSM86R destination) (attentionHeadLayoutSM86R address) offset attentionHeadLayoutSM86SetLoads)))) def attentionHeadLayoutSM86Store = (lambda unrestricted address : Byte . (lambda unrestricted value : Byte . (lambda unrestricted offset : (family SM86Unsigned32) . (constructor SM86InstructionBody SM86StoreGlobal (attentionHeadLayoutSM86R address) (attentionHeadLayoutSM86R value) offset sm86SafeControl)))) def attentionHeadLayoutSM86Multiply = (lambda unrestricted destination : Byte . (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (lambda unrestricted control : (family SM86Control) . (constructor SM86InstructionBody SM86FloatMultiply (attentionHeadLayoutSM86R destination) (attentionHeadLayoutSM86R left) (attentionHeadLayoutSM86R right) control))))) def attentionHeadLayoutSM86Negate = (lambda unrestricted register : Byte . (constructor SM86InstructionBody SM86FloatNegate (attentionHeadLayoutSM86R register) (attentionHeadLayoutSM86R register) sm86SafeControl)) def attentionHeadLayoutSM86NegateWithControl = (lambda unrestricted register : Byte . (lambda unrestricted control : (family SM86Control) . (constructor SM86InstructionBody SM86FloatNegate (attentionHeadLayoutSM86R register) (attentionHeadLayoutSM86R register) control))) def attentionHeadLayoutSM86FMA = (lambda unrestricted destination : Byte . (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd (attentionHeadLayoutSM86R destination) (attentionHeadLayoutSM86R left) (attentionHeadLayoutSM86R right) (attentionHeadLayoutSM86R destination) sm86SafeControl)))) def attentionHeadLayoutSM86Pack = (lambda unrestricted destination : Byte . (lambda unrestricted high : Byte . (lambda unrestricted low : Byte . (lambda unrestricted control : (family SM86Control) . (constructor SM86InstructionBody SM86FloatPairToPackedHalfPair (attentionHeadLayoutSM86R destination) (attentionHeadLayoutSM86R high) (attentionHeadLayoutSM86R low) control))))) -- the rotation of one component: x1 (first half), x2 (second half), cos, sin → -- out1 = x1·cos − x2·sin ; out2 = x2·cos + x1·sin. `first` waits on the loads. def attentionHeadLayoutSM86Rotate = (lambda unrestricted out1 : Byte . (lambda unrestricted out2 : Byte . (lambda unrestricted x1 : Byte . (lambda unrestricted x2 : Byte . (lambda unrestricted cosine : Byte . (lambda unrestricted sine : Byte . (lambda unrestricted first : (family SM86Control) . (lambda unrestricted tail : (family SM86Program) . (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Multiply out1 x2 sine first) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Negate out1) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86FMA out1 x1 cosine) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Multiply out2 x1 sine sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86FMA out2 x2 cosine) tail))))))))))))) -- shared prologue: R1 ← c[0x28]; R0 = tid; R1 = block; R4 = 4; R7 = 0; R9 = 2; -- R5 = mask; R2 = tid >> shift; R3 = tid & mask def attentionHeadLayoutSM86Prologue = (lambda unrestricted shift : Byte . (lambda unrestricted mask : (family SM86Unsigned32) . (lambda unrestricted tail : (family SM86Program) . (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86MoveConstant (attentionHeadLayoutSM86R (byte 1)) (byte 0) attentionHeadLayoutSM86ConstantBase sm86SafeControl) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86SpecialToRegister (attentionHeadLayoutSM86R (byte 0)) (constructor SM86SpecialRegister SM86ThreadIdX) attentionHeadLayoutSM86SetSpecials) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86SpecialToRegister (attentionHeadLayoutSM86R (byte 1)) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) attentionHeadLayoutSM86SetSpecials) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 4) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 7) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 5) mask) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 9) attentionHeadLayoutSM86U2) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86ShiftRightImmediate (attentionHeadLayoutSM86R (byte 2)) (attentionHeadLayoutSM86R (byte 0)) shift attentionHeadLayoutSM86WaitSpecials) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable (attentionHeadLayoutSM86R (byte 3)) (attentionHeadLayoutSM86R (byte 0)) (attentionHeadLayoutSM86R (byte 5)) (byte 192) sm86SafeControl) tail)))))))))))) -- QK rotary: 63 instructions def attentionHeadLayoutSM86QKRotaryProgram : (family SM86Program) = (attentionHeadLayoutSM86Prologue (byte 4) attentionHeadLayoutSM86U15 (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 6) (byte 3) attentionHeadLayoutSM86U2 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 1) attentionHeadLayoutSM86U1536 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 6) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) (byte 8) (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 14) (byte 10) attentionHeadLayoutSM86U128) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 15) (byte 10) attentionHeadLayoutSM86U132) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 16) (byte 10) attentionHeadLayoutSM86U2048) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 17) (byte 10) attentionHeadLayoutSM86U2052) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 18) (byte 10) attentionHeadLayoutSM86U2176) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 19) (byte 10) attentionHeadLayoutSM86U2180) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 20) (byte 1) attentionHeadLayoutSM86U32 (byte 6)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 22) (byte 20) (byte 4) attentionHeadLayoutSM86CosinePointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 24) (byte 22) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 25) (byte 22) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 26) (byte 20) (byte 4) attentionHeadLayoutSM86SinePointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 28) (byte 26) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 29) (byte 26) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Rotate (byte 30) (byte 31) (byte 12) (byte 14) (byte 24) (byte 28) attentionHeadLayoutSM86WaitLoads (attentionHeadLayoutSM86Rotate (byte 32) (byte 33) (byte 13) (byte 15) (byte 25) (byte 29) sm86SafeControl (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 34) (byte 32) (byte 30) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 35) (byte 33) (byte 31) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 36) (byte 2) attentionHeadLayoutSM86U65536 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 36) (byte 1) attentionHeadLayoutSM86U64 (byte 36)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 36) (byte 6) attentionHeadLayoutSM86U1 (byte 36)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 38) (byte 36) (byte 9) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 34) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 35) attentionHeadLayoutSM86U64) (attentionHeadLayoutSM86Rotate (byte 40) (byte 41) (byte 16) (byte 18) (byte 24) (byte 28) sm86SafeControl (attentionHeadLayoutSM86Rotate (byte 42) (byte 43) (byte 17) (byte 19) (byte 25) (byte 29) sm86SafeControl (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 44) (byte 42) (byte 40) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 45) (byte 43) (byte 41) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 46) (byte 36) (byte 9) attentionHeadLayoutSM86SecondOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 44) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 45) attentionHeadLayoutSM86U64) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))))))))))))))))))))))))))))))))))) -- value transpose: 23 instructions def attentionHeadLayoutSM86ValueTransposeProgram : (family SM86Program) = (attentionHeadLayoutSM86Prologue (byte 6) attentionHeadLayoutSM86U63 (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 1) attentionHeadLayoutSM86U3072 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 3) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate (attentionHeadLayoutSM86R (byte 8)) (attentionHeadLayoutSM86R (byte 8)) attentionHeadLayoutSM86U1024 sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) (byte 8) (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) attentionHeadLayoutSM86U6144) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 2) attentionHeadLayoutSM86U64 (byte 3)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 16) attentionHeadLayoutSM86U1024 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 1) attentionHeadLayoutSM86U2 (byte 16)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 18) (byte 16) (byte 9) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 14) (byte 13) (byte 12) attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 18) (byte 14) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))))))))))) -- Join the eight fp32 head-major context matrices [head][position][64] into -- one fp16 token-major matrix [position][512]. A 256-thread block owns one -- position; each thread converts one adjacent component pair. def attentionHeadLayoutSM86HeadToTokenProgram : (family SM86Program) = (attentionHeadLayoutSM86Prologue (byte 5) attentionHeadLayoutSM86U31 (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 6) (byte 3) attentionHeadLayoutSM86U2 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U65536 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 1) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 6) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) (byte 8) (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 1) attentionHeadLayoutSM86U512 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 2) attentionHeadLayoutSM86U64 (byte 16)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 6) attentionHeadLayoutSM86U1 (byte 16)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 18) (byte 16) (byte 9) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 14) (byte 13) (byte 12) attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 18) (byte 14) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))))))))))) -- Reverse the preceding layout for the attention-output adjoint: fp32 -- token-major [position][512] to fp16 head-major [head][position][64]. def attentionHeadLayoutSM86TokenToHeadProgram : (family SM86Program) = (attentionHeadLayoutSM86Prologue (byte 5) attentionHeadLayoutSM86U31 (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 6) (byte 3) attentionHeadLayoutSM86U2 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 1) attentionHeadLayoutSM86U512 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 6) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) (byte 8) (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 2) attentionHeadLayoutSM86U65536 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 1) attentionHeadLayoutSM86U64 (byte 16)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 6) attentionHeadLayoutSM86U1 (byte 16)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 18) (byte 16) (byte 9) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 14) (byte 13) (byte 12) attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 18) (byte 14) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))))))))))) -- The attention adjoint produces dQ and dK as fp32 -- [head][position][component], and dV transposed as fp32 -- [head][component][position]. Apply the inverse rotary transform to Q/K, -- merge all three planes into the projection's token-major QKV order, and -- pack the result to fp16 for the QKV input/weight GEMMs. Pointer ABI: -- 0x160 output QKV, 0x168 dQ, 0x170 dK, 0x178 cos, 0x180 sin, 0x188 dV^T. def attentionHeadLayoutSM86InverseRoPEQKVMergeProgram : (family SM86Program) = (attentionHeadLayoutSM86Prologue (byte 4) attentionHeadLayoutSM86U15 (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 6) (byte 3) attentionHeadLayoutSM86U2 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U65536 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 1) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 6) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) (byte 8) (byte 4) attentionHeadLayoutSM86SecondOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 14) (byte 10) attentionHeadLayoutSM86U128) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 15) (byte 10) attentionHeadLayoutSM86U132) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 16) (byte 8) (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 18) (byte 16) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 19) (byte 16) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 20) (byte 16) attentionHeadLayoutSM86U128) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 21) (byte 16) attentionHeadLayoutSM86U132) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 22) (byte 1) attentionHeadLayoutSM86U32 (byte 6)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 24) (byte 22) (byte 4) attentionHeadLayoutSM86CosinePointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 26) (byte 24) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 27) (byte 24) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 28) (byte 22) (byte 4) attentionHeadLayoutSM86SinePointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 30) (byte 28) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 31) (byte 28) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86NegateWithControl (byte 30) attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Negate (byte 31)) (attentionHeadLayoutSM86Rotate (byte 32) (byte 33) (byte 12) (byte 14) (byte 26) (byte 30) attentionHeadLayoutSM86WaitLoads (attentionHeadLayoutSM86Rotate (byte 34) (byte 35) (byte 13) (byte 15) (byte 27) (byte 31) sm86SafeControl (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 36) (byte 34) (byte 32) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 37) (byte 35) (byte 33) sm86SafeControl) (attentionHeadLayoutSM86Rotate (byte 38) (byte 39) (byte 18) (byte 20) (byte 26) (byte 30) sm86SafeControl (attentionHeadLayoutSM86Rotate (byte 40) (byte 41) (byte 19) (byte 21) (byte 27) (byte 31) sm86SafeControl (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 42) (byte 40) (byte 38) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 43) (byte 41) (byte 39) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 44) (byte 1) attentionHeadLayoutSM86U1536 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 44) (byte 2) attentionHeadLayoutSM86U64 (byte 44)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 44) (byte 6) attentionHeadLayoutSM86U1 (byte 44)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 46) (byte 44) (byte 9) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 36) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 37) attentionHeadLayoutSM86U64) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 42) attentionHeadLayoutSM86U1024) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 43) attentionHeadLayoutSM86U1088) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 48) (byte 2) attentionHeadLayoutSM86U65536 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 48) (byte 3) attentionHeadLayoutSM86U2048 (byte 48)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 48) (byte 1) attentionHeadLayoutSM86U1 (byte 48)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 50) (byte 48) (byte 4) attentionHeadLayoutSM86ValueGradientPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 52) (byte 50) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 53) (byte 50) attentionHeadLayoutSM86U4096) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 55) (byte 50) attentionHeadLayoutSM86U131072) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 56) (byte 50) attentionHeadLayoutSM86U135168) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 54) (byte 53) (byte 52) attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 58) (byte 56) (byte 55) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 54) attentionHeadLayoutSM86U2048) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 46) (byte 58) attentionHeadLayoutSM86U2112) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))))))))))))))))))))))))))))))))))))))))))))))))) def attentionHeadLayoutSM86Program = (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) . (eliminate AttentionHeadLayoutSM86Kind (lambda unrestricted current : (family AttentionHeadLayoutSM86Kind) . (family SM86Program)) kind (branch AttentionHeadLayoutQKRotary . attentionHeadLayoutSM86QKRotaryProgram) (branch AttentionHeadLayoutValueTranspose . attentionHeadLayoutSM86ValueTransposeProgram) (branch AttentionHeadLayoutHeadToToken . attentionHeadLayoutSM86HeadToTokenProgram) (branch AttentionHeadLayoutTokenToHead . attentionHeadLayoutSM86TokenToHeadProgram) (branch AttentionHeadLayoutInverseRoPEQKVMerge . attentionHeadLayoutSM86InverseRoPEQKVMergeProgram))) def attentionHeadLayoutSM86ExpectedInstructions = (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) . (eliminate AttentionHeadLayoutSM86Kind (lambda unrestricted current : (family AttentionHeadLayoutSM86Kind) . Nat) kind (branch AttentionHeadLayoutQKRotary . attentionHeadLayoutSM86N63) (branch AttentionHeadLayoutValueTranspose . attentionHeadLayoutSM86N23) (branch AttentionHeadLayoutHeadToToken . attentionHeadLayoutSM86N23) (branch AttentionHeadLayoutTokenToHead . attentionHeadLayoutSM86N23) (branch AttentionHeadLayoutInverseRoPEQKVMerge . attentionHeadLayoutSM86N77))) def attentionHeadLayoutSM86Registers = (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) . (eliminate AttentionHeadLayoutSM86Kind (lambda unrestricted current : (family AttentionHeadLayoutSM86Kind) . Nat) kind (branch AttentionHeadLayoutQKRotary . attentionHeadLayoutSM86N48) (branch AttentionHeadLayoutValueTranspose . attentionHeadLayoutSM86N24) (branch AttentionHeadLayoutHeadToToken . attentionHeadLayoutSM86N24) (branch AttentionHeadLayoutTokenToHead . attentionHeadLayoutSM86N24) (branch AttentionHeadLayoutInverseRoPEQKVMerge . attentionHeadLayoutSM86N64))) def attentionHeadLayoutSM86GridX = (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) . (eliminate AttentionHeadLayoutSM86Kind (lambda unrestricted current : (family AttentionHeadLayoutSM86Kind) . Nat) kind (branch AttentionHeadLayoutQKRotary . attentionHeadLayoutSM86N1024) (branch AttentionHeadLayoutValueTranspose . attentionHeadLayoutSM86N512) (branch AttentionHeadLayoutHeadToToken . attentionHeadLayoutSM86N1024) (branch AttentionHeadLayoutTokenToHead . attentionHeadLayoutSM86N1024) (branch AttentionHeadLayoutInverseRoPEQKVMerge . attentionHeadLayoutSM86N1024))) def attentionHeadLayoutSM86BlockX = (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) . (eliminate AttentionHeadLayoutSM86Kind (lambda unrestricted current : (family AttentionHeadLayoutSM86Kind) . Nat) kind (branch AttentionHeadLayoutQKRotary . attentionHeadLayoutSM86N128) (branch AttentionHeadLayoutValueTranspose . attentionHeadLayoutSM86N512) (branch AttentionHeadLayoutHeadToToken . attentionHeadLayoutSM86N256) (branch AttentionHeadLayoutTokenToHead . attentionHeadLayoutSM86N256) (branch AttentionHeadLayoutInverseRoPEQKVMerge . attentionHeadLayoutSM86N128))) def attentionHeadLayoutSM86FailureCodeBytes = (lambda unrestricted code : (family AttentionHeadLayoutSM86FailureCode) . (eliminate AttentionHeadLayoutSM86FailureCode (lambda unrestricted current : (family AttentionHeadLayoutSM86FailureCode) . Bytes) code (branch AttentionHeadLayoutInstructionCountMismatch . b"ALPHA-SM86-ATTN-LAYOUT-001") (branch AttentionHeadLayoutEncodingFailed . b"ALPHA-SM86-ATTN-LAYOUT-002") (branch AttentionHeadLayoutIdentityInvalid . b"ALPHA-SM86-ATTN-LAYOUT-003"))) def attentionHeadLayoutSM86TelemetryFor = (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) . (lambda unrestricted actual : Nat . (lambda unrestricted bytes : Nat . (lambda unrestricted fields : Nat . (lambda unrestricted bits : Nat . (constructor AttentionHeadLayoutSM86Telemetry AttentionHeadLayoutSM86TelemetryValue kind (attentionHeadLayoutSM86ExpectedInstructions kind) actual (attentionHeadLayoutSM86Registers kind) (attentionHeadLayoutSM86GridX kind) (attentionHeadLayoutSM86BlockX kind) attentionHeadLayoutSM86Extents bytes fields bits)))))) def attentionHeadLayoutSM86Image = (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) . (app (lambda unrestricted program : (family SM86Program) . (app (lambda unrestricted actual : Nat . (nat-eliminate (lambda unrestricted countValid : Nat . (family AttentionHeadLayoutSM86ImageResult)) (constructor AttentionHeadLayoutSM86ImageResult AttentionHeadLayoutSM86ImageFailed (constructor AttentionHeadLayoutSM86FailureCode AttentionHeadLayoutInstructionCountMismatch) actual (attentionHeadLayoutSM86FailureCodeBytes (constructor AttentionHeadLayoutSM86FailureCode AttentionHeadLayoutInstructionCountMismatch)) (attentionHeadLayoutSM86TelemetryFor kind actual zero zero zero)) (lambda unrestricted countPredecessor : Nat . (lambda unrestricted countInduction : (family AttentionHeadLayoutSM86ImageResult) . (eliminate SM86ProgramEncodingResult (lambda unrestricted current : (family SM86ProgramEncodingResult) . (family AttentionHeadLayoutSM86ImageResult)) (sm86EncodeProgram program) (branch SM86ProgramEncodingSucceeded image encodingTelemetry . (eliminate SM86ProgramEncodingTelemetry (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) . (family AttentionHeadLayoutSM86ImageResult)) encodingTelemetry (branch SM86ProgramEncodingTelemetryValue instructions bytes fields bits highest . (app (lambda unrestricted identity : Bytes . (nat-eliminate (lambda unrestricted valid : Nat . (family AttentionHeadLayoutSM86ImageResult)) (constructor AttentionHeadLayoutSM86ImageResult AttentionHeadLayoutSM86ImageFailed (constructor AttentionHeadLayoutSM86FailureCode AttentionHeadLayoutIdentityInvalid) zero (attentionHeadLayoutSM86FailureCodeBytes (constructor AttentionHeadLayoutSM86FailureCode AttentionHeadLayoutIdentityInvalid)) (attentionHeadLayoutSM86TelemetryFor kind instructions bytes fields bits)) (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : (family AttentionHeadLayoutSM86ImageResult) . (constructor AttentionHeadLayoutSM86ImageResult AttentionHeadLayoutSM86ImageReady kind image identity (attentionHeadLayoutSM86TelemetryFor kind instructions bytes fields bits)))) (naturalEqual (bytes-length identity) attentionHeadLayoutSM86N64))) (sha256HexBytesOrEmpty (sha256Hex image)))))) (branch SM86ProgramEncodingFailed index failure encodingTelemetry . (constructor AttentionHeadLayoutSM86ImageResult AttentionHeadLayoutSM86ImageFailed (constructor AttentionHeadLayoutSM86FailureCode AttentionHeadLayoutEncodingFailed) index (sm86InstructionEncodingStableCode failure) (attentionHeadLayoutSM86TelemetryFor kind actual zero zero zero)))))) (naturalEqual actual (attentionHeadLayoutSM86ExpectedInstructions kind)))) (sm86ProgramCount program))) (attentionHeadLayoutSM86Program kind))) -- One half-split rotation plane from a token-major f32 projection to a -- head-major packed-f16 attention operand. Grid (sequence/16, heads, 1), -- block 256: each group of 16 threads owns one position, with each thread -- owning adjacent components in both 32-wide halves. Query -- and key use the same program with different projection offsets, so K can -- have fewer heads without materializing repeated K. def attentionHeadLayoutSM86RotatePlaneAdmitted = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (naturalAnd (naturalNonzero seq) (naturalAnd (naturalEqual (naturalModuloUnchecked seq 16) 0) (naturalAnd (naturalNonzero heads) (naturalAnd (naturalLessOrEqual (naturalAdd planeOffset (naturalMultiply heads 64)) projectionWidth) (naturalAnd (naturalLessOrEqual (naturalMultiply seq (naturalMultiply projectionWidth 4)) 4294967295) (naturalLessOrEqual (naturalMultiply heads (naturalMultiply seq 128)) 4294967295)))))))))) def attentionHeadLayoutSM86RotatePlaneWord = (lambda unrestricted value : Nat . (sm86Unsigned32FromNaturalTruncated value)) def attentionHeadLayoutSM86RotatePlaneSpecial = (lambda unrestricted destination : Byte . (lambda unrestricted source : (family SM86SpecialRegister) . (lambda unrestricted tail : (family SM86Program) . (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86SpecialToRegister (attentionHeadLayoutSM86R destination) source attentionHeadLayoutSM86SetSpecials) tail)))) -- R8 is the projection element, R20 the table element, R36 the output -- element. They are derived from the shape and the CTA coordinates. def attentionHeadLayoutSM86RotatePlaneEntry = (lambda unrestricted seq : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (lambda unrestricted tail : (family SM86Program) . (attentionHeadLayoutSM86RotatePlaneSpecial (byte 0) (constructor SM86SpecialRegister SM86ThreadIdX) (attentionHeadLayoutSM86RotatePlaneSpecial (byte 1) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) (attentionHeadLayoutSM86RotatePlaneSpecial (byte 2) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 4) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 7) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 9) attentionHeadLayoutSM86U2) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 15) attentionHeadLayoutSM86U15) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86MoveImmediate (attentionHeadLayoutSM86R (byte 5)) attentionHeadLayoutSM86U0 attentionHeadLayoutSM86WaitSpecials) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86ShiftRightImmediate (attentionHeadLayoutSM86R (byte 6)) (attentionHeadLayoutSM86R (byte 0)) (byte 4) sm86SafeControl) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable (attentionHeadLayoutSM86R (byte 3)) (attentionHeadLayoutSM86R (byte 0)) (attentionHeadLayoutSM86R (byte 15)) (byte 192) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 1) (byte 1) (attentionHeadLayoutSM86RotatePlaneWord 16) (byte 6)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 3) (byte 3) attentionHeadLayoutSM86U2 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 6) (attentionHeadLayoutSM86RotatePlaneWord planeOffset)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 1) (attentionHeadLayoutSM86RotatePlaneWord projectionWidth) (byte 6)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 3) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 20) (byte 1) attentionHeadLayoutSM86U32 (byte 3)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 36) (byte 1) attentionHeadLayoutSM86U64 (byte 3)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 36) (byte 2) (attentionHeadLayoutSM86RotatePlaneWord (naturalMultiply seq 64)) (byte 36)) tail))))))))))))))))))))))) def attentionHeadLayoutSM86RotatePlaneRead = (lambda unrestricted inputIndex : Byte . (lambda unrestricted tail : (family SM86Program) . (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) inputIndex (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 14) (byte 10) attentionHeadLayoutSM86U128) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 15) (byte 10) attentionHeadLayoutSM86U132) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 22) (byte 20) (byte 4) attentionHeadLayoutSM86CosinePointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 24) (byte 22) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 25) (byte 22) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 26) (byte 20) (byte 4) attentionHeadLayoutSM86SinePointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 28) (byte 26) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 29) (byte 26) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 5) attentionHeadLayoutSM86U0) tail)))))))))))))) def attentionHeadLayoutSM86RotatePlaneWrite = (lambda unrestricted tail : (family SM86Program) . (attentionHeadLayoutSM86Rotate (byte 30) (byte 31) (byte 12) (byte 14) (byte 24) (byte 28) attentionHeadLayoutSM86WaitLoads (attentionHeadLayoutSM86Rotate (byte 32) (byte 33) (byte 13) (byte 15) (byte 25) (byte 29) sm86SafeControl (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 34) (byte 32) (byte 30) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 35) (byte 33) (byte 31) sm86SafeControl) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 38) (byte 36) (byte 9) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 34) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 35) attentionHeadLayoutSM86U64) tail)))))))) def attentionHeadLayoutSM86RotatePlaneUnchecked = (lambda unrestricted seq : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (attentionHeadLayoutSM86RotatePlaneEntry seq projectionWidth planeOffset (attentionHeadLayoutSM86RotatePlaneRead (byte 8) (attentionHeadLayoutSM86RotatePlaneWrite (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))) def attentionHeadLayoutSM86RotatePlane = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (lambda erased admitted : (equal Nat (attentionHeadLayoutSM86RotatePlaneAdmitted seq heads projectionWidth planeOffset) 1) . (attentionHeadLayoutSM86RotatePlaneUnchecked seq projectionWidth planeOffset)))))) def attentionHeadLayoutSM86RotatePlaneRegisters : Nat = 48 def attentionHeadLayoutSM86RotatePlaneThreads : Nat = 256 def attentionHeadLayoutSM86RotatePlaneConstantBytes : Nat = 0x188 def attentionHeadLayoutSM86RotatePlaneBlocks = (lambda unrestricted seq : Nat . (naturalDivideUnchecked seq 16)) -- The pullback uses the transpose of the forward rotation: negating sine -- lets the same checked two-component rotation express it. Its source is a -- head-major f32 gradient plane; the destination is the matching slice of -- the token-major projection gradient. Q and K writes are disjoint. def attentionHeadLayoutSM86InverseRotatePlaneAdmitted = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (naturalAnd (attentionHeadLayoutSM86RotatePlaneAdmitted seq heads projectionWidth planeOffset) (naturalLessOrEqual (naturalMultiply heads (naturalMultiply seq 256)) 4294967295)))))) def attentionHeadLayoutSM86InverseRotatePlaneWrite = (lambda unrestricted tail : (family SM86Program) . (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86NegateWithControl (byte 28) attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Negate (byte 29)) (attentionHeadLayoutSM86Rotate (byte 30) (byte 31) (byte 12) (byte 14) (byte 24) (byte 28) sm86SafeControl (attentionHeadLayoutSM86Rotate (byte 32) (byte 33) (byte 13) (byte 15) (byte 25) (byte 29) sm86SafeControl (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 38) (byte 8) (byte 4) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 30) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 32) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 31) attentionHeadLayoutSM86U128) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 38) (byte 33) attentionHeadLayoutSM86U132) tail)))))))))) def attentionHeadLayoutSM86InverseRotatePlaneUnchecked = (lambda unrestricted seq : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (attentionHeadLayoutSM86RotatePlaneEntry seq projectionWidth planeOffset (attentionHeadLayoutSM86RotatePlaneRead (byte 36) (attentionHeadLayoutSM86InverseRotatePlaneWrite (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))) def attentionHeadLayoutSM86InverseRotatePlane = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (lambda erased admitted : (equal Nat (attentionHeadLayoutSM86InverseRotatePlaneAdmitted seq heads projectionWidth planeOffset) 1) . (attentionHeadLayoutSM86InverseRotatePlaneUnchecked seq projectionWidth planeOffset)))))) def attentionHeadLayoutSM86InverseRotatePlaneRegisters : Nat = 48 def attentionHeadLayoutSM86InverseRotatePlaneThreads : Nat = 256 def attentionHeadLayoutSM86InverseRotatePlaneConstantBytes : Nat = 0x188 -- Transpose one token-major f32 value plane to head-major [head][component] -- [position] packed BF16/f16. Grid (sequence/2, heads, 1), block 64. Each -- thread packs two adjacent positions of one component into a 32-bit store. def attentionHeadLayoutSM86TransposeValueAdmitted = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (naturalAnd (naturalNonzero seq) (naturalAnd (naturalEqual (naturalModuloUnchecked seq 2) 0) (naturalAnd (naturalNonzero heads) (naturalAnd (naturalLessOrEqual (naturalAdd planeOffset (naturalMultiply heads 64)) projectionWidth) (naturalAnd (naturalLessOrEqual (naturalMultiply seq (naturalMultiply projectionWidth 4)) 4294967295) (naturalLessOrEqual (naturalMultiply heads (naturalMultiply seq 128)) 4294967295)))))))))) def attentionHeadLayoutSM86TransposeValueUnchecked = (lambda unrestricted seq : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (attentionHeadLayoutSM86RotatePlaneSpecial (byte 0) (constructor SM86SpecialRegister SM86ThreadIdX) (attentionHeadLayoutSM86RotatePlaneSpecial (byte 1) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) (attentionHeadLayoutSM86RotatePlaneSpecial (byte 2) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 4) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 7) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 9) attentionHeadLayoutSM86U2) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86MoveImmediate (attentionHeadLayoutSM86R (byte 5)) attentionHeadLayoutSM86U0 attentionHeadLayoutSM86WaitSpecials) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 6) (attentionHeadLayoutSM86RotatePlaneWord planeOffset)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 3) (byte 1) attentionHeadLayoutSM86U2 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 3) (attentionHeadLayoutSM86RotatePlaneWord projectionWidth) (byte 6)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 0) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) (byte 8) (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) (attentionHeadLayoutSM86RotatePlaneWord (naturalMultiply projectionWidth 4))) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 5) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Pack (byte 14) (byte 13) (byte 12) attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 0) (attentionHeadLayoutSM86RotatePlaneWord seq) (byte 3)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 2) (attentionHeadLayoutSM86RotatePlaneWord (naturalMultiply seq 64)) (byte 16)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 18) (byte 16) (byte 9) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 18) (byte 14) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))))))))))))))))))))) def attentionHeadLayoutSM86TransposeValue = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (lambda erased admitted : (equal Nat (attentionHeadLayoutSM86TransposeValueAdmitted seq heads projectionWidth planeOffset) 1) . (attentionHeadLayoutSM86TransposeValueUnchecked seq projectionWidth planeOffset)))))) def attentionHeadLayoutSM86TransposeValueRegisters : Nat = 24 def attentionHeadLayoutSM86TransposeValueThreads : Nat = 64 def attentionHeadLayoutSM86TransposeValueConstantBytes : Nat = 0x178 def attentionHeadLayoutSM86TransposeValueBlocks = (lambda unrestricted seq : Nat . (naturalDivideUnchecked seq 2)) -- Pull back the transposed V operand into its token-major projection slice. -- The incoming dV^T is f32 [head][component][position]; no rotation applies -- to V. The two positions owned by one thread have disjoint output words. def attentionHeadLayoutSM86InverseTransposeValueAdmitted = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (naturalAnd (attentionHeadLayoutSM86TransposeValueAdmitted seq heads projectionWidth planeOffset) (naturalLessOrEqual (naturalMultiply heads (naturalMultiply seq 256)) 4294967295)))))) def attentionHeadLayoutSM86InverseTransposeValueUnchecked = (lambda unrestricted seq : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (attentionHeadLayoutSM86RotatePlaneSpecial (byte 0) (constructor SM86SpecialRegister SM86ThreadIdX) (attentionHeadLayoutSM86RotatePlaneSpecial (byte 1) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) (attentionHeadLayoutSM86RotatePlaneSpecial (byte 2) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 4) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 7) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86MoveImmediate (attentionHeadLayoutSM86R (byte 5)) attentionHeadLayoutSM86U0 attentionHeadLayoutSM86WaitSpecials) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 6) (attentionHeadLayoutSM86RotatePlaneWord planeOffset)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 3) (byte 1) attentionHeadLayoutSM86U2 (byte 7)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 0) (attentionHeadLayoutSM86RotatePlaneWord seq) (byte 3)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 16) (byte 2) (attentionHeadLayoutSM86RotatePlaneWord (naturalMultiply seq 64)) (byte 16)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 10) (byte 16) (byte 4) attentionHeadLayoutSM86InputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 12) (byte 10) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Load (byte 13) (byte 10) attentionHeadLayoutSM86U4) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Move (byte 5) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86MoveImmediate (attentionHeadLayoutSM86R (byte 5)) attentionHeadLayoutSM86U0 attentionHeadLayoutSM86WaitLoads) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 3) (attentionHeadLayoutSM86RotatePlaneWord projectionWidth) (byte 6)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 2) attentionHeadLayoutSM86U64 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86IMAD (byte 8) (byte 0) attentionHeadLayoutSM86U1 (byte 8)) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Wide (byte 18) (byte 8) (byte 4) attentionHeadLayoutSM86FirstOutputPointer) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 18) (byte 12) attentionHeadLayoutSM86U0) (attentionHeadLayoutSM86Next (attentionHeadLayoutSM86Store (byte 18) (byte 13) (attentionHeadLayoutSM86RotatePlaneWord (naturalMultiply projectionWidth 4))) (attentionHeadLayoutSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) attentionHeadLayoutSM86End))))))))))))))))))))))))) def attentionHeadLayoutSM86InverseTransposeValue = (lambda unrestricted seq : Nat . (lambda unrestricted heads : Nat . (lambda unrestricted projectionWidth : Nat . (lambda unrestricted planeOffset : Nat . (lambda erased admitted : (equal Nat (attentionHeadLayoutSM86InverseTransposeValueAdmitted seq heads projectionWidth planeOffset) 1) . (attentionHeadLayoutSM86InverseTransposeValueUnchecked seq projectionWidth planeOffset)))))) def attentionHeadLayoutSM86InverseTransposeValueRegisters : Nat = 24 def attentionHeadLayoutSM86InverseTransposeValueThreads : Nat = 64 def attentionHeadLayoutSM86InverseTransposeValueConstantBytes : Nat = 0x178