Module fiat_crypto::p256_64

Autogenerated: ‘src/ExtractionOCaml/word_by_word_montgomery’ –lang Rust p256 64 ‘2^256 - 2^224 + 2^192 + 2^96 - 1’ mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp curve description: p256 machine_wordsize = 64 (from “64”) requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp m = 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff (from “2^256 - 2^224 + 2^192 + 2^96 - 1”)

NOTE: In addition to the bounds specified above each function, all functions synthesized for this Montgomery arithmetic require the input to be strictly less than the prime modulus (m), and also require the input to be in the unique saturated representation. All functions also ensure that these two properties are true of return values.

Computed values: eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) in if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256

Functions

fiat_p256_add	The function fiat_p256_add adds two field elements in the Montgomery domain.
fiat_p256_addcarryx_u64	The function fiat_p256_addcarryx_u64 is an addition with carry.
fiat_p256_cmovznz_u64	The function fiat_p256_cmovznz_u64 is a single-word conditional move.
fiat_p256_divstep	The function fiat_p256_divstep computes a divstep.
fiat_p256_divstep_precomp	The function fiat_p256_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
fiat_p256_from_bytes	The function fiat_p256_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
fiat_p256_from_montgomery	The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain.
fiat_p256_msat	The function fiat_p256_msat returns the saturated representation of the prime modulus.
fiat_p256_mul	The function fiat_p256_mul multiplies two field elements in the Montgomery domain.
fiat_p256_mulx_u64	The function fiat_p256_mulx_u64 is a multiplication, returning the full double-width result.
fiat_p256_nonzero	The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
fiat_p256_opp	The function fiat_p256_opp negates a field element in the Montgomery domain.
fiat_p256_selectznz	The function fiat_p256_selectznz is a multi-limb conditional select.
fiat_p256_set_one	The function fiat_p256_set_one returns the field element one in the Montgomery domain.
fiat_p256_square	The function fiat_p256_square squares a field element in the Montgomery domain.
fiat_p256_sub	The function fiat_p256_sub subtracts two field elements in the Montgomery domain.
fiat_p256_subborrowx_u64	The function fiat_p256_subborrowx_u64 is a subtraction with borrow.
fiat_p256_to_bytes	The function fiat_p256_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
fiat_p256_to_montgomery	The function fiat_p256_to_montgomery translates a field element into the Montgomery domain.

Type Definitions

fiat_p256_i1
fiat_p256_i2
fiat_p256_u1
fiat_p256_u2