diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index deee570d..e5e9776c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -82,6 +82,8 @@ set(PROJECT_SOURCE_FILES ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_Bignum4096.h ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_Bignum4096_32.c ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_Bignum4096_32.h + ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_GenericField32.c + ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_GenericField32.h ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_GenericField64.c ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_GenericField64.h ${PROJECT_SOURCE_DIR}/src/karamel/Hacl_Hash.c diff --git a/src/electionguard/facades/Hacl_Bignum4096.cpp b/src/electionguard/facades/Hacl_Bignum4096.cpp index 96b887d4..4c95782c 100644 --- a/src/electionguard/facades/Hacl_Bignum4096.cpp +++ b/src/electionguard/facades/Hacl_Bignum4096.cpp @@ -1,6 +1,9 @@ #include "Hacl_Bignum4096.hpp" #include "../../karamel/Hacl_Bignum4096.h" +#ifdef _WIN32 +#include "../../karamel/Hacl_GenericField32.h" +#endif // _WIN32 #include "../../karamel/Hacl_GenericField64.h" #include "../log.hpp" @@ -8,44 +11,92 @@ using electionguard::Log; namespace hacl { +#ifdef _WIN32 + Bignum4096::Bignum4096(uint32_t *elem) + { + HaclBignumContext4096 ctx{Hacl_Bignum4096_32_mont_ctx_init(elem)}; + context = std::move(ctx); + } +#else Bignum4096::Bignum4096(uint64_t *elem) { HaclBignumContext4096 ctx{Hacl_Bignum4096_mont_ctx_init(elem)}; context = std::move(ctx); } +#endif // _WIN32 Bignum4096::~Bignum4096() {} uint64_t Bignum4096::add(uint64_t *a, uint64_t *b, uint64_t *res) { +#ifdef _WIN32 + return Hacl_Bignum4096_32_add(reinterpret_cast(a), + reinterpret_cast(b), + reinterpret_cast(res)); +#else return Hacl_Bignum4096_add(a, b, res); +#endif // _WIN32 } uint64_t Bignum4096::sub(uint64_t *a, uint64_t *b, uint64_t *res) { +#ifdef _WIN32 + return Hacl_Bignum4096_32_sub(reinterpret_cast(a), + reinterpret_cast(b), + reinterpret_cast(res)); +#else return Hacl_Bignum4096_sub(a, b, res); +#endif // _WIN32 } void Bignum4096::mul(uint64_t *a, uint64_t *b, uint64_t *res) { +#ifdef _WIN32 + Hacl_Bignum4096_32_mul(reinterpret_cast(a), + reinterpret_cast(b), + reinterpret_cast(res)); +#else Hacl_Bignum4096_mul(a, b, res); +#endif // _WIN32 } bool Bignum4096::mod(uint64_t *n, uint64_t *a, uint64_t *res) { + +#ifdef _WIN32 + return Hacl_Bignum4096_32_mod(reinterpret_cast(n), + reinterpret_cast(a), + reinterpret_cast(res)); +#else return Hacl_Bignum4096_mod(n, a, res); +#endif // _WIN32 } bool Bignum4096::modExp(uint64_t *n, uint64_t *a, uint32_t bBits, uint64_t *b, uint64_t *res, bool useConstTime /* = true */) - { + { if (bBits <= 0) { Log::trace("Bignum4096::modExp:: bbits <= 0"); return false; } if (useConstTime) { +#ifdef _WIN32 + return Hacl_Bignum4096_32_mod_exp_consttime(reinterpret_cast(n), + reinterpret_cast(a), bBits, + reinterpret_cast(b), + reinterpret_cast(res)); +#else return Hacl_Bignum4096_mod_exp_consttime(n, a, bBits, b, res); +#endif // WIN32 } +#ifdef _WIN32 + return Hacl_Bignum4096_32_mod_exp_vartime(reinterpret_cast(n), + reinterpret_cast(a), + bBits, + reinterpret_cast(b), + reinterpret_cast(res)); +#else return Hacl_Bignum4096_mod_exp_vartime(n, a, bBits, b, res); +#endif // _WIN32 } uint64_t *Bignum4096::fromBytes(uint32_t len, uint8_t *bytes) @@ -65,7 +116,12 @@ namespace hacl void Bignum4096::mod(uint64_t *a, uint64_t *res) const { +#ifdef _WIN32 + Hacl_Bignum4096_32_mod_precomp(context.get(), reinterpret_cast(a), + reinterpret_cast(res)); +#else Hacl_Bignum4096_mod_precomp(context.get(), a, res); +#endif // _WIN32 } void Bignum4096::modExp(uint64_t *a, uint32_t bBits, uint64_t *b, uint64_t *res, @@ -76,29 +132,61 @@ namespace hacl return throw; } if (useConstTime) { +#ifdef _WIN32 + return Hacl_Bignum4096_32_mod_exp_consttime_precomp(context.get(), + reinterpret_cast(a), bBits, + reinterpret_cast(b), + reinterpret_cast(res)); +#else return Hacl_Bignum4096_mod_exp_consttime_precomp(context.get(), a, bBits, b, res); +#endif // _WIN32 } +#ifdef _WIN32 + return Hacl_Bignum4096_32_mod_exp_vartime_precomp(context.get(), reinterpret_cast(a), + bBits, reinterpret_cast(b), + reinterpret_cast(res)); +#else return Hacl_Bignum4096_mod_exp_vartime_precomp(context.get(), a, bBits, b, res); +#endif // _WIN32 } void Bignum4096::to_montgomery_form(uint64_t *a, uint64_t *aM) const { +#ifdef _WIN32 + Hacl_GenericField32_to_field(context.get(), reinterpret_cast(a), + reinterpret_cast(aM)); +#else Hacl_GenericField64_to_field(context.get(), a, aM); +#endif // _WIN32 } void Bignum4096::from_montgomery_form(uint64_t *aM, uint64_t *a) const { +#ifdef _WIN32 + Hacl_GenericField32_from_field(context.get(), reinterpret_cast(aM), + reinterpret_cast(a)); +#else Hacl_GenericField64_from_field(context.get(), aM, a); +#endif // _WIN32 } void Bignum4096::montgomery_mod_mul_stay_in_mont_form(uint64_t *aM, uint64_t *bM, uint64_t *cM) const { +#ifdef _WIN32 + Hacl_GenericField32_mul(context.get(), reinterpret_cast(aM), + reinterpret_cast(bM), reinterpret_cast(cM)); +#else Hacl_GenericField64_mul(context.get(), aM, bM, cM); +#endif // _WIN32 } const Bignum4096 &CONTEXT_P() { +#ifdef _WIN32 + static Bignum4096 instance{(uint32_t*)(P_ARRAY_REVERSE)}; +#else static Bignum4096 instance{const_cast(P_ARRAY_REVERSE)}; +#endif // _WIN32 return instance; } } // namespace hacl diff --git a/src/electionguard/facades/Hacl_Bignum4096.hpp b/src/electionguard/facades/Hacl_Bignum4096.hpp index 7fe2d951..99dc23f6 100644 --- a/src/electionguard/facades/Hacl_Bignum4096.hpp +++ b/src/electionguard/facades/Hacl_Bignum4096.hpp @@ -1,6 +1,9 @@ #ifndef __FACADES__Hacl_Bignum4096_H_INCLUDED__ #define __FACADES__Hacl_Bignum4096_H_INCLUDED__ +#ifdef _WIN32 +#include "../../karamel/Hacl_Bignum4096_32.h" +#endif // _WIN32 #include "../../karamel/Hacl_Bignum4096.h" #include "electionguard/export.h" @@ -18,7 +21,11 @@ namespace hacl class EG_INTERNAL_API Bignum4096 { public: +#ifdef _WIN32 + explicit Bignum4096(uint32_t *elem); +#else explicit Bignum4096(uint64_t *elem); +#endif // _WIN32 ~Bignum4096(); static uint64_t add(uint64_t *a, uint64_t *b, uint64_t *res); @@ -63,13 +70,25 @@ namespace hacl private: struct handle_destructor { +#ifdef _WIN32 + void operator()(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *handle) const + { + Hacl_Bignum4096_32_mont_ctx_free(handle); + } +#else void operator()(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *handle) const { Hacl_Bignum4096_mont_ctx_free(handle); } +#endif // _WIN32 }; +#ifdef _WIN32 + typedef std::unique_ptr + HaclBignumContext4096; +#else typedef std::unique_ptr HaclBignumContext4096; +#endif // _WIN32 HaclBignumContext4096 context; }; diff --git a/src/karamel/Hacl_GenericField32.c b/src/karamel/Hacl_GenericField32.c index c2a0233a..3ada97f4 100644 --- a/src/karamel/Hacl_GenericField32.c +++ b/src/karamel/Hacl_GenericField32.c @@ -21,7 +21,6 @@ * SOFTWARE. */ - #include "Hacl_GenericField32.h" #include "internal/Hacl_Bignum.h" @@ -41,7 +40,6 @@ Montgomery form. *******************************************************************************/ - /* Check whether this library will work for a modulus `n`. @@ -52,8 +50,8 @@ Check whether this library will work for a modulus `n`. */ bool Hacl_GenericField32_field_modulus_check(uint32_t len, uint32_t *n) { - uint32_t m = Hacl_Bignum_Montgomery_bn_check_modulus_u32(len, n); - return m == (uint32_t)0xFFFFFFFFU; + uint32_t m = Hacl_Bignum_Montgomery_bn_check_modulus_u32(len, n); + return m == (uint32_t)0xFFFFFFFFU; } /* @@ -69,42 +67,40 @@ Heap-allocate and initialize a montgomery context. The caller will need to call Hacl_GenericField32_field_free on the return value to avoid memory leaks. */ -Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 -*Hacl_GenericField32_field_init(uint32_t len, uint32_t *n) +Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *Hacl_GenericField32_field_init(uint32_t len, + uint32_t *n) { - KRML_CHECK_SIZE(sizeof (uint32_t), len); - { - uint32_t *r2 = (uint32_t *)KRML_HOST_CALLOC(len, sizeof (uint32_t)); - KRML_CHECK_SIZE(sizeof (uint32_t), len); + KRML_CHECK_SIZE(sizeof(uint32_t), len); { - uint32_t *n1 = (uint32_t *)KRML_HOST_CALLOC(len, sizeof (uint32_t)); - uint32_t *r21 = r2; - uint32_t *n11 = n1; - uint32_t nBits; - uint32_t mu; - memcpy(n11, n, len * sizeof (uint32_t)); - nBits = (uint32_t)32U * Hacl_Bignum_Lib_bn_get_top_index_u32(len, n); - Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u32(len, nBits, n, r21); - mu = Hacl_Bignum_ModInvLimb_mod_inv_uint32(n[0U]); - { - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 res; - res.len = len; - res.n = n11; - res.mu = mu; - res.r2 = r21; - KRML_CHECK_SIZE(sizeof (Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32), (uint32_t)1U); + uint32_t *r2 = (uint32_t *)KRML_HOST_CALLOC(len, sizeof(uint32_t)); + KRML_CHECK_SIZE(sizeof(uint32_t), len); { - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 - *buf = - (Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *)KRML_HOST_MALLOC(sizeof ( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 - )); - buf[0U] = res; - return buf; + uint32_t *n1 = (uint32_t *)KRML_HOST_CALLOC(len, sizeof(uint32_t)); + uint32_t *r21 = r2; + uint32_t *n11 = n1; + uint32_t nBits; + uint32_t mu; + memcpy(n11, n, len * sizeof(uint32_t)); + nBits = (uint32_t)32U * Hacl_Bignum_Lib_bn_get_top_index_u32(len, n); + Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u32(len, nBits, n, r21); + mu = Hacl_Bignum_ModInvLimb_mod_inv_uint32(n[0U]); + { + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 res; + res.len = len; + res.n = n11; + res.mu = mu; + res.r2 = r21; + KRML_CHECK_SIZE(sizeof(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32), (uint32_t)1U); + { + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *buf = + (Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *)KRML_HOST_MALLOC( + sizeof(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32)); + buf[0U] = res; + return buf; + } + } } - } } - } } /* @@ -114,12 +110,12 @@ Deallocate the memory previously allocated by Hacl_GenericField32_field_init. */ void Hacl_GenericField32_field_free(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k) { - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - uint32_t *n = k1.n; - uint32_t *r2 = k1.r2; - KRML_HOST_FREE(n); - KRML_HOST_FREE(r2); - KRML_HOST_FREE(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + uint32_t *n = k1.n; + uint32_t *r2 = k1.r2; + KRML_HOST_FREE(n); + KRML_HOST_FREE(r2); + KRML_HOST_FREE(k); } /* @@ -129,8 +125,8 @@ Return the size of a modulus `n` in limbs. */ uint32_t Hacl_GenericField32_field_get_len(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k) { - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - return k1.len; + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + return k1.len; } /* @@ -141,16 +137,12 @@ Convert a bignum from the regular representation to the Montgomery representatio The argument a and the outparam aM are meant to be `len` limbs in size, i.e. uint32_t[len]. The argument k is a montgomery context obtained through Hacl_GenericField32_field_init. */ -void -Hacl_GenericField32_to_field( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *a, - uint32_t *aM -) +void Hacl_GenericField32_to_field(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *a, + uint32_t *aM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - Hacl_Bignum_Montgomery_bn_to_mont_u32(len1, k1.n, k1.mu, k1.r2, a, aM); + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + Hacl_Bignum_Montgomery_bn_to_mont_u32(len1, k1.n, k1.mu, k1.r2, a, aM); } /* @@ -162,16 +154,12 @@ Convert a result back from the Montgomery representation to the regular represen The argument aM and the outparam a are meant to be `len` limbs in size, i.e. uint32_t[len]. The argument k is a montgomery context obtained through Hacl_GenericField32_field_init. */ -void -Hacl_GenericField32_from_field( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t *a -) +void Hacl_GenericField32_from_field(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t *a) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, aM, a); + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, aM, a); } /* @@ -180,17 +168,12 @@ Write `aM + bM mod n` in `cM`. The arguments aM, bM, and the outparam cM are meant to be `len` limbs in size, i.e. uint32_t[len]. The argument k is a montgomery context obtained through Hacl_GenericField32_field_init. */ -void -Hacl_GenericField32_add( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t *bM, - uint32_t *cM -) +void Hacl_GenericField32_add(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t *bM, uint32_t *cM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - Hacl_Bignum_bn_add_mod_n_u32(len1, k1.n, aM, bM, cM); + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + Hacl_Bignum_bn_add_mod_n_u32(len1, k1.n, aM, bM, cM); } /* @@ -199,17 +182,12 @@ Write `aM - bM mod n` to `cM`. The arguments aM, bM, and the outparam cM are meant to be `len` limbs in size, i.e. uint32_t[len]. The argument k is a montgomery context obtained through Hacl_GenericField32_field_init. */ -void -Hacl_GenericField32_sub( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t *bM, - uint32_t *cM -) +void Hacl_GenericField32_sub(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t *bM, uint32_t *cM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - Hacl_Bignum_bn_sub_mod_n_u32(len1, k1.n, aM, bM, cM); + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + Hacl_Bignum_bn_sub_mod_n_u32(len1, k1.n, aM, bM, cM); } /* @@ -218,17 +196,12 @@ Write `aM * bM mod n` in `cM`. The arguments aM, bM, and the outparam cM are meant to be `len` limbs in size, i.e. uint32_t[len]. The argument k is a montgomery context obtained through Hacl_GenericField32_field_init. */ -void -Hacl_GenericField32_mul( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t *bM, - uint32_t *cM -) +void Hacl_GenericField32_mul(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t *bM, uint32_t *cM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aM, bM, cM); + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aM, bM, cM); } /* @@ -237,16 +210,12 @@ Write `aM * aM mod n` in `cM`. The argument aM and the outparam cM are meant to be `len` limbs in size, i.e. uint32_t[len]. The argument k is a montgomery context obtained through Hacl_GenericField32_field_init. */ -void -Hacl_GenericField32_sqr( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t *cM -) +void Hacl_GenericField32_sqr(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t *cM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, aM, cM); + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, aM, cM); } /* @@ -257,9 +226,9 @@ Convert a bignum `one` to its Montgomery representation. */ void Hacl_GenericField32_one(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *oneM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, oneM); + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, oneM); } /* @@ -280,190 +249,168 @@ Write `aM ^ b mod n` in `resM`. precondition is observed. • b < pow2 bBits */ -void -Hacl_GenericField32_exp_consttime( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t bBits, - uint32_t *b, - uint32_t *resM -) +void Hacl_GenericField32_exp_consttime(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t bBits, uint32_t *b, uint32_t *resM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - KRML_CHECK_SIZE(sizeof (uint32_t), k1.len); - { - uint32_t *aMc = (uint32_t *)alloca(k1.len * sizeof (uint32_t)); - memset(aMc, 0U, k1.len * sizeof (uint32_t)); - memcpy(aMc, aM, k1.len * sizeof (uint32_t)); - if (bBits < (uint32_t)200U) - { - Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); - { - uint32_t sw = (uint32_t)0U; - { - uint32_t i0; - for (i0 = (uint32_t)0U; i0 < bBits; i0++) - { - uint32_t i1 = (bBits - i0 - (uint32_t)1U) / (uint32_t)32U; - uint32_t j = (bBits - i0 - (uint32_t)1U) % (uint32_t)32U; - uint32_t tmp = b[i1]; - uint32_t bit = tmp >> j & (uint32_t)1U; - uint32_t sw1 = bit ^ sw; - { - uint32_t i; - for (i = (uint32_t)0U; i < len1; i++) - { - uint32_t dummy = ((uint32_t)0U - sw1) & (resM[i] ^ aMc[i]); - resM[i] = resM[i] ^ dummy; - aMc[i] = aMc[i] ^ dummy; - } - } - Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aMc, resM, aMc); - Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, resM, resM); - sw = bit; - } - } - { - uint32_t sw0 = sw; - { - uint32_t i; - for (i = (uint32_t)0U; i < len1; i++) - { - uint32_t dummy = ((uint32_t)0U - sw0) & (resM[i] ^ aMc[i]); - resM[i] = resM[i] ^ dummy; - aMc[i] = aMc[i] ^ dummy; - } - } - } - } - } - else + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + KRML_CHECK_SIZE(sizeof(uint32_t), k1.len); { - uint32_t bLen; - if (bBits == (uint32_t)0U) - { - bLen = (uint32_t)1U; - } - else - { - bLen = (bBits - (uint32_t)1U) / (uint32_t)32U + (uint32_t)1U; - } - Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); - KRML_CHECK_SIZE(sizeof (uint32_t), (uint32_t)16U * len1); - { - uint32_t *table = (uint32_t *)alloca((uint32_t)16U * len1 * sizeof (uint32_t)); - memset(table, 0U, (uint32_t)16U * len1 * sizeof (uint32_t)); - memcpy(table, resM, len1 * sizeof (uint32_t)); - { - uint32_t *t1 = table + len1; - memcpy(t1, aMc, len1 * sizeof (uint32_t)); - { - uint32_t i; - for (i = (uint32_t)0U; i < (uint32_t)15U; i++) - { - uint32_t *t11 = table + i * len1; - uint32_t *t2 = table + i * len1 + len1; - Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aMc, t11, t2); - } - } - if (bBits % (uint32_t)4U != (uint32_t)0U) - { - uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; - uint32_t i0 = bBits / (uint32_t)4U * (uint32_t)4U / (uint32_t)32U; - uint32_t j = bBits / (uint32_t)4U * (uint32_t)4U % (uint32_t)32U; - uint32_t p1 = b[i0] >> j; - uint32_t ite; - if (i0 + (uint32_t)1U < bLen && (uint32_t)0U < j) - { - ite = p1 | b[i0 + (uint32_t)1U] << ((uint32_t)32U - j); - } - else - { - ite = p1; - } + uint32_t *aMc = (uint32_t *)alloca(k1.len * sizeof(uint32_t)); + memset(aMc, 0U, k1.len * sizeof(uint32_t)); + memcpy(aMc, aM, k1.len * sizeof(uint32_t)); + if (bBits < (uint32_t)200U) { + Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); { - uint32_t bits_c = ite & mask_l; - memcpy(resM, table, len1 * sizeof (uint32_t)); - { - uint32_t i1; - for (i1 = (uint32_t)0U; i1 < (uint32_t)15U; i1++) + uint32_t sw = (uint32_t)0U; { - uint32_t c = FStar_UInt32_eq_mask(bits_c, i1 + (uint32_t)1U); - uint32_t *res_j = table + (i1 + (uint32_t)1U) * len1; - { - uint32_t i; - for (i = (uint32_t)0U; i < len1; i++) + uint32_t i0; + for (i0 = (uint32_t)0U; i0 < bBits; i0++) { + uint32_t i1 = (bBits - i0 - (uint32_t)1U) / (uint32_t)32U; + uint32_t j = (bBits - i0 - (uint32_t)1U) % (uint32_t)32U; + uint32_t tmp = b[i1]; + uint32_t bit = tmp >> j & (uint32_t)1U; + uint32_t sw1 = bit ^ sw; + { + uint32_t i; + for (i = (uint32_t)0U; i < len1; i++) { + uint32_t dummy = ((uint32_t)0U - sw1) & (resM[i] ^ aMc[i]); + resM[i] = resM[i] ^ dummy; + aMc[i] = aMc[i] ^ dummy; + } + } + Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aMc, resM, aMc); + Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, resM, resM); + sw = bit; + } + } + { + uint32_t sw0 = sw; { - uint32_t *os = resM; - uint32_t x = (c & res_j[i]) | (~c & resM[i]); - os[i] = x; + uint32_t i; + for (i = (uint32_t)0U; i < len1; i++) { + uint32_t dummy = ((uint32_t)0U - sw0) & (resM[i] ^ aMc[i]); + resM[i] = resM[i] ^ dummy; + aMc[i] = aMc[i] ^ dummy; + } } - } } - } } - } - { - uint32_t i0; - for (i0 = (uint32_t)0U; i0 < bBits / (uint32_t)4U; i0++) + } else { + uint32_t bLen; + if (bBits == (uint32_t)0U) { + bLen = (uint32_t)1U; + } else { + bLen = (bBits - (uint32_t)1U) / (uint32_t)32U + (uint32_t)1U; + } + Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); + KRML_CHECK_SIZE(sizeof(uint32_t), (uint32_t)16U * len1); { - { - uint32_t i; - for (i = (uint32_t)0U; i < (uint32_t)4U; i++) - { - Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, resM, resM); - } - } - { - uint32_t bk = bBits - bBits % (uint32_t)4U; - uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; - uint32_t i1 = (bk - (uint32_t)4U * i0 - (uint32_t)4U) / (uint32_t)32U; - uint32_t j = (bk - (uint32_t)4U * i0 - (uint32_t)4U) % (uint32_t)32U; - uint32_t p1 = b[i1] >> j; - uint32_t ite; - if (i1 + (uint32_t)1U < bLen && (uint32_t)0U < j) - { - ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)32U - j); - } - else + uint32_t *table = (uint32_t *)alloca((uint32_t)16U * len1 * sizeof(uint32_t)); + memset(table, 0U, (uint32_t)16U * len1 * sizeof(uint32_t)); + memcpy(table, resM, len1 * sizeof(uint32_t)); { - ite = p1; - } - { - uint32_t bits_l = ite & mask_l; - KRML_CHECK_SIZE(sizeof (uint32_t), len1); - { - uint32_t *a_bits_l = (uint32_t *)alloca(len1 * sizeof (uint32_t)); - memset(a_bits_l, 0U, len1 * sizeof (uint32_t)); - memcpy(a_bits_l, table, len1 * sizeof (uint32_t)); + uint32_t *t1 = table + len1; + memcpy(t1, aMc, len1 * sizeof(uint32_t)); { - uint32_t i2; - for (i2 = (uint32_t)0U; i2 < (uint32_t)15U; i2++) - { - uint32_t c = FStar_UInt32_eq_mask(bits_l, i2 + (uint32_t)1U); - uint32_t *res_j = table + (i2 + (uint32_t)1U) * len1; + uint32_t i; + for (i = (uint32_t)0U; i < (uint32_t)15U; i++) { + uint32_t *t11 = table + i * len1; + uint32_t *t2 = table + i * len1 + len1; + Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aMc, t11, t2); + } + } + if (bBits % (uint32_t)4U != (uint32_t)0U) { + uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; + uint32_t i0 = bBits / (uint32_t)4U * (uint32_t)4U / (uint32_t)32U; + uint32_t j = bBits / (uint32_t)4U * (uint32_t)4U % (uint32_t)32U; + uint32_t p1 = b[i0] >> j; + uint32_t ite; + if (i0 + (uint32_t)1U < bLen && (uint32_t)0U < j) { + ite = p1 | b[i0 + (uint32_t)1U] << ((uint32_t)32U - j); + } else { + ite = p1; + } { - uint32_t i; - for (i = (uint32_t)0U; i < len1; i++) - { - uint32_t *os = a_bits_l; - uint32_t x = (c & res_j[i]) | (~c & a_bits_l[i]); - os[i] = x; - } + uint32_t bits_c = ite & mask_l; + memcpy(resM, table, len1 * sizeof(uint32_t)); + { + uint32_t i1; + for (i1 = (uint32_t)0U; i1 < (uint32_t)15U; i1++) { + uint32_t c = FStar_UInt32_eq_mask(bits_c, i1 + (uint32_t)1U); + uint32_t *res_j = table + (i1 + (uint32_t)1U) * len1; + { + uint32_t i; + for (i = (uint32_t)0U; i < len1; i++) { + uint32_t *os = resM; + uint32_t x = (c & res_j[i]) | (~c & resM[i]); + os[i] = x; + } + } + } + } + } + } + { + uint32_t i0; + uint32_t *a_bits_l = (uint32_t *)alloca(len1 * sizeof(uint32_t)); + for (i0 = (uint32_t)0U; i0 < bBits / (uint32_t)4U; i0++) { + { + uint32_t i; + for (i = (uint32_t)0U; i < (uint32_t)4U; i++) { + Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, resM, + resM); + } + } + { + uint32_t bk = bBits - bBits % (uint32_t)4U; + uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; + uint32_t i1 = + (bk - (uint32_t)4U * i0 - (uint32_t)4U) / (uint32_t)32U; + uint32_t j = + (bk - (uint32_t)4U * i0 - (uint32_t)4U) % (uint32_t)32U; + uint32_t p1 = b[i1] >> j; + uint32_t ite; + if (i1 + (uint32_t)1U < bLen && (uint32_t)0U < j) { + ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)32U - j); + } else { + ite = p1; + } + { + uint32_t bits_l = ite & mask_l; + KRML_CHECK_SIZE(sizeof(uint32_t), len1); + { + memset(a_bits_l, 0U, len1 * sizeof(uint32_t)); + memcpy(a_bits_l, table, len1 * sizeof(uint32_t)); + { + uint32_t i2; + for (i2 = (uint32_t)0U; i2 < (uint32_t)15U; i2++) { + uint32_t c = + FStar_UInt32_eq_mask(bits_l, i2 + (uint32_t)1U); + uint32_t *res_j = + table + (i2 + (uint32_t)1U) * len1; + { + uint32_t i; + for (i = (uint32_t)0U; i < len1; i++) { + uint32_t *os = a_bits_l; + uint32_t x = + (c & res_j[i]) | (~c & a_bits_l[i]); + os[i] = x; + } + } + } + } + Hacl_Bignum_Montgomery_bn_mont_mul_u32( + len1, k1.n, k1.mu, resM, a_bits_l, resM); + } + } + } } - } } - Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, resM, a_bits_l, resM); - } } - } } - } } - } } - } } /* @@ -484,144 +431,118 @@ Write `aM ^ b mod n` in `resM`. precondition is observed. • b < pow2 bBits */ -void -Hacl_GenericField32_exp_vartime( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t bBits, - uint32_t *b, - uint32_t *resM -) +void Hacl_GenericField32_exp_vartime(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t bBits, uint32_t *b, uint32_t *resM) { - uint32_t len1 = Hacl_GenericField32_field_get_len(k); - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - KRML_CHECK_SIZE(sizeof (uint32_t), k1.len); - { - uint32_t *aMc = (uint32_t *)alloca(k1.len * sizeof (uint32_t)); - memset(aMc, 0U, k1.len * sizeof (uint32_t)); - memcpy(aMc, aM, k1.len * sizeof (uint32_t)); - if (bBits < (uint32_t)200U) + uint32_t len1 = Hacl_GenericField32_field_get_len(k); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + KRML_CHECK_SIZE(sizeof(uint32_t), k1.len); { - Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); - { - uint32_t i; - for (i = (uint32_t)0U; i < bBits; i++) - { - uint32_t i1 = i / (uint32_t)32U; - uint32_t j = i % (uint32_t)32U; - uint32_t tmp = b[i1]; - uint32_t bit = tmp >> j & (uint32_t)1U; - if (!(bit == (uint32_t)0U)) - { - Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, resM, aMc, resM); - } - Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, aMc, aMc); - } - } - } - else - { - uint32_t bLen; - if (bBits == (uint32_t)0U) - { - bLen = (uint32_t)1U; - } - else - { - bLen = (bBits - (uint32_t)1U) / (uint32_t)32U + (uint32_t)1U; - } - Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); - KRML_CHECK_SIZE(sizeof (uint32_t), (uint32_t)16U * len1); - { - uint32_t *table = (uint32_t *)alloca((uint32_t)16U * len1 * sizeof (uint32_t)); - memset(table, 0U, (uint32_t)16U * len1 * sizeof (uint32_t)); - memcpy(table, resM, len1 * sizeof (uint32_t)); - { - uint32_t *t1 = table + len1; - memcpy(t1, aMc, len1 * sizeof (uint32_t)); - { - uint32_t i; - for (i = (uint32_t)0U; i < (uint32_t)15U; i++) + uint32_t *aMc = (uint32_t *)alloca(k1.len * sizeof(uint32_t)); + memset(aMc, 0U, k1.len * sizeof(uint32_t)); + memcpy(aMc, aM, k1.len * sizeof(uint32_t)); + if (bBits < (uint32_t)200U) { + Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); { - uint32_t *t11 = table + i * len1; - uint32_t *t2 = table + i * len1 + len1; - Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aMc, t11, t2); - } - } - if (bBits % (uint32_t)4U != (uint32_t)0U) - { - uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; - uint32_t i = bBits / (uint32_t)4U * (uint32_t)4U / (uint32_t)32U; - uint32_t j = bBits / (uint32_t)4U * (uint32_t)4U % (uint32_t)32U; - uint32_t p1 = b[i] >> j; - uint32_t ite; - if (i + (uint32_t)1U < bLen && (uint32_t)0U < j) - { - ite = p1 | b[i + (uint32_t)1U] << ((uint32_t)32U - j); - } - else - { - ite = p1; + uint32_t i; + for (i = (uint32_t)0U; i < bBits; i++) { + uint32_t i1 = i / (uint32_t)32U; + uint32_t j = i % (uint32_t)32U; + uint32_t tmp = b[i1]; + uint32_t bit = tmp >> j & (uint32_t)1U; + if (!(bit == (uint32_t)0U)) { + Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, resM, aMc, resM); + } + Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, aMc, aMc); + } } - { - uint32_t bits_c = ite & mask_l; - uint32_t bits_l32 = bits_c; - uint32_t *a_bits_l = table + bits_l32 * len1; - memcpy(resM, a_bits_l, len1 * sizeof (uint32_t)); + } else { + uint32_t bLen; + if (bBits == (uint32_t)0U) { + bLen = (uint32_t)1U; + } else { + bLen = (bBits - (uint32_t)1U) / (uint32_t)32U + (uint32_t)1U; } - } - { - uint32_t i; - for (i = (uint32_t)0U; i < bBits / (uint32_t)4U; i++) + Hacl_Bignum_Montgomery_bn_from_mont_u32(len1, k1.n, k1.mu, k1.r2, resM); + KRML_CHECK_SIZE(sizeof(uint32_t), (uint32_t)16U * len1); { - { - uint32_t i0; - for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++) - { - Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, resM, resM); - } - } - { - uint32_t bk = bBits - bBits % (uint32_t)4U; - uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; - uint32_t i1 = (bk - (uint32_t)4U * i - (uint32_t)4U) / (uint32_t)32U; - uint32_t j = (bk - (uint32_t)4U * i - (uint32_t)4U) % (uint32_t)32U; - uint32_t p1 = b[i1] >> j; - uint32_t ite; - if (i1 + (uint32_t)1U < bLen && (uint32_t)0U < j) - { - ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)32U - j); - } - else + uint32_t *table = (uint32_t *)alloca((uint32_t)16U * len1 * sizeof(uint32_t)); + memset(table, 0U, (uint32_t)16U * len1 * sizeof(uint32_t)); + memcpy(table, resM, len1 * sizeof(uint32_t)); { - ite = p1; - } - { - uint32_t bits_l = ite & mask_l; - KRML_CHECK_SIZE(sizeof (uint32_t), len1); - { - uint32_t *a_bits_l = (uint32_t *)alloca(len1 * sizeof (uint32_t)); - memset(a_bits_l, 0U, len1 * sizeof (uint32_t)); + uint32_t *t1 = table + len1; + memcpy(t1, aMc, len1 * sizeof(uint32_t)); { - uint32_t bits_l32 = bits_l; - uint32_t *a_bits_l1 = table + bits_l32 * len1; - memcpy(a_bits_l, a_bits_l1, len1 * sizeof (uint32_t)); - Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, - k1.n, - k1.mu, - resM, - a_bits_l, - resM); + uint32_t i; + for (i = (uint32_t)0U; i < (uint32_t)15U; i++) { + uint32_t *t11 = table + i * len1; + uint32_t *t2 = table + i * len1 + len1; + Hacl_Bignum_Montgomery_bn_mont_mul_u32(len1, k1.n, k1.mu, aMc, t11, t2); + } + } + if (bBits % (uint32_t)4U != (uint32_t)0U) { + uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; + uint32_t i = bBits / (uint32_t)4U * (uint32_t)4U / (uint32_t)32U; + uint32_t j = bBits / (uint32_t)4U * (uint32_t)4U % (uint32_t)32U; + uint32_t p1 = b[i] >> j; + uint32_t ite; + if (i + (uint32_t)1U < bLen && (uint32_t)0U < j) { + ite = p1 | b[i + (uint32_t)1U] << ((uint32_t)32U - j); + } else { + ite = p1; + } + { + uint32_t bits_c = ite & mask_l; + uint32_t bits_l32 = bits_c; + uint32_t *a_bits_l = table + bits_l32 * len1; + memcpy(resM, a_bits_l, len1 * sizeof(uint32_t)); + } + } + { + uint32_t i; + uint32_t *a_bits_l = (uint32_t *)alloca(len1 * sizeof(uint32_t)); + for (i = (uint32_t)0U; i < bBits / (uint32_t)4U; i++) { + { + uint32_t i0; + for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++) { + Hacl_Bignum_Montgomery_bn_mont_sqr_u32(len1, k1.n, k1.mu, resM, + resM); + } + } + { + uint32_t bk = bBits - bBits % (uint32_t)4U; + uint32_t mask_l = (uint32_t)16U - (uint32_t)1U; + uint32_t i1 = + (bk - (uint32_t)4U * i - (uint32_t)4U) / (uint32_t)32U; + uint32_t j = (bk - (uint32_t)4U * i - (uint32_t)4U) % (uint32_t)32U; + uint32_t p1 = b[i1] >> j; + uint32_t ite; + if (i1 + (uint32_t)1U < bLen && (uint32_t)0U < j) { + ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)32U - j); + } else { + ite = p1; + } + { + uint32_t bits_l = ite & mask_l; + KRML_CHECK_SIZE(sizeof(uint32_t), len1); + { + memset(a_bits_l, 0U, len1 * sizeof(uint32_t)); + { + uint32_t bits_l32 = bits_l; + uint32_t *a_bits_l1 = table + bits_l32 * len1; + memcpy(a_bits_l, a_bits_l1, len1 * sizeof(uint32_t)); + Hacl_Bignum_Montgomery_bn_mont_mul_u32( + len1, k1.n, k1.mu, resM, a_bits_l, resM); + } + } + } + } + } } - } } - } } - } } - } } - } } /* @@ -635,73 +556,66 @@ Write `aM ^ (-1) mod n` in `aInvM`. • n is a prime • 0 < aM */ -void -Hacl_GenericField32_inverse( - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, - uint32_t *aM, - uint32_t *aInvM -) +void Hacl_GenericField32_inverse(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, + uint32_t *aInvM) { - Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; - uint32_t len1 = k1.len; - KRML_CHECK_SIZE(sizeof (uint32_t), len1); - { - uint32_t *n2 = (uint32_t *)alloca(len1 * sizeof (uint32_t)); - memset(n2, 0U, len1 * sizeof (uint32_t)); + Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 k1 = *k; + uint32_t len1 = k1.len; + KRML_CHECK_SIZE(sizeof(uint32_t), len1); { - uint32_t - c0 = Lib_IntTypes_Intrinsics_sub_borrow_u32((uint32_t)0U, k1.n[0U], (uint32_t)2U, n2); - uint32_t c1; - if ((uint32_t)1U < len1) - { - uint32_t rLen = len1 - (uint32_t)1U; - uint32_t *a1 = k1.n + (uint32_t)1U; - uint32_t *res1 = n2 + (uint32_t)1U; - uint32_t c = c0; + uint32_t *n2 = (uint32_t *)alloca(len1 * sizeof(uint32_t)); + memset(n2, 0U, len1 * sizeof(uint32_t)); { - uint32_t i; - for (i = (uint32_t)0U; i < rLen / (uint32_t)4U; i++) - { - uint32_t t1 = a1[(uint32_t)4U * i]; - uint32_t *res_i0 = res1 + (uint32_t)4U * i; - c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t1, (uint32_t)0U, res_i0); - { - uint32_t t10 = a1[(uint32_t)4U * i + (uint32_t)1U]; - uint32_t *res_i1 = res1 + (uint32_t)4U * i + (uint32_t)1U; - c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t10, (uint32_t)0U, res_i1); - { - uint32_t t11 = a1[(uint32_t)4U * i + (uint32_t)2U]; - uint32_t *res_i2 = res1 + (uint32_t)4U * i + (uint32_t)2U; - c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t11, (uint32_t)0U, res_i2); + uint32_t c0 = + Lib_IntTypes_Intrinsics_sub_borrow_u32((uint32_t)0U, k1.n[0U], (uint32_t)2U, n2); + uint32_t c1; + if ((uint32_t)1U < len1) { + uint32_t rLen = len1 - (uint32_t)1U; + uint32_t *a1 = k1.n + (uint32_t)1U; + uint32_t *res1 = n2 + (uint32_t)1U; + uint32_t c = c0; { - uint32_t t12 = a1[(uint32_t)4U * i + (uint32_t)3U]; - uint32_t *res_i = res1 + (uint32_t)4U * i + (uint32_t)3U; - c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t12, (uint32_t)0U, res_i); + uint32_t i; + for (i = (uint32_t)0U; i < rLen / (uint32_t)4U; i++) { + uint32_t t1 = a1[(uint32_t)4U * i]; + uint32_t *res_i0 = res1 + (uint32_t)4U * i; + c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t1, (uint32_t)0U, res_i0); + { + uint32_t t10 = a1[(uint32_t)4U * i + (uint32_t)1U]; + uint32_t *res_i1 = res1 + (uint32_t)4U * i + (uint32_t)1U; + c = + Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t10, (uint32_t)0U, res_i1); + { + uint32_t t11 = a1[(uint32_t)4U * i + (uint32_t)2U]; + uint32_t *res_i2 = res1 + (uint32_t)4U * i + (uint32_t)2U; + c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t11, (uint32_t)0U, + res_i2); + { + uint32_t t12 = a1[(uint32_t)4U * i + (uint32_t)3U]; + uint32_t *res_i = res1 + (uint32_t)4U * i + (uint32_t)3U; + c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t12, (uint32_t)0U, + res_i); + } + } + } + } } - } + { + uint32_t i; + for (i = rLen / (uint32_t)4U * (uint32_t)4U; i < rLen; i++) { + uint32_t t1 = a1[i]; + uint32_t *res_i = res1 + i; + c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t1, (uint32_t)0U, res_i); + } + } + { + uint32_t c10 = c; + c1 = c10; + } + } else { + c1 = c0; } - } + Hacl_GenericField32_exp_vartime(k, aM, k1.len * (uint32_t)32U, n2, aInvM); } - { - uint32_t i; - for (i = rLen / (uint32_t)4U * (uint32_t)4U; i < rLen; i++) - { - uint32_t t1 = a1[i]; - uint32_t *res_i = res1 + i; - c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t1, (uint32_t)0U, res_i); - } - } - { - uint32_t c10 = c; - c1 = c10; - } - } - else - { - c1 = c0; - } - Hacl_GenericField32_exp_vartime(k, aM, k1.len * (uint32_t)32U, n2, aInvM); } - } } - diff --git a/src/karamel/Hacl_GenericField32.h b/src/karamel/Hacl_GenericField32.h index 31541804..5f6ad46a 100644 --- a/src/karamel/Hacl_GenericField32.h +++ b/src/karamel/Hacl_GenericField32.h @@ -30,11 +30,10 @@ extern "C" { #endif #include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" -#include "krml/internal/builtin.h" - +#include "karamel/krml/internal/types.h" +#include "karamel/krml/lowstar_endianness.h" +#include "karamel/krml/internal/target.h" +#include "karamel/krml/internal/builtin.h" #include "Hacl_Bignum256_32.h" #include "evercrypt_targetconfig.h"