1module Realization.Nvidia.SM86.ReductionSM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.Program
8import Data.SHA256Digest
9import Std.Natural
10import Accelerator.SM86.Types
11import Accelerator.SM86.NumericSemantics
12
13family ReductionSM86Primitive : Type 0
14constructor ReductionSM86WarpSum64
15constructor ReductionSM86WarpSum256
16constructor ReductionSM86WarpSum1024
17constructor ReductionSM86WarpMaximum256
18
19end-family
20
21family ReductionSM86FailureCode : Type 0
22constructor ReductionSM86WarpSum64InstructionCountMismatch
23constructor ReductionSM86WarpSum256InstructionCountMismatch
24constructor ReductionSM86WarpSum1024InstructionCountMismatch
25constructor ReductionSM86WarpMaximum256InstructionCountMismatch
26constructor ReductionSM86EncodingFailed
27constructor ReductionSM86IdentityFailed
28constructor ReductionSM86IdentityLengthInvalid
29
30end-family
31
32family ReductionSM86Telemetry : Type 0
33constructor ReductionSM86TelemetryValue
34field unrestricted reductionSM86TelemetryPrimitive : (family ReductionSM86Primitive)
35field unrestricted reductionSM86TelemetryExpectedInstructions : Nat
36field unrestricted reductionSM86TelemetryObservedInstructions : Nat
37field unrestricted reductionSM86TelemetryRegisters : Nat
38field unrestricted reductionSM86TelemetrySharedBytes : Nat
39field unrestricted reductionSM86TelemetryRequiredThreads : Nat
40
41end-family
42
43family ReductionSM86BuildResult : Type 0
44constructor ReductionSM86BuildSucceeded
45field unrestricted reductionSM86EncodedBytes : Bytes
46field unrestricted reductionSM86SnippetIdentity : Bytes
47field unrestricted reductionSM86ProgramEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
48field unrestricted reductionSM86IdentityTelemetry : (family SHA256DigestTelemetry)
49field unrestricted reductionSM86BuildTelemetry : (family ReductionSM86Telemetry)
50constructor ReductionSM86ContractFailed
51field unrestricted reductionSM86ContractFailure : (family ReductionSM86FailureCode)
52field unrestricted reductionSM86ContractFailureTelemetry : (family ReductionSM86Telemetry)
53constructor ReductionSM86SnippetEncodingFailed
54field unrestricted reductionSM86EncodingFailure : (family ReductionSM86FailureCode)
55field unrestricted reductionSM86FailedEncoding : (family SM86ProgramEncodingResult)
56field unrestricted reductionSM86EncodingFailureTelemetry : (family ReductionSM86Telemetry)
57constructor ReductionSM86SnippetIdentityFailed
58field unrestricted reductionSM86IdentityFailure : (family ReductionSM86FailureCode)
59field unrestricted reductionSM86FailedIdentity : (family SHA256HexResult)
60field unrestricted reductionSM86IdentityFailureTelemetry : (family ReductionSM86Telemetry)
61
62end-family
63
64def reductionSM86FailureCodeBytes =
65 (lambda unrestricted code : (family ReductionSM86FailureCode) .
66 (eliminate
67 ReductionSM86FailureCode
68 (lambda unrestricted current : (family ReductionSM86FailureCode) . Bytes)
69 code
70 (branch ReductionSM86WarpSum64InstructionCountMismatch . b"ALPHA-SM86-REDUCE-001")
71 (branch ReductionSM86WarpSum256InstructionCountMismatch . b"ALPHA-SM86-REDUCE-002")
72 (branch ReductionSM86WarpSum1024InstructionCountMismatch . b"ALPHA-SM86-REDUCE-003")
73 (branch ReductionSM86WarpMaximum256InstructionCountMismatch . b"ALPHA-SM86-REDUCE-004")
74 (branch ReductionSM86EncodingFailed . b"ALPHA-SM86-REDUCE-005")
75 (branch ReductionSM86IdentityFailed . b"ALPHA-SM86-REDUCE-006")
76 (branch ReductionSM86IdentityLengthInvalid . b"ALPHA-SM86-REDUCE-007")))
77
78def reductionSM86R0 =
79 (sm86Register (byte 0))
80
81def reductionSM86R1 =
82 (sm86Register (byte 1))
83
84def reductionSM86R2 =
85 (sm86Register (byte 2))
86
87def reductionSM86R3 =
88 (sm86Register (byte 3))
89
90def reductionSM86ThreadId =
91 reductionSM86R0
92
93def reductionSM86Accumulator =
94 reductionSM86R1
95
96def reductionSM86Scratch =
97 reductionSM86R2
98
99def reductionSM86Identity =
100 reductionSM86R3
101
102def reductionSM86P0 : (family SM86Predicate) =
103 (constructor SM86Predicate SM86Predicate0)
104
105def reductionSM86U0 =
106 sm86Unsigned32Zero
107
108def reductionSM86U1 =
109 sm86Unsigned32One
110
111def reductionSM86U7 =
112 (sm86Unsigned32 (byte 7) (byte 0) (byte 0) (byte 0))
113
114def reductionSM86U31 =
115 (sm86Unsigned32 (byte 31) (byte 0) (byte 0) (byte 0))
116
117def reductionSM86NegativeInfinity =
118 (sm86Unsigned32 (byte 0) (byte 0) (byte 128) (byte 255))
119
120def reductionSM86ShuffleSegment32 =
121 reductionSM86U31
122
123def reductionSM86ShuffleButterfly : (family SM86ShuffleMode) =
124 (constructor SM86ShuffleMode SM86ShuffleButterfly)
125
126def reductionSM86FloatMaximum : (family SM86FloatExtremum) =
127 (constructor SM86FloatExtremum SM86FloatMaximum)
128
129def reductionSM86Set2 =
130 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))
131
132def reductionSM86Set4 =
133 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier4))
134
135def reductionSM86Set5 =
136 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier5))
137
138def reductionSM86Wait4 =
139 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier4))
140
141def reductionSM86Wait5 =
142 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier5))
143
144def reductionSM86Read4 : (family SM86Control) =
145 (constructor
146 SM86Control
147 SM86ControlValue
148 (byte 7)
149 (constructor SM86YieldMode SM86Continue)
150 (constructor SM86Barrier SM86BarrierNone)
151 (constructor SM86Barrier SM86Barrier4)
152 (byte 0)
153 (byte 0))
154
155def reductionSM86Wait2Set4 : (family SM86Control) =
156 (constructor
157 SM86Control
158 SM86ControlValue
159 (byte 1)
160 (constructor SM86YieldMode SM86Continue)
161 (constructor SM86Barrier SM86Barrier4)
162 (constructor SM86Barrier SM86BarrierNone)
163 (byte 4)
164 (byte 0))
165
166def reductionSM86NotP0 =
167 (lambda unrestricted body : (family SM86InstructionBody) .
168 (sm86NegatedPredicatedInstruction reductionSM86P0 body))
169
170def reductionSM86InitialBarrierProgram : (family SM86Program) =
171 (sm86ProgramSingleton
172 (sm86Instruction (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl)))
173
174def reductionSM86SumButterflies =
175 (lambda unrestricted firstControl : (family SM86Control) .
176 (constructor
177 SM86Program
178 SM86ProgramNext
179 (sm86Instruction
180 (constructor
181 SM86InstructionBody
182 SM86WarpShuffle
183 reductionSM86Scratch
184 reductionSM86Accumulator
185 (byte 16)
186 reductionSM86ShuffleSegment32
187 reductionSM86ShuffleButterfly
188 firstControl))
189 (constructor
190 SM86Program
191 SM86ProgramNext
192 (sm86Instruction
193 (constructor
194 SM86InstructionBody
195 SM86FloatAdd
196 reductionSM86Accumulator
197 reductionSM86Accumulator
198 reductionSM86Scratch
199 reductionSM86Wait4))
200 (constructor
201 SM86Program
202 SM86ProgramNext
203 (sm86Instruction
204 (constructor
205 SM86InstructionBody
206 SM86WarpShuffle
207 reductionSM86Scratch
208 reductionSM86Accumulator
209 (byte 8)
210 reductionSM86ShuffleSegment32
211 reductionSM86ShuffleButterfly
212 reductionSM86Set5))
213 (constructor
214 SM86Program
215 SM86ProgramNext
216 (sm86Instruction
217 (constructor
218 SM86InstructionBody
219 SM86FloatAdd
220 reductionSM86Accumulator
221 reductionSM86Accumulator
222 reductionSM86Scratch
223 reductionSM86Wait5))
224 (constructor
225 SM86Program
226 SM86ProgramNext
227 (sm86Instruction
228 (constructor
229 SM86InstructionBody
230 SM86WarpShuffle
231 reductionSM86Scratch
232 reductionSM86Accumulator
233 (byte 4)
234 reductionSM86ShuffleSegment32
235 reductionSM86ShuffleButterfly
236 reductionSM86Set4))
237 (constructor
238 SM86Program
239 SM86ProgramNext
240 (sm86Instruction
241 (constructor
242 SM86InstructionBody
243 SM86FloatAdd
244 reductionSM86Accumulator
245 reductionSM86Accumulator
246 reductionSM86Scratch
247 reductionSM86Wait4))
248 (constructor
249 SM86Program
250 SM86ProgramNext
251 (sm86Instruction
252 (constructor
253 SM86InstructionBody
254 SM86WarpShuffle
255 reductionSM86Scratch
256 reductionSM86Accumulator
257 (byte 2)
258 reductionSM86ShuffleSegment32
259 reductionSM86ShuffleButterfly
260 reductionSM86Set5))
261 (constructor
262 SM86Program
263 SM86ProgramNext
264 (sm86Instruction
265 (constructor
266 SM86InstructionBody
267 SM86FloatAdd
268 reductionSM86Accumulator
269 reductionSM86Accumulator
270 reductionSM86Scratch
271 reductionSM86Wait5))
272 (constructor
273 SM86Program
274 SM86ProgramNext
275 (sm86Instruction
276 (constructor
277 SM86InstructionBody
278 SM86WarpShuffle
279 reductionSM86Scratch
280 reductionSM86Accumulator
281 (byte 1)
282 reductionSM86ShuffleSegment32
283 reductionSM86ShuffleButterfly
284 reductionSM86Set4))
285 (constructor
286 SM86Program
287 SM86ProgramNext
288 (sm86Instruction
289 (constructor
290 SM86InstructionBody
291 SM86FloatAdd
292 reductionSM86Accumulator
293 reductionSM86Accumulator
294 reductionSM86Scratch
295 reductionSM86Wait4))
296 (constructor SM86Program SM86ProgramEnd))))))))))))
297
298def reductionSM86MaximumButterflies =
299 (lambda unrestricted firstControl : (family SM86Control) .
300 (constructor
301 SM86Program
302 SM86ProgramNext
303 (sm86Instruction
304 (constructor
305 SM86InstructionBody
306 SM86WarpShuffle
307 reductionSM86Scratch
308 reductionSM86Accumulator
309 (byte 16)
310 reductionSM86ShuffleSegment32
311 reductionSM86ShuffleButterfly
312 firstControl))
313 (constructor
314 SM86Program
315 SM86ProgramNext
316 (sm86Instruction
317 (constructor
318 SM86InstructionBody
319 SM86FloatMinimumOrMaximum
320 reductionSM86Accumulator
321 reductionSM86Accumulator
322 reductionSM86Scratch
323 reductionSM86FloatMaximum
324 reductionSM86Wait4))
325 (constructor
326 SM86Program
327 SM86ProgramNext
328 (sm86Instruction
329 (constructor
330 SM86InstructionBody
331 SM86WarpShuffle
332 reductionSM86Scratch
333 reductionSM86Accumulator
334 (byte 8)
335 reductionSM86ShuffleSegment32
336 reductionSM86ShuffleButterfly
337 reductionSM86Set5))
338 (constructor
339 SM86Program
340 SM86ProgramNext
341 (sm86Instruction
342 (constructor
343 SM86InstructionBody
344 SM86FloatMinimumOrMaximum
345 reductionSM86Accumulator
346 reductionSM86Accumulator
347 reductionSM86Scratch
348 reductionSM86FloatMaximum
349 reductionSM86Wait5))
350 (constructor
351 SM86Program
352 SM86ProgramNext
353 (sm86Instruction
354 (constructor
355 SM86InstructionBody
356 SM86WarpShuffle
357 reductionSM86Scratch
358 reductionSM86Accumulator
359 (byte 4)
360 reductionSM86ShuffleSegment32
361 reductionSM86ShuffleButterfly
362 reductionSM86Set4))
363 (constructor
364 SM86Program
365 SM86ProgramNext
366 (sm86Instruction
367 (constructor
368 SM86InstructionBody
369 SM86FloatMinimumOrMaximum
370 reductionSM86Accumulator
371 reductionSM86Accumulator
372 reductionSM86Scratch
373 reductionSM86FloatMaximum
374 reductionSM86Wait4))
375 (constructor
376 SM86Program
377 SM86ProgramNext
378 (sm86Instruction
379 (constructor
380 SM86InstructionBody
381 SM86WarpShuffle
382 reductionSM86Scratch
383 reductionSM86Accumulator
384 (byte 2)
385 reductionSM86ShuffleSegment32
386 reductionSM86ShuffleButterfly
387 reductionSM86Set5))
388 (constructor
389 SM86Program
390 SM86ProgramNext
391 (sm86Instruction
392 (constructor
393 SM86InstructionBody
394 SM86FloatMinimumOrMaximum
395 reductionSM86Accumulator
396 reductionSM86Accumulator
397 reductionSM86Scratch
398 reductionSM86FloatMaximum
399 reductionSM86Wait5))
400 (constructor
401 SM86Program
402 SM86ProgramNext
403 (sm86Instruction
404 (constructor
405 SM86InstructionBody
406 SM86WarpShuffle
407 reductionSM86Scratch
408 reductionSM86Accumulator
409 (byte 1)
410 reductionSM86ShuffleSegment32
411 reductionSM86ShuffleButterfly
412 reductionSM86Set4))
413 (constructor
414 SM86Program
415 SM86ProgramNext
416 (sm86Instruction
417 (constructor
418 SM86InstructionBody
419 SM86FloatMinimumOrMaximum
420 reductionSM86Accumulator
421 reductionSM86Accumulator
422 reductionSM86Scratch
423 reductionSM86FloatMaximum
424 reductionSM86Wait4))
425 (constructor SM86Program SM86ProgramEnd))))))))))))
426
427def reductionSM86WarpSum64Middle : (family SM86Program) =
428 (constructor
429 SM86Program
430 SM86ProgramNext
431 (sm86Instruction
432 (constructor
433 SM86InstructionBody
434 SM86MoveImmediate
435 reductionSM86Scratch
436 reductionSM86U31
437 sm86SafeControl))
438 (constructor
439 SM86Program
440 SM86ProgramNext
441 (sm86Instruction
442 (constructor
443 SM86InstructionBody
444 SM86LogicThreeInputTruthTable
445 reductionSM86Scratch
446 reductionSM86ThreadId
447 reductionSM86Scratch
448 (byte 192)
449 sm86SafeControl))
450 (constructor
451 SM86Program
452 SM86ProgramNext
453 (sm86Instruction
454 (constructor
455 SM86InstructionBody
456 SM86PredicateGreaterThanImmediate
457 reductionSM86P0
458 reductionSM86Scratch
459 reductionSM86U0
460 sm86SafeControl))
461 (constructor
462 SM86Program
463 SM86ProgramNext
464 (sm86Instruction
465 (constructor
466 SM86InstructionBody
467 SM86ShiftRightImmediate
468 reductionSM86Scratch
469 reductionSM86ThreadId
470 (byte 5)
471 sm86SafeControl))
472 (constructor
473 SM86Program
474 SM86ProgramNext
475 (reductionSM86NotP0
476 (constructor
477 SM86InstructionBody
478 SM86StoreShared
479 reductionSM86Scratch
480 reductionSM86Accumulator
481 reductionSM86U0
482 reductionSM86Read4))
483 (constructor
484 SM86Program
485 SM86ProgramNext
486 (sm86Instruction
487 (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl))
488 (constructor
489 SM86Program
490 SM86ProgramNext
491 (sm86Instruction
492 (constructor
493 SM86InstructionBody
494 SM86MoveImmediate
495 reductionSM86Scratch
496 reductionSM86U31
497 reductionSM86Wait4))
498 (constructor
499 SM86Program
500 SM86ProgramNext
501 (sm86Instruction
502 (constructor
503 SM86InstructionBody
504 SM86LogicThreeInputTruthTable
505 reductionSM86Scratch
506 reductionSM86ThreadId
507 reductionSM86Scratch
508 (byte 192)
509 sm86SafeControl))
510 (constructor
511 SM86Program
512 SM86ProgramNext
513 (sm86Instruction
514 (constructor
515 SM86InstructionBody
516 SM86MoveImmediate
517 reductionSM86Accumulator
518 reductionSM86U0
519 sm86SafeControl))
520 (constructor
521 SM86Program
522 SM86ProgramNext
523 (sm86Instruction
524 (constructor
525 SM86InstructionBody
526 SM86PredicateGreaterThanImmediate
527 reductionSM86P0
528 reductionSM86Scratch
529 reductionSM86U1
530 sm86SafeControl))
531 (constructor
532 SM86Program
533 SM86ProgramNext
534 (reductionSM86NotP0
535 (constructor
536 SM86InstructionBody
537 SM86LoadShared
538 reductionSM86Accumulator
539 reductionSM86Scratch
540 reductionSM86U0
541 reductionSM86Set2))
542 (constructor SM86Program SM86ProgramEnd))))))))))))
543
544def reductionSM86WarpSum1024Middle : (family SM86Program) =
545 (constructor
546 SM86Program
547 SM86ProgramNext
548 (sm86Instruction
549 (constructor
550 SM86InstructionBody
551 SM86MoveImmediate
552 reductionSM86Scratch
553 reductionSM86U31
554 sm86SafeControl))
555 (constructor
556 SM86Program
557 SM86ProgramNext
558 (sm86Instruction
559 (constructor
560 SM86InstructionBody
561 SM86LogicThreeInputTruthTable
562 reductionSM86Scratch
563 reductionSM86ThreadId
564 reductionSM86Scratch
565 (byte 192)
566 sm86SafeControl))
567 (constructor
568 SM86Program
569 SM86ProgramNext
570 (sm86Instruction
571 (constructor
572 SM86InstructionBody
573 SM86PredicateGreaterThanImmediate
574 reductionSM86P0
575 reductionSM86Scratch
576 reductionSM86U0
577 sm86SafeControl))
578 (constructor
579 SM86Program
580 SM86ProgramNext
581 (sm86Instruction
582 (constructor
583 SM86InstructionBody
584 SM86ShiftRightImmediate
585 reductionSM86Scratch
586 reductionSM86ThreadId
587 (byte 5)
588 sm86SafeControl))
589 (constructor
590 SM86Program
591 SM86ProgramNext
592 (reductionSM86NotP0
593 (constructor
594 SM86InstructionBody
595 SM86StoreShared
596 reductionSM86Scratch
597 reductionSM86Accumulator
598 reductionSM86U0
599 reductionSM86Read4))
600 (constructor
601 SM86Program
602 SM86ProgramNext
603 (sm86Instruction
604 (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl))
605 (constructor
606 SM86Program
607 SM86ProgramNext
608 (sm86Instruction
609 (constructor
610 SM86InstructionBody
611 SM86MoveImmediate
612 reductionSM86Scratch
613 reductionSM86U31
614 reductionSM86Wait4))
615 (constructor
616 SM86Program
617 SM86ProgramNext
618 (sm86Instruction
619 (constructor
620 SM86InstructionBody
621 SM86LogicThreeInputTruthTable
622 reductionSM86Scratch
623 reductionSM86ThreadId
624 reductionSM86Scratch
625 (byte 192)
626 sm86SafeControl))
627 (constructor
628 SM86Program
629 SM86ProgramNext
630 (sm86Instruction
631 (constructor
632 SM86InstructionBody
633 SM86LoadShared
634 reductionSM86Accumulator
635 reductionSM86Scratch
636 reductionSM86U0
637 reductionSM86Set2))
638 (constructor SM86Program SM86ProgramEnd))))))))))
639
640def reductionSM86IdentityInitializedMiddle =
641 (lambda unrestricted identityValue : (family SM86Unsigned32) .
642 (constructor
643 SM86Program
644 SM86ProgramNext
645 (sm86Instruction
646 (constructor
647 SM86InstructionBody
648 SM86MoveImmediate
649 reductionSM86Scratch
650 reductionSM86U31
651 sm86SafeControl))
652 (constructor
653 SM86Program
654 SM86ProgramNext
655 (sm86Instruction
656 (constructor
657 SM86InstructionBody
658 SM86LogicThreeInputTruthTable
659 reductionSM86Scratch
660 reductionSM86ThreadId
661 reductionSM86Scratch
662 (byte 192)
663 sm86SafeControl))
664 (constructor
665 SM86Program
666 SM86ProgramNext
667 (sm86Instruction
668 (constructor
669 SM86InstructionBody
670 SM86MoveImmediate
671 reductionSM86Identity
672 identityValue
673 sm86SafeControl))
674 (constructor
675 SM86Program
676 SM86ProgramNext
677 (sm86Instruction
678 (constructor
679 SM86InstructionBody
680 SM86PredicateGreaterThanImmediate
681 reductionSM86P0
682 reductionSM86ThreadId
683 reductionSM86U31
684 sm86SafeControl))
685 (constructor
686 SM86Program
687 SM86ProgramNext
688 (reductionSM86NotP0
689 (constructor
690 SM86InstructionBody
691 SM86StoreShared
692 reductionSM86Scratch
693 reductionSM86Identity
694 reductionSM86U0
695 sm86SafeControl))
696 (constructor
697 SM86Program
698 SM86ProgramNext
699 (sm86Instruction
700 (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl))
701 (constructor
702 SM86Program
703 SM86ProgramNext
704 (sm86Instruction
705 (constructor
706 SM86InstructionBody
707 SM86PredicateGreaterThanImmediate
708 reductionSM86P0
709 reductionSM86Scratch
710 reductionSM86U0
711 sm86SafeControl))
712 (constructor
713 SM86Program
714 SM86ProgramNext
715 (sm86Instruction
716 (constructor
717 SM86InstructionBody
718 SM86ShiftRightImmediate
719 reductionSM86Identity
720 reductionSM86ThreadId
721 (byte 5)
722 sm86SafeControl))
723 (constructor
724 SM86Program
725 SM86ProgramNext
726 (reductionSM86NotP0
727 (constructor
728 SM86InstructionBody
729 SM86StoreShared
730 reductionSM86Identity
731 reductionSM86Accumulator
732 reductionSM86U0
733 reductionSM86Read4))
734 (constructor
735 SM86Program
736 SM86ProgramNext
737 (sm86Instruction
738 (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl))
739 (constructor
740 SM86Program
741 SM86ProgramNext
742 (sm86Instruction
743 (constructor
744 SM86InstructionBody
745 SM86MoveImmediate
746 reductionSM86Scratch
747 reductionSM86U31
748 reductionSM86Wait4))
749 (constructor
750 SM86Program
751 SM86ProgramNext
752 (sm86Instruction
753 (constructor
754 SM86InstructionBody
755 SM86LogicThreeInputTruthTable
756 reductionSM86Scratch
757 reductionSM86ThreadId
758 reductionSM86Scratch
759 (byte 192)
760 sm86SafeControl))
761 (constructor
762 SM86Program
763 SM86ProgramNext
764 (sm86Instruction
765 (constructor
766 SM86InstructionBody
767 SM86LoadShared
768 reductionSM86Accumulator
769 reductionSM86Scratch
770 reductionSM86U0
771 reductionSM86Set2))
772 (constructor SM86Program SM86ProgramEnd)))))))))))))))
773
774def reductionSM86WarpSum64Program : (family SM86Program) =
775 (sm86ProgramAppend
776 reductionSM86InitialBarrierProgram
777 (sm86ProgramAppend
778 (reductionSM86SumButterflies reductionSM86Set4)
779 (sm86ProgramAppend
780 reductionSM86WarpSum64Middle
781 (reductionSM86SumButterflies reductionSM86Wait2Set4))))
782
783def reductionSM86WarpSum256Program : (family SM86Program) =
784 (sm86ProgramAppend
785 reductionSM86InitialBarrierProgram
786 (sm86ProgramAppend
787 (reductionSM86SumButterflies reductionSM86Set4)
788 (sm86ProgramAppend
789 (reductionSM86IdentityInitializedMiddle reductionSM86U0)
790 (reductionSM86SumButterflies reductionSM86Wait2Set4))))
791
792def reductionSM86WarpSum1024Program : (family SM86Program) =
793 (sm86ProgramAppend
794 reductionSM86InitialBarrierProgram
795 (sm86ProgramAppend
796 (reductionSM86SumButterflies reductionSM86Set4)
797 (sm86ProgramAppend
798 reductionSM86WarpSum1024Middle
799 (reductionSM86SumButterflies reductionSM86Wait2Set4))))
800
801def reductionSM86WarpMaximum256Program : (family SM86Program) =
802 (sm86ProgramAppend
803 reductionSM86InitialBarrierProgram
804 (sm86ProgramAppend
805 (reductionSM86MaximumButterflies reductionSM86Set4)
806 (sm86ProgramAppend
807 (reductionSM86IdentityInitializedMiddle reductionSM86NegativeInfinity)
808 (reductionSM86MaximumButterflies reductionSM86Wait2Set4))))
809
810def reductionSM86WarpSum64ExpectedInstructions =
811 (byte-to-nat (byte 32))
812
813def reductionSM86WarpSum256ExpectedInstructions =
814 (byte-to-nat (byte 34))
815
816def reductionSM86WarpSum1024ExpectedInstructions =
817 (byte-to-nat (byte 30))
818
819def reductionSM86WarpMaximum256ExpectedInstructions =
820 (byte-to-nat (byte 34))
821
822def reductionSM86WarpSum64RegisterCount =
823 (byte-to-nat (byte 3))
824
825def reductionSM86WarpSum256RegisterCount =
826 (byte-to-nat (byte 4))
827
828def reductionSM86WarpSum1024RegisterCount =
829 (byte-to-nat (byte 3))
830
831def reductionSM86WarpMaximum256RegisterCount =
832 (byte-to-nat (byte 4))
833
834def reductionSM86SharedBytes =
835 (byte-to-nat (byte 128))
836
837def reductionSM86WarpSum64RequiredThreads =
838 (byte-to-nat (byte 64))
839
840def reductionSM86WarpSum256RequiredThreads =
841 (succ (byte-to-nat (byte 255)))
842
843def reductionSM86WarpSum1024RequiredThreads =
844 (naturalPowerOfTwo (byte-to-nat (byte 10)))
845
846def reductionSM86WarpMaximum256RequiredThreads =
847 reductionSM86WarpSum256RequiredThreads
848
849def reductionSM86WarpSum64Telemetry =
850 (lambda unrestricted observed : Nat .
851 (constructor
852 ReductionSM86Telemetry
853 ReductionSM86TelemetryValue
854 (constructor ReductionSM86Primitive ReductionSM86WarpSum64)
855 reductionSM86WarpSum64ExpectedInstructions
856 observed
857 reductionSM86WarpSum64RegisterCount
858 reductionSM86SharedBytes
859 reductionSM86WarpSum64RequiredThreads))
860
861def reductionSM86WarpSum256Telemetry =
862 (lambda unrestricted observed : Nat .
863 (constructor
864 ReductionSM86Telemetry
865 ReductionSM86TelemetryValue
866 (constructor ReductionSM86Primitive ReductionSM86WarpSum256)
867 reductionSM86WarpSum256ExpectedInstructions
868 observed
869 reductionSM86WarpSum256RegisterCount
870 reductionSM86SharedBytes
871 reductionSM86WarpSum256RequiredThreads))
872
873def reductionSM86WarpSum1024Telemetry =
874 (lambda unrestricted observed : Nat .
875 (constructor
876 ReductionSM86Telemetry
877 ReductionSM86TelemetryValue
878 (constructor ReductionSM86Primitive ReductionSM86WarpSum1024)
879 reductionSM86WarpSum1024ExpectedInstructions
880 observed
881 reductionSM86WarpSum1024RegisterCount
882 reductionSM86SharedBytes
883 reductionSM86WarpSum1024RequiredThreads))
884
885def reductionSM86WarpMaximum256Telemetry =
886 (lambda unrestricted observed : Nat .
887 (constructor
888 ReductionSM86Telemetry
889 ReductionSM86TelemetryValue
890 (constructor ReductionSM86Primitive ReductionSM86WarpMaximum256)
891 reductionSM86WarpMaximum256ExpectedInstructions
892 observed
893 reductionSM86WarpMaximum256RegisterCount
894 reductionSM86SharedBytes
895 reductionSM86WarpMaximum256RequiredThreads))
896
897def reductionSM86Build =
898 (lambda unrestricted program : (family SM86Program) .
899 (lambda unrestricted expected : Nat .
900 (lambda unrestricted mismatchCode : (family ReductionSM86FailureCode) .
901 (lambda unrestricted makeTelemetry : (pi unrestricted observed : Nat . (family ReductionSM86Telemetry)) .
902 (app
903 (lambda unrestricted observed : Nat .
904 (app
905 (lambda unrestricted telemetry : (family ReductionSM86Telemetry) .
906 (nat-eliminate
907 (lambda unrestricted countMatched : Nat . (family ReductionSM86BuildResult))
908 (constructor
909 ReductionSM86BuildResult
910 ReductionSM86ContractFailed
911 mismatchCode
912 telemetry)
913 (lambda unrestricted matchedPredecessor : Nat .
914 (lambda unrestricted matchedInduction : (family ReductionSM86BuildResult) .
915 (app
916 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
917 (eliminate
918 SM86ProgramEncodingResult
919 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
920 (family ReductionSM86BuildResult))
921 encoding
922 (branch
923 SM86ProgramEncodingSucceeded
924 bytes
925 encodingTelemetry
926 .
927 (app
928 (lambda unrestricted identityResult : (family SHA256HexResult) .
929 (eliminate
930 SHA256HexResult
931 (lambda unrestricted current : (family SHA256HexResult) .
932 (family ReductionSM86BuildResult))
933 identityResult
934 (branch
935 SHA256HexSucceeded
936 identity
937 identityTelemetry
938 .
939 (nat-eliminate
940 (lambda unrestricted validIdentityLength : Nat .
941 (family ReductionSM86BuildResult))
942 (constructor
943 ReductionSM86BuildResult
944 ReductionSM86SnippetIdentityFailed
945 (constructor
946 ReductionSM86FailureCode
947 ReductionSM86IdentityLengthInvalid)
948 identityResult
949 telemetry)
950 (lambda unrestricted identityLengthPredecessor : Nat .
951 (lambda unrestricted identityLengthInduction : (family ReductionSM86BuildResult) .
952 (constructor
953 ReductionSM86BuildResult
954 ReductionSM86BuildSucceeded
955 bytes
956 identity
957 encodingTelemetry
958 identityTelemetry
959 telemetry)))
960 (naturalEqual
961 (bytes-length identity)
962 (byte-to-nat (byte 64)))))
963 (branch
964 SHA256HexFailed
965 error
966 ordinal
967 identityTelemetry
968 .
969 (constructor
970 ReductionSM86BuildResult
971 ReductionSM86SnippetIdentityFailed
972 (constructor
973 ReductionSM86FailureCode
974 ReductionSM86IdentityFailed)
975 identityResult
976 telemetry))))
977 (sha256Hex bytes)))
978 (branch
979 SM86ProgramEncodingFailed
980 instructionIndex
981 failure
982 encodingTelemetry
983 .
984 (constructor
985 ReductionSM86BuildResult
986 ReductionSM86SnippetEncodingFailed
987 (constructor ReductionSM86FailureCode ReductionSM86EncodingFailed)
988 encoding
989 telemetry))))
990 (sm86EncodeProgram program))))
991 (naturalEqual observed expected)))
992 (makeTelemetry observed)))
993 (sm86ProgramCount program))))))
994
995def reductionSM86BuildWarpSum64 : (family ReductionSM86BuildResult) =
996 (reductionSM86Build
997 reductionSM86WarpSum64Program
998 reductionSM86WarpSum64ExpectedInstructions
999 (constructor ReductionSM86FailureCode ReductionSM86WarpSum64InstructionCountMismatch)
1000 reductionSM86WarpSum64Telemetry)
1001
1002def reductionSM86BuildWarpSum256 : (family ReductionSM86BuildResult) =
1003 (reductionSM86Build
1004 reductionSM86WarpSum256Program
1005 reductionSM86WarpSum256ExpectedInstructions
1006 (constructor ReductionSM86FailureCode ReductionSM86WarpSum256InstructionCountMismatch)
1007 reductionSM86WarpSum256Telemetry)
1008
1009def reductionSM86BuildWarpSum1024 : (family ReductionSM86BuildResult) =
1010 (reductionSM86Build
1011 reductionSM86WarpSum1024Program
1012 reductionSM86WarpSum1024ExpectedInstructions
1013 (constructor ReductionSM86FailureCode ReductionSM86WarpSum1024InstructionCountMismatch)
1014 reductionSM86WarpSum1024Telemetry)
1015
1016def reductionSM86BuildWarpMaximum256 : (family ReductionSM86BuildResult) =
1017 (reductionSM86Build
1018 reductionSM86WarpMaximum256Program
1019 reductionSM86WarpMaximum256ExpectedInstructions
1020 (constructor ReductionSM86FailureCode ReductionSM86WarpMaximum256InstructionCountMismatch)
1021 reductionSM86WarpMaximum256Telemetry)
1022
1023def reductionSM86SumCombine =
1024 (lambda unrestricted destination : (family SM86Register) .
1025 (lambda unrestricted left : (family SM86Register) .
1026 (lambda unrestricted right : (family SM86Register) .
1027 (lambda unrestricted control : (family SM86Control) .
1028 (constructor SM86InstructionBody SM86FloatAdd destination left right control)))))
1029
1030def reductionSM86MaximumCombine =
1031 (lambda unrestricted destination : (family SM86Register) .
1032 (lambda unrestricted left : (family SM86Register) .
1033 (lambda unrestricted right : (family SM86Register) .
1034 (lambda unrestricted control : (family SM86Control) .
1035 (constructor
1036 SM86InstructionBody
1037 SM86FloatMinimumOrMaximum
1038 destination
1039 left
1040 right
1041 reductionSM86FloatMaximum
1042 control)))))
1043
1044def reductionSM86ParameterizedButterflies =
1045 (lambda unrestricted combine : (pi unrestricted destination : (family SM86Register) . (pi unrestricted left : (family SM86Register) . (pi unrestricted right : (family SM86Register) . (pi unrestricted control : (family SM86Control) . (family SM86InstructionBody))))) .
1046 (lambda unrestricted accumulator : (family SM86Register) .
1047 (lambda unrestricted scratch : (family SM86Register) .
1048 (lambda unrestricted firstControl : (family SM86Control) .
1049 (constructor
1050 SM86Program
1051 SM86ProgramNext
1052 (sm86Instruction
1053 (constructor
1054 SM86InstructionBody
1055 SM86WarpShuffle
1056 scratch
1057 accumulator
1058 (byte 16)
1059 reductionSM86ShuffleSegment32
1060 reductionSM86ShuffleButterfly
1061 firstControl))
1062 (constructor
1063 SM86Program
1064 SM86ProgramNext
1065 (sm86Instruction (combine accumulator accumulator scratch reductionSM86Wait4))
1066 (constructor
1067 SM86Program
1068 SM86ProgramNext
1069 (sm86Instruction
1070 (constructor
1071 SM86InstructionBody
1072 SM86WarpShuffle
1073 scratch
1074 accumulator
1075 (byte 8)
1076 reductionSM86ShuffleSegment32
1077 reductionSM86ShuffleButterfly
1078 reductionSM86Set5))
1079 (constructor
1080 SM86Program
1081 SM86ProgramNext
1082 (sm86Instruction (combine accumulator accumulator scratch reductionSM86Wait5))
1083 (constructor
1084 SM86Program
1085 SM86ProgramNext
1086 (sm86Instruction
1087 (constructor
1088 SM86InstructionBody
1089 SM86WarpShuffle
1090 scratch
1091 accumulator
1092 (byte 4)
1093 reductionSM86ShuffleSegment32
1094 reductionSM86ShuffleButterfly
1095 reductionSM86Set4))
1096 (constructor
1097 SM86Program
1098 SM86ProgramNext
1099 (sm86Instruction (combine accumulator accumulator scratch reductionSM86Wait4))
1100 (constructor
1101 SM86Program
1102 SM86ProgramNext
1103 (sm86Instruction
1104 (constructor
1105 SM86InstructionBody
1106 SM86WarpShuffle
1107 scratch
1108 accumulator
1109 (byte 2)
1110 reductionSM86ShuffleSegment32
1111 reductionSM86ShuffleButterfly
1112 reductionSM86Set5))
1113 (constructor
1114 SM86Program
1115 SM86ProgramNext
1116 (sm86Instruction
1117 (combine accumulator accumulator scratch reductionSM86Wait5))
1118 (constructor
1119 SM86Program
1120 SM86ProgramNext
1121 (sm86Instruction
1122 (constructor
1123 SM86InstructionBody
1124 SM86WarpShuffle
1125 scratch
1126 accumulator
1127 (byte 1)
1128 reductionSM86ShuffleSegment32
1129 reductionSM86ShuffleButterfly
1130 reductionSM86Set4))
1131 (constructor
1132 SM86Program
1133 SM86ProgramNext
1134 (sm86Instruction
1135 (combine accumulator accumulator scratch reductionSM86Wait4))
1136 (constructor SM86Program SM86ProgramEnd)))))))))))))))
1137
1138def reductionSM86ParameterizedLegacyMiddle =
1139 (lambda unrestricted thread : (family SM86Register) .
1140 (lambda unrestricted accumulator : (family SM86Register) .
1141 (lambda unrestricted scratch : (family SM86Register) .
1142 (lambda unrestricted warpCountMinusOne : (family SM86Unsigned32) .
1143 (constructor
1144 SM86Program
1145 SM86ProgramNext
1146 (sm86Instruction
1147 (constructor
1148 SM86InstructionBody
1149 SM86MoveImmediate
1150 scratch
1151 reductionSM86U31
1152 sm86SafeControl))
1153 (constructor
1154 SM86Program
1155 SM86ProgramNext
1156 (sm86Instruction
1157 (constructor
1158 SM86InstructionBody
1159 SM86LogicThreeInputTruthTable
1160 scratch
1161 thread
1162 scratch
1163 (byte 192)
1164 sm86SafeControl))
1165 (constructor
1166 SM86Program
1167 SM86ProgramNext
1168 (sm86Instruction
1169 (constructor
1170 SM86InstructionBody
1171 SM86PredicateGreaterThanImmediate
1172 reductionSM86P0
1173 scratch
1174 reductionSM86U0
1175 sm86SafeControl))
1176 (constructor
1177 SM86Program
1178 SM86ProgramNext
1179 (sm86Instruction
1180 (constructor
1181 SM86InstructionBody
1182 SM86ShiftRightImmediate
1183 scratch
1184 thread
1185 (byte 5)
1186 sm86SafeControl))
1187 (constructor
1188 SM86Program
1189 SM86ProgramNext
1190 (reductionSM86NotP0
1191 (constructor
1192 SM86InstructionBody
1193 SM86StoreShared
1194 scratch
1195 accumulator
1196 reductionSM86U0
1197 reductionSM86Read4))
1198 (constructor
1199 SM86Program
1200 SM86ProgramNext
1201 (sm86Instruction
1202 (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl))
1203 (constructor
1204 SM86Program
1205 SM86ProgramNext
1206 (sm86Instruction
1207 (constructor
1208 SM86InstructionBody
1209 SM86MoveImmediate
1210 scratch
1211 reductionSM86U31
1212 reductionSM86Wait4))
1213 (constructor
1214 SM86Program
1215 SM86ProgramNext
1216 (sm86Instruction
1217 (constructor
1218 SM86InstructionBody
1219 SM86LogicThreeInputTruthTable
1220 scratch
1221 thread
1222 scratch
1223 (byte 192)
1224 sm86SafeControl))
1225 (constructor
1226 SM86Program
1227 SM86ProgramNext
1228 (sm86Instruction
1229 (constructor
1230 SM86InstructionBody
1231 SM86MoveImmediate
1232 accumulator
1233 reductionSM86U0
1234 sm86SafeControl))
1235 (constructor
1236 SM86Program
1237 SM86ProgramNext
1238 (sm86Instruction
1239 (constructor
1240 SM86InstructionBody
1241 SM86PredicateGreaterThanImmediate
1242 reductionSM86P0
1243 scratch
1244 warpCountMinusOne
1245 sm86SafeControl))
1246 (constructor
1247 SM86Program
1248 SM86ProgramNext
1249 (reductionSM86NotP0
1250 (constructor
1251 SM86InstructionBody
1252 SM86LoadShared
1253 accumulator
1254 scratch
1255 reductionSM86U0
1256 reductionSM86Set2))
1257 (constructor SM86Program SM86ProgramEnd))))))))))))))))
1258
1259def reductionSM86ParameterizedLegacyWarpSum =
1260 (lambda unrestricted thread : (family SM86Register) .
1261 (lambda unrestricted accumulator : (family SM86Register) .
1262 (lambda unrestricted scratch : (family SM86Register) .
1263 (lambda unrestricted warpCountMinusOne : (family SM86Unsigned32) .
1264 (sm86ProgramAppend
1265 reductionSM86InitialBarrierProgram
1266 (sm86ProgramAppend
1267 (reductionSM86ParameterizedButterflies
1268 reductionSM86SumCombine
1269 accumulator
1270 scratch
1271 reductionSM86Set4)
1272 (sm86ProgramAppend
1273 (reductionSM86ParameterizedLegacyMiddle
1274 thread
1275 accumulator
1276 scratch
1277 warpCountMinusOne)
1278 (reductionSM86ParameterizedButterflies
1279 reductionSM86SumCombine
1280 accumulator
1281 scratch
1282 reductionSM86Wait2Set4))))))))
1283
1284def reductionSM86Parameterized1024Middle =
1285 (lambda unrestricted thread : (family SM86Register) .
1286 (lambda unrestricted accumulator : (family SM86Register) .
1287 (lambda unrestricted scratch : (family SM86Register) .
1288 (constructor
1289 SM86Program
1290 SM86ProgramNext
1291 (sm86Instruction
1292 (constructor
1293 SM86InstructionBody
1294 SM86MoveImmediate
1295 scratch
1296 reductionSM86U31
1297 sm86SafeControl))
1298 (constructor
1299 SM86Program
1300 SM86ProgramNext
1301 (sm86Instruction
1302 (constructor
1303 SM86InstructionBody
1304 SM86LogicThreeInputTruthTable
1305 scratch
1306 thread
1307 scratch
1308 (byte 192)
1309 sm86SafeControl))
1310 (constructor
1311 SM86Program
1312 SM86ProgramNext
1313 (sm86Instruction
1314 (constructor
1315 SM86InstructionBody
1316 SM86PredicateGreaterThanImmediate
1317 reductionSM86P0
1318 scratch
1319 reductionSM86U0
1320 sm86SafeControl))
1321 (constructor
1322 SM86Program
1323 SM86ProgramNext
1324 (sm86Instruction
1325 (constructor
1326 SM86InstructionBody
1327 SM86ShiftRightImmediate
1328 scratch
1329 thread
1330 (byte 5)
1331 sm86SafeControl))
1332 (constructor
1333 SM86Program
1334 SM86ProgramNext
1335 (reductionSM86NotP0
1336 (constructor
1337 SM86InstructionBody
1338 SM86StoreShared
1339 scratch
1340 accumulator
1341 reductionSM86U0
1342 reductionSM86Read4))
1343 (constructor
1344 SM86Program
1345 SM86ProgramNext
1346 (sm86Instruction
1347 (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl))
1348 (constructor
1349 SM86Program
1350 SM86ProgramNext
1351 (sm86Instruction
1352 (constructor
1353 SM86InstructionBody
1354 SM86MoveImmediate
1355 scratch
1356 reductionSM86U31
1357 reductionSM86Wait4))
1358 (constructor
1359 SM86Program
1360 SM86ProgramNext
1361 (sm86Instruction
1362 (constructor
1363 SM86InstructionBody
1364 SM86LogicThreeInputTruthTable
1365 scratch
1366 thread
1367 scratch
1368 (byte 192)
1369 sm86SafeControl))
1370 (constructor
1371 SM86Program
1372 SM86ProgramNext
1373 (sm86Instruction
1374 (constructor
1375 SM86InstructionBody
1376 SM86LoadShared
1377 accumulator
1378 scratch
1379 reductionSM86U0
1380 reductionSM86Set2))
1381 (constructor SM86Program SM86ProgramEnd)))))))))))))
1382
1383def reductionSM86ParameterizedWarpSum1024 =
1384 (lambda unrestricted thread : (family SM86Register) .
1385 (lambda unrestricted accumulator : (family SM86Register) .
1386 (lambda unrestricted scratch : (family SM86Register) .
1387 (sm86ProgramAppend
1388 reductionSM86InitialBarrierProgram
1389 (sm86ProgramAppend
1390 (reductionSM86ParameterizedButterflies
1391 reductionSM86SumCombine
1392 accumulator
1393 scratch
1394 reductionSM86Set4)
1395 (sm86ProgramAppend
1396 (reductionSM86Parameterized1024Middle thread accumulator scratch)
1397 (reductionSM86ParameterizedButterflies
1398 reductionSM86SumCombine
1399 accumulator
1400 scratch
1401 reductionSM86Wait2Set4)))))))
1402
1403def reductionSM86ParameterizedIdentityMiddle =
1404 (lambda unrestricted thread : (family SM86Register) .
1405 (lambda unrestricted accumulator : (family SM86Register) .
1406 (lambda unrestricted scratch : (family SM86Register) .
1407 (lambda unrestricted identity : (family SM86Register) .
1408 (lambda unrestricted identityBits : (family SM86Unsigned32) .
1409 (constructor
1410 SM86Program
1411 SM86ProgramNext
1412 (sm86Instruction
1413 (constructor
1414 SM86InstructionBody
1415 SM86MoveImmediate
1416 scratch
1417 reductionSM86U31
1418 sm86SafeControl))
1419 (constructor
1420 SM86Program
1421 SM86ProgramNext
1422 (sm86Instruction
1423 (constructor
1424 SM86InstructionBody
1425 SM86LogicThreeInputTruthTable
1426 scratch
1427 thread
1428 scratch
1429 (byte 192)
1430 sm86SafeControl))
1431 (constructor
1432 SM86Program
1433 SM86ProgramNext
1434 (sm86Instruction
1435 (constructor
1436 SM86InstructionBody
1437 SM86MoveImmediate
1438 identity
1439 identityBits
1440 sm86SafeControl))
1441 (constructor
1442 SM86Program
1443 SM86ProgramNext
1444 (sm86Instruction
1445 (constructor
1446 SM86InstructionBody
1447 SM86PredicateGreaterThanImmediate
1448 reductionSM86P0
1449 thread
1450 reductionSM86U31
1451 sm86SafeControl))
1452 (constructor
1453 SM86Program
1454 SM86ProgramNext
1455 (reductionSM86NotP0
1456 (constructor
1457 SM86InstructionBody
1458 SM86StoreShared
1459 scratch
1460 identity
1461 reductionSM86U0
1462 sm86SafeControl))
1463 (constructor
1464 SM86Program
1465 SM86ProgramNext
1466 (sm86Instruction
1467 (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl))
1468 (constructor
1469 SM86Program
1470 SM86ProgramNext
1471 (sm86Instruction
1472 (constructor
1473 SM86InstructionBody
1474 SM86PredicateGreaterThanImmediate
1475 reductionSM86P0
1476 scratch
1477 reductionSM86U0
1478 sm86SafeControl))
1479 (constructor
1480 SM86Program
1481 SM86ProgramNext
1482 (sm86Instruction
1483 (constructor
1484 SM86InstructionBody
1485 SM86ShiftRightImmediate
1486 identity
1487 thread
1488 (byte 5)
1489 sm86SafeControl))
1490 (constructor
1491 SM86Program
1492 SM86ProgramNext
1493 (reductionSM86NotP0
1494 (constructor
1495 SM86InstructionBody
1496 SM86StoreShared
1497 identity
1498 accumulator
1499 reductionSM86U0
1500 reductionSM86Read4))
1501 (constructor
1502 SM86Program
1503 SM86ProgramNext
1504 (sm86Instruction
1505 (constructor
1506 SM86InstructionBody
1507 SM86BarrierSynchronize
1508 sm86SafeControl))
1509 (constructor
1510 SM86Program
1511 SM86ProgramNext
1512 (sm86Instruction
1513 (constructor
1514 SM86InstructionBody
1515 SM86MoveImmediate
1516 scratch
1517 reductionSM86U31
1518 reductionSM86Wait4))
1519 (constructor
1520 SM86Program
1521 SM86ProgramNext
1522 (sm86Instruction
1523 (constructor
1524 SM86InstructionBody
1525 SM86LogicThreeInputTruthTable
1526 scratch
1527 thread
1528 scratch
1529 (byte 192)
1530 sm86SafeControl))
1531 (constructor
1532 SM86Program
1533 SM86ProgramNext
1534 (sm86Instruction
1535 (constructor
1536 SM86InstructionBody
1537 SM86LoadShared
1538 accumulator
1539 scratch
1540 reductionSM86U0
1541 reductionSM86Set2))
1542 (constructor SM86Program SM86ProgramEnd)))))))))))))))))))
1543
1544def reductionSM86ParameterizedIdentityReduction =
1545 (lambda unrestricted combine : (pi unrestricted destination : (family SM86Register) . (pi unrestricted left : (family SM86Register) . (pi unrestricted right : (family SM86Register) . (pi unrestricted control : (family SM86Control) . (family SM86InstructionBody))))) .
1546 (lambda unrestricted thread : (family SM86Register) .
1547 (lambda unrestricted accumulator : (family SM86Register) .
1548 (lambda unrestricted scratch : (family SM86Register) .
1549 (lambda unrestricted identity : (family SM86Register) .
1550 (lambda unrestricted identityBits : (family SM86Unsigned32) .
1551 (sm86ProgramAppend
1552 reductionSM86InitialBarrierProgram
1553 (sm86ProgramAppend
1554 (reductionSM86ParameterizedButterflies
1555 combine
1556 accumulator
1557 scratch
1558 reductionSM86Set4)
1559 (sm86ProgramAppend
1560 (reductionSM86ParameterizedIdentityMiddle
1561 thread
1562 accumulator
1563 scratch
1564 identity
1565 identityBits)
1566 (reductionSM86ParameterizedButterflies
1567 combine
1568 accumulator
1569 scratch
1570 reductionSM86Wait2Set4))))))))))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.