Revision 539576ec53104316dacac738fca7bc8fd967de62 authored by Son Ho on 26 February 2021, 12:56:35 UTC, committed by Son Ho on 26 February 2021, 12:56:35 UTC
generate the target architecture #define
1 parent 7fc6186
Hacl_HMAC_DRBG.c
/* MIT License
*
* Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
*
* 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 "Hacl_HMAC_DRBG.h"
uint32_t Hacl_HMAC_DRBG_reseed_interval = (uint32_t)1024U;
uint32_t Hacl_HMAC_DRBG_max_output_length = (uint32_t)65536U;
uint32_t Hacl_HMAC_DRBG_max_length = (uint32_t)65536U;
uint32_t Hacl_HMAC_DRBG_max_personalization_string_length = (uint32_t)65536U;
uint32_t Hacl_HMAC_DRBG_max_additional_input_length = (uint32_t)65536U;
uint32_t Hacl_HMAC_DRBG_min_length(Spec_Hash_Definitions_hash_alg a)
{
switch (a)
{
case Spec_Hash_Definitions_SHA1:
{
return (uint32_t)16U;
}
case Spec_Hash_Definitions_SHA2_256:
{
return (uint32_t)32U;
}
case Spec_Hash_Definitions_SHA2_384:
{
return (uint32_t)32U;
}
case Spec_Hash_Definitions_SHA2_512:
{
return (uint32_t)32U;
}
default:
{
KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
bool
Hacl_HMAC_DRBG_uu___is_State(Spec_Hash_Definitions_hash_alg a, Hacl_HMAC_DRBG_state projectee)
{
return true;
}
uint8_t
*Hacl_HMAC_DRBG___proj__State__item__k(
Spec_Hash_Definitions_hash_alg a,
Hacl_HMAC_DRBG_state projectee
)
{
return projectee.k;
}
uint8_t
*Hacl_HMAC_DRBG___proj__State__item__v(
Spec_Hash_Definitions_hash_alg a,
Hacl_HMAC_DRBG_state projectee
)
{
return projectee.v;
}
uint32_t
*Hacl_HMAC_DRBG___proj__State__item__reseed_counter(
Spec_Hash_Definitions_hash_alg a,
Hacl_HMAC_DRBG_state projectee
)
{
return projectee.reseed_counter;
}
Hacl_HMAC_DRBG_state Hacl_HMAC_DRBG_create_in(Spec_Hash_Definitions_hash_alg a)
{
uint8_t *k;
switch (a)
{
case Spec_Hash_Definitions_SHA1:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)20U, sizeof (uint8_t));
k = buf;
break;
}
case Spec_Hash_Definitions_SHA2_256:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)32U, sizeof (uint8_t));
k = buf;
break;
}
case Spec_Hash_Definitions_SHA2_384:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)48U, sizeof (uint8_t));
k = buf;
break;
}
case Spec_Hash_Definitions_SHA2_512:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
k = buf;
break;
}
default:
{
KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
{
uint8_t *v;
switch (a)
{
case Spec_Hash_Definitions_SHA1:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)20U, sizeof (uint8_t));
v = buf;
break;
}
case Spec_Hash_Definitions_SHA2_256:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)32U, sizeof (uint8_t));
v = buf;
break;
}
case Spec_Hash_Definitions_SHA2_384:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)48U, sizeof (uint8_t));
v = buf;
break;
}
case Spec_Hash_Definitions_SHA2_512:
{
uint8_t *buf = KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
v = buf;
break;
}
default:
{
KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
{
uint32_t *ctr = KRML_HOST_MALLOC(sizeof (uint32_t));
ctr[0U] = (uint32_t)1U;
{
Hacl_HMAC_DRBG_state lit;
lit.k = k;
lit.v = v;
lit.reseed_counter = ctr;
return lit;
}
}
}
}
void
Hacl_HMAC_DRBG_instantiate(
Spec_Hash_Definitions_hash_alg a,
Hacl_HMAC_DRBG_state st,
uint32_t entropy_input_len,
uint8_t *entropy_input,
uint32_t nonce_len,
uint8_t *nonce,
uint32_t personalization_string_len,
uint8_t *personalization_string
)
{
switch (a)
{
case Spec_Hash_Definitions_SHA1:
{
KRML_CHECK_SIZE(sizeof (uint8_t),
entropy_input_len + nonce_len + personalization_string_len);
{
uint8_t seed_material[entropy_input_len + nonce_len + personalization_string_len];
memset(seed_material,
0U,
(entropy_input_len + nonce_len + personalization_string_len) * sizeof (uint8_t));
{
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len, nonce, nonce_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len + nonce_len,
personalization_string,
personalization_string_len * sizeof (uint8_t));
k = st.k;
v = st.v;
ctr = st.reseed_counter;
memset(k, 0U, (uint32_t)20U * sizeof (uint8_t));
memset(v, (uint8_t)1U, (uint32_t)20U * sizeof (uint8_t));
ctr[0U] = (uint32_t)1U;
{
uint32_t
input_len = (uint32_t)21U + entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)20U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)21U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input0[20U] = (uint8_t)0U;
Hacl_HMAC_legacy_compute_sha1(k_, k, (uint32_t)20U, input0, input_len);
Hacl_HMAC_legacy_compute_sha1(v, k_, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_, (uint32_t)20U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
uint32_t
input_len0 =
(uint32_t)21U
+ entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)20U * sizeof (uint8_t));
if
(entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)21U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input[20U] = (uint8_t)1U;
Hacl_HMAC_legacy_compute_sha1(k_0, k, (uint32_t)20U, input, input_len0);
Hacl_HMAC_legacy_compute_sha1(v, k_0, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_0, (uint32_t)20U * sizeof (uint8_t));
}
}
}
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_256:
{
KRML_CHECK_SIZE(sizeof (uint8_t),
entropy_input_len + nonce_len + personalization_string_len);
{
uint8_t seed_material[entropy_input_len + nonce_len + personalization_string_len];
memset(seed_material,
0U,
(entropy_input_len + nonce_len + personalization_string_len) * sizeof (uint8_t));
{
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len, nonce, nonce_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len + nonce_len,
personalization_string,
personalization_string_len * sizeof (uint8_t));
k = st.k;
v = st.v;
ctr = st.reseed_counter;
memset(k, 0U, (uint32_t)32U * sizeof (uint8_t));
memset(v, (uint8_t)1U, (uint32_t)32U * sizeof (uint8_t));
ctr[0U] = (uint32_t)1U;
{
uint32_t
input_len = (uint32_t)33U + entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)32U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)33U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input0[32U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_256(k_, k, (uint32_t)32U, input0, input_len);
Hacl_HMAC_compute_sha2_256(v, k_, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_, (uint32_t)32U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
uint32_t
input_len0 =
(uint32_t)33U
+ entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)32U * sizeof (uint8_t));
if
(entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)33U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input[32U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_256(k_0, k, (uint32_t)32U, input, input_len0);
Hacl_HMAC_compute_sha2_256(v, k_0, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_0, (uint32_t)32U * sizeof (uint8_t));
}
}
}
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_384:
{
KRML_CHECK_SIZE(sizeof (uint8_t),
entropy_input_len + nonce_len + personalization_string_len);
{
uint8_t seed_material[entropy_input_len + nonce_len + personalization_string_len];
memset(seed_material,
0U,
(entropy_input_len + nonce_len + personalization_string_len) * sizeof (uint8_t));
{
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len, nonce, nonce_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len + nonce_len,
personalization_string,
personalization_string_len * sizeof (uint8_t));
k = st.k;
v = st.v;
ctr = st.reseed_counter;
memset(k, 0U, (uint32_t)48U * sizeof (uint8_t));
memset(v, (uint8_t)1U, (uint32_t)48U * sizeof (uint8_t));
ctr[0U] = (uint32_t)1U;
{
uint32_t
input_len = (uint32_t)49U + entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)48U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)49U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input0[48U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_384(k_, k, (uint32_t)48U, input0, input_len);
Hacl_HMAC_compute_sha2_384(v, k_, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_, (uint32_t)48U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
uint32_t
input_len0 =
(uint32_t)49U
+ entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)48U * sizeof (uint8_t));
if
(entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)49U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input[48U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_384(k_0, k, (uint32_t)48U, input, input_len0);
Hacl_HMAC_compute_sha2_384(v, k_0, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_0, (uint32_t)48U * sizeof (uint8_t));
}
}
}
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_512:
{
KRML_CHECK_SIZE(sizeof (uint8_t),
entropy_input_len + nonce_len + personalization_string_len);
{
uint8_t seed_material[entropy_input_len + nonce_len + personalization_string_len];
memset(seed_material,
0U,
(entropy_input_len + nonce_len + personalization_string_len) * sizeof (uint8_t));
{
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len, nonce, nonce_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len + nonce_len,
personalization_string,
personalization_string_len * sizeof (uint8_t));
k = st.k;
v = st.v;
ctr = st.reseed_counter;
memset(k, 0U, (uint32_t)64U * sizeof (uint8_t));
memset(v, (uint8_t)1U, (uint32_t)64U * sizeof (uint8_t));
ctr[0U] = (uint32_t)1U;
{
uint32_t
input_len = (uint32_t)65U + entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)64U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)65U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input0[64U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_512(k_, k, (uint32_t)64U, input0, input_len);
Hacl_HMAC_compute_sha2_512(v, k_, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_, (uint32_t)64U * sizeof (uint8_t));
if (entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
uint32_t
input_len0 =
(uint32_t)65U
+ entropy_input_len + nonce_len + personalization_string_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)64U * sizeof (uint8_t));
if
(entropy_input_len + nonce_len + personalization_string_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)65U,
seed_material,
(entropy_input_len + nonce_len + personalization_string_len)
* sizeof (uint8_t));
}
input[64U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_512(k_0, k, (uint32_t)64U, input, input_len0);
Hacl_HMAC_compute_sha2_512(v, k_0, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_0, (uint32_t)64U * sizeof (uint8_t));
}
}
}
}
}
}
}
}
break;
}
default:
{
KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
void
Hacl_HMAC_DRBG_reseed(
Spec_Hash_Definitions_hash_alg a,
Hacl_HMAC_DRBG_state st,
uint32_t entropy_input_len,
uint8_t *entropy_input,
uint32_t additional_input_input_len,
uint8_t *additional_input_input
)
{
switch (a)
{
case Spec_Hash_Definitions_SHA1:
{
KRML_CHECK_SIZE(sizeof (uint8_t), entropy_input_len + additional_input_input_len);
{
uint8_t seed_material[entropy_input_len + additional_input_input_len];
memset(seed_material,
0U,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
{
Hacl_HMAC_DRBG_state uu____0;
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len,
additional_input_input,
additional_input_input_len * sizeof (uint8_t));
uu____0 = st;
k = uu____0.k;
v = uu____0.v;
ctr = uu____0.reseed_counter;
{
uint32_t input_len = (uint32_t)21U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)20U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)21U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input0[20U] = (uint8_t)0U;
Hacl_HMAC_legacy_compute_sha1(k_, k, (uint32_t)20U, input0, input_len);
Hacl_HMAC_legacy_compute_sha1(v, k_, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_, (uint32_t)20U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
uint32_t
input_len0 = (uint32_t)21U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)20U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)21U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input[20U] = (uint8_t)1U;
Hacl_HMAC_legacy_compute_sha1(k_0, k, (uint32_t)20U, input, input_len0);
Hacl_HMAC_legacy_compute_sha1(v, k_0, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_0, (uint32_t)20U * sizeof (uint8_t));
}
}
}
ctr[0U] = (uint32_t)1U;
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_256:
{
KRML_CHECK_SIZE(sizeof (uint8_t), entropy_input_len + additional_input_input_len);
{
uint8_t seed_material[entropy_input_len + additional_input_input_len];
memset(seed_material,
0U,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
{
Hacl_HMAC_DRBG_state uu____1;
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len,
additional_input_input,
additional_input_input_len * sizeof (uint8_t));
uu____1 = st;
k = uu____1.k;
v = uu____1.v;
ctr = uu____1.reseed_counter;
{
uint32_t input_len = (uint32_t)33U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)32U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)33U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input0[32U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_256(k_, k, (uint32_t)32U, input0, input_len);
Hacl_HMAC_compute_sha2_256(v, k_, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_, (uint32_t)32U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
uint32_t
input_len0 = (uint32_t)33U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)32U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)33U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input[32U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_256(k_0, k, (uint32_t)32U, input, input_len0);
Hacl_HMAC_compute_sha2_256(v, k_0, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_0, (uint32_t)32U * sizeof (uint8_t));
}
}
}
ctr[0U] = (uint32_t)1U;
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_384:
{
KRML_CHECK_SIZE(sizeof (uint8_t), entropy_input_len + additional_input_input_len);
{
uint8_t seed_material[entropy_input_len + additional_input_input_len];
memset(seed_material,
0U,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
{
Hacl_HMAC_DRBG_state uu____2;
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len,
additional_input_input,
additional_input_input_len * sizeof (uint8_t));
uu____2 = st;
k = uu____2.k;
v = uu____2.v;
ctr = uu____2.reseed_counter;
{
uint32_t input_len = (uint32_t)49U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)48U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)49U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input0[48U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_384(k_, k, (uint32_t)48U, input0, input_len);
Hacl_HMAC_compute_sha2_384(v, k_, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_, (uint32_t)48U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
uint32_t
input_len0 = (uint32_t)49U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)48U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)49U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input[48U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_384(k_0, k, (uint32_t)48U, input, input_len0);
Hacl_HMAC_compute_sha2_384(v, k_0, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_0, (uint32_t)48U * sizeof (uint8_t));
}
}
}
ctr[0U] = (uint32_t)1U;
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_512:
{
KRML_CHECK_SIZE(sizeof (uint8_t), entropy_input_len + additional_input_input_len);
{
uint8_t seed_material[entropy_input_len + additional_input_input_len];
memset(seed_material,
0U,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
{
Hacl_HMAC_DRBG_state uu____3;
uint8_t *k;
uint8_t *v;
uint32_t *ctr;
memcpy(seed_material, entropy_input, entropy_input_len * sizeof (uint8_t));
memcpy(seed_material + entropy_input_len,
additional_input_input,
additional_input_input_len * sizeof (uint8_t));
uu____3 = st;
k = uu____3.k;
v = uu____3.v;
ctr = uu____3.reseed_counter;
{
uint32_t input_len = (uint32_t)65U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)64U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)65U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input0[64U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_512(k_, k, (uint32_t)64U, input0, input_len);
Hacl_HMAC_compute_sha2_512(v, k_, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_, (uint32_t)64U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
uint32_t
input_len0 = (uint32_t)65U + entropy_input_len + additional_input_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)64U * sizeof (uint8_t));
if (entropy_input_len + additional_input_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)65U,
seed_material,
(entropy_input_len + additional_input_input_len) * sizeof (uint8_t));
}
input[64U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_512(k_0, k, (uint32_t)64U, input, input_len0);
Hacl_HMAC_compute_sha2_512(v, k_0, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_0, (uint32_t)64U * sizeof (uint8_t));
}
}
}
ctr[0U] = (uint32_t)1U;
}
}
}
}
}
break;
}
default:
{
KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
bool
Hacl_HMAC_DRBG_generate(
Spec_Hash_Definitions_hash_alg a,
uint8_t *output,
Hacl_HMAC_DRBG_state st,
uint32_t n,
uint32_t additional_input_len,
uint8_t *additional_input
)
{
switch (a)
{
case Spec_Hash_Definitions_SHA1:
{
if (st.reseed_counter[0U] > Hacl_HMAC_DRBG_reseed_interval)
{
return false;
}
{
uint8_t *k = st.k;
uint8_t *v = st.v;
uint32_t *ctr = st.reseed_counter;
if (additional_input_len > (uint32_t)0U)
{
uint32_t input_len = (uint32_t)21U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)20U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)21U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[20U] = (uint8_t)0U;
Hacl_HMAC_legacy_compute_sha1(k_, k, (uint32_t)20U, input0, input_len);
Hacl_HMAC_legacy_compute_sha1(v, k_, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_, (uint32_t)20U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)21U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)20U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)21U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[20U] = (uint8_t)1U;
Hacl_HMAC_legacy_compute_sha1(k_0, k, (uint32_t)20U, input, input_len0);
Hacl_HMAC_legacy_compute_sha1(v, k_0, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_0, (uint32_t)20U * sizeof (uint8_t));
}
}
}
}
}
}
{
uint8_t *output1 = output;
uint32_t max = n / (uint32_t)20U;
uint8_t *out = output1;
{
uint32_t i;
for (i = (uint32_t)0U; i < max; i++)
{
Hacl_HMAC_legacy_compute_sha1(v, k, (uint32_t)20U, v, (uint32_t)20U);
memcpy(out + i * (uint32_t)20U, v, (uint32_t)20U * sizeof (uint8_t));
}
}
if (max * (uint32_t)20U < n)
{
uint8_t *block = output1 + max * (uint32_t)20U;
Hacl_HMAC_legacy_compute_sha1(v, k, (uint32_t)20U, v, (uint32_t)20U);
memcpy(block, v, (n - max * (uint32_t)20U) * sizeof (uint8_t));
}
{
uint32_t input_len = (uint32_t)21U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)20U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)21U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[20U] = (uint8_t)0U;
Hacl_HMAC_legacy_compute_sha1(k_, k, (uint32_t)20U, input0, input_len);
Hacl_HMAC_legacy_compute_sha1(v, k_, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_, (uint32_t)20U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)21U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)20U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)21U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[20U] = (uint8_t)1U;
Hacl_HMAC_legacy_compute_sha1(k_0, k, (uint32_t)20U, input, input_len0);
Hacl_HMAC_legacy_compute_sha1(v, k_0, (uint32_t)20U, v, (uint32_t)20U);
memcpy(k, k_0, (uint32_t)20U * sizeof (uint8_t));
}
}
}
{
uint32_t old_ctr = ctr[0U];
ctr[0U] = old_ctr + (uint32_t)1U;
return true;
}
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_256:
{
if (st.reseed_counter[0U] > Hacl_HMAC_DRBG_reseed_interval)
{
return false;
}
{
uint8_t *k = st.k;
uint8_t *v = st.v;
uint32_t *ctr = st.reseed_counter;
if (additional_input_len > (uint32_t)0U)
{
uint32_t input_len = (uint32_t)33U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)32U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)33U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[32U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_256(k_, k, (uint32_t)32U, input0, input_len);
Hacl_HMAC_compute_sha2_256(v, k_, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_, (uint32_t)32U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)33U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)32U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)33U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[32U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_256(k_0, k, (uint32_t)32U, input, input_len0);
Hacl_HMAC_compute_sha2_256(v, k_0, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_0, (uint32_t)32U * sizeof (uint8_t));
}
}
}
}
}
}
{
uint8_t *output1 = output;
uint32_t max = n / (uint32_t)32U;
uint8_t *out = output1;
{
uint32_t i;
for (i = (uint32_t)0U; i < max; i++)
{
Hacl_HMAC_compute_sha2_256(v, k, (uint32_t)32U, v, (uint32_t)32U);
memcpy(out + i * (uint32_t)32U, v, (uint32_t)32U * sizeof (uint8_t));
}
}
if (max * (uint32_t)32U < n)
{
uint8_t *block = output1 + max * (uint32_t)32U;
Hacl_HMAC_compute_sha2_256(v, k, (uint32_t)32U, v, (uint32_t)32U);
memcpy(block, v, (n - max * (uint32_t)32U) * sizeof (uint8_t));
}
{
uint32_t input_len = (uint32_t)33U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)32U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)33U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[32U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_256(k_, k, (uint32_t)32U, input0, input_len);
Hacl_HMAC_compute_sha2_256(v, k_, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_, (uint32_t)32U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)33U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)32U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)33U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[32U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_256(k_0, k, (uint32_t)32U, input, input_len0);
Hacl_HMAC_compute_sha2_256(v, k_0, (uint32_t)32U, v, (uint32_t)32U);
memcpy(k, k_0, (uint32_t)32U * sizeof (uint8_t));
}
}
}
{
uint32_t old_ctr = ctr[0U];
ctr[0U] = old_ctr + (uint32_t)1U;
return true;
}
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_384:
{
if (st.reseed_counter[0U] > Hacl_HMAC_DRBG_reseed_interval)
{
return false;
}
{
uint8_t *k = st.k;
uint8_t *v = st.v;
uint32_t *ctr = st.reseed_counter;
if (additional_input_len > (uint32_t)0U)
{
uint32_t input_len = (uint32_t)49U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)48U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)49U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[48U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_384(k_, k, (uint32_t)48U, input0, input_len);
Hacl_HMAC_compute_sha2_384(v, k_, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_, (uint32_t)48U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)49U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)48U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)49U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[48U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_384(k_0, k, (uint32_t)48U, input, input_len0);
Hacl_HMAC_compute_sha2_384(v, k_0, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_0, (uint32_t)48U * sizeof (uint8_t));
}
}
}
}
}
}
{
uint8_t *output1 = output;
uint32_t max = n / (uint32_t)48U;
uint8_t *out = output1;
{
uint32_t i;
for (i = (uint32_t)0U; i < max; i++)
{
Hacl_HMAC_compute_sha2_384(v, k, (uint32_t)48U, v, (uint32_t)48U);
memcpy(out + i * (uint32_t)48U, v, (uint32_t)48U * sizeof (uint8_t));
}
}
if (max * (uint32_t)48U < n)
{
uint8_t *block = output1 + max * (uint32_t)48U;
Hacl_HMAC_compute_sha2_384(v, k, (uint32_t)48U, v, (uint32_t)48U);
memcpy(block, v, (n - max * (uint32_t)48U) * sizeof (uint8_t));
}
{
uint32_t input_len = (uint32_t)49U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)48U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)49U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[48U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_384(k_, k, (uint32_t)48U, input0, input_len);
Hacl_HMAC_compute_sha2_384(v, k_, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_, (uint32_t)48U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)49U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)48U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)49U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[48U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_384(k_0, k, (uint32_t)48U, input, input_len0);
Hacl_HMAC_compute_sha2_384(v, k_0, (uint32_t)48U, v, (uint32_t)48U);
memcpy(k, k_0, (uint32_t)48U * sizeof (uint8_t));
}
}
}
{
uint32_t old_ctr = ctr[0U];
ctr[0U] = old_ctr + (uint32_t)1U;
return true;
}
}
}
}
}
}
break;
}
case Spec_Hash_Definitions_SHA2_512:
{
if (st.reseed_counter[0U] > Hacl_HMAC_DRBG_reseed_interval)
{
return false;
}
{
uint8_t *k = st.k;
uint8_t *v = st.v;
uint32_t *ctr = st.reseed_counter;
if (additional_input_len > (uint32_t)0U)
{
uint32_t input_len = (uint32_t)65U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)64U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)65U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[64U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_512(k_, k, (uint32_t)64U, input0, input_len);
Hacl_HMAC_compute_sha2_512(v, k_, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_, (uint32_t)64U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)65U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)64U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)65U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[64U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_512(k_0, k, (uint32_t)64U, input, input_len0);
Hacl_HMAC_compute_sha2_512(v, k_0, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_0, (uint32_t)64U * sizeof (uint8_t));
}
}
}
}
}
}
{
uint8_t *output1 = output;
uint32_t max = n / (uint32_t)64U;
uint8_t *out = output1;
{
uint32_t i;
for (i = (uint32_t)0U; i < max; i++)
{
Hacl_HMAC_compute_sha2_512(v, k, (uint32_t)64U, v, (uint32_t)64U);
memcpy(out + i * (uint32_t)64U, v, (uint32_t)64U * sizeof (uint8_t));
}
}
if (max * (uint32_t)64U < n)
{
uint8_t *block = output1 + max * (uint32_t)64U;
Hacl_HMAC_compute_sha2_512(v, k, (uint32_t)64U, v, (uint32_t)64U);
memcpy(block, v, (n - max * (uint32_t)64U) * sizeof (uint8_t));
}
{
uint32_t input_len = (uint32_t)65U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
{
uint8_t input0[input_len];
memset(input0, 0U, input_len * sizeof (uint8_t));
{
uint8_t *k_ = input0;
memcpy(k_, v, (uint32_t)64U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input0 + (uint32_t)65U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input0[64U] = (uint8_t)0U;
Hacl_HMAC_compute_sha2_512(k_, k, (uint32_t)64U, input0, input_len);
Hacl_HMAC_compute_sha2_512(v, k_, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_, (uint32_t)64U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
uint32_t input_len0 = (uint32_t)65U + additional_input_len;
KRML_CHECK_SIZE(sizeof (uint8_t), input_len0);
{
uint8_t input[input_len0];
memset(input, 0U, input_len0 * sizeof (uint8_t));
{
uint8_t *k_0 = input;
memcpy(k_0, v, (uint32_t)64U * sizeof (uint8_t));
if (additional_input_len != (uint32_t)0U)
{
memcpy(input + (uint32_t)65U,
additional_input,
additional_input_len * sizeof (uint8_t));
}
input[64U] = (uint8_t)1U;
Hacl_HMAC_compute_sha2_512(k_0, k, (uint32_t)64U, input, input_len0);
Hacl_HMAC_compute_sha2_512(v, k_0, (uint32_t)64U, v, (uint32_t)64U);
memcpy(k, k_0, (uint32_t)64U * sizeof (uint8_t));
}
}
}
{
uint32_t old_ctr = ctr[0U];
ctr[0U] = old_ctr + (uint32_t)1U;
return true;
}
}
}
}
}
}
break;
}
default:
{
KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
Computing file changes ...
