Robert Sloan | 4c22c5f | 2019-03-01 15:53:37 -0800 | [diff] [blame] | 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)); |
Srinivas Paladugu | dd42a61 | 2019-08-09 19:30:39 +0000 | [diff] [blame^] | 80 | uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); |
Robert Sloan | 4c22c5f | 2019-03-01 15:53:37 -0800 | [diff] [blame] | 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 | |