microsoft
/
electionguard-cpp
зеркало из https://github.com/microsoft/electionguard-cpp.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

Add support for using the 32 bit optimized HACL code. (#279) 

* Add support for using the 32 bit optimized HACL code.

* Remove comment.

* fixed allocation for alloca inside of loops

* A bit of cleanup.

Co-authored-by: Steve Maier <ysfred4@hotmail.com>
This commit is contained in:
jeffspel-crypto 2022-05-16 11:23:58 -07:00 коммит произвёл GitHub
Родитель 32b55893c3
Коммит 0ea2ffdf63
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: 4AEE18F83AFDEB23
5 изменённых файлов: 495 добавлений и 473 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

2
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

90
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<uint32_t *>(a),
reinterpret_cast<uint32_t *>(b),
reinterpret_cast<uint32_t *>(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<uint32_t *>(a),
reinterpret_cast<uint32_t *>(b),
reinterpret_cast<uint32_t *>(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<uint32_t *>(a),
reinterpret_cast<uint32_t *>(b),
reinterpret_cast<uint32_t *>(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<uint32_t *>(n),
reinterpret_cast<uint32_t *>(a),
reinterpret_cast<uint32_t *>(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<uint32_t *>(n),
reinterpret_cast<uint32_t *>(a), bBits,
reinterpret_cast<uint32_t *>(b),
reinterpret_cast<uint32_t *>(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<uint32_t *>(n),
reinterpret_cast<uint32_t *>(a),
bBits,
reinterpret_cast<uint32_t *>(b),
reinterpret_cast<uint32_t *>(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<uint32_t *>(a),
reinterpret_cast<uint32_t *>(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<uint32_t *>(a), bBits,
reinterpret_cast<uint32_t *>(b),
reinterpret_cast<uint32_t *>(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<uint32_t *>(a),
bBits, reinterpret_cast<uint32_t *>(b),
reinterpret_cast<uint32_t *>(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<uint32_t *>(a),
reinterpret_cast<uint32_t *>(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<uint32_t *>(aM),
reinterpret_cast<uint32_t *>(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<uint32_t *>(aM),
reinterpret_cast<uint32_t *>(bM), reinterpret_cast<uint32_t *>(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<uint64_t *>(P_ARRAY_REVERSE)};
#endif // _WIN32
return instance;
}
} // namespace hacl

19
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<Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32, handle_destructor>
HaclBignumContext4096;
#else
typedef std::unique_ptr<Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64, handle_destructor>
HaclBignumContext4096;
#endif // _WIN32
HaclBignumContext4096 context;
};

848
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)
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 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 *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 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 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 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 *os = resM;
uint32_t x = (c & res_j[i]) | (~c & resM[i]);
os[i] = x;
}
}
}
}
}
}
{
uint32_t i0;
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);
{
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 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 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 *os = a_bits_l;
uint32_t x = (c & res_j[i]) | (~c & a_bits_l[i]);
os[i] = x;
}
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 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 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 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;
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);
{
uint32_t *a_bits_l = (uint32_t *)alloca(len1 * sizeof (uint32_t));
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);
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 *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);
}
}
}

9
src/karamel/Hacl_GenericField32.h
Просмотреть файл

@ -30,11 +30,10 @@ extern "C" {
#endif
#include <string.h>
#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"