Expand description
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.