Realization.Nvidia.SM86.ExactCrossEntropyBackwardSM86

1module Realization.Nvidia.SM86.ExactCrossEntropyBackwardSM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.NumericSemantics
8import Accelerator.SM86.Program
9import Accelerator.SM86.Types
10import Data.SHA256Digest
11import Realization.Nvidia.SM86.ExactCrossEntropySM86
12import Std.Natural
13
14-- Exact full-vocabulary logit gradient for coppelius. The preceding exact
15-- forward pass supplies loss[r] = logsumexp(logits[r]) - correct[r], so this
16-- kernel reconstructs logsumexp as loss + correct and writes
17-- (exp(logit - logsumexp) - one_hot(target)) / rows. Grid Y selects one of 48
18-- vocabulary tiles, avoiding a source-level 48-way instruction expansion.
19family ExactCrossEntropyBackwardSM86FailureCode : Type 0
20constructor ExactCrossEntropyBackwardInstructionCountMismatch
21constructor ExactCrossEntropyBackwardEncodedByteCountMismatch
22constructor ExactCrossEntropyBackwardEncodingFailed
23constructor ExactCrossEntropyBackwardIdentityFailed
24constructor ExactCrossEntropyBackwardIdentityLengthInvalid
25
26end-family
27
28family ExactCrossEntropyBackwardSM86ABI : Type 0
29constructor ExactCrossEntropyBackwardSM86ABIValue
30field unrestricted exactCrossEntropyBackwardABIGradient : Nat
31field unrestricted exactCrossEntropyBackwardABILogits : Nat
32field unrestricted exactCrossEntropyBackwardABILoss : Nat
33field unrestricted exactCrossEntropyBackwardABICorrectLogit : Nat
34field unrestricted exactCrossEntropyBackwardABITarget : Nat
35field unrestricted exactCrossEntropyBackwardABILog2E : Nat
36field unrestricted exactCrossEntropyBackwardABIInverseRows : Nat
37
38end-family
39
40family ExactCrossEntropyBackwardSM86Extents : Type 0
41constructor ExactCrossEntropyBackwardSM86ExtentsValue
42field unrestricted exactCrossEntropyBackwardExtentRows : Nat
43field unrestricted exactCrossEntropyBackwardExtentVocabulary : Nat
44field unrestricted exactCrossEntropyBackwardExtentLogitsRead : Nat
45field unrestricted exactCrossEntropyBackwardExtentGradientWrite : Nat
46field unrestricted exactCrossEntropyBackwardExtentLossRead : Nat
47field unrestricted exactCrossEntropyBackwardExtentCorrectLogitRead : Nat
48field unrestricted exactCrossEntropyBackwardExtentTargetRead : Nat
49
50end-family
51
52family ExactCrossEntropyBackwardSM86Manifest : Type 0
53constructor ExactCrossEntropyBackwardSM86ManifestValue
54field unrestricted exactCrossEntropyBackwardManifestExpectedInstructions : Nat
55field unrestricted exactCrossEntropyBackwardManifestExpectedEncodedBytes : Nat
56field unrestricted exactCrossEntropyBackwardManifestRegisters : Nat
57field unrestricted exactCrossEntropyBackwardManifestSharedBytes : Nat
58field unrestricted exactCrossEntropyBackwardManifestGridX : Nat
59field unrestricted exactCrossEntropyBackwardManifestGridY : Nat
60field unrestricted exactCrossEntropyBackwardManifestBlockX : Nat
61field unrestricted exactCrossEntropyBackwardManifestABI : (family ExactCrossEntropyBackwardSM86ABI)
62field unrestricted exactCrossEntropyBackwardManifestExtents : (family ExactCrossEntropyBackwardSM86Extents)
63field unrestricted exactCrossEntropyBackwardManifestHostFallbackOperations : Nat
64
65end-family
66
67family ExactCrossEntropyBackwardSM86Telemetry : Type 0
68constructor ExactCrossEntropyBackwardSM86TelemetryValue
69field unrestricted exactCrossEntropyBackwardTelemetryManifest : (family ExactCrossEntropyBackwardSM86Manifest)
70field unrestricted exactCrossEntropyBackwardTelemetryObservedInstructions : Nat
71field unrestricted exactCrossEntropyBackwardTelemetryObservedEncodedBytes : Nat
72
73end-family
74
75family ExactCrossEntropyBackwardSM86BuildResult : Type 0
76constructor ExactCrossEntropyBackwardSM86BuildSucceeded
77field unrestricted exactCrossEntropyBackwardEncodedBytes : Bytes
78field unrestricted exactCrossEntropyBackwardImageIdentity : Bytes
79field unrestricted exactCrossEntropyBackwardProgramEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
80field unrestricted exactCrossEntropyBackwardIdentityTelemetry : (family SHA256DigestTelemetry)
81field unrestricted exactCrossEntropyBackwardBuildTelemetry : (family ExactCrossEntropyBackwardSM86Telemetry)
82constructor ExactCrossEntropyBackwardSM86ContractFailed
83field unrestricted exactCrossEntropyBackwardContractFailure : (family ExactCrossEntropyBackwardSM86FailureCode)
84field unrestricted exactCrossEntropyBackwardContractFailureTelemetry : (family ExactCrossEntropyBackwardSM86Telemetry)
85constructor ExactCrossEntropyBackwardSM86ImageEncodingFailed
86field unrestricted exactCrossEntropyBackwardEncodingFailure : (family ExactCrossEntropyBackwardSM86FailureCode)
87field unrestricted exactCrossEntropyBackwardFailedEncoding : (family SM86ProgramEncodingResult)
88field unrestricted exactCrossEntropyBackwardEncodingFailureTelemetry : (family ExactCrossEntropyBackwardSM86Telemetry)
89constructor ExactCrossEntropyBackwardSM86ImageIdentityFailed
90field unrestricted exactCrossEntropyBackwardIdentityFailure : (family ExactCrossEntropyBackwardSM86FailureCode)
91field unrestricted exactCrossEntropyBackwardFailedIdentity : (family SHA256HexResult)
92field unrestricted exactCrossEntropyBackwardIdentityFailureTelemetry : (family ExactCrossEntropyBackwardSM86Telemetry)
93
94end-family
95
96def exactCrossEntropyBackwardR0 =
97  (sm86Register (byte 0))
98
99def exactCrossEntropyBackwardR1 =
100  (sm86Register (byte 1))
101
102def exactCrossEntropyBackwardR2 =
103  (sm86Register (byte 2))
104
105def exactCrossEntropyBackwardR3 =
106  (sm86Register (byte 3))
107
108def exactCrossEntropyBackwardR4 =
109  (sm86Register (byte 4))
110
111def exactCrossEntropyBackwardR5 =
112  (sm86Register (byte 5))
113
114def exactCrossEntropyBackwardR6 =
115  (sm86Register (byte 6))
116
117def exactCrossEntropyBackwardR7 =
118  (sm86Register (byte 7))
119
120def exactCrossEntropyBackwardR8 =
121  (sm86Register (byte 8))
122
123def exactCrossEntropyBackwardR9 =
124  (sm86Register (byte 9))
125
126def exactCrossEntropyBackwardR10 =
127  (sm86Register (byte 10))
128
129def exactCrossEntropyBackwardR11 =
130  (sm86Register (byte 11))
131
132def exactCrossEntropyBackwardR12 =
133  (sm86Register (byte 12))
134
135def exactCrossEntropyBackwardR13 =
136  (sm86Register (byte 13))
137
138def exactCrossEntropyBackwardR14 =
139  (sm86Register (byte 14))
140
141def exactCrossEntropyBackwardR15 =
142  (sm86Register (byte 15))
143
144def exactCrossEntropyBackwardR16 =
145  (sm86Register (byte 16))
146
147def exactCrossEntropyBackwardR17 =
148  (sm86Register (byte 17))
149
150def exactCrossEntropyBackwardR18 =
151  (sm86Register (byte 18))
152
153def exactCrossEntropyBackwardR19 =
154  (sm86Register (byte 19))
155
156def exactCrossEntropyBackwardR20 =
157  (sm86Register (byte 20))
158
159def exactCrossEntropyBackwardR21 =
160  (sm86Register (byte 21))
161
162def exactCrossEntropyBackwardR22 =
163  (sm86Register (byte 22))
164
165def exactCrossEntropyBackwardR23 =
166  (sm86Register (byte 23))
167
168def exactCrossEntropyBackwardR24 =
169  (sm86Register (byte 24))
170
171def exactCrossEntropyBackwardR25 =
172  (sm86Register (byte 25))
173
174def exactCrossEntropyBackwardP0 : (family SM86Predicate) =
175  (constructor SM86Predicate SM86Predicate0)
176
177def exactCrossEntropyBackwardGradientArgument : Nat = 0
178def exactCrossEntropyBackwardLogitsArgument : Nat = 1
179def exactCrossEntropyBackwardLossRowsArgument : Nat = 2
180def exactCrossEntropyBackwardCorrectLogitArgument : Nat = 3
181def exactCrossEntropyBackwardTargetsArgument : Nat = 4
182def exactCrossEntropyBackwardLog2EArgument : Nat = 6
183def exactCrossEntropyBackwardInverseRowsArgument : Nat = 7
184
185def exactCrossEntropyBackwardU0 =
186  sm86Unsigned32Zero
187
188def exactCrossEntropyBackwardU4 =
189  (sm86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))
190
191def exactCrossEntropyBackwardU256 =
192  (sm86Unsigned32 (byte 0) (byte 1) (byte 0) (byte 0))
193
194def exactCrossEntropyBackwardU12288 =
195  (sm86Unsigned32 (byte 0) (byte 48) (byte 0) (byte 0))
196
197def exactCrossEntropyBackwardOffset160 =
198  (sm86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))
199
200def exactCrossEntropyBackwardOffset168 =
201  (sm86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))
202
203def exactCrossEntropyBackwardOffset170 =
204  (sm86Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0))
205
206def exactCrossEntropyBackwardOffset178 =
207  (sm86Unsigned32 (byte 120) (byte 1) (byte 0) (byte 0))
208
209def exactCrossEntropyBackwardOffset180 =
210  (sm86Unsigned32 (byte 128) (byte 1) (byte 0) (byte 0))
211
212def exactCrossEntropyBackwardOffset190 =
213  (sm86Unsigned32 (byte 144) (byte 1) (byte 0) (byte 0))
214
215def exactCrossEntropyBackwardOffset198 =
216  (sm86Unsigned32 (byte 152) (byte 1) (byte 0) (byte 0))
217
218def exactCrossEntropyBackwardNext =
219  (lambda unrestricted body : (family SM86InstructionBody) .
220    (lambda unrestricted tail : (family SM86Program) .
221      (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))
222
223def exactCrossEntropyBackwardGuardedNext =
224  (lambda unrestricted instruction : (family SM86Instruction) .
225    (lambda unrestricted tail : (family SM86Program) .
226      (constructor SM86Program SM86ProgramNext instruction tail)))
227
228def exactCrossEntropyBackwardEnd : (family SM86Program) =
229  (constructor SM86Program SM86ProgramEnd)
230
231def exactCrossEntropyBackwardProgramForUnchecked =
232  (lambda unrestricted vocabulary : Nat .
233  (exactCrossEntropyBackwardNext
234    (constructor
235      SM86InstructionBody
236      SM86SpecialToRegister
237      exactCrossEntropyBackwardR0
238      (constructor SM86SpecialRegister SM86ThreadIdX)
239      exactCrossEntropyRowsSet0)
240    (exactCrossEntropyBackwardNext
241      (constructor
242        SM86InstructionBody
243        SM86SpecialToRegister
244        exactCrossEntropyBackwardR1
245        (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
246        exactCrossEntropyRowsSet0)
247      (exactCrossEntropyBackwardNext
248        (constructor
249          SM86InstructionBody
250          SM86SpecialToRegister
251          exactCrossEntropyBackwardR2
252          (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY)
253          exactCrossEntropyRowsSet0)
254        (exactCrossEntropyBackwardNext
255          (constructor
256            SM86InstructionBody
257            SM86IntegerMultiplyAddImmediate
258            exactCrossEntropyBackwardR3
259            exactCrossEntropyBackwardR2
260            exactCrossEntropyBackwardU256
261            exactCrossEntropyBackwardR0
262            exactCrossEntropyRowsWait0)
263          (exactCrossEntropyBackwardNext
264            (constructor
265              SM86InstructionBody
266              SM86MoveImmediate
267              exactCrossEntropyBackwardR5
268              exactCrossEntropyBackwardU4
269              sm86SafeControl)
270            (exactCrossEntropyBackwardNext
271              (constructor
272                SM86InstructionBody
273                SM86IntegerMultiplyAddImmediate
274                exactCrossEntropyBackwardR4
275                exactCrossEntropyBackwardR1
276                (sm86Unsigned32FromNaturalTruncated vocabulary)
277                exactCrossEntropyBackwardR3
278                sm86SafeControl)
279              (exactCrossEntropyBackwardNext
280                (constructor
281                  SM86InstructionBody
282                  SM86IntegerMultiplyAddWideConstant
283                  exactCrossEntropyBackwardR6
284                  exactCrossEntropyBackwardR4
285                  exactCrossEntropyBackwardR5
286                  (byte 0)
287                  exactCrossEntropyBackwardOffset168
288                  sm86SafeControl)
289                (exactCrossEntropyBackwardNext
290                  (constructor
291                    SM86InstructionBody
292                    SM86IntegerMultiplyAddWideConstant
293                    exactCrossEntropyBackwardR8
294                    exactCrossEntropyBackwardR4
295                    exactCrossEntropyBackwardR5
296                    (byte 0)
297                    exactCrossEntropyBackwardOffset160
298                    sm86SafeControl)
299                  (exactCrossEntropyBackwardNext
300                    (constructor
301                      SM86InstructionBody
302                      SM86IntegerMultiplyAddWideConstant
303                      exactCrossEntropyBackwardR10
304                      exactCrossEntropyBackwardR1
305                      exactCrossEntropyBackwardR5
306                      (byte 0)
307                      exactCrossEntropyBackwardOffset170
308                      sm86SafeControl)
309                    (exactCrossEntropyBackwardNext
310                      (constructor
311                        SM86InstructionBody
312                        SM86IntegerMultiplyAddWideConstant
313                        exactCrossEntropyBackwardR12
314                        exactCrossEntropyBackwardR1
315                        exactCrossEntropyBackwardR5
316                        (byte 0)
317                        exactCrossEntropyBackwardOffset178
318                        sm86SafeControl)
319                      (exactCrossEntropyBackwardNext
320                        (constructor
321                          SM86InstructionBody
322                          SM86IntegerMultiplyAddWideConstant
323                          exactCrossEntropyBackwardR14
324                          exactCrossEntropyBackwardR1
325                          exactCrossEntropyBackwardR5
326                          (byte 0)
327                          exactCrossEntropyBackwardOffset180
328                          sm86SafeControl)
329                        (exactCrossEntropyBackwardNext
330                          (constructor
331                            SM86InstructionBody
332                            SM86LoadGlobal
333                            exactCrossEntropyBackwardR16
334                            exactCrossEntropyBackwardR10
335                            exactCrossEntropyBackwardU0
336                            exactCrossEntropyRowsSet0)
337                          (exactCrossEntropyBackwardNext
338                            (constructor
339                              SM86InstructionBody
340                              SM86LoadGlobal
341                              exactCrossEntropyBackwardR17
342                              exactCrossEntropyBackwardR12
343                              exactCrossEntropyBackwardU0
344                              exactCrossEntropyRowsSet1)
345                            (exactCrossEntropyBackwardNext
346                              (constructor
347                                SM86InstructionBody
348                                SM86LoadGlobal
349                                exactCrossEntropyBackwardR21
350                                exactCrossEntropyBackwardR14
351                                exactCrossEntropyBackwardU0
352                                exactCrossEntropyRowsSet2)
353                              (exactCrossEntropyBackwardNext
354                                (constructor
355                                  SM86InstructionBody
356                                  SM86IntegerAddThreeImmediate
357                                  exactCrossEntropyBackwardR21
358                                  exactCrossEntropyBackwardR21
359                                  exactCrossEntropyBackwardU0
360                                  exactCrossEntropyRowsWait2)
361                                (exactCrossEntropyBackwardNext
362                                  (constructor
363                                    SM86InstructionBody
364                                    SM86IntegerAddThreeImmediate
365                                    exactCrossEntropyBackwardR17
366                                    exactCrossEntropyBackwardR17
367                                    exactCrossEntropyBackwardU0
368                                    exactCrossEntropyRowsWait1)
369                                  (exactCrossEntropyBackwardNext
370                                    (constructor
371                                      SM86InstructionBody
372                                      SM86FloatAdd
373                                      exactCrossEntropyBackwardR18
374                                      exactCrossEntropyBackwardR16
375                                      exactCrossEntropyBackwardR17
376                                      exactCrossEntropyRowsWait0)
377                                    (exactCrossEntropyBackwardNext
378                                      (constructor
379                                        SM86InstructionBody
380                                        SM86FloatNegate
381                                        exactCrossEntropyBackwardR19
382                                        exactCrossEntropyBackwardR18
383                                        sm86SafeControl)
384                                      (exactCrossEntropyBackwardNext
385                                        (constructor
386                                        SM86InstructionBody
387                                        SM86MoveConstant
388                                        exactCrossEntropyBackwardR20
389                                        (byte 0)
390                                        exactCrossEntropyBackwardOffset190
391                                        sm86SafeControl)
392                                        (exactCrossEntropyBackwardNext
393                                        (constructor
394                                        SM86InstructionBody
395                                        SM86MoveConstant
396                                        exactCrossEntropyBackwardR22
397                                        (byte 0)
398                                        exactCrossEntropyBackwardOffset198
399                                        sm86SafeControl)
400                                        (exactCrossEntropyBackwardNext
401                                        (constructor
402                                        SM86InstructionBody
403                                        SM86FloatNegate
404                                        exactCrossEntropyBackwardR23
405                                        exactCrossEntropyBackwardR22
406                                        sm86SafeControl)
407                                        (exactCrossEntropyBackwardNext
408                                        (constructor
409                                        SM86InstructionBody
410                                        SM86LoadGlobal
411                                        exactCrossEntropyBackwardR24
412                                        exactCrossEntropyBackwardR6
413                                        exactCrossEntropyBackwardU0
414                                        exactCrossEntropyRowsSet1)
415                                        (exactCrossEntropyBackwardNext
416                                        (constructor
417                                        SM86InstructionBody
418                                        SM86FloatAdd
419                                        exactCrossEntropyBackwardR24
420                                        exactCrossEntropyBackwardR24
421                                        exactCrossEntropyBackwardR19
422                                        exactCrossEntropyRowsWait1)
423                                        (exactCrossEntropyBackwardNext
424                                        (constructor
425                                        SM86InstructionBody
426                                        SM86FloatMultiply
427                                        exactCrossEntropyBackwardR24
428                                        exactCrossEntropyBackwardR24
429                                        exactCrossEntropyBackwardR20
430                                        sm86SafeControl)
431                                        (exactCrossEntropyBackwardNext
432                                        (constructor
433                                        SM86InstructionBody
434                                        SM86MultiFunctionUnitApproximation
435                                        exactCrossEntropyBackwardR24
436                                        exactCrossEntropyBackwardR24
437                                        (constructor SM86MultiFunction SM86ExponentialBase2)
438                                        exactCrossEntropyRowsSet3)
439                                        (exactCrossEntropyBackwardNext
440                                        (constructor
441                                        SM86InstructionBody
442                                        SM86FloatMultiply
443                                        exactCrossEntropyBackwardR24
444                                        exactCrossEntropyBackwardR24
445                                        exactCrossEntropyBackwardR22
446                                        exactCrossEntropyRowsWait3)
447                                        (exactCrossEntropyBackwardNext
448                                        (constructor
449                                        SM86InstructionBody
450                                        SM86LogicThreeInputTruthTable
451                                        exactCrossEntropyBackwardR25
452                                        exactCrossEntropyBackwardR3
453                                        exactCrossEntropyBackwardR21
454                                        (byte 60)
455                                        sm86SafeControl)
456                                        (exactCrossEntropyBackwardNext
457                                        (constructor
458                                        SM86InstructionBody
459                                        SM86PredicateGreaterThanImmediate
460                                        exactCrossEntropyBackwardP0
461                                        exactCrossEntropyBackwardR25
462                                        exactCrossEntropyBackwardU0
463                                        sm86SafeControl)
464                                        (exactCrossEntropyBackwardGuardedNext
465                                        (sm86NegatedPredicatedInstruction
466                                        exactCrossEntropyBackwardP0
467                                        (constructor
468                                        SM86InstructionBody
469                                        SM86FloatAdd
470                                        exactCrossEntropyBackwardR24
471                                        exactCrossEntropyBackwardR24
472                                        exactCrossEntropyBackwardR23
473                                        sm86SafeControl))
474                                        (exactCrossEntropyBackwardNext
475                                        (constructor
476                                        SM86InstructionBody
477                                        SM86StoreGlobal
478                                        exactCrossEntropyBackwardR8
479                                        exactCrossEntropyBackwardR24
480                                        exactCrossEntropyBackwardU0
481                                        sm86SafeControl)
482                                        (exactCrossEntropyBackwardNext
483                                        (constructor SM86InstructionBody SM86Exit sm86SafeControl)
484                                        exactCrossEntropyBackwardEnd))))))))))))))))))))))))))))))))
485
486def exactCrossEntropyBackwardProgramFor =
487  (lambda unrestricted rows : Nat . (lambda unrestricted vocabulary : Nat .
488    (lambda erased admitted :
489      (equal Nat (exactCrossEntropyRowsShapeAdmitted rows vocabulary) 1) .
490      (exactCrossEntropyBackwardProgramForUnchecked vocabulary))))
491def exactCrossEntropyBackwardProgram : (family SM86Program) =
492  (exactCrossEntropyBackwardProgramForUnchecked 12288)
493
494def exactCrossEntropyBackwardABI =
495  (constructor
496    ExactCrossEntropyBackwardSM86ABI
497    ExactCrossEntropyBackwardSM86ABIValue
498    352
499    360
500    368
501    376
502    384
503    400
504    408)
505
506def exactCrossEntropyBackwardElements =
507  (naturalMultiply 1024 12288)
508
509def exactCrossEntropyBackwardExtents =
510  (constructor
511    ExactCrossEntropyBackwardSM86Extents
512    ExactCrossEntropyBackwardSM86ExtentsValue
513    1024
514    12288
515    exactCrossEntropyBackwardElements
516    exactCrossEntropyBackwardElements
517    1024
518    1024
519    1024)
520
521def exactCrossEntropyBackwardManifest =
522  (constructor
523    ExactCrossEntropyBackwardSM86Manifest
524    ExactCrossEntropyBackwardSM86ManifestValue
525    31
526    496
527    32
528    zero
529    1024
530    48
531    256
532    exactCrossEntropyBackwardABI
533    exactCrossEntropyBackwardExtents
534    zero)
535
536def exactCrossEntropyBackwardManifestInstructions =
537  (lambda unrestricted manifest : (family ExactCrossEntropyBackwardSM86Manifest) .
538    (eliminate
539      ExactCrossEntropyBackwardSM86Manifest
540      (lambda unrestricted current : (family ExactCrossEntropyBackwardSM86Manifest) . Nat)
541      manifest
542      (branch
543        ExactCrossEntropyBackwardSM86ManifestValue
544        instructions
545        bytes
546        registers
547        shared
548        gridX
549        gridY
550        blockX
551        abi
552        extents
553        hostFallback
554        .
555        instructions)))
556
557def exactCrossEntropyBackwardManifestBytes =
558  (lambda unrestricted manifest : (family ExactCrossEntropyBackwardSM86Manifest) .
559    (eliminate
560      ExactCrossEntropyBackwardSM86Manifest
561      (lambda unrestricted current : (family ExactCrossEntropyBackwardSM86Manifest) . Nat)
562      manifest
563      (branch
564        ExactCrossEntropyBackwardSM86ManifestValue
565        instructions
566        bytes
567        registers
568        shared
569        gridX
570        gridY
571        blockX
572        abi
573        extents
574        hostFallback
575        .
576        bytes)))
577
578def exactCrossEntropyBackwardTelemetryFor =
579  (lambda unrestricted instructions : Nat .
580    (lambda unrestricted bytes : Nat .
581      (constructor
582        ExactCrossEntropyBackwardSM86Telemetry
583        ExactCrossEntropyBackwardSM86TelemetryValue
584        exactCrossEntropyBackwardManifest
585        instructions
586        bytes)))
587
588def exactCrossEntropyBackwardBuild =
589  (app
590    (lambda unrestricted observedInstructions : Nat .
591      (nat-eliminate
592        (lambda unrestricted countMatched : Nat . (family ExactCrossEntropyBackwardSM86BuildResult))
593        (constructor
594          ExactCrossEntropyBackwardSM86BuildResult
595          ExactCrossEntropyBackwardSM86ContractFailed
596          (constructor
597            ExactCrossEntropyBackwardSM86FailureCode
598            ExactCrossEntropyBackwardInstructionCountMismatch)
599          (exactCrossEntropyBackwardTelemetryFor observedInstructions zero))
600        (lambda unrestricted countPredecessor : Nat .
601          (lambda unrestricted countInduction : (family ExactCrossEntropyBackwardSM86BuildResult) .
602            (app
603              (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
604                (eliminate
605                  SM86ProgramEncodingResult
606                  (lambda unrestricted current : (family SM86ProgramEncodingResult) .
607                    (family ExactCrossEntropyBackwardSM86BuildResult))
608                  encoding
609                  (branch
610                    SM86ProgramEncodingSucceeded
611                    bytes
612                    encodingTelemetry
613                    .
614                    (app
615                      (lambda unrestricted telemetry : (family ExactCrossEntropyBackwardSM86Telemetry) .
616                        (nat-eliminate
617                          (lambda unrestricted bytesMatched : Nat .
618                            (family ExactCrossEntropyBackwardSM86BuildResult))
619                          (constructor
620                            ExactCrossEntropyBackwardSM86BuildResult
621                            ExactCrossEntropyBackwardSM86ContractFailed
622                            (constructor
623                              ExactCrossEntropyBackwardSM86FailureCode
624                              ExactCrossEntropyBackwardEncodedByteCountMismatch)
625                            telemetry)
626                          (lambda unrestricted bytesPredecessor : Nat .
627                            (lambda unrestricted bytesInduction : (family ExactCrossEntropyBackwardSM86BuildResult) .
628                              (app
629                                (lambda unrestricted identityResult : (family SHA256HexResult) .
630                                  (eliminate
631                                    SHA256HexResult
632                                    (lambda unrestricted current : (family SHA256HexResult) .
633                                      (family ExactCrossEntropyBackwardSM86BuildResult))
634                                    identityResult
635                                    (branch
636                                      SHA256HexSucceeded
637                                      identity
638                                      identityTelemetry
639                                      .
640                                      (nat-eliminate
641                                        (lambda unrestricted identityLengthMatched : Nat .
642                                        (family ExactCrossEntropyBackwardSM86BuildResult))
643                                        (constructor
644                                        ExactCrossEntropyBackwardSM86BuildResult
645                                        ExactCrossEntropyBackwardSM86ImageIdentityFailed
646                                        (constructor
647                                        ExactCrossEntropyBackwardSM86FailureCode
648                                        ExactCrossEntropyBackwardIdentityLengthInvalid)
649                                        identityResult
650                                        telemetry)
651                                        (lambda unrestricted identityLengthPredecessor : Nat .
652                                        (lambda unrestricted identityLengthInduction : (family ExactCrossEntropyBackwardSM86BuildResult) .
653                                        (constructor
654                                        ExactCrossEntropyBackwardSM86BuildResult
655                                        ExactCrossEntropyBackwardSM86BuildSucceeded
656                                        bytes
657                                        identity
658                                        encodingTelemetry
659                                        identityTelemetry
660                                        telemetry)))
661                                        (naturalEqual (bytes-length identity) 64)))
662                                    (branch
663                                      SHA256HexFailed
664                                      error
665                                      ordinal
666                                      identityTelemetry
667                                      .
668                                      (constructor
669                                        ExactCrossEntropyBackwardSM86BuildResult
670                                        ExactCrossEntropyBackwardSM86ImageIdentityFailed
671                                        (constructor
672                                        ExactCrossEntropyBackwardSM86FailureCode
673                                        ExactCrossEntropyBackwardIdentityFailed)
674                                        identityResult
675                                        telemetry))))
676                                (sha256Hex bytes))))
677                          (naturalEqual
678                            (bytes-length bytes)
679                            (exactCrossEntropyBackwardManifestBytes
680                              exactCrossEntropyBackwardManifest))))
681                      (exactCrossEntropyBackwardTelemetryFor
682                        observedInstructions
683                        (bytes-length bytes))))
684                  (branch
685                    SM86ProgramEncodingFailed
686                    instructionIndex
687                    failure
688                    encodingTelemetry
689                    .
690                    (constructor
691                      ExactCrossEntropyBackwardSM86BuildResult
692                      ExactCrossEntropyBackwardSM86ImageEncodingFailed
693                      (constructor
694                        ExactCrossEntropyBackwardSM86FailureCode
695                        ExactCrossEntropyBackwardEncodingFailed)
696                      encoding
697                      (exactCrossEntropyBackwardTelemetryFor observedInstructions zero)))))
698              (sm86EncodeProgram exactCrossEntropyBackwardProgram))))
699        (naturalEqual
700          observedInstructions
701          (exactCrossEntropyBackwardManifestInstructions exactCrossEntropyBackwardManifest))))
702    (sm86ProgramCount exactCrossEntropyBackwardProgram))