• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
1 /* MIT License
2  *
3  * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
4  * Copyright (c) 2022-2023 HACL* Contributors
5  *
6  * Permission is hereby granted, free of charge, to any person obtaining a copy
7  * of this software and associated documentation files (the "Software"), to deal
8  * in the Software without restriction, including without limitation the rights
9  * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10  * copies of the Software, and to permit persons to whom the Software is
11  * furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be included in all
14  * copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21  * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
22  * SOFTWARE.
23  */
24 
25 
26 #include "internal/Hacl_Hash_MD5.h"
27 
28 static uint32_t _h0[4U] = { 0x67452301U, 0xefcdab89U, 0x98badcfeU, 0x10325476U };
29 
30 static uint32_t
31 _t[64U] =
32   {
33     0xd76aa478U, 0xe8c7b756U, 0x242070dbU, 0xc1bdceeeU, 0xf57c0fafU, 0x4787c62aU, 0xa8304613U,
34     0xfd469501U, 0x698098d8U, 0x8b44f7afU, 0xffff5bb1U, 0x895cd7beU, 0x6b901122U, 0xfd987193U,
35     0xa679438eU, 0x49b40821U, 0xf61e2562U, 0xc040b340U, 0x265e5a51U, 0xe9b6c7aaU, 0xd62f105dU,
36     0x02441453U, 0xd8a1e681U, 0xe7d3fbc8U, 0x21e1cde6U, 0xc33707d6U, 0xf4d50d87U, 0x455a14edU,
37     0xa9e3e905U, 0xfcefa3f8U, 0x676f02d9U, 0x8d2a4c8aU, 0xfffa3942U, 0x8771f681U, 0x6d9d6122U,
38     0xfde5380cU, 0xa4beea44U, 0x4bdecfa9U, 0xf6bb4b60U, 0xbebfbc70U, 0x289b7ec6U, 0xeaa127faU,
39     0xd4ef3085U, 0x4881d05U, 0xd9d4d039U, 0xe6db99e5U, 0x1fa27cf8U, 0xc4ac5665U, 0xf4292244U,
40     0x432aff97U, 0xab9423a7U, 0xfc93a039U, 0x655b59c3U, 0x8f0ccc92U, 0xffeff47dU, 0x85845dd1U,
41     0x6fa87e4fU, 0xfe2ce6e0U, 0xa3014314U, 0x4e0811a1U, 0xf7537e82U, 0xbd3af235U, 0x2ad7d2bbU,
42     0xeb86d391U
43   };
44 
Hacl_Hash_MD5_init(uint32_t * s)45 void Hacl_Hash_MD5_init(uint32_t *s)
46 {
47   KRML_MAYBE_FOR4(i, 0U, 4U, 1U, s[i] = _h0[i];);
48 }
49 
update(uint32_t * abcd,uint8_t * x)50 static void update(uint32_t *abcd, uint8_t *x)
51 {
52   uint32_t aa = abcd[0U];
53   uint32_t bb = abcd[1U];
54   uint32_t cc = abcd[2U];
55   uint32_t dd = abcd[3U];
56   uint32_t va = abcd[0U];
57   uint32_t vb0 = abcd[1U];
58   uint32_t vc0 = abcd[2U];
59   uint32_t vd0 = abcd[3U];
60   uint8_t *b0 = x;
61   uint32_t u = load32_le(b0);
62   uint32_t xk = u;
63   uint32_t ti0 = _t[0U];
64   uint32_t
65   v =
66     vb0
67     +
68       ((va + ((vb0 & vc0) | (~vb0 & vd0)) + xk + ti0)
69       << 7U
70       | (va + ((vb0 & vc0) | (~vb0 & vd0)) + xk + ti0) >> 25U);
71   abcd[0U] = v;
72   uint32_t va0 = abcd[3U];
73   uint32_t vb1 = abcd[0U];
74   uint32_t vc1 = abcd[1U];
75   uint32_t vd1 = abcd[2U];
76   uint8_t *b1 = x + 4U;
77   uint32_t u0 = load32_le(b1);
78   uint32_t xk0 = u0;
79   uint32_t ti1 = _t[1U];
80   uint32_t
81   v0 =
82     vb1
83     +
84       ((va0 + ((vb1 & vc1) | (~vb1 & vd1)) + xk0 + ti1)
85       << 12U
86       | (va0 + ((vb1 & vc1) | (~vb1 & vd1)) + xk0 + ti1) >> 20U);
87   abcd[3U] = v0;
88   uint32_t va1 = abcd[2U];
89   uint32_t vb2 = abcd[3U];
90   uint32_t vc2 = abcd[0U];
91   uint32_t vd2 = abcd[1U];
92   uint8_t *b2 = x + 8U;
93   uint32_t u1 = load32_le(b2);
94   uint32_t xk1 = u1;
95   uint32_t ti2 = _t[2U];
96   uint32_t
97   v1 =
98     vb2
99     +
100       ((va1 + ((vb2 & vc2) | (~vb2 & vd2)) + xk1 + ti2)
101       << 17U
102       | (va1 + ((vb2 & vc2) | (~vb2 & vd2)) + xk1 + ti2) >> 15U);
103   abcd[2U] = v1;
104   uint32_t va2 = abcd[1U];
105   uint32_t vb3 = abcd[2U];
106   uint32_t vc3 = abcd[3U];
107   uint32_t vd3 = abcd[0U];
108   uint8_t *b3 = x + 12U;
109   uint32_t u2 = load32_le(b3);
110   uint32_t xk2 = u2;
111   uint32_t ti3 = _t[3U];
112   uint32_t
113   v2 =
114     vb3
115     +
116       ((va2 + ((vb3 & vc3) | (~vb3 & vd3)) + xk2 + ti3)
117       << 22U
118       | (va2 + ((vb3 & vc3) | (~vb3 & vd3)) + xk2 + ti3) >> 10U);
119   abcd[1U] = v2;
120   uint32_t va3 = abcd[0U];
121   uint32_t vb4 = abcd[1U];
122   uint32_t vc4 = abcd[2U];
123   uint32_t vd4 = abcd[3U];
124   uint8_t *b4 = x + 16U;
125   uint32_t u3 = load32_le(b4);
126   uint32_t xk3 = u3;
127   uint32_t ti4 = _t[4U];
128   uint32_t
129   v3 =
130     vb4
131     +
132       ((va3 + ((vb4 & vc4) | (~vb4 & vd4)) + xk3 + ti4)
133       << 7U
134       | (va3 + ((vb4 & vc4) | (~vb4 & vd4)) + xk3 + ti4) >> 25U);
135   abcd[0U] = v3;
136   uint32_t va4 = abcd[3U];
137   uint32_t vb5 = abcd[0U];
138   uint32_t vc5 = abcd[1U];
139   uint32_t vd5 = abcd[2U];
140   uint8_t *b5 = x + 20U;
141   uint32_t u4 = load32_le(b5);
142   uint32_t xk4 = u4;
143   uint32_t ti5 = _t[5U];
144   uint32_t
145   v4 =
146     vb5
147     +
148       ((va4 + ((vb5 & vc5) | (~vb5 & vd5)) + xk4 + ti5)
149       << 12U
150       | (va4 + ((vb5 & vc5) | (~vb5 & vd5)) + xk4 + ti5) >> 20U);
151   abcd[3U] = v4;
152   uint32_t va5 = abcd[2U];
153   uint32_t vb6 = abcd[3U];
154   uint32_t vc6 = abcd[0U];
155   uint32_t vd6 = abcd[1U];
156   uint8_t *b6 = x + 24U;
157   uint32_t u5 = load32_le(b6);
158   uint32_t xk5 = u5;
159   uint32_t ti6 = _t[6U];
160   uint32_t
161   v5 =
162     vb6
163     +
164       ((va5 + ((vb6 & vc6) | (~vb6 & vd6)) + xk5 + ti6)
165       << 17U
166       | (va5 + ((vb6 & vc6) | (~vb6 & vd6)) + xk5 + ti6) >> 15U);
167   abcd[2U] = v5;
168   uint32_t va6 = abcd[1U];
169   uint32_t vb7 = abcd[2U];
170   uint32_t vc7 = abcd[3U];
171   uint32_t vd7 = abcd[0U];
172   uint8_t *b7 = x + 28U;
173   uint32_t u6 = load32_le(b7);
174   uint32_t xk6 = u6;
175   uint32_t ti7 = _t[7U];
176   uint32_t
177   v6 =
178     vb7
179     +
180       ((va6 + ((vb7 & vc7) | (~vb7 & vd7)) + xk6 + ti7)
181       << 22U
182       | (va6 + ((vb7 & vc7) | (~vb7 & vd7)) + xk6 + ti7) >> 10U);
183   abcd[1U] = v6;
184   uint32_t va7 = abcd[0U];
185   uint32_t vb8 = abcd[1U];
186   uint32_t vc8 = abcd[2U];
187   uint32_t vd8 = abcd[3U];
188   uint8_t *b8 = x + 32U;
189   uint32_t u7 = load32_le(b8);
190   uint32_t xk7 = u7;
191   uint32_t ti8 = _t[8U];
192   uint32_t
193   v7 =
194     vb8
195     +
196       ((va7 + ((vb8 & vc8) | (~vb8 & vd8)) + xk7 + ti8)
197       << 7U
198       | (va7 + ((vb8 & vc8) | (~vb8 & vd8)) + xk7 + ti8) >> 25U);
199   abcd[0U] = v7;
200   uint32_t va8 = abcd[3U];
201   uint32_t vb9 = abcd[0U];
202   uint32_t vc9 = abcd[1U];
203   uint32_t vd9 = abcd[2U];
204   uint8_t *b9 = x + 36U;
205   uint32_t u8 = load32_le(b9);
206   uint32_t xk8 = u8;
207   uint32_t ti9 = _t[9U];
208   uint32_t
209   v8 =
210     vb9
211     +
212       ((va8 + ((vb9 & vc9) | (~vb9 & vd9)) + xk8 + ti9)
213       << 12U
214       | (va8 + ((vb9 & vc9) | (~vb9 & vd9)) + xk8 + ti9) >> 20U);
215   abcd[3U] = v8;
216   uint32_t va9 = abcd[2U];
217   uint32_t vb10 = abcd[3U];
218   uint32_t vc10 = abcd[0U];
219   uint32_t vd10 = abcd[1U];
220   uint8_t *b10 = x + 40U;
221   uint32_t u9 = load32_le(b10);
222   uint32_t xk9 = u9;
223   uint32_t ti10 = _t[10U];
224   uint32_t
225   v9 =
226     vb10
227     +
228       ((va9 + ((vb10 & vc10) | (~vb10 & vd10)) + xk9 + ti10)
229       << 17U
230       | (va9 + ((vb10 & vc10) | (~vb10 & vd10)) + xk9 + ti10) >> 15U);
231   abcd[2U] = v9;
232   uint32_t va10 = abcd[1U];
233   uint32_t vb11 = abcd[2U];
234   uint32_t vc11 = abcd[3U];
235   uint32_t vd11 = abcd[0U];
236   uint8_t *b11 = x + 44U;
237   uint32_t u10 = load32_le(b11);
238   uint32_t xk10 = u10;
239   uint32_t ti11 = _t[11U];
240   uint32_t
241   v10 =
242     vb11
243     +
244       ((va10 + ((vb11 & vc11) | (~vb11 & vd11)) + xk10 + ti11)
245       << 22U
246       | (va10 + ((vb11 & vc11) | (~vb11 & vd11)) + xk10 + ti11) >> 10U);
247   abcd[1U] = v10;
248   uint32_t va11 = abcd[0U];
249   uint32_t vb12 = abcd[1U];
250   uint32_t vc12 = abcd[2U];
251   uint32_t vd12 = abcd[3U];
252   uint8_t *b12 = x + 48U;
253   uint32_t u11 = load32_le(b12);
254   uint32_t xk11 = u11;
255   uint32_t ti12 = _t[12U];
256   uint32_t
257   v11 =
258     vb12
259     +
260       ((va11 + ((vb12 & vc12) | (~vb12 & vd12)) + xk11 + ti12)
261       << 7U
262       | (va11 + ((vb12 & vc12) | (~vb12 & vd12)) + xk11 + ti12) >> 25U);
263   abcd[0U] = v11;
264   uint32_t va12 = abcd[3U];
265   uint32_t vb13 = abcd[0U];
266   uint32_t vc13 = abcd[1U];
267   uint32_t vd13 = abcd[2U];
268   uint8_t *b13 = x + 52U;
269   uint32_t u12 = load32_le(b13);
270   uint32_t xk12 = u12;
271   uint32_t ti13 = _t[13U];
272   uint32_t
273   v12 =
274     vb13
275     +
276       ((va12 + ((vb13 & vc13) | (~vb13 & vd13)) + xk12 + ti13)
277       << 12U
278       | (va12 + ((vb13 & vc13) | (~vb13 & vd13)) + xk12 + ti13) >> 20U);
279   abcd[3U] = v12;
280   uint32_t va13 = abcd[2U];
281   uint32_t vb14 = abcd[3U];
282   uint32_t vc14 = abcd[0U];
283   uint32_t vd14 = abcd[1U];
284   uint8_t *b14 = x + 56U;
285   uint32_t u13 = load32_le(b14);
286   uint32_t xk13 = u13;
287   uint32_t ti14 = _t[14U];
288   uint32_t
289   v13 =
290     vb14
291     +
292       ((va13 + ((vb14 & vc14) | (~vb14 & vd14)) + xk13 + ti14)
293       << 17U
294       | (va13 + ((vb14 & vc14) | (~vb14 & vd14)) + xk13 + ti14) >> 15U);
295   abcd[2U] = v13;
296   uint32_t va14 = abcd[1U];
297   uint32_t vb15 = abcd[2U];
298   uint32_t vc15 = abcd[3U];
299   uint32_t vd15 = abcd[0U];
300   uint8_t *b15 = x + 60U;
301   uint32_t u14 = load32_le(b15);
302   uint32_t xk14 = u14;
303   uint32_t ti15 = _t[15U];
304   uint32_t
305   v14 =
306     vb15
307     +
308       ((va14 + ((vb15 & vc15) | (~vb15 & vd15)) + xk14 + ti15)
309       << 22U
310       | (va14 + ((vb15 & vc15) | (~vb15 & vd15)) + xk14 + ti15) >> 10U);
311   abcd[1U] = v14;
312   uint32_t va15 = abcd[0U];
313   uint32_t vb16 = abcd[1U];
314   uint32_t vc16 = abcd[2U];
315   uint32_t vd16 = abcd[3U];
316   uint8_t *b16 = x + 4U;
317   uint32_t u15 = load32_le(b16);
318   uint32_t xk15 = u15;
319   uint32_t ti16 = _t[16U];
320   uint32_t
321   v15 =
322     vb16
323     +
324       ((va15 + ((vb16 & vd16) | (vc16 & ~vd16)) + xk15 + ti16)
325       << 5U
326       | (va15 + ((vb16 & vd16) | (vc16 & ~vd16)) + xk15 + ti16) >> 27U);
327   abcd[0U] = v15;
328   uint32_t va16 = abcd[3U];
329   uint32_t vb17 = abcd[0U];
330   uint32_t vc17 = abcd[1U];
331   uint32_t vd17 = abcd[2U];
332   uint8_t *b17 = x + 24U;
333   uint32_t u16 = load32_le(b17);
334   uint32_t xk16 = u16;
335   uint32_t ti17 = _t[17U];
336   uint32_t
337   v16 =
338     vb17
339     +
340       ((va16 + ((vb17 & vd17) | (vc17 & ~vd17)) + xk16 + ti17)
341       << 9U
342       | (va16 + ((vb17 & vd17) | (vc17 & ~vd17)) + xk16 + ti17) >> 23U);
343   abcd[3U] = v16;
344   uint32_t va17 = abcd[2U];
345   uint32_t vb18 = abcd[3U];
346   uint32_t vc18 = abcd[0U];
347   uint32_t vd18 = abcd[1U];
348   uint8_t *b18 = x + 44U;
349   uint32_t u17 = load32_le(b18);
350   uint32_t xk17 = u17;
351   uint32_t ti18 = _t[18U];
352   uint32_t
353   v17 =
354     vb18
355     +
356       ((va17 + ((vb18 & vd18) | (vc18 & ~vd18)) + xk17 + ti18)
357       << 14U
358       | (va17 + ((vb18 & vd18) | (vc18 & ~vd18)) + xk17 + ti18) >> 18U);
359   abcd[2U] = v17;
360   uint32_t va18 = abcd[1U];
361   uint32_t vb19 = abcd[2U];
362   uint32_t vc19 = abcd[3U];
363   uint32_t vd19 = abcd[0U];
364   uint8_t *b19 = x;
365   uint32_t u18 = load32_le(b19);
366   uint32_t xk18 = u18;
367   uint32_t ti19 = _t[19U];
368   uint32_t
369   v18 =
370     vb19
371     +
372       ((va18 + ((vb19 & vd19) | (vc19 & ~vd19)) + xk18 + ti19)
373       << 20U
374       | (va18 + ((vb19 & vd19) | (vc19 & ~vd19)) + xk18 + ti19) >> 12U);
375   abcd[1U] = v18;
376   uint32_t va19 = abcd[0U];
377   uint32_t vb20 = abcd[1U];
378   uint32_t vc20 = abcd[2U];
379   uint32_t vd20 = abcd[3U];
380   uint8_t *b20 = x + 20U;
381   uint32_t u19 = load32_le(b20);
382   uint32_t xk19 = u19;
383   uint32_t ti20 = _t[20U];
384   uint32_t
385   v19 =
386     vb20
387     +
388       ((va19 + ((vb20 & vd20) | (vc20 & ~vd20)) + xk19 + ti20)
389       << 5U
390       | (va19 + ((vb20 & vd20) | (vc20 & ~vd20)) + xk19 + ti20) >> 27U);
391   abcd[0U] = v19;
392   uint32_t va20 = abcd[3U];
393   uint32_t vb21 = abcd[0U];
394   uint32_t vc21 = abcd[1U];
395   uint32_t vd21 = abcd[2U];
396   uint8_t *b21 = x + 40U;
397   uint32_t u20 = load32_le(b21);
398   uint32_t xk20 = u20;
399   uint32_t ti21 = _t[21U];
400   uint32_t
401   v20 =
402     vb21
403     +
404       ((va20 + ((vb21 & vd21) | (vc21 & ~vd21)) + xk20 + ti21)
405       << 9U
406       | (va20 + ((vb21 & vd21) | (vc21 & ~vd21)) + xk20 + ti21) >> 23U);
407   abcd[3U] = v20;
408   uint32_t va21 = abcd[2U];
409   uint32_t vb22 = abcd[3U];
410   uint32_t vc22 = abcd[0U];
411   uint32_t vd22 = abcd[1U];
412   uint8_t *b22 = x + 60U;
413   uint32_t u21 = load32_le(b22);
414   uint32_t xk21 = u21;
415   uint32_t ti22 = _t[22U];
416   uint32_t
417   v21 =
418     vb22
419     +
420       ((va21 + ((vb22 & vd22) | (vc22 & ~vd22)) + xk21 + ti22)
421       << 14U
422       | (va21 + ((vb22 & vd22) | (vc22 & ~vd22)) + xk21 + ti22) >> 18U);
423   abcd[2U] = v21;
424   uint32_t va22 = abcd[1U];
425   uint32_t vb23 = abcd[2U];
426   uint32_t vc23 = abcd[3U];
427   uint32_t vd23 = abcd[0U];
428   uint8_t *b23 = x + 16U;
429   uint32_t u22 = load32_le(b23);
430   uint32_t xk22 = u22;
431   uint32_t ti23 = _t[23U];
432   uint32_t
433   v22 =
434     vb23
435     +
436       ((va22 + ((vb23 & vd23) | (vc23 & ~vd23)) + xk22 + ti23)
437       << 20U
438       | (va22 + ((vb23 & vd23) | (vc23 & ~vd23)) + xk22 + ti23) >> 12U);
439   abcd[1U] = v22;
440   uint32_t va23 = abcd[0U];
441   uint32_t vb24 = abcd[1U];
442   uint32_t vc24 = abcd[2U];
443   uint32_t vd24 = abcd[3U];
444   uint8_t *b24 = x + 36U;
445   uint32_t u23 = load32_le(b24);
446   uint32_t xk23 = u23;
447   uint32_t ti24 = _t[24U];
448   uint32_t
449   v23 =
450     vb24
451     +
452       ((va23 + ((vb24 & vd24) | (vc24 & ~vd24)) + xk23 + ti24)
453       << 5U
454       | (va23 + ((vb24 & vd24) | (vc24 & ~vd24)) + xk23 + ti24) >> 27U);
455   abcd[0U] = v23;
456   uint32_t va24 = abcd[3U];
457   uint32_t vb25 = abcd[0U];
458   uint32_t vc25 = abcd[1U];
459   uint32_t vd25 = abcd[2U];
460   uint8_t *b25 = x + 56U;
461   uint32_t u24 = load32_le(b25);
462   uint32_t xk24 = u24;
463   uint32_t ti25 = _t[25U];
464   uint32_t
465   v24 =
466     vb25
467     +
468       ((va24 + ((vb25 & vd25) | (vc25 & ~vd25)) + xk24 + ti25)
469       << 9U
470       | (va24 + ((vb25 & vd25) | (vc25 & ~vd25)) + xk24 + ti25) >> 23U);
471   abcd[3U] = v24;
472   uint32_t va25 = abcd[2U];
473   uint32_t vb26 = abcd[3U];
474   uint32_t vc26 = abcd[0U];
475   uint32_t vd26 = abcd[1U];
476   uint8_t *b26 = x + 12U;
477   uint32_t u25 = load32_le(b26);
478   uint32_t xk25 = u25;
479   uint32_t ti26 = _t[26U];
480   uint32_t
481   v25 =
482     vb26
483     +
484       ((va25 + ((vb26 & vd26) | (vc26 & ~vd26)) + xk25 + ti26)
485       << 14U
486       | (va25 + ((vb26 & vd26) | (vc26 & ~vd26)) + xk25 + ti26) >> 18U);
487   abcd[2U] = v25;
488   uint32_t va26 = abcd[1U];
489   uint32_t vb27 = abcd[2U];
490   uint32_t vc27 = abcd[3U];
491   uint32_t vd27 = abcd[0U];
492   uint8_t *b27 = x + 32U;
493   uint32_t u26 = load32_le(b27);
494   uint32_t xk26 = u26;
495   uint32_t ti27 = _t[27U];
496   uint32_t
497   v26 =
498     vb27
499     +
500       ((va26 + ((vb27 & vd27) | (vc27 & ~vd27)) + xk26 + ti27)
501       << 20U
502       | (va26 + ((vb27 & vd27) | (vc27 & ~vd27)) + xk26 + ti27) >> 12U);
503   abcd[1U] = v26;
504   uint32_t va27 = abcd[0U];
505   uint32_t vb28 = abcd[1U];
506   uint32_t vc28 = abcd[2U];
507   uint32_t vd28 = abcd[3U];
508   uint8_t *b28 = x + 52U;
509   uint32_t u27 = load32_le(b28);
510   uint32_t xk27 = u27;
511   uint32_t ti28 = _t[28U];
512   uint32_t
513   v27 =
514     vb28
515     +
516       ((va27 + ((vb28 & vd28) | (vc28 & ~vd28)) + xk27 + ti28)
517       << 5U
518       | (va27 + ((vb28 & vd28) | (vc28 & ~vd28)) + xk27 + ti28) >> 27U);
519   abcd[0U] = v27;
520   uint32_t va28 = abcd[3U];
521   uint32_t vb29 = abcd[0U];
522   uint32_t vc29 = abcd[1U];
523   uint32_t vd29 = abcd[2U];
524   uint8_t *b29 = x + 8U;
525   uint32_t u28 = load32_le(b29);
526   uint32_t xk28 = u28;
527   uint32_t ti29 = _t[29U];
528   uint32_t
529   v28 =
530     vb29
531     +
532       ((va28 + ((vb29 & vd29) | (vc29 & ~vd29)) + xk28 + ti29)
533       << 9U
534       | (va28 + ((vb29 & vd29) | (vc29 & ~vd29)) + xk28 + ti29) >> 23U);
535   abcd[3U] = v28;
536   uint32_t va29 = abcd[2U];
537   uint32_t vb30 = abcd[3U];
538   uint32_t vc30 = abcd[0U];
539   uint32_t vd30 = abcd[1U];
540   uint8_t *b30 = x + 28U;
541   uint32_t u29 = load32_le(b30);
542   uint32_t xk29 = u29;
543   uint32_t ti30 = _t[30U];
544   uint32_t
545   v29 =
546     vb30
547     +
548       ((va29 + ((vb30 & vd30) | (vc30 & ~vd30)) + xk29 + ti30)
549       << 14U
550       | (va29 + ((vb30 & vd30) | (vc30 & ~vd30)) + xk29 + ti30) >> 18U);
551   abcd[2U] = v29;
552   uint32_t va30 = abcd[1U];
553   uint32_t vb31 = abcd[2U];
554   uint32_t vc31 = abcd[3U];
555   uint32_t vd31 = abcd[0U];
556   uint8_t *b31 = x + 48U;
557   uint32_t u30 = load32_le(b31);
558   uint32_t xk30 = u30;
559   uint32_t ti31 = _t[31U];
560   uint32_t
561   v30 =
562     vb31
563     +
564       ((va30 + ((vb31 & vd31) | (vc31 & ~vd31)) + xk30 + ti31)
565       << 20U
566       | (va30 + ((vb31 & vd31) | (vc31 & ~vd31)) + xk30 + ti31) >> 12U);
567   abcd[1U] = v30;
568   uint32_t va31 = abcd[0U];
569   uint32_t vb32 = abcd[1U];
570   uint32_t vc32 = abcd[2U];
571   uint32_t vd32 = abcd[3U];
572   uint8_t *b32 = x + 20U;
573   uint32_t u31 = load32_le(b32);
574   uint32_t xk31 = u31;
575   uint32_t ti32 = _t[32U];
576   uint32_t
577   v31 =
578     vb32
579     +
580       ((va31 + (vb32 ^ (vc32 ^ vd32)) + xk31 + ti32)
581       << 4U
582       | (va31 + (vb32 ^ (vc32 ^ vd32)) + xk31 + ti32) >> 28U);
583   abcd[0U] = v31;
584   uint32_t va32 = abcd[3U];
585   uint32_t vb33 = abcd[0U];
586   uint32_t vc33 = abcd[1U];
587   uint32_t vd33 = abcd[2U];
588   uint8_t *b33 = x + 32U;
589   uint32_t u32 = load32_le(b33);
590   uint32_t xk32 = u32;
591   uint32_t ti33 = _t[33U];
592   uint32_t
593   v32 =
594     vb33
595     +
596       ((va32 + (vb33 ^ (vc33 ^ vd33)) + xk32 + ti33)
597       << 11U
598       | (va32 + (vb33 ^ (vc33 ^ vd33)) + xk32 + ti33) >> 21U);
599   abcd[3U] = v32;
600   uint32_t va33 = abcd[2U];
601   uint32_t vb34 = abcd[3U];
602   uint32_t vc34 = abcd[0U];
603   uint32_t vd34 = abcd[1U];
604   uint8_t *b34 = x + 44U;
605   uint32_t u33 = load32_le(b34);
606   uint32_t xk33 = u33;
607   uint32_t ti34 = _t[34U];
608   uint32_t
609   v33 =
610     vb34
611     +
612       ((va33 + (vb34 ^ (vc34 ^ vd34)) + xk33 + ti34)
613       << 16U
614       | (va33 + (vb34 ^ (vc34 ^ vd34)) + xk33 + ti34) >> 16U);
615   abcd[2U] = v33;
616   uint32_t va34 = abcd[1U];
617   uint32_t vb35 = abcd[2U];
618   uint32_t vc35 = abcd[3U];
619   uint32_t vd35 = abcd[0U];
620   uint8_t *b35 = x + 56U;
621   uint32_t u34 = load32_le(b35);
622   uint32_t xk34 = u34;
623   uint32_t ti35 = _t[35U];
624   uint32_t
625   v34 =
626     vb35
627     +
628       ((va34 + (vb35 ^ (vc35 ^ vd35)) + xk34 + ti35)
629       << 23U
630       | (va34 + (vb35 ^ (vc35 ^ vd35)) + xk34 + ti35) >> 9U);
631   abcd[1U] = v34;
632   uint32_t va35 = abcd[0U];
633   uint32_t vb36 = abcd[1U];
634   uint32_t vc36 = abcd[2U];
635   uint32_t vd36 = abcd[3U];
636   uint8_t *b36 = x + 4U;
637   uint32_t u35 = load32_le(b36);
638   uint32_t xk35 = u35;
639   uint32_t ti36 = _t[36U];
640   uint32_t
641   v35 =
642     vb36
643     +
644       ((va35 + (vb36 ^ (vc36 ^ vd36)) + xk35 + ti36)
645       << 4U
646       | (va35 + (vb36 ^ (vc36 ^ vd36)) + xk35 + ti36) >> 28U);
647   abcd[0U] = v35;
648   uint32_t va36 = abcd[3U];
649   uint32_t vb37 = abcd[0U];
650   uint32_t vc37 = abcd[1U];
651   uint32_t vd37 = abcd[2U];
652   uint8_t *b37 = x + 16U;
653   uint32_t u36 = load32_le(b37);
654   uint32_t xk36 = u36;
655   uint32_t ti37 = _t[37U];
656   uint32_t
657   v36 =
658     vb37
659     +
660       ((va36 + (vb37 ^ (vc37 ^ vd37)) + xk36 + ti37)
661       << 11U
662       | (va36 + (vb37 ^ (vc37 ^ vd37)) + xk36 + ti37) >> 21U);
663   abcd[3U] = v36;
664   uint32_t va37 = abcd[2U];
665   uint32_t vb38 = abcd[3U];
666   uint32_t vc38 = abcd[0U];
667   uint32_t vd38 = abcd[1U];
668   uint8_t *b38 = x + 28U;
669   uint32_t u37 = load32_le(b38);
670   uint32_t xk37 = u37;
671   uint32_t ti38 = _t[38U];
672   uint32_t
673   v37 =
674     vb38
675     +
676       ((va37 + (vb38 ^ (vc38 ^ vd38)) + xk37 + ti38)
677       << 16U
678       | (va37 + (vb38 ^ (vc38 ^ vd38)) + xk37 + ti38) >> 16U);
679   abcd[2U] = v37;
680   uint32_t va38 = abcd[1U];
681   uint32_t vb39 = abcd[2U];
682   uint32_t vc39 = abcd[3U];
683   uint32_t vd39 = abcd[0U];
684   uint8_t *b39 = x + 40U;
685   uint32_t u38 = load32_le(b39);
686   uint32_t xk38 = u38;
687   uint32_t ti39 = _t[39U];
688   uint32_t
689   v38 =
690     vb39
691     +
692       ((va38 + (vb39 ^ (vc39 ^ vd39)) + xk38 + ti39)
693       << 23U
694       | (va38 + (vb39 ^ (vc39 ^ vd39)) + xk38 + ti39) >> 9U);
695   abcd[1U] = v38;
696   uint32_t va39 = abcd[0U];
697   uint32_t vb40 = abcd[1U];
698   uint32_t vc40 = abcd[2U];
699   uint32_t vd40 = abcd[3U];
700   uint8_t *b40 = x + 52U;
701   uint32_t u39 = load32_le(b40);
702   uint32_t xk39 = u39;
703   uint32_t ti40 = _t[40U];
704   uint32_t
705   v39 =
706     vb40
707     +
708       ((va39 + (vb40 ^ (vc40 ^ vd40)) + xk39 + ti40)
709       << 4U
710       | (va39 + (vb40 ^ (vc40 ^ vd40)) + xk39 + ti40) >> 28U);
711   abcd[0U] = v39;
712   uint32_t va40 = abcd[3U];
713   uint32_t vb41 = abcd[0U];
714   uint32_t vc41 = abcd[1U];
715   uint32_t vd41 = abcd[2U];
716   uint8_t *b41 = x;
717   uint32_t u40 = load32_le(b41);
718   uint32_t xk40 = u40;
719   uint32_t ti41 = _t[41U];
720   uint32_t
721   v40 =
722     vb41
723     +
724       ((va40 + (vb41 ^ (vc41 ^ vd41)) + xk40 + ti41)
725       << 11U
726       | (va40 + (vb41 ^ (vc41 ^ vd41)) + xk40 + ti41) >> 21U);
727   abcd[3U] = v40;
728   uint32_t va41 = abcd[2U];
729   uint32_t vb42 = abcd[3U];
730   uint32_t vc42 = abcd[0U];
731   uint32_t vd42 = abcd[1U];
732   uint8_t *b42 = x + 12U;
733   uint32_t u41 = load32_le(b42);
734   uint32_t xk41 = u41;
735   uint32_t ti42 = _t[42U];
736   uint32_t
737   v41 =
738     vb42
739     +
740       ((va41 + (vb42 ^ (vc42 ^ vd42)) + xk41 + ti42)
741       << 16U
742       | (va41 + (vb42 ^ (vc42 ^ vd42)) + xk41 + ti42) >> 16U);
743   abcd[2U] = v41;
744   uint32_t va42 = abcd[1U];
745   uint32_t vb43 = abcd[2U];
746   uint32_t vc43 = abcd[3U];
747   uint32_t vd43 = abcd[0U];
748   uint8_t *b43 = x + 24U;
749   uint32_t u42 = load32_le(b43);
750   uint32_t xk42 = u42;
751   uint32_t ti43 = _t[43U];
752   uint32_t
753   v42 =
754     vb43
755     +
756       ((va42 + (vb43 ^ (vc43 ^ vd43)) + xk42 + ti43)
757       << 23U
758       | (va42 + (vb43 ^ (vc43 ^ vd43)) + xk42 + ti43) >> 9U);
759   abcd[1U] = v42;
760   uint32_t va43 = abcd[0U];
761   uint32_t vb44 = abcd[1U];
762   uint32_t vc44 = abcd[2U];
763   uint32_t vd44 = abcd[3U];
764   uint8_t *b44 = x + 36U;
765   uint32_t u43 = load32_le(b44);
766   uint32_t xk43 = u43;
767   uint32_t ti44 = _t[44U];
768   uint32_t
769   v43 =
770     vb44
771     +
772       ((va43 + (vb44 ^ (vc44 ^ vd44)) + xk43 + ti44)
773       << 4U
774       | (va43 + (vb44 ^ (vc44 ^ vd44)) + xk43 + ti44) >> 28U);
775   abcd[0U] = v43;
776   uint32_t va44 = abcd[3U];
777   uint32_t vb45 = abcd[0U];
778   uint32_t vc45 = abcd[1U];
779   uint32_t vd45 = abcd[2U];
780   uint8_t *b45 = x + 48U;
781   uint32_t u44 = load32_le(b45);
782   uint32_t xk44 = u44;
783   uint32_t ti45 = _t[45U];
784   uint32_t
785   v44 =
786     vb45
787     +
788       ((va44 + (vb45 ^ (vc45 ^ vd45)) + xk44 + ti45)
789       << 11U
790       | (va44 + (vb45 ^ (vc45 ^ vd45)) + xk44 + ti45) >> 21U);
791   abcd[3U] = v44;
792   uint32_t va45 = abcd[2U];
793   uint32_t vb46 = abcd[3U];
794   uint32_t vc46 = abcd[0U];
795   uint32_t vd46 = abcd[1U];
796   uint8_t *b46 = x + 60U;
797   uint32_t u45 = load32_le(b46);
798   uint32_t xk45 = u45;
799   uint32_t ti46 = _t[46U];
800   uint32_t
801   v45 =
802     vb46
803     +
804       ((va45 + (vb46 ^ (vc46 ^ vd46)) + xk45 + ti46)
805       << 16U
806       | (va45 + (vb46 ^ (vc46 ^ vd46)) + xk45 + ti46) >> 16U);
807   abcd[2U] = v45;
808   uint32_t va46 = abcd[1U];
809   uint32_t vb47 = abcd[2U];
810   uint32_t vc47 = abcd[3U];
811   uint32_t vd47 = abcd[0U];
812   uint8_t *b47 = x + 8U;
813   uint32_t u46 = load32_le(b47);
814   uint32_t xk46 = u46;
815   uint32_t ti47 = _t[47U];
816   uint32_t
817   v46 =
818     vb47
819     +
820       ((va46 + (vb47 ^ (vc47 ^ vd47)) + xk46 + ti47)
821       << 23U
822       | (va46 + (vb47 ^ (vc47 ^ vd47)) + xk46 + ti47) >> 9U);
823   abcd[1U] = v46;
824   uint32_t va47 = abcd[0U];
825   uint32_t vb48 = abcd[1U];
826   uint32_t vc48 = abcd[2U];
827   uint32_t vd48 = abcd[3U];
828   uint8_t *b48 = x;
829   uint32_t u47 = load32_le(b48);
830   uint32_t xk47 = u47;
831   uint32_t ti48 = _t[48U];
832   uint32_t
833   v47 =
834     vb48
835     +
836       ((va47 + (vc48 ^ (vb48 | ~vd48)) + xk47 + ti48)
837       << 6U
838       | (va47 + (vc48 ^ (vb48 | ~vd48)) + xk47 + ti48) >> 26U);
839   abcd[0U] = v47;
840   uint32_t va48 = abcd[3U];
841   uint32_t vb49 = abcd[0U];
842   uint32_t vc49 = abcd[1U];
843   uint32_t vd49 = abcd[2U];
844   uint8_t *b49 = x + 28U;
845   uint32_t u48 = load32_le(b49);
846   uint32_t xk48 = u48;
847   uint32_t ti49 = _t[49U];
848   uint32_t
849   v48 =
850     vb49
851     +
852       ((va48 + (vc49 ^ (vb49 | ~vd49)) + xk48 + ti49)
853       << 10U
854       | (va48 + (vc49 ^ (vb49 | ~vd49)) + xk48 + ti49) >> 22U);
855   abcd[3U] = v48;
856   uint32_t va49 = abcd[2U];
857   uint32_t vb50 = abcd[3U];
858   uint32_t vc50 = abcd[0U];
859   uint32_t vd50 = abcd[1U];
860   uint8_t *b50 = x + 56U;
861   uint32_t u49 = load32_le(b50);
862   uint32_t xk49 = u49;
863   uint32_t ti50 = _t[50U];
864   uint32_t
865   v49 =
866     vb50
867     +
868       ((va49 + (vc50 ^ (vb50 | ~vd50)) + xk49 + ti50)
869       << 15U
870       | (va49 + (vc50 ^ (vb50 | ~vd50)) + xk49 + ti50) >> 17U);
871   abcd[2U] = v49;
872   uint32_t va50 = abcd[1U];
873   uint32_t vb51 = abcd[2U];
874   uint32_t vc51 = abcd[3U];
875   uint32_t vd51 = abcd[0U];
876   uint8_t *b51 = x + 20U;
877   uint32_t u50 = load32_le(b51);
878   uint32_t xk50 = u50;
879   uint32_t ti51 = _t[51U];
880   uint32_t
881   v50 =
882     vb51
883     +
884       ((va50 + (vc51 ^ (vb51 | ~vd51)) + xk50 + ti51)
885       << 21U
886       | (va50 + (vc51 ^ (vb51 | ~vd51)) + xk50 + ti51) >> 11U);
887   abcd[1U] = v50;
888   uint32_t va51 = abcd[0U];
889   uint32_t vb52 = abcd[1U];
890   uint32_t vc52 = abcd[2U];
891   uint32_t vd52 = abcd[3U];
892   uint8_t *b52 = x + 48U;
893   uint32_t u51 = load32_le(b52);
894   uint32_t xk51 = u51;
895   uint32_t ti52 = _t[52U];
896   uint32_t
897   v51 =
898     vb52
899     +
900       ((va51 + (vc52 ^ (vb52 | ~vd52)) + xk51 + ti52)
901       << 6U
902       | (va51 + (vc52 ^ (vb52 | ~vd52)) + xk51 + ti52) >> 26U);
903   abcd[0U] = v51;
904   uint32_t va52 = abcd[3U];
905   uint32_t vb53 = abcd[0U];
906   uint32_t vc53 = abcd[1U];
907   uint32_t vd53 = abcd[2U];
908   uint8_t *b53 = x + 12U;
909   uint32_t u52 = load32_le(b53);
910   uint32_t xk52 = u52;
911   uint32_t ti53 = _t[53U];
912   uint32_t
913   v52 =
914     vb53
915     +
916       ((va52 + (vc53 ^ (vb53 | ~vd53)) + xk52 + ti53)
917       << 10U
918       | (va52 + (vc53 ^ (vb53 | ~vd53)) + xk52 + ti53) >> 22U);
919   abcd[3U] = v52;
920   uint32_t va53 = abcd[2U];
921   uint32_t vb54 = abcd[3U];
922   uint32_t vc54 = abcd[0U];
923   uint32_t vd54 = abcd[1U];
924   uint8_t *b54 = x + 40U;
925   uint32_t u53 = load32_le(b54);
926   uint32_t xk53 = u53;
927   uint32_t ti54 = _t[54U];
928   uint32_t
929   v53 =
930     vb54
931     +
932       ((va53 + (vc54 ^ (vb54 | ~vd54)) + xk53 + ti54)
933       << 15U
934       | (va53 + (vc54 ^ (vb54 | ~vd54)) + xk53 + ti54) >> 17U);
935   abcd[2U] = v53;
936   uint32_t va54 = abcd[1U];
937   uint32_t vb55 = abcd[2U];
938   uint32_t vc55 = abcd[3U];
939   uint32_t vd55 = abcd[0U];
940   uint8_t *b55 = x + 4U;
941   uint32_t u54 = load32_le(b55);
942   uint32_t xk54 = u54;
943   uint32_t ti55 = _t[55U];
944   uint32_t
945   v54 =
946     vb55
947     +
948       ((va54 + (vc55 ^ (vb55 | ~vd55)) + xk54 + ti55)
949       << 21U
950       | (va54 + (vc55 ^ (vb55 | ~vd55)) + xk54 + ti55) >> 11U);
951   abcd[1U] = v54;
952   uint32_t va55 = abcd[0U];
953   uint32_t vb56 = abcd[1U];
954   uint32_t vc56 = abcd[2U];
955   uint32_t vd56 = abcd[3U];
956   uint8_t *b56 = x + 32U;
957   uint32_t u55 = load32_le(b56);
958   uint32_t xk55 = u55;
959   uint32_t ti56 = _t[56U];
960   uint32_t
961   v55 =
962     vb56
963     +
964       ((va55 + (vc56 ^ (vb56 | ~vd56)) + xk55 + ti56)
965       << 6U
966       | (va55 + (vc56 ^ (vb56 | ~vd56)) + xk55 + ti56) >> 26U);
967   abcd[0U] = v55;
968   uint32_t va56 = abcd[3U];
969   uint32_t vb57 = abcd[0U];
970   uint32_t vc57 = abcd[1U];
971   uint32_t vd57 = abcd[2U];
972   uint8_t *b57 = x + 60U;
973   uint32_t u56 = load32_le(b57);
974   uint32_t xk56 = u56;
975   uint32_t ti57 = _t[57U];
976   uint32_t
977   v56 =
978     vb57
979     +
980       ((va56 + (vc57 ^ (vb57 | ~vd57)) + xk56 + ti57)
981       << 10U
982       | (va56 + (vc57 ^ (vb57 | ~vd57)) + xk56 + ti57) >> 22U);
983   abcd[3U] = v56;
984   uint32_t va57 = abcd[2U];
985   uint32_t vb58 = abcd[3U];
986   uint32_t vc58 = abcd[0U];
987   uint32_t vd58 = abcd[1U];
988   uint8_t *b58 = x + 24U;
989   uint32_t u57 = load32_le(b58);
990   uint32_t xk57 = u57;
991   uint32_t ti58 = _t[58U];
992   uint32_t
993   v57 =
994     vb58
995     +
996       ((va57 + (vc58 ^ (vb58 | ~vd58)) + xk57 + ti58)
997       << 15U
998       | (va57 + (vc58 ^ (vb58 | ~vd58)) + xk57 + ti58) >> 17U);
999   abcd[2U] = v57;
1000   uint32_t va58 = abcd[1U];
1001   uint32_t vb59 = abcd[2U];
1002   uint32_t vc59 = abcd[3U];
1003   uint32_t vd59 = abcd[0U];
1004   uint8_t *b59 = x + 52U;
1005   uint32_t u58 = load32_le(b59);
1006   uint32_t xk58 = u58;
1007   uint32_t ti59 = _t[59U];
1008   uint32_t
1009   v58 =
1010     vb59
1011     +
1012       ((va58 + (vc59 ^ (vb59 | ~vd59)) + xk58 + ti59)
1013       << 21U
1014       | (va58 + (vc59 ^ (vb59 | ~vd59)) + xk58 + ti59) >> 11U);
1015   abcd[1U] = v58;
1016   uint32_t va59 = abcd[0U];
1017   uint32_t vb60 = abcd[1U];
1018   uint32_t vc60 = abcd[2U];
1019   uint32_t vd60 = abcd[3U];
1020   uint8_t *b60 = x + 16U;
1021   uint32_t u59 = load32_le(b60);
1022   uint32_t xk59 = u59;
1023   uint32_t ti60 = _t[60U];
1024   uint32_t
1025   v59 =
1026     vb60
1027     +
1028       ((va59 + (vc60 ^ (vb60 | ~vd60)) + xk59 + ti60)
1029       << 6U
1030       | (va59 + (vc60 ^ (vb60 | ~vd60)) + xk59 + ti60) >> 26U);
1031   abcd[0U] = v59;
1032   uint32_t va60 = abcd[3U];
1033   uint32_t vb61 = abcd[0U];
1034   uint32_t vc61 = abcd[1U];
1035   uint32_t vd61 = abcd[2U];
1036   uint8_t *b61 = x + 44U;
1037   uint32_t u60 = load32_le(b61);
1038   uint32_t xk60 = u60;
1039   uint32_t ti61 = _t[61U];
1040   uint32_t
1041   v60 =
1042     vb61
1043     +
1044       ((va60 + (vc61 ^ (vb61 | ~vd61)) + xk60 + ti61)
1045       << 10U
1046       | (va60 + (vc61 ^ (vb61 | ~vd61)) + xk60 + ti61) >> 22U);
1047   abcd[3U] = v60;
1048   uint32_t va61 = abcd[2U];
1049   uint32_t vb62 = abcd[3U];
1050   uint32_t vc62 = abcd[0U];
1051   uint32_t vd62 = abcd[1U];
1052   uint8_t *b62 = x + 8U;
1053   uint32_t u61 = load32_le(b62);
1054   uint32_t xk61 = u61;
1055   uint32_t ti62 = _t[62U];
1056   uint32_t
1057   v61 =
1058     vb62
1059     +
1060       ((va61 + (vc62 ^ (vb62 | ~vd62)) + xk61 + ti62)
1061       << 15U
1062       | (va61 + (vc62 ^ (vb62 | ~vd62)) + xk61 + ti62) >> 17U);
1063   abcd[2U] = v61;
1064   uint32_t va62 = abcd[1U];
1065   uint32_t vb = abcd[2U];
1066   uint32_t vc = abcd[3U];
1067   uint32_t vd = abcd[0U];
1068   uint8_t *b63 = x + 36U;
1069   uint32_t u62 = load32_le(b63);
1070   uint32_t xk62 = u62;
1071   uint32_t ti = _t[63U];
1072   uint32_t
1073   v62 =
1074     vb
1075     +
1076       ((va62 + (vc ^ (vb | ~vd)) + xk62 + ti)
1077       << 21U
1078       | (va62 + (vc ^ (vb | ~vd)) + xk62 + ti) >> 11U);
1079   abcd[1U] = v62;
1080   uint32_t a = abcd[0U];
1081   uint32_t b = abcd[1U];
1082   uint32_t c = abcd[2U];
1083   uint32_t d = abcd[3U];
1084   abcd[0U] = a + aa;
1085   abcd[1U] = b + bb;
1086   abcd[2U] = c + cc;
1087   abcd[3U] = d + dd;
1088 }
1089 
pad(uint64_t len,uint8_t * dst)1090 static void pad(uint64_t len, uint8_t *dst)
1091 {
1092   uint8_t *dst1 = dst;
1093   dst1[0U] = 0x80U;
1094   uint8_t *dst2 = dst + 1U;
1095   for (uint32_t i = 0U; i < (128U - (9U + (uint32_t)(len % (uint64_t)64U))) % 64U; i++)
1096   {
1097     dst2[i] = 0U;
1098   }
1099   uint8_t *dst3 = dst + 1U + (128U - (9U + (uint32_t)(len % (uint64_t)64U))) % 64U;
1100   store64_le(dst3, len << 3U);
1101 }
1102 
Hacl_Hash_MD5_finish(uint32_t * s,uint8_t * dst)1103 void Hacl_Hash_MD5_finish(uint32_t *s, uint8_t *dst)
1104 {
1105   KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store32_le(dst + i * 4U, s[i]););
1106 }
1107 
Hacl_Hash_MD5_update_multi(uint32_t * s,uint8_t * blocks,uint32_t n_blocks)1108 void Hacl_Hash_MD5_update_multi(uint32_t *s, uint8_t *blocks, uint32_t n_blocks)
1109 {
1110   for (uint32_t i = 0U; i < n_blocks; i++)
1111   {
1112     uint32_t sz = 64U;
1113     uint8_t *block = blocks + sz * i;
1114     update(s, block);
1115   }
1116 }
1117 
1118 void
Hacl_Hash_MD5_update_last(uint32_t * s,uint64_t prev_len,uint8_t * input,uint32_t input_len)1119 Hacl_Hash_MD5_update_last(uint32_t *s, uint64_t prev_len, uint8_t *input, uint32_t input_len)
1120 {
1121   uint32_t blocks_n = input_len / 64U;
1122   uint32_t blocks_len = blocks_n * 64U;
1123   uint8_t *blocks = input;
1124   uint32_t rest_len = input_len - blocks_len;
1125   uint8_t *rest = input + blocks_len;
1126   Hacl_Hash_MD5_update_multi(s, blocks, blocks_n);
1127   uint64_t total_input_len = prev_len + (uint64_t)input_len;
1128   uint32_t pad_len = 1U + (128U - (9U + (uint32_t)(total_input_len % (uint64_t)64U))) % 64U + 8U;
1129   uint32_t tmp_len = rest_len + pad_len;
1130   uint8_t tmp_twoblocks[128U] = { 0U };
1131   uint8_t *tmp = tmp_twoblocks;
1132   uint8_t *tmp_rest = tmp;
1133   uint8_t *tmp_pad = tmp + rest_len;
1134   memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t));
1135   pad(total_input_len, tmp_pad);
1136   Hacl_Hash_MD5_update_multi(s, tmp, tmp_len / 64U);
1137 }
1138 
Hacl_Hash_MD5_hash_oneshot(uint8_t * output,uint8_t * input,uint32_t input_len)1139 void Hacl_Hash_MD5_hash_oneshot(uint8_t *output, uint8_t *input, uint32_t input_len)
1140 {
1141   uint32_t s[4U] = { 0x67452301U, 0xefcdab89U, 0x98badcfeU, 0x10325476U };
1142   uint32_t blocks_n0 = input_len / 64U;
1143   uint32_t blocks_n1;
1144   if (input_len % 64U == 0U && blocks_n0 > 0U)
1145   {
1146     blocks_n1 = blocks_n0 - 1U;
1147   }
1148   else
1149   {
1150     blocks_n1 = blocks_n0;
1151   }
1152   uint32_t blocks_len0 = blocks_n1 * 64U;
1153   uint8_t *blocks0 = input;
1154   uint32_t rest_len0 = input_len - blocks_len0;
1155   uint8_t *rest0 = input + blocks_len0;
1156   uint32_t blocks_n = blocks_n1;
1157   uint32_t blocks_len = blocks_len0;
1158   uint8_t *blocks = blocks0;
1159   uint32_t rest_len = rest_len0;
1160   uint8_t *rest = rest0;
1161   Hacl_Hash_MD5_update_multi(s, blocks, blocks_n);
1162   Hacl_Hash_MD5_update_last(s, (uint64_t)blocks_len, rest, rest_len);
1163   Hacl_Hash_MD5_finish(s, output);
1164 }
1165 
Hacl_Hash_MD5_malloc(void)1166 Hacl_Streaming_MD_state_32 *Hacl_Hash_MD5_malloc(void)
1167 {
1168   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
1169   uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t));
1170   Hacl_Streaming_MD_state_32
1171   s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
1172   Hacl_Streaming_MD_state_32
1173   *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
1174   p[0U] = s;
1175   Hacl_Hash_MD5_init(block_state);
1176   return p;
1177 }
1178 
Hacl_Hash_MD5_reset(Hacl_Streaming_MD_state_32 * state)1179 void Hacl_Hash_MD5_reset(Hacl_Streaming_MD_state_32 *state)
1180 {
1181   Hacl_Streaming_MD_state_32 scrut = *state;
1182   uint8_t *buf = scrut.buf;
1183   uint32_t *block_state = scrut.block_state;
1184   Hacl_Hash_MD5_init(block_state);
1185   Hacl_Streaming_MD_state_32
1186   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
1187   state[0U] = tmp;
1188 }
1189 
1190 /**
1191 0 = success, 1 = max length exceeded
1192 */
1193 Hacl_Streaming_Types_error_code
Hacl_Hash_MD5_update(Hacl_Streaming_MD_state_32 * state,uint8_t * chunk,uint32_t chunk_len)1194 Hacl_Hash_MD5_update(Hacl_Streaming_MD_state_32 *state, uint8_t *chunk, uint32_t chunk_len)
1195 {
1196   Hacl_Streaming_MD_state_32 s = *state;
1197   uint64_t total_len = s.total_len;
1198   if ((uint64_t)chunk_len > 2305843009213693951ULL - total_len)
1199   {
1200     return Hacl_Streaming_Types_MaximumLengthExceeded;
1201   }
1202   uint32_t sz;
1203   if (total_len % (uint64_t)64U == 0ULL && total_len > 0ULL)
1204   {
1205     sz = 64U;
1206   }
1207   else
1208   {
1209     sz = (uint32_t)(total_len % (uint64_t)64U);
1210   }
1211   if (chunk_len <= 64U - sz)
1212   {
1213     Hacl_Streaming_MD_state_32 s1 = *state;
1214     uint32_t *block_state1 = s1.block_state;
1215     uint8_t *buf = s1.buf;
1216     uint64_t total_len1 = s1.total_len;
1217     uint32_t sz1;
1218     if (total_len1 % (uint64_t)64U == 0ULL && total_len1 > 0ULL)
1219     {
1220       sz1 = 64U;
1221     }
1222     else
1223     {
1224       sz1 = (uint32_t)(total_len1 % (uint64_t)64U);
1225     }
1226     uint8_t *buf2 = buf + sz1;
1227     memcpy(buf2, chunk, chunk_len * sizeof (uint8_t));
1228     uint64_t total_len2 = total_len1 + (uint64_t)chunk_len;
1229     *state
1230     =
1231       (
1232         (Hacl_Streaming_MD_state_32){
1233           .block_state = block_state1,
1234           .buf = buf,
1235           .total_len = total_len2
1236         }
1237       );
1238   }
1239   else if (sz == 0U)
1240   {
1241     Hacl_Streaming_MD_state_32 s1 = *state;
1242     uint32_t *block_state1 = s1.block_state;
1243     uint8_t *buf = s1.buf;
1244     uint64_t total_len1 = s1.total_len;
1245     uint32_t sz1;
1246     if (total_len1 % (uint64_t)64U == 0ULL && total_len1 > 0ULL)
1247     {
1248       sz1 = 64U;
1249     }
1250     else
1251     {
1252       sz1 = (uint32_t)(total_len1 % (uint64_t)64U);
1253     }
1254     if (!(sz1 == 0U))
1255     {
1256       Hacl_Hash_MD5_update_multi(block_state1, buf, 1U);
1257     }
1258     uint32_t ite;
1259     if ((uint64_t)chunk_len % (uint64_t)64U == 0ULL && (uint64_t)chunk_len > 0ULL)
1260     {
1261       ite = 64U;
1262     }
1263     else
1264     {
1265       ite = (uint32_t)((uint64_t)chunk_len % (uint64_t)64U);
1266     }
1267     uint32_t n_blocks = (chunk_len - ite) / 64U;
1268     uint32_t data1_len = n_blocks * 64U;
1269     uint32_t data2_len = chunk_len - data1_len;
1270     uint8_t *data1 = chunk;
1271     uint8_t *data2 = chunk + data1_len;
1272     Hacl_Hash_MD5_update_multi(block_state1, data1, data1_len / 64U);
1273     uint8_t *dst = buf;
1274     memcpy(dst, data2, data2_len * sizeof (uint8_t));
1275     *state
1276     =
1277       (
1278         (Hacl_Streaming_MD_state_32){
1279           .block_state = block_state1,
1280           .buf = buf,
1281           .total_len = total_len1 + (uint64_t)chunk_len
1282         }
1283       );
1284   }
1285   else
1286   {
1287     uint32_t diff = 64U - sz;
1288     uint8_t *chunk1 = chunk;
1289     uint8_t *chunk2 = chunk + diff;
1290     Hacl_Streaming_MD_state_32 s1 = *state;
1291     uint32_t *block_state10 = s1.block_state;
1292     uint8_t *buf0 = s1.buf;
1293     uint64_t total_len10 = s1.total_len;
1294     uint32_t sz10;
1295     if (total_len10 % (uint64_t)64U == 0ULL && total_len10 > 0ULL)
1296     {
1297       sz10 = 64U;
1298     }
1299     else
1300     {
1301       sz10 = (uint32_t)(total_len10 % (uint64_t)64U);
1302     }
1303     uint8_t *buf2 = buf0 + sz10;
1304     memcpy(buf2, chunk1, diff * sizeof (uint8_t));
1305     uint64_t total_len2 = total_len10 + (uint64_t)diff;
1306     *state
1307     =
1308       (
1309         (Hacl_Streaming_MD_state_32){
1310           .block_state = block_state10,
1311           .buf = buf0,
1312           .total_len = total_len2
1313         }
1314       );
1315     Hacl_Streaming_MD_state_32 s10 = *state;
1316     uint32_t *block_state1 = s10.block_state;
1317     uint8_t *buf = s10.buf;
1318     uint64_t total_len1 = s10.total_len;
1319     uint32_t sz1;
1320     if (total_len1 % (uint64_t)64U == 0ULL && total_len1 > 0ULL)
1321     {
1322       sz1 = 64U;
1323     }
1324     else
1325     {
1326       sz1 = (uint32_t)(total_len1 % (uint64_t)64U);
1327     }
1328     if (!(sz1 == 0U))
1329     {
1330       Hacl_Hash_MD5_update_multi(block_state1, buf, 1U);
1331     }
1332     uint32_t ite;
1333     if
1334     ((uint64_t)(chunk_len - diff) % (uint64_t)64U == 0ULL && (uint64_t)(chunk_len - diff) > 0ULL)
1335     {
1336       ite = 64U;
1337     }
1338     else
1339     {
1340       ite = (uint32_t)((uint64_t)(chunk_len - diff) % (uint64_t)64U);
1341     }
1342     uint32_t n_blocks = (chunk_len - diff - ite) / 64U;
1343     uint32_t data1_len = n_blocks * 64U;
1344     uint32_t data2_len = chunk_len - diff - data1_len;
1345     uint8_t *data1 = chunk2;
1346     uint8_t *data2 = chunk2 + data1_len;
1347     Hacl_Hash_MD5_update_multi(block_state1, data1, data1_len / 64U);
1348     uint8_t *dst = buf;
1349     memcpy(dst, data2, data2_len * sizeof (uint8_t));
1350     *state
1351     =
1352       (
1353         (Hacl_Streaming_MD_state_32){
1354           .block_state = block_state1,
1355           .buf = buf,
1356           .total_len = total_len1 + (uint64_t)(chunk_len - diff)
1357         }
1358       );
1359   }
1360   return Hacl_Streaming_Types_Success;
1361 }
1362 
Hacl_Hash_MD5_digest(Hacl_Streaming_MD_state_32 * state,uint8_t * output)1363 void Hacl_Hash_MD5_digest(Hacl_Streaming_MD_state_32 *state, uint8_t *output)
1364 {
1365   Hacl_Streaming_MD_state_32 scrut = *state;
1366   uint32_t *block_state = scrut.block_state;
1367   uint8_t *buf_ = scrut.buf;
1368   uint64_t total_len = scrut.total_len;
1369   uint32_t r;
1370   if (total_len % (uint64_t)64U == 0ULL && total_len > 0ULL)
1371   {
1372     r = 64U;
1373   }
1374   else
1375   {
1376     r = (uint32_t)(total_len % (uint64_t)64U);
1377   }
1378   uint8_t *buf_1 = buf_;
1379   uint32_t tmp_block_state[4U] = { 0U };
1380   memcpy(tmp_block_state, block_state, 4U * sizeof (uint32_t));
1381   uint32_t ite;
1382   if (r % 64U == 0U && r > 0U)
1383   {
1384     ite = 64U;
1385   }
1386   else
1387   {
1388     ite = r % 64U;
1389   }
1390   uint8_t *buf_last = buf_1 + r - ite;
1391   uint8_t *buf_multi = buf_1;
1392   Hacl_Hash_MD5_update_multi(tmp_block_state, buf_multi, 0U);
1393   uint64_t prev_len_last = total_len - (uint64_t)r;
1394   Hacl_Hash_MD5_update_last(tmp_block_state, prev_len_last, buf_last, r);
1395   Hacl_Hash_MD5_finish(tmp_block_state, output);
1396 }
1397 
Hacl_Hash_MD5_free(Hacl_Streaming_MD_state_32 * state)1398 void Hacl_Hash_MD5_free(Hacl_Streaming_MD_state_32 *state)
1399 {
1400   Hacl_Streaming_MD_state_32 scrut = *state;
1401   uint8_t *buf = scrut.buf;
1402   uint32_t *block_state = scrut.block_state;
1403   KRML_HOST_FREE(block_state);
1404   KRML_HOST_FREE(buf);
1405   KRML_HOST_FREE(state);
1406 }
1407 
Hacl_Hash_MD5_copy(Hacl_Streaming_MD_state_32 * state)1408 Hacl_Streaming_MD_state_32 *Hacl_Hash_MD5_copy(Hacl_Streaming_MD_state_32 *state)
1409 {
1410   Hacl_Streaming_MD_state_32 scrut = *state;
1411   uint32_t *block_state0 = scrut.block_state;
1412   uint8_t *buf0 = scrut.buf;
1413   uint64_t total_len0 = scrut.total_len;
1414   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
1415   memcpy(buf, buf0, 64U * sizeof (uint8_t));
1416   uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t));
1417   memcpy(block_state, block_state0, 4U * sizeof (uint32_t));
1418   Hacl_Streaming_MD_state_32
1419   s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
1420   Hacl_Streaming_MD_state_32
1421   *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
1422   p[0U] = s;
1423   return p;
1424 }
1425 
Hacl_Hash_MD5_hash(uint8_t * output,uint8_t * input,uint32_t input_len)1426 void Hacl_Hash_MD5_hash(uint8_t *output, uint8_t *input, uint32_t input_len)
1427 {
1428   Hacl_Hash_MD5_hash_oneshot(output, input, input_len);
1429 }
1430 
1431