module Bob.Build.BigramLossGradientSM86 import Accelerator.SM86.Control import Accelerator.SM86.Immediate import Accelerator.SM86.Instruction import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.NumericSemantics import Accelerator.SM86.Program import Accelerator.SM86.Types import Std.Natural -- A deliberately small physical realization of Bob's complete objective. -- One 256-thread block assigns one row to each thread. A thread walks that -- row's 256 logits serially, writes its exact full-vocabulary cross-entropy, -- and writes all 256 gradient elements. The schedule favors transparent -- qualification over throughput and introduces no CPU learning path. family BobBigramLossGradientSM86Manifest : Type 0 constructor BobBigramLossGradientSM86ManifestValue field unrestricted bobBigramLossRows : Nat field unrestricted bobBigramLossVocabulary : Nat field unrestricted bobBigramLossParameterElements : Nat field unrestricted bobBigramLossRegisters : Nat field unrestricted bobBigramLossGridX : Nat field unrestricted bobBigramLossBlockX : Nat field unrestricted bobBigramLossHostFallbackOperations : Nat end-family def bobBigramLossGradientManifest : (family BobBigramLossGradientSM86Manifest) = (record BobBigramLossGradientSM86Manifest (bobBigramLossRows = 256) (bobBigramLossVocabulary = 256) (bobBigramLossParameterElements = 65_536) (bobBigramLossRegisters = 32) (bobBigramLossGridX = 1) (bobBigramLossBlockX = 256) (bobBigramLossHostFallbackOperations = 0)) def bobBigramR = (lambda unrestricted index : Byte . (sm86Register index)) def bobBigramR0 = (bobBigramR (byte 0)) def bobBigramR1 = (bobBigramR (byte 1)) def bobBigramR4 = (bobBigramR (byte 4)) def bobBigramR8 = (bobBigramR (byte 8)) def bobBigramR9 = (bobBigramR (byte 9)) def bobBigramR10 = (bobBigramR (byte 10)) def bobBigramR11 = (bobBigramR (byte 11)) def bobBigramR12 = (bobBigramR (byte 12)) def bobBigramR13 = (bobBigramR (byte 13)) def bobBigramR14 = (bobBigramR (byte 14)) def bobBigramR15 = (bobBigramR (byte 15)) def bobBigramR16 = (bobBigramR (byte 16)) def bobBigramR17 = (bobBigramR (byte 17)) def bobBigramR18 = (bobBigramR (byte 18)) def bobBigramR19 = (bobBigramR (byte 19)) def bobBigramR20 = (bobBigramR (byte 20)) def bobBigramR21 = (bobBigramR (byte 21)) def bobBigramR22 = (bobBigramR (byte 22)) def bobBigramR23 = (bobBigramR (byte 23)) def bobBigramR24 = (bobBigramR (byte 24)) def bobBigramR25 = (bobBigramR (byte 25)) def bobBigramR26 = (bobBigramR (byte 26)) def bobBigramR27 = (bobBigramR (byte 27)) def bobBigramR28 = (bobBigramR (byte 28)) def bobBigramU32 = (lambda unrestricted b0 : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (lambda unrestricted b3 : Byte . (sm86Unsigned32 b0 b1 b2 b3))))) def bobBigramU0 = (bobBigramU32 (byte 0) (byte 0) (byte 0) (byte 0)) def bobBigramU4 = (bobBigramU32 (byte 4) (byte 0) (byte 0) (byte 0)) def bobBigramU1024 = (bobBigramU32 (byte 0) (byte 4) (byte 0) (byte 0)) def bobBigramNegativeInfinity = (bobBigramU32 (byte 0) (byte 0) (byte 128) (byte 255)) def bobBigramOffset028 = (bobBigramU32 (byte 40) (byte 0) (byte 0) (byte 0)) def bobBigramOffset160 = (bobBigramU32 (byte 96) (byte 1) (byte 0) (byte 0)) def bobBigramOffset168 = (bobBigramU32 (byte 104) (byte 1) (byte 0) (byte 0)) def bobBigramOffset170 = (bobBigramU32 (byte 112) (byte 1) (byte 0) (byte 0)) def bobBigramOffset178 = (bobBigramU32 (byte 120) (byte 1) (byte 0) (byte 0)) def bobBigramOffset190 = (bobBigramU32 (byte 144) (byte 1) (byte 0) (byte 0)) def bobBigramOffset194 = (bobBigramU32 (byte 148) (byte 1) (byte 0) (byte 0)) def bobBigramOffset198 = (bobBigramU32 (byte 152) (byte 1) (byte 0) (byte 0)) def bobBigramSet0 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0)) def bobBigramSet1 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1)) def bobBigramWait0 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0)) def bobBigramWait1 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier1)) def bobBigramNext = (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail))) def bobBigramAppend = (lambda unrestricted left : (family SM86Program) . (lambda unrestricted right : (family SM86Program) . (sm86ProgramAppend left right))) def bobBigramRepeat = (lambda unrestricted segment : (family SM86Program) . (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family SM86Program)) (constructor SM86Program SM86ProgramEnd) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) . (bobBigramAppend segment induction))) count))) def bobBigramPrologue : (family SM86Program) = (bobBigramNext (constructor SM86InstructionBody SM86MoveConstant bobBigramR1 (byte 0) bobBigramOffset028 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86SpecialToRegister bobBigramR0 (constructor SM86SpecialRegister SM86ThreadIdX) bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR8 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset160 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR10 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset168 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU4 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR20 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset170 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86LoadGlobal bobBigramR23 bobBigramR20 bobBigramU0 bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR28 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset178 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveConstant bobBigramR16 (byte 0) bobBigramOffset190 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveConstant bobBigramR17 (byte 0) bobBigramOffset194 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveConstant bobBigramR18 (byte 0) bobBigramOffset198 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR13 bobBigramNegativeInfinity sm86SafeControl) (constructor SM86Program SM86ProgramEnd)))))))))))))) def bobBigramMaximumStep : (family SM86Program) = (bobBigramNext (constructor SM86InstructionBody SM86LoadGlobal bobBigramR12 bobBigramR8 bobBigramU0 bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatMinimumOrMaximum bobBigramR13 bobBigramR13 bobBigramR12 (constructor SM86FloatExtremum SM86FloatMaximum) bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR8 bobBigramR8 bobBigramU4 sm86SafeControl) (constructor SM86Program SM86ProgramEnd)))) def bobBigramAfterMaximum : (family SM86Program) = (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR8 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset160 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate bobBigramR24 bobBigramR23 bobBigramU4 bobBigramR8 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU0 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerAddThreeRegister bobBigramR25 bobBigramR9 bobBigramR4 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86LoadGlobal bobBigramR21 bobBigramR24 bobBigramU0 bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatNegate bobBigramR26 bobBigramR13 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR14 bobBigramU0 sm86SafeControl) (constructor SM86Program SM86ProgramEnd))))))))) def bobBigramSumStep : (family SM86Program) = (bobBigramNext (constructor SM86InstructionBody SM86LoadGlobal bobBigramR12 bobBigramR8 bobBigramU0 bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatAdd bobBigramR15 bobBigramR12 bobBigramR26 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR16 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR15 bobBigramR15 (constructor SM86MultiFunction SM86ExponentialBase2) bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatAdd bobBigramR14 bobBigramR14 bobBigramR15 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR8 bobBigramR8 bobBigramU4 sm86SafeControl) (constructor SM86Program SM86ProgramEnd))))))) def bobBigramLossAndGradientSetup : (family SM86Program) = (bobBigramNext (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR19 bobBigramR14 (constructor SM86MultiFunction SM86Reciprocal) bobBigramSet1) (bobBigramNext (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR22 bobBigramR14 (constructor SM86MultiFunction SM86LogarithmBase2) bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatMultiply bobBigramR22 bobBigramR22 bobBigramR17 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86FloatAdd bobBigramR22 bobBigramR22 bobBigramR13 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86FloatNegate bobBigramR27 bobBigramR21 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86FloatAdd bobBigramR22 bobBigramR22 bobBigramR27 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86StoreGlobal bobBigramR28 bobBigramR22 bobBigramU0 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU0 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86FloatAdd bobBigramR19 bobBigramR19 bobBigramR4 bobBigramWait1) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR8 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset160 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR10 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset168 sm86SafeControl) (constructor SM86Program SM86ProgramEnd))))))))))))) def bobBigramGradientStep : (family SM86Program) = (bobBigramNext (constructor SM86InstructionBody SM86LoadGlobal bobBigramR12 bobBigramR8 bobBigramU0 bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatAdd bobBigramR15 bobBigramR12 bobBigramR26 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR16 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR15 bobBigramR15 (constructor SM86MultiFunction SM86ExponentialBase2) bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR19 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR18 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86StoreGlobal bobBigramR10 bobBigramR15 bobBigramU0 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR8 bobBigramR8 bobBigramU4 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR10 bobBigramR10 bobBigramU4 sm86SafeControl) (constructor SM86Program SM86ProgramEnd)))))))))) def bobBigramCorrectGradientAndExit : (family SM86Program) = (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR10 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset168 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate bobBigramR24 bobBigramR23 bobBigramU4 bobBigramR10 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU0 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86IntegerAddThreeRegister bobBigramR25 bobBigramR11 bobBigramR4 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86LoadGlobal bobBigramR26 bobBigramR24 bobBigramU0 bobBigramSet0) (bobBigramNext (constructor SM86InstructionBody SM86FloatNegate bobBigramR27 bobBigramR18 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86FloatAdd bobBigramR26 bobBigramR26 bobBigramR27 bobBigramWait0) (bobBigramNext (constructor SM86InstructionBody SM86StoreGlobal bobBigramR24 bobBigramR26 bobBigramU0 sm86SafeControl) (bobBigramNext (constructor SM86InstructionBody SM86Exit sm86SafeControl) (constructor SM86Program SM86ProgramEnd))))))))))) def bobBigramLossGradientProgram : (family SM86Program) = (bobBigramAppend bobBigramPrologue (bobBigramAppend (bobBigramRepeat bobBigramMaximumStep 256) (bobBigramAppend bobBigramAfterMaximum (bobBigramAppend (bobBigramRepeat bobBigramSumStep 256) (bobBigramAppend bobBigramLossAndGradientSetup (bobBigramAppend (bobBigramRepeat bobBigramGradientStep 256) bobBigramCorrectGradientAndExit)))))) def bobBigramLossGradientImage : (family SM86ProgramEncodingResult) = (sm86ProgramEncodingAppend (sm86EncodeProgram bobBigramPrologue) (sm86ProgramEncodingAppend (sm86EncodeProgramRepeated bobBigramMaximumStep 256) (sm86ProgramEncodingAppend (sm86EncodeProgram bobBigramAfterMaximum) (sm86ProgramEncodingAppend (sm86EncodeProgramRepeated bobBigramSumStep 256) (sm86ProgramEncodingAppend (sm86EncodeProgram bobBigramLossAndGradientSetup) (sm86ProgramEncodingAppend (sm86EncodeProgramRepeated bobBigramGradientStep 256) (sm86EncodeProgram bobBigramCorrectGradientAndExit)))))))