1 #if defined(BORINGSSL_CURVE25519_64BIT) 2 3 /* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier 25519 64 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666 */ 4 /* curve description: 25519 */ 5 /* machine_wordsize = 64 (from "64") */ 6 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666 */ 7 /* n = 5 (from "(auto)") */ 8 /* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */ 9 /* tight_bounds_multiplier = 1 (from "") */ 10 /* */ 11 /* Computed values: */ 12 /* carry_chain = [0, 1, 2, 3, 4, 0, 1] */ 13 /* eval z = z[0] + (z[1] << 51) + (z[2] << 102) + (z[3] << 153) + (z[4] << 204) */ 14 /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */ 15 /* balance = [0xfffffffffffda, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe] */ 16 17 #include <stdint.h> 18 typedef unsigned char fiat_25519_uint1; 19 typedef signed char fiat_25519_int1; 20 #if defined(__GNUC__) || defined(__clang__) 21 # define FIAT_25519_FIAT_EXTENSION __extension__ 22 # define FIAT_25519_FIAT_INLINE __inline__ 23 #else 24 # define FIAT_25519_FIAT_EXTENSION 25 # define FIAT_25519_FIAT_INLINE 26 #endif 27 28 FIAT_25519_FIAT_EXTENSION typedef int128_t fiat_25519_int128; 29 FIAT_25519_FIAT_EXTENSION typedef uint128_t fiat_25519_uint128; 30 31 /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ 32 /* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */ 33 typedef uint64_t fiat_25519_loose_field_element[5]; 34 35 /* The type fiat_25519_tight_field_element is a field element with tight bounds. */ 36 /* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */ 37 typedef uint64_t fiat_25519_tight_field_element[5]; 38 39 #if (-1 & 3) != 3 40 #error "This code only works on a two's complement system" 41 #endif 42 43 #if !defined(FIAT_25519_NO_ASM) && (defined(__GNUC__) || defined(__clang__)) 44 static __inline__ uint64_t fiat_25519_value_barrier_u64(uint64_t a) { 45 __asm__("" : "+r"(a) : /* no inputs */); 46 return a; 47 } 48 #else 49 # define fiat_25519_value_barrier_u64(x) (x) 50 #endif 51 52 53 /* 54 * The function fiat_25519_addcarryx_u51 is an addition with carry. 55 * 56 * Postconditions: 57 * out1 = (arg1 + arg2 + arg3) mod 2^51 58 * out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋ 59 * 60 * Input Bounds: 61 * arg1: [0x0 ~> 0x1] 62 * arg2: [0x0 ~> 0x7ffffffffffff] 63 * arg3: [0x0 ~> 0x7ffffffffffff] 64 * Output Bounds: 65 * out1: [0x0 ~> 0x7ffffffffffff] 66 * out2: [0x0 ~> 0x1] 67 */ 68 static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { 69 uint64_t x1; 70 uint64_t x2; 71 fiat_25519_uint1 x3; 72 x1 = ((arg1 + arg2) + arg3); 73 x2 = (x1 & UINT64_C(0x7ffffffffffff)); 74 x3 = (fiat_25519_uint1)(x1 >> 51); 75 *out1 = x2; 76 *out2 = x3; 77 } 78 79 /* 80 * The function fiat_25519_subborrowx_u51 is a subtraction with borrow. 81 * 82 * Postconditions: 83 * out1 = (-arg1 + arg2 + -arg3) mod 2^51 84 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋ 85 * 86 * Input Bounds: 87 * arg1: [0x0 ~> 0x1] 88 * arg2: [0x0 ~> 0x7ffffffffffff] 89 * arg3: [0x0 ~> 0x7ffffffffffff] 90 * Output Bounds: 91 * out1: [0x0 ~> 0x7ffffffffffff] 92 * out2: [0x0 ~> 0x1] 93 */ 94 static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { 95 int64_t x1; 96 fiat_25519_int1 x2; 97 uint64_t x3; 98 x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3); 99 x2 = (fiat_25519_int1)(x1 >> 51); 100 x3 = (x1 & UINT64_C(0x7ffffffffffff)); 101 *out1 = x3; 102 *out2 = (fiat_25519_uint1)(0x0 - x2); 103 } 104 105 /* 106 * The function fiat_25519_cmovznz_u64 is a single-word conditional move. 107 * 108 * Postconditions: 109 * out1 = (if arg1 = 0 then arg2 else arg3) 110 * 111 * Input Bounds: 112 * arg1: [0x0 ~> 0x1] 113 * arg2: [0x0 ~> 0xffffffffffffffff] 114 * arg3: [0x0 ~> 0xffffffffffffffff] 115 * Output Bounds: 116 * out1: [0x0 ~> 0xffffffffffffffff] 117 */ 118 static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { 119 fiat_25519_uint1 x1; 120 uint64_t x2; 121 uint64_t x3; 122 x1 = (!(!arg1)); 123 x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); 124 x3 = ((fiat_25519_value_barrier_u64(x2) & arg3) | (fiat_25519_value_barrier_u64((~x2)) & arg2)); 125 *out1 = x3; 126 } 127 128 /* 129 * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. 130 * 131 * Postconditions: 132 * eval out1 mod m = (eval arg1 * eval arg2) mod m 133 * 134 */ 135 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_mul(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1, const fiat_25519_loose_field_element arg2) { 136 fiat_25519_uint128 x1; 137 fiat_25519_uint128 x2; 138 fiat_25519_uint128 x3; 139 fiat_25519_uint128 x4; 140 fiat_25519_uint128 x5; 141 fiat_25519_uint128 x6; 142 fiat_25519_uint128 x7; 143 fiat_25519_uint128 x8; 144 fiat_25519_uint128 x9; 145 fiat_25519_uint128 x10; 146 fiat_25519_uint128 x11; 147 fiat_25519_uint128 x12; 148 fiat_25519_uint128 x13; 149 fiat_25519_uint128 x14; 150 fiat_25519_uint128 x15; 151 fiat_25519_uint128 x16; 152 fiat_25519_uint128 x17; 153 fiat_25519_uint128 x18; 154 fiat_25519_uint128 x19; 155 fiat_25519_uint128 x20; 156 fiat_25519_uint128 x21; 157 fiat_25519_uint128 x22; 158 fiat_25519_uint128 x23; 159 fiat_25519_uint128 x24; 160 fiat_25519_uint128 x25; 161 fiat_25519_uint128 x26; 162 uint64_t x27; 163 uint64_t x28; 164 fiat_25519_uint128 x29; 165 fiat_25519_uint128 x30; 166 fiat_25519_uint128 x31; 167 fiat_25519_uint128 x32; 168 fiat_25519_uint128 x33; 169 uint64_t x34; 170 uint64_t x35; 171 fiat_25519_uint128 x36; 172 uint64_t x37; 173 uint64_t x38; 174 fiat_25519_uint128 x39; 175 uint64_t x40; 176 uint64_t x41; 177 fiat_25519_uint128 x42; 178 uint64_t x43; 179 uint64_t x44; 180 uint64_t x45; 181 uint64_t x46; 182 uint64_t x47; 183 uint64_t x48; 184 uint64_t x49; 185 fiat_25519_uint1 x50; 186 uint64_t x51; 187 uint64_t x52; 188 x1 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[4]) * UINT8_C(0x13))); 189 x2 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[3]) * UINT8_C(0x13))); 190 x3 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[2]) * UINT8_C(0x13))); 191 x4 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[1]) * UINT8_C(0x13))); 192 x5 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[4]) * UINT8_C(0x13))); 193 x6 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[3]) * UINT8_C(0x13))); 194 x7 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * UINT8_C(0x13))); 195 x8 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[4]) * UINT8_C(0x13))); 196 x9 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * UINT8_C(0x13))); 197 x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * UINT8_C(0x13))); 198 x11 = ((fiat_25519_uint128)(arg1[4]) * (arg2[0])); 199 x12 = ((fiat_25519_uint128)(arg1[3]) * (arg2[1])); 200 x13 = ((fiat_25519_uint128)(arg1[3]) * (arg2[0])); 201 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg2[2])); 202 x15 = ((fiat_25519_uint128)(arg1[2]) * (arg2[1])); 203 x16 = ((fiat_25519_uint128)(arg1[2]) * (arg2[0])); 204 x17 = ((fiat_25519_uint128)(arg1[1]) * (arg2[3])); 205 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg2[2])); 206 x19 = ((fiat_25519_uint128)(arg1[1]) * (arg2[1])); 207 x20 = ((fiat_25519_uint128)(arg1[1]) * (arg2[0])); 208 x21 = ((fiat_25519_uint128)(arg1[0]) * (arg2[4])); 209 x22 = ((fiat_25519_uint128)(arg1[0]) * (arg2[3])); 210 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg2[2])); 211 x24 = ((fiat_25519_uint128)(arg1[0]) * (arg2[1])); 212 x25 = ((fiat_25519_uint128)(arg1[0]) * (arg2[0])); 213 x26 = (x25 + (x10 + (x9 + (x7 + x4)))); 214 x27 = (uint64_t)(x26 >> 51); 215 x28 = (uint64_t)(x26 & UINT64_C(0x7ffffffffffff)); 216 x29 = (x21 + (x17 + (x14 + (x12 + x11)))); 217 x30 = (x22 + (x18 + (x15 + (x13 + x1)))); 218 x31 = (x23 + (x19 + (x16 + (x5 + x2)))); 219 x32 = (x24 + (x20 + (x8 + (x6 + x3)))); 220 x33 = (x27 + x32); 221 x34 = (uint64_t)(x33 >> 51); 222 x35 = (uint64_t)(x33 & UINT64_C(0x7ffffffffffff)); 223 x36 = (x34 + x31); 224 x37 = (uint64_t)(x36 >> 51); 225 x38 = (uint64_t)(x36 & UINT64_C(0x7ffffffffffff)); 226 x39 = (x37 + x30); 227 x40 = (uint64_t)(x39 >> 51); 228 x41 = (uint64_t)(x39 & UINT64_C(0x7ffffffffffff)); 229 x42 = (x40 + x29); 230 x43 = (uint64_t)(x42 >> 51); 231 x44 = (uint64_t)(x42 & UINT64_C(0x7ffffffffffff)); 232 x45 = (x43 * UINT8_C(0x13)); 233 x46 = (x28 + x45); 234 x47 = (x46 >> 51); 235 x48 = (x46 & UINT64_C(0x7ffffffffffff)); 236 x49 = (x47 + x35); 237 x50 = (fiat_25519_uint1)(x49 >> 51); 238 x51 = (x49 & UINT64_C(0x7ffffffffffff)); 239 x52 = (x50 + x38); 240 out1[0] = x48; 241 out1[1] = x51; 242 out1[2] = x52; 243 out1[3] = x41; 244 out1[4] = x44; 245 } 246 247 /* 248 * The function fiat_25519_carry_square squares a field element and reduces the result. 249 * 250 * Postconditions: 251 * eval out1 mod m = (eval arg1 * eval arg1) mod m 252 * 253 */ 254 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_square(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) { 255 uint64_t x1; 256 uint64_t x2; 257 uint64_t x3; 258 uint64_t x4; 259 uint64_t x5; 260 uint64_t x6; 261 uint64_t x7; 262 uint64_t x8; 263 fiat_25519_uint128 x9; 264 fiat_25519_uint128 x10; 265 fiat_25519_uint128 x11; 266 fiat_25519_uint128 x12; 267 fiat_25519_uint128 x13; 268 fiat_25519_uint128 x14; 269 fiat_25519_uint128 x15; 270 fiat_25519_uint128 x16; 271 fiat_25519_uint128 x17; 272 fiat_25519_uint128 x18; 273 fiat_25519_uint128 x19; 274 fiat_25519_uint128 x20; 275 fiat_25519_uint128 x21; 276 fiat_25519_uint128 x22; 277 fiat_25519_uint128 x23; 278 fiat_25519_uint128 x24; 279 uint64_t x25; 280 uint64_t x26; 281 fiat_25519_uint128 x27; 282 fiat_25519_uint128 x28; 283 fiat_25519_uint128 x29; 284 fiat_25519_uint128 x30; 285 fiat_25519_uint128 x31; 286 uint64_t x32; 287 uint64_t x33; 288 fiat_25519_uint128 x34; 289 uint64_t x35; 290 uint64_t x36; 291 fiat_25519_uint128 x37; 292 uint64_t x38; 293 uint64_t x39; 294 fiat_25519_uint128 x40; 295 uint64_t x41; 296 uint64_t x42; 297 uint64_t x43; 298 uint64_t x44; 299 uint64_t x45; 300 uint64_t x46; 301 uint64_t x47; 302 fiat_25519_uint1 x48; 303 uint64_t x49; 304 uint64_t x50; 305 x1 = ((arg1[4]) * UINT8_C(0x13)); 306 x2 = (x1 * 0x2); 307 x3 = ((arg1[4]) * 0x2); 308 x4 = ((arg1[3]) * UINT8_C(0x13)); 309 x5 = (x4 * 0x2); 310 x6 = ((arg1[3]) * 0x2); 311 x7 = ((arg1[2]) * 0x2); 312 x8 = ((arg1[1]) * 0x2); 313 x9 = ((fiat_25519_uint128)(arg1[4]) * x1); 314 x10 = ((fiat_25519_uint128)(arg1[3]) * x2); 315 x11 = ((fiat_25519_uint128)(arg1[3]) * x4); 316 x12 = ((fiat_25519_uint128)(arg1[2]) * x2); 317 x13 = ((fiat_25519_uint128)(arg1[2]) * x5); 318 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg1[2])); 319 x15 = ((fiat_25519_uint128)(arg1[1]) * x2); 320 x16 = ((fiat_25519_uint128)(arg1[1]) * x6); 321 x17 = ((fiat_25519_uint128)(arg1[1]) * x7); 322 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg1[1])); 323 x19 = ((fiat_25519_uint128)(arg1[0]) * x3); 324 x20 = ((fiat_25519_uint128)(arg1[0]) * x6); 325 x21 = ((fiat_25519_uint128)(arg1[0]) * x7); 326 x22 = ((fiat_25519_uint128)(arg1[0]) * x8); 327 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg1[0])); 328 x24 = (x23 + (x15 + x13)); 329 x25 = (uint64_t)(x24 >> 51); 330 x26 = (uint64_t)(x24 & UINT64_C(0x7ffffffffffff)); 331 x27 = (x19 + (x16 + x14)); 332 x28 = (x20 + (x17 + x9)); 333 x29 = (x21 + (x18 + x10)); 334 x30 = (x22 + (x12 + x11)); 335 x31 = (x25 + x30); 336 x32 = (uint64_t)(x31 >> 51); 337 x33 = (uint64_t)(x31 & UINT64_C(0x7ffffffffffff)); 338 x34 = (x32 + x29); 339 x35 = (uint64_t)(x34 >> 51); 340 x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff)); 341 x37 = (x35 + x28); 342 x38 = (uint64_t)(x37 >> 51); 343 x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff)); 344 x40 = (x38 + x27); 345 x41 = (uint64_t)(x40 >> 51); 346 x42 = (uint64_t)(x40 & UINT64_C(0x7ffffffffffff)); 347 x43 = (x41 * UINT8_C(0x13)); 348 x44 = (x26 + x43); 349 x45 = (x44 >> 51); 350 x46 = (x44 & UINT64_C(0x7ffffffffffff)); 351 x47 = (x45 + x33); 352 x48 = (fiat_25519_uint1)(x47 >> 51); 353 x49 = (x47 & UINT64_C(0x7ffffffffffff)); 354 x50 = (x48 + x36); 355 out1[0] = x46; 356 out1[1] = x49; 357 out1[2] = x50; 358 out1[3] = x39; 359 out1[4] = x42; 360 } 361 362 /* 363 * The function fiat_25519_carry reduces a field element. 364 * 365 * Postconditions: 366 * eval out1 mod m = eval arg1 mod m 367 * 368 */ 369 static FIAT_25519_FIAT_INLINE void fiat_25519_carry(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) { 370 uint64_t x1; 371 uint64_t x2; 372 uint64_t x3; 373 uint64_t x4; 374 uint64_t x5; 375 uint64_t x6; 376 uint64_t x7; 377 uint64_t x8; 378 uint64_t x9; 379 uint64_t x10; 380 uint64_t x11; 381 uint64_t x12; 382 x1 = (arg1[0]); 383 x2 = ((x1 >> 51) + (arg1[1])); 384 x3 = ((x2 >> 51) + (arg1[2])); 385 x4 = ((x3 >> 51) + (arg1[3])); 386 x5 = ((x4 >> 51) + (arg1[4])); 387 x6 = ((x1 & UINT64_C(0x7ffffffffffff)) + ((x5 >> 51) * UINT8_C(0x13))); 388 x7 = ((fiat_25519_uint1)(x6 >> 51) + (x2 & UINT64_C(0x7ffffffffffff))); 389 x8 = (x6 & UINT64_C(0x7ffffffffffff)); 390 x9 = (x7 & UINT64_C(0x7ffffffffffff)); 391 x10 = ((fiat_25519_uint1)(x7 >> 51) + (x3 & UINT64_C(0x7ffffffffffff))); 392 x11 = (x4 & UINT64_C(0x7ffffffffffff)); 393 x12 = (x5 & UINT64_C(0x7ffffffffffff)); 394 out1[0] = x8; 395 out1[1] = x9; 396 out1[2] = x10; 397 out1[3] = x11; 398 out1[4] = x12; 399 } 400 401 /* 402 * The function fiat_25519_add adds two field elements. 403 * 404 * Postconditions: 405 * eval out1 mod m = (eval arg1 + eval arg2) mod m 406 * 407 */ 408 static FIAT_25519_FIAT_INLINE void fiat_25519_add(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) { 409 uint64_t x1; 410 uint64_t x2; 411 uint64_t x3; 412 uint64_t x4; 413 uint64_t x5; 414 x1 = ((arg1[0]) + (arg2[0])); 415 x2 = ((arg1[1]) + (arg2[1])); 416 x3 = ((arg1[2]) + (arg2[2])); 417 x4 = ((arg1[3]) + (arg2[3])); 418 x5 = ((arg1[4]) + (arg2[4])); 419 out1[0] = x1; 420 out1[1] = x2; 421 out1[2] = x3; 422 out1[3] = x4; 423 out1[4] = x5; 424 } 425 426 /* 427 * The function fiat_25519_sub subtracts two field elements. 428 * 429 * Postconditions: 430 * eval out1 mod m = (eval arg1 - eval arg2) mod m 431 * 432 */ 433 static FIAT_25519_FIAT_INLINE void fiat_25519_sub(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) { 434 uint64_t x1; 435 uint64_t x2; 436 uint64_t x3; 437 uint64_t x4; 438 uint64_t x5; 439 x1 = ((UINT64_C(0xfffffffffffda) + (arg1[0])) - (arg2[0])); 440 x2 = ((UINT64_C(0xffffffffffffe) + (arg1[1])) - (arg2[1])); 441 x3 = ((UINT64_C(0xffffffffffffe) + (arg1[2])) - (arg2[2])); 442 x4 = ((UINT64_C(0xffffffffffffe) + (arg1[3])) - (arg2[3])); 443 x5 = ((UINT64_C(0xffffffffffffe) + (arg1[4])) - (arg2[4])); 444 out1[0] = x1; 445 out1[1] = x2; 446 out1[2] = x3; 447 out1[3] = x4; 448 out1[4] = x5; 449 } 450 451 /* 452 * The function fiat_25519_opp negates a field element. 453 * 454 * Postconditions: 455 * eval out1 mod m = -eval arg1 mod m 456 * 457 */ 458 static FIAT_25519_FIAT_INLINE void fiat_25519_opp(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) { 459 uint64_t x1; 460 uint64_t x2; 461 uint64_t x3; 462 uint64_t x4; 463 uint64_t x5; 464 x1 = (UINT64_C(0xfffffffffffda) - (arg1[0])); 465 x2 = (UINT64_C(0xffffffffffffe) - (arg1[1])); 466 x3 = (UINT64_C(0xffffffffffffe) - (arg1[2])); 467 x4 = (UINT64_C(0xffffffffffffe) - (arg1[3])); 468 x5 = (UINT64_C(0xffffffffffffe) - (arg1[4])); 469 out1[0] = x1; 470 out1[1] = x2; 471 out1[2] = x3; 472 out1[3] = x4; 473 out1[4] = x5; 474 } 475 476 /* 477 * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order. 478 * 479 * Postconditions: 480 * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] 481 * 482 * Output Bounds: 483 * 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]] 484 */ 485 static FIAT_25519_FIAT_INLINE void fiat_25519_to_bytes(uint8_t out1[32], const fiat_25519_tight_field_element arg1) { 486 uint64_t x1; 487 fiat_25519_uint1 x2; 488 uint64_t x3; 489 fiat_25519_uint1 x4; 490 uint64_t x5; 491 fiat_25519_uint1 x6; 492 uint64_t x7; 493 fiat_25519_uint1 x8; 494 uint64_t x9; 495 fiat_25519_uint1 x10; 496 uint64_t x11; 497 uint64_t x12; 498 fiat_25519_uint1 x13; 499 uint64_t x14; 500 fiat_25519_uint1 x15; 501 uint64_t x16; 502 fiat_25519_uint1 x17; 503 uint64_t x18; 504 fiat_25519_uint1 x19; 505 uint64_t x20; 506 fiat_25519_uint1 x21; 507 uint64_t x22; 508 uint64_t x23; 509 uint64_t x24; 510 uint64_t x25; 511 uint8_t x26; 512 uint64_t x27; 513 uint8_t x28; 514 uint64_t x29; 515 uint8_t x30; 516 uint64_t x31; 517 uint8_t x32; 518 uint64_t x33; 519 uint8_t x34; 520 uint64_t x35; 521 uint8_t x36; 522 uint8_t x37; 523 uint64_t x38; 524 uint8_t x39; 525 uint64_t x40; 526 uint8_t x41; 527 uint64_t x42; 528 uint8_t x43; 529 uint64_t x44; 530 uint8_t x45; 531 uint64_t x46; 532 uint8_t x47; 533 uint64_t x48; 534 uint8_t x49; 535 uint8_t x50; 536 uint64_t x51; 537 uint8_t x52; 538 uint64_t x53; 539 uint8_t x54; 540 uint64_t x55; 541 uint8_t x56; 542 uint64_t x57; 543 uint8_t x58; 544 uint64_t x59; 545 uint8_t x60; 546 uint64_t x61; 547 uint8_t x62; 548 uint64_t x63; 549 uint8_t x64; 550 fiat_25519_uint1 x65; 551 uint64_t x66; 552 uint8_t x67; 553 uint64_t x68; 554 uint8_t x69; 555 uint64_t x70; 556 uint8_t x71; 557 uint64_t x72; 558 uint8_t x73; 559 uint64_t x74; 560 uint8_t x75; 561 uint64_t x76; 562 uint8_t x77; 563 uint8_t x78; 564 uint64_t x79; 565 uint8_t x80; 566 uint64_t x81; 567 uint8_t x82; 568 uint64_t x83; 569 uint8_t x84; 570 uint64_t x85; 571 uint8_t x86; 572 uint64_t x87; 573 uint8_t x88; 574 uint64_t x89; 575 uint8_t x90; 576 uint8_t x91; 577 fiat_25519_subborrowx_u51(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0x7ffffffffffed)); 578 fiat_25519_subborrowx_u51(&x3, &x4, x2, (arg1[1]), UINT64_C(0x7ffffffffffff)); 579 fiat_25519_subborrowx_u51(&x5, &x6, x4, (arg1[2]), UINT64_C(0x7ffffffffffff)); 580 fiat_25519_subborrowx_u51(&x7, &x8, x6, (arg1[3]), UINT64_C(0x7ffffffffffff)); 581 fiat_25519_subborrowx_u51(&x9, &x10, x8, (arg1[4]), UINT64_C(0x7ffffffffffff)); 582 fiat_25519_cmovznz_u64(&x11, x10, 0x0, UINT64_C(0xffffffffffffffff)); 583 fiat_25519_addcarryx_u51(&x12, &x13, 0x0, x1, (x11 & UINT64_C(0x7ffffffffffed))); 584 fiat_25519_addcarryx_u51(&x14, &x15, x13, x3, (x11 & UINT64_C(0x7ffffffffffff))); 585 fiat_25519_addcarryx_u51(&x16, &x17, x15, x5, (x11 & UINT64_C(0x7ffffffffffff))); 586 fiat_25519_addcarryx_u51(&x18, &x19, x17, x7, (x11 & UINT64_C(0x7ffffffffffff))); 587 fiat_25519_addcarryx_u51(&x20, &x21, x19, x9, (x11 & UINT64_C(0x7ffffffffffff))); 588 x22 = (x20 << 4); 589 x23 = (x18 * (uint64_t)0x2); 590 x24 = (x16 << 6); 591 x25 = (x14 << 3); 592 x26 = (uint8_t)(x12 & UINT8_C(0xff)); 593 x27 = (x12 >> 8); 594 x28 = (uint8_t)(x27 & UINT8_C(0xff)); 595 x29 = (x27 >> 8); 596 x30 = (uint8_t)(x29 & UINT8_C(0xff)); 597 x31 = (x29 >> 8); 598 x32 = (uint8_t)(x31 & UINT8_C(0xff)); 599 x33 = (x31 >> 8); 600 x34 = (uint8_t)(x33 & UINT8_C(0xff)); 601 x35 = (x33 >> 8); 602 x36 = (uint8_t)(x35 & UINT8_C(0xff)); 603 x37 = (uint8_t)(x35 >> 8); 604 x38 = (x25 + (uint64_t)x37); 605 x39 = (uint8_t)(x38 & UINT8_C(0xff)); 606 x40 = (x38 >> 8); 607 x41 = (uint8_t)(x40 & UINT8_C(0xff)); 608 x42 = (x40 >> 8); 609 x43 = (uint8_t)(x42 & UINT8_C(0xff)); 610 x44 = (x42 >> 8); 611 x45 = (uint8_t)(x44 & UINT8_C(0xff)); 612 x46 = (x44 >> 8); 613 x47 = (uint8_t)(x46 & UINT8_C(0xff)); 614 x48 = (x46 >> 8); 615 x49 = (uint8_t)(x48 & UINT8_C(0xff)); 616 x50 = (uint8_t)(x48 >> 8); 617 x51 = (x24 + (uint64_t)x50); 618 x52 = (uint8_t)(x51 & UINT8_C(0xff)); 619 x53 = (x51 >> 8); 620 x54 = (uint8_t)(x53 & UINT8_C(0xff)); 621 x55 = (x53 >> 8); 622 x56 = (uint8_t)(x55 & UINT8_C(0xff)); 623 x57 = (x55 >> 8); 624 x58 = (uint8_t)(x57 & UINT8_C(0xff)); 625 x59 = (x57 >> 8); 626 x60 = (uint8_t)(x59 & UINT8_C(0xff)); 627 x61 = (x59 >> 8); 628 x62 = (uint8_t)(x61 & UINT8_C(0xff)); 629 x63 = (x61 >> 8); 630 x64 = (uint8_t)(x63 & UINT8_C(0xff)); 631 x65 = (fiat_25519_uint1)(x63 >> 8); 632 x66 = (x23 + (uint64_t)x65); 633 x67 = (uint8_t)(x66 & UINT8_C(0xff)); 634 x68 = (x66 >> 8); 635 x69 = (uint8_t)(x68 & UINT8_C(0xff)); 636 x70 = (x68 >> 8); 637 x71 = (uint8_t)(x70 & UINT8_C(0xff)); 638 x72 = (x70 >> 8); 639 x73 = (uint8_t)(x72 & UINT8_C(0xff)); 640 x74 = (x72 >> 8); 641 x75 = (uint8_t)(x74 & UINT8_C(0xff)); 642 x76 = (x74 >> 8); 643 x77 = (uint8_t)(x76 & UINT8_C(0xff)); 644 x78 = (uint8_t)(x76 >> 8); 645 x79 = (x22 + (uint64_t)x78); 646 x80 = (uint8_t)(x79 & UINT8_C(0xff)); 647 x81 = (x79 >> 8); 648 x82 = (uint8_t)(x81 & UINT8_C(0xff)); 649 x83 = (x81 >> 8); 650 x84 = (uint8_t)(x83 & UINT8_C(0xff)); 651 x85 = (x83 >> 8); 652 x86 = (uint8_t)(x85 & UINT8_C(0xff)); 653 x87 = (x85 >> 8); 654 x88 = (uint8_t)(x87 & UINT8_C(0xff)); 655 x89 = (x87 >> 8); 656 x90 = (uint8_t)(x89 & UINT8_C(0xff)); 657 x91 = (uint8_t)(x89 >> 8); 658 out1[0] = x26; 659 out1[1] = x28; 660 out1[2] = x30; 661 out1[3] = x32; 662 out1[4] = x34; 663 out1[5] = x36; 664 out1[6] = x39; 665 out1[7] = x41; 666 out1[8] = x43; 667 out1[9] = x45; 668 out1[10] = x47; 669 out1[11] = x49; 670 out1[12] = x52; 671 out1[13] = x54; 672 out1[14] = x56; 673 out1[15] = x58; 674 out1[16] = x60; 675 out1[17] = x62; 676 out1[18] = x64; 677 out1[19] = x67; 678 out1[20] = x69; 679 out1[21] = x71; 680 out1[22] = x73; 681 out1[23] = x75; 682 out1[24] = x77; 683 out1[25] = x80; 684 out1[26] = x82; 685 out1[27] = x84; 686 out1[28] = x86; 687 out1[29] = x88; 688 out1[30] = x90; 689 out1[31] = x91; 690 } 691 692 /* 693 * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order. 694 * 695 * Postconditions: 696 * eval out1 mod m = bytes_eval arg1 mod m 697 * 698 * Input Bounds: 699 * 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]] 700 */ 701 static FIAT_25519_FIAT_INLINE void fiat_25519_from_bytes(fiat_25519_tight_field_element out1, const uint8_t arg1[32]) { 702 uint64_t x1; 703 uint64_t x2; 704 uint64_t x3; 705 uint64_t x4; 706 uint64_t x5; 707 uint64_t x6; 708 uint64_t x7; 709 uint64_t x8; 710 uint64_t x9; 711 uint64_t x10; 712 uint64_t x11; 713 uint64_t x12; 714 uint64_t x13; 715 uint64_t x14; 716 uint64_t x15; 717 uint64_t x16; 718 uint64_t x17; 719 uint64_t x18; 720 uint64_t x19; 721 uint64_t x20; 722 uint64_t x21; 723 uint64_t x22; 724 uint64_t x23; 725 uint64_t x24; 726 uint64_t x25; 727 uint64_t x26; 728 uint64_t x27; 729 uint64_t x28; 730 uint64_t x29; 731 uint64_t x30; 732 uint64_t x31; 733 uint8_t x32; 734 uint64_t x33; 735 uint64_t x34; 736 uint64_t x35; 737 uint64_t x36; 738 uint64_t x37; 739 uint64_t x38; 740 uint64_t x39; 741 uint8_t x40; 742 uint64_t x41; 743 uint64_t x42; 744 uint64_t x43; 745 uint64_t x44; 746 uint64_t x45; 747 uint64_t x46; 748 uint64_t x47; 749 uint8_t x48; 750 uint64_t x49; 751 uint64_t x50; 752 uint64_t x51; 753 uint64_t x52; 754 uint64_t x53; 755 uint64_t x54; 756 uint64_t x55; 757 uint64_t x56; 758 uint8_t x57; 759 uint64_t x58; 760 uint64_t x59; 761 uint64_t x60; 762 uint64_t x61; 763 uint64_t x62; 764 uint64_t x63; 765 uint64_t x64; 766 uint8_t x65; 767 uint64_t x66; 768 uint64_t x67; 769 uint64_t x68; 770 uint64_t x69; 771 uint64_t x70; 772 uint64_t x71; 773 x1 = ((uint64_t)(arg1[31]) << 44); 774 x2 = ((uint64_t)(arg1[30]) << 36); 775 x3 = ((uint64_t)(arg1[29]) << 28); 776 x4 = ((uint64_t)(arg1[28]) << 20); 777 x5 = ((uint64_t)(arg1[27]) << 12); 778 x6 = ((uint64_t)(arg1[26]) << 4); 779 x7 = ((uint64_t)(arg1[25]) << 47); 780 x8 = ((uint64_t)(arg1[24]) << 39); 781 x9 = ((uint64_t)(arg1[23]) << 31); 782 x10 = ((uint64_t)(arg1[22]) << 23); 783 x11 = ((uint64_t)(arg1[21]) << 15); 784 x12 = ((uint64_t)(arg1[20]) << 7); 785 x13 = ((uint64_t)(arg1[19]) << 50); 786 x14 = ((uint64_t)(arg1[18]) << 42); 787 x15 = ((uint64_t)(arg1[17]) << 34); 788 x16 = ((uint64_t)(arg1[16]) << 26); 789 x17 = ((uint64_t)(arg1[15]) << 18); 790 x18 = ((uint64_t)(arg1[14]) << 10); 791 x19 = ((uint64_t)(arg1[13]) << 2); 792 x20 = ((uint64_t)(arg1[12]) << 45); 793 x21 = ((uint64_t)(arg1[11]) << 37); 794 x22 = ((uint64_t)(arg1[10]) << 29); 795 x23 = ((uint64_t)(arg1[9]) << 21); 796 x24 = ((uint64_t)(arg1[8]) << 13); 797 x25 = ((uint64_t)(arg1[7]) << 5); 798 x26 = ((uint64_t)(arg1[6]) << 48); 799 x27 = ((uint64_t)(arg1[5]) << 40); 800 x28 = ((uint64_t)(arg1[4]) << 32); 801 x29 = ((uint64_t)(arg1[3]) << 24); 802 x30 = ((uint64_t)(arg1[2]) << 16); 803 x31 = ((uint64_t)(arg1[1]) << 8); 804 x32 = (arg1[0]); 805 x33 = (x31 + (uint64_t)x32); 806 x34 = (x30 + x33); 807 x35 = (x29 + x34); 808 x36 = (x28 + x35); 809 x37 = (x27 + x36); 810 x38 = (x26 + x37); 811 x39 = (x38 & UINT64_C(0x7ffffffffffff)); 812 x40 = (uint8_t)(x38 >> 51); 813 x41 = (x25 + (uint64_t)x40); 814 x42 = (x24 + x41); 815 x43 = (x23 + x42); 816 x44 = (x22 + x43); 817 x45 = (x21 + x44); 818 x46 = (x20 + x45); 819 x47 = (x46 & UINT64_C(0x7ffffffffffff)); 820 x48 = (uint8_t)(x46 >> 51); 821 x49 = (x19 + (uint64_t)x48); 822 x50 = (x18 + x49); 823 x51 = (x17 + x50); 824 x52 = (x16 + x51); 825 x53 = (x15 + x52); 826 x54 = (x14 + x53); 827 x55 = (x13 + x54); 828 x56 = (x55 & UINT64_C(0x7ffffffffffff)); 829 x57 = (uint8_t)(x55 >> 51); 830 x58 = (x12 + (uint64_t)x57); 831 x59 = (x11 + x58); 832 x60 = (x10 + x59); 833 x61 = (x9 + x60); 834 x62 = (x8 + x61); 835 x63 = (x7 + x62); 836 x64 = (x63 & UINT64_C(0x7ffffffffffff)); 837 x65 = (uint8_t)(x63 >> 51); 838 x66 = (x6 + (uint64_t)x65); 839 x67 = (x5 + x66); 840 x68 = (x4 + x67); 841 x69 = (x3 + x68); 842 x70 = (x2 + x69); 843 x71 = (x1 + x70); 844 out1[0] = x39; 845 out1[1] = x47; 846 out1[2] = x56; 847 out1[3] = x64; 848 out1[4] = x71; 849 } 850 851 #else /* defined(BORINGSSL_CURVE25519_64BIT) */ 852 853 /* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier 25519 32 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666 */ 854 /* curve description: 25519 */ 855 /* machine_wordsize = 32 (from "32") */ 856 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666 */ 857 /* n = 10 (from "(auto)") */ 858 /* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */ 859 /* tight_bounds_multiplier = 1 (from "") */ 860 /* */ 861 /* Computed values: */ 862 /* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1] */ 863 /* eval z = z[0] + (z[1] << 26) + (z[2] << 51) + (z[3] << 77) + (z[4] << 102) + (z[5] << 128) + (z[6] << 153) + (z[7] << 179) + (z[8] << 204) + (z[9] << 230) */ 864 /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */ 865 /* balance = [0x7ffffda, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe] */ 866 867 #include <stdint.h> 868 typedef unsigned char fiat_25519_uint1; 869 typedef signed char fiat_25519_int1; 870 #if defined(__GNUC__) || defined(__clang__) 871 # define FIAT_25519_FIAT_INLINE __inline__ 872 #else 873 # define FIAT_25519_FIAT_INLINE 874 #endif 875 876 /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ 877 /* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */ 878 typedef uint32_t fiat_25519_loose_field_element[10]; 879 880 /* The type fiat_25519_tight_field_element is a field element with tight bounds. */ 881 /* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */ 882 typedef uint32_t fiat_25519_tight_field_element[10]; 883 884 #if (-1 & 3) != 3 885 #error "This code only works on a two's complement system" 886 #endif 887 888 #if !defined(FIAT_25519_NO_ASM) && (defined(__GNUC__) || defined(__clang__)) 889 static __inline__ uint32_t fiat_25519_value_barrier_u32(uint32_t a) { 890 __asm__("" : "+r"(a) : /* no inputs */); 891 return a; 892 } 893 #else 894 # define fiat_25519_value_barrier_u32(x) (x) 895 #endif 896 897 898 /* 899 * The function fiat_25519_addcarryx_u26 is an addition with carry. 900 * 901 * Postconditions: 902 * out1 = (arg1 + arg2 + arg3) mod 2^26 903 * out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋ 904 * 905 * Input Bounds: 906 * arg1: [0x0 ~> 0x1] 907 * arg2: [0x0 ~> 0x3ffffff] 908 * arg3: [0x0 ~> 0x3ffffff] 909 * Output Bounds: 910 * out1: [0x0 ~> 0x3ffffff] 911 * out2: [0x0 ~> 0x1] 912 */ 913 static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 914 uint32_t x1; 915 uint32_t x2; 916 fiat_25519_uint1 x3; 917 x1 = ((arg1 + arg2) + arg3); 918 x2 = (x1 & UINT32_C(0x3ffffff)); 919 x3 = (fiat_25519_uint1)(x1 >> 26); 920 *out1 = x2; 921 *out2 = x3; 922 } 923 924 /* 925 * The function fiat_25519_subborrowx_u26 is a subtraction with borrow. 926 * 927 * Postconditions: 928 * out1 = (-arg1 + arg2 + -arg3) mod 2^26 929 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋ 930 * 931 * Input Bounds: 932 * arg1: [0x0 ~> 0x1] 933 * arg2: [0x0 ~> 0x3ffffff] 934 * arg3: [0x0 ~> 0x3ffffff] 935 * Output Bounds: 936 * out1: [0x0 ~> 0x3ffffff] 937 * out2: [0x0 ~> 0x1] 938 */ 939 static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 940 int32_t x1; 941 fiat_25519_int1 x2; 942 uint32_t x3; 943 x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3); 944 x2 = (fiat_25519_int1)(x1 >> 26); 945 x3 = (x1 & UINT32_C(0x3ffffff)); 946 *out1 = x3; 947 *out2 = (fiat_25519_uint1)(0x0 - x2); 948 } 949 950 /* 951 * The function fiat_25519_addcarryx_u25 is an addition with carry. 952 * 953 * Postconditions: 954 * out1 = (arg1 + arg2 + arg3) mod 2^25 955 * out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋ 956 * 957 * Input Bounds: 958 * arg1: [0x0 ~> 0x1] 959 * arg2: [0x0 ~> 0x1ffffff] 960 * arg3: [0x0 ~> 0x1ffffff] 961 * Output Bounds: 962 * out1: [0x0 ~> 0x1ffffff] 963 * out2: [0x0 ~> 0x1] 964 */ 965 static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 966 uint32_t x1; 967 uint32_t x2; 968 fiat_25519_uint1 x3; 969 x1 = ((arg1 + arg2) + arg3); 970 x2 = (x1 & UINT32_C(0x1ffffff)); 971 x3 = (fiat_25519_uint1)(x1 >> 25); 972 *out1 = x2; 973 *out2 = x3; 974 } 975 976 /* 977 * The function fiat_25519_subborrowx_u25 is a subtraction with borrow. 978 * 979 * Postconditions: 980 * out1 = (-arg1 + arg2 + -arg3) mod 2^25 981 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋ 982 * 983 * Input Bounds: 984 * arg1: [0x0 ~> 0x1] 985 * arg2: [0x0 ~> 0x1ffffff] 986 * arg3: [0x0 ~> 0x1ffffff] 987 * Output Bounds: 988 * out1: [0x0 ~> 0x1ffffff] 989 * out2: [0x0 ~> 0x1] 990 */ 991 static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 992 int32_t x1; 993 fiat_25519_int1 x2; 994 uint32_t x3; 995 x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3); 996 x2 = (fiat_25519_int1)(x1 >> 25); 997 x3 = (x1 & UINT32_C(0x1ffffff)); 998 *out1 = x3; 999 *out2 = (fiat_25519_uint1)(0x0 - x2); 1000 } 1001 1002 /* 1003 * The function fiat_25519_cmovznz_u32 is a single-word conditional move. 1004 * 1005 * Postconditions: 1006 * out1 = (if arg1 = 0 then arg2 else arg3) 1007 * 1008 * Input Bounds: 1009 * arg1: [0x0 ~> 0x1] 1010 * arg2: [0x0 ~> 0xffffffff] 1011 * arg3: [0x0 ~> 0xffffffff] 1012 * Output Bounds: 1013 * out1: [0x0 ~> 0xffffffff] 1014 */ 1015 static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 1016 fiat_25519_uint1 x1; 1017 uint32_t x2; 1018 uint32_t x3; 1019 x1 = (!(!arg1)); 1020 x2 = ((fiat_25519_int1)(0x0 - x1) & UINT32_C(0xffffffff)); 1021 x3 = ((fiat_25519_value_barrier_u32(x2) & arg3) | (fiat_25519_value_barrier_u32((~x2)) & arg2)); 1022 *out1 = x3; 1023 } 1024 1025 /* 1026 * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. 1027 * 1028 * Postconditions: 1029 * eval out1 mod m = (eval arg1 * eval arg2) mod m 1030 * 1031 */ 1032 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_mul(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1, const fiat_25519_loose_field_element arg2) { 1033 uint64_t x1; 1034 uint64_t x2; 1035 uint64_t x3; 1036 uint64_t x4; 1037 uint64_t x5; 1038 uint64_t x6; 1039 uint64_t x7; 1040 uint64_t x8; 1041 uint64_t x9; 1042 uint64_t x10; 1043 uint64_t x11; 1044 uint64_t x12; 1045 uint64_t x13; 1046 uint64_t x14; 1047 uint64_t x15; 1048 uint64_t x16; 1049 uint64_t x17; 1050 uint64_t x18; 1051 uint64_t x19; 1052 uint64_t x20; 1053 uint64_t x21; 1054 uint64_t x22; 1055 uint64_t x23; 1056 uint64_t x24; 1057 uint64_t x25; 1058 uint64_t x26; 1059 uint64_t x27; 1060 uint64_t x28; 1061 uint64_t x29; 1062 uint64_t x30; 1063 uint64_t x31; 1064 uint64_t x32; 1065 uint64_t x33; 1066 uint64_t x34; 1067 uint64_t x35; 1068 uint64_t x36; 1069 uint64_t x37; 1070 uint64_t x38; 1071 uint64_t x39; 1072 uint64_t x40; 1073 uint64_t x41; 1074 uint64_t x42; 1075 uint64_t x43; 1076 uint64_t x44; 1077 uint64_t x45; 1078 uint64_t x46; 1079 uint64_t x47; 1080 uint64_t x48; 1081 uint64_t x49; 1082 uint64_t x50; 1083 uint64_t x51; 1084 uint64_t x52; 1085 uint64_t x53; 1086 uint64_t x54; 1087 uint64_t x55; 1088 uint64_t x56; 1089 uint64_t x57; 1090 uint64_t x58; 1091 uint64_t x59; 1092 uint64_t x60; 1093 uint64_t x61; 1094 uint64_t x62; 1095 uint64_t x63; 1096 uint64_t x64; 1097 uint64_t x65; 1098 uint64_t x66; 1099 uint64_t x67; 1100 uint64_t x68; 1101 uint64_t x69; 1102 uint64_t x70; 1103 uint64_t x71; 1104 uint64_t x72; 1105 uint64_t x73; 1106 uint64_t x74; 1107 uint64_t x75; 1108 uint64_t x76; 1109 uint64_t x77; 1110 uint64_t x78; 1111 uint64_t x79; 1112 uint64_t x80; 1113 uint64_t x81; 1114 uint64_t x82; 1115 uint64_t x83; 1116 uint64_t x84; 1117 uint64_t x85; 1118 uint64_t x86; 1119 uint64_t x87; 1120 uint64_t x88; 1121 uint64_t x89; 1122 uint64_t x90; 1123 uint64_t x91; 1124 uint64_t x92; 1125 uint64_t x93; 1126 uint64_t x94; 1127 uint64_t x95; 1128 uint64_t x96; 1129 uint64_t x97; 1130 uint64_t x98; 1131 uint64_t x99; 1132 uint64_t x100; 1133 uint64_t x101; 1134 uint64_t x102; 1135 uint32_t x103; 1136 uint64_t x104; 1137 uint64_t x105; 1138 uint64_t x106; 1139 uint64_t x107; 1140 uint64_t x108; 1141 uint64_t x109; 1142 uint64_t x110; 1143 uint64_t x111; 1144 uint64_t x112; 1145 uint64_t x113; 1146 uint64_t x114; 1147 uint32_t x115; 1148 uint64_t x116; 1149 uint64_t x117; 1150 uint32_t x118; 1151 uint64_t x119; 1152 uint64_t x120; 1153 uint32_t x121; 1154 uint64_t x122; 1155 uint64_t x123; 1156 uint32_t x124; 1157 uint64_t x125; 1158 uint64_t x126; 1159 uint32_t x127; 1160 uint64_t x128; 1161 uint64_t x129; 1162 uint32_t x130; 1163 uint64_t x131; 1164 uint64_t x132; 1165 uint32_t x133; 1166 uint64_t x134; 1167 uint64_t x135; 1168 uint32_t x136; 1169 uint64_t x137; 1170 uint64_t x138; 1171 uint32_t x139; 1172 uint64_t x140; 1173 uint64_t x141; 1174 uint32_t x142; 1175 uint32_t x143; 1176 uint32_t x144; 1177 fiat_25519_uint1 x145; 1178 uint32_t x146; 1179 uint32_t x147; 1180 x1 = ((uint64_t)(arg1[9]) * ((arg2[9]) * UINT8_C(0x26))); 1181 x2 = ((uint64_t)(arg1[9]) * ((arg2[8]) * UINT8_C(0x13))); 1182 x3 = ((uint64_t)(arg1[9]) * ((arg2[7]) * UINT8_C(0x26))); 1183 x4 = ((uint64_t)(arg1[9]) * ((arg2[6]) * UINT8_C(0x13))); 1184 x5 = ((uint64_t)(arg1[9]) * ((arg2[5]) * UINT8_C(0x26))); 1185 x6 = ((uint64_t)(arg1[9]) * ((arg2[4]) * UINT8_C(0x13))); 1186 x7 = ((uint64_t)(arg1[9]) * ((arg2[3]) * UINT8_C(0x26))); 1187 x8 = ((uint64_t)(arg1[9]) * ((arg2[2]) * UINT8_C(0x13))); 1188 x9 = ((uint64_t)(arg1[9]) * ((arg2[1]) * UINT8_C(0x26))); 1189 x10 = ((uint64_t)(arg1[8]) * ((arg2[9]) * UINT8_C(0x13))); 1190 x11 = ((uint64_t)(arg1[8]) * ((arg2[8]) * UINT8_C(0x13))); 1191 x12 = ((uint64_t)(arg1[8]) * ((arg2[7]) * UINT8_C(0x13))); 1192 x13 = ((uint64_t)(arg1[8]) * ((arg2[6]) * UINT8_C(0x13))); 1193 x14 = ((uint64_t)(arg1[8]) * ((arg2[5]) * UINT8_C(0x13))); 1194 x15 = ((uint64_t)(arg1[8]) * ((arg2[4]) * UINT8_C(0x13))); 1195 x16 = ((uint64_t)(arg1[8]) * ((arg2[3]) * UINT8_C(0x13))); 1196 x17 = ((uint64_t)(arg1[8]) * ((arg2[2]) * UINT8_C(0x13))); 1197 x18 = ((uint64_t)(arg1[7]) * ((arg2[9]) * UINT8_C(0x26))); 1198 x19 = ((uint64_t)(arg1[7]) * ((arg2[8]) * UINT8_C(0x13))); 1199 x20 = ((uint64_t)(arg1[7]) * ((arg2[7]) * UINT8_C(0x26))); 1200 x21 = ((uint64_t)(arg1[7]) * ((arg2[6]) * UINT8_C(0x13))); 1201 x22 = ((uint64_t)(arg1[7]) * ((arg2[5]) * UINT8_C(0x26))); 1202 x23 = ((uint64_t)(arg1[7]) * ((arg2[4]) * UINT8_C(0x13))); 1203 x24 = ((uint64_t)(arg1[7]) * ((arg2[3]) * UINT8_C(0x26))); 1204 x25 = ((uint64_t)(arg1[6]) * ((arg2[9]) * UINT8_C(0x13))); 1205 x26 = ((uint64_t)(arg1[6]) * ((arg2[8]) * UINT8_C(0x13))); 1206 x27 = ((uint64_t)(arg1[6]) * ((arg2[7]) * UINT8_C(0x13))); 1207 x28 = ((uint64_t)(arg1[6]) * ((arg2[6]) * UINT8_C(0x13))); 1208 x29 = ((uint64_t)(arg1[6]) * ((arg2[5]) * UINT8_C(0x13))); 1209 x30 = ((uint64_t)(arg1[6]) * ((arg2[4]) * UINT8_C(0x13))); 1210 x31 = ((uint64_t)(arg1[5]) * ((arg2[9]) * UINT8_C(0x26))); 1211 x32 = ((uint64_t)(arg1[5]) * ((arg2[8]) * UINT8_C(0x13))); 1212 x33 = ((uint64_t)(arg1[5]) * ((arg2[7]) * UINT8_C(0x26))); 1213 x34 = ((uint64_t)(arg1[5]) * ((arg2[6]) * UINT8_C(0x13))); 1214 x35 = ((uint64_t)(arg1[5]) * ((arg2[5]) * UINT8_C(0x26))); 1215 x36 = ((uint64_t)(arg1[4]) * ((arg2[9]) * UINT8_C(0x13))); 1216 x37 = ((uint64_t)(arg1[4]) * ((arg2[8]) * UINT8_C(0x13))); 1217 x38 = ((uint64_t)(arg1[4]) * ((arg2[7]) * UINT8_C(0x13))); 1218 x39 = ((uint64_t)(arg1[4]) * ((arg2[6]) * UINT8_C(0x13))); 1219 x40 = ((uint64_t)(arg1[3]) * ((arg2[9]) * UINT8_C(0x26))); 1220 x41 = ((uint64_t)(arg1[3]) * ((arg2[8]) * UINT8_C(0x13))); 1221 x42 = ((uint64_t)(arg1[3]) * ((arg2[7]) * UINT8_C(0x26))); 1222 x43 = ((uint64_t)(arg1[2]) * ((arg2[9]) * UINT8_C(0x13))); 1223 x44 = ((uint64_t)(arg1[2]) * ((arg2[8]) * UINT8_C(0x13))); 1224 x45 = ((uint64_t)(arg1[1]) * ((arg2[9]) * UINT8_C(0x26))); 1225 x46 = ((uint64_t)(arg1[9]) * (arg2[0])); 1226 x47 = ((uint64_t)(arg1[8]) * (arg2[1])); 1227 x48 = ((uint64_t)(arg1[8]) * (arg2[0])); 1228 x49 = ((uint64_t)(arg1[7]) * (arg2[2])); 1229 x50 = ((uint64_t)(arg1[7]) * ((arg2[1]) * 0x2)); 1230 x51 = ((uint64_t)(arg1[7]) * (arg2[0])); 1231 x52 = ((uint64_t)(arg1[6]) * (arg2[3])); 1232 x53 = ((uint64_t)(arg1[6]) * (arg2[2])); 1233 x54 = ((uint64_t)(arg1[6]) * (arg2[1])); 1234 x55 = ((uint64_t)(arg1[6]) * (arg2[0])); 1235 x56 = ((uint64_t)(arg1[5]) * (arg2[4])); 1236 x57 = ((uint64_t)(arg1[5]) * ((arg2[3]) * 0x2)); 1237 x58 = ((uint64_t)(arg1[5]) * (arg2[2])); 1238 x59 = ((uint64_t)(arg1[5]) * ((arg2[1]) * 0x2)); 1239 x60 = ((uint64_t)(arg1[5]) * (arg2[0])); 1240 x61 = ((uint64_t)(arg1[4]) * (arg2[5])); 1241 x62 = ((uint64_t)(arg1[4]) * (arg2[4])); 1242 x63 = ((uint64_t)(arg1[4]) * (arg2[3])); 1243 x64 = ((uint64_t)(arg1[4]) * (arg2[2])); 1244 x65 = ((uint64_t)(arg1[4]) * (arg2[1])); 1245 x66 = ((uint64_t)(arg1[4]) * (arg2[0])); 1246 x67 = ((uint64_t)(arg1[3]) * (arg2[6])); 1247 x68 = ((uint64_t)(arg1[3]) * ((arg2[5]) * 0x2)); 1248 x69 = ((uint64_t)(arg1[3]) * (arg2[4])); 1249 x70 = ((uint64_t)(arg1[3]) * ((arg2[3]) * 0x2)); 1250 x71 = ((uint64_t)(arg1[3]) * (arg2[2])); 1251 x72 = ((uint64_t)(arg1[3]) * ((arg2[1]) * 0x2)); 1252 x73 = ((uint64_t)(arg1[3]) * (arg2[0])); 1253 x74 = ((uint64_t)(arg1[2]) * (arg2[7])); 1254 x75 = ((uint64_t)(arg1[2]) * (arg2[6])); 1255 x76 = ((uint64_t)(arg1[2]) * (arg2[5])); 1256 x77 = ((uint64_t)(arg1[2]) * (arg2[4])); 1257 x78 = ((uint64_t)(arg1[2]) * (arg2[3])); 1258 x79 = ((uint64_t)(arg1[2]) * (arg2[2])); 1259 x80 = ((uint64_t)(arg1[2]) * (arg2[1])); 1260 x81 = ((uint64_t)(arg1[2]) * (arg2[0])); 1261 x82 = ((uint64_t)(arg1[1]) * (arg2[8])); 1262 x83 = ((uint64_t)(arg1[1]) * ((arg2[7]) * 0x2)); 1263 x84 = ((uint64_t)(arg1[1]) * (arg2[6])); 1264 x85 = ((uint64_t)(arg1[1]) * ((arg2[5]) * 0x2)); 1265 x86 = ((uint64_t)(arg1[1]) * (arg2[4])); 1266 x87 = ((uint64_t)(arg1[1]) * ((arg2[3]) * 0x2)); 1267 x88 = ((uint64_t)(arg1[1]) * (arg2[2])); 1268 x89 = ((uint64_t)(arg1[1]) * ((arg2[1]) * 0x2)); 1269 x90 = ((uint64_t)(arg1[1]) * (arg2[0])); 1270 x91 = ((uint64_t)(arg1[0]) * (arg2[9])); 1271 x92 = ((uint64_t)(arg1[0]) * (arg2[8])); 1272 x93 = ((uint64_t)(arg1[0]) * (arg2[7])); 1273 x94 = ((uint64_t)(arg1[0]) * (arg2[6])); 1274 x95 = ((uint64_t)(arg1[0]) * (arg2[5])); 1275 x96 = ((uint64_t)(arg1[0]) * (arg2[4])); 1276 x97 = ((uint64_t)(arg1[0]) * (arg2[3])); 1277 x98 = ((uint64_t)(arg1[0]) * (arg2[2])); 1278 x99 = ((uint64_t)(arg1[0]) * (arg2[1])); 1279 x100 = ((uint64_t)(arg1[0]) * (arg2[0])); 1280 x101 = (x100 + (x45 + (x44 + (x42 + (x39 + (x35 + (x30 + (x24 + (x17 + x9))))))))); 1281 x102 = (x101 >> 26); 1282 x103 = (uint32_t)(x101 & UINT32_C(0x3ffffff)); 1283 x104 = (x91 + (x82 + (x74 + (x67 + (x61 + (x56 + (x52 + (x49 + (x47 + x46))))))))); 1284 x105 = (x92 + (x83 + (x75 + (x68 + (x62 + (x57 + (x53 + (x50 + (x48 + x1))))))))); 1285 x106 = (x93 + (x84 + (x76 + (x69 + (x63 + (x58 + (x54 + (x51 + (x10 + x2))))))))); 1286 x107 = (x94 + (x85 + (x77 + (x70 + (x64 + (x59 + (x55 + (x18 + (x11 + x3))))))))); 1287 x108 = (x95 + (x86 + (x78 + (x71 + (x65 + (x60 + (x25 + (x19 + (x12 + x4))))))))); 1288 x109 = (x96 + (x87 + (x79 + (x72 + (x66 + (x31 + (x26 + (x20 + (x13 + x5))))))))); 1289 x110 = (x97 + (x88 + (x80 + (x73 + (x36 + (x32 + (x27 + (x21 + (x14 + x6))))))))); 1290 x111 = (x98 + (x89 + (x81 + (x40 + (x37 + (x33 + (x28 + (x22 + (x15 + x7))))))))); 1291 x112 = (x99 + (x90 + (x43 + (x41 + (x38 + (x34 + (x29 + (x23 + (x16 + x8))))))))); 1292 x113 = (x102 + x112); 1293 x114 = (x113 >> 25); 1294 x115 = (uint32_t)(x113 & UINT32_C(0x1ffffff)); 1295 x116 = (x114 + x111); 1296 x117 = (x116 >> 26); 1297 x118 = (uint32_t)(x116 & UINT32_C(0x3ffffff)); 1298 x119 = (x117 + x110); 1299 x120 = (x119 >> 25); 1300 x121 = (uint32_t)(x119 & UINT32_C(0x1ffffff)); 1301 x122 = (x120 + x109); 1302 x123 = (x122 >> 26); 1303 x124 = (uint32_t)(x122 & UINT32_C(0x3ffffff)); 1304 x125 = (x123 + x108); 1305 x126 = (x125 >> 25); 1306 x127 = (uint32_t)(x125 & UINT32_C(0x1ffffff)); 1307 x128 = (x126 + x107); 1308 x129 = (x128 >> 26); 1309 x130 = (uint32_t)(x128 & UINT32_C(0x3ffffff)); 1310 x131 = (x129 + x106); 1311 x132 = (x131 >> 25); 1312 x133 = (uint32_t)(x131 & UINT32_C(0x1ffffff)); 1313 x134 = (x132 + x105); 1314 x135 = (x134 >> 26); 1315 x136 = (uint32_t)(x134 & UINT32_C(0x3ffffff)); 1316 x137 = (x135 + x104); 1317 x138 = (x137 >> 25); 1318 x139 = (uint32_t)(x137 & UINT32_C(0x1ffffff)); 1319 x140 = (x138 * UINT8_C(0x13)); 1320 x141 = (x103 + x140); 1321 x142 = (uint32_t)(x141 >> 26); 1322 x143 = (uint32_t)(x141 & UINT32_C(0x3ffffff)); 1323 x144 = (x142 + x115); 1324 x145 = (fiat_25519_uint1)(x144 >> 25); 1325 x146 = (x144 & UINT32_C(0x1ffffff)); 1326 x147 = (x145 + x118); 1327 out1[0] = x143; 1328 out1[1] = x146; 1329 out1[2] = x147; 1330 out1[3] = x121; 1331 out1[4] = x124; 1332 out1[5] = x127; 1333 out1[6] = x130; 1334 out1[7] = x133; 1335 out1[8] = x136; 1336 out1[9] = x139; 1337 } 1338 1339 /* 1340 * The function fiat_25519_carry_square squares a field element and reduces the result. 1341 * 1342 * Postconditions: 1343 * eval out1 mod m = (eval arg1 * eval arg1) mod m 1344 * 1345 */ 1346 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_square(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) { 1347 uint32_t x1; 1348 uint32_t x2; 1349 uint32_t x3; 1350 uint32_t x4; 1351 uint64_t x5; 1352 uint32_t x6; 1353 uint32_t x7; 1354 uint32_t x8; 1355 uint32_t x9; 1356 uint32_t x10; 1357 uint64_t x11; 1358 uint32_t x12; 1359 uint32_t x13; 1360 uint32_t x14; 1361 uint32_t x15; 1362 uint32_t x16; 1363 uint32_t x17; 1364 uint32_t x18; 1365 uint64_t x19; 1366 uint64_t x20; 1367 uint64_t x21; 1368 uint64_t x22; 1369 uint64_t x23; 1370 uint64_t x24; 1371 uint64_t x25; 1372 uint64_t x26; 1373 uint64_t x27; 1374 uint64_t x28; 1375 uint64_t x29; 1376 uint64_t x30; 1377 uint64_t x31; 1378 uint64_t x32; 1379 uint64_t x33; 1380 uint64_t x34; 1381 uint64_t x35; 1382 uint64_t x36; 1383 uint64_t x37; 1384 uint64_t x38; 1385 uint64_t x39; 1386 uint64_t x40; 1387 uint64_t x41; 1388 uint64_t x42; 1389 uint64_t x43; 1390 uint64_t x44; 1391 uint64_t x45; 1392 uint64_t x46; 1393 uint64_t x47; 1394 uint64_t x48; 1395 uint64_t x49; 1396 uint64_t x50; 1397 uint64_t x51; 1398 uint64_t x52; 1399 uint64_t x53; 1400 uint64_t x54; 1401 uint64_t x55; 1402 uint64_t x56; 1403 uint64_t x57; 1404 uint64_t x58; 1405 uint64_t x59; 1406 uint64_t x60; 1407 uint64_t x61; 1408 uint64_t x62; 1409 uint64_t x63; 1410 uint64_t x64; 1411 uint64_t x65; 1412 uint64_t x66; 1413 uint64_t x67; 1414 uint64_t x68; 1415 uint64_t x69; 1416 uint64_t x70; 1417 uint64_t x71; 1418 uint64_t x72; 1419 uint64_t x73; 1420 uint64_t x74; 1421 uint64_t x75; 1422 uint32_t x76; 1423 uint64_t x77; 1424 uint64_t x78; 1425 uint64_t x79; 1426 uint64_t x80; 1427 uint64_t x81; 1428 uint64_t x82; 1429 uint64_t x83; 1430 uint64_t x84; 1431 uint64_t x85; 1432 uint64_t x86; 1433 uint64_t x87; 1434 uint32_t x88; 1435 uint64_t x89; 1436 uint64_t x90; 1437 uint32_t x91; 1438 uint64_t x92; 1439 uint64_t x93; 1440 uint32_t x94; 1441 uint64_t x95; 1442 uint64_t x96; 1443 uint32_t x97; 1444 uint64_t x98; 1445 uint64_t x99; 1446 uint32_t x100; 1447 uint64_t x101; 1448 uint64_t x102; 1449 uint32_t x103; 1450 uint64_t x104; 1451 uint64_t x105; 1452 uint32_t x106; 1453 uint64_t x107; 1454 uint64_t x108; 1455 uint32_t x109; 1456 uint64_t x110; 1457 uint64_t x111; 1458 uint32_t x112; 1459 uint64_t x113; 1460 uint64_t x114; 1461 uint32_t x115; 1462 uint32_t x116; 1463 uint32_t x117; 1464 fiat_25519_uint1 x118; 1465 uint32_t x119; 1466 uint32_t x120; 1467 x1 = ((arg1[9]) * UINT8_C(0x13)); 1468 x2 = (x1 * 0x2); 1469 x3 = ((arg1[9]) * 0x2); 1470 x4 = ((arg1[8]) * UINT8_C(0x13)); 1471 x5 = ((uint64_t)x4 * 0x2); 1472 x6 = ((arg1[8]) * 0x2); 1473 x7 = ((arg1[7]) * UINT8_C(0x13)); 1474 x8 = (x7 * 0x2); 1475 x9 = ((arg1[7]) * 0x2); 1476 x10 = ((arg1[6]) * UINT8_C(0x13)); 1477 x11 = ((uint64_t)x10 * 0x2); 1478 x12 = ((arg1[6]) * 0x2); 1479 x13 = ((arg1[5]) * UINT8_C(0x13)); 1480 x14 = ((arg1[5]) * 0x2); 1481 x15 = ((arg1[4]) * 0x2); 1482 x16 = ((arg1[3]) * 0x2); 1483 x17 = ((arg1[2]) * 0x2); 1484 x18 = ((arg1[1]) * 0x2); 1485 x19 = ((uint64_t)(arg1[9]) * (x1 * 0x2)); 1486 x20 = ((uint64_t)(arg1[8]) * x2); 1487 x21 = ((uint64_t)(arg1[8]) * x4); 1488 x22 = ((arg1[7]) * ((uint64_t)x2 * 0x2)); 1489 x23 = ((arg1[7]) * x5); 1490 x24 = ((uint64_t)(arg1[7]) * (x7 * 0x2)); 1491 x25 = ((uint64_t)(arg1[6]) * x2); 1492 x26 = ((arg1[6]) * x5); 1493 x27 = ((uint64_t)(arg1[6]) * x8); 1494 x28 = ((uint64_t)(arg1[6]) * x10); 1495 x29 = ((arg1[5]) * ((uint64_t)x2 * 0x2)); 1496 x30 = ((arg1[5]) * x5); 1497 x31 = ((arg1[5]) * ((uint64_t)x8 * 0x2)); 1498 x32 = ((arg1[5]) * x11); 1499 x33 = ((uint64_t)(arg1[5]) * (x13 * 0x2)); 1500 x34 = ((uint64_t)(arg1[4]) * x2); 1501 x35 = ((arg1[4]) * x5); 1502 x36 = ((uint64_t)(arg1[4]) * x8); 1503 x37 = ((arg1[4]) * x11); 1504 x38 = ((uint64_t)(arg1[4]) * x14); 1505 x39 = ((uint64_t)(arg1[4]) * (arg1[4])); 1506 x40 = ((arg1[3]) * ((uint64_t)x2 * 0x2)); 1507 x41 = ((arg1[3]) * x5); 1508 x42 = ((arg1[3]) * ((uint64_t)x8 * 0x2)); 1509 x43 = ((uint64_t)(arg1[3]) * x12); 1510 x44 = ((uint64_t)(arg1[3]) * (x14 * 0x2)); 1511 x45 = ((uint64_t)(arg1[3]) * x15); 1512 x46 = ((uint64_t)(arg1[3]) * ((arg1[3]) * 0x2)); 1513 x47 = ((uint64_t)(arg1[2]) * x2); 1514 x48 = ((arg1[2]) * x5); 1515 x49 = ((uint64_t)(arg1[2]) * x9); 1516 x50 = ((uint64_t)(arg1[2]) * x12); 1517 x51 = ((uint64_t)(arg1[2]) * x14); 1518 x52 = ((uint64_t)(arg1[2]) * x15); 1519 x53 = ((uint64_t)(arg1[2]) * x16); 1520 x54 = ((uint64_t)(arg1[2]) * (arg1[2])); 1521 x55 = ((arg1[1]) * ((uint64_t)x2 * 0x2)); 1522 x56 = ((uint64_t)(arg1[1]) * x6); 1523 x57 = ((uint64_t)(arg1[1]) * (x9 * 0x2)); 1524 x58 = ((uint64_t)(arg1[1]) * x12); 1525 x59 = ((uint64_t)(arg1[1]) * (x14 * 0x2)); 1526 x60 = ((uint64_t)(arg1[1]) * x15); 1527 x61 = ((uint64_t)(arg1[1]) * (x16 * 0x2)); 1528 x62 = ((uint64_t)(arg1[1]) * x17); 1529 x63 = ((uint64_t)(arg1[1]) * ((arg1[1]) * 0x2)); 1530 x64 = ((uint64_t)(arg1[0]) * x3); 1531 x65 = ((uint64_t)(arg1[0]) * x6); 1532 x66 = ((uint64_t)(arg1[0]) * x9); 1533 x67 = ((uint64_t)(arg1[0]) * x12); 1534 x68 = ((uint64_t)(arg1[0]) * x14); 1535 x69 = ((uint64_t)(arg1[0]) * x15); 1536 x70 = ((uint64_t)(arg1[0]) * x16); 1537 x71 = ((uint64_t)(arg1[0]) * x17); 1538 x72 = ((uint64_t)(arg1[0]) * x18); 1539 x73 = ((uint64_t)(arg1[0]) * (arg1[0])); 1540 x74 = (x73 + (x55 + (x48 + (x42 + (x37 + x33))))); 1541 x75 = (x74 >> 26); 1542 x76 = (uint32_t)(x74 & UINT32_C(0x3ffffff)); 1543 x77 = (x64 + (x56 + (x49 + (x43 + x38)))); 1544 x78 = (x65 + (x57 + (x50 + (x44 + (x39 + x19))))); 1545 x79 = (x66 + (x58 + (x51 + (x45 + x20)))); 1546 x80 = (x67 + (x59 + (x52 + (x46 + (x22 + x21))))); 1547 x81 = (x68 + (x60 + (x53 + (x25 + x23)))); 1548 x82 = (x69 + (x61 + (x54 + (x29 + (x26 + x24))))); 1549 x83 = (x70 + (x62 + (x34 + (x30 + x27)))); 1550 x84 = (x71 + (x63 + (x40 + (x35 + (x31 + x28))))); 1551 x85 = (x72 + (x47 + (x41 + (x36 + x32)))); 1552 x86 = (x75 + x85); 1553 x87 = (x86 >> 25); 1554 x88 = (uint32_t)(x86 & UINT32_C(0x1ffffff)); 1555 x89 = (x87 + x84); 1556 x90 = (x89 >> 26); 1557 x91 = (uint32_t)(x89 & UINT32_C(0x3ffffff)); 1558 x92 = (x90 + x83); 1559 x93 = (x92 >> 25); 1560 x94 = (uint32_t)(x92 & UINT32_C(0x1ffffff)); 1561 x95 = (x93 + x82); 1562 x96 = (x95 >> 26); 1563 x97 = (uint32_t)(x95 & UINT32_C(0x3ffffff)); 1564 x98 = (x96 + x81); 1565 x99 = (x98 >> 25); 1566 x100 = (uint32_t)(x98 & UINT32_C(0x1ffffff)); 1567 x101 = (x99 + x80); 1568 x102 = (x101 >> 26); 1569 x103 = (uint32_t)(x101 & UINT32_C(0x3ffffff)); 1570 x104 = (x102 + x79); 1571 x105 = (x104 >> 25); 1572 x106 = (uint32_t)(x104 & UINT32_C(0x1ffffff)); 1573 x107 = (x105 + x78); 1574 x108 = (x107 >> 26); 1575 x109 = (uint32_t)(x107 & UINT32_C(0x3ffffff)); 1576 x110 = (x108 + x77); 1577 x111 = (x110 >> 25); 1578 x112 = (uint32_t)(x110 & UINT32_C(0x1ffffff)); 1579 x113 = (x111 * UINT8_C(0x13)); 1580 x114 = (x76 + x113); 1581 x115 = (uint32_t)(x114 >> 26); 1582 x116 = (uint32_t)(x114 & UINT32_C(0x3ffffff)); 1583 x117 = (x115 + x88); 1584 x118 = (fiat_25519_uint1)(x117 >> 25); 1585 x119 = (x117 & UINT32_C(0x1ffffff)); 1586 x120 = (x118 + x91); 1587 out1[0] = x116; 1588 out1[1] = x119; 1589 out1[2] = x120; 1590 out1[3] = x94; 1591 out1[4] = x97; 1592 out1[5] = x100; 1593 out1[6] = x103; 1594 out1[7] = x106; 1595 out1[8] = x109; 1596 out1[9] = x112; 1597 } 1598 1599 /* 1600 * The function fiat_25519_carry reduces a field element. 1601 * 1602 * Postconditions: 1603 * eval out1 mod m = eval arg1 mod m 1604 * 1605 */ 1606 static FIAT_25519_FIAT_INLINE void fiat_25519_carry(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) { 1607 uint32_t x1; 1608 uint32_t x2; 1609 uint32_t x3; 1610 uint32_t x4; 1611 uint32_t x5; 1612 uint32_t x6; 1613 uint32_t x7; 1614 uint32_t x8; 1615 uint32_t x9; 1616 uint32_t x10; 1617 uint32_t x11; 1618 uint32_t x12; 1619 uint32_t x13; 1620 uint32_t x14; 1621 uint32_t x15; 1622 uint32_t x16; 1623 uint32_t x17; 1624 uint32_t x18; 1625 uint32_t x19; 1626 uint32_t x20; 1627 uint32_t x21; 1628 uint32_t x22; 1629 x1 = (arg1[0]); 1630 x2 = ((x1 >> 26) + (arg1[1])); 1631 x3 = ((x2 >> 25) + (arg1[2])); 1632 x4 = ((x3 >> 26) + (arg1[3])); 1633 x5 = ((x4 >> 25) + (arg1[4])); 1634 x6 = ((x5 >> 26) + (arg1[5])); 1635 x7 = ((x6 >> 25) + (arg1[6])); 1636 x8 = ((x7 >> 26) + (arg1[7])); 1637 x9 = ((x8 >> 25) + (arg1[8])); 1638 x10 = ((x9 >> 26) + (arg1[9])); 1639 x11 = ((x1 & UINT32_C(0x3ffffff)) + ((x10 >> 25) * UINT8_C(0x13))); 1640 x12 = ((fiat_25519_uint1)(x11 >> 26) + (x2 & UINT32_C(0x1ffffff))); 1641 x13 = (x11 & UINT32_C(0x3ffffff)); 1642 x14 = (x12 & UINT32_C(0x1ffffff)); 1643 x15 = ((fiat_25519_uint1)(x12 >> 25) + (x3 & UINT32_C(0x3ffffff))); 1644 x16 = (x4 & UINT32_C(0x1ffffff)); 1645 x17 = (x5 & UINT32_C(0x3ffffff)); 1646 x18 = (x6 & UINT32_C(0x1ffffff)); 1647 x19 = (x7 & UINT32_C(0x3ffffff)); 1648 x20 = (x8 & UINT32_C(0x1ffffff)); 1649 x21 = (x9 & UINT32_C(0x3ffffff)); 1650 x22 = (x10 & UINT32_C(0x1ffffff)); 1651 out1[0] = x13; 1652 out1[1] = x14; 1653 out1[2] = x15; 1654 out1[3] = x16; 1655 out1[4] = x17; 1656 out1[5] = x18; 1657 out1[6] = x19; 1658 out1[7] = x20; 1659 out1[8] = x21; 1660 out1[9] = x22; 1661 } 1662 1663 /* 1664 * The function fiat_25519_add adds two field elements. 1665 * 1666 * Postconditions: 1667 * eval out1 mod m = (eval arg1 + eval arg2) mod m 1668 * 1669 */ 1670 static FIAT_25519_FIAT_INLINE void fiat_25519_add(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) { 1671 uint32_t x1; 1672 uint32_t x2; 1673 uint32_t x3; 1674 uint32_t x4; 1675 uint32_t x5; 1676 uint32_t x6; 1677 uint32_t x7; 1678 uint32_t x8; 1679 uint32_t x9; 1680 uint32_t x10; 1681 x1 = ((arg1[0]) + (arg2[0])); 1682 x2 = ((arg1[1]) + (arg2[1])); 1683 x3 = ((arg1[2]) + (arg2[2])); 1684 x4 = ((arg1[3]) + (arg2[3])); 1685 x5 = ((arg1[4]) + (arg2[4])); 1686 x6 = ((arg1[5]) + (arg2[5])); 1687 x7 = ((arg1[6]) + (arg2[6])); 1688 x8 = ((arg1[7]) + (arg2[7])); 1689 x9 = ((arg1[8]) + (arg2[8])); 1690 x10 = ((arg1[9]) + (arg2[9])); 1691 out1[0] = x1; 1692 out1[1] = x2; 1693 out1[2] = x3; 1694 out1[3] = x4; 1695 out1[4] = x5; 1696 out1[5] = x6; 1697 out1[6] = x7; 1698 out1[7] = x8; 1699 out1[8] = x9; 1700 out1[9] = x10; 1701 } 1702 1703 /* 1704 * The function fiat_25519_sub subtracts two field elements. 1705 * 1706 * Postconditions: 1707 * eval out1 mod m = (eval arg1 - eval arg2) mod m 1708 * 1709 */ 1710 static FIAT_25519_FIAT_INLINE void fiat_25519_sub(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) { 1711 uint32_t x1; 1712 uint32_t x2; 1713 uint32_t x3; 1714 uint32_t x4; 1715 uint32_t x5; 1716 uint32_t x6; 1717 uint32_t x7; 1718 uint32_t x8; 1719 uint32_t x9; 1720 uint32_t x10; 1721 x1 = ((UINT32_C(0x7ffffda) + (arg1[0])) - (arg2[0])); 1722 x2 = ((UINT32_C(0x3fffffe) + (arg1[1])) - (arg2[1])); 1723 x3 = ((UINT32_C(0x7fffffe) + (arg1[2])) - (arg2[2])); 1724 x4 = ((UINT32_C(0x3fffffe) + (arg1[3])) - (arg2[3])); 1725 x5 = ((UINT32_C(0x7fffffe) + (arg1[4])) - (arg2[4])); 1726 x6 = ((UINT32_C(0x3fffffe) + (arg1[5])) - (arg2[5])); 1727 x7 = ((UINT32_C(0x7fffffe) + (arg1[6])) - (arg2[6])); 1728 x8 = ((UINT32_C(0x3fffffe) + (arg1[7])) - (arg2[7])); 1729 x9 = ((UINT32_C(0x7fffffe) + (arg1[8])) - (arg2[8])); 1730 x10 = ((UINT32_C(0x3fffffe) + (arg1[9])) - (arg2[9])); 1731 out1[0] = x1; 1732 out1[1] = x2; 1733 out1[2] = x3; 1734 out1[3] = x4; 1735 out1[4] = x5; 1736 out1[5] = x6; 1737 out1[6] = x7; 1738 out1[7] = x8; 1739 out1[8] = x9; 1740 out1[9] = x10; 1741 } 1742 1743 /* 1744 * The function fiat_25519_opp negates a field element. 1745 * 1746 * Postconditions: 1747 * eval out1 mod m = -eval arg1 mod m 1748 * 1749 */ 1750 static FIAT_25519_FIAT_INLINE void fiat_25519_opp(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) { 1751 uint32_t x1; 1752 uint32_t x2; 1753 uint32_t x3; 1754 uint32_t x4; 1755 uint32_t x5; 1756 uint32_t x6; 1757 uint32_t x7; 1758 uint32_t x8; 1759 uint32_t x9; 1760 uint32_t x10; 1761 x1 = (UINT32_C(0x7ffffda) - (arg1[0])); 1762 x2 = (UINT32_C(0x3fffffe) - (arg1[1])); 1763 x3 = (UINT32_C(0x7fffffe) - (arg1[2])); 1764 x4 = (UINT32_C(0x3fffffe) - (arg1[3])); 1765 x5 = (UINT32_C(0x7fffffe) - (arg1[4])); 1766 x6 = (UINT32_C(0x3fffffe) - (arg1[5])); 1767 x7 = (UINT32_C(0x7fffffe) - (arg1[6])); 1768 x8 = (UINT32_C(0x3fffffe) - (arg1[7])); 1769 x9 = (UINT32_C(0x7fffffe) - (arg1[8])); 1770 x10 = (UINT32_C(0x3fffffe) - (arg1[9])); 1771 out1[0] = x1; 1772 out1[1] = x2; 1773 out1[2] = x3; 1774 out1[3] = x4; 1775 out1[4] = x5; 1776 out1[5] = x6; 1777 out1[6] = x7; 1778 out1[7] = x8; 1779 out1[8] = x9; 1780 out1[9] = x10; 1781 } 1782 1783 /* 1784 * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order. 1785 * 1786 * Postconditions: 1787 * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] 1788 * 1789 * Output Bounds: 1790 * 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]] 1791 */ 1792 static FIAT_25519_FIAT_INLINE void fiat_25519_to_bytes(uint8_t out1[32], const fiat_25519_tight_field_element arg1) { 1793 uint32_t x1; 1794 fiat_25519_uint1 x2; 1795 uint32_t x3; 1796 fiat_25519_uint1 x4; 1797 uint32_t x5; 1798 fiat_25519_uint1 x6; 1799 uint32_t x7; 1800 fiat_25519_uint1 x8; 1801 uint32_t x9; 1802 fiat_25519_uint1 x10; 1803 uint32_t x11; 1804 fiat_25519_uint1 x12; 1805 uint32_t x13; 1806 fiat_25519_uint1 x14; 1807 uint32_t x15; 1808 fiat_25519_uint1 x16; 1809 uint32_t x17; 1810 fiat_25519_uint1 x18; 1811 uint32_t x19; 1812 fiat_25519_uint1 x20; 1813 uint32_t x21; 1814 uint32_t x22; 1815 fiat_25519_uint1 x23; 1816 uint32_t x24; 1817 fiat_25519_uint1 x25; 1818 uint32_t x26; 1819 fiat_25519_uint1 x27; 1820 uint32_t x28; 1821 fiat_25519_uint1 x29; 1822 uint32_t x30; 1823 fiat_25519_uint1 x31; 1824 uint32_t x32; 1825 fiat_25519_uint1 x33; 1826 uint32_t x34; 1827 fiat_25519_uint1 x35; 1828 uint32_t x36; 1829 fiat_25519_uint1 x37; 1830 uint32_t x38; 1831 fiat_25519_uint1 x39; 1832 uint32_t x40; 1833 fiat_25519_uint1 x41; 1834 uint32_t x42; 1835 uint32_t x43; 1836 uint32_t x44; 1837 uint32_t x45; 1838 uint32_t x46; 1839 uint32_t x47; 1840 uint32_t x48; 1841 uint32_t x49; 1842 uint8_t x50; 1843 uint32_t x51; 1844 uint8_t x52; 1845 uint32_t x53; 1846 uint8_t x54; 1847 uint8_t x55; 1848 uint32_t x56; 1849 uint8_t x57; 1850 uint32_t x58; 1851 uint8_t x59; 1852 uint32_t x60; 1853 uint8_t x61; 1854 uint8_t x62; 1855 uint32_t x63; 1856 uint8_t x64; 1857 uint32_t x65; 1858 uint8_t x66; 1859 uint32_t x67; 1860 uint8_t x68; 1861 uint8_t x69; 1862 uint32_t x70; 1863 uint8_t x71; 1864 uint32_t x72; 1865 uint8_t x73; 1866 uint32_t x74; 1867 uint8_t x75; 1868 uint8_t x76; 1869 uint32_t x77; 1870 uint8_t x78; 1871 uint32_t x79; 1872 uint8_t x80; 1873 uint32_t x81; 1874 uint8_t x82; 1875 uint8_t x83; 1876 uint8_t x84; 1877 uint32_t x85; 1878 uint8_t x86; 1879 uint32_t x87; 1880 uint8_t x88; 1881 fiat_25519_uint1 x89; 1882 uint32_t x90; 1883 uint8_t x91; 1884 uint32_t x92; 1885 uint8_t x93; 1886 uint32_t x94; 1887 uint8_t x95; 1888 uint8_t x96; 1889 uint32_t x97; 1890 uint8_t x98; 1891 uint32_t x99; 1892 uint8_t x100; 1893 uint32_t x101; 1894 uint8_t x102; 1895 uint8_t x103; 1896 uint32_t x104; 1897 uint8_t x105; 1898 uint32_t x106; 1899 uint8_t x107; 1900 uint32_t x108; 1901 uint8_t x109; 1902 uint8_t x110; 1903 uint32_t x111; 1904 uint8_t x112; 1905 uint32_t x113; 1906 uint8_t x114; 1907 uint32_t x115; 1908 uint8_t x116; 1909 uint8_t x117; 1910 fiat_25519_subborrowx_u26(&x1, &x2, 0x0, (arg1[0]), UINT32_C(0x3ffffed)); 1911 fiat_25519_subborrowx_u25(&x3, &x4, x2, (arg1[1]), UINT32_C(0x1ffffff)); 1912 fiat_25519_subborrowx_u26(&x5, &x6, x4, (arg1[2]), UINT32_C(0x3ffffff)); 1913 fiat_25519_subborrowx_u25(&x7, &x8, x6, (arg1[3]), UINT32_C(0x1ffffff)); 1914 fiat_25519_subborrowx_u26(&x9, &x10, x8, (arg1[4]), UINT32_C(0x3ffffff)); 1915 fiat_25519_subborrowx_u25(&x11, &x12, x10, (arg1[5]), UINT32_C(0x1ffffff)); 1916 fiat_25519_subborrowx_u26(&x13, &x14, x12, (arg1[6]), UINT32_C(0x3ffffff)); 1917 fiat_25519_subborrowx_u25(&x15, &x16, x14, (arg1[7]), UINT32_C(0x1ffffff)); 1918 fiat_25519_subborrowx_u26(&x17, &x18, x16, (arg1[8]), UINT32_C(0x3ffffff)); 1919 fiat_25519_subborrowx_u25(&x19, &x20, x18, (arg1[9]), UINT32_C(0x1ffffff)); 1920 fiat_25519_cmovznz_u32(&x21, x20, 0x0, UINT32_C(0xffffffff)); 1921 fiat_25519_addcarryx_u26(&x22, &x23, 0x0, x1, (x21 & UINT32_C(0x3ffffed))); 1922 fiat_25519_addcarryx_u25(&x24, &x25, x23, x3, (x21 & UINT32_C(0x1ffffff))); 1923 fiat_25519_addcarryx_u26(&x26, &x27, x25, x5, (x21 & UINT32_C(0x3ffffff))); 1924 fiat_25519_addcarryx_u25(&x28, &x29, x27, x7, (x21 & UINT32_C(0x1ffffff))); 1925 fiat_25519_addcarryx_u26(&x30, &x31, x29, x9, (x21 & UINT32_C(0x3ffffff))); 1926 fiat_25519_addcarryx_u25(&x32, &x33, x31, x11, (x21 & UINT32_C(0x1ffffff))); 1927 fiat_25519_addcarryx_u26(&x34, &x35, x33, x13, (x21 & UINT32_C(0x3ffffff))); 1928 fiat_25519_addcarryx_u25(&x36, &x37, x35, x15, (x21 & UINT32_C(0x1ffffff))); 1929 fiat_25519_addcarryx_u26(&x38, &x39, x37, x17, (x21 & UINT32_C(0x3ffffff))); 1930 fiat_25519_addcarryx_u25(&x40, &x41, x39, x19, (x21 & UINT32_C(0x1ffffff))); 1931 x42 = (x40 << 6); 1932 x43 = (x38 << 4); 1933 x44 = (x36 << 3); 1934 x45 = (x34 * (uint32_t)0x2); 1935 x46 = (x30 << 6); 1936 x47 = (x28 << 5); 1937 x48 = (x26 << 3); 1938 x49 = (x24 << 2); 1939 x50 = (uint8_t)(x22 & UINT8_C(0xff)); 1940 x51 = (x22 >> 8); 1941 x52 = (uint8_t)(x51 & UINT8_C(0xff)); 1942 x53 = (x51 >> 8); 1943 x54 = (uint8_t)(x53 & UINT8_C(0xff)); 1944 x55 = (uint8_t)(x53 >> 8); 1945 x56 = (x49 + (uint32_t)x55); 1946 x57 = (uint8_t)(x56 & UINT8_C(0xff)); 1947 x58 = (x56 >> 8); 1948 x59 = (uint8_t)(x58 & UINT8_C(0xff)); 1949 x60 = (x58 >> 8); 1950 x61 = (uint8_t)(x60 & UINT8_C(0xff)); 1951 x62 = (uint8_t)(x60 >> 8); 1952 x63 = (x48 + (uint32_t)x62); 1953 x64 = (uint8_t)(x63 & UINT8_C(0xff)); 1954 x65 = (x63 >> 8); 1955 x66 = (uint8_t)(x65 & UINT8_C(0xff)); 1956 x67 = (x65 >> 8); 1957 x68 = (uint8_t)(x67 & UINT8_C(0xff)); 1958 x69 = (uint8_t)(x67 >> 8); 1959 x70 = (x47 + (uint32_t)x69); 1960 x71 = (uint8_t)(x70 & UINT8_C(0xff)); 1961 x72 = (x70 >> 8); 1962 x73 = (uint8_t)(x72 & UINT8_C(0xff)); 1963 x74 = (x72 >> 8); 1964 x75 = (uint8_t)(x74 & UINT8_C(0xff)); 1965 x76 = (uint8_t)(x74 >> 8); 1966 x77 = (x46 + (uint32_t)x76); 1967 x78 = (uint8_t)(x77 & UINT8_C(0xff)); 1968 x79 = (x77 >> 8); 1969 x80 = (uint8_t)(x79 & UINT8_C(0xff)); 1970 x81 = (x79 >> 8); 1971 x82 = (uint8_t)(x81 & UINT8_C(0xff)); 1972 x83 = (uint8_t)(x81 >> 8); 1973 x84 = (uint8_t)(x32 & UINT8_C(0xff)); 1974 x85 = (x32 >> 8); 1975 x86 = (uint8_t)(x85 & UINT8_C(0xff)); 1976 x87 = (x85 >> 8); 1977 x88 = (uint8_t)(x87 & UINT8_C(0xff)); 1978 x89 = (fiat_25519_uint1)(x87 >> 8); 1979 x90 = (x45 + (uint32_t)x89); 1980 x91 = (uint8_t)(x90 & UINT8_C(0xff)); 1981 x92 = (x90 >> 8); 1982 x93 = (uint8_t)(x92 & UINT8_C(0xff)); 1983 x94 = (x92 >> 8); 1984 x95 = (uint8_t)(x94 & UINT8_C(0xff)); 1985 x96 = (uint8_t)(x94 >> 8); 1986 x97 = (x44 + (uint32_t)x96); 1987 x98 = (uint8_t)(x97 & UINT8_C(0xff)); 1988 x99 = (x97 >> 8); 1989 x100 = (uint8_t)(x99 & UINT8_C(0xff)); 1990 x101 = (x99 >> 8); 1991 x102 = (uint8_t)(x101 & UINT8_C(0xff)); 1992 x103 = (uint8_t)(x101 >> 8); 1993 x104 = (x43 + (uint32_t)x103); 1994 x105 = (uint8_t)(x104 & UINT8_C(0xff)); 1995 x106 = (x104 >> 8); 1996 x107 = (uint8_t)(x106 & UINT8_C(0xff)); 1997 x108 = (x106 >> 8); 1998 x109 = (uint8_t)(x108 & UINT8_C(0xff)); 1999 x110 = (uint8_t)(x108 >> 8); 2000 x111 = (x42 + (uint32_t)x110); 2001 x112 = (uint8_t)(x111 & UINT8_C(0xff)); 2002 x113 = (x111 >> 8); 2003 x114 = (uint8_t)(x113 & UINT8_C(0xff)); 2004 x115 = (x113 >> 8); 2005 x116 = (uint8_t)(x115 & UINT8_C(0xff)); 2006 x117 = (uint8_t)(x115 >> 8); 2007 out1[0] = x50; 2008 out1[1] = x52; 2009 out1[2] = x54; 2010 out1[3] = x57; 2011 out1[4] = x59; 2012 out1[5] = x61; 2013 out1[6] = x64; 2014 out1[7] = x66; 2015 out1[8] = x68; 2016 out1[9] = x71; 2017 out1[10] = x73; 2018 out1[11] = x75; 2019 out1[12] = x78; 2020 out1[13] = x80; 2021 out1[14] = x82; 2022 out1[15] = x83; 2023 out1[16] = x84; 2024 out1[17] = x86; 2025 out1[18] = x88; 2026 out1[19] = x91; 2027 out1[20] = x93; 2028 out1[21] = x95; 2029 out1[22] = x98; 2030 out1[23] = x100; 2031 out1[24] = x102; 2032 out1[25] = x105; 2033 out1[26] = x107; 2034 out1[27] = x109; 2035 out1[28] = x112; 2036 out1[29] = x114; 2037 out1[30] = x116; 2038 out1[31] = x117; 2039 } 2040 2041 /* 2042 * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order. 2043 * 2044 * Postconditions: 2045 * eval out1 mod m = bytes_eval arg1 mod m 2046 * 2047 * Input Bounds: 2048 * 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]] 2049 */ 2050 static FIAT_25519_FIAT_INLINE void fiat_25519_from_bytes(fiat_25519_tight_field_element out1, const uint8_t arg1[32]) { 2051 uint32_t x1; 2052 uint32_t x2; 2053 uint32_t x3; 2054 uint32_t x4; 2055 uint32_t x5; 2056 uint32_t x6; 2057 uint32_t x7; 2058 uint32_t x8; 2059 uint32_t x9; 2060 uint32_t x10; 2061 uint32_t x11; 2062 uint32_t x12; 2063 uint32_t x13; 2064 uint32_t x14; 2065 uint32_t x15; 2066 uint8_t x16; 2067 uint32_t x17; 2068 uint32_t x18; 2069 uint32_t x19; 2070 uint32_t x20; 2071 uint32_t x21; 2072 uint32_t x22; 2073 uint32_t x23; 2074 uint32_t x24; 2075 uint32_t x25; 2076 uint32_t x26; 2077 uint32_t x27; 2078 uint32_t x28; 2079 uint32_t x29; 2080 uint32_t x30; 2081 uint32_t x31; 2082 uint8_t x32; 2083 uint32_t x33; 2084 uint32_t x34; 2085 uint32_t x35; 2086 uint32_t x36; 2087 uint8_t x37; 2088 uint32_t x38; 2089 uint32_t x39; 2090 uint32_t x40; 2091 uint32_t x41; 2092 uint8_t x42; 2093 uint32_t x43; 2094 uint32_t x44; 2095 uint32_t x45; 2096 uint32_t x46; 2097 uint8_t x47; 2098 uint32_t x48; 2099 uint32_t x49; 2100 uint32_t x50; 2101 uint32_t x51; 2102 uint8_t x52; 2103 uint32_t x53; 2104 uint32_t x54; 2105 uint32_t x55; 2106 uint32_t x56; 2107 uint32_t x57; 2108 uint32_t x58; 2109 uint32_t x59; 2110 uint8_t x60; 2111 uint32_t x61; 2112 uint32_t x62; 2113 uint32_t x63; 2114 uint32_t x64; 2115 uint8_t x65; 2116 uint32_t x66; 2117 uint32_t x67; 2118 uint32_t x68; 2119 uint32_t x69; 2120 uint8_t x70; 2121 uint32_t x71; 2122 uint32_t x72; 2123 uint32_t x73; 2124 uint32_t x74; 2125 uint8_t x75; 2126 uint32_t x76; 2127 uint32_t x77; 2128 uint32_t x78; 2129 x1 = ((uint32_t)(arg1[31]) << 18); 2130 x2 = ((uint32_t)(arg1[30]) << 10); 2131 x3 = ((uint32_t)(arg1[29]) << 2); 2132 x4 = ((uint32_t)(arg1[28]) << 20); 2133 x5 = ((uint32_t)(arg1[27]) << 12); 2134 x6 = ((uint32_t)(arg1[26]) << 4); 2135 x7 = ((uint32_t)(arg1[25]) << 21); 2136 x8 = ((uint32_t)(arg1[24]) << 13); 2137 x9 = ((uint32_t)(arg1[23]) << 5); 2138 x10 = ((uint32_t)(arg1[22]) << 23); 2139 x11 = ((uint32_t)(arg1[21]) << 15); 2140 x12 = ((uint32_t)(arg1[20]) << 7); 2141 x13 = ((uint32_t)(arg1[19]) << 24); 2142 x14 = ((uint32_t)(arg1[18]) << 16); 2143 x15 = ((uint32_t)(arg1[17]) << 8); 2144 x16 = (arg1[16]); 2145 x17 = ((uint32_t)(arg1[15]) << 18); 2146 x18 = ((uint32_t)(arg1[14]) << 10); 2147 x19 = ((uint32_t)(arg1[13]) << 2); 2148 x20 = ((uint32_t)(arg1[12]) << 19); 2149 x21 = ((uint32_t)(arg1[11]) << 11); 2150 x22 = ((uint32_t)(arg1[10]) << 3); 2151 x23 = ((uint32_t)(arg1[9]) << 21); 2152 x24 = ((uint32_t)(arg1[8]) << 13); 2153 x25 = ((uint32_t)(arg1[7]) << 5); 2154 x26 = ((uint32_t)(arg1[6]) << 22); 2155 x27 = ((uint32_t)(arg1[5]) << 14); 2156 x28 = ((uint32_t)(arg1[4]) << 6); 2157 x29 = ((uint32_t)(arg1[3]) << 24); 2158 x30 = ((uint32_t)(arg1[2]) << 16); 2159 x31 = ((uint32_t)(arg1[1]) << 8); 2160 x32 = (arg1[0]); 2161 x33 = (x31 + (uint32_t)x32); 2162 x34 = (x30 + x33); 2163 x35 = (x29 + x34); 2164 x36 = (x35 & UINT32_C(0x3ffffff)); 2165 x37 = (uint8_t)(x35 >> 26); 2166 x38 = (x28 + (uint32_t)x37); 2167 x39 = (x27 + x38); 2168 x40 = (x26 + x39); 2169 x41 = (x40 & UINT32_C(0x1ffffff)); 2170 x42 = (uint8_t)(x40 >> 25); 2171 x43 = (x25 + (uint32_t)x42); 2172 x44 = (x24 + x43); 2173 x45 = (x23 + x44); 2174 x46 = (x45 & UINT32_C(0x3ffffff)); 2175 x47 = (uint8_t)(x45 >> 26); 2176 x48 = (x22 + (uint32_t)x47); 2177 x49 = (x21 + x48); 2178 x50 = (x20 + x49); 2179 x51 = (x50 & UINT32_C(0x1ffffff)); 2180 x52 = (uint8_t)(x50 >> 25); 2181 x53 = (x19 + (uint32_t)x52); 2182 x54 = (x18 + x53); 2183 x55 = (x17 + x54); 2184 x56 = (x15 + (uint32_t)x16); 2185 x57 = (x14 + x56); 2186 x58 = (x13 + x57); 2187 x59 = (x58 & UINT32_C(0x1ffffff)); 2188 x60 = (uint8_t)(x58 >> 25); 2189 x61 = (x12 + (uint32_t)x60); 2190 x62 = (x11 + x61); 2191 x63 = (x10 + x62); 2192 x64 = (x63 & UINT32_C(0x3ffffff)); 2193 x65 = (uint8_t)(x63 >> 26); 2194 x66 = (x9 + (uint32_t)x65); 2195 x67 = (x8 + x66); 2196 x68 = (x7 + x67); 2197 x69 = (x68 & UINT32_C(0x1ffffff)); 2198 x70 = (uint8_t)(x68 >> 25); 2199 x71 = (x6 + (uint32_t)x70); 2200 x72 = (x5 + x71); 2201 x73 = (x4 + x72); 2202 x74 = (x73 & UINT32_C(0x3ffffff)); 2203 x75 = (uint8_t)(x73 >> 26); 2204 x76 = (x3 + (uint32_t)x75); 2205 x77 = (x2 + x76); 2206 x78 = (x1 + x77); 2207 out1[0] = x36; 2208 out1[1] = x41; 2209 out1[2] = x46; 2210 out1[3] = x51; 2211 out1[4] = x55; 2212 out1[5] = x59; 2213 out1[6] = x64; 2214 out1[7] = x69; 2215 out1[8] = x74; 2216 out1[9] = x78; 2217 } 2218 2219 #endif /* not defined(BORINGSSL_CURVE25519_64BIT) */ 2220