Module fiat_crypto::secp256k1_64

Autogenerated: src/ExtractionOCaml/word_by_word_montgomery --lang Rust secp256k1 64 '2^256 - 2^32 - 977' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp curve description: secp256k1 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 = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f (from "2^256 - 2^32 - 977")

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) 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_secp256k1_add	The function fiat_secp256k1_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_secp256k1_addcarryx_u64	The function fiat_secp256k1_addcarryx_u64 is an addition with carry. Postconditions: out1 = (arg1 + arg2 + arg3) mod 2^64 out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
fiat_secp256k1_cmovznz_u64	The function fiat_secp256k1_cmovznz_u64 is a single-word conditional move. Postconditions: out1 = (if arg1 = 0 then arg2 else arg3)
fiat_secp256k1_divstep	The function fiat_secp256k1_divstep computes a divstep. Preconditions: 0 ≤ eval arg4 < m 0 ≤ eval arg5 < m Postconditions: out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1) twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2) twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋) eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m) eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m) 0 ≤ eval out5 < m 0 ≤ eval out5 < m 0 ≤ eval out2 < m 0 ≤ eval out3 < m
fiat_secp256k1_divstep_precomp	The function fiat_secp256k1_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form). Postconditions: eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if (log2 m) + 1 < 46 then ⌊(49 * ((log2 m) + 1) + 80) / 17⌋ else ⌊(49 * ((log2 m) + 1) + 57) / 17⌋) 0 ≤ eval out1 < m
fiat_secp256k1_from_bytes	The function fiat_secp256k1_from_bytes deserializes a field element NOT 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_secp256k1_from_montgomery	The function fiat_secp256k1_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)^4) mod m 0 ≤ eval out1 < m
fiat_secp256k1_msat	The function fiat_secp256k1_msat returns the saturated represtation of the prime modulus. Postconditions: twos_complement_eval out1 = m 0 ≤ eval out1 < m
fiat_secp256k1_mul	The function fiat_secp256k1_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_secp256k1_mulx_u64	The function fiat_secp256k1_mulx_u64 is a multiplication, returning the full double-width result. Postconditions: out1 = (arg1 * arg2) mod 2^64 out2 = ⌊arg1 * arg2 / 2^64⌋
fiat_secp256k1_nonzero	The function fiat_secp256k1_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_secp256k1_opp	The function fiat_secp256k1_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_secp256k1_selectznz	The function fiat_secp256k1_selectznz is a multi-limb conditional select. Postconditions: eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
fiat_secp256k1_set_one	The function fiat_secp256k1_set_one returns the field element one in the Montgomery domain. Postconditions: eval (from_montgomery out1) mod m = 1 mod m 0 ≤ eval out1 < m
fiat_secp256k1_square	The function fiat_secp256k1_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_secp256k1_sub	The function fiat_secp256k1_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_secp256k1_subborrowx_u64	The function fiat_secp256k1_subborrowx_u64 is a subtraction with borrow. Postconditions: out1 = (-arg1 + arg2 + -arg3) mod 2^64 out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
fiat_secp256k1_to_bytes	The function fiat_secp256k1_to_bytes serializes a field element NOT 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..31]
fiat_secp256k1_to_montgomery	The function fiat_secp256k1_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

Type Definitions

fiat_secp256k1_i1
fiat_secp256k1_i2
fiat_secp256k1_u1
fiat_secp256k1_u2