update c

1 files changed, 128 insertions, 106 deletions

diff --git a/curve25519_32.c b/curve25519_32.c
index 4d31b5110..70ab9c0af 100644
--- a/curve25519_32.c
+++ b/curve25519_32.c
@@ -24,113 +24,135 @@ When doing bounds analysis on the syntax tree:
  *   out1: None
  */
 void f(uint256 out1[10], const uint32_t arg1[10]) {
-  uint32_t x1 = ((arg1[8]) * (uint32_t)UINT8_C(0x13));
-  uint64_t x2 = (x1 * (uint64_t)0x2);
-  uint32_t x3 = ((arg1[7]) * (uint32_t)UINT8_C(0x13));
-  uint32_t x4 = (x3 * (uint32_t)0x2);
-  uint32_t x5 = ((arg1[6]) * (uint32_t)UINT8_C(0x13));
-  uint64_t x6 = (x5 * (uint64_t)0x2);
-  uint32_t x7 = ((arg1[5]) * (uint32_t)UINT8_C(0x13));
+  uint32_t x1 = ((arg1[9]) * (uint32_t)UINT8_C(0x13));
+  uint32_t x2 = (x1 * (uint32_t)0x2);
+  uint32_t x3 = ((arg1[9]) * (uint32_t)0x2);
+  uint32_t x4 = ((arg1[8]) * (uint32_t)UINT8_C(0x13));
+  uint64_t x5 = (x4 * (uint64_t)0x2);
+  uint32_t x6 = ((arg1[8]) * (uint32_t)0x2);
+  uint32_t x7 = ((arg1[7]) * (uint32_t)UINT8_C(0x13));
   uint32_t x8 = (x7 * (uint32_t)0x2);
-  uint32_t x9 = ((arg1[4]) * (uint32_t)0x2);
-  uint32_t x10 = ((arg1[3]) * (uint32_t)0x2);
-  uint32_t x11 = ((arg1[2]) * (uint32_t)0x2);
-  uint32_t x12 = ((arg1[1]) * (uint32_t)0x2);
-  uint32_t x13 = ((arg1[0]) * (uint32_t)0x2);
-  uint512 x14 = ((uint512)((uint64_t)(arg1[9]) * (arg1[9])) << 230);
-  uint64_t x15 = ((arg1[8]) * x2);
-  uint256 x16 = ((uint256)((uint64_t)(arg1[8]) * (arg1[8])) << 178);
-  uint64_t x17 = ((arg1[7]) * (x4 * (uint64_t)0x2));
-  uint64_t x18 = ((arg1[7]) * (x4 * (uint64_t)0x2));
-  uint256 x19 = ((uint256)((uint64_t)(arg1[7]) * (arg1[7])) << 128);
-  uint64_t x20 = ((arg1[6]) * x6);
-  uint64_t x21 = ((arg1[6]) * x6);
-  uint64_t x22 = ((arg1[6]) * x6);
-  uint256 x23 = ((uint256)((uint64_t)(arg1[6]) * (arg1[6])) << 76);
-  uint64_t x24 = ((arg1[5]) * (x8 * (uint64_t)0x2));
-  uint64_t x25 = ((arg1[5]) * (x8 * (uint64_t)0x2));
-  uint64_t x26 = ((arg1[5]) * (x8 * (uint64_t)0x2));
-  uint64_t x27 = ((arg1[5]) * (x8 * (uint64_t)0x2));
-  uint128 x28 = ((uint128)((uint64_t)(arg1[5]) * (arg1[5])) << 26);
-  uint64_t x29 = ((uint64_t)(arg1[4]) * x9);
-  uint64_t x30 = ((uint64_t)(arg1[4]) * (arg1[4]));
-  uint64_t x31 = ((uint64_t)(arg1[3]) * (x10 * (uint32_t)0x2));
-  uint64_t x32 = ((uint64_t)(arg1[3]) * (x10 * (uint32_t)0x2));
-  uint64_t x33 = ((uint64_t)(arg1[3]) * (x10 * (uint32_t)0x2));
-  uint64_t x34 = ((uint64_t)(arg1[3]) * ((arg1[3]) * (uint32_t)0x2));
-  uint64_t x35 = ((uint64_t)(arg1[2]) * x11);
-  uint64_t x36 = ((uint64_t)(arg1[2]) * x11);
-  uint64_t x37 = ((uint64_t)(arg1[2]) * x11);
-  uint64_t x38 = ((uint64_t)(arg1[2]) * x11);
-  uint64_t x39 = ((uint64_t)(arg1[2]) * x11);
-  uint64_t x40 = ((uint64_t)(arg1[2]) * (arg1[2]));
-  uint64_t x41 = ((uint64_t)(arg1[1]) * (x12 * (uint32_t)0x2));
-  uint64_t x42 = ((uint64_t)(arg1[1]) * (x12 * (uint32_t)0x2));
-  uint64_t x43 = ((uint64_t)(arg1[1]) * (x12 * (uint32_t)0x2));
-  uint64_t x44 = ((uint64_t)(arg1[1]) * (x12 * (uint32_t)0x2));
-  uint64_t x45 = ((uint64_t)(arg1[1]) * (x12 * (uint32_t)0x2));
-  uint64_t x46 = ((uint64_t)(arg1[1]) * (x12 * (uint32_t)0x2));
-  uint64_t x47 = ((uint64_t)(arg1[1]) * (x12 * (uint32_t)0x2));
-  uint64_t x48 = ((uint64_t)(arg1[1]) * ((arg1[1]) * (uint32_t)0x2));
-  uint64_t x49 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x50 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x51 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x52 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x53 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x54 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x55 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x56 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x57 = ((uint64_t)(arg1[0]) * x13);
-  uint64_t x58 = ((uint64_t)(arg1[0]) * (arg1[0]));
-  uint64_t x59 = (x58 + (x57 + (x56 + (x55 + (x54 + (x53 + (x52 + (x51 + (x50 + (x49 + (x27 + (x26 + (x25 + x24)))))))))))));
-  uint64_t x60 = (x59 >> 26);
-  uint32_t x61 = (uint32_t)(x59 & UINT32_C(0x3ffffff));
-  uint512 x62 = (x28 + (x23 + (x19 + (x16 + x14))));
-  uint64_t x63 = (x30 + x29);
-  uint64_t x64 = (x34 + (x33 + (x32 + (x31 + x15))));
-  uint64_t x65 = (x40 + (x39 + (x38 + (x37 + (x36 + (x35 + (x18 + x17)))))));
-  uint64_t x66 = (x48 + (x47 + (x46 + (x45 + (x44 + (x43 + (x42 + (x41 + (x22 + (x21 + x20))))))))));
-  uint16_t x67 = (uint16_t)(x60 >> 25);
-  uint32_t x68 = (uint32_t)(x60 & UINT32_C(0x1ffffff));
-  uint64_t x69 = (x67 + x66);
-  uint64_t x70 = (x69 >> 26);
-  uint32_t x71 = (uint32_t)(x69 & UINT32_C(0x3ffffff));
-  uint16_t x72 = (uint16_t)(x70 >> 25);
-  uint32_t x73 = (uint32_t)(x70 & UINT32_C(0x1ffffff));
-  uint64_t x74 = (x72 + x65);
-  uint64_t x75 = (x74 >> 26);
-  uint32_t x76 = (uint32_t)(x74 & UINT32_C(0x3ffffff));
-  uint16_t x77 = (uint16_t)(x75 >> 25);
-  uint32_t x78 = (uint32_t)(x75 & UINT32_C(0x1ffffff));
-  uint64_t x79 = (x77 + x64);
-  uint64_t x80 = (x79 >> 26);
-  uint32_t x81 = (uint32_t)(x79 & UINT32_C(0x3ffffff));
-  uint16_t x82 = (uint16_t)(x80 >> 25);
-  uint32_t x83 = (uint32_t)(x80 & UINT32_C(0x1ffffff));
-  uint64_t x84 = (x82 + x63);
-  uint32_t x85 = (uint32_t)(x84 >> 26);
-  uint32_t x86 = (uint32_t)(x84 & UINT32_C(0x3ffffff));
-  uint512 x87 = (x85 + x62);
-  uint512 x88 = (x87 >> 25);
-  uint32_t x89 = (uint32_t)(x87 & UINT32_C(0x1ffffff));
-  uint512 x90 = (x88 * (uint512)UINT8_C(0x13));
-  uint512 x91 = (x61 + x90);
-  uint256 x92 = (uint256)(x91 >> 26);
-  uint32_t x93 = (uint32_t)(x91 & UINT32_C(0x3ffffff));
-  uint256 x94 = (x92 + x68);
-  uint256 x95 = (x94 >> 25);
-  uint32_t x96 = (uint32_t)(x94 & UINT32_C(0x1ffffff));
-  uint256 x97 = (x95 + x71);
-  out1[0] = x93;
-  out1[1] = x96;
-  out1[2] = x97;
-  out1[3] = x73;
-  out1[4] = x76;
-  out1[5] = x78;
-  out1[6] = x81;
-  out1[7] = x83;
-  out1[8] = x86;
-  out1[9] = x89;
+  uint32_t x9 = ((arg1[7]) * (uint32_t)0x2);
+  uint32_t x10 = ((arg1[6]) * (uint32_t)UINT8_C(0x13));
+  uint64_t x11 = (x10 * (uint64_t)0x2);
+  uint32_t x12 = ((arg1[6]) * (uint32_t)0x2);
+  uint32_t x13 = ((arg1[5]) * (uint32_t)0x2);
+  uint32_t x14 = ((arg1[4]) * (uint32_t)0x2);
+  uint32_t x15 = ((arg1[3]) * (uint32_t)0x2);
+  uint32_t x16 = ((arg1[2]) * (uint32_t)0x2);
+  uint32_t x17 = ((arg1[1]) * (uint32_t)0x2);
+  uint512 x18 = ((uint512)((uint64_t)(arg1[9]) * (arg1[9])) << 230);
+  uint64_t x19 = ((uint64_t)(arg1[8]) * x2);
+  uint256 x20 = ((uint256)((uint64_t)(arg1[8]) * (arg1[8])) << 178);
+  uint64_t x21 = ((arg1[7]) * (x2 * (uint64_t)0x2));
+  uint64_t x22 = ((arg1[7]) * x5);
+  uint256 x23 = ((uint256)((uint64_t)(arg1[7]) * (arg1[7])) << 128);
+  uint64_t x24 = ((uint64_t)(arg1[6]) * x2);
+  uint64_t x25 = ((arg1[6]) * x5);
+  uint64_t x26 = ((uint64_t)(arg1[6]) * x8);
+  uint256 x27 = ((uint256)((uint64_t)(arg1[6]) * (arg1[6])) << 76);
+  uint64_t x28 = ((arg1[5]) * (x2 * (uint64_t)0x2));
+  uint64_t x29 = ((arg1[5]) * x5);
+  uint64_t x30 = ((arg1[5]) * (x8 * (uint64_t)0x2));
+  uint64_t x31 = ((arg1[5]) * x11);
+  uint128 x32 = ((uint128)((uint64_t)(arg1[5]) * (arg1[5])) << 26);
+  uint64_t x33 = ((uint64_t)(arg1[4]) * x2);
+  uint64_t x34 = ((arg1[4]) * x5);
+  uint64_t x35 = ((uint64_t)(arg1[4]) * x8);
+  uint64_t x36 = ((arg1[4]) * x11);
+  uint64_t x37 = ((uint64_t)(arg1[4]) * x13);
+  uint64_t x38 = ((uint64_t)(arg1[4]) * (arg1[4]));
+  uint64_t x39 = ((arg1[3]) * (x2 * (uint64_t)0x2));
+  uint64_t x40 = ((arg1[3]) * x5);
+  uint64_t x41 = ((arg1[3]) * (x8 * (uint64_t)0x2));
+  uint64_t x42 = ((uint64_t)(arg1[3]) * x12);
+  uint64_t x43 = ((uint64_t)(arg1[3]) * (x13 * (uint32_t)0x2));
+  uint64_t x44 = ((uint64_t)(arg1[3]) * x14);
+  uint64_t x45 = ((uint64_t)(arg1[3]) * ((arg1[3]) * (uint32_t)0x2));
+  uint64_t x46 = ((uint64_t)(arg1[2]) * x2);
+  uint64_t x47 = ((arg1[2]) * x5);
+  uint64_t x48 = ((uint64_t)(arg1[2]) * x9);
+  uint64_t x49 = ((uint64_t)(arg1[2]) * x12);
+  uint64_t x50 = ((uint64_t)(arg1[2]) * x13);
+  uint64_t x51 = ((uint64_t)(arg1[2]) * x14);
+  uint64_t x52 = ((uint64_t)(arg1[2]) * x15);
+  uint64_t x53 = ((uint64_t)(arg1[2]) * (arg1[2]));
+  uint64_t x54 = ((arg1[1]) * (x2 * (uint64_t)0x2));
+  uint64_t x55 = ((uint64_t)(arg1[1]) * x6);
+  uint64_t x56 = ((uint64_t)(arg1[1]) * (x9 * (uint32_t)0x2));
+  uint64_t x57 = ((uint64_t)(arg1[1]) * x12);
+  uint64_t x58 = ((uint64_t)(arg1[1]) * (x13 * (uint32_t)0x2));
+  uint64_t x59 = ((uint64_t)(arg1[1]) * x14);
+  uint64_t x60 = ((uint64_t)(arg1[1]) * (x15 * (uint32_t)0x2));
+  uint64_t x61 = ((uint64_t)(arg1[1]) * x16);
+  uint64_t x62 = ((uint64_t)(arg1[1]) * ((arg1[1]) * (uint32_t)0x2));
+  uint64_t x63 = ((uint64_t)(arg1[0]) * x3);
+  uint64_t x64 = ((uint64_t)(arg1[0]) * x6);
+  uint64_t x65 = ((uint64_t)(arg1[0]) * x9);
+  uint64_t x66 = ((uint64_t)(arg1[0]) * x12);
+  uint64_t x67 = ((uint64_t)(arg1[0]) * x13);
+  uint64_t x68 = ((uint64_t)(arg1[0]) * x14);
+  uint64_t x69 = ((uint64_t)(arg1[0]) * x15);
+  uint64_t x70 = ((uint64_t)(arg1[0]) * x16);
+  uint64_t x71 = ((uint64_t)(arg1[0]) * x17);
+  uint64_t x72 = ((uint64_t)(arg1[0]) * (arg1[0]));
+  uint64_t x73 = (x72 + (x54 + (x47 + (x41 + x36))));
+  uint64_t x74 = (x73 >> 26);
+  uint32_t x75 = (uint32_t)(x73 & UINT32_C(0x3ffffff));
+  uint512 x76 = (x63 + (x55 + (x48 + (x42 + (x37 + (x32 + (x27 + (x23 + (x20 + x18)))))))));
+  uint64_t x77 = (x64 + (x56 + (x49 + (x43 + x38))));
+  uint64_t x78 = (x65 + (x57 + (x50 + (x44 + x19))));
+  uint64_t x79 = (x66 + (x58 + (x51 + (x45 + x21))));
+  uint64_t x80 = (x67 + (x59 + (x52 + (x24 + x22))));
+  uint64_t x81 = (x68 + (x60 + (x53 + (x28 + x25))));
+  uint64_t x82 = (x69 + (x61 + (x33 + (x29 + x26))));
+  uint64_t x83 = (x70 + (x62 + (x39 + (x34 + x30))));
+  uint64_t x84 = (x71 + (x46 + (x40 + (x35 + x31))));
+  uint64_t x85 = (x74 + x84);
+  uint64_t x86 = (x85 >> 25);
+  uint32_t x87 = (uint32_t)(x85 & UINT32_C(0x1ffffff));
+  uint64_t x88 = (x86 + x83);
+  uint64_t x89 = (x88 >> 26);
+  uint32_t x90 = (uint32_t)(x88 & UINT32_C(0x3ffffff));
+  uint64_t x91 = (x89 + x82);
+  uint64_t x92 = (x91 >> 25);
+  uint32_t x93 = (uint32_t)(x91 & UINT32_C(0x1ffffff));
+  uint64_t x94 = (x92 + x81);
+  uint64_t x95 = (x94 >> 26);
+  uint32_t x96 = (uint32_t)(x94 & UINT32_C(0x3ffffff));
+  uint64_t x97 = (x95 + x80);
+  uint64_t x98 = (x97 >> 25);
+  uint32_t x99 = (uint32_t)(x97 & UINT32_C(0x1ffffff));
+  uint64_t x100 = (x98 + x79);
+  uint64_t x101 = (x100 >> 26);
+  uint32_t x102 = (uint32_t)(x100 & UINT32_C(0x3ffffff));
+  uint64_t x103 = (x101 + x78);
+  uint64_t x104 = (x103 >> 25);
+  uint32_t x105 = (uint32_t)(x103 & UINT32_C(0x1ffffff));
+  uint64_t x106 = (x104 + x77);
+  uint64_t x107 = (x106 >> 26);
+  uint32_t x108 = (uint32_t)(x106 & UINT32_C(0x3ffffff));
+  uint512 x109 = (x107 + x76);
+  uint512 x110 = (x109 >> 25);
+  uint32_t x111 = (uint32_t)(x109 & UINT32_C(0x1ffffff));
+  uint512 x112 = (x110 * (uint512)UINT8_C(0x13));
+  uint512 x113 = (x75 + x112);
+  uint256 x114 = (uint256)(x113 >> 26);
+  uint32_t x115 = (uint32_t)(x113 & UINT32_C(0x3ffffff));
+  uint256 x116 = (x114 + x87);
+  uint256 x117 = (x116 >> 25);
+  uint32_t x118 = (uint32_t)(x116 & UINT32_C(0x1ffffff));
+  uint256 x119 = (x117 + x90);
+  out1[0] = x115;
+  out1[1] = x118;
+  out1[2] = x119;
+  out1[3] = x93;
+  out1[4] = x96;
+  out1[5] = x99;
+  out1[6] = x102;
+  out1[7] = x105;
+  out1[8] = x108;
+  out1[9] = x111;
 }
 
 with input bounds (Some [Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999]], tt).