Robert Sloan | 4c22c5f | 2019-03-01 15:53:37 -0800 | [diff] [blame] | 1 | /* Autogenerated */ |
| 2 | /* curve description: 25519 */ |
| 3 | /* requested operations: carry_mul, carry_square, carry_scmul121666, carry, add, sub, opp, selectznz, to_bytes, from_bytes */ |
| 4 | /* n = 5 (from "5") */ |
| 5 | /* s = 0x8000000000000000000000000000000000000000000000000000000000000000 (from "2^255") */ |
| 6 | /* c = [(1, 19)] (from "1,19") */ |
| 7 | /* machine_wordsize = 64 (from "64") */ |
| 8 | |
| 9 | #include <stdint.h> |
| 10 | typedef unsigned char fiat_25519_uint1; |
| 11 | typedef signed char fiat_25519_int1; |
| 12 | typedef signed __int128 fiat_25519_int128; |
| 13 | typedef unsigned __int128 fiat_25519_uint128; |
| 14 | |
| 15 | |
| 16 | /* |
| 17 | * Input Bounds: |
| 18 | * arg1: [0x0 ~> 0x1] |
| 19 | * arg2: [0x0 ~> 0x7ffffffffffff] |
| 20 | * arg3: [0x0 ~> 0x7ffffffffffff] |
| 21 | * Output Bounds: |
| 22 | * out1: [0x0 ~> 0x7ffffffffffff] |
| 23 | * out2: [0x0 ~> 0x1] |
| 24 | */ |
| 25 | static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { |
| 26 | uint64_t x1 = ((arg1 + arg2) + arg3); |
| 27 | uint64_t x2 = (x1 & UINT64_C(0x7ffffffffffff)); |
| 28 | fiat_25519_uint1 x3 = (fiat_25519_uint1)(x1 >> 51); |
| 29 | *out1 = x2; |
| 30 | *out2 = x3; |
| 31 | } |
| 32 | |
| 33 | /* |
| 34 | * Input Bounds: |
| 35 | * arg1: [0x0 ~> 0x1] |
| 36 | * arg2: [0x0 ~> 0x7ffffffffffff] |
| 37 | * arg3: [0x0 ~> 0x7ffffffffffff] |
| 38 | * Output Bounds: |
| 39 | * out1: [0x0 ~> 0x7ffffffffffff] |
| 40 | * out2: [0x0 ~> 0x1] |
| 41 | */ |
| 42 | static void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { |
| 43 | int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3); |
| 44 | fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 51); |
| 45 | uint64_t x3 = (x1 & UINT64_C(0x7ffffffffffff)); |
| 46 | *out1 = x3; |
| 47 | *out2 = (fiat_25519_uint1)(0x0 - x2); |
| 48 | } |
| 49 | |
| 50 | /* |
| 51 | * Input Bounds: |
| 52 | * arg1: [0x0 ~> 0x1] |
| 53 | * arg2: [0x0 ~> 0xffffffffffffffff] |
| 54 | * arg3: [0x0 ~> 0xffffffffffffffff] |
| 55 | * Output Bounds: |
| 56 | * out1: [0x0 ~> 0xffffffffffffffff] |
| 57 | */ |
| 58 | static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { |
| 59 | fiat_25519_uint1 x1 = (!(!arg1)); |
| 60 | uint64_t x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); |
Pete Bentley | 0c61efe | 2019-08-13 09:32:23 +0100 | [diff] [blame^] | 61 | // Note this line has been patched from the synthesized code to add value |
| 62 | // barriers. |
| 63 | // |
| 64 | // Clang recognizes this pattern as a select. While it usually transforms it |
| 65 | // to a cmov, it sometimes further transforms it into a branch, which we do |
| 66 | // not want. |
| 67 | uint64_t x3 = ((value_barrier_u64(x2) & arg3) | (value_barrier_u64(~x2) & arg2)); |
Robert Sloan | 4c22c5f | 2019-03-01 15:53:37 -0800 | [diff] [blame] | 68 | *out1 = x3; |
| 69 | } |
| 70 | |
| 71 | /* |
| 72 | * Input Bounds: |
| 73 | * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 74 | * arg2: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 75 | * Output Bounds: |
| 76 | * out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 77 | */ |
| 78 | static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) { |
| 79 | fiat_25519_uint128 x1 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13))); |
| 80 | fiat_25519_uint128 x2 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[3]) * (uint64_t)UINT8_C(0x13))); |
| 81 | fiat_25519_uint128 x3 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[2]) * (uint64_t)UINT8_C(0x13))); |
| 82 | fiat_25519_uint128 x4 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[1]) * (uint64_t)UINT8_C(0x13))); |
| 83 | fiat_25519_uint128 x5 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13))); |
| 84 | fiat_25519_uint128 x6 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[3]) * (uint64_t)UINT8_C(0x13))); |
| 85 | fiat_25519_uint128 x7 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * (uint64_t)UINT8_C(0x13))); |
| 86 | fiat_25519_uint128 x8 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13))); |
| 87 | fiat_25519_uint128 x9 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * (uint64_t)UINT8_C(0x13))); |
| 88 | fiat_25519_uint128 x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13))); |
| 89 | fiat_25519_uint128 x11 = ((fiat_25519_uint128)(arg1[4]) * (arg2[0])); |
| 90 | fiat_25519_uint128 x12 = ((fiat_25519_uint128)(arg1[3]) * (arg2[1])); |
| 91 | fiat_25519_uint128 x13 = ((fiat_25519_uint128)(arg1[3]) * (arg2[0])); |
| 92 | fiat_25519_uint128 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg2[2])); |
| 93 | fiat_25519_uint128 x15 = ((fiat_25519_uint128)(arg1[2]) * (arg2[1])); |
| 94 | fiat_25519_uint128 x16 = ((fiat_25519_uint128)(arg1[2]) * (arg2[0])); |
| 95 | fiat_25519_uint128 x17 = ((fiat_25519_uint128)(arg1[1]) * (arg2[3])); |
| 96 | fiat_25519_uint128 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg2[2])); |
| 97 | fiat_25519_uint128 x19 = ((fiat_25519_uint128)(arg1[1]) * (arg2[1])); |
| 98 | fiat_25519_uint128 x20 = ((fiat_25519_uint128)(arg1[1]) * (arg2[0])); |
| 99 | fiat_25519_uint128 x21 = ((fiat_25519_uint128)(arg1[0]) * (arg2[4])); |
| 100 | fiat_25519_uint128 x22 = ((fiat_25519_uint128)(arg1[0]) * (arg2[3])); |
| 101 | fiat_25519_uint128 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg2[2])); |
| 102 | fiat_25519_uint128 x24 = ((fiat_25519_uint128)(arg1[0]) * (arg2[1])); |
| 103 | fiat_25519_uint128 x25 = ((fiat_25519_uint128)(arg1[0]) * (arg2[0])); |
| 104 | fiat_25519_uint128 x26 = (x25 + (x10 + (x9 + (x7 + x4)))); |
| 105 | uint64_t x27 = (uint64_t)(x26 >> 51); |
| 106 | uint64_t x28 = (uint64_t)(x26 & UINT64_C(0x7ffffffffffff)); |
| 107 | fiat_25519_uint128 x29 = (x21 + (x17 + (x14 + (x12 + x11)))); |
| 108 | fiat_25519_uint128 x30 = (x22 + (x18 + (x15 + (x13 + x1)))); |
| 109 | fiat_25519_uint128 x31 = (x23 + (x19 + (x16 + (x5 + x2)))); |
| 110 | fiat_25519_uint128 x32 = (x24 + (x20 + (x8 + (x6 + x3)))); |
| 111 | fiat_25519_uint128 x33 = (x27 + x32); |
| 112 | uint64_t x34 = (uint64_t)(x33 >> 51); |
| 113 | uint64_t x35 = (uint64_t)(x33 & UINT64_C(0x7ffffffffffff)); |
| 114 | fiat_25519_uint128 x36 = (x34 + x31); |
| 115 | uint64_t x37 = (uint64_t)(x36 >> 51); |
| 116 | uint64_t x38 = (uint64_t)(x36 & UINT64_C(0x7ffffffffffff)); |
| 117 | fiat_25519_uint128 x39 = (x37 + x30); |
| 118 | uint64_t x40 = (uint64_t)(x39 >> 51); |
| 119 | uint64_t x41 = (uint64_t)(x39 & UINT64_C(0x7ffffffffffff)); |
| 120 | fiat_25519_uint128 x42 = (x40 + x29); |
| 121 | uint64_t x43 = (uint64_t)(x42 >> 51); |
| 122 | uint64_t x44 = (uint64_t)(x42 & UINT64_C(0x7ffffffffffff)); |
| 123 | uint64_t x45 = (x43 * (uint64_t)UINT8_C(0x13)); |
| 124 | uint64_t x46 = (x28 + x45); |
| 125 | uint64_t x47 = (x46 >> 51); |
| 126 | uint64_t x48 = (x46 & UINT64_C(0x7ffffffffffff)); |
| 127 | uint64_t x49 = (x47 + x35); |
| 128 | uint64_t x50 = (x49 >> 51); |
| 129 | uint64_t x51 = (x49 & UINT64_C(0x7ffffffffffff)); |
| 130 | uint64_t x52 = (x50 + x38); |
| 131 | out1[0] = x48; |
| 132 | out1[1] = x51; |
| 133 | out1[2] = x52; |
| 134 | out1[3] = x41; |
| 135 | out1[4] = x44; |
| 136 | } |
| 137 | |
| 138 | /* |
| 139 | * Input Bounds: |
| 140 | * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 141 | * Output Bounds: |
| 142 | * out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 143 | */ |
| 144 | static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) { |
| 145 | uint64_t x1 = ((arg1[4]) * (uint64_t)UINT8_C(0x13)); |
| 146 | uint64_t x2 = (x1 * (uint64_t)0x2); |
| 147 | uint64_t x3 = ((arg1[4]) * (uint64_t)0x2); |
| 148 | uint64_t x4 = ((arg1[3]) * (uint64_t)UINT8_C(0x13)); |
| 149 | uint64_t x5 = (x4 * (uint64_t)0x2); |
| 150 | uint64_t x6 = ((arg1[3]) * (uint64_t)0x2); |
| 151 | uint64_t x7 = ((arg1[2]) * (uint64_t)0x2); |
| 152 | uint64_t x8 = ((arg1[1]) * (uint64_t)0x2); |
| 153 | fiat_25519_uint128 x9 = ((fiat_25519_uint128)(arg1[4]) * x1); |
| 154 | fiat_25519_uint128 x10 = ((fiat_25519_uint128)(arg1[3]) * x2); |
| 155 | fiat_25519_uint128 x11 = ((fiat_25519_uint128)(arg1[3]) * x4); |
| 156 | fiat_25519_uint128 x12 = ((fiat_25519_uint128)(arg1[2]) * x2); |
| 157 | fiat_25519_uint128 x13 = ((fiat_25519_uint128)(arg1[2]) * x5); |
| 158 | fiat_25519_uint128 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg1[2])); |
| 159 | fiat_25519_uint128 x15 = ((fiat_25519_uint128)(arg1[1]) * x2); |
| 160 | fiat_25519_uint128 x16 = ((fiat_25519_uint128)(arg1[1]) * x6); |
| 161 | fiat_25519_uint128 x17 = ((fiat_25519_uint128)(arg1[1]) * x7); |
| 162 | fiat_25519_uint128 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg1[1])); |
| 163 | fiat_25519_uint128 x19 = ((fiat_25519_uint128)(arg1[0]) * x3); |
| 164 | fiat_25519_uint128 x20 = ((fiat_25519_uint128)(arg1[0]) * x6); |
| 165 | fiat_25519_uint128 x21 = ((fiat_25519_uint128)(arg1[0]) * x7); |
| 166 | fiat_25519_uint128 x22 = ((fiat_25519_uint128)(arg1[0]) * x8); |
| 167 | fiat_25519_uint128 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg1[0])); |
| 168 | fiat_25519_uint128 x24 = (x23 + (x15 + x13)); |
| 169 | uint64_t x25 = (uint64_t)(x24 >> 51); |
| 170 | uint64_t x26 = (uint64_t)(x24 & UINT64_C(0x7ffffffffffff)); |
| 171 | fiat_25519_uint128 x27 = (x19 + (x16 + x14)); |
| 172 | fiat_25519_uint128 x28 = (x20 + (x17 + x9)); |
| 173 | fiat_25519_uint128 x29 = (x21 + (x18 + x10)); |
| 174 | fiat_25519_uint128 x30 = (x22 + (x12 + x11)); |
| 175 | fiat_25519_uint128 x31 = (x25 + x30); |
| 176 | uint64_t x32 = (uint64_t)(x31 >> 51); |
| 177 | uint64_t x33 = (uint64_t)(x31 & UINT64_C(0x7ffffffffffff)); |
| 178 | fiat_25519_uint128 x34 = (x32 + x29); |
| 179 | uint64_t x35 = (uint64_t)(x34 >> 51); |
| 180 | uint64_t x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff)); |
| 181 | fiat_25519_uint128 x37 = (x35 + x28); |
| 182 | uint64_t x38 = (uint64_t)(x37 >> 51); |
| 183 | uint64_t x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff)); |
| 184 | fiat_25519_uint128 x40 = (x38 + x27); |
| 185 | uint64_t x41 = (uint64_t)(x40 >> 51); |
| 186 | uint64_t x42 = (uint64_t)(x40 & UINT64_C(0x7ffffffffffff)); |
| 187 | uint64_t x43 = (x41 * (uint64_t)UINT8_C(0x13)); |
| 188 | uint64_t x44 = (x26 + x43); |
| 189 | uint64_t x45 = (x44 >> 51); |
| 190 | uint64_t x46 = (x44 & UINT64_C(0x7ffffffffffff)); |
| 191 | uint64_t x47 = (x45 + x33); |
| 192 | uint64_t x48 = (x47 >> 51); |
| 193 | uint64_t x49 = (x47 & UINT64_C(0x7ffffffffffff)); |
| 194 | uint64_t x50 = (x48 + x36); |
| 195 | out1[0] = x46; |
| 196 | out1[1] = x49; |
| 197 | out1[2] = x50; |
| 198 | out1[3] = x39; |
| 199 | out1[4] = x42; |
| 200 | } |
| 201 | |
| 202 | /* |
| 203 | * Input Bounds: |
| 204 | * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 205 | * Output Bounds: |
| 206 | * out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 207 | */ |
| 208 | static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[5]) { |
| 209 | fiat_25519_uint128 x1 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[4])); |
| 210 | fiat_25519_uint128 x2 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[3])); |
| 211 | fiat_25519_uint128 x3 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[2])); |
| 212 | fiat_25519_uint128 x4 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[1])); |
| 213 | fiat_25519_uint128 x5 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[0])); |
| 214 | uint64_t x6 = (uint64_t)(x5 >> 51); |
| 215 | uint64_t x7 = (uint64_t)(x5 & UINT64_C(0x7ffffffffffff)); |
| 216 | fiat_25519_uint128 x8 = (x6 + x4); |
| 217 | uint64_t x9 = (uint64_t)(x8 >> 51); |
| 218 | uint64_t x10 = (uint64_t)(x8 & UINT64_C(0x7ffffffffffff)); |
| 219 | fiat_25519_uint128 x11 = (x9 + x3); |
| 220 | uint64_t x12 = (uint64_t)(x11 >> 51); |
| 221 | uint64_t x13 = (uint64_t)(x11 & UINT64_C(0x7ffffffffffff)); |
| 222 | fiat_25519_uint128 x14 = (x12 + x2); |
| 223 | uint64_t x15 = (uint64_t)(x14 >> 51); |
| 224 | uint64_t x16 = (uint64_t)(x14 & UINT64_C(0x7ffffffffffff)); |
| 225 | fiat_25519_uint128 x17 = (x15 + x1); |
| 226 | uint64_t x18 = (uint64_t)(x17 >> 51); |
| 227 | uint64_t x19 = (uint64_t)(x17 & UINT64_C(0x7ffffffffffff)); |
| 228 | uint64_t x20 = (x18 * (uint64_t)UINT8_C(0x13)); |
| 229 | uint64_t x21 = (x7 + x20); |
| 230 | uint64_t x22 = (x21 >> 51); |
| 231 | uint64_t x23 = (x21 & UINT64_C(0x7ffffffffffff)); |
| 232 | uint64_t x24 = (x22 + x10); |
| 233 | uint64_t x25 = (x24 >> 51); |
| 234 | uint64_t x26 = (x24 & UINT64_C(0x7ffffffffffff)); |
| 235 | uint64_t x27 = (x25 + x13); |
| 236 | out1[0] = x23; |
| 237 | out1[1] = x26; |
| 238 | out1[2] = x27; |
| 239 | out1[3] = x16; |
| 240 | out1[4] = x19; |
| 241 | } |
| 242 | |
| 243 | /* |
| 244 | * Input Bounds: |
| 245 | * arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 246 | * Output Bounds: |
| 247 | * out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 248 | */ |
| 249 | static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) { |
| 250 | uint64_t x1 = (arg1[0]); |
| 251 | uint64_t x2 = ((x1 >> 51) + (arg1[1])); |
| 252 | uint64_t x3 = ((x2 >> 51) + (arg1[2])); |
| 253 | uint64_t x4 = ((x3 >> 51) + (arg1[3])); |
| 254 | uint64_t x5 = ((x4 >> 51) + (arg1[4])); |
| 255 | uint64_t x6 = ((x1 & UINT64_C(0x7ffffffffffff)) + ((x5 >> 51) * (uint64_t)UINT8_C(0x13))); |
| 256 | uint64_t x7 = ((x6 >> 51) + (x2 & UINT64_C(0x7ffffffffffff))); |
| 257 | uint64_t x8 = (x6 & UINT64_C(0x7ffffffffffff)); |
| 258 | uint64_t x9 = (x7 & UINT64_C(0x7ffffffffffff)); |
| 259 | uint64_t x10 = ((x7 >> 51) + (x3 & UINT64_C(0x7ffffffffffff))); |
| 260 | uint64_t x11 = (x4 & UINT64_C(0x7ffffffffffff)); |
| 261 | uint64_t x12 = (x5 & UINT64_C(0x7ffffffffffff)); |
| 262 | out1[0] = x8; |
| 263 | out1[1] = x9; |
| 264 | out1[2] = x10; |
| 265 | out1[3] = x11; |
| 266 | out1[4] = x12; |
| 267 | } |
| 268 | |
| 269 | /* |
| 270 | * Input Bounds: |
| 271 | * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 272 | * arg2: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 273 | * Output Bounds: |
| 274 | * out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 275 | */ |
| 276 | static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) { |
| 277 | uint64_t x1 = ((arg1[0]) + (arg2[0])); |
| 278 | uint64_t x2 = ((arg1[1]) + (arg2[1])); |
| 279 | uint64_t x3 = ((arg1[2]) + (arg2[2])); |
| 280 | uint64_t x4 = ((arg1[3]) + (arg2[3])); |
| 281 | uint64_t x5 = ((arg1[4]) + (arg2[4])); |
| 282 | out1[0] = x1; |
| 283 | out1[1] = x2; |
| 284 | out1[2] = x3; |
| 285 | out1[3] = x4; |
| 286 | out1[4] = x5; |
| 287 | } |
| 288 | |
| 289 | /* |
| 290 | * Input Bounds: |
| 291 | * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 292 | * arg2: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 293 | * Output Bounds: |
| 294 | * out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 295 | */ |
| 296 | static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) { |
| 297 | uint64_t x1 = ((UINT64_C(0xfffffffffffda) + (arg1[0])) - (arg2[0])); |
| 298 | uint64_t x2 = ((UINT64_C(0xffffffffffffe) + (arg1[1])) - (arg2[1])); |
| 299 | uint64_t x3 = ((UINT64_C(0xffffffffffffe) + (arg1[2])) - (arg2[2])); |
| 300 | uint64_t x4 = ((UINT64_C(0xffffffffffffe) + (arg1[3])) - (arg2[3])); |
| 301 | uint64_t x5 = ((UINT64_C(0xffffffffffffe) + (arg1[4])) - (arg2[4])); |
| 302 | out1[0] = x1; |
| 303 | out1[1] = x2; |
| 304 | out1[2] = x3; |
| 305 | out1[3] = x4; |
| 306 | out1[4] = x5; |
| 307 | } |
| 308 | |
| 309 | /* |
| 310 | * Input Bounds: |
| 311 | * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 312 | * Output Bounds: |
| 313 | * out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]] |
| 314 | */ |
| 315 | static void fiat_25519_opp(uint64_t out1[5], const uint64_t arg1[5]) { |
| 316 | uint64_t x1 = (UINT64_C(0xfffffffffffda) - (arg1[0])); |
| 317 | uint64_t x2 = (UINT64_C(0xffffffffffffe) - (arg1[1])); |
| 318 | uint64_t x3 = (UINT64_C(0xffffffffffffe) - (arg1[2])); |
| 319 | uint64_t x4 = (UINT64_C(0xffffffffffffe) - (arg1[3])); |
| 320 | uint64_t x5 = (UINT64_C(0xffffffffffffe) - (arg1[4])); |
| 321 | out1[0] = x1; |
| 322 | out1[1] = x2; |
| 323 | out1[2] = x3; |
| 324 | out1[3] = x4; |
| 325 | out1[4] = x5; |
| 326 | } |
| 327 | |
| 328 | /* |
| 329 | * Input Bounds: |
| 330 | * arg1: [0x0 ~> 0x1] |
| 331 | * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] |
| 332 | * arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] |
| 333 | * Output Bounds: |
| 334 | * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] |
| 335 | */ |
| 336 | static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const uint64_t arg2[5], const uint64_t arg3[5]) { |
| 337 | uint64_t x1; |
| 338 | fiat_25519_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0])); |
| 339 | uint64_t x2; |
| 340 | fiat_25519_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1])); |
| 341 | uint64_t x3; |
| 342 | fiat_25519_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2])); |
| 343 | uint64_t x4; |
| 344 | fiat_25519_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3])); |
| 345 | uint64_t x5; |
| 346 | fiat_25519_cmovznz_u64(&x5, arg1, (arg2[4]), (arg3[4])); |
| 347 | out1[0] = x1; |
| 348 | out1[1] = x2; |
| 349 | out1[2] = x3; |
| 350 | out1[3] = x4; |
| 351 | out1[4] = x5; |
| 352 | } |
| 353 | |
| 354 | /* |
| 355 | * Input Bounds: |
| 356 | * arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 357 | * Output Bounds: |
| 358 | * 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 ~> 0x7f]] |
| 359 | */ |
| 360 | static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) { |
| 361 | uint64_t x1; |
| 362 | fiat_25519_uint1 x2; |
| 363 | fiat_25519_subborrowx_u51(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0x7ffffffffffed)); |
| 364 | uint64_t x3; |
| 365 | fiat_25519_uint1 x4; |
| 366 | fiat_25519_subborrowx_u51(&x3, &x4, x2, (arg1[1]), UINT64_C(0x7ffffffffffff)); |
| 367 | uint64_t x5; |
| 368 | fiat_25519_uint1 x6; |
| 369 | fiat_25519_subborrowx_u51(&x5, &x6, x4, (arg1[2]), UINT64_C(0x7ffffffffffff)); |
| 370 | uint64_t x7; |
| 371 | fiat_25519_uint1 x8; |
| 372 | fiat_25519_subborrowx_u51(&x7, &x8, x6, (arg1[3]), UINT64_C(0x7ffffffffffff)); |
| 373 | uint64_t x9; |
| 374 | fiat_25519_uint1 x10; |
| 375 | fiat_25519_subborrowx_u51(&x9, &x10, x8, (arg1[4]), UINT64_C(0x7ffffffffffff)); |
| 376 | uint64_t x11; |
| 377 | fiat_25519_cmovznz_u64(&x11, x10, 0x0, UINT64_C(0xffffffffffffffff)); |
| 378 | uint64_t x12; |
| 379 | fiat_25519_uint1 x13; |
| 380 | fiat_25519_addcarryx_u51(&x12, &x13, 0x0, (x11 & UINT64_C(0x7ffffffffffed)), x1); |
| 381 | uint64_t x14; |
| 382 | fiat_25519_uint1 x15; |
| 383 | fiat_25519_addcarryx_u51(&x14, &x15, x13, (x11 & UINT64_C(0x7ffffffffffff)), x3); |
| 384 | uint64_t x16; |
| 385 | fiat_25519_uint1 x17; |
| 386 | fiat_25519_addcarryx_u51(&x16, &x17, x15, (x11 & UINT64_C(0x7ffffffffffff)), x5); |
| 387 | uint64_t x18; |
| 388 | fiat_25519_uint1 x19; |
| 389 | fiat_25519_addcarryx_u51(&x18, &x19, x17, (x11 & UINT64_C(0x7ffffffffffff)), x7); |
| 390 | uint64_t x20; |
| 391 | fiat_25519_uint1 x21; |
| 392 | fiat_25519_addcarryx_u51(&x20, &x21, x19, (x11 & UINT64_C(0x7ffffffffffff)), x9); |
| 393 | uint64_t x22 = (x20 << 4); |
| 394 | uint64_t x23 = (x18 * (uint64_t)0x2); |
| 395 | uint64_t x24 = (x16 << 6); |
| 396 | uint64_t x25 = (x14 << 3); |
| 397 | uint64_t x26 = (x12 >> 8); |
| 398 | uint8_t x27 = (uint8_t)(x12 & UINT8_C(0xff)); |
| 399 | uint64_t x28 = (x26 >> 8); |
| 400 | uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); |
| 401 | uint64_t x30 = (x28 >> 8); |
| 402 | uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); |
| 403 | uint64_t x32 = (x30 >> 8); |
| 404 | uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); |
| 405 | uint64_t x34 = (x32 >> 8); |
| 406 | uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); |
| 407 | uint8_t x36 = (uint8_t)(x34 >> 8); |
| 408 | uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff)); |
| 409 | uint64_t x38 = (x36 + x25); |
| 410 | uint64_t x39 = (x38 >> 8); |
| 411 | uint8_t x40 = (uint8_t)(x38 & UINT8_C(0xff)); |
| 412 | uint64_t x41 = (x39 >> 8); |
| 413 | uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); |
| 414 | uint64_t x43 = (x41 >> 8); |
| 415 | uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); |
| 416 | uint64_t x45 = (x43 >> 8); |
| 417 | uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); |
| 418 | uint64_t x47 = (x45 >> 8); |
| 419 | uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); |
| 420 | uint8_t x49 = (uint8_t)(x47 >> 8); |
| 421 | uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); |
| 422 | uint64_t x51 = (x49 + x24); |
| 423 | uint64_t x52 = (x51 >> 8); |
| 424 | uint8_t x53 = (uint8_t)(x51 & UINT8_C(0xff)); |
| 425 | uint64_t x54 = (x52 >> 8); |
| 426 | uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); |
| 427 | uint64_t x56 = (x54 >> 8); |
| 428 | uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); |
| 429 | uint64_t x58 = (x56 >> 8); |
| 430 | uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); |
| 431 | uint64_t x60 = (x58 >> 8); |
| 432 | uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); |
| 433 | uint64_t x62 = (x60 >> 8); |
| 434 | uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); |
| 435 | fiat_25519_uint1 x64 = (fiat_25519_uint1)(x62 >> 8); |
| 436 | uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff)); |
| 437 | uint64_t x66 = (x64 + x23); |
| 438 | uint64_t x67 = (x66 >> 8); |
| 439 | uint8_t x68 = (uint8_t)(x66 & UINT8_C(0xff)); |
| 440 | uint64_t x69 = (x67 >> 8); |
| 441 | uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); |
| 442 | uint64_t x71 = (x69 >> 8); |
| 443 | uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff)); |
| 444 | uint64_t x73 = (x71 >> 8); |
| 445 | uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff)); |
| 446 | uint64_t x75 = (x73 >> 8); |
| 447 | uint8_t x76 = (uint8_t)(x73 & UINT8_C(0xff)); |
| 448 | uint8_t x77 = (uint8_t)(x75 >> 8); |
| 449 | uint8_t x78 = (uint8_t)(x75 & UINT8_C(0xff)); |
| 450 | uint64_t x79 = (x77 + x22); |
| 451 | uint64_t x80 = (x79 >> 8); |
| 452 | uint8_t x81 = (uint8_t)(x79 & UINT8_C(0xff)); |
| 453 | uint64_t x82 = (x80 >> 8); |
| 454 | uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff)); |
| 455 | uint64_t x84 = (x82 >> 8); |
| 456 | uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff)); |
| 457 | uint64_t x86 = (x84 >> 8); |
| 458 | uint8_t x87 = (uint8_t)(x84 & UINT8_C(0xff)); |
| 459 | uint64_t x88 = (x86 >> 8); |
| 460 | uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff)); |
| 461 | uint8_t x90 = (uint8_t)(x88 >> 8); |
| 462 | uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff)); |
| 463 | out1[0] = x27; |
| 464 | out1[1] = x29; |
| 465 | out1[2] = x31; |
| 466 | out1[3] = x33; |
| 467 | out1[4] = x35; |
| 468 | out1[5] = x37; |
| 469 | out1[6] = x40; |
| 470 | out1[7] = x42; |
| 471 | out1[8] = x44; |
| 472 | out1[9] = x46; |
| 473 | out1[10] = x48; |
| 474 | out1[11] = x50; |
| 475 | out1[12] = x53; |
| 476 | out1[13] = x55; |
| 477 | out1[14] = x57; |
| 478 | out1[15] = x59; |
| 479 | out1[16] = x61; |
| 480 | out1[17] = x63; |
| 481 | out1[18] = x65; |
| 482 | out1[19] = x68; |
| 483 | out1[20] = x70; |
| 484 | out1[21] = x72; |
| 485 | out1[22] = x74; |
| 486 | out1[23] = x76; |
| 487 | out1[24] = x78; |
| 488 | out1[25] = x81; |
| 489 | out1[26] = x83; |
| 490 | out1[27] = x85; |
| 491 | out1[28] = x87; |
| 492 | out1[29] = x89; |
| 493 | out1[30] = x91; |
| 494 | out1[31] = x90; |
| 495 | } |
| 496 | |
| 497 | /* |
| 498 | * Input Bounds: |
| 499 | * arg1: [[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 ~> 0x7f]] |
| 500 | * Output Bounds: |
| 501 | * out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]] |
| 502 | */ |
| 503 | static void fiat_25519_from_bytes(uint64_t out1[5], const uint8_t arg1[32]) { |
| 504 | uint64_t x1 = ((uint64_t)(arg1[31]) << 44); |
| 505 | uint64_t x2 = ((uint64_t)(arg1[30]) << 36); |
| 506 | uint64_t x3 = ((uint64_t)(arg1[29]) << 28); |
| 507 | uint64_t x4 = ((uint64_t)(arg1[28]) << 20); |
| 508 | uint64_t x5 = ((uint64_t)(arg1[27]) << 12); |
| 509 | uint64_t x6 = ((uint64_t)(arg1[26]) << 4); |
| 510 | uint64_t x7 = ((uint64_t)(arg1[25]) << 47); |
| 511 | uint64_t x8 = ((uint64_t)(arg1[24]) << 39); |
| 512 | uint64_t x9 = ((uint64_t)(arg1[23]) << 31); |
| 513 | uint64_t x10 = ((uint64_t)(arg1[22]) << 23); |
| 514 | uint64_t x11 = ((uint64_t)(arg1[21]) << 15); |
| 515 | uint64_t x12 = ((uint64_t)(arg1[20]) << 7); |
| 516 | uint64_t x13 = ((uint64_t)(arg1[19]) << 50); |
| 517 | uint64_t x14 = ((uint64_t)(arg1[18]) << 42); |
| 518 | uint64_t x15 = ((uint64_t)(arg1[17]) << 34); |
| 519 | uint64_t x16 = ((uint64_t)(arg1[16]) << 26); |
| 520 | uint64_t x17 = ((uint64_t)(arg1[15]) << 18); |
| 521 | uint64_t x18 = ((uint64_t)(arg1[14]) << 10); |
| 522 | uint64_t x19 = ((uint64_t)(arg1[13]) << 2); |
| 523 | uint64_t x20 = ((uint64_t)(arg1[12]) << 45); |
| 524 | uint64_t x21 = ((uint64_t)(arg1[11]) << 37); |
| 525 | uint64_t x22 = ((uint64_t)(arg1[10]) << 29); |
| 526 | uint64_t x23 = ((uint64_t)(arg1[9]) << 21); |
| 527 | uint64_t x24 = ((uint64_t)(arg1[8]) << 13); |
| 528 | uint64_t x25 = ((uint64_t)(arg1[7]) << 5); |
| 529 | uint64_t x26 = ((uint64_t)(arg1[6]) << 48); |
| 530 | uint64_t x27 = ((uint64_t)(arg1[5]) << 40); |
| 531 | uint64_t x28 = ((uint64_t)(arg1[4]) << 32); |
| 532 | uint64_t x29 = ((uint64_t)(arg1[3]) << 24); |
| 533 | uint64_t x30 = ((uint64_t)(arg1[2]) << 16); |
| 534 | uint64_t x31 = ((uint64_t)(arg1[1]) << 8); |
| 535 | uint8_t x32 = (arg1[0]); |
| 536 | uint64_t x33 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + x26)))))); |
| 537 | uint8_t x34 = (uint8_t)(x33 >> 51); |
| 538 | uint64_t x35 = (x33 & UINT64_C(0x7ffffffffffff)); |
| 539 | uint64_t x36 = (x6 + (x5 + (x4 + (x3 + (x2 + x1))))); |
| 540 | uint64_t x37 = (x12 + (x11 + (x10 + (x9 + (x8 + x7))))); |
| 541 | uint64_t x38 = (x19 + (x18 + (x17 + (x16 + (x15 + (x14 + x13)))))); |
| 542 | uint64_t x39 = (x25 + (x24 + (x23 + (x22 + (x21 + x20))))); |
| 543 | uint64_t x40 = (x34 + x39); |
| 544 | uint8_t x41 = (uint8_t)(x40 >> 51); |
| 545 | uint64_t x42 = (x40 & UINT64_C(0x7ffffffffffff)); |
| 546 | uint64_t x43 = (x41 + x38); |
| 547 | uint8_t x44 = (uint8_t)(x43 >> 51); |
| 548 | uint64_t x45 = (x43 & UINT64_C(0x7ffffffffffff)); |
| 549 | uint64_t x46 = (x44 + x37); |
| 550 | uint8_t x47 = (uint8_t)(x46 >> 51); |
| 551 | uint64_t x48 = (x46 & UINT64_C(0x7ffffffffffff)); |
| 552 | uint64_t x49 = (x47 + x36); |
| 553 | out1[0] = x35; |
| 554 | out1[1] = x42; |
| 555 | out1[2] = x45; |
| 556 | out1[3] = x48; |
| 557 | out1[4] = x49; |
| 558 | } |
| 559 | |