Module fiat_crypto::p224_32

source ·
Expand description

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

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) 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) 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) in if x1 & (2^224-1) < 2^223 then x1 & (2^224-1) else (x1 & (2^224-1)) - 2^224

Functions

  • fiat_p224_add
    The function fiat_p224_add adds two field elements in the Montgomery domain.
  • fiat_p224_addcarryx_u32
    The function fiat_p224_addcarryx_u32 is an addition with carry.
  • fiat_p224_cmovznz_u32
    The function fiat_p224_cmovznz_u32 is a single-word conditional move.
  • fiat_p224_divstep
    The function fiat_p224_divstep computes a divstep.
  • fiat_p224_divstep_precomp
    The function fiat_p224_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
  • fiat_p224_from_bytes
    The function fiat_p224_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
  • fiat_p224_from_montgomery
    The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain.
  • fiat_p224_msat
    The function fiat_p224_msat returns the saturated representation of the prime modulus.
  • fiat_p224_mul
    The function fiat_p224_mul multiplies two field elements in the Montgomery domain.
  • fiat_p224_mulx_u32
    The function fiat_p224_mulx_u32 is a multiplication, returning the full double-width result.
  • fiat_p224_nonzero
    The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  • fiat_p224_opp
    The function fiat_p224_opp negates a field element in the Montgomery domain.
  • fiat_p224_selectznz
    The function fiat_p224_selectznz is a multi-limb conditional select.
  • fiat_p224_set_one
    The function fiat_p224_set_one returns the field element one in the Montgomery domain.
  • fiat_p224_square
    The function fiat_p224_square squares a field element in the Montgomery domain.
  • fiat_p224_sub
    The function fiat_p224_sub subtracts two field elements in the Montgomery domain.
  • fiat_p224_subborrowx_u32
    The function fiat_p224_subborrowx_u32 is a subtraction with borrow.
  • fiat_p224_to_bytes
    The function fiat_p224_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
  • fiat_p224_to_montgomery
    The function fiat_p224_to_montgomery translates a field element into the Montgomery domain.

Type Definitions