update c

1 files changed, 52 insertions, 42 deletions

diff --git a/curve25519_64.c b/curve25519_64.c
index 799b4e93b..fbeac1509 100644
--- a/curve25519_64.c
+++ b/curve25519_64.c
@@ -26,51 +26,61 @@ When doing bounds analysis on the syntax tree:
  *   out1: None
  */
 void f(uint256 out1[5], const uint64_t arg1[5]) {
-  uint64_t x1 = ((arg1[3]) * (uint64_t)UINT8_C(0x13));
+  uint64_t x1 = ((arg1[4]) * (uint64_t)UINT8_C(0x13));
   uint64_t x2 = (x1 * (uint64_t)0x2);
-  uint64_t x3 = ((arg1[1]) * (uint64_t)0x2);
-  uint64_t x4 = ((arg1[0]) * (uint64_t)0x2);
-  uint512 x5 = ((uint512)((uint128)(arg1[4]) * (arg1[4])) << 204);
-  uint128 x6 = ((uint128)(arg1[3]) * x2);
-  uint256 x7 = ((uint256)((uint128)(arg1[3]) * (arg1[3])) << 102);
-  uint128 x8 = ((uint128)(arg1[2]) * (arg1[2]));
-  uint128 x9 = ((uint128)(arg1[1]) * x3);
-  uint128 x10 = ((uint128)(arg1[1]) * x3);
-  uint128 x11 = ((uint128)(arg1[1]) * (arg1[1]));
-  uint128 x12 = ((uint128)(arg1[0]) * x4);
-  uint128 x13 = ((uint128)(arg1[0]) * x4);
-  uint128 x14 = ((uint128)(arg1[0]) * x4);
-  uint128 x15 = ((uint128)(arg1[0]) * x4);
-  uint128 x16 = ((uint128)(arg1[0]) * (arg1[0]));
-  uint128 x17 = (x16 + (x15 + (x14 + (x13 + x12))));
-  uint64_t x18 = (uint64_t)(x17 >> 51);
-  uint64_t x19 = (uint64_t)(x17 & UINT64_C(0x7ffffffffffff));
-  uint512 x20 = (x8 + (x7 + x5));
-  uint128 x21 = (x11 + (x10 + x9));
-  uint128 x22 = (x18 + x6);
-  uint64_t x23 = (uint64_t)(x22 >> 51);
-  uint64_t x24 = (uint64_t)(x22 & UINT64_C(0x7ffffffffffff));
-  uint128 x25 = (x23 + x21);
-  uint64_t x26 = (uint64_t)(x25 >> 51);
-  uint64_t x27 = (uint64_t)(x25 & UINT64_C(0x7ffffffffffff));
-  uint8_t x28 = (uint8_t)(x26 >> 51);
-  uint64_t x29 = (x26 & UINT64_C(0x7ffffffffffff));
-  uint512 x30 = (x28 + x20);
-  uint512 x31 = (x30 >> 51);
-  uint64_t x32 = (uint64_t)(x30 & UINT64_C(0x7ffffffffffff));
-  uint512 x33 = (x31 * (uint512)UINT8_C(0x13));
-  uint512 x34 = (x19 + x33);
-  uint256 x35 = (uint256)(x34 >> 51);
+  uint64_t x3 = ((arg1[4]) * (uint64_t)0x2);
+  uint64_t x4 = ((arg1[3]) * (uint64_t)UINT8_C(0x13));
+  uint64_t x5 = (x4 * (uint64_t)0x2);
+  uint64_t x6 = ((arg1[3]) * (uint64_t)0x2);
+  uint64_t x7 = ((arg1[2]) * (uint64_t)0x2);
+  uint64_t x8 = ((arg1[1]) * (uint64_t)0x2);
+  uint512 x9 = ((uint512)((uint128)(arg1[4]) * (arg1[4])) << 204);
+  uint128 x10 = ((uint128)(arg1[3]) * x2);
+  uint256 x11 = ((uint256)((uint128)(arg1[3]) * (arg1[3])) << 102);
+  uint128 x12 = ((uint128)(arg1[2]) * x2);
+  uint128 x13 = ((uint128)(arg1[2]) * x5);
+  uint128 x14 = ((uint128)(arg1[2]) * (arg1[2]));
+  uint128 x15 = ((uint128)(arg1[1]) * x2);
+  uint128 x16 = ((uint128)(arg1[1]) * x6);
+  uint128 x17 = ((uint128)(arg1[1]) * x7);
+  uint128 x18 = ((uint128)(arg1[1]) * (arg1[1]));
+  uint128 x19 = ((uint128)(arg1[0]) * x3);
+  uint128 x20 = ((uint128)(arg1[0]) * x6);
+  uint128 x21 = ((uint128)(arg1[0]) * x7);
+  uint128 x22 = ((uint128)(arg1[0]) * x8);
+  uint128 x23 = ((uint128)(arg1[0]) * (arg1[0]));
+  uint128 x24 = (x23 + (x15 + x13));
+  uint64_t x25 = (uint64_t)(x24 >> 51);
+  uint64_t x26 = (uint64_t)(x24 & UINT64_C(0x7ffffffffffff));
+  uint512 x27 = (x19 + (x16 + (x14 + (x11 + x9))));
+  uint128 x28 = (x20 + x17);
+  uint128 x29 = (x21 + (x18 + x10));
+  uint128 x30 = (x22 + x12);
+  uint128 x31 = (x25 + x30);
+  uint64_t x32 = (uint64_t)(x31 >> 51);
+  uint64_t x33 = (uint64_t)(x31 & UINT64_C(0x7ffffffffffff));
+  uint128 x34 = (x32 + x29);
+  uint64_t x35 = (uint64_t)(x34 >> 51);
   uint64_t x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff));
-  uint256 x37 = (x35 + x24);
-  uint256 x38 = (x37 >> 51);
+  uint128 x37 = (x35 + x28);
+  uint64_t x38 = (uint64_t)(x37 >> 51);
   uint64_t x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff));
-  uint256 x40 = (x38 + x27);
-  out1[0] = x36;
-  out1[1] = x39;
-  out1[2] = x40;
-  out1[3] = x29;
-  out1[4] = x32;
+  uint512 x40 = (x38 + x27);
+  uint512 x41 = (x40 >> 51);
+  uint64_t x42 = (uint64_t)(x40 & UINT64_C(0x7ffffffffffff));
+  uint512 x43 = (x41 * (uint512)UINT8_C(0x13));
+  uint512 x44 = (x26 + x43);
+  uint256 x45 = (uint256)(x44 >> 51);
+  uint64_t x46 = (uint64_t)(x44 & UINT64_C(0x7ffffffffffff));
+  uint256 x47 = (x45 + x33);
+  uint256 x48 = (x47 >> 51);
+  uint64_t x49 = (uint64_t)(x47 & UINT64_C(0x7ffffffffffff));
+  uint256 x50 = (x48 + x36);
+  out1[0] = x46;
+  out1[1] = x49;
+  out1[2] = x50;
+  out1[3] = x39;
+  out1[4] = x42;
 }
 
 with input bounds (Some [Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664]], tt).