[−][src]Module fiat_crypto::p434_64
Autogenerated: src/ExtractionOCaml/word_by_word_montgomery --lang=Rust p434 '2^216 * 3^137 - 1' 64 mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes curve description: p434 requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes m = 0x2341f271773446cfc5fd681c520567bc65c783158aea3fdc1767ae2ffffffffffffffffffffffffffffffffffffffffffffffffffffff (from "2^216 * 3^137 - 1") machine_wordsize = 64 (from "64")
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) + (z[55] << 0x1b8)
Functions
| fiat_p434_mul | The function fiat_p434_mul multiplies two field elements in the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m 0 ≤ eval arg2 < m Postconditions: eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m 0 ≤ eval out1 < m |
| fiat_p434_square | The function fiat_p434_square squares a field element in the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m Postconditions: eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m 0 ≤ eval out1 < m |
| fiat_p434_add | The function fiat_p434_add adds two field elements in the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m 0 ≤ eval arg2 < m Postconditions: eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m 0 ≤ eval out1 < m |
| fiat_p434_sub | The function fiat_p434_sub subtracts two field elements in the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m 0 ≤ eval arg2 < m Postconditions: eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m 0 ≤ eval out1 < m |
| fiat_p434_opp | The function fiat_p434_opp negates a field element in the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m Postconditions: eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m 0 ≤ eval out1 < m |
| fiat_p434_from_montgomery | The function fiat_p434_from_montgomery translates a field element out of the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m Postconditions: eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^7) mod m 0 ≤ eval out1 < m |
| fiat_p434_to_montgomery | The function fiat_p434_to_montgomery translates a field element into the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m Postconditions: eval (from_montgomery out1) mod m = eval arg1 mod m 0 ≤ eval out1 < m |
| fiat_p434_nonzero | The function fiat_p434_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. Preconditions: 0 ≤ eval arg1 < m Postconditions: out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 |
| fiat_p434_selectznz | The function fiat_p434_selectznz is a multi-limb conditional select. Postconditions: eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) |
| fiat_p434_to_bytes | The function fiat_p434_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. Preconditions: 0 ≤ eval arg1 < m Postconditions: out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..55] |
| fiat_p434_from_bytes | The function fiat_p434_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. Preconditions: 0 ≤ bytes_eval arg1 < m Postconditions: eval out1 mod m = bytes_eval arg1 mod m 0 ≤ eval out1 < m |
| fiat_p434_addcarryx_u64 | The function fiat_p434_addcarryx_u64 is an addition with carry. Postconditions: out1 = (arg1 + arg2 + arg3) mod 2^64 out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ |
| fiat_p434_cmovznz_u64 | The function fiat_p434_cmovznz_u64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3) |
| fiat_p434_mulx_u64 | The function fiat_p434_mulx_u64 is a multiplication, returning the full double-width result. Postconditions: out1 = (arg1 * arg2) mod 2^64 out2 = ⌊arg1 * arg2 / 2^64⌋ |
| fiat_p434_subborrowx_u64 | The function fiat_p434_subborrowx_u64 is a subtraction with borrow. Postconditions: out1 = (-arg1 + arg2 + -arg3) mod 2^64 out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ |
Type Definitions
| fiat_p434_i1 | |
| fiat_p434_i2 | |
| fiat_p434_u1 | |
| fiat_p434_u2 |