1 /* Autogenerated */ 2 /* curve description: p256 */ 3 /* requested operations: (all) */ 4 /* m = 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff (from "2^256 - 2^224 + 2^192 + 2^96 - 1") */ 5 /* machine_wordsize = 32 (from "32") */ 6 /* */ 7 /* NOTE: In addition to the bounds specified above each function, all */ 8 /* functions synthesized for this Montgomery arithmetic require the */ 9 /* input to be strictly less than the prime modulus (m), and also */ 10 /* require the input to be in the unique saturated representation. */ 11 /* All functions also ensure that these two properties are true of */ 12 /* return values. */ 13 14 #include <stdint.h> 15 typedef unsigned char fiat_p256_uint1; 16 typedef signed char fiat_p256_int1; 17 18 19 /* 20 * Input Bounds: 21 * arg1: [0x0 ~> 0x1] 22 * arg2: [0x0 ~> 0xffffffff] 23 * arg3: [0x0 ~> 0xffffffff] 24 * Output Bounds: 25 * out1: [0x0 ~> 0xffffffff] 26 * out2: [0x0 ~> 0x1] 27 */ 28 static void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) { 29 uint64_t x1 = ((arg1 + (uint64_t)arg2) + arg3); 30 uint32_t x2 = (uint32_t)(x1 & UINT32_C(0xffffffff)); 31 fiat_p256_uint1 x3 = (fiat_p256_uint1)(x1 >> 32); 32 *out1 = x2; 33 *out2 = x3; 34 } 35 36 /* 37 * Input Bounds: 38 * arg1: [0x0 ~> 0x1] 39 * arg2: [0x0 ~> 0xffffffff] 40 * arg3: [0x0 ~> 0xffffffff] 41 * Output Bounds: 42 * out1: [0x0 ~> 0xffffffff] 43 * out2: [0x0 ~> 0x1] 44 */ 45 static void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) { 46 int64_t x1 = ((arg2 - (int64_t)arg1) - arg3); 47 fiat_p256_int1 x2 = (fiat_p256_int1)(x1 >> 32); 48 uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff)); 49 *out1 = x3; 50 *out2 = (fiat_p256_uint1)(0x0 - x2); 51 } 52 53 /* 54 * Input Bounds: 55 * arg1: [0x0 ~> 0xffffffff] 56 * arg2: [0x0 ~> 0xffffffff] 57 * Output Bounds: 58 * out1: [0x0 ~> 0xffffffff] 59 * out2: [0x0 ~> 0xffffffff] 60 */ 61 static void fiat_p256_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, uint32_t arg2) { 62 uint64_t x1 = ((uint64_t)arg1 * arg2); 63 uint32_t x2 = (uint32_t)(x1 & UINT32_C(0xffffffff)); 64 uint32_t x3 = (uint32_t)(x1 >> 32); 65 *out1 = x2; 66 *out2 = x3; 67 } 68 69 /* 70 * Input Bounds: 71 * arg1: [0x0 ~> 0x1] 72 * arg2: [0x0 ~> 0xffffffff] 73 * arg3: [0x0 ~> 0xffffffff] 74 * Output Bounds: 75 * out1: [0x0 ~> 0xffffffff] 76 */ 77 static void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) { 78 fiat_p256_uint1 x1 = (!(!arg1)); 79 uint32_t x2 = ((fiat_p256_int1)(0x0 - x1) & UINT32_C(0xffffffff)); 80 uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); 81 *out1 = x3; 82 } 83 84 /* 85 * Input Bounds: 86 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 87 * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 88 * Output Bounds: 89 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 90 */ 91 static void fiat_p256_mul(uint32_t out1[8], const uint32_t arg1[8], const uint32_t arg2[8]) { 92 uint32_t x1 = (arg1[1]); 93 uint32_t x2 = (arg1[2]); 94 uint32_t x3 = (arg1[3]); 95 uint32_t x4 = (arg1[4]); 96 uint32_t x5 = (arg1[5]); 97 uint32_t x6 = (arg1[6]); 98 uint32_t x7 = (arg1[7]); 99 uint32_t x8 = (arg1[0]); 100 uint32_t x9; 101 uint32_t x10; 102 fiat_p256_mulx_u32(&x9, &x10, x8, (arg2[7])); 103 uint32_t x11; 104 uint32_t x12; 105 fiat_p256_mulx_u32(&x11, &x12, x8, (arg2[6])); 106 uint32_t x13; 107 uint32_t x14; 108 fiat_p256_mulx_u32(&x13, &x14, x8, (arg2[5])); 109 uint32_t x15; 110 uint32_t x16; 111 fiat_p256_mulx_u32(&x15, &x16, x8, (arg2[4])); 112 uint32_t x17; 113 uint32_t x18; 114 fiat_p256_mulx_u32(&x17, &x18, x8, (arg2[3])); 115 uint32_t x19; 116 uint32_t x20; 117 fiat_p256_mulx_u32(&x19, &x20, x8, (arg2[2])); 118 uint32_t x21; 119 uint32_t x22; 120 fiat_p256_mulx_u32(&x21, &x22, x8, (arg2[1])); 121 uint32_t x23; 122 uint32_t x24; 123 fiat_p256_mulx_u32(&x23, &x24, x8, (arg2[0])); 124 uint32_t x25; 125 fiat_p256_uint1 x26; 126 fiat_p256_addcarryx_u32(&x25, &x26, 0x0, x21, x24); 127 uint32_t x27; 128 fiat_p256_uint1 x28; 129 fiat_p256_addcarryx_u32(&x27, &x28, x26, x19, x22); 130 uint32_t x29; 131 fiat_p256_uint1 x30; 132 fiat_p256_addcarryx_u32(&x29, &x30, x28, x17, x20); 133 uint32_t x31; 134 fiat_p256_uint1 x32; 135 fiat_p256_addcarryx_u32(&x31, &x32, x30, x15, x18); 136 uint32_t x33; 137 fiat_p256_uint1 x34; 138 fiat_p256_addcarryx_u32(&x33, &x34, x32, x13, x16); 139 uint32_t x35; 140 fiat_p256_uint1 x36; 141 fiat_p256_addcarryx_u32(&x35, &x36, x34, x11, x14); 142 uint32_t x37; 143 fiat_p256_uint1 x38; 144 fiat_p256_addcarryx_u32(&x37, &x38, x36, x9, x12); 145 uint32_t x39; 146 fiat_p256_uint1 x40; 147 fiat_p256_addcarryx_u32(&x39, &x40, x38, 0x0, x10); 148 uint32_t x41; 149 uint32_t x42; 150 fiat_p256_mulx_u32(&x41, &x42, x23, UINT32_C(0xffffffff)); 151 uint32_t x43; 152 uint32_t x44; 153 fiat_p256_mulx_u32(&x43, &x44, x23, UINT32_C(0xffffffff)); 154 uint32_t x45; 155 uint32_t x46; 156 fiat_p256_mulx_u32(&x45, &x46, x23, UINT32_C(0xffffffff)); 157 uint32_t x47; 158 uint32_t x48; 159 fiat_p256_mulx_u32(&x47, &x48, x23, UINT32_C(0xffffffff)); 160 uint32_t x49; 161 fiat_p256_uint1 x50; 162 fiat_p256_addcarryx_u32(&x49, &x50, 0x0, x45, x48); 163 uint32_t x51; 164 fiat_p256_uint1 x52; 165 fiat_p256_addcarryx_u32(&x51, &x52, x50, x43, x46); 166 uint32_t x53; 167 fiat_p256_uint1 x54; 168 fiat_p256_addcarryx_u32(&x53, &x54, x52, 0x0, x44); 169 uint32_t x55; 170 fiat_p256_uint1 x56; 171 fiat_p256_addcarryx_u32(&x55, &x56, 0x0, x47, x23); 172 uint32_t x57; 173 fiat_p256_uint1 x58; 174 fiat_p256_addcarryx_u32(&x57, &x58, x56, x49, x25); 175 uint32_t x59; 176 fiat_p256_uint1 x60; 177 fiat_p256_addcarryx_u32(&x59, &x60, x58, x51, x27); 178 uint32_t x61; 179 fiat_p256_uint1 x62; 180 fiat_p256_addcarryx_u32(&x61, &x62, x60, x53, x29); 181 uint32_t x63; 182 fiat_p256_uint1 x64; 183 fiat_p256_addcarryx_u32(&x63, &x64, x62, 0x0, x31); 184 uint32_t x65; 185 fiat_p256_uint1 x66; 186 fiat_p256_addcarryx_u32(&x65, &x66, x64, 0x0, x33); 187 uint32_t x67; 188 fiat_p256_uint1 x68; 189 fiat_p256_addcarryx_u32(&x67, &x68, x66, x23, x35); 190 uint32_t x69; 191 fiat_p256_uint1 x70; 192 fiat_p256_addcarryx_u32(&x69, &x70, x68, x41, x37); 193 uint32_t x71; 194 fiat_p256_uint1 x72; 195 fiat_p256_addcarryx_u32(&x71, &x72, x70, x42, x39); 196 uint32_t x73; 197 fiat_p256_uint1 x74; 198 fiat_p256_addcarryx_u32(&x73, &x74, x72, 0x0, 0x0); 199 uint32_t x75; 200 uint32_t x76; 201 fiat_p256_mulx_u32(&x75, &x76, x1, (arg2[7])); 202 uint32_t x77; 203 uint32_t x78; 204 fiat_p256_mulx_u32(&x77, &x78, x1, (arg2[6])); 205 uint32_t x79; 206 uint32_t x80; 207 fiat_p256_mulx_u32(&x79, &x80, x1, (arg2[5])); 208 uint32_t x81; 209 uint32_t x82; 210 fiat_p256_mulx_u32(&x81, &x82, x1, (arg2[4])); 211 uint32_t x83; 212 uint32_t x84; 213 fiat_p256_mulx_u32(&x83, &x84, x1, (arg2[3])); 214 uint32_t x85; 215 uint32_t x86; 216 fiat_p256_mulx_u32(&x85, &x86, x1, (arg2[2])); 217 uint32_t x87; 218 uint32_t x88; 219 fiat_p256_mulx_u32(&x87, &x88, x1, (arg2[1])); 220 uint32_t x89; 221 uint32_t x90; 222 fiat_p256_mulx_u32(&x89, &x90, x1, (arg2[0])); 223 uint32_t x91; 224 fiat_p256_uint1 x92; 225 fiat_p256_addcarryx_u32(&x91, &x92, 0x0, x87, x90); 226 uint32_t x93; 227 fiat_p256_uint1 x94; 228 fiat_p256_addcarryx_u32(&x93, &x94, x92, x85, x88); 229 uint32_t x95; 230 fiat_p256_uint1 x96; 231 fiat_p256_addcarryx_u32(&x95, &x96, x94, x83, x86); 232 uint32_t x97; 233 fiat_p256_uint1 x98; 234 fiat_p256_addcarryx_u32(&x97, &x98, x96, x81, x84); 235 uint32_t x99; 236 fiat_p256_uint1 x100; 237 fiat_p256_addcarryx_u32(&x99, &x100, x98, x79, x82); 238 uint32_t x101; 239 fiat_p256_uint1 x102; 240 fiat_p256_addcarryx_u32(&x101, &x102, x100, x77, x80); 241 uint32_t x103; 242 fiat_p256_uint1 x104; 243 fiat_p256_addcarryx_u32(&x103, &x104, x102, x75, x78); 244 uint32_t x105; 245 fiat_p256_uint1 x106; 246 fiat_p256_addcarryx_u32(&x105, &x106, x104, 0x0, x76); 247 uint32_t x107; 248 fiat_p256_uint1 x108; 249 fiat_p256_addcarryx_u32(&x107, &x108, 0x0, x89, x57); 250 uint32_t x109; 251 fiat_p256_uint1 x110; 252 fiat_p256_addcarryx_u32(&x109, &x110, x108, x91, x59); 253 uint32_t x111; 254 fiat_p256_uint1 x112; 255 fiat_p256_addcarryx_u32(&x111, &x112, x110, x93, x61); 256 uint32_t x113; 257 fiat_p256_uint1 x114; 258 fiat_p256_addcarryx_u32(&x113, &x114, x112, x95, x63); 259 uint32_t x115; 260 fiat_p256_uint1 x116; 261 fiat_p256_addcarryx_u32(&x115, &x116, x114, x97, x65); 262 uint32_t x117; 263 fiat_p256_uint1 x118; 264 fiat_p256_addcarryx_u32(&x117, &x118, x116, x99, x67); 265 uint32_t x119; 266 fiat_p256_uint1 x120; 267 fiat_p256_addcarryx_u32(&x119, &x120, x118, x101, x69); 268 uint32_t x121; 269 fiat_p256_uint1 x122; 270 fiat_p256_addcarryx_u32(&x121, &x122, x120, x103, x71); 271 uint32_t x123; 272 fiat_p256_uint1 x124; 273 fiat_p256_addcarryx_u32(&x123, &x124, x122, x105, (fiat_p256_uint1)x73); 274 uint32_t x125; 275 uint32_t x126; 276 fiat_p256_mulx_u32(&x125, &x126, x107, UINT32_C(0xffffffff)); 277 uint32_t x127; 278 uint32_t x128; 279 fiat_p256_mulx_u32(&x127, &x128, x107, UINT32_C(0xffffffff)); 280 uint32_t x129; 281 uint32_t x130; 282 fiat_p256_mulx_u32(&x129, &x130, x107, UINT32_C(0xffffffff)); 283 uint32_t x131; 284 uint32_t x132; 285 fiat_p256_mulx_u32(&x131, &x132, x107, UINT32_C(0xffffffff)); 286 uint32_t x133; 287 fiat_p256_uint1 x134; 288 fiat_p256_addcarryx_u32(&x133, &x134, 0x0, x129, x132); 289 uint32_t x135; 290 fiat_p256_uint1 x136; 291 fiat_p256_addcarryx_u32(&x135, &x136, x134, x127, x130); 292 uint32_t x137; 293 fiat_p256_uint1 x138; 294 fiat_p256_addcarryx_u32(&x137, &x138, x136, 0x0, x128); 295 uint32_t x139; 296 fiat_p256_uint1 x140; 297 fiat_p256_addcarryx_u32(&x139, &x140, 0x0, x131, x107); 298 uint32_t x141; 299 fiat_p256_uint1 x142; 300 fiat_p256_addcarryx_u32(&x141, &x142, x140, x133, x109); 301 uint32_t x143; 302 fiat_p256_uint1 x144; 303 fiat_p256_addcarryx_u32(&x143, &x144, x142, x135, x111); 304 uint32_t x145; 305 fiat_p256_uint1 x146; 306 fiat_p256_addcarryx_u32(&x145, &x146, x144, x137, x113); 307 uint32_t x147; 308 fiat_p256_uint1 x148; 309 fiat_p256_addcarryx_u32(&x147, &x148, x146, 0x0, x115); 310 uint32_t x149; 311 fiat_p256_uint1 x150; 312 fiat_p256_addcarryx_u32(&x149, &x150, x148, 0x0, x117); 313 uint32_t x151; 314 fiat_p256_uint1 x152; 315 fiat_p256_addcarryx_u32(&x151, &x152, x150, x107, x119); 316 uint32_t x153; 317 fiat_p256_uint1 x154; 318 fiat_p256_addcarryx_u32(&x153, &x154, x152, x125, x121); 319 uint32_t x155; 320 fiat_p256_uint1 x156; 321 fiat_p256_addcarryx_u32(&x155, &x156, x154, x126, x123); 322 uint32_t x157; 323 fiat_p256_uint1 x158; 324 fiat_p256_addcarryx_u32(&x157, &x158, x156, 0x0, x124); 325 uint32_t x159; 326 uint32_t x160; 327 fiat_p256_mulx_u32(&x159, &x160, x2, (arg2[7])); 328 uint32_t x161; 329 uint32_t x162; 330 fiat_p256_mulx_u32(&x161, &x162, x2, (arg2[6])); 331 uint32_t x163; 332 uint32_t x164; 333 fiat_p256_mulx_u32(&x163, &x164, x2, (arg2[5])); 334 uint32_t x165; 335 uint32_t x166; 336 fiat_p256_mulx_u32(&x165, &x166, x2, (arg2[4])); 337 uint32_t x167; 338 uint32_t x168; 339 fiat_p256_mulx_u32(&x167, &x168, x2, (arg2[3])); 340 uint32_t x169; 341 uint32_t x170; 342 fiat_p256_mulx_u32(&x169, &x170, x2, (arg2[2])); 343 uint32_t x171; 344 uint32_t x172; 345 fiat_p256_mulx_u32(&x171, &x172, x2, (arg2[1])); 346 uint32_t x173; 347 uint32_t x174; 348 fiat_p256_mulx_u32(&x173, &x174, x2, (arg2[0])); 349 uint32_t x175; 350 fiat_p256_uint1 x176; 351 fiat_p256_addcarryx_u32(&x175, &x176, 0x0, x171, x174); 352 uint32_t x177; 353 fiat_p256_uint1 x178; 354 fiat_p256_addcarryx_u32(&x177, &x178, x176, x169, x172); 355 uint32_t x179; 356 fiat_p256_uint1 x180; 357 fiat_p256_addcarryx_u32(&x179, &x180, x178, x167, x170); 358 uint32_t x181; 359 fiat_p256_uint1 x182; 360 fiat_p256_addcarryx_u32(&x181, &x182, x180, x165, x168); 361 uint32_t x183; 362 fiat_p256_uint1 x184; 363 fiat_p256_addcarryx_u32(&x183, &x184, x182, x163, x166); 364 uint32_t x185; 365 fiat_p256_uint1 x186; 366 fiat_p256_addcarryx_u32(&x185, &x186, x184, x161, x164); 367 uint32_t x187; 368 fiat_p256_uint1 x188; 369 fiat_p256_addcarryx_u32(&x187, &x188, x186, x159, x162); 370 uint32_t x189; 371 fiat_p256_uint1 x190; 372 fiat_p256_addcarryx_u32(&x189, &x190, x188, 0x0, x160); 373 uint32_t x191; 374 fiat_p256_uint1 x192; 375 fiat_p256_addcarryx_u32(&x191, &x192, 0x0, x173, x141); 376 uint32_t x193; 377 fiat_p256_uint1 x194; 378 fiat_p256_addcarryx_u32(&x193, &x194, x192, x175, x143); 379 uint32_t x195; 380 fiat_p256_uint1 x196; 381 fiat_p256_addcarryx_u32(&x195, &x196, x194, x177, x145); 382 uint32_t x197; 383 fiat_p256_uint1 x198; 384 fiat_p256_addcarryx_u32(&x197, &x198, x196, x179, x147); 385 uint32_t x199; 386 fiat_p256_uint1 x200; 387 fiat_p256_addcarryx_u32(&x199, &x200, x198, x181, x149); 388 uint32_t x201; 389 fiat_p256_uint1 x202; 390 fiat_p256_addcarryx_u32(&x201, &x202, x200, x183, x151); 391 uint32_t x203; 392 fiat_p256_uint1 x204; 393 fiat_p256_addcarryx_u32(&x203, &x204, x202, x185, x153); 394 uint32_t x205; 395 fiat_p256_uint1 x206; 396 fiat_p256_addcarryx_u32(&x205, &x206, x204, x187, x155); 397 uint32_t x207; 398 fiat_p256_uint1 x208; 399 fiat_p256_addcarryx_u32(&x207, &x208, x206, x189, x157); 400 uint32_t x209; 401 uint32_t x210; 402 fiat_p256_mulx_u32(&x209, &x210, x191, UINT32_C(0xffffffff)); 403 uint32_t x211; 404 uint32_t x212; 405 fiat_p256_mulx_u32(&x211, &x212, x191, UINT32_C(0xffffffff)); 406 uint32_t x213; 407 uint32_t x214; 408 fiat_p256_mulx_u32(&x213, &x214, x191, UINT32_C(0xffffffff)); 409 uint32_t x215; 410 uint32_t x216; 411 fiat_p256_mulx_u32(&x215, &x216, x191, UINT32_C(0xffffffff)); 412 uint32_t x217; 413 fiat_p256_uint1 x218; 414 fiat_p256_addcarryx_u32(&x217, &x218, 0x0, x213, x216); 415 uint32_t x219; 416 fiat_p256_uint1 x220; 417 fiat_p256_addcarryx_u32(&x219, &x220, x218, x211, x214); 418 uint32_t x221; 419 fiat_p256_uint1 x222; 420 fiat_p256_addcarryx_u32(&x221, &x222, x220, 0x0, x212); 421 uint32_t x223; 422 fiat_p256_uint1 x224; 423 fiat_p256_addcarryx_u32(&x223, &x224, 0x0, x215, x191); 424 uint32_t x225; 425 fiat_p256_uint1 x226; 426 fiat_p256_addcarryx_u32(&x225, &x226, x224, x217, x193); 427 uint32_t x227; 428 fiat_p256_uint1 x228; 429 fiat_p256_addcarryx_u32(&x227, &x228, x226, x219, x195); 430 uint32_t x229; 431 fiat_p256_uint1 x230; 432 fiat_p256_addcarryx_u32(&x229, &x230, x228, x221, x197); 433 uint32_t x231; 434 fiat_p256_uint1 x232; 435 fiat_p256_addcarryx_u32(&x231, &x232, x230, 0x0, x199); 436 uint32_t x233; 437 fiat_p256_uint1 x234; 438 fiat_p256_addcarryx_u32(&x233, &x234, x232, 0x0, x201); 439 uint32_t x235; 440 fiat_p256_uint1 x236; 441 fiat_p256_addcarryx_u32(&x235, &x236, x234, x191, x203); 442 uint32_t x237; 443 fiat_p256_uint1 x238; 444 fiat_p256_addcarryx_u32(&x237, &x238, x236, x209, x205); 445 uint32_t x239; 446 fiat_p256_uint1 x240; 447 fiat_p256_addcarryx_u32(&x239, &x240, x238, x210, x207); 448 uint32_t x241; 449 fiat_p256_uint1 x242; 450 fiat_p256_addcarryx_u32(&x241, &x242, x240, 0x0, x208); 451 uint32_t x243; 452 uint32_t x244; 453 fiat_p256_mulx_u32(&x243, &x244, x3, (arg2[7])); 454 uint32_t x245; 455 uint32_t x246; 456 fiat_p256_mulx_u32(&x245, &x246, x3, (arg2[6])); 457 uint32_t x247; 458 uint32_t x248; 459 fiat_p256_mulx_u32(&x247, &x248, x3, (arg2[5])); 460 uint32_t x249; 461 uint32_t x250; 462 fiat_p256_mulx_u32(&x249, &x250, x3, (arg2[4])); 463 uint32_t x251; 464 uint32_t x252; 465 fiat_p256_mulx_u32(&x251, &x252, x3, (arg2[3])); 466 uint32_t x253; 467 uint32_t x254; 468 fiat_p256_mulx_u32(&x253, &x254, x3, (arg2[2])); 469 uint32_t x255; 470 uint32_t x256; 471 fiat_p256_mulx_u32(&x255, &x256, x3, (arg2[1])); 472 uint32_t x257; 473 uint32_t x258; 474 fiat_p256_mulx_u32(&x257, &x258, x3, (arg2[0])); 475 uint32_t x259; 476 fiat_p256_uint1 x260; 477 fiat_p256_addcarryx_u32(&x259, &x260, 0x0, x255, x258); 478 uint32_t x261; 479 fiat_p256_uint1 x262; 480 fiat_p256_addcarryx_u32(&x261, &x262, x260, x253, x256); 481 uint32_t x263; 482 fiat_p256_uint1 x264; 483 fiat_p256_addcarryx_u32(&x263, &x264, x262, x251, x254); 484 uint32_t x265; 485 fiat_p256_uint1 x266; 486 fiat_p256_addcarryx_u32(&x265, &x266, x264, x249, x252); 487 uint32_t x267; 488 fiat_p256_uint1 x268; 489 fiat_p256_addcarryx_u32(&x267, &x268, x266, x247, x250); 490 uint32_t x269; 491 fiat_p256_uint1 x270; 492 fiat_p256_addcarryx_u32(&x269, &x270, x268, x245, x248); 493 uint32_t x271; 494 fiat_p256_uint1 x272; 495 fiat_p256_addcarryx_u32(&x271, &x272, x270, x243, x246); 496 uint32_t x273; 497 fiat_p256_uint1 x274; 498 fiat_p256_addcarryx_u32(&x273, &x274, x272, 0x0, x244); 499 uint32_t x275; 500 fiat_p256_uint1 x276; 501 fiat_p256_addcarryx_u32(&x275, &x276, 0x0, x257, x225); 502 uint32_t x277; 503 fiat_p256_uint1 x278; 504 fiat_p256_addcarryx_u32(&x277, &x278, x276, x259, x227); 505 uint32_t x279; 506 fiat_p256_uint1 x280; 507 fiat_p256_addcarryx_u32(&x279, &x280, x278, x261, x229); 508 uint32_t x281; 509 fiat_p256_uint1 x282; 510 fiat_p256_addcarryx_u32(&x281, &x282, x280, x263, x231); 511 uint32_t x283; 512 fiat_p256_uint1 x284; 513 fiat_p256_addcarryx_u32(&x283, &x284, x282, x265, x233); 514 uint32_t x285; 515 fiat_p256_uint1 x286; 516 fiat_p256_addcarryx_u32(&x285, &x286, x284, x267, x235); 517 uint32_t x287; 518 fiat_p256_uint1 x288; 519 fiat_p256_addcarryx_u32(&x287, &x288, x286, x269, x237); 520 uint32_t x289; 521 fiat_p256_uint1 x290; 522 fiat_p256_addcarryx_u32(&x289, &x290, x288, x271, x239); 523 uint32_t x291; 524 fiat_p256_uint1 x292; 525 fiat_p256_addcarryx_u32(&x291, &x292, x290, x273, x241); 526 uint32_t x293; 527 uint32_t x294; 528 fiat_p256_mulx_u32(&x293, &x294, x275, UINT32_C(0xffffffff)); 529 uint32_t x295; 530 uint32_t x296; 531 fiat_p256_mulx_u32(&x295, &x296, x275, UINT32_C(0xffffffff)); 532 uint32_t x297; 533 uint32_t x298; 534 fiat_p256_mulx_u32(&x297, &x298, x275, UINT32_C(0xffffffff)); 535 uint32_t x299; 536 uint32_t x300; 537 fiat_p256_mulx_u32(&x299, &x300, x275, UINT32_C(0xffffffff)); 538 uint32_t x301; 539 fiat_p256_uint1 x302; 540 fiat_p256_addcarryx_u32(&x301, &x302, 0x0, x297, x300); 541 uint32_t x303; 542 fiat_p256_uint1 x304; 543 fiat_p256_addcarryx_u32(&x303, &x304, x302, x295, x298); 544 uint32_t x305; 545 fiat_p256_uint1 x306; 546 fiat_p256_addcarryx_u32(&x305, &x306, x304, 0x0, x296); 547 uint32_t x307; 548 fiat_p256_uint1 x308; 549 fiat_p256_addcarryx_u32(&x307, &x308, 0x0, x299, x275); 550 uint32_t x309; 551 fiat_p256_uint1 x310; 552 fiat_p256_addcarryx_u32(&x309, &x310, x308, x301, x277); 553 uint32_t x311; 554 fiat_p256_uint1 x312; 555 fiat_p256_addcarryx_u32(&x311, &x312, x310, x303, x279); 556 uint32_t x313; 557 fiat_p256_uint1 x314; 558 fiat_p256_addcarryx_u32(&x313, &x314, x312, x305, x281); 559 uint32_t x315; 560 fiat_p256_uint1 x316; 561 fiat_p256_addcarryx_u32(&x315, &x316, x314, 0x0, x283); 562 uint32_t x317; 563 fiat_p256_uint1 x318; 564 fiat_p256_addcarryx_u32(&x317, &x318, x316, 0x0, x285); 565 uint32_t x319; 566 fiat_p256_uint1 x320; 567 fiat_p256_addcarryx_u32(&x319, &x320, x318, x275, x287); 568 uint32_t x321; 569 fiat_p256_uint1 x322; 570 fiat_p256_addcarryx_u32(&x321, &x322, x320, x293, x289); 571 uint32_t x323; 572 fiat_p256_uint1 x324; 573 fiat_p256_addcarryx_u32(&x323, &x324, x322, x294, x291); 574 uint32_t x325; 575 fiat_p256_uint1 x326; 576 fiat_p256_addcarryx_u32(&x325, &x326, x324, 0x0, x292); 577 uint32_t x327; 578 uint32_t x328; 579 fiat_p256_mulx_u32(&x327, &x328, x4, (arg2[7])); 580 uint32_t x329; 581 uint32_t x330; 582 fiat_p256_mulx_u32(&x329, &x330, x4, (arg2[6])); 583 uint32_t x331; 584 uint32_t x332; 585 fiat_p256_mulx_u32(&x331, &x332, x4, (arg2[5])); 586 uint32_t x333; 587 uint32_t x334; 588 fiat_p256_mulx_u32(&x333, &x334, x4, (arg2[4])); 589 uint32_t x335; 590 uint32_t x336; 591 fiat_p256_mulx_u32(&x335, &x336, x4, (arg2[3])); 592 uint32_t x337; 593 uint32_t x338; 594 fiat_p256_mulx_u32(&x337, &x338, x4, (arg2[2])); 595 uint32_t x339; 596 uint32_t x340; 597 fiat_p256_mulx_u32(&x339, &x340, x4, (arg2[1])); 598 uint32_t x341; 599 uint32_t x342; 600 fiat_p256_mulx_u32(&x341, &x342, x4, (arg2[0])); 601 uint32_t x343; 602 fiat_p256_uint1 x344; 603 fiat_p256_addcarryx_u32(&x343, &x344, 0x0, x339, x342); 604 uint32_t x345; 605 fiat_p256_uint1 x346; 606 fiat_p256_addcarryx_u32(&x345, &x346, x344, x337, x340); 607 uint32_t x347; 608 fiat_p256_uint1 x348; 609 fiat_p256_addcarryx_u32(&x347, &x348, x346, x335, x338); 610 uint32_t x349; 611 fiat_p256_uint1 x350; 612 fiat_p256_addcarryx_u32(&x349, &x350, x348, x333, x336); 613 uint32_t x351; 614 fiat_p256_uint1 x352; 615 fiat_p256_addcarryx_u32(&x351, &x352, x350, x331, x334); 616 uint32_t x353; 617 fiat_p256_uint1 x354; 618 fiat_p256_addcarryx_u32(&x353, &x354, x352, x329, x332); 619 uint32_t x355; 620 fiat_p256_uint1 x356; 621 fiat_p256_addcarryx_u32(&x355, &x356, x354, x327, x330); 622 uint32_t x357; 623 fiat_p256_uint1 x358; 624 fiat_p256_addcarryx_u32(&x357, &x358, x356, 0x0, x328); 625 uint32_t x359; 626 fiat_p256_uint1 x360; 627 fiat_p256_addcarryx_u32(&x359, &x360, 0x0, x341, x309); 628 uint32_t x361; 629 fiat_p256_uint1 x362; 630 fiat_p256_addcarryx_u32(&x361, &x362, x360, x343, x311); 631 uint32_t x363; 632 fiat_p256_uint1 x364; 633 fiat_p256_addcarryx_u32(&x363, &x364, x362, x345, x313); 634 uint32_t x365; 635 fiat_p256_uint1 x366; 636 fiat_p256_addcarryx_u32(&x365, &x366, x364, x347, x315); 637 uint32_t x367; 638 fiat_p256_uint1 x368; 639 fiat_p256_addcarryx_u32(&x367, &x368, x366, x349, x317); 640 uint32_t x369; 641 fiat_p256_uint1 x370; 642 fiat_p256_addcarryx_u32(&x369, &x370, x368, x351, x319); 643 uint32_t x371; 644 fiat_p256_uint1 x372; 645 fiat_p256_addcarryx_u32(&x371, &x372, x370, x353, x321); 646 uint32_t x373; 647 fiat_p256_uint1 x374; 648 fiat_p256_addcarryx_u32(&x373, &x374, x372, x355, x323); 649 uint32_t x375; 650 fiat_p256_uint1 x376; 651 fiat_p256_addcarryx_u32(&x375, &x376, x374, x357, x325); 652 uint32_t x377; 653 uint32_t x378; 654 fiat_p256_mulx_u32(&x377, &x378, x359, UINT32_C(0xffffffff)); 655 uint32_t x379; 656 uint32_t x380; 657 fiat_p256_mulx_u32(&x379, &x380, x359, UINT32_C(0xffffffff)); 658 uint32_t x381; 659 uint32_t x382; 660 fiat_p256_mulx_u32(&x381, &x382, x359, UINT32_C(0xffffffff)); 661 uint32_t x383; 662 uint32_t x384; 663 fiat_p256_mulx_u32(&x383, &x384, x359, UINT32_C(0xffffffff)); 664 uint32_t x385; 665 fiat_p256_uint1 x386; 666 fiat_p256_addcarryx_u32(&x385, &x386, 0x0, x381, x384); 667 uint32_t x387; 668 fiat_p256_uint1 x388; 669 fiat_p256_addcarryx_u32(&x387, &x388, x386, x379, x382); 670 uint32_t x389; 671 fiat_p256_uint1 x390; 672 fiat_p256_addcarryx_u32(&x389, &x390, x388, 0x0, x380); 673 uint32_t x391; 674 fiat_p256_uint1 x392; 675 fiat_p256_addcarryx_u32(&x391, &x392, 0x0, x383, x359); 676 uint32_t x393; 677 fiat_p256_uint1 x394; 678 fiat_p256_addcarryx_u32(&x393, &x394, x392, x385, x361); 679 uint32_t x395; 680 fiat_p256_uint1 x396; 681 fiat_p256_addcarryx_u32(&x395, &x396, x394, x387, x363); 682 uint32_t x397; 683 fiat_p256_uint1 x398; 684 fiat_p256_addcarryx_u32(&x397, &x398, x396, x389, x365); 685 uint32_t x399; 686 fiat_p256_uint1 x400; 687 fiat_p256_addcarryx_u32(&x399, &x400, x398, 0x0, x367); 688 uint32_t x401; 689 fiat_p256_uint1 x402; 690 fiat_p256_addcarryx_u32(&x401, &x402, x400, 0x0, x369); 691 uint32_t x403; 692 fiat_p256_uint1 x404; 693 fiat_p256_addcarryx_u32(&x403, &x404, x402, x359, x371); 694 uint32_t x405; 695 fiat_p256_uint1 x406; 696 fiat_p256_addcarryx_u32(&x405, &x406, x404, x377, x373); 697 uint32_t x407; 698 fiat_p256_uint1 x408; 699 fiat_p256_addcarryx_u32(&x407, &x408, x406, x378, x375); 700 uint32_t x409; 701 fiat_p256_uint1 x410; 702 fiat_p256_addcarryx_u32(&x409, &x410, x408, 0x0, x376); 703 uint32_t x411; 704 uint32_t x412; 705 fiat_p256_mulx_u32(&x411, &x412, x5, (arg2[7])); 706 uint32_t x413; 707 uint32_t x414; 708 fiat_p256_mulx_u32(&x413, &x414, x5, (arg2[6])); 709 uint32_t x415; 710 uint32_t x416; 711 fiat_p256_mulx_u32(&x415, &x416, x5, (arg2[5])); 712 uint32_t x417; 713 uint32_t x418; 714 fiat_p256_mulx_u32(&x417, &x418, x5, (arg2[4])); 715 uint32_t x419; 716 uint32_t x420; 717 fiat_p256_mulx_u32(&x419, &x420, x5, (arg2[3])); 718 uint32_t x421; 719 uint32_t x422; 720 fiat_p256_mulx_u32(&x421, &x422, x5, (arg2[2])); 721 uint32_t x423; 722 uint32_t x424; 723 fiat_p256_mulx_u32(&x423, &x424, x5, (arg2[1])); 724 uint32_t x425; 725 uint32_t x426; 726 fiat_p256_mulx_u32(&x425, &x426, x5, (arg2[0])); 727 uint32_t x427; 728 fiat_p256_uint1 x428; 729 fiat_p256_addcarryx_u32(&x427, &x428, 0x0, x423, x426); 730 uint32_t x429; 731 fiat_p256_uint1 x430; 732 fiat_p256_addcarryx_u32(&x429, &x430, x428, x421, x424); 733 uint32_t x431; 734 fiat_p256_uint1 x432; 735 fiat_p256_addcarryx_u32(&x431, &x432, x430, x419, x422); 736 uint32_t x433; 737 fiat_p256_uint1 x434; 738 fiat_p256_addcarryx_u32(&x433, &x434, x432, x417, x420); 739 uint32_t x435; 740 fiat_p256_uint1 x436; 741 fiat_p256_addcarryx_u32(&x435, &x436, x434, x415, x418); 742 uint32_t x437; 743 fiat_p256_uint1 x438; 744 fiat_p256_addcarryx_u32(&x437, &x438, x436, x413, x416); 745 uint32_t x439; 746 fiat_p256_uint1 x440; 747 fiat_p256_addcarryx_u32(&x439, &x440, x438, x411, x414); 748 uint32_t x441; 749 fiat_p256_uint1 x442; 750 fiat_p256_addcarryx_u32(&x441, &x442, x440, 0x0, x412); 751 uint32_t x443; 752 fiat_p256_uint1 x444; 753 fiat_p256_addcarryx_u32(&x443, &x444, 0x0, x425, x393); 754 uint32_t x445; 755 fiat_p256_uint1 x446; 756 fiat_p256_addcarryx_u32(&x445, &x446, x444, x427, x395); 757 uint32_t x447; 758 fiat_p256_uint1 x448; 759 fiat_p256_addcarryx_u32(&x447, &x448, x446, x429, x397); 760 uint32_t x449; 761 fiat_p256_uint1 x450; 762 fiat_p256_addcarryx_u32(&x449, &x450, x448, x431, x399); 763 uint32_t x451; 764 fiat_p256_uint1 x452; 765 fiat_p256_addcarryx_u32(&x451, &x452, x450, x433, x401); 766 uint32_t x453; 767 fiat_p256_uint1 x454; 768 fiat_p256_addcarryx_u32(&x453, &x454, x452, x435, x403); 769 uint32_t x455; 770 fiat_p256_uint1 x456; 771 fiat_p256_addcarryx_u32(&x455, &x456, x454, x437, x405); 772 uint32_t x457; 773 fiat_p256_uint1 x458; 774 fiat_p256_addcarryx_u32(&x457, &x458, x456, x439, x407); 775 uint32_t x459; 776 fiat_p256_uint1 x460; 777 fiat_p256_addcarryx_u32(&x459, &x460, x458, x441, x409); 778 uint32_t x461; 779 uint32_t x462; 780 fiat_p256_mulx_u32(&x461, &x462, x443, UINT32_C(0xffffffff)); 781 uint32_t x463; 782 uint32_t x464; 783 fiat_p256_mulx_u32(&x463, &x464, x443, UINT32_C(0xffffffff)); 784 uint32_t x465; 785 uint32_t x466; 786 fiat_p256_mulx_u32(&x465, &x466, x443, UINT32_C(0xffffffff)); 787 uint32_t x467; 788 uint32_t x468; 789 fiat_p256_mulx_u32(&x467, &x468, x443, UINT32_C(0xffffffff)); 790 uint32_t x469; 791 fiat_p256_uint1 x470; 792 fiat_p256_addcarryx_u32(&x469, &x470, 0x0, x465, x468); 793 uint32_t x471; 794 fiat_p256_uint1 x472; 795 fiat_p256_addcarryx_u32(&x471, &x472, x470, x463, x466); 796 uint32_t x473; 797 fiat_p256_uint1 x474; 798 fiat_p256_addcarryx_u32(&x473, &x474, x472, 0x0, x464); 799 uint32_t x475; 800 fiat_p256_uint1 x476; 801 fiat_p256_addcarryx_u32(&x475, &x476, 0x0, x467, x443); 802 uint32_t x477; 803 fiat_p256_uint1 x478; 804 fiat_p256_addcarryx_u32(&x477, &x478, x476, x469, x445); 805 uint32_t x479; 806 fiat_p256_uint1 x480; 807 fiat_p256_addcarryx_u32(&x479, &x480, x478, x471, x447); 808 uint32_t x481; 809 fiat_p256_uint1 x482; 810 fiat_p256_addcarryx_u32(&x481, &x482, x480, x473, x449); 811 uint32_t x483; 812 fiat_p256_uint1 x484; 813 fiat_p256_addcarryx_u32(&x483, &x484, x482, 0x0, x451); 814 uint32_t x485; 815 fiat_p256_uint1 x486; 816 fiat_p256_addcarryx_u32(&x485, &x486, x484, 0x0, x453); 817 uint32_t x487; 818 fiat_p256_uint1 x488; 819 fiat_p256_addcarryx_u32(&x487, &x488, x486, x443, x455); 820 uint32_t x489; 821 fiat_p256_uint1 x490; 822 fiat_p256_addcarryx_u32(&x489, &x490, x488, x461, x457); 823 uint32_t x491; 824 fiat_p256_uint1 x492; 825 fiat_p256_addcarryx_u32(&x491, &x492, x490, x462, x459); 826 uint32_t x493; 827 fiat_p256_uint1 x494; 828 fiat_p256_addcarryx_u32(&x493, &x494, x492, 0x0, x460); 829 uint32_t x495; 830 uint32_t x496; 831 fiat_p256_mulx_u32(&x495, &x496, x6, (arg2[7])); 832 uint32_t x497; 833 uint32_t x498; 834 fiat_p256_mulx_u32(&x497, &x498, x6, (arg2[6])); 835 uint32_t x499; 836 uint32_t x500; 837 fiat_p256_mulx_u32(&x499, &x500, x6, (arg2[5])); 838 uint32_t x501; 839 uint32_t x502; 840 fiat_p256_mulx_u32(&x501, &x502, x6, (arg2[4])); 841 uint32_t x503; 842 uint32_t x504; 843 fiat_p256_mulx_u32(&x503, &x504, x6, (arg2[3])); 844 uint32_t x505; 845 uint32_t x506; 846 fiat_p256_mulx_u32(&x505, &x506, x6, (arg2[2])); 847 uint32_t x507; 848 uint32_t x508; 849 fiat_p256_mulx_u32(&x507, &x508, x6, (arg2[1])); 850 uint32_t x509; 851 uint32_t x510; 852 fiat_p256_mulx_u32(&x509, &x510, x6, (arg2[0])); 853 uint32_t x511; 854 fiat_p256_uint1 x512; 855 fiat_p256_addcarryx_u32(&x511, &x512, 0x0, x507, x510); 856 uint32_t x513; 857 fiat_p256_uint1 x514; 858 fiat_p256_addcarryx_u32(&x513, &x514, x512, x505, x508); 859 uint32_t x515; 860 fiat_p256_uint1 x516; 861 fiat_p256_addcarryx_u32(&x515, &x516, x514, x503, x506); 862 uint32_t x517; 863 fiat_p256_uint1 x518; 864 fiat_p256_addcarryx_u32(&x517, &x518, x516, x501, x504); 865 uint32_t x519; 866 fiat_p256_uint1 x520; 867 fiat_p256_addcarryx_u32(&x519, &x520, x518, x499, x502); 868 uint32_t x521; 869 fiat_p256_uint1 x522; 870 fiat_p256_addcarryx_u32(&x521, &x522, x520, x497, x500); 871 uint32_t x523; 872 fiat_p256_uint1 x524; 873 fiat_p256_addcarryx_u32(&x523, &x524, x522, x495, x498); 874 uint32_t x525; 875 fiat_p256_uint1 x526; 876 fiat_p256_addcarryx_u32(&x525, &x526, x524, 0x0, x496); 877 uint32_t x527; 878 fiat_p256_uint1 x528; 879 fiat_p256_addcarryx_u32(&x527, &x528, 0x0, x509, x477); 880 uint32_t x529; 881 fiat_p256_uint1 x530; 882 fiat_p256_addcarryx_u32(&x529, &x530, x528, x511, x479); 883 uint32_t x531; 884 fiat_p256_uint1 x532; 885 fiat_p256_addcarryx_u32(&x531, &x532, x530, x513, x481); 886 uint32_t x533; 887 fiat_p256_uint1 x534; 888 fiat_p256_addcarryx_u32(&x533, &x534, x532, x515, x483); 889 uint32_t x535; 890 fiat_p256_uint1 x536; 891 fiat_p256_addcarryx_u32(&x535, &x536, x534, x517, x485); 892 uint32_t x537; 893 fiat_p256_uint1 x538; 894 fiat_p256_addcarryx_u32(&x537, &x538, x536, x519, x487); 895 uint32_t x539; 896 fiat_p256_uint1 x540; 897 fiat_p256_addcarryx_u32(&x539, &x540, x538, x521, x489); 898 uint32_t x541; 899 fiat_p256_uint1 x542; 900 fiat_p256_addcarryx_u32(&x541, &x542, x540, x523, x491); 901 uint32_t x543; 902 fiat_p256_uint1 x544; 903 fiat_p256_addcarryx_u32(&x543, &x544, x542, x525, x493); 904 uint32_t x545; 905 uint32_t x546; 906 fiat_p256_mulx_u32(&x545, &x546, x527, UINT32_C(0xffffffff)); 907 uint32_t x547; 908 uint32_t x548; 909 fiat_p256_mulx_u32(&x547, &x548, x527, UINT32_C(0xffffffff)); 910 uint32_t x549; 911 uint32_t x550; 912 fiat_p256_mulx_u32(&x549, &x550, x527, UINT32_C(0xffffffff)); 913 uint32_t x551; 914 uint32_t x552; 915 fiat_p256_mulx_u32(&x551, &x552, x527, UINT32_C(0xffffffff)); 916 uint32_t x553; 917 fiat_p256_uint1 x554; 918 fiat_p256_addcarryx_u32(&x553, &x554, 0x0, x549, x552); 919 uint32_t x555; 920 fiat_p256_uint1 x556; 921 fiat_p256_addcarryx_u32(&x555, &x556, x554, x547, x550); 922 uint32_t x557; 923 fiat_p256_uint1 x558; 924 fiat_p256_addcarryx_u32(&x557, &x558, x556, 0x0, x548); 925 uint32_t x559; 926 fiat_p256_uint1 x560; 927 fiat_p256_addcarryx_u32(&x559, &x560, 0x0, x551, x527); 928 uint32_t x561; 929 fiat_p256_uint1 x562; 930 fiat_p256_addcarryx_u32(&x561, &x562, x560, x553, x529); 931 uint32_t x563; 932 fiat_p256_uint1 x564; 933 fiat_p256_addcarryx_u32(&x563, &x564, x562, x555, x531); 934 uint32_t x565; 935 fiat_p256_uint1 x566; 936 fiat_p256_addcarryx_u32(&x565, &x566, x564, x557, x533); 937 uint32_t x567; 938 fiat_p256_uint1 x568; 939 fiat_p256_addcarryx_u32(&x567, &x568, x566, 0x0, x535); 940 uint32_t x569; 941 fiat_p256_uint1 x570; 942 fiat_p256_addcarryx_u32(&x569, &x570, x568, 0x0, x537); 943 uint32_t x571; 944 fiat_p256_uint1 x572; 945 fiat_p256_addcarryx_u32(&x571, &x572, x570, x527, x539); 946 uint32_t x573; 947 fiat_p256_uint1 x574; 948 fiat_p256_addcarryx_u32(&x573, &x574, x572, x545, x541); 949 uint32_t x575; 950 fiat_p256_uint1 x576; 951 fiat_p256_addcarryx_u32(&x575, &x576, x574, x546, x543); 952 uint32_t x577; 953 fiat_p256_uint1 x578; 954 fiat_p256_addcarryx_u32(&x577, &x578, x576, 0x0, x544); 955 uint32_t x579; 956 uint32_t x580; 957 fiat_p256_mulx_u32(&x579, &x580, x7, (arg2[7])); 958 uint32_t x581; 959 uint32_t x582; 960 fiat_p256_mulx_u32(&x581, &x582, x7, (arg2[6])); 961 uint32_t x583; 962 uint32_t x584; 963 fiat_p256_mulx_u32(&x583, &x584, x7, (arg2[5])); 964 uint32_t x585; 965 uint32_t x586; 966 fiat_p256_mulx_u32(&x585, &x586, x7, (arg2[4])); 967 uint32_t x587; 968 uint32_t x588; 969 fiat_p256_mulx_u32(&x587, &x588, x7, (arg2[3])); 970 uint32_t x589; 971 uint32_t x590; 972 fiat_p256_mulx_u32(&x589, &x590, x7, (arg2[2])); 973 uint32_t x591; 974 uint32_t x592; 975 fiat_p256_mulx_u32(&x591, &x592, x7, (arg2[1])); 976 uint32_t x593; 977 uint32_t x594; 978 fiat_p256_mulx_u32(&x593, &x594, x7, (arg2[0])); 979 uint32_t x595; 980 fiat_p256_uint1 x596; 981 fiat_p256_addcarryx_u32(&x595, &x596, 0x0, x591, x594); 982 uint32_t x597; 983 fiat_p256_uint1 x598; 984 fiat_p256_addcarryx_u32(&x597, &x598, x596, x589, x592); 985 uint32_t x599; 986 fiat_p256_uint1 x600; 987 fiat_p256_addcarryx_u32(&x599, &x600, x598, x587, x590); 988 uint32_t x601; 989 fiat_p256_uint1 x602; 990 fiat_p256_addcarryx_u32(&x601, &x602, x600, x585, x588); 991 uint32_t x603; 992 fiat_p256_uint1 x604; 993 fiat_p256_addcarryx_u32(&x603, &x604, x602, x583, x586); 994 uint32_t x605; 995 fiat_p256_uint1 x606; 996 fiat_p256_addcarryx_u32(&x605, &x606, x604, x581, x584); 997 uint32_t x607; 998 fiat_p256_uint1 x608; 999 fiat_p256_addcarryx_u32(&x607, &x608, x606, x579, x582); 1000 uint32_t x609; 1001 fiat_p256_uint1 x610; 1002 fiat_p256_addcarryx_u32(&x609, &x610, x608, 0x0, x580); 1003 uint32_t x611; 1004 fiat_p256_uint1 x612; 1005 fiat_p256_addcarryx_u32(&x611, &x612, 0x0, x593, x561); 1006 uint32_t x613; 1007 fiat_p256_uint1 x614; 1008 fiat_p256_addcarryx_u32(&x613, &x614, x612, x595, x563); 1009 uint32_t x615; 1010 fiat_p256_uint1 x616; 1011 fiat_p256_addcarryx_u32(&x615, &x616, x614, x597, x565); 1012 uint32_t x617; 1013 fiat_p256_uint1 x618; 1014 fiat_p256_addcarryx_u32(&x617, &x618, x616, x599, x567); 1015 uint32_t x619; 1016 fiat_p256_uint1 x620; 1017 fiat_p256_addcarryx_u32(&x619, &x620, x618, x601, x569); 1018 uint32_t x621; 1019 fiat_p256_uint1 x622; 1020 fiat_p256_addcarryx_u32(&x621, &x622, x620, x603, x571); 1021 uint32_t x623; 1022 fiat_p256_uint1 x624; 1023 fiat_p256_addcarryx_u32(&x623, &x624, x622, x605, x573); 1024 uint32_t x625; 1025 fiat_p256_uint1 x626; 1026 fiat_p256_addcarryx_u32(&x625, &x626, x624, x607, x575); 1027 uint32_t x627; 1028 fiat_p256_uint1 x628; 1029 fiat_p256_addcarryx_u32(&x627, &x628, x626, x609, x577); 1030 uint32_t x629; 1031 uint32_t x630; 1032 fiat_p256_mulx_u32(&x629, &x630, x611, UINT32_C(0xffffffff)); 1033 uint32_t x631; 1034 uint32_t x632; 1035 fiat_p256_mulx_u32(&x631, &x632, x611, UINT32_C(0xffffffff)); 1036 uint32_t x633; 1037 uint32_t x634; 1038 fiat_p256_mulx_u32(&x633, &x634, x611, UINT32_C(0xffffffff)); 1039 uint32_t x635; 1040 uint32_t x636; 1041 fiat_p256_mulx_u32(&x635, &x636, x611, UINT32_C(0xffffffff)); 1042 uint32_t x637; 1043 fiat_p256_uint1 x638; 1044 fiat_p256_addcarryx_u32(&x637, &x638, 0x0, x633, x636); 1045 uint32_t x639; 1046 fiat_p256_uint1 x640; 1047 fiat_p256_addcarryx_u32(&x639, &x640, x638, x631, x634); 1048 uint32_t x641; 1049 fiat_p256_uint1 x642; 1050 fiat_p256_addcarryx_u32(&x641, &x642, x640, 0x0, x632); 1051 uint32_t x643; 1052 fiat_p256_uint1 x644; 1053 fiat_p256_addcarryx_u32(&x643, &x644, 0x0, x635, x611); 1054 uint32_t x645; 1055 fiat_p256_uint1 x646; 1056 fiat_p256_addcarryx_u32(&x645, &x646, x644, x637, x613); 1057 uint32_t x647; 1058 fiat_p256_uint1 x648; 1059 fiat_p256_addcarryx_u32(&x647, &x648, x646, x639, x615); 1060 uint32_t x649; 1061 fiat_p256_uint1 x650; 1062 fiat_p256_addcarryx_u32(&x649, &x650, x648, x641, x617); 1063 uint32_t x651; 1064 fiat_p256_uint1 x652; 1065 fiat_p256_addcarryx_u32(&x651, &x652, x650, 0x0, x619); 1066 uint32_t x653; 1067 fiat_p256_uint1 x654; 1068 fiat_p256_addcarryx_u32(&x653, &x654, x652, 0x0, x621); 1069 uint32_t x655; 1070 fiat_p256_uint1 x656; 1071 fiat_p256_addcarryx_u32(&x655, &x656, x654, x611, x623); 1072 uint32_t x657; 1073 fiat_p256_uint1 x658; 1074 fiat_p256_addcarryx_u32(&x657, &x658, x656, x629, x625); 1075 uint32_t x659; 1076 fiat_p256_uint1 x660; 1077 fiat_p256_addcarryx_u32(&x659, &x660, x658, x630, x627); 1078 uint32_t x661; 1079 fiat_p256_uint1 x662; 1080 fiat_p256_addcarryx_u32(&x661, &x662, x660, 0x0, x628); 1081 uint32_t x663; 1082 fiat_p256_uint1 x664; 1083 fiat_p256_subborrowx_u32(&x663, &x664, 0x0, x645, UINT32_C(0xffffffff)); 1084 uint32_t x665; 1085 fiat_p256_uint1 x666; 1086 fiat_p256_subborrowx_u32(&x665, &x666, x664, x647, UINT32_C(0xffffffff)); 1087 uint32_t x667; 1088 fiat_p256_uint1 x668; 1089 fiat_p256_subborrowx_u32(&x667, &x668, x666, x649, UINT32_C(0xffffffff)); 1090 uint32_t x669; 1091 fiat_p256_uint1 x670; 1092 fiat_p256_subborrowx_u32(&x669, &x670, x668, x651, 0x0); 1093 uint32_t x671; 1094 fiat_p256_uint1 x672; 1095 fiat_p256_subborrowx_u32(&x671, &x672, x670, x653, 0x0); 1096 uint32_t x673; 1097 fiat_p256_uint1 x674; 1098 fiat_p256_subborrowx_u32(&x673, &x674, x672, x655, 0x0); 1099 uint32_t x675; 1100 fiat_p256_uint1 x676; 1101 fiat_p256_subborrowx_u32(&x675, &x676, x674, x657, 0x1); 1102 uint32_t x677; 1103 fiat_p256_uint1 x678; 1104 fiat_p256_subborrowx_u32(&x677, &x678, x676, x659, UINT32_C(0xffffffff)); 1105 uint32_t x679; 1106 fiat_p256_uint1 x680; 1107 fiat_p256_subborrowx_u32(&x679, &x680, x678, x661, 0x0); 1108 uint32_t x681; 1109 fiat_p256_cmovznz_u32(&x681, x680, x663, x645); 1110 uint32_t x682; 1111 fiat_p256_cmovznz_u32(&x682, x680, x665, x647); 1112 uint32_t x683; 1113 fiat_p256_cmovznz_u32(&x683, x680, x667, x649); 1114 uint32_t x684; 1115 fiat_p256_cmovznz_u32(&x684, x680, x669, x651); 1116 uint32_t x685; 1117 fiat_p256_cmovznz_u32(&x685, x680, x671, x653); 1118 uint32_t x686; 1119 fiat_p256_cmovznz_u32(&x686, x680, x673, x655); 1120 uint32_t x687; 1121 fiat_p256_cmovznz_u32(&x687, x680, x675, x657); 1122 uint32_t x688; 1123 fiat_p256_cmovznz_u32(&x688, x680, x677, x659); 1124 out1[0] = x681; 1125 out1[1] = x682; 1126 out1[2] = x683; 1127 out1[3] = x684; 1128 out1[4] = x685; 1129 out1[5] = x686; 1130 out1[6] = x687; 1131 out1[7] = x688; 1132 } 1133 1134 /* 1135 * Input Bounds: 1136 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 1137 * Output Bounds: 1138 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 1139 */ 1140 static void fiat_p256_square(uint32_t out1[8], const uint32_t arg1[8]) { 1141 uint32_t x1 = (arg1[1]); 1142 uint32_t x2 = (arg1[2]); 1143 uint32_t x3 = (arg1[3]); 1144 uint32_t x4 = (arg1[4]); 1145 uint32_t x5 = (arg1[5]); 1146 uint32_t x6 = (arg1[6]); 1147 uint32_t x7 = (arg1[7]); 1148 uint32_t x8 = (arg1[0]); 1149 uint32_t x9; 1150 uint32_t x10; 1151 fiat_p256_mulx_u32(&x9, &x10, x8, (arg1[7])); 1152 uint32_t x11; 1153 uint32_t x12; 1154 fiat_p256_mulx_u32(&x11, &x12, x8, (arg1[6])); 1155 uint32_t x13; 1156 uint32_t x14; 1157 fiat_p256_mulx_u32(&x13, &x14, x8, (arg1[5])); 1158 uint32_t x15; 1159 uint32_t x16; 1160 fiat_p256_mulx_u32(&x15, &x16, x8, (arg1[4])); 1161 uint32_t x17; 1162 uint32_t x18; 1163 fiat_p256_mulx_u32(&x17, &x18, x8, (arg1[3])); 1164 uint32_t x19; 1165 uint32_t x20; 1166 fiat_p256_mulx_u32(&x19, &x20, x8, (arg1[2])); 1167 uint32_t x21; 1168 uint32_t x22; 1169 fiat_p256_mulx_u32(&x21, &x22, x8, (arg1[1])); 1170 uint32_t x23; 1171 uint32_t x24; 1172 fiat_p256_mulx_u32(&x23, &x24, x8, (arg1[0])); 1173 uint32_t x25; 1174 fiat_p256_uint1 x26; 1175 fiat_p256_addcarryx_u32(&x25, &x26, 0x0, x21, x24); 1176 uint32_t x27; 1177 fiat_p256_uint1 x28; 1178 fiat_p256_addcarryx_u32(&x27, &x28, x26, x19, x22); 1179 uint32_t x29; 1180 fiat_p256_uint1 x30; 1181 fiat_p256_addcarryx_u32(&x29, &x30, x28, x17, x20); 1182 uint32_t x31; 1183 fiat_p256_uint1 x32; 1184 fiat_p256_addcarryx_u32(&x31, &x32, x30, x15, x18); 1185 uint32_t x33; 1186 fiat_p256_uint1 x34; 1187 fiat_p256_addcarryx_u32(&x33, &x34, x32, x13, x16); 1188 uint32_t x35; 1189 fiat_p256_uint1 x36; 1190 fiat_p256_addcarryx_u32(&x35, &x36, x34, x11, x14); 1191 uint32_t x37; 1192 fiat_p256_uint1 x38; 1193 fiat_p256_addcarryx_u32(&x37, &x38, x36, x9, x12); 1194 uint32_t x39; 1195 fiat_p256_uint1 x40; 1196 fiat_p256_addcarryx_u32(&x39, &x40, x38, 0x0, x10); 1197 uint32_t x41; 1198 uint32_t x42; 1199 fiat_p256_mulx_u32(&x41, &x42, x23, UINT32_C(0xffffffff)); 1200 uint32_t x43; 1201 uint32_t x44; 1202 fiat_p256_mulx_u32(&x43, &x44, x23, UINT32_C(0xffffffff)); 1203 uint32_t x45; 1204 uint32_t x46; 1205 fiat_p256_mulx_u32(&x45, &x46, x23, UINT32_C(0xffffffff)); 1206 uint32_t x47; 1207 uint32_t x48; 1208 fiat_p256_mulx_u32(&x47, &x48, x23, UINT32_C(0xffffffff)); 1209 uint32_t x49; 1210 fiat_p256_uint1 x50; 1211 fiat_p256_addcarryx_u32(&x49, &x50, 0x0, x45, x48); 1212 uint32_t x51; 1213 fiat_p256_uint1 x52; 1214 fiat_p256_addcarryx_u32(&x51, &x52, x50, x43, x46); 1215 uint32_t x53; 1216 fiat_p256_uint1 x54; 1217 fiat_p256_addcarryx_u32(&x53, &x54, x52, 0x0, x44); 1218 uint32_t x55; 1219 fiat_p256_uint1 x56; 1220 fiat_p256_addcarryx_u32(&x55, &x56, 0x0, x47, x23); 1221 uint32_t x57; 1222 fiat_p256_uint1 x58; 1223 fiat_p256_addcarryx_u32(&x57, &x58, x56, x49, x25); 1224 uint32_t x59; 1225 fiat_p256_uint1 x60; 1226 fiat_p256_addcarryx_u32(&x59, &x60, x58, x51, x27); 1227 uint32_t x61; 1228 fiat_p256_uint1 x62; 1229 fiat_p256_addcarryx_u32(&x61, &x62, x60, x53, x29); 1230 uint32_t x63; 1231 fiat_p256_uint1 x64; 1232 fiat_p256_addcarryx_u32(&x63, &x64, x62, 0x0, x31); 1233 uint32_t x65; 1234 fiat_p256_uint1 x66; 1235 fiat_p256_addcarryx_u32(&x65, &x66, x64, 0x0, x33); 1236 uint32_t x67; 1237 fiat_p256_uint1 x68; 1238 fiat_p256_addcarryx_u32(&x67, &x68, x66, x23, x35); 1239 uint32_t x69; 1240 fiat_p256_uint1 x70; 1241 fiat_p256_addcarryx_u32(&x69, &x70, x68, x41, x37); 1242 uint32_t x71; 1243 fiat_p256_uint1 x72; 1244 fiat_p256_addcarryx_u32(&x71, &x72, x70, x42, x39); 1245 uint32_t x73; 1246 fiat_p256_uint1 x74; 1247 fiat_p256_addcarryx_u32(&x73, &x74, x72, 0x0, 0x0); 1248 uint32_t x75; 1249 uint32_t x76; 1250 fiat_p256_mulx_u32(&x75, &x76, x1, (arg1[7])); 1251 uint32_t x77; 1252 uint32_t x78; 1253 fiat_p256_mulx_u32(&x77, &x78, x1, (arg1[6])); 1254 uint32_t x79; 1255 uint32_t x80; 1256 fiat_p256_mulx_u32(&x79, &x80, x1, (arg1[5])); 1257 uint32_t x81; 1258 uint32_t x82; 1259 fiat_p256_mulx_u32(&x81, &x82, x1, (arg1[4])); 1260 uint32_t x83; 1261 uint32_t x84; 1262 fiat_p256_mulx_u32(&x83, &x84, x1, (arg1[3])); 1263 uint32_t x85; 1264 uint32_t x86; 1265 fiat_p256_mulx_u32(&x85, &x86, x1, (arg1[2])); 1266 uint32_t x87; 1267 uint32_t x88; 1268 fiat_p256_mulx_u32(&x87, &x88, x1, (arg1[1])); 1269 uint32_t x89; 1270 uint32_t x90; 1271 fiat_p256_mulx_u32(&x89, &x90, x1, (arg1[0])); 1272 uint32_t x91; 1273 fiat_p256_uint1 x92; 1274 fiat_p256_addcarryx_u32(&x91, &x92, 0x0, x87, x90); 1275 uint32_t x93; 1276 fiat_p256_uint1 x94; 1277 fiat_p256_addcarryx_u32(&x93, &x94, x92, x85, x88); 1278 uint32_t x95; 1279 fiat_p256_uint1 x96; 1280 fiat_p256_addcarryx_u32(&x95, &x96, x94, x83, x86); 1281 uint32_t x97; 1282 fiat_p256_uint1 x98; 1283 fiat_p256_addcarryx_u32(&x97, &x98, x96, x81, x84); 1284 uint32_t x99; 1285 fiat_p256_uint1 x100; 1286 fiat_p256_addcarryx_u32(&x99, &x100, x98, x79, x82); 1287 uint32_t x101; 1288 fiat_p256_uint1 x102; 1289 fiat_p256_addcarryx_u32(&x101, &x102, x100, x77, x80); 1290 uint32_t x103; 1291 fiat_p256_uint1 x104; 1292 fiat_p256_addcarryx_u32(&x103, &x104, x102, x75, x78); 1293 uint32_t x105; 1294 fiat_p256_uint1 x106; 1295 fiat_p256_addcarryx_u32(&x105, &x106, x104, 0x0, x76); 1296 uint32_t x107; 1297 fiat_p256_uint1 x108; 1298 fiat_p256_addcarryx_u32(&x107, &x108, 0x0, x89, x57); 1299 uint32_t x109; 1300 fiat_p256_uint1 x110; 1301 fiat_p256_addcarryx_u32(&x109, &x110, x108, x91, x59); 1302 uint32_t x111; 1303 fiat_p256_uint1 x112; 1304 fiat_p256_addcarryx_u32(&x111, &x112, x110, x93, x61); 1305 uint32_t x113; 1306 fiat_p256_uint1 x114; 1307 fiat_p256_addcarryx_u32(&x113, &x114, x112, x95, x63); 1308 uint32_t x115; 1309 fiat_p256_uint1 x116; 1310 fiat_p256_addcarryx_u32(&x115, &x116, x114, x97, x65); 1311 uint32_t x117; 1312 fiat_p256_uint1 x118; 1313 fiat_p256_addcarryx_u32(&x117, &x118, x116, x99, x67); 1314 uint32_t x119; 1315 fiat_p256_uint1 x120; 1316 fiat_p256_addcarryx_u32(&x119, &x120, x118, x101, x69); 1317 uint32_t x121; 1318 fiat_p256_uint1 x122; 1319 fiat_p256_addcarryx_u32(&x121, &x122, x120, x103, x71); 1320 uint32_t x123; 1321 fiat_p256_uint1 x124; 1322 fiat_p256_addcarryx_u32(&x123, &x124, x122, x105, (fiat_p256_uint1)x73); 1323 uint32_t x125; 1324 uint32_t x126; 1325 fiat_p256_mulx_u32(&x125, &x126, x107, UINT32_C(0xffffffff)); 1326 uint32_t x127; 1327 uint32_t x128; 1328 fiat_p256_mulx_u32(&x127, &x128, x107, UINT32_C(0xffffffff)); 1329 uint32_t x129; 1330 uint32_t x130; 1331 fiat_p256_mulx_u32(&x129, &x130, x107, UINT32_C(0xffffffff)); 1332 uint32_t x131; 1333 uint32_t x132; 1334 fiat_p256_mulx_u32(&x131, &x132, x107, UINT32_C(0xffffffff)); 1335 uint32_t x133; 1336 fiat_p256_uint1 x134; 1337 fiat_p256_addcarryx_u32(&x133, &x134, 0x0, x129, x132); 1338 uint32_t x135; 1339 fiat_p256_uint1 x136; 1340 fiat_p256_addcarryx_u32(&x135, &x136, x134, x127, x130); 1341 uint32_t x137; 1342 fiat_p256_uint1 x138; 1343 fiat_p256_addcarryx_u32(&x137, &x138, x136, 0x0, x128); 1344 uint32_t x139; 1345 fiat_p256_uint1 x140; 1346 fiat_p256_addcarryx_u32(&x139, &x140, 0x0, x131, x107); 1347 uint32_t x141; 1348 fiat_p256_uint1 x142; 1349 fiat_p256_addcarryx_u32(&x141, &x142, x140, x133, x109); 1350 uint32_t x143; 1351 fiat_p256_uint1 x144; 1352 fiat_p256_addcarryx_u32(&x143, &x144, x142, x135, x111); 1353 uint32_t x145; 1354 fiat_p256_uint1 x146; 1355 fiat_p256_addcarryx_u32(&x145, &x146, x144, x137, x113); 1356 uint32_t x147; 1357 fiat_p256_uint1 x148; 1358 fiat_p256_addcarryx_u32(&x147, &x148, x146, 0x0, x115); 1359 uint32_t x149; 1360 fiat_p256_uint1 x150; 1361 fiat_p256_addcarryx_u32(&x149, &x150, x148, 0x0, x117); 1362 uint32_t x151; 1363 fiat_p256_uint1 x152; 1364 fiat_p256_addcarryx_u32(&x151, &x152, x150, x107, x119); 1365 uint32_t x153; 1366 fiat_p256_uint1 x154; 1367 fiat_p256_addcarryx_u32(&x153, &x154, x152, x125, x121); 1368 uint32_t x155; 1369 fiat_p256_uint1 x156; 1370 fiat_p256_addcarryx_u32(&x155, &x156, x154, x126, x123); 1371 uint32_t x157; 1372 fiat_p256_uint1 x158; 1373 fiat_p256_addcarryx_u32(&x157, &x158, x156, 0x0, x124); 1374 uint32_t x159; 1375 uint32_t x160; 1376 fiat_p256_mulx_u32(&x159, &x160, x2, (arg1[7])); 1377 uint32_t x161; 1378 uint32_t x162; 1379 fiat_p256_mulx_u32(&x161, &x162, x2, (arg1[6])); 1380 uint32_t x163; 1381 uint32_t x164; 1382 fiat_p256_mulx_u32(&x163, &x164, x2, (arg1[5])); 1383 uint32_t x165; 1384 uint32_t x166; 1385 fiat_p256_mulx_u32(&x165, &x166, x2, (arg1[4])); 1386 uint32_t x167; 1387 uint32_t x168; 1388 fiat_p256_mulx_u32(&x167, &x168, x2, (arg1[3])); 1389 uint32_t x169; 1390 uint32_t x170; 1391 fiat_p256_mulx_u32(&x169, &x170, x2, (arg1[2])); 1392 uint32_t x171; 1393 uint32_t x172; 1394 fiat_p256_mulx_u32(&x171, &x172, x2, (arg1[1])); 1395 uint32_t x173; 1396 uint32_t x174; 1397 fiat_p256_mulx_u32(&x173, &x174, x2, (arg1[0])); 1398 uint32_t x175; 1399 fiat_p256_uint1 x176; 1400 fiat_p256_addcarryx_u32(&x175, &x176, 0x0, x171, x174); 1401 uint32_t x177; 1402 fiat_p256_uint1 x178; 1403 fiat_p256_addcarryx_u32(&x177, &x178, x176, x169, x172); 1404 uint32_t x179; 1405 fiat_p256_uint1 x180; 1406 fiat_p256_addcarryx_u32(&x179, &x180, x178, x167, x170); 1407 uint32_t x181; 1408 fiat_p256_uint1 x182; 1409 fiat_p256_addcarryx_u32(&x181, &x182, x180, x165, x168); 1410 uint32_t x183; 1411 fiat_p256_uint1 x184; 1412 fiat_p256_addcarryx_u32(&x183, &x184, x182, x163, x166); 1413 uint32_t x185; 1414 fiat_p256_uint1 x186; 1415 fiat_p256_addcarryx_u32(&x185, &x186, x184, x161, x164); 1416 uint32_t x187; 1417 fiat_p256_uint1 x188; 1418 fiat_p256_addcarryx_u32(&x187, &x188, x186, x159, x162); 1419 uint32_t x189; 1420 fiat_p256_uint1 x190; 1421 fiat_p256_addcarryx_u32(&x189, &x190, x188, 0x0, x160); 1422 uint32_t x191; 1423 fiat_p256_uint1 x192; 1424 fiat_p256_addcarryx_u32(&x191, &x192, 0x0, x173, x141); 1425 uint32_t x193; 1426 fiat_p256_uint1 x194; 1427 fiat_p256_addcarryx_u32(&x193, &x194, x192, x175, x143); 1428 uint32_t x195; 1429 fiat_p256_uint1 x196; 1430 fiat_p256_addcarryx_u32(&x195, &x196, x194, x177, x145); 1431 uint32_t x197; 1432 fiat_p256_uint1 x198; 1433 fiat_p256_addcarryx_u32(&x197, &x198, x196, x179, x147); 1434 uint32_t x199; 1435 fiat_p256_uint1 x200; 1436 fiat_p256_addcarryx_u32(&x199, &x200, x198, x181, x149); 1437 uint32_t x201; 1438 fiat_p256_uint1 x202; 1439 fiat_p256_addcarryx_u32(&x201, &x202, x200, x183, x151); 1440 uint32_t x203; 1441 fiat_p256_uint1 x204; 1442 fiat_p256_addcarryx_u32(&x203, &x204, x202, x185, x153); 1443 uint32_t x205; 1444 fiat_p256_uint1 x206; 1445 fiat_p256_addcarryx_u32(&x205, &x206, x204, x187, x155); 1446 uint32_t x207; 1447 fiat_p256_uint1 x208; 1448 fiat_p256_addcarryx_u32(&x207, &x208, x206, x189, x157); 1449 uint32_t x209; 1450 uint32_t x210; 1451 fiat_p256_mulx_u32(&x209, &x210, x191, UINT32_C(0xffffffff)); 1452 uint32_t x211; 1453 uint32_t x212; 1454 fiat_p256_mulx_u32(&x211, &x212, x191, UINT32_C(0xffffffff)); 1455 uint32_t x213; 1456 uint32_t x214; 1457 fiat_p256_mulx_u32(&x213, &x214, x191, UINT32_C(0xffffffff)); 1458 uint32_t x215; 1459 uint32_t x216; 1460 fiat_p256_mulx_u32(&x215, &x216, x191, UINT32_C(0xffffffff)); 1461 uint32_t x217; 1462 fiat_p256_uint1 x218; 1463 fiat_p256_addcarryx_u32(&x217, &x218, 0x0, x213, x216); 1464 uint32_t x219; 1465 fiat_p256_uint1 x220; 1466 fiat_p256_addcarryx_u32(&x219, &x220, x218, x211, x214); 1467 uint32_t x221; 1468 fiat_p256_uint1 x222; 1469 fiat_p256_addcarryx_u32(&x221, &x222, x220, 0x0, x212); 1470 uint32_t x223; 1471 fiat_p256_uint1 x224; 1472 fiat_p256_addcarryx_u32(&x223, &x224, 0x0, x215, x191); 1473 uint32_t x225; 1474 fiat_p256_uint1 x226; 1475 fiat_p256_addcarryx_u32(&x225, &x226, x224, x217, x193); 1476 uint32_t x227; 1477 fiat_p256_uint1 x228; 1478 fiat_p256_addcarryx_u32(&x227, &x228, x226, x219, x195); 1479 uint32_t x229; 1480 fiat_p256_uint1 x230; 1481 fiat_p256_addcarryx_u32(&x229, &x230, x228, x221, x197); 1482 uint32_t x231; 1483 fiat_p256_uint1 x232; 1484 fiat_p256_addcarryx_u32(&x231, &x232, x230, 0x0, x199); 1485 uint32_t x233; 1486 fiat_p256_uint1 x234; 1487 fiat_p256_addcarryx_u32(&x233, &x234, x232, 0x0, x201); 1488 uint32_t x235; 1489 fiat_p256_uint1 x236; 1490 fiat_p256_addcarryx_u32(&x235, &x236, x234, x191, x203); 1491 uint32_t x237; 1492 fiat_p256_uint1 x238; 1493 fiat_p256_addcarryx_u32(&x237, &x238, x236, x209, x205); 1494 uint32_t x239; 1495 fiat_p256_uint1 x240; 1496 fiat_p256_addcarryx_u32(&x239, &x240, x238, x210, x207); 1497 uint32_t x241; 1498 fiat_p256_uint1 x242; 1499 fiat_p256_addcarryx_u32(&x241, &x242, x240, 0x0, x208); 1500 uint32_t x243; 1501 uint32_t x244; 1502 fiat_p256_mulx_u32(&x243, &x244, x3, (arg1[7])); 1503 uint32_t x245; 1504 uint32_t x246; 1505 fiat_p256_mulx_u32(&x245, &x246, x3, (arg1[6])); 1506 uint32_t x247; 1507 uint32_t x248; 1508 fiat_p256_mulx_u32(&x247, &x248, x3, (arg1[5])); 1509 uint32_t x249; 1510 uint32_t x250; 1511 fiat_p256_mulx_u32(&x249, &x250, x3, (arg1[4])); 1512 uint32_t x251; 1513 uint32_t x252; 1514 fiat_p256_mulx_u32(&x251, &x252, x3, (arg1[3])); 1515 uint32_t x253; 1516 uint32_t x254; 1517 fiat_p256_mulx_u32(&x253, &x254, x3, (arg1[2])); 1518 uint32_t x255; 1519 uint32_t x256; 1520 fiat_p256_mulx_u32(&x255, &x256, x3, (arg1[1])); 1521 uint32_t x257; 1522 uint32_t x258; 1523 fiat_p256_mulx_u32(&x257, &x258, x3, (arg1[0])); 1524 uint32_t x259; 1525 fiat_p256_uint1 x260; 1526 fiat_p256_addcarryx_u32(&x259, &x260, 0x0, x255, x258); 1527 uint32_t x261; 1528 fiat_p256_uint1 x262; 1529 fiat_p256_addcarryx_u32(&x261, &x262, x260, x253, x256); 1530 uint32_t x263; 1531 fiat_p256_uint1 x264; 1532 fiat_p256_addcarryx_u32(&x263, &x264, x262, x251, x254); 1533 uint32_t x265; 1534 fiat_p256_uint1 x266; 1535 fiat_p256_addcarryx_u32(&x265, &x266, x264, x249, x252); 1536 uint32_t x267; 1537 fiat_p256_uint1 x268; 1538 fiat_p256_addcarryx_u32(&x267, &x268, x266, x247, x250); 1539 uint32_t x269; 1540 fiat_p256_uint1 x270; 1541 fiat_p256_addcarryx_u32(&x269, &x270, x268, x245, x248); 1542 uint32_t x271; 1543 fiat_p256_uint1 x272; 1544 fiat_p256_addcarryx_u32(&x271, &x272, x270, x243, x246); 1545 uint32_t x273; 1546 fiat_p256_uint1 x274; 1547 fiat_p256_addcarryx_u32(&x273, &x274, x272, 0x0, x244); 1548 uint32_t x275; 1549 fiat_p256_uint1 x276; 1550 fiat_p256_addcarryx_u32(&x275, &x276, 0x0, x257, x225); 1551 uint32_t x277; 1552 fiat_p256_uint1 x278; 1553 fiat_p256_addcarryx_u32(&x277, &x278, x276, x259, x227); 1554 uint32_t x279; 1555 fiat_p256_uint1 x280; 1556 fiat_p256_addcarryx_u32(&x279, &x280, x278, x261, x229); 1557 uint32_t x281; 1558 fiat_p256_uint1 x282; 1559 fiat_p256_addcarryx_u32(&x281, &x282, x280, x263, x231); 1560 uint32_t x283; 1561 fiat_p256_uint1 x284; 1562 fiat_p256_addcarryx_u32(&x283, &x284, x282, x265, x233); 1563 uint32_t x285; 1564 fiat_p256_uint1 x286; 1565 fiat_p256_addcarryx_u32(&x285, &x286, x284, x267, x235); 1566 uint32_t x287; 1567 fiat_p256_uint1 x288; 1568 fiat_p256_addcarryx_u32(&x287, &x288, x286, x269, x237); 1569 uint32_t x289; 1570 fiat_p256_uint1 x290; 1571 fiat_p256_addcarryx_u32(&x289, &x290, x288, x271, x239); 1572 uint32_t x291; 1573 fiat_p256_uint1 x292; 1574 fiat_p256_addcarryx_u32(&x291, &x292, x290, x273, x241); 1575 uint32_t x293; 1576 uint32_t x294; 1577 fiat_p256_mulx_u32(&x293, &x294, x275, UINT32_C(0xffffffff)); 1578 uint32_t x295; 1579 uint32_t x296; 1580 fiat_p256_mulx_u32(&x295, &x296, x275, UINT32_C(0xffffffff)); 1581 uint32_t x297; 1582 uint32_t x298; 1583 fiat_p256_mulx_u32(&x297, &x298, x275, UINT32_C(0xffffffff)); 1584 uint32_t x299; 1585 uint32_t x300; 1586 fiat_p256_mulx_u32(&x299, &x300, x275, UINT32_C(0xffffffff)); 1587 uint32_t x301; 1588 fiat_p256_uint1 x302; 1589 fiat_p256_addcarryx_u32(&x301, &x302, 0x0, x297, x300); 1590 uint32_t x303; 1591 fiat_p256_uint1 x304; 1592 fiat_p256_addcarryx_u32(&x303, &x304, x302, x295, x298); 1593 uint32_t x305; 1594 fiat_p256_uint1 x306; 1595 fiat_p256_addcarryx_u32(&x305, &x306, x304, 0x0, x296); 1596 uint32_t x307; 1597 fiat_p256_uint1 x308; 1598 fiat_p256_addcarryx_u32(&x307, &x308, 0x0, x299, x275); 1599 uint32_t x309; 1600 fiat_p256_uint1 x310; 1601 fiat_p256_addcarryx_u32(&x309, &x310, x308, x301, x277); 1602 uint32_t x311; 1603 fiat_p256_uint1 x312; 1604 fiat_p256_addcarryx_u32(&x311, &x312, x310, x303, x279); 1605 uint32_t x313; 1606 fiat_p256_uint1 x314; 1607 fiat_p256_addcarryx_u32(&x313, &x314, x312, x305, x281); 1608 uint32_t x315; 1609 fiat_p256_uint1 x316; 1610 fiat_p256_addcarryx_u32(&x315, &x316, x314, 0x0, x283); 1611 uint32_t x317; 1612 fiat_p256_uint1 x318; 1613 fiat_p256_addcarryx_u32(&x317, &x318, x316, 0x0, x285); 1614 uint32_t x319; 1615 fiat_p256_uint1 x320; 1616 fiat_p256_addcarryx_u32(&x319, &x320, x318, x275, x287); 1617 uint32_t x321; 1618 fiat_p256_uint1 x322; 1619 fiat_p256_addcarryx_u32(&x321, &x322, x320, x293, x289); 1620 uint32_t x323; 1621 fiat_p256_uint1 x324; 1622 fiat_p256_addcarryx_u32(&x323, &x324, x322, x294, x291); 1623 uint32_t x325; 1624 fiat_p256_uint1 x326; 1625 fiat_p256_addcarryx_u32(&x325, &x326, x324, 0x0, x292); 1626 uint32_t x327; 1627 uint32_t x328; 1628 fiat_p256_mulx_u32(&x327, &x328, x4, (arg1[7])); 1629 uint32_t x329; 1630 uint32_t x330; 1631 fiat_p256_mulx_u32(&x329, &x330, x4, (arg1[6])); 1632 uint32_t x331; 1633 uint32_t x332; 1634 fiat_p256_mulx_u32(&x331, &x332, x4, (arg1[5])); 1635 uint32_t x333; 1636 uint32_t x334; 1637 fiat_p256_mulx_u32(&x333, &x334, x4, (arg1[4])); 1638 uint32_t x335; 1639 uint32_t x336; 1640 fiat_p256_mulx_u32(&x335, &x336, x4, (arg1[3])); 1641 uint32_t x337; 1642 uint32_t x338; 1643 fiat_p256_mulx_u32(&x337, &x338, x4, (arg1[2])); 1644 uint32_t x339; 1645 uint32_t x340; 1646 fiat_p256_mulx_u32(&x339, &x340, x4, (arg1[1])); 1647 uint32_t x341; 1648 uint32_t x342; 1649 fiat_p256_mulx_u32(&x341, &x342, x4, (arg1[0])); 1650 uint32_t x343; 1651 fiat_p256_uint1 x344; 1652 fiat_p256_addcarryx_u32(&x343, &x344, 0x0, x339, x342); 1653 uint32_t x345; 1654 fiat_p256_uint1 x346; 1655 fiat_p256_addcarryx_u32(&x345, &x346, x344, x337, x340); 1656 uint32_t x347; 1657 fiat_p256_uint1 x348; 1658 fiat_p256_addcarryx_u32(&x347, &x348, x346, x335, x338); 1659 uint32_t x349; 1660 fiat_p256_uint1 x350; 1661 fiat_p256_addcarryx_u32(&x349, &x350, x348, x333, x336); 1662 uint32_t x351; 1663 fiat_p256_uint1 x352; 1664 fiat_p256_addcarryx_u32(&x351, &x352, x350, x331, x334); 1665 uint32_t x353; 1666 fiat_p256_uint1 x354; 1667 fiat_p256_addcarryx_u32(&x353, &x354, x352, x329, x332); 1668 uint32_t x355; 1669 fiat_p256_uint1 x356; 1670 fiat_p256_addcarryx_u32(&x355, &x356, x354, x327, x330); 1671 uint32_t x357; 1672 fiat_p256_uint1 x358; 1673 fiat_p256_addcarryx_u32(&x357, &x358, x356, 0x0, x328); 1674 uint32_t x359; 1675 fiat_p256_uint1 x360; 1676 fiat_p256_addcarryx_u32(&x359, &x360, 0x0, x341, x309); 1677 uint32_t x361; 1678 fiat_p256_uint1 x362; 1679 fiat_p256_addcarryx_u32(&x361, &x362, x360, x343, x311); 1680 uint32_t x363; 1681 fiat_p256_uint1 x364; 1682 fiat_p256_addcarryx_u32(&x363, &x364, x362, x345, x313); 1683 uint32_t x365; 1684 fiat_p256_uint1 x366; 1685 fiat_p256_addcarryx_u32(&x365, &x366, x364, x347, x315); 1686 uint32_t x367; 1687 fiat_p256_uint1 x368; 1688 fiat_p256_addcarryx_u32(&x367, &x368, x366, x349, x317); 1689 uint32_t x369; 1690 fiat_p256_uint1 x370; 1691 fiat_p256_addcarryx_u32(&x369, &x370, x368, x351, x319); 1692 uint32_t x371; 1693 fiat_p256_uint1 x372; 1694 fiat_p256_addcarryx_u32(&x371, &x372, x370, x353, x321); 1695 uint32_t x373; 1696 fiat_p256_uint1 x374; 1697 fiat_p256_addcarryx_u32(&x373, &x374, x372, x355, x323); 1698 uint32_t x375; 1699 fiat_p256_uint1 x376; 1700 fiat_p256_addcarryx_u32(&x375, &x376, x374, x357, x325); 1701 uint32_t x377; 1702 uint32_t x378; 1703 fiat_p256_mulx_u32(&x377, &x378, x359, UINT32_C(0xffffffff)); 1704 uint32_t x379; 1705 uint32_t x380; 1706 fiat_p256_mulx_u32(&x379, &x380, x359, UINT32_C(0xffffffff)); 1707 uint32_t x381; 1708 uint32_t x382; 1709 fiat_p256_mulx_u32(&x381, &x382, x359, UINT32_C(0xffffffff)); 1710 uint32_t x383; 1711 uint32_t x384; 1712 fiat_p256_mulx_u32(&x383, &x384, x359, UINT32_C(0xffffffff)); 1713 uint32_t x385; 1714 fiat_p256_uint1 x386; 1715 fiat_p256_addcarryx_u32(&x385, &x386, 0x0, x381, x384); 1716 uint32_t x387; 1717 fiat_p256_uint1 x388; 1718 fiat_p256_addcarryx_u32(&x387, &x388, x386, x379, x382); 1719 uint32_t x389; 1720 fiat_p256_uint1 x390; 1721 fiat_p256_addcarryx_u32(&x389, &x390, x388, 0x0, x380); 1722 uint32_t x391; 1723 fiat_p256_uint1 x392; 1724 fiat_p256_addcarryx_u32(&x391, &x392, 0x0, x383, x359); 1725 uint32_t x393; 1726 fiat_p256_uint1 x394; 1727 fiat_p256_addcarryx_u32(&x393, &x394, x392, x385, x361); 1728 uint32_t x395; 1729 fiat_p256_uint1 x396; 1730 fiat_p256_addcarryx_u32(&x395, &x396, x394, x387, x363); 1731 uint32_t x397; 1732 fiat_p256_uint1 x398; 1733 fiat_p256_addcarryx_u32(&x397, &x398, x396, x389, x365); 1734 uint32_t x399; 1735 fiat_p256_uint1 x400; 1736 fiat_p256_addcarryx_u32(&x399, &x400, x398, 0x0, x367); 1737 uint32_t x401; 1738 fiat_p256_uint1 x402; 1739 fiat_p256_addcarryx_u32(&x401, &x402, x400, 0x0, x369); 1740 uint32_t x403; 1741 fiat_p256_uint1 x404; 1742 fiat_p256_addcarryx_u32(&x403, &x404, x402, x359, x371); 1743 uint32_t x405; 1744 fiat_p256_uint1 x406; 1745 fiat_p256_addcarryx_u32(&x405, &x406, x404, x377, x373); 1746 uint32_t x407; 1747 fiat_p256_uint1 x408; 1748 fiat_p256_addcarryx_u32(&x407, &x408, x406, x378, x375); 1749 uint32_t x409; 1750 fiat_p256_uint1 x410; 1751 fiat_p256_addcarryx_u32(&x409, &x410, x408, 0x0, x376); 1752 uint32_t x411; 1753 uint32_t x412; 1754 fiat_p256_mulx_u32(&x411, &x412, x5, (arg1[7])); 1755 uint32_t x413; 1756 uint32_t x414; 1757 fiat_p256_mulx_u32(&x413, &x414, x5, (arg1[6])); 1758 uint32_t x415; 1759 uint32_t x416; 1760 fiat_p256_mulx_u32(&x415, &x416, x5, (arg1[5])); 1761 uint32_t x417; 1762 uint32_t x418; 1763 fiat_p256_mulx_u32(&x417, &x418, x5, (arg1[4])); 1764 uint32_t x419; 1765 uint32_t x420; 1766 fiat_p256_mulx_u32(&x419, &x420, x5, (arg1[3])); 1767 uint32_t x421; 1768 uint32_t x422; 1769 fiat_p256_mulx_u32(&x421, &x422, x5, (arg1[2])); 1770 uint32_t x423; 1771 uint32_t x424; 1772 fiat_p256_mulx_u32(&x423, &x424, x5, (arg1[1])); 1773 uint32_t x425; 1774 uint32_t x426; 1775 fiat_p256_mulx_u32(&x425, &x426, x5, (arg1[0])); 1776 uint32_t x427; 1777 fiat_p256_uint1 x428; 1778 fiat_p256_addcarryx_u32(&x427, &x428, 0x0, x423, x426); 1779 uint32_t x429; 1780 fiat_p256_uint1 x430; 1781 fiat_p256_addcarryx_u32(&x429, &x430, x428, x421, x424); 1782 uint32_t x431; 1783 fiat_p256_uint1 x432; 1784 fiat_p256_addcarryx_u32(&x431, &x432, x430, x419, x422); 1785 uint32_t x433; 1786 fiat_p256_uint1 x434; 1787 fiat_p256_addcarryx_u32(&x433, &x434, x432, x417, x420); 1788 uint32_t x435; 1789 fiat_p256_uint1 x436; 1790 fiat_p256_addcarryx_u32(&x435, &x436, x434, x415, x418); 1791 uint32_t x437; 1792 fiat_p256_uint1 x438; 1793 fiat_p256_addcarryx_u32(&x437, &x438, x436, x413, x416); 1794 uint32_t x439; 1795 fiat_p256_uint1 x440; 1796 fiat_p256_addcarryx_u32(&x439, &x440, x438, x411, x414); 1797 uint32_t x441; 1798 fiat_p256_uint1 x442; 1799 fiat_p256_addcarryx_u32(&x441, &x442, x440, 0x0, x412); 1800 uint32_t x443; 1801 fiat_p256_uint1 x444; 1802 fiat_p256_addcarryx_u32(&x443, &x444, 0x0, x425, x393); 1803 uint32_t x445; 1804 fiat_p256_uint1 x446; 1805 fiat_p256_addcarryx_u32(&x445, &x446, x444, x427, x395); 1806 uint32_t x447; 1807 fiat_p256_uint1 x448; 1808 fiat_p256_addcarryx_u32(&x447, &x448, x446, x429, x397); 1809 uint32_t x449; 1810 fiat_p256_uint1 x450; 1811 fiat_p256_addcarryx_u32(&x449, &x450, x448, x431, x399); 1812 uint32_t x451; 1813 fiat_p256_uint1 x452; 1814 fiat_p256_addcarryx_u32(&x451, &x452, x450, x433, x401); 1815 uint32_t x453; 1816 fiat_p256_uint1 x454; 1817 fiat_p256_addcarryx_u32(&x453, &x454, x452, x435, x403); 1818 uint32_t x455; 1819 fiat_p256_uint1 x456; 1820 fiat_p256_addcarryx_u32(&x455, &x456, x454, x437, x405); 1821 uint32_t x457; 1822 fiat_p256_uint1 x458; 1823 fiat_p256_addcarryx_u32(&x457, &x458, x456, x439, x407); 1824 uint32_t x459; 1825 fiat_p256_uint1 x460; 1826 fiat_p256_addcarryx_u32(&x459, &x460, x458, x441, x409); 1827 uint32_t x461; 1828 uint32_t x462; 1829 fiat_p256_mulx_u32(&x461, &x462, x443, UINT32_C(0xffffffff)); 1830 uint32_t x463; 1831 uint32_t x464; 1832 fiat_p256_mulx_u32(&x463, &x464, x443, UINT32_C(0xffffffff)); 1833 uint32_t x465; 1834 uint32_t x466; 1835 fiat_p256_mulx_u32(&x465, &x466, x443, UINT32_C(0xffffffff)); 1836 uint32_t x467; 1837 uint32_t x468; 1838 fiat_p256_mulx_u32(&x467, &x468, x443, UINT32_C(0xffffffff)); 1839 uint32_t x469; 1840 fiat_p256_uint1 x470; 1841 fiat_p256_addcarryx_u32(&x469, &x470, 0x0, x465, x468); 1842 uint32_t x471; 1843 fiat_p256_uint1 x472; 1844 fiat_p256_addcarryx_u32(&x471, &x472, x470, x463, x466); 1845 uint32_t x473; 1846 fiat_p256_uint1 x474; 1847 fiat_p256_addcarryx_u32(&x473, &x474, x472, 0x0, x464); 1848 uint32_t x475; 1849 fiat_p256_uint1 x476; 1850 fiat_p256_addcarryx_u32(&x475, &x476, 0x0, x467, x443); 1851 uint32_t x477; 1852 fiat_p256_uint1 x478; 1853 fiat_p256_addcarryx_u32(&x477, &x478, x476, x469, x445); 1854 uint32_t x479; 1855 fiat_p256_uint1 x480; 1856 fiat_p256_addcarryx_u32(&x479, &x480, x478, x471, x447); 1857 uint32_t x481; 1858 fiat_p256_uint1 x482; 1859 fiat_p256_addcarryx_u32(&x481, &x482, x480, x473, x449); 1860 uint32_t x483; 1861 fiat_p256_uint1 x484; 1862 fiat_p256_addcarryx_u32(&x483, &x484, x482, 0x0, x451); 1863 uint32_t x485; 1864 fiat_p256_uint1 x486; 1865 fiat_p256_addcarryx_u32(&x485, &x486, x484, 0x0, x453); 1866 uint32_t x487; 1867 fiat_p256_uint1 x488; 1868 fiat_p256_addcarryx_u32(&x487, &x488, x486, x443, x455); 1869 uint32_t x489; 1870 fiat_p256_uint1 x490; 1871 fiat_p256_addcarryx_u32(&x489, &x490, x488, x461, x457); 1872 uint32_t x491; 1873 fiat_p256_uint1 x492; 1874 fiat_p256_addcarryx_u32(&x491, &x492, x490, x462, x459); 1875 uint32_t x493; 1876 fiat_p256_uint1 x494; 1877 fiat_p256_addcarryx_u32(&x493, &x494, x492, 0x0, x460); 1878 uint32_t x495; 1879 uint32_t x496; 1880 fiat_p256_mulx_u32(&x495, &x496, x6, (arg1[7])); 1881 uint32_t x497; 1882 uint32_t x498; 1883 fiat_p256_mulx_u32(&x497, &x498, x6, (arg1[6])); 1884 uint32_t x499; 1885 uint32_t x500; 1886 fiat_p256_mulx_u32(&x499, &x500, x6, (arg1[5])); 1887 uint32_t x501; 1888 uint32_t x502; 1889 fiat_p256_mulx_u32(&x501, &x502, x6, (arg1[4])); 1890 uint32_t x503; 1891 uint32_t x504; 1892 fiat_p256_mulx_u32(&x503, &x504, x6, (arg1[3])); 1893 uint32_t x505; 1894 uint32_t x506; 1895 fiat_p256_mulx_u32(&x505, &x506, x6, (arg1[2])); 1896 uint32_t x507; 1897 uint32_t x508; 1898 fiat_p256_mulx_u32(&x507, &x508, x6, (arg1[1])); 1899 uint32_t x509; 1900 uint32_t x510; 1901 fiat_p256_mulx_u32(&x509, &x510, x6, (arg1[0])); 1902 uint32_t x511; 1903 fiat_p256_uint1 x512; 1904 fiat_p256_addcarryx_u32(&x511, &x512, 0x0, x507, x510); 1905 uint32_t x513; 1906 fiat_p256_uint1 x514; 1907 fiat_p256_addcarryx_u32(&x513, &x514, x512, x505, x508); 1908 uint32_t x515; 1909 fiat_p256_uint1 x516; 1910 fiat_p256_addcarryx_u32(&x515, &x516, x514, x503, x506); 1911 uint32_t x517; 1912 fiat_p256_uint1 x518; 1913 fiat_p256_addcarryx_u32(&x517, &x518, x516, x501, x504); 1914 uint32_t x519; 1915 fiat_p256_uint1 x520; 1916 fiat_p256_addcarryx_u32(&x519, &x520, x518, x499, x502); 1917 uint32_t x521; 1918 fiat_p256_uint1 x522; 1919 fiat_p256_addcarryx_u32(&x521, &x522, x520, x497, x500); 1920 uint32_t x523; 1921 fiat_p256_uint1 x524; 1922 fiat_p256_addcarryx_u32(&x523, &x524, x522, x495, x498); 1923 uint32_t x525; 1924 fiat_p256_uint1 x526; 1925 fiat_p256_addcarryx_u32(&x525, &x526, x524, 0x0, x496); 1926 uint32_t x527; 1927 fiat_p256_uint1 x528; 1928 fiat_p256_addcarryx_u32(&x527, &x528, 0x0, x509, x477); 1929 uint32_t x529; 1930 fiat_p256_uint1 x530; 1931 fiat_p256_addcarryx_u32(&x529, &x530, x528, x511, x479); 1932 uint32_t x531; 1933 fiat_p256_uint1 x532; 1934 fiat_p256_addcarryx_u32(&x531, &x532, x530, x513, x481); 1935 uint32_t x533; 1936 fiat_p256_uint1 x534; 1937 fiat_p256_addcarryx_u32(&x533, &x534, x532, x515, x483); 1938 uint32_t x535; 1939 fiat_p256_uint1 x536; 1940 fiat_p256_addcarryx_u32(&x535, &x536, x534, x517, x485); 1941 uint32_t x537; 1942 fiat_p256_uint1 x538; 1943 fiat_p256_addcarryx_u32(&x537, &x538, x536, x519, x487); 1944 uint32_t x539; 1945 fiat_p256_uint1 x540; 1946 fiat_p256_addcarryx_u32(&x539, &x540, x538, x521, x489); 1947 uint32_t x541; 1948 fiat_p256_uint1 x542; 1949 fiat_p256_addcarryx_u32(&x541, &x542, x540, x523, x491); 1950 uint32_t x543; 1951 fiat_p256_uint1 x544; 1952 fiat_p256_addcarryx_u32(&x543, &x544, x542, x525, x493); 1953 uint32_t x545; 1954 uint32_t x546; 1955 fiat_p256_mulx_u32(&x545, &x546, x527, UINT32_C(0xffffffff)); 1956 uint32_t x547; 1957 uint32_t x548; 1958 fiat_p256_mulx_u32(&x547, &x548, x527, UINT32_C(0xffffffff)); 1959 uint32_t x549; 1960 uint32_t x550; 1961 fiat_p256_mulx_u32(&x549, &x550, x527, UINT32_C(0xffffffff)); 1962 uint32_t x551; 1963 uint32_t x552; 1964 fiat_p256_mulx_u32(&x551, &x552, x527, UINT32_C(0xffffffff)); 1965 uint32_t x553; 1966 fiat_p256_uint1 x554; 1967 fiat_p256_addcarryx_u32(&x553, &x554, 0x0, x549, x552); 1968 uint32_t x555; 1969 fiat_p256_uint1 x556; 1970 fiat_p256_addcarryx_u32(&x555, &x556, x554, x547, x550); 1971 uint32_t x557; 1972 fiat_p256_uint1 x558; 1973 fiat_p256_addcarryx_u32(&x557, &x558, x556, 0x0, x548); 1974 uint32_t x559; 1975 fiat_p256_uint1 x560; 1976 fiat_p256_addcarryx_u32(&x559, &x560, 0x0, x551, x527); 1977 uint32_t x561; 1978 fiat_p256_uint1 x562; 1979 fiat_p256_addcarryx_u32(&x561, &x562, x560, x553, x529); 1980 uint32_t x563; 1981 fiat_p256_uint1 x564; 1982 fiat_p256_addcarryx_u32(&x563, &x564, x562, x555, x531); 1983 uint32_t x565; 1984 fiat_p256_uint1 x566; 1985 fiat_p256_addcarryx_u32(&x565, &x566, x564, x557, x533); 1986 uint32_t x567; 1987 fiat_p256_uint1 x568; 1988 fiat_p256_addcarryx_u32(&x567, &x568, x566, 0x0, x535); 1989 uint32_t x569; 1990 fiat_p256_uint1 x570; 1991 fiat_p256_addcarryx_u32(&x569, &x570, x568, 0x0, x537); 1992 uint32_t x571; 1993 fiat_p256_uint1 x572; 1994 fiat_p256_addcarryx_u32(&x571, &x572, x570, x527, x539); 1995 uint32_t x573; 1996 fiat_p256_uint1 x574; 1997 fiat_p256_addcarryx_u32(&x573, &x574, x572, x545, x541); 1998 uint32_t x575; 1999 fiat_p256_uint1 x576; 2000 fiat_p256_addcarryx_u32(&x575, &x576, x574, x546, x543); 2001 uint32_t x577; 2002 fiat_p256_uint1 x578; 2003 fiat_p256_addcarryx_u32(&x577, &x578, x576, 0x0, x544); 2004 uint32_t x579; 2005 uint32_t x580; 2006 fiat_p256_mulx_u32(&x579, &x580, x7, (arg1[7])); 2007 uint32_t x581; 2008 uint32_t x582; 2009 fiat_p256_mulx_u32(&x581, &x582, x7, (arg1[6])); 2010 uint32_t x583; 2011 uint32_t x584; 2012 fiat_p256_mulx_u32(&x583, &x584, x7, (arg1[5])); 2013 uint32_t x585; 2014 uint32_t x586; 2015 fiat_p256_mulx_u32(&x585, &x586, x7, (arg1[4])); 2016 uint32_t x587; 2017 uint32_t x588; 2018 fiat_p256_mulx_u32(&x587, &x588, x7, (arg1[3])); 2019 uint32_t x589; 2020 uint32_t x590; 2021 fiat_p256_mulx_u32(&x589, &x590, x7, (arg1[2])); 2022 uint32_t x591; 2023 uint32_t x592; 2024 fiat_p256_mulx_u32(&x591, &x592, x7, (arg1[1])); 2025 uint32_t x593; 2026 uint32_t x594; 2027 fiat_p256_mulx_u32(&x593, &x594, x7, (arg1[0])); 2028 uint32_t x595; 2029 fiat_p256_uint1 x596; 2030 fiat_p256_addcarryx_u32(&x595, &x596, 0x0, x591, x594); 2031 uint32_t x597; 2032 fiat_p256_uint1 x598; 2033 fiat_p256_addcarryx_u32(&x597, &x598, x596, x589, x592); 2034 uint32_t x599; 2035 fiat_p256_uint1 x600; 2036 fiat_p256_addcarryx_u32(&x599, &x600, x598, x587, x590); 2037 uint32_t x601; 2038 fiat_p256_uint1 x602; 2039 fiat_p256_addcarryx_u32(&x601, &x602, x600, x585, x588); 2040 uint32_t x603; 2041 fiat_p256_uint1 x604; 2042 fiat_p256_addcarryx_u32(&x603, &x604, x602, x583, x586); 2043 uint32_t x605; 2044 fiat_p256_uint1 x606; 2045 fiat_p256_addcarryx_u32(&x605, &x606, x604, x581, x584); 2046 uint32_t x607; 2047 fiat_p256_uint1 x608; 2048 fiat_p256_addcarryx_u32(&x607, &x608, x606, x579, x582); 2049 uint32_t x609; 2050 fiat_p256_uint1 x610; 2051 fiat_p256_addcarryx_u32(&x609, &x610, x608, 0x0, x580); 2052 uint32_t x611; 2053 fiat_p256_uint1 x612; 2054 fiat_p256_addcarryx_u32(&x611, &x612, 0x0, x593, x561); 2055 uint32_t x613; 2056 fiat_p256_uint1 x614; 2057 fiat_p256_addcarryx_u32(&x613, &x614, x612, x595, x563); 2058 uint32_t x615; 2059 fiat_p256_uint1 x616; 2060 fiat_p256_addcarryx_u32(&x615, &x616, x614, x597, x565); 2061 uint32_t x617; 2062 fiat_p256_uint1 x618; 2063 fiat_p256_addcarryx_u32(&x617, &x618, x616, x599, x567); 2064 uint32_t x619; 2065 fiat_p256_uint1 x620; 2066 fiat_p256_addcarryx_u32(&x619, &x620, x618, x601, x569); 2067 uint32_t x621; 2068 fiat_p256_uint1 x622; 2069 fiat_p256_addcarryx_u32(&x621, &x622, x620, x603, x571); 2070 uint32_t x623; 2071 fiat_p256_uint1 x624; 2072 fiat_p256_addcarryx_u32(&x623, &x624, x622, x605, x573); 2073 uint32_t x625; 2074 fiat_p256_uint1 x626; 2075 fiat_p256_addcarryx_u32(&x625, &x626, x624, x607, x575); 2076 uint32_t x627; 2077 fiat_p256_uint1 x628; 2078 fiat_p256_addcarryx_u32(&x627, &x628, x626, x609, x577); 2079 uint32_t x629; 2080 uint32_t x630; 2081 fiat_p256_mulx_u32(&x629, &x630, x611, UINT32_C(0xffffffff)); 2082 uint32_t x631; 2083 uint32_t x632; 2084 fiat_p256_mulx_u32(&x631, &x632, x611, UINT32_C(0xffffffff)); 2085 uint32_t x633; 2086 uint32_t x634; 2087 fiat_p256_mulx_u32(&x633, &x634, x611, UINT32_C(0xffffffff)); 2088 uint32_t x635; 2089 uint32_t x636; 2090 fiat_p256_mulx_u32(&x635, &x636, x611, UINT32_C(0xffffffff)); 2091 uint32_t x637; 2092 fiat_p256_uint1 x638; 2093 fiat_p256_addcarryx_u32(&x637, &x638, 0x0, x633, x636); 2094 uint32_t x639; 2095 fiat_p256_uint1 x640; 2096 fiat_p256_addcarryx_u32(&x639, &x640, x638, x631, x634); 2097 uint32_t x641; 2098 fiat_p256_uint1 x642; 2099 fiat_p256_addcarryx_u32(&x641, &x642, x640, 0x0, x632); 2100 uint32_t x643; 2101 fiat_p256_uint1 x644; 2102 fiat_p256_addcarryx_u32(&x643, &x644, 0x0, x635, x611); 2103 uint32_t x645; 2104 fiat_p256_uint1 x646; 2105 fiat_p256_addcarryx_u32(&x645, &x646, x644, x637, x613); 2106 uint32_t x647; 2107 fiat_p256_uint1 x648; 2108 fiat_p256_addcarryx_u32(&x647, &x648, x646, x639, x615); 2109 uint32_t x649; 2110 fiat_p256_uint1 x650; 2111 fiat_p256_addcarryx_u32(&x649, &x650, x648, x641, x617); 2112 uint32_t x651; 2113 fiat_p256_uint1 x652; 2114 fiat_p256_addcarryx_u32(&x651, &x652, x650, 0x0, x619); 2115 uint32_t x653; 2116 fiat_p256_uint1 x654; 2117 fiat_p256_addcarryx_u32(&x653, &x654, x652, 0x0, x621); 2118 uint32_t x655; 2119 fiat_p256_uint1 x656; 2120 fiat_p256_addcarryx_u32(&x655, &x656, x654, x611, x623); 2121 uint32_t x657; 2122 fiat_p256_uint1 x658; 2123 fiat_p256_addcarryx_u32(&x657, &x658, x656, x629, x625); 2124 uint32_t x659; 2125 fiat_p256_uint1 x660; 2126 fiat_p256_addcarryx_u32(&x659, &x660, x658, x630, x627); 2127 uint32_t x661; 2128 fiat_p256_uint1 x662; 2129 fiat_p256_addcarryx_u32(&x661, &x662, x660, 0x0, x628); 2130 uint32_t x663; 2131 fiat_p256_uint1 x664; 2132 fiat_p256_subborrowx_u32(&x663, &x664, 0x0, x645, UINT32_C(0xffffffff)); 2133 uint32_t x665; 2134 fiat_p256_uint1 x666; 2135 fiat_p256_subborrowx_u32(&x665, &x666, x664, x647, UINT32_C(0xffffffff)); 2136 uint32_t x667; 2137 fiat_p256_uint1 x668; 2138 fiat_p256_subborrowx_u32(&x667, &x668, x666, x649, UINT32_C(0xffffffff)); 2139 uint32_t x669; 2140 fiat_p256_uint1 x670; 2141 fiat_p256_subborrowx_u32(&x669, &x670, x668, x651, 0x0); 2142 uint32_t x671; 2143 fiat_p256_uint1 x672; 2144 fiat_p256_subborrowx_u32(&x671, &x672, x670, x653, 0x0); 2145 uint32_t x673; 2146 fiat_p256_uint1 x674; 2147 fiat_p256_subborrowx_u32(&x673, &x674, x672, x655, 0x0); 2148 uint32_t x675; 2149 fiat_p256_uint1 x676; 2150 fiat_p256_subborrowx_u32(&x675, &x676, x674, x657, 0x1); 2151 uint32_t x677; 2152 fiat_p256_uint1 x678; 2153 fiat_p256_subborrowx_u32(&x677, &x678, x676, x659, UINT32_C(0xffffffff)); 2154 uint32_t x679; 2155 fiat_p256_uint1 x680; 2156 fiat_p256_subborrowx_u32(&x679, &x680, x678, x661, 0x0); 2157 uint32_t x681; 2158 fiat_p256_cmovznz_u32(&x681, x680, x663, x645); 2159 uint32_t x682; 2160 fiat_p256_cmovznz_u32(&x682, x680, x665, x647); 2161 uint32_t x683; 2162 fiat_p256_cmovznz_u32(&x683, x680, x667, x649); 2163 uint32_t x684; 2164 fiat_p256_cmovznz_u32(&x684, x680, x669, x651); 2165 uint32_t x685; 2166 fiat_p256_cmovznz_u32(&x685, x680, x671, x653); 2167 uint32_t x686; 2168 fiat_p256_cmovznz_u32(&x686, x680, x673, x655); 2169 uint32_t x687; 2170 fiat_p256_cmovznz_u32(&x687, x680, x675, x657); 2171 uint32_t x688; 2172 fiat_p256_cmovznz_u32(&x688, x680, x677, x659); 2173 out1[0] = x681; 2174 out1[1] = x682; 2175 out1[2] = x683; 2176 out1[3] = x684; 2177 out1[4] = x685; 2178 out1[5] = x686; 2179 out1[6] = x687; 2180 out1[7] = x688; 2181 } 2182 2183 /* 2184 * Input Bounds: 2185 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2186 * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2187 * Output Bounds: 2188 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2189 */ 2190 static void fiat_p256_add(uint32_t out1[8], const uint32_t arg1[8], const uint32_t arg2[8]) { 2191 uint32_t x1; 2192 fiat_p256_uint1 x2; 2193 fiat_p256_addcarryx_u32(&x1, &x2, 0x0, (arg2[0]), (arg1[0])); 2194 uint32_t x3; 2195 fiat_p256_uint1 x4; 2196 fiat_p256_addcarryx_u32(&x3, &x4, x2, (arg2[1]), (arg1[1])); 2197 uint32_t x5; 2198 fiat_p256_uint1 x6; 2199 fiat_p256_addcarryx_u32(&x5, &x6, x4, (arg2[2]), (arg1[2])); 2200 uint32_t x7; 2201 fiat_p256_uint1 x8; 2202 fiat_p256_addcarryx_u32(&x7, &x8, x6, (arg2[3]), (arg1[3])); 2203 uint32_t x9; 2204 fiat_p256_uint1 x10; 2205 fiat_p256_addcarryx_u32(&x9, &x10, x8, (arg2[4]), (arg1[4])); 2206 uint32_t x11; 2207 fiat_p256_uint1 x12; 2208 fiat_p256_addcarryx_u32(&x11, &x12, x10, (arg2[5]), (arg1[5])); 2209 uint32_t x13; 2210 fiat_p256_uint1 x14; 2211 fiat_p256_addcarryx_u32(&x13, &x14, x12, (arg2[6]), (arg1[6])); 2212 uint32_t x15; 2213 fiat_p256_uint1 x16; 2214 fiat_p256_addcarryx_u32(&x15, &x16, x14, (arg2[7]), (arg1[7])); 2215 uint32_t x17; 2216 fiat_p256_uint1 x18; 2217 fiat_p256_subborrowx_u32(&x17, &x18, 0x0, x1, UINT32_C(0xffffffff)); 2218 uint32_t x19; 2219 fiat_p256_uint1 x20; 2220 fiat_p256_subborrowx_u32(&x19, &x20, x18, x3, UINT32_C(0xffffffff)); 2221 uint32_t x21; 2222 fiat_p256_uint1 x22; 2223 fiat_p256_subborrowx_u32(&x21, &x22, x20, x5, UINT32_C(0xffffffff)); 2224 uint32_t x23; 2225 fiat_p256_uint1 x24; 2226 fiat_p256_subborrowx_u32(&x23, &x24, x22, x7, 0x0); 2227 uint32_t x25; 2228 fiat_p256_uint1 x26; 2229 fiat_p256_subborrowx_u32(&x25, &x26, x24, x9, 0x0); 2230 uint32_t x27; 2231 fiat_p256_uint1 x28; 2232 fiat_p256_subborrowx_u32(&x27, &x28, x26, x11, 0x0); 2233 uint32_t x29; 2234 fiat_p256_uint1 x30; 2235 fiat_p256_subborrowx_u32(&x29, &x30, x28, x13, 0x1); 2236 uint32_t x31; 2237 fiat_p256_uint1 x32; 2238 fiat_p256_subborrowx_u32(&x31, &x32, x30, x15, UINT32_C(0xffffffff)); 2239 uint32_t x33; 2240 fiat_p256_uint1 x34; 2241 fiat_p256_subborrowx_u32(&x33, &x34, x32, x16, 0x0); 2242 uint32_t x35; 2243 fiat_p256_cmovznz_u32(&x35, x34, x17, x1); 2244 uint32_t x36; 2245 fiat_p256_cmovznz_u32(&x36, x34, x19, x3); 2246 uint32_t x37; 2247 fiat_p256_cmovznz_u32(&x37, x34, x21, x5); 2248 uint32_t x38; 2249 fiat_p256_cmovznz_u32(&x38, x34, x23, x7); 2250 uint32_t x39; 2251 fiat_p256_cmovznz_u32(&x39, x34, x25, x9); 2252 uint32_t x40; 2253 fiat_p256_cmovznz_u32(&x40, x34, x27, x11); 2254 uint32_t x41; 2255 fiat_p256_cmovznz_u32(&x41, x34, x29, x13); 2256 uint32_t x42; 2257 fiat_p256_cmovznz_u32(&x42, x34, x31, x15); 2258 out1[0] = x35; 2259 out1[1] = x36; 2260 out1[2] = x37; 2261 out1[3] = x38; 2262 out1[4] = x39; 2263 out1[5] = x40; 2264 out1[6] = x41; 2265 out1[7] = x42; 2266 } 2267 2268 /* 2269 * Input Bounds: 2270 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2271 * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2272 * Output Bounds: 2273 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2274 */ 2275 static void fiat_p256_sub(uint32_t out1[8], const uint32_t arg1[8], const uint32_t arg2[8]) { 2276 uint32_t x1; 2277 fiat_p256_uint1 x2; 2278 fiat_p256_subborrowx_u32(&x1, &x2, 0x0, (arg1[0]), (arg2[0])); 2279 uint32_t x3; 2280 fiat_p256_uint1 x4; 2281 fiat_p256_subborrowx_u32(&x3, &x4, x2, (arg1[1]), (arg2[1])); 2282 uint32_t x5; 2283 fiat_p256_uint1 x6; 2284 fiat_p256_subborrowx_u32(&x5, &x6, x4, (arg1[2]), (arg2[2])); 2285 uint32_t x7; 2286 fiat_p256_uint1 x8; 2287 fiat_p256_subborrowx_u32(&x7, &x8, x6, (arg1[3]), (arg2[3])); 2288 uint32_t x9; 2289 fiat_p256_uint1 x10; 2290 fiat_p256_subborrowx_u32(&x9, &x10, x8, (arg1[4]), (arg2[4])); 2291 uint32_t x11; 2292 fiat_p256_uint1 x12; 2293 fiat_p256_subborrowx_u32(&x11, &x12, x10, (arg1[5]), (arg2[5])); 2294 uint32_t x13; 2295 fiat_p256_uint1 x14; 2296 fiat_p256_subborrowx_u32(&x13, &x14, x12, (arg1[6]), (arg2[6])); 2297 uint32_t x15; 2298 fiat_p256_uint1 x16; 2299 fiat_p256_subborrowx_u32(&x15, &x16, x14, (arg1[7]), (arg2[7])); 2300 uint32_t x17; 2301 fiat_p256_cmovznz_u32(&x17, x16, 0x0, UINT32_C(0xffffffff)); 2302 uint32_t x18; 2303 fiat_p256_uint1 x19; 2304 fiat_p256_addcarryx_u32(&x18, &x19, 0x0, (x17 & UINT32_C(0xffffffff)), x1); 2305 uint32_t x20; 2306 fiat_p256_uint1 x21; 2307 fiat_p256_addcarryx_u32(&x20, &x21, x19, (x17 & UINT32_C(0xffffffff)), x3); 2308 uint32_t x22; 2309 fiat_p256_uint1 x23; 2310 fiat_p256_addcarryx_u32(&x22, &x23, x21, (x17 & UINT32_C(0xffffffff)), x5); 2311 uint32_t x24; 2312 fiat_p256_uint1 x25; 2313 fiat_p256_addcarryx_u32(&x24, &x25, x23, 0x0, x7); 2314 uint32_t x26; 2315 fiat_p256_uint1 x27; 2316 fiat_p256_addcarryx_u32(&x26, &x27, x25, 0x0, x9); 2317 uint32_t x28; 2318 fiat_p256_uint1 x29; 2319 fiat_p256_addcarryx_u32(&x28, &x29, x27, 0x0, x11); 2320 uint32_t x30; 2321 fiat_p256_uint1 x31; 2322 fiat_p256_addcarryx_u32(&x30, &x31, x29, (fiat_p256_uint1)(x17 & 0x1), x13); 2323 uint32_t x32; 2324 fiat_p256_uint1 x33; 2325 fiat_p256_addcarryx_u32(&x32, &x33, x31, (x17 & UINT32_C(0xffffffff)), x15); 2326 out1[0] = x18; 2327 out1[1] = x20; 2328 out1[2] = x22; 2329 out1[3] = x24; 2330 out1[4] = x26; 2331 out1[5] = x28; 2332 out1[6] = x30; 2333 out1[7] = x32; 2334 } 2335 2336 /* 2337 * Input Bounds: 2338 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2339 * Output Bounds: 2340 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2341 */ 2342 static void fiat_p256_opp(uint32_t out1[8], const uint32_t arg1[8]) { 2343 uint32_t x1; 2344 fiat_p256_uint1 x2; 2345 fiat_p256_subborrowx_u32(&x1, &x2, 0x0, 0x0, (arg1[0])); 2346 uint32_t x3; 2347 fiat_p256_uint1 x4; 2348 fiat_p256_subborrowx_u32(&x3, &x4, x2, 0x0, (arg1[1])); 2349 uint32_t x5; 2350 fiat_p256_uint1 x6; 2351 fiat_p256_subborrowx_u32(&x5, &x6, x4, 0x0, (arg1[2])); 2352 uint32_t x7; 2353 fiat_p256_uint1 x8; 2354 fiat_p256_subborrowx_u32(&x7, &x8, x6, 0x0, (arg1[3])); 2355 uint32_t x9; 2356 fiat_p256_uint1 x10; 2357 fiat_p256_subborrowx_u32(&x9, &x10, x8, 0x0, (arg1[4])); 2358 uint32_t x11; 2359 fiat_p256_uint1 x12; 2360 fiat_p256_subborrowx_u32(&x11, &x12, x10, 0x0, (arg1[5])); 2361 uint32_t x13; 2362 fiat_p256_uint1 x14; 2363 fiat_p256_subborrowx_u32(&x13, &x14, x12, 0x0, (arg1[6])); 2364 uint32_t x15; 2365 fiat_p256_uint1 x16; 2366 fiat_p256_subborrowx_u32(&x15, &x16, x14, 0x0, (arg1[7])); 2367 uint32_t x17; 2368 fiat_p256_cmovznz_u32(&x17, x16, 0x0, UINT32_C(0xffffffff)); 2369 uint32_t x18; 2370 fiat_p256_uint1 x19; 2371 fiat_p256_addcarryx_u32(&x18, &x19, 0x0, (x17 & UINT32_C(0xffffffff)), x1); 2372 uint32_t x20; 2373 fiat_p256_uint1 x21; 2374 fiat_p256_addcarryx_u32(&x20, &x21, x19, (x17 & UINT32_C(0xffffffff)), x3); 2375 uint32_t x22; 2376 fiat_p256_uint1 x23; 2377 fiat_p256_addcarryx_u32(&x22, &x23, x21, (x17 & UINT32_C(0xffffffff)), x5); 2378 uint32_t x24; 2379 fiat_p256_uint1 x25; 2380 fiat_p256_addcarryx_u32(&x24, &x25, x23, 0x0, x7); 2381 uint32_t x26; 2382 fiat_p256_uint1 x27; 2383 fiat_p256_addcarryx_u32(&x26, &x27, x25, 0x0, x9); 2384 uint32_t x28; 2385 fiat_p256_uint1 x29; 2386 fiat_p256_addcarryx_u32(&x28, &x29, x27, 0x0, x11); 2387 uint32_t x30; 2388 fiat_p256_uint1 x31; 2389 fiat_p256_addcarryx_u32(&x30, &x31, x29, (fiat_p256_uint1)(x17 & 0x1), x13); 2390 uint32_t x32; 2391 fiat_p256_uint1 x33; 2392 fiat_p256_addcarryx_u32(&x32, &x33, x31, (x17 & UINT32_C(0xffffffff)), x15); 2393 out1[0] = x18; 2394 out1[1] = x20; 2395 out1[2] = x22; 2396 out1[3] = x24; 2397 out1[4] = x26; 2398 out1[5] = x28; 2399 out1[6] = x30; 2400 out1[7] = x32; 2401 } 2402 2403 /* 2404 * Input Bounds: 2405 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2406 * Output Bounds: 2407 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 2408 */ 2409 static void fiat_p256_from_montgomery(uint32_t out1[8], const uint32_t arg1[8]) { 2410 uint32_t x1 = (arg1[0]); 2411 uint32_t x2; 2412 uint32_t x3; 2413 fiat_p256_mulx_u32(&x2, &x3, x1, UINT32_C(0xffffffff)); 2414 uint32_t x4; 2415 uint32_t x5; 2416 fiat_p256_mulx_u32(&x4, &x5, x1, UINT32_C(0xffffffff)); 2417 uint32_t x6; 2418 uint32_t x7; 2419 fiat_p256_mulx_u32(&x6, &x7, x1, UINT32_C(0xffffffff)); 2420 uint32_t x8; 2421 uint32_t x9; 2422 fiat_p256_mulx_u32(&x8, &x9, x1, UINT32_C(0xffffffff)); 2423 uint32_t x10; 2424 fiat_p256_uint1 x11; 2425 fiat_p256_addcarryx_u32(&x10, &x11, 0x0, x6, x9); 2426 uint32_t x12; 2427 fiat_p256_uint1 x13; 2428 fiat_p256_addcarryx_u32(&x12, &x13, x11, x4, x7); 2429 uint32_t x14; 2430 fiat_p256_uint1 x15; 2431 fiat_p256_addcarryx_u32(&x14, &x15, 0x0, x8, x1); 2432 uint32_t x16; 2433 fiat_p256_uint1 x17; 2434 fiat_p256_addcarryx_u32(&x16, &x17, x15, x10, 0x0); 2435 uint32_t x18; 2436 fiat_p256_uint1 x19; 2437 fiat_p256_addcarryx_u32(&x18, &x19, x17, x12, 0x0); 2438 uint32_t x20; 2439 fiat_p256_uint1 x21; 2440 fiat_p256_addcarryx_u32(&x20, &x21, x13, 0x0, x5); 2441 uint32_t x22; 2442 fiat_p256_uint1 x23; 2443 fiat_p256_addcarryx_u32(&x22, &x23, x19, x20, 0x0); 2444 uint32_t x24; 2445 fiat_p256_uint1 x25; 2446 fiat_p256_addcarryx_u32(&x24, &x25, 0x0, (arg1[1]), x16); 2447 uint32_t x26; 2448 fiat_p256_uint1 x27; 2449 fiat_p256_addcarryx_u32(&x26, &x27, x25, 0x0, x18); 2450 uint32_t x28; 2451 fiat_p256_uint1 x29; 2452 fiat_p256_addcarryx_u32(&x28, &x29, x27, 0x0, x22); 2453 uint32_t x30; 2454 uint32_t x31; 2455 fiat_p256_mulx_u32(&x30, &x31, x24, UINT32_C(0xffffffff)); 2456 uint32_t x32; 2457 uint32_t x33; 2458 fiat_p256_mulx_u32(&x32, &x33, x24, UINT32_C(0xffffffff)); 2459 uint32_t x34; 2460 uint32_t x35; 2461 fiat_p256_mulx_u32(&x34, &x35, x24, UINT32_C(0xffffffff)); 2462 uint32_t x36; 2463 uint32_t x37; 2464 fiat_p256_mulx_u32(&x36, &x37, x24, UINT32_C(0xffffffff)); 2465 uint32_t x38; 2466 fiat_p256_uint1 x39; 2467 fiat_p256_addcarryx_u32(&x38, &x39, 0x0, x34, x37); 2468 uint32_t x40; 2469 fiat_p256_uint1 x41; 2470 fiat_p256_addcarryx_u32(&x40, &x41, x39, x32, x35); 2471 uint32_t x42; 2472 fiat_p256_uint1 x43; 2473 fiat_p256_addcarryx_u32(&x42, &x43, 0x0, x36, x24); 2474 uint32_t x44; 2475 fiat_p256_uint1 x45; 2476 fiat_p256_addcarryx_u32(&x44, &x45, x43, x38, x26); 2477 uint32_t x46; 2478 fiat_p256_uint1 x47; 2479 fiat_p256_addcarryx_u32(&x46, &x47, x45, x40, x28); 2480 uint32_t x48; 2481 fiat_p256_uint1 x49; 2482 fiat_p256_addcarryx_u32(&x48, &x49, x23, 0x0, 0x0); 2483 uint32_t x50; 2484 fiat_p256_uint1 x51; 2485 fiat_p256_addcarryx_u32(&x50, &x51, x29, 0x0, (fiat_p256_uint1)x48); 2486 uint32_t x52; 2487 fiat_p256_uint1 x53; 2488 fiat_p256_addcarryx_u32(&x52, &x53, x41, 0x0, x33); 2489 uint32_t x54; 2490 fiat_p256_uint1 x55; 2491 fiat_p256_addcarryx_u32(&x54, &x55, x47, x52, x50); 2492 uint32_t x56; 2493 fiat_p256_uint1 x57; 2494 fiat_p256_addcarryx_u32(&x56, &x57, 0x0, x24, x2); 2495 uint32_t x58; 2496 fiat_p256_uint1 x59; 2497 fiat_p256_addcarryx_u32(&x58, &x59, x57, x30, x3); 2498 uint32_t x60; 2499 fiat_p256_uint1 x61; 2500 fiat_p256_addcarryx_u32(&x60, &x61, 0x0, (arg1[2]), x44); 2501 uint32_t x62; 2502 fiat_p256_uint1 x63; 2503 fiat_p256_addcarryx_u32(&x62, &x63, x61, 0x0, x46); 2504 uint32_t x64; 2505 fiat_p256_uint1 x65; 2506 fiat_p256_addcarryx_u32(&x64, &x65, x63, 0x0, x54); 2507 uint32_t x66; 2508 uint32_t x67; 2509 fiat_p256_mulx_u32(&x66, &x67, x60, UINT32_C(0xffffffff)); 2510 uint32_t x68; 2511 uint32_t x69; 2512 fiat_p256_mulx_u32(&x68, &x69, x60, UINT32_C(0xffffffff)); 2513 uint32_t x70; 2514 uint32_t x71; 2515 fiat_p256_mulx_u32(&x70, &x71, x60, UINT32_C(0xffffffff)); 2516 uint32_t x72; 2517 uint32_t x73; 2518 fiat_p256_mulx_u32(&x72, &x73, x60, UINT32_C(0xffffffff)); 2519 uint32_t x74; 2520 fiat_p256_uint1 x75; 2521 fiat_p256_addcarryx_u32(&x74, &x75, 0x0, x70, x73); 2522 uint32_t x76; 2523 fiat_p256_uint1 x77; 2524 fiat_p256_addcarryx_u32(&x76, &x77, x75, x68, x71); 2525 uint32_t x78; 2526 fiat_p256_uint1 x79; 2527 fiat_p256_addcarryx_u32(&x78, &x79, 0x0, x72, x60); 2528 uint32_t x80; 2529 fiat_p256_uint1 x81; 2530 fiat_p256_addcarryx_u32(&x80, &x81, x79, x74, x62); 2531 uint32_t x82; 2532 fiat_p256_uint1 x83; 2533 fiat_p256_addcarryx_u32(&x82, &x83, x81, x76, x64); 2534 uint32_t x84; 2535 fiat_p256_uint1 x85; 2536 fiat_p256_addcarryx_u32(&x84, &x85, x55, 0x0, 0x0); 2537 uint32_t x86; 2538 fiat_p256_uint1 x87; 2539 fiat_p256_addcarryx_u32(&x86, &x87, x65, 0x0, (fiat_p256_uint1)x84); 2540 uint32_t x88; 2541 fiat_p256_uint1 x89; 2542 fiat_p256_addcarryx_u32(&x88, &x89, x77, 0x0, x69); 2543 uint32_t x90; 2544 fiat_p256_uint1 x91; 2545 fiat_p256_addcarryx_u32(&x90, &x91, x83, x88, x86); 2546 uint32_t x92; 2547 fiat_p256_uint1 x93; 2548 fiat_p256_addcarryx_u32(&x92, &x93, x91, 0x0, x1); 2549 uint32_t x94; 2550 fiat_p256_uint1 x95; 2551 fiat_p256_addcarryx_u32(&x94, &x95, x93, 0x0, x56); 2552 uint32_t x96; 2553 fiat_p256_uint1 x97; 2554 fiat_p256_addcarryx_u32(&x96, &x97, x95, x60, x58); 2555 uint32_t x98; 2556 fiat_p256_uint1 x99; 2557 fiat_p256_addcarryx_u32(&x98, &x99, x59, x31, 0x0); 2558 uint32_t x100; 2559 fiat_p256_uint1 x101; 2560 fiat_p256_addcarryx_u32(&x100, &x101, x97, x66, x98); 2561 uint32_t x102; 2562 fiat_p256_uint1 x103; 2563 fiat_p256_addcarryx_u32(&x102, &x103, 0x0, (arg1[3]), x80); 2564 uint32_t x104; 2565 fiat_p256_uint1 x105; 2566 fiat_p256_addcarryx_u32(&x104, &x105, x103, 0x0, x82); 2567 uint32_t x106; 2568 fiat_p256_uint1 x107; 2569 fiat_p256_addcarryx_u32(&x106, &x107, x105, 0x0, x90); 2570 uint32_t x108; 2571 fiat_p256_uint1 x109; 2572 fiat_p256_addcarryx_u32(&x108, &x109, x107, 0x0, x92); 2573 uint32_t x110; 2574 fiat_p256_uint1 x111; 2575 fiat_p256_addcarryx_u32(&x110, &x111, x109, 0x0, x94); 2576 uint32_t x112; 2577 fiat_p256_uint1 x113; 2578 fiat_p256_addcarryx_u32(&x112, &x113, x111, 0x0, x96); 2579 uint32_t x114; 2580 fiat_p256_uint1 x115; 2581 fiat_p256_addcarryx_u32(&x114, &x115, x113, 0x0, x100); 2582 uint32_t x116; 2583 fiat_p256_uint1 x117; 2584 fiat_p256_addcarryx_u32(&x116, &x117, x101, x67, 0x0); 2585 uint32_t x118; 2586 fiat_p256_uint1 x119; 2587 fiat_p256_addcarryx_u32(&x118, &x119, x115, 0x0, x116); 2588 uint32_t x120; 2589 uint32_t x121; 2590 fiat_p256_mulx_u32(&x120, &x121, x102, UINT32_C(0xffffffff)); 2591 uint32_t x122; 2592 uint32_t x123; 2593 fiat_p256_mulx_u32(&x122, &x123, x102, UINT32_C(0xffffffff)); 2594 uint32_t x124; 2595 uint32_t x125; 2596 fiat_p256_mulx_u32(&x124, &x125, x102, UINT32_C(0xffffffff)); 2597 uint32_t x126; 2598 uint32_t x127; 2599 fiat_p256_mulx_u32(&x126, &x127, x102, UINT32_C(0xffffffff)); 2600 uint32_t x128; 2601 fiat_p256_uint1 x129; 2602 fiat_p256_addcarryx_u32(&x128, &x129, 0x0, x124, x127); 2603 uint32_t x130; 2604 fiat_p256_uint1 x131; 2605 fiat_p256_addcarryx_u32(&x130, &x131, x129, x122, x125); 2606 uint32_t x132; 2607 fiat_p256_uint1 x133; 2608 fiat_p256_addcarryx_u32(&x132, &x133, 0x0, x126, x102); 2609 uint32_t x134; 2610 fiat_p256_uint1 x135; 2611 fiat_p256_addcarryx_u32(&x134, &x135, x133, x128, x104); 2612 uint32_t x136; 2613 fiat_p256_uint1 x137; 2614 fiat_p256_addcarryx_u32(&x136, &x137, x135, x130, x106); 2615 uint32_t x138; 2616 fiat_p256_uint1 x139; 2617 fiat_p256_addcarryx_u32(&x138, &x139, x131, 0x0, x123); 2618 uint32_t x140; 2619 fiat_p256_uint1 x141; 2620 fiat_p256_addcarryx_u32(&x140, &x141, x137, x138, x108); 2621 uint32_t x142; 2622 fiat_p256_uint1 x143; 2623 fiat_p256_addcarryx_u32(&x142, &x143, x141, 0x0, x110); 2624 uint32_t x144; 2625 fiat_p256_uint1 x145; 2626 fiat_p256_addcarryx_u32(&x144, &x145, x143, 0x0, x112); 2627 uint32_t x146; 2628 fiat_p256_uint1 x147; 2629 fiat_p256_addcarryx_u32(&x146, &x147, x145, x102, x114); 2630 uint32_t x148; 2631 fiat_p256_uint1 x149; 2632 fiat_p256_addcarryx_u32(&x148, &x149, x147, x120, x118); 2633 uint32_t x150; 2634 fiat_p256_uint1 x151; 2635 fiat_p256_addcarryx_u32(&x150, &x151, x119, 0x0, 0x0); 2636 uint32_t x152; 2637 fiat_p256_uint1 x153; 2638 fiat_p256_addcarryx_u32(&x152, &x153, x149, x121, (fiat_p256_uint1)x150); 2639 uint32_t x154; 2640 fiat_p256_uint1 x155; 2641 fiat_p256_addcarryx_u32(&x154, &x155, 0x0, (arg1[4]), x134); 2642 uint32_t x156; 2643 fiat_p256_uint1 x157; 2644 fiat_p256_addcarryx_u32(&x156, &x157, x155, 0x0, x136); 2645 uint32_t x158; 2646 fiat_p256_uint1 x159; 2647 fiat_p256_addcarryx_u32(&x158, &x159, x157, 0x0, x140); 2648 uint32_t x160; 2649 fiat_p256_uint1 x161; 2650 fiat_p256_addcarryx_u32(&x160, &x161, x159, 0x0, x142); 2651 uint32_t x162; 2652 fiat_p256_uint1 x163; 2653 fiat_p256_addcarryx_u32(&x162, &x163, x161, 0x0, x144); 2654 uint32_t x164; 2655 fiat_p256_uint1 x165; 2656 fiat_p256_addcarryx_u32(&x164, &x165, x163, 0x0, x146); 2657 uint32_t x166; 2658 fiat_p256_uint1 x167; 2659 fiat_p256_addcarryx_u32(&x166, &x167, x165, 0x0, x148); 2660 uint32_t x168; 2661 fiat_p256_uint1 x169; 2662 fiat_p256_addcarryx_u32(&x168, &x169, x167, 0x0, x152); 2663 uint32_t x170; 2664 uint32_t x171; 2665 fiat_p256_mulx_u32(&x170, &x171, x154, UINT32_C(0xffffffff)); 2666 uint32_t x172; 2667 uint32_t x173; 2668 fiat_p256_mulx_u32(&x172, &x173, x154, UINT32_C(0xffffffff)); 2669 uint32_t x174; 2670 uint32_t x175; 2671 fiat_p256_mulx_u32(&x174, &x175, x154, UINT32_C(0xffffffff)); 2672 uint32_t x176; 2673 uint32_t x177; 2674 fiat_p256_mulx_u32(&x176, &x177, x154, UINT32_C(0xffffffff)); 2675 uint32_t x178; 2676 fiat_p256_uint1 x179; 2677 fiat_p256_addcarryx_u32(&x178, &x179, 0x0, x174, x177); 2678 uint32_t x180; 2679 fiat_p256_uint1 x181; 2680 fiat_p256_addcarryx_u32(&x180, &x181, x179, x172, x175); 2681 uint32_t x182; 2682 fiat_p256_uint1 x183; 2683 fiat_p256_addcarryx_u32(&x182, &x183, 0x0, x176, x154); 2684 uint32_t x184; 2685 fiat_p256_uint1 x185; 2686 fiat_p256_addcarryx_u32(&x184, &x185, x183, x178, x156); 2687 uint32_t x186; 2688 fiat_p256_uint1 x187; 2689 fiat_p256_addcarryx_u32(&x186, &x187, x185, x180, x158); 2690 uint32_t x188; 2691 fiat_p256_uint1 x189; 2692 fiat_p256_addcarryx_u32(&x188, &x189, x181, 0x0, x173); 2693 uint32_t x190; 2694 fiat_p256_uint1 x191; 2695 fiat_p256_addcarryx_u32(&x190, &x191, x187, x188, x160); 2696 uint32_t x192; 2697 fiat_p256_uint1 x193; 2698 fiat_p256_addcarryx_u32(&x192, &x193, x191, 0x0, x162); 2699 uint32_t x194; 2700 fiat_p256_uint1 x195; 2701 fiat_p256_addcarryx_u32(&x194, &x195, x193, 0x0, x164); 2702 uint32_t x196; 2703 fiat_p256_uint1 x197; 2704 fiat_p256_addcarryx_u32(&x196, &x197, x195, x154, x166); 2705 uint32_t x198; 2706 fiat_p256_uint1 x199; 2707 fiat_p256_addcarryx_u32(&x198, &x199, x197, x170, x168); 2708 uint32_t x200; 2709 fiat_p256_uint1 x201; 2710 fiat_p256_addcarryx_u32(&x200, &x201, x153, 0x0, 0x0); 2711 uint32_t x202; 2712 fiat_p256_uint1 x203; 2713 fiat_p256_addcarryx_u32(&x202, &x203, x169, 0x0, (fiat_p256_uint1)x200); 2714 uint32_t x204; 2715 fiat_p256_uint1 x205; 2716 fiat_p256_addcarryx_u32(&x204, &x205, x199, x171, x202); 2717 uint32_t x206; 2718 fiat_p256_uint1 x207; 2719 fiat_p256_addcarryx_u32(&x206, &x207, 0x0, (arg1[5]), x184); 2720 uint32_t x208; 2721 fiat_p256_uint1 x209; 2722 fiat_p256_addcarryx_u32(&x208, &x209, x207, 0x0, x186); 2723 uint32_t x210; 2724 fiat_p256_uint1 x211; 2725 fiat_p256_addcarryx_u32(&x210, &x211, x209, 0x0, x190); 2726 uint32_t x212; 2727 fiat_p256_uint1 x213; 2728 fiat_p256_addcarryx_u32(&x212, &x213, x211, 0x0, x192); 2729 uint32_t x214; 2730 fiat_p256_uint1 x215; 2731 fiat_p256_addcarryx_u32(&x214, &x215, x213, 0x0, x194); 2732 uint32_t x216; 2733 fiat_p256_uint1 x217; 2734 fiat_p256_addcarryx_u32(&x216, &x217, x215, 0x0, x196); 2735 uint32_t x218; 2736 fiat_p256_uint1 x219; 2737 fiat_p256_addcarryx_u32(&x218, &x219, x217, 0x0, x198); 2738 uint32_t x220; 2739 fiat_p256_uint1 x221; 2740 fiat_p256_addcarryx_u32(&x220, &x221, x219, 0x0, x204); 2741 uint32_t x222; 2742 uint32_t x223; 2743 fiat_p256_mulx_u32(&x222, &x223, x206, UINT32_C(0xffffffff)); 2744 uint32_t x224; 2745 uint32_t x225; 2746 fiat_p256_mulx_u32(&x224, &x225, x206, UINT32_C(0xffffffff)); 2747 uint32_t x226; 2748 uint32_t x227; 2749 fiat_p256_mulx_u32(&x226, &x227, x206, UINT32_C(0xffffffff)); 2750 uint32_t x228; 2751 uint32_t x229; 2752 fiat_p256_mulx_u32(&x228, &x229, x206, UINT32_C(0xffffffff)); 2753 uint32_t x230; 2754 fiat_p256_uint1 x231; 2755 fiat_p256_addcarryx_u32(&x230, &x231, 0x0, x226, x229); 2756 uint32_t x232; 2757 fiat_p256_uint1 x233; 2758 fiat_p256_addcarryx_u32(&x232, &x233, x231, x224, x227); 2759 uint32_t x234; 2760 fiat_p256_uint1 x235; 2761 fiat_p256_addcarryx_u32(&x234, &x235, 0x0, x228, x206); 2762 uint32_t x236; 2763 fiat_p256_uint1 x237; 2764 fiat_p256_addcarryx_u32(&x236, &x237, x235, x230, x208); 2765 uint32_t x238; 2766 fiat_p256_uint1 x239; 2767 fiat_p256_addcarryx_u32(&x238, &x239, x237, x232, x210); 2768 uint32_t x240; 2769 fiat_p256_uint1 x241; 2770 fiat_p256_addcarryx_u32(&x240, &x241, x233, 0x0, x225); 2771 uint32_t x242; 2772 fiat_p256_uint1 x243; 2773 fiat_p256_addcarryx_u32(&x242, &x243, x239, x240, x212); 2774 uint32_t x244; 2775 fiat_p256_uint1 x245; 2776 fiat_p256_addcarryx_u32(&x244, &x245, x243, 0x0, x214); 2777 uint32_t x246; 2778 fiat_p256_uint1 x247; 2779 fiat_p256_addcarryx_u32(&x246, &x247, x245, 0x0, x216); 2780 uint32_t x248; 2781 fiat_p256_uint1 x249; 2782 fiat_p256_addcarryx_u32(&x248, &x249, x247, x206, x218); 2783 uint32_t x250; 2784 fiat_p256_uint1 x251; 2785 fiat_p256_addcarryx_u32(&x250, &x251, x249, x222, x220); 2786 uint32_t x252; 2787 fiat_p256_uint1 x253; 2788 fiat_p256_addcarryx_u32(&x252, &x253, x205, 0x0, 0x0); 2789 uint32_t x254; 2790 fiat_p256_uint1 x255; 2791 fiat_p256_addcarryx_u32(&x254, &x255, x221, 0x0, (fiat_p256_uint1)x252); 2792 uint32_t x256; 2793 fiat_p256_uint1 x257; 2794 fiat_p256_addcarryx_u32(&x256, &x257, x251, x223, x254); 2795 uint32_t x258; 2796 fiat_p256_uint1 x259; 2797 fiat_p256_addcarryx_u32(&x258, &x259, 0x0, (arg1[6]), x236); 2798 uint32_t x260; 2799 fiat_p256_uint1 x261; 2800 fiat_p256_addcarryx_u32(&x260, &x261, x259, 0x0, x238); 2801 uint32_t x262; 2802 fiat_p256_uint1 x263; 2803 fiat_p256_addcarryx_u32(&x262, &x263, x261, 0x0, x242); 2804 uint32_t x264; 2805 fiat_p256_uint1 x265; 2806 fiat_p256_addcarryx_u32(&x264, &x265, x263, 0x0, x244); 2807 uint32_t x266; 2808 fiat_p256_uint1 x267; 2809 fiat_p256_addcarryx_u32(&x266, &x267, x265, 0x0, x246); 2810 uint32_t x268; 2811 fiat_p256_uint1 x269; 2812 fiat_p256_addcarryx_u32(&x268, &x269, x267, 0x0, x248); 2813 uint32_t x270; 2814 fiat_p256_uint1 x271; 2815 fiat_p256_addcarryx_u32(&x270, &x271, x269, 0x0, x250); 2816 uint32_t x272; 2817 fiat_p256_uint1 x273; 2818 fiat_p256_addcarryx_u32(&x272, &x273, x271, 0x0, x256); 2819 uint32_t x274; 2820 uint32_t x275; 2821 fiat_p256_mulx_u32(&x274, &x275, x258, UINT32_C(0xffffffff)); 2822 uint32_t x276; 2823 uint32_t x277; 2824 fiat_p256_mulx_u32(&x276, &x277, x258, UINT32_C(0xffffffff)); 2825 uint32_t x278; 2826 uint32_t x279; 2827 fiat_p256_mulx_u32(&x278, &x279, x258, UINT32_C(0xffffffff)); 2828 uint32_t x280; 2829 uint32_t x281; 2830 fiat_p256_mulx_u32(&x280, &x281, x258, UINT32_C(0xffffffff)); 2831 uint32_t x282; 2832 fiat_p256_uint1 x283; 2833 fiat_p256_addcarryx_u32(&x282, &x283, 0x0, x278, x281); 2834 uint32_t x284; 2835 fiat_p256_uint1 x285; 2836 fiat_p256_addcarryx_u32(&x284, &x285, x283, x276, x279); 2837 uint32_t x286; 2838 fiat_p256_uint1 x287; 2839 fiat_p256_addcarryx_u32(&x286, &x287, 0x0, x280, x258); 2840 uint32_t x288; 2841 fiat_p256_uint1 x289; 2842 fiat_p256_addcarryx_u32(&x288, &x289, x287, x282, x260); 2843 uint32_t x290; 2844 fiat_p256_uint1 x291; 2845 fiat_p256_addcarryx_u32(&x290, &x291, x289, x284, x262); 2846 uint32_t x292; 2847 fiat_p256_uint1 x293; 2848 fiat_p256_addcarryx_u32(&x292, &x293, x285, 0x0, x277); 2849 uint32_t x294; 2850 fiat_p256_uint1 x295; 2851 fiat_p256_addcarryx_u32(&x294, &x295, x291, x292, x264); 2852 uint32_t x296; 2853 fiat_p256_uint1 x297; 2854 fiat_p256_addcarryx_u32(&x296, &x297, x295, 0x0, x266); 2855 uint32_t x298; 2856 fiat_p256_uint1 x299; 2857 fiat_p256_addcarryx_u32(&x298, &x299, x297, 0x0, x268); 2858 uint32_t x300; 2859 fiat_p256_uint1 x301; 2860 fiat_p256_addcarryx_u32(&x300, &x301, x299, x258, x270); 2861 uint32_t x302; 2862 fiat_p256_uint1 x303; 2863 fiat_p256_addcarryx_u32(&x302, &x303, x301, x274, x272); 2864 uint32_t x304; 2865 fiat_p256_uint1 x305; 2866 fiat_p256_addcarryx_u32(&x304, &x305, x257, 0x0, 0x0); 2867 uint32_t x306; 2868 fiat_p256_uint1 x307; 2869 fiat_p256_addcarryx_u32(&x306, &x307, x273, 0x0, (fiat_p256_uint1)x304); 2870 uint32_t x308; 2871 fiat_p256_uint1 x309; 2872 fiat_p256_addcarryx_u32(&x308, &x309, x303, x275, x306); 2873 uint32_t x310; 2874 fiat_p256_uint1 x311; 2875 fiat_p256_addcarryx_u32(&x310, &x311, 0x0, (arg1[7]), x288); 2876 uint32_t x312; 2877 fiat_p256_uint1 x313; 2878 fiat_p256_addcarryx_u32(&x312, &x313, x311, 0x0, x290); 2879 uint32_t x314; 2880 fiat_p256_uint1 x315; 2881 fiat_p256_addcarryx_u32(&x314, &x315, x313, 0x0, x294); 2882 uint32_t x316; 2883 fiat_p256_uint1 x317; 2884 fiat_p256_addcarryx_u32(&x316, &x317, x315, 0x0, x296); 2885 uint32_t x318; 2886 fiat_p256_uint1 x319; 2887 fiat_p256_addcarryx_u32(&x318, &x319, x317, 0x0, x298); 2888 uint32_t x320; 2889 fiat_p256_uint1 x321; 2890 fiat_p256_addcarryx_u32(&x320, &x321, x319, 0x0, x300); 2891 uint32_t x322; 2892 fiat_p256_uint1 x323; 2893 fiat_p256_addcarryx_u32(&x322, &x323, x321, 0x0, x302); 2894 uint32_t x324; 2895 fiat_p256_uint1 x325; 2896 fiat_p256_addcarryx_u32(&x324, &x325, x323, 0x0, x308); 2897 uint32_t x326; 2898 uint32_t x327; 2899 fiat_p256_mulx_u32(&x326, &x327, x310, UINT32_C(0xffffffff)); 2900 uint32_t x328; 2901 uint32_t x329; 2902 fiat_p256_mulx_u32(&x328, &x329, x310, UINT32_C(0xffffffff)); 2903 uint32_t x330; 2904 uint32_t x331; 2905 fiat_p256_mulx_u32(&x330, &x331, x310, UINT32_C(0xffffffff)); 2906 uint32_t x332; 2907 uint32_t x333; 2908 fiat_p256_mulx_u32(&x332, &x333, x310, UINT32_C(0xffffffff)); 2909 uint32_t x334; 2910 fiat_p256_uint1 x335; 2911 fiat_p256_addcarryx_u32(&x334, &x335, 0x0, x330, x333); 2912 uint32_t x336; 2913 fiat_p256_uint1 x337; 2914 fiat_p256_addcarryx_u32(&x336, &x337, x335, x328, x331); 2915 uint32_t x338; 2916 fiat_p256_uint1 x339; 2917 fiat_p256_addcarryx_u32(&x338, &x339, 0x0, x332, x310); 2918 uint32_t x340; 2919 fiat_p256_uint1 x341; 2920 fiat_p256_addcarryx_u32(&x340, &x341, x339, x334, x312); 2921 uint32_t x342; 2922 fiat_p256_uint1 x343; 2923 fiat_p256_addcarryx_u32(&x342, &x343, x341, x336, x314); 2924 uint32_t x344; 2925 fiat_p256_uint1 x345; 2926 fiat_p256_addcarryx_u32(&x344, &x345, x337, 0x0, x329); 2927 uint32_t x346; 2928 fiat_p256_uint1 x347; 2929 fiat_p256_addcarryx_u32(&x346, &x347, x343, x344, x316); 2930 uint32_t x348; 2931 fiat_p256_uint1 x349; 2932 fiat_p256_addcarryx_u32(&x348, &x349, x347, 0x0, x318); 2933 uint32_t x350; 2934 fiat_p256_uint1 x351; 2935 fiat_p256_addcarryx_u32(&x350, &x351, x349, 0x0, x320); 2936 uint32_t x352; 2937 fiat_p256_uint1 x353; 2938 fiat_p256_addcarryx_u32(&x352, &x353, x351, x310, x322); 2939 uint32_t x354; 2940 fiat_p256_uint1 x355; 2941 fiat_p256_addcarryx_u32(&x354, &x355, x353, x326, x324); 2942 uint32_t x356; 2943 fiat_p256_uint1 x357; 2944 fiat_p256_addcarryx_u32(&x356, &x357, x309, 0x0, 0x0); 2945 uint32_t x358; 2946 fiat_p256_uint1 x359; 2947 fiat_p256_addcarryx_u32(&x358, &x359, x325, 0x0, (fiat_p256_uint1)x356); 2948 uint32_t x360; 2949 fiat_p256_uint1 x361; 2950 fiat_p256_addcarryx_u32(&x360, &x361, x355, x327, x358); 2951 uint32_t x362; 2952 fiat_p256_uint1 x363; 2953 fiat_p256_subborrowx_u32(&x362, &x363, 0x0, x340, UINT32_C(0xffffffff)); 2954 uint32_t x364; 2955 fiat_p256_uint1 x365; 2956 fiat_p256_subborrowx_u32(&x364, &x365, x363, x342, UINT32_C(0xffffffff)); 2957 uint32_t x366; 2958 fiat_p256_uint1 x367; 2959 fiat_p256_subborrowx_u32(&x366, &x367, x365, x346, UINT32_C(0xffffffff)); 2960 uint32_t x368; 2961 fiat_p256_uint1 x369; 2962 fiat_p256_subborrowx_u32(&x368, &x369, x367, x348, 0x0); 2963 uint32_t x370; 2964 fiat_p256_uint1 x371; 2965 fiat_p256_subborrowx_u32(&x370, &x371, x369, x350, 0x0); 2966 uint32_t x372; 2967 fiat_p256_uint1 x373; 2968 fiat_p256_subborrowx_u32(&x372, &x373, x371, x352, 0x0); 2969 uint32_t x374; 2970 fiat_p256_uint1 x375; 2971 fiat_p256_subborrowx_u32(&x374, &x375, x373, x354, 0x1); 2972 uint32_t x376; 2973 fiat_p256_uint1 x377; 2974 fiat_p256_subborrowx_u32(&x376, &x377, x375, x360, UINT32_C(0xffffffff)); 2975 uint32_t x378; 2976 fiat_p256_uint1 x379; 2977 fiat_p256_addcarryx_u32(&x378, &x379, x361, 0x0, 0x0); 2978 uint32_t x380; 2979 fiat_p256_uint1 x381; 2980 fiat_p256_subborrowx_u32(&x380, &x381, x377, (fiat_p256_uint1)x378, 0x0); 2981 uint32_t x382; 2982 fiat_p256_cmovznz_u32(&x382, x381, x362, x340); 2983 uint32_t x383; 2984 fiat_p256_cmovznz_u32(&x383, x381, x364, x342); 2985 uint32_t x384; 2986 fiat_p256_cmovznz_u32(&x384, x381, x366, x346); 2987 uint32_t x385; 2988 fiat_p256_cmovznz_u32(&x385, x381, x368, x348); 2989 uint32_t x386; 2990 fiat_p256_cmovznz_u32(&x386, x381, x370, x350); 2991 uint32_t x387; 2992 fiat_p256_cmovznz_u32(&x387, x381, x372, x352); 2993 uint32_t x388; 2994 fiat_p256_cmovznz_u32(&x388, x381, x374, x354); 2995 uint32_t x389; 2996 fiat_p256_cmovznz_u32(&x389, x381, x376, x360); 2997 out1[0] = x382; 2998 out1[1] = x383; 2999 out1[2] = x384; 3000 out1[3] = x385; 3001 out1[4] = x386; 3002 out1[5] = x387; 3003 out1[6] = x388; 3004 out1[7] = x389; 3005 } 3006 3007 /* 3008 * Input Bounds: 3009 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 3010 * Output Bounds: 3011 * out1: [0x0 ~> 0xffffffff] 3012 */ 3013 static void fiat_p256_nonzero(uint32_t* out1, const uint32_t arg1[8]) { 3014 uint32_t x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | ((arg1[6]) | ((arg1[7]) | (uint32_t)0x0)))))))); 3015 *out1 = x1; 3016 } 3017 3018 /* 3019 * Input Bounds: 3020 * arg1: [0x0 ~> 0x1] 3021 * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 3022 * arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 3023 * Output Bounds: 3024 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 3025 */ 3026 static void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const uint32_t arg2[8], const uint32_t arg3[8]) { 3027 uint32_t x1; 3028 fiat_p256_cmovznz_u32(&x1, arg1, (arg2[0]), (arg3[0])); 3029 uint32_t x2; 3030 fiat_p256_cmovznz_u32(&x2, arg1, (arg2[1]), (arg3[1])); 3031 uint32_t x3; 3032 fiat_p256_cmovznz_u32(&x3, arg1, (arg2[2]), (arg3[2])); 3033 uint32_t x4; 3034 fiat_p256_cmovznz_u32(&x4, arg1, (arg2[3]), (arg3[3])); 3035 uint32_t x5; 3036 fiat_p256_cmovznz_u32(&x5, arg1, (arg2[4]), (arg3[4])); 3037 uint32_t x6; 3038 fiat_p256_cmovznz_u32(&x6, arg1, (arg2[5]), (arg3[5])); 3039 uint32_t x7; 3040 fiat_p256_cmovznz_u32(&x7, arg1, (arg2[6]), (arg3[6])); 3041 uint32_t x8; 3042 fiat_p256_cmovznz_u32(&x8, arg1, (arg2[7]), (arg3[7])); 3043 out1[0] = x1; 3044 out1[1] = x2; 3045 out1[2] = x3; 3046 out1[3] = x4; 3047 out1[4] = x5; 3048 out1[5] = x6; 3049 out1[6] = x7; 3050 out1[7] = x8; 3051 } 3052 3053 /* 3054 * Input Bounds: 3055 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 3056 * Output Bounds: 3057 * 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 ~> 0xff]] 3058 */ 3059 static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { 3060 uint32_t x1 = (arg1[7]); 3061 uint32_t x2 = (arg1[6]); 3062 uint32_t x3 = (arg1[5]); 3063 uint32_t x4 = (arg1[4]); 3064 uint32_t x5 = (arg1[3]); 3065 uint32_t x6 = (arg1[2]); 3066 uint32_t x7 = (arg1[1]); 3067 uint32_t x8 = (arg1[0]); 3068 uint32_t x9 = (x8 >> 8); 3069 uint8_t x10 = (uint8_t)(x8 & UINT8_C(0xff)); 3070 uint32_t x11 = (x9 >> 8); 3071 uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff)); 3072 uint8_t x13 = (uint8_t)(x11 >> 8); 3073 uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); 3074 uint8_t x15 = (uint8_t)(x13 & UINT8_C(0xff)); 3075 uint32_t x16 = (x7 >> 8); 3076 uint8_t x17 = (uint8_t)(x7 & UINT8_C(0xff)); 3077 uint32_t x18 = (x16 >> 8); 3078 uint8_t x19 = (uint8_t)(x16 & UINT8_C(0xff)); 3079 uint8_t x20 = (uint8_t)(x18 >> 8); 3080 uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); 3081 uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); 3082 uint32_t x23 = (x6 >> 8); 3083 uint8_t x24 = (uint8_t)(x6 & UINT8_C(0xff)); 3084 uint32_t x25 = (x23 >> 8); 3085 uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); 3086 uint8_t x27 = (uint8_t)(x25 >> 8); 3087 uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); 3088 uint8_t x29 = (uint8_t)(x27 & UINT8_C(0xff)); 3089 uint32_t x30 = (x5 >> 8); 3090 uint8_t x31 = (uint8_t)(x5 & UINT8_C(0xff)); 3091 uint32_t x32 = (x30 >> 8); 3092 uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); 3093 uint8_t x34 = (uint8_t)(x32 >> 8); 3094 uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); 3095 uint8_t x36 = (uint8_t)(x34 & UINT8_C(0xff)); 3096 uint32_t x37 = (x4 >> 8); 3097 uint8_t x38 = (uint8_t)(x4 & UINT8_C(0xff)); 3098 uint32_t x39 = (x37 >> 8); 3099 uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); 3100 uint8_t x41 = (uint8_t)(x39 >> 8); 3101 uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); 3102 uint8_t x43 = (uint8_t)(x41 & UINT8_C(0xff)); 3103 uint32_t x44 = (x3 >> 8); 3104 uint8_t x45 = (uint8_t)(x3 & UINT8_C(0xff)); 3105 uint32_t x46 = (x44 >> 8); 3106 uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff)); 3107 uint8_t x48 = (uint8_t)(x46 >> 8); 3108 uint8_t x49 = (uint8_t)(x46 & UINT8_C(0xff)); 3109 uint8_t x50 = (uint8_t)(x48 & UINT8_C(0xff)); 3110 uint32_t x51 = (x2 >> 8); 3111 uint8_t x52 = (uint8_t)(x2 & UINT8_C(0xff)); 3112 uint32_t x53 = (x51 >> 8); 3113 uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff)); 3114 uint8_t x55 = (uint8_t)(x53 >> 8); 3115 uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); 3116 uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff)); 3117 uint32_t x58 = (x1 >> 8); 3118 uint8_t x59 = (uint8_t)(x1 & UINT8_C(0xff)); 3119 uint32_t x60 = (x58 >> 8); 3120 uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); 3121 uint8_t x62 = (uint8_t)(x60 >> 8); 3122 uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); 3123 out1[0] = x10; 3124 out1[1] = x12; 3125 out1[2] = x14; 3126 out1[3] = x15; 3127 out1[4] = x17; 3128 out1[5] = x19; 3129 out1[6] = x21; 3130 out1[7] = x22; 3131 out1[8] = x24; 3132 out1[9] = x26; 3133 out1[10] = x28; 3134 out1[11] = x29; 3135 out1[12] = x31; 3136 out1[13] = x33; 3137 out1[14] = x35; 3138 out1[15] = x36; 3139 out1[16] = x38; 3140 out1[17] = x40; 3141 out1[18] = x42; 3142 out1[19] = x43; 3143 out1[20] = x45; 3144 out1[21] = x47; 3145 out1[22] = x49; 3146 out1[23] = x50; 3147 out1[24] = x52; 3148 out1[25] = x54; 3149 out1[26] = x56; 3150 out1[27] = x57; 3151 out1[28] = x59; 3152 out1[29] = x61; 3153 out1[30] = x63; 3154 out1[31] = x62; 3155 } 3156 3157 /* 3158 * Input Bounds: 3159 * 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 ~> 0xff]] 3160 * Output Bounds: 3161 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 3162 */ 3163 static void fiat_p256_from_bytes(uint32_t out1[8], const uint8_t arg1[32]) { 3164 uint32_t x1 = ((uint32_t)(arg1[31]) << 24); 3165 uint32_t x2 = ((uint32_t)(arg1[30]) << 16); 3166 uint32_t x3 = ((uint32_t)(arg1[29]) << 8); 3167 uint8_t x4 = (arg1[28]); 3168 uint32_t x5 = ((uint32_t)(arg1[27]) << 24); 3169 uint32_t x6 = ((uint32_t)(arg1[26]) << 16); 3170 uint32_t x7 = ((uint32_t)(arg1[25]) << 8); 3171 uint8_t x8 = (arg1[24]); 3172 uint32_t x9 = ((uint32_t)(arg1[23]) << 24); 3173 uint32_t x10 = ((uint32_t)(arg1[22]) << 16); 3174 uint32_t x11 = ((uint32_t)(arg1[21]) << 8); 3175 uint8_t x12 = (arg1[20]); 3176 uint32_t x13 = ((uint32_t)(arg1[19]) << 24); 3177 uint32_t x14 = ((uint32_t)(arg1[18]) << 16); 3178 uint32_t x15 = ((uint32_t)(arg1[17]) << 8); 3179 uint8_t x16 = (arg1[16]); 3180 uint32_t x17 = ((uint32_t)(arg1[15]) << 24); 3181 uint32_t x18 = ((uint32_t)(arg1[14]) << 16); 3182 uint32_t x19 = ((uint32_t)(arg1[13]) << 8); 3183 uint8_t x20 = (arg1[12]); 3184 uint32_t x21 = ((uint32_t)(arg1[11]) << 24); 3185 uint32_t x22 = ((uint32_t)(arg1[10]) << 16); 3186 uint32_t x23 = ((uint32_t)(arg1[9]) << 8); 3187 uint8_t x24 = (arg1[8]); 3188 uint32_t x25 = ((uint32_t)(arg1[7]) << 24); 3189 uint32_t x26 = ((uint32_t)(arg1[6]) << 16); 3190 uint32_t x27 = ((uint32_t)(arg1[5]) << 8); 3191 uint8_t x28 = (arg1[4]); 3192 uint32_t x29 = ((uint32_t)(arg1[3]) << 24); 3193 uint32_t x30 = ((uint32_t)(arg1[2]) << 16); 3194 uint32_t x31 = ((uint32_t)(arg1[1]) << 8); 3195 uint8_t x32 = (arg1[0]); 3196 uint32_t x33 = (x32 + (x31 + (x30 + x29))); 3197 uint32_t x34 = (x33 & UINT32_C(0xffffffff)); 3198 uint32_t x35 = (x4 + (x3 + (x2 + x1))); 3199 uint32_t x36 = (x8 + (x7 + (x6 + x5))); 3200 uint32_t x37 = (x12 + (x11 + (x10 + x9))); 3201 uint32_t x38 = (x16 + (x15 + (x14 + x13))); 3202 uint32_t x39 = (x20 + (x19 + (x18 + x17))); 3203 uint32_t x40 = (x24 + (x23 + (x22 + x21))); 3204 uint32_t x41 = (x28 + (x27 + (x26 + x25))); 3205 uint32_t x42 = (x41 & UINT32_C(0xffffffff)); 3206 uint32_t x43 = (x40 & UINT32_C(0xffffffff)); 3207 uint32_t x44 = (x39 & UINT32_C(0xffffffff)); 3208 uint32_t x45 = (x38 & UINT32_C(0xffffffff)); 3209 uint32_t x46 = (x37 & UINT32_C(0xffffffff)); 3210 uint32_t x47 = (x36 & UINT32_C(0xffffffff)); 3211 out1[0] = x34; 3212 out1[1] = x42; 3213 out1[2] = x43; 3214 out1[3] = x44; 3215 out1[4] = x45; 3216 out1[5] = x46; 3217 out1[6] = x47; 3218 out1[7] = x35; 3219 } 3220 3221
