Module fiat_crypto::curve25519_64

Autogenerated: src/ExtractionOCaml/unsaturated_solinas --lang=Rust 25519 5 '2^255 - 19' 64 carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes carry_scmul121666 curve description: 25519 requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, carry_scmul121666 n = 5 (from "5") s-c = 2^255 - [(1, 19)] (from "2^255 - 19") machine_wordsize = 64 (from "64")

Computed values: carry_chain = [0, 1, 2, 3, 4, 0, 1] eval z = z[0] + (z[1] << 51) + (z[2] << 102) + (z[3] << 153) + (z[4] << 204) 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)

Functions

fiat_25519_carry_mul	The function fiat_25519_carry_mul multiplies two field elements and reduces the result. Postconditions: eval out1 mod m = (eval arg1 * eval arg2) mod m
fiat_25519_carry_square	The function fiat_25519_carry_square squares a field element and reduces the result. Postconditions: eval out1 mod m = (eval arg1 * eval arg1) mod m
fiat_25519_carry	The function fiat_25519_carry reduces a field element. Postconditions: eval out1 mod m = eval arg1 mod m
fiat_25519_add	The function fiat_25519_add adds two field elements. Postconditions: eval out1 mod m = (eval arg1 + eval arg2) mod m
fiat_25519_sub	The function fiat_25519_sub subtracts two field elements. Postconditions: eval out1 mod m = (eval arg1 - eval arg2) mod m
fiat_25519_opp	The function fiat_25519_opp negates a field element. Postconditions: eval out1 mod m = -eval arg1 mod m
fiat_25519_selectznz	The function fiat_25519_selectznz is a multi-limb conditional select. Postconditions: eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
fiat_25519_to_bytes	The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order. Postconditions: out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
fiat_25519_from_bytes	The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order. Postconditions: eval out1 mod m = bytes_eval arg1 mod m
fiat_25519_addcarryx_u51	The function fiat_25519_addcarryx_u51 is an addition with carry. Postconditions: out1 = (arg1 + arg2 + arg3) mod 2^51 out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋
fiat_25519_carry_scmul_121666	The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result. Postconditions: eval out1 mod m = (121666 * eval arg1) mod m
fiat_25519_cmovznz_u64	The function fiat_25519_cmovznz_u64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3)
fiat_25519_subborrowx_u51	The function fiat_25519_subborrowx_u51 is a subtraction with borrow. Postconditions: out1 = (-arg1 + arg2 + -arg3) mod 2^51 out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋

Type Definitions

fiat_25519_i1
fiat_25519_i2
fiat_25519_u1
fiat_25519_u2