From 7637784874a58c09436027cefa9c36e79c803e83 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 29 Jun 2018 19:45:38 -0400 Subject: update c --- curve25519_64.c | 94 +++++++++++++++++++++++++++++++-------------------------- 1 file changed, 52 insertions(+), 42 deletions(-) (limited to 'curve25519_64.c') 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). -- cgit v1.2.3