Module p434_64

Autogenerated: ‘src/ExtractionOCaml/word_by_word_montgomery’ –lang Rust –inline p434 64 ‘2^216 * 3^137 - 1’ mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp curve description: p434 machine_wordsize = 64 (from “64”) requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp m = 0x2341f271773446cfc5fd681c520567bc65c783158aea3fdc1767ae2ffffffffffffffffffffffffffffffffffffffffffffffffffffff (from “2^216 * 3^137 - 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] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) 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) twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) in if x1 & (2^448-1) < 2^447 then x1 & (2^448-1) else (x1 & (2^448-1)) - 2^448

Structs

fiat_p434_montgomery_domain_field_element

The type fiat_p434_montgomery_domain_field_element is a field element in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

fiat_p434_non_montgomery_domain_field_element

The type fiat_p434_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]

Functions

fiat_p434_add

The function fiat_p434_add adds two field elements in the Montgomery domain.

fiat_p434_addcarryx_u64

The function fiat_p434_addcarryx_u64 is an addition with carry.

fiat_p434_cmovznz_u64

The function fiat_p434_cmovznz_u64 is a single-word conditional move.

fiat_p434_divstep

The function fiat_p434_divstep computes a divstep.

fiat_p434_divstep_precomp

The function fiat_p434_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).

fiat_p434_from_bytes

The function fiat_p434_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.

fiat_p434_from_montgomery

The function fiat_p434_from_montgomery translates a field element out of the Montgomery domain.

fiat_p434_msat

The function fiat_p434_msat returns the saturated representation of the prime modulus.

fiat_p434_mul

The function fiat_p434_mul multiplies two field elements in the Montgomery domain.

fiat_p434_mulx_u64

The function fiat_p434_mulx_u64 is a multiplication, returning the full double-width result.

fiat_p434_nonzero

The function fiat_p434_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.

fiat_p434_opp

The function fiat_p434_opp negates a field element in the Montgomery domain.

fiat_p434_selectznz

The function fiat_p434_selectznz is a multi-limb conditional select.

fiat_p434_set_one

The function fiat_p434_set_one returns the field element one in the Montgomery domain.

fiat_p434_square

The function fiat_p434_square squares a field element in the Montgomery domain.

fiat_p434_sub

The function fiat_p434_sub subtracts two field elements in the Montgomery domain.

fiat_p434_subborrowx_u64

The function fiat_p434_subborrowx_u64 is a subtraction with borrow.

fiat_p434_to_bytes

The function fiat_p434_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.

fiat_p434_to_montgomery

The function fiat_p434_to_montgomery translates a field element into the Montgomery domain.

Type Aliases

fiat_p434_i1

fiat_p434_i1 represents values of 1 bits, stored in one byte.

fiat_p434_i2

fiat_p434_i2 represents values of 2 bits, stored in one byte.

fiat_p434_u1

fiat_p434_u1 represents values of 1 bits, stored in one byte.

fiat_p434_u2

fiat_p434_u2 represents values of 2 bits, stored in one byte.