Add some primes to be synthesized

1 files changed, 84 insertions, 99 deletions

diff --git a/p256_64.c b/p256_64.c
index 1449d3175..56cb29fbc 100644
--- a/p256_64.c
+++ b/p256_64.c
@@ -4,6 +4,13 @@
 /* s = 0x10000000000000000000000000000000000000000000000000000000000000000 (from "2^256") */
 /* c = [(26959946667150639794667015087019630673637144422540572481103610249216, 1), (6277101735386680763835789423207666416102355444464034512896, -1), (79228162514264337593543950336, -1), (1, 1)] (from "2^224,1;2^192,-1;2^96,-1;1,1") */
 /* machine_wordsize = 64 (from "64") */
+/*                                                                    */
+/* NOTE: In addition to the bounds specified above each function, all */
+/*   functions synthesized for this Montgomery arithmetic require the */
+/*   input to be strictly less than the prime modulus (s-c), and also */
+/*   require the input to be in the unique saturated representation.  */
+/*   All functions also ensure that these two properties are true of  */
+/*   return values.                                                   */
 
 #include <stdint.h>
 typedef unsigned char fiat_p256_uint1;
@@ -1159,129 +1166,107 @@ static void fiat_p256_selectznz(uint64_t out1[4], fiat_p256_uint1 arg1, const ui
  *   out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
  */
 static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
-  uint64_t x1;
-  fiat_p256_uint1 x2;
-  fiat_p256_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0xffffffffffffffff));
-  uint64_t x3;
-  fiat_p256_uint1 x4;
-  fiat_p256_subborrowx_u64(&x3, &x4, x2, (arg1[1]), UINT32_C(0xffffffff));
-  uint64_t x5;
-  fiat_p256_uint1 x6;
-  fiat_p256_subborrowx_u64(&x5, &x6, x4, (arg1[2]), 0x0);
-  uint64_t x7;
-  fiat_p256_uint1 x8;
-  fiat_p256_subborrowx_u64(&x7, &x8, x6, (arg1[3]), UINT64_C(0xffffffff00000001));
-  uint64_t x9;
-  fiat_p256_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff));
-  uint64_t x10;
-  fiat_p256_uint1 x11;
-  fiat_p256_addcarryx_u64(&x10, &x11, 0x0, (x9 & UINT64_C(0xffffffffffffffff)), x1);
-  uint64_t x12;
-  fiat_p256_uint1 x13;
-  fiat_p256_addcarryx_u64(&x12, &x13, x11, (x9 & UINT32_C(0xffffffff)), x3);
-  uint64_t x14;
-  fiat_p256_uint1 x15;
-  fiat_p256_addcarryx_u64(&x14, &x15, x13, 0x0, x5);
-  uint64_t x16;
-  fiat_p256_uint1 x17;
-  fiat_p256_addcarryx_u64(&x16, &x17, x15, (x9 & UINT64_C(0xffffffff00000001)), x7);
-  uint64_t x18 = (x10 >> 8);
-  uint8_t x19 = (uint8_t)(x10 & UINT8_C(0xff));
-  uint64_t x20 = (x18 >> 8);
-  uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff));
-  uint64_t x22 = (x20 >> 8);
-  uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff));
+  uint64_t x1 = (arg1[3]);
+  uint64_t x2 = (arg1[2]);
+  uint64_t x3 = (arg1[1]);
+  uint64_t x4 = (arg1[0]);
+  uint64_t x5 = (x4 >> 8);
+  uint8_t x6 = (uint8_t)(x4 & UINT8_C(0xff));
+  uint64_t x7 = (x5 >> 8);
+  uint8_t x8 = (uint8_t)(x5 & UINT8_C(0xff));
+  uint64_t x9 = (x7 >> 8);
+  uint8_t x10 = (uint8_t)(x7 & UINT8_C(0xff));
+  uint64_t x11 = (x9 >> 8);
+  uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff));
+  uint64_t x13 = (x11 >> 8);
+  uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff));
+  uint64_t x15 = (x13 >> 8);
+  uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
+  uint8_t x17 = (uint8_t)(x15 >> 8);
+  uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff));
+  fiat_p256_uint1 x19 = (fiat_p256_uint1)(x17 >> 8);
+  uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
+  uint64_t x21 = (x19 + x3);
+  uint64_t x22 = (x21 >> 8);
+  uint8_t x23 = (uint8_t)(x21 & UINT8_C(0xff));
   uint64_t x24 = (x22 >> 8);
   uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff));
   uint64_t x26 = (x24 >> 8);
   uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff));
   uint64_t x28 = (x26 >> 8);
   uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff));
-  uint8_t x30 = (uint8_t)(x28 >> 8);
+  uint64_t x30 = (x28 >> 8);
   uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff));
-  fiat_p256_uint1 x32 = (fiat_p256_uint1)(x30 >> 8);
+  uint64_t x32 = (x30 >> 8);
   uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff));
