1module Realization.Nvidia.SM86.ExactCrossEntropySM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.Program
8import Data.SHA256Digest
9import Realization.Nvidia.SM86.ReductionSM86
10import Std.Natural
11import Accelerator.SM86.NumericSemantics
12import Accelerator.SM86.Types
13
14family ExactCrossEntropySM86Variant : Type 0
15constructor ExactCrossEntropyRows
16constructor ReduceExactRowLosses
17constructor FinalizeExactMeanLoss
18
19end-family
20
21family ExactCrossEntropySM86FailureCode : Type 0
22constructor ExactCrossEntropyInstructionCountMismatch
23constructor ExactCrossEntropyEncodedByteCountMismatch
24constructor ExactCrossEntropyEncodingFailed
25constructor ExactCrossEntropyIdentityFailed
26constructor ExactCrossEntropyIdentityLengthInvalid
27
28end-family
29
30family ExactCrossEntropySM86ABI : Type 0
31constructor ExactCrossEntropySM86ABIValue
32field unrestricted exactCrossEntropyABIWorkspace : Nat
33field unrestricted exactCrossEntropyABILogits : Nat
34field unrestricted exactCrossEntropyABIScalar : Nat
35field unrestricted exactCrossEntropyABICorrectLogit : Nat
36field unrestricted exactCrossEntropyABILog2E : Nat
37field unrestricted exactCrossEntropyABILn2 : Nat
38field unrestricted exactCrossEntropyABIInverseRows : Nat
39
40end-family
41
42family ExactCrossEntropySM86Extents : Type 0
43constructor ExactCrossEntropySM86ExtentsValue
44field unrestricted exactCrossEntropyExtentWorkspaceReadOffsetElements : Nat
45field unrestricted exactCrossEntropyExtentWorkspaceReadElements : Nat
46field unrestricted exactCrossEntropyExtentWorkspaceWriteOffsetElements : Nat
47field unrestricted exactCrossEntropyExtentWorkspaceWriteElements : Nat
48field unrestricted exactCrossEntropyExtentWorkspaceAddressableElements : Nat
49field unrestricted exactCrossEntropyExtentLogitsReadElements : Nat
50field unrestricted exactCrossEntropyExtentCorrectLogitsReadElements : Nat
51field unrestricted exactCrossEntropyExtentScalarWriteElements : Nat
52field unrestricted exactCrossEntropyExtentGlobalVocabularyMaterializations : Nat
53
54end-family
55
56family ExactCrossEntropySM86Manifest : Type 0
57constructor ExactCrossEntropySM86ManifestValue
58field unrestricted exactCrossEntropyManifestVariant : (family ExactCrossEntropySM86Variant)
59field unrestricted exactCrossEntropyManifestExpectedInstructions : Nat
60field unrestricted exactCrossEntropyManifestExpectedEncodedBytes : Nat
61field unrestricted exactCrossEntropyManifestRegisters : Nat
62field unrestricted exactCrossEntropyManifestSharedBytes : Nat
63field unrestricted exactCrossEntropyManifestGridX : Nat
64field unrestricted exactCrossEntropyManifestBlockX : Nat
65field unrestricted exactCrossEntropyManifestABI : (family ExactCrossEntropySM86ABI)
66field unrestricted exactCrossEntropyManifestExtents : (family ExactCrossEntropySM86Extents)
67field unrestricted exactCrossEntropyManifestReduction0Start : Nat
68field unrestricted exactCrossEntropyManifestReduction0End : Nat
69field unrestricted exactCrossEntropyManifestReduction1Start : Nat
70field unrestricted exactCrossEntropyManifestReduction1End : Nat
71field unrestricted exactCrossEntropyManifestRows : Nat
72field unrestricted exactCrossEntropyManifestVocabulary : Nat
73field unrestricted exactCrossEntropyManifestVocabularyTileElements : Nat
74field unrestricted exactCrossEntropyManifestVocabularyTiles : Nat
75field unrestricted exactCrossEntropyManifestHostFallbackOperations : Nat
76
77end-family
78
79family ExactCrossEntropySM86Telemetry : Type 0
80constructor ExactCrossEntropySM86TelemetryValue
81field unrestricted exactCrossEntropyTelemetryManifest : (family ExactCrossEntropySM86Manifest)
82field unrestricted exactCrossEntropyTelemetryObservedInstructions : Nat
83field unrestricted exactCrossEntropyTelemetryObservedEncodedBytes : Nat
84
85end-family
86
87family ExactCrossEntropySM86BuildResult : Type 0
88constructor ExactCrossEntropySM86BuildSucceeded
89field unrestricted exactCrossEntropyEncodedBytes : Bytes
90field unrestricted exactCrossEntropyImageIdentity : Bytes
91field unrestricted exactCrossEntropyProgramEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
92field unrestricted exactCrossEntropyIdentityTelemetry : (family SHA256DigestTelemetry)
93field unrestricted exactCrossEntropyBuildTelemetry : (family ExactCrossEntropySM86Telemetry)
94constructor ExactCrossEntropySM86ContractFailed
95field unrestricted exactCrossEntropyContractFailure : (family ExactCrossEntropySM86FailureCode)
96field unrestricted exactCrossEntropyContractFailureTelemetry : (family ExactCrossEntropySM86Telemetry)
97constructor ExactCrossEntropySM86ImageEncodingFailed
98field unrestricted exactCrossEntropyEncodingFailure : (family ExactCrossEntropySM86FailureCode)
99field unrestricted exactCrossEntropyFailedEncoding : (family SM86ProgramEncodingResult)
100field unrestricted exactCrossEntropyEncodingFailureTelemetry : (family ExactCrossEntropySM86Telemetry)
101constructor ExactCrossEntropySM86ImageIdentityFailed
102field unrestricted exactCrossEntropyIdentityFailure : (family ExactCrossEntropySM86FailureCode)
103field unrestricted exactCrossEntropyFailedIdentity : (family SHA256HexResult)
104field unrestricted exactCrossEntropyIdentityFailureTelemetry : (family ExactCrossEntropySM86Telemetry)
105
106end-family
107
108def exactCrossEntropySM86FailureCodeBytes =
109 (lambda unrestricted code : (family ExactCrossEntropySM86FailureCode) .
110 (eliminate
111 ExactCrossEntropySM86FailureCode
112 (lambda unrestricted current : (family ExactCrossEntropySM86FailureCode) . Bytes)
113 code
114 (branch ExactCrossEntropyInstructionCountMismatch . b"ALPHA-SM86-ECE-001")
115 (branch ExactCrossEntropyEncodedByteCountMismatch . b"ALPHA-SM86-ECE-002")
116 (branch ExactCrossEntropyEncodingFailed . b"ALPHA-SM86-ECE-003")
117 (branch ExactCrossEntropyIdentityFailed . b"ALPHA-SM86-ECE-004")
118 (branch ExactCrossEntropyIdentityLengthInvalid . b"ALPHA-SM86-ECE-005")))
119
120def exactCrossEntropySM86Next =
121 (lambda unrestricted instruction : (family SM86Instruction) .
122 (lambda unrestricted tail : (family SM86Program) .
123 (constructor SM86Program SM86ProgramNext instruction tail)))
124
125def exactCrossEntropySM86AlwaysNext =
126 (lambda unrestricted body : (family SM86InstructionBody) .
127 (lambda unrestricted tail : (family SM86Program) .
128 (exactCrossEntropySM86Next (sm86Instruction body) tail)))
129
130def exactCrossEntropySM86End : (family SM86Program) =
131 (constructor SM86Program SM86ProgramEnd)
132
133def exactCrossEntropyRowsR0 =
134 (sm86Register (byte 0))
135
136def exactCrossEntropyRowsR1 =
137 (sm86Register (byte 1))
138
139def exactCrossEntropyRowsR2 =
140 (sm86Register (byte 2))
141
142def exactCrossEntropyRowsR3 =
143 (sm86Register (byte 3))
144
145def exactCrossEntropyRowsR4 =
146 (sm86Register (byte 4))
147
148def exactCrossEntropyRowsR6 =
149 (sm86Register (byte 6))
150
151def exactCrossEntropyRowsR8 =
152 (sm86Register (byte 8))
153
154def exactCrossEntropyRowsR9 =
155 (sm86Register (byte 9))
156
157def exactCrossEntropyRowsR10 =
158 (sm86Register (byte 10))
159
160def exactCrossEntropyRowsR11 =
161 (sm86Register (byte 11))
162
163def exactCrossEntropyRowsR12 =
164 (sm86Register (byte 12))
165
166def exactCrossEntropyRowsR13 =
167 (sm86Register (byte 13))
168
169def exactCrossEntropyRowsR14 =
170 (sm86Register (byte 14))
171
172def exactCrossEntropyRowsR16 =
173 (sm86Register (byte 16))
174
175def exactCrossEntropyRowsR20 =
176 (sm86Register (byte 20))
177
178def exactCrossEntropyRowsR24 =
179 (sm86Register (byte 24))
180
181def exactCrossEntropyRowsR25 =
182 (sm86Register (byte 25))
183
184def exactCrossEntropyRowsR26 =
185 (sm86Register (byte 26))
186
187def exactCrossEntropyRowsP0 : (family SM86Predicate) =
188 (constructor SM86Predicate SM86Predicate0)
189
190def exactCrossEntropyRowsOutputArgument : Nat = 0
191def exactCrossEntropyRowsLogitsArgument : Nat = 1
192def exactCrossEntropyRowsCorrectLogitArgument : Nat = 2
193-- The shared CB0 ABI reserves six pointer slots before F32 scalar words.
194def exactCrossEntropyRowsScalarPairArgument : Nat = 6
195def exactCrossEntropyMeanWorkspaceArgument : Nat = 0
196def exactCrossEntropyMeanOutputArgument : Nat = 1
197def exactCrossEntropyMeanInverseRowsArgument : Nat = 7
198
199def exactCrossEntropyRowsU0 =
200 sm86Unsigned32Zero
201
202def exactCrossEntropyRowsU4 =
203 (sm86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))
204
205def exactCrossEntropyRowsOffset028 =
206 (sm86Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0))
207
208def exactCrossEntropyRowsOffset160 =
209 (sm86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))
210
211def exactCrossEntropyRowsOffset168 =
212 (sm86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))
213
214def exactCrossEntropyRowsOffset170 =
215 (sm86Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0))
216
217def exactCrossEntropyRowsOffset190 =
218 (sm86Unsigned32 (byte 144) (byte 1) (byte 0) (byte 0))
219
220def exactCrossEntropyRowsOffset194 =
221 (sm86Unsigned32 (byte 148) (byte 1) (byte 0) (byte 0))
222
223def exactCrossEntropyRowsOffset198 =
224 (sm86Unsigned32 (byte 152) (byte 1) (byte 0) (byte 0))
225
226def exactCrossEntropyRowsSet0 =
227 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
228
229def exactCrossEntropyRowsSet1 =
230 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))
231
232def exactCrossEntropyRowsSet2 =
233 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))
234
235def exactCrossEntropyRowsSet3 =
236 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3))
237
238def exactCrossEntropyRowsWait0 =
239 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))
240
241def exactCrossEntropyRowsWait1 =
242 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier1))
243
244def exactCrossEntropyRowsWait2 =
245 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2))
246
247def exactCrossEntropyRowsWait3 =
248 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier3))
249
250def exactCrossEntropyRowsWhenNotP0 =
251 (lambda unrestricted body : (family SM86InstructionBody) .
252 (sm86NegatedPredicatedInstruction exactCrossEntropyRowsP0 body))
253
254def exactCrossEntropyRowsPrefixFor =
255 (lambda unrestricted vocabulary : Nat .
256 (exactCrossEntropySM86AlwaysNext
257 (constructor
258 SM86InstructionBody
259 SM86MoveConstant
260 exactCrossEntropyRowsR1
261 (byte 0)
262 exactCrossEntropyRowsOffset028
263 sm86SafeControl)
264 (exactCrossEntropySM86AlwaysNext
265 (constructor
266 SM86InstructionBody
267 SM86SpecialToRegister
268 exactCrossEntropyRowsR0
269 (constructor SM86SpecialRegister SM86ThreadIdX)
270 exactCrossEntropyRowsSet0)
271 (exactCrossEntropySM86AlwaysNext
272 (constructor
273 SM86InstructionBody
274 SM86SpecialToRegister
275 exactCrossEntropyRowsR1
276 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
277 exactCrossEntropyRowsSet0)
278 (exactCrossEntropySM86AlwaysNext
279 (constructor
280 SM86InstructionBody
281 SM86MoveImmediate
282 exactCrossEntropyRowsR2
283 exactCrossEntropyRowsU4
284 sm86SafeControl)
285 (exactCrossEntropySM86AlwaysNext
286 (constructor
287 SM86InstructionBody
288 SM86IntegerMultiplyAddImmediate
289 exactCrossEntropyRowsR3
290 exactCrossEntropyRowsR1
291 (sm86Unsigned32FromNaturalTruncated vocabulary)
292 exactCrossEntropyRowsR0
293 exactCrossEntropyRowsWait0)
294 (exactCrossEntropySM86AlwaysNext
295 (constructor
296 SM86InstructionBody
297 SM86IntegerMultiplyAddWideConstant
298 exactCrossEntropyRowsR4
299 exactCrossEntropyRowsR3
300 exactCrossEntropyRowsR2
301 (byte 0)
302 exactCrossEntropyRowsOffset168
303 sm86SafeControl)
304 (exactCrossEntropySM86AlwaysNext
305 (constructor
306 SM86InstructionBody
307 SM86IntegerMultiplyAddWideConstant
308 exactCrossEntropyRowsR6
309 exactCrossEntropyRowsR1
310 exactCrossEntropyRowsR2
311 (byte 0)
312 exactCrossEntropyRowsOffset170
313 sm86SafeControl)
314 (exactCrossEntropySM86AlwaysNext
315 (constructor
316 SM86InstructionBody
317 SM86IntegerMultiplyAddWideConstant
318 exactCrossEntropyRowsR16
319 exactCrossEntropyRowsR1
320 exactCrossEntropyRowsR2
321 (byte 0)
322 exactCrossEntropyRowsOffset160
323 sm86SafeControl)
324 (exactCrossEntropySM86AlwaysNext
325 (constructor
326 SM86InstructionBody
327 SM86PredicateGreaterThanImmediate
328 exactCrossEntropyRowsP0
329 exactCrossEntropyRowsR0
330 exactCrossEntropyRowsU0
331 sm86SafeControl)
332 (exactCrossEntropySM86AlwaysNext
333 (constructor
334 SM86InstructionBody
335 SM86LoadGlobal
336 exactCrossEntropyRowsR8
337 exactCrossEntropyRowsR4
338 exactCrossEntropyRowsU0
339 exactCrossEntropyRowsSet1)
340 (exactCrossEntropySM86AlwaysNext
341 (constructor
342 SM86InstructionBody
343 SM86LoadGlobal
344 exactCrossEntropyRowsR20
345 exactCrossEntropyRowsR6
346 exactCrossEntropyRowsU0
347 exactCrossEntropyRowsSet2)
348 (exactCrossEntropySM86AlwaysNext
349 (constructor
350 SM86InstructionBody
351 SM86IntegerAddThreeImmediate
352 exactCrossEntropyRowsR9
353 exactCrossEntropyRowsR8
354 exactCrossEntropyRowsU0
355 exactCrossEntropyRowsWait1)
356 (exactCrossEntropySM86AlwaysNext
357 (constructor
358 SM86InstructionBody
359 SM86IntegerAddThreeImmediate
360 exactCrossEntropyRowsR20
361 exactCrossEntropyRowsR20
362 exactCrossEntropyRowsU0
363 exactCrossEntropyRowsWait2)
364 exactCrossEntropySM86End))))))))))))))
365def exactCrossEntropyRowsMaximumTile =
366 (lambda unrestricted offset : (family SM86Unsigned32) .
367 (exactCrossEntropySM86AlwaysNext
368 (constructor
369 SM86InstructionBody
370 SM86LoadGlobal
371 exactCrossEntropyRowsR8
372 exactCrossEntropyRowsR4
373 offset
374 exactCrossEntropyRowsSet1)
375 (exactCrossEntropySM86AlwaysNext
376 (constructor
377 SM86InstructionBody
378 SM86FloatMinimumOrMaximum
379 exactCrossEntropyRowsR9
380 exactCrossEntropyRowsR9
381 exactCrossEntropyRowsR8
382 reductionSM86FloatMaximum
383 exactCrossEntropyRowsWait1)
384 exactCrossEntropySM86End)))
385
386def exactCrossEntropyRowsMaximumReduction : (family SM86Program) =
387 (reductionSM86ParameterizedIdentityReduction
388 reductionSM86MaximumCombine
389 exactCrossEntropyRowsR0
390 exactCrossEntropyRowsR9
391 exactCrossEntropyRowsR10
392 exactCrossEntropyRowsR11
393 reductionSM86NegativeInfinity)
394
395def exactCrossEntropyRowsSumPrefix : (family SM86Program) =
396 (exactCrossEntropySM86AlwaysNext
397 (constructor
398 SM86InstructionBody
399 SM86IntegerAddThreeImmediate
400 exactCrossEntropyRowsR12
401 exactCrossEntropyRowsR9
402 exactCrossEntropyRowsU0
403 sm86SafeControl)
404 (exactCrossEntropySM86AlwaysNext
405 (constructor
406 SM86InstructionBody
407 SM86FloatNegate
408 exactCrossEntropyRowsR13
409 exactCrossEntropyRowsR12
410 sm86SafeControl)
411 (exactCrossEntropySM86AlwaysNext
412 (constructor
413 SM86InstructionBody
414 SM86MoveConstant
415 exactCrossEntropyRowsR14
416 (byte 0)
417 exactCrossEntropyRowsOffset190
418 sm86SafeControl)
419 (exactCrossEntropySM86AlwaysNext
420 (constructor
421 SM86InstructionBody
422 SM86MoveImmediate
423 exactCrossEntropyRowsR9
424 exactCrossEntropyRowsU0
425 sm86SafeControl)
426 exactCrossEntropySM86End))))
427
428def exactCrossEntropyRowsSumTile =
429 (lambda unrestricted offset : (family SM86Unsigned32) .
430 (exactCrossEntropySM86AlwaysNext
431 (constructor
432 SM86InstructionBody
433 SM86LoadGlobal
434 exactCrossEntropyRowsR8
435 exactCrossEntropyRowsR4
436 offset
437 exactCrossEntropyRowsSet1)
438 (exactCrossEntropySM86AlwaysNext
439 (constructor
440 SM86InstructionBody
441 SM86FloatAdd
442 exactCrossEntropyRowsR8
443 exactCrossEntropyRowsR8
444 exactCrossEntropyRowsR13
445 exactCrossEntropyRowsWait1)
446 (exactCrossEntropySM86AlwaysNext
447 (constructor
448 SM86InstructionBody
449 SM86FloatMultiply
450 exactCrossEntropyRowsR8
451 exactCrossEntropyRowsR8
452 exactCrossEntropyRowsR14
453 sm86SafeControl)
454 (exactCrossEntropySM86AlwaysNext
455 (constructor
456 SM86InstructionBody
457 SM86MultiFunctionUnitApproximation
458 exactCrossEntropyRowsR8
459 exactCrossEntropyRowsR8
460 (constructor SM86MultiFunction SM86ExponentialBase2)
461 exactCrossEntropyRowsSet3)
462 (exactCrossEntropySM86AlwaysNext
463 (constructor
464 SM86InstructionBody
465 SM86FloatAdd
466 exactCrossEntropyRowsR9
467 exactCrossEntropyRowsR9
468 exactCrossEntropyRowsR8
469 exactCrossEntropyRowsWait3)
470 exactCrossEntropySM86End))))))
471
472def exactCrossEntropyRowsSumReduction : (family SM86Program) =
473 (reductionSM86ParameterizedIdentityReduction
474 reductionSM86SumCombine
475 exactCrossEntropyRowsR0
476 exactCrossEntropyRowsR9
477 exactCrossEntropyRowsR10
478 exactCrossEntropyRowsR11
479 exactCrossEntropyRowsU0)
480
481def exactCrossEntropyRowsSuffix : (family SM86Program) =
482 (exactCrossEntropySM86AlwaysNext
483 (constructor
484 SM86InstructionBody
485 SM86MultiFunctionUnitApproximation
486 exactCrossEntropyRowsR25
487 exactCrossEntropyRowsR9
488 (constructor SM86MultiFunction SM86LogarithmBase2)
489 exactCrossEntropyRowsSet3)
490 (exactCrossEntropySM86AlwaysNext
491 (constructor
492 SM86InstructionBody
493 SM86MoveConstant
494 exactCrossEntropyRowsR24
495 (byte 0)
496 exactCrossEntropyRowsOffset194
497 sm86SafeControl)
498 (exactCrossEntropySM86AlwaysNext
499 (constructor
500 SM86InstructionBody
501 SM86FloatMultiply
502 exactCrossEntropyRowsR25
503 exactCrossEntropyRowsR25
504 exactCrossEntropyRowsR24
505 exactCrossEntropyRowsWait3)
506 (exactCrossEntropySM86AlwaysNext
507 (constructor
508 SM86InstructionBody
509 SM86FloatAdd
510 exactCrossEntropyRowsR25
511 exactCrossEntropyRowsR25
512 exactCrossEntropyRowsR12
513 sm86SafeControl)
514 (exactCrossEntropySM86AlwaysNext
515 (constructor
516 SM86InstructionBody
517 SM86FloatNegate
518 exactCrossEntropyRowsR26
519 exactCrossEntropyRowsR20
520 sm86SafeControl)
521 (exactCrossEntropySM86AlwaysNext
522 (constructor
523 SM86InstructionBody
524 SM86FloatAdd
525 exactCrossEntropyRowsR25
526 exactCrossEntropyRowsR25
527 exactCrossEntropyRowsR26
528 sm86SafeControl)
529 (exactCrossEntropySM86Next
530 (exactCrossEntropyRowsWhenNotP0
531 (constructor
532 SM86InstructionBody
533 SM86StoreGlobal
534 exactCrossEntropyRowsR16
535 exactCrossEntropyRowsR25
536 exactCrossEntropyRowsU0
537 sm86SafeControl))
538 (exactCrossEntropySM86AlwaysNext
539 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
540 exactCrossEntropySM86End))))))))
541
542-- A row uses one 256-thread CTA. Thread t visits vocabulary positions
543-- t + 256*k; the first maximum tile is already read by the prefix. Derive
544-- both tile traversals from the shape so a larger vocabulary cannot silently
545-- reuse the legacy 48-tile image.
546def exactCrossEntropyRowsTileStrideBytes : Nat =
547 (naturalMultiply reductionSM86WarpSum256RequiredThreads 4)
548def exactCrossEntropyRowsTileOffsetFor =
549 (lambda unrestricted tile : Nat .
550 (sm86Unsigned32FromNaturalTruncated
551 (naturalMultiply tile exactCrossEntropyRowsTileStrideBytes)))
552def exactCrossEntropyRowsMaximumTilesFor =
553 (lambda unrestricted tiles : Nat .
554 (nat-eliminate
555 (lambda unrestricted current : Nat . (family SM86Program))
556 exactCrossEntropySM86End
557 (lambda unrestricted predecessor : Nat .
558 (lambda unrestricted induction : (family SM86Program) .
559 (sm86ProgramAppend
560 (exactCrossEntropyRowsMaximumTile
561 (exactCrossEntropyRowsTileOffsetFor
562 (naturalSaturatingSubtract
563 (naturalSaturatingSubtract tiles 1) predecessor)))
564 induction)))
565 (naturalSaturatingSubtract tiles 1)))
566def exactCrossEntropyRowsSumTilesFor =
567 (lambda unrestricted tiles : Nat .
568 (nat-eliminate
569 (lambda unrestricted current : Nat . (family SM86Program))
570 exactCrossEntropySM86End
571 (lambda unrestricted predecessor : Nat .
572 (lambda unrestricted induction : (family SM86Program) .
573 (sm86ProgramAppend
574 (exactCrossEntropyRowsSumTile
575 (exactCrossEntropyRowsTileOffsetFor
576 (naturalSaturatingSubtract
577 (naturalSaturatingSubtract tiles 1) predecessor)))
578 induction)))
579 tiles))
580def exactCrossEntropyRowsProgramForUnchecked =
581 (lambda unrestricted vocabulary : Nat .
582 (sm86ProgramAppend
583 (exactCrossEntropyRowsPrefixFor vocabulary)
584 (sm86ProgramAppend
585 (exactCrossEntropyRowsMaximumTilesFor
586 (naturalDivideUnchecked vocabulary reductionSM86WarpSum256RequiredThreads))
587 (sm86ProgramAppend
588 exactCrossEntropyRowsMaximumReduction
589 (sm86ProgramAppend
590 exactCrossEntropyRowsSumPrefix
591 (sm86ProgramAppend
592 (exactCrossEntropyRowsSumTilesFor
593 (naturalDivideUnchecked vocabulary reductionSM86WarpSum256RequiredThreads))
594 (sm86ProgramAppend exactCrossEntropyRowsSumReduction
595 exactCrossEntropyRowsSuffix)))))))
596def exactCrossEntropyRowsShapeAdmitted =
597 (lambda unrestricted rows : Nat . (lambda unrestricted vocabulary : Nat .
598 (naturalAnd (naturalNonzero rows)
599 (naturalAnd
600 (naturalIsZero
601 (naturalModuloUnchecked vocabulary reductionSM86WarpSum256RequiredThreads))
602 (naturalLess
603 (naturalMultiply rows (naturalMultiply vocabulary 4))
604 (naturalPowerOfTwo 32))))))
605def exactCrossEntropyRowsProgramFor =
606 (lambda unrestricted rows : Nat . (lambda unrestricted vocabulary : Nat .
607 (lambda erased admitted :
608 (equal Nat (exactCrossEntropyRowsShapeAdmitted rows vocabulary) 1) .
609 (exactCrossEntropyRowsProgramForUnchecked vocabulary))))
610
611def exactCrossEntropyRowsProgram : (family SM86Program) =
612 (exactCrossEntropyRowsProgramForUnchecked 12288)
613
614def exactCrossEntropyPartialR0 =
615 exactCrossEntropyRowsR0
616
617def exactCrossEntropyPartialR1 =
618 exactCrossEntropyRowsR1
619
620def exactCrossEntropyPartialR2 =
621 exactCrossEntropyRowsR2
622
623def exactCrossEntropyPartialR3 =
624 exactCrossEntropyRowsR3
625
626def exactCrossEntropyPartialR4 =
627 exactCrossEntropyRowsR4
628
629def exactCrossEntropyPartialR8 =
630 exactCrossEntropyRowsR8
631
632def exactCrossEntropyPartialR9 =
633 exactCrossEntropyRowsR9
634
635def exactCrossEntropyPartialR10 =
636 exactCrossEntropyRowsR10
637
638def exactCrossEntropyPartialR12 =
639 exactCrossEntropyRowsR12
640
641def exactCrossEntropyPartialP0 =
642 exactCrossEntropyRowsP0
643
644def exactCrossEntropyPartialU0 =
645 exactCrossEntropyRowsU0
646
647def exactCrossEntropyPartialU4 =
648 exactCrossEntropyRowsU4
649
650def exactCrossEntropyPartialU1024 =
651 (sm86Unsigned32 (byte 0) (byte 4) (byte 0) (byte 0))
652
653def exactCrossEntropyPartialSet0 =
654 exactCrossEntropyRowsSet0
655
656def exactCrossEntropyPartialSet1 =
657 exactCrossEntropyRowsSet1
658
659def exactCrossEntropyPartialWait0 =
660 exactCrossEntropyRowsWait0
661
662def exactCrossEntropyPartialWait1 =
663 exactCrossEntropyRowsWait1
664
665def exactCrossEntropyPartialWhenNotP0 =
666 (lambda unrestricted body : (family SM86InstructionBody) .
667 (sm86NegatedPredicatedInstruction exactCrossEntropyPartialP0 body))
668
669def exactCrossEntropyPartialPrefix : (family SM86Program) =
670 (exactCrossEntropySM86AlwaysNext
671 (constructor
672 SM86InstructionBody
673 SM86MoveConstant
674 exactCrossEntropyPartialR1
675 (byte 0)
676 exactCrossEntropyRowsOffset028
677 sm86SafeControl)
678 (exactCrossEntropySM86AlwaysNext
679 (constructor
680 SM86InstructionBody
681 SM86SpecialToRegister
682 exactCrossEntropyPartialR0
683 (constructor SM86SpecialRegister SM86ThreadIdX)
684 exactCrossEntropyPartialSet0)
685 (exactCrossEntropySM86AlwaysNext
686 (constructor
687 SM86InstructionBody
688 SM86SpecialToRegister
689 exactCrossEntropyPartialR1
690 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
691 exactCrossEntropyPartialSet0)
692 (exactCrossEntropySM86AlwaysNext
693 (constructor
694 SM86InstructionBody
695 SM86MoveImmediate
696 exactCrossEntropyPartialR2
697 exactCrossEntropyPartialU4
698 sm86SafeControl)
699 (exactCrossEntropySM86AlwaysNext
700 (constructor
701 SM86InstructionBody
702 SM86IntegerMultiplyAddImmediate
703 exactCrossEntropyPartialR3
704 exactCrossEntropyPartialR1
705 exactCrossEntropyPartialU1024
706 exactCrossEntropyPartialR0
707 exactCrossEntropyPartialWait0)
708 (exactCrossEntropySM86AlwaysNext
709 (constructor
710 SM86InstructionBody
711 SM86IntegerMultiplyAddWideConstant
712 exactCrossEntropyPartialR4
713 exactCrossEntropyPartialR3
714 exactCrossEntropyPartialR2
715 (byte 0)
716 exactCrossEntropyRowsOffset160
717 sm86SafeControl)
718 (exactCrossEntropySM86AlwaysNext
719 (constructor
720 SM86InstructionBody
721 SM86LoadGlobal
722 exactCrossEntropyPartialR8
723 exactCrossEntropyPartialR4
724 exactCrossEntropyPartialU0
725 exactCrossEntropyPartialSet1)
726 (exactCrossEntropySM86AlwaysNext
727 (constructor
728 SM86InstructionBody
729 SM86IntegerAddThreeImmediate
730 exactCrossEntropyPartialR8
731 exactCrossEntropyPartialR8
732 exactCrossEntropyPartialU0
733 exactCrossEntropyPartialWait1)
734 exactCrossEntropySM86End))))))))
735
736def exactCrossEntropyPartialReduction : (family SM86Program) =
737 (reductionSM86ParameterizedWarpSum1024
738 exactCrossEntropyPartialR0
739 exactCrossEntropyPartialR8
740 exactCrossEntropyPartialR9)
741
742def exactCrossEntropyPartialSuffixFor =
743 (lambda unrestricted rows : Nat .
744 (exactCrossEntropySM86AlwaysNext
745 (constructor
746 SM86InstructionBody
747 SM86PredicateGreaterThanImmediate
748 exactCrossEntropyPartialP0
749 exactCrossEntropyPartialR0
750 exactCrossEntropyPartialU0
751 sm86SafeControl)
752 (exactCrossEntropySM86AlwaysNext
753 (constructor
754 SM86InstructionBody
755 SM86IntegerAddThreeImmediate
756 exactCrossEntropyPartialR10
757 exactCrossEntropyPartialR1
758 (sm86Unsigned32FromNaturalTruncated rows)
759 sm86SafeControl)
760 (exactCrossEntropySM86AlwaysNext
761 (constructor
762 SM86InstructionBody
763 SM86IntegerMultiplyAddWideConstant
764 exactCrossEntropyPartialR12
765 exactCrossEntropyPartialR10
766 exactCrossEntropyPartialR2
767 (byte 0)
768 exactCrossEntropyRowsOffset160
769 sm86SafeControl)
770 (exactCrossEntropySM86Next
771 (exactCrossEntropyPartialWhenNotP0
772 (constructor
773 SM86InstructionBody
774 SM86StoreGlobal
775 exactCrossEntropyPartialR12
776 exactCrossEntropyPartialR8
777 exactCrossEntropyPartialU0
778 sm86SafeControl))
779 (exactCrossEntropySM86AlwaysNext
780 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
781 exactCrossEntropySM86End))))))
782
783def exactCrossEntropyPartialProgramForUnchecked =
784 (lambda unrestricted rows : Nat .
785 (sm86ProgramAppend
786 exactCrossEntropyPartialPrefix
787 (sm86ProgramAppend exactCrossEntropyPartialReduction
788 (exactCrossEntropyPartialSuffixFor rows))))
789
790def exactCrossEntropyFinalizeR0 =
791 exactCrossEntropyRowsR0
792
793def exactCrossEntropyFinalizeR1 =
794 exactCrossEntropyRowsR1
795
796def exactCrossEntropyFinalizeR2 =
797 exactCrossEntropyRowsR2
798
799def exactCrossEntropyFinalizeR3 =
800 exactCrossEntropyRowsR3
801
802def exactCrossEntropyFinalizeR4 =
803 exactCrossEntropyRowsR4
804
805def exactCrossEntropyFinalizeR8 =
806 exactCrossEntropyRowsR8
807
808def exactCrossEntropyFinalizeR9 =
809 exactCrossEntropyRowsR9
810
811def exactCrossEntropyFinalizeR10 =
812 exactCrossEntropyRowsR10
813
814def exactCrossEntropyFinalizeR12 =
815 exactCrossEntropyRowsR12
816
817def exactCrossEntropyFinalizeP0 =
818 exactCrossEntropyRowsP0
819
820def exactCrossEntropyFinalizeU0 =
821 exactCrossEntropyRowsU0
822
823def exactCrossEntropyFinalizeU1 =
824 sm86Unsigned32One
825
826def exactCrossEntropyFinalizeU4 =
827 exactCrossEntropyRowsU4
828
829def exactCrossEntropyFinalizeSet0 =
830 exactCrossEntropyRowsSet0
831
832def exactCrossEntropyFinalizeSet1 =
833 exactCrossEntropyRowsSet1
834
835def exactCrossEntropyFinalizeWait0 =
836 exactCrossEntropyRowsWait0
837
838def exactCrossEntropyFinalizeWait1 =
839 exactCrossEntropyRowsWait1
840
841def exactCrossEntropyFinalizeWhenP0 =
842 (lambda unrestricted body : (family SM86InstructionBody) .
843 (sm86PredicatedInstruction exactCrossEntropyFinalizeP0 body))
844
845def exactCrossEntropyFinalizeWhenNotP0 =
846 (lambda unrestricted body : (family SM86InstructionBody) .
847 (sm86NegatedPredicatedInstruction exactCrossEntropyFinalizeP0 body))
848
849def exactCrossEntropyFinalizePrefixFor =
850 (lambda unrestricted rows : Nat .
851 (lambda unrestricted partials : Nat .
852 (exactCrossEntropySM86AlwaysNext
853 (constructor
854 SM86InstructionBody
855 SM86MoveConstant
856 exactCrossEntropyFinalizeR1
857 (byte 0)
858 exactCrossEntropyRowsOffset028
859 sm86SafeControl)
860 (exactCrossEntropySM86AlwaysNext
861 (constructor
862 SM86InstructionBody
863 SM86SpecialToRegister
864 exactCrossEntropyFinalizeR0
865 (constructor SM86SpecialRegister SM86ThreadIdX)
866 exactCrossEntropyFinalizeSet0)
867 (exactCrossEntropySM86AlwaysNext
868 (constructor
869 SM86InstructionBody
870 SM86MoveImmediate
871 exactCrossEntropyFinalizeR2
872 exactCrossEntropyFinalizeU4
873 exactCrossEntropyFinalizeWait0)
874 (exactCrossEntropySM86AlwaysNext
875 (constructor
876 SM86InstructionBody
877 SM86IntegerAddThreeImmediate
878 exactCrossEntropyFinalizeR3
879 exactCrossEntropyFinalizeR0
880 (sm86Unsigned32FromNaturalTruncated rows)
881 sm86SafeControl)
882 (exactCrossEntropySM86AlwaysNext
883 (constructor
884 SM86InstructionBody
885 SM86IntegerMultiplyAddWideConstant
886 exactCrossEntropyFinalizeR4
887 exactCrossEntropyFinalizeR3
888 exactCrossEntropyFinalizeR2
889 (byte 0)
890 exactCrossEntropyRowsOffset160
891 sm86SafeControl)
892 (exactCrossEntropySM86AlwaysNext
893 (constructor
894 SM86InstructionBody
895 SM86LoadGlobal
896 exactCrossEntropyFinalizeR8
897 exactCrossEntropyFinalizeR4
898 exactCrossEntropyFinalizeU0
899 exactCrossEntropyFinalizeSet1)
900 (exactCrossEntropySM86AlwaysNext
901 (constructor
902 SM86InstructionBody
903 SM86IntegerAddThreeImmediate
904 exactCrossEntropyFinalizeR8
905 exactCrossEntropyFinalizeR8
906 exactCrossEntropyFinalizeU0
907 exactCrossEntropyFinalizeWait1)
908 (exactCrossEntropySM86AlwaysNext
909 (constructor
910 SM86InstructionBody
911 SM86PredicateGreaterThanImmediate
912 exactCrossEntropyFinalizeP0
913 exactCrossEntropyFinalizeR0
914 (sm86Unsigned32FromNaturalTruncated
915 (naturalSaturatingSubtract partials 1))
916 sm86SafeControl)
917 (exactCrossEntropySM86Next
918 (exactCrossEntropyFinalizeWhenP0
919 (constructor
920 SM86InstructionBody
921 SM86MoveImmediate
922 exactCrossEntropyFinalizeR8
923 exactCrossEntropyFinalizeU0
924 sm86SafeControl))
925 exactCrossEntropySM86End)))))))))))
926
927def exactCrossEntropyFinalizeReduction : (family SM86Program) =
928 (reductionSM86ParameterizedLegacyWarpSum
929 exactCrossEntropyFinalizeR0
930 exactCrossEntropyFinalizeR8
931 exactCrossEntropyFinalizeR9
932 exactCrossEntropyFinalizeU1)
933
934def exactCrossEntropyFinalizeSuffix : (family SM86Program) =
935 (exactCrossEntropySM86AlwaysNext
936 (constructor
937 SM86InstructionBody
938 SM86PredicateGreaterThanImmediate
939 exactCrossEntropyFinalizeP0
940 exactCrossEntropyFinalizeR0
941 exactCrossEntropyFinalizeU0
942 sm86SafeControl)
943 (exactCrossEntropySM86AlwaysNext
944 (constructor
945 SM86InstructionBody
946 SM86MoveConstant
947 exactCrossEntropyFinalizeR10
948 (byte 0)
949 exactCrossEntropyRowsOffset198
950 sm86SafeControl)
951 (exactCrossEntropySM86AlwaysNext
952 (constructor
953 SM86InstructionBody
954 SM86FloatMultiply
955 exactCrossEntropyFinalizeR8
956 exactCrossEntropyFinalizeR8
957 exactCrossEntropyFinalizeR10
958 sm86SafeControl)
959 (exactCrossEntropySM86AlwaysNext
960 (constructor
961 SM86InstructionBody
962 SM86IntegerMultiplyAddWideConstant
963 exactCrossEntropyFinalizeR12
964 sm86ZeroRegister
965 exactCrossEntropyFinalizeR2
966 (byte 0)
967 exactCrossEntropyRowsOffset168
968 sm86SafeControl)
969 (exactCrossEntropySM86Next
970 (exactCrossEntropyFinalizeWhenNotP0
971 (constructor
972 SM86InstructionBody
973 SM86StoreGlobal
974 exactCrossEntropyFinalizeR12
975 exactCrossEntropyFinalizeR8
976 exactCrossEntropyFinalizeU0
977 sm86SafeControl))
978 (exactCrossEntropySM86AlwaysNext
979 (constructor SM86InstructionBody SM86Exit sm86SafeControl)
980 exactCrossEntropySM86End))))))
981
982def exactCrossEntropyFinalizeProgramForUnchecked =
983 (lambda unrestricted rows : Nat .
984 (sm86ProgramAppend
985 (exactCrossEntropyFinalizePrefixFor rows
986 (naturalDivideUnchecked rows reductionSM86WarpSum1024RequiredThreads))
987 (sm86ProgramAppend exactCrossEntropyFinalizeReduction
988 exactCrossEntropyFinalizeSuffix)))
989-- Both reductions read a complete CTA, including lanes masked after their
990-- load. The workspace therefore needs 64 slots beyond the loss rows even
991-- when fewer row groups contain useful partials.
992def exactCrossEntropyMeanPartialSlots : Nat =
993 reductionSM86WarpSum64RequiredThreads
994def exactCrossEntropyMeanShapeAdmitted =
995 (lambda unrestricted rows : Nat .
996 (naturalAnd (naturalNonzero rows)
997 (naturalAnd
998 (naturalIsZero (naturalModuloUnchecked rows
999 reductionSM86WarpSum1024RequiredThreads))
1000 (naturalAnd
1001 (naturalLessOrEqual
1002 (naturalDivideUnchecked rows reductionSM86WarpSum1024RequiredThreads)
1003 exactCrossEntropyMeanPartialSlots)
1004 (naturalLess (naturalAdd rows exactCrossEntropyMeanPartialSlots)
1005 (naturalPowerOfTwo 32))))))
1006def exactCrossEntropyPartialProgramFor =
1007 (lambda unrestricted rows : Nat .
1008 (lambda erased admitted :
1009 (equal Nat (exactCrossEntropyMeanShapeAdmitted rows) 1) .
1010 (exactCrossEntropyPartialProgramForUnchecked rows)))
1011def exactCrossEntropyFinalizeProgramFor =
1012 (lambda unrestricted rows : Nat .
1013 (lambda erased admitted :
1014 (equal Nat (exactCrossEntropyMeanShapeAdmitted rows) 1) .
1015 (exactCrossEntropyFinalizeProgramForUnchecked rows)))
1016def exactCrossEntropyPartialProgram : (family SM86Program) =
1017 (exactCrossEntropyPartialProgramForUnchecked 6144)
1018def exactCrossEntropyFinalizeProgram : (family SM86Program) =
1019 (exactCrossEntropyFinalizeProgramForUnchecked 6144)
1020
1021def exactCrossEntropySM86ProgramFor =
1022 (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) .
1023 (eliminate
1024 ExactCrossEntropySM86Variant
1025 (lambda unrestricted current : (family ExactCrossEntropySM86Variant) . (family SM86Program))
1026 variant
1027 (branch ExactCrossEntropyRows . exactCrossEntropyRowsProgram)
1028 (branch ReduceExactRowLosses . exactCrossEntropyPartialProgram)
1029 (branch FinalizeExactMeanLoss . exactCrossEntropyFinalizeProgram)))
1030
1031def exactCrossEntropySM86N6 =
1032 (byte-to-nat (byte 6))
1033
1034def exactCrossEntropySM86N16 =
1035 (byte-to-nat (byte 16))
1036
1037def exactCrossEntropySM86N24 =
1038 (byte-to-nat (byte 24))
1039
1040def exactCrossEntropySM86N32 =
1041 (byte-to-nat (byte 32))
1042
1043def exactCrossEntropySM86N34 =
1044 (byte-to-nat (byte 34))
1045
1046def exactCrossEntropySM86N43 =
1047 (byte-to-nat (byte 43))
1048
1049def exactCrossEntropySM86N47 =
1050 (byte-to-nat (byte 47))
1051
1052def exactCrossEntropySM86N48 =
1053 (byte-to-nat (byte 48))
1054
1055def exactCrossEntropySM86N64 =
1056 (byte-to-nat (byte 64))
1057
1058def exactCrossEntropySM86N96 =
1059 (byte-to-nat (byte 96))
1060
1061def exactCrossEntropySM86N104 =
1062 (byte-to-nat (byte 104))
1063
1064def exactCrossEntropySM86N112 =
1065 (byte-to-nat (byte 112))
1066
1067def exactCrossEntropySM86N128 =
1068 (byte-to-nat (byte 128))
1069
1070def exactCrossEntropySM86N144 =
1071 (byte-to-nat (byte 144))
1072
1073def exactCrossEntropySM86N148 =
1074 (byte-to-nat (byte 148))
1075
1076def exactCrossEntropySM86N152 =
1077 (byte-to-nat (byte 152))
1078
1079def exactCrossEntropySM86N171 =
1080 (byte-to-nat (byte 171))
1081
1082def exactCrossEntropySM86N256 =
1083 (succ (byte-to-nat (byte 255)))
1084
1085def exactCrossEntropySM86N427 =
1086 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N171)
1087
1088def exactCrossEntropySM86N1024 =
1089 (naturalPowerOfTwo (byte-to-nat (byte 10)))
1090
1091def exactCrossEntropySM86N6144 =
1092 (naturalMultiply exactCrossEntropySM86N24 exactCrossEntropySM86N256)
1093
1094def exactCrossEntropySM86N6150 =
1095 (naturalAdd exactCrossEntropySM86N6144 exactCrossEntropySM86N6)
1096
1097def exactCrossEntropySM86N12288 =
1098 (naturalMultiply exactCrossEntropySM86N48 exactCrossEntropySM86N256)
1099
1100def exactCrossEntropySM86LogitsElements =
1101 (naturalMultiply exactCrossEntropySM86N6144 exactCrossEntropySM86N12288)
1102
1103def exactCrossEntropySM86Offset160Natural =
1104 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N96)
1105
1106def exactCrossEntropySM86Offset168Natural =
1107 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N104)
1108
1109def exactCrossEntropySM86Offset170Natural =
1110 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N112)
1111
1112def exactCrossEntropySM86Offset190Natural =
1113 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N144)
1114
1115def exactCrossEntropySM86Offset194Natural =
1116 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N148)
1117
1118def exactCrossEntropySM86Offset198Natural =
1119 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N152)
1120
1121def exactCrossEntropySM86ABI : (family ExactCrossEntropySM86ABI) =
1122 (constructor
1123 ExactCrossEntropySM86ABI
1124 ExactCrossEntropySM86ABIValue
1125 exactCrossEntropySM86Offset160Natural
1126 exactCrossEntropySM86Offset168Natural
1127 exactCrossEntropySM86Offset168Natural
1128 exactCrossEntropySM86Offset170Natural
1129 exactCrossEntropySM86Offset190Natural
1130 exactCrossEntropySM86Offset194Natural
1131 exactCrossEntropySM86Offset198Natural)
1132
1133def exactCrossEntropySM86ExtentsFor =
1134 (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) .
1135 (eliminate
1136 ExactCrossEntropySM86Variant
1137 (lambda unrestricted current : (family ExactCrossEntropySM86Variant) .
1138 (family ExactCrossEntropySM86Extents))
1139 variant
1140 (branch
1141 ExactCrossEntropyRows
1142 .
1143 (constructor
1144 ExactCrossEntropySM86Extents
1145 ExactCrossEntropySM86ExtentsValue
1146 zero
1147 zero
1148 zero
1149 exactCrossEntropySM86N6144
1150 exactCrossEntropySM86N6144
1151 exactCrossEntropySM86LogitsElements
1152 exactCrossEntropySM86N6144
1153 zero
1154 zero))
1155 (branch
1156 ReduceExactRowLosses
1157 .
1158 (constructor
1159 ExactCrossEntropySM86Extents
1160 ExactCrossEntropySM86ExtentsValue
1161 zero
1162 exactCrossEntropySM86N6144
1163 exactCrossEntropySM86N6144
1164 exactCrossEntropySM86N6
1165 exactCrossEntropySM86N6150
1166 zero
1167 zero
1168 zero
1169 zero))
1170 (branch
1171 FinalizeExactMeanLoss
1172 .
1173 (constructor
1174 ExactCrossEntropySM86Extents
1175 ExactCrossEntropySM86ExtentsValue
1176 exactCrossEntropySM86N6144
1177 exactCrossEntropySM86N6
1178 zero
1179 zero
1180 exactCrossEntropySM86N6150
1181 zero
1182 zero
1183 (succ zero)
1184 zero))))
1185
1186def exactCrossEntropySM86ManifestFor =
1187 (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) .
1188 (eliminate
1189 ExactCrossEntropySM86Variant
1190 (lambda unrestricted current : (family ExactCrossEntropySM86Variant) .
1191 (family ExactCrossEntropySM86Manifest))
1192 variant
1193 (branch
1194 ExactCrossEntropyRows
1195 .
1196 (constructor
1197 ExactCrossEntropySM86Manifest
1198 ExactCrossEntropySM86ManifestValue
1199 variant
1200 exactCrossEntropySM86N427
1201 (naturalMultiply exactCrossEntropySM86N427 exactCrossEntropySM86N16)
1202 exactCrossEntropySM86N32
1203 exactCrossEntropySM86N128
1204 exactCrossEntropySM86N6144
1205 exactCrossEntropySM86N256
1206 exactCrossEntropySM86ABI
1207 (exactCrossEntropySM86ExtentsFor variant)
1208 (byte-to-nat (byte 107))
1209 (byte-to-nat (byte 140))
1210 (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N128)
1211 (naturalAdd exactCrossEntropySM86N256 (byte-to-nat (byte 162)))
1212 exactCrossEntropySM86N6144
1213 exactCrossEntropySM86N12288
1214 exactCrossEntropySM86N256
1215 exactCrossEntropySM86N48
1216 zero))
1217 (branch
1218 ReduceExactRowLosses
1219 .
1220 (constructor
1221 ExactCrossEntropySM86Manifest
1222 ExactCrossEntropySM86ManifestValue
1223 variant
1224 exactCrossEntropySM86N43
1225 (naturalMultiply exactCrossEntropySM86N43 exactCrossEntropySM86N16)
1226 exactCrossEntropySM86N24
1227 exactCrossEntropySM86N128
1228 exactCrossEntropySM86N6
1229 exactCrossEntropySM86N1024
1230 exactCrossEntropySM86ABI
1231 (exactCrossEntropySM86ExtentsFor variant)
1232 (byte-to-nat (byte 8))
1233 (byte-to-nat (byte 37))
1234 zero
1235 zero
1236 exactCrossEntropySM86N6144
1237 exactCrossEntropySM86N12288
1238 exactCrossEntropySM86N256
1239 exactCrossEntropySM86N48
1240 zero))
1241 (branch
1242 FinalizeExactMeanLoss
1243 .
1244 (constructor
1245 ExactCrossEntropySM86Manifest
1246 ExactCrossEntropySM86ManifestValue
1247 variant
1248 exactCrossEntropySM86N47
1249 (naturalMultiply exactCrossEntropySM86N47 exactCrossEntropySM86N16)
1250 exactCrossEntropySM86N24
1251 exactCrossEntropySM86N128
1252 (succ zero)
1253 exactCrossEntropySM86N64
1254 exactCrossEntropySM86ABI
1255 (exactCrossEntropySM86ExtentsFor variant)
1256 (byte-to-nat (byte 9))
1257 (byte-to-nat (byte 40))
1258 zero
1259 zero
1260 exactCrossEntropySM86N6144
1261 exactCrossEntropySM86N12288
1262 exactCrossEntropySM86N256
1263 exactCrossEntropySM86N48
1264 zero))))
1265
1266def exactCrossEntropySM86ManifestInstructions =
1267 (lambda unrestricted manifest : (family ExactCrossEntropySM86Manifest) .
1268 (eliminate
1269 ExactCrossEntropySM86Manifest
1270 (lambda unrestricted current : (family ExactCrossEntropySM86Manifest) . Nat)
1271 manifest
1272 (branch
1273 ExactCrossEntropySM86ManifestValue
1274 variant
1275 instructions
1276 bytes
1277 registers
1278 shared
1279 grid
1280 block
1281 abi
1282 extents
1283 r0s
1284 r0e
1285 r1s
1286 r1e
1287 rows
1288 vocabulary
1289 tile
1290 tiles
1291 hostFallback
1292 .
1293 instructions)))
1294
1295def exactCrossEntropySM86ManifestBytes =
1296 (lambda unrestricted manifest : (family ExactCrossEntropySM86Manifest) .
1297 (eliminate
1298 ExactCrossEntropySM86Manifest
1299 (lambda unrestricted current : (family ExactCrossEntropySM86Manifest) . Nat)
1300 manifest
1301 (branch
1302 ExactCrossEntropySM86ManifestValue
1303 variant
1304 instructions
1305 bytes
1306 registers
1307 shared
1308 grid
1309 block
1310 abi
1311 extents
1312 r0s
1313 r0e
1314 r1s
1315 r1e
1316 rows
1317 vocabulary
1318 tile
1319 tiles
1320 hostFallback
1321 .
1322 bytes)))
1323
1324def exactCrossEntropySM86TelemetryFor =
1325 (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) .
1326 (lambda unrestricted instructions : Nat .
1327 (lambda unrestricted bytes : Nat .
1328 (constructor
1329 ExactCrossEntropySM86Telemetry
1330 ExactCrossEntropySM86TelemetryValue
1331 (exactCrossEntropySM86ManifestFor variant)
1332 instructions
1333 bytes))))
1334
1335def exactCrossEntropySM86Build =
1336 (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) .
1337 (app
1338 (lambda unrestricted program : (family SM86Program) .
1339 (app
1340 (lambda unrestricted observedInstructions : Nat .
1341 (app
1342 (lambda unrestricted manifest : (family ExactCrossEntropySM86Manifest) .
1343 (nat-eliminate
1344 (lambda unrestricted countMatched : Nat .
1345 (family ExactCrossEntropySM86BuildResult))
1346 (constructor
1347 ExactCrossEntropySM86BuildResult
1348 ExactCrossEntropySM86ContractFailed
1349 (constructor
1350 ExactCrossEntropySM86FailureCode
1351 ExactCrossEntropyInstructionCountMismatch)
1352 (exactCrossEntropySM86TelemetryFor variant observedInstructions zero))
1353 (lambda unrestricted countPredecessor : Nat .
1354 (lambda unrestricted countInduction : (family ExactCrossEntropySM86BuildResult) .
1355 (app
1356 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
1357 (eliminate
1358 SM86ProgramEncodingResult
1359 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1360 (family ExactCrossEntropySM86BuildResult))
1361 encoding
1362 (branch
1363 SM86ProgramEncodingSucceeded
1364 bytes
1365 encodingTelemetry
1366 .
1367 (app
1368 (lambda unrestricted telemetry : (family ExactCrossEntropySM86Telemetry) .
1369 (nat-eliminate
1370 (lambda unrestricted bytesMatched : Nat .
1371 (family ExactCrossEntropySM86BuildResult))
1372 (constructor
1373 ExactCrossEntropySM86BuildResult
1374 ExactCrossEntropySM86ContractFailed
1375 (constructor
1376 ExactCrossEntropySM86FailureCode
1377 ExactCrossEntropyEncodedByteCountMismatch)
1378 telemetry)
1379 (lambda unrestricted bytesPredecessor : Nat .
1380 (lambda unrestricted bytesInduction : (family ExactCrossEntropySM86BuildResult) .
1381 (app
1382 (lambda unrestricted identityResult : (family SHA256HexResult) .
1383 (eliminate
1384 SHA256HexResult
1385 (lambda unrestricted current : (family SHA256HexResult) .
1386 (family ExactCrossEntropySM86BuildResult))
1387 identityResult
1388 (branch
1389 SHA256HexSucceeded
1390 identity
1391 identityTelemetry
1392 .
1393 (nat-eliminate
1394 (lambda unrestricted identityLengthMatched : Nat .
1395 (family ExactCrossEntropySM86BuildResult))
1396 (constructor
1397 ExactCrossEntropySM86BuildResult
1398 ExactCrossEntropySM86ImageIdentityFailed
1399 (constructor
1400 ExactCrossEntropySM86FailureCode
1401 ExactCrossEntropyIdentityLengthInvalid)
1402 identityResult
1403 telemetry)
1404 (lambda unrestricted identityLengthPredecessor : Nat .
1405 (lambda unrestricted identityLengthInduction : (family ExactCrossEntropySM86BuildResult) .
1406 (constructor
1407 ExactCrossEntropySM86BuildResult
1408 ExactCrossEntropySM86BuildSucceeded
1409 bytes
1410 identity
1411 encodingTelemetry
1412 identityTelemetry
1413 telemetry)))
1414 (naturalEqual
1415 (bytes-length identity)
1416 exactCrossEntropySM86N64)))
1417 (branch
1418 SHA256HexFailed
1419 error
1420 ordinal
1421 identityTelemetry
1422 .
1423 (constructor
1424 ExactCrossEntropySM86BuildResult
1425 ExactCrossEntropySM86ImageIdentityFailed
1426 (constructor
1427 ExactCrossEntropySM86FailureCode
1428 ExactCrossEntropyIdentityFailed)
1429 identityResult
1430 telemetry))))
1431 (sha256Hex bytes))))
1432 (naturalEqual
1433 (bytes-length bytes)
1434 (exactCrossEntropySM86ManifestBytes manifest))))
1435 (exactCrossEntropySM86TelemetryFor
1436 variant
1437 observedInstructions
1438 (bytes-length bytes))))
1439 (branch
1440 SM86ProgramEncodingFailed
1441 instructionIndex
1442 failure
1443 encodingTelemetry
1444 .
1445 (constructor
1446 ExactCrossEntropySM86BuildResult
1447 ExactCrossEntropySM86ImageEncodingFailed
1448 (constructor
1449 ExactCrossEntropySM86FailureCode
1450 ExactCrossEntropyEncodingFailed)
1451 encoding
1452 (exactCrossEntropySM86TelemetryFor
1453 variant
1454 observedInstructions
1455 zero)))))
1456 (sm86EncodeProgram program))))
1457 (naturalEqual
1458 observedInstructions
1459 (exactCrossEntropySM86ManifestInstructions manifest))))
1460 (exactCrossEntropySM86ManifestFor variant)))
1461 (sm86ProgramCount program)))
1462 (exactCrossEntropySM86ProgramFor variant)))
1463
1464def exactCrossEntropySM86BuildRows =
1465 (exactCrossEntropySM86Build (constructor ExactCrossEntropySM86Variant ExactCrossEntropyRows))
1466
1467def exactCrossEntropySM86BuildPartial =
1468 (exactCrossEntropySM86Build (constructor ExactCrossEntropySM86Variant ReduceExactRowLosses))
1469
1470def exactCrossEntropySM86BuildFinalize =
1471 (exactCrossEntropySM86Build (constructor ExactCrossEntropySM86Variant FinalizeExactMeanLoss))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.