Module fiat_crypto::curve25519_solinas_64

Autogenerated: ‘src/ExtractionOCaml/solinas_reduction’ –lang Rust –inline curve25519_solinas 64 ‘2^255 - 19’ mul square curve description: curve25519_solinas machine_wordsize = 64 (from “64”) requested operations: mul, square s-c = 2^255 - [(1, 19)] (from “2^255 - 19”)

Computed values:

Functions

• fiat_curve25519_solinas_addcarryx_u64
  The function fiat_curve25519_solinas_addcarryx_u64 is an addition with carry.
• fiat_curve25519_solinas_cmovznz_u64
  The function fiat_curve25519_solinas_cmovznz_u64 is a single-word conditional move.
• fiat_curve25519_solinas_mul
  The function fiat_curve25519_solinas_mul multiplies two field elements.
• fiat_curve25519_solinas_mulx_u64
  The function fiat_curve25519_solinas_mulx_u64 is a multiplication, returning the full double-width result.
• fiat_curve25519_solinas_square
  The function fiat_curve25519_solinas_square squares a field element.
• fiat_curve25519_solinas_subborrowx_u64
  The function fiat_curve25519_solinas_subborrowx_u64 is a subtraction with borrow.

Type Aliases

• fiat_curve25519_solinas_i1
  fiat_curve25519_solinas_i1 represents values of 1 bits, stored in one byte.
• fiat_curve25519_solinas_i2
  fiat_curve25519_solinas_i2 represents values of 2 bits, stored in one byte.
• fiat_curve25519_solinas_u1
  fiat_curve25519_solinas_u1 represents values of 1 bits, stored in one byte.
• fiat_curve25519_solinas_u2
  fiat_curve25519_solinas_u2 represents values of 2 bits, stored in one byte.