diff --git a/dist/msvc-compatible/Hacl_Streaming_SHA2.c b/dist/msvc-compatible/Hacl_Streaming_SHA2.c deleted file mode 100644 index 0e9172f298..0000000000 --- a/dist/msvc-compatible/Hacl_Streaming_SHA2.c +++ /dev/null @@ -1,1316 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#include "internal/Hacl_Streaming_SHA2.h" - -#include "internal/Hacl_SHA2_Generic.h" -#include "internal/Hacl_Krmllib.h" - -static inline void sha256_init(uint32_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = hash; - uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; - os[i] = x;); -} - -static inline void sha256_update0(uint8_t *b, uint32_t *hash) -{ - uint32_t hash_old[8U] = { 0U }; - uint32_t ws[16U] = { 0U }; - memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint32_t)); - uint8_t *b10 = b; - uint32_t u = load32_be(b10); - ws[0U] = u; - uint32_t u0 = load32_be(b10 + (uint32_t)4U); - ws[1U] = u0; - uint32_t u1 = load32_be(b10 + (uint32_t)8U); - ws[2U] = u1; - uint32_t u2 = load32_be(b10 + (uint32_t)12U); - ws[3U] = u2; - uint32_t u3 = load32_be(b10 + (uint32_t)16U); - ws[4U] = u3; - uint32_t u4 = load32_be(b10 + (uint32_t)20U); - ws[5U] = u4; - uint32_t u5 = load32_be(b10 + (uint32_t)24U); - ws[6U] = u5; - uint32_t u6 = load32_be(b10 + (uint32_t)28U); - ws[7U] = u6; - uint32_t u7 = load32_be(b10 + (uint32_t)32U); - ws[8U] = u7; - uint32_t u8 = load32_be(b10 + (uint32_t)36U); - ws[9U] = u8; - uint32_t u9 = load32_be(b10 + (uint32_t)40U); - ws[10U] = u9; - uint32_t u10 = load32_be(b10 + (uint32_t)44U); - ws[11U] = u10; - uint32_t u11 = load32_be(b10 + (uint32_t)48U); - ws[12U] = u11; - uint32_t u12 = load32_be(b10 + (uint32_t)52U); - ws[13U] = u12; - uint32_t u13 = load32_be(b10 + (uint32_t)56U); - ws[14U] = u13; - uint32_t u14 = load32_be(b10 + (uint32_t)60U); - ws[15U] = u14; - KRML_MAYBE_FOR4(i0, - (uint32_t)0U, - (uint32_t)4U, - (uint32_t)1U, - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256[(uint32_t)16U * i0 + i]; - uint32_t ws_t = ws[i]; - uint32_t a0 = hash[0U]; - uint32_t b0 = hash[1U]; - uint32_t c0 = hash[2U]; - uint32_t d0 = hash[3U]; - uint32_t e0 = hash[4U]; - uint32_t f0 = hash[5U]; - uint32_t g0 = hash[6U]; - uint32_t h02 = hash[7U]; - uint32_t k_e_t = k_t; - uint32_t - t1 = - h02 - + - ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U) - ^ - ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U) - ^ (e0 << (uint32_t)7U | e0 >> (uint32_t)25U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k_e_t - + ws_t; - uint32_t - t2 = - ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U) - ^ - ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U) - ^ (a0 << (uint32_t)10U | a0 >> (uint32_t)22U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - uint32_t a1 = t1 + t2; - uint32_t b1 = a0; - uint32_t c1 = b0; - uint32_t d1 = c0; - uint32_t e1 = d0 + t1; - uint32_t f1 = e0; - uint32_t g1 = f0; - uint32_t h12 = g0; - hash[0U] = a1; - hash[1U] = b1; - hash[2U] = c1; - hash[3U] = d1; - hash[4U] = e1; - hash[5U] = f1; - hash[6U] = g1; - hash[7U] = h12;); - if (i0 < (uint32_t)3U) - { - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint32_t t16 = ws[i]; - uint32_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; - uint32_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; - uint32_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; - uint32_t - s1 = - (t2 << (uint32_t)15U | t2 >> (uint32_t)17U) - ^ ((t2 << (uint32_t)13U | t2 >> (uint32_t)19U) ^ t2 >> (uint32_t)10U); - uint32_t - s0 = - (t15 << (uint32_t)25U | t15 >> (uint32_t)7U) - ^ ((t15 << (uint32_t)14U | t15 >> (uint32_t)18U) ^ t15 >> (uint32_t)3U); - ws[i] = s1 + t7 + s0 + t16;); - }); - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = hash; - uint32_t x = hash[i] + hash_old[i]; - os[i] = x;); -} - -static inline void sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) -{ - uint32_t blocks = len / (uint32_t)64U; - for (uint32_t i = (uint32_t)0U; i < blocks; i++) - { - uint8_t *b0 = b; - uint8_t *mb = b0 + i * (uint32_t)64U; - sha256_update0(mb, st); - } -} - -static inline void -sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash) -{ - uint32_t blocks; - if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U) - { - blocks = (uint32_t)1U; - } - else - { - blocks = (uint32_t)2U; - } - uint32_t fin = blocks * (uint32_t)64U; - uint8_t last[128U] = { 0U }; - uint8_t totlen_buf[8U] = { 0U }; - uint64_t total_len_bits = totlen << (uint32_t)3U; - store64_be(totlen_buf, total_len_bits); - uint8_t *b0 = b; - memcpy(last, b0, len * sizeof (uint8_t)); - last[len] = (uint8_t)0x80U; - memcpy(last + fin - (uint32_t)8U, totlen_buf, (uint32_t)8U * sizeof (uint8_t)); - uint8_t *last00 = last; - uint8_t *last10 = last + (uint32_t)64U; - uint8_t *l0 = last00; - uint8_t *l1 = last10; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - uint8_t *last0 = lb0; - uint8_t *last1 = lb1; - sha256_update0(last0, hash); - if (blocks > (uint32_t)1U) - { - sha256_update0(last1, hash); - return; - } -} - -static inline void sha256_finish(uint32_t *st, uint8_t *h) -{ - uint8_t hbuf[32U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store32_be(hbuf + i * (uint32_t)4U, st[i]);); - memcpy(h, hbuf, (uint32_t)32U * sizeof (uint8_t)); -} - -static inline void sha224_init(uint32_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = hash; - uint32_t x = Hacl_Impl_SHA2_Generic_h224[i]; - os[i] = x;); -} - -static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) -{ - sha256_update_nblocks(len, b, st); -} - -static void sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st) -{ - sha256_update_last(totlen, len, b, st); -} - -static inline void sha224_finish(uint32_t *st, uint8_t *h) -{ - uint8_t hbuf[32U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store32_be(hbuf + i * (uint32_t)4U, st[i]);); - memcpy(h, hbuf, (uint32_t)28U * sizeof (uint8_t)); -} - -void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = hash; - uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; - os[i] = x;); -} - -static inline void sha512_update(uint8_t *b, uint64_t *hash) -{ - uint64_t hash_old[8U] = { 0U }; - uint64_t ws[16U] = { 0U }; - memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint64_t)); - uint8_t *b10 = b; - uint64_t u = load64_be(b10); - ws[0U] = u; - uint64_t u0 = load64_be(b10 + (uint32_t)8U); - ws[1U] = u0; - uint64_t u1 = load64_be(b10 + (uint32_t)16U); - ws[2U] = u1; - uint64_t u2 = load64_be(b10 + (uint32_t)24U); - ws[3U] = u2; - uint64_t u3 = load64_be(b10 + (uint32_t)32U); - ws[4U] = u3; - uint64_t u4 = load64_be(b10 + (uint32_t)40U); - ws[5U] = u4; - uint64_t u5 = load64_be(b10 + (uint32_t)48U); - ws[6U] = u5; - uint64_t u6 = load64_be(b10 + (uint32_t)56U); - ws[7U] = u6; - uint64_t u7 = load64_be(b10 + (uint32_t)64U); - ws[8U] = u7; - uint64_t u8 = load64_be(b10 + (uint32_t)72U); - ws[9U] = u8; - uint64_t u9 = load64_be(b10 + (uint32_t)80U); - ws[10U] = u9; - uint64_t u10 = load64_be(b10 + (uint32_t)88U); - ws[11U] = u10; - uint64_t u11 = load64_be(b10 + (uint32_t)96U); - ws[12U] = u11; - uint64_t u12 = load64_be(b10 + (uint32_t)104U); - ws[13U] = u12; - uint64_t u13 = load64_be(b10 + (uint32_t)112U); - ws[14U] = u13; - uint64_t u14 = load64_be(b10 + (uint32_t)120U); - ws[15U] = u14; - KRML_MAYBE_FOR5(i0, - (uint32_t)0U, - (uint32_t)5U, - (uint32_t)1U, - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512[(uint32_t)16U * i0 + i]; - uint64_t ws_t = ws[i]; - uint64_t a0 = hash[0U]; - uint64_t b0 = hash[1U]; - uint64_t c0 = hash[2U]; - uint64_t d0 = hash[3U]; - uint64_t e0 = hash[4U]; - uint64_t f0 = hash[5U]; - uint64_t g0 = hash[6U]; - uint64_t h02 = hash[7U]; - uint64_t k_e_t = k_t; - uint64_t - t1 = - h02 - + - ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U) - ^ - ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U) - ^ (e0 << (uint32_t)23U | e0 >> (uint32_t)41U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k_e_t - + ws_t; - uint64_t - t2 = - ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U) - ^ - ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U) - ^ (a0 << (uint32_t)25U | a0 >> (uint32_t)39U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - uint64_t a1 = t1 + t2; - uint64_t b1 = a0; - uint64_t c1 = b0; - uint64_t d1 = c0; - uint64_t e1 = d0 + t1; - uint64_t f1 = e0; - uint64_t g1 = f0; - uint64_t h12 = g0; - hash[0U] = a1; - hash[1U] = b1; - hash[2U] = c1; - hash[3U] = d1; - hash[4U] = e1; - hash[5U] = f1; - hash[6U] = g1; - hash[7U] = h12;); - if (i0 < (uint32_t)4U) - { - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint64_t t16 = ws[i]; - uint64_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; - uint64_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; - uint64_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; - uint64_t - s1 = - (t2 << (uint32_t)45U | t2 >> (uint32_t)19U) - ^ ((t2 << (uint32_t)3U | t2 >> (uint32_t)61U) ^ t2 >> (uint32_t)6U); - uint64_t - s0 = - (t15 << (uint32_t)63U | t15 >> (uint32_t)1U) - ^ ((t15 << (uint32_t)56U | t15 >> (uint32_t)8U) ^ t15 >> (uint32_t)7U); - ws[i] = s1 + t7 + s0 + t16;); - }); - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = hash; - uint64_t x = hash[i] + hash_old[i]; - os[i] = x;); -} - -static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) -{ - uint32_t blocks = len / (uint32_t)128U; - for (uint32_t i = (uint32_t)0U; i < blocks; i++) - { - uint8_t *b0 = b; - uint8_t *mb = b0 + i * (uint32_t)128U; - sha512_update(mb, st); - } -} - -static inline void -sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash) -{ - uint32_t blocks; - if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U) - { - blocks = (uint32_t)1U; - } - else - { - blocks = (uint32_t)2U; - } - uint32_t fin = blocks * (uint32_t)128U; - uint8_t last[256U] = { 0U }; - uint8_t totlen_buf[16U] = { 0U }; - FStar_UInt128_uint128 total_len_bits = FStar_UInt128_shift_left(totlen, (uint32_t)3U); - store128_be(totlen_buf, total_len_bits); - uint8_t *b0 = b; - memcpy(last, b0, len * sizeof (uint8_t)); - last[len] = (uint8_t)0x80U; - memcpy(last + fin - (uint32_t)16U, totlen_buf, (uint32_t)16U * sizeof (uint8_t)); - uint8_t *last00 = last; - uint8_t *last10 = last + (uint32_t)128U; - uint8_t *l0 = last00; - uint8_t *l1 = last10; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - uint8_t *last0 = lb0; - uint8_t *last1 = lb1; - sha512_update(last0, hash); - if (blocks > (uint32_t)1U) - { - sha512_update(last1, hash); - return; - } -} - -static inline void sha512_finish(uint64_t *st, uint8_t *h) -{ - uint8_t hbuf[64U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store64_be(hbuf + i * (uint32_t)8U, st[i]);); - memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t)); -} - -static inline void sha384_init(uint64_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = hash; - uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; - os[i] = x;); -} - -static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) -{ - sha512_update_nblocks(len, b, st); -} - -static void -sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st) -{ - sha512_update_last(totlen, len, b, st); -} - -static inline void sha384_finish(uint64_t *st, uint8_t *h) -{ - uint8_t hbuf[64U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store64_be(hbuf + i * (uint32_t)8U, st[i]);); - memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t)); -} - -/** -Allocate initial state for the SHA2_256 hash. The state is to be freed by -calling `free_256`. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - sha256_init(block_state); - return p; -} - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_256`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0) -{ - Hacl_Streaming_MD_state_32 scrut = *s0; - uint32_t *block_state0 = scrut.block_state; - uint8_t *buf0 = scrut.buf; - uint64_t total_len0 = scrut.total_len; - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); - memcpy(buf, buf0, (uint32_t)64U * sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); - memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - return p; -} - -/** -Reset an existing state to the initial hash state with empty data. -*/ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) -{ - Hacl_Streaming_MD_state_32 scrut = *s; - uint8_t *buf = scrut.buf; - uint32_t *block_state = scrut.block_state; - sha256_init(block_state); - Hacl_Streaming_MD_state_32 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -static inline uint32_t -update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) -{ - Hacl_Streaming_MD_state_32 s = *p; - uint64_t total_len = s.total_len; - if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len) - { - return (uint32_t)1U; - } - uint32_t sz; - if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U) - { - sz = (uint32_t)64U; - } - else - { - sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); - } - if (len <= (uint32_t)64U - sz) - { - Hacl_Streaming_MD_state_32 s1 = *p; - uint32_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)64U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); - } - uint8_t *buf2 = buf + sz1; - memcpy(buf2, data, len * sizeof (uint8_t)); - uint64_t total_len2 = total_len1 + (uint64_t)len; - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len2 - } - ); - } - else if (sz == (uint32_t)0U) - { - Hacl_Streaming_MD_state_32 s1 = *p; - uint32_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)64U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha256_update_nblocks((uint32_t)64U, buf, block_state1); - } - uint32_t ite; - if ((uint64_t)len % (uint64_t)(uint32_t)64U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U) - { - ite = (uint32_t)64U; - } - else - { - ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)64U); - } - uint32_t n_blocks = (len - ite) / (uint32_t)64U; - uint32_t data1_len = n_blocks * (uint32_t)64U; - uint32_t data2_len = len - data1_len; - uint8_t *data1 = data; - uint8_t *data2 = data + data1_len; - sha256_update_nblocks(data1_len, data1, block_state1); - uint8_t *dst = buf; - memcpy(dst, data2, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)len - } - ); - } - else - { - uint32_t diff = (uint32_t)64U - sz; - uint8_t *data1 = data; - uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_32 s1 = *p; - uint32_t *block_state10 = s1.block_state; - uint8_t *buf0 = s1.buf; - uint64_t total_len10 = s1.total_len; - uint32_t sz10; - if (total_len10 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len10 > (uint64_t)0U) - { - sz10 = (uint32_t)64U; - } - else - { - sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)64U); - } - uint8_t *buf2 = buf0 + sz10; - memcpy(buf2, data1, diff * sizeof (uint8_t)); - uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state10, - .buf = buf0, - .total_len = total_len2 - } - ); - Hacl_Streaming_MD_state_32 s10 = *p; - uint32_t *block_state1 = s10.block_state; - uint8_t *buf = s10.buf; - uint64_t total_len1 = s10.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)64U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha256_update_nblocks((uint32_t)64U, buf, block_state1); - } - uint32_t ite; - if - ( - (uint64_t)(len - diff) - % (uint64_t)(uint32_t)64U - == (uint64_t)0U - && (uint64_t)(len - diff) > (uint64_t)0U - ) - { - ite = (uint32_t)64U; - } - else - { - ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)64U); - } - uint32_t n_blocks = (len - diff - ite) / (uint32_t)64U; - uint32_t data1_len = n_blocks * (uint32_t)64U; - uint32_t data2_len = len - diff - data1_len; - uint8_t *data11 = data2; - uint8_t *data21 = data2 + data1_len; - sha256_update_nblocks(data1_len, data11, block_state1); - uint8_t *dst = buf; - memcpy(dst, data21, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)(len - diff) - } - ); - } - return (uint32_t)0U; -} - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ -uint32_t -Hacl_Streaming_SHA2_update_256( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_224_256(p, input, input_len); -} - -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_32 scrut = *p; - uint32_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)64U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); - } - uint8_t *buf_1 = buf_; - uint32_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t)); - uint32_t ite; - if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)64U; - } - else - { - ite = r % (uint32_t)64U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha256_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha256_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state); - sha256_finish(tmp_block_state, dst); -} - -/** -Free a state allocated with `create_in_256`. - -This function is identical to the free function for SHA2_224. -*/ -void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s) -{ - Hacl_Streaming_MD_state_32 scrut = *s; - uint8_t *buf = scrut.buf; - uint32_t *block_state = scrut.block_state; - KRML_HOST_FREE(block_state); - KRML_HOST_FREE(buf); - KRML_HOST_FREE(s); -} - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ -void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint32_t st[8U] = { 0U }; - sha256_init(st); - uint32_t rem = input_len % (uint32_t)64U; - uint64_t len_ = (uint64_t)input_len; - sha256_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)64U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha256_update_last(len_, rem, lb, st); - sha256_finish(st, rb); -} - -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - sha224_init(block_state); - return p; -} - -void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) -{ - Hacl_Streaming_MD_state_32 scrut = *s; - uint8_t *buf = scrut.buf; - uint32_t *block_state = scrut.block_state; - sha224_init(block_state); - Hacl_Streaming_MD_state_32 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -uint32_t -Hacl_Streaming_SHA2_update_224( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_224_256(p, input, input_len); -} - -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_32 scrut = *p; - uint32_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)64U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); - } - uint8_t *buf_1 = buf_; - uint32_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t)); - uint32_t ite; - if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)64U; - } - else - { - ite = r % (uint32_t)64U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha224_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha224_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state); - sha224_finish(tmp_block_state, dst); -} - -void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p) -{ - Hacl_Streaming_SHA2_free_256(p); -} - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ -void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint32_t st[8U] = { 0U }; - sha224_init(st); - uint32_t rem = input_len % (uint32_t)64U; - uint64_t len_ = (uint64_t)input_len; - sha224_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)64U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha224_update_last(len_, rem, lb, st); - sha224_finish(st, rb); -} - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - Hacl_SHA2_Scalar32_sha512_init(block_state); - return p; -} - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_512`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0) -{ - Hacl_Streaming_MD_state_64 scrut = *s0; - uint64_t *block_state0 = scrut.block_state; - uint8_t *buf0 = scrut.buf; - uint64_t total_len0 = scrut.total_len; - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t)); - memcpy(buf, buf0, (uint32_t)128U * sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t)); - memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - return p; -} - -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) -{ - Hacl_Streaming_MD_state_64 scrut = *s; - uint8_t *buf = scrut.buf; - uint64_t *block_state = scrut.block_state; - Hacl_SHA2_Scalar32_sha512_init(block_state); - Hacl_Streaming_MD_state_64 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -static inline uint32_t -update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) -{ - Hacl_Streaming_MD_state_64 s = *p; - uint64_t total_len = s.total_len; - if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len) - { - return (uint32_t)1U; - } - uint32_t sz; - if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U) - { - sz = (uint32_t)128U; - } - else - { - sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); - } - if (len <= (uint32_t)128U - sz) - { - Hacl_Streaming_MD_state_64 s1 = *p; - uint64_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)128U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); - } - uint8_t *buf2 = buf + sz1; - memcpy(buf2, data, len * sizeof (uint8_t)); - uint64_t total_len2 = total_len1 + (uint64_t)len; - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len2 - } - ); - } - else if (sz == (uint32_t)0U) - { - Hacl_Streaming_MD_state_64 s1 = *p; - uint64_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)128U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha512_update_nblocks((uint32_t)128U, buf, block_state1); - } - uint32_t ite; - if ((uint64_t)len % (uint64_t)(uint32_t)128U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U) - { - ite = (uint32_t)128U; - } - else - { - ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)128U); - } - uint32_t n_blocks = (len - ite) / (uint32_t)128U; - uint32_t data1_len = n_blocks * (uint32_t)128U; - uint32_t data2_len = len - data1_len; - uint8_t *data1 = data; - uint8_t *data2 = data + data1_len; - sha512_update_nblocks(data1_len, data1, block_state1); - uint8_t *dst = buf; - memcpy(dst, data2, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)len - } - ); - } - else - { - uint32_t diff = (uint32_t)128U - sz; - uint8_t *data1 = data; - uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_64 s1 = *p; - uint64_t *block_state10 = s1.block_state; - uint8_t *buf0 = s1.buf; - uint64_t total_len10 = s1.total_len; - uint32_t sz10; - if (total_len10 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len10 > (uint64_t)0U) - { - sz10 = (uint32_t)128U; - } - else - { - sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)128U); - } - uint8_t *buf2 = buf0 + sz10; - memcpy(buf2, data1, diff * sizeof (uint8_t)); - uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state10, - .buf = buf0, - .total_len = total_len2 - } - ); - Hacl_Streaming_MD_state_64 s10 = *p; - uint64_t *block_state1 = s10.block_state; - uint8_t *buf = s10.buf; - uint64_t total_len1 = s10.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)128U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha512_update_nblocks((uint32_t)128U, buf, block_state1); - } - uint32_t ite; - if - ( - (uint64_t)(len - diff) - % (uint64_t)(uint32_t)128U - == (uint64_t)0U - && (uint64_t)(len - diff) > (uint64_t)0U - ) - { - ite = (uint32_t)128U; - } - else - { - ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)128U); - } - uint32_t n_blocks = (len - diff - ite) / (uint32_t)128U; - uint32_t data1_len = n_blocks * (uint32_t)128U; - uint32_t data2_len = len - diff - data1_len; - uint8_t *data11 = data2; - uint8_t *data21 = data2 + data1_len; - sha512_update_nblocks(data1_len, data11, block_state1); - uint8_t *dst = buf; - memcpy(dst, data21, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)(len - diff) - } - ); - } - return (uint32_t)0U; -} - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ -uint32_t -Hacl_Streaming_SHA2_update_512( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_384_512(p, input, input_len); -} - -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_64 scrut = *p; - uint64_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)128U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); - } - uint8_t *buf_1 = buf_; - uint64_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t)); - uint32_t ite; - if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)128U; - } - else - { - ite = r % (uint32_t)128U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha512_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha512_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last), - FStar_UInt128_uint64_to_uint128((uint64_t)r)), - r, - buf_last, - tmp_block_state); - sha512_finish(tmp_block_state, dst); -} - -/** -Free a state allocated with `create_in_512`. - -This function is identical to the free function for SHA2_384. -*/ -void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s) -{ - Hacl_Streaming_MD_state_64 scrut = *s; - uint8_t *buf = scrut.buf; - uint64_t *block_state = scrut.block_state; - KRML_HOST_FREE(block_state); - KRML_HOST_FREE(buf); - KRML_HOST_FREE(s); -} - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. -*/ -void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint64_t st[8U] = { 0U }; - Hacl_SHA2_Scalar32_sha512_init(st); - uint32_t rem = input_len % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); - sha512_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)128U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha512_update_last(len_, rem, lb, st); - sha512_finish(st, rb); -} - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - sha384_init(block_state); - return p; -} - -void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) -{ - Hacl_Streaming_MD_state_64 scrut = *s; - uint8_t *buf = scrut.buf; - uint64_t *block_state = scrut.block_state; - sha384_init(block_state); - Hacl_Streaming_MD_state_64 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -uint32_t -Hacl_Streaming_SHA2_update_384( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_384_512(p, input, input_len); -} - -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_64 scrut = *p; - uint64_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)128U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); - } - uint8_t *buf_1 = buf_; - uint64_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t)); - uint32_t ite; - if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)128U; - } - else - { - ite = r % (uint32_t)128U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha384_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha384_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last), - FStar_UInt128_uint64_to_uint128((uint64_t)r)), - r, - buf_last, - tmp_block_state); - sha384_finish(tmp_block_state, dst); -} - -void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p) -{ - Hacl_Streaming_SHA2_free_512(p); -} - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. -*/ -void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint64_t st[8U] = { 0U }; - sha384_init(st); - uint32_t rem = input_len % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); - sha384_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)128U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha384_update_last(len_, rem, lb, st); - sha384_finish(st, rb); -} - diff --git a/dist/msvc-compatible/Hacl_Streaming_SHA2.h b/dist/msvc-compatible/Hacl_Streaming_SHA2.h deleted file mode 100644 index 02517c0b27..0000000000 --- a/dist/msvc-compatible/Hacl_Streaming_SHA2.h +++ /dev/null @@ -1,203 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __Hacl_Streaming_SHA2_H -#define __Hacl_Streaming_SHA2_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - -#include "Hacl_Streaming_Types.h" -#include "Hacl_Krmllib.h" - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_224; - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_256; - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_384; - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_512; - -/** -Allocate initial state for the SHA2_256 hash. The state is to be freed by -calling `free_256`. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void); - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_256`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0); - -/** -Reset an existing state to the initial hash state with empty data. -*/ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s); - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ -uint32_t -Hacl_Streaming_SHA2_update_256( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -); - -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst); - -/** -Free a state allocated with `create_in_256`. - -This function is identical to the free function for SHA2_224. -*/ -void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s); - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ -void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst); - -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void); - -void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s); - -uint32_t -Hacl_Streaming_SHA2_update_224( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -); - -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst); - -void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p); - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ -void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst); - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void); - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_512`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0); - -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s); - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ -uint32_t -Hacl_Streaming_SHA2_update_512( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -); - -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst); - -/** -Free a state allocated with `create_in_512`. - -This function is identical to the free function for SHA2_384. -*/ -void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s); - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. -*/ -void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst); - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void); - -void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s); - -uint32_t -Hacl_Streaming_SHA2_update_384( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -); - -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst); - -void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p); - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. -*/ -void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst); - -#if defined(__cplusplus) -} -#endif - -#define __Hacl_Streaming_SHA2_H_DEFINED -#endif diff --git a/dist/msvc-compatible/internal/Hacl_SHA2_Generic.h b/dist/msvc-compatible/internal/Hacl_SHA2_Generic.h deleted file mode 100644 index c21d3c89af..0000000000 --- a/dist/msvc-compatible/internal/Hacl_SHA2_Generic.h +++ /dev/null @@ -1,132 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __internal_Hacl_SHA2_Generic_H -#define __internal_Hacl_SHA2_Generic_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - -static const -uint32_t -Hacl_Impl_SHA2_Generic_h224[8U] = - { - (uint32_t)0xc1059ed8U, (uint32_t)0x367cd507U, (uint32_t)0x3070dd17U, (uint32_t)0xf70e5939U, - (uint32_t)0xffc00b31U, (uint32_t)0x68581511U, (uint32_t)0x64f98fa7U, (uint32_t)0xbefa4fa4U - }; - -static const -uint32_t -Hacl_Impl_SHA2_Generic_h256[8U] = - { - (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, (uint32_t)0xa54ff53aU, - (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U - }; - -static const -uint64_t -Hacl_Impl_SHA2_Generic_h384[8U] = - { - (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, (uint64_t)0x9159015a3070dd17U, - (uint64_t)0x152fecd8f70e5939U, (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, - (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U - }; - -static const -uint64_t -Hacl_Impl_SHA2_Generic_h512[8U] = - { - (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, (uint64_t)0x3c6ef372fe94f82bU, - (uint64_t)0xa54ff53a5f1d36f1U, (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, - (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U - }; - -static const -uint32_t -Hacl_Impl_SHA2_Generic_k224_256[64U] = - { - (uint32_t)0x428a2f98U, (uint32_t)0x71374491U, (uint32_t)0xb5c0fbcfU, (uint32_t)0xe9b5dba5U, - (uint32_t)0x3956c25bU, (uint32_t)0x59f111f1U, (uint32_t)0x923f82a4U, (uint32_t)0xab1c5ed5U, - (uint32_t)0xd807aa98U, (uint32_t)0x12835b01U, (uint32_t)0x243185beU, (uint32_t)0x550c7dc3U, - (uint32_t)0x72be5d74U, (uint32_t)0x80deb1feU, (uint32_t)0x9bdc06a7U, (uint32_t)0xc19bf174U, - (uint32_t)0xe49b69c1U, (uint32_t)0xefbe4786U, (uint32_t)0x0fc19dc6U, (uint32_t)0x240ca1ccU, - (uint32_t)0x2de92c6fU, (uint32_t)0x4a7484aaU, (uint32_t)0x5cb0a9dcU, (uint32_t)0x76f988daU, - (uint32_t)0x983e5152U, (uint32_t)0xa831c66dU, (uint32_t)0xb00327c8U, (uint32_t)0xbf597fc7U, - (uint32_t)0xc6e00bf3U, (uint32_t)0xd5a79147U, (uint32_t)0x06ca6351U, (uint32_t)0x14292967U, - (uint32_t)0x27b70a85U, (uint32_t)0x2e1b2138U, (uint32_t)0x4d2c6dfcU, (uint32_t)0x53380d13U, - (uint32_t)0x650a7354U, (uint32_t)0x766a0abbU, (uint32_t)0x81c2c92eU, (uint32_t)0x92722c85U, - (uint32_t)0xa2bfe8a1U, (uint32_t)0xa81a664bU, (uint32_t)0xc24b8b70U, (uint32_t)0xc76c51a3U, - (uint32_t)0xd192e819U, (uint32_t)0xd6990624U, (uint32_t)0xf40e3585U, (uint32_t)0x106aa070U, - (uint32_t)0x19a4c116U, (uint32_t)0x1e376c08U, (uint32_t)0x2748774cU, (uint32_t)0x34b0bcb5U, - (uint32_t)0x391c0cb3U, (uint32_t)0x4ed8aa4aU, (uint32_t)0x5b9cca4fU, (uint32_t)0x682e6ff3U, - (uint32_t)0x748f82eeU, (uint32_t)0x78a5636fU, (uint32_t)0x84c87814U, (uint32_t)0x8cc70208U, - (uint32_t)0x90befffaU, (uint32_t)0xa4506cebU, (uint32_t)0xbef9a3f7U, (uint32_t)0xc67178f2U - }; - -static const -uint64_t -Hacl_Impl_SHA2_Generic_k384_512[80U] = - { - (uint64_t)0x428a2f98d728ae22U, (uint64_t)0x7137449123ef65cdU, (uint64_t)0xb5c0fbcfec4d3b2fU, - (uint64_t)0xe9b5dba58189dbbcU, (uint64_t)0x3956c25bf348b538U, (uint64_t)0x59f111f1b605d019U, - (uint64_t)0x923f82a4af194f9bU, (uint64_t)0xab1c5ed5da6d8118U, (uint64_t)0xd807aa98a3030242U, - (uint64_t)0x12835b0145706fbeU, (uint64_t)0x243185be4ee4b28cU, (uint64_t)0x550c7dc3d5ffb4e2U, - (uint64_t)0x72be5d74f27b896fU, (uint64_t)0x80deb1fe3b1696b1U, (uint64_t)0x9bdc06a725c71235U, - (uint64_t)0xc19bf174cf692694U, (uint64_t)0xe49b69c19ef14ad2U, (uint64_t)0xefbe4786384f25e3U, - (uint64_t)0x0fc19dc68b8cd5b5U, (uint64_t)0x240ca1cc77ac9c65U, (uint64_t)0x2de92c6f592b0275U, - (uint64_t)0x4a7484aa6ea6e483U, (uint64_t)0x5cb0a9dcbd41fbd4U, (uint64_t)0x76f988da831153b5U, - (uint64_t)0x983e5152ee66dfabU, (uint64_t)0xa831c66d2db43210U, (uint64_t)0xb00327c898fb213fU, - (uint64_t)0xbf597fc7beef0ee4U, (uint64_t)0xc6e00bf33da88fc2U, (uint64_t)0xd5a79147930aa725U, - (uint64_t)0x06ca6351e003826fU, (uint64_t)0x142929670a0e6e70U, (uint64_t)0x27b70a8546d22ffcU, - (uint64_t)0x2e1b21385c26c926U, (uint64_t)0x4d2c6dfc5ac42aedU, (uint64_t)0x53380d139d95b3dfU, - (uint64_t)0x650a73548baf63deU, (uint64_t)0x766a0abb3c77b2a8U, (uint64_t)0x81c2c92e47edaee6U, - (uint64_t)0x92722c851482353bU, (uint64_t)0xa2bfe8a14cf10364U, (uint64_t)0xa81a664bbc423001U, - (uint64_t)0xc24b8b70d0f89791U, (uint64_t)0xc76c51a30654be30U, (uint64_t)0xd192e819d6ef5218U, - (uint64_t)0xd69906245565a910U, (uint64_t)0xf40e35855771202aU, (uint64_t)0x106aa07032bbd1b8U, - (uint64_t)0x19a4c116b8d2d0c8U, (uint64_t)0x1e376c085141ab53U, (uint64_t)0x2748774cdf8eeb99U, - (uint64_t)0x34b0bcb5e19b48a8U, (uint64_t)0x391c0cb3c5c95a63U, (uint64_t)0x4ed8aa4ae3418acbU, - (uint64_t)0x5b9cca4f7763e373U, (uint64_t)0x682e6ff3d6b2b8a3U, (uint64_t)0x748f82ee5defb2fcU, - (uint64_t)0x78a5636f43172f60U, (uint64_t)0x84c87814a1f0ab72U, (uint64_t)0x8cc702081a6439ecU, - (uint64_t)0x90befffa23631e28U, (uint64_t)0xa4506cebde82bde9U, (uint64_t)0xbef9a3f7b2c67915U, - (uint64_t)0xc67178f2e372532bU, (uint64_t)0xca273eceea26619cU, (uint64_t)0xd186b8c721c0c207U, - (uint64_t)0xeada7dd6cde0eb1eU, (uint64_t)0xf57d4f7fee6ed178U, (uint64_t)0x06f067aa72176fbaU, - (uint64_t)0x0a637dc5a2c898a6U, (uint64_t)0x113f9804bef90daeU, (uint64_t)0x1b710b35131c471bU, - (uint64_t)0x28db77f523047d84U, (uint64_t)0x32caab7b40c72493U, (uint64_t)0x3c9ebe0a15c9bebcU, - (uint64_t)0x431d67c49c100d4cU, (uint64_t)0x4cc5d4becb3e42b6U, (uint64_t)0x597f299cfc657e2aU, - (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U - }; - -#if defined(__cplusplus) -} -#endif - -#define __internal_Hacl_SHA2_Generic_H_DEFINED -#endif diff --git a/dist/msvc-compatible/internal/Hacl_Streaming_SHA2.h b/dist/msvc-compatible/internal/Hacl_Streaming_SHA2.h deleted file mode 100644 index fa2e7c9229..0000000000 --- a/dist/msvc-compatible/internal/Hacl_Streaming_SHA2.h +++ /dev/null @@ -1,49 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __internal_Hacl_Streaming_SHA2_H -#define __internal_Hacl_Streaming_SHA2_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - -#include "internal/Hacl_SHA2_Generic.h" -#include "internal/Hacl_Krmllib.h" -#include "../Hacl_Streaming_SHA2.h" - -void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash); - -#if defined(__cplusplus) -} -#endif - -#define __internal_Hacl_Streaming_SHA2_H_DEFINED -#endif diff --git a/dist/portable-gcc-compatible/Hacl_Streaming_SHA2.c b/dist/portable-gcc-compatible/Hacl_Streaming_SHA2.c deleted file mode 100644 index fbbdc410bc..0000000000 --- a/dist/portable-gcc-compatible/Hacl_Streaming_SHA2.c +++ /dev/null @@ -1,1500 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#include "internal/Hacl_Streaming_SHA2.h" - -#include "internal/Hacl_SHA2_Generic.h" -#include "internal/Hacl_Krmllib.h" - -/* SNIPPET_START: sha256_init */ - -static inline void sha256_init(uint32_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = hash; - uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; - os[i] = x;); -} - -/* SNIPPET_END: sha256_init */ - -/* SNIPPET_START: sha256_update0 */ - -static inline void sha256_update0(uint8_t *b, uint32_t *hash) -{ - uint32_t hash_old[8U] = { 0U }; - uint32_t ws[16U] = { 0U }; - memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint32_t)); - uint8_t *b10 = b; - uint32_t u = load32_be(b10); - ws[0U] = u; - uint32_t u0 = load32_be(b10 + (uint32_t)4U); - ws[1U] = u0; - uint32_t u1 = load32_be(b10 + (uint32_t)8U); - ws[2U] = u1; - uint32_t u2 = load32_be(b10 + (uint32_t)12U); - ws[3U] = u2; - uint32_t u3 = load32_be(b10 + (uint32_t)16U); - ws[4U] = u3; - uint32_t u4 = load32_be(b10 + (uint32_t)20U); - ws[5U] = u4; - uint32_t u5 = load32_be(b10 + (uint32_t)24U); - ws[6U] = u5; - uint32_t u6 = load32_be(b10 + (uint32_t)28U); - ws[7U] = u6; - uint32_t u7 = load32_be(b10 + (uint32_t)32U); - ws[8U] = u7; - uint32_t u8 = load32_be(b10 + (uint32_t)36U); - ws[9U] = u8; - uint32_t u9 = load32_be(b10 + (uint32_t)40U); - ws[10U] = u9; - uint32_t u10 = load32_be(b10 + (uint32_t)44U); - ws[11U] = u10; - uint32_t u11 = load32_be(b10 + (uint32_t)48U); - ws[12U] = u11; - uint32_t u12 = load32_be(b10 + (uint32_t)52U); - ws[13U] = u12; - uint32_t u13 = load32_be(b10 + (uint32_t)56U); - ws[14U] = u13; - uint32_t u14 = load32_be(b10 + (uint32_t)60U); - ws[15U] = u14; - KRML_MAYBE_FOR4(i0, - (uint32_t)0U, - (uint32_t)4U, - (uint32_t)1U, - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256[(uint32_t)16U * i0 + i]; - uint32_t ws_t = ws[i]; - uint32_t a0 = hash[0U]; - uint32_t b0 = hash[1U]; - uint32_t c0 = hash[2U]; - uint32_t d0 = hash[3U]; - uint32_t e0 = hash[4U]; - uint32_t f0 = hash[5U]; - uint32_t g0 = hash[6U]; - uint32_t h02 = hash[7U]; - uint32_t k_e_t = k_t; - uint32_t - t1 = - h02 - + - ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U) - ^ - ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U) - ^ (e0 << (uint32_t)7U | e0 >> (uint32_t)25U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k_e_t - + ws_t; - uint32_t - t2 = - ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U) - ^ - ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U) - ^ (a0 << (uint32_t)10U | a0 >> (uint32_t)22U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - uint32_t a1 = t1 + t2; - uint32_t b1 = a0; - uint32_t c1 = b0; - uint32_t d1 = c0; - uint32_t e1 = d0 + t1; - uint32_t f1 = e0; - uint32_t g1 = f0; - uint32_t h12 = g0; - hash[0U] = a1; - hash[1U] = b1; - hash[2U] = c1; - hash[3U] = d1; - hash[4U] = e1; - hash[5U] = f1; - hash[6U] = g1; - hash[7U] = h12;); - if (i0 < (uint32_t)3U) - { - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint32_t t16 = ws[i]; - uint32_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; - uint32_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; - uint32_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; - uint32_t - s1 = - (t2 << (uint32_t)15U | t2 >> (uint32_t)17U) - ^ ((t2 << (uint32_t)13U | t2 >> (uint32_t)19U) ^ t2 >> (uint32_t)10U); - uint32_t - s0 = - (t15 << (uint32_t)25U | t15 >> (uint32_t)7U) - ^ ((t15 << (uint32_t)14U | t15 >> (uint32_t)18U) ^ t15 >> (uint32_t)3U); - ws[i] = s1 + t7 + s0 + t16;); - }); - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = hash; - uint32_t x = hash[i] + hash_old[i]; - os[i] = x;); -} - -/* SNIPPET_END: sha256_update0 */ - -/* SNIPPET_START: sha256_update_nblocks */ - -static inline void sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) -{ - uint32_t blocks = len / (uint32_t)64U; - for (uint32_t i = (uint32_t)0U; i < blocks; i++) - { - uint8_t *b0 = b; - uint8_t *mb = b0 + i * (uint32_t)64U; - sha256_update0(mb, st); - } -} - -/* SNIPPET_END: sha256_update_nblocks */ - -/* SNIPPET_START: sha256_update_last */ - -static inline void -sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash) -{ - uint32_t blocks; - if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U) - { - blocks = (uint32_t)1U; - } - else - { - blocks = (uint32_t)2U; - } - uint32_t fin = blocks * (uint32_t)64U; - uint8_t last[128U] = { 0U }; - uint8_t totlen_buf[8U] = { 0U }; - uint64_t total_len_bits = totlen << (uint32_t)3U; - store64_be(totlen_buf, total_len_bits); - uint8_t *b0 = b; - memcpy(last, b0, len * sizeof (uint8_t)); - last[len] = (uint8_t)0x80U; - memcpy(last + fin - (uint32_t)8U, totlen_buf, (uint32_t)8U * sizeof (uint8_t)); - uint8_t *last00 = last; - uint8_t *last10 = last + (uint32_t)64U; - uint8_t *l0 = last00; - uint8_t *l1 = last10; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - uint8_t *last0 = lb0; - uint8_t *last1 = lb1; - sha256_update0(last0, hash); - if (blocks > (uint32_t)1U) - { - sha256_update0(last1, hash); - return; - } -} - -/* SNIPPET_END: sha256_update_last */ - -/* SNIPPET_START: sha256_finish */ - -static inline void sha256_finish(uint32_t *st, uint8_t *h) -{ - uint8_t hbuf[32U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store32_be(hbuf + i * (uint32_t)4U, st[i]);); - memcpy(h, hbuf, (uint32_t)32U * sizeof (uint8_t)); -} - -/* SNIPPET_END: sha256_finish */ - -/* SNIPPET_START: sha224_init */ - -static inline void sha224_init(uint32_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = hash; - uint32_t x = Hacl_Impl_SHA2_Generic_h224[i]; - os[i] = x;); -} - -/* SNIPPET_END: sha224_init */ - -/* SNIPPET_START: sha224_update_nblocks */ - -static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) -{ - sha256_update_nblocks(len, b, st); -} - -/* SNIPPET_END: sha224_update_nblocks */ - -/* SNIPPET_START: sha224_update_last */ - -static void sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st) -{ - sha256_update_last(totlen, len, b, st); -} - -/* SNIPPET_END: sha224_update_last */ - -/* SNIPPET_START: sha224_finish */ - -static inline void sha224_finish(uint32_t *st, uint8_t *h) -{ - uint8_t hbuf[32U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store32_be(hbuf + i * (uint32_t)4U, st[i]);); - memcpy(h, hbuf, (uint32_t)28U * sizeof (uint8_t)); -} - -/* SNIPPET_END: sha224_finish */ - -/* SNIPPET_START: Hacl_SHA2_Scalar32_sha512_init */ - -void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = hash; - uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; - os[i] = x;); -} - -/* SNIPPET_END: Hacl_SHA2_Scalar32_sha512_init */ - -/* SNIPPET_START: sha512_update */ - -static inline void sha512_update(uint8_t *b, uint64_t *hash) -{ - uint64_t hash_old[8U] = { 0U }; - uint64_t ws[16U] = { 0U }; - memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint64_t)); - uint8_t *b10 = b; - uint64_t u = load64_be(b10); - ws[0U] = u; - uint64_t u0 = load64_be(b10 + (uint32_t)8U); - ws[1U] = u0; - uint64_t u1 = load64_be(b10 + (uint32_t)16U); - ws[2U] = u1; - uint64_t u2 = load64_be(b10 + (uint32_t)24U); - ws[3U] = u2; - uint64_t u3 = load64_be(b10 + (uint32_t)32U); - ws[4U] = u3; - uint64_t u4 = load64_be(b10 + (uint32_t)40U); - ws[5U] = u4; - uint64_t u5 = load64_be(b10 + (uint32_t)48U); - ws[6U] = u5; - uint64_t u6 = load64_be(b10 + (uint32_t)56U); - ws[7U] = u6; - uint64_t u7 = load64_be(b10 + (uint32_t)64U); - ws[8U] = u7; - uint64_t u8 = load64_be(b10 + (uint32_t)72U); - ws[9U] = u8; - uint64_t u9 = load64_be(b10 + (uint32_t)80U); - ws[10U] = u9; - uint64_t u10 = load64_be(b10 + (uint32_t)88U); - ws[11U] = u10; - uint64_t u11 = load64_be(b10 + (uint32_t)96U); - ws[12U] = u11; - uint64_t u12 = load64_be(b10 + (uint32_t)104U); - ws[13U] = u12; - uint64_t u13 = load64_be(b10 + (uint32_t)112U); - ws[14U] = u13; - uint64_t u14 = load64_be(b10 + (uint32_t)120U); - ws[15U] = u14; - KRML_MAYBE_FOR5(i0, - (uint32_t)0U, - (uint32_t)5U, - (uint32_t)1U, - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512[(uint32_t)16U * i0 + i]; - uint64_t ws_t = ws[i]; - uint64_t a0 = hash[0U]; - uint64_t b0 = hash[1U]; - uint64_t c0 = hash[2U]; - uint64_t d0 = hash[3U]; - uint64_t e0 = hash[4U]; - uint64_t f0 = hash[5U]; - uint64_t g0 = hash[6U]; - uint64_t h02 = hash[7U]; - uint64_t k_e_t = k_t; - uint64_t - t1 = - h02 - + - ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U) - ^ - ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U) - ^ (e0 << (uint32_t)23U | e0 >> (uint32_t)41U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k_e_t - + ws_t; - uint64_t - t2 = - ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U) - ^ - ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U) - ^ (a0 << (uint32_t)25U | a0 >> (uint32_t)39U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - uint64_t a1 = t1 + t2; - uint64_t b1 = a0; - uint64_t c1 = b0; - uint64_t d1 = c0; - uint64_t e1 = d0 + t1; - uint64_t f1 = e0; - uint64_t g1 = f0; - uint64_t h12 = g0; - hash[0U] = a1; - hash[1U] = b1; - hash[2U] = c1; - hash[3U] = d1; - hash[4U] = e1; - hash[5U] = f1; - hash[6U] = g1; - hash[7U] = h12;); - if (i0 < (uint32_t)4U) - { - KRML_MAYBE_FOR16(i, - (uint32_t)0U, - (uint32_t)16U, - (uint32_t)1U, - uint64_t t16 = ws[i]; - uint64_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; - uint64_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; - uint64_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; - uint64_t - s1 = - (t2 << (uint32_t)45U | t2 >> (uint32_t)19U) - ^ ((t2 << (uint32_t)3U | t2 >> (uint32_t)61U) ^ t2 >> (uint32_t)6U); - uint64_t - s0 = - (t15 << (uint32_t)63U | t15 >> (uint32_t)1U) - ^ ((t15 << (uint32_t)56U | t15 >> (uint32_t)8U) ^ t15 >> (uint32_t)7U); - ws[i] = s1 + t7 + s0 + t16;); - }); - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = hash; - uint64_t x = hash[i] + hash_old[i]; - os[i] = x;); -} - -/* SNIPPET_END: sha512_update */ - -/* SNIPPET_START: sha512_update_nblocks */ - -static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) -{ - uint32_t blocks = len / (uint32_t)128U; - for (uint32_t i = (uint32_t)0U; i < blocks; i++) - { - uint8_t *b0 = b; - uint8_t *mb = b0 + i * (uint32_t)128U; - sha512_update(mb, st); - } -} - -/* SNIPPET_END: sha512_update_nblocks */ - -/* SNIPPET_START: sha512_update_last */ - -static inline void -sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash) -{ - uint32_t blocks; - if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U) - { - blocks = (uint32_t)1U; - } - else - { - blocks = (uint32_t)2U; - } - uint32_t fin = blocks * (uint32_t)128U; - uint8_t last[256U] = { 0U }; - uint8_t totlen_buf[16U] = { 0U }; - FStar_UInt128_uint128 total_len_bits = FStar_UInt128_shift_left(totlen, (uint32_t)3U); - store128_be(totlen_buf, total_len_bits); - uint8_t *b0 = b; - memcpy(last, b0, len * sizeof (uint8_t)); - last[len] = (uint8_t)0x80U; - memcpy(last + fin - (uint32_t)16U, totlen_buf, (uint32_t)16U * sizeof (uint8_t)); - uint8_t *last00 = last; - uint8_t *last10 = last + (uint32_t)128U; - uint8_t *l0 = last00; - uint8_t *l1 = last10; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - uint8_t *last0 = lb0; - uint8_t *last1 = lb1; - sha512_update(last0, hash); - if (blocks > (uint32_t)1U) - { - sha512_update(last1, hash); - return; - } -} - -/* SNIPPET_END: sha512_update_last */ - -/* SNIPPET_START: sha512_finish */ - -static inline void sha512_finish(uint64_t *st, uint8_t *h) -{ - uint8_t hbuf[64U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store64_be(hbuf + i * (uint32_t)8U, st[i]);); - memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t)); -} - -/* SNIPPET_END: sha512_finish */ - -/* SNIPPET_START: sha384_init */ - -static inline void sha384_init(uint64_t *hash) -{ - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = hash; - uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; - os[i] = x;); -} - -/* SNIPPET_END: sha384_init */ - -/* SNIPPET_START: sha384_update_nblocks */ - -static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) -{ - sha512_update_nblocks(len, b, st); -} - -/* SNIPPET_END: sha384_update_nblocks */ - -/* SNIPPET_START: sha384_update_last */ - -static void -sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st) -{ - sha512_update_last(totlen, len, b, st); -} - -/* SNIPPET_END: sha384_update_last */ - -/* SNIPPET_START: sha384_finish */ - -static inline void sha384_finish(uint64_t *st, uint8_t *h) -{ - uint8_t hbuf[64U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - store64_be(hbuf + i * (uint32_t)8U, st[i]);); - memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t)); -} - -/* SNIPPET_END: sha384_finish */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_256 */ - -/** -Allocate initial state for the SHA2_256 hash. The state is to be freed by -calling `free_256`. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - sha256_init(block_state); - return p; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_copy_256 */ - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_256`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0) -{ - Hacl_Streaming_MD_state_32 scrut = *s0; - uint32_t *block_state0 = scrut.block_state; - uint8_t *buf0 = scrut.buf; - uint64_t total_len0 = scrut.total_len; - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); - memcpy(buf, buf0, (uint32_t)64U * sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); - memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - return p; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_copy_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_256 */ - -/** -Reset an existing state to the initial hash state with empty data. -*/ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) -{ - Hacl_Streaming_MD_state_32 scrut = *s; - uint8_t *buf = scrut.buf; - uint32_t *block_state = scrut.block_state; - sha256_init(block_state); - Hacl_Streaming_MD_state_32 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_256 */ - -/* SNIPPET_START: update_224_256 */ - -static inline uint32_t -update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) -{ - Hacl_Streaming_MD_state_32 s = *p; - uint64_t total_len = s.total_len; - if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len) - { - return (uint32_t)1U; - } - uint32_t sz; - if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U) - { - sz = (uint32_t)64U; - } - else - { - sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); - } - if (len <= (uint32_t)64U - sz) - { - Hacl_Streaming_MD_state_32 s1 = *p; - uint32_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)64U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); - } - uint8_t *buf2 = buf + sz1; - memcpy(buf2, data, len * sizeof (uint8_t)); - uint64_t total_len2 = total_len1 + (uint64_t)len; - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len2 - } - ); - } - else if (sz == (uint32_t)0U) - { - Hacl_Streaming_MD_state_32 s1 = *p; - uint32_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)64U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha256_update_nblocks((uint32_t)64U, buf, block_state1); - } - uint32_t ite; - if ((uint64_t)len % (uint64_t)(uint32_t)64U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U) - { - ite = (uint32_t)64U; - } - else - { - ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)64U); - } - uint32_t n_blocks = (len - ite) / (uint32_t)64U; - uint32_t data1_len = n_blocks * (uint32_t)64U; - uint32_t data2_len = len - data1_len; - uint8_t *data1 = data; - uint8_t *data2 = data + data1_len; - sha256_update_nblocks(data1_len, data1, block_state1); - uint8_t *dst = buf; - memcpy(dst, data2, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)len - } - ); - } - else - { - uint32_t diff = (uint32_t)64U - sz; - uint8_t *data1 = data; - uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_32 s1 = *p; - uint32_t *block_state10 = s1.block_state; - uint8_t *buf0 = s1.buf; - uint64_t total_len10 = s1.total_len; - uint32_t sz10; - if (total_len10 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len10 > (uint64_t)0U) - { - sz10 = (uint32_t)64U; - } - else - { - sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)64U); - } - uint8_t *buf2 = buf0 + sz10; - memcpy(buf2, data1, diff * sizeof (uint8_t)); - uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state10, - .buf = buf0, - .total_len = total_len2 - } - ); - Hacl_Streaming_MD_state_32 s10 = *p; - uint32_t *block_state1 = s10.block_state; - uint8_t *buf = s10.buf; - uint64_t total_len1 = s10.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)64U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha256_update_nblocks((uint32_t)64U, buf, block_state1); - } - uint32_t ite; - if - ( - (uint64_t)(len - diff) - % (uint64_t)(uint32_t)64U - == (uint64_t)0U - && (uint64_t)(len - diff) > (uint64_t)0U - ) - { - ite = (uint32_t)64U; - } - else - { - ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)64U); - } - uint32_t n_blocks = (len - diff - ite) / (uint32_t)64U; - uint32_t data1_len = n_blocks * (uint32_t)64U; - uint32_t data2_len = len - diff - data1_len; - uint8_t *data11 = data2; - uint8_t *data21 = data2 + data1_len; - sha256_update_nblocks(data1_len, data11, block_state1); - uint8_t *dst = buf; - memcpy(dst, data21, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_32){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)(len - diff) - } - ); - } - return (uint32_t)0U; -} - -/* SNIPPET_END: update_224_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_256 */ - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ -uint32_t -Hacl_Streaming_SHA2_update_256( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_224_256(p, input, input_len); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_256 */ - -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_32 scrut = *p; - uint32_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)64U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); - } - uint8_t *buf_1 = buf_; - uint32_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t)); - uint32_t ite; - if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)64U; - } - else - { - ite = r % (uint32_t)64U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha256_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha256_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state); - sha256_finish(tmp_block_state, dst); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_256 */ - -/** -Free a state allocated with `create_in_256`. - -This function is identical to the free function for SHA2_224. -*/ -void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s) -{ - Hacl_Streaming_MD_state_32 scrut = *s; - uint8_t *buf = scrut.buf; - uint32_t *block_state = scrut.block_state; - KRML_HOST_FREE(block_state); - KRML_HOST_FREE(buf); - KRML_HOST_FREE(s); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha256 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ -void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint32_t st[8U] = { 0U }; - sha256_init(st); - uint32_t rem = input_len % (uint32_t)64U; - uint64_t len_ = (uint64_t)input_len; - sha256_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)64U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha256_update_last(len_, rem, lb, st); - sha256_finish(st, rb); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_224 */ - -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - sha224_init(block_state); - return p; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_224 */ - -void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) -{ - Hacl_Streaming_MD_state_32 scrut = *s; - uint8_t *buf = scrut.buf; - uint32_t *block_state = scrut.block_state; - sha224_init(block_state); - Hacl_Streaming_MD_state_32 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_224 */ - -uint32_t -Hacl_Streaming_SHA2_update_224( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_224_256(p, input, input_len); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_224 */ - -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_32 scrut = *p; - uint32_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)64U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); - } - uint8_t *buf_1 = buf_; - uint32_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t)); - uint32_t ite; - if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)64U; - } - else - { - ite = r % (uint32_t)64U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha224_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha224_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state); - sha224_finish(tmp_block_state, dst); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_224 */ - -void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p) -{ - Hacl_Streaming_SHA2_free_256(p); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha224 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ -void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint32_t st[8U] = { 0U }; - sha224_init(st); - uint32_t rem = input_len % (uint32_t)64U; - uint64_t len_ = (uint64_t)input_len; - sha224_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)64U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha224_update_last(len_, rem, lb, st); - sha224_finish(st, rb); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_512 */ - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - Hacl_SHA2_Scalar32_sha512_init(block_state); - return p; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_copy_512 */ - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_512`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0) -{ - Hacl_Streaming_MD_state_64 scrut = *s0; - uint64_t *block_state0 = scrut.block_state; - uint8_t *buf0 = scrut.buf; - uint64_t total_len0 = scrut.total_len; - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t)); - memcpy(buf, buf0, (uint32_t)128U * sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t)); - memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - return p; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_copy_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_512 */ - -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) -{ - Hacl_Streaming_MD_state_64 scrut = *s; - uint8_t *buf = scrut.buf; - uint64_t *block_state = scrut.block_state; - Hacl_SHA2_Scalar32_sha512_init(block_state); - Hacl_Streaming_MD_state_64 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_512 */ - -/* SNIPPET_START: update_384_512 */ - -static inline uint32_t -update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) -{ - Hacl_Streaming_MD_state_64 s = *p; - uint64_t total_len = s.total_len; - if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len) - { - return (uint32_t)1U; - } - uint32_t sz; - if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U) - { - sz = (uint32_t)128U; - } - else - { - sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); - } - if (len <= (uint32_t)128U - sz) - { - Hacl_Streaming_MD_state_64 s1 = *p; - uint64_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)128U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); - } - uint8_t *buf2 = buf + sz1; - memcpy(buf2, data, len * sizeof (uint8_t)); - uint64_t total_len2 = total_len1 + (uint64_t)len; - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len2 - } - ); - } - else if (sz == (uint32_t)0U) - { - Hacl_Streaming_MD_state_64 s1 = *p; - uint64_t *block_state1 = s1.block_state; - uint8_t *buf = s1.buf; - uint64_t total_len1 = s1.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)128U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha512_update_nblocks((uint32_t)128U, buf, block_state1); - } - uint32_t ite; - if ((uint64_t)len % (uint64_t)(uint32_t)128U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U) - { - ite = (uint32_t)128U; - } - else - { - ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)128U); - } - uint32_t n_blocks = (len - ite) / (uint32_t)128U; - uint32_t data1_len = n_blocks * (uint32_t)128U; - uint32_t data2_len = len - data1_len; - uint8_t *data1 = data; - uint8_t *data2 = data + data1_len; - sha512_update_nblocks(data1_len, data1, block_state1); - uint8_t *dst = buf; - memcpy(dst, data2, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)len - } - ); - } - else - { - uint32_t diff = (uint32_t)128U - sz; - uint8_t *data1 = data; - uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_64 s1 = *p; - uint64_t *block_state10 = s1.block_state; - uint8_t *buf0 = s1.buf; - uint64_t total_len10 = s1.total_len; - uint32_t sz10; - if (total_len10 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len10 > (uint64_t)0U) - { - sz10 = (uint32_t)128U; - } - else - { - sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)128U); - } - uint8_t *buf2 = buf0 + sz10; - memcpy(buf2, data1, diff * sizeof (uint8_t)); - uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state10, - .buf = buf0, - .total_len = total_len2 - } - ); - Hacl_Streaming_MD_state_64 s10 = *p; - uint64_t *block_state1 = s10.block_state; - uint8_t *buf = s10.buf; - uint64_t total_len1 = s10.total_len; - uint32_t sz1; - if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U) - { - sz1 = (uint32_t)128U; - } - else - { - sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); - } - if (!(sz1 == (uint32_t)0U)) - { - sha512_update_nblocks((uint32_t)128U, buf, block_state1); - } - uint32_t ite; - if - ( - (uint64_t)(len - diff) - % (uint64_t)(uint32_t)128U - == (uint64_t)0U - && (uint64_t)(len - diff) > (uint64_t)0U - ) - { - ite = (uint32_t)128U; - } - else - { - ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)128U); - } - uint32_t n_blocks = (len - diff - ite) / (uint32_t)128U; - uint32_t data1_len = n_blocks * (uint32_t)128U; - uint32_t data2_len = len - diff - data1_len; - uint8_t *data11 = data2; - uint8_t *data21 = data2 + data1_len; - sha512_update_nblocks(data1_len, data11, block_state1); - uint8_t *dst = buf; - memcpy(dst, data21, data2_len * sizeof (uint8_t)); - *p - = - ( - (Hacl_Streaming_MD_state_64){ - .block_state = block_state1, - .buf = buf, - .total_len = total_len1 + (uint64_t)(len - diff) - } - ); - } - return (uint32_t)0U; -} - -/* SNIPPET_END: update_384_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_512 */ - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ -uint32_t -Hacl_Streaming_SHA2_update_512( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_384_512(p, input, input_len); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_512 */ - -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_64 scrut = *p; - uint64_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)128U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); - } - uint8_t *buf_1 = buf_; - uint64_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t)); - uint32_t ite; - if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)128U; - } - else - { - ite = r % (uint32_t)128U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha512_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha512_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last), - FStar_UInt128_uint64_to_uint128((uint64_t)r)), - r, - buf_last, - tmp_block_state); - sha512_finish(tmp_block_state, dst); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_512 */ - -/** -Free a state allocated with `create_in_512`. - -This function is identical to the free function for SHA2_384. -*/ -void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s) -{ - Hacl_Streaming_MD_state_64 scrut = *s; - uint8_t *buf = scrut.buf; - uint64_t *block_state = scrut.block_state; - KRML_HOST_FREE(block_state); - KRML_HOST_FREE(buf); - KRML_HOST_FREE(s); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha512 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. -*/ -void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint64_t st[8U] = { 0U }; - Hacl_SHA2_Scalar32_sha512_init(st); - uint32_t rem = input_len % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); - sha512_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)128U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha512_update_last(len_, rem, lb, st); - sha512_finish(st, rb); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_384 */ - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void) -{ - uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - sha384_init(block_state); - return p; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_384 */ - -void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) -{ - Hacl_Streaming_MD_state_64 scrut = *s; - uint8_t *buf = scrut.buf; - uint64_t *block_state = scrut.block_state; - sha384_init(block_state); - Hacl_Streaming_MD_state_64 - tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; - s[0U] = tmp; -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_384 */ - -uint32_t -Hacl_Streaming_SHA2_update_384( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -) -{ - return update_384_512(p, input, input_len); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_384 */ - -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) -{ - Hacl_Streaming_MD_state_64 scrut = *p; - uint64_t *block_state = scrut.block_state; - uint8_t *buf_ = scrut.buf; - uint64_t total_len = scrut.total_len; - uint32_t r; - if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U) - { - r = (uint32_t)128U; - } - else - { - r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); - } - uint8_t *buf_1 = buf_; - uint64_t tmp_block_state[8U] = { 0U }; - memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t)); - uint32_t ite; - if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) - { - ite = (uint32_t)128U; - } - else - { - ite = r % (uint32_t)128U; - } - uint8_t *buf_last = buf_1 + r - ite; - uint8_t *buf_multi = buf_1; - sha384_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); - uint64_t prev_len_last = total_len - (uint64_t)r; - sha384_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last), - FStar_UInt128_uint64_to_uint128((uint64_t)r)), - r, - buf_last, - tmp_block_state); - sha384_finish(tmp_block_state, dst); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_384 */ - -void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p) -{ - Hacl_Streaming_SHA2_free_512(p); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha384 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. -*/ -void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint64_t st[8U] = { 0U }; - sha384_init(st); - uint32_t rem = input_len % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); - sha384_update_nblocks(input_len, ib, st); - uint32_t rem1 = input_len % (uint32_t)128U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - sha384_update_last(len_, rem, lb, st); - sha384_finish(st, rb); -} - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha384 */ - diff --git a/dist/portable-gcc-compatible/Hacl_Streaming_SHA2.h b/dist/portable-gcc-compatible/Hacl_Streaming_SHA2.h deleted file mode 100644 index e68347ffa1..0000000000 --- a/dist/portable-gcc-compatible/Hacl_Streaming_SHA2.h +++ /dev/null @@ -1,323 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __Hacl_Streaming_SHA2_H -#define __Hacl_Streaming_SHA2_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - -#include "Hacl_Streaming_Types.h" -#include "Hacl_Krmllib.h" - -/* SNIPPET_START: Hacl_Streaming_SHA2_state_sha2_224 */ - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_224; - -/* SNIPPET_END: Hacl_Streaming_SHA2_state_sha2_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_state_sha2_256 */ - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_256; - -/* SNIPPET_END: Hacl_Streaming_SHA2_state_sha2_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_state_sha2_384 */ - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_384; - -/* SNIPPET_END: Hacl_Streaming_SHA2_state_sha2_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_state_sha2_512 */ - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_512; - -/* SNIPPET_END: Hacl_Streaming_SHA2_state_sha2_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_256 */ - -/** -Allocate initial state for the SHA2_256 hash. The state is to be freed by -calling `free_256`. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void); - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_copy_256 */ - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_256`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0); - -/* SNIPPET_END: Hacl_Streaming_SHA2_copy_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_256 */ - -/** -Reset an existing state to the initial hash state with empty data. -*/ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s); - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_256 */ - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ -uint32_t -Hacl_Streaming_SHA2_update_256( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -); - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_256 */ - -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_256 */ - -/** -Free a state allocated with `create_in_256`. - -This function is identical to the free function for SHA2_224. -*/ -void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s); - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha256 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ -void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha256 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_224 */ - -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void); - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_224 */ - -void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s); - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_224 */ - -uint32_t -Hacl_Streaming_SHA2_update_224( - Hacl_Streaming_MD_state_32 *p, - uint8_t *input, - uint32_t input_len -); - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_224 */ - -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_224 */ - -void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p); - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha224 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ -void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha224 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_512 */ - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void); - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_copy_512 */ - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_512`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0); - -/* SNIPPET_END: Hacl_Streaming_SHA2_copy_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_512 */ - -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s); - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_512 */ - -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ -uint32_t -Hacl_Streaming_SHA2_update_512( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -); - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_512 */ - -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy of -the state and therefore does not invalidate the client-held state `p`.) -*/ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_512 */ - -/** -Free a state allocated with `create_in_512`. - -This function is identical to the free function for SHA2_384. -*/ -void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s); - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha512 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. -*/ -void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha512 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_create_in_384 */ - -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void); - -/* SNIPPET_END: Hacl_Streaming_SHA2_create_in_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_init_384 */ - -void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s); - -/* SNIPPET_END: Hacl_Streaming_SHA2_init_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_update_384 */ - -uint32_t -Hacl_Streaming_SHA2_update_384( - Hacl_Streaming_MD_state_64 *p, - uint8_t *input, - uint32_t input_len -); - -/* SNIPPET_END: Hacl_Streaming_SHA2_update_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_finish_384 */ - -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_finish_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_free_384 */ - -void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p); - -/* SNIPPET_END: Hacl_Streaming_SHA2_free_384 */ - -/* SNIPPET_START: Hacl_Streaming_SHA2_sha384 */ - -/** -Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. -*/ -void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst); - -/* SNIPPET_END: Hacl_Streaming_SHA2_sha384 */ - -#if defined(__cplusplus) -} -#endif - -#define __Hacl_Streaming_SHA2_H_DEFINED -#endif diff --git a/dist/portable-gcc-compatible/internal/Hacl_SHA2_Generic.h b/dist/portable-gcc-compatible/internal/Hacl_SHA2_Generic.h deleted file mode 100644 index c200da7f29..0000000000 --- a/dist/portable-gcc-compatible/internal/Hacl_SHA2_Generic.h +++ /dev/null @@ -1,156 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __internal_Hacl_SHA2_Generic_H -#define __internal_Hacl_SHA2_Generic_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - -/* SNIPPET_START: Hacl_Impl_SHA2_Generic_h224 */ - -static const -uint32_t -Hacl_Impl_SHA2_Generic_h224[8U] = - { - (uint32_t)0xc1059ed8U, (uint32_t)0x367cd507U, (uint32_t)0x3070dd17U, (uint32_t)0xf70e5939U, - (uint32_t)0xffc00b31U, (uint32_t)0x68581511U, (uint32_t)0x64f98fa7U, (uint32_t)0xbefa4fa4U - }; - -/* SNIPPET_END: Hacl_Impl_SHA2_Generic_h224 */ - -/* SNIPPET_START: Hacl_Impl_SHA2_Generic_h256 */ - -static const -uint32_t -Hacl_Impl_SHA2_Generic_h256[8U] = - { - (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, (uint32_t)0xa54ff53aU, - (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U - }; - -/* SNIPPET_END: Hacl_Impl_SHA2_Generic_h256 */ - -/* SNIPPET_START: Hacl_Impl_SHA2_Generic_h384 */ - -static const -uint64_t -Hacl_Impl_SHA2_Generic_h384[8U] = - { - (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, (uint64_t)0x9159015a3070dd17U, - (uint64_t)0x152fecd8f70e5939U, (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, - (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U - }; - -/* SNIPPET_END: Hacl_Impl_SHA2_Generic_h384 */ - -/* SNIPPET_START: Hacl_Impl_SHA2_Generic_h512 */ - -static const -uint64_t -Hacl_Impl_SHA2_Generic_h512[8U] = - { - (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, (uint64_t)0x3c6ef372fe94f82bU, - (uint64_t)0xa54ff53a5f1d36f1U, (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, - (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U - }; - -/* SNIPPET_END: Hacl_Impl_SHA2_Generic_h512 */ - -/* SNIPPET_START: Hacl_Impl_SHA2_Generic_k224_256 */ - -static const -uint32_t -Hacl_Impl_SHA2_Generic_k224_256[64U] = - { - (uint32_t)0x428a2f98U, (uint32_t)0x71374491U, (uint32_t)0xb5c0fbcfU, (uint32_t)0xe9b5dba5U, - (uint32_t)0x3956c25bU, (uint32_t)0x59f111f1U, (uint32_t)0x923f82a4U, (uint32_t)0xab1c5ed5U, - (uint32_t)0xd807aa98U, (uint32_t)0x12835b01U, (uint32_t)0x243185beU, (uint32_t)0x550c7dc3U, - (uint32_t)0x72be5d74U, (uint32_t)0x80deb1feU, (uint32_t)0x9bdc06a7U, (uint32_t)0xc19bf174U, - (uint32_t)0xe49b69c1U, (uint32_t)0xefbe4786U, (uint32_t)0x0fc19dc6U, (uint32_t)0x240ca1ccU, - (uint32_t)0x2de92c6fU, (uint32_t)0x4a7484aaU, (uint32_t)0x5cb0a9dcU, (uint32_t)0x76f988daU, - (uint32_t)0x983e5152U, (uint32_t)0xa831c66dU, (uint32_t)0xb00327c8U, (uint32_t)0xbf597fc7U, - (uint32_t)0xc6e00bf3U, (uint32_t)0xd5a79147U, (uint32_t)0x06ca6351U, (uint32_t)0x14292967U, - (uint32_t)0x27b70a85U, (uint32_t)0x2e1b2138U, (uint32_t)0x4d2c6dfcU, (uint32_t)0x53380d13U, - (uint32_t)0x650a7354U, (uint32_t)0x766a0abbU, (uint32_t)0x81c2c92eU, (uint32_t)0x92722c85U, - (uint32_t)0xa2bfe8a1U, (uint32_t)0xa81a664bU, (uint32_t)0xc24b8b70U, (uint32_t)0xc76c51a3U, - (uint32_t)0xd192e819U, (uint32_t)0xd6990624U, (uint32_t)0xf40e3585U, (uint32_t)0x106aa070U, - (uint32_t)0x19a4c116U, (uint32_t)0x1e376c08U, (uint32_t)0x2748774cU, (uint32_t)0x34b0bcb5U, - (uint32_t)0x391c0cb3U, (uint32_t)0x4ed8aa4aU, (uint32_t)0x5b9cca4fU, (uint32_t)0x682e6ff3U, - (uint32_t)0x748f82eeU, (uint32_t)0x78a5636fU, (uint32_t)0x84c87814U, (uint32_t)0x8cc70208U, - (uint32_t)0x90befffaU, (uint32_t)0xa4506cebU, (uint32_t)0xbef9a3f7U, (uint32_t)0xc67178f2U - }; - -/* SNIPPET_END: Hacl_Impl_SHA2_Generic_k224_256 */ - -/* SNIPPET_START: Hacl_Impl_SHA2_Generic_k384_512 */ - -static const -uint64_t -Hacl_Impl_SHA2_Generic_k384_512[80U] = - { - (uint64_t)0x428a2f98d728ae22U, (uint64_t)0x7137449123ef65cdU, (uint64_t)0xb5c0fbcfec4d3b2fU, - (uint64_t)0xe9b5dba58189dbbcU, (uint64_t)0x3956c25bf348b538U, (uint64_t)0x59f111f1b605d019U, - (uint64_t)0x923f82a4af194f9bU, (uint64_t)0xab1c5ed5da6d8118U, (uint64_t)0xd807aa98a3030242U, - (uint64_t)0x12835b0145706fbeU, (uint64_t)0x243185be4ee4b28cU, (uint64_t)0x550c7dc3d5ffb4e2U, - (uint64_t)0x72be5d74f27b896fU, (uint64_t)0x80deb1fe3b1696b1U, (uint64_t)0x9bdc06a725c71235U, - (uint64_t)0xc19bf174cf692694U, (uint64_t)0xe49b69c19ef14ad2U, (uint64_t)0xefbe4786384f25e3U, - (uint64_t)0x0fc19dc68b8cd5b5U, (uint64_t)0x240ca1cc77ac9c65U, (uint64_t)0x2de92c6f592b0275U, - (uint64_t)0x4a7484aa6ea6e483U, (uint64_t)0x5cb0a9dcbd41fbd4U, (uint64_t)0x76f988da831153b5U, - (uint64_t)0x983e5152ee66dfabU, (uint64_t)0xa831c66d2db43210U, (uint64_t)0xb00327c898fb213fU, - (uint64_t)0xbf597fc7beef0ee4U, (uint64_t)0xc6e00bf33da88fc2U, (uint64_t)0xd5a79147930aa725U, - (uint64_t)0x06ca6351e003826fU, (uint64_t)0x142929670a0e6e70U, (uint64_t)0x27b70a8546d22ffcU, - (uint64_t)0x2e1b21385c26c926U, (uint64_t)0x4d2c6dfc5ac42aedU, (uint64_t)0x53380d139d95b3dfU, - (uint64_t)0x650a73548baf63deU, (uint64_t)0x766a0abb3c77b2a8U, (uint64_t)0x81c2c92e47edaee6U, - (uint64_t)0x92722c851482353bU, (uint64_t)0xa2bfe8a14cf10364U, (uint64_t)0xa81a664bbc423001U, - (uint64_t)0xc24b8b70d0f89791U, (uint64_t)0xc76c51a30654be30U, (uint64_t)0xd192e819d6ef5218U, - (uint64_t)0xd69906245565a910U, (uint64_t)0xf40e35855771202aU, (uint64_t)0x106aa07032bbd1b8U, - (uint64_t)0x19a4c116b8d2d0c8U, (uint64_t)0x1e376c085141ab53U, (uint64_t)0x2748774cdf8eeb99U, - (uint64_t)0x34b0bcb5e19b48a8U, (uint64_t)0x391c0cb3c5c95a63U, (uint64_t)0x4ed8aa4ae3418acbU, - (uint64_t)0x5b9cca4f7763e373U, (uint64_t)0x682e6ff3d6b2b8a3U, (uint64_t)0x748f82ee5defb2fcU, - (uint64_t)0x78a5636f43172f60U, (uint64_t)0x84c87814a1f0ab72U, (uint64_t)0x8cc702081a6439ecU, - (uint64_t)0x90befffa23631e28U, (uint64_t)0xa4506cebde82bde9U, (uint64_t)0xbef9a3f7b2c67915U, - (uint64_t)0xc67178f2e372532bU, (uint64_t)0xca273eceea26619cU, (uint64_t)0xd186b8c721c0c207U, - (uint64_t)0xeada7dd6cde0eb1eU, (uint64_t)0xf57d4f7fee6ed178U, (uint64_t)0x06f067aa72176fbaU, - (uint64_t)0x0a637dc5a2c898a6U, (uint64_t)0x113f9804bef90daeU, (uint64_t)0x1b710b35131c471bU, - (uint64_t)0x28db77f523047d84U, (uint64_t)0x32caab7b40c72493U, (uint64_t)0x3c9ebe0a15c9bebcU, - (uint64_t)0x431d67c49c100d4cU, (uint64_t)0x4cc5d4becb3e42b6U, (uint64_t)0x597f299cfc657e2aU, - (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U - }; - -/* SNIPPET_END: Hacl_Impl_SHA2_Generic_k384_512 */ - -#if defined(__cplusplus) -} -#endif - -#define __internal_Hacl_SHA2_Generic_H_DEFINED -#endif diff --git a/dist/portable-gcc-compatible/internal/Hacl_Streaming_SHA2.h b/dist/portable-gcc-compatible/internal/Hacl_Streaming_SHA2.h deleted file mode 100644 index 01c7749fdb..0000000000 --- a/dist/portable-gcc-compatible/internal/Hacl_Streaming_SHA2.h +++ /dev/null @@ -1,53 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation - * Copyright (c) 2022-2023 HACL* Contributors - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __internal_Hacl_Streaming_SHA2_H -#define __internal_Hacl_Streaming_SHA2_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - -#include "internal/Hacl_SHA2_Generic.h" -#include "internal/Hacl_Krmllib.h" -#include "../Hacl_Streaming_SHA2.h" - -/* SNIPPET_START: Hacl_SHA2_Scalar32_sha512_init */ - -void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash); - -/* SNIPPET_END: Hacl_SHA2_Scalar32_sha512_init */ - -#if defined(__cplusplus) -} -#endif - -#define __internal_Hacl_Streaming_SHA2_H_DEFINED -#endif diff --git a/dist/test/c/Hacl_Test_ECDSA.h b/dist/test/c/Hacl_Test_ECDSA.h index 4ef7d8d950..1a806555fb 100644 --- a/dist/test/c/Hacl_Test_ECDSA.h +++ b/dist/test/c/Hacl_Test_ECDSA.h @@ -26,6 +26,7 @@ #ifndef __Hacl_Test_ECDSA_H #define __Hacl_Test_ECDSA_H +#include "internal/Hacl_Hash_SHA2.h" #include "krmllib.h" #include "libintvector.h" #include "lib_intrinsics.h" diff --git a/dist/test/c/Hacl_Test_HMAC_DRBG.c b/dist/test/c/Hacl_Test_HMAC_DRBG.c index 73071f69d7..9f32a4a25a 100644 --- a/dist/test/c/Hacl_Test_HMAC_DRBG.c +++ b/dist/test/c/Hacl_Test_HMAC_DRBG.c @@ -42,674 +42,401 @@ typedef uint8_t hash_alg; -static uint32_t -h256[8U] = - { - (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, (uint32_t)0xa54ff53aU, - (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U - }; - -static uint64_t -h384[8U] = - { - (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, (uint64_t)0x9159015a3070dd17U, - (uint64_t)0x152fecd8f70e5939U, (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, - (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U - }; - -static uint64_t -h512[8U] = - { - (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, (uint64_t)0x3c6ef372fe94f82bU, - (uint64_t)0xa54ff53a5f1d36f1U, (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, - (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U - }; - -static uint32_t -k224_256[64U] = - { - (uint32_t)0x428a2f98U, (uint32_t)0x71374491U, (uint32_t)0xb5c0fbcfU, (uint32_t)0xe9b5dba5U, - (uint32_t)0x3956c25bU, (uint32_t)0x59f111f1U, (uint32_t)0x923f82a4U, (uint32_t)0xab1c5ed5U, - (uint32_t)0xd807aa98U, (uint32_t)0x12835b01U, (uint32_t)0x243185beU, (uint32_t)0x550c7dc3U, - (uint32_t)0x72be5d74U, (uint32_t)0x80deb1feU, (uint32_t)0x9bdc06a7U, (uint32_t)0xc19bf174U, - (uint32_t)0xe49b69c1U, (uint32_t)0xefbe4786U, (uint32_t)0x0fc19dc6U, (uint32_t)0x240ca1ccU, - (uint32_t)0x2de92c6fU, (uint32_t)0x4a7484aaU, (uint32_t)0x5cb0a9dcU, (uint32_t)0x76f988daU, - (uint32_t)0x983e5152U, (uint32_t)0xa831c66dU, (uint32_t)0xb00327c8U, (uint32_t)0xbf597fc7U, - (uint32_t)0xc6e00bf3U, (uint32_t)0xd5a79147U, (uint32_t)0x06ca6351U, (uint32_t)0x14292967U, - (uint32_t)0x27b70a85U, (uint32_t)0x2e1b2138U, (uint32_t)0x4d2c6dfcU, (uint32_t)0x53380d13U, - (uint32_t)0x650a7354U, (uint32_t)0x766a0abbU, (uint32_t)0x81c2c92eU, (uint32_t)0x92722c85U, - (uint32_t)0xa2bfe8a1U, (uint32_t)0xa81a664bU, (uint32_t)0xc24b8b70U, (uint32_t)0xc76c51a3U, - (uint32_t)0xd192e819U, (uint32_t)0xd6990624U, (uint32_t)0xf40e3585U, (uint32_t)0x106aa070U, - (uint32_t)0x19a4c116U, (uint32_t)0x1e376c08U, (uint32_t)0x2748774cU, (uint32_t)0x34b0bcb5U, - (uint32_t)0x391c0cb3U, (uint32_t)0x4ed8aa4aU, (uint32_t)0x5b9cca4fU, (uint32_t)0x682e6ff3U, - (uint32_t)0x748f82eeU, (uint32_t)0x78a5636fU, (uint32_t)0x84c87814U, (uint32_t)0x8cc70208U, - (uint32_t)0x90befffaU, (uint32_t)0xa4506cebU, (uint32_t)0xbef9a3f7U, (uint32_t)0xc67178f2U - }; - -static uint64_t -k384_512[80U] = - { - (uint64_t)0x428a2f98d728ae22U, (uint64_t)0x7137449123ef65cdU, (uint64_t)0xb5c0fbcfec4d3b2fU, - (uint64_t)0xe9b5dba58189dbbcU, (uint64_t)0x3956c25bf348b538U, (uint64_t)0x59f111f1b605d019U, - (uint64_t)0x923f82a4af194f9bU, (uint64_t)0xab1c5ed5da6d8118U, (uint64_t)0xd807aa98a3030242U, - (uint64_t)0x12835b0145706fbeU, (uint64_t)0x243185be4ee4b28cU, (uint64_t)0x550c7dc3d5ffb4e2U, - (uint64_t)0x72be5d74f27b896fU, (uint64_t)0x80deb1fe3b1696b1U, (uint64_t)0x9bdc06a725c71235U, - (uint64_t)0xc19bf174cf692694U, (uint64_t)0xe49b69c19ef14ad2U, (uint64_t)0xefbe4786384f25e3U, - (uint64_t)0x0fc19dc68b8cd5b5U, (uint64_t)0x240ca1cc77ac9c65U, (uint64_t)0x2de92c6f592b0275U, - (uint64_t)0x4a7484aa6ea6e483U, (uint64_t)0x5cb0a9dcbd41fbd4U, (uint64_t)0x76f988da831153b5U, - (uint64_t)0x983e5152ee66dfabU, (uint64_t)0xa831c66d2db43210U, (uint64_t)0xb00327c898fb213fU, - (uint64_t)0xbf597fc7beef0ee4U, (uint64_t)0xc6e00bf33da88fc2U, (uint64_t)0xd5a79147930aa725U, - (uint64_t)0x06ca6351e003826fU, (uint64_t)0x142929670a0e6e70U, (uint64_t)0x27b70a8546d22ffcU, - (uint64_t)0x2e1b21385c26c926U, (uint64_t)0x4d2c6dfc5ac42aedU, (uint64_t)0x53380d139d95b3dfU, - (uint64_t)0x650a73548baf63deU, (uint64_t)0x766a0abb3c77b2a8U, (uint64_t)0x81c2c92e47edaee6U, - (uint64_t)0x92722c851482353bU, (uint64_t)0xa2bfe8a14cf10364U, (uint64_t)0xa81a664bbc423001U, - (uint64_t)0xc24b8b70d0f89791U, (uint64_t)0xc76c51a30654be30U, (uint64_t)0xd192e819d6ef5218U, - (uint64_t)0xd69906245565a910U, (uint64_t)0xf40e35855771202aU, (uint64_t)0x106aa07032bbd1b8U, - (uint64_t)0x19a4c116b8d2d0c8U, (uint64_t)0x1e376c085141ab53U, (uint64_t)0x2748774cdf8eeb99U, - (uint64_t)0x34b0bcb5e19b48a8U, (uint64_t)0x391c0cb3c5c95a63U, (uint64_t)0x4ed8aa4ae3418acbU, - (uint64_t)0x5b9cca4f7763e373U, (uint64_t)0x682e6ff3d6b2b8a3U, (uint64_t)0x748f82ee5defb2fcU, - (uint64_t)0x78a5636f43172f60U, (uint64_t)0x84c87814a1f0ab72U, (uint64_t)0x8cc702081a6439ecU, - (uint64_t)0x90befffa23631e28U, (uint64_t)0xa4506cebde82bde9U, (uint64_t)0xbef9a3f7b2c67915U, - (uint64_t)0xc67178f2e372532bU, (uint64_t)0xca273eceea26619cU, (uint64_t)0xd186b8c721c0c207U, - (uint64_t)0xeada7dd6cde0eb1eU, (uint64_t)0xf57d4f7fee6ed178U, (uint64_t)0x06f067aa72176fbaU, - (uint64_t)0x0a637dc5a2c898a6U, (uint64_t)0x113f9804bef90daeU, (uint64_t)0x1b710b35131c471bU, - (uint64_t)0x28db77f523047d84U, (uint64_t)0x32caab7b40c72493U, (uint64_t)0x3c9ebe0a15c9bebcU, - (uint64_t)0x431d67c49c100d4cU, (uint64_t)0x4cc5d4becb3e42b6U, (uint64_t)0x597f299cfc657e2aU, - (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U - }; - -static void init_256(uint32_t *s) -{ - for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) - { - s[i] = h256[i]; - } -} - -static void init_384(uint64_t *s) +static inline void sha256_init(uint32_t *hash) { for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - s[i] = h384[i]; + uint32_t *os = hash; + uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; + os[i] = x; } } -static void init_512(uint64_t *s) +static inline void sha256_update(uint8_t *b, uint32_t *hash) { - for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) - { - s[i] = h512[i]; - } -} - -static void update_256(uint32_t *hash, uint8_t *block) -{ - uint32_t hash1[8U] = { 0U }; - uint32_t computed_ws[64U] = { 0U }; - for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) - { - if (i < (uint32_t)16U) + uint32_t hash_old[8U] = { 0U }; + uint32_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint32_t)); + uint8_t *b10 = b; + uint32_t u = load32_be(b10); + ws[0U] = u; + uint32_t u0 = load32_be(b10 + (uint32_t)4U); + ws[1U] = u0; + uint32_t u1 = load32_be(b10 + (uint32_t)8U); + ws[2U] = u1; + uint32_t u2 = load32_be(b10 + (uint32_t)12U); + ws[3U] = u2; + uint32_t u3 = load32_be(b10 + (uint32_t)16U); + ws[4U] = u3; + uint32_t u4 = load32_be(b10 + (uint32_t)20U); + ws[5U] = u4; + uint32_t u5 = load32_be(b10 + (uint32_t)24U); + ws[6U] = u5; + uint32_t u6 = load32_be(b10 + (uint32_t)28U); + ws[7U] = u6; + uint32_t u7 = load32_be(b10 + (uint32_t)32U); + ws[8U] = u7; + uint32_t u8 = load32_be(b10 + (uint32_t)36U); + ws[9U] = u8; + uint32_t u9 = load32_be(b10 + (uint32_t)40U); + ws[10U] = u9; + uint32_t u10 = load32_be(b10 + (uint32_t)44U); + ws[11U] = u10; + uint32_t u11 = load32_be(b10 + (uint32_t)48U); + ws[12U] = u11; + uint32_t u12 = load32_be(b10 + (uint32_t)52U); + ws[13U] = u12; + uint32_t u13 = load32_be(b10 + (uint32_t)56U); + ws[14U] = u13; + uint32_t u14 = load32_be(b10 + (uint32_t)60U); + ws[15U] = u14; + for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) { - uint8_t *b = block + i * (uint32_t)4U; - uint32_t u = load32_be(b); - computed_ws[i] = u; - } - else - { - uint32_t t16 = computed_ws[i - (uint32_t)16U]; - uint32_t t15 = computed_ws[i - (uint32_t)15U]; - uint32_t t7 = computed_ws[i - (uint32_t)7U]; - uint32_t t2 = computed_ws[i - (uint32_t)2U]; + uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256[(uint32_t)16U * i0 + i]; + uint32_t ws_t = ws[i]; + uint32_t a0 = hash[0U]; + uint32_t b0 = hash[1U]; + uint32_t c0 = hash[2U]; + uint32_t d0 = hash[3U]; + uint32_t e0 = hash[4U]; + uint32_t f0 = hash[5U]; + uint32_t g0 = hash[6U]; + uint32_t h02 = hash[7U]; + uint32_t k_e_t = k_t; uint32_t - s1 = - (t2 >> (uint32_t)17U | t2 << (uint32_t)15U) - ^ ((t2 >> (uint32_t)19U | t2 << (uint32_t)13U) ^ t2 >> (uint32_t)10U); + t1 = + h02 + + + ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U) + ^ + ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U) + ^ (e0 << (uint32_t)7U | e0 >> (uint32_t)25U))) + + ((e0 & f0) ^ (~e0 & g0)) + + k_e_t + + ws_t; uint32_t - s0 = - (t15 >> (uint32_t)7U | t15 << (uint32_t)25U) - ^ ((t15 >> (uint32_t)18U | t15 << (uint32_t)14U) ^ t15 >> (uint32_t)3U); - uint32_t w = s1 + t7 + s0 + t16; - computed_ws[i] = w; + t2 = + ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U) + ^ + ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U) + ^ (a0 << (uint32_t)10U | a0 >> (uint32_t)22U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint32_t a1 = t1 + t2; + uint32_t b1 = a0; + uint32_t c1 = b0; + uint32_t d1 = c0; + uint32_t e1 = d0 + t1; + uint32_t f1 = e0; + uint32_t g1 = f0; + uint32_t h12 = g0; + hash[0U] = a1; + hash[1U] = b1; + hash[2U] = c1; + hash[3U] = d1; + hash[4U] = e1; + hash[5U] = f1; + hash[6U] = g1; + hash[7U] = h12; + } + if (i0 < (uint32_t)3U) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) + { + uint32_t t16 = ws[i]; + uint32_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint32_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint32_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint32_t + s1 = + (t2 << (uint32_t)15U | t2 >> (uint32_t)17U) + ^ ((t2 << (uint32_t)13U | t2 >> (uint32_t)19U) ^ t2 >> (uint32_t)10U); + uint32_t + s0 = + (t15 << (uint32_t)25U | t15 >> (uint32_t)7U) + ^ ((t15 << (uint32_t)14U | t15 >> (uint32_t)18U) ^ t15 >> (uint32_t)3U); + ws[i] = s1 + t7 + s0 + t16; + } } - } - memcpy(hash1, hash, (uint32_t)8U * sizeof (uint32_t)); - for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) - { - uint32_t a0 = hash1[0U]; - uint32_t b0 = hash1[1U]; - uint32_t c0 = hash1[2U]; - uint32_t d0 = hash1[3U]; - uint32_t e0 = hash1[4U]; - uint32_t f0 = hash1[5U]; - uint32_t g0 = hash1[6U]; - uint32_t h02 = hash1[7U]; - uint32_t w = computed_ws[i]; - uint32_t - t1 = - h02 - + - ((e0 >> (uint32_t)6U | e0 << (uint32_t)26U) - ^ ((e0 >> (uint32_t)11U | e0 << (uint32_t)21U) ^ (e0 >> (uint32_t)25U | e0 << (uint32_t)7U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k224_256[i] - + w; - uint32_t - t2 = - ((a0 >> (uint32_t)2U | a0 << (uint32_t)30U) - ^ ((a0 >> (uint32_t)13U | a0 << (uint32_t)19U) ^ (a0 >> (uint32_t)22U | a0 << (uint32_t)10U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - hash1[0U] = t1 + t2; - hash1[1U] = a0; - hash1[2U] = b0; - hash1[3U] = c0; - hash1[4U] = d0 + t1; - hash1[5U] = e0; - hash1[6U] = f0; - hash1[7U] = g0; } for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - uint32_t xi = hash[i]; - uint32_t yi = hash1[i]; - hash[i] = xi + yi; + uint32_t *os = hash; + uint32_t x = hash[i] + hash_old[i]; + os[i] = x; } } -static void update_384(uint64_t *hash, uint8_t *block) +static inline void sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) { - uint64_t hash1[8U] = { 0U }; - uint64_t computed_ws[80U] = { 0U }; - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) + uint32_t blocks = len / (uint32_t)64U; + for (uint32_t i = (uint32_t)0U; i < blocks; i++) { - if (i < (uint32_t)16U) - { - uint8_t *b = block + i * (uint32_t)8U; - uint64_t u = load64_be(b); - computed_ws[i] = u; - } - else - { - uint64_t t16 = computed_ws[i - (uint32_t)16U]; - uint64_t t15 = computed_ws[i - (uint32_t)15U]; - uint64_t t7 = computed_ws[i - (uint32_t)7U]; - uint64_t t2 = computed_ws[i - (uint32_t)2U]; - uint64_t - s1 = - (t2 >> (uint32_t)19U | t2 << (uint32_t)45U) - ^ ((t2 >> (uint32_t)61U | t2 << (uint32_t)3U) ^ t2 >> (uint32_t)6U); - uint64_t - s0 = - (t15 >> (uint32_t)1U | t15 << (uint32_t)63U) - ^ ((t15 >> (uint32_t)8U | t15 << (uint32_t)56U) ^ t15 >> (uint32_t)7U); - uint64_t w = s1 + t7 + s0 + t16; - computed_ws[i] = w; - } - } - memcpy(hash1, hash, (uint32_t)8U * sizeof (uint64_t)); - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) - { - uint64_t a0 = hash1[0U]; - uint64_t b0 = hash1[1U]; - uint64_t c0 = hash1[2U]; - uint64_t d0 = hash1[3U]; - uint64_t e0 = hash1[4U]; - uint64_t f0 = hash1[5U]; - uint64_t g0 = hash1[6U]; - uint64_t h02 = hash1[7U]; - uint64_t w = computed_ws[i]; - uint64_t - t1 = - h02 - + - ((e0 >> (uint32_t)14U | e0 << (uint32_t)50U) - ^ - ((e0 >> (uint32_t)18U | e0 << (uint32_t)46U) - ^ (e0 >> (uint32_t)41U | e0 << (uint32_t)23U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k384_512[i] - + w; - uint64_t - t2 = - ((a0 >> (uint32_t)28U | a0 << (uint32_t)36U) - ^ ((a0 >> (uint32_t)34U | a0 << (uint32_t)30U) ^ (a0 >> (uint32_t)39U | a0 << (uint32_t)25U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - hash1[0U] = t1 + t2; - hash1[1U] = a0; - hash1[2U] = b0; - hash1[3U] = c0; - hash1[4U] = d0 + t1; - hash1[5U] = e0; - hash1[6U] = f0; - hash1[7U] = g0; - } - for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) - { - uint64_t xi = hash[i]; - uint64_t yi = hash1[i]; - hash[i] = xi + yi; + uint8_t *b0 = b; + uint8_t *mb = b0 + i * (uint32_t)64U; + sha256_update(mb, st); } } -static void update_512(uint64_t *hash, uint8_t *block) +static inline void +sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash) { - uint64_t hash1[8U] = { 0U }; - uint64_t computed_ws[80U] = { 0U }; - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) + uint32_t blocks; + if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U) { - if (i < (uint32_t)16U) - { - uint8_t *b = block + i * (uint32_t)8U; - uint64_t u = load64_be(b); - computed_ws[i] = u; - } - else - { - uint64_t t16 = computed_ws[i - (uint32_t)16U]; - uint64_t t15 = computed_ws[i - (uint32_t)15U]; - uint64_t t7 = computed_ws[i - (uint32_t)7U]; - uint64_t t2 = computed_ws[i - (uint32_t)2U]; - uint64_t - s1 = - (t2 >> (uint32_t)19U | t2 << (uint32_t)45U) - ^ ((t2 >> (uint32_t)61U | t2 << (uint32_t)3U) ^ t2 >> (uint32_t)6U); - uint64_t - s0 = - (t15 >> (uint32_t)1U | t15 << (uint32_t)63U) - ^ ((t15 >> (uint32_t)8U | t15 << (uint32_t)56U) ^ t15 >> (uint32_t)7U); - uint64_t w = s1 + t7 + s0 + t16; - computed_ws[i] = w; - } + blocks = (uint32_t)1U; } - memcpy(hash1, hash, (uint32_t)8U * sizeof (uint64_t)); - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) + else { - uint64_t a0 = hash1[0U]; - uint64_t b0 = hash1[1U]; - uint64_t c0 = hash1[2U]; - uint64_t d0 = hash1[3U]; - uint64_t e0 = hash1[4U]; - uint64_t f0 = hash1[5U]; - uint64_t g0 = hash1[6U]; - uint64_t h02 = hash1[7U]; - uint64_t w = computed_ws[i]; - uint64_t - t1 = - h02 - + - ((e0 >> (uint32_t)14U | e0 << (uint32_t)50U) - ^ - ((e0 >> (uint32_t)18U | e0 << (uint32_t)46U) - ^ (e0 >> (uint32_t)41U | e0 << (uint32_t)23U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k384_512[i] - + w; - uint64_t - t2 = - ((a0 >> (uint32_t)28U | a0 << (uint32_t)36U) - ^ ((a0 >> (uint32_t)34U | a0 << (uint32_t)30U) ^ (a0 >> (uint32_t)39U | a0 << (uint32_t)25U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - hash1[0U] = t1 + t2; - hash1[1U] = a0; - hash1[2U] = b0; - hash1[3U] = c0; - hash1[4U] = d0 + t1; - hash1[5U] = e0; - hash1[6U] = f0; - hash1[7U] = g0; + blocks = (uint32_t)2U; } - for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) - { - uint64_t xi = hash[i]; - uint64_t yi = hash1[i]; - hash[i] = xi + yi; + uint32_t fin = blocks * (uint32_t)64U; + uint8_t last[128U] = { 0U }; + uint8_t totlen_buf[8U] = { 0U }; + uint64_t total_len_bits = totlen << (uint32_t)3U; + store64_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof (uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)8U, totlen_buf, (uint32_t)8U * sizeof (uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)64U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha256_update(last0, hash); + if (blocks > (uint32_t)1U) + { + sha256_update(last1, hash); } } -static void pad_256(uint64_t len, uint8_t *dst) +static inline void sha256_finish(uint32_t *st, uint8_t *h) { - uint8_t *dst1 = dst; - dst1[0U] = (uint8_t)0x80U; - uint8_t *dst2 = dst + (uint32_t)1U; - for - (uint32_t - i = (uint32_t)0U; - i - < ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(len % (uint64_t)(uint32_t)64U))) % (uint32_t)64U; - i++) + uint8_t hbuf[32U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - dst2[i] = (uint8_t)0U; + store32_be(hbuf + i * (uint32_t)4U, st[i]); } - uint8_t - *dst3 = - dst - + - (uint32_t)1U - + - ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(len % (uint64_t)(uint32_t)64U))) - % (uint32_t)64U; - store64_be(dst3, len << (uint32_t)3U); + memcpy(h, hbuf, (uint32_t)32U * sizeof (uint8_t)); } -static void pad_384(FStar_UInt128_uint128 len, uint8_t *dst) +static void sha512_init(uint64_t *hash) { - uint8_t *dst1 = dst; - dst1[0U] = (uint8_t)0x80U; - uint8_t *dst2 = dst + (uint32_t)1U; - for - (uint32_t - i = (uint32_t)0U; - i - < - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - i++) + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - dst2[i] = (uint8_t)0U; + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; + os[i] = x; } - uint8_t - *dst3 = - dst - + - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_shift_left(len, (uint32_t)3U); - store128_be(dst3, len_); } -static void pad_512(FStar_UInt128_uint128 len, uint8_t *dst) +static inline void sha512_update(uint8_t *b, uint64_t *hash) { - uint8_t *dst1 = dst; - dst1[0U] = (uint8_t)0x80U; - uint8_t *dst2 = dst + (uint32_t)1U; - for - (uint32_t - i = (uint32_t)0U; - i - < - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - i++) - { - dst2[i] = (uint8_t)0U; + uint64_t hash_old[8U] = { 0U }; + uint64_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint64_t)); + uint8_t *b10 = b; + uint64_t u = load64_be(b10); + ws[0U] = u; + uint64_t u0 = load64_be(b10 + (uint32_t)8U); + ws[1U] = u0; + uint64_t u1 = load64_be(b10 + (uint32_t)16U); + ws[2U] = u1; + uint64_t u2 = load64_be(b10 + (uint32_t)24U); + ws[3U] = u2; + uint64_t u3 = load64_be(b10 + (uint32_t)32U); + ws[4U] = u3; + uint64_t u4 = load64_be(b10 + (uint32_t)40U); + ws[5U] = u4; + uint64_t u5 = load64_be(b10 + (uint32_t)48U); + ws[6U] = u5; + uint64_t u6 = load64_be(b10 + (uint32_t)56U); + ws[7U] = u6; + uint64_t u7 = load64_be(b10 + (uint32_t)64U); + ws[8U] = u7; + uint64_t u8 = load64_be(b10 + (uint32_t)72U); + ws[9U] = u8; + uint64_t u9 = load64_be(b10 + (uint32_t)80U); + ws[10U] = u9; + uint64_t u10 = load64_be(b10 + (uint32_t)88U); + ws[11U] = u10; + uint64_t u11 = load64_be(b10 + (uint32_t)96U); + ws[12U] = u11; + uint64_t u12 = load64_be(b10 + (uint32_t)104U); + ws[13U] = u12; + uint64_t u13 = load64_be(b10 + (uint32_t)112U); + ws[14U] = u13; + uint64_t u14 = load64_be(b10 + (uint32_t)120U); + ws[15U] = u14; + for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)5U; i0++) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) + { + uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512[(uint32_t)16U * i0 + i]; + uint64_t ws_t = ws[i]; + uint64_t a0 = hash[0U]; + uint64_t b0 = hash[1U]; + uint64_t c0 = hash[2U]; + uint64_t d0 = hash[3U]; + uint64_t e0 = hash[4U]; + uint64_t f0 = hash[5U]; + uint64_t g0 = hash[6U]; + uint64_t h02 = hash[7U]; + uint64_t k_e_t = k_t; + uint64_t + t1 = + h02 + + + ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U) + ^ + ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U) + ^ (e0 << (uint32_t)23U | e0 >> (uint32_t)41U))) + + ((e0 & f0) ^ (~e0 & g0)) + + k_e_t + + ws_t; + uint64_t + t2 = + ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U) + ^ + ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U) + ^ (a0 << (uint32_t)25U | a0 >> (uint32_t)39U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint64_t a1 = t1 + t2; + uint64_t b1 = a0; + uint64_t c1 = b0; + uint64_t d1 = c0; + uint64_t e1 = d0 + t1; + uint64_t f1 = e0; + uint64_t g1 = f0; + uint64_t h12 = g0; + hash[0U] = a1; + hash[1U] = b1; + hash[2U] = c1; + hash[3U] = d1; + hash[4U] = e1; + hash[5U] = f1; + hash[6U] = g1; + hash[7U] = h12; + } + if (i0 < (uint32_t)4U) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) + { + uint64_t t16 = ws[i]; + uint64_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint64_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint64_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint64_t + s1 = + (t2 << (uint32_t)45U | t2 >> (uint32_t)19U) + ^ ((t2 << (uint32_t)3U | t2 >> (uint32_t)61U) ^ t2 >> (uint32_t)6U); + uint64_t + s0 = + (t15 << (uint32_t)63U | t15 >> (uint32_t)1U) + ^ ((t15 << (uint32_t)56U | t15 >> (uint32_t)8U) ^ t15 >> (uint32_t)7U); + ws[i] = s1 + t7 + s0 + t16; + } + } } - uint8_t - *dst3 = - dst - + - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_shift_left(len, (uint32_t)3U); - store128_be(dst3, len_); -} - -static void finish_256(uint32_t *s, uint8_t *dst) -{ for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - store32_be(dst + i * (uint32_t)4U, s[i]); + uint64_t *os = hash; + uint64_t x = hash[i] + hash_old[i]; + os[i] = x; } } -static void finish_384(uint64_t *s, uint8_t *dst) +static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) { - for (uint32_t i = (uint32_t)0U; i < (uint32_t)6U; i++) + uint32_t blocks = len / (uint32_t)128U; + for (uint32_t i = (uint32_t)0U; i < blocks; i++) { - store64_be(dst + i * (uint32_t)8U, s[i]); + uint8_t *b0 = b; + uint8_t *mb = b0 + i * (uint32_t)128U; + sha512_update(mb, st); } } -static void finish_512(uint64_t *s, uint8_t *dst) +static inline void +sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash) { - for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) + uint32_t blocks; + if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U) { - store64_be(dst + i * (uint32_t)8U, s[i]); + blocks = (uint32_t)1U; } -} - -static void update_multi_256(uint32_t *s, uint8_t *blocks, uint32_t n_blocks) -{ - for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) + else { - uint32_t sz = (uint32_t)64U; - uint8_t *block = blocks + sz * i; - update_256(s, block); + blocks = (uint32_t)2U; + } + uint32_t fin = blocks * (uint32_t)128U; + uint8_t last[256U] = { 0U }; + uint8_t totlen_buf[16U] = { 0U }; + FStar_UInt128_uint128 total_len_bits = FStar_UInt128_shift_left(totlen, (uint32_t)3U); + store128_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof (uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)16U, totlen_buf, (uint32_t)16U * sizeof (uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)128U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha512_update(last0, hash); + if (blocks > (uint32_t)1U) + { + sha512_update(last1, hash); } } -static void update_multi_384(uint64_t *s, uint8_t *blocks, uint32_t n_blocks) +static inline void sha512_finish(uint64_t *st, uint8_t *h) { - for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) + uint8_t hbuf[64U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - uint32_t sz = (uint32_t)128U; - uint8_t *block = blocks + sz * i; - update_384(s, block); + store64_be(hbuf + i * (uint32_t)8U, st[i]); } + memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t)); } -static void update_multi_512(uint64_t *s, uint8_t *blocks, uint32_t n_blocks) +static inline void sha384_init(uint64_t *hash) { - for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - uint32_t sz = (uint32_t)128U; - uint8_t *block = blocks + sz * i; - update_512(s, block); + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; + os[i] = x; } } -static void update_last_256(uint32_t *s, uint64_t prev_len, uint8_t *input, uint32_t input_len) +static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) { - uint32_t blocks_n = input_len / (uint32_t)64U; - uint32_t blocks_len = blocks_n * (uint32_t)64U; - uint8_t *blocks = input; - uint32_t rest_len = input_len - blocks_len; - uint8_t *rest = input + blocks_len; - update_multi_256(s, blocks, blocks_n); - uint64_t total_input_len = prev_len + (uint64_t)input_len; - uint32_t - pad_len = - (uint32_t)1U - + - ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(total_input_len % (uint64_t)(uint32_t)64U))) - % (uint32_t)64U - + (uint32_t)8U; - uint32_t tmp_len = rest_len + pad_len; - uint8_t tmp_twoblocks[128U] = { 0U }; - uint8_t *tmp = tmp_twoblocks; - uint8_t *tmp_rest = tmp; - uint8_t *tmp_pad = tmp + rest_len; - memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t)); - pad_256(total_input_len, tmp_pad); - update_multi_256(s, tmp, tmp_len / (uint32_t)64U); -} - -static void -update_last_384( - uint64_t *s, - FStar_UInt128_uint128 prev_len, - uint8_t *input, - uint32_t input_len -) -{ - uint32_t blocks_n = input_len / (uint32_t)128U; - uint32_t blocks_len = blocks_n * (uint32_t)128U; - uint8_t *blocks = input; - uint32_t rest_len = input_len - blocks_len; - uint8_t *rest = input + blocks_len; - update_multi_384(s, blocks, blocks_n); - FStar_UInt128_uint128 - total_input_len = - FStar_UInt128_add(prev_len, - FStar_UInt128_uint64_to_uint128((uint64_t)input_len)); - uint32_t - pad_len = - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(total_input_len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U - + (uint32_t)16U; - uint32_t tmp_len = rest_len + pad_len; - uint8_t tmp_twoblocks[256U] = { 0U }; - uint8_t *tmp = tmp_twoblocks; - uint8_t *tmp_rest = tmp; - uint8_t *tmp_pad = tmp + rest_len; - memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t)); - pad_384(total_input_len, tmp_pad); - update_multi_384(s, tmp, tmp_len / (uint32_t)128U); + sha512_update_nblocks(len, b, st); } static void -update_last_512( - uint64_t *s, - FStar_UInt128_uint128 prev_len, - uint8_t *input, - uint32_t input_len -) -{ - uint32_t blocks_n = input_len / (uint32_t)128U; - uint32_t blocks_len = blocks_n * (uint32_t)128U; - uint8_t *blocks = input; - uint32_t rest_len = input_len - blocks_len; - uint8_t *rest = input + blocks_len; - update_multi_512(s, blocks, blocks_n); - FStar_UInt128_uint128 - total_input_len = - FStar_UInt128_add(prev_len, - FStar_UInt128_uint64_to_uint128((uint64_t)input_len)); - uint32_t - pad_len = - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(total_input_len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U - + (uint32_t)16U; - uint32_t tmp_len = rest_len + pad_len; - uint8_t tmp_twoblocks[256U] = { 0U }; - uint8_t *tmp = tmp_twoblocks; - uint8_t *tmp_rest = tmp; - uint8_t *tmp_pad = tmp + rest_len; - memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t)); - pad_512(total_input_len, tmp_pad); - update_multi_512(s, tmp, tmp_len / (uint32_t)128U); -} - -static void hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint32_t - s[8U] = - { - (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, (uint32_t)0xa54ff53aU, - (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U - }; - uint32_t blocks_n0 = input_len / (uint32_t)64U; - uint32_t blocks_n1; - if (input_len % (uint32_t)64U == (uint32_t)0U && blocks_n0 > (uint32_t)0U) - { - blocks_n1 = blocks_n0 - (uint32_t)1U; - } - else - { - blocks_n1 = blocks_n0; - } - uint32_t blocks_len0 = blocks_n1 * (uint32_t)64U; - uint8_t *blocks0 = input; - uint32_t rest_len0 = input_len - blocks_len0; - uint8_t *rest0 = input + blocks_len0; - uint32_t blocks_n = blocks_n1; - uint32_t blocks_len = blocks_len0; - uint8_t *blocks = blocks0; - uint32_t rest_len = rest_len0; - uint8_t *rest = rest0; - update_multi_256(s, blocks, blocks_n); - update_last_256(s, (uint64_t)blocks_len, rest, rest_len); - finish_256(s, dst); -} - -static void hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst) +sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st) { - uint64_t - s[8U] = - { - (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, (uint64_t)0x9159015a3070dd17U, - (uint64_t)0x152fecd8f70e5939U, (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, - (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U - }; - uint32_t blocks_n0 = input_len / (uint32_t)128U; - uint32_t blocks_n1; - if (input_len % (uint32_t)128U == (uint32_t)0U && blocks_n0 > (uint32_t)0U) - { - blocks_n1 = blocks_n0 - (uint32_t)1U; - } - else - { - blocks_n1 = blocks_n0; - } - uint32_t blocks_len0 = blocks_n1 * (uint32_t)128U; - uint8_t *blocks0 = input; - uint32_t rest_len0 = input_len - blocks_len0; - uint8_t *rest0 = input + blocks_len0; - uint32_t blocks_n = blocks_n1; - uint32_t blocks_len = blocks_len0; - uint8_t *blocks = blocks0; - uint32_t rest_len = rest_len0; - uint8_t *rest = rest0; - update_multi_384(s, blocks, blocks_n); - update_last_384(s, FStar_UInt128_uint64_to_uint128((uint64_t)blocks_len), rest, rest_len); - finish_384(s, dst); + sha512_update_last(totlen, len, b, st); } -static void hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst) +static inline void sha384_finish(uint64_t *st, uint8_t *h) { - uint64_t - s[8U] = - { - (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, (uint64_t)0x3c6ef372fe94f82bU, - (uint64_t)0xa54ff53a5f1d36f1U, (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, - (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U - }; - uint32_t blocks_n0 = input_len / (uint32_t)128U; - uint32_t blocks_n1; - if (input_len % (uint32_t)128U == (uint32_t)0U && blocks_n0 > (uint32_t)0U) - { - blocks_n1 = blocks_n0 - (uint32_t)1U; - } - else + uint8_t hbuf[64U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - blocks_n1 = blocks_n0; + store64_be(hbuf + i * (uint32_t)8U, st[i]); } - uint32_t blocks_len0 = blocks_n1 * (uint32_t)128U; - uint8_t *blocks0 = input; - uint32_t rest_len0 = input_len - blocks_len0; - uint8_t *rest0 = input + blocks_len0; - uint32_t blocks_n = blocks_n1; - uint32_t blocks_len = blocks_len0; - uint8_t *blocks = blocks0; - uint32_t rest_len = rest_len0; - uint8_t *rest = rest0; - update_multi_512(s, blocks, blocks_n); - update_last_512(s, FStar_UInt128_uint64_to_uint128((uint64_t)blocks_len), rest, rest_len); - finish_512(s, dst); + memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t)); } static uint32_t @@ -920,6 +647,63 @@ static void legacy_hash(uint8_t *input, uint32_t input_len, uint8_t *dst) legacy_finish(s, dst); } +/** +Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. +*/ +static void hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + sha256_init(st); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + sha256_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)64U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + sha256_update_last(len_, rem, lb, st); + sha256_finish(st, rb); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. +*/ +static void hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint64_t st[8U] = { 0U }; + sha512_init(st); + uint32_t rem = input_len % (uint32_t)128U; + FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); + sha512_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)128U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + sha512_update_last(len_, rem, lb, st); + sha512_finish(st, rb); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. +*/ +static void hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint64_t st[8U] = { 0U }; + sha384_init(st); + uint32_t rem = input_len % (uint32_t)128U; + FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); + sha384_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)128U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + sha384_update_last(len_, rem, lb, st); + sha384_finish(st, rb); +} + extern void C_String_print(C_String_t uu___); typedef struct __uint32_t_uint32_t_s @@ -1102,16 +886,18 @@ compute_sha2_256( uint8_t yi = key_block[i]; opad[i] = xi ^ yi; } - uint32_t - s[8U] = - { - (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, (uint32_t)0xa54ff53aU, - (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U - }; + uint32_t st[8U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) + { + uint32_t *os = st; + uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; + os[i] = x; + } + uint32_t *s = st; uint8_t *dst1 = ipad; if (data_len == (uint32_t)0U) { - update_last_256(s, (uint64_t)0U, ipad, (uint32_t)64U); + sha256_update_last((uint64_t)0U + (uint64_t)(uint32_t)64U, (uint32_t)64U, ipad, s); } else { @@ -1133,13 +919,16 @@ compute_sha2_256( uint32_t full_blocks_len = n_blocks * block_len; uint8_t *full_blocks = data; uint8_t *rem = data + full_blocks_len; - update_multi_256(s, ipad, (uint32_t)1U); - update_multi_256(s, full_blocks, n_blocks); - update_last_256(s, (uint64_t)(uint32_t)64U + (uint64_t)full_blocks_len, rem, rem_len); + sha256_update_nblocks((uint32_t)64U, ipad, s); + sha256_update_nblocks(n_blocks * (uint32_t)64U, full_blocks, s); + sha256_update_last((uint64_t)(uint32_t)64U + (uint64_t)full_blocks_len + (uint64_t)rem_len, + rem_len, + rem, + s); } - finish_256(s, dst1); + sha256_finish(s, dst1); uint8_t *hash1 = ipad; - init_256(s); + sha256_init(s); uint32_t block_len = (uint32_t)64U; uint32_t n_blocks0 = (uint32_t)32U / block_len; uint32_t rem0 = (uint32_t)32U % block_len; @@ -1159,10 +948,13 @@ compute_sha2_256( uint32_t full_blocks_len = n_blocks * block_len; uint8_t *full_blocks = hash1; uint8_t *rem = hash1 + full_blocks_len; - update_multi_256(s, opad, (uint32_t)1U); - update_multi_256(s, full_blocks, n_blocks); - update_last_256(s, (uint64_t)(uint32_t)64U + (uint64_t)full_blocks_len, rem, rem_len); - finish_256(s, dst); + sha256_update_nblocks((uint32_t)64U, opad, s); + sha256_update_nblocks(n_blocks * (uint32_t)64U, full_blocks, s); + sha256_update_last((uint64_t)(uint32_t)64U + (uint64_t)full_blocks_len + (uint64_t)rem_len, + rem_len, + rem, + s); + sha256_finish(s, dst); } /** @@ -1220,17 +1012,22 @@ compute_sha2_384( uint8_t yi = key_block[i]; opad[i] = xi ^ yi; } - uint64_t - s[8U] = - { - (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, (uint64_t)0x9159015a3070dd17U, - (uint64_t)0x152fecd8f70e5939U, (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, - (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U - }; + uint64_t st[8U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) + { + uint64_t *os = st; + uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; + os[i] = x; + } + uint64_t *s = st; uint8_t *dst1 = ipad; if (data_len == (uint32_t)0U) { - update_last_384(s, FStar_UInt128_uint64_to_uint128((uint64_t)0U), ipad, (uint32_t)128U); + sha384_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)0U), + FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U)), + (uint32_t)128U, + ipad, + s); } else { @@ -1252,17 +1049,18 @@ compute_sha2_384( uint32_t full_blocks_len = n_blocks * block_len; uint8_t *full_blocks = data; uint8_t *rem = data + full_blocks_len; - update_multi_384(s, ipad, (uint32_t)1U); - update_multi_384(s, full_blocks, n_blocks); - update_last_384(s, - FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), - FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + sha384_update_nblocks((uint32_t)128U, ipad, s); + sha384_update_nblocks(n_blocks * (uint32_t)128U, full_blocks, s); + sha384_update_last(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), + FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + FStar_UInt128_uint64_to_uint128((uint64_t)rem_len)), + rem_len, rem, - rem_len); + s); } - finish_384(s, dst1); + sha384_finish(s, dst1); uint8_t *hash1 = ipad; - init_384(s); + sha384_init(s); uint32_t block_len = (uint32_t)128U; uint32_t n_blocks0 = (uint32_t)48U / block_len; uint32_t rem0 = (uint32_t)48U % block_len; @@ -1282,14 +1080,15 @@ compute_sha2_384( uint32_t full_blocks_len = n_blocks * block_len; uint8_t *full_blocks = hash1; uint8_t *rem = hash1 + full_blocks_len; - update_multi_384(s, opad, (uint32_t)1U); - update_multi_384(s, full_blocks, n_blocks); - update_last_384(s, - FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), - FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + sha384_update_nblocks((uint32_t)128U, opad, s); + sha384_update_nblocks(n_blocks * (uint32_t)128U, full_blocks, s); + sha384_update_last(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), + FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + FStar_UInt128_uint64_to_uint128((uint64_t)rem_len)), + rem_len, rem, - rem_len); - finish_384(s, dst); + s); + sha384_finish(s, dst); } /** @@ -1347,17 +1146,22 @@ compute_sha2_512( uint8_t yi = key_block[i]; opad[i] = xi ^ yi; } - uint64_t - s[8U] = - { - (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, (uint64_t)0x3c6ef372fe94f82bU, - (uint64_t)0xa54ff53a5f1d36f1U, (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, - (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U - }; + uint64_t st[8U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) + { + uint64_t *os = st; + uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; + os[i] = x; + } + uint64_t *s = st; uint8_t *dst1 = ipad; if (data_len == (uint32_t)0U) { - update_last_512(s, FStar_UInt128_uint64_to_uint128((uint64_t)0U), ipad, (uint32_t)128U); + sha512_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)0U), + FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U)), + (uint32_t)128U, + ipad, + s); } else { @@ -1379,17 +1183,18 @@ compute_sha2_512( uint32_t full_blocks_len = n_blocks * block_len; uint8_t *full_blocks = data; uint8_t *rem = data + full_blocks_len; - update_multi_512(s, ipad, (uint32_t)1U); - update_multi_512(s, full_blocks, n_blocks); - update_last_512(s, - FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), - FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + sha512_update_nblocks((uint32_t)128U, ipad, s); + sha512_update_nblocks(n_blocks * (uint32_t)128U, full_blocks, s); + sha512_update_last(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), + FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + FStar_UInt128_uint64_to_uint128((uint64_t)rem_len)), + rem_len, rem, - rem_len); + s); } - finish_512(s, dst1); + sha512_finish(s, dst1); uint8_t *hash1 = ipad; - init_512(s); + sha512_init(s); uint32_t block_len = (uint32_t)128U; uint32_t n_blocks0 = (uint32_t)64U / block_len; uint32_t rem0 = (uint32_t)64U % block_len; @@ -1409,14 +1214,15 @@ compute_sha2_512( uint32_t full_blocks_len = n_blocks * block_len; uint8_t *full_blocks = hash1; uint8_t *rem = hash1 + full_blocks_len; - update_multi_512(s, opad, (uint32_t)1U); - update_multi_512(s, full_blocks, n_blocks); - update_last_512(s, - FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), - FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + sha512_update_nblocks((uint32_t)128U, opad, s); + sha512_update_nblocks(n_blocks * (uint32_t)128U, full_blocks, s); + sha512_update_last(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U), + FStar_UInt128_uint64_to_uint128((uint64_t)full_blocks_len)), + FStar_UInt128_uint64_to_uint128((uint64_t)rem_len)), + rem_len, rem, - rem_len); - finish_512(s, dst); + s); + sha512_finish(s, dst); } static bool is_supported_alg(hash_alg uu___) diff --git a/dist/test/c/Hacl_Test_HMAC_DRBG.h b/dist/test/c/Hacl_Test_HMAC_DRBG.h index cdc16ef924..0ada0db945 100644 --- a/dist/test/c/Hacl_Test_HMAC_DRBG.h +++ b/dist/test/c/Hacl_Test_HMAC_DRBG.h @@ -26,6 +26,7 @@ #ifndef __Hacl_Test_HMAC_DRBG_H #define __Hacl_Test_HMAC_DRBG_H +#include "internal/Hacl_Hash_SHA2.h" #include "krmllib.h" #include "libintvector.h" diff --git a/dist/test/c/Hacl_Test_K256.h b/dist/test/c/Hacl_Test_K256.h index 63c0da57ea..5fdc7444d0 100644 --- a/dist/test/c/Hacl_Test_K256.h +++ b/dist/test/c/Hacl_Test_K256.h @@ -26,6 +26,7 @@ #ifndef __Hacl_Test_K256_H #define __Hacl_Test_K256_H +#include "internal/Hacl_Hash_SHA2.h" #include "krmllib.h" #include "libintvector.h" #include "lib_intrinsics.h" diff --git a/dist/test/c/Hacl_Test_SHA2.c b/dist/test/c/Hacl_Test_SHA2.c index 61958aa499..ee7c5b87ce 100644 --- a/dist/test/c/Hacl_Test_SHA2.c +++ b/dist/test/c/Hacl_Test_SHA2.c @@ -25,801 +25,507 @@ #include "Hacl_Test_SHA2.h" -static uint32_t -k224_256[64U] = - { - (uint32_t)0x428a2f98U, (uint32_t)0x71374491U, (uint32_t)0xb5c0fbcfU, (uint32_t)0xe9b5dba5U, - (uint32_t)0x3956c25bU, (uint32_t)0x59f111f1U, (uint32_t)0x923f82a4U, (uint32_t)0xab1c5ed5U, - (uint32_t)0xd807aa98U, (uint32_t)0x12835b01U, (uint32_t)0x243185beU, (uint32_t)0x550c7dc3U, - (uint32_t)0x72be5d74U, (uint32_t)0x80deb1feU, (uint32_t)0x9bdc06a7U, (uint32_t)0xc19bf174U, - (uint32_t)0xe49b69c1U, (uint32_t)0xefbe4786U, (uint32_t)0x0fc19dc6U, (uint32_t)0x240ca1ccU, - (uint32_t)0x2de92c6fU, (uint32_t)0x4a7484aaU, (uint32_t)0x5cb0a9dcU, (uint32_t)0x76f988daU, - (uint32_t)0x983e5152U, (uint32_t)0xa831c66dU, (uint32_t)0xb00327c8U, (uint32_t)0xbf597fc7U, - (uint32_t)0xc6e00bf3U, (uint32_t)0xd5a79147U, (uint32_t)0x06ca6351U, (uint32_t)0x14292967U, - (uint32_t)0x27b70a85U, (uint32_t)0x2e1b2138U, (uint32_t)0x4d2c6dfcU, (uint32_t)0x53380d13U, - (uint32_t)0x650a7354U, (uint32_t)0x766a0abbU, (uint32_t)0x81c2c92eU, (uint32_t)0x92722c85U, - (uint32_t)0xa2bfe8a1U, (uint32_t)0xa81a664bU, (uint32_t)0xc24b8b70U, (uint32_t)0xc76c51a3U, - (uint32_t)0xd192e819U, (uint32_t)0xd6990624U, (uint32_t)0xf40e3585U, (uint32_t)0x106aa070U, - (uint32_t)0x19a4c116U, (uint32_t)0x1e376c08U, (uint32_t)0x2748774cU, (uint32_t)0x34b0bcb5U, - (uint32_t)0x391c0cb3U, (uint32_t)0x4ed8aa4aU, (uint32_t)0x5b9cca4fU, (uint32_t)0x682e6ff3U, - (uint32_t)0x748f82eeU, (uint32_t)0x78a5636fU, (uint32_t)0x84c87814U, (uint32_t)0x8cc70208U, - (uint32_t)0x90befffaU, (uint32_t)0xa4506cebU, (uint32_t)0xbef9a3f7U, (uint32_t)0xc67178f2U - }; - -static uint64_t -k384_512[80U] = - { - (uint64_t)0x428a2f98d728ae22U, (uint64_t)0x7137449123ef65cdU, (uint64_t)0xb5c0fbcfec4d3b2fU, - (uint64_t)0xe9b5dba58189dbbcU, (uint64_t)0x3956c25bf348b538U, (uint64_t)0x59f111f1b605d019U, - (uint64_t)0x923f82a4af194f9bU, (uint64_t)0xab1c5ed5da6d8118U, (uint64_t)0xd807aa98a3030242U, - (uint64_t)0x12835b0145706fbeU, (uint64_t)0x243185be4ee4b28cU, (uint64_t)0x550c7dc3d5ffb4e2U, - (uint64_t)0x72be5d74f27b896fU, (uint64_t)0x80deb1fe3b1696b1U, (uint64_t)0x9bdc06a725c71235U, - (uint64_t)0xc19bf174cf692694U, (uint64_t)0xe49b69c19ef14ad2U, (uint64_t)0xefbe4786384f25e3U, - (uint64_t)0x0fc19dc68b8cd5b5U, (uint64_t)0x240ca1cc77ac9c65U, (uint64_t)0x2de92c6f592b0275U, - (uint64_t)0x4a7484aa6ea6e483U, (uint64_t)0x5cb0a9dcbd41fbd4U, (uint64_t)0x76f988da831153b5U, - (uint64_t)0x983e5152ee66dfabU, (uint64_t)0xa831c66d2db43210U, (uint64_t)0xb00327c898fb213fU, - (uint64_t)0xbf597fc7beef0ee4U, (uint64_t)0xc6e00bf33da88fc2U, (uint64_t)0xd5a79147930aa725U, - (uint64_t)0x06ca6351e003826fU, (uint64_t)0x142929670a0e6e70U, (uint64_t)0x27b70a8546d22ffcU, - (uint64_t)0x2e1b21385c26c926U, (uint64_t)0x4d2c6dfc5ac42aedU, (uint64_t)0x53380d139d95b3dfU, - (uint64_t)0x650a73548baf63deU, (uint64_t)0x766a0abb3c77b2a8U, (uint64_t)0x81c2c92e47edaee6U, - (uint64_t)0x92722c851482353bU, (uint64_t)0xa2bfe8a14cf10364U, (uint64_t)0xa81a664bbc423001U, - (uint64_t)0xc24b8b70d0f89791U, (uint64_t)0xc76c51a30654be30U, (uint64_t)0xd192e819d6ef5218U, - (uint64_t)0xd69906245565a910U, (uint64_t)0xf40e35855771202aU, (uint64_t)0x106aa07032bbd1b8U, - (uint64_t)0x19a4c116b8d2d0c8U, (uint64_t)0x1e376c085141ab53U, (uint64_t)0x2748774cdf8eeb99U, - (uint64_t)0x34b0bcb5e19b48a8U, (uint64_t)0x391c0cb3c5c95a63U, (uint64_t)0x4ed8aa4ae3418acbU, - (uint64_t)0x5b9cca4f7763e373U, (uint64_t)0x682e6ff3d6b2b8a3U, (uint64_t)0x748f82ee5defb2fcU, - (uint64_t)0x78a5636f43172f60U, (uint64_t)0x84c87814a1f0ab72U, (uint64_t)0x8cc702081a6439ecU, - (uint64_t)0x90befffa23631e28U, (uint64_t)0xa4506cebde82bde9U, (uint64_t)0xbef9a3f7b2c67915U, - (uint64_t)0xc67178f2e372532bU, (uint64_t)0xca273eceea26619cU, (uint64_t)0xd186b8c721c0c207U, - (uint64_t)0xeada7dd6cde0eb1eU, (uint64_t)0xf57d4f7fee6ed178U, (uint64_t)0x06f067aa72176fbaU, - (uint64_t)0x0a637dc5a2c898a6U, (uint64_t)0x113f9804bef90daeU, (uint64_t)0x1b710b35131c471bU, - (uint64_t)0x28db77f523047d84U, (uint64_t)0x32caab7b40c72493U, (uint64_t)0x3c9ebe0a15c9bebcU, - (uint64_t)0x431d67c49c100d4cU, (uint64_t)0x4cc5d4becb3e42b6U, (uint64_t)0x597f299cfc657e2aU, - (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U - }; - -static void update_224(uint32_t *hash, uint8_t *block) +static inline void sha256_init(uint32_t *hash) { - uint32_t hash1[8U] = { 0U }; - uint32_t computed_ws[64U] = { 0U }; - for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) - { - if (i < (uint32_t)16U) - { - uint8_t *b = block + i * (uint32_t)4U; - uint32_t u = load32_be(b); - computed_ws[i] = u; - } - else - { - uint32_t t16 = computed_ws[i - (uint32_t)16U]; - uint32_t t15 = computed_ws[i - (uint32_t)15U]; - uint32_t t7 = computed_ws[i - (uint32_t)7U]; - uint32_t t2 = computed_ws[i - (uint32_t)2U]; - uint32_t - s1 = - (t2 >> (uint32_t)17U | t2 << (uint32_t)15U) - ^ ((t2 >> (uint32_t)19U | t2 << (uint32_t)13U) ^ t2 >> (uint32_t)10U); - uint32_t - s0 = - (t15 >> (uint32_t)7U | t15 << (uint32_t)25U) - ^ ((t15 >> (uint32_t)18U | t15 << (uint32_t)14U) ^ t15 >> (uint32_t)3U); - uint32_t w = s1 + t7 + s0 + t16; - computed_ws[i] = w; - } - } - memcpy(hash1, hash, (uint32_t)8U * sizeof (uint32_t)); - for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) - { - uint32_t a0 = hash1[0U]; - uint32_t b0 = hash1[1U]; - uint32_t c0 = hash1[2U]; - uint32_t d0 = hash1[3U]; - uint32_t e0 = hash1[4U]; - uint32_t f0 = hash1[5U]; - uint32_t g0 = hash1[6U]; - uint32_t h02 = hash1[7U]; - uint32_t w = computed_ws[i]; - uint32_t - t1 = - h02 - + - ((e0 >> (uint32_t)6U | e0 << (uint32_t)26U) - ^ ((e0 >> (uint32_t)11U | e0 << (uint32_t)21U) ^ (e0 >> (uint32_t)25U | e0 << (uint32_t)7U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k224_256[i] - + w; - uint32_t - t2 = - ((a0 >> (uint32_t)2U | a0 << (uint32_t)30U) - ^ ((a0 >> (uint32_t)13U | a0 << (uint32_t)19U) ^ (a0 >> (uint32_t)22U | a0 << (uint32_t)10U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - hash1[0U] = t1 + t2; - hash1[1U] = a0; - hash1[2U] = b0; - hash1[3U] = c0; - hash1[4U] = d0 + t1; - hash1[5U] = e0; - hash1[6U] = f0; - hash1[7U] = g0; - } for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - uint32_t xi = hash[i]; - uint32_t yi = hash1[i]; - hash[i] = xi + yi; + uint32_t *os = hash; + uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; + os[i] = x; } } -static void update_256(uint32_t *hash, uint8_t *block) +static inline void sha256_update(uint8_t *b, uint32_t *hash) { - uint32_t hash1[8U] = { 0U }; - uint32_t computed_ws[64U] = { 0U }; - for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) - { - if (i < (uint32_t)16U) + uint32_t hash_old[8U] = { 0U }; + uint32_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint32_t)); + uint8_t *b10 = b; + uint32_t u = load32_be(b10); + ws[0U] = u; + uint32_t u0 = load32_be(b10 + (uint32_t)4U); + ws[1U] = u0; + uint32_t u1 = load32_be(b10 + (uint32_t)8U); + ws[2U] = u1; + uint32_t u2 = load32_be(b10 + (uint32_t)12U); + ws[3U] = u2; + uint32_t u3 = load32_be(b10 + (uint32_t)16U); + ws[4U] = u3; + uint32_t u4 = load32_be(b10 + (uint32_t)20U); + ws[5U] = u4; + uint32_t u5 = load32_be(b10 + (uint32_t)24U); + ws[6U] = u5; + uint32_t u6 = load32_be(b10 + (uint32_t)28U); + ws[7U] = u6; + uint32_t u7 = load32_be(b10 + (uint32_t)32U); + ws[8U] = u7; + uint32_t u8 = load32_be(b10 + (uint32_t)36U); + ws[9U] = u8; + uint32_t u9 = load32_be(b10 + (uint32_t)40U); + ws[10U] = u9; + uint32_t u10 = load32_be(b10 + (uint32_t)44U); + ws[11U] = u10; + uint32_t u11 = load32_be(b10 + (uint32_t)48U); + ws[12U] = u11; + uint32_t u12 = load32_be(b10 + (uint32_t)52U); + ws[13U] = u12; + uint32_t u13 = load32_be(b10 + (uint32_t)56U); + ws[14U] = u13; + uint32_t u14 = load32_be(b10 + (uint32_t)60U); + ws[15U] = u14; + for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) { - uint8_t *b = block + i * (uint32_t)4U; - uint32_t u = load32_be(b); - computed_ws[i] = u; - } - else - { - uint32_t t16 = computed_ws[i - (uint32_t)16U]; - uint32_t t15 = computed_ws[i - (uint32_t)15U]; - uint32_t t7 = computed_ws[i - (uint32_t)7U]; - uint32_t t2 = computed_ws[i - (uint32_t)2U]; + uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256[(uint32_t)16U * i0 + i]; + uint32_t ws_t = ws[i]; + uint32_t a0 = hash[0U]; + uint32_t b0 = hash[1U]; + uint32_t c0 = hash[2U]; + uint32_t d0 = hash[3U]; + uint32_t e0 = hash[4U]; + uint32_t f0 = hash[5U]; + uint32_t g0 = hash[6U]; + uint32_t h02 = hash[7U]; + uint32_t k_e_t = k_t; uint32_t - s1 = - (t2 >> (uint32_t)17U | t2 << (uint32_t)15U) - ^ ((t2 >> (uint32_t)19U | t2 << (uint32_t)13U) ^ t2 >> (uint32_t)10U); + t1 = + h02 + + + ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U) + ^ + ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U) + ^ (e0 << (uint32_t)7U | e0 >> (uint32_t)25U))) + + ((e0 & f0) ^ (~e0 & g0)) + + k_e_t + + ws_t; uint32_t - s0 = - (t15 >> (uint32_t)7U | t15 << (uint32_t)25U) - ^ ((t15 >> (uint32_t)18U | t15 << (uint32_t)14U) ^ t15 >> (uint32_t)3U); - uint32_t w = s1 + t7 + s0 + t16; - computed_ws[i] = w; + t2 = + ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U) + ^ + ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U) + ^ (a0 << (uint32_t)10U | a0 >> (uint32_t)22U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint32_t a1 = t1 + t2; + uint32_t b1 = a0; + uint32_t c1 = b0; + uint32_t d1 = c0; + uint32_t e1 = d0 + t1; + uint32_t f1 = e0; + uint32_t g1 = f0; + uint32_t h12 = g0; + hash[0U] = a1; + hash[1U] = b1; + hash[2U] = c1; + hash[3U] = d1; + hash[4U] = e1; + hash[5U] = f1; + hash[6U] = g1; + hash[7U] = h12; + } + if (i0 < (uint32_t)3U) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) + { + uint32_t t16 = ws[i]; + uint32_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint32_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint32_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint32_t + s1 = + (t2 << (uint32_t)15U | t2 >> (uint32_t)17U) + ^ ((t2 << (uint32_t)13U | t2 >> (uint32_t)19U) ^ t2 >> (uint32_t)10U); + uint32_t + s0 = + (t15 << (uint32_t)25U | t15 >> (uint32_t)7U) + ^ ((t15 << (uint32_t)14U | t15 >> (uint32_t)18U) ^ t15 >> (uint32_t)3U); + ws[i] = s1 + t7 + s0 + t16; + } } - } - memcpy(hash1, hash, (uint32_t)8U * sizeof (uint32_t)); - for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) - { - uint32_t a0 = hash1[0U]; - uint32_t b0 = hash1[1U]; - uint32_t c0 = hash1[2U]; - uint32_t d0 = hash1[3U]; - uint32_t e0 = hash1[4U]; - uint32_t f0 = hash1[5U]; - uint32_t g0 = hash1[6U]; - uint32_t h02 = hash1[7U]; - uint32_t w = computed_ws[i]; - uint32_t - t1 = - h02 - + - ((e0 >> (uint32_t)6U | e0 << (uint32_t)26U) - ^ ((e0 >> (uint32_t)11U | e0 << (uint32_t)21U) ^ (e0 >> (uint32_t)25U | e0 << (uint32_t)7U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k224_256[i] - + w; - uint32_t - t2 = - ((a0 >> (uint32_t)2U | a0 << (uint32_t)30U) - ^ ((a0 >> (uint32_t)13U | a0 << (uint32_t)19U) ^ (a0 >> (uint32_t)22U | a0 << (uint32_t)10U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - hash1[0U] = t1 + t2; - hash1[1U] = a0; - hash1[2U] = b0; - hash1[3U] = c0; - hash1[4U] = d0 + t1; - hash1[5U] = e0; - hash1[6U] = f0; - hash1[7U] = g0; } for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - uint32_t xi = hash[i]; - uint32_t yi = hash1[i]; - hash[i] = xi + yi; + uint32_t *os = hash; + uint32_t x = hash[i] + hash_old[i]; + os[i] = x; } } -static void update_384(uint64_t *hash, uint8_t *block) +static inline void sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) { - uint64_t hash1[8U] = { 0U }; - uint64_t computed_ws[80U] = { 0U }; - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) + uint32_t blocks = len / (uint32_t)64U; + for (uint32_t i = (uint32_t)0U; i < blocks; i++) { - if (i < (uint32_t)16U) - { - uint8_t *b = block + i * (uint32_t)8U; - uint64_t u = load64_be(b); - computed_ws[i] = u; - } - else - { - uint64_t t16 = computed_ws[i - (uint32_t)16U]; - uint64_t t15 = computed_ws[i - (uint32_t)15U]; - uint64_t t7 = computed_ws[i - (uint32_t)7U]; - uint64_t t2 = computed_ws[i - (uint32_t)2U]; - uint64_t - s1 = - (t2 >> (uint32_t)19U | t2 << (uint32_t)45U) - ^ ((t2 >> (uint32_t)61U | t2 << (uint32_t)3U) ^ t2 >> (uint32_t)6U); - uint64_t - s0 = - (t15 >> (uint32_t)1U | t15 << (uint32_t)63U) - ^ ((t15 >> (uint32_t)8U | t15 << (uint32_t)56U) ^ t15 >> (uint32_t)7U); - uint64_t w = s1 + t7 + s0 + t16; - computed_ws[i] = w; - } - } - memcpy(hash1, hash, (uint32_t)8U * sizeof (uint64_t)); - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) - { - uint64_t a0 = hash1[0U]; - uint64_t b0 = hash1[1U]; - uint64_t c0 = hash1[2U]; - uint64_t d0 = hash1[3U]; - uint64_t e0 = hash1[4U]; - uint64_t f0 = hash1[5U]; - uint64_t g0 = hash1[6U]; - uint64_t h02 = hash1[7U]; - uint64_t w = computed_ws[i]; - uint64_t - t1 = - h02 - + - ((e0 >> (uint32_t)14U | e0 << (uint32_t)50U) - ^ - ((e0 >> (uint32_t)18U | e0 << (uint32_t)46U) - ^ (e0 >> (uint32_t)41U | e0 << (uint32_t)23U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k384_512[i] - + w; - uint64_t - t2 = - ((a0 >> (uint32_t)28U | a0 << (uint32_t)36U) - ^ ((a0 >> (uint32_t)34U | a0 << (uint32_t)30U) ^ (a0 >> (uint32_t)39U | a0 << (uint32_t)25U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - hash1[0U] = t1 + t2; - hash1[1U] = a0; - hash1[2U] = b0; - hash1[3U] = c0; - hash1[4U] = d0 + t1; - hash1[5U] = e0; - hash1[6U] = f0; - hash1[7U] = g0; - } - for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) - { - uint64_t xi = hash[i]; - uint64_t yi = hash1[i]; - hash[i] = xi + yi; + uint8_t *b0 = b; + uint8_t *mb = b0 + i * (uint32_t)64U; + sha256_update(mb, st); } } -static void update_512(uint64_t *hash, uint8_t *block) +static inline void +sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash) { - uint64_t hash1[8U] = { 0U }; - uint64_t computed_ws[80U] = { 0U }; - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) + uint32_t blocks; + if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U) { - if (i < (uint32_t)16U) - { - uint8_t *b = block + i * (uint32_t)8U; - uint64_t u = load64_be(b); - computed_ws[i] = u; - } - else - { - uint64_t t16 = computed_ws[i - (uint32_t)16U]; - uint64_t t15 = computed_ws[i - (uint32_t)15U]; - uint64_t t7 = computed_ws[i - (uint32_t)7U]; - uint64_t t2 = computed_ws[i - (uint32_t)2U]; - uint64_t - s1 = - (t2 >> (uint32_t)19U | t2 << (uint32_t)45U) - ^ ((t2 >> (uint32_t)61U | t2 << (uint32_t)3U) ^ t2 >> (uint32_t)6U); - uint64_t - s0 = - (t15 >> (uint32_t)1U | t15 << (uint32_t)63U) - ^ ((t15 >> (uint32_t)8U | t15 << (uint32_t)56U) ^ t15 >> (uint32_t)7U); - uint64_t w = s1 + t7 + s0 + t16; - computed_ws[i] = w; - } + blocks = (uint32_t)1U; } - memcpy(hash1, hash, (uint32_t)8U * sizeof (uint64_t)); - for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i++) - { - uint64_t a0 = hash1[0U]; - uint64_t b0 = hash1[1U]; - uint64_t c0 = hash1[2U]; - uint64_t d0 = hash1[3U]; - uint64_t e0 = hash1[4U]; - uint64_t f0 = hash1[5U]; - uint64_t g0 = hash1[6U]; - uint64_t h02 = hash1[7U]; - uint64_t w = computed_ws[i]; - uint64_t - t1 = - h02 - + - ((e0 >> (uint32_t)14U | e0 << (uint32_t)50U) - ^ - ((e0 >> (uint32_t)18U | e0 << (uint32_t)46U) - ^ (e0 >> (uint32_t)41U | e0 << (uint32_t)23U))) - + ((e0 & f0) ^ (~e0 & g0)) - + k384_512[i] - + w; - uint64_t - t2 = - ((a0 >> (uint32_t)28U | a0 << (uint32_t)36U) - ^ ((a0 >> (uint32_t)34U | a0 << (uint32_t)30U) ^ (a0 >> (uint32_t)39U | a0 << (uint32_t)25U))) - + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); - hash1[0U] = t1 + t2; - hash1[1U] = a0; - hash1[2U] = b0; - hash1[3U] = c0; - hash1[4U] = d0 + t1; - hash1[5U] = e0; - hash1[6U] = f0; - hash1[7U] = g0; - } - for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) + else { - uint64_t xi = hash[i]; - uint64_t yi = hash1[i]; - hash[i] = xi + yi; + blocks = (uint32_t)2U; + } + uint32_t fin = blocks * (uint32_t)64U; + uint8_t last[128U] = { 0U }; + uint8_t totlen_buf[8U] = { 0U }; + uint64_t total_len_bits = totlen << (uint32_t)3U; + store64_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof (uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)8U, totlen_buf, (uint32_t)8U * sizeof (uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)64U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha256_update(last0, hash); + if (blocks > (uint32_t)1U) + { + sha256_update(last1, hash); } } -static void pad_224(uint64_t len, uint8_t *dst) +static inline void sha256_finish(uint32_t *st, uint8_t *h) { - uint8_t *dst1 = dst; - dst1[0U] = (uint8_t)0x80U; - uint8_t *dst2 = dst + (uint32_t)1U; - for - (uint32_t - i = (uint32_t)0U; - i - < ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(len % (uint64_t)(uint32_t)64U))) % (uint32_t)64U; - i++) + uint8_t hbuf[32U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - dst2[i] = (uint8_t)0U; + store32_be(hbuf + i * (uint32_t)4U, st[i]); } - uint8_t - *dst3 = - dst - + - (uint32_t)1U - + - ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(len % (uint64_t)(uint32_t)64U))) - % (uint32_t)64U; - store64_be(dst3, len << (uint32_t)3U); + memcpy(h, hbuf, (uint32_t)32U * sizeof (uint8_t)); } -static void pad_256(uint64_t len, uint8_t *dst) +static inline void sha224_init(uint32_t *hash) { - uint8_t *dst1 = dst; - dst1[0U] = (uint8_t)0x80U; - uint8_t *dst2 = dst + (uint32_t)1U; - for - (uint32_t - i = (uint32_t)0U; - i - < ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(len % (uint64_t)(uint32_t)64U))) % (uint32_t)64U; - i++) + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - dst2[i] = (uint8_t)0U; + uint32_t *os = hash; + uint32_t x = Hacl_Impl_SHA2_Generic_h224[i]; + os[i] = x; } - uint8_t - *dst3 = - dst - + - (uint32_t)1U - + - ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(len % (uint64_t)(uint32_t)64U))) - % (uint32_t)64U; - store64_be(dst3, len << (uint32_t)3U); } -static void pad_384(FStar_UInt128_uint128 len, uint8_t *dst) +static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) { - uint8_t *dst1 = dst; - dst1[0U] = (uint8_t)0x80U; - uint8_t *dst2 = dst + (uint32_t)1U; - for - (uint32_t - i = (uint32_t)0U; - i - < - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - i++) - { - dst2[i] = (uint8_t)0U; - } - uint8_t - *dst3 = - dst - + - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_shift_left(len, (uint32_t)3U); - store128_be(dst3, len_); + sha256_update_nblocks(len, b, st); } -static void pad_512(FStar_UInt128_uint128 len, uint8_t *dst) +static void sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st) { - uint8_t *dst1 = dst; - dst1[0U] = (uint8_t)0x80U; - uint8_t *dst2 = dst + (uint32_t)1U; - for - (uint32_t - i = (uint32_t)0U; - i - < - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - i++) - { - dst2[i] = (uint8_t)0U; - } - uint8_t - *dst3 = - dst - + - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_shift_left(len, (uint32_t)3U); - store128_be(dst3, len_); + sha256_update_last(totlen, len, b, st); } -static void finish_224(uint32_t *s, uint8_t *dst) +static inline void sha224_finish(uint32_t *st, uint8_t *h) { - for (uint32_t i = (uint32_t)0U; i < (uint32_t)7U; i++) + uint8_t hbuf[32U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - store32_be(dst + i * (uint32_t)4U, s[i]); + store32_be(hbuf + i * (uint32_t)4U, st[i]); } + memcpy(h, hbuf, (uint32_t)28U * sizeof (uint8_t)); } -static void finish_256(uint32_t *s, uint8_t *dst) +static void sha512_init(uint64_t *hash) { for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - store32_be(dst + i * (uint32_t)4U, s[i]); + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; + os[i] = x; } } -static void finish_384(uint64_t *s, uint8_t *dst) +static inline void sha512_update(uint8_t *b, uint64_t *hash) { - for (uint32_t i = (uint32_t)0U; i < (uint32_t)6U; i++) - { - store64_be(dst + i * (uint32_t)8U, s[i]); + uint64_t hash_old[8U] = { 0U }; + uint64_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint64_t)); + uint8_t *b10 = b; + uint64_t u = load64_be(b10); + ws[0U] = u; + uint64_t u0 = load64_be(b10 + (uint32_t)8U); + ws[1U] = u0; + uint64_t u1 = load64_be(b10 + (uint32_t)16U); + ws[2U] = u1; + uint64_t u2 = load64_be(b10 + (uint32_t)24U); + ws[3U] = u2; + uint64_t u3 = load64_be(b10 + (uint32_t)32U); + ws[4U] = u3; + uint64_t u4 = load64_be(b10 + (uint32_t)40U); + ws[5U] = u4; + uint64_t u5 = load64_be(b10 + (uint32_t)48U); + ws[6U] = u5; + uint64_t u6 = load64_be(b10 + (uint32_t)56U); + ws[7U] = u6; + uint64_t u7 = load64_be(b10 + (uint32_t)64U); + ws[8U] = u7; + uint64_t u8 = load64_be(b10 + (uint32_t)72U); + ws[9U] = u8; + uint64_t u9 = load64_be(b10 + (uint32_t)80U); + ws[10U] = u9; + uint64_t u10 = load64_be(b10 + (uint32_t)88U); + ws[11U] = u10; + uint64_t u11 = load64_be(b10 + (uint32_t)96U); + ws[12U] = u11; + uint64_t u12 = load64_be(b10 + (uint32_t)104U); + ws[13U] = u12; + uint64_t u13 = load64_be(b10 + (uint32_t)112U); + ws[14U] = u13; + uint64_t u14 = load64_be(b10 + (uint32_t)120U); + ws[15U] = u14; + for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)5U; i0++) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) + { + uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512[(uint32_t)16U * i0 + i]; + uint64_t ws_t = ws[i]; + uint64_t a0 = hash[0U]; + uint64_t b0 = hash[1U]; + uint64_t c0 = hash[2U]; + uint64_t d0 = hash[3U]; + uint64_t e0 = hash[4U]; + uint64_t f0 = hash[5U]; + uint64_t g0 = hash[6U]; + uint64_t h02 = hash[7U]; + uint64_t k_e_t = k_t; + uint64_t + t1 = + h02 + + + ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U) + ^ + ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U) + ^ (e0 << (uint32_t)23U | e0 >> (uint32_t)41U))) + + ((e0 & f0) ^ (~e0 & g0)) + + k_e_t + + ws_t; + uint64_t + t2 = + ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U) + ^ + ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U) + ^ (a0 << (uint32_t)25U | a0 >> (uint32_t)39U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint64_t a1 = t1 + t2; + uint64_t b1 = a0; + uint64_t c1 = b0; + uint64_t d1 = c0; + uint64_t e1 = d0 + t1; + uint64_t f1 = e0; + uint64_t g1 = f0; + uint64_t h12 = g0; + hash[0U] = a1; + hash[1U] = b1; + hash[2U] = c1; + hash[3U] = d1; + hash[4U] = e1; + hash[5U] = f1; + hash[6U] = g1; + hash[7U] = h12; + } + if (i0 < (uint32_t)4U) + { + for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) + { + uint64_t t16 = ws[i]; + uint64_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint64_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint64_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint64_t + s1 = + (t2 << (uint32_t)45U | t2 >> (uint32_t)19U) + ^ ((t2 << (uint32_t)3U | t2 >> (uint32_t)61U) ^ t2 >> (uint32_t)6U); + uint64_t + s0 = + (t15 << (uint32_t)63U | t15 >> (uint32_t)1U) + ^ ((t15 << (uint32_t)56U | t15 >> (uint32_t)8U) ^ t15 >> (uint32_t)7U); + ws[i] = s1 + t7 + s0 + t16; + } + } } -} - -static void finish_512(uint64_t *s, uint8_t *dst) -{ for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - store64_be(dst + i * (uint32_t)8U, s[i]); + uint64_t *os = hash; + uint64_t x = hash[i] + hash_old[i]; + os[i] = x; } } -static void update_multi_224(uint32_t *s, uint8_t *blocks, uint32_t n_blocks) +static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) { - for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) + uint32_t blocks = len / (uint32_t)128U; + for (uint32_t i = (uint32_t)0U; i < blocks; i++) { - uint32_t sz = (uint32_t)64U; - uint8_t *block = blocks + sz * i; - update_224(s, block); + uint8_t *b0 = b; + uint8_t *mb = b0 + i * (uint32_t)128U; + sha512_update(mb, st); } } -static void update_multi_256(uint32_t *s, uint8_t *blocks, uint32_t n_blocks) +static inline void +sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash) { - for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) + uint32_t blocks; + if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U) { - uint32_t sz = (uint32_t)64U; - uint8_t *block = blocks + sz * i; - update_256(s, block); + blocks = (uint32_t)1U; } -} - -static void update_multi_384(uint64_t *s, uint8_t *blocks, uint32_t n_blocks) -{ - for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) + else { - uint32_t sz = (uint32_t)128U; - uint8_t *block = blocks + sz * i; - update_384(s, block); + blocks = (uint32_t)2U; + } + uint32_t fin = blocks * (uint32_t)128U; + uint8_t last[256U] = { 0U }; + uint8_t totlen_buf[16U] = { 0U }; + FStar_UInt128_uint128 total_len_bits = FStar_UInt128_shift_left(totlen, (uint32_t)3U); + store128_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof (uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)16U, totlen_buf, (uint32_t)16U * sizeof (uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)128U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha512_update(last0, hash); + if (blocks > (uint32_t)1U) + { + sha512_update(last1, hash); } } -static void update_multi_512(uint64_t *s, uint8_t *blocks, uint32_t n_blocks) +static inline void sha512_finish(uint64_t *st, uint8_t *h) { - for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) + uint8_t hbuf[64U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - uint32_t sz = (uint32_t)128U; - uint8_t *block = blocks + sz * i; - update_512(s, block); + store64_be(hbuf + i * (uint32_t)8U, st[i]); } + memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t)); } -static void update_last_224(uint32_t *s, uint64_t prev_len, uint8_t *input, uint32_t input_len) +static inline void sha384_init(uint64_t *hash) { - uint32_t blocks_n = input_len / (uint32_t)64U; - uint32_t blocks_len = blocks_n * (uint32_t)64U; - uint8_t *blocks = input; - uint32_t rest_len = input_len - blocks_len; - uint8_t *rest = input + blocks_len; - update_multi_224(s, blocks, blocks_n); - uint64_t total_input_len = prev_len + (uint64_t)input_len; - uint32_t - pad_len = - (uint32_t)1U - + - ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(total_input_len % (uint64_t)(uint32_t)64U))) - % (uint32_t)64U - + (uint32_t)8U; - uint32_t tmp_len = rest_len + pad_len; - uint8_t tmp_twoblocks[128U] = { 0U }; - uint8_t *tmp = tmp_twoblocks; - uint8_t *tmp_rest = tmp; - uint8_t *tmp_pad = tmp + rest_len; - memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t)); - pad_224(total_input_len, tmp_pad); - update_multi_224(s, tmp, tmp_len / (uint32_t)64U); + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) + { + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; + os[i] = x; + } } -static void update_last_256(uint32_t *s, uint64_t prev_len, uint8_t *input, uint32_t input_len) +static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st) { - uint32_t blocks_n = input_len / (uint32_t)64U; - uint32_t blocks_len = blocks_n * (uint32_t)64U; - uint8_t *blocks = input; - uint32_t rest_len = input_len - blocks_len; - uint8_t *rest = input + blocks_len; - update_multi_256(s, blocks, blocks_n); - uint64_t total_input_len = prev_len + (uint64_t)input_len; - uint32_t - pad_len = - (uint32_t)1U - + - ((uint32_t)128U - ((uint32_t)9U + (uint32_t)(total_input_len % (uint64_t)(uint32_t)64U))) - % (uint32_t)64U - + (uint32_t)8U; - uint32_t tmp_len = rest_len + pad_len; - uint8_t tmp_twoblocks[128U] = { 0U }; - uint8_t *tmp = tmp_twoblocks; - uint8_t *tmp_rest = tmp; - uint8_t *tmp_pad = tmp + rest_len; - memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t)); - pad_256(total_input_len, tmp_pad); - update_multi_256(s, tmp, tmp_len / (uint32_t)64U); + sha512_update_nblocks(len, b, st); } static void -update_last_384( - uint64_t *s, - FStar_UInt128_uint128 prev_len, - uint8_t *input, - uint32_t input_len -) +sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st) { - uint32_t blocks_n = input_len / (uint32_t)128U; - uint32_t blocks_len = blocks_n * (uint32_t)128U; - uint8_t *blocks = input; - uint32_t rest_len = input_len - blocks_len; - uint8_t *rest = input + blocks_len; - update_multi_384(s, blocks, blocks_n); - FStar_UInt128_uint128 - total_input_len = - FStar_UInt128_add(prev_len, - FStar_UInt128_uint64_to_uint128((uint64_t)input_len)); - uint32_t - pad_len = - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(total_input_len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U - + (uint32_t)16U; - uint32_t tmp_len = rest_len + pad_len; - uint8_t tmp_twoblocks[256U] = { 0U }; - uint8_t *tmp = tmp_twoblocks; - uint8_t *tmp_rest = tmp; - uint8_t *tmp_pad = tmp + rest_len; - memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t)); - pad_384(total_input_len, tmp_pad); - update_multi_384(s, tmp, tmp_len / (uint32_t)128U); + sha512_update_last(totlen, len, b, st); } -static void -update_last_512( - uint64_t *s, - FStar_UInt128_uint128 prev_len, - uint8_t *input, - uint32_t input_len -) +static inline void sha384_finish(uint64_t *st, uint8_t *h) { - uint32_t blocks_n = input_len / (uint32_t)128U; - uint32_t blocks_len = blocks_n * (uint32_t)128U; - uint8_t *blocks = input; - uint32_t rest_len = input_len - blocks_len; - uint8_t *rest = input + blocks_len; - update_multi_512(s, blocks, blocks_n); - FStar_UInt128_uint128 - total_input_len = - FStar_UInt128_add(prev_len, - FStar_UInt128_uint64_to_uint128((uint64_t)input_len)); - uint32_t - pad_len = - (uint32_t)1U - + - ((uint32_t)256U - - - ((uint32_t)17U - + (uint32_t)(FStar_UInt128_uint128_to_uint64(total_input_len) % (uint64_t)(uint32_t)128U))) - % (uint32_t)128U - + (uint32_t)16U; - uint32_t tmp_len = rest_len + pad_len; - uint8_t tmp_twoblocks[256U] = { 0U }; - uint8_t *tmp = tmp_twoblocks; - uint8_t *tmp_rest = tmp; - uint8_t *tmp_pad = tmp + rest_len; - memcpy(tmp_rest, rest, rest_len * sizeof (uint8_t)); - pad_512(total_input_len, tmp_pad); - update_multi_512(s, tmp, tmp_len / (uint32_t)128U); -} - -static void hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst) -{ - uint32_t - s[8U] = - { - (uint32_t)0xc1059ed8U, (uint32_t)0x367cd507U, (uint32_t)0x3070dd17U, (uint32_t)0xf70e5939U, - (uint32_t)0xffc00b31U, (uint32_t)0x68581511U, (uint32_t)0x64f98fa7U, (uint32_t)0xbefa4fa4U - }; - uint32_t blocks_n0 = input_len / (uint32_t)64U; - uint32_t blocks_n1; - if (input_len % (uint32_t)64U == (uint32_t)0U && blocks_n0 > (uint32_t)0U) - { - blocks_n1 = blocks_n0 - (uint32_t)1U; - } - else + uint8_t hbuf[64U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i++) { - blocks_n1 = blocks_n0; + store64_be(hbuf + i * (uint32_t)8U, st[i]); } - uint32_t blocks_len0 = blocks_n1 * (uint32_t)64U; - uint8_t *blocks0 = input; - uint32_t rest_len0 = input_len - blocks_len0; - uint8_t *rest0 = input + blocks_len0; - uint32_t blocks_n = blocks_n1; - uint32_t blocks_len = blocks_len0; - uint8_t *blocks = blocks0; - uint32_t rest_len = rest_len0; - uint8_t *rest = rest0; - update_multi_224(s, blocks, blocks_n); - update_last_224(s, (uint64_t)blocks_len, rest, rest_len); - finish_224(s, dst); + memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t)); } +/** +Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. +*/ static void hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst) { - uint32_t - s[8U] = - { - (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, (uint32_t)0xa54ff53aU, - (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U - }; - uint32_t blocks_n0 = input_len / (uint32_t)64U; - uint32_t blocks_n1; - if (input_len % (uint32_t)64U == (uint32_t)0U && blocks_n0 > (uint32_t)0U) - { - blocks_n1 = blocks_n0 - (uint32_t)1U; - } - else - { - blocks_n1 = blocks_n0; - } - uint32_t blocks_len0 = blocks_n1 * (uint32_t)64U; - uint8_t *blocks0 = input; - uint32_t rest_len0 = input_len - blocks_len0; - uint8_t *rest0 = input + blocks_len0; - uint32_t blocks_n = blocks_n1; - uint32_t blocks_len = blocks_len0; - uint8_t *blocks = blocks0; - uint32_t rest_len = rest_len0; - uint8_t *rest = rest0; - update_multi_256(s, blocks, blocks_n); - update_last_256(s, (uint64_t)blocks_len, rest, rest_len); - finish_256(s, dst); + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + sha256_init(st); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + sha256_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)64U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + sha256_update_last(len_, rem, lb, st); + sha256_finish(st, rb); } -static void hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst) +/** +Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. +*/ +static void hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst) { - uint64_t - s[8U] = - { - (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, (uint64_t)0x9159015a3070dd17U, - (uint64_t)0x152fecd8f70e5939U, (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, - (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U - }; - uint32_t blocks_n0 = input_len / (uint32_t)128U; - uint32_t blocks_n1; - if (input_len % (uint32_t)128U == (uint32_t)0U && blocks_n0 > (uint32_t)0U) - { - blocks_n1 = blocks_n0 - (uint32_t)1U; - } - else - { - blocks_n1 = blocks_n0; - } - uint32_t blocks_len0 = blocks_n1 * (uint32_t)128U; - uint8_t *blocks0 = input; - uint32_t rest_len0 = input_len - blocks_len0; - uint8_t *rest0 = input + blocks_len0; - uint32_t blocks_n = blocks_n1; - uint32_t blocks_len = blocks_len0; - uint8_t *blocks = blocks0; - uint32_t rest_len = rest_len0; - uint8_t *rest = rest0; - update_multi_384(s, blocks, blocks_n); - update_last_384(s, FStar_UInt128_uint64_to_uint128((uint64_t)blocks_len), rest, rest_len); - finish_384(s, dst); + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + sha224_init(st); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + sha224_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)64U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + sha224_update_last(len_, rem, lb, st); + sha224_finish(st, rb); } +/** +Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. +*/ static void hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst) { - uint64_t - s[8U] = - { - (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, (uint64_t)0x3c6ef372fe94f82bU, - (uint64_t)0xa54ff53a5f1d36f1U, (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, - (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U - }; - uint32_t blocks_n0 = input_len / (uint32_t)128U; - uint32_t blocks_n1; - if (input_len % (uint32_t)128U == (uint32_t)0U && blocks_n0 > (uint32_t)0U) - { - blocks_n1 = blocks_n0 - (uint32_t)1U; - } - else - { - blocks_n1 = blocks_n0; - } - uint32_t blocks_len0 = blocks_n1 * (uint32_t)128U; - uint8_t *blocks0 = input; - uint32_t rest_len0 = input_len - blocks_len0; - uint8_t *rest0 = input + blocks_len0; - uint32_t blocks_n = blocks_n1; - uint32_t blocks_len = blocks_len0; - uint8_t *blocks = blocks0; - uint32_t rest_len = rest_len0; - uint8_t *rest = rest0; - update_multi_512(s, blocks, blocks_n); - update_last_512(s, FStar_UInt128_uint64_to_uint128((uint64_t)blocks_len), rest, rest_len); - finish_512(s, dst); + uint8_t *ib = input; + uint8_t *rb = dst; + uint64_t st[8U] = { 0U }; + sha512_init(st); + uint32_t rem = input_len % (uint32_t)128U; + FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); + sha512_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)128U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + sha512_update_last(len_, rem, lb, st); + sha512_finish(st, rb); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. +*/ +static void hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint64_t st[8U] = { 0U }; + sha384_init(st); + uint32_t rem = input_len % (uint32_t)128U; + FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); + sha384_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)128U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + sha384_update_last(len_, rem, lb, st); + sha384_finish(st, rb); } extern void C_String_print(C_String_t uu___); diff --git a/dist/test/c/Hacl_Test_SHA2.h b/dist/test/c/Hacl_Test_SHA2.h index e6b22662ac..c6853307e5 100644 --- a/dist/test/c/Hacl_Test_SHA2.h +++ b/dist/test/c/Hacl_Test_SHA2.h @@ -26,6 +26,7 @@ #ifndef __Hacl_Test_SHA2_H #define __Hacl_Test_SHA2_H +#include "internal/Hacl_Hash_SHA2.h" #include "krmllib.h" #include "libintvector.h" diff --git a/dist/test/c/Hacl_Test_SHA3.h b/dist/test/c/Hacl_Test_SHA3.h index 4882360a84..27aee76dfc 100644 --- a/dist/test/c/Hacl_Test_SHA3.h +++ b/dist/test/c/Hacl_Test_SHA3.h @@ -26,6 +26,7 @@ #ifndef __Hacl_Test_SHA3_H #define __Hacl_Test_SHA3_H +#include "internal/Hacl_Hash_SHA2.h" #include "krmllib.h" #include "libintvector.h" diff --git a/dist/test/c/Test.h b/dist/test/c/Test.h index e91b2137c6..a83c369ae6 100644 --- a/dist/test/c/Test.h +++ b/dist/test/c/Test.h @@ -28,6 +28,7 @@ #include "krml/internal/compat.h" +#include "internal/Hacl_Hash_SHA2.h" #include "krmllib.h" #include "libintvector.h" diff --git a/dist/test/c/internal/Test.h b/dist/test/c/internal/Test.h index 9cd1e60498..f482c60247 100644 --- a/dist/test/c/internal/Test.h +++ b/dist/test/c/internal/Test.h @@ -29,6 +29,7 @@ #include "krml/internal/compat.h" #include "../Test.h" +#include "internal/Hacl_Hash_SHA2.h" #include "krmllib.h" #include "libintvector.h" diff --git a/dist/wasm/Hacl_SHA2_Generic.wasm b/dist/wasm/Hacl_SHA2_Generic.wasm deleted file mode 100644 index cf032070d6..0000000000 Binary files a/dist/wasm/Hacl_SHA2_Generic.wasm and /dev/null differ diff --git a/dist/wasm/Hacl_Streaming_SHA2.wasm b/dist/wasm/Hacl_Streaming_SHA2.wasm deleted file mode 100644 index 150957bfcc..0000000000 Binary files a/dist/wasm/Hacl_Streaming_SHA2.wasm and /dev/null differ