Add some primes to be synthesized

1 files changed, 106 insertions, 141 deletions

diff --git a/p256_32.c b/p256_32.c
index 5fc3d8679..944a7209c 100644
--- a/p256_32.c
+++ b/p256_32.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 = 32 (from "32") */
+/*                                                                    */
+/* 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;
@@ -3165,157 +3172,115 @@ static void fiat_p256_selectznz(uint32_t out1[8], 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 uint32_t arg1[8]) {
-  uint32_t x1;
-  fiat_p256_uint1 x2;
-  fiat_p256_subborrowx_u32(&x1, &x2, 0x0, (arg1[0]), UINT32_C(0xffffffff));
-  uint32_t x3;
-  fiat_p256_uint1 x4;
-  fiat_p256_subborrowx_u32(&x3, &x4, x2, (arg1[1]), UINT32_C(0xffffffff));
-  uint32_t x5;
-  fiat_p256_uint1 x6;
-  fiat_p256_subborrowx_u32(&x5, &x6, x4, (arg1[2]), UINT32_C(0xffffffff));
-  uint32_t x7;
-  fiat_p256_uint1 x8;
-  fiat_p256_subborrowx_u32(&x7, &x8, x6, (arg1[3]), 0x0);
-  uint32_t x9;
-  fiat_p256_uint1 x10;
-  fiat_p256_subborrowx_u32(&x9, &x10, x8, (arg1[4]), 0x0);
-  uint32_t x11;
-  fiat_p256_uint1 x12;
-  fiat_p256_subborrowx_u32(&x11, &x12, x10, (arg1[5]), 0x0);
-  uint32_t x13;
-  fiat_p256_uint1 x14;
-  fiat_p256_subborrowx_u32(&x13, &x14, x12, (arg1[6]), 0x1);
-  uint32_t x15;
-  fiat_p256_uint1 x16;
-  fiat_p256_subborrowx_u32(&x15, &x16, x14, (arg1[7]), UINT32_C(0xffffffff));
-  uint32_t x17;
-  fiat_p256_cmovznz_u32(&x17, x16, 0x0, UINT32_C(0xffffffff));
-  uint32_t x18;
-  fiat_p256_uint1 x19;
-  fiat_p256_addcarryx_u32(&x18, &x19, 0x0, (x17 & UINT32_C(0xffffffff)), x1);
-  uint32_t x20;
-  fiat_p256_uint1 x21;
-  fiat_p256_addcarryx_u32(&x20, &x21, x19, (x17 & UINT32_C(0xffffffff)), x3);
-  uint32_t x22;
-  fiat_p256_uint1 x23;
-  fiat_p256_addcarryx_u32(&x22, &x23, x21, (x17 & UINT32_C(0xffffffff)), x5);
-  uint32_t x24;
-  fiat_p256_uint1 x25;
-  fiat_p256_addcarryx_u32(&x24, &x25, x23, 0x0, x7);
-  uint32_t x26;
-  fiat_p256_uint1 x27;
-  fiat_p256_addcarryx_u32(&x26, &x27, x25, 0x0, x9);
-  uint32_t x28;
-  fiat_p256_uint1 x29;
-  fiat_p256_addcarryx_u32(&x28, &x29, x27, 0x0, x11);
-  uint32_t x30;
-  fiat_p256_uint1 x31;
-  fiat_p256_addcarryx_u32(&x30, &x31, x29, (fiat_p256_uint1)(x17 & 0x1), x13);
-  uint32_t x32;
-  fiat_p256_uint1 x33;
-  fiat_p256_addcarryx_u32(&x32, &x33, x31, (x17 & UINT32_C(0xffffffff)), x15);
-  uint32_t x34 = (x18 >> 8);
-  uint8_t x35 = (uint8_t)(x18 & UINT8_C(0xff));
-  uint32_t x36 = (x34 >> 8);
-  uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff));
-  uint8_t x38 = (uint8_t)(x36 >> 8);
+  uint32_t x1 = (arg1[7]);
+  uint32_t x2 = (arg1[6]);
+  uint32_t x3 = (arg1[5]);
+  uint32_t x4 = (arg1[4]);
+  uint32_t x5 = (arg1[3]);
+  uint32_t x6 = (arg1[2]);
+  uint32_t x7 = (arg1[1]);
+  uint32_t x8 = (arg1[0]);
+  uint32_t x9 = (x8 >> 8);
+  uint8_t x10 = (uint8_t)(x8 & UINT8_C(0xff));
+  uint32_t x11 = (x9 >> 8);
+  uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff));
+  uint8_t x13 = (uint8_t)(x11 >> 8);
+  uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff));
+  fiat_p256_uint1 x15 = (fiat_p256_uint1)(x13 >> 8);
+  uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
+  uint32_t x17 = (x15 + x7);
+  uint32_t x18 = (x17 >> 8);
+  uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff));
+  uint32_t x20 = (x18 >> 8);
+  uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff));
+  uint8_t x22 = (uint8_t)(x20 >> 8);
+  uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff));
+  fiat_p256_uint1 x24 = (fiat_p256_uint1)(x22 >> 8);
+  uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff));
+  uint32_t x26 = (x24 + x6);
+  uint32_t x27 = (x26 >> 8);
+  uint8_t x28 = (uint8_t)(x26 & UINT8_C(0xff));
+  uint32_t x29 = (x27 >> 8);
+  uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff));
+  uint8_t x31 = (uint8_t)(x29 >> 8);
+  uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff));
+  fiat_p256_uint1 x33 = (fiat_p256_uint1)(x31 >> 8);
+  uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff));
+  uint32_t x35 = (x33 + x5);
+  uint32_t x36 = (x35 >> 8);
+  uint8_t x37 = (uint8_t)(x35 & UINT8_C(0xff));
+  uint32_t x38 = (x36 >> 8);
   uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff));
-  fiat_p256_uint1 x40 = (fiat_p256_uint1)(x38 >> 8);
+  uint8_t x40 = (uint8_t)(x38 >> 8);
   uint8_t x41 = (uint8_t)(x38 & UINT8_C(0xff));
-  uint32_t x42 = (x40 + x20);
-  uint32_t x43 = (x42 >> 8);
-  uint8_t x44 = (uint8_t)(x42 & UINT8_C(0xff));
-  uint32_t x45 = (x43 >> 8);
-  uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff));
-  uint8_t x47 = (uint8_t)(x45 >> 8);
+  fiat_p256_uint1 x42 = (fiat_p256_uint1)(x40 >> 8);
+  uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff));
+  uint32_t x44 = (x42 + x4);
+  uint32_t x45 = (x44 >> 8);
+  uint8_t x46 = (uint8_t)(x44 & UINT8_C(0xff));
+  uint32_t x47 = (x45 >> 8);
   uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff));
-  fiat_p256_uint1 x49 = (fiat_p256_uint1)(x47 >> 8);
+  uint8_t x49 = (uint8_t)(x47 >> 8);
   uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
-  uint32_t x51 = (x49 + x22);
-  uint32_t x52 = (x51 >> 8);
-  uint8_t x53 = (uint8_t)(x51 & UINT8_C(0xff));
-  uint32_t x54 = (x52 >> 8);
-  uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff));
-  uint8_t x56 = (uint8_t)(x54 >> 8);
+  fiat_p256_uint1 x51 = (fiat_p256_uint1)(x49 >> 8);
+  uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
+  uint32_t x53 = (x51 + x3);
+  uint32_t x54 = (x53 >> 8);
+  uint8_t x55 = (uint8_t)(x53 & UINT8_C(0xff));
+  uint32_t x56 = (x54 >> 8);
   uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff));
-  fiat_p256_uint1 x58 = (fiat_p256_uint1)(x56 >> 8);
+  uint8_t x58 = (uint8_t)(x56 >> 8);
   uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff));
-  uint32_t x60 = (x58 + x24);
-  uint32_t x61 = (x60 >> 8);
-  uint8_t x62 = (uint8_t)(x60 & UINT8_C(0xff));
-  uint32_t x63 = (x61 >> 8);
-  uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff));
-  uint8_t x65 = (uint8_t)(x63 >> 8);
+  fiat_p256_uint1 x60 = (fiat_p256_uint1)(x58 >> 8);
+  uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
+  uint32_t x62 = (x60 + x2);
+  uint32_t x63 = (x62 >> 8);
+  uint8_t x64 = (uint8_t)(x62 & UINT8_C(0xff));
+  uint32_t x65 = (x63 >> 8);
   uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff));
-  fiat_p256_uint1 x67 = (fiat_p256_uint1)(x65 >> 8);
+  uint8_t x67 = (uint8_t)(x65 >> 8);
   uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff));
-  uint32_t x69 = (x67 + x26);
-  uint32_t x70 = (x69 >> 8);
-  uint8_t x71 = (uint8_t)(x69 & UINT8_C(0xff));
-  uint32_t x72 = (x70 >> 8);
-  uint8_t x73 = (uint8_t)(x70 & UINT8_C(0xff));
-  uint8_t x74 = (uint8_t)(x72 >> 8);
+  fiat_p256_uint1 x69 = (fiat_p256_uint1)(x67 >> 8);
+  uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff));
+  uint32_t x71 = (x69 + x1);
+  uint32_t x72 = (x71 >> 8);
+  uint8_t x73 = (uint8_t)(x71 & UINT8_C(0xff));
+  uint32_t x74 = (x72 >> 8);
   uint8_t x75 = (uint8_t)(x72 & UINT8_C(0xff));
-  fiat_p256_uint1 x76 = (fiat_p256_uint1)(x74 >> 8);
+  uint8_t x76 = (uint8_t)(x74 >> 8);
   uint8_t x77 = (uint8_t)(x74 & UINT8_C(0xff));
-  uint32_t x78 = (x76 + x28);
-  uint32_t x79 = (x78 >> 8);
-  uint8_t x80 = (uint8_t)(x78 & UINT8_C(0xff));
-  uint32_t x81 = (x79 >> 8);
-  uint8_t x82 = (uint8_t)(x79 & UINT8_C(0xff));
-  uint8_t x83 = (uint8_t)(x81 >> 8);
-  uint8_t x84 = (uint8_t)(x81 & UINT8_C(0xff));
-  fiat_p256_uint1 x85 = (fiat_p256_uint1)(x83 >> 8);
-  uint8_t x86 = (uint8_t)(x83 & UINT8_C(0xff));
-  uint32_t x87 = (x85 + x30);
-  uint32_t x88 = (x87 >> 8);
-  uint8_t x89 = (uint8_t)(x87 & UINT8_C(0xff));
-  uint32_t x90 = (x88 >> 8);
-  uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff));
-  uint8_t x92 = (uint8_t)(x90 >> 8);
-  uint8_t x93 = (uint8_t)(x90 & UINT8_C(0xff));
-  fiat_p256_uint1 x94 = (fiat_p256_uint1)(x92 >> 8);
-  uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff));
-  uint32_t x96 = (x94 + x32);
-  uint32_t x97 = (x96 >> 8);
-  uint8_t x98 = (uint8_t)(x96 & UINT8_C(0xff));
-  uint32_t x99 = (x97 >> 8);
-  uint8_t x100 = (uint8_t)(x97 & UINT8_C(0xff));
-  uint8_t x101 = (uint8_t)(x99 >> 8);
-  uint8_t x102 = (uint8_t)(x99 & UINT8_C(0xff));
-  out1[0] = x35;
-  out1[1] = x37;
-  out1[2] = x39;
-  out1[3] = x41;
-  out1[4] = x44;
-  out1[5] = x46;
-  out1[6] = x48;
-  out1[7] = x50;
-  out1[8] = x53;
-  out1[9] = x55;
-  out1[10] = x57;
-  out1[11] = x59;
-  out1[12] = x62;
-  out1[13] = x64;
-  out1[14] = x66;
-  out1[15] = x68;
-  out1[16] = x71;
-  out1[17] = x73;
-  out1[18] = x75;
-  out1[19] = x77;
-  out1[20] = x80;
-  out1[21] = x82;
-  out1[22] = x84;
-  out1[23] = x86;
-  out1[24] = x89;
-  out1[25] = x91;
-  out1[26] = x93;
-  out1[27] = x95;
-  out1[28] = x98;
-  out1[29] = x100;
-  out1[30] = x102;
-  out1[31] = x101;
+  out1[0] = x10;
+  out1[1] = x12;
+  out1[2] = x14;
+  out1[3] = x16;
+  out1[4] = x19;
+  out1[5] = x21;
+  out1[6] = x23;
+  out1[7] = x25;
+  out1[8] = x28;
+  out1[9] = x30;
+  out1[10] = x32;
+  out1[11] = x34;
+  out1[12] = x37;
+  out1[13] = x39;
+  out1[14] = x41;
+  out1[15] = x43;
+  out1[16] = x46;
+  out1[17] = x48;
+  out1[18] = x50;
+  out1[19] = x52;
+  out1[20] = x55;
+  out1[21] = x57;
+  out1[22] = x59;
+  out1[23] = x61;
+  out1[24] = x64;
+  out1[25] = x66;
+  out1[26] = x68;
+  out1[27] = x70;
+  out1[28] = x73;
+  out1[29] = x75;
+  out1[30] = x77;
+  out1[31] = x76;
 }
 
 /*