Bob.Build.BigramLossGradientSM86

1module Bob.Build.BigramLossGradientSM86
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 Std.Natural
11
12-- A deliberately small physical realization of Bob's complete objective.
13-- One 256-thread block assigns one row to each thread.  A thread walks that
14-- row's 256 logits serially, writes its exact full-vocabulary cross-entropy,
15-- and writes all 256 gradient elements.  The schedule favors transparent
16-- qualification over throughput and introduces no CPU learning path.
17family BobBigramLossGradientSM86Manifest : Type 0
18constructor BobBigramLossGradientSM86ManifestValue
19field unrestricted bobBigramLossRows : Nat
20field unrestricted bobBigramLossVocabulary : Nat
21field unrestricted bobBigramLossParameterElements : Nat
22field unrestricted bobBigramLossRegisters : Nat
23field unrestricted bobBigramLossGridX : Nat
24field unrestricted bobBigramLossBlockX : Nat
25field unrestricted bobBigramLossHostFallbackOperations : Nat
26
27end-family
28
29def bobBigramLossGradientManifest : (family BobBigramLossGradientSM86Manifest) =
30  (record
31    BobBigramLossGradientSM86Manifest
32    (bobBigramLossRows = 256)
33    (bobBigramLossVocabulary = 256)
34    (bobBigramLossParameterElements = 65_536)
35    (bobBigramLossRegisters = 32)
36    (bobBigramLossGridX = 1)
37    (bobBigramLossBlockX = 256)
38    (bobBigramLossHostFallbackOperations = 0))
39
40def bobBigramR =
41  (lambda unrestricted index : Byte . (sm86Register index))
42
43def bobBigramR0 = (bobBigramR (byte 0))
44def bobBigramR1 = (bobBigramR (byte 1))
45def bobBigramR4 = (bobBigramR (byte 4))
46def bobBigramR8 = (bobBigramR (byte 8))
47def bobBigramR9 = (bobBigramR (byte 9))
48def bobBigramR10 = (bobBigramR (byte 10))
49def bobBigramR11 = (bobBigramR (byte 11))
50def bobBigramR12 = (bobBigramR (byte 12))
51def bobBigramR13 = (bobBigramR (byte 13))
52def bobBigramR14 = (bobBigramR (byte 14))
53def bobBigramR15 = (bobBigramR (byte 15))
54def bobBigramR16 = (bobBigramR (byte 16))
55def bobBigramR17 = (bobBigramR (byte 17))
56def bobBigramR18 = (bobBigramR (byte 18))
57def bobBigramR19 = (bobBigramR (byte 19))
58def bobBigramR20 = (bobBigramR (byte 20))
59def bobBigramR21 = (bobBigramR (byte 21))
60def bobBigramR22 = (bobBigramR (byte 22))
61def bobBigramR23 = (bobBigramR (byte 23))
62def bobBigramR24 = (bobBigramR (byte 24))
63def bobBigramR25 = (bobBigramR (byte 25))
64def bobBigramR26 = (bobBigramR (byte 26))
65def bobBigramR27 = (bobBigramR (byte 27))
66def bobBigramR28 = (bobBigramR (byte 28))
67
68def bobBigramU32 =
69  (lambda unrestricted b0 : Byte .
70    (lambda unrestricted b1 : Byte .
71      (lambda unrestricted b2 : Byte .
72        (lambda unrestricted b3 : Byte . (sm86Unsigned32 b0 b1 b2 b3)))))
73
74def bobBigramU0 = (bobBigramU32 (byte 0) (byte 0) (byte 0) (byte 0))
75def bobBigramU4 = (bobBigramU32 (byte 4) (byte 0) (byte 0) (byte 0))
76def bobBigramU1024 = (bobBigramU32 (byte 0) (byte 4) (byte 0) (byte 0))
77def bobBigramNegativeInfinity = (bobBigramU32 (byte 0) (byte 0) (byte 128) (byte 255))
78def bobBigramOffset028 = (bobBigramU32 (byte 40) (byte 0) (byte 0) (byte 0))
79def bobBigramOffset160 = (bobBigramU32 (byte 96) (byte 1) (byte 0) (byte 0))
80def bobBigramOffset168 = (bobBigramU32 (byte 104) (byte 1) (byte 0) (byte 0))
81def bobBigramOffset170 = (bobBigramU32 (byte 112) (byte 1) (byte 0) (byte 0))
82def bobBigramOffset178 = (bobBigramU32 (byte 120) (byte 1) (byte 0) (byte 0))
83def bobBigramOffset190 = (bobBigramU32 (byte 144) (byte 1) (byte 0) (byte 0))
84def bobBigramOffset194 = (bobBigramU32 (byte 148) (byte 1) (byte 0) (byte 0))
85def bobBigramOffset198 = (bobBigramU32 (byte 152) (byte 1) (byte 0) (byte 0))
86
87def bobBigramSet0 =
88  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
89
90def bobBigramSet1 =
91  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))
92
93def bobBigramWait0 =
94  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))
95
96def bobBigramWait1 =
97  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier1))
98
99def bobBigramNext =
100  (lambda unrestricted body : (family SM86InstructionBody) .
101    (lambda unrestricted tail : (family SM86Program) .
102      (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))
103
104def bobBigramAppend =
105  (lambda unrestricted left : (family SM86Program) .
106    (lambda unrestricted right : (family SM86Program) . (sm86ProgramAppend left right)))
107
108def bobBigramRepeat =
109  (lambda unrestricted segment : (family SM86Program) .
110    (lambda unrestricted count : Nat .
111      (nat-eliminate
112        (lambda unrestricted current : Nat . (family SM86Program))
113        (constructor SM86Program SM86ProgramEnd)
114        (lambda unrestricted predecessor : Nat .
115          (lambda unrestricted induction : (family SM86Program) .
116            (bobBigramAppend segment induction)))
117        count)))
118
119def bobBigramPrologue : (family SM86Program) =
120  (bobBigramNext
121    (constructor SM86InstructionBody SM86MoveConstant bobBigramR1 (byte 0) bobBigramOffset028 sm86SafeControl)
122    (bobBigramNext
123      (constructor SM86InstructionBody SM86SpecialToRegister bobBigramR0 (constructor SM86SpecialRegister SM86ThreadIdX) bobBigramSet0)
124      (bobBigramNext
125        (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 bobBigramWait0)
126        (bobBigramNext
127          (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR8 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset160 sm86SafeControl)
128          (bobBigramNext
129            (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR10 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset168 sm86SafeControl)
130            (bobBigramNext
131              (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU4 sm86SafeControl)
132              (bobBigramNext
133                (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR20 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset170 sm86SafeControl)
134                (bobBigramNext
135                  (constructor SM86InstructionBody SM86LoadGlobal bobBigramR23 bobBigramR20 bobBigramU0 bobBigramSet0)
136                  (bobBigramNext
137                    (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR28 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset178 sm86SafeControl)
138                    (bobBigramNext
139                      (constructor SM86InstructionBody SM86MoveConstant bobBigramR16 (byte 0) bobBigramOffset190 sm86SafeControl)
140                      (bobBigramNext
141                        (constructor SM86InstructionBody SM86MoveConstant bobBigramR17 (byte 0) bobBigramOffset194 sm86SafeControl)
142                        (bobBigramNext
143                          (constructor SM86InstructionBody SM86MoveConstant bobBigramR18 (byte 0) bobBigramOffset198 sm86SafeControl)
144                          (bobBigramNext
145                            (constructor SM86InstructionBody SM86MoveImmediate bobBigramR13 bobBigramNegativeInfinity sm86SafeControl)
146                            (constructor SM86Program SM86ProgramEnd))))))))))))))
147
148def bobBigramMaximumStep : (family SM86Program) =
149  (bobBigramNext
150    (constructor SM86InstructionBody SM86LoadGlobal bobBigramR12 bobBigramR8 bobBigramU0 bobBigramSet0)
151    (bobBigramNext
152      (constructor SM86InstructionBody SM86FloatMinimumOrMaximum bobBigramR13 bobBigramR13 bobBigramR12 (constructor SM86FloatExtremum SM86FloatMaximum) bobBigramWait0)
153      (bobBigramNext
154        (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR8 bobBigramR8 bobBigramU4 sm86SafeControl)
155        (constructor SM86Program SM86ProgramEnd))))
156
157def bobBigramAfterMaximum : (family SM86Program) =
158  (bobBigramNext
159    (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 sm86SafeControl)
160    (bobBigramNext
161      (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR8 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset160 sm86SafeControl)
162      (bobBigramNext
163        (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate bobBigramR24 bobBigramR23 bobBigramU4 bobBigramR8 bobBigramWait0)
164        (bobBigramNext
165          (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU0 sm86SafeControl)
166          (bobBigramNext
167            (constructor SM86InstructionBody SM86IntegerAddThreeRegister bobBigramR25 bobBigramR9 bobBigramR4 sm86SafeControl)
168            (bobBigramNext
169              (constructor SM86InstructionBody SM86LoadGlobal bobBigramR21 bobBigramR24 bobBigramU0 bobBigramSet0)
170              (bobBigramNext
171                (constructor SM86InstructionBody SM86FloatNegate bobBigramR26 bobBigramR13 sm86SafeControl)
172                (bobBigramNext
173                  (constructor SM86InstructionBody SM86MoveImmediate bobBigramR14 bobBigramU0 sm86SafeControl)
174                  (constructor SM86Program SM86ProgramEnd)))))))))
175
176def bobBigramSumStep : (family SM86Program) =
177  (bobBigramNext
178    (constructor SM86InstructionBody SM86LoadGlobal bobBigramR12 bobBigramR8 bobBigramU0 bobBigramSet0)
179    (bobBigramNext
180      (constructor SM86InstructionBody SM86FloatAdd bobBigramR15 bobBigramR12 bobBigramR26 bobBigramWait0)
181      (bobBigramNext
182        (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR16 sm86SafeControl)
183        (bobBigramNext
184          (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR15 bobBigramR15 (constructor SM86MultiFunction SM86ExponentialBase2) bobBigramSet0)
185          (bobBigramNext
186            (constructor SM86InstructionBody SM86FloatAdd bobBigramR14 bobBigramR14 bobBigramR15 bobBigramWait0)
187            (bobBigramNext
188              (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR8 bobBigramR8 bobBigramU4 sm86SafeControl)
189              (constructor SM86Program SM86ProgramEnd)))))))
190
191def bobBigramLossAndGradientSetup : (family SM86Program) =
192  (bobBigramNext
193    (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR19 bobBigramR14 (constructor SM86MultiFunction SM86Reciprocal) bobBigramSet1)
194    (bobBigramNext
195      (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR22 bobBigramR14 (constructor SM86MultiFunction SM86LogarithmBase2) bobBigramSet0)
196      (bobBigramNext
197        (constructor SM86InstructionBody SM86FloatMultiply bobBigramR22 bobBigramR22 bobBigramR17 bobBigramWait0)
198        (bobBigramNext
199          (constructor SM86InstructionBody SM86FloatAdd bobBigramR22 bobBigramR22 bobBigramR13 sm86SafeControl)
200          (bobBigramNext
201            (constructor SM86InstructionBody SM86FloatNegate bobBigramR27 bobBigramR21 bobBigramWait0)
202            (bobBigramNext
203              (constructor SM86InstructionBody SM86FloatAdd bobBigramR22 bobBigramR22 bobBigramR27 sm86SafeControl)
204              (bobBigramNext
205                (constructor SM86InstructionBody SM86StoreGlobal bobBigramR28 bobBigramR22 bobBigramU0 sm86SafeControl)
206                (bobBigramNext
207                  (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU0 sm86SafeControl)
208                  (bobBigramNext
209                    (constructor SM86InstructionBody SM86FloatAdd bobBigramR19 bobBigramR19 bobBigramR4 bobBigramWait1)
210                    (bobBigramNext
211                      (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 sm86SafeControl)
212                      (bobBigramNext
213                        (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR8 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset160 sm86SafeControl)
214                        (bobBigramNext
215                          (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR10 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset168 sm86SafeControl)
216                          (constructor SM86Program SM86ProgramEnd)))))))))))))
217
218def bobBigramGradientStep : (family SM86Program) =
219  (bobBigramNext
220    (constructor SM86InstructionBody SM86LoadGlobal bobBigramR12 bobBigramR8 bobBigramU0 bobBigramSet0)
221    (bobBigramNext
222      (constructor SM86InstructionBody SM86FloatAdd bobBigramR15 bobBigramR12 bobBigramR26 bobBigramWait0)
223      (bobBigramNext
224        (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR16 sm86SafeControl)
225        (bobBigramNext
226          (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation bobBigramR15 bobBigramR15 (constructor SM86MultiFunction SM86ExponentialBase2) bobBigramSet0)
227          (bobBigramNext
228            (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR19 bobBigramWait0)
229            (bobBigramNext
230              (constructor SM86InstructionBody SM86FloatMultiply bobBigramR15 bobBigramR15 bobBigramR18 sm86SafeControl)
231              (bobBigramNext
232                (constructor SM86InstructionBody SM86StoreGlobal bobBigramR10 bobBigramR15 bobBigramU0 sm86SafeControl)
233                (bobBigramNext
234                  (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR8 bobBigramR8 bobBigramU4 sm86SafeControl)
235                  (bobBigramNext
236                    (constructor SM86InstructionBody SM86IntegerAddThreeImmediate bobBigramR10 bobBigramR10 bobBigramU4 sm86SafeControl)
237                    (constructor SM86Program SM86ProgramEnd))))))))))
238
239def bobBigramCorrectGradientAndExit : (family SM86Program) =
240  (bobBigramNext
241    (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU1024 sm86SafeControl)
242    (bobBigramNext
243      (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant bobBigramR10 bobBigramR0 bobBigramR4 (byte 0) bobBigramOffset168 sm86SafeControl)
244      (bobBigramNext
245        (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate bobBigramR24 bobBigramR23 bobBigramU4 bobBigramR10 sm86SafeControl)
246        (bobBigramNext
247          (constructor SM86InstructionBody SM86MoveImmediate bobBigramR4 bobBigramU0 sm86SafeControl)
248          (bobBigramNext
249            (constructor SM86InstructionBody SM86IntegerAddThreeRegister bobBigramR25 bobBigramR11 bobBigramR4 sm86SafeControl)
250            (bobBigramNext
251              (constructor SM86InstructionBody SM86LoadGlobal bobBigramR26 bobBigramR24 bobBigramU0 bobBigramSet0)
252              (bobBigramNext
253                (constructor SM86InstructionBody SM86FloatNegate bobBigramR27 bobBigramR18 sm86SafeControl)
254                (bobBigramNext
255                  (constructor SM86InstructionBody SM86FloatAdd bobBigramR26 bobBigramR26 bobBigramR27 bobBigramWait0)
256                  (bobBigramNext
257                    (constructor SM86InstructionBody SM86StoreGlobal bobBigramR24 bobBigramR26 bobBigramU0 sm86SafeControl)
258                    (bobBigramNext
259                      (constructor SM86InstructionBody SM86Exit sm86SafeControl)
260                      (constructor SM86Program SM86ProgramEnd)))))))))))
261
262def bobBigramLossGradientProgram : (family SM86Program) =
263  (bobBigramAppend
264    bobBigramPrologue
265    (bobBigramAppend
266      (bobBigramRepeat bobBigramMaximumStep 256)
267      (bobBigramAppend
268        bobBigramAfterMaximum
269        (bobBigramAppend
270          (bobBigramRepeat bobBigramSumStep 256)
271          (bobBigramAppend
272            bobBigramLossAndGradientSetup
273            (bobBigramAppend
274              (bobBigramRepeat bobBigramGradientStep 256)
275              bobBigramCorrectGradientAndExit))))))
276
277def bobBigramLossGradientImage : (family SM86ProgramEncodingResult) =
278  (sm86ProgramEncodingAppend
279    (sm86EncodeProgram bobBigramPrologue)
280    (sm86ProgramEncodingAppend
281      (sm86EncodeProgramRepeated bobBigramMaximumStep 256)
282      (sm86ProgramEncodingAppend
283        (sm86EncodeProgram bobBigramAfterMaximum)
284        (sm86ProgramEncodingAppend
285          (sm86EncodeProgramRepeated bobBigramSumStep 256)
286          (sm86ProgramEncodingAppend
287            (sm86EncodeProgram bobBigramLossAndGradientSetup)
288            (sm86ProgramEncodingAppend
289              (sm86EncodeProgramRepeated bobBigramGradientStep 256)
290              (sm86EncodeProgram bobBigramCorrectGradientAndExit)))))))