1module Realization.Nvidia.SM86.ElementwiseVectorSM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.Program
8import Accelerator.SM86.Types
9import Data.SHA256Digest
10import Std.Natural
11import Std.Byte
12
13family ElementwiseVectorSM86Kind : Type 0
14constructor ElementwiseVectorSM86Fill
15constructor ElementwiseVectorSM86Copy
16constructor ElementwiseVectorSM86Add
17constructor ElementwiseVectorSM86Fanout
18
19end-family
20
21family ElementwiseVectorSM86FailureCode : Type 0
22constructor ElementwiseVectorSM86ElementCountZero
23constructor ElementwiseVectorSM86ElementCountMisaligned
24constructor ElementwiseVectorSM86InstructionCountMismatch
25constructor ElementwiseVectorSM86EncodingFailed
26constructor ElementwiseVectorSM86IdentityInvalid
27
28end-family
29
30family ElementwiseVectorSM86Telemetry : Type 0
31constructor ElementwiseVectorSM86TelemetryValue
32field unrestricted elementwiseVectorTelemetryKind : (family ElementwiseVectorSM86Kind)
33field unrestricted elementwiseVectorTelemetryExpectedInstructions : Nat
34field unrestricted elementwiseVectorTelemetryActualInstructions : Nat
35field unrestricted elementwiseVectorTelemetryRegisters : Nat
36field unrestricted elementwiseVectorTelemetryElements : Nat
37field unrestricted elementwiseVectorTelemetryGridX : Nat
38field unrestricted elementwiseVectorTelemetryBlockX : Nat
39field unrestricted elementwiseVectorTelemetryInputs : Nat
40field unrestricted elementwiseVectorTelemetryOutputs : Nat
41field unrestricted elementwiseVectorTelemetryScalarBindings : Nat
42field unrestricted elementwiseVectorTelemetryHostOperations : Nat
43field unrestricted elementwiseVectorTelemetryEncodedBytes : Nat
44field unrestricted elementwiseVectorTelemetryEncodedFields : Nat
45field unrestricted elementwiseVectorTelemetryEncodedBits : Nat
46constructor ElementwiseVectorSM86TelemetryRejected
47field unrestricted elementwiseVectorTelemetryFailure : (family ElementwiseVectorSM86FailureCode)
48field unrestricted elementwiseVectorTelemetryFailureOrdinal : Nat
49
50end-family
51
52family ElementwiseVectorSM86Plan : Type 0
53constructor ElementwiseVectorSM86PlanValue
54field unrestricted elementwiseVectorPlanKind : (family ElementwiseVectorSM86Kind)
55field unrestricted elementwiseVectorPlanElements : Nat
56field unrestricted elementwiseVectorPlanProgram : (family SM86Program)
57field unrestricted elementwiseVectorPlanTelemetry : (family ElementwiseVectorSM86Telemetry)
58
59end-family
60
61family ElementwiseVectorSM86PlanResult : Type 0
62constructor ElementwiseVectorSM86PlanReady
63field unrestricted elementwiseVectorReadyPlan : (family ElementwiseVectorSM86Plan)
64constructor ElementwiseVectorSM86PlanFailed
65field unrestricted elementwiseVectorPlanFailure : (family ElementwiseVectorSM86FailureCode)
66field unrestricted elementwiseVectorPlanFailureTelemetry : (family ElementwiseVectorSM86Telemetry)
67
68end-family
69
70family ElementwiseVectorSM86ImageResult : Type 0
71constructor ElementwiseVectorSM86ImageReady
72field unrestricted elementwiseVectorImageKind : (family ElementwiseVectorSM86Kind)
73field unrestricted elementwiseVectorImageBytes : Bytes
74field unrestricted elementwiseVectorImageSHA256 : Bytes
75field unrestricted elementwiseVectorImageTelemetry : (family ElementwiseVectorSM86Telemetry)
76constructor ElementwiseVectorSM86ImageFailed
77field unrestricted elementwiseVectorImageFailure : (family ElementwiseVectorSM86FailureCode)
78field unrestricted elementwiseVectorImageFailureInstruction : Nat
79field unrestricted elementwiseVectorImageFailureDetail : Bytes
80field unrestricted elementwiseVectorImageFailureTelemetry : (family ElementwiseVectorSM86Telemetry)
81
82end-family
83
84def elementwiseVectorNaturalNine =
85 (byte-to-nat (byte 9))
86
87def elementwiseVectorNaturalTen =
88 (byte-to-nat (byte 10))
89
90def elementwiseVectorNaturalTwelve =
91 (byte-to-nat (byte 12))
92
93def elementwiseVectorNaturalThirteen =
94 (byte-to-nat (byte 13))
95
96def elementwiseVectorNaturalSixteen =
97 (byte-to-nat (byte 16))
98
99def elementwiseVectorNaturalTwentyFour =
100 (byte-to-nat (byte 24))
101
102def elementwiseVectorBlockX =
103 byteNaturalTwoHundredFiftySix
104
105def elementwiseVectorUnsigned32 =
106 (lambda unrestricted b0 : Byte .
107 (lambda unrestricted b1 : Byte .
108 (lambda unrestricted b2 : Byte .
109 (lambda unrestricted b3 : Byte . (sm86Unsigned32 b0 b1 b2 b3)))))
110
111def elementwiseVectorZero =
112 (elementwiseVectorUnsigned32 (byte 0) (byte 0) (byte 0) (byte 0))
113
114def elementwiseVectorFour =
115 (elementwiseVectorUnsigned32 (byte 4) (byte 0) (byte 0) (byte 0))
116
117def elementwiseVectorTwoHundredFiftySix =
118 (elementwiseVectorUnsigned32 (byte 0) (byte 1) (byte 0) (byte 0))
119
120def elementwiseVectorConstantBase =
121 (elementwiseVectorUnsigned32 (byte 40) (byte 0) (byte 0) (byte 0))
122
123def elementwiseVectorOutput0 =
124 (elementwiseVectorUnsigned32 (byte 96) (byte 1) (byte 0) (byte 0))
125
126def elementwiseVectorInput0 =
127 (elementwiseVectorUnsigned32 (byte 104) (byte 1) (byte 0) (byte 0))
128
129def elementwiseVectorInput1OrOutput1 =
130 (elementwiseVectorUnsigned32 (byte 112) (byte 1) (byte 0) (byte 0))
131
132def elementwiseVectorScalar0 =
133 (elementwiseVectorUnsigned32 (byte 144) (byte 1) (byte 0) (byte 0))
134
135def elementwiseVectorRegister =
136 (lambda unrestricted value : Byte . (sm86Register value))
137
138def elementwiseVectorInstruction =
139 (lambda unrestricted body : (family SM86InstructionBody) .
140 (constructor
141 SM86Instruction
142 SM86InstructionValue
143 (constructor SM86InstructionGuard SM86InstructionAlways)
144 body))
145
146def elementwiseVectorNext =
147 (lambda unrestricted body : (family SM86InstructionBody) .
148 (lambda unrestricted tail : (family SM86Program) .
149 (constructor SM86Program SM86ProgramNext (elementwiseVectorInstruction body) tail)))
150
151def elementwiseVectorEnd =
152 (constructor SM86Program SM86ProgramEnd)
153
154def elementwiseVectorSet0 =
155 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
156
157def elementwiseVectorSet1 =
158 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))
159
160def elementwiseVectorSet2 =
161 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))
162
163def elementwiseVectorWait0 =
164 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))
165
166def elementwiseVectorWait2 =
167 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2))
168
169def elementwiseVectorWaitSpecials : (family SM86Control) =
170 (constructor
171 SM86Control
172 SM86ControlValue
173 (byte 7)
174 (constructor SM86YieldMode SM86Continue)
175 (constructor SM86Barrier SM86BarrierNone)
176 (constructor SM86Barrier SM86BarrierNone)
177 (byte 3)
178 (byte 0))
179
180def elementwiseVectorWaitInputs : (family SM86Control) =
181 (constructor
182 SM86Control
183 SM86ControlValue
184 (byte 7)
185 (constructor SM86YieldMode SM86Continue)
186 (constructor SM86Barrier SM86BarrierNone)
187 (constructor SM86Barrier SM86BarrierNone)
188 (byte 3)
189 (byte 0))
190
191def elementwiseVectorFillPrologueControl : (family SM86Control) =
192 (constructor
193 SM86Control
194 SM86ControlValue
195 (byte 2)
196 (constructor SM86YieldMode SM86Yield)
197 (constructor SM86Barrier SM86BarrierNone)
198 (constructor SM86Barrier SM86BarrierNone)
199 (byte 0)
200 (byte 0))
201
202def elementwiseVectorFillProgram : (family SM86Program) =
203 (elementwiseVectorNext
204 (constructor
205 SM86InstructionBody
206 SM86MoveConstant
207 (elementwiseVectorRegister (byte 1))
208 (byte 0)
209 elementwiseVectorConstantBase
210 elementwiseVectorFillPrologueControl)
211 (elementwiseVectorNext
212 (constructor
213 SM86InstructionBody
214 SM86SpecialToRegister
215 (elementwiseVectorRegister (byte 0))
216 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
217 elementwiseVectorSet0)
218 (elementwiseVectorNext
219 (constructor
220 SM86InstructionBody
221 SM86MoveImmediate
222 (elementwiseVectorRegister (byte 3))
223 elementwiseVectorFour
224 elementwiseVectorWait0)
225 (elementwiseVectorNext
226 (constructor
227 SM86InstructionBody
228 SM86SpecialToRegister
229 (elementwiseVectorRegister (byte 2))
230 (constructor SM86SpecialRegister SM86ThreadIdX)
231 elementwiseVectorSet0)
232 (elementwiseVectorNext
233 (constructor
234 SM86InstructionBody
235 SM86IntegerMultiplyAddConstant
236 (elementwiseVectorRegister (byte 0))
237 (elementwiseVectorRegister (byte 0))
238 (byte 0)
239 elementwiseVectorZero
240 (elementwiseVectorRegister (byte 2))
241 elementwiseVectorWait0)
242 (elementwiseVectorNext
243 (constructor
244 SM86InstructionBody
245 SM86MoveConstant
246 (elementwiseVectorRegister (byte 4))
247 (byte 0)
248 elementwiseVectorScalar0
249 sm86SafeControl)
250 (elementwiseVectorNext
251 (constructor
252 SM86InstructionBody
253 SM86IntegerMultiplyAddWideConstant
254 (elementwiseVectorRegister (byte 6))
255 (elementwiseVectorRegister (byte 0))
256 (elementwiseVectorRegister (byte 3))
257 (byte 0)
258 elementwiseVectorOutput0
259 sm86SafeControl)
260 (elementwiseVectorNext
261 (constructor
262 SM86InstructionBody
263 SM86StoreGlobal
264 (elementwiseVectorRegister (byte 6))
265 (elementwiseVectorRegister (byte 4))
266 elementwiseVectorZero
267 sm86SafeControl)
268 (elementwiseVectorNext
269 (constructor SM86InstructionBody SM86Exit sm86BranchControl)
270 elementwiseVectorEnd)))))))))
271
272def elementwiseVectorCopyProgram : (family SM86Program) =
273 (elementwiseVectorNext
274 (constructor
275 SM86InstructionBody
276 SM86MoveConstant
277 (elementwiseVectorRegister (byte 1))
278 (byte 0)
279 elementwiseVectorConstantBase
280 sm86SafeControl)
281 (elementwiseVectorNext
282 (constructor
283 SM86InstructionBody
284 SM86SpecialToRegister
285 (elementwiseVectorRegister (byte 0))
286 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
287 elementwiseVectorSet0)
288 (elementwiseVectorNext
289 (constructor
290 SM86InstructionBody
291 SM86SpecialToRegister
292 (elementwiseVectorRegister (byte 2))
293 (constructor SM86SpecialRegister SM86ThreadIdX)
294 elementwiseVectorSet1)
295 (elementwiseVectorNext
296 (constructor
297 SM86InstructionBody
298 SM86IntegerMultiplyAddImmediate
299 (elementwiseVectorRegister (byte 3))
300 (elementwiseVectorRegister (byte 0))
301 elementwiseVectorTwoHundredFiftySix
302 (elementwiseVectorRegister (byte 2))
303 elementwiseVectorWaitSpecials)
304 (elementwiseVectorNext
305 (constructor
306 SM86InstructionBody
307 SM86MoveImmediate
308 (elementwiseVectorRegister (byte 4))
309 elementwiseVectorFour
310 sm86SafeControl)
311 (elementwiseVectorNext
312 (constructor
313 SM86InstructionBody
314 SM86IntegerMultiplyAddWideConstant
315 (elementwiseVectorRegister (byte 6))
316 (elementwiseVectorRegister (byte 3))
317 (elementwiseVectorRegister (byte 4))
318 (byte 0)
319 elementwiseVectorInput0
320 sm86SafeControl)
321 (elementwiseVectorNext
322 (constructor
323 SM86InstructionBody
324 SM86LoadGlobal
325 (elementwiseVectorRegister (byte 12))
326 (elementwiseVectorRegister (byte 6))
327 elementwiseVectorZero
328 elementwiseVectorSet2)
329 (elementwiseVectorNext
330 (constructor
331 SM86InstructionBody
332 SM86IntegerMultiplyAddWideConstant
333 (elementwiseVectorRegister (byte 8))
334 (elementwiseVectorRegister (byte 3))
335 (elementwiseVectorRegister (byte 4))
336 (byte 0)
337 elementwiseVectorOutput0
338 sm86SafeControl)
339 (elementwiseVectorNext
340 (constructor
341 SM86InstructionBody
342 SM86StoreGlobal
343 (elementwiseVectorRegister (byte 8))
344 (elementwiseVectorRegister (byte 12))
345 elementwiseVectorZero
346 elementwiseVectorWait2)
347 (elementwiseVectorNext
348 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
349 elementwiseVectorEnd))))))))))
350
351def elementwiseVectorAddProgram : (family SM86Program) =
352 (elementwiseVectorNext
353 (constructor
354 SM86InstructionBody
355 SM86MoveConstant
356 (elementwiseVectorRegister (byte 1))
357 (byte 0)
358 elementwiseVectorConstantBase
359 sm86SafeControl)
360 (elementwiseVectorNext
361 (constructor
362 SM86InstructionBody
363 SM86SpecialToRegister
364 (elementwiseVectorRegister (byte 0))
365 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
366 elementwiseVectorSet0)
367 (elementwiseVectorNext
368 (constructor
369 SM86InstructionBody
370 SM86SpecialToRegister
371 (elementwiseVectorRegister (byte 2))
372 (constructor SM86SpecialRegister SM86ThreadIdX)
373 elementwiseVectorSet1)
374 (elementwiseVectorNext
375 (constructor
376 SM86InstructionBody
377 SM86IntegerMultiplyAddImmediate
378 (elementwiseVectorRegister (byte 0))
379 (elementwiseVectorRegister (byte 0))
380 elementwiseVectorTwoHundredFiftySix
381 (elementwiseVectorRegister (byte 2))
382 elementwiseVectorWaitSpecials)
383 (elementwiseVectorNext
384 (constructor
385 SM86InstructionBody
386 SM86MoveImmediate
387 (elementwiseVectorRegister (byte 3))
388 elementwiseVectorFour
389 sm86SafeControl)
390 (elementwiseVectorNext
391 (constructor
392 SM86InstructionBody
393 SM86IntegerMultiplyAddWideConstant
394 (elementwiseVectorRegister (byte 6))
395 (elementwiseVectorRegister (byte 0))
396 (elementwiseVectorRegister (byte 3))
397 (byte 0)
398 elementwiseVectorInput0
399 sm86SafeControl)
400 (elementwiseVectorNext
401 (constructor
402 SM86InstructionBody
403 SM86LoadGlobal
404 (elementwiseVectorRegister (byte 8))
405 (elementwiseVectorRegister (byte 6))
406 elementwiseVectorZero
407 elementwiseVectorSet0)
408 (elementwiseVectorNext
409 (constructor
410 SM86InstructionBody
411 SM86IntegerMultiplyAddWideConstant
412 (elementwiseVectorRegister (byte 10))
413 (elementwiseVectorRegister (byte 0))
414 (elementwiseVectorRegister (byte 3))
415 (byte 0)
416 elementwiseVectorInput1OrOutput1
417 sm86SafeControl)
418 (elementwiseVectorNext
419 (constructor
420 SM86InstructionBody
421 SM86LoadGlobal
422 (elementwiseVectorRegister (byte 12))
423 (elementwiseVectorRegister (byte 10))
424 elementwiseVectorZero
425 elementwiseVectorSet1)
426 (elementwiseVectorNext
427 (constructor
428 SM86InstructionBody
429 SM86IntegerMultiplyAddWideConstant
430 (elementwiseVectorRegister (byte 14))
431 (elementwiseVectorRegister (byte 0))
432 (elementwiseVectorRegister (byte 3))
433 (byte 0)
434 elementwiseVectorOutput0
435 sm86SafeControl)
436 (elementwiseVectorNext
437 (constructor
438 SM86InstructionBody
439 SM86FloatAdd
440 (elementwiseVectorRegister (byte 16))
441 (elementwiseVectorRegister (byte 8))
442 (elementwiseVectorRegister (byte 12))
443 elementwiseVectorWaitInputs)
444 (elementwiseVectorNext
445 (constructor
446 SM86InstructionBody
447 SM86StoreGlobal
448 (elementwiseVectorRegister (byte 14))
449 (elementwiseVectorRegister (byte 16))
450 elementwiseVectorZero
451 sm86SafeControl)
452 (elementwiseVectorNext
453 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
454 elementwiseVectorEnd)))))))))))))
455
456def elementwiseVectorFanoutProgram : (family SM86Program) =
457 (elementwiseVectorNext
458 (constructor
459 SM86InstructionBody
460 SM86MoveConstant
461 (elementwiseVectorRegister (byte 1))
462 (byte 0)
463 elementwiseVectorConstantBase
464 sm86SafeControl)
465 (elementwiseVectorNext
466 (constructor
467 SM86InstructionBody
468 SM86SpecialToRegister
469 (elementwiseVectorRegister (byte 0))
470 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
471 elementwiseVectorSet0)
472 (elementwiseVectorNext
473 (constructor
474 SM86InstructionBody
475 SM86SpecialToRegister
476 (elementwiseVectorRegister (byte 2))
477 (constructor SM86SpecialRegister SM86ThreadIdX)
478 elementwiseVectorSet1)
479 (elementwiseVectorNext
480 (constructor
481 SM86InstructionBody
482 SM86IntegerMultiplyAddImmediate
483 (elementwiseVectorRegister (byte 3))
484 (elementwiseVectorRegister (byte 0))
485 elementwiseVectorTwoHundredFiftySix
486 (elementwiseVectorRegister (byte 2))
487 elementwiseVectorWaitSpecials)
488 (elementwiseVectorNext
489 (constructor
490 SM86InstructionBody
491 SM86MoveImmediate
492 (elementwiseVectorRegister (byte 4))
493 elementwiseVectorFour
494 sm86SafeControl)
495 (elementwiseVectorNext
496 (constructor
497 SM86InstructionBody
498 SM86IntegerMultiplyAddWideConstant
499 (elementwiseVectorRegister (byte 6))
500 (elementwiseVectorRegister (byte 3))
501 (elementwiseVectorRegister (byte 4))
502 (byte 0)
503 elementwiseVectorInput0
504 sm86SafeControl)
505 (elementwiseVectorNext
506 (constructor
507 SM86InstructionBody
508 SM86LoadGlobal
509 (elementwiseVectorRegister (byte 12))
510 (elementwiseVectorRegister (byte 6))
511 elementwiseVectorZero
512 elementwiseVectorSet2)
513 (elementwiseVectorNext
514 (constructor
515 SM86InstructionBody
516 SM86IntegerMultiplyAddWideConstant
517 (elementwiseVectorRegister (byte 8))
518 (elementwiseVectorRegister (byte 3))
519 (elementwiseVectorRegister (byte 4))
520 (byte 0)
521 elementwiseVectorOutput0
522 sm86SafeControl)
523 (elementwiseVectorNext
524 (constructor
525 SM86InstructionBody
526 SM86IntegerMultiplyAddWideConstant
527 (elementwiseVectorRegister (byte 10))
528 (elementwiseVectorRegister (byte 3))
529 (elementwiseVectorRegister (byte 4))
530 (byte 0)
531 elementwiseVectorInput1OrOutput1
532 sm86SafeControl)
533 (elementwiseVectorNext
534 (constructor
535 SM86InstructionBody
536 SM86StoreGlobal
537 (elementwiseVectorRegister (byte 8))
538 (elementwiseVectorRegister (byte 12))
539 elementwiseVectorZero
540 elementwiseVectorWait2)
541 (elementwiseVectorNext
542 (constructor
543 SM86InstructionBody
544 SM86StoreGlobal
545 (elementwiseVectorRegister (byte 10))
546 (elementwiseVectorRegister (byte 12))
547 elementwiseVectorZero
548 sm86SafeControl)
549 (elementwiseVectorNext
550 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
551 elementwiseVectorEnd))))))))))))
552
553def elementwiseVectorProgram =
554 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
555 (eliminate
556 ElementwiseVectorSM86Kind
557 (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . (family SM86Program))
558 kind
559 (branch ElementwiseVectorSM86Fill . elementwiseVectorFillProgram)
560 (branch ElementwiseVectorSM86Copy . elementwiseVectorCopyProgram)
561 (branch ElementwiseVectorSM86Add . elementwiseVectorAddProgram)
562 (branch ElementwiseVectorSM86Fanout . elementwiseVectorFanoutProgram)))
563
564def elementwiseVectorExpectedInstructions =
565 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
566 (eliminate
567 ElementwiseVectorSM86Kind
568 (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
569 kind
570 (branch ElementwiseVectorSM86Fill . elementwiseVectorNaturalNine)
571 (branch ElementwiseVectorSM86Copy . elementwiseVectorNaturalTen)
572 (branch ElementwiseVectorSM86Add . elementwiseVectorNaturalThirteen)
573 (branch ElementwiseVectorSM86Fanout . elementwiseVectorNaturalTwelve)))
574
575def elementwiseVectorRegisterCount =
576 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
577 (eliminate
578 ElementwiseVectorSM86Kind
579 (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
580 kind
581 (branch ElementwiseVectorSM86Fill . elementwiseVectorNaturalSixteen)
582 (branch ElementwiseVectorSM86Copy . elementwiseVectorNaturalTwentyFour)
583 (branch ElementwiseVectorSM86Add . elementwiseVectorNaturalTwentyFour)
584 (branch ElementwiseVectorSM86Fanout . elementwiseVectorNaturalTwentyFour)))
585
586def elementwiseVectorInputCount =
587 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
588 (eliminate
589 ElementwiseVectorSM86Kind
590 (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
591 kind
592 (branch ElementwiseVectorSM86Fill . zero)
593 (branch ElementwiseVectorSM86Copy . (succ zero))
594 (branch ElementwiseVectorSM86Add . (byte-to-nat (byte 2)))
595 (branch ElementwiseVectorSM86Fanout . (succ zero))))
596
597def elementwiseVectorOutputCount =
598 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
599 (eliminate
600 ElementwiseVectorSM86Kind
601 (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
602 kind
603 (branch ElementwiseVectorSM86Fill . (succ zero))
604 (branch ElementwiseVectorSM86Copy . (succ zero))
605 (branch ElementwiseVectorSM86Add . (succ zero))
606 (branch ElementwiseVectorSM86Fanout . (byte-to-nat (byte 2)))))
607
608def elementwiseVectorScalarCount =
609 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
610 (eliminate
611 ElementwiseVectorSM86Kind
612 (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
613 kind
614 (branch ElementwiseVectorSM86Fill . (succ zero))
615 (branch ElementwiseVectorSM86Copy . zero)
616 (branch ElementwiseVectorSM86Add . zero)
617 (branch ElementwiseVectorSM86Fanout . zero)))
618
619def elementwiseVectorFailureCodeBytes =
620 (lambda unrestricted code : (family ElementwiseVectorSM86FailureCode) .
621 (eliminate
622 ElementwiseVectorSM86FailureCode
623 (lambda unrestricted current : (family ElementwiseVectorSM86FailureCode) . Bytes)
624 code
625 (branch ElementwiseVectorSM86ElementCountZero . b"ALPHA-SM86-VEC-001")
626 (branch ElementwiseVectorSM86ElementCountMisaligned . b"ALPHA-SM86-VEC-002")
627 (branch ElementwiseVectorSM86InstructionCountMismatch . b"ALPHA-SM86-VEC-003")
628 (branch ElementwiseVectorSM86EncodingFailed . b"ALPHA-SM86-VEC-004")
629 (branch ElementwiseVectorSM86IdentityInvalid . b"ALPHA-SM86-VEC-005")))
630
631def elementwiseVectorRejectedTelemetry =
632 (lambda unrestricted code : (family ElementwiseVectorSM86FailureCode) .
633 (lambda unrestricted ordinal : Nat .
634 (constructor
635 ElementwiseVectorSM86Telemetry
636 ElementwiseVectorSM86TelemetryRejected
637 code
638 ordinal)))
639
640def elementwiseVectorPlan =
641 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
642 (lambda unrestricted elements : Nat .
643 (nat-eliminate
644 (lambda unrestricted nonzero : Nat . (family ElementwiseVectorSM86PlanResult))
645 (constructor
646 ElementwiseVectorSM86PlanResult
647 ElementwiseVectorSM86PlanFailed
648 (constructor ElementwiseVectorSM86FailureCode ElementwiseVectorSM86ElementCountZero)
649 (elementwiseVectorRejectedTelemetry
650 (constructor ElementwiseVectorSM86FailureCode ElementwiseVectorSM86ElementCountZero)
651 zero))
652 (lambda unrestricted nonzeroPredecessor : Nat .
653 (lambda unrestricted nonzeroInduction : (family ElementwiseVectorSM86PlanResult) .
654 (nat-eliminate
655 (lambda unrestricted aligned : Nat . (family ElementwiseVectorSM86PlanResult))
656 (constructor
657 ElementwiseVectorSM86PlanResult
658 ElementwiseVectorSM86PlanFailed
659 (constructor
660 ElementwiseVectorSM86FailureCode
661 ElementwiseVectorSM86ElementCountMisaligned)
662 (elementwiseVectorRejectedTelemetry
663 (constructor
664 ElementwiseVectorSM86FailureCode
665 ElementwiseVectorSM86ElementCountMisaligned)
666 elements))
667 (lambda unrestricted alignedPredecessor : Nat .
668 (lambda unrestricted alignedInduction : (family ElementwiseVectorSM86PlanResult) .
669 (app
670 (lambda unrestricted program : (family SM86Program) .
671 (app
672 (lambda unrestricted actual : Nat .
673 (nat-eliminate
674 (lambda unrestricted countValid : Nat .
675 (family ElementwiseVectorSM86PlanResult))
676 (constructor
677 ElementwiseVectorSM86PlanResult
678 ElementwiseVectorSM86PlanFailed
679 (constructor
680 ElementwiseVectorSM86FailureCode
681 ElementwiseVectorSM86InstructionCountMismatch)
682 (elementwiseVectorRejectedTelemetry
683 (constructor
684 ElementwiseVectorSM86FailureCode
685 ElementwiseVectorSM86InstructionCountMismatch)
686 actual))
687 (lambda unrestricted countPredecessor : Nat .
688 (lambda unrestricted countInduction : (family ElementwiseVectorSM86PlanResult) .
689 (constructor
690 ElementwiseVectorSM86PlanResult
691 ElementwiseVectorSM86PlanReady
692 (constructor
693 ElementwiseVectorSM86Plan
694 ElementwiseVectorSM86PlanValue
695 kind
696 elements
697 program
698 (constructor
699 ElementwiseVectorSM86Telemetry
700 ElementwiseVectorSM86TelemetryValue
701 kind
702 (elementwiseVectorExpectedInstructions kind)
703 actual
704 (elementwiseVectorRegisterCount kind)
705 elements
706 (naturalDivideUnchecked elements elementwiseVectorBlockX)
707 elementwiseVectorBlockX
708 (elementwiseVectorInputCount kind)
709 (elementwiseVectorOutputCount kind)
710 (elementwiseVectorScalarCount kind)
711 zero
712 zero
713 zero
714 zero)))))
715 (naturalEqual actual (elementwiseVectorExpectedInstructions kind))))
716 (sm86ProgramCount program)))
717 (elementwiseVectorProgram kind))))
718 (naturalIsZero (naturalModuloUnchecked elements elementwiseVectorBlockX)))))
719 (naturalNonzero elements))))
720
721def elementwiseVectorImage =
722 (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
723 (lambda unrestricted elements : Nat .
724 (eliminate
725 ElementwiseVectorSM86PlanResult
726 (lambda unrestricted current : (family ElementwiseVectorSM86PlanResult) .
727 (family ElementwiseVectorSM86ImageResult))
728 (elementwiseVectorPlan kind elements)
729 (branch
730 ElementwiseVectorSM86PlanReady
731 plan
732 .
733 (eliminate
734 ElementwiseVectorSM86Plan
735 (lambda unrestricted current : (family ElementwiseVectorSM86Plan) .
736 (family ElementwiseVectorSM86ImageResult))
737 plan
738 (branch
739 ElementwiseVectorSM86PlanValue
740 plannedKind
741 plannedElements
742 program
743 telemetry
744 .
745 (eliminate
746 SM86ProgramEncodingResult
747 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
748 (family ElementwiseVectorSM86ImageResult))
749 (sm86EncodeProgram program)
750 (branch
751 SM86ProgramEncodingSucceeded
752 image
753 encodingTelemetry
754 .
755 (app
756 (lambda unrestricted identity : Bytes .
757 (nat-eliminate
758 (lambda unrestricted valid : Nat .
759 (family ElementwiseVectorSM86ImageResult))
760 (constructor
761 ElementwiseVectorSM86ImageResult
762 ElementwiseVectorSM86ImageFailed
763 (constructor
764 ElementwiseVectorSM86FailureCode
765 ElementwiseVectorSM86IdentityInvalid)
766 zero
767 (elementwiseVectorFailureCodeBytes
768 (constructor
769 ElementwiseVectorSM86FailureCode
770 ElementwiseVectorSM86IdentityInvalid))
771 telemetry)
772 (lambda unrestricted validPredecessor : Nat .
773 (lambda unrestricted validInduction : (family ElementwiseVectorSM86ImageResult) .
774 (eliminate
775 SM86ProgramEncodingTelemetry
776 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
777 (family ElementwiseVectorSM86ImageResult))
778 encodingTelemetry
779 (branch
780 SM86ProgramEncodingTelemetryValue
781 instructions
782 bytes
783 fields
784 bits
785 highest
786 .
787 (constructor
788 ElementwiseVectorSM86ImageResult
789 ElementwiseVectorSM86ImageReady
790 plannedKind
791 image
792 identity
793 (constructor
794 ElementwiseVectorSM86Telemetry
795 ElementwiseVectorSM86TelemetryValue
796 plannedKind
797 (elementwiseVectorExpectedInstructions plannedKind)
798 instructions
799 (elementwiseVectorRegisterCount plannedKind)
800 plannedElements
801 (naturalDivideUnchecked plannedElements elementwiseVectorBlockX)
802 elementwiseVectorBlockX
803 (elementwiseVectorInputCount plannedKind)
804 (elementwiseVectorOutputCount plannedKind)
805 (elementwiseVectorScalarCount plannedKind)
806 zero
807 bytes
808 fields
809 bits))))))
810 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
811 (sha256HexBytesOrEmpty (sha256Hex image))))
812 (branch
813 SM86ProgramEncodingFailed
814 index
815 failure
816 encodingTelemetry
817 .
818 (constructor
819 ElementwiseVectorSM86ImageResult
820 ElementwiseVectorSM86ImageFailed
821 (constructor
822 ElementwiseVectorSM86FailureCode
823 ElementwiseVectorSM86EncodingFailed)
824 index
825 (sm86InstructionEncodingStableCode failure)
826 telemetry))))))
827 (branch
828 ElementwiseVectorSM86PlanFailed
829 code
830 telemetry
831 .
832 (constructor
833 ElementwiseVectorSM86ImageResult
834 ElementwiseVectorSM86ImageFailed
835 code
836 zero
837 (elementwiseVectorFailureCodeBytes code)
838 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.