Module fiat_crypto::curve25519_32

Autogenerated: ‘src/ExtractionOCaml/unsaturated_solinas’ –lang Rust –inline 25519 32 ‘(auto)’ ‘2^255 - 19’ carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666 curve description: 25519 machine_wordsize = 32 (from “32”) requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666 n = 10 (from “(auto)”) s-c = 2^255 - [(1, 19)] (from “2^255 - 19”) tight_bounds_multiplier = 1 (from “”)

Computed values: carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1] eval z = z[0] + (z[1] << 26) + (z[2] << 51) + (z[3] << 77) + (z[4] << 102) + (z[5] << 128) + (z[6] << 153) + (z[7] << 179) + (z[8] << 204) + (z[9] << 230) 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) balance = [0x7ffffda, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe]

Structs

• fiat_25519_loose_field_element
  The type fiat_25519_loose_field_element is a field element with loose bounds. Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]]
• fiat_25519_tight_field_element
  The type fiat_25519_tight_field_element is a field element with tight bounds. Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]]

Functions

• fiat_25519_add
  The function fiat_25519_add adds two field elements.
• fiat_25519_addcarryx_u25
  The function fiat_25519_addcarryx_u25 is an addition with carry.
• fiat_25519_addcarryx_u26
  The function fiat_25519_addcarryx_u26 is an addition with carry.
• fiat_25519_carry
  The function fiat_25519_carry reduces a field element.
• fiat_25519_carry_mul
  The function fiat_25519_carry_mul multiplies two field elements and reduces the result.
• fiat_25519_carry_scmul_121666
  The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result.
• fiat_25519_carry_square
  The function fiat_25519_carry_square squares a field element and reduces the result.
• fiat_25519_cmovznz_u32
  The function fiat_25519_cmovznz_u32 is a single-word conditional move.
• fiat_25519_from_bytes
  The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order.
• fiat_25519_opp
  The function fiat_25519_opp negates a field element.
• fiat_25519_relax
  The function fiat_25519_relax is the identity function converting from tight field elements to loose field elements.
• fiat_25519_selectznz
  The function fiat_25519_selectznz is a multi-limb conditional select.
• fiat_25519_sub
  The function fiat_25519_sub subtracts two field elements.
• fiat_25519_subborrowx_u25
  The function fiat_25519_subborrowx_u25 is a subtraction with borrow.
• fiat_25519_subborrowx_u26
  The function fiat_25519_subborrowx_u26 is a subtraction with borrow.
• fiat_25519_to_bytes
  The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order.

Type Aliases

• fiat_25519_i1
  fiat_25519_i1 represents values of 1 bits, stored in one byte.
• fiat_25519_i2
  fiat_25519_i2 represents values of 2 bits, stored in one byte.
• fiat_25519_u1
  fiat_25519_u1 represents values of 1 bits, stored in one byte.
• fiat_25519_u2
  fiat_25519_u2 represents values of 2 bits, stored in one byte.