Module fiat_crypto::p384_32
source · Expand description
Autogenerated: ‘src/ExtractionOCaml/word_by_word_montgomery’ –lang Rust –inline p384 32 ‘2^384 - 2^128 - 2^96 + 2^32 - 1’ mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp curve description: p384 machine_wordsize = 32 (from “32”) requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp m = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff (from “2^384 - 2^128 - 2^96 + 2^32 - 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] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) + (z[7] << 224) + (z[8] << 256) + (z[9] << 0x120) + (z[10] << 0x140) + (z[11] << 0x160) 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) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) twos_complement_eval z = let x1 := z[0] + (z[1] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) + (z[7] << 224) + (z[8] << 256) + (z[9] << 0x120) + (z[10] << 0x140) + (z[11] << 0x160) in if x1 & (2^384-1) < 2^383 then x1 & (2^384-1) else (x1 & (2^384-1)) - 2^384
Functions
- The function fiat_p384_add adds two field elements in the Montgomery domain.
- The function fiat_p384_addcarryx_u32 is an addition with carry.
- The function fiat_p384_cmovznz_u32 is a single-word conditional move.
- The function fiat_p384_divstep computes a divstep.
- The function fiat_p384_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
- The function fiat_p384_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
- The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain.
- The function fiat_p384_msat returns the saturated representation of the prime modulus.
- The function fiat_p384_mul multiplies two field elements in the Montgomery domain.
- The function fiat_p384_mulx_u32 is a multiplication, returning the full double-width result.
- The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- The function fiat_p384_opp negates a field element in the Montgomery domain.
- The function fiat_p384_selectznz is a multi-limb conditional select.
- The function fiat_p384_set_one returns the field element one in the Montgomery domain.
- The function fiat_p384_square squares a field element in the Montgomery domain.
- The function fiat_p384_sub subtracts two field elements in the Montgomery domain.
- The function fiat_p384_subborrowx_u32 is a subtraction with borrow.
- The function fiat_p384_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
- The function fiat_p384_to_montgomery translates a field element into the Montgomery domain.