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_SHA3.h"
27
28 static uint32_t block_len(Spec_Hash_Definitions_hash_alg a)
29 {
30 switch (a)
31 {
32 case Spec_Hash_Definitions_SHA3_224:
33 {
34 return (uint32_t)144U;
35 }
36 case Spec_Hash_Definitions_SHA3_256:
37 {
38 return (uint32_t)136U;
39 }
40 case Spec_Hash_Definitions_SHA3_384:
41 {
42 return (uint32_t)104U;
43 }
44 case Spec_Hash_Definitions_SHA3_512:
45 {
46 return (uint32_t)72U;
47 }
48 case Spec_Hash_Definitions_Shake128:
49 {
50 return (uint32_t)168U;
51 }
52 case Spec_Hash_Definitions_Shake256:
53 {
54 return (uint32_t)136U;
55 }
56 default:
57 {
58 KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
59 KRML_HOST_EXIT(253U);
60 }
61 }
62 }
63
64 static uint32_t hash_len(Spec_Hash_Definitions_hash_alg a)
65 {
66 switch (a)
67 {
68 case Spec_Hash_Definitions_SHA3_224:
69 {
70 return (uint32_t)28U;
71 }
72 case Spec_Hash_Definitions_SHA3_256:
73 {
74 return (uint32_t)32U;
75 }
76 case Spec_Hash_Definitions_SHA3_384:
77 {
78 return (uint32_t)48U;
79 }
80 case Spec_Hash_Definitions_SHA3_512:
81 {
82 return (uint32_t)64U;
83 }
84 default:
85 {
86 KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
87 KRML_HOST_EXIT(253U);
88 }
89 }
90 }
91
92 void
93 Hacl_Hash_SHA3_update_multi_sha3(
94 Spec_Hash_Definitions_hash_alg a,
95 uint64_t *s,
96 uint8_t *blocks,
97 uint32_t n_blocks
98 )
99 {
100 for (uint32_t i = (uint32_t)0U; i < n_blocks; i++)
101 {
102 uint8_t *block = blocks + i * block_len(a);
103 Hacl_Impl_SHA3_absorb_inner(block_len(a), block, s);
104 }
105 }
106
107 void
108 Hacl_Hash_SHA3_update_last_sha3(
109 Spec_Hash_Definitions_hash_alg a,
110 uint64_t *s,
111 uint8_t *input,
112 uint32_t input_len
113 )
114 {
115 uint8_t suffix;
116 if (a == Spec_Hash_Definitions_Shake128 || a == Spec_Hash_Definitions_Shake256)
117 {
118 suffix = (uint8_t)0x1fU;
119 }
120 else
121 {
122 suffix = (uint8_t)0x06U;
123 }
124 uint32_t len = block_len(a);
125 if (input_len == len)
126 {
127 Hacl_Impl_SHA3_absorb_inner(len, input, s);
128 uint8_t *uu____0 = input + input_len;
129 uint8_t lastBlock_[200U] = { 0U };
130 uint8_t *lastBlock = lastBlock_;
131 memcpy(lastBlock, uu____0, (uint32_t)0U * sizeof (uint8_t));
132 lastBlock[0U] = suffix;
133 Hacl_Impl_SHA3_loadState(len, lastBlock, s);
134 if (!((suffix & (uint8_t)0x80U) == (uint8_t)0U) && (uint32_t)0U == len - (uint32_t)1U)
135 {
136 Hacl_Impl_SHA3_state_permute(s);
137 }
138 uint8_t nextBlock_[200U] = { 0U };
139 uint8_t *nextBlock = nextBlock_;
140 nextBlock[len - (uint32_t)1U] = (uint8_t)0x80U;
141 Hacl_Impl_SHA3_loadState(len, nextBlock, s);
142 Hacl_Impl_SHA3_state_permute(s);
143 return;
144 }
145 uint8_t lastBlock_[200U] = { 0U };
146 uint8_t *lastBlock = lastBlock_;
147 memcpy(lastBlock, input, input_len * sizeof (uint8_t));
148 lastBlock[input_len] = suffix;
149 Hacl_Impl_SHA3_loadState(len, lastBlock, s);
150 if (!((suffix & (uint8_t)0x80U) == (uint8_t)0U) && input_len == len - (uint32_t)1U)
151 {
152 Hacl_Impl_SHA3_state_permute(s);
153 }
154 uint8_t nextBlock_[200U] = { 0U };
155 uint8_t *nextBlock = nextBlock_;
156 nextBlock[len - (uint32_t)1U] = (uint8_t)0x80U;
157 Hacl_Impl_SHA3_loadState(len, nextBlock, s);
158 Hacl_Impl_SHA3_state_permute(s);
159 }
160
161 typedef struct hash_buf2_s
162 {
163 Hacl_Streaming_Keccak_hash_buf fst;
164 Hacl_Streaming_Keccak_hash_buf snd;
165 }
166 hash_buf2;
167
168 Spec_Hash_Definitions_hash_alg Hacl_Streaming_Keccak_get_alg(Hacl_Streaming_Keccak_state *s)
169 {
170 Hacl_Streaming_Keccak_state scrut = *s;
171 Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state;
172 return block_state.fst;
173 }
174
175 Hacl_Streaming_Keccak_state *Hacl_Streaming_Keccak_malloc(Spec_Hash_Definitions_hash_alg a)
176 {
177 KRML_CHECK_SIZE(sizeof (uint8_t), block_len(a));
178 uint8_t *buf0 = (uint8_t *)KRML_HOST_CALLOC(block_len(a), sizeof (uint8_t));
179 uint64_t *buf = (uint64_t *)KRML_HOST_CALLOC((uint32_t)25U, sizeof (uint64_t));
180 Hacl_Streaming_Keccak_hash_buf block_state = { .fst = a, .snd = buf };
181 Hacl_Streaming_Keccak_state
182 s = { .block_state = block_state, .buf = buf0, .total_len = (uint64_t)(uint32_t)0U };
183 Hacl_Streaming_Keccak_state
184 *p = (Hacl_Streaming_Keccak_state *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_Keccak_state));
185 p[0U] = s;
186 uint64_t *s1 = block_state.snd;
187 memset(s1, 0U, (uint32_t)25U * sizeof (uint64_t));
188 return p;
189 }
190
191 void Hacl_Streaming_Keccak_free(Hacl_Streaming_Keccak_state *s)
192 {
193 Hacl_Streaming_Keccak_state scrut = *s;
194 uint8_t *buf = scrut.buf;
195 Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state;
196 uint64_t *s1 = block_state.snd;
197 KRML_HOST_FREE(s1);
198 KRML_HOST_FREE(buf);
199 KRML_HOST_FREE(s);
200 }
201
202 Hacl_Streaming_Keccak_state *Hacl_Streaming_Keccak_copy(Hacl_Streaming_Keccak_state *s0)
203 {
204 Hacl_Streaming_Keccak_state scrut0 = *s0;
205 Hacl_Streaming_Keccak_hash_buf block_state0 = scrut0.block_state;
206 uint8_t *buf0 = scrut0.buf;
207 uint64_t total_len0 = scrut0.total_len;
208 Spec_Hash_Definitions_hash_alg i = block_state0.fst;
209 KRML_CHECK_SIZE(sizeof (uint8_t), block_len(i));
210 uint8_t *buf1 = (uint8_t *)KRML_HOST_CALLOC(block_len(i), sizeof (uint8_t));
211 memcpy(buf1, buf0, block_len(i) * sizeof (uint8_t));
212 uint64_t *buf = (uint64_t *)KRML_HOST_CALLOC((uint32_t)25U, sizeof (uint64_t));
213 Hacl_Streaming_Keccak_hash_buf block_state = { .fst = i, .snd = buf };
214 hash_buf2 scrut = { .fst = block_state0, .snd = block_state };
215 uint64_t *s_dst = scrut.snd.snd;
216 uint64_t *s_src = scrut.fst.snd;
217 memcpy(s_dst, s_src, (uint32_t)25U * sizeof (uint64_t));
218 Hacl_Streaming_Keccak_state
219 s = { .block_state = block_state, .buf = buf1, .total_len = total_len0 };
220 Hacl_Streaming_Keccak_state
221 *p = (Hacl_Streaming_Keccak_state *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_Keccak_state));
222 p[0U] = s;
223 return p;
224 }
225
226 void Hacl_Streaming_Keccak_reset(Hacl_Streaming_Keccak_state *s)
227 {
228 Hacl_Streaming_Keccak_state scrut = *s;
229 uint8_t *buf = scrut.buf;
230 Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state;
231 uint64_t *s1 = block_state.snd;
232 memset(s1, 0U, (uint32_t)25U * sizeof (uint64_t));
233 Hacl_Streaming_Keccak_state
234 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
235 s[0U] = tmp;
236 }
237
238 Hacl_Streaming_Types_error_code
239 Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint32_t len)
240 {
241 Hacl_Streaming_Keccak_state s = *p;
242 Hacl_Streaming_Keccak_hash_buf block_state = s.block_state;
243 uint64_t total_len = s.total_len;
244 Spec_Hash_Definitions_hash_alg i = block_state.fst;
245 if ((uint64_t)len > (uint64_t)0xFFFFFFFFFFFFFFFFU - total_len)
246 {
247 return Hacl_Streaming_Types_MaximumLengthExceeded;
248 }
249 uint32_t sz;
250 if (total_len % (uint64_t)block_len(i) == (uint64_t)0U && total_len > (uint64_t)0U)
251 {
252 sz = block_len(i);
253 }
254 else
255 {
256 sz = (uint32_t)(total_len % (uint64_t)block_len(i));
257 }
258 if (len <= block_len(i) - sz)
259 {
260 Hacl_Streaming_Keccak_state s1 = *p;
261 Hacl_Streaming_Keccak_hash_buf block_state1 = s1.block_state;
262 uint8_t *buf = s1.buf;
263 uint64_t total_len1 = s1.total_len;
264 uint32_t sz1;
265 if (total_len1 % (uint64_t)block_len(i) == (uint64_t)0U && total_len1 > (uint64_t)0U)
266 {
267 sz1 = block_len(i);
268 }
269 else
270 {
271 sz1 = (uint32_t)(total_len1 % (uint64_t)block_len(i));
272 }
273 uint8_t *buf2 = buf + sz1;
274 memcpy(buf2, data, len * sizeof (uint8_t));
275 uint64_t total_len2 = total_len1 + (uint64_t)len;
276 *p
277 =
278 (
279 (Hacl_Streaming_Keccak_state){
280 .block_state = block_state1,
281 .buf = buf,
282 .total_len = total_len2
283 }
284 );
285 }
286 else if (sz == (uint32_t)0U)
287 {
288 Hacl_Streaming_Keccak_state s1 = *p;
289 Hacl_Streaming_Keccak_hash_buf block_state1 = s1.block_state;
290 uint8_t *buf = s1.buf;
291 uint64_t total_len1 = s1.total_len;
292 uint32_t sz1;
293 if (total_len1 % (uint64_t)block_len(i) == (uint64_t)0U && total_len1 > (uint64_t)0U)
294 {
295 sz1 = block_len(i);
296 }
297 else
298 {
299 sz1 = (uint32_t)(total_len1 % (uint64_t)block_len(i));
300 }
301 if (!(sz1 == (uint32_t)0U))
302 {
303 Spec_Hash_Definitions_hash_alg a1 = block_state1.fst;
304 uint64_t *s2 = block_state1.snd;
305 Hacl_Hash_SHA3_update_multi_sha3(a1, s2, buf, block_len(i) / block_len(a1));
306 }
307 uint32_t ite;
308 if ((uint64_t)len % (uint64_t)block_len(i) == (uint64_t)0U && (uint64_t)len > (uint64_t)0U)
309 {
310 ite = block_len(i);
311 }
312 else
313 {
314 ite = (uint32_t)((uint64_t)len % (uint64_t)block_len(i));
315 }
316 uint32_t n_blocks = (len - ite) / block_len(i);
317 uint32_t data1_len = n_blocks * block_len(i);
318 uint32_t data2_len = len - data1_len;
319 uint8_t *data1 = data;
320 uint8_t *data2 = data + data1_len;
321 Spec_Hash_Definitions_hash_alg a1 = block_state1.fst;
322 uint64_t *s2 = block_state1.snd;
323 Hacl_Hash_SHA3_update_multi_sha3(a1, s2, data1, data1_len / block_len(a1));
324 uint8_t *dst = buf;
325 memcpy(dst, data2, data2_len * sizeof (uint8_t));
326 *p
327 =
328 (
329 (Hacl_Streaming_Keccak_state){
330 .block_state = block_state1,
331 .buf = buf,
332 .total_len = total_len1 + (uint64_t)len
333 }
334 );
335 }
336 else
337 {
338 uint32_t diff = block_len(i) - sz;
339 uint8_t *data1 = data;
340 uint8_t *data2 = data + diff;
341 Hacl_Streaming_Keccak_state s1 = *p;
342 Hacl_Streaming_Keccak_hash_buf block_state10 = s1.block_state;
343 uint8_t *buf0 = s1.buf;
344 uint64_t total_len10 = s1.total_len;
345 uint32_t sz10;
346 if (total_len10 % (uint64_t)block_len(i) == (uint64_t)0U && total_len10 > (uint64_t)0U)
347 {
348 sz10 = block_len(i);
349 }
350 else
351 {
352 sz10 = (uint32_t)(total_len10 % (uint64_t)block_len(i));
353 }
354 uint8_t *buf2 = buf0 + sz10;
355 memcpy(buf2, data1, diff * sizeof (uint8_t));
356 uint64_t total_len2 = total_len10 + (uint64_t)diff;
357 *p
358 =
359 (
360 (Hacl_Streaming_Keccak_state){
361 .block_state = block_state10,
362 .buf = buf0,
363 .total_len = total_len2
364 }
365 );
366 Hacl_Streaming_Keccak_state s10 = *p;
367 Hacl_Streaming_Keccak_hash_buf block_state1 = s10.block_state;
368 uint8_t *buf = s10.buf;
369 uint64_t total_len1 = s10.total_len;
370 uint32_t sz1;
371 if (total_len1 % (uint64_t)block_len(i) == (uint64_t)0U && total_len1 > (uint64_t)0U)
372 {
373 sz1 = block_len(i);
374 }
375 else
376 {
377 sz1 = (uint32_t)(total_len1 % (uint64_t)block_len(i));
378 }
379 if (!(sz1 == (uint32_t)0U))
380 {
381 Spec_Hash_Definitions_hash_alg a1 = block_state1.fst;
382 uint64_t *s2 = block_state1.snd;
383 Hacl_Hash_SHA3_update_multi_sha3(a1, s2, buf, block_len(i) / block_len(a1));
384 }
385 uint32_t ite;
386 if
387 (
388 (uint64_t)(len - diff)
389 % (uint64_t)block_len(i)
390 == (uint64_t)0U
391 && (uint64_t)(len - diff) > (uint64_t)0U
392 )
393 {
394 ite = block_len(i);
395 }
396 else
397 {
398 ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)block_len(i));
399 }
400 uint32_t n_blocks = (len - diff - ite) / block_len(i);
401 uint32_t data1_len = n_blocks * block_len(i);
402 uint32_t data2_len = len - diff - data1_len;
403 uint8_t *data11 = data2;
404 uint8_t *data21 = data2 + data1_len;
405 Spec_Hash_Definitions_hash_alg a1 = block_state1.fst;
406 uint64_t *s2 = block_state1.snd;
407 Hacl_Hash_SHA3_update_multi_sha3(a1, s2, data11, data1_len / block_len(a1));
408 uint8_t *dst = buf;
409 memcpy(dst, data21, data2_len * sizeof (uint8_t));
410 *p
411 =
412 (
413 (Hacl_Streaming_Keccak_state){
414 .block_state = block_state1,
415 .buf = buf,
416 .total_len = total_len1 + (uint64_t)(len - diff)
417 }
418 );
419 }
420 return Hacl_Streaming_Types_Success;
421 }
422
423 static void
424 finish_(
425 Spec_Hash_Definitions_hash_alg a,
426 Hacl_Streaming_Keccak_state *p,
427 uint8_t *dst,
428 uint32_t l
429 )
430 {
431 Hacl_Streaming_Keccak_state scrut0 = *p;
432 Hacl_Streaming_Keccak_hash_buf block_state = scrut0.block_state;
433 uint8_t *buf_ = scrut0.buf;
434 uint64_t total_len = scrut0.total_len;
435 uint32_t r;
436 if (total_len % (uint64_t)block_len(a) == (uint64_t)0U && total_len > (uint64_t)0U)
437 {
438 r = block_len(a);
439 }
440 else
441 {
442 r = (uint32_t)(total_len % (uint64_t)block_len(a));
443 }
444 uint8_t *buf_1 = buf_;
445 uint64_t buf[25U] = { 0U };
446 Hacl_Streaming_Keccak_hash_buf tmp_block_state = { .fst = a, .snd = buf };
447 hash_buf2 scrut = { .fst = block_state, .snd = tmp_block_state };
448 uint64_t *s_dst = scrut.snd.snd;
449 uint64_t *s_src = scrut.fst.snd;
450 memcpy(s_dst, s_src, (uint32_t)25U * sizeof (uint64_t));
451 uint32_t ite0;
452 if (r % block_len(a) == (uint32_t)0U && r > (uint32_t)0U)
453 {
454 ite0 = block_len(a);
455 }
456 else
457 {
458 ite0 = r % block_len(a);
459 }
460 uint8_t *buf_last = buf_1 + r - ite0;
461 uint8_t *buf_multi = buf_1;
462 Spec_Hash_Definitions_hash_alg a1 = tmp_block_state.fst;
463 uint64_t *s0 = tmp_block_state.snd;
464 Hacl_Hash_SHA3_update_multi_sha3(a1, s0, buf_multi, (uint32_t)0U / block_len(a1));
465 Spec_Hash_Definitions_hash_alg a10 = tmp_block_state.fst;
466 uint64_t *s1 = tmp_block_state.snd;
467 Hacl_Hash_SHA3_update_last_sha3(a10, s1, buf_last, r);
468 Spec_Hash_Definitions_hash_alg a11 = tmp_block_state.fst;
469 uint64_t *s = tmp_block_state.snd;
470 if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256)
471 {
472 uint32_t ite;
473 if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256)
474 {
475 ite = l;
476 }
477 else
478 {
479 ite = hash_len(a11);
480 }
481 Hacl_Impl_SHA3_squeeze(s, block_len(a11), ite, dst);
482 return;
483 }
484 Hacl_Impl_SHA3_squeeze(s, block_len(a11), hash_len(a11), dst);
485 }
486
487 Hacl_Streaming_Types_error_code
488 Hacl_Streaming_Keccak_finish(Hacl_Streaming_Keccak_state *s, uint8_t *dst)
489 {
490 Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
491 if (a1 == Spec_Hash_Definitions_Shake128 || a1 == Spec_Hash_Definitions_Shake256)
492 {
493 return Hacl_Streaming_Types_InvalidAlgorithm;
494 }
495 finish_(a1, s, dst, hash_len(a1));
496 return Hacl_Streaming_Types_Success;
497 }
498
499 Hacl_Streaming_Types_error_code
500 Hacl_Streaming_Keccak_squeeze(Hacl_Streaming_Keccak_state *s, uint8_t *dst, uint32_t l)
501 {
502 Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
503 if (!(a1 == Spec_Hash_Definitions_Shake128 || a1 == Spec_Hash_Definitions_Shake256))
504 {
505 return Hacl_Streaming_Types_InvalidAlgorithm;
506 }
507 if (l == (uint32_t)0U)
508 {
509 return Hacl_Streaming_Types_InvalidLength;
510 }
511 finish_(a1, s, dst, l);
512 return Hacl_Streaming_Types_Success;
513 }
514
515 uint32_t Hacl_Streaming_Keccak_block_len(Hacl_Streaming_Keccak_state *s)
516 {
517 Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
518 return block_len(a1);
519 }
520
521 uint32_t Hacl_Streaming_Keccak_hash_len(Hacl_Streaming_Keccak_state *s)
522 {
523 Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
524 return hash_len(a1);
525 }
526
527 bool Hacl_Streaming_Keccak_is_shake(Hacl_Streaming_Keccak_state *s)
528 {
529 Spec_Hash_Definitions_hash_alg uu____0 = Hacl_Streaming_Keccak_get_alg(s);
530 return uu____0 == Spec_Hash_Definitions_Shake128 || uu____0 == Spec_Hash_Definitions_Shake256;
531 }
532
533 void
534 Hacl_SHA3_shake128_hacl(
535 uint32_t inputByteLen,
536 uint8_t *input,
537 uint32_t outputByteLen,
538 uint8_t *output
539 )
540 {
541 Hacl_Impl_SHA3_keccak((uint32_t)1344U,
542 (uint32_t)256U,
543 inputByteLen,
544 input,
545 (uint8_t)0x1FU,
546 outputByteLen,
547 output);
548 }
549
550 void
551 Hacl_SHA3_shake256_hacl(
552 uint32_t inputByteLen,
553 uint8_t *input,
554 uint32_t outputByteLen,
555 uint8_t *output
556 )
557 {
558 Hacl_Impl_SHA3_keccak((uint32_t)1088U,
559 (uint32_t)512U,
560 inputByteLen,
561 input,
562 (uint8_t)0x1FU,
563 outputByteLen,
564 output);
565 }
566
567 void Hacl_SHA3_sha3_224(uint32_t inputByteLen, uint8_t *input, uint8_t *output)
568 {
569 Hacl_Impl_SHA3_keccak((uint32_t)1152U,
570 (uint32_t)448U,
571 inputByteLen,
572 input,
573 (uint8_t)0x06U,
574 (uint32_t)28U,
575 output);
576 }
577
578 void Hacl_SHA3_sha3_256(uint32_t inputByteLen, uint8_t *input, uint8_t *output)
579 {
580 Hacl_Impl_SHA3_keccak((uint32_t)1088U,
581 (uint32_t)512U,
582 inputByteLen,
583 input,
584 (uint8_t)0x06U,
585 (uint32_t)32U,
586 output);
587 }
588
589 void Hacl_SHA3_sha3_384(uint32_t inputByteLen, uint8_t *input, uint8_t *output)
590 {
591 Hacl_Impl_SHA3_keccak((uint32_t)832U,
592 (uint32_t)768U,
593 inputByteLen,
594 input,
595 (uint8_t)0x06U,
596 (uint32_t)48U,
597 output);
598 }
599
600 void Hacl_SHA3_sha3_512(uint32_t inputByteLen, uint8_t *input, uint8_t *output)
601 {
602 Hacl_Impl_SHA3_keccak((uint32_t)576U,
603 (uint32_t)1024U,
604 inputByteLen,
605 input,
606 (uint8_t)0x06U,
607 (uint32_t)64U,
608 output);
609 }
610
611 static const
612 uint32_t
613 keccak_rotc[24U] =
614 {
615 (uint32_t)1U, (uint32_t)3U, (uint32_t)6U, (uint32_t)10U, (uint32_t)15U, (uint32_t)21U,
616 (uint32_t)28U, (uint32_t)36U, (uint32_t)45U, (uint32_t)55U, (uint32_t)2U, (uint32_t)14U,
617 (uint32_t)27U, (uint32_t)41U, (uint32_t)56U, (uint32_t)8U, (uint32_t)25U, (uint32_t)43U,
618 (uint32_t)62U, (uint32_t)18U, (uint32_t)39U, (uint32_t)61U, (uint32_t)20U, (uint32_t)44U
619 };
620
621 static const
622 uint32_t
623 keccak_piln[24U] =
624 {
625 (uint32_t)10U, (uint32_t)7U, (uint32_t)11U, (uint32_t)17U, (uint32_t)18U, (uint32_t)3U,
626 (uint32_t)5U, (uint32_t)16U, (uint32_t)8U, (uint32_t)21U, (uint32_t)24U, (uint32_t)4U,
627 (uint32_t)15U, (uint32_t)23U, (uint32_t)19U, (uint32_t)13U, (uint32_t)12U, (uint32_t)2U,
628 (uint32_t)20U, (uint32_t)14U, (uint32_t)22U, (uint32_t)9U, (uint32_t)6U, (uint32_t)1U
629 };
630
631 static const
632 uint64_t
633 keccak_rndc[24U] =
634 {
635 (uint64_t)0x0000000000000001U, (uint64_t)0x0000000000008082U, (uint64_t)0x800000000000808aU,
636 (uint64_t)0x8000000080008000U, (uint64_t)0x000000000000808bU, (uint64_t)0x0000000080000001U,
637 (uint64_t)0x8000000080008081U, (uint64_t)0x8000000000008009U, (uint64_t)0x000000000000008aU,
638 (uint64_t)0x0000000000000088U, (uint64_t)0x0000000080008009U, (uint64_t)0x000000008000000aU,
639 (uint64_t)0x000000008000808bU, (uint64_t)0x800000000000008bU, (uint64_t)0x8000000000008089U,
640 (uint64_t)0x8000000000008003U, (uint64_t)0x8000000000008002U, (uint64_t)0x8000000000000080U,
641 (uint64_t)0x000000000000800aU, (uint64_t)0x800000008000000aU, (uint64_t)0x8000000080008081U,
642 (uint64_t)0x8000000000008080U, (uint64_t)0x0000000080000001U, (uint64_t)0x8000000080008008U
643 };
644
645 void Hacl_Impl_SHA3_state_permute(uint64_t *s)
646 {
647 for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)24U; i0++)
648 {
649 uint64_t _C[5U] = { 0U };
650 KRML_MAYBE_FOR5(i,
651 (uint32_t)0U,
652 (uint32_t)5U,
653 (uint32_t)1U,
654 _C[i] =
655 s[i
656 + (uint32_t)0U]
657 ^
658 (s[i
659 + (uint32_t)5U]
660 ^ (s[i + (uint32_t)10U] ^ (s[i + (uint32_t)15U] ^ s[i + (uint32_t)20U]))););
661 KRML_MAYBE_FOR5(i1,
662 (uint32_t)0U,
663 (uint32_t)5U,
664 (uint32_t)1U,
665 uint64_t uu____0 = _C[(i1 + (uint32_t)1U) % (uint32_t)5U];
666 uint64_t
667 _D =
668 _C[(i1 + (uint32_t)4U)
669 % (uint32_t)5U]
670 ^ (uu____0 << (uint32_t)1U | uu____0 >> (uint32_t)63U);
671 KRML_MAYBE_FOR5(i,
672 (uint32_t)0U,
673 (uint32_t)5U,
674 (uint32_t)1U,
675 s[i1 + (uint32_t)5U * i] = s[i1 + (uint32_t)5U * i] ^ _D;););
676 uint64_t x = s[1U];
677 uint64_t current = x;
678 for (uint32_t i = (uint32_t)0U; i < (uint32_t)24U; i++)
679 {
680 uint32_t _Y = keccak_piln[i];
681 uint32_t r = keccak_rotc[i];
682 uint64_t temp = s[_Y];
683 uint64_t uu____1 = current;
684 s[_Y] = uu____1 << r | uu____1 >> ((uint32_t)64U - r);
685 current = temp;
686 }
687 KRML_MAYBE_FOR5(i,
688 (uint32_t)0U,
689 (uint32_t)5U,
690 (uint32_t)1U,
691 uint64_t
692 v0 =
693 s[(uint32_t)0U
694 + (uint32_t)5U * i]
695 ^ (~s[(uint32_t)1U + (uint32_t)5U * i] & s[(uint32_t)2U + (uint32_t)5U * i]);
696 uint64_t
697 v1 =
698 s[(uint32_t)1U
699 + (uint32_t)5U * i]
700 ^ (~s[(uint32_t)2U + (uint32_t)5U * i] & s[(uint32_t)3U + (uint32_t)5U * i]);
701 uint64_t
702 v2 =
703 s[(uint32_t)2U
704 + (uint32_t)5U * i]
705 ^ (~s[(uint32_t)3U + (uint32_t)5U * i] & s[(uint32_t)4U + (uint32_t)5U * i]);
706 uint64_t
707 v3 =
708 s[(uint32_t)3U
709 + (uint32_t)5U * i]
710 ^ (~s[(uint32_t)4U + (uint32_t)5U * i] & s[(uint32_t)0U + (uint32_t)5U * i]);
711 uint64_t
712 v4 =
713 s[(uint32_t)4U
714 + (uint32_t)5U * i]
715 ^ (~s[(uint32_t)0U + (uint32_t)5U * i] & s[(uint32_t)1U + (uint32_t)5U * i]);
716 s[(uint32_t)0U + (uint32_t)5U * i] = v0;
717 s[(uint32_t)1U + (uint32_t)5U * i] = v1;
718 s[(uint32_t)2U + (uint32_t)5U * i] = v2;
719 s[(uint32_t)3U + (uint32_t)5U * i] = v3;
720 s[(uint32_t)4U + (uint32_t)5U * i] = v4;);
721 uint64_t c = keccak_rndc[i0];
722 s[0U] = s[0U] ^ c;
723 }
724 }
725
726 void Hacl_Impl_SHA3_loadState(uint32_t rateInBytes, uint8_t *input, uint64_t *s)
727 {
728 uint8_t block[200U] = { 0U };
729 memcpy(block, input, rateInBytes * sizeof (uint8_t));
730 for (uint32_t i = (uint32_t)0U; i < (uint32_t)25U; i++)
731 {
732 uint64_t u = load64_le(block + i * (uint32_t)8U);
733 uint64_t x = u;
734 s[i] = s[i] ^ x;
735 }
736 }
737
738 static void storeState(uint32_t rateInBytes, uint64_t *s, uint8_t *res)
739 {
740 uint8_t block[200U] = { 0U };
741 for (uint32_t i = (uint32_t)0U; i < (uint32_t)25U; i++)
742 {
743 uint64_t sj = s[i];
744 store64_le(block + i * (uint32_t)8U, sj);
745 }
746 memcpy(res, block, rateInBytes * sizeof (uint8_t));
747 }
748
749 void Hacl_Impl_SHA3_absorb_inner(uint32_t rateInBytes, uint8_t *block, uint64_t *s)
750 {
751 Hacl_Impl_SHA3_loadState(rateInBytes, block, s);
752 Hacl_Impl_SHA3_state_permute(s);
753 }
754
755 static void
756 absorb(
757 uint64_t *s,
758 uint32_t rateInBytes,
759 uint32_t inputByteLen,
760 uint8_t *input,
761 uint8_t delimitedSuffix
762 )
763 {
764 uint32_t n_blocks = inputByteLen / rateInBytes;
765 uint32_t rem = inputByteLen % rateInBytes;
766 for (uint32_t i = (uint32_t)0U; i < n_blocks; i++)
767 {
768 uint8_t *block = input + i * rateInBytes;
769 Hacl_Impl_SHA3_absorb_inner(rateInBytes, block, s);
770 }
771 uint8_t *last = input + n_blocks * rateInBytes;
772 uint8_t lastBlock_[200U] = { 0U };
773 uint8_t *lastBlock = lastBlock_;
774 memcpy(lastBlock, last, rem * sizeof (uint8_t));
775 lastBlock[rem] = delimitedSuffix;
776 Hacl_Impl_SHA3_loadState(rateInBytes, lastBlock, s);
777 if (!((delimitedSuffix & (uint8_t)0x80U) == (uint8_t)0U) && rem == rateInBytes - (uint32_t)1U)
778 {
779 Hacl_Impl_SHA3_state_permute(s);
780 }
781 uint8_t nextBlock_[200U] = { 0U };
782 uint8_t *nextBlock = nextBlock_;
783 nextBlock[rateInBytes - (uint32_t)1U] = (uint8_t)0x80U;
784 Hacl_Impl_SHA3_loadState(rateInBytes, nextBlock, s);
785 Hacl_Impl_SHA3_state_permute(s);
786 }
787
788 void
789 Hacl_Impl_SHA3_squeeze(
790 uint64_t *s,
791 uint32_t rateInBytes,
792 uint32_t outputByteLen,
793 uint8_t *output
794 )
795 {
796 uint32_t outBlocks = outputByteLen / rateInBytes;
797 uint32_t remOut = outputByteLen % rateInBytes;
798 uint8_t *last = output + outputByteLen - remOut;
799 uint8_t *blocks = output;
800 for (uint32_t i = (uint32_t)0U; i < outBlocks; i++)
801 {
802 storeState(rateInBytes, s, blocks + i * rateInBytes);
803 Hacl_Impl_SHA3_state_permute(s);
804 }
805 storeState(remOut, s, last);
806 }
807
808 void
809 Hacl_Impl_SHA3_keccak(
810 uint32_t rate,
811 uint32_t capacity,
812 uint32_t inputByteLen,
813 uint8_t *input,
814 uint8_t delimitedSuffix,
815 uint32_t outputByteLen,
816 uint8_t *output
817 )
818 {
819 uint32_t rateInBytes = rate / (uint32_t)8U;
820 uint64_t s[25U] = { 0U };
821 absorb(s, rateInBytes, inputByteLen, input, delimitedSuffix);
822 Hacl_Impl_SHA3_squeeze(s, rateInBytes, outputByteLen, output);
823 }
824