1module Data.SHA256Constants
2
3import Data.SHA256
4import Model.Config
5
6-- Part of `sha256RoundConstants`, lifted out to keep it inside the §28.3 size and
7-- nesting limits; the parameters are the locals it still needs.
8def sha256RoundConstantsPart1 =
9 (constructor
10 SHA256Schedule
11 SHA256ScheduleNext
12 (constructor ModelWord32 ModelWord32Value (byte 36) (byte 6) (byte 153) (byte 214))
13 (constructor
14 SHA256Schedule
15 SHA256ScheduleNext
16 (constructor ModelWord32 ModelWord32Value (byte 133) (byte 53) (byte 14) (byte 244))
17 (constructor
18 SHA256Schedule
19 SHA256ScheduleNext
20 (constructor ModelWord32 ModelWord32Value (byte 112) (byte 160) (byte 106) (byte 16))
21 (constructor
22 SHA256Schedule
23 SHA256ScheduleNext
24 (constructor ModelWord32 ModelWord32Value (byte 22) (byte 193) (byte 164) (byte 25))
25 (constructor
26 SHA256Schedule
27 SHA256ScheduleNext
28 (constructor ModelWord32 ModelWord32Value (byte 8) (byte 108) (byte 55) (byte 30))
29 (constructor
30 SHA256Schedule
31 SHA256ScheduleNext
32 (constructor ModelWord32 ModelWord32Value (byte 76) (byte 119) (byte 72) (byte 39))
33 (constructor
34 SHA256Schedule
35 SHA256ScheduleNext
36 (constructor
37 ModelWord32
38 ModelWord32Value
39 (byte 181)
40 (byte 188)
41 (byte 176)
42 (byte 52))
43 (constructor
44 SHA256Schedule
45 SHA256ScheduleNext
46 (constructor
47 ModelWord32
48 ModelWord32Value
49 (byte 179)
50 (byte 12)
51 (byte 28)
52 (byte 57))
53 (constructor
54 SHA256Schedule
55 SHA256ScheduleNext
56 (constructor
57 ModelWord32
58 ModelWord32Value
59 (byte 74)
60 (byte 170)
61 (byte 216)
62 (byte 78))
63 (constructor
64 SHA256Schedule
65 SHA256ScheduleNext
66 (constructor
67 ModelWord32
68 ModelWord32Value
69 (byte 79)
70 (byte 202)
71 (byte 156)
72 (byte 91))
73 (constructor
74 SHA256Schedule
75 SHA256ScheduleNext
76 (constructor
77 ModelWord32
78 ModelWord32Value
79 (byte 243)
80 (byte 111)
81 (byte 46)
82 (byte 104))
83 (constructor
84 SHA256Schedule
85 SHA256ScheduleNext
86 (constructor
87 ModelWord32
88 ModelWord32Value
89 (byte 238)
90 (byte 130)
91 (byte 143)
92 (byte 116))
93 (constructor
94 SHA256Schedule
95 SHA256ScheduleNext
96 (constructor
97 ModelWord32
98 ModelWord32Value
99 (byte 111)
100 (byte 99)
101 (byte 165)
102 (byte 120))
103 (constructor
104 SHA256Schedule
105 SHA256ScheduleNext
106 (constructor
107 ModelWord32
108 ModelWord32Value
109 (byte 20)
110 (byte 120)
111 (byte 200)
112 (byte 132))
113 (constructor
114 SHA256Schedule
115 SHA256ScheduleNext
116 (constructor
117 ModelWord32
118 ModelWord32Value
119 (byte 8)
120 (byte 2)
121 (byte 199)
122 (byte 140))
123 (constructor
124 SHA256Schedule
125 SHA256ScheduleNext
126 (constructor
127 ModelWord32
128 ModelWord32Value
129 (byte 250)
130 (byte 255)
131 (byte 190)
132 (byte 144))
133 (constructor
134 SHA256Schedule
135 SHA256ScheduleNext
136 (constructor
137 ModelWord32
138 ModelWord32Value
139 (byte 235)
140 (byte 108)
141 (byte 80)
142 (byte 164))
143 (constructor
144 SHA256Schedule
145 SHA256ScheduleNext
146 (constructor
147 ModelWord32
148 ModelWord32Value
149 (byte 247)
150 (byte 163)
151 (byte 249)
152 (byte 190))
153 (constructor
154 SHA256Schedule
155 SHA256ScheduleNext
156 (constructor
157 ModelWord32
158 ModelWord32Value
159 (byte 242)
160 (byte 120)
161 (byte 113)
162 (byte 198))
163 (constructor SHA256Schedule SHA256ScheduleEnd))))))))))))))))))))
164
165-- Part of `sha256RoundConstants`, lifted out to keep it inside the §28.3 size and
166-- nesting limits; the parameters are the locals it still needs.
167def sha256RoundConstantsPart2 =
168 (constructor
169 SHA256Schedule
170 SHA256ScheduleNext
171 (constructor ModelWord32 ModelWord32Value (byte 200) (byte 39) (byte 3) (byte 176))
172 (constructor
173 SHA256Schedule
174 SHA256ScheduleNext
175 (constructor ModelWord32 ModelWord32Value (byte 199) (byte 127) (byte 89) (byte 191))
176 (constructor
177 SHA256Schedule
178 SHA256ScheduleNext
179 (constructor ModelWord32 ModelWord32Value (byte 243) (byte 11) (byte 224) (byte 198))
180 (constructor
181 SHA256Schedule
182 SHA256ScheduleNext
183 (constructor ModelWord32 ModelWord32Value (byte 71) (byte 145) (byte 167) (byte 213))
184 (constructor
185 SHA256Schedule
186 SHA256ScheduleNext
187 (constructor ModelWord32 ModelWord32Value (byte 81) (byte 99) (byte 202) (byte 6))
188 (constructor
189 SHA256Schedule
190 SHA256ScheduleNext
191 (constructor ModelWord32 ModelWord32Value (byte 103) (byte 41) (byte 41) (byte 20))
192 (constructor
193 SHA256Schedule
194 SHA256ScheduleNext
195 (constructor ModelWord32 ModelWord32Value (byte 133) (byte 10) (byte 183) (byte 39))
196 (constructor
197 SHA256Schedule
198 SHA256ScheduleNext
199 (constructor ModelWord32 ModelWord32Value (byte 56) (byte 33) (byte 27) (byte 46))
200 (constructor
201 SHA256Schedule
202 SHA256ScheduleNext
203 (constructor
204 ModelWord32
205 ModelWord32Value
206 (byte 252)
207 (byte 109)
208 (byte 44)
209 (byte 77))
210 (constructor
211 SHA256Schedule
212 SHA256ScheduleNext
213 (constructor
214 ModelWord32
215 ModelWord32Value
216 (byte 19)
217 (byte 13)
218 (byte 56)
219 (byte 83))
220 (constructor
221 SHA256Schedule
222 SHA256ScheduleNext
223 (constructor
224 ModelWord32
225 ModelWord32Value
226 (byte 84)
227 (byte 115)
228 (byte 10)
229 (byte 101))
230 (constructor
231 SHA256Schedule
232 SHA256ScheduleNext
233 (constructor
234 ModelWord32
235 ModelWord32Value
236 (byte 187)
237 (byte 10)
238 (byte 106)
239 (byte 118))
240 (constructor
241 SHA256Schedule
242 SHA256ScheduleNext
243 (constructor
244 ModelWord32
245 ModelWord32Value
246 (byte 46)
247 (byte 201)
248 (byte 194)
249 (byte 129))
250 (constructor
251 SHA256Schedule
252 SHA256ScheduleNext
253 (constructor
254 ModelWord32
255 ModelWord32Value
256 (byte 133)
257 (byte 44)
258 (byte 114)
259 (byte 146))
260 (constructor
261 SHA256Schedule
262 SHA256ScheduleNext
263 (constructor
264 ModelWord32
265 ModelWord32Value
266 (byte 161)
267 (byte 232)
268 (byte 191)
269 (byte 162))
270 (constructor
271 SHA256Schedule
272 SHA256ScheduleNext
273 (constructor
274 ModelWord32
275 ModelWord32Value
276 (byte 75)
277 (byte 102)
278 (byte 26)
279 (byte 168))
280 (constructor
281 SHA256Schedule
282 SHA256ScheduleNext
283 (constructor
284 ModelWord32
285 ModelWord32Value
286 (byte 112)
287 (byte 139)
288 (byte 75)
289 (byte 194))
290 (constructor
291 SHA256Schedule
292 SHA256ScheduleNext
293 (constructor
294 ModelWord32
295 ModelWord32Value
296 (byte 163)
297 (byte 81)
298 (byte 108)
299 (byte 199))
300 (constructor
301 SHA256Schedule
302 SHA256ScheduleNext
303 (constructor
304 ModelWord32
305 ModelWord32Value
306 (byte 25)
307 (byte 232)
308 (byte 146)
309 (byte 209))
310 sha256RoundConstantsPart1)))))))))))))))))))
311
312-- Part of `sha256RoundConstants`, lifted out to keep it inside the §28.3 size and
313-- nesting limits; the parameters are the locals it still needs.
314def sha256RoundConstantsPart3 =
315 (constructor
316 SHA256Schedule
317 SHA256ScheduleNext
318 (constructor ModelWord32 ModelWord32Value (byte 254) (byte 177) (byte 222) (byte 128))
319 (constructor
320 SHA256Schedule
321 SHA256ScheduleNext
322 (constructor ModelWord32 ModelWord32Value (byte 167) (byte 6) (byte 220) (byte 155))
323 (constructor
324 SHA256Schedule
325 SHA256ScheduleNext
326 (constructor ModelWord32 ModelWord32Value (byte 116) (byte 241) (byte 155) (byte 193))
327 (constructor
328 SHA256Schedule
329 SHA256ScheduleNext
330 (constructor ModelWord32 ModelWord32Value (byte 193) (byte 105) (byte 155) (byte 228))
331 (constructor
332 SHA256Schedule
333 SHA256ScheduleNext
334 (constructor ModelWord32 ModelWord32Value (byte 134) (byte 71) (byte 190) (byte 239))
335 (constructor
336 SHA256Schedule
337 SHA256ScheduleNext
338 (constructor ModelWord32 ModelWord32Value (byte 198) (byte 157) (byte 193) (byte 15))
339 (constructor
340 SHA256Schedule
341 SHA256ScheduleNext
342 (constructor ModelWord32 ModelWord32Value (byte 204) (byte 161) (byte 12) (byte 36))
343 (constructor
344 SHA256Schedule
345 SHA256ScheduleNext
346 (constructor
347 ModelWord32
348 ModelWord32Value
349 (byte 111)
350 (byte 44)
351 (byte 233)
352 (byte 45))
353 (constructor
354 SHA256Schedule
355 SHA256ScheduleNext
356 (constructor
357 ModelWord32
358 ModelWord32Value
359 (byte 170)
360 (byte 132)
361 (byte 116)
362 (byte 74))
363 (constructor
364 SHA256Schedule
365 SHA256ScheduleNext
366 (constructor
367 ModelWord32
368 ModelWord32Value
369 (byte 220)
370 (byte 169)
371 (byte 176)
372 (byte 92))
373 (constructor
374 SHA256Schedule
375 SHA256ScheduleNext
376 (constructor
377 ModelWord32
378 ModelWord32Value
379 (byte 218)
380 (byte 136)
381 (byte 249)
382 (byte 118))
383 (constructor
384 SHA256Schedule
385 SHA256ScheduleNext
386 (constructor
387 ModelWord32
388 ModelWord32Value
389 (byte 82)
390 (byte 81)
391 (byte 62)
392 (byte 152))
393 (constructor
394 SHA256Schedule
395 SHA256ScheduleNext
396 (constructor
397 ModelWord32
398 ModelWord32Value
399 (byte 109)
400 (byte 198)
401 (byte 49)
402 (byte 168))
403 sha256RoundConstantsPart2)))))))))))))
404
405def sha256RoundConstants =
406 (constructor
407 SHA256Schedule
408 SHA256ScheduleNext
409 (constructor ModelWord32 ModelWord32Value (byte 152) (byte 47) (byte 138) (byte 66))
410 (constructor
411 SHA256Schedule
412 SHA256ScheduleNext
413 (constructor ModelWord32 ModelWord32Value (byte 145) (byte 68) (byte 55) (byte 113))
414 (constructor
415 SHA256Schedule
416 SHA256ScheduleNext
417 (constructor ModelWord32 ModelWord32Value (byte 207) (byte 251) (byte 192) (byte 181))
418 (constructor
419 SHA256Schedule
420 SHA256ScheduleNext
421 (constructor ModelWord32 ModelWord32Value (byte 165) (byte 219) (byte 181) (byte 233))
422 (constructor
423 SHA256Schedule
424 SHA256ScheduleNext
425 (constructor ModelWord32 ModelWord32Value (byte 91) (byte 194) (byte 86) (byte 57))
426 (constructor
427 SHA256Schedule
428 SHA256ScheduleNext
429 (constructor ModelWord32 ModelWord32Value (byte 241) (byte 17) (byte 241) (byte 89))
430 (constructor
431 SHA256Schedule
432 SHA256ScheduleNext
433 (constructor
434 ModelWord32
435 ModelWord32Value
436 (byte 164)
437 (byte 130)
438 (byte 63)
439 (byte 146))
440 (constructor
441 SHA256Schedule
442 SHA256ScheduleNext
443 (constructor
444 ModelWord32
445 ModelWord32Value
446 (byte 213)
447 (byte 94)
448 (byte 28)
449 (byte 171))
450 (constructor
451 SHA256Schedule
452 SHA256ScheduleNext
453 (constructor
454 ModelWord32
455 ModelWord32Value
456 (byte 152)
457 (byte 170)
458 (byte 7)
459 (byte 216))
460 (constructor
461 SHA256Schedule
462 SHA256ScheduleNext
463 (constructor
464 ModelWord32
465 ModelWord32Value
466 (byte 1)
467 (byte 91)
468 (byte 131)
469 (byte 18))
470 (constructor
471 SHA256Schedule
472 SHA256ScheduleNext
473 (constructor
474 ModelWord32
475 ModelWord32Value
476 (byte 190)
477 (byte 133)
478 (byte 49)
479 (byte 36))
480 (constructor
481 SHA256Schedule
482 SHA256ScheduleNext
483 (constructor
484 ModelWord32
485 ModelWord32Value
486 (byte 195)
487 (byte 125)
488 (byte 12)
489 (byte 85))
490 (constructor
491 SHA256Schedule
492 SHA256ScheduleNext
493 (constructor
494 ModelWord32
495 ModelWord32Value
496 (byte 116)
497 (byte 93)
498 (byte 190)
499 (byte 114))
500 sha256RoundConstantsPart3)))))))))))))
501
502def sha256RoundConstantCount =
503 (byte-to-nat (byte 64))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.