Branch data Line data Source code
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 "Hacl_Streaming_SHA2.h"
27 : :
28 : : #include "internal/Hacl_SHA2_Generic.h"
29 : :
30 : :
31 : 0 : static inline void sha256_init(uint32_t *hash)
32 : : {
33 : 0 : KRML_MAYBE_FOR8(i,
34 : : (uint32_t)0U,
35 : : (uint32_t)8U,
36 : : (uint32_t)1U,
37 : : uint32_t *os = hash;
38 : : uint32_t x = Hacl_Impl_SHA2_Generic_h256[i];
39 : : os[i] = x;);
40 : 0 : }
41 : :
42 : 0 : static inline void sha256_update0(uint8_t *b, uint32_t *hash)
43 : : {
44 : 0 : uint32_t hash_old[8U] = { 0U };
45 : 0 : uint32_t ws[16U] = { 0U };
46 : 0 : memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint32_t));
47 : 0 : uint8_t *b10 = b;
48 : 0 : uint32_t u = load32_be(b10);
49 : 0 : ws[0U] = u;
50 : 0 : uint32_t u0 = load32_be(b10 + (uint32_t)4U);
51 : 0 : ws[1U] = u0;
52 : 0 : uint32_t u1 = load32_be(b10 + (uint32_t)8U);
53 : 0 : ws[2U] = u1;
54 : 0 : uint32_t u2 = load32_be(b10 + (uint32_t)12U);
55 : 0 : ws[3U] = u2;
56 : 0 : uint32_t u3 = load32_be(b10 + (uint32_t)16U);
57 : 0 : ws[4U] = u3;
58 : 0 : uint32_t u4 = load32_be(b10 + (uint32_t)20U);
59 : 0 : ws[5U] = u4;
60 : 0 : uint32_t u5 = load32_be(b10 + (uint32_t)24U);
61 : 0 : ws[6U] = u5;
62 : 0 : uint32_t u6 = load32_be(b10 + (uint32_t)28U);
63 : 0 : ws[7U] = u6;
64 : 0 : uint32_t u7 = load32_be(b10 + (uint32_t)32U);
65 : 0 : ws[8U] = u7;
66 : 0 : uint32_t u8 = load32_be(b10 + (uint32_t)36U);
67 : 0 : ws[9U] = u8;
68 : 0 : uint32_t u9 = load32_be(b10 + (uint32_t)40U);
69 : 0 : ws[10U] = u9;
70 : 0 : uint32_t u10 = load32_be(b10 + (uint32_t)44U);
71 : 0 : ws[11U] = u10;
72 : 0 : uint32_t u11 = load32_be(b10 + (uint32_t)48U);
73 : 0 : ws[12U] = u11;
74 : 0 : uint32_t u12 = load32_be(b10 + (uint32_t)52U);
75 : 0 : ws[13U] = u12;
76 : 0 : uint32_t u13 = load32_be(b10 + (uint32_t)56U);
77 : 0 : ws[14U] = u13;
78 : 0 : uint32_t u14 = load32_be(b10 + (uint32_t)60U);
79 : 0 : ws[15U] = u14;
80 [ # # # # : 0 : KRML_MAYBE_FOR4(i0,
# # # # ]
81 : : (uint32_t)0U,
82 : : (uint32_t)4U,
83 : : (uint32_t)1U,
84 : : KRML_MAYBE_FOR16(i,
85 : : (uint32_t)0U,
86 : : (uint32_t)16U,
87 : : (uint32_t)1U,
88 : : uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256[(uint32_t)16U * i0 + i];
89 : : uint32_t ws_t = ws[i];
90 : : uint32_t a0 = hash[0U];
91 : : uint32_t b0 = hash[1U];
92 : : uint32_t c0 = hash[2U];
93 : : uint32_t d0 = hash[3U];
94 : : uint32_t e0 = hash[4U];
95 : : uint32_t f0 = hash[5U];
96 : : uint32_t g0 = hash[6U];
97 : : uint32_t h02 = hash[7U];
98 : : uint32_t k_e_t = k_t;
99 : : uint32_t
100 : : t1 =
101 : : h02
102 : : +
103 : : ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U)
104 : : ^
105 : : ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U)
106 : : ^ (e0 << (uint32_t)7U | e0 >> (uint32_t)25U)))
107 : : + ((e0 & f0) ^ (~e0 & g0))
108 : : + k_e_t
109 : : + ws_t;
110 : : uint32_t
111 : : t2 =
112 : : ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U)
113 : : ^
114 : : ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U)
115 : : ^ (a0 << (uint32_t)10U | a0 >> (uint32_t)22U)))
116 : : + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0)));
117 : : uint32_t a1 = t1 + t2;
118 : : uint32_t b1 = a0;
119 : : uint32_t c1 = b0;
120 : : uint32_t d1 = c0;
121 : : uint32_t e1 = d0 + t1;
122 : : uint32_t f1 = e0;
123 : : uint32_t g1 = f0;
124 : : uint32_t h12 = g0;
125 : : hash[0U] = a1;
126 : : hash[1U] = b1;
127 : : hash[2U] = c1;
128 : : hash[3U] = d1;
129 : : hash[4U] = e1;
130 : : hash[5U] = f1;
131 : : hash[6U] = g1;
132 : : hash[7U] = h12;);
133 : : if (i0 < (uint32_t)3U)
134 : : {
135 : : KRML_MAYBE_FOR16(i,
136 : : (uint32_t)0U,
137 : : (uint32_t)16U,
138 : : (uint32_t)1U,
139 : : uint32_t t16 = ws[i];
140 : : uint32_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U];
141 : : uint32_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U];
142 : : uint32_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U];
143 : : uint32_t
144 : : s1 =
145 : : (t2 << (uint32_t)15U | t2 >> (uint32_t)17U)
146 : : ^ ((t2 << (uint32_t)13U | t2 >> (uint32_t)19U) ^ t2 >> (uint32_t)10U);
147 : : uint32_t
148 : : s0 =
149 : : (t15 << (uint32_t)25U | t15 >> (uint32_t)7U)
150 : : ^ ((t15 << (uint32_t)14U | t15 >> (uint32_t)18U) ^ t15 >> (uint32_t)3U);
151 : : ws[i] = s1 + t7 + s0 + t16;);
152 : : });
153 : 0 : KRML_MAYBE_FOR8(i,
154 : : (uint32_t)0U,
155 : : (uint32_t)8U,
156 : : (uint32_t)1U,
157 : : uint32_t *os = hash;
158 : : uint32_t x = hash[i] + hash_old[i];
159 : : os[i] = x;);
160 : 0 : }
161 : :
162 : 0 : static inline void sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st)
163 : : {
164 : 0 : uint32_t blocks = len / (uint32_t)64U;
165 [ # # ]: 0 : for (uint32_t i = (uint32_t)0U; i < blocks; i++)
166 : : {
167 : 0 : uint8_t *b0 = b;
168 : 0 : uint8_t *mb = b0 + i * (uint32_t)64U;
169 : 0 : sha256_update0(mb, st);
170 : : }
171 : 0 : }
172 : :
173 : : static inline void
174 : 0 : sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash)
175 : : {
176 : : uint32_t blocks;
177 [ # # ]: 0 : if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U)
178 : : {
179 : 0 : blocks = (uint32_t)1U;
180 : : }
181 : : else
182 : : {
183 : 0 : blocks = (uint32_t)2U;
184 : : }
185 : 0 : uint32_t fin = blocks * (uint32_t)64U;
186 : 0 : uint8_t last[128U] = { 0U };
187 : 0 : uint8_t totlen_buf[8U] = { 0U };
188 : 0 : uint64_t total_len_bits = totlen << (uint32_t)3U;
189 : 0 : store64_be(totlen_buf, total_len_bits);
190 : 0 : uint8_t *b0 = b;
191 : 0 : memcpy(last, b0, len * sizeof (uint8_t));
192 : 0 : last[len] = (uint8_t)0x80U;
193 : 0 : memcpy(last + fin - (uint32_t)8U, totlen_buf, (uint32_t)8U * sizeof (uint8_t));
194 : 0 : uint8_t *last00 = last;
195 : 0 : uint8_t *last10 = last + (uint32_t)64U;
196 : 0 : uint8_t *l0 = last00;
197 : 0 : uint8_t *l1 = last10;
198 : 0 : uint8_t *lb0 = l0;
199 : 0 : uint8_t *lb1 = l1;
200 : 0 : uint8_t *last0 = lb0;
201 : 0 : uint8_t *last1 = lb1;
202 : 0 : sha256_update0(last0, hash);
203 [ # # ]: 0 : if (blocks > (uint32_t)1U)
204 : : {
205 : 0 : sha256_update0(last1, hash);
206 : 0 : return;
207 : : }
208 : : }
209 : :
210 : 0 : static inline void sha256_finish(uint32_t *st, uint8_t *h)
211 : : {
212 : 0 : uint8_t hbuf[32U] = { 0U };
213 : 0 : KRML_MAYBE_FOR8(i,
214 : : (uint32_t)0U,
215 : : (uint32_t)8U,
216 : : (uint32_t)1U,
217 : : store32_be(hbuf + i * (uint32_t)4U, st[i]););
218 : 0 : memcpy(h, hbuf, (uint32_t)32U * sizeof (uint8_t));
219 : 0 : }
220 : :
221 : 0 : static inline void sha224_init(uint32_t *hash)
222 : : {
223 : 0 : KRML_MAYBE_FOR8(i,
224 : : (uint32_t)0U,
225 : : (uint32_t)8U,
226 : : (uint32_t)1U,
227 : : uint32_t *os = hash;
228 : : uint32_t x = Hacl_Impl_SHA2_Generic_h224[i];
229 : : os[i] = x;);
230 : 0 : }
231 : :
232 : 0 : static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st)
233 : : {
234 : 0 : sha256_update_nblocks(len, b, st);
235 : 0 : }
236 : :
237 : 0 : static void sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st)
238 : : {
239 : 0 : sha256_update_last(totlen, len, b, st);
240 : 0 : }
241 : :
242 : 0 : static inline void sha224_finish(uint32_t *st, uint8_t *h)
243 : : {
244 : 0 : uint8_t hbuf[32U] = { 0U };
245 : 0 : KRML_MAYBE_FOR8(i,
246 : : (uint32_t)0U,
247 : : (uint32_t)8U,
248 : : (uint32_t)1U,
249 : : store32_be(hbuf + i * (uint32_t)4U, st[i]););
250 : 0 : memcpy(h, hbuf, (uint32_t)28U * sizeof (uint8_t));
251 : 0 : }
252 : :
253 : 0 : void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash)
254 : : {
255 : 0 : KRML_MAYBE_FOR8(i,
256 : : (uint32_t)0U,
257 : : (uint32_t)8U,
258 : : (uint32_t)1U,
259 : : uint64_t *os = hash;
260 : : uint64_t x = Hacl_Impl_SHA2_Generic_h512[i];
261 : : os[i] = x;);
262 : 0 : }
263 : :
264 : 0 : static inline void sha512_update(uint8_t *b, uint64_t *hash)
265 : : {
266 : 0 : uint64_t hash_old[8U] = { 0U };
267 : 0 : uint64_t ws[16U] = { 0U };
268 : 0 : memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint64_t));
269 : 0 : uint8_t *b10 = b;
270 : 0 : uint64_t u = load64_be(b10);
271 : 0 : ws[0U] = u;
272 : 0 : uint64_t u0 = load64_be(b10 + (uint32_t)8U);
273 : 0 : ws[1U] = u0;
274 : 0 : uint64_t u1 = load64_be(b10 + (uint32_t)16U);
275 : 0 : ws[2U] = u1;
276 : 0 : uint64_t u2 = load64_be(b10 + (uint32_t)24U);
277 : 0 : ws[3U] = u2;
278 : 0 : uint64_t u3 = load64_be(b10 + (uint32_t)32U);
279 : 0 : ws[4U] = u3;
280 : 0 : uint64_t u4 = load64_be(b10 + (uint32_t)40U);
281 : 0 : ws[5U] = u4;
282 : 0 : uint64_t u5 = load64_be(b10 + (uint32_t)48U);
283 : 0 : ws[6U] = u5;
284 : 0 : uint64_t u6 = load64_be(b10 + (uint32_t)56U);
285 : 0 : ws[7U] = u6;
286 : 0 : uint64_t u7 = load64_be(b10 + (uint32_t)64U);
287 : 0 : ws[8U] = u7;
288 : 0 : uint64_t u8 = load64_be(b10 + (uint32_t)72U);
289 : 0 : ws[9U] = u8;
290 : 0 : uint64_t u9 = load64_be(b10 + (uint32_t)80U);
291 : 0 : ws[10U] = u9;
292 : 0 : uint64_t u10 = load64_be(b10 + (uint32_t)88U);
293 : 0 : ws[11U] = u10;
294 : 0 : uint64_t u11 = load64_be(b10 + (uint32_t)96U);
295 : 0 : ws[12U] = u11;
296 : 0 : uint64_t u12 = load64_be(b10 + (uint32_t)104U);
297 : 0 : ws[13U] = u12;
298 : 0 : uint64_t u13 = load64_be(b10 + (uint32_t)112U);
299 : 0 : ws[14U] = u13;
300 : 0 : uint64_t u14 = load64_be(b10 + (uint32_t)120U);
301 : 0 : ws[15U] = u14;
302 [ # # # # : 0 : KRML_MAYBE_FOR5(i0,
# # # # #
# ]
303 : : (uint32_t)0U,
304 : : (uint32_t)5U,
305 : : (uint32_t)1U,
306 : : KRML_MAYBE_FOR16(i,
307 : : (uint32_t)0U,
308 : : (uint32_t)16U,
309 : : (uint32_t)1U,
310 : : uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512[(uint32_t)16U * i0 + i];
311 : : uint64_t ws_t = ws[i];
312 : : uint64_t a0 = hash[0U];
313 : : uint64_t b0 = hash[1U];
314 : : uint64_t c0 = hash[2U];
315 : : uint64_t d0 = hash[3U];
316 : : uint64_t e0 = hash[4U];
317 : : uint64_t f0 = hash[5U];
318 : : uint64_t g0 = hash[6U];
319 : : uint64_t h02 = hash[7U];
320 : : uint64_t k_e_t = k_t;
321 : : uint64_t
322 : : t1 =
323 : : h02
324 : : +
325 : : ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U)
326 : : ^
327 : : ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U)
328 : : ^ (e0 << (uint32_t)23U | e0 >> (uint32_t)41U)))
329 : : + ((e0 & f0) ^ (~e0 & g0))
330 : : + k_e_t
331 : : + ws_t;
332 : : uint64_t
333 : : t2 =
334 : : ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U)
335 : : ^
336 : : ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U)
337 : : ^ (a0 << (uint32_t)25U | a0 >> (uint32_t)39U)))
338 : : + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0)));
339 : : uint64_t a1 = t1 + t2;
340 : : uint64_t b1 = a0;
341 : : uint64_t c1 = b0;
342 : : uint64_t d1 = c0;
343 : : uint64_t e1 = d0 + t1;
344 : : uint64_t f1 = e0;
345 : : uint64_t g1 = f0;
346 : : uint64_t h12 = g0;
347 : : hash[0U] = a1;
348 : : hash[1U] = b1;
349 : : hash[2U] = c1;
350 : : hash[3U] = d1;
351 : : hash[4U] = e1;
352 : : hash[5U] = f1;
353 : : hash[6U] = g1;
354 : : hash[7U] = h12;);
355 : : if (i0 < (uint32_t)4U)
356 : : {
357 : : KRML_MAYBE_FOR16(i,
358 : : (uint32_t)0U,
359 : : (uint32_t)16U,
360 : : (uint32_t)1U,
361 : : uint64_t t16 = ws[i];
362 : : uint64_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U];
363 : : uint64_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U];
364 : : uint64_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U];
365 : : uint64_t
366 : : s1 =
367 : : (t2 << (uint32_t)45U | t2 >> (uint32_t)19U)
368 : : ^ ((t2 << (uint32_t)3U | t2 >> (uint32_t)61U) ^ t2 >> (uint32_t)6U);
369 : : uint64_t
370 : : s0 =
371 : : (t15 << (uint32_t)63U | t15 >> (uint32_t)1U)
372 : : ^ ((t15 << (uint32_t)56U | t15 >> (uint32_t)8U) ^ t15 >> (uint32_t)7U);
373 : : ws[i] = s1 + t7 + s0 + t16;);
374 : : });
375 : 0 : KRML_MAYBE_FOR8(i,
376 : : (uint32_t)0U,
377 : : (uint32_t)8U,
378 : : (uint32_t)1U,
379 : : uint64_t *os = hash;
380 : : uint64_t x = hash[i] + hash_old[i];
381 : : os[i] = x;);
382 : 0 : }
383 : :
384 : 0 : static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
385 : : {
386 : 0 : uint32_t blocks = len / (uint32_t)128U;
387 [ # # ]: 0 : for (uint32_t i = (uint32_t)0U; i < blocks; i++)
388 : : {
389 : 0 : uint8_t *b0 = b;
390 : 0 : uint8_t *mb = b0 + i * (uint32_t)128U;
391 : 0 : sha512_update(mb, st);
392 : : }
393 : 0 : }
394 : :
395 : : static inline void
396 : 0 : sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash)
397 : : {
398 : : uint32_t blocks;
399 [ # # ]: 0 : if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U)
400 : : {
401 : 0 : blocks = (uint32_t)1U;
402 : : }
403 : : else
404 : : {
405 : 0 : blocks = (uint32_t)2U;
406 : : }
407 : 0 : uint32_t fin = blocks * (uint32_t)128U;
408 : 0 : uint8_t last[256U] = { 0U };
409 : 0 : uint8_t totlen_buf[16U] = { 0U };
410 : 0 : FStar_UInt128_uint128 total_len_bits = FStar_UInt128_shift_left(totlen, (uint32_t)3U);
411 : 0 : store128_be(totlen_buf, total_len_bits);
412 : 0 : uint8_t *b0 = b;
413 : 0 : memcpy(last, b0, len * sizeof (uint8_t));
414 : 0 : last[len] = (uint8_t)0x80U;
415 : 0 : memcpy(last + fin - (uint32_t)16U, totlen_buf, (uint32_t)16U * sizeof (uint8_t));
416 : 0 : uint8_t *last00 = last;
417 : 0 : uint8_t *last10 = last + (uint32_t)128U;
418 : 0 : uint8_t *l0 = last00;
419 : 0 : uint8_t *l1 = last10;
420 : 0 : uint8_t *lb0 = l0;
421 : 0 : uint8_t *lb1 = l1;
422 : 0 : uint8_t *last0 = lb0;
423 : 0 : uint8_t *last1 = lb1;
424 : 0 : sha512_update(last0, hash);
425 [ # # ]: 0 : if (blocks > (uint32_t)1U)
426 : : {
427 : 0 : sha512_update(last1, hash);
428 : 0 : return;
429 : : }
430 : : }
431 : :
432 : 0 : static inline void sha512_finish(uint64_t *st, uint8_t *h)
433 : : {
434 : 0 : uint8_t hbuf[64U] = { 0U };
435 : 0 : KRML_MAYBE_FOR8(i,
436 : : (uint32_t)0U,
437 : : (uint32_t)8U,
438 : : (uint32_t)1U,
439 : : store64_be(hbuf + i * (uint32_t)8U, st[i]););
440 : 0 : memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t));
441 : 0 : }
442 : :
443 : 0 : static inline void sha384_init(uint64_t *hash)
444 : : {
445 : 0 : KRML_MAYBE_FOR8(i,
446 : : (uint32_t)0U,
447 : : (uint32_t)8U,
448 : : (uint32_t)1U,
449 : : uint64_t *os = hash;
450 : : uint64_t x = Hacl_Impl_SHA2_Generic_h384[i];
451 : : os[i] = x;);
452 : 0 : }
453 : :
454 : 0 : static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
455 : : {
456 : 0 : sha512_update_nblocks(len, b, st);
457 : 0 : }
458 : :
459 : : static void
460 : 0 : sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st)
461 : : {
462 : 0 : sha512_update_last(totlen, len, b, st);
463 : 0 : }
464 : :
465 : 0 : static inline void sha384_finish(uint64_t *st, uint8_t *h)
466 : : {
467 : 0 : uint8_t hbuf[64U] = { 0U };
468 : 0 : KRML_MAYBE_FOR8(i,
469 : : (uint32_t)0U,
470 : : (uint32_t)8U,
471 : : (uint32_t)1U,
472 : : store64_be(hbuf + i * (uint32_t)8U, st[i]););
473 : 0 : memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t));
474 : 0 : }
475 : :
476 : : /**
477 : : Allocate initial state for the SHA2_256 hash. The state is to be freed by
478 : : calling `free_256`.
479 : : */
480 : 0 : Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void)
481 : : {
482 : 0 : uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
483 : 0 : uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t));
484 : : Hacl_Streaming_MD_state_32
485 : 0 : s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
486 : : Hacl_Streaming_MD_state_32
487 : 0 : *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
488 : 0 : p[0U] = s;
489 : 0 : sha256_init(block_state);
490 : 0 : return p;
491 : : }
492 : :
493 : : /**
494 : : Copies the state passed as argument into a newly allocated state (deep copy).
495 : : The state is to be freed by calling `free_256`. Cloning the state this way is
496 : : useful, for instance, if your control-flow diverges and you need to feed
497 : : more (different) data into the hash in each branch.
498 : : */
499 : 0 : Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0)
500 : : {
501 : 0 : Hacl_Streaming_MD_state_32 scrut = *s0;
502 : 0 : uint32_t *block_state0 = scrut.block_state;
503 : 0 : uint8_t *buf0 = scrut.buf;
504 : 0 : uint64_t total_len0 = scrut.total_len;
505 : 0 : uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
506 : 0 : memcpy(buf, buf0, (uint32_t)64U * sizeof (uint8_t));
507 : 0 : uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t));
508 : 0 : memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint32_t));
509 : : Hacl_Streaming_MD_state_32
510 : 0 : s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
511 : : Hacl_Streaming_MD_state_32
512 : 0 : *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
513 : 0 : p[0U] = s;
514 : 0 : return p;
515 : : }
516 : :
517 : : /**
518 : : Reset an existing state to the initial hash state with empty data.
519 : : */
520 : 0 : void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s)
521 : : {
522 : 0 : Hacl_Streaming_MD_state_32 scrut = *s;
523 : 0 : uint8_t *buf = scrut.buf;
524 : 0 : uint32_t *block_state = scrut.block_state;
525 : 0 : sha256_init(block_state);
526 : : Hacl_Streaming_MD_state_32
527 : 0 : tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
528 : 0 : s[0U] = tmp;
529 : 0 : }
530 : :
531 : : static inline uint32_t
532 : 0 : update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
533 : : {
534 : 0 : Hacl_Streaming_MD_state_32 s = *p;
535 : 0 : uint64_t total_len = s.total_len;
536 [ # # ]: 0 : if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len)
537 : : {
538 : 0 : return (uint32_t)1U;
539 : : }
540 : : uint32_t sz;
541 [ # # # # ]: 0 : if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
542 : : {
543 : 0 : sz = (uint32_t)64U;
544 : : }
545 : : else
546 : : {
547 : 0 : sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U);
548 : : }
549 [ # # ]: 0 : if (len <= (uint32_t)64U - sz)
550 : : {
551 : 0 : Hacl_Streaming_MD_state_32 s1 = *p;
552 : 0 : uint32_t *block_state1 = s1.block_state;
553 : 0 : uint8_t *buf = s1.buf;
554 : 0 : uint64_t total_len1 = s1.total_len;
555 : : uint32_t sz1;
556 [ # # # # ]: 0 : if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U)
557 : : {
558 : 0 : sz1 = (uint32_t)64U;
559 : : }
560 : : else
561 : : {
562 : 0 : sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U);
563 : : }
564 : 0 : uint8_t *buf2 = buf + sz1;
565 : 0 : memcpy(buf2, data, len * sizeof (uint8_t));
566 : 0 : uint64_t total_len2 = total_len1 + (uint64_t)len;
567 : : *p
568 : 0 : =
569 : : (
570 : : (Hacl_Streaming_MD_state_32){
571 : : .block_state = block_state1,
572 : : .buf = buf,
573 : : .total_len = total_len2
574 : : }
575 : : );
576 : : }
577 [ # # ]: 0 : else if (sz == (uint32_t)0U)
578 : : {
579 : 0 : Hacl_Streaming_MD_state_32 s1 = *p;
580 : 0 : uint32_t *block_state1 = s1.block_state;
581 : 0 : uint8_t *buf = s1.buf;
582 : 0 : uint64_t total_len1 = s1.total_len;
583 : : uint32_t sz1;
584 [ # # # # ]: 0 : if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U)
585 : : {
586 : 0 : sz1 = (uint32_t)64U;
587 : : }
588 : : else
589 : : {
590 : 0 : sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U);
591 : : }
592 [ # # ]: 0 : if (!(sz1 == (uint32_t)0U))
593 : : {
594 : 0 : sha256_update_nblocks((uint32_t)64U, buf, block_state1);
595 : : }
596 : : uint32_t ite;
597 [ # # # # ]: 0 : if ((uint64_t)len % (uint64_t)(uint32_t)64U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U)
598 : : {
599 : 0 : ite = (uint32_t)64U;
600 : : }
601 : : else
602 : : {
603 : 0 : ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)64U);
604 : : }
605 : 0 : uint32_t n_blocks = (len - ite) / (uint32_t)64U;
606 : 0 : uint32_t data1_len = n_blocks * (uint32_t)64U;
607 : 0 : uint32_t data2_len = len - data1_len;
608 : 0 : uint8_t *data1 = data;
609 : 0 : uint8_t *data2 = data + data1_len;
610 : 0 : sha256_update_nblocks(data1_len, data1, block_state1);
611 : 0 : uint8_t *dst = buf;
612 : 0 : memcpy(dst, data2, data2_len * sizeof (uint8_t));
613 : : *p
614 : 0 : =
615 : : (
616 : : (Hacl_Streaming_MD_state_32){
617 : : .block_state = block_state1,
618 : : .buf = buf,
619 : 0 : .total_len = total_len1 + (uint64_t)len
620 : : }
621 : : );
622 : : }
623 : : else
624 : : {
625 : 0 : uint32_t diff = (uint32_t)64U - sz;
626 : 0 : uint8_t *data1 = data;
627 : 0 : uint8_t *data2 = data + diff;
628 : 0 : Hacl_Streaming_MD_state_32 s1 = *p;
629 : 0 : uint32_t *block_state10 = s1.block_state;
630 : 0 : uint8_t *buf0 = s1.buf;
631 : 0 : uint64_t total_len10 = s1.total_len;
632 : : uint32_t sz10;
633 [ # # # # ]: 0 : if (total_len10 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len10 > (uint64_t)0U)
634 : : {
635 : 0 : sz10 = (uint32_t)64U;
636 : : }
637 : : else
638 : : {
639 : 0 : sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)64U);
640 : : }
641 : 0 : uint8_t *buf2 = buf0 + sz10;
642 : 0 : memcpy(buf2, data1, diff * sizeof (uint8_t));
643 : 0 : uint64_t total_len2 = total_len10 + (uint64_t)diff;
644 : : *p
645 : 0 : =
646 : : (
647 : : (Hacl_Streaming_MD_state_32){
648 : : .block_state = block_state10,
649 : : .buf = buf0,
650 : : .total_len = total_len2
651 : : }
652 : : );
653 : 0 : Hacl_Streaming_MD_state_32 s10 = *p;
654 : 0 : uint32_t *block_state1 = s10.block_state;
655 : 0 : uint8_t *buf = s10.buf;
656 : 0 : uint64_t total_len1 = s10.total_len;
657 : : uint32_t sz1;
658 [ # # # # ]: 0 : if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U)
659 : : {
660 : 0 : sz1 = (uint32_t)64U;
661 : : }
662 : : else
663 : : {
664 : 0 : sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U);
665 : : }
666 [ # # ]: 0 : if (!(sz1 == (uint32_t)0U))
667 : : {
668 : 0 : sha256_update_nblocks((uint32_t)64U, buf, block_state1);
669 : : }
670 : : uint32_t ite;
671 : : if
672 : 0 : (
673 : 0 : (uint64_t)(len - diff)
674 : : % (uint64_t)(uint32_t)64U
675 [ # # ]: 0 : == (uint64_t)0U
676 [ # # ]: 0 : && (uint64_t)(len - diff) > (uint64_t)0U
677 : : )
678 : : {
679 : 0 : ite = (uint32_t)64U;
680 : : }
681 : : else
682 : : {
683 : 0 : ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)64U);
684 : : }
685 : 0 : uint32_t n_blocks = (len - diff - ite) / (uint32_t)64U;
686 : 0 : uint32_t data1_len = n_blocks * (uint32_t)64U;
687 : 0 : uint32_t data2_len = len - diff - data1_len;
688 : 0 : uint8_t *data11 = data2;
689 : 0 : uint8_t *data21 = data2 + data1_len;
690 : 0 : sha256_update_nblocks(data1_len, data11, block_state1);
691 : 0 : uint8_t *dst = buf;
692 : 0 : memcpy(dst, data21, data2_len * sizeof (uint8_t));
693 : : *p
694 : 0 : =
695 : : (
696 : : (Hacl_Streaming_MD_state_32){
697 : : .block_state = block_state1,
698 : : .buf = buf,
699 : 0 : .total_len = total_len1 + (uint64_t)(len - diff)
700 : : }
701 : : );
702 : : }
703 : 0 : return (uint32_t)0U;
704 : : }
705 : :
706 : : /**
707 : : Feed an arbitrary amount of data into the hash. This function returns 0 for
708 : : success, or 1 if the combined length of all of the data passed to `update_256`
709 : : (since the last call to `init_256`) exceeds 2^61-1 bytes.
710 : :
711 : : This function is identical to the update function for SHA2_224.
712 : : */
713 : : uint32_t
714 : 0 : Hacl_Streaming_SHA2_update_256(
715 : : Hacl_Streaming_MD_state_32 *p,
716 : : uint8_t *input,
717 : : uint32_t input_len
718 : : )
719 : : {
720 : 0 : return update_224_256(p, input, input_len);
721 : : }
722 : :
723 : : /**
724 : : Write the resulting hash into `dst`, an array of 32 bytes. The state remains
725 : : valid after a call to `finish_256`, meaning the user may feed more data into
726 : : the hash via `update_256`. (The finish_256 function operates on an internal copy of
727 : : the state and therefore does not invalidate the client-held state `p`.)
728 : : */
729 : 0 : void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
730 : : {
731 : 0 : Hacl_Streaming_MD_state_32 scrut = *p;
732 : 0 : uint32_t *block_state = scrut.block_state;
733 : 0 : uint8_t *buf_ = scrut.buf;
734 : 0 : uint64_t total_len = scrut.total_len;
735 : : uint32_t r;
736 [ # # # # ]: 0 : if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
737 : : {
738 : 0 : r = (uint32_t)64U;
739 : : }
740 : : else
741 : : {
742 : 0 : r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U);
743 : : }
744 : 0 : uint8_t *buf_1 = buf_;
745 : 0 : uint32_t tmp_block_state[8U] = { 0U };
746 : 0 : memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t));
747 : : uint32_t ite;
748 [ # # # # ]: 0 : if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U)
749 : : {
750 : 0 : ite = (uint32_t)64U;
751 : : }
752 : : else
753 : : {
754 : 0 : ite = r % (uint32_t)64U;
755 : : }
756 : 0 : uint8_t *buf_last = buf_1 + r - ite;
757 : 0 : uint8_t *buf_multi = buf_1;
758 : 0 : sha256_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
759 : 0 : uint64_t prev_len_last = total_len - (uint64_t)r;
760 : 0 : sha256_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state);
761 : 0 : sha256_finish(tmp_block_state, dst);
762 : 0 : }
763 : :
764 : : /**
765 : : Free a state allocated with `create_in_256`.
766 : :
767 : : This function is identical to the free function for SHA2_224.
768 : : */
769 : 0 : void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s)
770 : : {
771 : 0 : Hacl_Streaming_MD_state_32 scrut = *s;
772 : 0 : uint8_t *buf = scrut.buf;
773 : 0 : uint32_t *block_state = scrut.block_state;
774 : 0 : KRML_HOST_FREE(block_state);
775 : 0 : KRML_HOST_FREE(buf);
776 : 0 : KRML_HOST_FREE(s);
777 : 0 : }
778 : :
779 : : /**
780 : : Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes.
781 : : */
782 : 0 : void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst)
783 : : {
784 : 0 : uint8_t *ib = input;
785 : 0 : uint8_t *rb = dst;
786 : 0 : uint32_t st[8U] = { 0U };
787 : 0 : sha256_init(st);
788 : 0 : uint32_t rem = input_len % (uint32_t)64U;
789 : 0 : uint64_t len_ = (uint64_t)input_len;
790 : 0 : sha256_update_nblocks(input_len, ib, st);
791 : 0 : uint32_t rem1 = input_len % (uint32_t)64U;
792 : 0 : uint8_t *b0 = ib;
793 : 0 : uint8_t *lb = b0 + input_len - rem1;
794 : 0 : sha256_update_last(len_, rem, lb, st);
795 : 0 : sha256_finish(st, rb);
796 : 0 : }
797 : :
798 : 0 : Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void)
799 : : {
800 : 0 : uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
801 : 0 : uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t));
802 : : Hacl_Streaming_MD_state_32
803 : 0 : s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
804 : : Hacl_Streaming_MD_state_32
805 : 0 : *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
806 : 0 : p[0U] = s;
807 : 0 : sha224_init(block_state);
808 : 0 : return p;
809 : : }
810 : :
811 : 0 : void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s)
812 : : {
813 : 0 : Hacl_Streaming_MD_state_32 scrut = *s;
814 : 0 : uint8_t *buf = scrut.buf;
815 : 0 : uint32_t *block_state = scrut.block_state;
816 : 0 : sha224_init(block_state);
817 : : Hacl_Streaming_MD_state_32
818 : 0 : tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
819 : 0 : s[0U] = tmp;
820 : 0 : }
821 : :
822 : : uint32_t
823 : 0 : Hacl_Streaming_SHA2_update_224(
824 : : Hacl_Streaming_MD_state_32 *p,
825 : : uint8_t *input,
826 : : uint32_t input_len
827 : : )
828 : : {
829 : 0 : return update_224_256(p, input, input_len);
830 : : }
831 : :
832 : : /**
833 : : Write the resulting hash into `dst`, an array of 28 bytes. The state remains
834 : : valid after a call to `finish_224`, meaning the user may feed more data into
835 : : the hash via `update_224`.
836 : : */
837 : 0 : void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
838 : : {
839 : 0 : Hacl_Streaming_MD_state_32 scrut = *p;
840 : 0 : uint32_t *block_state = scrut.block_state;
841 : 0 : uint8_t *buf_ = scrut.buf;
842 : 0 : uint64_t total_len = scrut.total_len;
843 : : uint32_t r;
844 [ # # # # ]: 0 : if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
845 : : {
846 : 0 : r = (uint32_t)64U;
847 : : }
848 : : else
849 : : {
850 : 0 : r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U);
851 : : }
852 : 0 : uint8_t *buf_1 = buf_;
853 : 0 : uint32_t tmp_block_state[8U] = { 0U };
854 : 0 : memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t));
855 : : uint32_t ite;
856 [ # # # # ]: 0 : if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U)
857 : : {
858 : 0 : ite = (uint32_t)64U;
859 : : }
860 : : else
861 : : {
862 : 0 : ite = r % (uint32_t)64U;
863 : : }
864 : 0 : uint8_t *buf_last = buf_1 + r - ite;
865 : 0 : uint8_t *buf_multi = buf_1;
866 : 0 : sha224_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
867 : 0 : uint64_t prev_len_last = total_len - (uint64_t)r;
868 : 0 : sha224_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state);
869 : 0 : sha224_finish(tmp_block_state, dst);
870 : 0 : }
871 : :
872 : 0 : void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p)
873 : : {
874 : 0 : Hacl_Streaming_SHA2_free_256(p);
875 : 0 : }
876 : :
877 : : /**
878 : : Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes.
879 : : */
880 : 0 : void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst)
881 : : {
882 : 0 : uint8_t *ib = input;
883 : 0 : uint8_t *rb = dst;
884 : 0 : uint32_t st[8U] = { 0U };
885 : 0 : sha224_init(st);
886 : 0 : uint32_t rem = input_len % (uint32_t)64U;
887 : 0 : uint64_t len_ = (uint64_t)input_len;
888 : 0 : sha224_update_nblocks(input_len, ib, st);
889 : 0 : uint32_t rem1 = input_len % (uint32_t)64U;
890 : 0 : uint8_t *b0 = ib;
891 : 0 : uint8_t *lb = b0 + input_len - rem1;
892 : 0 : sha224_update_last(len_, rem, lb, st);
893 : 0 : sha224_finish(st, rb);
894 : 0 : }
895 : :
896 : 0 : Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void)
897 : : {
898 : 0 : uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t));
899 : 0 : uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t));
900 : : Hacl_Streaming_MD_state_64
901 : 0 : s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
902 : : Hacl_Streaming_MD_state_64
903 : 0 : *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
904 : 0 : p[0U] = s;
905 : 0 : Hacl_SHA2_Scalar32_sha512_init(block_state);
906 : 0 : return p;
907 : : }
908 : :
909 : : /**
910 : : Copies the state passed as argument into a newly allocated state (deep copy).
911 : : The state is to be freed by calling `free_512`. Cloning the state this way is
912 : : useful, for instance, if your control-flow diverges and you need to feed
913 : : more (different) data into the hash in each branch.
914 : : */
915 : 0 : Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0)
916 : : {
917 : 0 : Hacl_Streaming_MD_state_64 scrut = *s0;
918 : 0 : uint64_t *block_state0 = scrut.block_state;
919 : 0 : uint8_t *buf0 = scrut.buf;
920 : 0 : uint64_t total_len0 = scrut.total_len;
921 : 0 : uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t));
922 : 0 : memcpy(buf, buf0, (uint32_t)128U * sizeof (uint8_t));
923 : 0 : uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t));
924 : 0 : memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint64_t));
925 : : Hacl_Streaming_MD_state_64
926 : 0 : s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
927 : : Hacl_Streaming_MD_state_64
928 : 0 : *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
929 : 0 : p[0U] = s;
930 : 0 : return p;
931 : : }
932 : :
933 : 0 : void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s)
934 : : {
935 : 0 : Hacl_Streaming_MD_state_64 scrut = *s;
936 : 0 : uint8_t *buf = scrut.buf;
937 : 0 : uint64_t *block_state = scrut.block_state;
938 : 0 : Hacl_SHA2_Scalar32_sha512_init(block_state);
939 : : Hacl_Streaming_MD_state_64
940 : 0 : tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
941 : 0 : s[0U] = tmp;
942 : 0 : }
943 : :
944 : : static inline uint32_t
945 : 0 : update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
946 : : {
947 : 0 : Hacl_Streaming_MD_state_64 s = *p;
948 : 0 : uint64_t total_len = s.total_len;
949 [ # # ]: 0 : if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len)
950 : : {
951 : 0 : return (uint32_t)1U;
952 : : }
953 : : uint32_t sz;
954 [ # # # # ]: 0 : if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
955 : : {
956 : 0 : sz = (uint32_t)128U;
957 : : }
958 : : else
959 : : {
960 : 0 : sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U);
961 : : }
962 [ # # ]: 0 : if (len <= (uint32_t)128U - sz)
963 : : {
964 : 0 : Hacl_Streaming_MD_state_64 s1 = *p;
965 : 0 : uint64_t *block_state1 = s1.block_state;
966 : 0 : uint8_t *buf = s1.buf;
967 : 0 : uint64_t total_len1 = s1.total_len;
968 : : uint32_t sz1;
969 [ # # # # ]: 0 : if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U)
970 : : {
971 : 0 : sz1 = (uint32_t)128U;
972 : : }
973 : : else
974 : : {
975 : 0 : sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U);
976 : : }
977 : 0 : uint8_t *buf2 = buf + sz1;
978 : 0 : memcpy(buf2, data, len * sizeof (uint8_t));
979 : 0 : uint64_t total_len2 = total_len1 + (uint64_t)len;
980 : : *p
981 : 0 : =
982 : : (
983 : : (Hacl_Streaming_MD_state_64){
984 : : .block_state = block_state1,
985 : : .buf = buf,
986 : : .total_len = total_len2
987 : : }
988 : : );
989 : : }
990 [ # # ]: 0 : else if (sz == (uint32_t)0U)
991 : : {
992 : 0 : Hacl_Streaming_MD_state_64 s1 = *p;
993 : 0 : uint64_t *block_state1 = s1.block_state;
994 : 0 : uint8_t *buf = s1.buf;
995 : 0 : uint64_t total_len1 = s1.total_len;
996 : : uint32_t sz1;
997 [ # # # # ]: 0 : if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U)
998 : : {
999 : 0 : sz1 = (uint32_t)128U;
1000 : : }
1001 : : else
1002 : : {
1003 : 0 : sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U);
1004 : : }
1005 [ # # ]: 0 : if (!(sz1 == (uint32_t)0U))
1006 : : {
1007 : 0 : sha512_update_nblocks((uint32_t)128U, buf, block_state1);
1008 : : }
1009 : : uint32_t ite;
1010 [ # # # # ]: 0 : if ((uint64_t)len % (uint64_t)(uint32_t)128U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U)
1011 : : {
1012 : 0 : ite = (uint32_t)128U;
1013 : : }
1014 : : else
1015 : : {
1016 : 0 : ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)128U);
1017 : : }
1018 : 0 : uint32_t n_blocks = (len - ite) / (uint32_t)128U;
1019 : 0 : uint32_t data1_len = n_blocks * (uint32_t)128U;
1020 : 0 : uint32_t data2_len = len - data1_len;
1021 : 0 : uint8_t *data1 = data;
1022 : 0 : uint8_t *data2 = data + data1_len;
1023 : 0 : sha512_update_nblocks(data1_len, data1, block_state1);
1024 : 0 : uint8_t *dst = buf;
1025 : 0 : memcpy(dst, data2, data2_len * sizeof (uint8_t));
1026 : : *p
1027 : 0 : =
1028 : : (
1029 : : (Hacl_Streaming_MD_state_64){
1030 : : .block_state = block_state1,
1031 : : .buf = buf,
1032 : 0 : .total_len = total_len1 + (uint64_t)len
1033 : : }
1034 : : );
1035 : : }
1036 : : else
1037 : : {
1038 : 0 : uint32_t diff = (uint32_t)128U - sz;
1039 : 0 : uint8_t *data1 = data;
1040 : 0 : uint8_t *data2 = data + diff;
1041 : 0 : Hacl_Streaming_MD_state_64 s1 = *p;
1042 : 0 : uint64_t *block_state10 = s1.block_state;
1043 : 0 : uint8_t *buf0 = s1.buf;
1044 : 0 : uint64_t total_len10 = s1.total_len;
1045 : : uint32_t sz10;
1046 [ # # # # ]: 0 : if (total_len10 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len10 > (uint64_t)0U)
1047 : : {
1048 : 0 : sz10 = (uint32_t)128U;
1049 : : }
1050 : : else
1051 : : {
1052 : 0 : sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)128U);
1053 : : }
1054 : 0 : uint8_t *buf2 = buf0 + sz10;
1055 : 0 : memcpy(buf2, data1, diff * sizeof (uint8_t));
1056 : 0 : uint64_t total_len2 = total_len10 + (uint64_t)diff;
1057 : : *p
1058 : 0 : =
1059 : : (
1060 : : (Hacl_Streaming_MD_state_64){
1061 : : .block_state = block_state10,
1062 : : .buf = buf0,
1063 : : .total_len = total_len2
1064 : : }
1065 : : );
1066 : 0 : Hacl_Streaming_MD_state_64 s10 = *p;
1067 : 0 : uint64_t *block_state1 = s10.block_state;
1068 : 0 : uint8_t *buf = s10.buf;
1069 : 0 : uint64_t total_len1 = s10.total_len;
1070 : : uint32_t sz1;
1071 [ # # # # ]: 0 : if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U)
1072 : : {
1073 : 0 : sz1 = (uint32_t)128U;
1074 : : }
1075 : : else
1076 : : {
1077 : 0 : sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U);
1078 : : }
1079 [ # # ]: 0 : if (!(sz1 == (uint32_t)0U))
1080 : : {
1081 : 0 : sha512_update_nblocks((uint32_t)128U, buf, block_state1);
1082 : : }
1083 : : uint32_t ite;
1084 : : if
1085 : 0 : (
1086 : 0 : (uint64_t)(len - diff)
1087 : : % (uint64_t)(uint32_t)128U
1088 [ # # ]: 0 : == (uint64_t)0U
1089 [ # # ]: 0 : && (uint64_t)(len - diff) > (uint64_t)0U
1090 : : )
1091 : : {
1092 : 0 : ite = (uint32_t)128U;
1093 : : }
1094 : : else
1095 : : {
1096 : 0 : ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)128U);
1097 : : }
1098 : 0 : uint32_t n_blocks = (len - diff - ite) / (uint32_t)128U;
1099 : 0 : uint32_t data1_len = n_blocks * (uint32_t)128U;
1100 : 0 : uint32_t data2_len = len - diff - data1_len;
1101 : 0 : uint8_t *data11 = data2;
1102 : 0 : uint8_t *data21 = data2 + data1_len;
1103 : 0 : sha512_update_nblocks(data1_len, data11, block_state1);
1104 : 0 : uint8_t *dst = buf;
1105 : 0 : memcpy(dst, data21, data2_len * sizeof (uint8_t));
1106 : : *p
1107 : 0 : =
1108 : : (
1109 : : (Hacl_Streaming_MD_state_64){
1110 : : .block_state = block_state1,
1111 : : .buf = buf,
1112 : 0 : .total_len = total_len1 + (uint64_t)(len - diff)
1113 : : }
1114 : : );
1115 : : }
1116 : 0 : return (uint32_t)0U;
1117 : : }
1118 : :
1119 : : /**
1120 : : Feed an arbitrary amount of data into the hash. This function returns 0 for
1121 : : success, or 1 if the combined length of all of the data passed to `update_512`
1122 : : (since the last call to `init_512`) exceeds 2^125-1 bytes.
1123 : :
1124 : : This function is identical to the update function for SHA2_384.
1125 : : */
1126 : : uint32_t
1127 : 0 : Hacl_Streaming_SHA2_update_512(
1128 : : Hacl_Streaming_MD_state_64 *p,
1129 : : uint8_t *input,
1130 : : uint32_t input_len
1131 : : )
1132 : : {
1133 : 0 : return update_384_512(p, input, input_len);
1134 : : }
1135 : :
1136 : : /**
1137 : : Write the resulting hash into `dst`, an array of 64 bytes. The state remains
1138 : : valid after a call to `finish_512`, meaning the user may feed more data into
1139 : : the hash via `update_512`. (The finish_512 function operates on an internal copy of
1140 : : the state and therefore does not invalidate the client-held state `p`.)
1141 : : */
1142 : 0 : void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst)
1143 : : {
1144 : 0 : Hacl_Streaming_MD_state_64 scrut = *p;
1145 : 0 : uint64_t *block_state = scrut.block_state;
1146 : 0 : uint8_t *buf_ = scrut.buf;
1147 : 0 : uint64_t total_len = scrut.total_len;
1148 : : uint32_t r;
1149 [ # # # # ]: 0 : if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
1150 : : {
1151 : 0 : r = (uint32_t)128U;
1152 : : }
1153 : : else
1154 : : {
1155 : 0 : r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U);
1156 : : }
1157 : 0 : uint8_t *buf_1 = buf_;
1158 : 0 : uint64_t tmp_block_state[8U] = { 0U };
1159 : 0 : memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t));
1160 : : uint32_t ite;
1161 [ # # # # ]: 0 : if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U)
1162 : : {
1163 : 0 : ite = (uint32_t)128U;
1164 : : }
1165 : : else
1166 : : {
1167 : 0 : ite = r % (uint32_t)128U;
1168 : : }
1169 : 0 : uint8_t *buf_last = buf_1 + r - ite;
1170 : 0 : uint8_t *buf_multi = buf_1;
1171 : 0 : sha512_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
1172 : 0 : uint64_t prev_len_last = total_len - (uint64_t)r;
1173 : 0 : sha512_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
1174 : : FStar_UInt128_uint64_to_uint128((uint64_t)r)),
1175 : : r,
1176 : : buf_last,
1177 : : tmp_block_state);
1178 : 0 : sha512_finish(tmp_block_state, dst);
1179 : 0 : }
1180 : :
1181 : : /**
1182 : : Free a state allocated with `create_in_512`.
1183 : :
1184 : : This function is identical to the free function for SHA2_384.
1185 : : */
1186 : 0 : void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s)
1187 : : {
1188 : 0 : Hacl_Streaming_MD_state_64 scrut = *s;
1189 : 0 : uint8_t *buf = scrut.buf;
1190 : 0 : uint64_t *block_state = scrut.block_state;
1191 : 0 : KRML_HOST_FREE(block_state);
1192 : 0 : KRML_HOST_FREE(buf);
1193 : 0 : KRML_HOST_FREE(s);
1194 : 0 : }
1195 : :
1196 : : /**
1197 : : Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes.
1198 : : */
1199 : 0 : void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst)
1200 : : {
1201 : 0 : uint8_t *ib = input;
1202 : 0 : uint8_t *rb = dst;
1203 : 0 : uint64_t st[8U] = { 0U };
1204 : 0 : Hacl_SHA2_Scalar32_sha512_init(st);
1205 : 0 : uint32_t rem = input_len % (uint32_t)128U;
1206 : 0 : FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len);
1207 : 0 : sha512_update_nblocks(input_len, ib, st);
1208 : 0 : uint32_t rem1 = input_len % (uint32_t)128U;
1209 : 0 : uint8_t *b0 = ib;
1210 : 0 : uint8_t *lb = b0 + input_len - rem1;
1211 : 0 : sha512_update_last(len_, rem, lb, st);
1212 : 0 : sha512_finish(st, rb);
1213 : 0 : }
1214 : :
1215 : 0 : Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void)
1216 : : {
1217 : 0 : uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t));
1218 : 0 : uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t));
1219 : : Hacl_Streaming_MD_state_64
1220 : 0 : s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
1221 : : Hacl_Streaming_MD_state_64
1222 : 0 : *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
1223 : 0 : p[0U] = s;
1224 : 0 : sha384_init(block_state);
1225 : 0 : return p;
1226 : : }
1227 : :
1228 : 0 : void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s)
1229 : : {
1230 : 0 : Hacl_Streaming_MD_state_64 scrut = *s;
1231 : 0 : uint8_t *buf = scrut.buf;
1232 : 0 : uint64_t *block_state = scrut.block_state;
1233 : 0 : sha384_init(block_state);
1234 : : Hacl_Streaming_MD_state_64
1235 : 0 : tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
1236 : 0 : s[0U] = tmp;
1237 : 0 : }
1238 : :
1239 : : uint32_t
1240 : 0 : Hacl_Streaming_SHA2_update_384(
1241 : : Hacl_Streaming_MD_state_64 *p,
1242 : : uint8_t *input,
1243 : : uint32_t input_len
1244 : : )
1245 : : {
1246 : 0 : return update_384_512(p, input, input_len);
1247 : : }
1248 : :
1249 : : /**
1250 : : Write the resulting hash into `dst`, an array of 48 bytes. The state remains
1251 : : valid after a call to `finish_384`, meaning the user may feed more data into
1252 : : the hash via `update_384`.
1253 : : */
1254 : 0 : void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst)
1255 : : {
1256 : 0 : Hacl_Streaming_MD_state_64 scrut = *p;
1257 : 0 : uint64_t *block_state = scrut.block_state;
1258 : 0 : uint8_t *buf_ = scrut.buf;
1259 : 0 : uint64_t total_len = scrut.total_len;
1260 : : uint32_t r;
1261 [ # # # # ]: 0 : if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
1262 : : {
1263 : 0 : r = (uint32_t)128U;
1264 : : }
1265 : : else
1266 : : {
1267 : 0 : r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U);
1268 : : }
1269 : 0 : uint8_t *buf_1 = buf_;
1270 : 0 : uint64_t tmp_block_state[8U] = { 0U };
1271 : 0 : memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t));
1272 : : uint32_t ite;
1273 [ # # # # ]: 0 : if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U)
1274 : : {
1275 : 0 : ite = (uint32_t)128U;
1276 : : }
1277 : : else
1278 : : {
1279 : 0 : ite = r % (uint32_t)128U;
1280 : : }
1281 : 0 : uint8_t *buf_last = buf_1 + r - ite;
1282 : 0 : uint8_t *buf_multi = buf_1;
1283 : 0 : sha384_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
1284 : 0 : uint64_t prev_len_last = total_len - (uint64_t)r;
1285 : 0 : sha384_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
1286 : : FStar_UInt128_uint64_to_uint128((uint64_t)r)),
1287 : : r,
1288 : : buf_last,
1289 : : tmp_block_state);
1290 : 0 : sha384_finish(tmp_block_state, dst);
1291 : 0 : }
1292 : :
1293 : 0 : void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p)
1294 : : {
1295 : 0 : Hacl_Streaming_SHA2_free_512(p);
1296 : 0 : }
1297 : :
1298 : : /**
1299 : : Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes.
1300 : : */
1301 : 0 : void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst)
1302 : : {
1303 : 0 : uint8_t *ib = input;
1304 : 0 : uint8_t *rb = dst;
1305 : 0 : uint64_t st[8U] = { 0U };
1306 : 0 : sha384_init(st);
1307 : 0 : uint32_t rem = input_len % (uint32_t)128U;
1308 : 0 : FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len);
1309 : 0 : sha384_update_nblocks(input_len, ib, st);
1310 : 0 : uint32_t rem1 = input_len % (uint32_t)128U;
1311 : 0 : uint8_t *b0 = ib;
1312 : 0 : uint8_t *lb = b0 + input_len - rem1;
1313 : 0 : sha384_update_last(len_, rem, lb, st);
1314 : 0 : sha384_finish(st, rb);
1315 : 0 : }
1316 : :
|