1module Realization.Nvidia.SM86.Transpose.FP16SM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.Program
8import Accelerator.SM86.Types
9import Compiler.AST
10import Compiler.ApplicationBuilder
11import Data.SHA256Digest
12import Std.Natural
13
14family GroupedTransposeGeometry : Type 0
15constructor GroupedTransposeGeometryValue
16field unrestricted groupedTransposeGroups : Nat
17field unrestricted groupedTransposeRows : Nat
18field unrestricted groupedTransposeColumns : Nat
19
20end-family
21
22family GroupedTransposeGrid : Type 0
23constructor GroupedTransposeGridValue
24field unrestricted groupedTransposeGridX : Nat
25field unrestricted groupedTransposeGridY : Nat
26field unrestricted groupedTransposeGridZ : Nat
27
28end-family
29
30family GroupedTransposeABI : Type 0
31constructor GroupedTransposeABIValue
32field unrestricted groupedTransposeABIConstantBank : Byte
33field unrestricted groupedTransposeABIOutputPointerOffset : Nat
34field unrestricted groupedTransposeABIInputPointerOffset : Nat
35field unrestricted groupedTransposeABIPointerAlignment : Nat
36field unrestricted groupedTransposeABIElementBytes : Nat
37field unrestricted groupedTransposeABIPackedWordBytes : Nat
38field unrestricted groupedTransposeABIBlockX : Nat
39field unrestricted groupedTransposeABITileRows : Nat
40field unrestricted groupedTransposeABITileColumns : Nat
41
42end-family
43
44family GroupedTransposeResourcePolicy : Type 0
45constructor GroupedTransposeResourcePolicyValue
46field unrestricted groupedTransposeResourceRegisters : Nat
47field unrestricted groupedTransposeResourceSharedBytes : Nat
48field unrestricted groupedTransposeResourceGlobalLoads : Nat
49field unrestricted groupedTransposeResourceGlobalStores : Nat
50field unrestricted groupedTransposeResourceHostFallbackCalls : Nat
51field unrestricted groupedTransposeResourceHostStagingTransfers : Nat
52field unrestricted groupedTransposeResourceHostCallbacks : Nat
53field unrestricted groupedTransposeResourceApplicationBuilderNativeOnly : Nat
54
55end-family
56
57family GroupedTransposeDifferentialReceipt : Type 0
58constructor GroupedTransposeDifferentialReceiptValue
59field unrestricted groupedTransposeDifferentialReferenceBytes : Nat
60field unrestricted groupedTransposeDifferentialCandidateBytes : Nat
61field unrestricted groupedTransposeDifferentialReferenceIdentity : Bytes
62field unrestricted groupedTransposeDifferentialCandidateIdentity : Bytes
63field unrestricted groupedTransposeDifferentialEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
64field unrestricted groupedTransposeDifferentialIdentityTelemetry : (family SHA256DigestTelemetry)
65field unrestricted groupedTransposeDifferentialRuns : Nat
66
67end-family
68
69family GroupedTransposeFailureCode : Type 0
70constructor GroupedTransposeNoError
71constructor GroupedTransposeGroupsZero
72constructor GroupedTransposeGroupsOutOfRange
73constructor GroupedTransposeDimensionZero
74constructor GroupedTransposeDimensionNotTileMultiple
75constructor GroupedTransposeSourceOffsetOverflow
76constructor GroupedTransposeTensorExtentOverflow
77constructor GroupedTransposeInstructionCountMismatch
78constructor GroupedTransposeEncodingFailed
79constructor GroupedTransposeEncodedByteCountMismatch
80constructor GroupedTransposeIdentityFailed
81constructor GroupedTransposeIdentityLengthInvalid
82constructor GroupedTransposeApplicationBuilderRejected
83constructor GroupedTransposeHostFallbackObserved
84constructor GroupedTransposeHostStagingObserved
85constructor GroupedTransposeHostCallbackObserved
86constructor GroupedTransposeDifferentialEncodingFailed
87constructor GroupedTransposeDifferentialEncodedByteCountMismatch
88constructor GroupedTransposeDifferentialImageMismatch
89constructor GroupedTransposeDifferentialIdentityFailed
90constructor GroupedTransposeDifferentialIdentityMismatch
91
92end-family
93
94family GroupedTransposeTelemetry : Type 0
95constructor GroupedTransposeTelemetryValue
96field unrestricted groupedTransposeTelemetryGroups : Nat
97field unrestricted groupedTransposeTelemetryRows : Nat
98field unrestricted groupedTransposeTelemetryColumns : Nat
99field unrestricted groupedTransposeTelemetryGridX : Nat
100field unrestricted groupedTransposeTelemetryGridY : Nat
101field unrestricted groupedTransposeTelemetryGridZ : Nat
102field unrestricted groupedTransposeTelemetryInstructions : Nat
103field unrestricted groupedTransposeTelemetryEncodedBytes : Nat
104field unrestricted groupedTransposeTelemetryGlobalLoads : Nat
105field unrestricted groupedTransposeTelemetryGlobalStores : Nat
106field unrestricted groupedTransposeTelemetryRegisters : Nat
107field unrestricted groupedTransposeTelemetrySharedBytes : Nat
108field unrestricted groupedTransposeTelemetryHostFallbackCalls : Nat
109field unrestricted groupedTransposeTelemetryHostStagingTransfers : Nat
110field unrestricted groupedTransposeTelemetryHostCallbacks : Nat
111field unrestricted groupedTransposeTelemetryApplicationBuilderNativeOnly : Nat
112field unrestricted groupedTransposeTelemetryABI : (family GroupedTransposeABI)
113field unrestricted groupedTransposeTelemetryResourcePolicy : (family GroupedTransposeResourcePolicy)
114field unrestricted groupedTransposeTelemetryDifferentialRuns : Nat
115field unrestricted groupedTransposeTelemetryCompositionWitness : (family Term)
116
117end-family
118
119family GroupedTransposeValidationResult : Type 0
120constructor GroupedTransposeGeometryValidated
121field unrestricted groupedTransposeValidatedGrid : (family GroupedTransposeGrid)
122constructor GroupedTransposeGeometryRejected
123field unrestricted groupedTransposeGeometryFailure : (family GroupedTransposeFailureCode)
124
125end-family
126
127family GroupedTransposeBuildResult : Type 0
128constructor GroupedTransposeBuildSucceeded
129field unrestricted groupedTransposeEncodedBytes : Bytes
130field unrestricted groupedTransposeImageIdentity : Bytes
131field unrestricted groupedTransposeBuildABI : (family GroupedTransposeABI)
132field unrestricted groupedTransposeBuildResourcePolicy : (family GroupedTransposeResourcePolicy)
133field unrestricted groupedTransposeBuildDifferentialReceipt : (family GroupedTransposeDifferentialReceipt)
134field unrestricted groupedTransposeEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
135field unrestricted groupedTransposeIdentityTelemetry : (family SHA256DigestTelemetry)
136field unrestricted groupedTransposeBuildTelemetry : (family GroupedTransposeTelemetry)
137constructor GroupedTransposeContractFailed
138field unrestricted groupedTransposeContractFailure : (family GroupedTransposeFailureCode)
139field unrestricted groupedTransposeContractTelemetry : (family GroupedTransposeTelemetry)
140constructor GroupedTransposeImageEncodingFailed
141field unrestricted groupedTransposeEncodingFailure : (family GroupedTransposeFailureCode)
142field unrestricted groupedTransposeFailedEncoding : (family SM86ProgramEncodingResult)
143field unrestricted groupedTransposeEncodingFailureTelemetry : (family GroupedTransposeTelemetry)
144constructor GroupedTransposeImageIdentityFailed
145field unrestricted groupedTransposeIdentityFailure : (family GroupedTransposeFailureCode)
146field unrestricted groupedTransposeFailedIdentity : (family SHA256HexResult)
147field unrestricted groupedTransposeIdentityFailureTelemetry : (family GroupedTransposeTelemetry)
148
149end-family
150
151def groupedTransposeOne : Nat =
152 (succ zero)
153
154def groupedTransposeN2 : Nat =
155 (byte-to-nat (byte 2))
156
157def groupedTransposeN4 : Nat =
158 (byte-to-nat (byte 4))
159
160def groupedTransposeN10 : Nat =
161 (byte-to-nat (byte 10))
162
163def groupedTransposeN16 : Nat =
164 (byte-to-nat (byte 16))
165
166def groupedTransposeN22 : Nat =
167 (byte-to-nat (byte 22))
168
169def groupedTransposeN32 : Nat =
170 (byte-to-nat (byte 32))
171
172def groupedTransposeN62 : Nat =
173 (byte-to-nat (byte 62))
174
175def groupedTransposeN64 : Nat =
176 (byte-to-nat (byte 64))
177
178def groupedTransposeN160 : Nat =
179 (byte-to-nat (byte 160))
180
181def groupedTransposeN256 : Nat =
182 (succ (byte-to-nat (byte 255)))
183
184def groupedTransposeInstructionCount : Nat =
185 (byte-to-nat (byte 183))
186
187def groupedTransposeRegisterCount : Nat =
188 groupedTransposeN32
189
190def groupedTransposeSharedBytes : Nat =
191 zero
192
193def groupedTransposeEncodedByteCount : Nat =
194 (naturalMultiply groupedTransposeInstructionCount groupedTransposeN16)
195
196def groupedTransposeBase256 : Nat =
197 (succ (byte-to-nat (byte 255)))
198
199def groupedTransposeMaximumGroups : Nat =
200 (naturalPredecessor (naturalPowerOfTwo groupedTransposeN16))
201
202def groupedTransposeMaximumOffset24 : Nat =
203 (naturalPredecessor (naturalPowerOfTwo (byte-to-nat (byte 24))))
204
205def groupedTransposeMaximumWord32 : Nat =
206 (naturalPredecessor (naturalPowerOfTwo groupedTransposeN32))
207
208def groupedTransposeHostFallbackCalls : Nat =
209 zero
210
211def groupedTransposeHostStagingTransfers : Nat =
212 zero
213
214def groupedTransposeHostCallbacks : Nat =
215 zero
216
217def groupedTransposeDifferentialRuns : Nat =
218 groupedTransposeN2
219
220def groupedTransposePointerAlignment : Nat =
221 groupedTransposeN4
222
223def groupedTransposeElementBytes : Nat =
224 groupedTransposeN2
225
226def groupedTransposePackedWordBytes : Nat =
227 groupedTransposeN4
228
229-- CB0 contains the destination pointer before the source pointer. Keep the
230-- launch ABI with the realization so consumers do not restate slot numbers.
231def groupedTransposeOutputArgument : Nat = 0
232def groupedTransposeInputArgument : Nat = 1
233def groupedTransposeArgumentCount : Nat = groupedTransposeN2
234
235def groupedTransposeOutputPointerOffset : Nat =
236 (naturalAdd (byte-to-nat (byte 96)) groupedTransposeN256)
237
238def groupedTransposeInputPointerOffset : Nat =
239 (naturalAdd (byte-to-nat (byte 104)) groupedTransposeN256)
240
241def groupedTransposeApplicationWitness : (family Term) =
242 (Compiler.ApplicationBuilder/app2
243 (constructor
244 Term
245 Variable
246 b"grouped-transpose")
247 (constructor Term NaturalLiteral groupedTransposeN32)
248 (constructor Term NaturalLiteral groupedTransposeInstructionCount))
249
250def groupedTransposeABI : (family GroupedTransposeABI) =
251 (constructor
252 GroupedTransposeABI
253 GroupedTransposeABIValue
254 (byte 0)
255 groupedTransposeOutputPointerOffset
256 groupedTransposeInputPointerOffset
257 groupedTransposePointerAlignment
258 groupedTransposeElementBytes
259 groupedTransposePackedWordBytes
260 groupedTransposeN32
261 groupedTransposeN32
262 groupedTransposeN32)
263
264def groupedTransposeResourcePolicy : (family GroupedTransposeResourcePolicy) =
265 (constructor
266 GroupedTransposeResourcePolicy
267 GroupedTransposeResourcePolicyValue
268 groupedTransposeRegisterCount
269 groupedTransposeSharedBytes
270 groupedTransposeN32
271 groupedTransposeN32
272 groupedTransposeHostFallbackCalls
273 groupedTransposeHostStagingTransfers
274 groupedTransposeHostCallbacks
275 applicationBuilderNativeOnly)
276
277def groupedTransposeFailureStableCode :
278 (pi unrestricted code : (family GroupedTransposeFailureCode) . Bytes) =
279 (lambda unrestricted code : (family GroupedTransposeFailureCode) .
280 (eliminate
281 GroupedTransposeFailureCode
282 (lambda unrestricted current : (family GroupedTransposeFailureCode) . Bytes)
283 code
284 (branch GroupedTransposeNoError . b"ALPHA-TR-000")
285 (branch GroupedTransposeGroupsZero . b"ALPHA-TR-001")
286 (branch GroupedTransposeGroupsOutOfRange . b"ALPHA-TR-002")
287 (branch GroupedTransposeDimensionZero . b"ALPHA-TR-003")
288 (branch
289 GroupedTransposeDimensionNotTileMultiple
290 .
291 b"ALPHA-TR-004")
292 (branch GroupedTransposeSourceOffsetOverflow . b"ALPHA-TR-005")
293 (branch GroupedTransposeTensorExtentOverflow . b"ALPHA-TR-006")
294 (branch
295 GroupedTransposeInstructionCountMismatch
296 .
297 b"ALPHA-TR-007")
298 (branch GroupedTransposeEncodingFailed . b"ALPHA-TR-008")
299 (branch
300 GroupedTransposeEncodedByteCountMismatch
301 .
302 b"ALPHA-TR-009")
303 (branch GroupedTransposeIdentityFailed . b"ALPHA-TR-010")
304 (branch GroupedTransposeIdentityLengthInvalid . b"ALPHA-TR-011")
305 (branch
306 GroupedTransposeApplicationBuilderRejected
307 .
308 b"ALPHA-TR-012")
309 (branch GroupedTransposeHostFallbackObserved . b"ALPHA-TR-013")
310 (branch GroupedTransposeHostStagingObserved . b"ALPHA-TR-014")
311 (branch GroupedTransposeHostCallbackObserved . b"ALPHA-TR-015")
312 (branch
313 GroupedTransposeDifferentialEncodingFailed
314 .
315 b"ALPHA-TR-016")
316 (branch
317 GroupedTransposeDifferentialEncodedByteCountMismatch
318 .
319 b"ALPHA-TR-017")
320 (branch
321 GroupedTransposeDifferentialImageMismatch
322 .
323 b"ALPHA-TR-018")
324 (branch
325 GroupedTransposeDifferentialIdentityFailed
326 .
327 b"ALPHA-TR-019")
328 (branch
329 GroupedTransposeDifferentialIdentityMismatch
330 .
331 b"ALPHA-TR-020")))
332
333def groupedTransposeNaturalByte =
334 (lambda unrestricted value : Nat .
335 (nat-to-byte (naturalModuloUnchecked value groupedTransposeBase256)))
336
337def groupedTransposeNaturalQuotient256 =
338 (lambda unrestricted value : Nat . (naturalDivideUnchecked value groupedTransposeBase256))
339
340def groupedTransposeUnsigned32FromNatural =
341 (lambda unrestricted value : Nat .
342 (Accelerator.SM86.Immediate/sm86Unsigned32
343 (groupedTransposeNaturalByte value)
344 (groupedTransposeNaturalByte (groupedTransposeNaturalQuotient256 value))
345 (groupedTransposeNaturalByte
346 (groupedTransposeNaturalQuotient256 (groupedTransposeNaturalQuotient256 value)))
347 (groupedTransposeNaturalByte
348 (groupedTransposeNaturalQuotient256
349 (groupedTransposeNaturalQuotient256 (groupedTransposeNaturalQuotient256 value))))))
350
351def groupedTransposeU0 =
352 (groupedTransposeUnsigned32FromNatural zero)
353
354def groupedTransposeU4 =
355 (groupedTransposeUnsigned32FromNatural groupedTransposeN4)
356
357def groupedTransposeU16 =
358 (groupedTransposeUnsigned32FromNatural groupedTransposeN16)
359
360def groupedTransposeU65535 =
361 (groupedTransposeUnsigned32FromNatural groupedTransposeMaximumGroups)
362
363def groupedTransposeConstantBase =
364 (groupedTransposeUnsigned32FromNatural (byte-to-nat (byte 40)))
365
366def groupedTransposeInputPointer =
367 (groupedTransposeUnsigned32FromNatural groupedTransposeInputPointerOffset)
368
369def groupedTransposeOutputPointer =
370 (groupedTransposeUnsigned32FromNatural groupedTransposeOutputPointerOffset)
371
372def groupedTransposeR =
373 (lambda unrestricted value : Byte . (sm86Register value))
374
375def groupedTransposeR0 =
376 (groupedTransposeR (byte 0))
377
378def groupedTransposeR1 =
379 (groupedTransposeR (byte 1))
380
381def groupedTransposeR2 =
382 (groupedTransposeR (byte 2))
383
384def groupedTransposeR3 =
385 (groupedTransposeR (byte 3))
386
387def groupedTransposeR4 =
388 (groupedTransposeR (byte 4))
389
390def groupedTransposeR5 =
391 (groupedTransposeR (byte 5))
392
393def groupedTransposeR6 =
394 (groupedTransposeR (byte 6))
395
396def groupedTransposeR8 =
397 (groupedTransposeR (byte 8))
398
399def groupedTransposeR10 =
400 (groupedTransposeR (byte 10))
401
402def groupedTransposeR12 =
403 (groupedTransposeR (byte 12))
404
405def groupedTransposeR13 =
406 (groupedTransposeR (byte 13))
407
408def groupedTransposeR14 =
409 (groupedTransposeR (byte 14))
410
411def groupedTransposeR15 =
412 (groupedTransposeR (byte 15))
413
414def groupedTransposeR16 =
415 (groupedTransposeR (byte 16))
416
417def groupedTransposeR17 =
418 (groupedTransposeR (byte 17))
419
420def groupedTransposeR18 =
421 (groupedTransposeR (byte 18))
422
423def groupedTransposeR19 =
424 (groupedTransposeR (byte 19))
425
426def groupedTransposeR20 =
427 (groupedTransposeR (byte 20))
428
429def groupedTransposeR22 =
430 (groupedTransposeR (byte 22))
431
432def groupedTransposeR24 =
433 (groupedTransposeR (byte 24))
434
435def groupedTransposeSet0 =
436 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
437
438def groupedTransposeWait0 =
439 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))
440
441def groupedTransposeNext =
442 (lambda unrestricted body : (family SM86InstructionBody) .
443 (lambda unrestricted tail : (family SM86Program) .
444 (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))
445
446def validateGroupedTransposeGeometry =
447 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
448 (eliminate
449 GroupedTransposeGeometry
450 (lambda unrestricted current : (family GroupedTransposeGeometry) .
451 (family GroupedTransposeValidationResult))
452 geometry
453 (branch
454 GroupedTransposeGeometryValue
455 groups
456 rows
457 columns
458 .
459 (nat-eliminate
460 (lambda unrestricted groupsPositive : Nat . (family GroupedTransposeValidationResult))
461 (constructor
462 GroupedTransposeValidationResult
463 GroupedTransposeGeometryRejected
464 (constructor GroupedTransposeFailureCode GroupedTransposeGroupsZero))
465 (lambda unrestricted groupsPred : Nat .
466 (lambda unrestricted groupsInd : (family GroupedTransposeValidationResult) .
467 (nat-eliminate
468 (lambda unrestricted groupsBounded : Nat .
469 (family GroupedTransposeValidationResult))
470 (constructor
471 GroupedTransposeValidationResult
472 GroupedTransposeGeometryRejected
473 (constructor GroupedTransposeFailureCode GroupedTransposeGroupsOutOfRange))
474 (lambda unrestricted groupsBoundPred : Nat .
475 (lambda unrestricted groupsBoundInd : (family GroupedTransposeValidationResult) .
476 (nat-eliminate
477 (lambda unrestricted dimensionsPositive : Nat .
478 (family GroupedTransposeValidationResult))
479 (constructor
480 GroupedTransposeValidationResult
481 GroupedTransposeGeometryRejected
482 (constructor GroupedTransposeFailureCode GroupedTransposeDimensionZero))
483 (lambda unrestricted dimensionsPred : Nat .
484 (lambda unrestricted dimensionsInd : (family GroupedTransposeValidationResult) .
485 (nat-eliminate
486 (lambda unrestricted tileExact : Nat .
487 (family GroupedTransposeValidationResult))
488 (constructor
489 GroupedTransposeValidationResult
490 GroupedTransposeGeometryRejected
491 (constructor
492 GroupedTransposeFailureCode
493 GroupedTransposeDimensionNotTileMultiple))
494 (lambda unrestricted tilePred : Nat .
495 (lambda unrestricted tileInd : (family GroupedTransposeValidationResult) .
496 (nat-eliminate
497 (lambda unrestricted sourceOffsetBounded : Nat .
498 (family GroupedTransposeValidationResult))
499 (constructor
500 GroupedTransposeValidationResult
501 GroupedTransposeGeometryRejected
502 (constructor
503 GroupedTransposeFailureCode
504 GroupedTransposeSourceOffsetOverflow))
505 (lambda unrestricted sourcePred : Nat .
506 (lambda unrestricted sourceInd : (family GroupedTransposeValidationResult) .
507 (nat-eliminate
508 (lambda unrestricted extentBounded : Nat .
509 (family GroupedTransposeValidationResult))
510 (constructor
511 GroupedTransposeValidationResult
512 GroupedTransposeGeometryRejected
513 (constructor
514 GroupedTransposeFailureCode
515 GroupedTransposeTensorExtentOverflow))
516 (lambda unrestricted extentPred : Nat .
517 (lambda unrestricted extentInd : (family GroupedTransposeValidationResult) .
518 (constructor
519 GroupedTransposeValidationResult
520 GroupedTransposeGeometryValidated
521 (constructor
522 GroupedTransposeGrid
523 GroupedTransposeGridValue
524 (naturalDivideUnchecked columns groupedTransposeN32)
525 (naturalDivideUnchecked rows groupedTransposeN32)
526 groups))))
527 (naturalFitsWord32
528 (naturalDivideUnchecked
529 (naturalMultiply groups (naturalMultiply rows columns))
530 groupedTransposeN2)))))
531 (naturalBelowTwoPower
532 (byte-to-nat (byte 24))
533 (naturalMultiply groupedTransposeN62 columns)))))
534 (naturalAnd
535 (naturalIsZero (naturalModuloUnchecked rows groupedTransposeN32))
536 (naturalIsZero (naturalModuloUnchecked columns groupedTransposeN32))))))
537 (naturalAnd (naturalNonzero rows) (naturalNonzero columns)))))
538 (naturalBelowTwoPower groupedTransposeN16 groups))))
539 (naturalNonzero groups)))))
540
541def groupedTransposeGrid =
542 validateGroupedTransposeGeometry
543
544def groupedTransposePrefix =
545 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
546 (eliminate
547 GroupedTransposeGeometry
548 (lambda unrestricted current : (family GroupedTransposeGeometry) . (family SM86Program))
549 geometry
550 (branch
551 GroupedTransposeGeometryValue
552 groups
553 rows
554 columns
555 .
556 (groupedTransposeNext
557 (constructor
558 SM86InstructionBody
559 SM86MoveConstant
560 groupedTransposeR1
561 (byte 0)
562 groupedTransposeConstantBase
563 sm86SafeControl)
564 (groupedTransposeNext
565 (constructor
566 SM86InstructionBody
567 SM86SpecialToRegister
568 groupedTransposeR2
569 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
570 groupedTransposeSet0)
571 (groupedTransposeNext
572 (constructor
573 SM86InstructionBody
574 SM86MoveImmediate
575 groupedTransposeR3
576 groupedTransposeU4
577 groupedTransposeWait0)
578 (groupedTransposeNext
579 (constructor
580 SM86InstructionBody
581 SM86SpecialToRegister
582 groupedTransposeR4
583 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY)
584 groupedTransposeSet0)
585 (groupedTransposeNext
586 (constructor
587 SM86InstructionBody
588 SM86IntegerAddThreeImmediate
589 groupedTransposeR4
590 groupedTransposeR4
591 groupedTransposeU0
592 groupedTransposeWait0)
593 (groupedTransposeNext
594 (constructor
595 SM86InstructionBody
596 SM86SpecialToRegister
597 groupedTransposeR5
598 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdZ)
599 groupedTransposeSet0)
600 (groupedTransposeNext
601 (constructor
602 SM86InstructionBody
603 SM86IntegerAddThreeImmediate
604 groupedTransposeR5
605 groupedTransposeR5
606 groupedTransposeU0
607 groupedTransposeWait0)
608 (groupedTransposeNext
609 (constructor
610 SM86InstructionBody
611 SM86SpecialToRegister
612 groupedTransposeR0
613 (constructor SM86SpecialRegister SM86ThreadIdX)
614 groupedTransposeSet0)
615 (groupedTransposeNext
616 (constructor
617 SM86InstructionBody
618 SM86IntegerAddThreeImmediate
619 groupedTransposeR0
620 groupedTransposeR0
621 groupedTransposeU0
622 groupedTransposeWait0)
623 (groupedTransposeNext
624 (constructor
625 SM86InstructionBody
626 SM86MoveImmediate
627 groupedTransposeR6
628 groupedTransposeU65535
629 sm86SafeControl)
630 (groupedTransposeNext
631 (constructor
632 SM86InstructionBody
633 SM86IntegerMultiplyAddImmediate
634 groupedTransposeR8
635 groupedTransposeR5
636 (groupedTransposeUnsigned32FromNatural
637 (naturalDivideUnchecked
638 (naturalMultiply rows columns)
639 groupedTransposeN2))
640 sm86ZeroRegister
641 sm86SafeControl)
642 (groupedTransposeNext
643 (constructor
644 SM86InstructionBody
645 SM86IntegerMultiplyAddImmediate
646 groupedTransposeR8
647 groupedTransposeR4
648 (groupedTransposeUnsigned32FromNatural
649 (naturalMultiply groupedTransposeN16 columns))
650 groupedTransposeR8
651 sm86SafeControl)
652 (groupedTransposeNext
653 (constructor
654 SM86InstructionBody
655 SM86IntegerMultiplyAddImmediate
656 groupedTransposeR8
657 groupedTransposeR2
658 groupedTransposeU16
659 groupedTransposeR8
660 sm86SafeControl)
661 (groupedTransposeNext
662 (constructor
663 SM86InstructionBody
664 SM86IntegerMultiplyAddImmediate
665 groupedTransposeR8
666 groupedTransposeR0
667 (groupedTransposeUnsigned32FromNatural groupedTransposeOne)
668 groupedTransposeR8
669 sm86SafeControl)
670 (groupedTransposeNext
671 (constructor
672 SM86InstructionBody
673 SM86IntegerMultiplyAddWideConstant
674 groupedTransposeR10
675 groupedTransposeR8
676 groupedTransposeR3
677 (byte 0)
678 groupedTransposeInputPointer
679 sm86SafeControl)
680 (groupedTransposeNext
681 (constructor
682 SM86InstructionBody
683 SM86IntegerMultiplyAddImmediate
684 groupedTransposeR20
685 groupedTransposeR5
686 (groupedTransposeUnsigned32FromNatural
687 (naturalDivideUnchecked
688 (naturalMultiply rows columns)
689 groupedTransposeN2))
690 sm86ZeroRegister
691 sm86SafeControl)
692 (groupedTransposeNext
693 (constructor
694 SM86InstructionBody
695 SM86IntegerMultiplyAddImmediate
696 groupedTransposeR20
697 groupedTransposeR2
698 (groupedTransposeUnsigned32FromNatural
699 (naturalMultiply groupedTransposeN16 rows))
700 groupedTransposeR20
701 sm86SafeControl)
702 (groupedTransposeNext
703 (constructor
704 SM86InstructionBody
705 SM86IntegerMultiplyAddImmediate
706 groupedTransposeR20
707 groupedTransposeR0
708 (groupedTransposeUnsigned32FromNatural rows)
709 groupedTransposeR20
710 sm86SafeControl)
711 (groupedTransposeNext
712 (constructor
713 SM86InstructionBody
714 SM86IntegerMultiplyAddImmediate
715 groupedTransposeR20
716 groupedTransposeR4
717 groupedTransposeU16
718 groupedTransposeR20
719 sm86SafeControl)
720 (groupedTransposeNext
721 (constructor
722 SM86InstructionBody
723 SM86IntegerMultiplyAddWideConstant
724 groupedTransposeR22
725 groupedTransposeR20
726 groupedTransposeR3
727 (byte 0)
728 groupedTransposeOutputPointer
729 sm86SafeControl)
730 (groupedTransposeNext
731 (constructor
732 SM86InstructionBody
733 SM86IntegerAddThreeImmediate
734 groupedTransposeR20
735 groupedTransposeR20
736 (groupedTransposeUnsigned32FromNatural
737 (naturalDivideUnchecked rows groupedTransposeN2))
738 sm86SafeControl)
739 (groupedTransposeNext
740 (constructor
741 SM86InstructionBody
742 SM86IntegerMultiplyAddWideConstant
743 groupedTransposeR24
744 groupedTransposeR20
745 groupedTransposeR3
746 (byte 0)
747 groupedTransposeOutputPointer
748 sm86SafeControl)
749 (constructor SM86Program SM86ProgramEnd))))))))))))))))))))))))))
750
751def groupedTransposeRowPair =
752 (lambda unrestricted pairIndex : Nat .
753 (lambda unrestricted columns : Nat .
754 (lambda unrestricted tail : (family SM86Program) .
755 (groupedTransposeNext
756 (constructor
757 SM86InstructionBody
758 SM86LoadGlobal
759 groupedTransposeR12
760 groupedTransposeR10
761 (groupedTransposeUnsigned32FromNatural
762 (naturalMultiply pairIndex (naturalMultiply groupedTransposeN4 columns)))
763 groupedTransposeSet0)
764 (groupedTransposeNext
765 (constructor
766 SM86InstructionBody
767 SM86LogicThreeInputTruthTable
768 groupedTransposeR14
769 groupedTransposeR12
770 groupedTransposeR6
771 (byte 192)
772 groupedTransposeWait0)
773 (groupedTransposeNext
774 (constructor
775 SM86InstructionBody
776 SM86ShiftRightImmediate
777 groupedTransposeR15
778 groupedTransposeR12
779 (byte 16)
780 sm86SafeControl)
781 (groupedTransposeNext
782 (constructor
783 SM86InstructionBody
784 SM86LoadGlobal
785 groupedTransposeR13
786 groupedTransposeR10
787 (groupedTransposeUnsigned32FromNatural
788 (naturalMultiply
789 (succ (naturalMultiply pairIndex groupedTransposeN2))
790 (naturalMultiply groupedTransposeN2 columns)))
791 groupedTransposeSet0)
792 (groupedTransposeNext
793 (constructor
794 SM86InstructionBody
795 SM86LogicThreeInputTruthTable
796 groupedTransposeR16
797 groupedTransposeR13
798 groupedTransposeR6
799 (byte 192)
800 groupedTransposeWait0)
801 (groupedTransposeNext
802 (constructor
803 SM86InstructionBody
804 SM86ShiftRightImmediate
805 groupedTransposeR17
806 groupedTransposeR13
807 (byte 16)
808 sm86SafeControl)
809 (groupedTransposeNext
810 (constructor
811 SM86InstructionBody
812 SM86IntegerMultiplyAddImmediate
813 groupedTransposeR18
814 groupedTransposeR16
815 (groupedTransposeUnsigned32FromNatural
816 (naturalPowerOfTwo groupedTransposeN16))
817 groupedTransposeR14
818 sm86SafeControl)
819 (groupedTransposeNext
820 (constructor
821 SM86InstructionBody
822 SM86IntegerMultiplyAddImmediate
823 groupedTransposeR19
824 groupedTransposeR17
825 (groupedTransposeUnsigned32FromNatural
826 (naturalPowerOfTwo groupedTransposeN16))
827 groupedTransposeR15
828 sm86SafeControl)
829 (groupedTransposeNext
830 (constructor
831 SM86InstructionBody
832 SM86StoreGlobal
833 groupedTransposeR22
834 groupedTransposeR18
835 (groupedTransposeUnsigned32FromNatural
836 (naturalMultiply pairIndex groupedTransposeN4))
837 sm86SafeControl)
838 (groupedTransposeNext
839 (constructor
840 SM86InstructionBody
841 SM86StoreGlobal
842 groupedTransposeR24
843 groupedTransposeR19
844 (groupedTransposeUnsigned32FromNatural
845 (naturalMultiply pairIndex groupedTransposeN4))
846 sm86SafeControl)
847 tail)))))))))))))
848
849def groupedTransposeRows =
850 (lambda unrestricted count : Nat .
851 (lambda unrestricted columns : Nat .
852 (nat-eliminate
853 (lambda unrestricted current : Nat . (family SM86Program))
854 (constructor SM86Program SM86ProgramEnd)
855 (lambda unrestricted predecessor : Nat .
856 (lambda unrestricted induction : (family SM86Program) .
857 (groupedTransposeRowPair predecessor columns induction)))
858 count)))
859
860def emitGroupedTransposeFP16SM86 =
861 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
862 (eliminate
863 GroupedTransposeGeometry
864 (lambda unrestricted current : (family GroupedTransposeGeometry) . (family SM86Program))
865 geometry
866 (branch
867 GroupedTransposeGeometryValue
868 groups
869 rows
870 columns
871 .
872 (sm86ProgramAppend
873 (groupedTransposePrefix geometry)
874 (sm86ProgramAppend
875 (groupedTransposeRows groupedTransposeN16 columns)
876 (groupedTransposeNext
877 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
878 (constructor SM86Program SM86ProgramEnd)))))))
879
880def groupedTransposeTelemetryFor =
881 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
882 (lambda unrestricted instructions : Nat .
883 (lambda unrestricted encodedBytes : Nat .
884 (eliminate
885 GroupedTransposeGeometry
886 (lambda unrestricted current : (family GroupedTransposeGeometry) .
887 (family GroupedTransposeTelemetry))
888 geometry
889 (branch
890 GroupedTransposeGeometryValue
891 groups
892 rows
893 columns
894 .
895 (constructor
896 GroupedTransposeTelemetry
897 GroupedTransposeTelemetryValue
898 groups
899 rows
900 columns
901 (naturalDivideUnchecked columns groupedTransposeN32)
902 (naturalDivideUnchecked rows groupedTransposeN32)
903 groups
904 instructions
905 encodedBytes
906 groupedTransposeN32
907 groupedTransposeN32
908 groupedTransposeRegisterCount
909 groupedTransposeSharedBytes
910 groupedTransposeHostFallbackCalls
911 groupedTransposeHostStagingTransfers
912 groupedTransposeHostCallbacks
913 applicationBuilderNativeOnly
914 groupedTransposeABI
915 groupedTransposeResourcePolicy
916 groupedTransposeDifferentialRuns
917 groupedTransposeApplicationWitness))))))
918
919def groupedTransposeEmptyTelemetry =
920 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
921 (groupedTransposeTelemetryFor geometry zero zero))
922
923def groupedTransposeObservedTelemetry =
924 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
925 (lambda unrestricted instructions : Nat .
926 (lambda unrestricted encodedBytes : Nat .
927 (groupedTransposeTelemetryFor geometry instructions encodedBytes))))
928
929def groupedTransposeContractFailureFor =
930 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
931 (lambda unrestricted instructions : Nat .
932 (lambda unrestricted encodedBytes : Nat .
933 (lambda unrestricted failure : (family GroupedTransposeFailureCode) .
934 (constructor
935 GroupedTransposeBuildResult
936 GroupedTransposeContractFailed
937 failure
938 (groupedTransposeObservedTelemetry geometry instructions encodedBytes))))))
939
940def groupedTransposeEncodingFailureFor =
941 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
942 (lambda unrestricted instructions : Nat .
943 (lambda unrestricted encodedBytes : Nat .
944 (lambda unrestricted failure : (family GroupedTransposeFailureCode) .
945 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
946 (constructor
947 GroupedTransposeBuildResult
948 GroupedTransposeImageEncodingFailed
949 failure
950 encoding
951 (groupedTransposeObservedTelemetry geometry instructions encodedBytes)))))))
952
953def groupedTransposeIdentityFailureFor =
954 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
955 (lambda unrestricted instructions : Nat .
956 (lambda unrestricted encodedBytes : Nat .
957 (lambda unrestricted failure : (family GroupedTransposeFailureCode) .
958 (lambda unrestricted identityResult : (family SHA256HexResult) .
959 (constructor
960 GroupedTransposeBuildResult
961 GroupedTransposeImageIdentityFailed
962 failure
963 identityResult
964 (groupedTransposeObservedTelemetry geometry instructions encodedBytes)))))))
965
966def groupedTransposeDifferentialIdentity =
967 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
968 (lambda unrestricted count : Nat .
969 (lambda unrestricted bytes : Bytes .
970 (lambda unrestricted identity : Bytes .
971 (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) .
972 (lambda unrestricted identityTelemetry : (family SHA256DigestTelemetry) .
973 (lambda unrestricted candidateBytes : Bytes .
974 (lambda unrestricted candidateEncodingTelemetry : (family SM86ProgramEncodingTelemetry) .
975 (lambda unrestricted candidateIdentityResult : (family SHA256HexResult) .
976 (eliminate
977 SHA256HexResult
978 (lambda unrestricted current : (family SHA256HexResult) .
979 (family GroupedTransposeBuildResult))
980 candidateIdentityResult
981 (branch
982 SHA256HexSucceeded
983 candidateIdentity
984 candidateIdentityTelemetry
985 .
986 (nat-eliminate
987 (lambda unrestricted identityLengthExact : Nat .
988 (family GroupedTransposeBuildResult))
989 (groupedTransposeIdentityFailureFor
990 geometry
991 count
992 (bytes-length candidateBytes)
993 (constructor
994 GroupedTransposeFailureCode
995 GroupedTransposeIdentityLengthInvalid)
996 candidateIdentityResult)
997 (lambda unrestricted identityLengthPred : Nat .
998 (lambda unrestricted identityLengthInd : (family GroupedTransposeBuildResult) .
999 (nat-eliminate
1000 (lambda unrestricted identityExact : Nat .
1001 (family GroupedTransposeBuildResult))
1002 (groupedTransposeContractFailureFor
1003 geometry
1004 count
1005 (bytes-length candidateBytes)
1006 (constructor
1007 GroupedTransposeFailureCode
1008 GroupedTransposeDifferentialIdentityMismatch))
1009 (lambda unrestricted identityPred : Nat .
1010 (lambda unrestricted identityInd : (family GroupedTransposeBuildResult) .
1011 (constructor
1012 GroupedTransposeBuildResult
1013 GroupedTransposeBuildSucceeded
1014 bytes
1015 identity
1016 groupedTransposeABI
1017 groupedTransposeResourcePolicy
1018 (constructor
1019 GroupedTransposeDifferentialReceipt
1020 GroupedTransposeDifferentialReceiptValue
1021 (bytes-length bytes)
1022 (bytes-length candidateBytes)
1023 identity
1024 candidateIdentity
1025 candidateEncodingTelemetry
1026 candidateIdentityTelemetry
1027 groupedTransposeDifferentialRuns)
1028 encodingTelemetry
1029 identityTelemetry
1030 (groupedTransposeObservedTelemetry
1031 geometry
1032 count
1033 (bytes-length bytes)))))
1034 (bytes-equal identity candidateIdentity))))
1035 (naturalEqual (bytes-length candidateIdentity) groupedTransposeN64)))
1036 (branch
1037 SHA256HexFailed
1038 error
1039 ordinal
1040 candidateIdentityTelemetry
1041 .
1042 (groupedTransposeIdentityFailureFor
1043 geometry
1044 count
1045 (bytes-length candidateBytes)
1046 (constructor
1047 GroupedTransposeFailureCode
1048 GroupedTransposeDifferentialIdentityFailed)
1049 candidateIdentityResult))))))))))))
1050
1051def groupedTransposeDifferentialEncoding =
1052 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
1053 (lambda unrestricted count : Nat .
1054 (lambda unrestricted bytes : Bytes .
1055 (lambda unrestricted identity : Bytes .
1056 (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) .
1057 (lambda unrestricted identityTelemetry : (family SHA256DigestTelemetry) .
1058 (lambda unrestricted candidateEncoding : (family SM86ProgramEncodingResult) .
1059 (eliminate
1060 SM86ProgramEncodingResult
1061 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1062 (family GroupedTransposeBuildResult))
1063 candidateEncoding
1064 (branch
1065 SM86ProgramEncodingSucceeded
1066 candidateBytes
1067 candidateTelemetry
1068 .
1069 (nat-eliminate
1070 (lambda unrestricted candidateLengthExact : Nat .
1071 (family GroupedTransposeBuildResult))
1072 (groupedTransposeContractFailureFor
1073 geometry
1074 count
1075 (bytes-length candidateBytes)
1076 (constructor
1077 GroupedTransposeFailureCode
1078 GroupedTransposeDifferentialEncodedByteCountMismatch))
1079 (lambda unrestricted candidateLengthPred : Nat .
1080 (lambda unrestricted candidateLengthInd : (family GroupedTransposeBuildResult) .
1081 (nat-eliminate
1082 (lambda unrestricted imageExact : Nat .
1083 (family GroupedTransposeBuildResult))
1084 (groupedTransposeContractFailureFor
1085 geometry
1086 count
1087 (bytes-length candidateBytes)
1088 (constructor
1089 GroupedTransposeFailureCode
1090 GroupedTransposeDifferentialImageMismatch))
1091 (lambda unrestricted imagePred : Nat .
1092 (lambda unrestricted imageInd : (family GroupedTransposeBuildResult) .
1093 (groupedTransposeDifferentialIdentity
1094 geometry
1095 count
1096 bytes
1097 identity
1098 encodingTelemetry
1099 identityTelemetry
1100 candidateBytes
1101 candidateTelemetry
1102 (sha256Hex candidateBytes))))
1103 (bytes-equal bytes candidateBytes))))
1104 (naturalEqual (bytes-length candidateBytes) groupedTransposeEncodedByteCount)))
1105 (branch
1106 SM86ProgramEncodingFailed
1107 index
1108 failure
1109 candidateTelemetry
1110 .
1111 (groupedTransposeEncodingFailureFor
1112 geometry
1113 count
1114 (bytes-length bytes)
1115 (constructor
1116 GroupedTransposeFailureCode
1117 GroupedTransposeDifferentialEncodingFailed)
1118 candidateEncoding))))))))))
1119
1120def groupedTransposeFinalizeNative =
1121 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
1122 (lambda unrestricted program : (family SM86Program) .
1123 (lambda unrestricted count : Nat .
1124 (lambda unrestricted bytes : Bytes .
1125 (lambda unrestricted identity : Bytes .
1126 (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) .
1127 (lambda unrestricted identityTelemetry : (family SHA256DigestTelemetry) .
1128 (nat-eliminate
1129 (lambda unrestricted builderNative : Nat . (family GroupedTransposeBuildResult))
1130 (groupedTransposeContractFailureFor
1131 geometry
1132 count
1133 (bytes-length bytes)
1134 (constructor
1135 GroupedTransposeFailureCode
1136 GroupedTransposeApplicationBuilderRejected))
1137 (lambda unrestricted builderPred : Nat .
1138 (lambda unrestricted builderInd : (family GroupedTransposeBuildResult) .
1139 (nat-eliminate
1140 (lambda unrestricted fallbackFree : Nat .
1141 (family GroupedTransposeBuildResult))
1142 (groupedTransposeContractFailureFor
1143 geometry
1144 count
1145 (bytes-length bytes)
1146 (constructor
1147 GroupedTransposeFailureCode
1148 GroupedTransposeHostFallbackObserved))
1149 (lambda unrestricted fallbackPred : Nat .
1150 (lambda unrestricted fallbackInd : (family GroupedTransposeBuildResult) .
1151 (nat-eliminate
1152 (lambda unrestricted stagingFree : Nat .
1153 (family GroupedTransposeBuildResult))
1154 (groupedTransposeContractFailureFor
1155 geometry
1156 count
1157 (bytes-length bytes)
1158 (constructor
1159 GroupedTransposeFailureCode
1160 GroupedTransposeHostStagingObserved))
1161 (lambda unrestricted stagingPred : Nat .
1162 (lambda unrestricted stagingInd : (family GroupedTransposeBuildResult) .
1163 (nat-eliminate
1164 (lambda unrestricted callbackFree : Nat .
1165 (family GroupedTransposeBuildResult))
1166 (groupedTransposeContractFailureFor
1167 geometry
1168 count
1169 (bytes-length bytes)
1170 (constructor
1171 GroupedTransposeFailureCode
1172 GroupedTransposeHostCallbackObserved))
1173 (lambda unrestricted callbackPred : Nat .
1174 (lambda unrestricted callbackInd : (family GroupedTransposeBuildResult) .
1175 (groupedTransposeDifferentialEncoding
1176 geometry
1177 count
1178 bytes
1179 identity
1180 encodingTelemetry
1181 identityTelemetry
1182 (sm86EncodeProgram program))))
1183 (naturalEqual groupedTransposeHostCallbacks zero))))
1184 (naturalEqual groupedTransposeHostStagingTransfers zero))))
1185 (naturalEqual groupedTransposeHostFallbackCalls zero))))
1186 applicationBuilderNativeOnly))))))))
1187
1188def groupedTransposeBuildEncoded =
1189 (lambda unrestricted geometry : (family GroupedTransposeGeometry) .
1190 (eliminate
1191 GroupedTransposeValidationResult
1192 (lambda unrestricted current : (family GroupedTransposeValidationResult) .
1193 (family GroupedTransposeBuildResult))
1194 (validateGroupedTransposeGeometry geometry)
1195 (branch
1196 GroupedTransposeGeometryValidated
1197 grid
1198 .
1199 (app
1200 (lambda unrestricted program : (family SM86Program) .
1201 (app
1202 (lambda unrestricted count : Nat .
1203 (nat-eliminate
1204 (lambda unrestricted countExact : Nat . (family GroupedTransposeBuildResult))
1205 (constructor
1206 GroupedTransposeBuildResult
1207 GroupedTransposeContractFailed
1208 (constructor
1209 GroupedTransposeFailureCode
1210 GroupedTransposeInstructionCountMismatch)
1211 (groupedTransposeTelemetryFor geometry count zero))
1212 (lambda unrestricted countPred : Nat .
1213 (lambda unrestricted countInd : (family GroupedTransposeBuildResult) .
1214 (app
1215 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
1216 (eliminate
1217 SM86ProgramEncodingResult
1218 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1219 (family GroupedTransposeBuildResult))
1220 encoding
1221 (branch
1222 SM86ProgramEncodingSucceeded
1223 bytes
1224 encodingTelemetry
1225 .
1226 (nat-eliminate
1227 (lambda unrestricted bytesExact : Nat .
1228 (family GroupedTransposeBuildResult))
1229 (constructor
1230 GroupedTransposeBuildResult
1231 GroupedTransposeContractFailed
1232 (constructor
1233 GroupedTransposeFailureCode
1234 GroupedTransposeEncodedByteCountMismatch)
1235 (groupedTransposeTelemetryFor geometry count (bytes-length bytes)))
1236 (lambda unrestricted bytesPred : Nat .
1237 (lambda unrestricted bytesInd : (family GroupedTransposeBuildResult) .
1238 (app
1239 (lambda unrestricted identityResult : (family SHA256HexResult) .
1240 (eliminate
1241 SHA256HexResult
1242 (lambda unrestricted current : (family SHA256HexResult) .
1243 (family GroupedTransposeBuildResult))
1244 identityResult
1245 (branch
1246 SHA256HexSucceeded
1247 identity
1248 identityTelemetry
1249 .
1250 (nat-eliminate
1251 (lambda unrestricted identityExact : Nat .
1252 (family GroupedTransposeBuildResult))
1253 (constructor
1254 GroupedTransposeBuildResult
1255 GroupedTransposeImageIdentityFailed
1256 (constructor
1257 GroupedTransposeFailureCode
1258 GroupedTransposeIdentityLengthInvalid)
1259 identityResult
1260 (groupedTransposeTelemetryFor
1261 geometry
1262 count
1263 (bytes-length bytes)))
1264 (lambda unrestricted identityPred : Nat .
1265 (lambda unrestricted identityInd : (family GroupedTransposeBuildResult) .
1266 (groupedTransposeFinalizeNative
1267 geometry
1268 program
1269 count
1270 bytes
1271 identity
1272 encodingTelemetry
1273 identityTelemetry)))
1274 (naturalEqual (bytes-length identity) groupedTransposeN64)))
1275 (branch
1276 SHA256HexFailed
1277 error
1278 ordinal
1279 identityTelemetry
1280 .
1281 (constructor
1282 GroupedTransposeBuildResult
1283 GroupedTransposeImageIdentityFailed
1284 (constructor
1285 GroupedTransposeFailureCode
1286 GroupedTransposeIdentityFailed)
1287 identityResult
1288 (groupedTransposeTelemetryFor
1289 geometry
1290 count
1291 (bytes-length bytes))))))
1292 (sha256Hex bytes))))
1293 (naturalEqual (bytes-length bytes) groupedTransposeEncodedByteCount)))
1294 (branch
1295 SM86ProgramEncodingFailed
1296 index
1297 failure
1298 encodingTelemetry
1299 .
1300 (constructor
1301 GroupedTransposeBuildResult
1302 GroupedTransposeImageEncodingFailed
1303 (constructor
1304 GroupedTransposeFailureCode
1305 GroupedTransposeEncodingFailed)
1306 encoding
1307 (groupedTransposeTelemetryFor geometry count zero)))))
1308 (sm86EncodeProgram program))))
1309 (naturalEqual count groupedTransposeInstructionCount)))
1310 (sm86ProgramCount program)))
1311 (emitGroupedTransposeFP16SM86 geometry)))
1312 (branch
1313 GroupedTransposeGeometryRejected
1314 failure
1315 .
1316 (constructor
1317 GroupedTransposeBuildResult
1318 GroupedTransposeContractFailed
1319 failure
1320 (groupedTransposeEmptyTelemetry geometry)))))
1321
1322-- Coppelius uses a deliberately small tiled transpose realization for dense
1323-- backward operands. A CTA owns a pair of input rows and one 128-column tile;
1324-- every one of its 64 threads owns two adjacent columns. The two source packed
1325-- words are unpacked and then repacked as two adjacent-row destination words.
1326-- This makes every global access 32-bit while preserving each FP16 payload
1327-- bit-for-bit, without making the block width grow with the matrix width.
1328--
1329-- Launch contract for rows x columns:
1330-- grid = (rows / 2, columns / tile, groups)
1331-- block = (tile / 2, 1, 1) (coppeliusFP16TransposeBlockThreads)
1332-- c[0][0x160] = output pointer, c[0][0x168] = input pointer
1333-- Rows must be even and columns must be a multiple of 128. Every Coppelius
1334-- activation and weight geometry satisfies that contract, including the
1335-- 1408-wide feed-forward and 12288-wide vocabulary matrices.
1336def coppeliusFP16TransposeInstructionCount : Nat =
1337 (byte-to-nat (byte 31))
1338
1339def coppeliusFP16TransposeRegisterCount : Nat =
1340 (byte-to-nat (byte 27))
1341
1342def coppeliusFP16TransposeTiledProgram =
1343 (lambda unrestricted tileColumns : Nat .
1344 (app
1345 (lambda unrestricted halfTileColumns : Nat .
1346 (lambda unrestricted groups : Nat .
1347 (lambda unrestricted rows : Nat .
1348 (lambda unrestricted columns : Nat .
1349 (app
1350 (lambda unrestricted halfRows : Nat .
1351 (app
1352 (lambda unrestricted halfColumns : Nat .
1353 (app
1354 (lambda unrestricted groupWords : Nat .
1355 (groupedTransposeNext
1356 (constructor
1357 SM86InstructionBody
1358 SM86SpecialToRegister
1359 groupedTransposeR0
1360 (constructor SM86SpecialRegister SM86ThreadIdX)
1361 groupedTransposeSet0)
1362 (groupedTransposeNext
1363 (constructor
1364 SM86InstructionBody
1365 SM86IntegerMultiplyAddImmediate
1366 groupedTransposeR4
1367 groupedTransposeR0
1368 (groupedTransposeUnsigned32FromNatural groupedTransposeN2)
1369 sm86ZeroRegister
1370 groupedTransposeWait0)
1371 (groupedTransposeNext
1372 (constructor
1373 SM86InstructionBody
1374 SM86SpecialToRegister
1375 groupedTransposeR1
1376 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
1377 groupedTransposeSet0)
1378 (groupedTransposeNext
1379 (constructor
1380 SM86InstructionBody
1381 SM86IntegerMultiplyAddImmediate
1382 groupedTransposeR14
1383 groupedTransposeR1
1384 (groupedTransposeUnsigned32FromNatural columns)
1385 sm86ZeroRegister
1386 groupedTransposeWait0)
1387 (groupedTransposeNext
1388 (constructor
1389 SM86InstructionBody
1390 SM86SpecialToRegister
1391 groupedTransposeR2
1392 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY)
1393 groupedTransposeSet0)
1394 (groupedTransposeNext
1395 (constructor
1396 SM86InstructionBody
1397 SM86SpecialToRegister
1398 (groupedTransposeR (byte 26))
1399 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdZ)
1400 groupedTransposeSet0)
1401 (groupedTransposeNext
1402 (constructor
1403 SM86InstructionBody
1404 SM86IntegerMultiplyAddImmediate
1405 groupedTransposeR5
1406 (groupedTransposeR (byte 26))
1407 (groupedTransposeUnsigned32FromNatural groupWords)
1408 sm86ZeroRegister
1409 groupedTransposeWait0)
1410 (groupedTransposeNext
1411 (constructor
1412 SM86InstructionBody
1413 SM86MoveImmediate
1414 groupedTransposeR3
1415 groupedTransposeU4
1416 sm86SafeControl)
1417 (groupedTransposeNext
1418 (constructor
1419 SM86InstructionBody
1420 SM86IntegerMultiplyAddImmediate
1421 groupedTransposeR14
1422 groupedTransposeR5
1423 (groupedTransposeUnsigned32FromNatural groupedTransposeOne)
1424 groupedTransposeR14
1425 sm86SafeControl)
1426 (groupedTransposeNext
1427 (constructor
1428 SM86InstructionBody
1429 SM86IntegerMultiplyAddImmediate
1430 groupedTransposeR14
1431 groupedTransposeR2
1432 (groupedTransposeUnsigned32FromNatural halfTileColumns)
1433 groupedTransposeR14
1434 sm86SafeControl)
1435 (groupedTransposeNext
1436 (constructor
1437 SM86InstructionBody
1438 SM86IntegerMultiplyAddImmediate
1439 groupedTransposeR14
1440 groupedTransposeR0
1441 (groupedTransposeUnsigned32FromNatural groupedTransposeOne)
1442 groupedTransposeR14
1443 sm86SafeControl)
1444 (groupedTransposeNext
1445 (constructor
1446 SM86InstructionBody
1447 SM86IntegerAddThreeImmediate
1448 groupedTransposeR15
1449 groupedTransposeR14
1450 (groupedTransposeUnsigned32FromNatural halfColumns)
1451 sm86SafeControl)
1452 (groupedTransposeNext
1453 (constructor
1454 SM86InstructionBody
1455 SM86IntegerMultiplyAddWideConstant
1456 groupedTransposeR6
1457 groupedTransposeR14
1458 groupedTransposeR3
1459 (byte 0)
1460 groupedTransposeInputPointer
1461 sm86SafeControl)
1462 (groupedTransposeNext
1463 (constructor
1464 SM86InstructionBody
1465 SM86IntegerMultiplyAddWideConstant
1466 groupedTransposeR8
1467 groupedTransposeR15
1468 groupedTransposeR3
1469 (byte 0)
1470 groupedTransposeInputPointer
1471 sm86SafeControl)
1472 (groupedTransposeNext
1473 (constructor
1474 SM86InstructionBody
1475 SM86IntegerMultiplyAddImmediate
1476 groupedTransposeR4
1477 groupedTransposeR2
1478 (groupedTransposeUnsigned32FromNatural tileColumns)
1479 groupedTransposeR4
1480 sm86SafeControl)
1481 (groupedTransposeNext
1482 (constructor
1483 SM86InstructionBody
1484 SM86IntegerMultiplyAddImmediate
1485 groupedTransposeR16
1486 groupedTransposeR4
1487 (groupedTransposeUnsigned32FromNatural halfRows)
1488 groupedTransposeR1
1489 sm86SafeControl)
1490 (groupedTransposeNext
1491 (constructor
1492 SM86InstructionBody
1493 SM86IntegerMultiplyAddImmediate
1494 groupedTransposeR16
1495 groupedTransposeR5
1496 (groupedTransposeUnsigned32FromNatural groupedTransposeOne)
1497 groupedTransposeR16
1498 sm86SafeControl)
1499 (groupedTransposeNext
1500 (constructor
1501 SM86InstructionBody
1502 SM86IntegerAddThreeImmediate
1503 groupedTransposeR17
1504 groupedTransposeR16
1505 (groupedTransposeUnsigned32FromNatural halfRows)
1506 sm86SafeControl)
1507 (groupedTransposeNext
1508 (constructor
1509 SM86InstructionBody
1510 SM86IntegerMultiplyAddWideConstant
1511 groupedTransposeR10
1512 groupedTransposeR16
1513 groupedTransposeR3
1514 (byte 0)
1515 groupedTransposeOutputPointer
1516 sm86SafeControl)
1517 (groupedTransposeNext
1518 (constructor
1519 SM86InstructionBody
1520 SM86IntegerMultiplyAddWideConstant
1521 groupedTransposeR12
1522 groupedTransposeR17
1523 groupedTransposeR3
1524 (byte 0)
1525 groupedTransposeOutputPointer
1526 sm86SafeControl)
1527 (groupedTransposeNext
1528 (constructor
1529 SM86InstructionBody
1530 SM86LoadGlobal
1531 groupedTransposeR18
1532 groupedTransposeR6
1533 groupedTransposeU0
1534 groupedTransposeSet0)
1535 (groupedTransposeNext
1536 (constructor
1537 SM86InstructionBody
1538 SM86HalfToFloat
1539 groupedTransposeR20
1540 groupedTransposeR18
1541 (constructor SM86HalfSelector SM86LowHalf)
1542 groupedTransposeWait0)
1543 (groupedTransposeNext
1544 (constructor
1545 SM86InstructionBody
1546 SM86HalfToFloat
1547 groupedTransposeR22
1548 groupedTransposeR18
1549 (constructor SM86HalfSelector SM86HighHalf)
1550 sm86SafeControl)
1551 (groupedTransposeNext
1552 (constructor
1553 SM86InstructionBody
1554 SM86LoadGlobal
1555 groupedTransposeR19
1556 groupedTransposeR8
1557 groupedTransposeU0
1558 groupedTransposeSet0)
1559 (groupedTransposeNext
1560 (constructor
1561 SM86InstructionBody
1562 SM86HalfToFloat
1563 (groupedTransposeR (byte 21))
1564 groupedTransposeR19
1565 (constructor SM86HalfSelector SM86LowHalf)
1566 groupedTransposeWait0)
1567 (groupedTransposeNext
1568 (constructor
1569 SM86InstructionBody
1570 SM86HalfToFloat
1571 (groupedTransposeR (byte 23))
1572 groupedTransposeR19
1573 (constructor SM86HalfSelector SM86HighHalf)
1574 sm86SafeControl)
1575 (groupedTransposeNext
1576 (constructor
1577 SM86InstructionBody
1578 SM86FloatPairToPackedHalfPair
1579 groupedTransposeR24
1580 (groupedTransposeR (byte 21))
1581 groupedTransposeR20
1582 sm86SafeControl)
1583 (groupedTransposeNext
1584 (constructor
1585 SM86InstructionBody
1586 SM86FloatPairToPackedHalfPair
1587 (groupedTransposeR (byte 25))
1588 (groupedTransposeR (byte 23))
1589 groupedTransposeR22
1590 sm86SafeControl)
1591 (groupedTransposeNext
1592 (constructor
1593 SM86InstructionBody
1594 SM86StoreGlobal
1595 groupedTransposeR10
1596 groupedTransposeR24
1597 groupedTransposeU0
1598 sm86SafeControl)
1599 (groupedTransposeNext
1600 (constructor
1601 SM86InstructionBody
1602 SM86StoreGlobal
1603 groupedTransposeR12
1604 (groupedTransposeR (byte 25))
1605 groupedTransposeU0
1606 sm86SafeControl)
1607 (groupedTransposeNext
1608 (constructor
1609 SM86InstructionBody
1610 SM86Exit
1611 sm86SafeControl)
1612 (constructor SM86Program SM86ProgramEnd)))))))))))))))))))))))))))))))))
1613 (naturalDivideUnchecked (naturalMultiply rows columns) groupedTransposeN2)))
1614 (naturalDivideUnchecked columns groupedTransposeN2)))
1615 (naturalDivideUnchecked rows groupedTransposeN2))))))
1616 (naturalDivideUnchecked tileColumns groupedTransposeN2)))
1617
1618def coppeliusFP16TransposeProgram =
1619 (lambda unrestricted groups : Nat .
1620 (lambda unrestricted rows : Nat .
1621 (lambda unrestricted columns : Nat .
1622 (coppeliusFP16TransposeTiledProgram 128 groups rows columns))))
1623
1624def coppeliusFP16Transpose64TileProgram =
1625 (lambda unrestricted groups : Nat .
1626 (lambda unrestricted rows : Nat .
1627 (lambda unrestricted columns : Nat .
1628 (coppeliusFP16TransposeTiledProgram 64 groups rows columns))))
1629
1630-- The block a tile needs: a thread per packed word of the tile's row pair
1631-- (two columns), so tileColumns / 2 threads. A wider block's extra threads
1632-- address words past the tile -- the next row's -- and store past the
1633-- group's output, over the next group's (the 64-column tile run with the
1634-- 128-column tile's 64 threads raced the next head's blocks).
1635def coppeliusFP16TransposeBlockThreads =
1636 (lambda unrestricted tileColumns : Nat .
1637 (naturalDivideUnchecked tileColumns 2))
1638
1639def coppeliusFP16Transpose1024x512Program : (family SM86Program) =
1640 (coppeliusFP16TransposeProgram 1 1024 512)
1641
1642def coppeliusFP16Transpose512x512Program : (family SM86Program) =
1643 (coppeliusFP16TransposeProgram 1 512 512)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.