Module fiat_crypto::p521_64

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

Computed values: carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1]

Functions

fiat_p521_carry_mul	The function fiat_p521_carry_mul multiplies two field elements and reduces the result. Postconditions: eval out1 mod m = (eval arg1 * eval arg2) mod m
fiat_p521_carry_square	The function fiat_p521_carry_square squares a field element and reduces the result. Postconditions: eval out1 mod m = (eval arg1 * eval arg1) mod m
fiat_p521_carry	The function fiat_p521_carry reduces a field element. Postconditions: eval out1 mod m = eval arg1 mod m
fiat_p521_add	The function fiat_p521_add adds two field elements. Postconditions: eval out1 mod m = (eval arg1 + eval arg2) mod m
fiat_p521_sub	The function fiat_p521_sub subtracts two field elements. Postconditions: eval out1 mod m = (eval arg1 - eval arg2) mod m
fiat_p521_opp	The function fiat_p521_opp negates a field element. Postconditions: eval out1 mod m = -eval arg1 mod m
fiat_p521_selectznz	The function fiat_p521_selectznz is a multi-limb conditional select. Postconditions: eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
fiat_p521_to_bytes	The function fiat_p521_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..65]
fiat_p521_from_bytes	The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order. Postconditions: eval out1 mod m = bytes_eval arg1 mod m
fiat_p521_addcarryx_u57	The function fiat_p521_addcarryx_u57 is an addition with carry. Postconditions: out1 = (arg1 + arg2 + arg3) mod 2^57 out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋
fiat_p521_addcarryx_u58	The function fiat_p521_addcarryx_u58 is an addition with carry. Postconditions: out1 = (arg1 + arg2 + arg3) mod 2^58 out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋
fiat_p521_cmovznz_u64	The function fiat_p521_cmovznz_u64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3)
fiat_p521_subborrowx_u57	The function fiat_p521_subborrowx_u57 is a subtraction with borrow. Postconditions: out1 = (-arg1 + arg2 + -arg3) mod 2^57 out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋
fiat_p521_subborrowx_u58	The function fiat_p521_subborrowx_u58 is a subtraction with borrow. Postconditions: out1 = (-arg1 + arg2 + -arg3) mod 2^58 out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋

Type Definitions

fiat_p521_i1
fiat_p521_i2
fiat_p521_u1
fiat_p521_u2