Realization.Nvidia.SM86.GreedyArgmaxSM86

1module Realization.Nvidia.SM86.GreedyArgmaxSM86
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 Accelerator.SM86.NumericSemantics
12
13family GreedyArgmaxSM86ExecutionContract : Type 0
14constructor GreedyArgmaxSM86NativeOnly
15
16end-family
17
18family GreedyArgmaxSM86FailureCode : Type 0
19constructor GreedyArgmaxSM86VocabularyZero
20constructor GreedyArgmaxSM86VocabularyTooLarge
21constructor GreedyArgmaxSM86InstructionCountMismatch
22constructor GreedyArgmaxSM86EncodedInstructionCountMismatch
23constructor GreedyArgmaxSM86EncodedByteCountMismatch
24constructor GreedyArgmaxSM86RegisterCountMismatch
25constructor GreedyArgmaxSM86SharedByteCountMismatch
26constructor GreedyArgmaxSM86GridCountMismatch
27constructor GreedyArgmaxSM86ThreadCountMismatch
28constructor GreedyArgmaxSM86ImageEncodingFailed
29constructor GreedyArgmaxSM86ImageIdentityFailed
30constructor GreedyArgmaxSM86ImageIdentityLengthInvalid
31constructor GreedyArgmaxSM86HostFallbackDetected
32
33end-family
34
35family GreedyArgmaxSM86Validation : Type 0
36constructor GreedyArgmaxSM86ValidationAccepted
37constructor GreedyArgmaxSM86ValidationRejected
38field unrestricted greedyArgmaxSM86ValidationFailure : (family GreedyArgmaxSM86FailureCode)
39
40end-family
41
42family GreedyArgmaxSM86OutputReceipt : Type 0
43constructor GreedyArgmaxSM86OutputReceiptValue
44field unrestricted greedyArgmaxSM86ReceiptTokenOffset : Nat
45field unrestricted greedyArgmaxSM86ReceiptValidityOffset : Nat
46field unrestricted greedyArgmaxSM86ReceiptWordBytes : Nat
47field unrestricted greedyArgmaxSM86ReceiptValidValue : Nat
48field unrestricted greedyArgmaxSM86ReceiptInvalidValue : Nat
49
50end-family
51
52family GreedyArgmaxSM86ABI : Type 0
53constructor GreedyArgmaxSM86ABIValue
54field unrestricted greedyArgmaxSM86ABIConstantBank : Nat
55field unrestricted greedyArgmaxSM86ABIOutputPointerOffset : Nat
56field unrestricted greedyArgmaxSM86ABILogitsPointerOffset : Nat
57field unrestricted greedyArgmaxSM86ABILogitElementBytes : Nat
58field unrestricted greedyArgmaxSM86ABIReceipt : (family GreedyArgmaxSM86OutputReceipt)
59
60end-family
61
62family GreedyArgmaxSM86Manifest : Type 0
63constructor GreedyArgmaxSM86ManifestValue
64field unrestricted greedyArgmaxSM86ManifestVocabulary : Nat
65field unrestricted greedyArgmaxSM86ManifestFullSlots : Nat
66field unrestricted greedyArgmaxSM86ManifestTailLanes : Nat
67field unrestricted greedyArgmaxSM86ManifestExpectedInstructions : Nat
68field unrestricted greedyArgmaxSM86ManifestExpectedBytes : Nat
69field unrestricted greedyArgmaxSM86ManifestRegisters : Nat
70field unrestricted greedyArgmaxSM86ManifestSharedBytes : Nat
71field unrestricted greedyArgmaxSM86ManifestGridX : Nat
72field unrestricted greedyArgmaxSM86ManifestThreadsPerBlock : Nat
73field unrestricted greedyArgmaxSM86ManifestActiveLogitLoads : Nat
74field unrestricted greedyArgmaxSM86ManifestActiveFiniteChecks : Nat
75field unrestricted greedyArgmaxSM86ManifestInactiveFiniteChecks : Nat
76field unrestricted greedyArgmaxSM86ManifestTailMaskWrites : Nat
77field unrestricted greedyArgmaxSM86ManifestTieReductionStages : Nat
78field unrestricted greedyArgmaxSM86ManifestTokenWrites : Nat
79field unrestricted greedyArgmaxSM86ManifestValidityWrites : Nat
80field unrestricted greedyArgmaxSM86ManifestHostLogitReads : Nat
81field unrestricted greedyArgmaxSM86ManifestHostFallbackOperations : Nat
82field unrestricted greedyArgmaxSM86ManifestABI : (family GreedyArgmaxSM86ABI)
83
84end-family
85
86family GreedyArgmaxSM86Telemetry : Type 0
87constructor GreedyArgmaxSM86TelemetryValue
88field unrestricted greedyArgmaxSM86TelemetryContract : (family GreedyArgmaxSM86ExecutionContract)
89field unrestricted greedyArgmaxSM86TelemetryManifest : (family GreedyArgmaxSM86Manifest)
90field unrestricted greedyArgmaxSM86TelemetryObservedInstructions : Nat
91field unrestricted greedyArgmaxSM86TelemetryObservedBytes : Nat
92field unrestricted greedyArgmaxSM86TelemetryEncodingFields : Nat
93field unrestricted greedyArgmaxSM86TelemetryEncodingBits : Nat
94field unrestricted greedyArgmaxSM86TelemetryHighestEncodedBit : Nat
95field unrestricted greedyArgmaxSM86TelemetryIdentityInputBytes : Nat
96field unrestricted greedyArgmaxSM86TelemetryIdentityOutputBytes : Nat
97field unrestricted greedyArgmaxSM86TelemetryTailValidationSeparated : Nat
98field unrestricted greedyArgmaxSM86TelemetryLowestTokenTieBreak : Nat
99field unrestricted greedyArgmaxSM86TelemetryHostFallbackOperations : Nat
100
101end-family
102
103family GreedyArgmaxSM86Artifact : Type 0
104constructor GreedyArgmaxSM86ArtifactReady
105field unrestricted greedyArgmaxSM86ArtifactProgram : (family SM86Program)
106field unrestricted greedyArgmaxSM86ArtifactImage : Bytes
107field unrestricted greedyArgmaxSM86ArtifactImageSHA256 : Bytes
108field unrestricted greedyArgmaxSM86ArtifactManifest : (family GreedyArgmaxSM86Manifest)
109field unrestricted greedyArgmaxSM86ArtifactEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
110field unrestricted greedyArgmaxSM86ArtifactIdentityTelemetry : (family SHA256DigestTelemetry)
111field unrestricted greedyArgmaxSM86ArtifactTelemetry : (family GreedyArgmaxSM86Telemetry)
112constructor GreedyArgmaxSM86ArtifactFailed
113field unrestricted greedyArgmaxSM86ArtifactFailure : (family GreedyArgmaxSM86FailureCode)
114field unrestricted greedyArgmaxSM86ArtifactFailureOrdinal : Nat
115field unrestricted greedyArgmaxSM86ArtifactFailureDetail : Bytes
116field unrestricted greedyArgmaxSM86ArtifactFailureTelemetry : (family GreedyArgmaxSM86Telemetry)
117
118end-family
119
120def greedyArgmaxSM86N1 =
121  (succ zero)
122
123def greedyArgmaxSM86N2 =
124  (byte-to-nat (byte 2))
125
126def greedyArgmaxSM86N4 =
127  (byte-to-nat (byte 4))
128
129def greedyArgmaxSM86N5 =
130  (byte-to-nat (byte 5))
131
132def greedyArgmaxSM86N7 =
133  (byte-to-nat (byte 7))
134
135def greedyArgmaxSM86N8 =
136  (byte-to-nat (byte 8))
137
138def greedyArgmaxSM86N12 =
139  (byte-to-nat (byte 12))
140
141def greedyArgmaxSM86N16 =
142  (byte-to-nat (byte 16))
143
144def greedyArgmaxSM86N23 =
145  (byte-to-nat (byte 23))
146
147def greedyArgmaxSM86N30 =
148  (byte-to-nat (byte 30))
149
150def greedyArgmaxSM86N31 =
151  (byte-to-nat (byte 31))
152
153def greedyArgmaxSM86N32 =
154  (byte-to-nat (byte 32))
155
156def greedyArgmaxSM86N33 =
157  (byte-to-nat (byte 33))
158
159def greedyArgmaxSM86N64 =
160  (byte-to-nat (byte 64))
161
162def greedyArgmaxSM86N96 =
163  (byte-to-nat (byte 96))
164
165def greedyArgmaxSM86N115 =
166  (byte-to-nat (byte 115))
167
168def greedyArgmaxSM86N251 =
169  (byte-to-nat (byte 251))
170
171def greedyArgmaxSM86N254 =
172  (byte-to-nat (byte 254))
173
174def greedyArgmaxSM86N255 =
175  (byte-to-nat (byte 255))
176
177def greedyArgmaxSM86N256 =
178  (succ greedyArgmaxSM86N255)
179
180def greedyArgmaxSM86N277 =
181  (naturalAdd
182    greedyArgmaxSM86N256
183    (naturalAdd greedyArgmaxSM86N16 greedyArgmaxSM86N5))
184
185def greedyArgmaxSM86N352 =
186  (naturalAdd greedyArgmaxSM86N256 greedyArgmaxSM86N96)
187
188def greedyArgmaxSM86N360 =
189  (naturalAdd greedyArgmaxSM86N352 greedyArgmaxSM86N8)
190
191def greedyArgmaxSM86N12288 =
192  (naturalMultiply (byte-to-nat (byte 48)) greedyArgmaxSM86N256)
193
194def greedyArgmaxSM86N49152 =
195  (naturalMultiply greedyArgmaxSM86N12288 greedyArgmaxSM86N4)
196
197def greedyArgmaxSM86N1717 =
198  (naturalAdd (naturalMultiply (byte-to-nat (byte 48)) greedyArgmaxSM86N30) greedyArgmaxSM86N277)
199
200def greedyArgmaxSM86N27472 =
201  (naturalMultiply greedyArgmaxSM86N1717 greedyArgmaxSM86N16)
202
203def greedyArgmaxSM86N10 =
204  (byte-to-nat (byte 10))
205
206def greedyArgmaxSM86MaximumVocabulary =
207  greedyArgmaxSM86N12288
208
209def greedyArgmaxSM86PromotedVocabulary =
210  greedyArgmaxSM86N12288
211
212def greedyArgmaxSM86PromotedInstructions =
213  greedyArgmaxSM86N1717
214
215def greedyArgmaxSM86PromotedBytes =
216  greedyArgmaxSM86N27472
217
218def greedyArgmaxSM86Registers =
219  greedyArgmaxSM86N32
220
221def greedyArgmaxSM86SharedBytes =
222  greedyArgmaxSM86N96
223
224def greedyArgmaxSM86GridX =
225  greedyArgmaxSM86N1
226
227def greedyArgmaxSM86ThreadsPerBlock =
228  greedyArgmaxSM86N256
229
230def greedyArgmaxSM86InstructionBytes =
231  greedyArgmaxSM86N16
232
233def greedyArgmaxSM86HostLogitReads =
234  zero
235
236def greedyArgmaxSM86HostFallbackOperations =
237  zero
238
239def greedyArgmaxSM86U0 =
240  sm86Unsigned32Zero
241
242def greedyArgmaxSM86U1 =
243  sm86Unsigned32One
244
245def greedyArgmaxSM86U4 =
246  (sm86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))
247
248def greedyArgmaxSM86U7 =
249  (sm86Unsigned32 (byte 7) (byte 0) (byte 0) (byte 0))
250
251def greedyArgmaxSM86U8 =
252  (sm86Unsigned32 (byte 8) (byte 0) (byte 0) (byte 0))
253
254def greedyArgmaxSM86U12 =
255  (sm86Unsigned32 (byte 12) (byte 0) (byte 0) (byte 0))
256
257def greedyArgmaxSM86U31 =
258  (sm86Unsigned32 (byte 31) (byte 0) (byte 0) (byte 0))
259
260def greedyArgmaxSM86U254 =
261  (sm86Unsigned32 (byte 254) (byte 0) (byte 0) (byte 0))
262
263def greedyArgmaxSM86U352 =
264  (sm86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))
265
266def greedyArgmaxSM86U356 =
267  (sm86Unsigned32 (byte 100) (byte 1) (byte 0) (byte 0))
268
269def greedyArgmaxSM86U360 =
270  (sm86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))
271
272def greedyArgmaxSM86UFloatZero =
273  greedyArgmaxSM86U0
274
275def greedyArgmaxSM86UFloatOne =
276  (sm86Unsigned32 (byte 0) (byte 0) (byte 128) (byte 63))
277
278def greedyArgmaxSM86UFloatNegativeInfinity =
279  (sm86Unsigned32 (byte 0) (byte 0) (byte 128) (byte 255))
280
281def greedyArgmaxSM86UAbsMask =
282  (sm86Unsigned32 (byte 255) (byte 255) (byte 255) (byte 127))
283
284def greedyArgmaxSM86UByteMask =
285  (sm86Unsigned32 (byte 255) (byte 0) (byte 0) (byte 0))
286
287def greedyArgmaxSM86UMaximumToken =
288  (sm86Unsigned32 (byte 255) (byte 255) (byte 255) (byte 255))
289
290def greedyArgmaxSM86ByteLoopBackOffset =
291  (sm86Unsigned32 (byte 64) (byte 255) (byte 255) (byte 255))
292
293def greedyArgmaxSM86BackwardBranchDescriptor =
294  (sm86Unsigned32 (byte 255) (byte 255) (byte 131) (byte 3))
295
296def greedyArgmaxSM86R0 =
297  (sm86Register (byte 0))
298
299def greedyArgmaxSM86R1 =
300  (sm86Register (byte 1))
301
302def greedyArgmaxSM86R2 =
303  (sm86Register (byte 2))
304
305def greedyArgmaxSM86R3 =
306  (sm86Register (byte 3))
307
308def greedyArgmaxSM86R4 =
309  (sm86Register (byte 4))
310
311def greedyArgmaxSM86R6 =
312  (sm86Register (byte 6))
313
314def greedyArgmaxSM86R7 =
315  (sm86Register (byte 7))
316
317def greedyArgmaxSM86R8 =
318  (sm86Register (byte 8))
319
320def greedyArgmaxSM86R9 =
321  (sm86Register (byte 9))
322
323def greedyArgmaxSM86R10 =
324  (sm86Register (byte 10))
325
326def greedyArgmaxSM86R11 =
327  (sm86Register (byte 11))
328
329def greedyArgmaxSM86R12 =
330  (sm86Register (byte 12))
331
332def greedyArgmaxSM86R13 =
333  (sm86Register (byte 13))
334
335def greedyArgmaxSM86R14 =
336  (sm86Register (byte 14))
337
338def greedyArgmaxSM86R15 =
339  (sm86Register (byte 15))
340
341def greedyArgmaxSM86R16 =
342  (sm86Register (byte 16))
343
344def greedyArgmaxSM86R17 =
345  (sm86Register (byte 17))
346
347def greedyArgmaxSM86R18 =
348  (sm86Register (byte 18))
349
350def greedyArgmaxSM86R19 =
351  (sm86Register (byte 19))
352
353def greedyArgmaxSM86R20 =
354  (sm86Register (byte 20))
355
356def greedyArgmaxSM86R21 =
357  (sm86Register (byte 21))
358
359def greedyArgmaxSM86R22 =
360  (sm86Register (byte 22))
361
362def greedyArgmaxSM86R23 =
363  (sm86Register (byte 23))
364
365def greedyArgmaxSM86R24 =
366  (sm86Register (byte 24))
367
368def greedyArgmaxSM86R25 =
369  (sm86Register (byte 25))
370
371def greedyArgmaxSM86R26 =
372  (sm86Register (byte 26))
373
374def greedyArgmaxSM86R27 =
375  (sm86Register (byte 27))
376
377def greedyArgmaxSM86R28 =
378  (sm86Register (byte 28))
379
380def greedyArgmaxSM86R29 =
381  (sm86Register (byte 29))
382
383def greedyArgmaxSM86P0 : (family SM86Predicate) =
384  (constructor SM86Predicate SM86Predicate0)
385
386def greedyArgmaxSM86P1 : (family SM86Predicate) =
387  (constructor SM86Predicate SM86Predicate1)
388
389def greedyArgmaxSM86P2 : (family SM86Predicate) =
390  (constructor SM86Predicate SM86Predicate2)
391
392def greedyArgmaxSM86P3 : (family SM86Predicate) =
393  (constructor SM86Predicate SM86Predicate3)
394
395def greedyArgmaxSM86FloatMaximum : (family SM86FloatExtremum) =
396  (constructor SM86FloatExtremum SM86FloatMaximum)
397
398def greedyArgmaxSM86FloatMinimum : (family SM86FloatExtremum) =
399  (constructor SM86FloatExtremum SM86FloatMinimum)
400
401def greedyArgmaxSM86ShuffleButterfly : (family SM86ShuffleMode) =
402  (constructor SM86ShuffleMode SM86ShuffleButterfly)
403
404def greedyArgmaxSM86Set0 =
405  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
406
407def greedyArgmaxSM86Set1 =
408  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))
409
410def greedyArgmaxSM86Set2 =
411  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))
412
413def greedyArgmaxSM86Wait0 =
414  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))
415
416def greedyArgmaxSM86Wait1 =
417  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier1))
418
419def greedyArgmaxSM86Wait2 =
420  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2))
421
422def greedyArgmaxSM86Next =
423  (lambda unrestricted body : (family SM86InstructionBody) .
424    (lambda unrestricted tail : (family SM86Program) .
425      (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))
426
427def greedyArgmaxSM86When =
428  (lambda unrestricted predicate : (family SM86Predicate) .
429    (lambda unrestricted body : (family SM86InstructionBody) .
430      (lambda unrestricted tail : (family SM86Program) .
431        (constructor SM86Program SM86ProgramNext (sm86PredicatedInstruction predicate body) tail))))
432
433def greedyArgmaxSM86WhenNot =
434  (lambda unrestricted predicate : (family SM86Predicate) .
435    (lambda unrestricted body : (family SM86InstructionBody) .
436      (lambda unrestricted tail : (family SM86Program) .
437        (constructor
438          SM86Program
439          SM86ProgramNext
440          (sm86NegatedPredicatedInstruction predicate body)
441          tail))))
442
443def greedyArgmaxSM86Unsigned32FromNatural =
444  (lambda unrestricted value : Nat .
445    (app
446      (lambda unrestricted quotient1 : Nat .
447        (app
448          (lambda unrestricted quotient2 : Nat .
449            (app
450              (lambda unrestricted quotient3 : Nat .
451                (sm86Unsigned32
452                  (nat-to-byte (naturalModuloUnchecked value greedyArgmaxSM86N256))
453                  (nat-to-byte (naturalModuloUnchecked quotient1 greedyArgmaxSM86N256))
454                  (nat-to-byte (naturalModuloUnchecked quotient2 greedyArgmaxSM86N256))
455                  (nat-to-byte (naturalModuloUnchecked quotient3 greedyArgmaxSM86N256))))
456              (naturalDivideUnchecked quotient2 greedyArgmaxSM86N256)))
457          (naturalDivideUnchecked quotient1 greedyArgmaxSM86N256)))
458      (naturalDivideUnchecked value greedyArgmaxSM86N256)))
459
460def greedyArgmaxSM86ReceiptValue =
461  (constructor
462    GreedyArgmaxSM86OutputReceipt
463    GreedyArgmaxSM86OutputReceiptValue
464    zero
465    greedyArgmaxSM86N4
466    greedyArgmaxSM86N4
467    greedyArgmaxSM86N1
468    zero)
469
470def greedyArgmaxSM86ABIValue =
471  (constructor
472    GreedyArgmaxSM86ABI
473    GreedyArgmaxSM86ABIValue
474    zero
475    greedyArgmaxSM86N352
476    greedyArgmaxSM86N360
477    greedyArgmaxSM86N4
478    greedyArgmaxSM86ReceiptValue)
479
480def greedyArgmaxSM86FailureCodeBytes =
481  (lambda unrestricted code : (family GreedyArgmaxSM86FailureCode) .
482    (eliminate
483      GreedyArgmaxSM86FailureCode
484      (lambda unrestricted current : (family GreedyArgmaxSM86FailureCode) . Bytes)
485      code
486      (branch GreedyArgmaxSM86VocabularyZero . b"ALPHA-SM86-GREEDY-001")
487      (branch GreedyArgmaxSM86VocabularyTooLarge . b"ALPHA-SM86-GREEDY-002")
488      (branch GreedyArgmaxSM86InstructionCountMismatch . b"ALPHA-SM86-GREEDY-003")
489      (branch GreedyArgmaxSM86EncodedInstructionCountMismatch . b"ALPHA-SM86-GREEDY-004")
490      (branch GreedyArgmaxSM86EncodedByteCountMismatch . b"ALPHA-SM86-GREEDY-005")
491      (branch GreedyArgmaxSM86RegisterCountMismatch . b"ALPHA-SM86-GREEDY-006")
492      (branch GreedyArgmaxSM86SharedByteCountMismatch . b"ALPHA-SM86-GREEDY-007")
493      (branch GreedyArgmaxSM86GridCountMismatch . b"ALPHA-SM86-GREEDY-008")
494      (branch GreedyArgmaxSM86ThreadCountMismatch . b"ALPHA-SM86-GREEDY-009")
495      (branch GreedyArgmaxSM86ImageEncodingFailed . b"ALPHA-SM86-GREEDY-010")
496      (branch GreedyArgmaxSM86ImageIdentityFailed . b"ALPHA-SM86-GREEDY-011")
497      (branch GreedyArgmaxSM86ImageIdentityLengthInvalid . b"ALPHA-SM86-GREEDY-012")
498      (branch GreedyArgmaxSM86HostFallbackDetected . b"ALPHA-SM86-GREEDY-013")))
499
500def greedyArgmaxSM86ValidateVocabulary =
501  (lambda unrestricted vocabulary : Nat .
502    (nat-eliminate
503      (lambda unrestricted positive : Nat . (family GreedyArgmaxSM86Validation))
504      (constructor
505        GreedyArgmaxSM86Validation
506        GreedyArgmaxSM86ValidationRejected
507        (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyZero))
508      (lambda unrestricted positivePredecessor : Nat .
509        (lambda unrestricted positiveInduction : (family GreedyArgmaxSM86Validation) .
510          (nat-eliminate
511            (lambda unrestricted bounded : Nat . (family GreedyArgmaxSM86Validation))
512            (constructor
513              GreedyArgmaxSM86Validation
514              GreedyArgmaxSM86ValidationRejected
515              (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyTooLarge))
516            (lambda unrestricted boundedPredecessor : Nat .
517              (lambda unrestricted boundedInduction : (family GreedyArgmaxSM86Validation) .
518                (constructor GreedyArgmaxSM86Validation GreedyArgmaxSM86ValidationAccepted)))
519            (naturalLessOrEqual vocabulary greedyArgmaxSM86MaximumVocabulary))))
520      (naturalNonzero vocabulary)))
521
522def greedyArgmaxSM86InitialProgram : (family SM86Program) =
523  (greedyArgmaxSM86Next
524    (constructor
525      SM86InstructionBody
526      SM86SpecialToRegister
527      greedyArgmaxSM86R0
528      (constructor SM86SpecialRegister SM86ThreadIdX)
529      greedyArgmaxSM86Set0)
530    (greedyArgmaxSM86Next
531      (constructor
532        SM86InstructionBody
533        SM86MoveImmediate
534        greedyArgmaxSM86R4
535        greedyArgmaxSM86U4
536        greedyArgmaxSM86Wait0)
537      (greedyArgmaxSM86Next
538        (constructor
539          SM86InstructionBody
540          SM86MoveImmediate
541          greedyArgmaxSM86R7
542          greedyArgmaxSM86UFloatNegativeInfinity
543          sm86SafeControl)
544        (greedyArgmaxSM86Next
545          (constructor
546            SM86InstructionBody
547            SM86MoveImmediate
548            greedyArgmaxSM86R8
549            greedyArgmaxSM86UMaximumToken
550            sm86SafeControl)
551          (greedyArgmaxSM86Next
552            (constructor
553              SM86InstructionBody
554              SM86MoveImmediate
555              greedyArgmaxSM86R9
556              greedyArgmaxSM86UAbsMask
557              sm86SafeControl)
558            (greedyArgmaxSM86Next
559              (constructor
560                SM86InstructionBody
561                SM86MoveImmediate
562                greedyArgmaxSM86R12
563                greedyArgmaxSM86UFloatZero
564                sm86SafeControl)
565              (greedyArgmaxSM86Next
566                (constructor
567                  SM86InstructionBody
568                  SM86MoveImmediate
569                  greedyArgmaxSM86R11
570                  greedyArgmaxSM86UByteMask
571                  sm86SafeControl)
572                sm86ProgramEmpty)))))))
573
574def greedyArgmaxSM86ValidateCandidateProgram : (family SM86Program) =
575  (greedyArgmaxSM86Next
576    (constructor
577      SM86InstructionBody
578      SM86ShiftRightImmediate
579      greedyArgmaxSM86R14
580      greedyArgmaxSM86R10
581      (byte 23)
582      sm86SafeControl)
583    (greedyArgmaxSM86Next
584      (constructor
585        SM86InstructionBody
586        SM86LogicThreeInputTruthTable
587        greedyArgmaxSM86R14
588        greedyArgmaxSM86R14
589        greedyArgmaxSM86R11
590        (byte 192)
591        sm86SafeControl)
592      (greedyArgmaxSM86Next
593        (constructor
594          SM86InstructionBody
595          SM86PredicateGreaterThanImmediate
596          greedyArgmaxSM86P1
597          greedyArgmaxSM86R14
598          greedyArgmaxSM86U254
599          sm86SafeControl)
600        (greedyArgmaxSM86Next
601          (constructor
602            SM86InstructionBody
603            SM86MoveImmediate
604            greedyArgmaxSM86R13
605            greedyArgmaxSM86UFloatZero
606            sm86SafeControl)
607          (greedyArgmaxSM86When
608            greedyArgmaxSM86P1
609            (constructor
610              SM86InstructionBody
611              SM86MoveImmediate
612              greedyArgmaxSM86R13
613              greedyArgmaxSM86UFloatOne
614              sm86SafeControl)
615            (greedyArgmaxSM86Next
616              (constructor
617                SM86InstructionBody
618                SM86FloatAdd
619                greedyArgmaxSM86R12
620                greedyArgmaxSM86R12
621                greedyArgmaxSM86R13
622                sm86SafeControl)
623              (greedyArgmaxSM86When
624                greedyArgmaxSM86P1
625                (constructor
626                  SM86InstructionBody
627                  SM86MoveImmediate
628                  greedyArgmaxSM86R10
629                  greedyArgmaxSM86UFloatNegativeInfinity
630                  sm86SafeControl)
631                sm86ProgramEmpty)))))))
632
633def greedyArgmaxSM86CandidateProgram : (family SM86Program) =
634  (greedyArgmaxSM86Next
635    (constructor
636      SM86InstructionBody
637      SM86FloatMinimumOrMaximum
638      greedyArgmaxSM86R14
639      greedyArgmaxSM86R7
640      greedyArgmaxSM86R10
641      greedyArgmaxSM86FloatMaximum
642      sm86SafeControl)
643    (greedyArgmaxSM86Next
644      (constructor
645        SM86InstructionBody
646        SM86FloatNegate
647        greedyArgmaxSM86R15
648        greedyArgmaxSM86R14
649        sm86SafeControl)
650      (greedyArgmaxSM86Next
651        (constructor
652          SM86InstructionBody
653          SM86FloatAdd
654          greedyArgmaxSM86R16
655          greedyArgmaxSM86R7
656          greedyArgmaxSM86R15
657          sm86SafeControl)
658        (greedyArgmaxSM86Next
659          (constructor
660            SM86InstructionBody
661            SM86LogicThreeInputTruthTable
662            greedyArgmaxSM86R16
663            greedyArgmaxSM86R16
664            greedyArgmaxSM86R9
665            (byte 192)
666            sm86SafeControl)
667          (greedyArgmaxSM86Next
668            (constructor
669              SM86InstructionBody
670              SM86PredicateGreaterThanImmediate
671              greedyArgmaxSM86P2
672              greedyArgmaxSM86R16
673              greedyArgmaxSM86U0
674              sm86SafeControl)
675            (greedyArgmaxSM86When
676              greedyArgmaxSM86P2
677              (constructor
678                SM86InstructionBody
679                SM86IntegerAddThreeImmediate
680                greedyArgmaxSM86R8
681                greedyArgmaxSM86R3
682                greedyArgmaxSM86U0
683                sm86SafeControl)
684              (greedyArgmaxSM86Next
685                (constructor
686                  SM86InstructionBody
687                  SM86FloatAdd
688                  greedyArgmaxSM86R17
689                  greedyArgmaxSM86R10
690                  greedyArgmaxSM86R15
691                  sm86SafeControl)
692                (greedyArgmaxSM86Next
693                  (constructor
694                    SM86InstructionBody
695                    SM86LogicThreeInputTruthTable
696                    greedyArgmaxSM86R17
697                    greedyArgmaxSM86R17
698                    greedyArgmaxSM86R9
699                    (byte 192)
700                    sm86SafeControl)
701                  (greedyArgmaxSM86Next
702                    (constructor
703                      SM86InstructionBody
704                      SM86PredicateGreaterThanImmediate
705                      greedyArgmaxSM86P3
706                      greedyArgmaxSM86R17
707                      greedyArgmaxSM86U0
708                      sm86SafeControl)
709                    (greedyArgmaxSM86When
710                      greedyArgmaxSM86P3
711                      (constructor
712                        SM86InstructionBody
713                        SM86IntegerAddThreeImmediate
714                        greedyArgmaxSM86R3
715                        greedyArgmaxSM86R8
716                        greedyArgmaxSM86U0
717                        sm86SafeControl)
718                      (greedyArgmaxSM86Next
719                        (constructor
720                          SM86InstructionBody
721                          SM86IntegerToFloat
722                          greedyArgmaxSM86R23
723                          greedyArgmaxSM86R8
724                          sm86SafeControl)
725                        (greedyArgmaxSM86Next
726                          (constructor
727                            SM86InstructionBody
728                            SM86IntegerToFloat
729                            greedyArgmaxSM86R24
730                            greedyArgmaxSM86R3
731                            sm86SafeControl)
732                          (greedyArgmaxSM86Next
733                            (constructor
734                              SM86InstructionBody
735                              SM86FloatMinimumOrMaximum
736                              greedyArgmaxSM86R25
737                              greedyArgmaxSM86R23
738                              greedyArgmaxSM86R24
739                              greedyArgmaxSM86FloatMinimum
740                              sm86SafeControl)
741                            (greedyArgmaxSM86Next
742                              (constructor
743                                SM86InstructionBody
744                                SM86FloatNegate
745                                greedyArgmaxSM86R26
746                                greedyArgmaxSM86R25
747                                sm86SafeControl)
748                              (greedyArgmaxSM86Next
749                                (constructor
750                                  SM86InstructionBody
751                                  SM86FloatAdd
752                                  greedyArgmaxSM86R27
753                                  greedyArgmaxSM86R23
754                                  greedyArgmaxSM86R26
755                                  sm86SafeControl)
756                                (greedyArgmaxSM86Next
757                                  (constructor
758                                    SM86InstructionBody
759                                    SM86LogicThreeInputTruthTable
760                                    greedyArgmaxSM86R27
761                                    greedyArgmaxSM86R27
762                                    greedyArgmaxSM86R9
763                                    (byte 192)
764                                    sm86SafeControl)
765                                  (greedyArgmaxSM86Next
766                                    (constructor
767                                      SM86InstructionBody
768                                      SM86PredicateGreaterThanImmediate
769                                      greedyArgmaxSM86P1
770                                      greedyArgmaxSM86R27
771                                      greedyArgmaxSM86U0
772                                      sm86SafeControl)
773                                    (greedyArgmaxSM86When
774                                      greedyArgmaxSM86P1
775                                      (constructor
776                                        SM86InstructionBody
777                                        SM86IntegerAddThreeImmediate
778                                        greedyArgmaxSM86R8
779                                        greedyArgmaxSM86R3
780                                        greedyArgmaxSM86U0
781                                        sm86SafeControl)
782                                      (greedyArgmaxSM86Next
783                                        (constructor
784                                        SM86InstructionBody
785                                        SM86IntegerAddThreeImmediate
786                                        greedyArgmaxSM86R7
787                                        greedyArgmaxSM86R14
788                                        greedyArgmaxSM86U0
789                                        sm86SafeControl)
790                                        sm86ProgramEmpty)))))))))))))))))))
791
792def greedyArgmaxSM86ByteVocabularyInitialProgram : (family SM86Program) =
793  (greedyArgmaxSM86Next
794    (constructor
795      SM86InstructionBody
796      SM86MoveImmediate
797      greedyArgmaxSM86R3
798      greedyArgmaxSM86U0
799      sm86SafeControl)
800    (greedyArgmaxSM86Next
801      (constructor
802        SM86InstructionBody
803        SM86MoveImmediate
804        greedyArgmaxSM86R4
805        greedyArgmaxSM86U4
806        sm86SafeControl)
807      (greedyArgmaxSM86Next
808        (constructor
809          SM86InstructionBody
810          SM86MoveImmediate
811          greedyArgmaxSM86R7
812          greedyArgmaxSM86UFloatNegativeInfinity
813          sm86SafeControl)
814        (greedyArgmaxSM86Next
815          (constructor
816            SM86InstructionBody
817            SM86MoveImmediate
818            greedyArgmaxSM86R8
819            greedyArgmaxSM86UMaximumToken
820            sm86SafeControl)
821          sm86ProgramEmpty))))
822
823def greedyArgmaxSM86AscendingCandidateProgram : (family SM86Program) =
824  (greedyArgmaxSM86Next
825    (constructor
826      SM86InstructionBody
827      SM86FloatMinimumOrMaximum
828      greedyArgmaxSM86R14
829      greedyArgmaxSM86R7
830      greedyArgmaxSM86R10
831      greedyArgmaxSM86FloatMaximum
832      sm86SafeControl)
833    (greedyArgmaxSM86Next
834      (constructor
835        SM86InstructionBody
836        SM86FloatNegate
837        greedyArgmaxSM86R15
838        greedyArgmaxSM86R14
839        sm86SafeControl)
840      (greedyArgmaxSM86Next
841        (constructor
842          SM86InstructionBody
843          SM86FloatAdd
844          greedyArgmaxSM86R16
845          greedyArgmaxSM86R7
846          greedyArgmaxSM86R15
847          sm86SafeControl)
848        (greedyArgmaxSM86Next
849          (constructor
850            SM86InstructionBody
851            SM86PredicateGreaterThanImmediate
852            greedyArgmaxSM86P2
853            greedyArgmaxSM86R16
854            greedyArgmaxSM86U0
855            sm86SafeControl)
856          (greedyArgmaxSM86When
857            greedyArgmaxSM86P2
858            (constructor
859              SM86InstructionBody
860              SM86IntegerAddThreeImmediate
861              greedyArgmaxSM86R8
862              greedyArgmaxSM86R3
863              greedyArgmaxSM86U0
864              sm86SafeControl)
865            (greedyArgmaxSM86Next
866              (constructor
867                SM86InstructionBody
868                SM86IntegerAddThreeImmediate
869                greedyArgmaxSM86R7
870                greedyArgmaxSM86R14
871                greedyArgmaxSM86U0
872                sm86SafeControl)
873              sm86ProgramEmpty))))))
874
875-- Bob uses one thread and one native backward branch to scan all 256 byte
876-- logits.  The twelve-instruction loop advances R3 from 0 through 255, so the
877-- branch offset is -192 bytes from the instruction following BRA.
878def greedyArgmaxSM86ByteVocabularyLoopProgram : (family SM86Program) =
879  (sm86ProgramAppend
880    (greedyArgmaxSM86Next
881      (constructor
882        SM86InstructionBody
883        SM86IntegerMultiplyAddWideConstant
884        greedyArgmaxSM86R24
885        greedyArgmaxSM86R3
886        greedyArgmaxSM86R4
887        (byte 0)
888        greedyArgmaxSM86U360
889        sm86SafeControl)
890      (greedyArgmaxSM86Next
891        (constructor
892          SM86InstructionBody
893          SM86LoadGlobal
894          greedyArgmaxSM86R10
895          greedyArgmaxSM86R24
896          greedyArgmaxSM86U0
897          greedyArgmaxSM86Set0)
898        (greedyArgmaxSM86Next
899          (constructor
900            SM86InstructionBody
901            SM86IntegerAddThreeImmediate
902            greedyArgmaxSM86R10
903            greedyArgmaxSM86R10
904            greedyArgmaxSM86U0
905            greedyArgmaxSM86Wait0)
906          sm86ProgramEmpty)))
907    (sm86ProgramAppend
908      greedyArgmaxSM86AscendingCandidateProgram
909      (greedyArgmaxSM86Next
910        (constructor
911          SM86InstructionBody
912          SM86IntegerAddThreeImmediate
913          greedyArgmaxSM86R3
914          greedyArgmaxSM86R3
915          greedyArgmaxSM86U1
916          sm86SafeControl)
917        (greedyArgmaxSM86Next
918          (constructor
919            SM86InstructionBody
920            SM86PredicateGreaterThanImmediate
921            greedyArgmaxSM86P0
922            greedyArgmaxSM86R3
923            greedyArgmaxSM86UByteMask
924            sm86SafeControl)
925          (greedyArgmaxSM86WhenNot
926            greedyArgmaxSM86P0
927            (constructor
928              SM86InstructionBody
929              SM86Branch
930              greedyArgmaxSM86ByteLoopBackOffset
931              greedyArgmaxSM86BackwardBranchDescriptor
932              sm86BranchControl)
933            sm86ProgramEmpty)))))
934
935def greedyArgmaxSM86FullSlotProgram =
936  (lambda unrestricted slot : Nat .
937    (app
938      (lambda unrestricted base : Nat .
939        (sm86ProgramAppend
940          (greedyArgmaxSM86Next
941            (constructor
942              SM86InstructionBody
943              SM86IntegerAddThreeImmediate
944              greedyArgmaxSM86R3
945              greedyArgmaxSM86R0
946              (greedyArgmaxSM86Unsigned32FromNatural base)
947              sm86SafeControl)
948            (greedyArgmaxSM86Next
949              (constructor
950                SM86InstructionBody
951                SM86IntegerMultiplyAddWideConstant
952                greedyArgmaxSM86R28
953                greedyArgmaxSM86R3
954                greedyArgmaxSM86R4
955                (byte 0)
956                greedyArgmaxSM86U360
957                sm86SafeControl)
958              (greedyArgmaxSM86Next
959                (constructor
960                  SM86InstructionBody
961                  SM86LoadGlobal
962                  greedyArgmaxSM86R10
963                  greedyArgmaxSM86R28
964                  greedyArgmaxSM86U0
965                  greedyArgmaxSM86Set0)
966                (greedyArgmaxSM86Next
967                  (constructor
968                    SM86InstructionBody
969                    SM86IntegerAddThreeImmediate
970                    greedyArgmaxSM86R10
971                    greedyArgmaxSM86R10
972                    greedyArgmaxSM86U0
973                    greedyArgmaxSM86Wait0)
974                  sm86ProgramEmpty))))
975          (sm86ProgramAppend
976            greedyArgmaxSM86ValidateCandidateProgram
977            greedyArgmaxSM86CandidateProgram)))
978      (naturalMultiply slot greedyArgmaxSM86N256)))
979
980def greedyArgmaxSM86PartialSlotProgram =
981  (lambda unrestricted slot : Nat .
982    (lambda unrestricted lastLane : Nat .
983      (app
984        (lambda unrestricted base : Nat .
985          (sm86ProgramAppend
986            (greedyArgmaxSM86Next
987              (constructor
988                SM86InstructionBody
989                SM86PredicateGreaterThanImmediate
990                greedyArgmaxSM86P0
991                greedyArgmaxSM86R0
992                (greedyArgmaxSM86Unsigned32FromNatural lastLane)
993                sm86SafeControl)
994              (greedyArgmaxSM86Next
995                (constructor
996                  SM86InstructionBody
997                  SM86IntegerAddThreeImmediate
998                  greedyArgmaxSM86R3
999                  greedyArgmaxSM86R0
1000                  (greedyArgmaxSM86Unsigned32FromNatural base)
1001                  sm86SafeControl)
1002                (greedyArgmaxSM86Next
1003                  (constructor
1004                    SM86InstructionBody
1005                    SM86IntegerMultiplyAddWideConstant
1006                    greedyArgmaxSM86R28
1007                    greedyArgmaxSM86R3
1008                    greedyArgmaxSM86R4
1009                    (byte 0)
1010                    greedyArgmaxSM86U360
1011                    sm86SafeControl)
1012                  (greedyArgmaxSM86Next
1013                    (constructor
1014                      SM86InstructionBody
1015                      SM86MoveImmediate
1016                      greedyArgmaxSM86R10
1017                      greedyArgmaxSM86UFloatZero
1018                      sm86SafeControl)
1019                    (greedyArgmaxSM86WhenNot
1020                      greedyArgmaxSM86P0
1021                      (constructor
1022                        SM86InstructionBody
1023                        SM86LoadGlobal
1024                        greedyArgmaxSM86R10
1025                        greedyArgmaxSM86R28
1026                        greedyArgmaxSM86U0
1027                        greedyArgmaxSM86Set0)
1028                      (greedyArgmaxSM86WhenNot
1029                        greedyArgmaxSM86P0
1030                        (constructor
1031                          SM86InstructionBody
1032                          SM86IntegerAddThreeImmediate
1033                          greedyArgmaxSM86R10
1034                          greedyArgmaxSM86R10
1035                          greedyArgmaxSM86U0
1036                          greedyArgmaxSM86Wait0)
1037                        sm86ProgramEmpty))))))
1038            (sm86ProgramAppend
1039              greedyArgmaxSM86ValidateCandidateProgram
1040              (greedyArgmaxSM86When
1041                greedyArgmaxSM86P0
1042                (constructor
1043                  SM86InstructionBody
1044                  SM86MoveImmediate
1045                  greedyArgmaxSM86R10
1046                  greedyArgmaxSM86UFloatNegativeInfinity
1047                  sm86SafeControl)
1048                greedyArgmaxSM86CandidateProgram))))
1049        (naturalMultiply slot greedyArgmaxSM86N256))))
1050
1051def greedyArgmaxSM86FullSlotPrograms =
1052  (lambda unrestricted count : Nat .
1053    (nat-eliminate
1054      (lambda unrestricted current : Nat . (family SM86Program))
1055      sm86ProgramEmpty
1056      (lambda unrestricted predecessor : Nat .
1057        (lambda unrestricted induction : (family SM86Program) .
1058          (sm86ProgramAppend induction (greedyArgmaxSM86FullSlotProgram predecessor))))
1059      count))
1060
1061def greedyArgmaxSM86SlotPrograms =
1062  (lambda unrestricted vocabulary : Nat .
1063    (app
1064      (lambda unrestricted fullSlots : Nat .
1065        (app
1066          (lambda unrestricted remainder : Nat .
1067            (app
1068              (lambda unrestricted fullProgram : (family SM86Program) .
1069                (nat-eliminate
1070                  (lambda unrestricted tailLanes : Nat . (family SM86Program))
1071                  fullProgram
1072                  (lambda unrestricted lastLane : Nat .
1073                    (lambda unrestricted tailInduction : (family SM86Program) .
1074                      (sm86ProgramAppend
1075                        fullProgram
1076                        (greedyArgmaxSM86PartialSlotProgram fullSlots lastLane))))
1077                  remainder))
1078              (greedyArgmaxSM86FullSlotPrograms fullSlots)))
1079          (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256)))
1080      (naturalDivideUnchecked vocabulary greedyArgmaxSM86N256)))
1081
1082def greedyArgmaxSM86PairStage =
1083  (lambda unrestricted lane : Byte .
1084    (greedyArgmaxSM86Next
1085      (constructor
1086        SM86InstructionBody
1087        SM86WarpShuffle
1088        greedyArgmaxSM86R17
1089        greedyArgmaxSM86R7
1090        lane
1091        greedyArgmaxSM86U31
1092        greedyArgmaxSM86ShuffleButterfly
1093        greedyArgmaxSM86Set0)
1094      (greedyArgmaxSM86Next
1095        (constructor
1096          SM86InstructionBody
1097          SM86WarpShuffle
1098          greedyArgmaxSM86R18
1099          greedyArgmaxSM86R8
1100          lane
1101          greedyArgmaxSM86U31
1102          greedyArgmaxSM86ShuffleButterfly
1103          greedyArgmaxSM86Set1)
1104        (greedyArgmaxSM86Next
1105          (constructor
1106            SM86InstructionBody
1107            SM86IntegerAddThreeImmediate
1108            greedyArgmaxSM86R18
1109            greedyArgmaxSM86R18
1110            greedyArgmaxSM86U0
1111            greedyArgmaxSM86Wait1)
1112          (greedyArgmaxSM86Next
1113          (constructor
1114            SM86InstructionBody
1115            SM86FloatMinimumOrMaximum
1116            greedyArgmaxSM86R19
1117            greedyArgmaxSM86R7
1118            greedyArgmaxSM86R17
1119            greedyArgmaxSM86FloatMaximum
1120            greedyArgmaxSM86Wait0)
1121          (greedyArgmaxSM86Next
1122            (constructor
1123              SM86InstructionBody
1124              SM86FloatNegate
1125              greedyArgmaxSM86R20
1126              greedyArgmaxSM86R19
1127              sm86SafeControl)
1128            (greedyArgmaxSM86Next
1129              (constructor
1130                SM86InstructionBody
1131                SM86FloatAdd
1132                greedyArgmaxSM86R21
1133                greedyArgmaxSM86R7
1134                greedyArgmaxSM86R20
1135                sm86SafeControl)
1136              (greedyArgmaxSM86Next
1137                (constructor
1138                  SM86InstructionBody
1139                  SM86LogicThreeInputTruthTable
1140                  greedyArgmaxSM86R21
1141                  greedyArgmaxSM86R21
1142                  greedyArgmaxSM86R9
1143                  (byte 192)
1144                  sm86SafeControl)
1145                (greedyArgmaxSM86Next
1146                  (constructor
1147                    SM86InstructionBody
1148                    SM86PredicateGreaterThanImmediate
1149                    greedyArgmaxSM86P1
1150                    greedyArgmaxSM86R21
1151                    greedyArgmaxSM86U0
1152                    sm86SafeControl)
1153                  (greedyArgmaxSM86Next
1154                    (constructor
1155                      SM86InstructionBody
1156                      SM86FloatAdd
1157                      greedyArgmaxSM86R22
1158                      greedyArgmaxSM86R17
1159                      greedyArgmaxSM86R20
1160                      sm86SafeControl)
1161                    (greedyArgmaxSM86Next
1162                      (constructor
1163                        SM86InstructionBody
1164                        SM86LogicThreeInputTruthTable
1165                        greedyArgmaxSM86R22
1166                        greedyArgmaxSM86R22
1167                        greedyArgmaxSM86R9
1168                        (byte 192)
1169                        sm86SafeControl)
1170                      (greedyArgmaxSM86Next
1171                        (constructor
1172                          SM86InstructionBody
1173                          SM86PredicateGreaterThanImmediate
1174                          greedyArgmaxSM86P2
1175                          greedyArgmaxSM86R22
1176                          greedyArgmaxSM86U0
1177                          sm86SafeControl)
1178                        (greedyArgmaxSM86When
1179                          greedyArgmaxSM86P1
1180                          (constructor
1181                            SM86InstructionBody
1182                            SM86IntegerAddThreeImmediate
1183                            greedyArgmaxSM86R8
1184                            greedyArgmaxSM86R18
1185                            greedyArgmaxSM86U0
1186                            sm86SafeControl)
1187                          (greedyArgmaxSM86When
1188                            greedyArgmaxSM86P2
1189                            (constructor
1190                              SM86InstructionBody
1191                              SM86IntegerAddThreeImmediate
1192                              greedyArgmaxSM86R18
1193                              greedyArgmaxSM86R8
1194                              greedyArgmaxSM86U0
1195                              sm86SafeControl)
1196                            (greedyArgmaxSM86Next
1197                              (constructor
1198                                SM86InstructionBody
1199                                SM86IntegerToFloat
1200                                greedyArgmaxSM86R23
1201                                greedyArgmaxSM86R8
1202                                sm86SafeControl)
1203                              (greedyArgmaxSM86Next
1204                                (constructor
1205                                  SM86InstructionBody
1206                                  SM86IntegerToFloat
1207                                  greedyArgmaxSM86R24
1208                                  greedyArgmaxSM86R18
1209                                  sm86SafeControl)
1210                                (greedyArgmaxSM86Next
1211                                  (constructor
1212                                    SM86InstructionBody
1213                                    SM86FloatMinimumOrMaximum
1214                                    greedyArgmaxSM86R25
1215                                    greedyArgmaxSM86R23
1216                                    greedyArgmaxSM86R24
1217                                    greedyArgmaxSM86FloatMinimum
1218                                    sm86SafeControl)
1219                                  (greedyArgmaxSM86Next
1220                                    (constructor
1221                                      SM86InstructionBody
1222                                      SM86FloatNegate
1223                                      greedyArgmaxSM86R26
1224                                      greedyArgmaxSM86R25
1225                                      sm86SafeControl)
1226                                    (greedyArgmaxSM86Next
1227                                      (constructor
1228                                        SM86InstructionBody
1229                                        SM86FloatAdd
1230                                        greedyArgmaxSM86R27
1231                                        greedyArgmaxSM86R23
1232                                        greedyArgmaxSM86R26
1233                                        sm86SafeControl)
1234                                      (greedyArgmaxSM86Next
1235                                        (constructor
1236                                        SM86InstructionBody
1237                                        SM86LogicThreeInputTruthTable
1238                                        greedyArgmaxSM86R27
1239                                        greedyArgmaxSM86R27
1240                                        greedyArgmaxSM86R9
1241                                        (byte 192)
1242                                        sm86SafeControl)
1243                                        (greedyArgmaxSM86Next
1244                                        (constructor
1245                                        SM86InstructionBody
1246                                        SM86PredicateGreaterThanImmediate
1247                                        greedyArgmaxSM86P3
1248                                        greedyArgmaxSM86R27
1249                                        greedyArgmaxSM86U0
1250                                        sm86SafeControl)
1251                                        (greedyArgmaxSM86When
1252                                        greedyArgmaxSM86P3
1253                                        (constructor
1254                                        SM86InstructionBody
1255                                        SM86IntegerAddThreeImmediate
1256                                        greedyArgmaxSM86R8
1257                                        greedyArgmaxSM86R18
1258                                        greedyArgmaxSM86U0
1259                                        sm86SafeControl)
1260                                        (greedyArgmaxSM86Next
1261                                        (constructor
1262                                        SM86InstructionBody
1263                                        SM86IntegerAddThreeImmediate
1264                                        greedyArgmaxSM86R7
1265                                        greedyArgmaxSM86R19
1266                                        greedyArgmaxSM86U0
1267                                        sm86SafeControl)
1268                                        (greedyArgmaxSM86Next
1269                                        (constructor
1270                                        SM86InstructionBody
1271                                        SM86WarpShuffle
1272                                        greedyArgmaxSM86R17
1273                                        greedyArgmaxSM86R12
1274                                        lane
1275                                        greedyArgmaxSM86U31
1276                                        greedyArgmaxSM86ShuffleButterfly
1277                                        greedyArgmaxSM86Set2)
1278                                        (greedyArgmaxSM86Next
1279                                        (constructor
1280                                        SM86InstructionBody
1281                                        SM86FloatAdd
1282                                        greedyArgmaxSM86R12
1283                                        greedyArgmaxSM86R12
1284                                        greedyArgmaxSM86R17
1285                                        greedyArgmaxSM86Wait2)
1286                                        sm86ProgramEmpty)))))))))))))))))))))))))
1287
1288def greedyArgmaxSM86WarpReduceProgram : (family SM86Program) =
1289  (sm86ProgramAppend
1290    (greedyArgmaxSM86PairStage (byte 16))
1291    (sm86ProgramAppend
1292      (greedyArgmaxSM86PairStage (byte 8))
1293      (sm86ProgramAppend
1294        (greedyArgmaxSM86PairStage (byte 4))
1295        (sm86ProgramAppend
1296          (greedyArgmaxSM86PairStage (byte 2))
1297          (greedyArgmaxSM86PairStage (byte 1))))))
1298
1299def greedyArgmaxSM86BlockReduceProgram : (family SM86Program) =
1300  (sm86ProgramAppend
1301    greedyArgmaxSM86WarpReduceProgram
1302    (greedyArgmaxSM86Next
1303      (constructor
1304        SM86InstructionBody
1305        SM86MoveImmediate
1306        greedyArgmaxSM86R1
1307        greedyArgmaxSM86U31
1308        sm86SafeControl)
1309      (greedyArgmaxSM86Next
1310        (constructor
1311          SM86InstructionBody
1312          SM86LogicThreeInputTruthTable
1313          greedyArgmaxSM86R2
1314          greedyArgmaxSM86R0
1315          greedyArgmaxSM86R1
1316          (byte 192)
1317          sm86SafeControl)
1318        (greedyArgmaxSM86Next
1319          (constructor
1320            SM86InstructionBody
1321            SM86PredicateGreaterThanImmediate
1322            greedyArgmaxSM86P0
1323            greedyArgmaxSM86R2
1324            greedyArgmaxSM86U0
1325            sm86SafeControl)
1326          (greedyArgmaxSM86Next
1327            (constructor
1328              SM86InstructionBody
1329              SM86ShiftRightImmediate
1330              greedyArgmaxSM86R3
1331              greedyArgmaxSM86R0
1332              (byte 5)
1333              sm86SafeControl)
1334            (greedyArgmaxSM86Next
1335              (constructor
1336                SM86InstructionBody
1337                SM86IntegerMultiplyAddImmediate
1338                greedyArgmaxSM86R4
1339                greedyArgmaxSM86R3
1340                greedyArgmaxSM86U12
1341                sm86ZeroRegister
1342                sm86SafeControl)
1343              (greedyArgmaxSM86WhenNot
1344                greedyArgmaxSM86P0
1345                (constructor
1346                  SM86InstructionBody
1347                  SM86StoreShared
1348                  greedyArgmaxSM86R4
1349                  greedyArgmaxSM86R7
1350                  greedyArgmaxSM86U0
1351                  sm86SafeControl)
1352                (greedyArgmaxSM86WhenNot
1353                  greedyArgmaxSM86P0
1354                  (constructor
1355                    SM86InstructionBody
1356                    SM86StoreShared
1357                    greedyArgmaxSM86R4
1358                    greedyArgmaxSM86R8
1359                    greedyArgmaxSM86U4
1360                    sm86SafeControl)
1361                  (greedyArgmaxSM86WhenNot
1362                    greedyArgmaxSM86P0
1363                    (constructor
1364                      SM86InstructionBody
1365                      SM86StoreShared
1366                      greedyArgmaxSM86R4
1367                      greedyArgmaxSM86R12
1368                      greedyArgmaxSM86U8
1369                      sm86SafeControl)
1370                    (greedyArgmaxSM86Next
1371                      (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl)
1372                      (greedyArgmaxSM86Next
1373                        (constructor
1374                          SM86InstructionBody
1375                          SM86MoveImmediate
1376                          greedyArgmaxSM86R7
1377                          greedyArgmaxSM86UFloatNegativeInfinity
1378                          sm86SafeControl)
1379                        (greedyArgmaxSM86Next
1380                          (constructor
1381                            SM86InstructionBody
1382                            SM86MoveImmediate
1383                            greedyArgmaxSM86R8
1384                            greedyArgmaxSM86UMaximumToken
1385                            sm86SafeControl)
1386                          (greedyArgmaxSM86Next
1387                            (constructor
1388                              SM86InstructionBody
1389                              SM86MoveImmediate
1390                              greedyArgmaxSM86R12
1391                              greedyArgmaxSM86UFloatZero
1392                              sm86SafeControl)
1393                            (greedyArgmaxSM86Next
1394                              (constructor
1395                                SM86InstructionBody
1396                                SM86PredicateGreaterThanImmediate
1397                                greedyArgmaxSM86P0
1398                                greedyArgmaxSM86R0
1399                                greedyArgmaxSM86U7
1400                                sm86SafeControl)
1401                              (greedyArgmaxSM86Next
1402                                (constructor
1403                                  SM86InstructionBody
1404                                  SM86IntegerMultiplyAddImmediate
1405                                  greedyArgmaxSM86R4
1406                                  greedyArgmaxSM86R0
1407                                  greedyArgmaxSM86U12
1408                                  sm86ZeroRegister
1409                                  sm86SafeControl)
1410                                (greedyArgmaxSM86WhenNot
1411                                  greedyArgmaxSM86P0
1412                                  (constructor
1413                                    SM86InstructionBody
1414                                    SM86LoadShared
1415                                    greedyArgmaxSM86R7
1416                                    greedyArgmaxSM86R4
1417                                    greedyArgmaxSM86U0
1418                                    greedyArgmaxSM86Set0)
1419                                  (greedyArgmaxSM86WhenNot
1420                                    greedyArgmaxSM86P0
1421                                    (constructor
1422                                      SM86InstructionBody
1423                                      SM86LoadShared
1424                                      greedyArgmaxSM86R8
1425                                      greedyArgmaxSM86R4
1426                                      greedyArgmaxSM86U4
1427                                      greedyArgmaxSM86Set1)
1428                                    (greedyArgmaxSM86WhenNot
1429                                      greedyArgmaxSM86P0
1430                                      (constructor
1431                                        SM86InstructionBody
1432                                        SM86LoadShared
1433                                        greedyArgmaxSM86R12
1434                                        greedyArgmaxSM86R4
1435                                        greedyArgmaxSM86U8
1436                                        greedyArgmaxSM86Set2)
1437                                      (greedyArgmaxSM86WhenNot
1438                                        greedyArgmaxSM86P0
1439                                        (constructor
1440                                        SM86InstructionBody
1441                                        SM86IntegerAddThreeImmediate
1442                                        greedyArgmaxSM86R7
1443                                        greedyArgmaxSM86R7
1444                                        greedyArgmaxSM86U0
1445                                        greedyArgmaxSM86Wait0)
1446                                        (greedyArgmaxSM86WhenNot
1447                                        greedyArgmaxSM86P0
1448                                        (constructor
1449                                        SM86InstructionBody
1450                                        SM86IntegerAddThreeImmediate
1451                                        greedyArgmaxSM86R8
1452                                        greedyArgmaxSM86R8
1453                                        greedyArgmaxSM86U0
1454                                        greedyArgmaxSM86Wait1)
1455                                        (greedyArgmaxSM86WhenNot
1456                                        greedyArgmaxSM86P0
1457                                        (constructor
1458                                        SM86InstructionBody
1459                                        SM86FloatAdd
1460                                        greedyArgmaxSM86R12
1461                                        greedyArgmaxSM86R12
1462                                        greedyArgmaxSM86R13
1463                                        greedyArgmaxSM86Wait2)
1464                                        (greedyArgmaxSM86Next
1465                                        (constructor
1466                                        SM86InstructionBody
1467                                        SM86BarrierSynchronize
1468                                        sm86SafeControl)
1469                                        greedyArgmaxSM86WarpReduceProgram))))))))))))))))))))))
1470
1471def greedyArgmaxSM86SuffixProgram : (family SM86Program) =
1472  (greedyArgmaxSM86Next
1473    (constructor
1474      SM86InstructionBody
1475      SM86MoveConstant
1476      greedyArgmaxSM86R28
1477      (byte 0)
1478      greedyArgmaxSM86U352
1479      sm86SafeControl)
1480    (greedyArgmaxSM86Next
1481      (constructor
1482        SM86InstructionBody
1483        SM86MoveConstant
1484        greedyArgmaxSM86R29
1485        (byte 0)
1486        greedyArgmaxSM86U356
1487        sm86SafeControl)
1488      (greedyArgmaxSM86Next
1489        (constructor
1490          SM86InstructionBody
1491          SM86MoveImmediate
1492          greedyArgmaxSM86R27
1493          greedyArgmaxSM86U1
1494          sm86SafeControl)
1495        (greedyArgmaxSM86Next
1496          (constructor
1497            SM86InstructionBody
1498          SM86PredicateGreaterThanImmediate
1499          greedyArgmaxSM86P1
1500          greedyArgmaxSM86R12
1501          greedyArgmaxSM86U0
1502          sm86SafeControl)
1503        (greedyArgmaxSM86When
1504          greedyArgmaxSM86P1
1505          (constructor
1506            SM86InstructionBody
1507            SM86MoveImmediate
1508            greedyArgmaxSM86R27
1509            greedyArgmaxSM86U0
1510            sm86SafeControl)
1511          (greedyArgmaxSM86Next
1512            (constructor
1513              SM86InstructionBody
1514              SM86PredicateGreaterThanImmediate
1515              greedyArgmaxSM86P0
1516              greedyArgmaxSM86R0
1517              greedyArgmaxSM86U0
1518              sm86SafeControl)
1519                (greedyArgmaxSM86WhenNot
1520                  greedyArgmaxSM86P0
1521                  (constructor
1522                    SM86InstructionBody
1523                    SM86StoreGlobal
1524                    greedyArgmaxSM86R28
1525                    greedyArgmaxSM86R8
1526                    greedyArgmaxSM86U0
1527                    sm86SafeControl)
1528                  (greedyArgmaxSM86WhenNot
1529                    greedyArgmaxSM86P0
1530                    (constructor
1531                      SM86InstructionBody
1532                      SM86StoreGlobal
1533                      greedyArgmaxSM86R28
1534                      greedyArgmaxSM86R27
1535                      greedyArgmaxSM86U4
1536                      sm86SafeControl)
1537                    (greedyArgmaxSM86Next
1538                      (constructor SM86InstructionBody SM86Exit sm86SafeControl)
1539                      sm86ProgramEmpty)))))))))
1540
1541-- Bob's byte reference schedule has one thread, hence one writer.
1542def greedyArgmaxSM86ByteVocabularySuffixProgram : (family SM86Program) =
1543  (greedyArgmaxSM86Next
1544    (constructor
1545      SM86InstructionBody
1546      SM86MoveConstant
1547      greedyArgmaxSM86R28
1548      (byte 0)
1549      greedyArgmaxSM86U352
1550      sm86SafeControl)
1551    (greedyArgmaxSM86Next
1552      (constructor
1553        SM86InstructionBody
1554        SM86MoveConstant
1555        greedyArgmaxSM86R29
1556        (byte 0)
1557        greedyArgmaxSM86U356
1558        sm86SafeControl)
1559      (greedyArgmaxSM86Next
1560        (constructor
1561          SM86InstructionBody
1562          SM86MoveImmediate
1563          greedyArgmaxSM86R27
1564          greedyArgmaxSM86U1
1565          sm86SafeControl)
1566        (greedyArgmaxSM86Next
1567          (constructor
1568            SM86InstructionBody
1569            SM86StoreGlobal
1570            greedyArgmaxSM86R28
1571            greedyArgmaxSM86R8
1572            greedyArgmaxSM86U0
1573            sm86SafeControl)
1574          (greedyArgmaxSM86Next
1575            (constructor
1576              SM86InstructionBody
1577              SM86StoreGlobal
1578              greedyArgmaxSM86R28
1579              greedyArgmaxSM86R27
1580              greedyArgmaxSM86U4
1581              sm86SafeControl)
1582            (greedyArgmaxSM86Next
1583              (constructor SM86InstructionBody SM86Exit sm86SafeControl)
1584              sm86ProgramEmpty))))))
1585
1586def greedyArgmaxSM86ProgramFor =
1587  (lambda unrestricted vocabulary : Nat .
1588    (sm86ProgramAppend
1589      greedyArgmaxSM86InitialProgram
1590      (sm86ProgramAppend
1591        (greedyArgmaxSM86SlotPrograms vocabulary)
1592        (sm86ProgramAppend greedyArgmaxSM86BlockReduceProgram greedyArgmaxSM86SuffixProgram))))
1593
1594def greedyArgmaxSM86ByteVocabularyProgram : (family SM86Program) =
1595  (sm86ProgramAppend
1596    greedyArgmaxSM86ByteVocabularyInitialProgram
1597    (sm86ProgramAppend
1598      greedyArgmaxSM86ByteVocabularyLoopProgram
1599      greedyArgmaxSM86ByteVocabularySuffixProgram))
1600
1601def greedyArgmaxSM86HasTail =
1602  (lambda unrestricted vocabulary : Nat .
1603    (naturalNonzero (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256)))
1604
1605def greedyArgmaxSM86ExpectedInstructions =
1606  (lambda unrestricted vocabulary : Nat .
1607    (naturalAdd
1608      greedyArgmaxSM86N277
1609      (naturalAdd
1610        (naturalMultiply
1611          (naturalDivideUnchecked vocabulary greedyArgmaxSM86N256)
1612          greedyArgmaxSM86N30)
1613        (naturalMultiply (greedyArgmaxSM86HasTail vocabulary) greedyArgmaxSM86N33))))
1614
1615def greedyArgmaxSM86TailMaskWrites =
1616  (lambda unrestricted vocabulary : Nat .
1617    (naturalMultiply
1618      (greedyArgmaxSM86HasTail vocabulary)
1619      (naturalSaturatingSubtract
1620        greedyArgmaxSM86N256
1621        (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256))))
1622
1623def greedyArgmaxSM86ManifestFor =
1624  (lambda unrestricted vocabulary : Nat .
1625    (app
1626      (lambda unrestricted expectedInstructions : Nat .
1627        (constructor
1628          GreedyArgmaxSM86Manifest
1629          GreedyArgmaxSM86ManifestValue
1630          vocabulary
1631          (naturalDivideUnchecked vocabulary greedyArgmaxSM86N256)
1632          (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256)
1633          expectedInstructions
1634          (naturalMultiply expectedInstructions greedyArgmaxSM86InstructionBytes)
1635          greedyArgmaxSM86Registers
1636          greedyArgmaxSM86SharedBytes
1637          greedyArgmaxSM86GridX
1638          greedyArgmaxSM86ThreadsPerBlock
1639          vocabulary
1640          vocabulary
1641          zero
1642          (greedyArgmaxSM86TailMaskWrites vocabulary)
1643          greedyArgmaxSM86N10
1644          greedyArgmaxSM86N1
1645          greedyArgmaxSM86N1
1646          greedyArgmaxSM86HostLogitReads
1647          greedyArgmaxSM86HostFallbackOperations
1648          greedyArgmaxSM86ABIValue))
1649      (greedyArgmaxSM86ExpectedInstructions vocabulary)))
1650
1651def greedyArgmaxSM86TelemetryFor =
1652  (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1653    (lambda unrestricted observedInstructions : Nat .
1654      (lambda unrestricted observedBytes : Nat .
1655        (lambda unrestricted fields : Nat .
1656          (lambda unrestricted bits : Nat .
1657            (lambda unrestricted highest : Nat .
1658              (lambda unrestricted identityInput : Nat .
1659                (lambda unrestricted identityOutput : Nat .
1660                  (constructor
1661                    GreedyArgmaxSM86Telemetry
1662                    GreedyArgmaxSM86TelemetryValue
1663                    (constructor GreedyArgmaxSM86ExecutionContract GreedyArgmaxSM86NativeOnly)
1664                    manifest
1665                    observedInstructions
1666                    observedBytes
1667                    fields
1668                    bits
1669                    highest
1670                    identityInput
1671                    identityOutput
1672                    greedyArgmaxSM86N1
1673                    greedyArgmaxSM86N1
1674                    greedyArgmaxSM86HostFallbackOperations)))))))))
1675
1676def greedyArgmaxSM86EmptyTelemetry =
1677  (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1678    (lambda unrestricted observedInstructions : Nat .
1679      (lambda unrestricted observedBytes : Nat .
1680        (greedyArgmaxSM86TelemetryFor
1681          manifest
1682          observedInstructions
1683          observedBytes
1684          zero
1685          zero
1686          zero
1687          zero
1688          zero))))
1689
1690def greedyArgmaxSM86Failed =
1691  (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1692    (lambda unrestricted code : (family GreedyArgmaxSM86FailureCode) .
1693      (lambda unrestricted ordinal : Nat .
1694        (lambda unrestricted observedInstructions : Nat .
1695          (lambda unrestricted observedBytes : Nat .
1696            (constructor
1697              GreedyArgmaxSM86Artifact
1698              GreedyArgmaxSM86ArtifactFailed
1699              code
1700              ordinal
1701              (greedyArgmaxSM86FailureCodeBytes code)
1702              (greedyArgmaxSM86EmptyTelemetry manifest observedInstructions observedBytes)))))))
1703
1704def greedyArgmaxSM86BuildIdentity =
1705  (lambda unrestricted program : (family SM86Program) .
1706    (lambda unrestricted image : Bytes .
1707      (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1708        (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) .
1709          (eliminate
1710            SM86ProgramEncodingTelemetry
1711            (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
1712              (family GreedyArgmaxSM86Artifact))
1713            encodingTelemetry
1714            (branch
1715              SM86ProgramEncodingTelemetryValue
1716              instructions
1717              encodedBytes
1718              fields
1719              bits
1720              highest
1721              .
1722              (eliminate
1723                SHA256HexResult
1724                (lambda unrestricted current : (family SHA256HexResult) .
1725                  (family GreedyArgmaxSM86Artifact))
1726                (sha256Hex image)
1727                (branch
1728                  SHA256HexSucceeded
1729                  identity
1730                  digestTelemetry
1731                  .
1732                  (nat-eliminate
1733                    (lambda unrestricted exactLength : Nat . (family GreedyArgmaxSM86Artifact))
1734                    (greedyArgmaxSM86Failed
1735                      manifest
1736                      (constructor
1737                        GreedyArgmaxSM86FailureCode
1738                        GreedyArgmaxSM86ImageIdentityLengthInvalid)
1739                      (bytes-length identity)
1740                      instructions
1741                      encodedBytes)
1742                    (lambda unrestricted predecessor : Nat .
1743                      (lambda unrestricted induction : (family GreedyArgmaxSM86Artifact) .
1744                        (constructor
1745                          GreedyArgmaxSM86Artifact
1746                          GreedyArgmaxSM86ArtifactReady
1747                          program
1748                          image
1749                          identity
1750                          manifest
1751                          encodingTelemetry
1752                          digestTelemetry
1753                          (greedyArgmaxSM86TelemetryFor
1754                            manifest
1755                            instructions
1756                            encodedBytes
1757                            fields
1758                            bits
1759                            highest
1760                            (bytes-length image)
1761                            (bytes-length identity)))))
1762                    (naturalEqual (bytes-length identity) greedyArgmaxSM86N64)))
1763                (branch
1764                  SHA256HexFailed
1765                  failure
1766                  hexFailureOrdinal
1767                  digestTelemetry
1768                  .
1769                  (greedyArgmaxSM86Failed
1770                    manifest
1771                    (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageIdentityFailed)
1772                    zero
1773                    instructions
1774                    encodedBytes)))))))))
1775
1776def greedyArgmaxSM86BuildEncoded =
1777  (lambda unrestricted program : (family SM86Program) .
1778    (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1779      (eliminate
1780        SM86ProgramEncodingResult
1781        (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1782          (family GreedyArgmaxSM86Artifact))
1783        (sm86EncodeProgram program)
1784        (branch
1785          SM86ProgramEncodingSucceeded
1786          image
1787          telemetry
1788          .
1789          (eliminate
1790            SM86ProgramEncodingTelemetry
1791            (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
1792              (family GreedyArgmaxSM86Artifact))
1793            telemetry
1794            (branch
1795              SM86ProgramEncodingTelemetryValue
1796              instructions
1797              encodedBytes
1798              fields
1799              bits
1800              highest
1801              .
1802              (eliminate
1803                GreedyArgmaxSM86Manifest
1804                (lambda unrestricted current : (family GreedyArgmaxSM86Manifest) .
1805                  (family GreedyArgmaxSM86Artifact))
1806                manifest
1807                (branch
1808                  GreedyArgmaxSM86ManifestValue
1809                  vocabulary
1810                  fullSlots
1811                  tailLanes
1812                  expectedInstructions
1813                  expectedBytes
1814                  registers
1815                  sharedBytes
1816                  gridX
1817                  threads
1818                  activeLoads
1819                  activeFinite
1820                  inactiveFinite
1821                  tailMasks
1822                  tieStages
1823                  tokenWrites
1824                  validityWrites
1825                  hostReads
1826                  fallbacks
1827                  abi
1828                  .
1829                  (nat-eliminate
1830                    (lambda unrestricted instructionsExact : Nat .
1831                      (family GreedyArgmaxSM86Artifact))
1832                    (greedyArgmaxSM86Failed
1833                      manifest
1834                      (constructor
1835                        GreedyArgmaxSM86FailureCode
1836                        GreedyArgmaxSM86EncodedInstructionCountMismatch)
1837                      instructions
1838                      instructions
1839                      encodedBytes)
1840                    (lambda unrestricted instructionPredecessor : Nat .
1841                      (lambda unrestricted instructionInduction : (family GreedyArgmaxSM86Artifact) .
1842                        (nat-eliminate
1843                          (lambda unrestricted bytesExact : Nat . (family GreedyArgmaxSM86Artifact))
1844                          (greedyArgmaxSM86Failed
1845                            manifest
1846                            (constructor
1847                              GreedyArgmaxSM86FailureCode
1848                              GreedyArgmaxSM86EncodedByteCountMismatch)
1849                            encodedBytes
1850                            instructions
1851                            encodedBytes)
1852                          (lambda unrestricted bytePredecessor : Nat .
1853                            (lambda unrestricted byteInduction : (family GreedyArgmaxSM86Artifact) .
1854                              (greedyArgmaxSM86BuildIdentity program image manifest telemetry)))
1855                          (naturalEqual encodedBytes expectedBytes))))
1856                    (naturalEqual instructions expectedInstructions)))))))
1857        (branch
1858          SM86ProgramEncodingFailed
1859          instructionIndex
1860          failure
1861          telemetry
1862          .
1863          (greedyArgmaxSM86Failed
1864            manifest
1865            (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageEncodingFailed)
1866            instructionIndex
1867            (sm86ProgramCount program)
1868            zero)))))
1869
1870def greedyArgmaxSM86BuildValidated =
1871  (lambda unrestricted vocabulary : Nat .
1872    (app
1873      (lambda unrestricted program : (family SM86Program) .
1874        (app
1875          (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1876            (eliminate
1877              GreedyArgmaxSM86Manifest
1878              (lambda unrestricted current : (family GreedyArgmaxSM86Manifest) .
1879                (family GreedyArgmaxSM86Artifact))
1880              manifest
1881              (branch
1882                GreedyArgmaxSM86ManifestValue
1883                manifestVocabulary
1884                fullSlots
1885                tailLanes
1886                expectedInstructions
1887                expectedBytes
1888                registers
1889                sharedBytes
1890                gridX
1891                threads
1892                activeLoads
1893                activeFinite
1894                inactiveFinite
1895                tailMasks
1896                tieStages
1897                tokenWrites
1898                validityWrites
1899                hostReads
1900                fallbacks
1901                abi
1902                .
1903                (nat-eliminate
1904                  (lambda unrestricted fallbackFree : Nat . (family GreedyArgmaxSM86Artifact))
1905                  (greedyArgmaxSM86Failed
1906                    manifest
1907                    (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86HostFallbackDetected)
1908                    fallbacks
1909                    (sm86ProgramCount program)
1910                    zero)
1911                  (lambda unrestricted fallbackPredecessor : Nat .
1912                    (lambda unrestricted fallbackInduction : (family GreedyArgmaxSM86Artifact) .
1913                      (nat-eliminate
1914                        (lambda unrestricted programExact : Nat . (family GreedyArgmaxSM86Artifact))
1915                        (greedyArgmaxSM86Failed
1916                          manifest
1917                          (constructor
1918                            GreedyArgmaxSM86FailureCode
1919                            GreedyArgmaxSM86InstructionCountMismatch)
1920                          (sm86ProgramCount program)
1921                          (sm86ProgramCount program)
1922                          zero)
1923                        (lambda unrestricted programPredecessor : Nat .
1924                          (lambda unrestricted programInduction : (family GreedyArgmaxSM86Artifact) .
1925                            (greedyArgmaxSM86BuildEncoded program manifest)))
1926                        (naturalEqual (sm86ProgramCount program) expectedInstructions))))
1927                  (naturalEqual fallbacks zero)))))
1928          (greedyArgmaxSM86ManifestFor vocabulary)))
1929      (greedyArgmaxSM86ProgramFor vocabulary)))
1930
1931def greedyArgmaxSM86Build =
1932  (lambda unrestricted vocabulary : Nat .
1933    (eliminate
1934      GreedyArgmaxSM86Validation
1935      (lambda unrestricted current : (family GreedyArgmaxSM86Validation) .
1936        (family GreedyArgmaxSM86Artifact))
1937      (greedyArgmaxSM86ValidateVocabulary vocabulary)
1938      (branch GreedyArgmaxSM86ValidationAccepted . (greedyArgmaxSM86BuildValidated vocabulary))
1939      (branch
1940        GreedyArgmaxSM86ValidationRejected
1941        failure
1942        .
1943        (greedyArgmaxSM86Failed (greedyArgmaxSM86ManifestFor vocabulary) failure zero zero zero))))
1944
1945def greedyArgmaxSM86BuildPromoted =
1946  (greedyArgmaxSM86Build greedyArgmaxSM86PromotedVocabulary)
1947
1948def greedyArgmaxSM86ByteVocabularyManifest : (family GreedyArgmaxSM86Manifest) =
1949  (app
1950    (lambda unrestricted expectedInstructions : Nat .
1951      (constructor
1952        GreedyArgmaxSM86Manifest
1953        GreedyArgmaxSM86ManifestValue
1954        greedyArgmaxSM86N256
1955        greedyArgmaxSM86N256
1956        zero
1957        expectedInstructions
1958        (naturalMultiply expectedInstructions greedyArgmaxSM86InstructionBytes)
1959        greedyArgmaxSM86Registers
1960        zero
1961        greedyArgmaxSM86GridX
1962        greedyArgmaxSM86N1
1963        greedyArgmaxSM86N256
1964        zero
1965        zero
1966        zero
1967        zero
1968        greedyArgmaxSM86N1
1969        greedyArgmaxSM86N1
1970        greedyArgmaxSM86HostLogitReads
1971        greedyArgmaxSM86HostFallbackOperations
1972        greedyArgmaxSM86ABIValue))
1973    (sm86ProgramCount greedyArgmaxSM86ByteVocabularyProgram))
1974
1975def greedyArgmaxSM86BuildByteVocabulary : (family GreedyArgmaxSM86Artifact) =
1976  (greedyArgmaxSM86BuildEncoded
1977    greedyArgmaxSM86ByteVocabularyProgram
1978    greedyArgmaxSM86ByteVocabularyManifest)