Realization.Nvidia.SM86.AdamWSM86

1module Realization.Nvidia.SM86.AdamWSM86
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.Byte
12import Std.Natural
13
14family AdamWF32SM86Variant : Type 0
15constructor AdamWF32SM86Unbounded
16constructor AdamWF32SM86Bounded
17
18end-family
19
20family AdamWF32SM86FailureCode : Type 0
21constructor AdamWF32SM86ElementCountZero
22constructor AdamWF32SM86UnboundedExtentMisaligned
23constructor AdamWF32SM86InstructionCountMismatch
24constructor AdamWF32SM86EncodedByteCountMismatch
25constructor AdamWF32SM86EncodingFailed
26constructor AdamWF32SM86IdentityFailed
27constructor AdamWF32SM86IdentityLengthInvalid
28
29end-family
30
31family AdamWF32SM86ABI : Type 0
32constructor AdamWF32SM86ABIValue
33field unrestricted adamWF32ABIParameterPointerOffset : Nat
34field unrestricted adamWF32ABIGradientPointerOffset : Nat
35field unrestricted adamWF32ABIFirstMomentPointerOffset : Nat
36field unrestricted adamWF32ABISecondMomentPointerOffset : Nat
37field unrestricted adamWF32ABIGradientScaleOffset : Nat
38field unrestricted adamWF32ABIBeta1Offset : Nat
39field unrestricted adamWF32ABIOneMinusBeta1Offset : Nat
40field unrestricted adamWF32ABIBeta2Offset : Nat
41field unrestricted adamWF32ABIOneMinusBeta2Offset : Nat
42field unrestricted adamWF32ABIDecayMultiplierOffset : Nat
43field unrestricted adamWF32ABICorrectedStepSizeOffset : Nat
44field unrestricted adamWF32ABIScaledEpsilonOffset : Nat
45field unrestricted adamWF32ABIFP32OneOffset : Nat
46
47end-family
48
49family AdamWF32SM86Extents : Type 0
50constructor AdamWF32SM86ExtentsValue
51field unrestricted adamWF32ExtentsLogicalElements : Nat
52field unrestricted adamWF32ExtentsParameterElements : Nat
53field unrestricted adamWF32ExtentsGradientElements : Nat
54field unrestricted adamWF32ExtentsFirstMomentElements : Nat
55field unrestricted adamWF32ExtentsSecondMomentElements : Nat
56
57end-family
58
59family AdamWF32SM86Manifest : Type 0
60constructor AdamWF32SM86ManifestValue
61field unrestricted adamWF32ManifestVariant : (family AdamWF32SM86Variant)
62field unrestricted adamWF32ManifestExpectedInstructions : Nat
63field unrestricted adamWF32ManifestExpectedEncodedBytes : Nat
64field unrestricted adamWF32ManifestRegisters : Nat
65field unrestricted adamWF32ManifestSharedBytes : Nat
66field unrestricted adamWF32ManifestGridX : Nat
67field unrestricted adamWF32ManifestBlockX : Nat
68field unrestricted adamWF32ManifestABI : (family AdamWF32SM86ABI)
69field unrestricted adamWF32ManifestExtents : (family AdamWF32SM86Extents)
70field unrestricted adamWF32ManifestSetBarrierControls : Nat
71field unrestricted adamWF32ManifestWaitSpecialsMask : Nat
72field unrestricted adamWF32ManifestWaitLoadsMask : Nat
73field unrestricted adamWF32ManifestWaitMufuMask : Nat
74field unrestricted adamWF32ManifestGuardedMemoryInstructions : Nat
75field unrestricted adamWF32ManifestHostFallbackOperations : Nat
76
77end-family
78
79family AdamWF32SM86Telemetry : Type 0
80constructor AdamWF32SM86TelemetryValue
81field unrestricted adamWF32TelemetryManifest : (family AdamWF32SM86Manifest)
82field unrestricted adamWF32TelemetryObservedInstructions : Nat
83field unrestricted adamWF32TelemetryObservedEncodedBytes : Nat
84field unrestricted adamWF32TelemetryEncodedFields : Nat
85field unrestricted adamWF32TelemetryEncodedBits : Nat
86field unrestricted adamWF32TelemetryHighestEncodedBit : Nat
87field unrestricted adamWF32TelemetryFailureOrdinal : Nat
88
89end-family
90
91family AdamWF32SM86Plan : Type 0
92constructor AdamWF32SM86PlanValue
93field unrestricted adamWF32PlanVariant : (family AdamWF32SM86Variant)
94field unrestricted adamWF32PlanLogicalElements : Nat
95field unrestricted adamWF32PlanProgram : (family SM86Program)
96field unrestricted adamWF32PlanTelemetry : (family AdamWF32SM86Telemetry)
97
98end-family
99
100family AdamWF32SM86PlanResult : Type 0
101constructor AdamWF32SM86PlanReady
102field unrestricted adamWF32ReadyPlan : (family AdamWF32SM86Plan)
103constructor AdamWF32SM86PlanFailed
104field unrestricted adamWF32PlanFailure : (family AdamWF32SM86FailureCode)
105field unrestricted adamWF32PlanFailureTelemetry : (family AdamWF32SM86Telemetry)
106
107end-family
108
109family AdamWF32SM86ImageResult : Type 0
110constructor AdamWF32SM86ImageReady
111field unrestricted adamWF32ImageBytes : Bytes
112field unrestricted adamWF32ImageSHA256 : Bytes
113field unrestricted adamWF32ImageEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
114field unrestricted adamWF32ImageIdentityTelemetry : (family SHA256DigestTelemetry)
115field unrestricted adamWF32ImageTelemetry : (family AdamWF32SM86Telemetry)
116constructor AdamWF32SM86ImageFailed
117field unrestricted adamWF32ImageFailure : (family AdamWF32SM86FailureCode)
118field unrestricted adamWF32ImageFailureOrdinal : Nat
119field unrestricted adamWF32ImageFailureDetail : Bytes
120field unrestricted adamWF32ImageFailureTelemetry : (family AdamWF32SM86Telemetry)
121
122end-family
123
124def adamWF32SM86FailureCodeBytes =
125  (lambda unrestricted code : (family AdamWF32SM86FailureCode) .
126    (eliminate
127      AdamWF32SM86FailureCode
128      (lambda unrestricted current : (family AdamWF32SM86FailureCode) . Bytes)
129      code
130      (branch AdamWF32SM86ElementCountZero . b"ALPHA-SM86-ADAMW-001")
131      (branch AdamWF32SM86UnboundedExtentMisaligned . b"ALPHA-SM86-ADAMW-002")
132      (branch AdamWF32SM86InstructionCountMismatch . b"ALPHA-SM86-ADAMW-003")
133      (branch AdamWF32SM86EncodedByteCountMismatch . b"ALPHA-SM86-ADAMW-004")
134      (branch AdamWF32SM86EncodingFailed . b"ALPHA-SM86-ADAMW-005")
135      (branch AdamWF32SM86IdentityFailed . b"ALPHA-SM86-ADAMW-006")
136      (branch AdamWF32SM86IdentityLengthInvalid . b"ALPHA-SM86-ADAMW-007")))
137
138def adamWF32R0 =
139  (sm86Register (byte 0))
140
141def adamWF32R1 =
142  (sm86Register (byte 1))
143
144def adamWF32R2 =
145  (sm86Register (byte 2))
146
147def adamWF32R3 =
148  (sm86Register (byte 3))
149
150def adamWF32R6 =
151  (sm86Register (byte 6))
152
153def adamWF32R8 =
154  (sm86Register (byte 8))
155
156def adamWF32R10 =
157  (sm86Register (byte 10))
158
159def adamWF32R12 =
160  (sm86Register (byte 12))
161
162def adamWF32R14 =
163  (sm86Register (byte 14))
164
165def adamWF32R15 =
166  (sm86Register (byte 15))
167
168def adamWF32R16 =
169  (sm86Register (byte 16))
170
171def adamWF32R17 =
172  (sm86Register (byte 17))
173
174def adamWF32R18 =
175  (sm86Register (byte 18))
176
177def adamWF32R19 =
178  (sm86Register (byte 19))
179
180def adamWF32R20 =
181  (sm86Register (byte 20))
182
183def adamWF32R21 =
184  (sm86Register (byte 21))
185
186def adamWF32R22 =
187  (sm86Register (byte 22))
188
189def adamWF32R23 =
190  (sm86Register (byte 23))
191
192def adamWF32R24 =
193  (sm86Register (byte 24))
194
195def adamWF32R25 =
196  (sm86Register (byte 25))
197
198def adamWF32R26 =
199  (sm86Register (byte 26))
200
201def adamWF32R27 =
202  (sm86Register (byte 27))
203
204def adamWF32R28 =
205  (sm86Register (byte 28))
206
207def adamWF32P0 =
208  (constructor SM86Predicate SM86Predicate0)
209
210def adamWF32U0 =
211  sm86Unsigned32Zero
212
213def adamWF32U4 =
214  (sm86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))
215
216def adamWF32U256 =
217  (sm86Unsigned32 (byte 0) (byte 1) (byte 0) (byte 0))
218
219def adamWF32Offset028 =
220  (sm86Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0))
221
222def adamWF32Offset160 =
223  (sm86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))
224
225def adamWF32Offset168 =
226  (sm86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))
227
228def adamWF32Offset170 =
229  (sm86Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0))
230
231def adamWF32Offset178 =
232  (sm86Unsigned32 (byte 120) (byte 1) (byte 0) (byte 0))
233
234def adamWF32Offset180 =
235  (sm86Unsigned32 (byte 128) (byte 1) (byte 0) (byte 0))
236
237def adamWF32Offset184 =
238  (sm86Unsigned32 (byte 132) (byte 1) (byte 0) (byte 0))
239
240def adamWF32Offset188 =
241  (sm86Unsigned32 (byte 136) (byte 1) (byte 0) (byte 0))
242
243def adamWF32Offset18c =
244  (sm86Unsigned32 (byte 140) (byte 1) (byte 0) (byte 0))
245
246def adamWF32Offset190 =
247  (sm86Unsigned32 (byte 144) (byte 1) (byte 0) (byte 0))
248
249def adamWF32Offset194 =
250  (sm86Unsigned32 (byte 148) (byte 1) (byte 0) (byte 0))
251
252def adamWF32Offset198 =
253  (sm86Unsigned32 (byte 152) (byte 1) (byte 0) (byte 0))
254
255def adamWF32Offset19c =
256  (sm86Unsigned32 (byte 156) (byte 1) (byte 0) (byte 0))
257
258def adamWF32Offset1a0 =
259  (sm86Unsigned32 (byte 160) (byte 1) (byte 0) (byte 0))
260
261def adamWF32Unsigned32FromNatural =
262  (lambda unrestricted value : Nat .
263    (app
264      (lambda unrestricted quotient1 : Nat .
265        (app
266          (lambda unrestricted quotient2 : Nat .
267            (app
268              (lambda unrestricted quotient3 : Nat .
269                (sm86Unsigned32
270                  (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
271                  (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
272                  (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
273                  (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
274              (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
275          (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
276      (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))
277
278def adamWF32Set0 =
279  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
280
281def adamWF32Set1 =
282  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))
283
284def adamWF32Set2 =
285  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))
286
287def adamWF32Set3 =
288  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3))
289
290def adamWF32Wait0 =
291  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))
292
293def adamWF32WaitSpecials : (family SM86Control) =
294  (constructor
295    SM86Control
296    SM86ControlValue
297    (byte 7)
298    (constructor SM86YieldMode SM86Continue)
299    (constructor SM86Barrier SM86BarrierNone)
300    (constructor SM86Barrier SM86BarrierNone)
301    (byte 3)
302    (byte 0))
303
304def adamWF32WaitLoads : (family SM86Control) =
305  (constructor
306    SM86Control
307    SM86ControlValue
308    (byte 7)
309    (constructor SM86YieldMode SM86Continue)
310    (constructor SM86Barrier SM86BarrierNone)
311    (constructor SM86Barrier SM86BarrierNone)
312    (byte 15)
313    (byte 0))
314
315def adamWF32Next =
316  (lambda unrestricted body : (family SM86InstructionBody) .
317    (lambda unrestricted tail : (family SM86Program) .
318      (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))
319
320def adamWF32InstructionFor =
321  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
322    (lambda unrestricted body : (family SM86InstructionBody) .
323      (eliminate
324        AdamWF32SM86Variant
325        (lambda unrestricted current : (family AdamWF32SM86Variant) . (family SM86Instruction))
326        variant
327        (branch AdamWF32SM86Unbounded . (sm86Instruction body))
328        (branch AdamWF32SM86Bounded . (sm86NegatedPredicatedInstruction adamWF32P0 body)))))
329
330def adamWF32GuardedNext =
331  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
332    (lambda unrestricted body : (family SM86InstructionBody) .
333      (lambda unrestricted tail : (family SM86Program) .
334        (constructor SM86Program SM86ProgramNext (adamWF32InstructionFor variant body) tail))))
335
336def adamWF32PrefixProgram : (family SM86Program) =
337  (adamWF32Next
338    (constructor
339      SM86InstructionBody
340      SM86MoveConstant
341      adamWF32R1
342      (byte 0)
343      adamWF32Offset028
344      sm86SafeControl)
345    (adamWF32Next
346      (constructor
347        SM86InstructionBody
348        SM86SpecialToRegister
349        adamWF32R0
350        (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
351        adamWF32Set0)
352      (adamWF32Next
353        (constructor
354          SM86InstructionBody
355          SM86SpecialToRegister
356          adamWF32R2
357          (constructor SM86SpecialRegister SM86ThreadIdX)
358          adamWF32Set1)
359        (adamWF32Next
360          (constructor
361            SM86InstructionBody
362            SM86MoveImmediate
363            adamWF32R3
364            adamWF32U4
365            adamWF32WaitSpecials)
366          (adamWF32Next
367            (constructor
368              SM86InstructionBody
369              SM86IntegerMultiplyAddImmediate
370              adamWF32R0
371              adamWF32R0
372              adamWF32U256
373              adamWF32R2
374              sm86SafeControl)
375            (constructor SM86Program SM86ProgramEnd))))))
376
377def adamWF32BoundsProgram =
378  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
379    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
380      (eliminate
381        AdamWF32SM86Variant
382        (lambda unrestricted current : (family AdamWF32SM86Variant) . (family SM86Program))
383        variant
384        (branch AdamWF32SM86Unbounded . (constructor SM86Program SM86ProgramEnd))
385        (branch
386          AdamWF32SM86Bounded
387          .
388          (adamWF32Next
389            (constructor
390              SM86InstructionBody
391              SM86PredicateGreaterThanImmediate
392              adamWF32P0
393              adamWF32R0
394              (adamWF32Unsigned32FromNatural
395                (naturalPredecessor (sm86Unsigned32Natural logicalElements)))
396              sm86SafeControl)
397            (constructor SM86Program SM86ProgramEnd))))))
398
399def adamWF32AddressProgram : (family SM86Program) =
400  (adamWF32Next
401    (constructor
402      SM86InstructionBody
403      SM86IntegerMultiplyAddWideConstant
404      adamWF32R6
405      adamWF32R0
406      adamWF32R3
407      (byte 0)
408      adamWF32Offset160
409      sm86SafeControl)
410    (adamWF32Next
411      (constructor
412        SM86InstructionBody
413        SM86IntegerMultiplyAddWideConstant
414        adamWF32R8
415        adamWF32R0
416        adamWF32R3
417        (byte 0)
418        adamWF32Offset168
419        sm86SafeControl)
420      (adamWF32Next
421        (constructor
422          SM86InstructionBody
423          SM86IntegerMultiplyAddWideConstant
424          adamWF32R10
425          adamWF32R0
426          adamWF32R3
427          (byte 0)
428          adamWF32Offset170
429          sm86SafeControl)
430        (adamWF32Next
431          (constructor
432            SM86InstructionBody
433            SM86IntegerMultiplyAddWideConstant
434            adamWF32R12
435            adamWF32R0
436            adamWF32R3
437            (byte 0)
438            adamWF32Offset178
439            sm86SafeControl)
440          (constructor SM86Program SM86ProgramEnd)))))
441
442def adamWF32LoadProgram =
443  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
444    (adamWF32GuardedNext
445      variant
446      (constructor
447        SM86InstructionBody
448        SM86LoadGlobal
449        adamWF32R14
450        adamWF32R6
451        adamWF32U0
452        adamWF32Set0)
453      (adamWF32GuardedNext
454        variant
455        (constructor
456          SM86InstructionBody
457          SM86LoadGlobal
458          adamWF32R15
459          adamWF32R8
460          adamWF32U0
461          adamWF32Set1)
462        (adamWF32GuardedNext
463          variant
464          (constructor
465            SM86InstructionBody
466            SM86LoadGlobal
467            adamWF32R16
468            adamWF32R10
469            adamWF32U0
470            adamWF32Set2)
471          (adamWF32GuardedNext
472            variant
473            (constructor
474              SM86InstructionBody
475              SM86LoadGlobal
476              adamWF32R17
477              adamWF32R12
478              adamWF32U0
479              adamWF32Set3)
480            (constructor SM86Program SM86ProgramEnd))))))
481
482def adamWF32ScalarProgram : (family SM86Program) =
483  (adamWF32Next
484    (constructor
485      SM86InstructionBody
486      SM86MoveConstant
487      adamWF32R18
488      (byte 0)
489      adamWF32Offset180
490      sm86SafeControl)
491    (adamWF32Next
492      (constructor
493        SM86InstructionBody
494        SM86MoveConstant
495        adamWF32R19
496        (byte 0)
497        adamWF32Offset184
498        sm86SafeControl)
499      (adamWF32Next
500        (constructor
501          SM86InstructionBody
502          SM86MoveConstant
503          adamWF32R20
504          (byte 0)
505          adamWF32Offset188
506          sm86SafeControl)
507        (adamWF32Next
508          (constructor
509            SM86InstructionBody
510            SM86MoveConstant
511            adamWF32R21
512            (byte 0)
513            adamWF32Offset18c
514            sm86SafeControl)
515          (adamWF32Next
516            (constructor
517              SM86InstructionBody
518              SM86MoveConstant
519              adamWF32R22
520              (byte 0)
521              adamWF32Offset190
522              sm86SafeControl)
523            (adamWF32Next
524              (constructor
525                SM86InstructionBody
526                SM86MoveConstant
527                adamWF32R23
528                (byte 0)
529                adamWF32Offset194
530                sm86SafeControl)
531              (adamWF32Next
532                (constructor
533                  SM86InstructionBody
534                  SM86MoveConstant
535                  adamWF32R24
536                  (byte 0)
537                  adamWF32Offset198
538                  sm86SafeControl)
539                (adamWF32Next
540                  (constructor
541                    SM86InstructionBody
542                    SM86MoveConstant
543                    adamWF32R25
544                    (byte 0)
545                    adamWF32Offset19c
546                    sm86SafeControl)
547                  (constructor SM86Program SM86ProgramEnd)))))))))
548
549def adamWF32MathProgram : (family SM86Program) =
550  (adamWF32Next
551    (constructor
552      SM86InstructionBody
553      SM86FloatMultiply
554      adamWF32R15
555      adamWF32R15
556      adamWF32R18
557      adamWF32WaitLoads)
558    (adamWF32Next
559      (constructor
560        SM86InstructionBody
561        SM86FloatMultiply
562        adamWF32R26
563        adamWF32R15
564        adamWF32R20
565        sm86SafeControl)
566      (adamWF32Next
567        (constructor
568          SM86InstructionBody
569          SM86FloatFusedMultiplyAdd
570          adamWF32R16
571          adamWF32R16
572          adamWF32R19
573          adamWF32R26
574          sm86SafeControl)
575        (adamWF32Next
576          (constructor
577            SM86InstructionBody
578            SM86FloatMultiply
579            adamWF32R28
580            adamWF32R15
581            adamWF32R15
582            sm86SafeControl)
583          (adamWF32Next
584            (constructor
585              SM86InstructionBody
586              SM86FloatMultiply
587              adamWF32R28
588              adamWF32R28
589              adamWF32R22
590              sm86SafeControl)
591            (adamWF32Next
592              (constructor
593                SM86InstructionBody
594                SM86FloatFusedMultiplyAdd
595                adamWF32R17
596                adamWF32R17
597                adamWF32R21
598                adamWF32R28
599                sm86SafeControl)
600              (adamWF32Next
601                (constructor
602                  SM86InstructionBody
603                  SM86MultiFunctionUnitApproximation
604                  adamWF32R27
605                  adamWF32R17
606                  (constructor SM86MultiFunction SM86SquareRoot)
607                  adamWF32Set0)
608                (adamWF32Next
609                  (constructor
610                    SM86InstructionBody
611                    SM86FloatAdd
612                    adamWF32R27
613                    adamWF32R27
614                    adamWF32R25
615                    adamWF32Wait0)
616                  (adamWF32Next
617                    (constructor
618                      SM86InstructionBody
619                      SM86MultiFunctionUnitApproximation
620                      adamWF32R27
621                      adamWF32R27
622                      (constructor SM86MultiFunction SM86Reciprocal)
623                      adamWF32Set0)
624                    (adamWF32Next
625                      (constructor
626                        SM86InstructionBody
627                        SM86FloatMultiply
628                        adamWF32R26
629                        adamWF32R16
630                        adamWF32R24
631                        sm86SafeControl)
632                      (adamWF32Next
633                        (constructor
634                          SM86InstructionBody
635                          SM86FloatMultiply
636                          adamWF32R26
637                          adamWF32R26
638                          adamWF32R27
639                          adamWF32Wait0)
640                        (adamWF32Next
641                          (constructor
642                            SM86InstructionBody
643                            SM86FloatNegate
644                            adamWF32R26
645                            adamWF32R26
646                            sm86SafeControl)
647                          (adamWF32Next
648                            (constructor
649                              SM86InstructionBody
650                              SM86FloatMultiply
651                              adamWF32R14
652                              adamWF32R14
653                              adamWF32R23
654                              sm86SafeControl)
655                            (adamWF32Next
656                              (constructor
657                                SM86InstructionBody
658                                SM86FloatAdd
659                                adamWF32R14
660                                adamWF32R14
661                                adamWF32R26
662                                sm86SafeControl)
663                              (constructor SM86Program SM86ProgramEnd)))))))))))))))
664
665def adamWF32SuffixProgram =
666  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
667    (adamWF32GuardedNext
668      variant
669      (constructor
670        SM86InstructionBody
671        SM86StoreGlobal
672        adamWF32R6
673        adamWF32R14
674        adamWF32U0
675        sm86SafeControl)
676      (adamWF32GuardedNext
677        variant
678        (constructor
679          SM86InstructionBody
680          SM86StoreGlobal
681          adamWF32R10
682          adamWF32R16
683          adamWF32U0
684          sm86SafeControl)
685        (adamWF32GuardedNext
686          variant
687          (constructor
688            SM86InstructionBody
689            SM86StoreGlobal
690            adamWF32R12
691            adamWF32R17
692            adamWF32U0
693            sm86SafeControl)
694          (adamWF32Next
695            (constructor SM86InstructionBody SM86Exit sm86SafeControl)
696            (constructor SM86Program SM86ProgramEnd))))))
697
698def adamWF32BodyProgram =
699  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
700    (sm86ProgramAppend
701      adamWF32AddressProgram
702      (sm86ProgramAppend
703        (adamWF32LoadProgram variant)
704        (sm86ProgramAppend
705          adamWF32ScalarProgram
706          (sm86ProgramAppend adamWF32MathProgram (adamWF32SuffixProgram variant))))))
707
708def adamWF32ProgramFor =
709  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
710    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
711      (sm86ProgramAppend
712        adamWF32PrefixProgram
713        (sm86ProgramAppend
714          (adamWF32BoundsProgram variant logicalElements)
715          (adamWF32BodyProgram variant)))))
716
717def adamWF32UnboundedProgram : (family SM86Program) =
718  (adamWF32ProgramFor (constructor AdamWF32SM86Variant AdamWF32SM86Unbounded) adamWF32U256)
719
720def adamWF32BoundedProgram =
721  (lambda unrestricted logicalElements : (family SM86Unsigned32) .
722    (adamWF32ProgramFor (constructor AdamWF32SM86Variant AdamWF32SM86Bounded) logicalElements))
723
724def adamWF32N3 =
725  (byte-to-nat (byte 3))
726
727def adamWF32N4 =
728  (byte-to-nat (byte 4))
729
730def adamWF32N7 =
731  (byte-to-nat (byte 7))
732
733def adamWF32N15 =
734  (byte-to-nat (byte 15))
735
736def adamWF32N16 =
737  (byte-to-nat (byte 16))
738
739def adamWF32N32 =
740  (byte-to-nat (byte 32))
741
742def adamWF32N39 =
743  (byte-to-nat (byte 39))
744
745def adamWF32N40 =
746  (byte-to-nat (byte 40))
747
748def adamWF32N64 =
749  (byte-to-nat (byte 64))
750
751def adamWF32N255 =
752  (byte-to-nat (byte 255))
753
754def adamWF32N256 =
755  (succ adamWF32N255)
756
757def adamWF32ExpectedInstructions =
758  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
759    (eliminate
760      AdamWF32SM86Variant
761      (lambda unrestricted current : (family AdamWF32SM86Variant) . Nat)
762      variant
763      (branch AdamWF32SM86Unbounded . adamWF32N39)
764      (branch AdamWF32SM86Bounded . adamWF32N40)))
765
766def adamWF32ExpectedEncodedBytes =
767  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
768    (naturalMultiply (adamWF32ExpectedInstructions variant) adamWF32N16))
769
770def adamWF32GridX =
771  (lambda unrestricted logicalElements : Nat .
772    (naturalDivideUnchecked (naturalAdd logicalElements adamWF32N255) adamWF32N256))
773
774def adamWF32ABI : (family AdamWF32SM86ABI) =
775  (constructor
776    AdamWF32SM86ABI
777    AdamWF32SM86ABIValue
778    (sm86Unsigned32Natural adamWF32Offset160)
779    (sm86Unsigned32Natural adamWF32Offset168)
780    (sm86Unsigned32Natural adamWF32Offset170)
781    (sm86Unsigned32Natural adamWF32Offset178)
782    (sm86Unsigned32Natural adamWF32Offset180)
783    (sm86Unsigned32Natural adamWF32Offset184)
784    (sm86Unsigned32Natural adamWF32Offset188)
785    (sm86Unsigned32Natural adamWF32Offset18c)
786    (sm86Unsigned32Natural adamWF32Offset190)
787    (sm86Unsigned32Natural adamWF32Offset194)
788    (sm86Unsigned32Natural adamWF32Offset198)
789    (sm86Unsigned32Natural adamWF32Offset19c)
790    (sm86Unsigned32Natural adamWF32Offset1a0))
791
792-- where the step-dependent scalars sit in the parameter block (a host that
793-- supplies them at run time writes there)
794def adamWF32CorrectedStepSizeOffsetOf =
795  (lambda unrestricted abi : (family AdamWF32SM86ABI) .
796    (eliminate AdamWF32SM86ABI (lambda unrestricted current : (family AdamWF32SM86ABI) . Nat) abi
797      (branch AdamWF32SM86ABIValue p g m v scale b1 c1 b2 c2 decay step epsilon one . step)))
798
799def adamWF32ScaledEpsilonOffsetOf =
800  (lambda unrestricted abi : (family AdamWF32SM86ABI) .
801    (eliminate AdamWF32SM86ABI (lambda unrestricted current : (family AdamWF32SM86ABI) . Nat) abi
802      (branch AdamWF32SM86ABIValue p g m v scale b1 c1 b2 c2 decay step epsilon one . epsilon)))
803
804def adamWF32GuardedMemoryInstructions =
805  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
806    (eliminate
807      AdamWF32SM86Variant
808      (lambda unrestricted current : (family AdamWF32SM86Variant) . Nat)
809      variant
810      (branch AdamWF32SM86Unbounded . zero)
811      (branch AdamWF32SM86Bounded . adamWF32N7)))
812
813def adamWF32ManifestFor =
814  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
815    (lambda unrestricted logicalElements : Nat .
816      (constructor
817        AdamWF32SM86Manifest
818        AdamWF32SM86ManifestValue
819        variant
820        (adamWF32ExpectedInstructions variant)
821        (adamWF32ExpectedEncodedBytes variant)
822        adamWF32N32
823        zero
824        (adamWF32GridX logicalElements)
825        adamWF32N256
826        adamWF32ABI
827        (constructor
828          AdamWF32SM86Extents
829          AdamWF32SM86ExtentsValue
830          logicalElements
831          logicalElements
832          logicalElements
833          logicalElements
834          logicalElements)
835        adamWF32N4
836        adamWF32N3
837        adamWF32N15
838        (succ zero)
839        (adamWF32GuardedMemoryInstructions variant)
840        zero)))
841
842def adamWF32TelemetryFor =
843  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
844    (lambda unrestricted logicalElements : Nat .
845      (lambda unrestricted observedInstructions : Nat .
846        (lambda unrestricted observedEncodedBytes : Nat .
847          (lambda unrestricted encodedFields : Nat .
848            (lambda unrestricted encodedBits : Nat .
849              (lambda unrestricted highestEncodedBit : Nat .
850                (lambda unrestricted failureOrdinal : Nat .
851                  (constructor
852                    AdamWF32SM86Telemetry
853                    AdamWF32SM86TelemetryValue
854                    (adamWF32ManifestFor variant logicalElements)
855                    observedInstructions
856                    observedEncodedBytes
857                    encodedFields
858                    encodedBits
859                    highestEncodedBit
860                    failureOrdinal)))))))))
861
862def adamWF32RejectedTelemetry =
863  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
864    (lambda unrestricted logicalElements : Nat .
865      (lambda unrestricted ordinal : Nat .
866        (adamWF32TelemetryFor variant logicalElements zero zero zero zero zero ordinal))))
867
868def adamWF32AlignmentValid =
869  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
870    (lambda unrestricted logicalElements : Nat .
871      (eliminate
872        AdamWF32SM86Variant
873        (lambda unrestricted current : (family AdamWF32SM86Variant) . Nat)
874        variant
875        (branch
876          AdamWF32SM86Unbounded
877          .
878          (naturalIsZero (naturalModuloUnchecked logicalElements adamWF32N256)))
879        (branch AdamWF32SM86Bounded . (succ zero)))))
880
881def adamWF32Plan =
882  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
883    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
884      (app
885        (lambda unrestricted elements : Nat .
886          (nat-eliminate
887            (lambda unrestricted nonzero : Nat . (family AdamWF32SM86PlanResult))
888            (constructor
889              AdamWF32SM86PlanResult
890              AdamWF32SM86PlanFailed
891              (constructor AdamWF32SM86FailureCode AdamWF32SM86ElementCountZero)
892              (adamWF32RejectedTelemetry variant elements zero))
893            (lambda unrestricted nonzeroPredecessor : Nat .
894              (lambda unrestricted nonzeroInduction : (family AdamWF32SM86PlanResult) .
895                (nat-eliminate
896                  (lambda unrestricted aligned : Nat . (family AdamWF32SM86PlanResult))
897                  (constructor
898                    AdamWF32SM86PlanResult
899                    AdamWF32SM86PlanFailed
900                    (constructor AdamWF32SM86FailureCode AdamWF32SM86UnboundedExtentMisaligned)
901                    (adamWF32RejectedTelemetry variant elements elements))
902                  (lambda unrestricted alignedPredecessor : Nat .
903                    (lambda unrestricted alignedInduction : (family AdamWF32SM86PlanResult) .
904                      (app
905                        (lambda unrestricted program : (family SM86Program) .
906                          (app
907                            (lambda unrestricted observedInstructions : Nat .
908                              (nat-eliminate
909                                (lambda unrestricted countMatched : Nat .
910                                  (family AdamWF32SM86PlanResult))
911                                (constructor
912                                  AdamWF32SM86PlanResult
913                                  AdamWF32SM86PlanFailed
914                                  (constructor
915                                    AdamWF32SM86FailureCode
916                                    AdamWF32SM86InstructionCountMismatch)
917                                  (adamWF32TelemetryFor
918                                    variant
919                                    elements
920                                    observedInstructions
921                                    zero
922                                    zero
923                                    zero
924                                    zero
925                                    observedInstructions))
926                                (lambda unrestricted countPredecessor : Nat .
927                                  (lambda unrestricted countInduction : (family AdamWF32SM86PlanResult) .
928                                    (constructor
929                                      AdamWF32SM86PlanResult
930                                      AdamWF32SM86PlanReady
931                                      (constructor
932                                        AdamWF32SM86Plan
933                                        AdamWF32SM86PlanValue
934                                        variant
935                                        elements
936                                        program
937                                        (adamWF32TelemetryFor
938                                        variant
939                                        elements
940                                        observedInstructions
941                                        zero
942                                        zero
943                                        zero
944                                        zero
945                                        zero)))))
946                                (naturalEqual
947                                  observedInstructions
948                                  (adamWF32ExpectedInstructions variant))))
949                            (sm86ProgramCount program)))
950                        (adamWF32ProgramFor variant logicalElements))))
951                  (adamWF32AlignmentValid variant elements))))
952            (naturalNonzero elements)))
953        (sm86Unsigned32Natural logicalElements))))
954
955def adamWF32Image =
956  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
957    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
958      (eliminate
959        AdamWF32SM86PlanResult
960        (lambda unrestricted current : (family AdamWF32SM86PlanResult) .
961          (family AdamWF32SM86ImageResult))
962        (adamWF32Plan variant logicalElements)
963        (branch
964          AdamWF32SM86PlanReady
965          plan
966          .
967          (eliminate
968            AdamWF32SM86Plan
969            (lambda unrestricted current : (family AdamWF32SM86Plan) .
970              (family AdamWF32SM86ImageResult))
971            plan
972            (branch
973              AdamWF32SM86PlanValue
974              plannedVariant
975              plannedElements
976              program
977              planTelemetry
978              .
979              (eliminate
980                SM86ProgramEncodingResult
981                (lambda unrestricted current : (family SM86ProgramEncodingResult) .
982                  (family AdamWF32SM86ImageResult))
983                (sm86EncodeProgram program)
984                (branch
985                  SM86ProgramEncodingSucceeded
986                  image
987                  encodingTelemetry
988                  .
989                  (eliminate
990                    SM86ProgramEncodingTelemetry
991                    (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
992                      (family AdamWF32SM86ImageResult))
993                    encodingTelemetry
994                    (branch
995                      SM86ProgramEncodingTelemetryValue
996                      instructions
997                      bytes
998                      fields
999                      bits
1000                      highest
1001                      .
1002                      (app
1003                        (lambda unrestricted telemetry : (family AdamWF32SM86Telemetry) .
1004                          (nat-eliminate
1005                            (lambda unrestricted byteCountMatched : Nat .
1006                              (family AdamWF32SM86ImageResult))
1007                            (constructor
1008                              AdamWF32SM86ImageResult
1009                              AdamWF32SM86ImageFailed
1010                              (constructor
1011                                AdamWF32SM86FailureCode
1012                                AdamWF32SM86EncodedByteCountMismatch)
1013                              bytes
1014                              (adamWF32SM86FailureCodeBytes
1015                                (constructor
1016                                  AdamWF32SM86FailureCode
1017                                  AdamWF32SM86EncodedByteCountMismatch))
1018                              telemetry)
1019                            (lambda unrestricted byteCountPredecessor : Nat .
1020                              (lambda unrestricted byteCountInduction : (family AdamWF32SM86ImageResult) .
1021                                (eliminate
1022                                  SHA256HexResult
1023                                  (lambda unrestricted current : (family SHA256HexResult) .
1024                                    (family AdamWF32SM86ImageResult))
1025                                  (sha256Hex image)
1026                                  (branch
1027                                    SHA256HexSucceeded
1028                                    identity
1029                                    identityTelemetry
1030                                    .
1031                                    (nat-eliminate
1032                                      (lambda unrestricted lengthMatched : Nat .
1033                                        (family AdamWF32SM86ImageResult))
1034                                      (constructor
1035                                        AdamWF32SM86ImageResult
1036                                        AdamWF32SM86ImageFailed
1037                                        (constructor
1038                                        AdamWF32SM86FailureCode
1039                                        AdamWF32SM86IdentityLengthInvalid)
1040                                        (bytes-length identity)
1041                                        (adamWF32SM86FailureCodeBytes
1042                                        (constructor
1043                                        AdamWF32SM86FailureCode
1044                                        AdamWF32SM86IdentityLengthInvalid))
1045                                        telemetry)
1046                                      (lambda unrestricted lengthPredecessor : Nat .
1047                                        (lambda unrestricted lengthInduction : (family AdamWF32SM86ImageResult) .
1048                                        (constructor
1049                                        AdamWF32SM86ImageResult
1050                                        AdamWF32SM86ImageReady
1051                                        image
1052                                        identity
1053                                        encodingTelemetry
1054                                        identityTelemetry
1055                                        telemetry)))
1056                                      (naturalEqual (bytes-length identity) adamWF32N64)))
1057                                  (branch
1058                                    SHA256HexFailed
1059                                    error
1060                                    ordinal
1061                                    identityTelemetry
1062                                    .
1063                                    (constructor
1064                                      AdamWF32SM86ImageResult
1065                                      AdamWF32SM86ImageFailed
1066                                      (constructor
1067                                        AdamWF32SM86FailureCode
1068                                        AdamWF32SM86IdentityFailed)
1069                                      ordinal
1070                                      (adamWF32SM86FailureCodeBytes
1071                                        (constructor
1072                                        AdamWF32SM86FailureCode
1073                                        AdamWF32SM86IdentityFailed))
1074                                      telemetry)))))
1075                            (naturalEqual
1076                              (bytes-length image)
1077                              (adamWF32ExpectedEncodedBytes plannedVariant))))
1078                        (adamWF32TelemetryFor
1079                          plannedVariant
1080                          plannedElements
1081                          instructions
1082                          bytes
1083                          fields
1084                          bits
1085                          highest
1086                          zero)))))
1087                (branch
1088                  SM86ProgramEncodingFailed
1089                  instructionIndex
1090                  failure
1091                  encodingTelemetry
1092                  .
1093                  (constructor
1094                    AdamWF32SM86ImageResult
1095                    AdamWF32SM86ImageFailed
1096                    (constructor AdamWF32SM86FailureCode AdamWF32SM86EncodingFailed)
1097                    instructionIndex
1098                    (sm86InstructionEncodingStableCode failure)
1099                    (adamWF32TelemetryFor
1100                      plannedVariant
1101                      plannedElements
1102                      (sm86ProgramCount program)
1103                      zero
1104                      zero
1105                      zero
1106                      zero
1107                      instructionIndex)))))))
1108        (branch
1109          AdamWF32SM86PlanFailed
1110          code
1111          telemetry
1112          .
1113          (constructor
1114            AdamWF32SM86ImageResult
1115            AdamWF32SM86ImageFailed
1116            code
1117            zero
1118            (adamWF32SM86FailureCodeBytes code)
1119            telemetry)))))
1120
1121def adamWF32UnboundedImage =
1122  (lambda unrestricted logicalElements : (family SM86Unsigned32) .
1123    (adamWF32Image (constructor AdamWF32SM86Variant AdamWF32SM86Unbounded) logicalElements))
1124
1125def adamWF32BoundedImage =
1126  (lambda unrestricted logicalElements : (family SM86Unsigned32) .
1127    (adamWF32Image (constructor AdamWF32SM86Variant AdamWF32SM86Bounded) logicalElements))