diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-02-01 18:50:00 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-02 18:22:15 -0500 |
| commit | ce583d76bdb8f15148fc4222d8bdec096547682a (patch) | |
| tree | ffb083673e6be283d7f67ad857bc2f30af892767 | |
| parent | 069e5cce23669707f11e59d9f68a31ad24990fe0 (diff) | |
Use Preconditions: Postconditions:, rather than /\ and ->
| -rw-r--r-- | curve25519_32.c | 68 | ||||
| -rw-r--r-- | curve25519_64.c | 56 | ||||
| -rw-r--r-- | p224_32.c | 109 | ||||
| -rw-r--r-- | p224_64.c | 109 | ||||
| -rw-r--r-- | p256_32.c | 109 | ||||
| -rw-r--r-- | p256_64.c | 109 | ||||
| -rw-r--r-- | p384_32.c | 109 | ||||
| -rw-r--r-- | p384_64.c | 109 | ||||
| -rw-r--r-- | p448_solinas_64.c | 52 | ||||
| -rw-r--r-- | p484_64.c | 109 | ||||
| -rw-r--r-- | p521_32.c | 64 | ||||
| -rw-r--r-- | p521_64.c | 64 | ||||
| -rw-r--r-- | secp256k1_32.c | 109 | ||||
| -rw-r--r-- | secp256k1_64.c | 109 | ||||
| -rw-r--r-- | src/CStringification.v | 2 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 52 |
16 files changed, 916 insertions, 423 deletions
diff --git a/curve25519_32.c b/curve25519_32.c index 76f266afd..4d4565689 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -16,8 +16,10 @@ typedef signed char fiat_25519_int1; /* * The function fiat_25519_addcarryx_u26 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^26 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^26 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffff] @@ -36,8 +38,10 @@ static void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fia /* * The function fiat_25519_subborrowx_u26 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^26 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^26 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffff] @@ -56,8 +60,10 @@ static void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fi /* * The function fiat_25519_addcarryx_u25 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^25 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^25 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffff] @@ -76,8 +82,10 @@ static void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fia /* * The function fiat_25519_subborrowx_u25 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^25 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^25 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffff] @@ -96,7 +104,9 @@ static void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fi /* * The function fiat_25519_cmovznz_u32 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -113,7 +123,9 @@ static void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32 /* * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] @@ -282,7 +294,9 @@ static void fiat_25519_carry_mul(uint32_t out1[10], const uint32_t arg1[10], con /* * The function fiat_25519_carry_square squares a field element and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg1) mod m + * Postconditions: + * 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]] * Output Bounds: @@ -423,7 +437,9 @@ static void fiat_25519_carry_square(uint32_t out1[10], const uint32_t arg1[10]) /* * 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 + * Postconditions: + * 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]] * Output Bounds: @@ -491,7 +507,9 @@ static void fiat_25519_carry_scmul_121666(uint32_t out1[10], const uint32_t arg1 /* * The function fiat_25519_carry reduces a field element. - * eval out1 mod m = eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -534,7 +552,9 @@ static void fiat_25519_carry(uint32_t out1[10], const uint32_t arg1[10]) { /* * The function fiat_25519_add adds two field elements. - * eval out1 mod m = (eval arg1 + eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] @@ -566,7 +586,9 @@ static void fiat_25519_add(uint32_t out1[10], const uint32_t arg1[10], const uin /* * The function fiat_25519_sub subtracts two field elements. - * eval out1 mod m = (eval arg1 - eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] @@ -598,7 +620,9 @@ static void fiat_25519_sub(uint32_t out1[10], const uint32_t arg1[10], const uin /* * The function fiat_25519_opp negates a field element. - * eval out1 mod m = -eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -629,7 +653,9 @@ static void fiat_25519_opp(uint32_t out1[10], const uint32_t arg1[10]) { /* * The function fiat_25519_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -672,7 +698,9 @@ static void fiat_25519_selectznz(uint32_t out1[10], fiat_25519_uint1 arg1, const /* * 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] + * Postconditions: + * 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]] * Output Bounds: @@ -854,7 +882,9 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { /* * 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 + * Postconditions: + * 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]] * Output Bounds: diff --git a/curve25519_64.c b/curve25519_64.c index fef38dfa5..5341181f6 100644 --- a/curve25519_64.c +++ b/curve25519_64.c @@ -18,8 +18,10 @@ typedef unsigned __int128 fiat_25519_uint128; /* * The function fiat_25519_addcarryx_u51 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^51 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^51 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7ffffffffffff] @@ -38,8 +40,10 @@ static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fia /* * The function fiat_25519_subborrowx_u51 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^51 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^51 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7ffffffffffff] @@ -58,7 +62,9 @@ static void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fi /* * The function fiat_25519_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -75,7 +81,9 @@ static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64 /* * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg2) mod m + * Postconditions: + * eval out1 mod m = (eval arg1 * eval arg2) mod m + * * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] * arg2: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] @@ -144,7 +152,9 @@ static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const /* * The function fiat_25519_carry_square squares a field element and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg1) mod m + * Postconditions: + * eval out1 mod m = (eval arg1 * eval arg1) mod m + * * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] * Output Bounds: @@ -210,7 +220,9 @@ static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) { /* * 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 + * Postconditions: + * eval out1 mod m = (121666 * eval arg1) mod m + * * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] * Output Bounds: @@ -253,7 +265,9 @@ static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[ /* * The function fiat_25519_carry reduces a field element. - * eval out1 mod m = eval arg1 mod m + * Postconditions: + * eval out1 mod m = eval arg1 mod m + * * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] * Output Bounds: @@ -281,7 +295,9 @@ static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) { /* * The function fiat_25519_add adds two field elements. - * eval out1 mod m = (eval arg1 + eval arg2) mod m + * Postconditions: + * eval out1 mod m = (eval arg1 + eval arg2) mod m + * * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] * arg2: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] @@ -303,7 +319,9 @@ static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint6 /* * The function fiat_25519_sub subtracts two field elements. - * eval out1 mod m = (eval arg1 - eval arg2) mod m + * Postconditions: + * eval out1 mod m = (eval arg1 - eval arg2) mod m + * * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] * arg2: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] @@ -325,7 +343,9 @@ static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint6 /* * The function fiat_25519_opp negates a field element. - * eval out1 mod m = -eval arg1 mod m + * Postconditions: + * eval out1 mod m = -eval arg1 mod m + * * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] * Output Bounds: @@ -346,7 +366,9 @@ static void fiat_25519_opp(uint64_t out1[5], const uint64_t arg1[5]) { /* * The function fiat_25519_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -374,7 +396,9 @@ static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const /* * 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] + * Postconditions: + * 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]] * Output Bounds: @@ -519,7 +543,9 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) { /* * 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 + * Postconditions: + * 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]] * Output Bounds: @@ -18,8 +18,10 @@ typedef signed char fiat_p224_int1; /* * The function fiat_p224_addcarryx_u32 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^32 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -38,8 +40,10 @@ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_ /* * The function fiat_p224_subborrowx_u32 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^32 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -58,8 +62,10 @@ static void fiat_p224_subborrowx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat /* * The function fiat_p224_mulx_u32 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^32 - * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^32 + * out2 = ⌊arg1 * arg2 / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -77,7 +83,9 @@ static void fiat_p224_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, ui /* * The function fiat_p224_cmovznz_u32 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -94,10 +102,13 @@ static void fiat_p224_cmovznz_u32(uint32_t* out1, fiat_p224_uint1 arg1, uint32_t /* * The function fiat_p224_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -977,9 +988,12 @@ static void fiat_p224_mul(uint32_t out1[7], const uint32_t arg1[7], const uint32 /* * The function fiat_p224_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -1858,10 +1872,13 @@ static void fiat_p224_square(uint32_t out1[7], const uint32_t arg1[7]) { /* * The function fiat_p224_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -1939,10 +1956,13 @@ static void fiat_p224_add(uint32_t out1[7], const uint32_t arg1[7], const uint32 /* * The function fiat_p224_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2005,9 +2025,12 @@ static void fiat_p224_sub(uint32_t out1[7], const uint32_t arg1[7], const uint32 /* * The function fiat_p224_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2069,9 +2092,12 @@ static void fiat_p224_opp(uint32_t out1[7], const uint32_t arg1[7]) { /* * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2608,8 +2634,11 @@ static void fiat_p224_from_montgomery(uint32_t out1[7], const uint32_t arg1[7]) /* * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2622,7 +2651,9 @@ static void fiat_p224_nonzero(uint32_t* out1, const uint32_t arg1[7]) { /* * The function fiat_p224_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2656,8 +2687,11 @@ static void fiat_p224_selectznz(uint32_t out1[7], fiat_p224_uint1 arg1, const ui /* * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..27] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2751,9 +2785,12 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) { /* * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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]] * Output Bounds: @@ -20,8 +20,10 @@ typedef unsigned __int128 fiat_p224_uint128; /* * The function fiat_p224_addcarryx_u64 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^64 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -40,8 +42,10 @@ static void fiat_p224_addcarryx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_ /* * The function fiat_p224_subborrowx_u64 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^64 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -60,8 +64,10 @@ static void fiat_p224_subborrowx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat /* * The function fiat_p224_mulx_u64 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^64 - * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^64 + * out2 = ⌊arg1 * arg2 / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -79,7 +85,9 @@ static void fiat_p224_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui /* * The function fiat_p224_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -96,10 +104,13 @@ static void fiat_p224_cmovznz_u64(uint64_t* out1, fiat_p224_uint1 arg1, uint64_t /* * The function fiat_p224_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -439,9 +450,12 @@ static void fiat_p224_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64 /* * The function fiat_p224_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -780,10 +794,13 @@ static void fiat_p224_square(uint64_t out1[4], const uint64_t arg1[4]) { /* * The function fiat_p224_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -834,10 +851,13 @@ static void fiat_p224_add(uint64_t out1[4], const uint64_t arg1[4], const uint64 /* * The function fiat_p224_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -879,9 +899,12 @@ static void fiat_p224_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64 /* * The function fiat_p224_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -922,9 +945,12 @@ static void fiat_p224_opp(uint64_t out1[4], const uint64_t arg1[4]) { /* * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1143,8 +1169,11 @@ static void fiat_p224_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) /* * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1157,7 +1186,9 @@ static void fiat_p224_nonzero(uint64_t* out1, const uint64_t arg1[4]) { /* * The function fiat_p224_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1182,8 +1213,11 @@ static void fiat_p224_selectznz(uint64_t out1[4], fiat_p224_uint1 arg1, const ui /* * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -1282,9 +1316,12 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { /* * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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 ~> 0x0], [0x0 ~> 0x0], [0x0 ~> 0x0], [0x0 ~> 0x0]] * Output Bounds: @@ -18,8 +18,10 @@ typedef signed char fiat_p256_int1; /* * The function fiat_p256_addcarryx_u32 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^32 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -38,8 +40,10 @@ static void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_ /* * The function fiat_p256_subborrowx_u32 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^32 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -58,8 +62,10 @@ static void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat /* * The function fiat_p256_mulx_u32 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^32 - * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^32 + * out2 = ⌊arg1 * arg2 / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -77,7 +83,9 @@ static void fiat_p256_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, ui /* * The function fiat_p256_cmovznz_u32 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -94,10 +102,13 @@ static void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t /* * The function fiat_p256_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -1149,9 +1160,12 @@ static void fiat_p256_mul(uint32_t out1[8], const uint32_t arg1[8], const uint32 /* * The function fiat_p256_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2202,10 +2216,13 @@ static void fiat_p256_square(uint32_t out1[8], const uint32_t arg1[8]) { /* * The function fiat_p256_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2292,10 +2309,13 @@ static void fiat_p256_add(uint32_t out1[8], const uint32_t arg1[8], const uint32 /* * The function fiat_p256_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2365,9 +2385,12 @@ static void fiat_p256_sub(uint32_t out1[8], const uint32_t arg1[8], const uint32 /* * The function fiat_p256_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2436,9 +2459,12 @@ static void fiat_p256_opp(uint32_t out1[8], const uint32_t arg1[8]) { /* * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3044,8 +3070,11 @@ static void fiat_p256_from_montgomery(uint32_t out1[8], const uint32_t arg1[8]) /* * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3058,7 +3087,9 @@ static void fiat_p256_nonzero(uint32_t* out1, const uint32_t arg1[8]) { /* * The function fiat_p256_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -3095,8 +3126,11 @@ static void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const ui /* * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3202,9 +3236,12 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { /* * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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]] * Output Bounds: @@ -20,8 +20,10 @@ typedef unsigned __int128 fiat_p256_uint128; /* * The function fiat_p256_addcarryx_u64 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^64 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -40,8 +42,10 @@ static void fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_ /* * The function fiat_p256_subborrowx_u64 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^64 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -60,8 +64,10 @@ static void fiat_p256_subborrowx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat /* * The function fiat_p256_mulx_u64 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^64 - * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^64 + * out2 = ⌊arg1 * arg2 / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -79,7 +85,9 @@ static void fiat_p256_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui /* * The function fiat_p256_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -96,10 +104,13 @@ static void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t /* * The function fiat_p256_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -415,9 +426,12 @@ static void fiat_p256_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64 /* * The function fiat_p256_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -732,10 +746,13 @@ static void fiat_p256_square(uint64_t out1[4], const uint64_t arg1[4]) { /* * The function fiat_p256_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -786,10 +803,13 @@ static void fiat_p256_add(uint64_t out1[4], const uint64_t arg1[4], const uint64 /* * The function fiat_p256_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -831,9 +851,12 @@ static void fiat_p256_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64 /* * The function fiat_p256_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -874,9 +897,12 @@ static void fiat_p256_opp(uint64_t out1[4], const uint64_t arg1[4]) { /* * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1059,8 +1085,11 @@ static void fiat_p256_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) /* * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1073,7 +1102,9 @@ static void fiat_p256_nonzero(uint64_t* out1, const uint64_t arg1[4]) { /* * The function fiat_p256_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1098,8 +1129,11 @@ static void fiat_p256_selectznz(uint64_t out1[4], fiat_p256_uint1 arg1, const ui /* * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1205,9 +1239,12 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { /* * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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]] * Output Bounds: @@ -18,8 +18,10 @@ typedef signed char fiat_p384_int1; /* * The function fiat_p384_addcarryx_u32 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^32 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -38,8 +40,10 @@ static void fiat_p384_addcarryx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_ /* * The function fiat_p384_subborrowx_u32 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^32 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -58,8 +62,10 @@ static void fiat_p384_subborrowx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat /* * The function fiat_p384_mulx_u32 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^32 - * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^32 + * out2 = ⌊arg1 * arg2 / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -77,7 +83,9 @@ static void fiat_p384_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, ui /* * The function fiat_p384_cmovznz_u32 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -94,10 +102,13 @@ static void fiat_p384_cmovznz_u32(uint32_t* out1, fiat_p384_uint1 arg1, uint32_t /* * The function fiat_p384_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2677,9 +2688,12 @@ static void fiat_p384_mul(uint32_t out1[12], const uint32_t arg1[12], const uint /* * The function fiat_p384_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -5258,10 +5272,13 @@ static void fiat_p384_square(uint32_t out1[12], const uint32_t arg1[12]) { /* * The function fiat_p384_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -5384,10 +5401,13 @@ static void fiat_p384_add(uint32_t out1[12], const uint32_t arg1[12], const uint /* * The function fiat_p384_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -5485,9 +5505,12 @@ static void fiat_p384_sub(uint32_t out1[12], const uint32_t arg1[12], const uint /* * The function fiat_p384_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -5584,9 +5607,12 @@ static void fiat_p384_opp(uint32_t out1[12], const uint32_t arg1[12]) { /* * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^12) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^12) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -7221,8 +7247,11 @@ static void fiat_p384_from_montgomery(uint32_t out1[12], const uint32_t arg1[12] /* * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -7235,7 +7264,9 @@ static void fiat_p384_nonzero(uint32_t* out1, const uint32_t arg1[12]) { /* * The function fiat_p384_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -7284,8 +7315,11 @@ static void fiat_p384_selectznz(uint32_t out1[12], fiat_p384_uint1 arg1, const u /* * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..47] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -7439,9 +7473,12 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) { /* * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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]] * Output Bounds: @@ -20,8 +20,10 @@ typedef unsigned __int128 fiat_p384_uint128; /* * The function fiat_p384_addcarryx_u64 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^64 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -40,8 +42,10 @@ static void fiat_p384_addcarryx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_ /* * The function fiat_p384_subborrowx_u64 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^64 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -60,8 +64,10 @@ static void fiat_p384_subborrowx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat /* * The function fiat_p384_mulx_u64 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^64 - * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^64 + * out2 = ⌊arg1 * arg2 / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -79,7 +85,9 @@ static void fiat_p384_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui /* * The function fiat_p384_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -96,10 +104,13 @@ static void fiat_p384_cmovznz_u64(uint64_t* out1, fiat_p384_uint1 arg1, uint64_t /* * The function fiat_p384_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -855,9 +866,12 @@ static void fiat_p384_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64 /* * The function fiat_p384_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1612,10 +1626,13 @@ static void fiat_p384_square(uint64_t out1[6], const uint64_t arg1[6]) { /* * The function fiat_p384_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1684,10 +1701,13 @@ static void fiat_p384_add(uint64_t out1[6], const uint64_t arg1[6], const uint64 /* * The function fiat_p384_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1743,9 +1763,12 @@ static void fiat_p384_sub(uint64_t out1[6], const uint64_t arg1[6], const uint64 /* * The function fiat_p384_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1800,9 +1823,12 @@ static void fiat_p384_opp(uint64_t out1[6], const uint64_t arg1[6]) { /* * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2336,8 +2362,11 @@ static void fiat_p384_from_montgomery(uint64_t out1[6], const uint64_t arg1[6]) /* * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2350,7 +2379,9 @@ static void fiat_p384_nonzero(uint64_t* out1, const uint64_t arg1[6]) { /* * The function fiat_p384_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -2381,8 +2412,11 @@ static void fiat_p384_selectznz(uint64_t out1[6], fiat_p384_uint1 arg1, const ui /* * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..47] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2536,9 +2570,12 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) { /* * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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]] * Output Bounds: diff --git a/p448_solinas_64.c b/p448_solinas_64.c index 16dbbfe89..6e5c8066b 100644 --- a/p448_solinas_64.c +++ b/p448_solinas_64.c @@ -18,8 +18,10 @@ typedef unsigned __int128 fiat_p448_uint128; /* * The function fiat_p448_addcarryx_u56 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^56 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^56⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^56 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^56⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffff] @@ -38,8 +40,10 @@ static void fiat_p448_addcarryx_u56(uint64_t* out1, fiat_p448_uint1* out2, fiat_ /* * The function fiat_p448_subborrowx_u56 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^56 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^56⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^56 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^56⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffff] @@ -58,7 +62,9 @@ static void fiat_p448_subborrowx_u56(uint64_t* out1, fiat_p448_uint1* out2, fiat /* * The function fiat_p448_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -75,7 +81,9 @@ static void fiat_p448_cmovznz_u64(uint64_t* out1, fiat_p448_uint1 arg1, uint64_t /* * The function fiat_p448_carry_mul multiplies two field elements and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]] @@ -239,7 +247,9 @@ static void fiat_p448_carry_mul(uint64_t out1[8], const uint64_t arg1[8], const /* * The function fiat_p448_carry_square squares a field element and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg1) mod m + * Postconditions: + * 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]] * Output Bounds: @@ -381,7 +391,9 @@ static void fiat_p448_carry_square(uint64_t out1[8], const uint64_t arg1[8]) { /* * The function fiat_p448_carry reduces a field element. - * eval out1 mod m = eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -422,7 +434,9 @@ static void fiat_p448_carry(uint64_t out1[8], const uint64_t arg1[8]) { /* * The function fiat_p448_add adds two field elements. - * eval out1 mod m = (eval arg1 + eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]] @@ -450,7 +464,9 @@ static void fiat_p448_add(uint64_t out1[8], const uint64_t arg1[8], const uint64 /* * The function fiat_p448_sub subtracts two field elements. - * eval out1 mod m = (eval arg1 - eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]] @@ -478,7 +494,9 @@ static void fiat_p448_sub(uint64_t out1[8], const uint64_t arg1[8], const uint64 /* * The function fiat_p448_opp negates a field element. - * eval out1 mod m = -eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -505,7 +523,9 @@ static void fiat_p448_opp(uint64_t out1[8], const uint64_t arg1[8]) { /* * The function fiat_p448_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -542,7 +562,9 @@ static void fiat_p448_selectznz(uint64_t out1[8], fiat_p448_uint1 arg1, const ui /* * 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] + * Postconditions: + * 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]] * Output Bounds: @@ -762,7 +784,9 @@ static void fiat_p448_to_bytes(uint8_t out1[56], const uint64_t arg1[8]) { /* * 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 + * Postconditions: + * 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]] * Output Bounds: @@ -20,8 +20,10 @@ typedef unsigned __int128 fiat_p484_uint128; /* * The function fiat_p484_addcarryx_u64 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^64 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -40,8 +42,10 @@ static void fiat_p484_addcarryx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_ /* * The function fiat_p484_subborrowx_u64 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^64 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -60,8 +64,10 @@ static void fiat_p484_subborrowx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat /* * The function fiat_p484_mulx_u64 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^64 - * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^64 + * out2 = ⌊arg1 * arg2 / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -79,7 +85,9 @@ static void fiat_p484_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui /* * The function fiat_p484_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -96,10 +104,13 @@ static void fiat_p484_cmovznz_u64(uint64_t* out1, fiat_p484_uint1 arg1, uint64_t /* * The function fiat_p484_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1084,9 +1095,12 @@ static void fiat_p484_mul(uint64_t out1[7], const uint64_t arg1[7], const uint64 /* * The function fiat_p484_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2070,10 +2084,13 @@ static void fiat_p484_square(uint64_t out1[7], const uint64_t arg1[7]) { /* * The function fiat_p484_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -2151,10 +2168,13 @@ static void fiat_p484_add(uint64_t out1[7], const uint64_t arg1[7], const uint64 /* * The function fiat_p484_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -2217,9 +2237,12 @@ static void fiat_p484_sub(uint64_t out1[7], const uint64_t arg1[7], const uint64 /* * The function fiat_p484_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2281,9 +2304,12 @@ static void fiat_p484_opp(uint64_t out1[7], const uint64_t arg1[7]) { /* * The function fiat_p484_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^7) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^7) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2928,8 +2954,11 @@ static void fiat_p484_from_montgomery(uint64_t out1[7], const uint64_t arg1[7]) /* * The function fiat_p484_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2942,7 +2971,9 @@ static void fiat_p484_nonzero(uint64_t* out1, const uint64_t arg1[7]) { /* * The function fiat_p484_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -2976,8 +3007,11 @@ static void fiat_p484_selectznz(uint64_t out1[7], fiat_p484_uint1 arg1, const ui /* * The function fiat_p484_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..55] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x3ffffffffffff]] * Output Bounds: @@ -3154,9 +3188,12 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) { /* * The function fiat_p484_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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 ~> 0x3], [0x0 ~> 0x0]] * Output Bounds: @@ -18,8 +18,10 @@ typedef unsigned __int128 fiat_p521_uint128; /* * The function fiat_p521_addcarryx_u30 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^30 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^30⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^30 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^30⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3fffffff] @@ -38,8 +40,10 @@ static void fiat_p521_addcarryx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_ /* * The function fiat_p521_subborrowx_u30 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^30 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^30⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^30 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^30⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3fffffff] @@ -58,8 +62,10 @@ static void fiat_p521_subborrowx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat /* * The function fiat_p521_addcarryx_u31 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^31 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^31⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^31 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^31⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7fffffff] @@ -78,8 +84,10 @@ static void fiat_p521_addcarryx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat_ /* * The function fiat_p521_subborrowx_u31 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^31 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^31⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^31 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^31⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7fffffff] @@ -98,7 +106,9 @@ static void fiat_p521_subborrowx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat /* * The function fiat_p521_cmovznz_u32 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -115,7 +125,9 @@ static void fiat_p521_cmovznz_u32(uint32_t* out1, fiat_p521_uint1 arg1, uint32_t /* * The function fiat_p521_carry_mul multiplies two field elements and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[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]] @@ -507,7 +519,9 @@ static void fiat_p521_carry_mul(uint32_t out1[17], const uint64_t arg1[17], cons /* * The function fiat_p521_carry_square squares a field element and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg1) mod m + * Postconditions: + * 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]] * Output Bounds: @@ -794,7 +808,9 @@ static void fiat_p521_carry_square(uint32_t out1[17], const uint64_t arg1[17]) { /* * The function fiat_p521_carry reduces a field element. - * eval out1 mod m = eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -858,7 +874,9 @@ static void fiat_p521_carry(uint32_t out1[17], const uint64_t arg1[17]) { /* * The function fiat_p521_add adds two field elements. - * eval out1 mod m = (eval arg1 + eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[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]] @@ -904,7 +922,9 @@ static void fiat_p521_add(uint64_t out1[17], const uint32_t arg1[17], const uint /* * The function fiat_p521_sub subtracts two field elements. - * eval out1 mod m = (eval arg1 - eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[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]] @@ -950,7 +970,9 @@ static void fiat_p521_sub(uint64_t out1[17], const uint32_t arg1[17], const uint /* * The function fiat_p521_opp negates a field element. - * eval out1 mod m = -eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -995,7 +1017,9 @@ static void fiat_p521_opp(uint32_t out1[17], const uint32_t arg1[17]) { /* * The function fiat_p521_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -1059,7 +1083,9 @@ static void fiat_p521_selectznz(uint32_t out1[17], fiat_p521_uint1 arg1, const u /* * 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] + * Postconditions: + * 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]] * Output Bounds: @@ -1396,7 +1422,9 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) { /* * 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 + * Postconditions: + * 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]] * Output Bounds: @@ -18,8 +18,10 @@ typedef unsigned __int128 fiat_p521_uint128; /* * The function fiat_p521_addcarryx_u58 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^58 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^58 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffffffffffff] @@ -38,8 +40,10 @@ static void fiat_p521_addcarryx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_ /* * The function fiat_p521_subborrowx_u58 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^58 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^58 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffffffffffff] @@ -58,8 +62,10 @@ static void fiat_p521_subborrowx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat /* * The function fiat_p521_addcarryx_u57 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^57 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^57 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffffffffffff] @@ -78,8 +84,10 @@ static void fiat_p521_addcarryx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_ /* * The function fiat_p521_subborrowx_u57 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^57 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^57 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffffffffffff] @@ -98,7 +106,9 @@ static void fiat_p521_subborrowx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat /* * The function fiat_p521_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -115,7 +125,9 @@ static void fiat_p521_cmovznz_u64(uint64_t* out1, fiat_p521_uint1 arg1, uint64_t /* * The function fiat_p521_carry_mul multiplies two field elements and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0x699999999999999]] @@ -259,7 +271,9 @@ static void fiat_p521_carry_mul(uint64_t out1[9], const uint64_t arg1[9], const /* * The function fiat_p521_carry_square squares a field element and reduces the result. - * eval out1 mod m = (eval arg1 * eval arg1) mod m + * Postconditions: + * 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]] * Output Bounds: @@ -382,7 +396,9 @@ static void fiat_p521_carry_square(uint64_t out1[9], const uint64_t arg1[9]) { /* * The function fiat_p521_carry reduces a field element. - * eval out1 mod m = eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -422,7 +438,9 @@ static void fiat_p521_carry(uint64_t out1[9], const uint64_t arg1[9]) { /* * The function fiat_p521_add adds two field elements. - * eval out1 mod m = (eval arg1 + eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]] @@ -452,7 +470,9 @@ static void fiat_p521_add(uint64_t out1[9], const uint64_t arg1[9], const uint64 /* * The function fiat_p521_sub subtracts two field elements. - * eval out1 mod m = (eval arg1 - eval arg2) mod m + * Postconditions: + * 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]] * arg2: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]] @@ -482,7 +502,9 @@ static void fiat_p521_sub(uint64_t out1[9], const uint64_t arg1[9], const uint64 /* * The function fiat_p521_opp negates a field element. - * eval out1 mod m = -eval arg1 mod m + * Postconditions: + * 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]] * Output Bounds: @@ -511,7 +533,9 @@ static void fiat_p521_opp(uint64_t out1[9], const uint64_t arg1[9]) { /* * The function fiat_p521_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -551,7 +575,9 @@ static void fiat_p521_selectznz(uint64_t out1[9], fiat_p521_uint1 arg1, const ui /* * 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] + * Postconditions: + * 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]] * Output Bounds: @@ -824,7 +850,9 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { /* * 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 + * Postconditions: + * 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]] * Output Bounds: diff --git a/secp256k1_32.c b/secp256k1_32.c index 354338e62..cfa8e76f8 100644 --- a/secp256k1_32.c +++ b/secp256k1_32.c @@ -18,8 +18,10 @@ typedef signed char fiat_secp256k1_int1; /* * The function fiat_secp256k1_addcarryx_u32 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^32 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -38,8 +40,10 @@ static void fiat_secp256k1_addcarryx_u32(uint32_t* out1, fiat_secp256k1_uint1* o /* * The function fiat_secp256k1_subborrowx_u32 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^32 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -58,8 +62,10 @@ static void fiat_secp256k1_subborrowx_u32(uint32_t* out1, fiat_secp256k1_uint1* /* * The function fiat_secp256k1_mulx_u32 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^32 - * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^32 + * out2 = ⌊arg1 * arg2 / 2^32⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -77,7 +83,9 @@ static void fiat_secp256k1_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg /* * The function fiat_secp256k1_cmovznz_u32 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -94,10 +102,13 @@ static void fiat_secp256k1_cmovznz_u32(uint32_t* out1, fiat_secp256k1_uint1 arg1 /* * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -1389,9 +1400,12 @@ static void fiat_secp256k1_mul(uint32_t out1[8], const uint32_t arg1[8], const u /* * The function fiat_secp256k1_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2682,10 +2696,13 @@ static void fiat_secp256k1_square(uint32_t out1[8], const uint32_t arg1[8]) { /* * The function fiat_secp256k1_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2772,10 +2789,13 @@ static void fiat_secp256k1_add(uint32_t out1[8], const uint32_t arg1[8], const u /* * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2845,9 +2865,12 @@ static void fiat_secp256k1_sub(uint32_t out1[8], const uint32_t arg1[8], const u /* * The function fiat_secp256k1_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2916,9 +2939,12 @@ static void fiat_secp256k1_opp(uint32_t out1[8], const uint32_t arg1[8]) { /* * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3818,8 +3844,11 @@ static void fiat_secp256k1_from_montgomery(uint32_t out1[8], const uint32_t arg1 /* * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3832,7 +3861,9 @@ static void fiat_secp256k1_nonzero(uint32_t* out1, const uint32_t arg1[8]) { /* * The function fiat_secp256k1_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -3869,8 +3900,11 @@ static void fiat_secp256k1_selectznz(uint32_t out1[8], fiat_secp256k1_uint1 arg1 /* * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3976,9 +4010,12 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { /* * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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]] * Output Bounds: diff --git a/secp256k1_64.c b/secp256k1_64.c index 04bb1c8e8..2706759bd 100644 --- a/secp256k1_64.c +++ b/secp256k1_64.c @@ -20,8 +20,10 @@ typedef unsigned __int128 fiat_secp256k1_uint128; /* * The function fiat_secp256k1_addcarryx_u64 is an addition with carry. - * out1 = (arg1 + arg2 + arg3) mod 2^64 - * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * Postconditions: + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -40,8 +42,10 @@ static void fiat_secp256k1_addcarryx_u64(uint64_t* out1, fiat_secp256k1_uint1* o /* * The function fiat_secp256k1_subborrowx_u64 is a subtraction with borrow. - * out1 = (-arg1 + arg2 + -arg3) mod 2^64 - * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * Postconditions: + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -60,8 +64,10 @@ static void fiat_secp256k1_subborrowx_u64(uint64_t* out1, fiat_secp256k1_uint1* /* * The function fiat_secp256k1_mulx_u64 is a multiplication, returning the full double-width result. - * out1 = (arg1 * arg2) mod 2^64 - * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ + * Postconditions: + * out1 = (arg1 * arg2) mod 2^64 + * out2 = ⌊arg1 * arg2 / 2^64⌋ + * * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -79,7 +85,9 @@ static void fiat_secp256k1_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg /* * The function fiat_secp256k1_cmovznz_u64 is a single-word conditional move. - * out1 = (if arg1 = 0 then arg2 else arg3) + * Postconditions: + * out1 = (if arg1 = 0 then arg2 else arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -96,10 +104,13 @@ static void fiat_secp256k1_cmovznz_u64(uint64_t* out1, fiat_secp256k1_uint1 arg1 /* * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -463,9 +474,12 @@ static void fiat_secp256k1_mul(uint64_t out1[4], const uint64_t arg1[4], const u /* * The function fiat_secp256k1_square squares a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -828,10 +842,13 @@ static void fiat_secp256k1_square(uint64_t out1[4], const uint64_t arg1[4]) { /* * The function fiat_secp256k1_add adds two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -882,10 +899,13 @@ static void fiat_secp256k1_add(uint64_t out1[4], const uint64_t arg1[4], const u /* * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * 0 ≤ eval arg2 < m → - * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * 0 ≤ eval arg2 < m + * Postconditions: + * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -927,9 +947,12 @@ static void fiat_secp256k1_sub(uint64_t out1[4], const uint64_t arg1[4], const u /* * The function fiat_secp256k1_opp negates a field element in the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -970,9 +993,12 @@ static void fiat_secp256k1_opp(uint64_t out1[4], const uint64_t arg1[4]) { /* * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain. - * 0 ≤ eval arg1 < m → - * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m + * 0 ≤ eval out1 < m + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1236,8 +1262,11 @@ static void fiat_secp256k1_from_montgomery(uint64_t out1[4], const uint64_t arg1 /* * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. - * 0 ≤ eval arg1 < m → - * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1250,7 +1279,9 @@ static void fiat_secp256k1_nonzero(uint64_t* out1, const uint64_t arg1[4]) { /* * The function fiat_secp256k1_selectznz is a multi-limb conditional select. - * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * Postconditions: + * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) + * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1275,8 +1306,11 @@ static void fiat_secp256k1_selectznz(uint64_t out1[4], fiat_secp256k1_uint1 arg1 /* * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. - * 0 ≤ eval arg1 < m → - * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] + * Preconditions: + * 0 ≤ eval arg1 < m + * Postconditions: + * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] + * * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1382,9 +1416,12 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { /* * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. - * 0 ≤ bytes_eval arg1 < m → - * eval out1 mod m = bytes_eval arg1 mod m - * ∧ 0 ≤ eval out1 < m + * Preconditions: + * 0 ≤ bytes_eval arg1 < m + * Postconditions: + * eval out1 mod m = bytes_eval arg1 mod m + * 0 ≤ eval out1 < 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]] * Output Bounds: diff --git a/src/CStringification.v b/src/CStringification.v index d31fa55e8..b50957dcd 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -2212,7 +2212,7 @@ Module Compilers. := match ExprOfPHOAS do_bounds_check e name_list inbounds with | inl (indata, outdata, f) => inl ((["/*"] - ++ (List.map (fun s => " * " ++ s)%string (comment indata outdata)) + ++ (List.map (fun s => if (String.length s =? 0)%nat then " *" else (" * " ++ s))%string (comment indata outdata)) ++ [" * Input Bounds:"] ++ List.map (fun v => " * " ++ v)%string (input_bounds_to_string indata inbounds) ++ [" * Output Bounds:"] diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 67b743ad3..c72b5a50d 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -459,7 +459,7 @@ Module CorrectnessStringification. | ?x < ?y < ?z => stringify_infix2 "<" "<" 70 69 69 69 | iff _ _ => stringify_infix "↔" 95 94 94 | and _ _ => stringify_infix "∧" 80 80 80 - | Z.modulo _ _ => stringify_infix "mod" 40 39 39 + | Z.modulo _ _ => stringify_infix "mod" 41 39 39 | Z.mul _ _ => stringify_infix "*" 40 40 39 | Z.pow _ _ => stringify_infix_without_space "^" 30 29 30 | Z.add _ _ => stringify_infix "+" 50 50 49 @@ -508,31 +508,55 @@ Module CorrectnessStringification. end end. - Ltac stringify_rec prefix ctx correctness lvl := - let recurse' prefix v lvl := stringify_rec prefix ctx v lvl in - let recurse := recurse' "" in - let default _ := let v := stringify_rec0 ctx correctness lvl in - constr:((prefix ++ v)::nil) in + Ltac stringify_preconditions ctx so_far_rev correctness := + let recurse so_far_rev v := stringify_preconditions ctx so_far_rev v in lazymatch correctness with | ?A -> ?B - => let sA := stringify_rec0 ctx A 98 in - let sB := recurse B 200 in - constr:((prefix ++ sA ++ " →")%string :: sB) + => let sA := stringify_rec0 ctx A 200 in + recurse (sA :: so_far_rev) B + | ?T + => let so_far := (eval cbv [List.rev] in (List.rev so_far_rev)) in + constr:((so_far, T)) + end. + + Ltac stringify_postconditions ctx correctness := + let recurse v := stringify_postconditions ctx v in + let default _ := let v := stringify_rec0 ctx correctness 200 in + constr:(v::nil) in + lazymatch correctness with | _ <= _ < _ => default () | _ <= _ <= _ => default () | _ < _ <= _ => default () | _ < _ < _ => default () | and ?A ?B - => let sA := recurse' prefix A 80 in - let sB := recurse' "∧ " B 80 in - constr:(List.app sA sB) + => let sA := recurse A in + let sB := recurse B in + (eval cbv [List.app] in (List.app sA sB)) | ?x = ?y :> prod ?A ?B => let v := (eval cbn [fst snd] in (fst x = fst y /\ snd x = snd y)) in - recurse' prefix v lvl + recurse v | _ => default () end. + Ltac stringify_rec ctx correctness := + let pre_rest := stringify_preconditions ctx (@nil string) correctness in + lazymatch pre_rest with + | (?preconditions, ?correctness) + => let postconditions := stringify_postconditions ctx correctness in + let preconditions_list_string + := lazymatch preconditions with + | nil => constr:(@nil string) + | _ => constr:((["Preconditions:"] + ++ List.map (fun s => " " ++ s)%string preconditions)%list%string) + end in + let postconditions_list_string + := constr:((["Postconditions:"] + ++ List.map (fun s => " " ++ s)%string postconditions)%list%string) in + (eval cbv [List.map List.app] in + (preconditions_list_string ++ postconditions_list_string ++ [""])%list%string) + end. + Ltac strip_lambdas v := lazymatch v with | fun _ => ?f => strip_lambdas f @@ -553,7 +577,7 @@ Module CorrectnessStringification. out_var_names ltac:( fun ctx T - => let v := stringify_rec "" ctx T 200 in refine v + => let v := stringify_rec ctx T in refine v ) in let res := strip_lambdas res in res. |