From 6fbafbb3a90a5491103e0044042bfc726b9eab7b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 30 Jan 2019 23:04:35 -0500 Subject: Address code review comments to improve docstrings --- curve25519_32.c | 26 ++++++++++----------- curve25519_64.c | 22 +++++++++--------- p224_32.c | 24 +++++++++---------- p224_64.c | 24 +++++++++---------- p256_32.c | 24 +++++++++---------- p256_64.c | 24 +++++++++---------- p384_32.c | 24 +++++++++---------- p384_64.c | 24 +++++++++---------- p448_solinas_64.c | 20 ++++++++-------- p484_64.c | 24 +++++++++---------- p521_32.c | 24 +++++++++---------- p521_64.c | 24 +++++++++---------- secp256k1_32.c | 24 +++++++++---------- secp256k1_64.c | 24 +++++++++---------- src/PushButtonSynthesis/Primitives.v | 4 ++-- src/PushButtonSynthesis/SaturatedSolinas.v | 2 +- src/PushButtonSynthesis/UnsaturatedSolinas.v | 24 +++++++++---------- src/PushButtonSynthesis/WordByWordMontgomery.v | 32 ++++++++++++++------------ 18 files changed, 198 insertions(+), 196 deletions(-) diff --git a/curve25519_32.c b/curve25519_32.c index ccb1085fb..76f266afd 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -15,7 +15,7 @@ typedef signed char fiat_25519_int1; /* - * The function fiat_25519_addcarryx_u26 is an add with carry. + * The function fiat_25519_addcarryx_u26 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^26 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋ * Input Bounds: @@ -35,7 +35,7 @@ static void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fia } /* - * The function fiat_25519_subborrowx_u26 is a sub with borrow. + * The function fiat_25519_subborrowx_u26 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^26 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋ * Input Bounds: @@ -55,7 +55,7 @@ static void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fi } /* - * The function fiat_25519_addcarryx_u25 is an add with carry. + * The function fiat_25519_addcarryx_u25 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^25 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋ * Input Bounds: @@ -75,7 +75,7 @@ static void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fia } /* - * The function fiat_25519_subborrowx_u25 is a sub with borrow. + * The function fiat_25519_subborrowx_u25 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^25 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋ * Input Bounds: @@ -112,7 +112,7 @@ static void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32 } /* - * The function fiat_25519_carry_mul does stuff. + * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. * eval out1 mod m = (eval arg1 * eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] @@ -281,7 +281,7 @@ static void fiat_25519_carry_mul(uint32_t out1[10], const uint32_t arg1[10], con } /* - * The function fiat_25519_carry_square does stuff. + * The function fiat_25519_carry_square squares a field element and reduces the result. * eval out1 mod m = (eval arg1 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] @@ -422,7 +422,7 @@ static void fiat_25519_carry_square(uint32_t out1[10], const uint32_t arg1[10]) } /* - * The function fiat_25519_carry_scmul_121666 does stuff. + * The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result. * eval out1 mod m = (121666 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] @@ -490,7 +490,7 @@ static void fiat_25519_carry_scmul_121666(uint32_t out1[10], const uint32_t arg1 } /* - * The function fiat_25519_carry does stuff. + * The function fiat_25519_carry reduces a field element. * eval out1 mod m = eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] @@ -533,7 +533,7 @@ static void fiat_25519_carry(uint32_t out1[10], const uint32_t arg1[10]) { } /* - * The function fiat_25519_add does stuff. + * The function fiat_25519_add adds two field elements. * eval out1 mod m = (eval arg1 + eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] @@ -565,7 +565,7 @@ static void fiat_25519_add(uint32_t out1[10], const uint32_t arg1[10], const uin } /* - * The function fiat_25519_sub does stuff. + * The function fiat_25519_sub subtracts two field elements. * eval out1 mod m = (eval arg1 - eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] @@ -597,7 +597,7 @@ static void fiat_25519_sub(uint32_t out1[10], const uint32_t arg1[10], const uin } /* - * The function fiat_25519_opp does stuff. + * The function fiat_25519_opp negates a field element. * eval out1 mod m = -eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] @@ -671,7 +671,7 @@ static void fiat_25519_selectznz(uint32_t out1[10], fiat_25519_uint1 arg1, const } /* - * The function fiat_25519_to_bytes does stuff. + * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order. * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] @@ -853,7 +853,7 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { } /* - * The function fiat_25519_from_bytes does stuff. + * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order. * eval out1 mod m = bytes_eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]] diff --git a/curve25519_64.c b/curve25519_64.c index 5b350177b..fef38dfa5 100644 --- a/curve25519_64.c +++ b/curve25519_64.c @@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_25519_uint128; /* - * The function fiat_25519_addcarryx_u51 is an add with carry. + * The function fiat_25519_addcarryx_u51 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^51 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fia } /* - * The function fiat_25519_subborrowx_u51 is a sub with borrow. + * The function fiat_25519_subborrowx_u51 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^51 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋ * Input Bounds: @@ -74,7 +74,7 @@ static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64 } /* - * The function fiat_25519_carry_mul does stuff. + * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. * eval out1 mod m = (eval arg1 * eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] @@ -143,7 +143,7 @@ static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const } /* - * The function fiat_25519_carry_square does stuff. + * The function fiat_25519_carry_square squares a field element and reduces the result. * eval out1 mod m = (eval arg1 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] @@ -209,7 +209,7 @@ static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) { } /* - * The function fiat_25519_carry_scmul_121666 does stuff. + * The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result. * eval out1 mod m = (121666 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] @@ -252,7 +252,7 @@ static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[ } /* - * The function fiat_25519_carry does stuff. + * The function fiat_25519_carry reduces a field element. * eval out1 mod m = eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] @@ -280,7 +280,7 @@ static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) { } /* - * The function fiat_25519_add does stuff. + * The function fiat_25519_add adds two field elements. * eval out1 mod m = (eval arg1 + eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] @@ -302,7 +302,7 @@ static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint6 } /* - * The function fiat_25519_sub does stuff. + * The function fiat_25519_sub subtracts two field elements. * eval out1 mod m = (eval arg1 - eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] @@ -324,7 +324,7 @@ static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint6 } /* - * The function fiat_25519_opp does stuff. + * The function fiat_25519_opp negates a field element. * eval out1 mod m = -eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] @@ -373,7 +373,7 @@ static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const } /* - * The function fiat_25519_to_bytes does stuff. + * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order. * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] @@ -518,7 +518,7 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) { } /* - * The function fiat_25519_from_bytes does stuff. + * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order. * eval out1 mod m = bytes_eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]] diff --git a/p224_32.c b/p224_32.c index 438ad8c55..2cae5b631 100644 --- a/p224_32.c +++ b/p224_32.c @@ -17,7 +17,7 @@ typedef signed char fiat_p224_int1; /* - * The function fiat_p224_addcarryx_u32 is an add with carry. + * The function fiat_p224_addcarryx_u32 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^32 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_ } /* - * The function fiat_p224_subborrowx_u32 is a sub with borrow. + * The function fiat_p224_subborrowx_u32 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^32 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: @@ -93,7 +93,7 @@ static void fiat_p224_cmovznz_u32(uint32_t* out1, fiat_p224_uint1 arg1, uint32_t } /* - * The function fiat_p224_mul does stuff. + * The function fiat_p224_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m @@ -977,7 +977,7 @@ static void fiat_p224_mul(uint32_t out1[7], const uint32_t arg1[7], const uint32 } /* - * The function fiat_p224_square does stuff. + * The function fiat_p224_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] @@ -1859,7 +1859,7 @@ static void fiat_p224_square(uint32_t out1[7], const uint32_t arg1[7]) { } /* - * The function fiat_p224_add does stuff. + * The function fiat_p224_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m @@ -1941,7 +1941,7 @@ static void fiat_p224_add(uint32_t out1[7], const uint32_t arg1[7], const uint32 } /* - * The function fiat_p224_sub does stuff. + * The function fiat_p224_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m @@ -2008,7 +2008,7 @@ static void fiat_p224_sub(uint32_t out1[7], const uint32_t arg1[7], const uint32 } /* - * The function fiat_p224_opp does stuff. + * The function fiat_p224_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] @@ -2073,9 +2073,9 @@ static void fiat_p224_opp(uint32_t out1[7], const uint32_t arg1[7]) { } /* - * The function fiat_p224_from_montgomery does stuff. + * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 26959946660873538059280334323183841250350249843942399443119741337601^7) mod m + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -2613,7 +2613,7 @@ static void fiat_p224_from_montgomery(uint32_t out1[7], const uint32_t arg1[7]) } /* - * The function fiat_p224_nonzero does stuff. + * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -2661,7 +2661,7 @@ static void fiat_p224_selectznz(uint32_t out1[7], fiat_p224_uint1 arg1, const ui } /* - * The function fiat_p224_to_bytes does stuff. + * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27] * Input Bounds: @@ -2756,7 +2756,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) { } /* - * The function fiat_p224_from_bytes does stuff. + * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] diff --git a/p224_64.c b/p224_64.c index 5c0f3fb9b..c2cba2768 100644 --- a/p224_64.c +++ b/p224_64.c @@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p224_uint128; /* - * The function fiat_p224_addcarryx_u64 is an add with carry. + * The function fiat_p224_addcarryx_u64 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^64 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: @@ -39,7 +39,7 @@ static void fiat_p224_addcarryx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_ } /* - * The function fiat_p224_subborrowx_u64 is a sub with borrow. + * The function fiat_p224_subborrowx_u64 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^64 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: @@ -95,7 +95,7 @@ static void fiat_p224_cmovznz_u64(uint64_t* out1, fiat_p224_uint1 arg1, uint64_t } /* - * The function fiat_p224_mul does stuff. + * The function fiat_p224_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m @@ -439,7 +439,7 @@ static void fiat_p224_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* - * The function fiat_p224_square does stuff. + * The function fiat_p224_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] @@ -781,7 +781,7 @@ static void fiat_p224_square(uint64_t out1[4], const uint64_t arg1[4]) { } /* - * The function fiat_p224_add does stuff. + * The function fiat_p224_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m @@ -836,7 +836,7 @@ static void fiat_p224_add(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* - * The function fiat_p224_sub does stuff. + * The function fiat_p224_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m @@ -882,7 +882,7 @@ static void fiat_p224_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* - * The function fiat_p224_opp does stuff. + * The function fiat_p224_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] @@ -926,9 +926,9 @@ static void fiat_p224_opp(uint64_t out1[4], const uint64_t arg1[4]) { } /* - * The function fiat_p224_from_montgomery does stuff. + * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 26959946667150639793205513449688727755354231427310025123858428723201^4) mod m + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -1148,7 +1148,7 @@ static void fiat_p224_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) } /* - * The function fiat_p224_nonzero does stuff. + * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -1187,7 +1187,7 @@ static void fiat_p224_selectznz(uint64_t out1[4], fiat_p224_uint1 arg1, const ui } /* - * The function fiat_p224_to_bytes does stuff. + * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: @@ -1287,7 +1287,7 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { } /* - * The function fiat_p224_from_bytes does stuff. + * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] diff --git a/p256_32.c b/p256_32.c index ef038ddfa..27c1983df 100644 --- a/p256_32.c +++ b/p256_32.c @@ -17,7 +17,7 @@ typedef signed char fiat_p256_int1; /* - * The function fiat_p256_addcarryx_u32 is an add with carry. + * The function fiat_p256_addcarryx_u32 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^32 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_ } /* - * The function fiat_p256_subborrowx_u32 is a sub with borrow. + * The function fiat_p256_subborrowx_u32 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^32 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: @@ -93,7 +93,7 @@ static void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t } /* - * The function fiat_p256_mul does stuff. + * The function fiat_p256_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m @@ -1149,7 +1149,7 @@ static void fiat_p256_mul(uint32_t out1[8], const uint32_t arg1[8], const uint32 } /* - * The function fiat_p256_square does stuff. + * The function fiat_p256_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] @@ -2203,7 +2203,7 @@ static void fiat_p256_square(uint32_t out1[8], const uint32_t arg1[8]) { } /* - * The function fiat_p256_add does stuff. + * The function fiat_p256_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m @@ -2294,7 +2294,7 @@ static void fiat_p256_add(uint32_t out1[8], const uint32_t arg1[8], const uint32 } /* - * The function fiat_p256_sub does stuff. + * The function fiat_p256_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m @@ -2368,7 +2368,7 @@ static void fiat_p256_sub(uint32_t out1[8], const uint32_t arg1[8], const uint32 } /* - * The function fiat_p256_opp does stuff. + * The function fiat_p256_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] @@ -2440,9 +2440,9 @@ static void fiat_p256_opp(uint32_t out1[8], const uint32_t arg1[8]) { } /* - * The function fiat_p256_from_montgomery does stuff. + * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 26959946660873538060741835960514744168633162839172946800369217830912^8) mod m + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -3049,7 +3049,7 @@ static void fiat_p256_from_montgomery(uint32_t out1[8], const uint32_t arg1[8]) } /* - * The function fiat_p256_nonzero does stuff. + * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -3100,7 +3100,7 @@ static void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const ui } /* - * The function fiat_p256_to_bytes does stuff. + * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: @@ -3207,7 +3207,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { } /* - * The function fiat_p256_from_bytes does stuff. + * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] diff --git a/p256_64.c b/p256_64.c index 46f7835a8..6961f5433 100644 --- a/p256_64.c +++ b/p256_64.c @@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p256_uint128; /* - * The function fiat_p256_addcarryx_u64 is an add with carry. + * The function fiat_p256_addcarryx_u64 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^64 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: @@ -39,7 +39,7 @@ static void fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_ } /* - * The function fiat_p256_subborrowx_u64 is a sub with borrow. + * The function fiat_p256_subborrowx_u64 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^64 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: @@ -95,7 +95,7 @@ static void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t } /* - * The function fiat_p256_mul does stuff. + * The function fiat_p256_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m @@ -415,7 +415,7 @@ static void fiat_p256_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* - * The function fiat_p256_square does stuff. + * The function fiat_p256_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] @@ -733,7 +733,7 @@ static void fiat_p256_square(uint64_t out1[4], const uint64_t arg1[4]) { } /* - * The function fiat_p256_add does stuff. + * The function fiat_p256_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m @@ -788,7 +788,7 @@ static void fiat_p256_add(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* - * The function fiat_p256_sub does stuff. + * The function fiat_p256_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m @@ -834,7 +834,7 @@ static void fiat_p256_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* - * The function fiat_p256_opp does stuff. + * The function fiat_p256_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] @@ -878,9 +878,9 @@ static void fiat_p256_opp(uint64_t out1[4], const uint64_t arg1[4]) { } /* - * The function fiat_p256_from_montgomery does stuff. + * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 6277101733925179126845168871924920046849447032244165148672^4) mod m + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -1064,7 +1064,7 @@ static void fiat_p256_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) } /* - * The function fiat_p256_nonzero does stuff. + * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -1103,7 +1103,7 @@ static void fiat_p256_selectznz(uint64_t out1[4], fiat_p256_uint1 arg1, const ui } /* - * The function fiat_p256_to_bytes does stuff. + * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: @@ -1210,7 +1210,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { } /* - * The function fiat_p256_from_bytes does stuff. + * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] diff --git a/p384_32.c b/p384_32.c index 7a9235c2a..90ad22621 100644 --- a/p384_32.c +++ b/p384_32.c @@ -17,7 +17,7 @@ typedef signed char fiat_p384_int1; /* - * The function fiat_p384_addcarryx_u32 is an add with carry. + * The function fiat_p384_addcarryx_u32 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^32 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_p384_addcarryx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_ } /* - * The function fiat_p384_subborrowx_u32 is a sub with borrow. + * The function fiat_p384_subborrowx_u32 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^32 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: @@ -93,7 +93,7 @@ static void fiat_p384_cmovznz_u32(uint32_t* out1, fiat_p384_uint1 arg1, uint32_t } /* - * The function fiat_p384_mul does stuff. + * The function fiat_p384_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m @@ -2677,7 +2677,7 @@ static void fiat_p384_mul(uint32_t out1[12], const uint32_t arg1[12], const uint } /* - * The function fiat_p384_square does stuff. + * The function fiat_p384_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] @@ -5259,7 +5259,7 @@ static void fiat_p384_square(uint32_t out1[12], const uint32_t arg1[12]) { } /* - * The function fiat_p384_add does stuff. + * The function fiat_p384_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m @@ -5386,7 +5386,7 @@ static void fiat_p384_add(uint32_t out1[12], const uint32_t arg1[12], const uint } /* - * The function fiat_p384_sub does stuff. + * The function fiat_p384_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m @@ -5488,7 +5488,7 @@ static void fiat_p384_sub(uint32_t out1[12], const uint32_t arg1[12], const uint } /* - * The function fiat_p384_opp does stuff. + * The function fiat_p384_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] @@ -5588,9 +5588,9 @@ static void fiat_p384_opp(uint32_t out1[12], const uint32_t arg1[12]) { } /* - * The function fiat_p384_from_montgomery does stuff. + * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 9173994463960286046443283581208347763186259956673124494950355357547691504353860004117541501358835492716545^12) mod m + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^12) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -7226,7 +7226,7 @@ static void fiat_p384_from_montgomery(uint32_t out1[12], const uint32_t arg1[12] } /* - * The function fiat_p384_nonzero does stuff. + * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -7289,7 +7289,7 @@ static void fiat_p384_selectznz(uint32_t out1[12], fiat_p384_uint1 arg1, const u } /* - * The function fiat_p384_to_bytes does stuff. + * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] * Input Bounds: @@ -7444,7 +7444,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) { } /* - * The function fiat_p384_from_bytes does stuff. + * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] diff --git a/p384_64.c b/p384_64.c index ad116b2c7..d3585876a 100644 --- a/p384_64.c +++ b/p384_64.c @@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p384_uint128; /* - * The function fiat_p384_addcarryx_u64 is an add with carry. + * The function fiat_p384_addcarryx_u64 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^64 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: @@ -39,7 +39,7 @@ static void fiat_p384_addcarryx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_ } /* - * The function fiat_p384_subborrowx_u64 is a sub with borrow. + * The function fiat_p384_subborrowx_u64 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^64 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: @@ -95,7 +95,7 @@ static void fiat_p384_cmovznz_u64(uint64_t* out1, fiat_p384_uint1 arg1, uint64_t } /* - * The function fiat_p384_mul does stuff. + * The function fiat_p384_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m @@ -855,7 +855,7 @@ static void fiat_p384_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64 } /* - * The function fiat_p384_square does stuff. + * The function fiat_p384_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] @@ -1613,7 +1613,7 @@ static void fiat_p384_square(uint64_t out1[6], const uint64_t arg1[6]) { } /* - * The function fiat_p384_add does stuff. + * The function fiat_p384_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m @@ -1686,7 +1686,7 @@ static void fiat_p384_add(uint64_t out1[6], const uint64_t arg1[6], const uint64 } /* - * The function fiat_p384_sub does stuff. + * The function fiat_p384_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m @@ -1746,7 +1746,7 @@ static void fiat_p384_sub(uint64_t out1[6], const uint64_t arg1[6], const uint64 } /* - * The function fiat_p384_opp does stuff. + * The function fiat_p384_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] @@ -1804,9 +1804,9 @@ static void fiat_p384_opp(uint64_t out1[6], const uint64_t arg1[6]) { } /* - * The function fiat_p384_from_montgomery does stuff. + * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 9173994466096273082364193663603369469355812071275829017307008127494733112176079729898163604637719575134209^6) mod m + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -2341,7 +2341,7 @@ static void fiat_p384_from_montgomery(uint64_t out1[6], const uint64_t arg1[6]) } /* - * The function fiat_p384_nonzero does stuff. + * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -2386,7 +2386,7 @@ static void fiat_p384_selectznz(uint64_t out1[6], fiat_p384_uint1 arg1, const ui } /* - * The function fiat_p384_to_bytes does stuff. + * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] * Input Bounds: @@ -2541,7 +2541,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) { } /* - * The function fiat_p384_from_bytes does stuff. + * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] diff --git a/p448_solinas_64.c b/p448_solinas_64.c index edf5fceb4..16dbbfe89 100644 --- a/p448_solinas_64.c +++ b/p448_solinas_64.c @@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_p448_uint128; /* - * The function fiat_p448_addcarryx_u56 is an add with carry. + * The function fiat_p448_addcarryx_u56 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^56 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^56⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_p448_addcarryx_u56(uint64_t* out1, fiat_p448_uint1* out2, fiat_ } /* - * The function fiat_p448_subborrowx_u56 is a sub with borrow. + * The function fiat_p448_subborrowx_u56 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^56 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^56⌋ * Input Bounds: @@ -74,7 +74,7 @@ static void fiat_p448_cmovznz_u64(uint64_t* out1, fiat_p448_uint1 arg1, uint64_t } /* - * The function fiat_p448_carry_mul does stuff. + * The function fiat_p448_carry_mul multiplies two field elements and reduces the result. * eval out1 mod m = (eval arg1 * eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]] @@ -238,7 +238,7 @@ static void fiat_p448_carry_mul(uint64_t out1[8], const uint64_t arg1[8], const } /* - * The function fiat_p448_carry_square does stuff. + * The function fiat_p448_carry_square squares a field element and reduces the result. * eval out1 mod m = (eval arg1 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]] @@ -380,7 +380,7 @@ static void fiat_p448_carry_square(uint64_t out1[8], const uint64_t arg1[8]) { } /* - * The function fiat_p448_carry does stuff. + * The function fiat_p448_carry reduces a field element. * eval out1 mod m = eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]] @@ -421,7 +421,7 @@ static void fiat_p448_carry(uint64_t out1[8], const uint64_t arg1[8]) { } /* - * The function fiat_p448_add does stuff. + * The function fiat_p448_add adds two field elements. * eval out1 mod m = (eval arg1 + eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]] @@ -449,7 +449,7 @@ static void fiat_p448_add(uint64_t out1[8], const uint64_t arg1[8], const uint64 } /* - * The function fiat_p448_sub does stuff. + * The function fiat_p448_sub subtracts two field elements. * eval out1 mod m = (eval arg1 - eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]] @@ -477,7 +477,7 @@ static void fiat_p448_sub(uint64_t out1[8], const uint64_t arg1[8], const uint64 } /* - * The function fiat_p448_opp does stuff. + * The function fiat_p448_opp negates a field element. * eval out1 mod m = -eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]] @@ -541,7 +541,7 @@ static void fiat_p448_selectznz(uint64_t out1[8], fiat_p448_uint1 arg1, const ui } /* - * The function fiat_p448_to_bytes does stuff. + * The function fiat_p448_to_bytes serializes a field element to bytes in little-endian order. * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] * Input Bounds: * arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]] @@ -761,7 +761,7 @@ static void fiat_p448_to_bytes(uint8_t out1[56], const uint64_t arg1[8]) { } /* - * The function fiat_p448_from_bytes does stuff. + * The function fiat_p448_from_bytes deserializes a field element from bytes in little-endian order. * eval out1 mod m = bytes_eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]] diff --git a/p484_64.c b/p484_64.c index 43aec500c..41c1a0c90 100644 --- a/p484_64.c +++ b/p484_64.c @@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p484_uint128; /* - * The function fiat_p484_addcarryx_u64 is an add with carry. + * The function fiat_p484_addcarryx_u64 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^64 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: @@ -39,7 +39,7 @@ static void fiat_p484_addcarryx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_ } /* - * The function fiat_p484_subborrowx_u64 is a sub with borrow. + * The function fiat_p484_subborrowx_u64 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^64 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: @@ -95,7 +95,7 @@ static void fiat_p484_cmovznz_u64(uint64_t* out1, fiat_p484_uint1 arg1, uint64_t } /* - * The function fiat_p484_mul does stuff. + * The function fiat_p484_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg2)) mod m @@ -1084,7 +1084,7 @@ static void fiat_p484_mul(uint64_t out1[7], const uint64_t arg1[7], const uint64 } /* - * The function fiat_p484_square does stuff. + * The function fiat_p484_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] @@ -2071,7 +2071,7 @@ static void fiat_p484_square(uint64_t out1[7], const uint64_t arg1[7]) { } /* - * The function fiat_p484_add does stuff. + * The function fiat_p484_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) + eval (fiat_p484_from_montgomery arg2)) mod m @@ -2153,7 +2153,7 @@ static void fiat_p484_add(uint64_t out1[7], const uint64_t arg1[7], const uint64 } /* - * The function fiat_p484_sub does stuff. + * The function fiat_p484_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) - eval (fiat_p484_from_montgomery arg2)) mod m @@ -2220,7 +2220,7 @@ static void fiat_p484_sub(uint64_t out1[7], const uint64_t arg1[7], const uint64 } /* - * The function fiat_p484_opp does stuff. + * The function fiat_p484_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * eval (fiat_p484_from_montgomery out1) mod m = -eval (fiat_p484_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] @@ -2285,9 +2285,9 @@ static void fiat_p484_opp(uint64_t out1[7], const uint64_t arg1[7]) { } /* - * The function fiat_p484_from_montgomery does stuff. + * The function fiat_p484_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 1324863811396206510028543369708678912454650048974215908631025180695212704414528066624039943565284982500305666048^7) mod m + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^7) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -2933,7 +2933,7 @@ static void fiat_p484_from_montgomery(uint64_t out1[7], const uint64_t arg1[7]) } /* - * The function fiat_p484_nonzero does stuff. + * The function fiat_p484_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_p484_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -2981,7 +2981,7 @@ static void fiat_p484_selectznz(uint64_t out1[7], fiat_p484_uint1 arg1, const ui } /* - * The function fiat_p484_to_bytes does stuff. + * The function fiat_p484_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] * Input Bounds: @@ -3159,7 +3159,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) { } /* - * The function fiat_p484_from_bytes does stuff. + * The function fiat_p484_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] diff --git a/p521_32.c b/p521_32.c index 3998e1016..9d7fc2515 100644 --- a/p521_32.c +++ b/p521_32.c @@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_p521_uint128; /* - * The function fiat_p521_addcarryx_u30 is an add with carry. + * The function fiat_p521_addcarryx_u30 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^30 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^30⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_p521_addcarryx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_ } /* - * The function fiat_p521_subborrowx_u30 is a sub with borrow. + * The function fiat_p521_subborrowx_u30 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^30 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^30⌋ * Input Bounds: @@ -57,7 +57,7 @@ static void fiat_p521_subborrowx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat } /* - * The function fiat_p521_addcarryx_u31 is an add with carry. + * The function fiat_p521_addcarryx_u31 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^31 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^31⌋ * Input Bounds: @@ -77,7 +77,7 @@ static void fiat_p521_addcarryx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat_ } /* - * The function fiat_p521_subborrowx_u31 is a sub with borrow. + * The function fiat_p521_subborrowx_u31 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^31 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^31⌋ * Input Bounds: @@ -114,7 +114,7 @@ static void fiat_p521_cmovznz_u32(uint32_t* out1, fiat_p521_uint1 arg1, uint32_t } /* - * The function fiat_p521_carry_mul does stuff. + * The function fiat_p521_carry_mul multiplies two field elements and reduces the result. * eval out1 mod m = (eval arg1 * eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332]] @@ -506,7 +506,7 @@ static void fiat_p521_carry_mul(uint32_t out1[17], const uint64_t arg1[17], cons } /* - * The function fiat_p521_carry_square does stuff. + * The function fiat_p521_carry_square squares a field element and reduces the result. * eval out1 mod m = (eval arg1 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332]] @@ -793,7 +793,7 @@ static void fiat_p521_carry_square(uint32_t out1[17], const uint64_t arg1[17]) { } /* - * The function fiat_p521_carry does stuff. + * The function fiat_p521_carry reduces a field element. * eval out1 mod m = eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332]] @@ -857,7 +857,7 @@ static void fiat_p521_carry(uint32_t out1[17], const uint64_t arg1[17]) { } /* - * The function fiat_p521_add does stuff. + * The function fiat_p521_add adds two field elements. * eval out1 mod m = (eval arg1 + eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]] @@ -903,7 +903,7 @@ static void fiat_p521_add(uint64_t out1[17], const uint32_t arg1[17], const uint } /* - * The function fiat_p521_sub does stuff. + * The function fiat_p521_sub subtracts two field elements. * eval out1 mod m = (eval arg1 - eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]] @@ -949,7 +949,7 @@ static void fiat_p521_sub(uint64_t out1[17], const uint32_t arg1[17], const uint } /* - * The function fiat_p521_opp does stuff. + * The function fiat_p521_opp negates a field element. * eval out1 mod m = -eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]] @@ -1058,7 +1058,7 @@ static void fiat_p521_selectznz(uint32_t out1[17], fiat_p521_uint1 arg1, const u } /* - * The function fiat_p521_to_bytes does stuff. + * The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order. * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..65] * Input Bounds: * arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]] @@ -1395,7 +1395,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) { } /* - * The function fiat_p521_from_bytes does stuff. + * The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order. * eval out1 mod m = bytes_eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] diff --git a/p521_64.c b/p521_64.c index 595abcba0..6eeab0b58 100644 --- a/p521_64.c +++ b/p521_64.c @@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_p521_uint128; /* - * The function fiat_p521_addcarryx_u58 is an add with carry. + * The function fiat_p521_addcarryx_u58 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^58 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_p521_addcarryx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_ } /* - * The function fiat_p521_subborrowx_u58 is a sub with borrow. + * The function fiat_p521_subborrowx_u58 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^58 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋ * Input Bounds: @@ -57,7 +57,7 @@ static void fiat_p521_subborrowx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat } /* - * The function fiat_p521_addcarryx_u57 is an add with carry. + * The function fiat_p521_addcarryx_u57 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^57 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋ * Input Bounds: @@ -77,7 +77,7 @@ static void fiat_p521_addcarryx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_ } /* - * The function fiat_p521_subborrowx_u57 is a sub with borrow. + * The function fiat_p521_subborrowx_u57 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^57 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋ * Input Bounds: @@ -114,7 +114,7 @@ static void fiat_p521_cmovznz_u64(uint64_t* out1, fiat_p521_uint1 arg1, uint64_t } /* - * The function fiat_p521_carry_mul does stuff. + * The function fiat_p521_carry_mul multiplies two field elements and reduces the result. * eval out1 mod m = (eval arg1 * eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0x699999999999999]] @@ -258,7 +258,7 @@ static void fiat_p521_carry_mul(uint64_t out1[9], const uint64_t arg1[9], const } /* - * The function fiat_p521_carry_square does stuff. + * The function fiat_p521_carry_square squares a field element and reduces the result. * eval out1 mod m = (eval arg1 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0x699999999999999]] @@ -381,7 +381,7 @@ static void fiat_p521_carry_square(uint64_t out1[9], const uint64_t arg1[9]) { } /* - * The function fiat_p521_carry does stuff. + * The function fiat_p521_carry reduces a field element. * eval out1 mod m = eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0x699999999999999]] @@ -421,7 +421,7 @@ static void fiat_p521_carry(uint64_t out1[9], const uint64_t arg1[9]) { } /* - * The function fiat_p521_add does stuff. + * The function fiat_p521_add adds two field elements. * eval out1 mod m = (eval arg1 + eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]] @@ -451,7 +451,7 @@ static void fiat_p521_add(uint64_t out1[9], const uint64_t arg1[9], const uint64 } /* - * The function fiat_p521_sub does stuff. + * The function fiat_p521_sub subtracts two field elements. * eval out1 mod m = (eval arg1 - eval arg2) mod m * Input Bounds: * arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]] @@ -481,7 +481,7 @@ static void fiat_p521_sub(uint64_t out1[9], const uint64_t arg1[9], const uint64 } /* - * The function fiat_p521_opp does stuff. + * The function fiat_p521_opp negates a field element. * eval out1 mod m = -eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]] @@ -550,7 +550,7 @@ static void fiat_p521_selectznz(uint64_t out1[9], fiat_p521_uint1 arg1, const ui } /* - * The function fiat_p521_to_bytes does stuff. + * The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order. * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..65] * Input Bounds: * arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]] @@ -823,7 +823,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { } /* - * The function fiat_p521_from_bytes does stuff. + * The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order. * eval out1 mod m = bytes_eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] diff --git a/secp256k1_32.c b/secp256k1_32.c index 19469b433..4ded0f935 100644 --- a/secp256k1_32.c +++ b/secp256k1_32.c @@ -17,7 +17,7 @@ typedef signed char fiat_secp256k1_int1; /* - * The function fiat_secp256k1_addcarryx_u32 is an add with carry. + * The function fiat_secp256k1_addcarryx_u32 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^32 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: @@ -37,7 +37,7 @@ static void fiat_secp256k1_addcarryx_u32(uint32_t* out1, fiat_secp256k1_uint1* o } /* - * The function fiat_secp256k1_subborrowx_u32 is a sub with borrow. + * The function fiat_secp256k1_subborrowx_u32 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^32 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: @@ -93,7 +93,7 @@ static void fiat_secp256k1_cmovznz_u32(uint32_t* out1, fiat_secp256k1_uint1 arg1 } /* - * The function fiat_secp256k1_mul does stuff. + * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m @@ -1389,7 +1389,7 @@ static void fiat_secp256k1_mul(uint32_t out1[8], const uint32_t arg1[8], const u } /* - * The function fiat_secp256k1_square does stuff. + * The function fiat_secp256k1_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] @@ -2683,7 +2683,7 @@ static void fiat_secp256k1_square(uint32_t out1[8], const uint32_t arg1[8]) { } /* - * The function fiat_secp256k1_add does stuff. + * The function fiat_secp256k1_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m @@ -2774,7 +2774,7 @@ static void fiat_secp256k1_add(uint32_t out1[8], const uint32_t arg1[8], const u } /* - * The function fiat_secp256k1_sub does stuff. + * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m @@ -2848,7 +2848,7 @@ static void fiat_secp256k1_sub(uint32_t out1[8], const uint32_t arg1[8], const u } /* - * The function fiat_secp256k1_opp does stuff. + * The function fiat_secp256k1_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] @@ -2920,9 +2920,9 @@ static void fiat_secp256k1_opp(uint32_t out1[8], const uint32_t arg1[8]) { } /* - * The function fiat_secp256k1_from_montgomery does stuff. + * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 95051438657476508368854739628211227342282034117213274825043523998796304009133^8) mod m + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -3823,7 +3823,7 @@ static void fiat_secp256k1_from_montgomery(uint32_t out1[8], const uint32_t arg1 } /* - * The function fiat_secp256k1_nonzero does stuff. + * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -3874,7 +3874,7 @@ static void fiat_secp256k1_selectznz(uint32_t out1[8], fiat_secp256k1_uint1 arg1 } /* - * The function fiat_secp256k1_to_bytes does stuff. + * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: @@ -3981,7 +3981,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { } /* - * The function fiat_secp256k1_from_bytes does stuff. + * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] diff --git a/secp256k1_64.c b/secp256k1_64.c index 3dc5beeab..b1437e2dc 100644 --- a/secp256k1_64.c +++ b/secp256k1_64.c @@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_secp256k1_uint128; /* - * The function fiat_secp256k1_addcarryx_u64 is an add with carry. + * The function fiat_secp256k1_addcarryx_u64 is an addition with carry. * out1 = (arg1 + arg2 + arg3) mod 2^64 * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: @@ -39,7 +39,7 @@ static void fiat_secp256k1_addcarryx_u64(uint64_t* out1, fiat_secp256k1_uint1* o } /* - * The function fiat_secp256k1_subborrowx_u64 is a sub with borrow. + * The function fiat_secp256k1_subborrowx_u64 is a subtraction with borrow. * out1 = (-arg1 + arg2 + -arg3) mod 2^64 * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: @@ -95,7 +95,7 @@ static void fiat_secp256k1_cmovznz_u64(uint64_t* out1, fiat_secp256k1_uint1 arg1 } /* - * The function fiat_secp256k1_mul does stuff. + * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m @@ -463,7 +463,7 @@ static void fiat_secp256k1_mul(uint64_t out1[4], const uint64_t arg1[4], const u } /* - * The function fiat_secp256k1_square does stuff. + * The function fiat_secp256k1_square squares a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] @@ -829,7 +829,7 @@ static void fiat_secp256k1_square(uint64_t out1[4], const uint64_t arg1[4]) { } /* - * The function fiat_secp256k1_add does stuff. + * The function fiat_secp256k1_add adds two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m @@ -884,7 +884,7 @@ static void fiat_secp256k1_add(uint64_t out1[4], const uint64_t arg1[4], const u } /* - * The function fiat_secp256k1_sub does stuff. + * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m @@ -930,7 +930,7 @@ static void fiat_secp256k1_sub(uint64_t out1[4], const uint64_t arg1[4], const u } /* - * The function fiat_secp256k1_opp does stuff. + * The function fiat_secp256k1_opp negates a field element in the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] @@ -974,9 +974,9 @@ static void fiat_secp256k1_opp(uint64_t out1[4], const uint64_t arg1[4]) { } /* - * The function fiat_secp256k1_from_montgomery does stuff. + * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * 97798581649299591516383885342152904135335272353249846763749256112567415731113^4) mod m + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] * ∧ 0 ≤ eval out1 < m * Input Bounds: @@ -1241,7 +1241,7 @@ static void fiat_secp256k1_from_montgomery(uint64_t out1[4], const uint64_t arg1 } /* - * The function fiat_secp256k1_nonzero does stuff. + * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0 * Input Bounds: @@ -1280,7 +1280,7 @@ static void fiat_secp256k1_selectznz(uint64_t out1[4], fiat_secp256k1_uint1 arg1 } /* - * The function fiat_secp256k1_to_bytes does stuff. + * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: @@ -1387,7 +1387,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { } /* - * The function fiat_secp256k1_from_bytes does stuff. + * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → * eval out1 mod m = bytes_eval arg1 mod m * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index e45940369..ee2793c40 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -660,7 +660,7 @@ Section __. prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s) (stringify_correctness evalf - (fun fname : string => ["The function " ++ fname ++ " is an add with carry."]%string) + (fun fname : string => ["The function " ++ fname ++ " is an addition with carry."]%string) (addcarryx_correct s)). Definition subborrowx (s : Z) @@ -680,7 +680,7 @@ Section __. prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s) (stringify_correctness evalf - (fun fname : string => ["The function " ++ fname ++ " is a sub with borrow."]%string) + (fun fname : string => ["The function " ++ fname ++ " is a subtraction with borrow."]%string) (subborrowx_correct s)). diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 7ff799c80..2549d190a 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -162,7 +162,7 @@ Section __. FromPipelineToString prefix "mul" mul (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string) (mul_correct weightf n m boundsn)). Local Ltac solve_extra_bounds_side_conditions := diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index 75e430a24..9730eb5e4 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -285,7 +285,7 @@ else: FromPipelineToString prefix "carry_mul" carry_mul (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements and reduces the result."]%string) (carry_mul_correct weightf n m tight_bounds loose_bounds)). Definition carry_square @@ -304,7 +304,7 @@ else: FromPipelineToString prefix "carry_square" carry_square (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " squares a field element and reduces the result."]%string) (carry_square_correct weightf n m tight_bounds loose_bounds)). Definition carry_scmul_const (x : Z) @@ -323,7 +323,7 @@ else: FromPipelineToString prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x) (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " multiplies a field element by " ++ decimal_string_of_Z x ++ " and reduces the result."]%string) (carry_scmul_const_correct weightf n m tight_bounds loose_bounds x)). Definition carry @@ -342,7 +342,7 @@ else: FromPipelineToString prefix "carry" carry (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " reduces a field element."]%string) (carry_correct weightf n m tight_bounds loose_bounds)). Definition add @@ -361,7 +361,7 @@ else: FromPipelineToString prefix "add" add (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " adds two field elements."]%string) (add_correct weightf n m tight_bounds loose_bounds)). Definition sub @@ -380,7 +380,7 @@ else: FromPipelineToString prefix "sub" sub (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " subtracts two field elements."]%string) (sub_correct weightf n m tight_bounds loose_bounds)). Definition opp @@ -399,7 +399,7 @@ else: FromPipelineToString prefix "opp" opp (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " negates a field element."]%string) (opp_correct weightf n m tight_bounds loose_bounds)). Definition to_bytes @@ -418,7 +418,7 @@ else: FromPipelineToString prefix "to_bytes" to_bytes (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " serializes a field element to bytes in little-endian order."]%string) (to_bytes_correct weightf n n_bytes m tight_bounds)). Definition from_bytes @@ -437,7 +437,7 @@ else: FromPipelineToString prefix "from_bytes" from_bytes (stringify_correctness - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " deserializes a field element from bytes in little-endian order."]%string) (from_bytes_correct weightf n n_bytes m s tight_bounds)). Definition encode @@ -456,7 +456,7 @@ else: FromPipelineToString prefix "encode" encode (stringify_correctness - (fun fname : string => [fname ++ ":"]%string) + (fun fname : string => ["The function " ++ fname ++ " encodes an integer as a field element."]%string) (encode_correct weightf n m tight_bounds)). Definition zero @@ -475,7 +475,7 @@ else: FromPipelineToString prefix "zero" zero (stringify_correctness - (fun fname : string => @nil string) + (fun fname => ["The function " ++ fname ++ " returns the field element zero."]%string) (zero_correct weightf n m tight_bounds)). Definition one @@ -494,7 +494,7 @@ else: FromPipelineToString prefix "one" one (stringify_correctness - (fun fname : string => @nil string) + (fun fname => ["The function " ++ fname ++ " returns the field element one."]%string) (one_correct weightf n m tight_bounds)). Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index f64e4a8c3..46ffa083f 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -233,10 +233,12 @@ Section __. := (CorrectnessStringification.dyn_context.cons m "m"%string (CorrectnessStringification.dyn_context.cons - from_montgomery_res (prefix ++ "from_montgomery")%string + r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string (CorrectnessStringification.dyn_context.cons - (@eval 8 n_bytes) "bytes_eval"%string - CorrectnessStringification.dyn_context.nil))). + from_montgomery_res (prefix ++ "from_montgomery")%string + (CorrectnessStringification.dyn_context.cons + (@eval 8 n_bytes) "bytes_eval"%string + CorrectnessStringification.dyn_context.nil)))). Local Notation stringify_correctness prefix pre_extra correctness := (stringify_correctness_with_ctx (initial_ctx prefix) @@ -262,7 +264,7 @@ Section __. prefix "mul" mul (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements in the Montgomery domain."]%string) (mul_correct machine_wordsize n m valid from_montgomery_res)). Definition square @@ -282,7 +284,7 @@ Section __. prefix "square" square (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " squares a field element in the Montgomery domain."]%string) (square_correct machine_wordsize n m valid from_montgomery_res)). Definition add @@ -302,7 +304,7 @@ Section __. prefix "add" add (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " adds two field elements in the Montgomery domain."]%string) (add_correct machine_wordsize n m valid from_montgomery_res)). Definition sub @@ -322,7 +324,7 @@ Section __. prefix "sub" sub (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " subtracts two field elements in the Montgomery domain."]%string) (sub_correct machine_wordsize n m valid from_montgomery_res)). Definition opp @@ -342,7 +344,7 @@ Section __. prefix "opp" opp (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " negates a field element in the Montgomery domain."]%string) (opp_correct machine_wordsize n m valid from_montgomery_res)). Definition from_montgomery @@ -362,7 +364,7 @@ Section __. prefix "from_montgomery" from_montgomery (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " translates a field element out of the Montgomery domain."]%string) (from_montgomery_correct machine_wordsize n m r' valid)). Definition nonzero @@ -381,7 +383,7 @@ Section __. prefix "nonzero" nonzero (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " outputs a single non-zero word if the input is non-zero and zero otherwise."]%string) (nonzero_correct machine_wordsize n m valid from_montgomery_res)). Definition to_bytes @@ -401,7 +403,7 @@ Section __. prefix "to_bytes" to_bytes (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " serializes a field element in the Montgomery domain to bytes in little-endian order."]%string) (to_bytes_correct machine_wordsize n n_bytes m valid)). Definition from_bytes @@ -421,7 +423,7 @@ Section __. prefix "from_bytes" from_bytes (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " deserializes a field element in the Montgomery domain from bytes in little-endian order."]%string) (from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid)). Definition encode @@ -441,7 +443,7 @@ Section __. prefix "encode" encode (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname : string => ["The function " ++ fname ++ " encodes an integer as a field element in the Montgomery domain."]%string) (encode_correct machine_wordsize n m valid from_montgomery_res)). Definition zero @@ -461,7 +463,7 @@ Section __. prefix "zero" zero (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname => ["The function " ++ fname ++ " returns the field element zero in the Montgomery domain."]%string) (zero_correct machine_wordsize n m valid from_montgomery_res)). Definition one @@ -481,7 +483,7 @@ Section __. prefix "one" one (stringify_correctness prefix - (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (fun fname => ["The function " ++ fname ++ " returns the field element one in the Montgomery domain."]%string) (one_correct machine_wordsize n m valid from_montgomery_res)). Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. -- cgit v1.2.3