Montgomery Field Arithmetic

Montgomery Field Arithmetic#

A verified Montgomery field arithmetic library.

HACL Packages comes with two versions, a 32-bit optimized version, where bignums are represented as an array of len unsigned 32-bit integers, i.e., uint32_t[len] and a 64-bit optimized version.

All the arithmetic operations are performed in the Montgomery domain and preserve the invariant that aM < n for a bignum aM in Montgomery form.

API Reference#

#include "Hacl_GenericField32.h"

Typedefs#

typedef Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *Hacl_GenericField32_pbn_mont_ctx_u32#

Functions#

bool Hacl_GenericField32_field_modulus_check(uint32_t len, uint32_t *n)#

Check whether this library will work for a modulus n.

The function returns false if any of the following preconditions are violated, true otherwise. • n % 2 = 1 • 1 < n

Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *Hacl_GenericField32_field_init(uint32_t len, uint32_t *n)#

Heap-allocate and initialize a montgomery context.

The argument n is meant to be len limbs in size, i.e. uint32_t[len].

Before calling this function, the caller will need to ensure that the following preconditions are observed. • n % 2 = 1 • 1 < n

The caller will need to call Hacl_GenericField32_field_free on the return value to avoid memory leaks.

void Hacl_GenericField32_field_free(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k)#

Deallocate the memory previously allocated by Hacl_GenericField32_field_init.

The argument k is a montgomery context obtained through Hacl_GenericField32_field_init.

uint32_t Hacl_GenericField32_field_get_len(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k)#

Return the size of a modulus n in limbs.

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)#

Convert a bignum from the regular representation to the Montgomery representation.

Write a * R mod n in aM.

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_from_field(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, uint32_t *a)#

Convert a result back from the Montgomery representation to the regular representation.

Write aM / R mod n in a, i.e. Hacl_GenericField32_from_field(k, Hacl_GenericField32_to_field(k, a)) == a % n

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_add(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, uint32_t *bM, uint32_t *cM)#

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_sub(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, uint32_t *bM, uint32_t *cM)#

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_mul(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, uint32_t *bM, uint32_t *cM)#

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_sqr(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, uint32_t *cM)#

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_one(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *oneM)#

Convert a bignum one to its Montgomery representation.

The outparam oneM is 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_exp_consttime(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, uint32_t bBits, uint32_t *b, uint32_t *resM)#

Write aM ^ b mod n in resM.

The argument aM and the outparam resM 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.

The argument b is a bignum of any size, and bBits is an upper bound on the number of significant bits of b. A tighter bound results in faster execution time. When in doubt, the number of bits for the bignum size is always a safe default, e.g. if b is a 256-bit bignum, bBits should be 256.

This function is constant-time over its argument b, at the cost of a slower execution time than exp_vartime.

Before calling this function, the caller will need to ensure that the following 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)#

Write aM ^ b mod n in resM.

The argument aM and the outparam resM 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.

The argument b is a bignum of any size, and bBits is an upper bound on the number of significant bits of b. A tighter bound results in faster execution time. When in doubt, the number of bits for the bignum size is always a safe default, e.g. if b is a 256-bit bignum, bBits should be 256.

The function is NOT constant-time on the argument b. See the exp_consttime function for constant-time variant.

Before calling this function, the caller will need to ensure that the following precondition is observed. • b < pow2 bBits

void Hacl_GenericField32_inverse(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 *k, uint32_t *aM, uint32_t *aInvM)#

Write aM ^ (-1) mod n in aInvM.

The argument aM and the outparam aInvM 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.

Before calling this function, the caller will need to ensure that the following preconditions are observed. • n is a prime • 0 < aM

Contents