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