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_32.c | 234 +++++++++++++++++++++++++++++++------------------------- 1 file changed, 128 insertions(+), 106 deletions(-) (limited to 'curve25519_32.c') 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). -- cgit v1.2.3