1module Realization.Nvidia.SM86.GELUSM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.NumericSemantics
8import Accelerator.SM86.Program
9import Accelerator.SM86.Types
10import Data.SHA256Digest
11import Std.Natural
12import Std.Byte
13
14family GELUSM86ProgramKind : Type 0
15constructor GELUSM86Forward
16constructor GELUSM86Backward
17
18end-family
19
20family GELUSM86ScalarKind : Type 0
21constructor GELUSM86ScaleScalar
22constructor GELUSM86CubicScalar
23constructor GELUSM86HalfScalar
24constructor GELUSM86OneScalar
25constructor GELUSM86ThreeCubicScalar
26
27end-family
28
29family GELUSM86ScalarBinding : Type 0
30constructor GELUSM86ScalarBindingValue
31field unrestricted geluSM86ScalarKind : (family GELUSM86ScalarKind)
32field unrestricted geluSM86ScalarOffset : (family SM86Unsigned32)
33
34end-family
35
36family GELUSM86ScalarBindings : Type 0
37constructor GELUSM86ScalarBindingsEnd
38constructor GELUSM86ScalarBindingsNext
39field unrestricted geluSM86ScalarBindingHead : (family GELUSM86ScalarBinding)
40recursive unrestricted geluSM86ScalarBindingTail
41
42end-family
43
44family GELUSM86FailureCode : Type 0
45constructor GELUSM86ElementCountZero
46constructor GELUSM86ElementCountMisaligned
47constructor GELUSM86InstructionCountMismatch
48constructor GELUSM86EncodingFailed
49constructor GELUSM86IdentityInvalid
50
51end-family
52
53family GELUSM86Telemetry : Type 0
54constructor GELUSM86TelemetryValue
55field unrestricted geluSM86TelemetryKind : (family GELUSM86ProgramKind)
56field unrestricted geluSM86TelemetryExpectedInstructions : Nat
57field unrestricted geluSM86TelemetryActualInstructions : Nat
58field unrestricted geluSM86TelemetryRegisters : Nat
59field unrestricted geluSM86TelemetryElements : Nat
60field unrestricted geluSM86TelemetryGridX : Nat
61field unrestricted geluSM86TelemetryBlockX : Nat
62field unrestricted geluSM86TelemetryScalarBindings : Nat
63field unrestricted geluSM86TelemetryHostOperations : Nat
64field unrestricted geluSM86TelemetryEncodedBytes : Nat
65field unrestricted geluSM86TelemetryEncodedFields : Nat
66field unrestricted geluSM86TelemetryEncodedBits : Nat
67constructor GELUSM86TelemetryRejected
68field unrestricted geluSM86TelemetryFailure : (family GELUSM86FailureCode)
69field unrestricted geluSM86TelemetryFailureOrdinal : Nat
70
71end-family
72
73family GELUSM86Plan : Type 0
74constructor GELUSM86PlanValue
75field unrestricted geluSM86PlanKind : (family GELUSM86ProgramKind)
76field unrestricted geluSM86PlanElements : Nat
77field unrestricted geluSM86PlanProgram : (family SM86Program)
78field unrestricted geluSM86PlanScalars : (family GELUSM86ScalarBindings)
79field unrestricted geluSM86PlanTelemetry : (family GELUSM86Telemetry)
80
81end-family
82
83family GELUSM86PlanResult : Type 0
84constructor GELUSM86PlanReady
85field unrestricted geluSM86ReadyPlan : (family GELUSM86Plan)
86constructor GELUSM86PlanFailed
87field unrestricted geluSM86PlanFailure : (family GELUSM86FailureCode)
88field unrestricted geluSM86PlanFailureTelemetry : (family GELUSM86Telemetry)
89
90end-family
91
92family GELUSM86ImageResult : Type 0
93constructor GELUSM86ImageReady
94field unrestricted geluSM86ImageKind : (family GELUSM86ProgramKind)
95field unrestricted geluSM86ImageBytes : Bytes
96field unrestricted geluSM86ImageSHA256 : Bytes
97field unrestricted geluSM86ImageTelemetry : (family GELUSM86Telemetry)
98constructor GELUSM86ImageFailed
99field unrestricted geluSM86ImageFailure : (family GELUSM86FailureCode)
100field unrestricted geluSM86ImageFailureInstruction : Nat
101field unrestricted geluSM86ImageFailureDetail : Bytes
102field unrestricted geluSM86ImageFailureTelemetry : (family GELUSM86Telemetry)
103
104end-family
105
106def geluSM86NaturalFive =
107 (byte-to-nat (byte 5))
108
109def geluSM86NaturalTwentyTwo =
110 (byte-to-nat (byte 22))
111
112def geluSM86NaturalTwentyFour =
113 (byte-to-nat (byte 24))
114
115def geluSM86NaturalThirtyTwo =
116 (byte-to-nat (byte 32))
117
118def geluSM86NaturalThirtyFour =
119 (byte-to-nat (byte 34))
120
121def geluSM86BlockX =
122 byteNaturalTwoHundredFiftySix
123
124def geluSM86Unsigned32 =
125 (lambda unrestricted b0 : Byte .
126 (lambda unrestricted b1 : Byte .
127 (lambda unrestricted b2 : Byte .
128 (lambda unrestricted b3 : Byte . (sm86Unsigned32 b0 b1 b2 b3)))))
129
130def geluSM86ImmediateZero =
131 (geluSM86Unsigned32 (byte 0) (byte 0) (byte 0) (byte 0))
132
133def geluSM86ImmediateFour =
134 (geluSM86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))
135
136def geluSM86ImmediateTwoHundredFiftySix =
137 (geluSM86Unsigned32 (byte 0) (byte 1) (byte 0) (byte 0))
138
139def geluSM86ConstantBase =
140 (geluSM86Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0))
141
142def geluSM86OutputPointer =
143 (geluSM86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))
144
145def geluSM86InputPointer =
146 (geluSM86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))
147
148def geluSM86UpstreamPointer =
149 (geluSM86Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0))
150
151def geluSM86ScaleOffset =
152 (geluSM86Unsigned32 (byte 144) (byte 1) (byte 0) (byte 0))
153
154def geluSM86CubicOffset =
155 (geluSM86Unsigned32 (byte 148) (byte 1) (byte 0) (byte 0))
156
157def geluSM86HalfOffset =
158 (geluSM86Unsigned32 (byte 152) (byte 1) (byte 0) (byte 0))
159
160def geluSM86OneOffset =
161 (geluSM86Unsigned32 (byte 156) (byte 1) (byte 0) (byte 0))
162
163def geluSM86ThreeCubicOffset =
164 (geluSM86Unsigned32 (byte 160) (byte 1) (byte 0) (byte 0))
165
166def geluSM86ScalarBindings : (family GELUSM86ScalarBindings) =
167 (constructor
168 GELUSM86ScalarBindings
169 GELUSM86ScalarBindingsNext
170 (constructor
171 GELUSM86ScalarBinding
172 GELUSM86ScalarBindingValue
173 (constructor GELUSM86ScalarKind GELUSM86ScaleScalar)
174 geluSM86ScaleOffset)
175 (constructor
176 GELUSM86ScalarBindings
177 GELUSM86ScalarBindingsNext
178 (constructor
179 GELUSM86ScalarBinding
180 GELUSM86ScalarBindingValue
181 (constructor GELUSM86ScalarKind GELUSM86CubicScalar)
182 geluSM86CubicOffset)
183 (constructor
184 GELUSM86ScalarBindings
185 GELUSM86ScalarBindingsNext
186 (constructor
187 GELUSM86ScalarBinding
188 GELUSM86ScalarBindingValue
189 (constructor GELUSM86ScalarKind GELUSM86HalfScalar)
190 geluSM86HalfOffset)
191 (constructor
192 GELUSM86ScalarBindings
193 GELUSM86ScalarBindingsNext
194 (constructor
195 GELUSM86ScalarBinding
196 GELUSM86ScalarBindingValue
197 (constructor GELUSM86ScalarKind GELUSM86OneScalar)
198 geluSM86OneOffset)
199 (constructor
200 GELUSM86ScalarBindings
201 GELUSM86ScalarBindingsNext
202 (constructor
203 GELUSM86ScalarBinding
204 GELUSM86ScalarBindingValue
205 (constructor GELUSM86ScalarKind GELUSM86ThreeCubicScalar)
206 geluSM86ThreeCubicOffset)
207 (constructor GELUSM86ScalarBindings GELUSM86ScalarBindingsEnd))))))
208
209def geluSM86Register =
210 (lambda unrestricted value : Byte . (sm86Register value))
211
212def geluSM86Instruction =
213 (lambda unrestricted body : (family SM86InstructionBody) .
214 (constructor
215 SM86Instruction
216 SM86InstructionValue
217 (constructor SM86InstructionGuard SM86InstructionAlways)
218 body))
219
220def geluSM86Next =
221 (lambda unrestricted body : (family SM86InstructionBody) .
222 (lambda unrestricted tail : (family SM86Program) .
223 (constructor SM86Program SM86ProgramNext (geluSM86Instruction body) tail)))
224
225def geluSM86End =
226 (constructor SM86Program SM86ProgramEnd)
227
228def geluSM86SetBarrier0 =
229 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
230
231def geluSM86SetBarrier1 =
232 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))
233
234def geluSM86SetBarrier2 =
235 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))
236
237def geluSM86SetBarrier3 =
238 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3))
239
240def geluSM86SetBarrier4 =
241 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier4))
242
243def geluSM86WaitBarrier3 =
244 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier3))
245
246def geluSM86WaitBarrier4 =
247 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier4))
248
249def geluSM86WaitSpecials : (family SM86Control) =
250 (constructor
251 SM86Control
252 SM86ControlValue
253 (byte 7)
254 (constructor SM86YieldMode SM86Continue)
255 (constructor SM86Barrier SM86BarrierNone)
256 (constructor SM86Barrier SM86BarrierNone)
257 (byte 3)
258 (byte 0))
259
260def geluSM86WaitInputs : (family SM86Control) =
261 (constructor
262 SM86Control
263 SM86ControlValue
264 (byte 7)
265 (constructor SM86YieldMode SM86Continue)
266 (constructor SM86Barrier SM86BarrierNone)
267 (constructor SM86Barrier SM86BarrierNone)
268 (byte 12)
269 (byte 0))
270
271def geluSM86ForwardProgram : (family SM86Program) =
272 (geluSM86Next
273 (constructor
274 SM86InstructionBody
275 SM86MoveConstant
276 (geluSM86Register (byte 1))
277 (byte 0)
278 geluSM86ConstantBase
279 sm86SafeControl)
280 (geluSM86Next
281 (constructor
282 SM86InstructionBody
283 SM86SpecialToRegister
284 (geluSM86Register (byte 0))
285 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
286 geluSM86SetBarrier0)
287 (geluSM86Next
288 (constructor
289 SM86InstructionBody
290 SM86SpecialToRegister
291 (geluSM86Register (byte 2))
292 (constructor SM86SpecialRegister SM86ThreadIdX)
293 geluSM86SetBarrier1)
294 (geluSM86Next
295 (constructor
296 SM86InstructionBody
297 SM86IntegerMultiplyAddImmediate
298 (geluSM86Register (byte 3))
299 (geluSM86Register (byte 0))
300 geluSM86ImmediateTwoHundredFiftySix
301 (geluSM86Register (byte 2))
302 geluSM86WaitSpecials)
303 (geluSM86Next
304 (constructor
305 SM86InstructionBody
306 SM86MoveImmediate
307 (geluSM86Register (byte 4))
308 geluSM86ImmediateFour
309 sm86SafeControl)
310 (geluSM86Next
311 (constructor
312 SM86InstructionBody
313 SM86IntegerMultiplyAddWideConstant
314 (geluSM86Register (byte 6))
315 (geluSM86Register (byte 3))
316 (geluSM86Register (byte 4))
317 (byte 0)
318 geluSM86InputPointer
319 sm86SafeControl)
320 (geluSM86Next
321 (constructor
322 SM86InstructionBody
323 SM86LoadGlobal
324 (geluSM86Register (byte 8))
325 (geluSM86Register (byte 6))
326 geluSM86ImmediateZero
327 geluSM86SetBarrier2)
328 (geluSM86Next
329 (constructor
330 SM86InstructionBody
331 SM86MoveConstant
332 (geluSM86Register (byte 10))
333 (byte 0)
334 geluSM86ScaleOffset
335 sm86SafeControl)
336 (geluSM86Next
337 (constructor
338 SM86InstructionBody
339 SM86MoveConstant
340 (geluSM86Register (byte 11))
341 (byte 0)
342 geluSM86CubicOffset
343 sm86SafeControl)
344 (geluSM86Next
345 (constructor
346 SM86InstructionBody
347 SM86MoveConstant
348 (geluSM86Register (byte 12))
349 (byte 0)
350 geluSM86HalfOffset
351 sm86SafeControl)
352 (geluSM86Next
353 (constructor
354 SM86InstructionBody
355 SM86MoveConstant
356 (geluSM86Register (byte 13))
357 (byte 0)
358 geluSM86OneOffset
359 sm86SafeControl)
360 (geluSM86Next
361 (constructor
362 SM86InstructionBody
363 SM86FloatMultiply
364 (geluSM86Register (byte 14))
365 (geluSM86Register (byte 8))
366 (geluSM86Register (byte 8))
367 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2)))
368 (geluSM86Next
369 (constructor
370 SM86InstructionBody
371 SM86FloatMultiply
372 (geluSM86Register (byte 15))
373 (geluSM86Register (byte 14))
374 (geluSM86Register (byte 8))
375 sm86SafeControl)
376 (geluSM86Next
377 (constructor
378 SM86InstructionBody
379 SM86FloatFusedMultiplyAdd
380 (geluSM86Register (byte 16))
381 (geluSM86Register (byte 15))
382 (geluSM86Register (byte 11))
383 (geluSM86Register (byte 8))
384 sm86SafeControl)
385 (geluSM86Next
386 (constructor
387 SM86InstructionBody
388 SM86FloatMultiply
389 (geluSM86Register (byte 16))
390 (geluSM86Register (byte 16))
391 (geluSM86Register (byte 10))
392 sm86SafeControl)
393 (geluSM86Next
394 (constructor
395 SM86InstructionBody
396 SM86MultiFunctionUnitApproximation
397 (geluSM86Register (byte 17))
398 (geluSM86Register (byte 16))
399 (constructor SM86MultiFunction SM86HyperbolicTangent)
400 geluSM86SetBarrier3)
401 (geluSM86Next
402 (constructor
403 SM86InstructionBody
404 SM86FloatAdd
405 (geluSM86Register (byte 17))
406 (geluSM86Register (byte 17))
407 (geluSM86Register (byte 13))
408 geluSM86WaitBarrier3)
409 (geluSM86Next
410 (constructor
411 SM86InstructionBody
412 SM86FloatMultiply
413 (geluSM86Register (byte 17))
414 (geluSM86Register (byte 17))
415 (geluSM86Register (byte 12))
416 sm86SafeControl)
417 (geluSM86Next
418 (constructor
419 SM86InstructionBody
420 SM86FloatMultiply
421 (geluSM86Register (byte 18))
422 (geluSM86Register (byte 8))
423 (geluSM86Register (byte 17))
424 sm86SafeControl)
425 (geluSM86Next
426 (constructor
427 SM86InstructionBody
428 SM86IntegerMultiplyAddWideConstant
429 (geluSM86Register (byte 20))
430 (geluSM86Register (byte 3))
431 (geluSM86Register (byte 4))
432 (byte 0)
433 geluSM86OutputPointer
434 sm86SafeControl)
435 (geluSM86Next
436 (constructor
437 SM86InstructionBody
438 SM86StoreGlobal
439 (geluSM86Register (byte 20))
440 (geluSM86Register (byte 18))
441 geluSM86ImmediateZero
442 sm86SafeControl)
443 (geluSM86Next
444 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
445 geluSM86End))))))))))))))))))))))
446
447def geluSM86BackwardProgram : (family SM86Program) =
448 (geluSM86Next
449 (constructor
450 SM86InstructionBody
451 SM86MoveConstant
452 (geluSM86Register (byte 1))
453 (byte 0)
454 geluSM86ConstantBase
455 sm86SafeControl)
456 (geluSM86Next
457 (constructor
458 SM86InstructionBody
459 SM86SpecialToRegister
460 (geluSM86Register (byte 0))
461 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
462 geluSM86SetBarrier0)
463 (geluSM86Next
464 (constructor
465 SM86InstructionBody
466 SM86SpecialToRegister
467 (geluSM86Register (byte 2))
468 (constructor SM86SpecialRegister SM86ThreadIdX)
469 geluSM86SetBarrier1)
470 (geluSM86Next
471 (constructor
472 SM86InstructionBody
473 SM86IntegerMultiplyAddImmediate
474 (geluSM86Register (byte 3))
475 (geluSM86Register (byte 0))
476 geluSM86ImmediateTwoHundredFiftySix
477 (geluSM86Register (byte 2))
478 geluSM86WaitSpecials)
479 (geluSM86Next
480 (constructor
481 SM86InstructionBody
482 SM86MoveImmediate
483 (geluSM86Register (byte 4))
484 geluSM86ImmediateFour
485 sm86SafeControl)
486 (geluSM86Next
487 (constructor
488 SM86InstructionBody
489 SM86IntegerMultiplyAddWideConstant
490 (geluSM86Register (byte 6))
491 (geluSM86Register (byte 3))
492 (geluSM86Register (byte 4))
493 (byte 0)
494 geluSM86InputPointer
495 sm86SafeControl)
496 (geluSM86Next
497 (constructor
498 SM86InstructionBody
499 SM86IntegerMultiplyAddWideConstant
500 (geluSM86Register (byte 8))
501 (geluSM86Register (byte 3))
502 (geluSM86Register (byte 4))
503 (byte 0)
504 geluSM86UpstreamPointer
505 sm86SafeControl)
506 (geluSM86Next
507 (constructor
508 SM86InstructionBody
509 SM86LoadGlobal
510 (geluSM86Register (byte 10))
511 (geluSM86Register (byte 6))
512 geluSM86ImmediateZero
513 geluSM86SetBarrier2)
514 (geluSM86Next
515 (constructor
516 SM86InstructionBody
517 SM86LoadGlobal
518 (geluSM86Register (byte 11))
519 (geluSM86Register (byte 8))
520 geluSM86ImmediateZero
521 geluSM86SetBarrier3)
522 (geluSM86Next
523 (constructor
524 SM86InstructionBody
525 SM86MoveConstant
526 (geluSM86Register (byte 12))
527 (byte 0)
528 geluSM86ScaleOffset
529 sm86SafeControl)
530 (geluSM86Next
531 (constructor
532 SM86InstructionBody
533 SM86MoveConstant
534 (geluSM86Register (byte 13))
535 (byte 0)
536 geluSM86CubicOffset
537 sm86SafeControl)
538 (geluSM86Next
539 (constructor
540 SM86InstructionBody
541 SM86MoveConstant
542 (geluSM86Register (byte 14))
543 (byte 0)
544 geluSM86HalfOffset
545 sm86SafeControl)
546 (geluSM86Next
547 (constructor
548 SM86InstructionBody
549 SM86MoveConstant
550 (geluSM86Register (byte 15))
551 (byte 0)
552 geluSM86OneOffset
553 sm86SafeControl)
554 (geluSM86Next
555 (constructor
556 SM86InstructionBody
557 SM86MoveConstant
558 (geluSM86Register (byte 16))
559 (byte 0)
560 geluSM86ThreeCubicOffset
561 sm86SafeControl)
562 (geluSM86Next
563 (constructor
564 SM86InstructionBody
565 SM86FloatMultiply
566 (geluSM86Register (byte 17))
567 (geluSM86Register (byte 10))
568 (geluSM86Register (byte 10))
569 geluSM86WaitInputs)
570 (geluSM86Next
571 (constructor
572 SM86InstructionBody
573 SM86FloatMultiply
574 (geluSM86Register (byte 18))
575 (geluSM86Register (byte 17))
576 (geluSM86Register (byte 10))
577 sm86SafeControl)
578 (geluSM86Next
579 (constructor
580 SM86InstructionBody
581 SM86FloatFusedMultiplyAdd
582 (geluSM86Register (byte 19))
583 (geluSM86Register (byte 18))
584 (geluSM86Register (byte 13))
585 (geluSM86Register (byte 10))
586 sm86SafeControl)
587 (geluSM86Next
588 (constructor
589 SM86InstructionBody
590 SM86FloatMultiply
591 (geluSM86Register (byte 19))
592 (geluSM86Register (byte 19))
593 (geluSM86Register (byte 12))
594 sm86SafeControl)
595 (geluSM86Next
596 (constructor
597 SM86InstructionBody
598 SM86MultiFunctionUnitApproximation
599 (geluSM86Register (byte 20))
600 (geluSM86Register (byte 19))
601 (constructor SM86MultiFunction SM86HyperbolicTangent)
602 geluSM86SetBarrier4)
603 (geluSM86Next
604 (constructor
605 SM86InstructionBody
606 SM86FloatMultiply
607 (geluSM86Register (byte 21))
608 (geluSM86Register (byte 20))
609 (geluSM86Register (byte 20))
610 geluSM86WaitBarrier4)
611 (geluSM86Next
612 (constructor
613 SM86InstructionBody
614 SM86FloatNegate
615 (geluSM86Register (byte 21))
616 (geluSM86Register (byte 21))
617 sm86SafeControl)
618 (geluSM86Next
619 (constructor
620 SM86InstructionBody
621 SM86FloatAdd
622 (geluSM86Register (byte 21))
623 (geluSM86Register (byte 15))
624 (geluSM86Register (byte 21))
625 sm86SafeControl)
626 (geluSM86Next
627 (constructor
628 SM86InstructionBody
629 SM86FloatFusedMultiplyAdd
630 (geluSM86Register (byte 22))
631 (geluSM86Register (byte 17))
632 (geluSM86Register (byte 16))
633 (geluSM86Register (byte 15))
634 sm86SafeControl)
635 (geluSM86Next
636 (constructor
637 SM86InstructionBody
638 SM86FloatMultiply
639 (geluSM86Register (byte 22))
640 (geluSM86Register (byte 22))
641 (geluSM86Register (byte 12))
642 sm86SafeControl)
643 (geluSM86Next
644 (constructor
645 SM86InstructionBody
646 SM86FloatAdd
647 (geluSM86Register (byte 23))
648 (geluSM86Register (byte 15))
649 (geluSM86Register (byte 20))
650 sm86SafeControl)
651 (geluSM86Next
652 (constructor
653 SM86InstructionBody
654 SM86FloatMultiply
655 (geluSM86Register (byte 23))
656 (geluSM86Register (byte 23))
657 (geluSM86Register (byte 14))
658 sm86SafeControl)
659 (geluSM86Next
660 (constructor
661 SM86InstructionBody
662 SM86FloatMultiply
663 (geluSM86Register (byte 24))
664 (geluSM86Register (byte 10))
665 (geluSM86Register (byte 21))
666 sm86SafeControl)
667 (geluSM86Next
668 (constructor
669 SM86InstructionBody
670 SM86FloatMultiply
671 (geluSM86Register (byte 24))
672 (geluSM86Register (byte 24))
673 (geluSM86Register (byte 22))
674 sm86SafeControl)
675 (geluSM86Next
676 (constructor
677 SM86InstructionBody
678 SM86FloatMultiply
679 (geluSM86Register (byte 24))
680 (geluSM86Register (byte 24))
681 (geluSM86Register (byte 14))
682 sm86SafeControl)
683 (geluSM86Next
684 (constructor
685 SM86InstructionBody
686 SM86FloatAdd
687 (geluSM86Register (byte 25))
688 (geluSM86Register (byte 23))
689 (geluSM86Register (byte 24))
690 sm86SafeControl)
691 (geluSM86Next
692 (constructor
693 SM86InstructionBody
694 SM86FloatMultiply
695 (geluSM86Register (byte 25))
696 (geluSM86Register (byte 11))
697 (geluSM86Register (byte 25))
698 sm86SafeControl)
699 (geluSM86Next
700 (constructor
701 SM86InstructionBody
702 SM86IntegerMultiplyAddWideConstant
703 (geluSM86Register (byte 26))
704 (geluSM86Register (byte 3))
705 (geluSM86Register (byte 4))
706 (byte 0)
707 geluSM86OutputPointer
708 sm86SafeControl)
709 (geluSM86Next
710 (constructor
711 SM86InstructionBody
712 SM86StoreGlobal
713 (geluSM86Register (byte 26))
714 (geluSM86Register (byte 25))
715 geluSM86ImmediateZero
716 sm86SafeControl)
717 (geluSM86Next
718 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
719 geluSM86End))))))))))))))))))))))))))))))))))
720
721def geluSM86Program =
722 (lambda unrestricted kind : (family GELUSM86ProgramKind) .
723 (eliminate
724 GELUSM86ProgramKind
725 (lambda unrestricted current : (family GELUSM86ProgramKind) . (family SM86Program))
726 kind
727 (branch GELUSM86Forward . geluSM86ForwardProgram)
728 (branch GELUSM86Backward . geluSM86BackwardProgram)))
729
730def geluSM86ExpectedInstructions =
731 (lambda unrestricted kind : (family GELUSM86ProgramKind) .
732 (eliminate
733 GELUSM86ProgramKind
734 (lambda unrestricted current : (family GELUSM86ProgramKind) . Nat)
735 kind
736 (branch GELUSM86Forward . geluSM86NaturalTwentyTwo)
737 (branch GELUSM86Backward . geluSM86NaturalThirtyFour)))
738
739def geluSM86RegisterCount =
740 (lambda unrestricted kind : (family GELUSM86ProgramKind) .
741 (eliminate
742 GELUSM86ProgramKind
743 (lambda unrestricted current : (family GELUSM86ProgramKind) . Nat)
744 kind
745 (branch GELUSM86Forward . geluSM86NaturalTwentyFour)
746 (branch GELUSM86Backward . geluSM86NaturalThirtyTwo)))
747
748def geluSM86FailureCodeBytes =
749 (lambda unrestricted code : (family GELUSM86FailureCode) .
750 (eliminate
751 GELUSM86FailureCode
752 (lambda unrestricted current : (family GELUSM86FailureCode) . Bytes)
753 code
754 (branch GELUSM86ElementCountZero . b"ALPHA-SM86-GELU-001")
755 (branch GELUSM86ElementCountMisaligned . b"ALPHA-SM86-GELU-002")
756 (branch GELUSM86InstructionCountMismatch . b"ALPHA-SM86-GELU-003")
757 (branch GELUSM86EncodingFailed . b"ALPHA-SM86-GELU-004")
758 (branch GELUSM86IdentityInvalid . b"ALPHA-SM86-GELU-005")))
759
760def geluSM86RejectedTelemetry =
761 (lambda unrestricted code : (family GELUSM86FailureCode) .
762 (lambda unrestricted ordinal : Nat .
763 (constructor GELUSM86Telemetry GELUSM86TelemetryRejected code ordinal)))
764
765def geluSM86Plan =
766 (lambda unrestricted kind : (family GELUSM86ProgramKind) .
767 (lambda unrestricted elements : Nat .
768 (nat-eliminate
769 (lambda unrestricted nonzero : Nat . (family GELUSM86PlanResult))
770 (constructor
771 GELUSM86PlanResult
772 GELUSM86PlanFailed
773 (constructor GELUSM86FailureCode GELUSM86ElementCountZero)
774 (geluSM86RejectedTelemetry
775 (constructor GELUSM86FailureCode GELUSM86ElementCountZero)
776 zero))
777 (lambda unrestricted nonzeroPredecessor : Nat .
778 (lambda unrestricted nonzeroInduction : (family GELUSM86PlanResult) .
779 (nat-eliminate
780 (lambda unrestricted aligned : Nat . (family GELUSM86PlanResult))
781 (constructor
782 GELUSM86PlanResult
783 GELUSM86PlanFailed
784 (constructor GELUSM86FailureCode GELUSM86ElementCountMisaligned)
785 (geluSM86RejectedTelemetry
786 (constructor GELUSM86FailureCode GELUSM86ElementCountMisaligned)
787 elements))
788 (lambda unrestricted alignedPredecessor : Nat .
789 (lambda unrestricted alignedInduction : (family GELUSM86PlanResult) .
790 (app
791 (lambda unrestricted program : (family SM86Program) .
792 (app
793 (lambda unrestricted actual : Nat .
794 (nat-eliminate
795 (lambda unrestricted countValid : Nat . (family GELUSM86PlanResult))
796 (constructor
797 GELUSM86PlanResult
798 GELUSM86PlanFailed
799 (constructor GELUSM86FailureCode GELUSM86InstructionCountMismatch)
800 (geluSM86RejectedTelemetry
801 (constructor GELUSM86FailureCode GELUSM86InstructionCountMismatch)
802 actual))
803 (lambda unrestricted countPredecessor : Nat .
804 (lambda unrestricted countInduction : (family GELUSM86PlanResult) .
805 (constructor
806 GELUSM86PlanResult
807 GELUSM86PlanReady
808 (constructor
809 GELUSM86Plan
810 GELUSM86PlanValue
811 kind
812 elements
813 program
814 geluSM86ScalarBindings
815 (constructor
816 GELUSM86Telemetry
817 GELUSM86TelemetryValue
818 kind
819 (geluSM86ExpectedInstructions kind)
820 actual
821 (geluSM86RegisterCount kind)
822 elements
823 (naturalDivideUnchecked elements geluSM86BlockX)
824 geluSM86BlockX
825 geluSM86NaturalFive
826 zero
827 zero
828 zero
829 zero)))))
830 (naturalEqual actual (geluSM86ExpectedInstructions kind))))
831 (sm86ProgramCount program)))
832 (geluSM86Program kind))))
833 (naturalIsZero (naturalModuloUnchecked elements geluSM86BlockX)))))
834 (naturalNonzero elements))))
835
836def geluSM86Image =
837 (lambda unrestricted kind : (family GELUSM86ProgramKind) .
838 (lambda unrestricted elements : Nat .
839 (eliminate
840 GELUSM86PlanResult
841 (lambda unrestricted current : (family GELUSM86PlanResult) . (family GELUSM86ImageResult))
842 (geluSM86Plan kind elements)
843 (branch
844 GELUSM86PlanReady
845 plan
846 .
847 (eliminate
848 GELUSM86Plan
849 (lambda unrestricted current : (family GELUSM86Plan) . (family GELUSM86ImageResult))
850 plan
851 (branch
852 GELUSM86PlanValue
853 plannedKind
854 plannedElements
855 program
856 scalars
857 telemetry
858 .
859 (eliminate
860 SM86ProgramEncodingResult
861 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
862 (family GELUSM86ImageResult))
863 (sm86EncodeProgram program)
864 (branch
865 SM86ProgramEncodingSucceeded
866 image
867 encodingTelemetry
868 .
869 (app
870 (lambda unrestricted identity : Bytes .
871 (nat-eliminate
872 (lambda unrestricted valid : Nat . (family GELUSM86ImageResult))
873 (constructor
874 GELUSM86ImageResult
875 GELUSM86ImageFailed
876 (constructor GELUSM86FailureCode GELUSM86IdentityInvalid)
877 zero
878 (geluSM86FailureCodeBytes
879 (constructor GELUSM86FailureCode GELUSM86IdentityInvalid))
880 telemetry)
881 (lambda unrestricted validPredecessor : Nat .
882 (lambda unrestricted validInduction : (family GELUSM86ImageResult) .
883 (eliminate
884 SM86ProgramEncodingTelemetry
885 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
886 (family GELUSM86ImageResult))
887 encodingTelemetry
888 (branch
889 SM86ProgramEncodingTelemetryValue
890 instructions
891 bytes
892 fields
893 bits
894 highest
895 .
896 (constructor
897 GELUSM86ImageResult
898 GELUSM86ImageReady
899 plannedKind
900 image
901 identity
902 (constructor
903 GELUSM86Telemetry
904 GELUSM86TelemetryValue
905 plannedKind
906 (geluSM86ExpectedInstructions plannedKind)
907 instructions
908 (geluSM86RegisterCount plannedKind)
909 plannedElements
910 (naturalDivideUnchecked plannedElements geluSM86BlockX)
911 geluSM86BlockX
912 geluSM86NaturalFive
913 zero
914 bytes
915 fields
916 bits))))))
917 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
918 (sha256HexBytesOrEmpty (sha256Hex image))))
919 (branch
920 SM86ProgramEncodingFailed
921 index
922 failure
923 encodingTelemetry
924 .
925 (constructor
926 GELUSM86ImageResult
927 GELUSM86ImageFailed
928 (constructor GELUSM86FailureCode GELUSM86EncodingFailed)
929 index
930 (sm86InstructionEncodingStableCode failure)
931 telemetry))))))
932 (branch
933 GELUSM86PlanFailed
934 code
935 telemetry
936 .
937 (constructor
938 GELUSM86ImageResult
939 GELUSM86ImageFailed
940 code
941 zero
942 (geluSM86FailureCodeBytes code)
943 telemetry)))))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.