diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-30 19:13:27 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-02 18:22:15 -0500 |
| commit | 496271f86e9dc6df1b23a189d6b8fd2a82db33aa (patch) | |
| tree | 1b531bac09c49efb594642ea85d398f7893f8494 | |
| parent | cd1d339aa57c09abc716ef30a5a153ac5aadb563 (diff) | |
Add autogenerated docstrings to synthesized code
We now stringify the correctness conditions to generate docstrings for
the synthesized code.
Closes #512
Time commitment: about 6 hours
| -rw-r--r-- | curve25519_32.c | 34 | ||||
| -rw-r--r-- | curve25519_64.c | 28 | ||||
| -rw-r--r-- | p224_32.c | 57 | ||||
| -rw-r--r-- | p224_64.c | 57 | ||||
| -rw-r--r-- | p256_32.c | 57 | ||||
| -rw-r--r-- | p256_64.c | 57 | ||||
| -rw-r--r-- | p384_32.c | 57 | ||||
| -rw-r--r-- | p384_64.c | 57 | ||||
| -rw-r--r-- | p448_solinas_64.c | 26 | ||||
| -rw-r--r-- | p484_64.c | 57 | ||||
| -rw-r--r-- | p521_32.c | 32 | ||||
| -rw-r--r-- | p521_64.c | 32 | ||||
| -rw-r--r-- | secp256k1_32.c | 57 | ||||
| -rw-r--r-- | secp256k1_64.c | 57 | ||||
| -rw-r--r-- | src/BoundsPipeline.v | 47 | ||||
| -rw-r--r-- | src/CStringification.v | 44 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/BarrettReduction.v | 5 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/MontgomeryReduction.v | 5 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 472 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinas.v | 18 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/SmallExamples.v | 18 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/UnsaturatedSolinas.v | 95 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/WordByWordMontgomery.v | 123 | ||||
| -rw-r--r-- | src/SlowPrimeSynthesisExamples.v | 2 |
24 files changed, 1411 insertions, 83 deletions
diff --git a/curve25519_32.c b/curve25519_32.c index 83453d82b..ccb1085fb 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -15,6 +15,9 @@ typedef signed char fiat_25519_int1; /* + * The function fiat_25519_addcarryx_u26 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^26 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffff] @@ -32,6 +35,9 @@ static void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fia } /* + * The function fiat_25519_subborrowx_u26 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^26 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffff] @@ -49,6 +55,9 @@ static void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fi } /* + * The function fiat_25519_addcarryx_u25 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^25 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffff] @@ -66,6 +75,9 @@ static void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fia } /* + * The function fiat_25519_subborrowx_u25 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^25 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffff] @@ -83,6 +95,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -98,6 +112,8 @@ static void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32 } /* + * The function fiat_25519_carry_mul does stuff. + * 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]] @@ -265,6 +281,8 @@ static void fiat_25519_carry_mul(uint32_t out1[10], const uint32_t arg1[10], con } /* + * The function fiat_25519_carry_square does stuff. + * 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: @@ -404,6 +422,8 @@ static void fiat_25519_carry_square(uint32_t out1[10], const uint32_t arg1[10]) } /* + * The function fiat_25519_carry_scmul_121666 does stuff. + * 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: @@ -470,6 +490,8 @@ static void fiat_25519_carry_scmul_121666(uint32_t out1[10], const uint32_t arg1 } /* + * The function fiat_25519_carry does stuff. + * 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: @@ -511,6 +533,8 @@ static void fiat_25519_carry(uint32_t out1[10], const uint32_t arg1[10]) { } /* + * The function fiat_25519_add does stuff. + * 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]] @@ -541,6 +565,8 @@ static void fiat_25519_add(uint32_t out1[10], const uint32_t arg1[10], const uin } /* + * The function fiat_25519_sub does stuff. + * 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]] @@ -571,6 +597,8 @@ static void fiat_25519_sub(uint32_t out1[10], const uint32_t arg1[10], const uin } /* + * The function fiat_25519_opp does stuff. + * 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: @@ -600,6 +628,8 @@ 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) * 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]] @@ -641,6 +671,8 @@ static void fiat_25519_selectznz(uint32_t out1[10], fiat_25519_uint1 arg1, const } /* + * The function fiat_25519_to_bytes does stuff. + * 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: @@ -821,6 +853,8 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { } /* + * The function fiat_25519_from_bytes does stuff. + * 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 59beaf93a..5b350177b 100644 --- a/curve25519_64.c +++ b/curve25519_64.c @@ -17,6 +17,9 @@ typedef unsigned __int128 fiat_25519_uint128; /* + * The function fiat_25519_addcarryx_u51 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^51 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7ffffffffffff] @@ -34,6 +37,9 @@ static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fia } /* + * The function fiat_25519_subborrowx_u51 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^51 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7ffffffffffff] @@ -51,6 +57,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -66,6 +74,8 @@ static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64 } /* + * The function fiat_25519_carry_mul does stuff. + * 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]] @@ -133,6 +143,8 @@ static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const } /* + * The function fiat_25519_carry_square does stuff. + * 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: @@ -197,6 +209,8 @@ static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) { } /* + * The function fiat_25519_carry_scmul_121666 does stuff. + * eval out1 mod m = (121666 * eval arg1) mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] * Output Bounds: @@ -238,6 +252,8 @@ static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[ } /* + * The function fiat_25519_carry does stuff. + * eval out1 mod m = eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] * Output Bounds: @@ -264,6 +280,8 @@ static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) { } /* + * The function fiat_25519_add does stuff. + * 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]] @@ -284,6 +302,8 @@ static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint6 } /* + * The function fiat_25519_sub does stuff. + * 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]] @@ -304,6 +324,8 @@ static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint6 } /* + * The function fiat_25519_opp does stuff. + * eval out1 mod m = -eval arg1 mod m * Input Bounds: * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] * Output Bounds: @@ -323,6 +345,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -349,6 +373,8 @@ static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const } /* + * The function fiat_25519_to_bytes does stuff. + * 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: @@ -492,6 +518,8 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) { } /* + * The function fiat_25519_from_bytes does stuff. + * 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: @@ -17,6 +17,9 @@ typedef signed char fiat_p224_int1; /* + * The function fiat_p224_addcarryx_u32 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -34,6 +37,9 @@ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_ } /* + * The function fiat_p224_subborrowx_u32 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -51,6 +57,9 @@ static void fiat_p224_subborrowx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat } /* + * The function fiat_p224_mulx_u32 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^32 + * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -67,6 +76,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -82,6 +93,12 @@ static void fiat_p224_cmovznz_u32(uint32_t* out1, fiat_p224_uint1 arg1, uint32_t } /* + * The function fiat_p224_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] + * ∧ 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]] @@ -960,6 +977,11 @@ static void fiat_p224_mul(uint32_t out1[7], const uint32_t arg1[7], const uint32 } /* + * The function fiat_p224_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -1837,6 +1859,12 @@ static void fiat_p224_square(uint32_t out1[7], const uint32_t arg1[7]) { } /* + * The function fiat_p224_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] + * ∧ 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]] @@ -1913,6 +1941,12 @@ static void fiat_p224_add(uint32_t out1[7], const uint32_t arg1[7], const uint32 } /* + * The function fiat_p224_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] + * ∧ 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]] @@ -1974,6 +2008,11 @@ static void fiat_p224_sub(uint32_t out1[7], const uint32_t arg1[7], const uint32 } /* + * The function fiat_p224_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2034,6 +2073,11 @@ static void fiat_p224_opp(uint32_t out1[7], const uint32_t arg1[7]) { } /* + * The function fiat_p224_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 26959946660873538059280334323183841250350249843942399443119741337601^7) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2569,6 +2613,9 @@ static void fiat_p224_from_montgomery(uint32_t out1[7], const uint32_t arg1[7]) } /* + * The function fiat_p224_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2580,6 +2627,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -2612,6 +2661,9 @@ static void fiat_p224_selectznz(uint32_t out1[7], fiat_p224_uint1 arg1, const ui } /* + * The function fiat_p224_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27] * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -2704,6 +2756,11 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) { } /* + * The function fiat_p224_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] + * ∧ 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: @@ -19,6 +19,9 @@ typedef unsigned __int128 fiat_p224_uint128; /* + * The function fiat_p224_addcarryx_u64 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -36,6 +39,9 @@ static void fiat_p224_addcarryx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_ } /* + * The function fiat_p224_subborrowx_u64 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -53,6 +59,9 @@ static void fiat_p224_subborrowx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat } /* + * The function fiat_p224_mulx_u64 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^64 + * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -69,6 +78,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -84,6 +95,12 @@ static void fiat_p224_cmovznz_u64(uint64_t* out1, fiat_p224_uint1 arg1, uint64_t } /* + * The function fiat_p224_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -422,6 +439,11 @@ static void fiat_p224_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* + * The function fiat_p224_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -759,6 +781,12 @@ static void fiat_p224_square(uint64_t out1[4], const uint64_t arg1[4]) { } /* + * The function fiat_p224_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -808,6 +836,12 @@ static void fiat_p224_add(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* + * The function fiat_p224_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -848,6 +882,11 @@ static void fiat_p224_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* + * The function fiat_p224_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -887,6 +926,11 @@ static void fiat_p224_opp(uint64_t out1[4], const uint64_t arg1[4]) { } /* + * The function fiat_p224_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 26959946667150639793205513449688727755354231427310025123858428723201^4) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1104,6 +1148,9 @@ static void fiat_p224_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) } /* + * The function fiat_p224_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1115,6 +1162,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1138,6 +1187,9 @@ static void fiat_p224_selectznz(uint64_t out1[4], fiat_p224_uint1 arg1, const ui } /* + * The function fiat_p224_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -1235,6 +1287,11 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { } /* + * The function fiat_p224_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 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: @@ -17,6 +17,9 @@ typedef signed char fiat_p256_int1; /* + * The function fiat_p256_addcarryx_u32 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -34,6 +37,9 @@ static void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_ } /* + * The function fiat_p256_subborrowx_u32 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -51,6 +57,9 @@ static void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat } /* + * The function fiat_p256_mulx_u32 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^32 + * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -67,6 +76,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -82,6 +93,12 @@ static void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t } /* + * The function fiat_p256_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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]] @@ -1132,6 +1149,11 @@ static void fiat_p256_mul(uint32_t out1[8], const uint32_t arg1[8], const uint32 } /* + * The function fiat_p256_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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: @@ -2181,6 +2203,12 @@ static void fiat_p256_square(uint32_t out1[8], const uint32_t arg1[8]) { } /* + * The function fiat_p256_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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]] @@ -2266,6 +2294,12 @@ static void fiat_p256_add(uint32_t out1[8], const uint32_t arg1[8], const uint32 } /* + * The function fiat_p256_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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]] @@ -2334,6 +2368,11 @@ static void fiat_p256_sub(uint32_t out1[8], const uint32_t arg1[8], const uint32 } /* + * The function fiat_p256_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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: @@ -2401,6 +2440,11 @@ static void fiat_p256_opp(uint32_t out1[8], const uint32_t arg1[8]) { } /* + * The function fiat_p256_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 26959946660873538060741835960514744168633162839172946800369217830912^8) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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: @@ -3005,6 +3049,9 @@ static void fiat_p256_from_montgomery(uint32_t out1[8], const uint32_t arg1[8]) } /* + * The function fiat_p256_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3016,6 +3063,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -3051,6 +3100,9 @@ static void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const ui } /* + * The function fiat_p256_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3155,6 +3207,11 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { } /* + * The function fiat_p256_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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: @@ -19,6 +19,9 @@ typedef unsigned __int128 fiat_p256_uint128; /* + * The function fiat_p256_addcarryx_u64 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -36,6 +39,9 @@ static void fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_ } /* + * The function fiat_p256_subborrowx_u64 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -53,6 +59,9 @@ static void fiat_p256_subborrowx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat } /* + * The function fiat_p256_mulx_u64 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^64 + * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -69,6 +78,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -84,6 +95,12 @@ static void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t } /* + * The function fiat_p256_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -398,6 +415,11 @@ static void fiat_p256_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* + * The function fiat_p256_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -711,6 +733,12 @@ static void fiat_p256_square(uint64_t out1[4], const uint64_t arg1[4]) { } /* + * The function fiat_p256_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -760,6 +788,12 @@ static void fiat_p256_add(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* + * The function fiat_p256_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -800,6 +834,11 @@ static void fiat_p256_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64 } /* + * The function fiat_p256_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -839,6 +878,11 @@ static void fiat_p256_opp(uint64_t out1[4], const uint64_t arg1[4]) { } /* + * The function fiat_p256_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 6277101733925179126845168871924920046849447032244165148672^4) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1020,6 +1064,9 @@ static void fiat_p256_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) } /* + * The function fiat_p256_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1031,6 +1078,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1054,6 +1103,9 @@ static void fiat_p256_selectznz(uint64_t out1[4], fiat_p256_uint1 arg1, const ui } /* + * The function fiat_p256_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1158,6 +1210,11 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { } /* + * The function fiat_p256_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 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: @@ -17,6 +17,9 @@ typedef signed char fiat_p384_int1; /* + * The function fiat_p384_addcarryx_u32 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -34,6 +37,9 @@ static void fiat_p384_addcarryx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_ } /* + * The function fiat_p384_subborrowx_u32 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -51,6 +57,9 @@ static void fiat_p384_subborrowx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat } /* + * The function fiat_p384_mulx_u32 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^32 + * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -67,6 +76,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -82,6 +93,12 @@ static void fiat_p384_cmovznz_u32(uint32_t* out1, fiat_p384_uint1 arg1, uint32_t } /* + * The function fiat_p384_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] + * ∧ 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]] @@ -2660,6 +2677,11 @@ static void fiat_p384_mul(uint32_t out1[12], const uint32_t arg1[12], const uint } /* + * The function fiat_p384_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] + * ∧ 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: @@ -5237,6 +5259,12 @@ static void fiat_p384_square(uint32_t out1[12], const uint32_t arg1[12]) { } /* + * The function fiat_p384_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] + * ∧ 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]] @@ -5358,6 +5386,12 @@ static void fiat_p384_add(uint32_t out1[12], const uint32_t arg1[12], const uint } /* + * The function fiat_p384_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] + * ∧ 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]] @@ -5454,6 +5488,11 @@ static void fiat_p384_sub(uint32_t out1[12], const uint32_t arg1[12], const uint } /* + * The function fiat_p384_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] + * ∧ 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: @@ -5549,6 +5588,11 @@ static void fiat_p384_opp(uint32_t out1[12], const uint32_t arg1[12]) { } /* + * The function fiat_p384_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 9173994463960286046443283581208347763186259956673124494950355357547691504353860004117541501358835492716545^12) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] + * ∧ 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: @@ -7182,6 +7226,9 @@ static void fiat_p384_from_montgomery(uint32_t out1[12], const uint32_t arg1[12] } /* + * The function fiat_p384_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0 * Input Bounds: * 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: @@ -7193,6 +7240,8 @@ 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) * 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]] @@ -7240,6 +7289,9 @@ static void fiat_p384_selectznz(uint32_t out1[12], fiat_p384_uint1 arg1, const u } /* + * The function fiat_p384_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] * Input Bounds: * 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: @@ -7392,6 +7444,11 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) { } /* + * The function fiat_p384_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] + * ∧ 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: @@ -19,6 +19,9 @@ typedef unsigned __int128 fiat_p384_uint128; /* + * The function fiat_p384_addcarryx_u64 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -36,6 +39,9 @@ static void fiat_p384_addcarryx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_ } /* + * The function fiat_p384_subborrowx_u64 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -53,6 +59,9 @@ static void fiat_p384_subborrowx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat } /* + * The function fiat_p384_mulx_u64 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^64 + * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -69,6 +78,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -84,6 +95,12 @@ static void fiat_p384_cmovznz_u64(uint64_t* out1, fiat_p384_uint1 arg1, uint64_t } /* + * The function fiat_p384_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] + * ∧ 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]] @@ -838,6 +855,11 @@ static void fiat_p384_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64 } /* + * The function fiat_p384_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1591,6 +1613,12 @@ static void fiat_p384_square(uint64_t out1[6], const uint64_t arg1[6]) { } /* + * The function fiat_p384_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] + * ∧ 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]] @@ -1658,6 +1686,12 @@ static void fiat_p384_add(uint64_t out1[6], const uint64_t arg1[6], const uint64 } /* + * The function fiat_p384_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] + * ∧ 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]] @@ -1712,6 +1746,11 @@ static void fiat_p384_sub(uint64_t out1[6], const uint64_t arg1[6], const uint64 } /* + * The function fiat_p384_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1765,6 +1804,11 @@ static void fiat_p384_opp(uint64_t out1[6], const uint64_t arg1[6]) { } /* + * The function fiat_p384_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 9173994466096273082364193663603369469355812071275829017307008127494733112176079729898163604637719575134209^6) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2297,6 +2341,9 @@ static void fiat_p384_from_montgomery(uint64_t out1[6], const uint64_t arg1[6]) } /* + * The function fiat_p384_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2308,6 +2355,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -2337,6 +2386,9 @@ static void fiat_p384_selectznz(uint64_t out1[6], fiat_p384_uint1 arg1, const ui } /* + * The function fiat_p384_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2489,6 +2541,11 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) { } /* + * The function fiat_p384_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] + * ∧ 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 8604acca6..edf5fceb4 100644 --- a/p448_solinas_64.c +++ b/p448_solinas_64.c @@ -17,6 +17,9 @@ typedef unsigned __int128 fiat_p448_uint128; /* + * The function fiat_p448_addcarryx_u56 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^56 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^56⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffff] @@ -34,6 +37,9 @@ static void fiat_p448_addcarryx_u56(uint64_t* out1, fiat_p448_uint1* out2, fiat_ } /* + * The function fiat_p448_subborrowx_u56 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^56 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^56⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffff] @@ -51,6 +57,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -66,6 +74,8 @@ static void fiat_p448_cmovznz_u64(uint64_t* out1, fiat_p448_uint1 arg1, uint64_t } /* + * The function fiat_p448_carry_mul does stuff. + * 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]] @@ -228,6 +238,8 @@ static void fiat_p448_carry_mul(uint64_t out1[8], const uint64_t arg1[8], const } /* + * The function fiat_p448_carry_square does stuff. + * 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: @@ -368,6 +380,8 @@ static void fiat_p448_carry_square(uint64_t out1[8], const uint64_t arg1[8]) { } /* + * The function fiat_p448_carry does stuff. + * 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: @@ -407,6 +421,8 @@ static void fiat_p448_carry(uint64_t out1[8], const uint64_t arg1[8]) { } /* + * The function fiat_p448_add does stuff. + * 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]] @@ -433,6 +449,8 @@ static void fiat_p448_add(uint64_t out1[8], const uint64_t arg1[8], const uint64 } /* + * The function fiat_p448_sub does stuff. + * 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]] @@ -459,6 +477,8 @@ static void fiat_p448_sub(uint64_t out1[8], const uint64_t arg1[8], const uint64 } /* + * The function fiat_p448_opp does stuff. + * 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: @@ -484,6 +504,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -519,6 +541,8 @@ static void fiat_p448_selectznz(uint64_t out1[8], fiat_p448_uint1 arg1, const ui } /* + * The function fiat_p448_to_bytes does stuff. + * 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: @@ -737,6 +761,8 @@ static void fiat_p448_to_bytes(uint8_t out1[56], const uint64_t arg1[8]) { } /* + * The function fiat_p448_from_bytes does stuff. + * 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: @@ -19,6 +19,9 @@ typedef unsigned __int128 fiat_p484_uint128; /* + * The function fiat_p484_addcarryx_u64 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -36,6 +39,9 @@ static void fiat_p484_addcarryx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_ } /* + * The function fiat_p484_subborrowx_u64 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -53,6 +59,9 @@ static void fiat_p484_subborrowx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat } /* + * The function fiat_p484_mulx_u64 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^64 + * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -69,6 +78,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -84,6 +95,12 @@ static void fiat_p484_cmovznz_u64(uint64_t* out1, fiat_p484_uint1 arg1, uint64_t } /* + * The function fiat_p484_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] + * ∧ 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]] @@ -1067,6 +1084,11 @@ static void fiat_p484_mul(uint64_t out1[7], const uint64_t arg1[7], const uint64 } /* + * The function fiat_p484_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2049,6 +2071,12 @@ static void fiat_p484_square(uint64_t out1[7], const uint64_t arg1[7]) { } /* + * The function fiat_p484_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) + eval (fiat_p484_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] + * ∧ 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]] @@ -2125,6 +2153,12 @@ static void fiat_p484_add(uint64_t out1[7], const uint64_t arg1[7], const uint64 } /* + * The function fiat_p484_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) - eval (fiat_p484_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] + * ∧ 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]] @@ -2186,6 +2220,11 @@ static void fiat_p484_sub(uint64_t out1[7], const uint64_t arg1[7], const uint64 } /* + * The function fiat_p484_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_p484_from_montgomery out1) mod m = -eval (fiat_p484_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2246,6 +2285,11 @@ static void fiat_p484_opp(uint64_t out1[7], const uint64_t arg1[7]) { } /* + * The function fiat_p484_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 1324863811396206510028543369708678912454650048974215908631025180695212704414528066624039943565284982500305666048^7) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2889,6 +2933,9 @@ static void fiat_p484_from_montgomery(uint64_t out1[7], const uint64_t arg1[7]) } /* + * The function fiat_p484_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_p484_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -2900,6 +2947,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -2932,6 +2981,9 @@ static void fiat_p484_selectznz(uint64_t out1[7], fiat_p484_uint1 arg1, const ui } /* + * The function fiat_p484_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x3ffffffffffff]] * Output Bounds: @@ -3107,6 +3159,11 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) { } /* + * The function fiat_p484_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] + * ∧ 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: @@ -17,6 +17,9 @@ typedef unsigned __int128 fiat_p521_uint128; /* + * The function fiat_p521_addcarryx_u30 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^30 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^30⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3fffffff] @@ -34,6 +37,9 @@ static void fiat_p521_addcarryx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_ } /* + * The function fiat_p521_subborrowx_u30 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^30 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^30⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3fffffff] @@ -51,6 +57,9 @@ static void fiat_p521_subborrowx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat } /* + * The function fiat_p521_addcarryx_u31 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^31 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^31⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7fffffff] @@ -68,6 +77,9 @@ static void fiat_p521_addcarryx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat_ } /* + * The function fiat_p521_subborrowx_u31 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^31 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^31⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x7fffffff] @@ -85,6 +97,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -100,6 +114,8 @@ static void fiat_p521_cmovznz_u32(uint32_t* out1, fiat_p521_uint1 arg1, uint32_t } /* + * The function fiat_p521_carry_mul does stuff. + * 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]] @@ -490,6 +506,8 @@ static void fiat_p521_carry_mul(uint32_t out1[17], const uint64_t arg1[17], cons } /* + * The function fiat_p521_carry_square does stuff. + * 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: @@ -775,6 +793,8 @@ static void fiat_p521_carry_square(uint32_t out1[17], const uint64_t arg1[17]) { } /* + * The function fiat_p521_carry does stuff. + * 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: @@ -837,6 +857,8 @@ static void fiat_p521_carry(uint32_t out1[17], const uint64_t arg1[17]) { } /* + * The function fiat_p521_add does stuff. + * 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]] @@ -881,6 +903,8 @@ static void fiat_p521_add(uint64_t out1[17], const uint32_t arg1[17], const uint } /* + * The function fiat_p521_sub does stuff. + * 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]] @@ -925,6 +949,8 @@ static void fiat_p521_sub(uint64_t out1[17], const uint32_t arg1[17], const uint } /* + * The function fiat_p521_opp does stuff. + * 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: @@ -968,6 +994,8 @@ 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) * 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]] @@ -1030,6 +1058,8 @@ static void fiat_p521_selectznz(uint32_t out1[17], fiat_p521_uint1 arg1, const u } /* + * The function fiat_p521_to_bytes does stuff. + * 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: @@ -1365,6 +1395,8 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) { } /* + * The function fiat_p521_from_bytes does stuff. + * 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: @@ -17,6 +17,9 @@ typedef unsigned __int128 fiat_p521_uint128; /* + * The function fiat_p521_addcarryx_u58 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^58 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffffffffffff] @@ -34,6 +37,9 @@ static void fiat_p521_addcarryx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_ } /* + * The function fiat_p521_subborrowx_u58 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^58 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x3ffffffffffffff] @@ -51,6 +57,9 @@ static void fiat_p521_subborrowx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat } /* + * The function fiat_p521_addcarryx_u57 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^57 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffffffffffff] @@ -68,6 +77,9 @@ static void fiat_p521_addcarryx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_ } /* + * The function fiat_p521_subborrowx_u57 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^57 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffffffffffff] @@ -85,6 +97,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -100,6 +114,8 @@ static void fiat_p521_cmovznz_u64(uint64_t* out1, fiat_p521_uint1 arg1, uint64_t } /* + * The function fiat_p521_carry_mul does stuff. + * 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]] @@ -242,6 +258,8 @@ static void fiat_p521_carry_mul(uint64_t out1[9], const uint64_t arg1[9], const } /* + * The function fiat_p521_carry_square does stuff. + * 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: @@ -363,6 +381,8 @@ static void fiat_p521_carry_square(uint64_t out1[9], const uint64_t arg1[9]) { } /* + * The function fiat_p521_carry does stuff. + * 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: @@ -401,6 +421,8 @@ static void fiat_p521_carry(uint64_t out1[9], const uint64_t arg1[9]) { } /* + * The function fiat_p521_add does stuff. + * 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]] @@ -429,6 +451,8 @@ static void fiat_p521_add(uint64_t out1[9], const uint64_t arg1[9], const uint64 } /* + * The function fiat_p521_sub does stuff. + * 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]] @@ -457,6 +481,8 @@ static void fiat_p521_sub(uint64_t out1[9], const uint64_t arg1[9], const uint64 } /* + * The function fiat_p521_opp does stuff. + * 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: @@ -484,6 +510,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -522,6 +550,8 @@ static void fiat_p521_selectznz(uint64_t out1[9], fiat_p521_uint1 arg1, const ui } /* + * The function fiat_p521_to_bytes does stuff. + * 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: @@ -793,6 +823,8 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { } /* + * The function fiat_p521_from_bytes does stuff. + * 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 ec19bd1a9..19469b433 100644 --- a/secp256k1_32.c +++ b/secp256k1_32.c @@ -17,6 +17,9 @@ typedef signed char fiat_secp256k1_int1; /* + * The function fiat_secp256k1_addcarryx_u32 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^32 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -34,6 +37,9 @@ static void fiat_secp256k1_addcarryx_u32(uint32_t* out1, fiat_secp256k1_uint1* o } /* + * The function fiat_secp256k1_subborrowx_u32 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^32 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -51,6 +57,9 @@ static void fiat_secp256k1_subborrowx_u32(uint32_t* out1, fiat_secp256k1_uint1* } /* + * The function fiat_secp256k1_mulx_u32 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^32 + * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] @@ -67,6 +76,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] @@ -82,6 +93,12 @@ static void fiat_secp256k1_cmovznz_u32(uint32_t* out1, fiat_secp256k1_uint1 arg1 } /* + * The function fiat_secp256k1_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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]] @@ -1372,6 +1389,11 @@ static void fiat_secp256k1_mul(uint32_t out1[8], const uint32_t arg1[8], const u } /* + * The function fiat_secp256k1_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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: @@ -2661,6 +2683,12 @@ static void fiat_secp256k1_square(uint32_t out1[8], const uint32_t arg1[8]) { } /* + * The function fiat_secp256k1_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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]] @@ -2746,6 +2774,12 @@ static void fiat_secp256k1_add(uint32_t out1[8], const uint32_t arg1[8], const u } /* + * The function fiat_secp256k1_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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]] @@ -2814,6 +2848,11 @@ static void fiat_secp256k1_sub(uint32_t out1[8], const uint32_t arg1[8], const u } /* + * The function fiat_secp256k1_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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: @@ -2881,6 +2920,11 @@ static void fiat_secp256k1_opp(uint32_t out1[8], const uint32_t arg1[8]) { } /* + * The function fiat_secp256k1_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 95051438657476508368854739628211227342282034117213274825043523998796304009133^8) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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: @@ -3779,6 +3823,9 @@ static void fiat_secp256k1_from_montgomery(uint32_t out1[8], const uint32_t arg1 } /* + * The function fiat_secp256k1_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3790,6 +3837,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] @@ -3825,6 +3874,9 @@ static void fiat_secp256k1_selectznz(uint32_t out1[8], fiat_secp256k1_uint1 arg1 } /* + * The function fiat_secp256k1_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: @@ -3929,6 +3981,11 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { } /* + * The function fiat_secp256k1_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] + * ∧ 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 0481fab65..3dc5beeab 100644 --- a/secp256k1_64.c +++ b/secp256k1_64.c @@ -19,6 +19,9 @@ typedef unsigned __int128 fiat_secp256k1_uint128; /* + * The function fiat_secp256k1_addcarryx_u64 is an add with carry. + * out1 = (arg1 + arg2 + arg3) mod 2^64 + * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -36,6 +39,9 @@ static void fiat_secp256k1_addcarryx_u64(uint64_t* out1, fiat_secp256k1_uint1* o } /* + * The function fiat_secp256k1_subborrowx_u64 is a sub with borrow. + * out1 = (-arg1 + arg2 + -arg3) mod 2^64 + * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -53,6 +59,9 @@ static void fiat_secp256k1_subborrowx_u64(uint64_t* out1, fiat_secp256k1_uint1* } /* + * The function fiat_secp256k1_mulx_u64 is an extended multiplication. + * out1 = (arg1 * arg2) mod 2^64 + * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋ * Input Bounds: * arg1: [0x0 ~> 0xffffffffffffffff] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -69,6 +78,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffffffffffff] @@ -84,6 +95,12 @@ static void fiat_secp256k1_cmovznz_u64(uint64_t* out1, fiat_secp256k1_uint1 arg1 } /* + * The function fiat_secp256k1_mul does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -446,6 +463,11 @@ static void fiat_secp256k1_mul(uint64_t out1[4], const uint64_t arg1[4], const u } /* + * The function fiat_secp256k1_square does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -807,6 +829,12 @@ static void fiat_secp256k1_square(uint64_t out1[4], const uint64_t arg1[4]) { } /* + * The function fiat_secp256k1_add does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -856,6 +884,12 @@ static void fiat_secp256k1_add(uint64_t out1[4], const uint64_t arg1[4], const u } /* + * The function fiat_secp256k1_sub does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -896,6 +930,11 @@ static void fiat_secp256k1_sub(uint64_t out1[4], const uint64_t arg1[4], const u } /* + * The function fiat_secp256k1_opp does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -935,6 +974,11 @@ static void fiat_secp256k1_opp(uint64_t out1[4], const uint64_t arg1[4]) { } /* + * The function fiat_secp256k1_from_montgomery does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * eval out1 mod m = (eval arg1 * 97798581649299591516383885342152904135335272353249846763749256112567415731113^4) mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 0 ≤ eval out1 < m * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1197,6 +1241,9 @@ static void fiat_secp256k1_from_montgomery(uint64_t out1[4], const uint64_t arg1 } /* + * The function fiat_secp256k1_nonzero does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0 * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1208,6 +1255,8 @@ 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) * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] @@ -1231,6 +1280,9 @@ static void fiat_secp256k1_selectznz(uint64_t out1[4], fiat_secp256k1_uint1 arg1 } /* + * The function fiat_secp256k1_to_bytes does stuff. + * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m → + * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] * Output Bounds: @@ -1335,6 +1387,11 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { } /* + * The function fiat_secp256k1_from_bytes does stuff. + * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m → + * eval out1 mod m = bytes_eval arg1 mod m + * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] + * ∧ 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/BoundsPipeline.v b/src/BoundsPipeline.v index 2b74545f3..0299f2e9e 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -211,7 +211,7 @@ Module Pipeline. => ((["Computed bounds " ++ show true computed_bounds ++ " are not tight enough (expected bounds not looser than " ++ show true expected_bounds ++ ")."]%string) ++ [explain_too_loose_bounds (t:=type.base _) computed_bounds expected_bounds] ++ match ToString.C.ToFunctionLines - false (* do extra bounds check *) false (* static *) "" "f" nil syntax_tree None arg_bounds ZRange.type.base.option.None with + false (* do extra bounds check *) false (* static *) "" "f" syntax_tree (fun _ _ => nil) None arg_bounds ZRange.type.base.option.None with | inl (E_lines, types_used) => ["When doing bounds analysis on the syntax tree:"] ++ E_lines ++ [""] @@ -322,13 +322,13 @@ Module Pipeline. (static : bool) (type_prefix : string) (name : string) - (comment : list string) (with_dead_code_elimination : bool := true) (with_subst01 : bool) (translate_to_fancy : option to_fancy_args) (possible_values : list Z) {t} (E : Expr t) + (comment : type.for_each_lhs_of_arrow ToString.C.OfPHOAS.var_data t -> ToString.C.OfPHOAS.var_data (type.final_codomain t) -> list string) arg_bounds out_bounds : ErrorT (list string * ToString.C.ident_infos) @@ -340,7 +340,7 @@ Module Pipeline. E arg_bounds out_bounds in match E with | Success E' => let E := ToString.C.ToFunctionLines - true static type_prefix name comment E' None arg_bounds out_bounds in + true static type_prefix name E' comment None arg_bounds out_bounds in match E with | inl E => Success E | inr err => Error (Stringification_failed E' err) @@ -352,50 +352,53 @@ Module Pipeline. (static : bool) (type_prefix : string) (name : string) - (comment : list string) (with_dead_code_elimination : bool := true) (with_subst01 : bool) (translate_to_fancy : option to_fancy_args) relax_zrange {t} (E : Expr t) + (comment : type.for_each_lhs_of_arrow ToString.C.OfPHOAS.var_data t -> ToString.C.OfPHOAS.var_data (type.final_codomain t) -> list string) arg_bounds out_bounds : ErrorT (string * ToString.C.ident_infos) := let E := BoundsPipelineToStrings - static type_prefix name comment + static type_prefix name (*with_dead_code_elimination*) with_subst01 translate_to_fancy relax_zrange - E arg_bounds out_bounds in + E comment arg_bounds out_bounds in match E with | Success (E, types_used) => Success (ToString.C.LinesToString E, types_used) | Error err => Error err end. Local Notation arg_bounds_of_pipeline result - := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl) + := ((fun a b c t E arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c t E arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl) (only parsing). Local Notation out_bounds_of_pipeline result - := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl) + := ((fun a b c t E arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c t E arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl) (only parsing). Notation FromPipelineToString prefix name result - := (((prefix ++ name)%string, - match result with - | Success E' - => let E := ToString.C.ToFunctionLines - true true (* static *) prefix (prefix ++ name)%string [] E' None - (arg_bounds_of_pipeline result) - (out_bounds_of_pipeline result) in - match E with - | inl E => Success E - | inr err => Error (Pipeline.Stringification_failed E' err) - end - | Error err => Error err - end)). - + := (fun comment + => ((prefix ++ name)%string, + match result with + | Success E' + => let E := ToString.C.ToFunctionLines + true true (* static *) prefix (prefix ++ name)%string + E' + (comment (prefix ++ name)%string) + None + (arg_bounds_of_pipeline result) + (out_bounds_of_pipeline result) in + match E with + | inl E => Success E + | inr err => Error (Pipeline.Stringification_failed E' err) + end + | Error err => Error err + end)). Local Ltac wf_interp_t := repeat first [ progress destruct_head'_and diff --git a/src/CStringification.v b/src/CStringification.v index 5c73b8e26..d31fa55e8 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -784,6 +784,40 @@ Module Compilers. | type.arrow s d => Empty_set end. + Fixpoint base_var_names (t : base.type) : Set + := match t with + | base.type.unit + => unit + | base.type.nat + | base.type.bool + => Empty_set + | base.type.Z => string + | base.type.prod A B => base_var_names A * base_var_names B + | base.type.list A => string + end. + Definition var_names (t : Compilers.type.type base.type) : Set + := match t with + | type.base t => base_var_names t + | type.arrow s d => Empty_set + end. + + Fixpoint names_of_base_var_data {t} : base_var_data t -> base_var_names t + := match t return base_var_data t -> base_var_names t with + | base.type.unit + | base.type.nat + | base.type.bool + => fun x => x + | base.type.Z => @fst _ _ + | base.type.prod A B + => fun xy => (@names_of_base_var_data A (fst xy), @names_of_base_var_data B (snd xy)) + | base.type.list A => fun x => fst (fst x) + end. + Definition names_of_var_data {t} : var_data t -> var_names t + := match t with + | type.base t => names_of_base_var_data + | type.arrow _ _ => fun x => x + end. + Fixpoint arith_expr_for_base (t : base.type) : Set := match t with | base.type.Z @@ -2167,9 +2201,10 @@ Module Compilers. :: (List.map (fun s => " " ++ s)%string (to_strings prefix body))) ++ ["}"])%list. - Definition ToFunctionLines (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) (comment : list string) + Definition ToFunctionLines (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) {t} (e : @Compilers.expr.Expr base.type ident.ident t) + (comment : type.for_each_lhs_of_arrow var_data t -> var_data (type.final_codomain t) -> list string) (name_list : option (list string)) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (outbounds : ZRange.type.base.option.interp (type.final_codomain t)) @@ -2177,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) + ++ (List.map (fun s => " * " ++ s)%string (comment indata outdata)) ++ [" * Input Bounds:"] ++ List.map (fun v => " * " ++ v)%string (input_bounds_to_string indata inbounds) ++ [" * Output Bounds:"] @@ -2197,14 +2232,15 @@ Module Compilers. : string := String.concat String.NewLine lines. - Definition ToFunctionString (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) (comment : list string) + Definition ToFunctionString (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) {t} (e : @Compilers.expr.Expr base.type ident.ident t) + (comment : type.for_each_lhs_of_arrow var_data t -> var_data (type.final_codomain t) -> list string) (name_list : option (list string)) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (outbounds : ZRange.type.option.interp (type.final_codomain t)) : (string * ident_infos) + string - := match ToFunctionLines do_bounds_check static prefix name comment e name_list inbounds outbounds with + := match ToFunctionLines do_bounds_check static prefix name e comment name_list inbounds outbounds with | inl (ls, used_types) => inl (LinesToString ls, used_types) | inr err => inr err end. diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index 3e3e4e105..bc525412a 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -91,7 +91,10 @@ Section rbarrett_red. Definition sbarrett_red (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "barrett_red" barrett_red. + := Eval cbv beta in + FromPipelineToString + prefix "barrett_red" barrett_red + (fun _ _ _ => @nil string). (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v index 2b7841ac0..a452a047c 100644 --- a/src/PushButtonSynthesis/MontgomeryReduction.v +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -82,7 +82,10 @@ Section rmontred. Definition smontred (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "montred" montred. + := Eval cbv beta in + FromPipelineToString + prefix "montred" montred + (fun _ _ _ => @nil string). (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index f36f4cb9c..e45940369 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -133,19 +133,7 @@ Local Notation out_bounds_of_pipeline result (only parsing). Notation FromPipelineToString prefix name result - := (((prefix ++ name)%string, - match result with - | Success E' - => let E := ToString.C.ToFunctionLines - true true (* static *) prefix (prefix ++ name)%string [] E' None - (arg_bounds_of_pipeline result) - (out_bounds_of_pipeline result) in - match E with - | inl E => Success E - | inr err => Error (Pipeline.Stringification_failed E' err) - end - | Error err => Error err - end)). + := (Pipeline.FromPipelineToString prefix name result). Ltac prove_correctness use_curve_good := let Hres := match goal with H : _ = Success _ |- _ => H end in @@ -175,6 +163,419 @@ Ltac prove_correctness use_curve_good := | progress autorewrite with distr_length in * ] | .. ]. +Module CorrectnessStringification. + Module dyn_context. + Inductive list := + | nil + | cons {T1 T2} (k : T1) (v : T2) (ctx : list). + End dyn_context. + + Ltac strip_bounds_info correctness := + lazymatch correctness with + | (fun x : ?T => ?f) + => let fx := fresh in + constr:(fun x : T => match f return _ with + | fx => ltac:(let fx := (eval cbv [fx] in fx) in + let v := strip_bounds_info fx in + exact v) + end) + | ((lower ?r <=? ?v) && (?v <=? upper ?r))%bool%Z = true -> ?T + => strip_bounds_info T + | list_Z_bounded_by _ _ -> ?T + => strip_bounds_info T + | ?T /\ list_Z_bounded_by _ _ + => T + | ?T /\ (match _ with pair _ _ => _ end = true) + => T + | ?T /\ ((lower ?r <=? ?v) && (?v <=? upper ?r))%bool%Z = true + => T + | iff _ _ + => correctness + | _ = _ /\ (_ = _ /\ (_ <= _ < _)) + => correctness + | _ = _ :> list Z + => correctness + | forall x : ?T, ?f + => let fx := fresh in + constr:(forall x : T, match f return _ with + | fx => ltac:(let fx := (eval cbv [fx] in fx) in + let v := strip_bounds_info fx in + exact v) + end) + | ?T + => let __ := match goal with _ => idtac "Unrecognized bounds component:" T end in + constr:(I : I) + end. + + Ltac with_assoc_list ctx correctness arg_var_names out_var_names cont := + lazymatch correctness with + | (fun x : ?T => ?f) + => let fx := fresh in + constr:(fun x : T + => match f return _ with + | fx + => ltac:(let fx' := (eval cbv delta [fx] in fx) in + clear fx; + let ret := with_assoc_list + (dyn_context.cons x out_var_names ctx) + fx' + arg_var_names + () + cont in + exact ret) + end) + | _ + => let T := type of arg_var_names in + lazymatch (eval hnf in T) with + | prod _ _ + => lazymatch correctness with + | (forall x : ?T, ?f) + => let fx := fresh in + constr:(fun x : T + => match f return _ with + | fx + => ltac:(let fx' := (eval cbv delta [fx] in fx) in + clear fx; + let ret := with_assoc_list + (dyn_context.cons x (fst arg_var_names) ctx) + fx' + (snd arg_var_names) + out_var_names + cont in + exact ret) + end) + | ?T + => cont ctx T + end + | _ => cont ctx correctness + end + end. + + Ltac maybe_parenthesize str natural cur_lvl := + let should_paren := (eval cbv in (Z.ltb cur_lvl natural)) in + lazymatch should_paren with + | true => constr:(("(" ++ str ++ ")")%string) + | false => str + end. + + Ltac find_head_in_ctx' ctx x cont := + let h := head x in + lazymatch ctx with + | context[dyn_context.cons h ?name _] => cont name + | context[dyn_context.cons x ?name _] => cont name + | _ => lazymatch x with + | fst ?x + => find_head_in_ctx' ctx x ltac:(fun x => cont (fst x)) + | snd ?x + => find_head_in_ctx' ctx x ltac:(fun x => cont (snd x)) + | _ => constr:(@None string) + end + end. + Ltac find_head_in_ctx ctx x := + find_head_in_ctx' ctx x ltac:(fun x => constr:(Some x)). + + Ltac find_in_ctx' ctx x cont := + lazymatch ctx with + | context[dyn_context.cons x ?name _] => cont name + | _ => lazymatch x with + | fst ?x + => find_in_ctx' ctx x ltac:(fun x => cont (fst x)) + | snd ?x + => find_in_ctx' ctx x ltac:(fun x => cont (snd x)) + | _ => constr:(@None string) + end + end. + Ltac find_in_ctx ctx x := + find_in_ctx' ctx x ltac:(fun x => constr:(Some x)). + + Ltac test_is_var v := + constr:(ltac:(tryif is_var v then exact true else exact false)). + + Local Open Scope string_scope. + + Ltac fresh_from' ctx check_list start_val := + lazymatch check_list with + | cons ?n ?check_list + => lazymatch ctx with + | context[dyn_context.cons _ n] + => fresh_from' ctx check_list start_val + | _ => n + end + | _ + => let n := (eval cbv in ("x" ++ decimal_string_of_Z start_val)) in + lazymatch ctx with + | context[dyn_context.cons _ n] + => fresh_from' ctx check_list (Z.succ start_val) + | _ => n + end + end. + + Ltac fresh_from ctx := fresh_from' ctx ["x"; "y"; "z"] 0%Z. + + Ltac stringify_function_binders ctx correctness stringify_body := + lazymatch correctness with + | (fun x : ?T => ?f) + => let fx := fresh in + let xn := fresh_from ctx in + lazymatch + constr:( + fun x : T + => match f return string with + | fx + => ltac:( + let fx' := (eval cbv delta [fx] in fx) in + clear fx; + let res := stringify_function_binders + (dyn_context.cons x xn ctx) + fx' + stringify_body in + exact (" " ++ xn ++ res)) + end) with + | fun _ => ?f => f + | ?F => let __ := match goal with _ => idtac "Failed to eliminate functional dependencies in" F end in + constr:(I : I) + end + | ?v => let res := stringify_body ctx v in + constr:(", " ++ res) + end. + + Ltac is_literal x := + lazymatch x with + | O => true + | S ?x => is_literal x + | _ => false + end. + + Ltac stringify_rec0 evalf ctx correctness lvl := + let recurse v lvl := stringify_rec0 evalf ctx v lvl in + let name_of_var := find_head_in_ctx ctx correctness in + let weightf := lazymatch evalf with eval ?weightf _ => weightf | _ => I end in + let stringify_if testv t f := + let stest := recurse testv 200 in + let st := recurse t 200 in + let sf := recurse f 200 in + maybe_parenthesize (("if " ++ stest ++ " then " ++ st ++ " else " ++ sf)%string) 200 lvl in + let show_Z _ := + maybe_parenthesize (Show.Decimal.show_Z false correctness) 1 lvl in + let show_nat _ := + maybe_parenthesize (Show.Decimal.show_nat false correctness) 1 lvl in + let stringify_prefix f natural arg_lvl := + lazymatch correctness with + | ?F ?x + => let sx := recurse x arg_lvl in + maybe_parenthesize (f ++ sx)%string natural lvl + end in + let stringify_postfix f natural arg_lvl := + lazymatch correctness with + | ?F ?x + => let sx := recurse x arg_lvl in + maybe_parenthesize (sx ++ f)%string natural lvl + end in + let stringify_infix' lvl space f natural l_lvl r_lvl := + lazymatch correctness with + | ?F ?x ?y + => let sx := recurse x l_lvl in + let sy := recurse y r_lvl in + maybe_parenthesize (sx ++ space ++ f ++ space ++ sy)%string natural lvl + end in + let stringify_infix := stringify_infix' lvl " " in + let stringify_infix_without_space := stringify_infix' lvl "" in + let stringify_infix2 f1 f2 natural l_lvl c_lvl r_lvl := + lazymatch correctness with + | and (?F1 ?x ?y) (?F2 ?y ?z) + => let sx := recurse x l_lvl in + let sy := recurse y c_lvl in + let sz := recurse z r_lvl in + maybe_parenthesize (sx ++ " " ++ f1 ++ " " ++ sy ++ " " ++ f2 ++ " " ++ sz)%string natural lvl + end in + let name_of_fun := + lazymatch correctness with + | ?f ?x => find_in_ctx ctx f + | _ => constr:(@None string) + end in + lazymatch constr:((name_of_var, name_of_fun)) with + | (Some ?name, _) + => maybe_parenthesize name 1 lvl + | (None, Some ?name) + => lazymatch correctness with + | ?f ?x + => let sx := recurse x 9 in + maybe_parenthesize ((name ++ " " ++ sx)%string) 10 lvl + end + | (None, None) + => lazymatch correctness with + | ?x = ?y :> ?T + => lazymatch (eval cbv in T) with + | Z => let sx := recurse x 69 in + let sy := recurse y 69 in + maybe_parenthesize ((sx ++ " = " ++ sy)%string) 70 lvl + | list Z + => let sx := recurse x 69 in + let sy := recurse y 69 in + maybe_parenthesize ((sx ++ " = " ++ sy)%string) 70 lvl + | prod ?A ?B + => let v := (eval cbn [fst snd] in (fst x = fst y /\ snd x = snd y)) in + recurse v lvl + | ?T' => let __ := match goal with _ => idtac "Error: Unrecognized type for equality:" T' end in + constr:(I : I) + end + | evalf ?v + => let sv := recurse v 9 in + maybe_parenthesize (("eval " ++ sv)%string) 10 lvl + | weightf ?v + => let sv := recurse v 9 in + maybe_parenthesize (("weight " ++ sv)%string) 10 lvl + | eval (weight 8 1) _ ?v + => let sv := recurse v 9 in + maybe_parenthesize (("bytes_eval " ++ sv)%string) 10 lvl + | UniformWeight.uweight ?machine_wordsize ?v + => recurse (2^(machine_wordsize * Z.of_nat v)) lvl + | weight 8 1 ?i + => recurse (2^(8 * Z.of_nat i)) lvl + | List.map ?x ?y + => let sx := recurse x 9 in + let sy := recurse y 9 in + maybe_parenthesize (("map " ++ sx ++ " " ++ sy)%string) 10 lvl + | match ?testv with true => ?t | false => ?f end + => stringify_if testv t f + | match ?testv with or_introl _ => ?t | or_intror _ => ?f end + => stringify_if testv t f + | match ?testv with left _ => ?t | right _ => ?f end + => stringify_if testv t f + | Decidable.dec ?p + => recurse p lvl + | Z0 => show_Z () + | Zpos _ => show_Z () + | Zneg _ => show_Z () + | O => show_nat () + | S ?x + => let is_lit := is_literal x in + lazymatch is_lit with + | true => show_nat () + | false => recurse (x + 1)%nat lvl + end + | Z.of_nat ?x => recurse x lvl + | ?x <= ?y < ?z => stringify_infix2 "≤" "<" 70 69 69 69 + | ?x <= ?y <= ?z => stringify_infix2 "≤" "≤" 70 69 69 69 + | ?x < ?y <= ?z => stringify_infix2 "<" "≤" 70 69 69 69 + | ?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.mul _ _ => stringify_infix "*" 40 40 39 + | Z.pow _ _ => stringify_infix_without_space "^" 30 29 30 + | Z.add _ _ => stringify_infix "+" 50 50 49 + | Z.sub _ _ => stringify_infix "-" 50 50 49 + | Z.opp _ => stringify_prefix "-" 35 35 + | Z.le _ _ => stringify_infix "≤" 70 69 69 + | Z.lt _ _ => stringify_infix "<" 70 69 69 + | Nat.mul _ _ => stringify_infix "*" 40 40 39 + | Nat.pow _ _ => stringify_infix "^" 30 29 30 + | Nat.add _ _ => stringify_infix "+" 50 50 49 + | Nat.sub _ _ => stringify_infix "-ℕ" 50 50 49 + | Z.div _ _ + => let res := stringify_infix' 69 " " "/" 40 40 39 in + maybe_parenthesize ("⌊" ++ res ++ "⌋") 9 lvl + | List.seq ?x ?y + => let sx := recurse x 9 in + let sy := recurse (pred y) 9 in + constr:("[" ++ sx ++ ".." ++ sy ++ "]") + | pred ?n + => let iv := test_is_var n in + let il := is_literal n in + lazymatch (eval cbv in (orb il iv)) with + | true => show_nat () + | false + => recurse (n - 1)%nat lvl + end + | fun x : ?T => ?f + => let slam := stringify_function_binders ctx correctness ltac:(fun ctx body => stringify_rec0 evalf ctx body 200) in + maybe_parenthesize ("λ" ++ slam) 200 lvl + | ?v + => let iv := test_is_var v in + lazymatch iv with + | true + => let T := type of v in + lazymatch (eval hnf in T) with + | Z => show_Z () + | nat => show_nat () + | _ + => let __ := match goal with _ => idtac "Error: Unrecognized var:" v " in " ctx end in + constr:(I : I) + end + | false + => let __ := match goal with _ => idtac "Error: Unrecognized term:" v " in " ctx end in + constr:(I : I) + end + end + end. + + Ltac stringify_rec prefix evalf ctx correctness lvl := + let recurse' prefix v lvl := stringify_rec prefix evalf ctx v lvl in + let recurse := recurse' "" in + let default _ := let v := stringify_rec0 evalf ctx correctness lvl in + constr:((prefix ++ v)::nil) in + lazymatch correctness with + | ?A -> ?B + => let sA := stringify_rec0 evalf ctx A 98 in + let sB := recurse B 200 in + constr:((prefix ++ sA ++ " →")%string :: sB) + | _ <= _ < _ => 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) + | ?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 + | _ + => default () + end. + + Ltac strip_lambdas v := + lazymatch v with + | fun _ => ?f => strip_lambdas f + | ?v => v + end. + + Ltac stringify ctx correctness evalf fname arg_var_data out_var_data := + let G := match goal with |- ?G => G end in + let correctness := (eval hnf in correctness) in + let correctness := (eval cbv [Partition.partition Arithmetic.WordByWordMontgomery.valid Arithmetic.WordByWordMontgomery.small] in correctness) in + let correctness := strip_bounds_info correctness in + let arg_var_names := constr:(type.map_for_each_lhs_of_arrow (@ToString.C.OfPHOAS.names_of_var_data) arg_var_data) in + let out_var_names := constr:(ToString.C.OfPHOAS.names_of_base_var_data out_var_data) in + let res := with_assoc_list + ctx + correctness + arg_var_names + out_var_names + ltac:( + fun ctx T + => let v := stringify_rec "" evalf ctx T 200 in refine v + ) in + let res := strip_lambdas res in + res. + + Notation stringify_correctness_with_ctx ctx evalf pre_extra correctness + := (fun fname arg_var_data out_var_data + => ltac:(let res := stringify ctx correctness evalf fname arg_var_data out_var_data in + refine (List.app (pre_extra fname) res))) (only parsing). + Notation stringify_correctness evalf pre_extra correctness + := (match dyn_context.nil with + | ctx' => stringify_correctness_with_ctx ctx' evalf pre_extra correctness + end) + (only parsing). +End CorrectnessStringification. + +Notation stringify_correctness_with_ctx ctx evalf pre_extra correctness + := (CorrectnessStringification.stringify_correctness_with_ctx ctx evalf pre_extra correctness) (only parsing). +Notation stringify_correctness evalf pre_extra correctness + := (CorrectnessStringification.stringify_correctness evalf pre_extra correctness) (only parsing). + Section __. Context (n : nat) (machine_wordsize : Z). @@ -199,6 +600,9 @@ Section __. Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. Hint Rewrite length_saturated_bounds_list : distr_length. + Local Notation dummy_weight := (weight 0 0). + Local Notation evalf := (eval dummy_weight n). + Definition selectznz := Pipeline.BoundsPipeline false (* subst01 *) @@ -210,7 +614,13 @@ Section __. Definition sselectznz (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "selectznz" selectznz. + := Eval cbv beta in + FromPipelineToString + prefix "selectznz" selectznz + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is a multi-limb conditional select."]%string) + (selectznz_correct dummy_weight n saturated_bounds_list)). Definition mulx (s : Z) := Pipeline.BoundsPipeline @@ -224,7 +634,13 @@ Section __. Definition smulx (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s). + := Eval cbv beta in + FromPipelineToString + prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is an extended multiplication."]%string) + (mulx_correct s)). Definition addcarryx (s : Z) := Pipeline.BoundsPipeline @@ -236,9 +652,16 @@ Section __. (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange (Some r[0~>2^s-1], Some r[0~>1])%zrange. + Definition saddcarryx (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s). + := Eval cbv beta in + FromPipelineToString + prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is an add with carry."]%string) + (addcarryx_correct s)). Definition subborrowx (s : Z) := Pipeline.BoundsPipeline @@ -252,7 +675,14 @@ Section __. Definition ssubborrowx (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s). + := Eval cbv beta in + FromPipelineToString + prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is a sub with borrow."]%string) + (subborrowx_correct s)). + Definition cmovznz (s : Z) := Pipeline.BoundsPipeline @@ -266,7 +696,13 @@ Section __. Definition scmovznz (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s). + := Eval cbv beta in + FromPipelineToString + prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is a single-word conditional move."]%string) + (cmovznz_correct s)). Local Ltac solve_extra_bounds_side_conditions := cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 334c2a475..7ff799c80 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -135,6 +135,17 @@ Section __. { use_curve_good_t. } Qed. + Local Notation weightf := (weight machine_wordsize 1). + Local Notation evalf := (eval weightf n). + Local Notation initial_ctx := (CorrectnessStringification.dyn_context.nil). + Local Notation stringify_correctness pre_extra correctness + := (stringify_correctness_with_ctx + initial_ctx + evalf + pre_extra + correctness) + (only parsing). + Definition mul := Pipeline.BoundsPipeline false (* subst01 *) @@ -147,7 +158,12 @@ Section __. Definition smul (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "mul" mul. + := Eval cbv beta in + FromPipelineToString + prefix "mul" mul + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (mul_correct weightf n m boundsn)). Local Ltac solve_extra_bounds_side_conditions := cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. diff --git a/src/PushButtonSynthesis/SmallExamples.v b/src/PushButtonSynthesis/SmallExamples.v index 09f361356..daa50c9e9 100644 --- a/src/PushButtonSynthesis/SmallExamples.v +++ b/src/PushButtonSynthesis/SmallExamples.v @@ -43,53 +43,59 @@ Compute Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_mulx_u64" [] + true "fiat_" "fiat_mulx_u64" true None [64; 128] ltac:(let r := Reify (Arithmetic.mulx 64) in exact r) + (fun _ _ => []) (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange (Some r[0~>2^64-1], Some r[0~>2^64-1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u64" [] + true "fiat_" "fiat_addcarryx_u64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.addcarryx 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u51" [] + true "fiat_" "fiat_addcarryx_u51" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.addcarryx 51) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange (Some r[0~>2^51-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u64" [] + true "fiat_" "fiat_subborrowx_u64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.subborrowx 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u51" [] + true "fiat_" "fiat_subborrowx_u51" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.subborrowx 51) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange (Some r[0~>2^51-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_cmovznz64" [] + true "fiat_" "fiat_cmovznz64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.cmovznz 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1])%zrange). diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index 8923aa10e..75e430a24 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -258,6 +258,17 @@ else: { use_curve_good_t. } Qed. + Local Notation weightf := (weight (Qnum limbwidth) (QDen limbwidth)). + Local Notation evalf := (eval weightf n). + Local Notation initial_ctx := (CorrectnessStringification.dyn_context.cons m "m"%string CorrectnessStringification.dyn_context.nil). + Local Notation stringify_correctness pre_extra correctness + := (stringify_correctness_with_ctx + initial_ctx + evalf + pre_extra + correctness) + (only parsing). + Definition carry_mul := Pipeline.BoundsPipeline false (* subst01 *) @@ -270,7 +281,12 @@ else: Definition scarry_mul (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry_mul" carry_mul. + := Eval cbv beta in + FromPipelineToString + prefix "carry_mul" carry_mul + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_mul_correct weightf n m tight_bounds loose_bounds)). Definition carry_square := Pipeline.BoundsPipeline @@ -284,7 +300,12 @@ else: Definition scarry_square (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry_square" carry_square. + := Eval cbv beta in + FromPipelineToString + prefix "carry_square" carry_square + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_square_correct weightf n m tight_bounds loose_bounds)). Definition carry_scmul_const (x : Z) := Pipeline.BoundsPipeline @@ -298,7 +319,12 @@ else: Definition scarry_scmul_const (prefix : string) (x : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x). + := Eval cbv beta in + FromPipelineToString + prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x) + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_scmul_const_correct weightf n m tight_bounds loose_bounds x)). Definition carry := Pipeline.BoundsPipeline @@ -312,7 +338,12 @@ else: Definition scarry (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry" carry. + := Eval cbv beta in + FromPipelineToString + prefix "carry" carry + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_correct weightf n m tight_bounds loose_bounds)). Definition add := Pipeline.BoundsPipeline @@ -326,7 +357,12 @@ else: Definition sadd (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "add" add. + := Eval cbv beta in + FromPipelineToString + prefix "add" add + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (add_correct weightf n m tight_bounds loose_bounds)). Definition sub := Pipeline.BoundsPipeline @@ -340,7 +376,12 @@ else: Definition ssub (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "sub" sub. + := Eval cbv beta in + FromPipelineToString + prefix "sub" sub + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (sub_correct weightf n m tight_bounds loose_bounds)). Definition opp := Pipeline.BoundsPipeline @@ -354,7 +395,12 @@ else: Definition sopp (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "opp" opp. + := Eval cbv beta in + FromPipelineToString + prefix "opp" opp + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (opp_correct weightf n m tight_bounds loose_bounds)). Definition to_bytes := Pipeline.BoundsPipeline @@ -368,7 +414,12 @@ else: Definition sto_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "to_bytes" to_bytes + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (to_bytes_correct weightf n n_bytes m tight_bounds)). Definition from_bytes := Pipeline.BoundsPipeline @@ -382,7 +433,12 @@ else: Definition sfrom_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "from_bytes" from_bytes + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (from_bytes_correct weightf n n_bytes m s tight_bounds)). Definition encode := Pipeline.BoundsPipeline @@ -396,7 +452,12 @@ else: Definition sencode (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "encode" encode. + := Eval cbv beta in + FromPipelineToString + prefix "encode" encode + (stringify_correctness + (fun fname : string => [fname ++ ":"]%string) + (encode_correct weightf n m tight_bounds)). Definition zero := Pipeline.BoundsPipeline @@ -410,7 +471,12 @@ else: Definition szero (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "zero" zero. + := Eval cbv beta in + FromPipelineToString + prefix "zero" zero + (stringify_correctness + (fun fname : string => @nil string) + (zero_correct weightf n m tight_bounds)). Definition one := Pipeline.BoundsPipeline @@ -424,7 +490,12 @@ else: Definition sone (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "one" one. + := Eval cbv beta in + FromPipelineToString + prefix "one" one + (stringify_correctness + (fun fname : string => @nil string) + (one_correct weightf n m tight_bounds)). Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. Definition sselectznz (prefix : string) diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index a97c829e2..f64e4a8c3 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -223,6 +223,28 @@ Section __. Qed. + Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). + Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). + + Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). + + Local Notation evalf := (@eval machine_wordsize n). + Local Notation initial_ctx prefix + := (CorrectnessStringification.dyn_context.cons + m "m"%string + (CorrectnessStringification.dyn_context.cons + from_montgomery_res (prefix ++ "from_montgomery")%string + (CorrectnessStringification.dyn_context.cons + (@eval 8 n_bytes) "bytes_eval"%string + CorrectnessStringification.dyn_context.nil))). + Local Notation stringify_correctness prefix pre_extra correctness + := (stringify_correctness_with_ctx + (initial_ctx prefix) + evalf + pre_extra + correctness) + (only parsing). + Definition mul := Pipeline.BoundsPipeline false (* subst01 *) @@ -235,7 +257,13 @@ Section __. Definition smul (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "mul" mul. + := Eval cbv beta in + FromPipelineToString + prefix "mul" mul + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (mul_correct machine_wordsize n m valid from_montgomery_res)). Definition square := Pipeline.BoundsPipeline @@ -249,7 +277,13 @@ Section __. Definition ssquare (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "square" square. + := Eval cbv beta in + FromPipelineToString + prefix "square" square + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (square_correct machine_wordsize n m valid from_montgomery_res)). Definition add := Pipeline.BoundsPipeline @@ -263,7 +297,13 @@ Section __. Definition sadd (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "add" add. + := Eval cbv beta in + FromPipelineToString + prefix "add" add + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (add_correct machine_wordsize n m valid from_montgomery_res)). Definition sub := Pipeline.BoundsPipeline @@ -277,7 +317,13 @@ Section __. Definition ssub (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "sub" sub. + := Eval cbv beta in + FromPipelineToString + prefix "sub" sub + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (sub_correct machine_wordsize n m valid from_montgomery_res)). Definition opp := Pipeline.BoundsPipeline @@ -291,7 +337,13 @@ Section __. Definition sopp (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "opp" opp. + := Eval cbv beta in + FromPipelineToString + prefix "opp" opp + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (opp_correct machine_wordsize n m valid from_montgomery_res)). Definition from_montgomery := Pipeline.BoundsPipeline @@ -305,7 +357,13 @@ Section __. Definition sfrom_montgomery (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_montgomery" from_montgomery. + := Eval cbv beta in + FromPipelineToString + prefix "from_montgomery" from_montgomery + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (from_montgomery_correct machine_wordsize n m r' valid)). Definition nonzero := Pipeline.BoundsPipeline @@ -318,7 +376,13 @@ Section __. Definition snonzero (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "nonzero" nonzero. + := Eval cbv beta in + FromPipelineToString + prefix "nonzero" nonzero + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (nonzero_correct machine_wordsize n m valid from_montgomery_res)). Definition to_bytes := Pipeline.BoundsPipeline @@ -332,7 +396,13 @@ Section __. Definition sto_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "to_bytes" to_bytes + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (to_bytes_correct machine_wordsize n n_bytes m valid)). Definition from_bytes := Pipeline.BoundsPipeline @@ -346,7 +416,13 @@ Section __. Definition sfrom_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "from_bytes" from_bytes + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid)). Definition encode := Pipeline.BoundsPipeline @@ -360,7 +436,13 @@ Section __. Definition sencode (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "encode" encode. + := Eval cbv beta in + FromPipelineToString + prefix "encode" encode + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (encode_correct machine_wordsize n m valid from_montgomery_res)). Definition zero := Pipeline.BoundsPipeline @@ -374,7 +456,13 @@ Section __. Definition szero (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "zero" zero. + := Eval cbv beta in + FromPipelineToString + prefix "zero" zero + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (zero_correct machine_wordsize n m valid from_montgomery_res)). Definition one := Pipeline.BoundsPipeline @@ -388,16 +476,19 @@ Section __. Definition sone (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "one" one. + := Eval cbv beta in + FromPipelineToString + prefix "one" one + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (one_correct machine_wordsize n m valid from_montgomery_res)). Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. Definition sselectznz (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) := Primitives.sselectznz n machine_wordsize prefix. - Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). - Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). - Lemma bounded_by_of_valid x (H : valid x) : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some bounds) x = true. @@ -618,8 +709,6 @@ Section __. reified_from_montgomery` (the post-pipeline version), and take in success of the pipeline on `from_montgomery` as well? *) - Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). - Lemma mul_correct res (Hres : mul = Success res) : mul_correct machine_wordsize n m valid from_montgomery_res (Interp res). diff --git a/src/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v index a84455a6c..9bac61295 100644 --- a/src/SlowPrimeSynthesisExamples.v +++ b/src/SlowPrimeSynthesisExamples.v @@ -73,12 +73,12 @@ Section debugging_p448. true (* static *) "" (* prefix *) "mul" - [] (* comment *) false (* subst01 *) None (* fancy *) possible_values ltac:(let r := Reify ((carry_mulmod limbwidth_num limbwidth_den s c n [3; 7; 4; 0; 5; 1; 6; 2; 7; 3; 4; 0]%nat)) in exact r) + (fun _ _ => []) (* comment *) (Some loose_bounds, (Some loose_bounds, tt)) (Some tight_bounds). |