Expand description
fiat-crypto output postprocessed by fiat-constify: https://github.com/rustcrypto/utils Autogenerated: ‘./word_by_word_montgomery’ –lang Rust –inline p521_scalar 64 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 curve description: p521_scalar machine_wordsize = 64 (from “64”) requested operations: (all) m = 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 (from “0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409”)
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) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) 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) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) in if x1 & (2^576-1) < 2^575 then x1 & (2^576-1) else (x1 & (2^576-1)) - 2^576
Functions§
- fiat_
p521_ scalar_ add - The function fiat_p521_scalar_add adds two field elements in the Montgomery domain.
- fiat_
p521_ scalar_ addcarryx_ u64 - The function fiat_p521_scalar_addcarryx_u64 is an addition with carry.
- fiat_
p521_ scalar_ cmovznz_ u64 - The function fiat_p521_scalar_cmovznz_u64 is a single-word conditional move.
- fiat_
p521_ scalar_ divstep - The function fiat_p521_scalar_divstep computes a divstep.
- fiat_
p521_ scalar_ divstep_ precomp - The function fiat_p521_scalar_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
- fiat_
p521_ scalar_ from_ bytes - The function fiat_p521_scalar_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
- fiat_
p521_ scalar_ from_ montgomery - The function fiat_p521_scalar_from_montgomery translates a field element out of the Montgomery domain.
- fiat_
p521_ scalar_ msat - The function fiat_p521_scalar_msat returns the saturated representation of the prime modulus.
- fiat_
p521_ scalar_ mul - The function fiat_p521_scalar_mul multiplies two field elements in the Montgomery domain.
- fiat_
p521_ scalar_ mulx_ u64 - The function fiat_p521_scalar_mulx_u64 is a multiplication, returning the full double-width result.
- fiat_
p521_ scalar_ nonzero - The function fiat_p521_scalar_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- fiat_
p521_ scalar_ opp - The function fiat_p521_scalar_opp negates a field element in the Montgomery domain.
- fiat_
p521_ scalar_ selectznz - The function fiat_p521_scalar_selectznz is a multi-limb conditional select.
- fiat_
p521_ scalar_ set_ one - The function fiat_p521_scalar_set_one returns the field element one in the Montgomery domain.
- fiat_
p521_ scalar_ square - The function fiat_p521_scalar_square squares a field element in the Montgomery domain.
- fiat_
p521_ scalar_ sub - The function fiat_p521_scalar_sub subtracts two field elements in the Montgomery domain.
- fiat_
p521_ scalar_ subborrowx_ u64 - The function fiat_p521_scalar_subborrowx_u64 is a subtraction with borrow.
- fiat_
p521_ scalar_ to_ bytes - The function fiat_p521_scalar_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
- fiat_
p521_ scalar_ to_ montgomery - The function fiat_p521_scalar_to_montgomery translates a field element into the Montgomery domain.