Accelerator.SM86.RNG.RandomNormal

1module Accelerator.SM86.RNG.RandomNormal
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.Program
7import Accelerator.SM86.Types
8
9def randomNormalRegister =
10  (lambda unrestricted number : Byte .
11    (app Accelerator.SM86.Types/sm86Register number))
12
13def randomNormalImmediate =
14  (lambda unrestricted b0 : Byte .
15    (lambda unrestricted b1 : Byte .
16      (lambda unrestricted b2 : Byte .
17        (lambda unrestricted b3 : Byte .
18          (app Accelerator.SM86.Immediate/sm86Unsigned32 b0 b1 b2 b3)))))
19
20def randomNormalZero =
21  (app randomNormalImmediate (byte 0) (byte 0) (byte 0) (byte 0))
22def randomNormalThree =
23  (app randomNormalImmediate (byte 3) (byte 0) (byte 0) (byte 0))
24def randomNormalFour =
25  (app randomNormalImmediate (byte 4) (byte 0) (byte 0) (byte 0))
26def randomNormalConstantBase =
27  (app randomNormalImmediate (byte 40) (byte 0) (byte 0) (byte 0))
28def randomNormalOutputPointer =
29  (app randomNormalImmediate (byte 96) (byte 1) (byte 0) (byte 0))
30def randomNormalSeedScalar =
31  (app randomNormalImmediate (byte 144) (byte 1) (byte 0) (byte 0))
32def randomNormalCounterScalar =
33  (app randomNormalImmediate (byte 148) (byte 1) (byte 0) (byte 0))
34def randomNormalScaleScalar =
35  (app randomNormalImmediate (byte 152) (byte 1) (byte 0) (byte 0))
36def randomNormalMixCounter =
37  (app randomNormalImmediate (byte 177) (byte 121) (byte 55) (byte 158))
38def randomNormalMix1 =
39  (app randomNormalImmediate (byte 107) (byte 202) (byte 235) (byte 133))
40def randomNormalMix2 =
41  (app randomNormalImmediate (byte 53) (byte 174) (byte 178) (byte 194))
42def randomNormalCenter =
43  (app randomNormalImmediate (byte 6) (byte 250) (byte 255) (byte 255))
44
45def randomNormalSetBarrier =
46  (app
47    Accelerator.SM86.Control/sm86SetBarrierControl
48    (constructor SM86Barrier SM86Barrier0))
49def randomNormalWaitBarrier =
50  (app
51    Accelerator.SM86.Control/sm86WaitBarrierControl
52    (constructor SM86WaitBarrier SM86WaitBarrier0))
53def randomNormalPrologueControl : (family SM86Control) =
54  (constructor SM86Control SM86ControlValue
55    (byte 2)
56    (constructor SM86YieldMode SM86Yield)
57    (constructor SM86Barrier SM86BarrierNone)
58    (constructor SM86Barrier SM86BarrierNone)
59    (byte 0) (byte 0))
60
61def randomNormalInstruction =
62  (lambda unrestricted body : (family SM86InstructionBody) .
63    (app Accelerator.SM86.Program/sm86ProgramSingleton
64      (app Accelerator.SM86.Instruction/sm86Instruction body)))
65
66def randomNormalAppend =
67  (lambda unrestricted left : (family SM86Program) .
68    (lambda unrestricted right : (family SM86Program) .
69      (app (app Accelerator.SM86.Program/sm86ProgramAppend left) right)))
70
71def randomNormalPrologue =
72  (app randomNormalAppend
73    (app randomNormalInstruction
74      (constructor SM86InstructionBody SM86MoveConstant
75        (app randomNormalRegister (byte 1)) (byte 0)
76        randomNormalConstantBase randomNormalPrologueControl))
77    (app randomNormalAppend
78      (app randomNormalInstruction
79        (constructor SM86InstructionBody SM86SpecialToRegister
80          (app randomNormalRegister (byte 0))
81          (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
82          randomNormalSetBarrier))
83      (app randomNormalAppend
84        (app randomNormalInstruction
85          (constructor SM86InstructionBody SM86MoveImmediate
86            (app randomNormalRegister (byte 15)) randomNormalFour
87            randomNormalWaitBarrier))
88        (app randomNormalAppend
89          (app randomNormalInstruction
90            (constructor SM86InstructionBody SM86SpecialToRegister
91              (app randomNormalRegister (byte 18))
92              (constructor SM86SpecialRegister SM86ThreadIdX)
93              randomNormalSetBarrier))
94          (app randomNormalAppend
95            (app randomNormalInstruction
96              (constructor SM86InstructionBody SM86IntegerMultiplyAddConstant
97                (app randomNormalRegister (byte 0))
98                (app randomNormalRegister (byte 0))
99                (byte 0) randomNormalZero
100                (app randomNormalRegister (byte 18)) randomNormalWaitBarrier))
101            (app randomNormalAppend
102              (app randomNormalInstruction
103                (constructor SM86InstructionBody SM86MoveConstant
104                  (app randomNormalRegister (byte 6)) (byte 0)
105                  randomNormalSeedScalar sm86SafeControl))
106              (app randomNormalAppend
107                (app randomNormalInstruction
108                  (constructor SM86InstructionBody SM86MoveConstant
109                    (app randomNormalRegister (byte 7)) (byte 0)
110                    randomNormalCounterScalar sm86SafeControl))
111                (app randomNormalAppend
112                  (app randomNormalInstruction
113                    (constructor SM86InstructionBody SM86MoveConstant
114                      (app randomNormalRegister (byte 8)) (byte 0)
115                      randomNormalScaleScalar sm86SafeControl))
116                  (app randomNormalAppend
117                    (app randomNormalInstruction
118                      (constructor SM86InstructionBody
119                        SM86IntegerMultiplyAddImmediate
120                        (app randomNormalRegister (byte 2))
121                        (app randomNormalRegister (byte 0))
122                        randomNormalThree
123                        (app randomNormalRegister (byte 7)) sm86SafeControl))
124                    (app randomNormalInstruction
125                      (constructor SM86InstructionBody SM86MoveImmediate
126                        (app randomNormalRegister (byte 9)) randomNormalZero
127                        sm86SafeControl)))))))))))
128
129def randomNormalMix =
130  (lambda unrestricted shift : Byte .
131    (lambda unrestricted multiplier : (family SM86Unsigned32) .
132      (app randomNormalAppend
133        (app randomNormalInstruction
134          (constructor SM86InstructionBody SM86ShiftRightImmediate
135            (app randomNormalRegister (byte 5))
136            (app randomNormalRegister (byte 4)) shift sm86SafeControl))
137        (app randomNormalAppend
138          (app randomNormalInstruction
139            (constructor SM86InstructionBody SM86LogicThreeInputTruthTable
140              (app randomNormalRegister (byte 4))
141              (app randomNormalRegister (byte 4))
142              (app randomNormalRegister (byte 5)) (byte 60) sm86SafeControl))
143          (app randomNormalInstruction
144            (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
145              (app randomNormalRegister (byte 4))
146              (app randomNormalRegister (byte 4)) multiplier
147              sm86ZeroRegister sm86SafeControl))))))
148
149def randomNormalByteSum =
150  (app randomNormalAppend
151    (app randomNormalInstruction
152      (constructor SM86InstructionBody SM86ShiftRightImmediate
153        (app randomNormalRegister (byte 10))
154        (app randomNormalRegister (byte 4)) (byte 8) sm86SafeControl))
155    (app randomNormalAppend
156      (app randomNormalInstruction
157        (constructor SM86InstructionBody SM86ShiftRightImmediate
158          (app randomNormalRegister (byte 11))
159          (app randomNormalRegister (byte 4)) (byte 16) sm86SafeControl))
160      (app randomNormalAppend
161        (app randomNormalInstruction
162          (constructor SM86InstructionBody SM86ShiftRightImmediate
163            (app randomNormalRegister (byte 12))
164            (app randomNormalRegister (byte 4)) (byte 24) sm86SafeControl))
165        (app randomNormalAppend
166          (app randomNormalInstruction
167            (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
168              (app randomNormalRegister (byte 13))
169              (app randomNormalRegister (byte 10))
170              (app randomNormalImmediate
171                (byte 0) (byte 255) (byte 255) (byte 255))
172              (app randomNormalRegister (byte 4)) sm86SafeControl))
173          (app randomNormalAppend
174            (app randomNormalInstruction
175              (constructor SM86InstructionBody SM86IntegerAddThreeRegister
176                (app randomNormalRegister (byte 9))
177                (app randomNormalRegister (byte 9))
178                (app randomNormalRegister (byte 13)) sm86SafeControl))
179            (app randomNormalAppend
180              (app randomNormalInstruction
181                (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
182                  (app randomNormalRegister (byte 13))
183                  (app randomNormalRegister (byte 11))
184                  (app randomNormalImmediate
185                    (byte 0) (byte 255) (byte 255) (byte 255))
186                  (app randomNormalRegister (byte 10)) sm86SafeControl))
187              (app randomNormalAppend
188                (app randomNormalInstruction
189                  (constructor SM86InstructionBody SM86IntegerAddThreeRegister
190                    (app randomNormalRegister (byte 9))
191                    (app randomNormalRegister (byte 9))
192                    (app randomNormalRegister (byte 13)) sm86SafeControl))
193                (app randomNormalAppend
194                  (app randomNormalInstruction
195                    (constructor SM86InstructionBody
196                      SM86IntegerMultiplyAddImmediate
197                      (app randomNormalRegister (byte 13))
198                      (app randomNormalRegister (byte 12))
199                      (app randomNormalImmediate
200                        (byte 0) (byte 255) (byte 255) (byte 255))
201                      (app randomNormalRegister (byte 11)) sm86SafeControl))
202                  (app randomNormalAppend
203                    (app randomNormalInstruction
204                      (constructor SM86InstructionBody SM86IntegerAddThreeRegister
205                        (app randomNormalRegister (byte 9))
206                        (app randomNormalRegister (byte 9))
207                        (app randomNormalRegister (byte 13)) sm86SafeControl))
208                    (app randomNormalInstruction
209                      (constructor SM86InstructionBody SM86IntegerAddThreeRegister
210                        (app randomNormalRegister (byte 9))
211                        (app randomNormalRegister (byte 9))
212                        (app randomNormalRegister (byte 12))
213                        sm86SafeControl)))))))))))
214
215def randomNormalHash =
216  (lambda unrestricted stream : (family SM86Unsigned32) .
217    (app randomNormalAppend
218      (app randomNormalInstruction
219        (constructor SM86InstructionBody SM86IntegerAddThreeImmediate
220          (app randomNormalRegister (byte 3))
221          (app randomNormalRegister (byte 2)) stream sm86SafeControl))
222      (app randomNormalAppend
223        (app randomNormalInstruction
224          (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
225            (app randomNormalRegister (byte 4))
226            (app randomNormalRegister (byte 3)) randomNormalMixCounter
227            (app randomNormalRegister (byte 6)) sm86SafeControl))
228        (app randomNormalAppend
229          (app (app randomNormalMix (byte 16)) randomNormalMix1)
230          (app randomNormalAppend
231            (app (app randomNormalMix (byte 13)) randomNormalMix2)
232            (app randomNormalAppend
233              (app randomNormalInstruction
234                (constructor SM86InstructionBody SM86ShiftRightImmediate
235                  (app randomNormalRegister (byte 5))
236                  (app randomNormalRegister (byte 4))
237                  (byte 16) sm86SafeControl))
238              (app randomNormalAppend
239                (app randomNormalInstruction
240                  (constructor SM86InstructionBody SM86LogicThreeInputTruthTable
241                    (app randomNormalRegister (byte 4))
242                    (app randomNormalRegister (byte 4))
243                    (app randomNormalRegister (byte 5))
244                    (byte 60) sm86SafeControl))
245                randomNormalByteSum)))))))
246
247def randomNormalEpilogue =
248  (app randomNormalAppend
249    (app randomNormalInstruction
250      (constructor SM86InstructionBody SM86IntegerAddThreeImmediate
251        (app randomNormalRegister (byte 9))
252        (app randomNormalRegister (byte 9)) randomNormalCenter
253        sm86SafeControl))
254    (app randomNormalAppend
255      (app randomNormalInstruction
256        (constructor SM86InstructionBody SM86IntegerToFloat
257          (app randomNormalRegister (byte 14))
258          (app randomNormalRegister (byte 9)) sm86SafeControl))
259      (app randomNormalAppend
260        (app randomNormalInstruction
261          (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant
262            (app randomNormalRegister (byte 16))
263            (app randomNormalRegister (byte 0))
264            (app randomNormalRegister (byte 15))
265            (byte 0) randomNormalOutputPointer sm86SafeControl))
266        (app randomNormalAppend
267          (app randomNormalInstruction
268            (constructor SM86InstructionBody SM86FloatMultiply
269              (app randomNormalRegister (byte 14))
270              (app randomNormalRegister (byte 14))
271              (app randomNormalRegister (byte 8)) sm86SafeControl))
272          (app randomNormalAppend
273            (app randomNormalInstruction
274              (constructor SM86InstructionBody SM86StoreGlobal
275                (app randomNormalRegister (byte 16))
276                (app randomNormalRegister (byte 14)) randomNormalZero
277                sm86SafeControl))
278            (app randomNormalInstruction
279              (constructor SM86InstructionBody SM86Exit
280                sm86BranchControl)))))))
281
282def randomNormalSM86Program : (family SM86Program) =
283  (app randomNormalAppend randomNormalPrologue
284    (app randomNormalAppend
285      (app randomNormalHash randomNormalZero)
286      (app randomNormalAppend
287        (app randomNormalHash
288          (app randomNormalImmediate (byte 1) (byte 0) (byte 0) (byte 0)))
289        (app randomNormalAppend
290          (app randomNormalHash
291            (app randomNormalImmediate (byte 2) (byte 0) (byte 0) (byte 0)))
292          randomNormalEpilogue))))
293
294def randomNormalSM86InstructionCount =
295  (app Accelerator.SM86.Program/sm86ProgramCount randomNormalSM86Program)
296
297def randomNormalSM86RegisterCount = (byte-to-nat (byte 24))