module Realization.Nvidia.SM86.ExactCrossEntropySM86 import Accelerator.SM86.Control import Accelerator.SM86.Immediate import Accelerator.SM86.Instruction import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.Program import Data.SHA256Digest import Realization.Nvidia.SM86.ReductionSM86 import Std.Natural import Accelerator.SM86.NumericSemantics import Accelerator.SM86.Types family ExactCrossEntropySM86Variant : Type 0 constructor ExactCrossEntropyRows constructor ReduceExactRowLosses constructor FinalizeExactMeanLoss end-family family ExactCrossEntropySM86FailureCode : Type 0 constructor ExactCrossEntropyInstructionCountMismatch constructor ExactCrossEntropyEncodedByteCountMismatch constructor ExactCrossEntropyEncodingFailed constructor ExactCrossEntropyIdentityFailed constructor ExactCrossEntropyIdentityLengthInvalid end-family family ExactCrossEntropySM86ABI : Type 0 constructor ExactCrossEntropySM86ABIValue field unrestricted exactCrossEntropyABIWorkspace : Nat field unrestricted exactCrossEntropyABILogits : Nat field unrestricted exactCrossEntropyABIScalar : Nat field unrestricted exactCrossEntropyABICorrectLogit : Nat field unrestricted exactCrossEntropyABILog2E : Nat field unrestricted exactCrossEntropyABILn2 : Nat field unrestricted exactCrossEntropyABIInverseRows : Nat end-family family ExactCrossEntropySM86Extents : Type 0 constructor ExactCrossEntropySM86ExtentsValue field unrestricted exactCrossEntropyExtentWorkspaceReadOffsetElements : Nat field unrestricted exactCrossEntropyExtentWorkspaceReadElements : Nat field unrestricted exactCrossEntropyExtentWorkspaceWriteOffsetElements : Nat field unrestricted exactCrossEntropyExtentWorkspaceWriteElements : Nat field unrestricted exactCrossEntropyExtentWorkspaceAddressableElements : Nat field unrestricted exactCrossEntropyExtentLogitsReadElements : Nat field unrestricted exactCrossEntropyExtentCorrectLogitsReadElements : Nat field unrestricted exactCrossEntropyExtentScalarWriteElements : Nat field unrestricted exactCrossEntropyExtentGlobalVocabularyMaterializations : Nat end-family family ExactCrossEntropySM86Manifest : Type 0 constructor ExactCrossEntropySM86ManifestValue field unrestricted exactCrossEntropyManifestVariant : (family ExactCrossEntropySM86Variant) field unrestricted exactCrossEntropyManifestExpectedInstructions : Nat field unrestricted exactCrossEntropyManifestExpectedEncodedBytes : Nat field unrestricted exactCrossEntropyManifestRegisters : Nat field unrestricted exactCrossEntropyManifestSharedBytes : Nat field unrestricted exactCrossEntropyManifestGridX : Nat field unrestricted exactCrossEntropyManifestBlockX : Nat field unrestricted exactCrossEntropyManifestABI : (family ExactCrossEntropySM86ABI) field unrestricted exactCrossEntropyManifestExtents : (family ExactCrossEntropySM86Extents) field unrestricted exactCrossEntropyManifestReduction0Start : Nat field unrestricted exactCrossEntropyManifestReduction0End : Nat field unrestricted exactCrossEntropyManifestReduction1Start : Nat field unrestricted exactCrossEntropyManifestReduction1End : Nat field unrestricted exactCrossEntropyManifestRows : Nat field unrestricted exactCrossEntropyManifestVocabulary : Nat field unrestricted exactCrossEntropyManifestVocabularyTileElements : Nat field unrestricted exactCrossEntropyManifestVocabularyTiles : Nat field unrestricted exactCrossEntropyManifestHostFallbackOperations : Nat end-family family ExactCrossEntropySM86Telemetry : Type 0 constructor ExactCrossEntropySM86TelemetryValue field unrestricted exactCrossEntropyTelemetryManifest : (family ExactCrossEntropySM86Manifest) field unrestricted exactCrossEntropyTelemetryObservedInstructions : Nat field unrestricted exactCrossEntropyTelemetryObservedEncodedBytes : Nat end-family family ExactCrossEntropySM86BuildResult : Type 0 constructor ExactCrossEntropySM86BuildSucceeded field unrestricted exactCrossEntropyEncodedBytes : Bytes field unrestricted exactCrossEntropyImageIdentity : Bytes field unrestricted exactCrossEntropyProgramEncodingTelemetry : (family SM86ProgramEncodingTelemetry) field unrestricted exactCrossEntropyIdentityTelemetry : (family SHA256DigestTelemetry) field unrestricted exactCrossEntropyBuildTelemetry : (family ExactCrossEntropySM86Telemetry) constructor ExactCrossEntropySM86ContractFailed field unrestricted exactCrossEntropyContractFailure : (family ExactCrossEntropySM86FailureCode) field unrestricted exactCrossEntropyContractFailureTelemetry : (family ExactCrossEntropySM86Telemetry) constructor ExactCrossEntropySM86ImageEncodingFailed field unrestricted exactCrossEntropyEncodingFailure : (family ExactCrossEntropySM86FailureCode) field unrestricted exactCrossEntropyFailedEncoding : (family SM86ProgramEncodingResult) field unrestricted exactCrossEntropyEncodingFailureTelemetry : (family ExactCrossEntropySM86Telemetry) constructor ExactCrossEntropySM86ImageIdentityFailed field unrestricted exactCrossEntropyIdentityFailure : (family ExactCrossEntropySM86FailureCode) field unrestricted exactCrossEntropyFailedIdentity : (family SHA256HexResult) field unrestricted exactCrossEntropyIdentityFailureTelemetry : (family ExactCrossEntropySM86Telemetry) end-family def exactCrossEntropySM86FailureCodeBytes = (lambda unrestricted code : (family ExactCrossEntropySM86FailureCode) . (eliminate ExactCrossEntropySM86FailureCode (lambda unrestricted current : (family ExactCrossEntropySM86FailureCode) . Bytes) code (branch ExactCrossEntropyInstructionCountMismatch . b"ALPHA-SM86-ECE-001") (branch ExactCrossEntropyEncodedByteCountMismatch . b"ALPHA-SM86-ECE-002") (branch ExactCrossEntropyEncodingFailed . b"ALPHA-SM86-ECE-003") (branch ExactCrossEntropyIdentityFailed . b"ALPHA-SM86-ECE-004") (branch ExactCrossEntropyIdentityLengthInvalid . b"ALPHA-SM86-ECE-005"))) def exactCrossEntropySM86Next = (lambda unrestricted instruction : (family SM86Instruction) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext instruction tail))) def exactCrossEntropySM86AlwaysNext = (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (exactCrossEntropySM86Next (sm86Instruction body) tail))) def exactCrossEntropySM86End : (family SM86Program) = (constructor SM86Program SM86ProgramEnd) def exactCrossEntropyRowsR0 = (sm86Register (byte 0)) def exactCrossEntropyRowsR1 = (sm86Register (byte 1)) def exactCrossEntropyRowsR2 = (sm86Register (byte 2)) def exactCrossEntropyRowsR3 = (sm86Register (byte 3)) def exactCrossEntropyRowsR4 = (sm86Register (byte 4)) def exactCrossEntropyRowsR6 = (sm86Register (byte 6)) def exactCrossEntropyRowsR8 = (sm86Register (byte 8)) def exactCrossEntropyRowsR9 = (sm86Register (byte 9)) def exactCrossEntropyRowsR10 = (sm86Register (byte 10)) def exactCrossEntropyRowsR11 = (sm86Register (byte 11)) def exactCrossEntropyRowsR12 = (sm86Register (byte 12)) def exactCrossEntropyRowsR13 = (sm86Register (byte 13)) def exactCrossEntropyRowsR14 = (sm86Register (byte 14)) def exactCrossEntropyRowsR16 = (sm86Register (byte 16)) def exactCrossEntropyRowsR20 = (sm86Register (byte 20)) def exactCrossEntropyRowsR24 = (sm86Register (byte 24)) def exactCrossEntropyRowsR25 = (sm86Register (byte 25)) def exactCrossEntropyRowsR26 = (sm86Register (byte 26)) def exactCrossEntropyRowsP0 : (family SM86Predicate) = (constructor SM86Predicate SM86Predicate0) def exactCrossEntropyRowsOutputArgument : Nat = 0 def exactCrossEntropyRowsLogitsArgument : Nat = 1 def exactCrossEntropyRowsCorrectLogitArgument : Nat = 2 -- The shared CB0 ABI reserves six pointer slots before F32 scalar words. def exactCrossEntropyRowsScalarPairArgument : Nat = 6 def exactCrossEntropyMeanWorkspaceArgument : Nat = 0 def exactCrossEntropyMeanOutputArgument : Nat = 1 def exactCrossEntropyMeanInverseRowsArgument : Nat = 7 def exactCrossEntropyRowsU0 = sm86Unsigned32Zero def exactCrossEntropyRowsU4 = (sm86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0)) def exactCrossEntropyRowsOffset028 = (sm86Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0)) def exactCrossEntropyRowsOffset160 = (sm86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0)) def exactCrossEntropyRowsOffset168 = (sm86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0)) def exactCrossEntropyRowsOffset170 = (sm86Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0)) def exactCrossEntropyRowsOffset190 = (sm86Unsigned32 (byte 144) (byte 1) (byte 0) (byte 0)) def exactCrossEntropyRowsOffset194 = (sm86Unsigned32 (byte 148) (byte 1) (byte 0) (byte 0)) def exactCrossEntropyRowsOffset198 = (sm86Unsigned32 (byte 152) (byte 1) (byte 0) (byte 0)) def exactCrossEntropyRowsSet0 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0)) def exactCrossEntropyRowsSet1 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1)) def exactCrossEntropyRowsSet2 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2)) def exactCrossEntropyRowsSet3 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3)) def exactCrossEntropyRowsWait0 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0)) def exactCrossEntropyRowsWait1 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier1)) def exactCrossEntropyRowsWait2 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2)) def exactCrossEntropyRowsWait3 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier3)) def exactCrossEntropyRowsWhenNotP0 = (lambda unrestricted body : (family SM86InstructionBody) . (sm86NegatedPredicatedInstruction exactCrossEntropyRowsP0 body)) def exactCrossEntropyRowsPrefixFor = (lambda unrestricted vocabulary : Nat . (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveConstant exactCrossEntropyRowsR1 (byte 0) exactCrossEntropyRowsOffset028 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86SpecialToRegister exactCrossEntropyRowsR0 (constructor SM86SpecialRegister SM86ThreadIdX) exactCrossEntropyRowsSet0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86SpecialToRegister exactCrossEntropyRowsR1 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) exactCrossEntropyRowsSet0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveImmediate exactCrossEntropyRowsR2 exactCrossEntropyRowsU4 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate exactCrossEntropyRowsR3 exactCrossEntropyRowsR1 (sm86Unsigned32FromNaturalTruncated vocabulary) exactCrossEntropyRowsR0 exactCrossEntropyRowsWait0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant exactCrossEntropyRowsR4 exactCrossEntropyRowsR3 exactCrossEntropyRowsR2 (byte 0) exactCrossEntropyRowsOffset168 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant exactCrossEntropyRowsR6 exactCrossEntropyRowsR1 exactCrossEntropyRowsR2 (byte 0) exactCrossEntropyRowsOffset170 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant exactCrossEntropyRowsR16 exactCrossEntropyRowsR1 exactCrossEntropyRowsR2 (byte 0) exactCrossEntropyRowsOffset160 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate exactCrossEntropyRowsP0 exactCrossEntropyRowsR0 exactCrossEntropyRowsU0 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86LoadGlobal exactCrossEntropyRowsR8 exactCrossEntropyRowsR4 exactCrossEntropyRowsU0 exactCrossEntropyRowsSet1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86LoadGlobal exactCrossEntropyRowsR20 exactCrossEntropyRowsR6 exactCrossEntropyRowsU0 exactCrossEntropyRowsSet2) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate exactCrossEntropyRowsR9 exactCrossEntropyRowsR8 exactCrossEntropyRowsU0 exactCrossEntropyRowsWait1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate exactCrossEntropyRowsR20 exactCrossEntropyRowsR20 exactCrossEntropyRowsU0 exactCrossEntropyRowsWait2) exactCrossEntropySM86End)))))))))))))) def exactCrossEntropyRowsMaximumTile = (lambda unrestricted offset : (family SM86Unsigned32) . (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86LoadGlobal exactCrossEntropyRowsR8 exactCrossEntropyRowsR4 offset exactCrossEntropyRowsSet1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatMinimumOrMaximum exactCrossEntropyRowsR9 exactCrossEntropyRowsR9 exactCrossEntropyRowsR8 reductionSM86FloatMaximum exactCrossEntropyRowsWait1) exactCrossEntropySM86End))) def exactCrossEntropyRowsMaximumReduction : (family SM86Program) = (reductionSM86ParameterizedIdentityReduction reductionSM86MaximumCombine exactCrossEntropyRowsR0 exactCrossEntropyRowsR9 exactCrossEntropyRowsR10 exactCrossEntropyRowsR11 reductionSM86NegativeInfinity) def exactCrossEntropyRowsSumPrefix : (family SM86Program) = (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate exactCrossEntropyRowsR12 exactCrossEntropyRowsR9 exactCrossEntropyRowsU0 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatNegate exactCrossEntropyRowsR13 exactCrossEntropyRowsR12 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveConstant exactCrossEntropyRowsR14 (byte 0) exactCrossEntropyRowsOffset190 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveImmediate exactCrossEntropyRowsR9 exactCrossEntropyRowsU0 sm86SafeControl) exactCrossEntropySM86End)))) def exactCrossEntropyRowsSumTile = (lambda unrestricted offset : (family SM86Unsigned32) . (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86LoadGlobal exactCrossEntropyRowsR8 exactCrossEntropyRowsR4 offset exactCrossEntropyRowsSet1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatAdd exactCrossEntropyRowsR8 exactCrossEntropyRowsR8 exactCrossEntropyRowsR13 exactCrossEntropyRowsWait1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatMultiply exactCrossEntropyRowsR8 exactCrossEntropyRowsR8 exactCrossEntropyRowsR14 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation exactCrossEntropyRowsR8 exactCrossEntropyRowsR8 (constructor SM86MultiFunction SM86ExponentialBase2) exactCrossEntropyRowsSet3) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatAdd exactCrossEntropyRowsR9 exactCrossEntropyRowsR9 exactCrossEntropyRowsR8 exactCrossEntropyRowsWait3) exactCrossEntropySM86End)))))) def exactCrossEntropyRowsSumReduction : (family SM86Program) = (reductionSM86ParameterizedIdentityReduction reductionSM86SumCombine exactCrossEntropyRowsR0 exactCrossEntropyRowsR9 exactCrossEntropyRowsR10 exactCrossEntropyRowsR11 exactCrossEntropyRowsU0) def exactCrossEntropyRowsSuffix : (family SM86Program) = (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation exactCrossEntropyRowsR25 exactCrossEntropyRowsR9 (constructor SM86MultiFunction SM86LogarithmBase2) exactCrossEntropyRowsSet3) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveConstant exactCrossEntropyRowsR24 (byte 0) exactCrossEntropyRowsOffset194 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatMultiply exactCrossEntropyRowsR25 exactCrossEntropyRowsR25 exactCrossEntropyRowsR24 exactCrossEntropyRowsWait3) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatAdd exactCrossEntropyRowsR25 exactCrossEntropyRowsR25 exactCrossEntropyRowsR12 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatNegate exactCrossEntropyRowsR26 exactCrossEntropyRowsR20 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatAdd exactCrossEntropyRowsR25 exactCrossEntropyRowsR25 exactCrossEntropyRowsR26 sm86SafeControl) (exactCrossEntropySM86Next (exactCrossEntropyRowsWhenNotP0 (constructor SM86InstructionBody SM86StoreGlobal exactCrossEntropyRowsR16 exactCrossEntropyRowsR25 exactCrossEntropyRowsU0 sm86SafeControl)) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86Exit sm86SafeControl) exactCrossEntropySM86End)))))))) -- A row uses one 256-thread CTA. Thread t visits vocabulary positions -- t + 256*k; the first maximum tile is already read by the prefix. Derive -- both tile traversals from the shape so a larger vocabulary cannot silently -- reuse the legacy 48-tile image. def exactCrossEntropyRowsTileStrideBytes : Nat = (naturalMultiply reductionSM86WarpSum256RequiredThreads 4) def exactCrossEntropyRowsTileOffsetFor = (lambda unrestricted tile : Nat . (sm86Unsigned32FromNaturalTruncated (naturalMultiply tile exactCrossEntropyRowsTileStrideBytes))) def exactCrossEntropyRowsMaximumTilesFor = (lambda unrestricted tiles : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family SM86Program)) exactCrossEntropySM86End (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) . (sm86ProgramAppend (exactCrossEntropyRowsMaximumTile (exactCrossEntropyRowsTileOffsetFor (naturalSaturatingSubtract (naturalSaturatingSubtract tiles 1) predecessor))) induction))) (naturalSaturatingSubtract tiles 1))) def exactCrossEntropyRowsSumTilesFor = (lambda unrestricted tiles : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family SM86Program)) exactCrossEntropySM86End (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) . (sm86ProgramAppend (exactCrossEntropyRowsSumTile (exactCrossEntropyRowsTileOffsetFor (naturalSaturatingSubtract (naturalSaturatingSubtract tiles 1) predecessor))) induction))) tiles)) def exactCrossEntropyRowsProgramForUnchecked = (lambda unrestricted vocabulary : Nat . (sm86ProgramAppend (exactCrossEntropyRowsPrefixFor vocabulary) (sm86ProgramAppend (exactCrossEntropyRowsMaximumTilesFor (naturalDivideUnchecked vocabulary reductionSM86WarpSum256RequiredThreads)) (sm86ProgramAppend exactCrossEntropyRowsMaximumReduction (sm86ProgramAppend exactCrossEntropyRowsSumPrefix (sm86ProgramAppend (exactCrossEntropyRowsSumTilesFor (naturalDivideUnchecked vocabulary reductionSM86WarpSum256RequiredThreads)) (sm86ProgramAppend exactCrossEntropyRowsSumReduction exactCrossEntropyRowsSuffix))))))) def exactCrossEntropyRowsShapeAdmitted = (lambda unrestricted rows : Nat . (lambda unrestricted vocabulary : Nat . (naturalAnd (naturalNonzero rows) (naturalAnd (naturalIsZero (naturalModuloUnchecked vocabulary reductionSM86WarpSum256RequiredThreads)) (naturalLess (naturalMultiply rows (naturalMultiply vocabulary 4)) (naturalPowerOfTwo 32)))))) def exactCrossEntropyRowsProgramFor = (lambda unrestricted rows : Nat . (lambda unrestricted vocabulary : Nat . (lambda erased admitted : (equal Nat (exactCrossEntropyRowsShapeAdmitted rows vocabulary) 1) . (exactCrossEntropyRowsProgramForUnchecked vocabulary)))) def exactCrossEntropyRowsProgram : (family SM86Program) = (exactCrossEntropyRowsProgramForUnchecked 12288) def exactCrossEntropyPartialR0 = exactCrossEntropyRowsR0 def exactCrossEntropyPartialR1 = exactCrossEntropyRowsR1 def exactCrossEntropyPartialR2 = exactCrossEntropyRowsR2 def exactCrossEntropyPartialR3 = exactCrossEntropyRowsR3 def exactCrossEntropyPartialR4 = exactCrossEntropyRowsR4 def exactCrossEntropyPartialR8 = exactCrossEntropyRowsR8 def exactCrossEntropyPartialR9 = exactCrossEntropyRowsR9 def exactCrossEntropyPartialR10 = exactCrossEntropyRowsR10 def exactCrossEntropyPartialR12 = exactCrossEntropyRowsR12 def exactCrossEntropyPartialP0 = exactCrossEntropyRowsP0 def exactCrossEntropyPartialU0 = exactCrossEntropyRowsU0 def exactCrossEntropyPartialU4 = exactCrossEntropyRowsU4 def exactCrossEntropyPartialU1024 = (sm86Unsigned32 (byte 0) (byte 4) (byte 0) (byte 0)) def exactCrossEntropyPartialSet0 = exactCrossEntropyRowsSet0 def exactCrossEntropyPartialSet1 = exactCrossEntropyRowsSet1 def exactCrossEntropyPartialWait0 = exactCrossEntropyRowsWait0 def exactCrossEntropyPartialWait1 = exactCrossEntropyRowsWait1 def exactCrossEntropyPartialWhenNotP0 = (lambda unrestricted body : (family SM86InstructionBody) . (sm86NegatedPredicatedInstruction exactCrossEntropyPartialP0 body)) def exactCrossEntropyPartialPrefix : (family SM86Program) = (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveConstant exactCrossEntropyPartialR1 (byte 0) exactCrossEntropyRowsOffset028 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86SpecialToRegister exactCrossEntropyPartialR0 (constructor SM86SpecialRegister SM86ThreadIdX) exactCrossEntropyPartialSet0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86SpecialToRegister exactCrossEntropyPartialR1 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) exactCrossEntropyPartialSet0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveImmediate exactCrossEntropyPartialR2 exactCrossEntropyPartialU4 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate exactCrossEntropyPartialR3 exactCrossEntropyPartialR1 exactCrossEntropyPartialU1024 exactCrossEntropyPartialR0 exactCrossEntropyPartialWait0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant exactCrossEntropyPartialR4 exactCrossEntropyPartialR3 exactCrossEntropyPartialR2 (byte 0) exactCrossEntropyRowsOffset160 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86LoadGlobal exactCrossEntropyPartialR8 exactCrossEntropyPartialR4 exactCrossEntropyPartialU0 exactCrossEntropyPartialSet1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate exactCrossEntropyPartialR8 exactCrossEntropyPartialR8 exactCrossEntropyPartialU0 exactCrossEntropyPartialWait1) exactCrossEntropySM86End)))))))) def exactCrossEntropyPartialReduction : (family SM86Program) = (reductionSM86ParameterizedWarpSum1024 exactCrossEntropyPartialR0 exactCrossEntropyPartialR8 exactCrossEntropyPartialR9) def exactCrossEntropyPartialSuffixFor = (lambda unrestricted rows : Nat . (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate exactCrossEntropyPartialP0 exactCrossEntropyPartialR0 exactCrossEntropyPartialU0 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate exactCrossEntropyPartialR10 exactCrossEntropyPartialR1 (sm86Unsigned32FromNaturalTruncated rows) sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant exactCrossEntropyPartialR12 exactCrossEntropyPartialR10 exactCrossEntropyPartialR2 (byte 0) exactCrossEntropyRowsOffset160 sm86SafeControl) (exactCrossEntropySM86Next (exactCrossEntropyPartialWhenNotP0 (constructor SM86InstructionBody SM86StoreGlobal exactCrossEntropyPartialR12 exactCrossEntropyPartialR8 exactCrossEntropyPartialU0 sm86SafeControl)) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86Exit sm86SafeControl) exactCrossEntropySM86End)))))) def exactCrossEntropyPartialProgramForUnchecked = (lambda unrestricted rows : Nat . (sm86ProgramAppend exactCrossEntropyPartialPrefix (sm86ProgramAppend exactCrossEntropyPartialReduction (exactCrossEntropyPartialSuffixFor rows)))) def exactCrossEntropyFinalizeR0 = exactCrossEntropyRowsR0 def exactCrossEntropyFinalizeR1 = exactCrossEntropyRowsR1 def exactCrossEntropyFinalizeR2 = exactCrossEntropyRowsR2 def exactCrossEntropyFinalizeR3 = exactCrossEntropyRowsR3 def exactCrossEntropyFinalizeR4 = exactCrossEntropyRowsR4 def exactCrossEntropyFinalizeR8 = exactCrossEntropyRowsR8 def exactCrossEntropyFinalizeR9 = exactCrossEntropyRowsR9 def exactCrossEntropyFinalizeR10 = exactCrossEntropyRowsR10 def exactCrossEntropyFinalizeR12 = exactCrossEntropyRowsR12 def exactCrossEntropyFinalizeP0 = exactCrossEntropyRowsP0 def exactCrossEntropyFinalizeU0 = exactCrossEntropyRowsU0 def exactCrossEntropyFinalizeU1 = sm86Unsigned32One def exactCrossEntropyFinalizeU4 = exactCrossEntropyRowsU4 def exactCrossEntropyFinalizeSet0 = exactCrossEntropyRowsSet0 def exactCrossEntropyFinalizeSet1 = exactCrossEntropyRowsSet1 def exactCrossEntropyFinalizeWait0 = exactCrossEntropyRowsWait0 def exactCrossEntropyFinalizeWait1 = exactCrossEntropyRowsWait1 def exactCrossEntropyFinalizeWhenP0 = (lambda unrestricted body : (family SM86InstructionBody) . (sm86PredicatedInstruction exactCrossEntropyFinalizeP0 body)) def exactCrossEntropyFinalizeWhenNotP0 = (lambda unrestricted body : (family SM86InstructionBody) . (sm86NegatedPredicatedInstruction exactCrossEntropyFinalizeP0 body)) def exactCrossEntropyFinalizePrefixFor = (lambda unrestricted rows : Nat . (lambda unrestricted partials : Nat . (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveConstant exactCrossEntropyFinalizeR1 (byte 0) exactCrossEntropyRowsOffset028 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86SpecialToRegister exactCrossEntropyFinalizeR0 (constructor SM86SpecialRegister SM86ThreadIdX) exactCrossEntropyFinalizeSet0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveImmediate exactCrossEntropyFinalizeR2 exactCrossEntropyFinalizeU4 exactCrossEntropyFinalizeWait0) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate exactCrossEntropyFinalizeR3 exactCrossEntropyFinalizeR0 (sm86Unsigned32FromNaturalTruncated rows) sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant exactCrossEntropyFinalizeR4 exactCrossEntropyFinalizeR3 exactCrossEntropyFinalizeR2 (byte 0) exactCrossEntropyRowsOffset160 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86LoadGlobal exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeR4 exactCrossEntropyFinalizeU0 exactCrossEntropyFinalizeSet1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeU0 exactCrossEntropyFinalizeWait1) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate exactCrossEntropyFinalizeP0 exactCrossEntropyFinalizeR0 (sm86Unsigned32FromNaturalTruncated (naturalSaturatingSubtract partials 1)) sm86SafeControl) (exactCrossEntropySM86Next (exactCrossEntropyFinalizeWhenP0 (constructor SM86InstructionBody SM86MoveImmediate exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeU0 sm86SafeControl)) exactCrossEntropySM86End))))))))))) def exactCrossEntropyFinalizeReduction : (family SM86Program) = (reductionSM86ParameterizedLegacyWarpSum exactCrossEntropyFinalizeR0 exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeR9 exactCrossEntropyFinalizeU1) def exactCrossEntropyFinalizeSuffix : (family SM86Program) = (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate exactCrossEntropyFinalizeP0 exactCrossEntropyFinalizeR0 exactCrossEntropyFinalizeU0 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86MoveConstant exactCrossEntropyFinalizeR10 (byte 0) exactCrossEntropyRowsOffset198 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86FloatMultiply exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeR10 sm86SafeControl) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant exactCrossEntropyFinalizeR12 sm86ZeroRegister exactCrossEntropyFinalizeR2 (byte 0) exactCrossEntropyRowsOffset168 sm86SafeControl) (exactCrossEntropySM86Next (exactCrossEntropyFinalizeWhenNotP0 (constructor SM86InstructionBody SM86StoreGlobal exactCrossEntropyFinalizeR12 exactCrossEntropyFinalizeR8 exactCrossEntropyFinalizeU0 sm86SafeControl)) (exactCrossEntropySM86AlwaysNext (constructor SM86InstructionBody SM86Exit sm86SafeControl) exactCrossEntropySM86End)))))) def exactCrossEntropyFinalizeProgramForUnchecked = (lambda unrestricted rows : Nat . (sm86ProgramAppend (exactCrossEntropyFinalizePrefixFor rows (naturalDivideUnchecked rows reductionSM86WarpSum1024RequiredThreads)) (sm86ProgramAppend exactCrossEntropyFinalizeReduction exactCrossEntropyFinalizeSuffix))) -- Both reductions read a complete CTA, including lanes masked after their -- load. The workspace therefore needs 64 slots beyond the loss rows even -- when fewer row groups contain useful partials. def exactCrossEntropyMeanPartialSlots : Nat = reductionSM86WarpSum64RequiredThreads def exactCrossEntropyMeanShapeAdmitted = (lambda unrestricted rows : Nat . (naturalAnd (naturalNonzero rows) (naturalAnd (naturalIsZero (naturalModuloUnchecked rows reductionSM86WarpSum1024RequiredThreads)) (naturalAnd (naturalLessOrEqual (naturalDivideUnchecked rows reductionSM86WarpSum1024RequiredThreads) exactCrossEntropyMeanPartialSlots) (naturalLess (naturalAdd rows exactCrossEntropyMeanPartialSlots) (naturalPowerOfTwo 32)))))) def exactCrossEntropyPartialProgramFor = (lambda unrestricted rows : Nat . (lambda erased admitted : (equal Nat (exactCrossEntropyMeanShapeAdmitted rows) 1) . (exactCrossEntropyPartialProgramForUnchecked rows))) def exactCrossEntropyFinalizeProgramFor = (lambda unrestricted rows : Nat . (lambda erased admitted : (equal Nat (exactCrossEntropyMeanShapeAdmitted rows) 1) . (exactCrossEntropyFinalizeProgramForUnchecked rows))) def exactCrossEntropyPartialProgram : (family SM86Program) = (exactCrossEntropyPartialProgramForUnchecked 6144) def exactCrossEntropyFinalizeProgram : (family SM86Program) = (exactCrossEntropyFinalizeProgramForUnchecked 6144) def exactCrossEntropySM86ProgramFor = (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) . (eliminate ExactCrossEntropySM86Variant (lambda unrestricted current : (family ExactCrossEntropySM86Variant) . (family SM86Program)) variant (branch ExactCrossEntropyRows . exactCrossEntropyRowsProgram) (branch ReduceExactRowLosses . exactCrossEntropyPartialProgram) (branch FinalizeExactMeanLoss . exactCrossEntropyFinalizeProgram))) def exactCrossEntropySM86N6 = (byte-to-nat (byte 6)) def exactCrossEntropySM86N16 = (byte-to-nat (byte 16)) def exactCrossEntropySM86N24 = (byte-to-nat (byte 24)) def exactCrossEntropySM86N32 = (byte-to-nat (byte 32)) def exactCrossEntropySM86N34 = (byte-to-nat (byte 34)) def exactCrossEntropySM86N43 = (byte-to-nat (byte 43)) def exactCrossEntropySM86N47 = (byte-to-nat (byte 47)) def exactCrossEntropySM86N48 = (byte-to-nat (byte 48)) def exactCrossEntropySM86N64 = (byte-to-nat (byte 64)) def exactCrossEntropySM86N96 = (byte-to-nat (byte 96)) def exactCrossEntropySM86N104 = (byte-to-nat (byte 104)) def exactCrossEntropySM86N112 = (byte-to-nat (byte 112)) def exactCrossEntropySM86N128 = (byte-to-nat (byte 128)) def exactCrossEntropySM86N144 = (byte-to-nat (byte 144)) def exactCrossEntropySM86N148 = (byte-to-nat (byte 148)) def exactCrossEntropySM86N152 = (byte-to-nat (byte 152)) def exactCrossEntropySM86N171 = (byte-to-nat (byte 171)) def exactCrossEntropySM86N256 = (succ (byte-to-nat (byte 255))) def exactCrossEntropySM86N427 = (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N171) def exactCrossEntropySM86N1024 = (naturalPowerOfTwo (byte-to-nat (byte 10))) def exactCrossEntropySM86N6144 = (naturalMultiply exactCrossEntropySM86N24 exactCrossEntropySM86N256) def exactCrossEntropySM86N6150 = (naturalAdd exactCrossEntropySM86N6144 exactCrossEntropySM86N6) def exactCrossEntropySM86N12288 = (naturalMultiply exactCrossEntropySM86N48 exactCrossEntropySM86N256) def exactCrossEntropySM86LogitsElements = (naturalMultiply exactCrossEntropySM86N6144 exactCrossEntropySM86N12288) def exactCrossEntropySM86Offset160Natural = (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N96) def exactCrossEntropySM86Offset168Natural = (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N104) def exactCrossEntropySM86Offset170Natural = (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N112) def exactCrossEntropySM86Offset190Natural = (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N144) def exactCrossEntropySM86Offset194Natural = (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N148) def exactCrossEntropySM86Offset198Natural = (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N152) def exactCrossEntropySM86ABI : (family ExactCrossEntropySM86ABI) = (constructor ExactCrossEntropySM86ABI ExactCrossEntropySM86ABIValue exactCrossEntropySM86Offset160Natural exactCrossEntropySM86Offset168Natural exactCrossEntropySM86Offset168Natural exactCrossEntropySM86Offset170Natural exactCrossEntropySM86Offset190Natural exactCrossEntropySM86Offset194Natural exactCrossEntropySM86Offset198Natural) def exactCrossEntropySM86ExtentsFor = (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) . (eliminate ExactCrossEntropySM86Variant (lambda unrestricted current : (family ExactCrossEntropySM86Variant) . (family ExactCrossEntropySM86Extents)) variant (branch ExactCrossEntropyRows . (constructor ExactCrossEntropySM86Extents ExactCrossEntropySM86ExtentsValue zero zero zero exactCrossEntropySM86N6144 exactCrossEntropySM86N6144 exactCrossEntropySM86LogitsElements exactCrossEntropySM86N6144 zero zero)) (branch ReduceExactRowLosses . (constructor ExactCrossEntropySM86Extents ExactCrossEntropySM86ExtentsValue zero exactCrossEntropySM86N6144 exactCrossEntropySM86N6144 exactCrossEntropySM86N6 exactCrossEntropySM86N6150 zero zero zero zero)) (branch FinalizeExactMeanLoss . (constructor ExactCrossEntropySM86Extents ExactCrossEntropySM86ExtentsValue exactCrossEntropySM86N6144 exactCrossEntropySM86N6 zero zero exactCrossEntropySM86N6150 zero zero (succ zero) zero)))) def exactCrossEntropySM86ManifestFor = (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) . (eliminate ExactCrossEntropySM86Variant (lambda unrestricted current : (family ExactCrossEntropySM86Variant) . (family ExactCrossEntropySM86Manifest)) variant (branch ExactCrossEntropyRows . (constructor ExactCrossEntropySM86Manifest ExactCrossEntropySM86ManifestValue variant exactCrossEntropySM86N427 (naturalMultiply exactCrossEntropySM86N427 exactCrossEntropySM86N16) exactCrossEntropySM86N32 exactCrossEntropySM86N128 exactCrossEntropySM86N6144 exactCrossEntropySM86N256 exactCrossEntropySM86ABI (exactCrossEntropySM86ExtentsFor variant) (byte-to-nat (byte 107)) (byte-to-nat (byte 140)) (naturalAdd exactCrossEntropySM86N256 exactCrossEntropySM86N128) (naturalAdd exactCrossEntropySM86N256 (byte-to-nat (byte 162))) exactCrossEntropySM86N6144 exactCrossEntropySM86N12288 exactCrossEntropySM86N256 exactCrossEntropySM86N48 zero)) (branch ReduceExactRowLosses . (constructor ExactCrossEntropySM86Manifest ExactCrossEntropySM86ManifestValue variant exactCrossEntropySM86N43 (naturalMultiply exactCrossEntropySM86N43 exactCrossEntropySM86N16) exactCrossEntropySM86N24 exactCrossEntropySM86N128 exactCrossEntropySM86N6 exactCrossEntropySM86N1024 exactCrossEntropySM86ABI (exactCrossEntropySM86ExtentsFor variant) (byte-to-nat (byte 8)) (byte-to-nat (byte 37)) zero zero exactCrossEntropySM86N6144 exactCrossEntropySM86N12288 exactCrossEntropySM86N256 exactCrossEntropySM86N48 zero)) (branch FinalizeExactMeanLoss . (constructor ExactCrossEntropySM86Manifest ExactCrossEntropySM86ManifestValue variant exactCrossEntropySM86N47 (naturalMultiply exactCrossEntropySM86N47 exactCrossEntropySM86N16) exactCrossEntropySM86N24 exactCrossEntropySM86N128 (succ zero) exactCrossEntropySM86N64 exactCrossEntropySM86ABI (exactCrossEntropySM86ExtentsFor variant) (byte-to-nat (byte 9)) (byte-to-nat (byte 40)) zero zero exactCrossEntropySM86N6144 exactCrossEntropySM86N12288 exactCrossEntropySM86N256 exactCrossEntropySM86N48 zero)))) def exactCrossEntropySM86ManifestInstructions = (lambda unrestricted manifest : (family ExactCrossEntropySM86Manifest) . (eliminate ExactCrossEntropySM86Manifest (lambda unrestricted current : (family ExactCrossEntropySM86Manifest) . Nat) manifest (branch ExactCrossEntropySM86ManifestValue variant instructions bytes registers shared grid block abi extents r0s r0e r1s r1e rows vocabulary tile tiles hostFallback . instructions))) def exactCrossEntropySM86ManifestBytes = (lambda unrestricted manifest : (family ExactCrossEntropySM86Manifest) . (eliminate ExactCrossEntropySM86Manifest (lambda unrestricted current : (family ExactCrossEntropySM86Manifest) . Nat) manifest (branch ExactCrossEntropySM86ManifestValue variant instructions bytes registers shared grid block abi extents r0s r0e r1s r1e rows vocabulary tile tiles hostFallback . bytes))) def exactCrossEntropySM86TelemetryFor = (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) . (lambda unrestricted instructions : Nat . (lambda unrestricted bytes : Nat . (constructor ExactCrossEntropySM86Telemetry ExactCrossEntropySM86TelemetryValue (exactCrossEntropySM86ManifestFor variant) instructions bytes)))) def exactCrossEntropySM86Build = (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) . (app (lambda unrestricted program : (family SM86Program) . (app (lambda unrestricted observedInstructions : Nat . (app (lambda unrestricted manifest : (family ExactCrossEntropySM86Manifest) . (nat-eliminate (lambda unrestricted countMatched : Nat . (family ExactCrossEntropySM86BuildResult)) (constructor ExactCrossEntropySM86BuildResult ExactCrossEntropySM86ContractFailed (constructor ExactCrossEntropySM86FailureCode ExactCrossEntropyInstructionCountMismatch) (exactCrossEntropySM86TelemetryFor variant observedInstructions zero)) (lambda unrestricted countPredecessor : Nat . (lambda unrestricted countInduction : (family ExactCrossEntropySM86BuildResult) . (app (lambda unrestricted encoding : (family SM86ProgramEncodingResult) . (eliminate SM86ProgramEncodingResult (lambda unrestricted current : (family SM86ProgramEncodingResult) . (family ExactCrossEntropySM86BuildResult)) encoding (branch SM86ProgramEncodingSucceeded bytes encodingTelemetry . (app (lambda unrestricted telemetry : (family ExactCrossEntropySM86Telemetry) . (nat-eliminate (lambda unrestricted bytesMatched : Nat . (family ExactCrossEntropySM86BuildResult)) (constructor ExactCrossEntropySM86BuildResult ExactCrossEntropySM86ContractFailed (constructor ExactCrossEntropySM86FailureCode ExactCrossEntropyEncodedByteCountMismatch) telemetry) (lambda unrestricted bytesPredecessor : Nat . (lambda unrestricted bytesInduction : (family ExactCrossEntropySM86BuildResult) . (app (lambda unrestricted identityResult : (family SHA256HexResult) . (eliminate SHA256HexResult (lambda unrestricted current : (family SHA256HexResult) . (family ExactCrossEntropySM86BuildResult)) identityResult (branch SHA256HexSucceeded identity identityTelemetry . (nat-eliminate (lambda unrestricted identityLengthMatched : Nat . (family ExactCrossEntropySM86BuildResult)) (constructor ExactCrossEntropySM86BuildResult ExactCrossEntropySM86ImageIdentityFailed (constructor ExactCrossEntropySM86FailureCode ExactCrossEntropyIdentityLengthInvalid) identityResult telemetry) (lambda unrestricted identityLengthPredecessor : Nat . (lambda unrestricted identityLengthInduction : (family ExactCrossEntropySM86BuildResult) . (constructor ExactCrossEntropySM86BuildResult ExactCrossEntropySM86BuildSucceeded bytes identity encodingTelemetry identityTelemetry telemetry))) (naturalEqual (bytes-length identity) exactCrossEntropySM86N64))) (branch SHA256HexFailed error ordinal identityTelemetry . (constructor ExactCrossEntropySM86BuildResult ExactCrossEntropySM86ImageIdentityFailed (constructor ExactCrossEntropySM86FailureCode ExactCrossEntropyIdentityFailed) identityResult telemetry)))) (sha256Hex bytes)))) (naturalEqual (bytes-length bytes) (exactCrossEntropySM86ManifestBytes manifest)))) (exactCrossEntropySM86TelemetryFor variant observedInstructions (bytes-length bytes)))) (branch SM86ProgramEncodingFailed instructionIndex failure encodingTelemetry . (constructor ExactCrossEntropySM86BuildResult ExactCrossEntropySM86ImageEncodingFailed (constructor ExactCrossEntropySM86FailureCode ExactCrossEntropyEncodingFailed) encoding (exactCrossEntropySM86TelemetryFor variant observedInstructions zero))))) (sm86EncodeProgram program)))) (naturalEqual observedInstructions (exactCrossEntropySM86ManifestInstructions manifest)))) (exactCrossEntropySM86ManifestFor variant))) (sm86ProgramCount program))) (exactCrossEntropySM86ProgramFor variant))) def exactCrossEntropySM86BuildRows = (exactCrossEntropySM86Build (constructor ExactCrossEntropySM86Variant ExactCrossEntropyRows)) def exactCrossEntropySM86BuildPartial = (exactCrossEntropySM86Build (constructor ExactCrossEntropySM86Variant ReduceExactRowLosses)) def exactCrossEntropySM86BuildFinalize = (exactCrossEntropySM86Build (constructor ExactCrossEntropySM86Variant FinalizeExactMeanLoss))