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