-  uint64_t x34 = (x32 + x12);
-  uint64_t x35 = (x34 >> 8);
-  uint8_t x36 = (uint8_t)(x34 & UINT8_C(0xff));
-  uint64_t x37 = (x35 >> 8);
-  uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff));
-  uint64_t x39 = (x37 >> 8);
-  uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff));
+  uint8_t x34 = (uint8_t)(x32 >> 8);
+  uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff));
+  fiat_p256_uint1 x36 = (fiat_p256_uint1)(x34 >> 8);
+  uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff));
+  uint64_t x38 = (x36 + x2);
+  uint64_t x39 = (x38 >> 8);
+  uint8_t x40 = (uint8_t)(x38 & UINT8_C(0xff));
   uint64_t x41 = (x39 >> 8);
   uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff));
   uint64_t x43 = (x41 >> 8);
   uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff));
   uint64_t x45 = (x43 >> 8);
   uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff));
-  uint8_t x47 = (uint8_t)(x45 >> 8);
+  uint64_t x47 = (x45 >> 8);
   uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff));
-  fiat_p256_uint1 x49 = (fiat_p256_uint1)(x47 >> 8);
+  uint64_t x49 = (x47 >> 8);
   uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
-  uint64_t x51 = (x49 + x14);
-  uint64_t x52 = (x51 >> 8);
-  uint8_t x53 = (uint8_t)(x51 & UINT8_C(0xff));
-  uint64_t x54 = (x52 >> 8);
-  uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff));
-  uint64_t x56 = (x54 >> 8);
-  uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff));
+  uint8_t x51 = (uint8_t)(x49 >> 8);
+  uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
+  fiat_p256_uint1 x53 = (fiat_p256_uint1)(x51 >> 8);
+  uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff));
+  uint64_t x55 = (x53 + x1);
+  uint64_t x56 = (x55 >> 8);
+  uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff));
   uint64_t x58 = (x56 >> 8);
   uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff));
   uint64_t x60 = (x58 >> 8);
   uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
   uint64_t x62 = (x60 >> 8);
   uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff));
-  uint8_t x64 = (uint8_t)(x62 >> 8);
+  uint64_t x64 = (x62 >> 8);
   uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff));
-  fiat_p256_uint1 x66 = (fiat_p256_uint1)(x64 >> 8);
+  uint64_t x66 = (x64 >> 8);
   uint8_t x67 = (uint8_t)(x64 & UINT8_C(0xff));
-  uint64_t x68 = (x66 + x16);
-  uint64_t x69 = (x68 >> 8);
-  uint8_t x70 = (uint8_t)(x68 & UINT8_C(0xff));
-  uint64_t x71 = (x69 >> 8);
-  uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff));
-  uint64_t x73 = (x71 >> 8);
-  uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff));
-  uint64_t x75 = (x73 >> 8);
-  uint8_t x76 = (uint8_t)(x73 & UINT8_C(0xff));
-  uint64_t x77 = (x75 >> 8);
-  uint8_t x78 = (uint8_t)(x75 & UINT8_C(0xff));
-  uint64_t x79 = (x77 >> 8);
-  uint8_t x80 = (uint8_t)(x77 & UINT8_C(0xff));
-  uint8_t x81 = (uint8_t)(x79 >> 8);
-  uint8_t x82 = (uint8_t)(x79 & UINT8_C(0xff));
-  out1[0] = x19;
-  out1[1] = x21;
-  out1[2] = x23;
-  out1[3] = x25;
-  out1[4] = x27;
-  out1[5] = x29;
-  out1[6] = x31;
-  out1[7] = x33;
-  out1[8] = x36;
-  out1[9] = x38;
-  out1[10] = x40;
-  out1[11] = x42;
-  out1[12] = x44;
-  out1[13] = x46;
-  out1[14] = x48;
-  out1[15] = x50;
-  out1[16] = x53;
-  out1[17] = x55;
-  out1[18] = x57;
-  out1[19] = x59;
-  out1[20] = x61;
-  out1[21] = x63;
-  out1[22] = x65;
-  out1[23] = x67;
-  out1[24] = x70;
-  out1[25] = x72;
-  out1[26] = x74;
-  out1[27] = x76;
-  out1[28] = x78;
-  out1[29] = x80;
-  out1[30] = x82;
-  out1[31] = x81;
+  uint8_t x68 = (uint8_t)(x66 >> 8);
+  uint8_t x69 = (uint8_t)(x66 & UINT8_C(0xff));
+  out1[0] = x6;
+  out1[1] = x8;
+  out1[2] = x10;
+  out1[3] = x12;
+  out1[4] = x14;
+  out1[5] = x16;
+  out1[6] = x18;
+  out1[7] = x20;
+  out1[8] = x23;
+  out1[9] = x25;
+  out1[10] = x27;
+  out1[11] = x29;
+  out1[12] = x31;
+  out1[13] = x33;
+  out1[14] = x35;
+  out1[15] = x37;
+  out1[16] = x40;
+  out1[17] = x42;
+  out1[18] = x44;
+  out1[19] = x46;
+  out1[20] = x48;
+  out1[21] = x50;
+  out1[22] = x52;
+  out1[23] = x54;
+  out1[24] = x57;
+  out1[25] = x59;
+  out1[26] = x61;
+  out1[27] = x63;
+  out1[28] = x65;
+  out1[29] = x67;
+  out1[30] = x69;
+  out1[31] = x68;
 }
 
 /*