Module fiat_crypto::p448_solinas_32

source ·
Expand description

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

Computed values: carry_chain = [7, 15, 8, 0, 9, 1, 10, 2, 11, 3, 12, 4, 13, 5, 14, 6, 15, 7, 8, 0] eval z = z[0] + (z[1] << 28) + (z[2] << 56) + (z[3] << 84) + (z[4] << 112) + (z[5] << 140) + (z[6] << 168) + (z[7] << 196) + (z[8] << 224) + (z[9] << 252) + (z[10] << 0x118) + (z[11] << 0x134) + (z[12] << 0x150) + (z[13] << 0x16c) + (z[14] << 0x188) + (z[15] << 0x1a4) 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) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) balance = [0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffc, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe]

Structs§

  • fiat_p448_loose_field_element
    The type fiat_p448_loose_field_element is a field element with loose bounds. Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000]]
  • fiat_p448_tight_field_element
    The type fiat_p448_tight_field_element is a field element with tight bounds. Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000]]

Functions§

  • fiat_p448_add
    The function fiat_p448_add adds two field elements.
  • fiat_p448_addcarryx_u28
    The function fiat_p448_addcarryx_u28 is an addition with carry.
  • fiat_p448_carry
    The function fiat_p448_carry reduces a field element.
  • fiat_p448_carry_mul
    The function fiat_p448_carry_mul multiplies two field elements and reduces the result.
  • fiat_p448_carry_square
    The function fiat_p448_carry_square squares a field element and reduces the result.
  • fiat_p448_cmovznz_u32
    The function fiat_p448_cmovznz_u32 is a single-word conditional move.
  • fiat_p448_from_bytes
    The function fiat_p448_from_bytes deserializes a field element from bytes in little-endian order.
  • fiat_p448_opp
    The function fiat_p448_opp negates a field element.
  • fiat_p448_relax
    The function fiat_p448_relax is the identity function converting from tight field elements to loose field elements.
  • fiat_p448_selectznz
    The function fiat_p448_selectznz is a multi-limb conditional select.
  • fiat_p448_sub
    The function fiat_p448_sub subtracts two field elements.
  • fiat_p448_subborrowx_u28
    The function fiat_p448_subborrowx_u28 is a subtraction with borrow.
  • fiat_p448_to_bytes
    The function fiat_p448_to_bytes serializes a field element to bytes in little-endian order.

Type Aliases§

  • fiat_p448_i1
    fiat_p448_i1 represents values of 1 bits, stored in one byte.
  • fiat_p448_i2
    fiat_p448_i2 represents values of 2 bits, stored in one byte.
  • fiat_p448_u1
    fiat_p448_u1 represents values of 1 bits, stored in one byte.
  • fiat_p448_u2
    fiat_p448_u2 represents values of 2 bits, stored in one byte.