Module fiat_crypto::curve25519_scalar_32

Autogenerated: ‘src/ExtractionOCaml/word_by_word_montgomery’ –lang Rust –inline 25519_scalar 32 ‘2^252 + 27742317777372353535851937790883648493’ mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp curve description: 25519_scalar 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 = 0x1000000000000000000000000000000014def9dea2f79cd65812631a5cf5d3ed (from “2^252 + 27742317777372353535851937790883648493”)

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) 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] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) + (z[7] << 224) in if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256

Structs

• fiat_25519_scalar_montgomery_domain_field_element
  The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
• fiat_25519_scalar_non_montgomery_domain_field_element
  The type fiat_25519_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]

Functions

• fiat_25519_scalar_add
  The function fiat_25519_scalar_add adds two field elements in the Montgomery domain.
• fiat_25519_scalar_addcarryx_u32
  The function fiat_25519_scalar_addcarryx_u32 is an addition with carry.
• fiat_25519_scalar_cmovznz_u32
  The function fiat_25519_scalar_cmovznz_u32 is a single-word conditional move.
• fiat_25519_scalar_divstep
  The function fiat_25519_scalar_divstep computes a divstep.
• fiat_25519_scalar_divstep_precomp
  The function fiat_25519_scalar_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
• fiat_25519_scalar_from_bytes
  The function fiat_25519_scalar_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
• fiat_25519_scalar_from_montgomery
  The function fiat_25519_scalar_from_montgomery translates a field element out of the Montgomery domain.
• fiat_25519_scalar_msat
  The function fiat_25519_scalar_msat returns the saturated representation of the prime modulus.
• fiat_25519_scalar_mul
  The function fiat_25519_scalar_mul multiplies two field elements in the Montgomery domain.
• fiat_25519_scalar_mulx_u32
  The function fiat_25519_scalar_mulx_u32 is a multiplication, returning the full double-width result.
• fiat_25519_scalar_nonzero
  The function fiat_25519_scalar_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
• fiat_25519_scalar_opp
  The function fiat_25519_scalar_opp negates a field element in the Montgomery domain.
• fiat_25519_scalar_selectznz
  The function fiat_25519_scalar_selectznz is a multi-limb conditional select.
• fiat_25519_scalar_set_one
  The function fiat_25519_scalar_set_one returns the field element one in the Montgomery domain.
• fiat_25519_scalar_square
  The function fiat_25519_scalar_square squares a field element in the Montgomery domain.
• fiat_25519_scalar_sub
  The function fiat_25519_scalar_sub subtracts two field elements in the Montgomery domain.
• fiat_25519_scalar_subborrowx_u32
  The function fiat_25519_scalar_subborrowx_u32 is a subtraction with borrow.
• fiat_25519_scalar_to_bytes
  The function fiat_25519_scalar_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
• fiat_25519_scalar_to_montgomery
  The function fiat_25519_scalar_to_montgomery translates a field element into the Montgomery domain.

Type Aliases

• fiat_25519_scalar_i1
  fiat_25519_scalar_i1 represents values of 1 bits, stored in one byte.
• fiat_25519_scalar_i2
  fiat_25519_scalar_i2 represents values of 2 bits, stored in one byte.
• fiat_25519_scalar_u1
  fiat_25519_scalar_u1 represents values of 1 bits, stored in one byte.
• fiat_25519_scalar_u2
  fiat_25519_scalar_u2 represents values of 2 bits, stored in one byte.