Expand description
Autogenerated: ‘src/ExtractionOCaml/word_by_word_montgomery’ –lang Rust –inline secp256k1_montgomery 64 ‘2^256 - 2^32 - 977’ mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp curve description: secp256k1_montgomery 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 = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f (from “2^256 - 2^32 - 977”)
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
Structs§
- fiat_
secp256k1_ montgomery_ montgomery_ domain_ field_ element - The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
- fiat_
secp256k1_ montgomery_ non_ montgomery_ domain_ field_ element - The type fiat_secp256k1_montgomery_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
Functions§
- fiat_
secp256k1_ montgomery_ add - The function fiat_secp256k1_montgomery_add adds two field elements in the Montgomery domain.
- fiat_
secp256k1_ montgomery_ addcarryx_ u64 - The function fiat_secp256k1_montgomery_addcarryx_u64 is an addition with carry.
- fiat_
secp256k1_ montgomery_ cmovznz_ u64 - The function fiat_secp256k1_montgomery_cmovznz_u64 is a single-word conditional move.
- fiat_
secp256k1_ montgomery_ divstep - The function fiat_secp256k1_montgomery_divstep computes a divstep.
- fiat_
secp256k1_ montgomery_ divstep_ precomp - The function fiat_secp256k1_montgomery_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
- fiat_
secp256k1_ montgomery_ from_ bytes - The function fiat_secp256k1_montgomery_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
- fiat_
secp256k1_ montgomery_ from_ montgomery - The function fiat_secp256k1_montgomery_from_montgomery translates a field element out of the Montgomery domain.
- fiat_
secp256k1_ montgomery_ msat - The function fiat_secp256k1_montgomery_msat returns the saturated representation of the prime modulus.
- fiat_
secp256k1_ montgomery_ mul - The function fiat_secp256k1_montgomery_mul multiplies two field elements in the Montgomery domain.
- fiat_
secp256k1_ montgomery_ mulx_ u64 - The function fiat_secp256k1_montgomery_mulx_u64 is a multiplication, returning the full double-width result.
- fiat_
secp256k1_ montgomery_ nonzero - The function fiat_secp256k1_montgomery_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- fiat_
secp256k1_ montgomery_ opp - The function fiat_secp256k1_montgomery_opp negates a field element in the Montgomery domain.
- fiat_
secp256k1_ montgomery_ selectznz - The function fiat_secp256k1_montgomery_selectznz is a multi-limb conditional select.
- fiat_
secp256k1_ montgomery_ set_ one - The function fiat_secp256k1_montgomery_set_one returns the field element one in the Montgomery domain.
- fiat_
secp256k1_ montgomery_ square - The function fiat_secp256k1_montgomery_square squares a field element in the Montgomery domain.
- fiat_
secp256k1_ montgomery_ sub - The function fiat_secp256k1_montgomery_sub subtracts two field elements in the Montgomery domain.
- fiat_
secp256k1_ montgomery_ subborrowx_ u64 - The function fiat_secp256k1_montgomery_subborrowx_u64 is a subtraction with borrow.
- fiat_
secp256k1_ montgomery_ to_ bytes - The function fiat_secp256k1_montgomery_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
- fiat_
secp256k1_ montgomery_ to_ montgomery - The function fiat_secp256k1_montgomery_to_montgomery translates a field element into the Montgomery domain.
Type Aliases§
- fiat_
secp256k1_ montgomery_ i1 - fiat_secp256k1_montgomery_i1 represents values of 1 bits, stored in one byte.
- fiat_
secp256k1_ montgomery_ i2 - fiat_secp256k1_montgomery_i2 represents values of 2 bits, stored in one byte.
- fiat_
secp256k1_ montgomery_ u1 - fiat_secp256k1_montgomery_u1 represents values of 1 bits, stored in one byte.
- fiat_
secp256k1_ montgomery_ u2 - fiat_secp256k1_montgomery_u2 represents values of 2 bits, stored in one byte.