/* Autogenerated: /src/ExtractionOCaml/word_by_word_montgomery --static p224 32 '2^224 - 2^96 + 1' add sub opp mul square nonzero selectznz to_montgomery from_montgomery to_bytes from_bytes */ /* curve description: p224 */ /* machine_wordsize = 32 (from "32") */ /* requested operations: add, sub, opp, mul, square, nonzero, selectznz, to_montgomery, from_montgomery, to_bytes, from_bytes */ /* m = 0xffffffffffffffffffffffffffffffff000000000000000000000001 (from "2^224 - 2^96 + 1") */ /* */ /* NOTE: In addition to the bounds specified above each function, all */ /* functions synthesized for this Montgomery arithmetic require the */ /* input to be strictly less than the prime modulus (m), and also */ /* require the input to be in the unique saturated representation. */ /* All functions also ensure that these two properties are true of */ /* return values. */ /* */ /* Computed values: */ /* eval z = z[0] + (z[1] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) */ /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) */ #include typedef unsigned char fiat_p224_uint1; typedef signed char fiat_p224_int1; #if (-1 & 3) != 3 #error "This code only works on a two's complement system" #endif /* * The function fiat_p224_addcarryx_u32 is an addition with carry. * Postconditions: * out1 = (arg1 + arg2 + arg3) mod 2^32 * out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋ * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] * arg3: [0x0 ~> 0xffffffff] * Output Bounds: * out1: [0x0 ~> 0xffffffff] * out2: [0x0 ~> 0x1] */ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_p224_uint1 arg1, uint32_t arg2, uint32_t arg3) { uint64_t x1; uint32_t x2; fiat_p224_uint1 x3; x1 = ((arg1 + (uint64_t)arg2) + arg3); x2 = (uint32_t)(x1 & UINT32_C(0xffffffff)); x3 = (fiat_p224_uint1)(x1 >> 32); *out1 = x2; *out2 = x3; } /* * The function fiat_p224_subborrowx_u32 is a subtraction with borrow. * Postconditions: * out1 = (-arg1 + arg2 + -arg3) mod 2^32 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋ * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] * arg3: [0x0 ~> 0xffffffff] * Output Bounds: * out1: [0x0 ~> 0xffffffff] * out2: [0x0 ~> 0x1] */ static void fiat_p224_subborrowx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_p224_uint1 arg1, uint32_t arg2, uint32_t arg3) { int64_t x1; fiat_p224_int1 x2; uint32_t x3; x1 = ((arg2 - (int64_t)arg1) - arg3); x2 = (fiat_p224_int1)(x1 >> 32); x3 = (uint32_t)(x1 & UINT32_C(0xffffffff)); *out1 = x3; *out2 = (fiat_p224_uint1)(0x0 - x2); } /* * The function fiat_p224_mulx_u32 is a multiplication, returning the full double-width result. * Postconditions: * out1 = (arg1 * arg2) mod 2^32 * out2 = ⌊arg1 * arg2 / 2^32⌋ * * Input Bounds: * arg1: [0x0 ~> 0xffffffff] * arg2: [0x0 ~> 0xffffffff] * Output Bounds: * out1: [0x0 ~> 0xffffffff] * out2: [0x0 ~> 0xffffffff] */ static void fiat_p224_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, uint32_t arg2) { uint64_t x1; uint32_t x2; uint32_t x3; x1 = ((uint64_t)arg1 * arg2); x2 = (uint32_t)(x1 & UINT32_C(0xffffffff)); x3 = (uint32_t)(x1 >> 32); *out1 = x2; *out2 = x3; } /* * The function fiat_p224_cmovznz_u32 is a single-word conditional move. * Postconditions: * out1 = (if arg1 = 0 then arg2 else arg3) * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] * arg3: [0x0 ~> 0xffffffff] * Output Bounds: * out1: [0x0 ~> 0xffffffff] */ static void fiat_p224_cmovznz_u32(uint32_t* out1, fiat_p224_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_p224_uint1 x1; uint32_t x2; uint32_t x3; x1 = (!(!arg1)); x2 = ((fiat_p224_int1)(0x0 - x1) & UINT32_C(0xffffffff)); x3 = ((fe_word_barrier(x2) & arg3) | (fe_word_barrier(~x2) & arg2)); *out1 = x3; } /* * The function fiat_p224_add adds two field elements in the Montgomery domain. * Preconditions: * 0 ≤ eval arg1 < m * 0 ≤ eval arg2 < m * Postconditions: * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m * 0 ≤ eval out1 < m * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_add(uint32_t out1[7], const uint32_t arg1[7], const uint32_t arg2[7]) { uint32_t x1; fiat_p224_uint1 x2; uint32_t x3; fiat_p224_uint1 x4; uint32_t x5; fiat_p224_uint1 x6; uint32_t x7; fiat_p224_uint1 x8; uint32_t x9; fiat_p224_uint1 x10; uint32_t x11; fiat_p224_uint1 x12; uint32_t x13; fiat_p224_uint1 x14; uint32_t x15; fiat_p224_uint1 x16; uint32_t x17; fiat_p224_uint1 x18; uint32_t x19; fiat_p224_uint1 x20; uint32_t x21; fiat_p224_uint1 x22; uint32_t x23; fiat_p224_uint1 x24; uint32_t x25; fiat_p224_uint1 x26; uint32_t x27; fiat_p224_uint1 x28; uint32_t x29; fiat_p224_uint1 x30; uint32_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; fiat_p224_addcarryx_u32(&x1, &x2, 0x0, (arg1[0]), (arg2[0])); fiat_p224_addcarryx_u32(&x3, &x4, x2, (arg1[1]), (arg2[1])); fiat_p224_addcarryx_u32(&x5, &x6, x4, (arg1[2]), (arg2[2])); fiat_p224_addcarryx_u32(&x7, &x8, x6, (arg1[3]), (arg2[3])); fiat_p224_addcarryx_u32(&x9, &x10, x8, (arg1[4]), (arg2[4])); fiat_p224_addcarryx_u32(&x11, &x12, x10, (arg1[5]), (arg2[5])); fiat_p224_addcarryx_u32(&x13, &x14, x12, (arg1[6]), (arg2[6])); fiat_p224_subborrowx_u32(&x15, &x16, 0x0, x1, 0x1); fiat_p224_subborrowx_u32(&x17, &x18, x16, x3, 0x0); fiat_p224_subborrowx_u32(&x19, &x20, x18, x5, 0x0); fiat_p224_subborrowx_u32(&x21, &x22, x20, x7, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x23, &x24, x22, x9, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x25, &x26, x24, x11, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x27, &x28, x26, x13, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x29, &x30, x28, x14, 0x0); fiat_p224_cmovznz_u32(&x31, x30, x15, x1); fiat_p224_cmovznz_u32(&x32, x30, x17, x3); fiat_p224_cmovznz_u32(&x33, x30, x19, x5); fiat_p224_cmovznz_u32(&x34, x30, x21, x7); fiat_p224_cmovznz_u32(&x35, x30, x23, x9); fiat_p224_cmovznz_u32(&x36, x30, x25, x11); fiat_p224_cmovznz_u32(&x37, x30, x27, x13); out1[0] = x31; out1[1] = x32; out1[2] = x33; out1[3] = x34; out1[4] = x35; out1[5] = x36; out1[6] = x37; } /* * The function fiat_p224_sub subtracts two field elements in the Montgomery domain. * Preconditions: * 0 ≤ eval arg1 < m * 0 ≤ eval arg2 < m * Postconditions: * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m * 0 ≤ eval out1 < m * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_sub(uint32_t out1[7], const uint32_t arg1[7], const uint32_t arg2[7]) { uint32_t x1; fiat_p224_uint1 x2; uint32_t x3; fiat_p224_uint1 x4; uint32_t x5; fiat_p224_uint1 x6; uint32_t x7; fiat_p224_uint1 x8; uint32_t x9; fiat_p224_uint1 x10; uint32_t x11; fiat_p224_uint1 x12; uint32_t x13; fiat_p224_uint1 x14; uint32_t x15; uint32_t x16; fiat_p224_uint1 x17; uint32_t x18; fiat_p224_uint1 x19; uint32_t x20; fiat_p224_uint1 x21; uint32_t x22; fiat_p224_uint1 x23; uint32_t x24; fiat_p224_uint1 x25; uint32_t x26; fiat_p224_uint1 x27; uint32_t x28; fiat_p224_uint1 x29; fiat_p224_subborrowx_u32(&x1, &x2, 0x0, (arg1[0]), (arg2[0])); fiat_p224_subborrowx_u32(&x3, &x4, x2, (arg1[1]), (arg2[1])); fiat_p224_subborrowx_u32(&x5, &x6, x4, (arg1[2]), (arg2[2])); fiat_p224_subborrowx_u32(&x7, &x8, x6, (arg1[3]), (arg2[3])); fiat_p224_subborrowx_u32(&x9, &x10, x8, (arg1[4]), (arg2[4])); fiat_p224_subborrowx_u32(&x11, &x12, x10, (arg1[5]), (arg2[5])); fiat_p224_subborrowx_u32(&x13, &x14, x12, (arg1[6]), (arg2[6])); fiat_p224_cmovznz_u32(&x15, x14, 0x0, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x16, &x17, 0x0, x1, (fiat_p224_uint1)(x15 & 0x1)); fiat_p224_addcarryx_u32(&x18, &x19, x17, x3, 0x0); fiat_p224_addcarryx_u32(&x20, &x21, x19, x5, 0x0); fiat_p224_addcarryx_u32(&x22, &x23, x21, x7, x15); fiat_p224_addcarryx_u32(&x24, &x25, x23, x9, x15); fiat_p224_addcarryx_u32(&x26, &x27, x25, x11, x15); fiat_p224_addcarryx_u32(&x28, &x29, x27, x13, x15); out1[0] = x16; out1[1] = x18; out1[2] = x20; out1[3] = x22; out1[4] = x24; out1[5] = x26; out1[6] = x28; } /* * The function fiat_p224_opp negates a field element in the Montgomery domain. * Preconditions: * 0 ≤ eval arg1 < m * Postconditions: * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m * 0 ≤ eval out1 < m * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_opp(uint32_t out1[7], const uint32_t arg1[7]) { uint32_t x1; fiat_p224_uint1 x2; uint32_t x3; fiat_p224_uint1 x4; uint32_t x5; fiat_p224_uint1 x6; uint32_t x7; fiat_p224_uint1 x8; uint32_t x9; fiat_p224_uint1 x10; uint32_t x11; fiat_p224_uint1 x12; uint32_t x13; fiat_p224_uint1 x14; uint32_t x15; uint32_t x16; fiat_p224_uint1 x17; uint32_t x18; fiat_p224_uint1 x19; uint32_t x20; fiat_p224_uint1 x21; uint32_t x22; fiat_p224_uint1 x23; uint32_t x24; fiat_p224_uint1 x25; uint32_t x26; fiat_p224_uint1 x27; uint32_t x28; fiat_p224_uint1 x29; fiat_p224_subborrowx_u32(&x1, &x2, 0x0, 0x0, (arg1[0])); fiat_p224_subborrowx_u32(&x3, &x4, x2, 0x0, (arg1[1])); fiat_p224_subborrowx_u32(&x5, &x6, x4, 0x0, (arg1[2])); fiat_p224_subborrowx_u32(&x7, &x8, x6, 0x0, (arg1[3])); fiat_p224_subborrowx_u32(&x9, &x10, x8, 0x0, (arg1[4])); fiat_p224_subborrowx_u32(&x11, &x12, x10, 0x0, (arg1[5])); fiat_p224_subborrowx_u32(&x13, &x14, x12, 0x0, (arg1[6])); fiat_p224_cmovznz_u32(&x15, x14, 0x0, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x16, &x17, 0x0, x1, (fiat_p224_uint1)(x15 & 0x1)); fiat_p224_addcarryx_u32(&x18, &x19, x17, x3, 0x0); fiat_p224_addcarryx_u32(&x20, &x21, x19, x5, 0x0); fiat_p224_addcarryx_u32(&x22, &x23, x21, x7, x15); fiat_p224_addcarryx_u32(&x24, &x25, x23, x9, x15); fiat_p224_addcarryx_u32(&x26, &x27, x25, x11, x15); fiat_p224_addcarryx_u32(&x28, &x29, x27, x13, x15); out1[0] = x16; out1[1] = x18; out1[2] = x20; out1[3] = x22; out1[4] = x24; out1[5] = x26; out1[6] = x28; } /* * The function fiat_p224_mul multiplies two field elements in the Montgomery domain. * Preconditions: * 0 ≤ eval arg1 < m * 0 ≤ eval arg2 < m * Postconditions: * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m * 0 ≤ eval out1 < m * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_mul(uint32_t out1[7], const uint32_t arg1[7], const uint32_t arg2[7]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; fiat_p224_uint1 x23; uint32_t x24; fiat_p224_uint1 x25; uint32_t x26; fiat_p224_uint1 x27; uint32_t x28; fiat_p224_uint1 x29; uint32_t x30; fiat_p224_uint1 x31; uint32_t x32; fiat_p224_uint1 x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; fiat_p224_uint1 x46; uint32_t x47; fiat_p224_uint1 x48; uint32_t x49; fiat_p224_uint1 x50; uint32_t x51; uint32_t x52; fiat_p224_uint1 x53; uint32_t x54; fiat_p224_uint1 x55; uint32_t x56; fiat_p224_uint1 x57; uint32_t x58; fiat_p224_uint1 x59; uint32_t x60; fiat_p224_uint1 x61; uint32_t x62; fiat_p224_uint1 x63; uint32_t x64; fiat_p224_uint1 x65; uint32_t x66; fiat_p224_uint1 x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; uint32_t x74; uint32_t x75; uint32_t x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; uint32_t x81; uint32_t x82; fiat_p224_uint1 x83; uint32_t x84; fiat_p224_uint1 x85; uint32_t x86; fiat_p224_uint1 x87; uint32_t x88; fiat_p224_uint1 x89; uint32_t x90; fiat_p224_uint1 x91; uint32_t x92; fiat_p224_uint1 x93; uint32_t x94; uint32_t x95; fiat_p224_uint1 x96; uint32_t x97; fiat_p224_uint1 x98; uint32_t x99; fiat_p224_uint1 x100; uint32_t x101; fiat_p224_uint1 x102; uint32_t x103; fiat_p224_uint1 x104; uint32_t x105; fiat_p224_uint1 x106; uint32_t x107; fiat_p224_uint1 x108; uint32_t x109; fiat_p224_uint1 x110; uint32_t x111; uint32_t x112; uint32_t x113; uint32_t x114; uint32_t x115; uint32_t x116; uint32_t x117; uint32_t x118; uint32_t x119; uint32_t x120; uint32_t x121; fiat_p224_uint1 x122; uint32_t x123; fiat_p224_uint1 x124; uint32_t x125; fiat_p224_uint1 x126; uint32_t x127; uint32_t x128; fiat_p224_uint1 x129; uint32_t x130; fiat_p224_uint1 x131; uint32_t x132; fiat_p224_uint1 x133; uint32_t x134; fiat_p224_uint1 x135; uint32_t x136; fiat_p224_uint1 x137; uint32_t x138; fiat_p224_uint1 x139; uint32_t x140; fiat_p224_uint1 x141; uint32_t x142; fiat_p224_uint1 x143; uint32_t x144; uint32_t x145; uint32_t x146; uint32_t x147; uint32_t x148; uint32_t x149; uint32_t x150; uint32_t x151; uint32_t x152; uint32_t x153; uint32_t x154; uint32_t x155; uint32_t x156; uint32_t x157; uint32_t x158; uint32_t x159; fiat_p224_uint1 x160; uint32_t x161; fiat_p224_uint1 x162; uint32_t x163; fiat_p224_uint1 x164; uint32_t x165; fiat_p224_uint1 x166; uint32_t x167; fiat_p224_uint1 x168; uint32_t x169; fiat_p224_uint1 x170; uint32_t x171; uint32_t x172; fiat_p224_uint1 x173; uint32_t x174; fiat_p224_uint1 x175; uint32_t x176; fiat_p224_uint1 x177; uint32_t x178; fiat_p224_uint1 x179; uint32_t x180; fiat_p224_uint1 x181; uint32_t x182; fiat_p224_uint1 x183; uint32_t x184; fiat_p224_uint1 x185; uint32_t x186; fiat_p224_uint1 x187; uint32_t x188; uint32_t x189; uint32_t x190; uint32_t x191; uint32_t x192; uint32_t x193; uint32_t x194; uint32_t x195; uint32_t x196; uint32_t x197; uint32_t x198; fiat_p224_uint1 x199; uint32_t x200; fiat_p224_uint1 x201; uint32_t x202; fiat_p224_uint1 x203; uint32_t x204; uint32_t x205; fiat_p224_uint1 x206; uint32_t x207; fiat_p224_uint1 x208; uint32_t x209; fiat_p224_uint1 x210; uint32_t x211; fiat_p224_uint1 x212; uint32_t x213; fiat_p224_uint1 x214; uint32_t x215; fiat_p224_uint1 x216; uint32_t x217; fiat_p224_uint1 x218; uint32_t x219; fiat_p224_uint1 x220; uint32_t x221; uint32_t x222; uint32_t x223; uint32_t x224; uint32_t x225; uint32_t x226; uint32_t x227; uint32_t x228; uint32_t x229; uint32_t x230; uint32_t x231; uint32_t x232; uint32_t x233; uint32_t x234; uint32_t x235; uint32_t x236; fiat_p224_uint1 x237; uint32_t x238; fiat_p224_uint1 x239; uint32_t x240; fiat_p224_uint1 x241; uint32_t x242; fiat_p224_uint1 x243; uint32_t x244; fiat_p224_uint1 x245; uint32_t x246; fiat_p224_uint1 x247; uint32_t x248; uint32_t x249; fiat_p224_uint1 x250; uint32_t x251; fiat_p224_uint1 x252; uint32_t x253; fiat_p224_uint1 x254; uint32_t x255; fiat_p224_uint1 x256; uint32_t x257; fiat_p224_uint1 x258; uint32_t x259; fiat_p224_uint1 x260; uint32_t x261; fiat_p224_uint1 x262; uint32_t x263; fiat_p224_uint1 x264; uint32_t x265; uint32_t x266; uint32_t x267; uint32_t x268; uint32_t x269; uint32_t x270; uint32_t x271; uint32_t x272; uint32_t x273; uint32_t x274; uint32_t x275; fiat_p224_uint1 x276; uint32_t x277; fiat_p224_uint1 x278; uint32_t x279; fiat_p224_uint1 x280; uint32_t x281; uint32_t x282; fiat_p224_uint1 x283; uint32_t x284; fiat_p224_uint1 x285; uint32_t x286; fiat_p224_uint1 x287; uint32_t x288; fiat_p224_uint1 x289; uint32_t x290; fiat_p224_uint1 x291; uint32_t x292; fiat_p224_uint1 x293; uint32_t x294; fiat_p224_uint1 x295; uint32_t x296; fiat_p224_uint1 x297; uint32_t x298; uint32_t x299; uint32_t x300; uint32_t x301; uint32_t x302; uint32_t x303; uint32_t x304; uint32_t x305; uint32_t x306; uint32_t x307; uint32_t x308; uint32_t x309; uint32_t x310; uint32_t x311; uint32_t x312; uint32_t x313; fiat_p224_uint1 x314; uint32_t x315; fiat_p224_uint1 x316; uint32_t x317; fiat_p224_uint1 x318; uint32_t x319; fiat_p224_uint1 x320; uint32_t x321; fiat_p224_uint1 x322; uint32_t x323; fiat_p224_uint1 x324; uint32_t x325; uint32_t x326; fiat_p224_uint1 x327; uint32_t x328; fiat_p224_uint1 x329; uint32_t x330; fiat_p224_uint1 x331; uint32_t x332; fiat_p224_uint1 x333; uint32_t x334; fiat_p224_uint1 x335; uint32_t x336; fiat_p224_uint1 x337; uint32_t x338; fiat_p224_uint1 x339; uint32_t x340; fiat_p224_uint1 x341; uint32_t x342; uint32_t x343; uint32_t x344; uint32_t x345; uint32_t x346; uint32_t x347; uint32_t x348; uint32_t x349; uint32_t x350; uint32_t x351; uint32_t x352; fiat_p224_uint1 x353; uint32_t x354; fiat_p224_uint1 x355; uint32_t x356; fiat_p224_uint1 x357; uint32_t x358; uint32_t x359; fiat_p224_uint1 x360; uint32_t x361; fiat_p224_uint1 x362; uint32_t x363; fiat_p224_uint1 x364; uint32_t x365; fiat_p224_uint1 x366; uint32_t x367; fiat_p224_uint1 x368; uint32_t x369; fiat_p224_uint1 x370; uint32_t x371; fiat_p224_uint1 x372; uint32_t x373; fiat_p224_uint1 x374; uint32_t x375; uint32_t x376; uint32_t x377; uint32_t x378; uint32_t x379; uint32_t x380; uint32_t x381; uint32_t x382; uint32_t x383; uint32_t x384; uint32_t x385; uint32_t x386; uint32_t x387; uint32_t x388; uint32_t x389; uint32_t x390; fiat_p224_uint1 x391; uint32_t x392; fiat_p224_uint1 x393; uint32_t x394; fiat_p224_uint1 x395; uint32_t x396; fiat_p224_uint1 x397; uint32_t x398; fiat_p224_uint1 x399; uint32_t x400; fiat_p224_uint1 x401; uint32_t x402; uint32_t x403; fiat_p224_uint1 x404; uint32_t x405; fiat_p224_uint1 x406; uint32_t x407; fiat_p224_uint1 x408; uint32_t x409; fiat_p224_uint1 x410; uint32_t x411; fiat_p224_uint1 x412; uint32_t x413; fiat_p224_uint1 x414; uint32_t x415; fiat_p224_uint1 x416; uint32_t x417; fiat_p224_uint1 x418; uint32_t x419; uint32_t x420; uint32_t x421; uint32_t x422; uint32_t x423; uint32_t x424; uint32_t x425; uint32_t x426; uint32_t x427; uint32_t x428; uint32_t x429; fiat_p224_uint1 x430; uint32_t x431; fiat_p224_uint1 x432; uint32_t x433; fiat_p224_uint1 x434; uint32_t x435; uint32_t x436; fiat_p224_uint1 x437; uint32_t x438; fiat_p224_uint1 x439; uint32_t x440; fiat_p224_uint1 x441; uint32_t x442; fiat_p224_uint1 x443; uint32_t x444; fiat_p224_uint1 x445; uint32_t x446; fiat_p224_uint1 x447; uint32_t x448; fiat_p224_uint1 x449; uint32_t x450; fiat_p224_uint1 x451; uint32_t x452; uint32_t x453; uint32_t x454; uint32_t x455; uint32_t x456; uint32_t x457; uint32_t x458; uint32_t x459; uint32_t x460; uint32_t x461; uint32_t x462; uint32_t x463; uint32_t x464; uint32_t x465; uint32_t x466; uint32_t x467; fiat_p224_uint1 x468; uint32_t x469; fiat_p224_uint1 x470; uint32_t x471; fiat_p224_uint1 x472; uint32_t x473; fiat_p224_uint1 x474; uint32_t x475; fiat_p224_uint1 x476; uint32_t x477; fiat_p224_uint1 x478; uint32_t x479; uint32_t x480; fiat_p224_uint1 x481; uint32_t x482; fiat_p224_uint1 x483; uint32_t x484; fiat_p224_uint1 x485; uint32_t x486; fiat_p224_uint1 x487; uint32_t x488; fiat_p224_uint1 x489; uint32_t x490; fiat_p224_uint1 x491; uint32_t x492; fiat_p224_uint1 x493; uint32_t x494; fiat_p224_uint1 x495; uint32_t x496; uint32_t x497; uint32_t x498; uint32_t x499; uint32_t x500; uint32_t x501; uint32_t x502; uint32_t x503; uint32_t x504; uint32_t x505; uint32_t x506; fiat_p224_uint1 x507; uint32_t x508; fiat_p224_uint1 x509; uint32_t x510; fiat_p224_uint1 x511; uint32_t x512; uint32_t x513; fiat_p224_uint1 x514; uint32_t x515; fiat_p224_uint1 x516; uint32_t x517; fiat_p224_uint1 x518; uint32_t x519; fiat_p224_uint1 x520; uint32_t x521; fiat_p224_uint1 x522; uint32_t x523; fiat_p224_uint1 x524; uint32_t x525; fiat_p224_uint1 x526; uint32_t x527; fiat_p224_uint1 x528; uint32_t x529; uint32_t x530; fiat_p224_uint1 x531; uint32_t x532; fiat_p224_uint1 x533; uint32_t x534; fiat_p224_uint1 x535; uint32_t x536; fiat_p224_uint1 x537; uint32_t x538; fiat_p224_uint1 x539; uint32_t x540; fiat_p224_uint1 x541; uint32_t x542; fiat_p224_uint1 x543; uint32_t x544; fiat_p224_uint1 x545; uint32_t x546; uint32_t x547; uint32_t x548; uint32_t x549; uint32_t x550; uint32_t x551; uint32_t x552; x1 = (arg1[1]); x2 = (arg1[2]); x3 = (arg1[3]); x4 = (arg1[4]); x5 = (arg1[5]); x6 = (arg1[6]); x7 = (arg1[0]); fiat_p224_mulx_u32(&x8, &x9, x7, (arg2[6])); fiat_p224_mulx_u32(&x10, &x11, x7, (arg2[5])); fiat_p224_mulx_u32(&x12, &x13, x7, (arg2[4])); fiat_p224_mulx_u32(&x14, &x15, x7, (arg2[3])); fiat_p224_mulx_u32(&x16, &x17, x7, (arg2[2])); fiat_p224_mulx_u32(&x18, &x19, x7, (arg2[1])); fiat_p224_mulx_u32(&x20, &x21, x7, (arg2[0])); fiat_p224_addcarryx_u32(&x22, &x23, 0x0, x21, x18); fiat_p224_addcarryx_u32(&x24, &x25, x23, x19, x16); fiat_p224_addcarryx_u32(&x26, &x27, x25, x17, x14); fiat_p224_addcarryx_u32(&x28, &x29, x27, x15, x12); fiat_p224_addcarryx_u32(&x30, &x31, x29, x13, x10); fiat_p224_addcarryx_u32(&x32, &x33, x31, x11, x8); x34 = (x33 + x9); fiat_p224_mulx_u32(&x35, &x36, x20, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x37, &x38, x35, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x39, &x40, x35, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x41, &x42, x35, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x43, &x44, x35, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x45, &x46, 0x0, x44, x41); fiat_p224_addcarryx_u32(&x47, &x48, x46, x42, x39); fiat_p224_addcarryx_u32(&x49, &x50, x48, x40, x37); x51 = (x50 + x38); fiat_p224_addcarryx_u32(&x52, &x53, 0x0, x20, x35); fiat_p224_addcarryx_u32(&x54, &x55, x53, x22, 0x0); fiat_p224_addcarryx_u32(&x56, &x57, x55, x24, 0x0); fiat_p224_addcarryx_u32(&x58, &x59, x57, x26, x43); fiat_p224_addcarryx_u32(&x60, &x61, x59, x28, x45); fiat_p224_addcarryx_u32(&x62, &x63, x61, x30, x47); fiat_p224_addcarryx_u32(&x64, &x65, x63, x32, x49); fiat_p224_addcarryx_u32(&x66, &x67, x65, x34, x51); fiat_p224_mulx_u32(&x68, &x69, x1, (arg2[6])); fiat_p224_mulx_u32(&x70, &x71, x1, (arg2[5])); fiat_p224_mulx_u32(&x72, &x73, x1, (arg2[4])); fiat_p224_mulx_u32(&x74, &x75, x1, (arg2[3])); fiat_p224_mulx_u32(&x76, &x77, x1, (arg2[2])); fiat_p224_mulx_u32(&x78, &x79, x1, (arg2[1])); fiat_p224_mulx_u32(&x80, &x81, x1, (arg2[0])); fiat_p224_addcarryx_u32(&x82, &x83, 0x0, x81, x78); fiat_p224_addcarryx_u32(&x84, &x85, x83, x79, x76); fiat_p224_addcarryx_u32(&x86, &x87, x85, x77, x74); fiat_p224_addcarryx_u32(&x88, &x89, x87, x75, x72); fiat_p224_addcarryx_u32(&x90, &x91, x89, x73, x70); fiat_p224_addcarryx_u32(&x92, &x93, x91, x71, x68); x94 = (x93 + x69); fiat_p224_addcarryx_u32(&x95, &x96, 0x0, x54, x80); fiat_p224_addcarryx_u32(&x97, &x98, x96, x56, x82); fiat_p224_addcarryx_u32(&x99, &x100, x98, x58, x84); fiat_p224_addcarryx_u32(&x101, &x102, x100, x60, x86); fiat_p224_addcarryx_u32(&x103, &x104, x102, x62, x88); fiat_p224_addcarryx_u32(&x105, &x106, x104, x64, x90); fiat_p224_addcarryx_u32(&x107, &x108, x106, x66, x92); fiat_p224_addcarryx_u32(&x109, &x110, x108, x67, x94); fiat_p224_mulx_u32(&x111, &x112, x95, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x113, &x114, x111, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x115, &x116, x111, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x117, &x118, x111, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x119, &x120, x111, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x121, &x122, 0x0, x120, x117); fiat_p224_addcarryx_u32(&x123, &x124, x122, x118, x115); fiat_p224_addcarryx_u32(&x125, &x126, x124, x116, x113); x127 = (x126 + x114); fiat_p224_addcarryx_u32(&x128, &x129, 0x0, x95, x111); fiat_p224_addcarryx_u32(&x130, &x131, x129, x97, 0x0); fiat_p224_addcarryx_u32(&x132, &x133, x131, x99, 0x0); fiat_p224_addcarryx_u32(&x134, &x135, x133, x101, x119); fiat_p224_addcarryx_u32(&x136, &x137, x135, x103, x121); fiat_p224_addcarryx_u32(&x138, &x139, x137, x105, x123); fiat_p224_addcarryx_u32(&x140, &x141, x139, x107, x125); fiat_p224_addcarryx_u32(&x142, &x143, x141, x109, x127); x144 = ((uint32_t)x143 + x110); fiat_p224_mulx_u32(&x145, &x146, x2, (arg2[6])); fiat_p224_mulx_u32(&x147, &x148, x2, (arg2[5])); fiat_p224_mulx_u32(&x149, &x150, x2, (arg2[4])); fiat_p224_mulx_u32(&x151, &x152, x2, (arg2[3])); fiat_p224_mulx_u32(&x153, &x154, x2, (arg2[2])); fiat_p224_mulx_u32(&x155, &x156, x2, (arg2[1])); fiat_p224_mulx_u32(&x157, &x158, x2, (arg2[0])); fiat_p224_addcarryx_u32(&x159, &x160, 0x0, x158, x155); fiat_p224_addcarryx_u32(&x161, &x162, x160, x156, x153); fiat_p224_addcarryx_u32(&x163, &x164, x162, x154, x151); fiat_p224_addcarryx_u32(&x165, &x166, x164, x152, x149); fiat_p224_addcarryx_u32(&x167, &x168, x166, x150, x147); fiat_p224_addcarryx_u32(&x169, &x170, x168, x148, x145); x171 = (x170 + x146); fiat_p224_addcarryx_u32(&x172, &x173, 0x0, x130, x157); fiat_p224_addcarryx_u32(&x174, &x175, x173, x132, x159); fiat_p224_addcarryx_u32(&x176, &x177, x175, x134, x161); fiat_p224_addcarryx_u32(&x178, &x179, x177, x136, x163); fiat_p224_addcarryx_u32(&x180, &x181, x179, x138, x165); fiat_p224_addcarryx_u32(&x182, &x183, x181, x140, x167); fiat_p224_addcarryx_u32(&x184, &x185, x183, x142, x169); fiat_p224_addcarryx_u32(&x186, &x187, x185, x144, x171); fiat_p224_mulx_u32(&x188, &x189, x172, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x190, &x191, x188, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x192, &x193, x188, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x194, &x195, x188, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x196, &x197, x188, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x198, &x199, 0x0, x197, x194); fiat_p224_addcarryx_u32(&x200, &x201, x199, x195, x192); fiat_p224_addcarryx_u32(&x202, &x203, x201, x193, x190); x204 = (x203 + x191); fiat_p224_addcarryx_u32(&x205, &x206, 0x0, x172, x188); fiat_p224_addcarryx_u32(&x207, &x208, x206, x174, 0x0); fiat_p224_addcarryx_u32(&x209, &x210, x208, x176, 0x0); fiat_p224_addcarryx_u32(&x211, &x212, x210, x178, x196); fiat_p224_addcarryx_u32(&x213, &x214, x212, x180, x198); fiat_p224_addcarryx_u32(&x215, &x216, x214, x182, x200); fiat_p224_addcarryx_u32(&x217, &x218, x216, x184, x202); fiat_p224_addcarryx_u32(&x219, &x220, x218, x186, x204); x221 = ((uint32_t)x220 + x187); fiat_p224_mulx_u32(&x222, &x223, x3, (arg2[6])); fiat_p224_mulx_u32(&x224, &x225, x3, (arg2[5])); fiat_p224_mulx_u32(&x226, &x227, x3, (arg2[4])); fiat_p224_mulx_u32(&x228, &x229, x3, (arg2[3])); fiat_p224_mulx_u32(&x230, &x231, x3, (arg2[2])); fiat_p224_mulx_u32(&x232, &x233, x3, (arg2[1])); fiat_p224_mulx_u32(&x234, &x235, x3, (arg2[0])); fiat_p224_addcarryx_u32(&x236, &x237, 0x0, x235, x232); fiat_p224_addcarryx_u32(&x238, &x239, x237, x233, x230); fiat_p224_addcarryx_u32(&x240, &x241, x239, x231, x228); fiat_p224_addcarryx_u32(&x242, &x243, x241, x229, x226); fiat_p224_addcarryx_u32(&x244, &x245, x243, x227, x224); fiat_p224_addcarryx_u32(&x246, &x247, x245, x225, x222); x248 = (x247 + x223); fiat_p224_addcarryx_u32(&x249, &x250, 0x0, x207, x234); fiat_p224_addcarryx_u32(&x251, &x252, x250, x209, x236); fiat_p224_addcarryx_u32(&x253, &x254, x252, x211, x238); fiat_p224_addcarryx_u32(&x255, &x256, x254, x213, x240); fiat_p224_addcarryx_u32(&x257, &x258, x256, x215, x242); fiat_p224_addcarryx_u32(&x259, &x260, x258, x217, x244); fiat_p224_addcarryx_u32(&x261, &x262, x260, x219, x246); fiat_p224_addcarryx_u32(&x263, &x264, x262, x221, x248); fiat_p224_mulx_u32(&x265, &x266, x249, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x267, &x268, x265, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x269, &x270, x265, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x271, &x272, x265, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x273, &x274, x265, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x275, &x276, 0x0, x274, x271); fiat_p224_addcarryx_u32(&x277, &x278, x276, x272, x269); fiat_p224_addcarryx_u32(&x279, &x280, x278, x270, x267); x281 = (x280 + x268); fiat_p224_addcarryx_u32(&x282, &x283, 0x0, x249, x265); fiat_p224_addcarryx_u32(&x284, &x285, x283, x251, 0x0); fiat_p224_addcarryx_u32(&x286, &x287, x285, x253, 0x0); fiat_p224_addcarryx_u32(&x288, &x289, x287, x255, x273); fiat_p224_addcarryx_u32(&x290, &x291, x289, x257, x275); fiat_p224_addcarryx_u32(&x292, &x293, x291, x259, x277); fiat_p224_addcarryx_u32(&x294, &x295, x293, x261, x279); fiat_p224_addcarryx_u32(&x296, &x297, x295, x263, x281); x298 = ((uint32_t)x297 + x264); fiat_p224_mulx_u32(&x299, &x300, x4, (arg2[6])); fiat_p224_mulx_u32(&x301, &x302, x4, (arg2[5])); fiat_p224_mulx_u32(&x303, &x304, x4, (arg2[4])); fiat_p224_mulx_u32(&x305, &x306, x4, (arg2[3])); fiat_p224_mulx_u32(&x307, &x308, x4, (arg2[2])); fiat_p224_mulx_u32(&x309, &x310, x4, (arg2[1])); fiat_p224_mulx_u32(&x311, &x312, x4, (arg2[0])); fiat_p224_addcarryx_u32(&x313, &x314, 0x0, x312, x309); fiat_p224_addcarryx_u32(&x315, &x316, x314, x310, x307); fiat_p224_addcarryx_u32(&x317, &x318, x316, x308, x305); fiat_p224_addcarryx_u32(&x319, &x320, x318, x306, x303); fiat_p224_addcarryx_u32(&x321, &x322, x320, x304, x301); fiat_p224_addcarryx_u32(&x323, &x324, x322, x302, x299); x325 = (x324 + x300); fiat_p224_addcarryx_u32(&x326, &x327, 0x0, x284, x311); fiat_p224_addcarryx_u32(&x328, &x329, x327, x286, x313); fiat_p224_addcarryx_u32(&x330, &x331, x329, x288, x315); fiat_p224_addcarryx_u32(&x332, &x333, x331, x290, x317); fiat_p224_addcarryx_u32(&x334, &x335, x333, x292, x319); fiat_p224_addcarryx_u32(&x336, &x337, x335, x294, x321); fiat_p224_addcarryx_u32(&x338, &x339, x337, x296, x323); fiat_p224_addcarryx_u32(&x340, &x341, x339, x298, x325); fiat_p224_mulx_u32(&x342, &x343, x326, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x344, &x345, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x346, &x347, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x348, &x349, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x350, &x351, x342, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x352, &x353, 0x0, x351, x348); fiat_p224_addcarryx_u32(&x354, &x355, x353, x349, x346); fiat_p224_addcarryx_u32(&x356, &x357, x355, x347, x344); x358 = (x357 + x345); fiat_p224_addcarryx_u32(&x359, &x360, 0x0, x326, x342); fiat_p224_addcarryx_u32(&x361, &x362, x360, x328, 0x0); fiat_p224_addcarryx_u32(&x363, &x364, x362, x330, 0x0); fiat_p224_addcarryx_u32(&x365, &x366, x364, x332, x350); fiat_p224_addcarryx_u32(&x367, &x368, x366, x334, x352); fiat_p224_addcarryx_u32(&x369, &x370, x368, x336, x354); fiat_p224_addcarryx_u32(&x371, &x372, x370, x338, x356); fiat_p224_addcarryx_u32(&x373, &x374, x372, x340, x358); x375 = ((uint32_t)x374 + x341); fiat_p224_mulx_u32(&x376, &x377, x5, (arg2[6])); fiat_p224_mulx_u32(&x378, &x379, x5, (arg2[5])); fiat_p224_mulx_u32(&x380, &x381, x5, (arg2[4])); fiat_p224_mulx_u32(&x382, &x383, x5, (arg2[3])); fiat_p224_mulx_u32(&x384, &x385, x5, (arg2[2])); fiat_p224_mulx_u32(&x386, &x387, x5, (arg2[1])); fiat_p224_mulx_u32(&x388, &x389, x5, (arg2[0])); fiat_p224_addcarryx_u32(&x390, &x391, 0x0, x389, x386); fiat_p224_addcarryx_u32(&x392, &x393, x391, x387, x384); fiat_p224_addcarryx_u32(&x394, &x395, x393, x385, x382); fiat_p224_addcarryx_u32(&x396, &x397, x395, x383, x380); fiat_p224_addcarryx_u32(&x398, &x399, x397, x381, x378); fiat_p224_addcarryx_u32(&x400, &x401, x399, x379, x376); x402 = (x401 + x377); fiat_p224_addcarryx_u32(&x403, &x404, 0x0, x361, x388); fiat_p224_addcarryx_u32(&x405, &x406, x404, x363, x390); fiat_p224_addcarryx_u32(&x407, &x408, x406, x365, x392); fiat_p224_addcarryx_u32(&x409, &x410, x408, x367, x394); fiat_p224_addcarryx_u32(&x411, &x412, x410, x369, x396); fiat_p224_addcarryx_u32(&x413, &x414, x412, x371, x398); fiat_p224_addcarryx_u32(&x415, &x416, x414, x373, x400); fiat_p224_addcarryx_u32(&x417, &x418, x416, x375, x402); fiat_p224_mulx_u32(&x419, &x420, x403, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x421, &x422, x419, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x423, &x424, x419, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x425, &x426, x419, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x427, &x428, x419, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x429, &x430, 0x0, x428, x425); fiat_p224_addcarryx_u32(&x431, &x432, x430, x426, x423); fiat_p224_addcarryx_u32(&x433, &x434, x432, x424, x421); x435 = (x434 + x422); fiat_p224_addcarryx_u32(&x436, &x437, 0x0, x403, x419); fiat_p224_addcarryx_u32(&x438, &x439, x437, x405, 0x0); fiat_p224_addcarryx_u32(&x440, &x441, x439, x407, 0x0); fiat_p224_addcarryx_u32(&x442, &x443, x441, x409, x427); fiat_p224_addcarryx_u32(&x444, &x445, x443, x411, x429); fiat_p224_addcarryx_u32(&x446, &x447, x445, x413, x431); fiat_p224_addcarryx_u32(&x448, &x449, x447, x415, x433); fiat_p224_addcarryx_u32(&x450, &x451, x449, x417, x435); x452 = ((uint32_t)x451 + x418); fiat_p224_mulx_u32(&x453, &x454, x6, (arg2[6])); fiat_p224_mulx_u32(&x455, &x456, x6, (arg2[5])); fiat_p224_mulx_u32(&x457, &x458, x6, (arg2[4])); fiat_p224_mulx_u32(&x459, &x460, x6, (arg2[3])); fiat_p224_mulx_u32(&x461, &x462, x6, (arg2[2])); fiat_p224_mulx_u32(&x463, &x464, x6, (arg2[1])); fiat_p224_mulx_u32(&x465, &x466, x6, (arg2[0])); fiat_p224_addcarryx_u32(&x467, &x468, 0x0, x466, x463); fiat_p224_addcarryx_u32(&x469, &x470, x468, x464, x461); fiat_p224_addcarryx_u32(&x471, &x472, x470, x462, x459); fiat_p224_addcarryx_u32(&x473, &x474, x472, x460, x457); fiat_p224_addcarryx_u32(&x475, &x476, x474, x458, x455); fiat_p224_addcarryx_u32(&x477, &x478, x476, x456, x453); x479 = (x478 + x454); fiat_p224_addcarryx_u32(&x480, &x481, 0x0, x438, x465); fiat_p224_addcarryx_u32(&x482, &x483, x481, x440, x467); fiat_p224_addcarryx_u32(&x484, &x485, x483, x442, x469); fiat_p224_addcarryx_u32(&x486, &x487, x485, x444, x471); fiat_p224_addcarryx_u32(&x488, &x489, x487, x446, x473); fiat_p224_addcarryx_u32(&x490, &x491, x489, x448, x475); fiat_p224_addcarryx_u32(&x492, &x493, x491, x450, x477); fiat_p224_addcarryx_u32(&x494, &x495, x493, x452, x479); fiat_p224_mulx_u32(&x496, &x497, x480, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x498, &x499, x496, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x500, &x501, x496, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x502, &x503, x496, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x504, &x505, x496, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x506, &x507, 0x0, x505, x502); fiat_p224_addcarryx_u32(&x508, &x509, x507, x503, x500); fiat_p224_addcarryx_u32(&x510, &x511, x509, x501, x498); x512 = (x511 + x499); fiat_p224_addcarryx_u32(&x513, &x514, 0x0, x480, x496); fiat_p224_addcarryx_u32(&x515, &x516, x514, x482, 0x0); fiat_p224_addcarryx_u32(&x517, &x518, x516, x484, 0x0); fiat_p224_addcarryx_u32(&x519, &x520, x518, x486, x504); fiat_p224_addcarryx_u32(&x521, &x522, x520, x488, x506); fiat_p224_addcarryx_u32(&x523, &x524, x522, x490, x508); fiat_p224_addcarryx_u32(&x525, &x526, x524, x492, x510); fiat_p224_addcarryx_u32(&x527, &x528, x526, x494, x512); x529 = ((uint32_t)x528 + x495); fiat_p224_subborrowx_u32(&x530, &x531, 0x0, x515, 0x1); fiat_p224_subborrowx_u32(&x532, &x533, x531, x517, 0x0); fiat_p224_subborrowx_u32(&x534, &x535, x533, x519, 0x0); fiat_p224_subborrowx_u32(&x536, &x537, x535, x521, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x538, &x539, x537, x523, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x540, &x541, x539, x525, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x542, &x543, x541, x527, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x544, &x545, x543, x529, 0x0); fiat_p224_cmovznz_u32(&x546, x545, x530, x515); fiat_p224_cmovznz_u32(&x547, x545, x532, x517); fiat_p224_cmovznz_u32(&x548, x545, x534, x519); fiat_p224_cmovznz_u32(&x549, x545, x536, x521); fiat_p224_cmovznz_u32(&x550, x545, x538, x523); fiat_p224_cmovznz_u32(&x551, x545, x540, x525); fiat_p224_cmovznz_u32(&x552, x545, x542, x527); out1[0] = x546; out1[1] = x547; out1[2] = x548; out1[3] = x549; out1[4] = x550; out1[5] = x551; out1[6] = x552; } /* * The function fiat_p224_square squares a field element in the Montgomery domain. * Preconditions: * 0 ≤ eval arg1 < m * Postconditions: * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m * 0 ≤ eval out1 < m * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_square(uint32_t out1[7], const uint32_t arg1[7]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; fiat_p224_uint1 x23; uint32_t x24; fiat_p224_uint1 x25; uint32_t x26; fiat_p224_uint1 x27; uint32_t x28; fiat_p224_uint1 x29; uint32_t x30; fiat_p224_uint1 x31; uint32_t x32; fiat_p224_uint1 x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; fiat_p224_uint1 x46; uint32_t x47; fiat_p224_uint1 x48; uint32_t x49; fiat_p224_uint1 x50; uint32_t x51; uint32_t x52; fiat_p224_uint1 x53; uint32_t x54; fiat_p224_uint1 x55; uint32_t x56; fiat_p224_uint1 x57; uint32_t x58; fiat_p224_uint1 x59; uint32_t x60; fiat_p224_uint1 x61; uint32_t x62; fiat_p224_uint1 x63; uint32_t x64; fiat_p224_uint1 x65; uint32_t x66; fiat_p224_uint1 x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; uint32_t x74; uint32_t x75; uint32_t x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; uint32_t x81; uint32_t x82; fiat_p224_uint1 x83; uint32_t x84; fiat_p224_uint1 x85; uint32_t x86; fiat_p224_uint1 x87; uint32_t x88; fiat_p224_uint1 x89; uint32_t x90; fiat_p224_uint1 x91; uint32_t x92; fiat_p224_uint1 x93; uint32_t x94; uint32_t x95; fiat_p224_uint1 x96; uint32_t x97; fiat_p224_uint1 x98; uint32_t x99; fiat_p224_uint1 x100; uint32_t x101; fiat_p224_uint1 x102; uint32_t x103; fiat_p224_uint1 x104; uint32_t x105; fiat_p224_uint1 x106; uint32_t x107; fiat_p224_uint1 x108; uint32_t x109; fiat_p224_uint1 x110; uint32_t x111; uint32_t x112; uint32_t x113; uint32_t x114; uint32_t x115; uint32_t x116; uint32_t x117; uint32_t x118; uint32_t x119; uint32_t x120; uint32_t x121; fiat_p224_uint1 x122; uint32_t x123; fiat_p224_uint1 x124; uint32_t x125; fiat_p224_uint1 x126; uint32_t x127; uint32_t x128; fiat_p224_uint1 x129; uint32_t x130; fiat_p224_uint1 x131; uint32_t x132; fiat_p224_uint1 x133; uint32_t x134; fiat_p224_uint1 x135; uint32_t x136; fiat_p224_uint1 x137; uint32_t x138; fiat_p224_uint1 x139; uint32_t x140; fiat_p224_uint1 x141; uint32_t x142; fiat_p224_uint1 x143; uint32_t x144; uint32_t x145; uint32_t x146; uint32_t x147; uint32_t x148; uint32_t x149; uint32_t x150; uint32_t x151; uint32_t x152; uint32_t x153; uint32_t x154; uint32_t x155; uint32_t x156; uint32_t x157; uint32_t x158; uint32_t x159; fiat_p224_uint1 x160; uint32_t x161; fiat_p224_uint1 x162; uint32_t x163; fiat_p224_uint1 x164; uint32_t x165; fiat_p224_uint1 x166; uint32_t x167; fiat_p224_uint1 x168; uint32_t x169; fiat_p224_uint1 x170; uint32_t x171; uint32_t x172; fiat_p224_uint1 x173; uint32_t x174; fiat_p224_uint1 x175; uint32_t x176; fiat_p224_uint1 x177; uint32_t x178; fiat_p224_uint1 x179; uint32_t x180; fiat_p224_uint1 x181; uint32_t x182; fiat_p224_uint1 x183; uint32_t x184; fiat_p224_uint1 x185; uint32_t x186; fiat_p224_uint1 x187; uint32_t x188; uint32_t x189; uint32_t x190; uint32_t x191; uint32_t x192; uint32_t x193; uint32_t x194; uint32_t x195; uint32_t x196; uint32_t x197; uint32_t x198; fiat_p224_uint1 x199; uint32_t x200; fiat_p224_uint1 x201; uint32_t x202; fiat_p224_uint1 x203; uint32_t x204; uint32_t x205; fiat_p224_uint1 x206; uint32_t x207; fiat_p224_uint1 x208; uint32_t x209; fiat_p224_uint1 x210; uint32_t x211; fiat_p224_uint1 x212; uint32_t x213; fiat_p224_uint1 x214; uint32_t x215; fiat_p224_uint1 x216; uint32_t x217; fiat_p224_uint1 x218; uint32_t x219; fiat_p224_uint1 x220; uint32_t x221; uint32_t x222; uint32_t x223; uint32_t x224; uint32_t x225; uint32_t x226; uint32_t x227; uint32_t x228; uint32_t x229; uint32_t x230; uint32_t x231; uint32_t x232; uint32_t x233; uint32_t x234; uint32_t x235; uint32_t x236; fiat_p224_uint1 x237; uint32_t x238; fiat_p224_uint1 x239; uint32_t x240; fiat_p224_uint1 x241; uint32_t x242; fiat_p224_uint1 x243; uint32_t x244; fiat_p224_uint1 x245; uint32_t x246; fiat_p224_uint1 x247; uint32_t x248; uint32_t x249; fiat_p224_uint1 x250; uint32_t x251; fiat_p224_uint1 x252; uint32_t x253; fiat_p224_uint1 x254; uint32_t x255; fiat_p224_uint1 x256; uint32_t x257; fiat_p224_uint1 x258; uint32_t x259; fiat_p224_uint1 x260; uint32_t x261; fiat_p224_uint1 x262; uint32_t x263; fiat_p224_uint1 x264; uint32_t x265; uint32_t x266; uint32_t x267; uint32_t x268; uint32_t x269; uint32_t x270; uint32_t x271; uint32_t x272; uint32_t x273; uint32_t x274; uint32_t x275; fiat_p224_uint1 x276; uint32_t x277; fiat_p224_uint1 x278; uint32_t x279; fiat_p224_uint1 x280; uint32_t x281; uint32_t x282; fiat_p224_uint1 x283; uint32_t x284; fiat_p224_uint1 x285; uint32_t x286; fiat_p224_uint1 x287; uint32_t x288; fiat_p224_uint1 x289; uint32_t x290; fiat_p224_uint1 x291; uint32_t x292; fiat_p224_uint1 x293; uint32_t x294; fiat_p224_uint1 x295; uint32_t x296; fiat_p224_uint1 x297; uint32_t x298; uint32_t x299; uint32_t x300; uint32_t x301; uint32_t x302; uint32_t x303; uint32_t x304; uint32_t x305; uint32_t x306; uint32_t x307; uint32_t x308; uint32_t x309; uint32_t x310; uint32_t x311; uint32_t x312; uint32_t x313; fiat_p224_uint1 x314; uint32_t x315; fiat_p224_uint1 x316; uint32_t x317; fiat_p224_uint1 x318; uint32_t x319; fiat_p224_uint1 x320; uint32_t x321; fiat_p224_uint1 x322; uint32_t x323; fiat_p224_uint1 x324; uint32_t x325; uint32_t x326; fiat_p224_uint1 x327; uint32_t x328; fiat_p224_uint1 x329; uint32_t x330; fiat_p224_uint1 x331; uint32_t x332; fiat_p224_uint1 x333; uint32_t x334; fiat_p224_uint1 x335; uint32_t x336; fiat_p224_uint1 x337; uint32_t x338; fiat_p224_uint1 x339; uint32_t x340; fiat_p224_uint1 x341; uint32_t x342; uint32_t x343; uint32_t x344; uint32_t x345; uint32_t x346; uint32_t x347; uint32_t x348; uint32_t x349; uint32_t x350; uint32_t x351; uint32_t x352; fiat_p224_uint1 x353; uint32_t x354; fiat_p224_uint1 x355; uint32_t x356; fiat_p224_uint1 x357; uint32_t x358; uint32_t x359; fiat_p224_uint1 x360; uint32_t x361; fiat_p224_uint1 x362; uint32_t x363; fiat_p224_uint1 x364; uint32_t x365; fiat_p224_uint1 x366; uint32_t x367; fiat_p224_uint1 x368; uint32_t x369; fiat_p224_uint1 x370; uint32_t x371; fiat_p224_uint1 x372; uint32_t x373; fiat_p224_uint1 x374; uint32_t x375; uint32_t x376; uint32_t x377; uint32_t x378; uint32_t x379; uint32_t x380; uint32_t x381; uint32_t x382; uint32_t x383; uint32_t x384; uint32_t x385; uint32_t x386; uint32_t x387; uint32_t x388; uint32_t x389; uint32_t x390; fiat_p224_uint1 x391; uint32_t x392; fiat_p224_uint1 x393; uint32_t x394; fiat_p224_uint1 x395; uint32_t x396; fiat_p224_uint1 x397; uint32_t x398; fiat_p224_uint1 x399; uint32_t x400; fiat_p224_uint1 x401; uint32_t x402; uint32_t x403; fiat_p224_uint1 x404; uint32_t x405; fiat_p224_uint1 x406; uint32_t x407; fiat_p224_uint1 x408; uint32_t x409; fiat_p224_uint1 x410; uint32_t x411; fiat_p224_uint1 x412; uint32_t x413; fiat_p224_uint1 x414; uint32_t x415; fiat_p224_uint1 x416; uint32_t x417; fiat_p224_uint1 x418; uint32_t x419; uint32_t x420; uint32_t x421; uint32_t x422; uint32_t x423; uint32_t x424; uint32_t x425; uint32_t x426; uint32_t x427; uint32_t x428; uint32_t x429; fiat_p224_uint1 x430; uint32_t x431; fiat_p224_uint1 x432; uint32_t x433; fiat_p224_uint1 x434; uint32_t x435; uint32_t x436; fiat_p224_uint1 x437; uint32_t x438; fiat_p224_uint1 x439; uint32_t x440; fiat_p224_uint1 x441; uint32_t x442; fiat_p224_uint1 x443; uint32_t x444; fiat_p224_uint1 x445; uint32_t x446; fiat_p224_uint1 x447; uint32_t x448; fiat_p224_uint1 x449; uint32_t x450; fiat_p224_uint1 x451; uint32_t x452; uint32_t x453; uint32_t x454; uint32_t x455; uint32_t x456; uint32_t x457; uint32_t x458; uint32_t x459; uint32_t x460; uint32_t x461; uint32_t x462; uint32_t x463; uint32_t x464; uint32_t x465; uint32_t x466; uint32_t x467; fiat_p224_uint1 x468; uint32_t x469; fiat_p224_uint1 x470; uint32_t x471; fiat_p224_uint1 x472; uint32_t x473; fiat_p224_uint1 x474; uint32_t x475; fiat_p224_uint1 x476; uint32_t x477; fiat_p224_uint1 x478; uint32_t x479; uint32_t x480; fiat_p224_uint1 x481; uint32_t x482; fiat_p224_uint1 x483; uint32_t x484; fiat_p224_uint1 x485; uint32_t x486; fiat_p224_uint1 x487; uint32_t x488; fiat_p224_uint1 x489; uint32_t x490; fiat_p224_uint1 x491; uint32_t x492; fiat_p224_uint1 x493; uint32_t x494; fiat_p224_uint1 x495; uint32_t x496; uint32_t x497; uint32_t x498; uint32_t x499; uint32_t x500; uint32_t x501; uint32_t x502; uint32_t x503; uint32_t x504; uint32_t x505; uint32_t x506; fiat_p224_uint1 x507; uint32_t x508; fiat_p224_uint1 x509; uint32_t x510; fiat_p224_uint1 x511; uint32_t x512; uint32_t x513; fiat_p224_uint1 x514; uint32_t x515; fiat_p224_uint1 x516; uint32_t x517; fiat_p224_uint1 x518; uint32_t x519; fiat_p224_uint1 x520; uint32_t x521; fiat_p224_uint1 x522; uint32_t x523; fiat_p224_uint1 x524; uint32_t x525; fiat_p224_uint1 x526; uint32_t x527; fiat_p224_uint1 x528; uint32_t x529; uint32_t x530; fiat_p224_uint1 x531; uint32_t x532; fiat_p224_uint1 x533; uint32_t x534; fiat_p224_uint1 x535; uint32_t x536; fiat_p224_uint1 x537; uint32_t x538; fiat_p224_uint1 x539; uint32_t x540; fiat_p224_uint1 x541; uint32_t x542; fiat_p224_uint1 x543; uint32_t x544; fiat_p224_uint1 x545; uint32_t x546; uint32_t x547; uint32_t x548; uint32_t x549; uint32_t x550; uint32_t x551; uint32_t x552; x1 = (arg1[1]); x2 = (arg1[2]); x3 = (arg1[3]); x4 = (arg1[4]); x5 = (arg1[5]); x6 = (arg1[6]); x7 = (arg1[0]); fiat_p224_mulx_u32(&x8, &x9, x7, (arg1[6])); fiat_p224_mulx_u32(&x10, &x11, x7, (arg1[5])); fiat_p224_mulx_u32(&x12, &x13, x7, (arg1[4])); fiat_p224_mulx_u32(&x14, &x15, x7, (arg1[3])); fiat_p224_mulx_u32(&x16, &x17, x7, (arg1[2])); fiat_p224_mulx_u32(&x18, &x19, x7, (arg1[1])); fiat_p224_mulx_u32(&x20, &x21, x7, (arg1[0])); fiat_p224_addcarryx_u32(&x22, &x23, 0x0, x21, x18); fiat_p224_addcarryx_u32(&x24, &x25, x23, x19, x16); fiat_p224_addcarryx_u32(&x26, &x27, x25, x17, x14); fiat_p224_addcarryx_u32(&x28, &x29, x27, x15, x12); fiat_p224_addcarryx_u32(&x30, &x31, x29, x13, x10); fiat_p224_addcarryx_u32(&x32, &x33, x31, x11, x8); x34 = (x33 + x9); fiat_p224_mulx_u32(&x35, &x36, x20, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x37, &x38, x35, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x39, &x40, x35, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x41, &x42, x35, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x43, &x44, x35, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x45, &x46, 0x0, x44, x41); fiat_p224_addcarryx_u32(&x47, &x48, x46, x42, x39); fiat_p224_addcarryx_u32(&x49, &x50, x48, x40, x37); x51 = (x50 + x38); fiat_p224_addcarryx_u32(&x52, &x53, 0x0, x20, x35); fiat_p224_addcarryx_u32(&x54, &x55, x53, x22, 0x0); fiat_p224_addcarryx_u32(&x56, &x57, x55, x24, 0x0); fiat_p224_addcarryx_u32(&x58, &x59, x57, x26, x43); fiat_p224_addcarryx_u32(&x60, &x61, x59, x28, x45); fiat_p224_addcarryx_u32(&x62, &x63, x61, x30, x47); fiat_p224_addcarryx_u32(&x64, &x65, x63, x32, x49); fiat_p224_addcarryx_u32(&x66, &x67, x65, x34, x51); fiat_p224_mulx_u32(&x68, &x69, x1, (arg1[6])); fiat_p224_mulx_u32(&x70, &x71, x1, (arg1[5])); fiat_p224_mulx_u32(&x72, &x73, x1, (arg1[4])); fiat_p224_mulx_u32(&x74, &x75, x1, (arg1[3])); fiat_p224_mulx_u32(&x76, &x77, x1, (arg1[2])); fiat_p224_mulx_u32(&x78, &x79, x1, (arg1[1])); fiat_p224_mulx_u32(&x80, &x81, x1, (arg1[0])); fiat_p224_addcarryx_u32(&x82, &x83, 0x0, x81, x78); fiat_p224_addcarryx_u32(&x84, &x85, x83, x79, x76); fiat_p224_addcarryx_u32(&x86, &x87, x85, x77, x74); fiat_p224_addcarryx_u32(&x88, &x89, x87, x75, x72); fiat_p224_addcarryx_u32(&x90, &x91, x89, x73, x70); fiat_p224_addcarryx_u32(&x92, &x93, x91, x71, x68); x94 = (x93 + x69); fiat_p224_addcarryx_u32(&x95, &x96, 0x0, x54, x80); fiat_p224_addcarryx_u32(&x97, &x98, x96, x56, x82); fiat_p224_addcarryx_u32(&x99, &x100, x98, x58, x84); fiat_p224_addcarryx_u32(&x101, &x102, x100, x60, x86); fiat_p224_addcarryx_u32(&x103, &x104, x102, x62, x88); fiat_p224_addcarryx_u32(&x105, &x106, x104, x64, x90); fiat_p224_addcarryx_u32(&x107, &x108, x106, x66, x92); fiat_p224_addcarryx_u32(&x109, &x110, x108, x67, x94); fiat_p224_mulx_u32(&x111, &x112, x95, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x113, &x114, x111, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x115, &x116, x111, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x117, &x118, x111, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x119, &x120, x111, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x121, &x122, 0x0, x120, x117); fiat_p224_addcarryx_u32(&x123, &x124, x122, x118, x115); fiat_p224_addcarryx_u32(&x125, &x126, x124, x116, x113); x127 = (x126 + x114); fiat_p224_addcarryx_u32(&x128, &x129, 0x0, x95, x111); fiat_p224_addcarryx_u32(&x130, &x131, x129, x97, 0x0); fiat_p224_addcarryx_u32(&x132, &x133, x131, x99, 0x0); fiat_p224_addcarryx_u32(&x134, &x135, x133, x101, x119); fiat_p224_addcarryx_u32(&x136, &x137, x135, x103, x121); fiat_p224_addcarryx_u32(&x138, &x139, x137, x105, x123); fiat_p224_addcarryx_u32(&x140, &x141, x139, x107, x125); fiat_p224_addcarryx_u32(&x142, &x143, x141, x109, x127); x144 = ((uint32_t)x143 + x110); fiat_p224_mulx_u32(&x145, &x146, x2, (arg1[6])); fiat_p224_mulx_u32(&x147, &x148, x2, (arg1[5])); fiat_p224_mulx_u32(&x149, &x150, x2, (arg1[4])); fiat_p224_mulx_u32(&x151, &x152, x2, (arg1[3])); fiat_p224_mulx_u32(&x153, &x154, x2, (arg1[2])); fiat_p224_mulx_u32(&x155, &x156, x2, (arg1[1])); fiat_p224_mulx_u32(&x157, &x158, x2, (arg1[0])); fiat_p224_addcarryx_u32(&x159, &x160, 0x0, x158, x155); fiat_p224_addcarryx_u32(&x161, &x162, x160, x156, x153); fiat_p224_addcarryx_u32(&x163, &x164, x162, x154, x151); fiat_p224_addcarryx_u32(&x165, &x166, x164, x152, x149); fiat_p224_addcarryx_u32(&x167, &x168, x166, x150, x147); fiat_p224_addcarryx_u32(&x169, &x170, x168, x148, x145); x171 = (x170 + x146); fiat_p224_addcarryx_u32(&x172, &x173, 0x0, x130, x157); fiat_p224_addcarryx_u32(&x174, &x175, x173, x132, x159); fiat_p224_addcarryx_u32(&x176, &x177, x175, x134, x161); fiat_p224_addcarryx_u32(&x178, &x179, x177, x136, x163); fiat_p224_addcarryx_u32(&x180, &x181, x179, x138, x165); fiat_p224_addcarryx_u32(&x182, &x183, x181, x140, x167); fiat_p224_addcarryx_u32(&x184, &x185, x183, x142, x169); fiat_p224_addcarryx_u32(&x186, &x187, x185, x144, x171); fiat_p224_mulx_u32(&x188, &x189, x172, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x190, &x191, x188, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x192, &x193, x188, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x194, &x195, x188, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x196, &x197, x188, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x198, &x199, 0x0, x197, x194); fiat_p224_addcarryx_u32(&x200, &x201, x199, x195, x192); fiat_p224_addcarryx_u32(&x202, &x203, x201, x193, x190); x204 = (x203 + x191); fiat_p224_addcarryx_u32(&x205, &x206, 0x0, x172, x188); fiat_p224_addcarryx_u32(&x207, &x208, x206, x174, 0x0); fiat_p224_addcarryx_u32(&x209, &x210, x208, x176, 0x0); fiat_p224_addcarryx_u32(&x211, &x212, x210, x178, x196); fiat_p224_addcarryx_u32(&x213, &x214, x212, x180, x198); fiat_p224_addcarryx_u32(&x215, &x216, x214, x182, x200); fiat_p224_addcarryx_u32(&x217, &x218, x216, x184, x202); fiat_p224_addcarryx_u32(&x219, &x220, x218, x186, x204); x221 = ((uint32_t)x220 + x187); fiat_p224_mulx_u32(&x222, &x223, x3, (arg1[6])); fiat_p224_mulx_u32(&x224, &x225, x3, (arg1[5])); fiat_p224_mulx_u32(&x226, &x227, x3, (arg1[4])); fiat_p224_mulx_u32(&x228, &x229, x3, (arg1[3])); fiat_p224_mulx_u32(&x230, &x231, x3, (arg1[2])); fiat_p224_mulx_u32(&x232, &x233, x3, (arg1[1])); fiat_p224_mulx_u32(&x234, &x235, x3, (arg1[0])); fiat_p224_addcarryx_u32(&x236, &x237, 0x0, x235, x232); fiat_p224_addcarryx_u32(&x238, &x239, x237, x233, x230); fiat_p224_addcarryx_u32(&x240, &x241, x239, x231, x228); fiat_p224_addcarryx_u32(&x242, &x243, x241, x229, x226); fiat_p224_addcarryx_u32(&x244, &x245, x243, x227, x224); fiat_p224_addcarryx_u32(&x246, &x247, x245, x225, x222); x248 = (x247 + x223); fiat_p224_addcarryx_u32(&x249, &x250, 0x0, x207, x234); fiat_p224_addcarryx_u32(&x251, &x252, x250, x209, x236); fiat_p224_addcarryx_u32(&x253, &x254, x252, x211, x238); fiat_p224_addcarryx_u32(&x255, &x256, x254, x213, x240); fiat_p224_addcarryx_u32(&x257, &x258, x256, x215, x242); fiat_p224_addcarryx_u32(&x259, &x260, x258, x217, x244); fiat_p224_addcarryx_u32(&x261, &x262, x260, x219, x246); fiat_p224_addcarryx_u32(&x263, &x264, x262, x221, x248); fiat_p224_mulx_u32(&x265, &x266, x249, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x267, &x268, x265, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x269, &x270, x265, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x271, &x272, x265, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x273, &x274, x265, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x275, &x276, 0x0, x274, x271); fiat_p224_addcarryx_u32(&x277, &x278, x276, x272, x269); fiat_p224_addcarryx_u32(&x279, &x280, x278, x270, x267); x281 = (x280 + x268); fiat_p224_addcarryx_u32(&x282, &x283, 0x0, x249, x265); fiat_p224_addcarryx_u32(&x284, &x285, x283, x251, 0x0); fiat_p224_addcarryx_u32(&x286, &x287, x285, x253, 0x0); fiat_p224_addcarryx_u32(&x288, &x289, x287, x255, x273); fiat_p224_addcarryx_u32(&x290, &x291, x289, x257, x275); fiat_p224_addcarryx_u32(&x292, &x293, x291, x259, x277); fiat_p224_addcarryx_u32(&x294, &x295, x293, x261, x279); fiat_p224_addcarryx_u32(&x296, &x297, x295, x263, x281); x298 = ((uint32_t)x297 + x264); fiat_p224_mulx_u32(&x299, &x300, x4, (arg1[6])); fiat_p224_mulx_u32(&x301, &x302, x4, (arg1[5])); fiat_p224_mulx_u32(&x303, &x304, x4, (arg1[4])); fiat_p224_mulx_u32(&x305, &x306, x4, (arg1[3])); fiat_p224_mulx_u32(&x307, &x308, x4, (arg1[2])); fiat_p224_mulx_u32(&x309, &x310, x4, (arg1[1])); fiat_p224_mulx_u32(&x311, &x312, x4, (arg1[0])); fiat_p224_addcarryx_u32(&x313, &x314, 0x0, x312, x309); fiat_p224_addcarryx_u32(&x315, &x316, x314, x310, x307); fiat_p224_addcarryx_u32(&x317, &x318, x316, x308, x305); fiat_p224_addcarryx_u32(&x319, &x320, x318, x306, x303); fiat_p224_addcarryx_u32(&x321, &x322, x320, x304, x301); fiat_p224_addcarryx_u32(&x323, &x324, x322, x302, x299); x325 = (x324 + x300); fiat_p224_addcarryx_u32(&x326, &x327, 0x0, x284, x311); fiat_p224_addcarryx_u32(&x328, &x329, x327, x286, x313); fiat_p224_addcarryx_u32(&x330, &x331, x329, x288, x315); fiat_p224_addcarryx_u32(&x332, &x333, x331, x290, x317); fiat_p224_addcarryx_u32(&x334, &x335, x333, x292, x319); fiat_p224_addcarryx_u32(&x336, &x337, x335, x294, x321); fiat_p224_addcarryx_u32(&x338, &x339, x337, x296, x323); fiat_p224_addcarryx_u32(&x340, &x341, x339, x298, x325); fiat_p224_mulx_u32(&x342, &x343, x326, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x344, &x345, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x346, &x347, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x348, &x349, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x350, &x351, x342, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x352, &x353, 0x0, x351, x348); fiat_p224_addcarryx_u32(&x354, &x355, x353, x349, x346); fiat_p224_addcarryx_u32(&x356, &x357, x355, x347, x344); x358 = (x357 + x345); fiat_p224_addcarryx_u32(&x359, &x360, 0x0, x326, x342); fiat_p224_addcarryx_u32(&x361, &x362, x360, x328, 0x0); fiat_p224_addcarryx_u32(&x363, &x364, x362, x330, 0x0); fiat_p224_addcarryx_u32(&x365, &x366, x364, x332, x350); fiat_p224_addcarryx_u32(&x367, &x368, x366, x334, x352); fiat_p224_addcarryx_u32(&x369, &x370, x368, x336, x354); fiat_p224_addcarryx_u32(&x371, &x372, x370, x338, x356); fiat_p224_addcarryx_u32(&x373, &x374, x372, x340, x358); x375 = ((uint32_t)x374 + x341); fiat_p224_mulx_u32(&x376, &x377, x5, (arg1[6])); fiat_p224_mulx_u32(&x378, &x379, x5, (arg1[5])); fiat_p224_mulx_u32(&x380, &x381, x5, (arg1[4])); fiat_p224_mulx_u32(&x382, &x383, x5, (arg1[3])); fiat_p224_mulx_u32(&x384, &x385, x5, (arg1[2])); fiat_p224_mulx_u32(&x386, &x387, x5, (arg1[1])); fiat_p224_mulx_u32(&x388, &x389, x5, (arg1[0])); fiat_p224_addcarryx_u32(&x390, &x391, 0x0, x389, x386); fiat_p224_addcarryx_u32(&x392, &x393, x391, x387, x384); fiat_p224_addcarryx_u32(&x394, &x395, x393, x385, x382); fiat_p224_addcarryx_u32(&x396, &x397, x395, x383, x380); fiat_p224_addcarryx_u32(&x398, &x399, x397, x381, x378); fiat_p224_addcarryx_u32(&x400, &x401, x399, x379, x376); x402 = (x401 + x377); fiat_p224_addcarryx_u32(&x403, &x404, 0x0, x361, x388); fiat_p224_addcarryx_u32(&x405, &x406, x404, x363, x390); fiat_p224_addcarryx_u32(&x407, &x408, x406, x365, x392); fiat_p224_addcarryx_u32(&x409, &x410, x408, x367, x394); fiat_p224_addcarryx_u32(&x411, &x412, x410, x369, x396); fiat_p224_addcarryx_u32(&x413, &x414, x412, x371, x398); fiat_p224_addcarryx_u32(&x415, &x416, x414, x373, x400); fiat_p224_addcarryx_u32(&x417, &x418, x416, x375, x402); fiat_p224_mulx_u32(&x419, &x420, x403, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x421, &x422, x419, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x423, &x424, x419, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x425, &x426, x419, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x427, &x428, x419, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x429, &x430, 0x0, x428, x425); fiat_p224_addcarryx_u32(&x431, &x432, x430, x426, x423); fiat_p224_addcarryx_u32(&x433, &x434, x432, x424, x421); x435 = (x434 + x422); fiat_p224_addcarryx_u32(&x436, &x437, 0x0, x403, x419); fiat_p224_addcarryx_u32(&x438, &x439, x437, x405, 0x0); fiat_p224_addcarryx_u32(&x440, &x441, x439, x407, 0x0); fiat_p224_addcarryx_u32(&x442, &x443, x441, x409, x427); fiat_p224_addcarryx_u32(&x444, &x445, x443, x411, x429); fiat_p224_addcarryx_u32(&x446, &x447, x445, x413, x431); fiat_p224_addcarryx_u32(&x448, &x449, x447, x415, x433); fiat_p224_addcarryx_u32(&x450, &x451, x449, x417, x435); x452 = ((uint32_t)x451 + x418); fiat_p224_mulx_u32(&x453, &x454, x6, (arg1[6])); fiat_p224_mulx_u32(&x455, &x456, x6, (arg1[5])); fiat_p224_mulx_u32(&x457, &x458, x6, (arg1[4])); fiat_p224_mulx_u32(&x459, &x460, x6, (arg1[3])); fiat_p224_mulx_u32(&x461, &x462, x6, (arg1[2])); fiat_p224_mulx_u32(&x463, &x464, x6, (arg1[1])); fiat_p224_mulx_u32(&x465, &x466, x6, (arg1[0])); fiat_p224_addcarryx_u32(&x467, &x468, 0x0, x466, x463); fiat_p224_addcarryx_u32(&x469, &x470, x468, x464, x461); fiat_p224_addcarryx_u32(&x471, &x472, x470, x462, x459); fiat_p224_addcarryx_u32(&x473, &x474, x472, x460, x457); fiat_p224_addcarryx_u32(&x475, &x476, x474, x458, x455); fiat_p224_addcarryx_u32(&x477, &x478, x476, x456, x453); x479 = (x478 + x454); fiat_p224_addcarryx_u32(&x480, &x481, 0x0, x438, x465); fiat_p224_addcarryx_u32(&x482, &x483, x481, x440, x467); fiat_p224_addcarryx_u32(&x484, &x485, x483, x442, x469); fiat_p224_addcarryx_u32(&x486, &x487, x485, x444, x471); fiat_p224_addcarryx_u32(&x488, &x489, x487, x446, x473); fiat_p224_addcarryx_u32(&x490, &x491, x489, x448, x475); fiat_p224_addcarryx_u32(&x492, &x493, x491, x450, x477); fiat_p224_addcarryx_u32(&x494, &x495, x493, x452, x479); fiat_p224_mulx_u32(&x496, &x497, x480, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x498, &x499, x496, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x500, &x501, x496, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x502, &x503, x496, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x504, &x505, x496, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x506, &x507, 0x0, x505, x502); fiat_p224_addcarryx_u32(&x508, &x509, x507, x503, x500); fiat_p224_addcarryx_u32(&x510, &x511, x509, x501, x498); x512 = (x511 + x499); fiat_p224_addcarryx_u32(&x513, &x514, 0x0, x480, x496); fiat_p224_addcarryx_u32(&x515, &x516, x514, x482, 0x0); fiat_p224_addcarryx_u32(&x517, &x518, x516, x484, 0x0); fiat_p224_addcarryx_u32(&x519, &x520, x518, x486, x504); fiat_p224_addcarryx_u32(&x521, &x522, x520, x488, x506); fiat_p224_addcarryx_u32(&x523, &x524, x522, x490, x508); fiat_p224_addcarryx_u32(&x525, &x526, x524, x492, x510); fiat_p224_addcarryx_u32(&x527, &x528, x526, x494, x512); x529 = ((uint32_t)x528 + x495); fiat_p224_subborrowx_u32(&x530, &x531, 0x0, x515, 0x1); fiat_p224_subborrowx_u32(&x532, &x533, x531, x517, 0x0); fiat_p224_subborrowx_u32(&x534, &x535, x533, x519, 0x0); fiat_p224_subborrowx_u32(&x536, &x537, x535, x521, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x538, &x539, x537, x523, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x540, &x541, x539, x525, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x542, &x543, x541, x527, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x544, &x545, x543, x529, 0x0); fiat_p224_cmovznz_u32(&x546, x545, x530, x515); fiat_p224_cmovznz_u32(&x547, x545, x532, x517); fiat_p224_cmovznz_u32(&x548, x545, x534, x519); fiat_p224_cmovznz_u32(&x549, x545, x536, x521); fiat_p224_cmovznz_u32(&x550, x545, x538, x523); fiat_p224_cmovznz_u32(&x551, x545, x540, x525); fiat_p224_cmovznz_u32(&x552, x545, x542, x527); out1[0] = x546; out1[1] = x547; out1[2] = x548; out1[3] = x549; out1[4] = x550; out1[5] = x551; out1[6] = x552; } /* * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. * Preconditions: * 0 ≤ eval arg1 < m * Postconditions: * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [0x0 ~> 0xffffffff] */ static void fiat_p224_nonzero(uint32_t* out1, const uint32_t arg1[7]) { uint32_t x1; x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | (arg1[6]))))))); *out1 = x1; } /* * The function fiat_p224_selectznz is a multi-limb conditional select. * Postconditions: * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_selectznz(uint32_t out1[7], fiat_p224_uint1 arg1, const uint32_t arg2[7], const uint32_t arg3[7]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; fiat_p224_cmovznz_u32(&x1, arg1, (arg2[0]), (arg3[0])); fiat_p224_cmovznz_u32(&x2, arg1, (arg2[1]), (arg3[1])); fiat_p224_cmovznz_u32(&x3, arg1, (arg2[2]), (arg3[2])); fiat_p224_cmovznz_u32(&x4, arg1, (arg2[3]), (arg3[3])); fiat_p224_cmovznz_u32(&x5, arg1, (arg2[4]), (arg3[4])); fiat_p224_cmovznz_u32(&x6, arg1, (arg2[5]), (arg3[5])); fiat_p224_cmovznz_u32(&x7, arg1, (arg2[6]), (arg3[6])); out1[0] = x1; out1[1] = x2; out1[2] = x3; out1[3] = x4; out1[4] = x5; out1[5] = x6; out1[6] = x7; } /* * The function fiat_p224_to_montgomery translates a field element into the Montgomery domain. * Preconditions: * 0 ≤ eval arg1 < m * Postconditions: * eval (from_montgomery out1) mod m = eval arg1 mod m * 0 ≤ eval out1 < m * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_to_montgomery(uint32_t out1[7], const uint32_t arg1[7]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; fiat_p224_uint1 x15; uint32_t x16; fiat_p224_uint1 x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint32_t x28; fiat_p224_uint1 x29; uint32_t x30; fiat_p224_uint1 x31; uint32_t x32; fiat_p224_uint1 x33; uint32_t x34; fiat_p224_uint1 x35; uint32_t x36; fiat_p224_uint1 x37; uint32_t x38; fiat_p224_uint1 x39; uint32_t x40; fiat_p224_uint1 x41; uint32_t x42; fiat_p224_uint1 x43; uint32_t x44; uint32_t x45; uint32_t x46; uint32_t x47; uint32_t x48; uint32_t x49; uint32_t x50; fiat_p224_uint1 x51; uint32_t x52; fiat_p224_uint1 x53; uint32_t x54; fiat_p224_uint1 x55; uint32_t x56; fiat_p224_uint1 x57; uint32_t x58; fiat_p224_uint1 x59; uint32_t x60; fiat_p224_uint1 x61; uint32_t x62; fiat_p224_uint1 x63; uint32_t x64; fiat_p224_uint1 x65; uint32_t x66; uint32_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; uint32_t x74; uint32_t x75; uint32_t x76; fiat_p224_uint1 x77; uint32_t x78; fiat_p224_uint1 x79; uint32_t x80; fiat_p224_uint1 x81; uint32_t x82; fiat_p224_uint1 x83; uint32_t x84; fiat_p224_uint1 x85; uint32_t x86; fiat_p224_uint1 x87; uint32_t x88; fiat_p224_uint1 x89; uint32_t x90; fiat_p224_uint1 x91; uint32_t x92; uint32_t x93; uint32_t x94; uint32_t x95; uint32_t x96; uint32_t x97; uint32_t x98; fiat_p224_uint1 x99; uint32_t x100; fiat_p224_uint1 x101; uint32_t x102; fiat_p224_uint1 x103; uint32_t x104; fiat_p224_uint1 x105; uint32_t x106; fiat_p224_uint1 x107; uint32_t x108; fiat_p224_uint1 x109; uint32_t x110; fiat_p224_uint1 x111; uint32_t x112; fiat_p224_uint1 x113; uint32_t x114; fiat_p224_uint1 x115; uint32_t x116; fiat_p224_uint1 x117; uint32_t x118; uint32_t x119; uint32_t x120; uint32_t x121; uint32_t x122; uint32_t x123; uint32_t x124; uint32_t x125; uint32_t x126; uint32_t x127; uint32_t x128; fiat_p224_uint1 x129; uint32_t x130; fiat_p224_uint1 x131; uint32_t x132; fiat_p224_uint1 x133; uint32_t x134; fiat_p224_uint1 x135; uint32_t x136; fiat_p224_uint1 x137; uint32_t x138; fiat_p224_uint1 x139; uint32_t x140; fiat_p224_uint1 x141; uint32_t x142; fiat_p224_uint1 x143; uint32_t x144; fiat_p224_uint1 x145; uint32_t x146; fiat_p224_uint1 x147; uint32_t x148; fiat_p224_uint1 x149; uint32_t x150; uint32_t x151; uint32_t x152; uint32_t x153; uint32_t x154; uint32_t x155; uint32_t x156; fiat_p224_uint1 x157; uint32_t x158; fiat_p224_uint1 x159; uint32_t x160; fiat_p224_uint1 x161; uint32_t x162; fiat_p224_uint1 x163; uint32_t x164; fiat_p224_uint1 x165; uint32_t x166; fiat_p224_uint1 x167; uint32_t x168; fiat_p224_uint1 x169; uint32_t x170; fiat_p224_uint1 x171; uint32_t x172; fiat_p224_uint1 x173; uint32_t x174; uint32_t x175; uint32_t x176; uint32_t x177; uint32_t x178; uint32_t x179; uint32_t x180; uint32_t x181; uint32_t x182; uint32_t x183; uint32_t x184; fiat_p224_uint1 x185; uint32_t x186; fiat_p224_uint1 x187; uint32_t x188; fiat_p224_uint1 x189; uint32_t x190; fiat_p224_uint1 x191; uint32_t x192; fiat_p224_uint1 x193; uint32_t x194; fiat_p224_uint1 x195; uint32_t x196; fiat_p224_uint1 x197; uint32_t x198; fiat_p224_uint1 x199; uint32_t x200; fiat_p224_uint1 x201; uint32_t x202; fiat_p224_uint1 x203; uint32_t x204; fiat_p224_uint1 x205; uint32_t x206; uint32_t x207; uint32_t x208; uint32_t x209; uint32_t x210; uint32_t x211; uint32_t x212; fiat_p224_uint1 x213; uint32_t x214; fiat_p224_uint1 x215; uint32_t x216; fiat_p224_uint1 x217; uint32_t x218; fiat_p224_uint1 x219; uint32_t x220; fiat_p224_uint1 x221; uint32_t x222; fiat_p224_uint1 x223; uint32_t x224; fiat_p224_uint1 x225; uint32_t x226; fiat_p224_uint1 x227; uint32_t x228; fiat_p224_uint1 x229; uint32_t x230; uint32_t x231; uint32_t x232; uint32_t x233; uint32_t x234; uint32_t x235; uint32_t x236; uint32_t x237; uint32_t x238; uint32_t x239; uint32_t x240; fiat_p224_uint1 x241; uint32_t x242; fiat_p224_uint1 x243; uint32_t x244; fiat_p224_uint1 x245; uint32_t x246; fiat_p224_uint1 x247; uint32_t x248; fiat_p224_uint1 x249; uint32_t x250; fiat_p224_uint1 x251; uint32_t x252; fiat_p224_uint1 x253; uint32_t x254; fiat_p224_uint1 x255; uint32_t x256; fiat_p224_uint1 x257; uint32_t x258; fiat_p224_uint1 x259; uint32_t x260; fiat_p224_uint1 x261; uint32_t x262; uint32_t x263; uint32_t x264; uint32_t x265; uint32_t x266; uint32_t x267; uint32_t x268; fiat_p224_uint1 x269; uint32_t x270; fiat_p224_uint1 x271; uint32_t x272; fiat_p224_uint1 x273; uint32_t x274; fiat_p224_uint1 x275; uint32_t x276; fiat_p224_uint1 x277; uint32_t x278; fiat_p224_uint1 x279; uint32_t x280; fiat_p224_uint1 x281; uint32_t x282; fiat_p224_uint1 x283; uint32_t x284; fiat_p224_uint1 x285; uint32_t x286; uint32_t x287; uint32_t x288; uint32_t x289; uint32_t x290; uint32_t x291; uint32_t x292; uint32_t x293; uint32_t x294; uint32_t x295; uint32_t x296; fiat_p224_uint1 x297; uint32_t x298; fiat_p224_uint1 x299; uint32_t x300; fiat_p224_uint1 x301; uint32_t x302; fiat_p224_uint1 x303; uint32_t x304; fiat_p224_uint1 x305; uint32_t x306; fiat_p224_uint1 x307; uint32_t x308; fiat_p224_uint1 x309; uint32_t x310; fiat_p224_uint1 x311; uint32_t x312; fiat_p224_uint1 x313; uint32_t x314; fiat_p224_uint1 x315; uint32_t x316; fiat_p224_uint1 x317; uint32_t x318; uint32_t x319; uint32_t x320; uint32_t x321; uint32_t x322; uint32_t x323; uint32_t x324; fiat_p224_uint1 x325; uint32_t x326; fiat_p224_uint1 x327; uint32_t x328; fiat_p224_uint1 x329; uint32_t x330; fiat_p224_uint1 x331; uint32_t x332; fiat_p224_uint1 x333; uint32_t x334; fiat_p224_uint1 x335; uint32_t x336; fiat_p224_uint1 x337; uint32_t x338; fiat_p224_uint1 x339; uint32_t x340; fiat_p224_uint1 x341; uint32_t x342; uint32_t x343; uint32_t x344; uint32_t x345; uint32_t x346; uint32_t x347; uint32_t x348; uint32_t x349; uint32_t x350; uint32_t x351; uint32_t x352; fiat_p224_uint1 x353; uint32_t x354; fiat_p224_uint1 x355; uint32_t x356; fiat_p224_uint1 x357; uint32_t x358; fiat_p224_uint1 x359; uint32_t x360; fiat_p224_uint1 x361; uint32_t x362; fiat_p224_uint1 x363; uint32_t x364; fiat_p224_uint1 x365; uint32_t x366; fiat_p224_uint1 x367; uint32_t x368; fiat_p224_uint1 x369; uint32_t x370; fiat_p224_uint1 x371; uint32_t x372; fiat_p224_uint1 x373; uint32_t x374; fiat_p224_uint1 x375; uint32_t x376; fiat_p224_uint1 x377; uint32_t x378; fiat_p224_uint1 x379; uint32_t x380; fiat_p224_uint1 x381; uint32_t x382; fiat_p224_uint1 x383; uint32_t x384; fiat_p224_uint1 x385; uint32_t x386; fiat_p224_uint1 x387; uint32_t x388; fiat_p224_uint1 x389; uint32_t x390; uint32_t x391; uint32_t x392; uint32_t x393; uint32_t x394; uint32_t x395; uint32_t x396; x1 = (arg1[1]); x2 = (arg1[2]); x3 = (arg1[3]); x4 = (arg1[4]); x5 = (arg1[5]); x6 = (arg1[6]); x7 = (arg1[0]); fiat_p224_mulx_u32(&x8, &x9, x7, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x10, &x11, x7, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x12, &x13, x7, UINT32_C(0xfffffffe)); fiat_p224_addcarryx_u32(&x14, &x15, 0x0, x13, x10); fiat_p224_addcarryx_u32(&x16, &x17, x15, x11, x8); fiat_p224_mulx_u32(&x18, &x19, x7, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x20, &x21, x18, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x22, &x23, x18, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x24, &x25, x18, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x26, &x27, x18, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x28, &x29, 0x0, x27, x24); fiat_p224_addcarryx_u32(&x30, &x31, x29, x25, x22); fiat_p224_addcarryx_u32(&x32, &x33, x31, x23, x20); fiat_p224_addcarryx_u32(&x34, &x35, 0x0, x12, x26); fiat_p224_addcarryx_u32(&x36, &x37, x35, x14, x28); fiat_p224_addcarryx_u32(&x38, &x39, x37, x16, x30); fiat_p224_addcarryx_u32(&x40, &x41, x39, (x17 + x9), x32); fiat_p224_addcarryx_u32(&x42, &x43, x41, 0x0, (x33 + x21)); fiat_p224_mulx_u32(&x44, &x45, x1, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x46, &x47, x1, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x48, &x49, x1, UINT32_C(0xfffffffe)); fiat_p224_addcarryx_u32(&x50, &x51, 0x0, x49, x46); fiat_p224_addcarryx_u32(&x52, &x53, x51, x47, x44); fiat_p224_addcarryx_u32(&x54, &x55, 0x0, x7, x18); fiat_p224_addcarryx_u32(&x56, &x57, 0x0, x55, x1); fiat_p224_addcarryx_u32(&x58, &x59, 0x0, x36, x48); fiat_p224_addcarryx_u32(&x60, &x61, x59, x38, x50); fiat_p224_addcarryx_u32(&x62, &x63, x61, x40, x52); fiat_p224_addcarryx_u32(&x64, &x65, x63, x42, (x53 + x45)); fiat_p224_mulx_u32(&x66, &x67, x56, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x68, &x69, x66, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x70, &x71, x66, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x72, &x73, x66, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x74, &x75, x66, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x76, &x77, 0x0, x75, x72); fiat_p224_addcarryx_u32(&x78, &x79, x77, x73, x70); fiat_p224_addcarryx_u32(&x80, &x81, x79, x71, x68); fiat_p224_addcarryx_u32(&x82, &x83, 0x0, x58, x74); fiat_p224_addcarryx_u32(&x84, &x85, x83, x60, x76); fiat_p224_addcarryx_u32(&x86, &x87, x85, x62, x78); fiat_p224_addcarryx_u32(&x88, &x89, x87, x64, x80); fiat_p224_addcarryx_u32(&x90, &x91, x89, ((uint32_t)x65 + x43), (x81 + x69)); fiat_p224_mulx_u32(&x92, &x93, x2, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x94, &x95, x2, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x96, &x97, x2, UINT32_C(0xfffffffe)); fiat_p224_addcarryx_u32(&x98, &x99, 0x0, x97, x94); fiat_p224_addcarryx_u32(&x100, &x101, x99, x95, x92); fiat_p224_addcarryx_u32(&x102, &x103, 0x0, x56, x66); fiat_p224_addcarryx_u32(&x104, &x105, 0x0, ((uint32_t)x103 + x57), x2); fiat_p224_addcarryx_u32(&x106, &x107, x105, x34, 0x0); fiat_p224_addcarryx_u32(&x108, &x109, x107, x82, 0x0); fiat_p224_addcarryx_u32(&x110, &x111, x109, x84, x96); fiat_p224_addcarryx_u32(&x112, &x113, x111, x86, x98); fiat_p224_addcarryx_u32(&x114, &x115, x113, x88, x100); fiat_p224_addcarryx_u32(&x116, &x117, x115, x90, (x101 + x93)); fiat_p224_mulx_u32(&x118, &x119, x104, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x120, &x121, x118, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x122, &x123, x118, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x124, &x125, x118, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x126, &x127, x118, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x128, &x129, 0x0, x127, x124); fiat_p224_addcarryx_u32(&x130, &x131, x129, x125, x122); fiat_p224_addcarryx_u32(&x132, &x133, x131, x123, x120); fiat_p224_addcarryx_u32(&x134, &x135, 0x0, x104, x118); fiat_p224_addcarryx_u32(&x136, &x137, x135, x106, 0x0); fiat_p224_addcarryx_u32(&x138, &x139, x137, x108, 0x0); fiat_p224_addcarryx_u32(&x140, &x141, x139, x110, x126); fiat_p224_addcarryx_u32(&x142, &x143, x141, x112, x128); fiat_p224_addcarryx_u32(&x144, &x145, x143, x114, x130); fiat_p224_addcarryx_u32(&x146, &x147, x145, x116, x132); fiat_p224_addcarryx_u32(&x148, &x149, x147, ((uint32_t)x117 + x91), (x133 + x121)); fiat_p224_mulx_u32(&x150, &x151, x3, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x152, &x153, x3, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x154, &x155, x3, UINT32_C(0xfffffffe)); fiat_p224_addcarryx_u32(&x156, &x157, 0x0, x155, x152); fiat_p224_addcarryx_u32(&x158, &x159, x157, x153, x150); fiat_p224_addcarryx_u32(&x160, &x161, 0x0, x136, x3); fiat_p224_addcarryx_u32(&x162, &x163, x161, x138, 0x0); fiat_p224_addcarryx_u32(&x164, &x165, x163, x140, 0x0); fiat_p224_addcarryx_u32(&x166, &x167, x165, x142, x154); fiat_p224_addcarryx_u32(&x168, &x169, x167, x144, x156); fiat_p224_addcarryx_u32(&x170, &x171, x169, x146, x158); fiat_p224_addcarryx_u32(&x172, &x173, x171, x148, (x159 + x151)); fiat_p224_mulx_u32(&x174, &x175, x160, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x176, &x177, x174, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x178, &x179, x174, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x180, &x181, x174, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x182, &x183, x174, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x184, &x185, 0x0, x183, x180); fiat_p224_addcarryx_u32(&x186, &x187, x185, x181, x178); fiat_p224_addcarryx_u32(&x188, &x189, x187, x179, x176); fiat_p224_addcarryx_u32(&x190, &x191, 0x0, x160, x174); fiat_p224_addcarryx_u32(&x192, &x193, x191, x162, 0x0); fiat_p224_addcarryx_u32(&x194, &x195, x193, x164, 0x0); fiat_p224_addcarryx_u32(&x196, &x197, x195, x166, x182); fiat_p224_addcarryx_u32(&x198, &x199, x197, x168, x184); fiat_p224_addcarryx_u32(&x200, &x201, x199, x170, x186); fiat_p224_addcarryx_u32(&x202, &x203, x201, x172, x188); fiat_p224_addcarryx_u32(&x204, &x205, x203, ((uint32_t)x173 + x149), (x189 + x177)); fiat_p224_mulx_u32(&x206, &x207, x4, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x208, &x209, x4, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x210, &x211, x4, UINT32_C(0xfffffffe)); fiat_p224_addcarryx_u32(&x212, &x213, 0x0, x211, x208); fiat_p224_addcarryx_u32(&x214, &x215, x213, x209, x206); fiat_p224_addcarryx_u32(&x216, &x217, 0x0, x192, x4); fiat_p224_addcarryx_u32(&x218, &x219, x217, x194, 0x0); fiat_p224_addcarryx_u32(&x220, &x221, x219, x196, 0x0); fiat_p224_addcarryx_u32(&x222, &x223, x221, x198, x210); fiat_p224_addcarryx_u32(&x224, &x225, x223, x200, x212); fiat_p224_addcarryx_u32(&x226, &x227, x225, x202, x214); fiat_p224_addcarryx_u32(&x228, &x229, x227, x204, (x215 + x207)); fiat_p224_mulx_u32(&x230, &x231, x216, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x232, &x233, x230, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x234, &x235, x230, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x236, &x237, x230, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x238, &x239, x230, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x240, &x241, 0x0, x239, x236); fiat_p224_addcarryx_u32(&x242, &x243, x241, x237, x234); fiat_p224_addcarryx_u32(&x244, &x245, x243, x235, x232); fiat_p224_addcarryx_u32(&x246, &x247, 0x0, x216, x230); fiat_p224_addcarryx_u32(&x248, &x249, x247, x218, 0x0); fiat_p224_addcarryx_u32(&x250, &x251, x249, x220, 0x0); fiat_p224_addcarryx_u32(&x252, &x253, x251, x222, x238); fiat_p224_addcarryx_u32(&x254, &x255, x253, x224, x240); fiat_p224_addcarryx_u32(&x256, &x257, x255, x226, x242); fiat_p224_addcarryx_u32(&x258, &x259, x257, x228, x244); fiat_p224_addcarryx_u32(&x260, &x261, x259, ((uint32_t)x229 + x205), (x245 + x233)); fiat_p224_mulx_u32(&x262, &x263, x5, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x264, &x265, x5, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x266, &x267, x5, UINT32_C(0xfffffffe)); fiat_p224_addcarryx_u32(&x268, &x269, 0x0, x267, x264); fiat_p224_addcarryx_u32(&x270, &x271, x269, x265, x262); fiat_p224_addcarryx_u32(&x272, &x273, 0x0, x248, x5); fiat_p224_addcarryx_u32(&x274, &x275, x273, x250, 0x0); fiat_p224_addcarryx_u32(&x276, &x277, x275, x252, 0x0); fiat_p224_addcarryx_u32(&x278, &x279, x277, x254, x266); fiat_p224_addcarryx_u32(&x280, &x281, x279, x256, x268); fiat_p224_addcarryx_u32(&x282, &x283, x281, x258, x270); fiat_p224_addcarryx_u32(&x284, &x285, x283, x260, (x271 + x263)); fiat_p224_mulx_u32(&x286, &x287, x272, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x288, &x289, x286, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x290, &x291, x286, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x292, &x293, x286, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x294, &x295, x286, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x296, &x297, 0x0, x295, x292); fiat_p224_addcarryx_u32(&x298, &x299, x297, x293, x290); fiat_p224_addcarryx_u32(&x300, &x301, x299, x291, x288); fiat_p224_addcarryx_u32(&x302, &x303, 0x0, x272, x286); fiat_p224_addcarryx_u32(&x304, &x305, x303, x274, 0x0); fiat_p224_addcarryx_u32(&x306, &x307, x305, x276, 0x0); fiat_p224_addcarryx_u32(&x308, &x309, x307, x278, x294); fiat_p224_addcarryx_u32(&x310, &x311, x309, x280, x296); fiat_p224_addcarryx_u32(&x312, &x313, x311, x282, x298); fiat_p224_addcarryx_u32(&x314, &x315, x313, x284, x300); fiat_p224_addcarryx_u32(&x316, &x317, x315, ((uint32_t)x285 + x261), (x301 + x289)); fiat_p224_mulx_u32(&x318, &x319, x6, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x320, &x321, x6, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x322, &x323, x6, UINT32_C(0xfffffffe)); fiat_p224_addcarryx_u32(&x324, &x325, 0x0, x323, x320); fiat_p224_addcarryx_u32(&x326, &x327, x325, x321, x318); fiat_p224_addcarryx_u32(&x328, &x329, 0x0, x304, x6); fiat_p224_addcarryx_u32(&x330, &x331, x329, x306, 0x0); fiat_p224_addcarryx_u32(&x332, &x333, x331, x308, 0x0); fiat_p224_addcarryx_u32(&x334, &x335, x333, x310, x322); fiat_p224_addcarryx_u32(&x336, &x337, x335, x312, x324); fiat_p224_addcarryx_u32(&x338, &x339, x337, x314, x326); fiat_p224_addcarryx_u32(&x340, &x341, x339, x316, (x327 + x319)); fiat_p224_mulx_u32(&x342, &x343, x328, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x344, &x345, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x346, &x347, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x348, &x349, x342, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x350, &x351, x342, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x352, &x353, 0x0, x351, x348); fiat_p224_addcarryx_u32(&x354, &x355, x353, x349, x346); fiat_p224_addcarryx_u32(&x356, &x357, x355, x347, x344); fiat_p224_addcarryx_u32(&x358, &x359, 0x0, x328, x342); fiat_p224_addcarryx_u32(&x360, &x361, x359, x330, 0x0); fiat_p224_addcarryx_u32(&x362, &x363, x361, x332, 0x0); fiat_p224_addcarryx_u32(&x364, &x365, x363, x334, x350); fiat_p224_addcarryx_u32(&x366, &x367, x365, x336, x352); fiat_p224_addcarryx_u32(&x368, &x369, x367, x338, x354); fiat_p224_addcarryx_u32(&x370, &x371, x369, x340, x356); fiat_p224_addcarryx_u32(&x372, &x373, x371, ((uint32_t)x341 + x317), (x357 + x345)); fiat_p224_subborrowx_u32(&x374, &x375, 0x0, x360, 0x1); fiat_p224_subborrowx_u32(&x376, &x377, x375, x362, 0x0); fiat_p224_subborrowx_u32(&x378, &x379, x377, x364, 0x0); fiat_p224_subborrowx_u32(&x380, &x381, x379, x366, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x382, &x383, x381, x368, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x384, &x385, x383, x370, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x386, &x387, x385, x372, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x388, &x389, x387, x373, 0x0); fiat_p224_cmovznz_u32(&x390, x389, x374, x360); fiat_p224_cmovznz_u32(&x391, x389, x376, x362); fiat_p224_cmovznz_u32(&x392, x389, x378, x364); fiat_p224_cmovznz_u32(&x393, x389, x380, x366); fiat_p224_cmovznz_u32(&x394, x389, x382, x368); fiat_p224_cmovznz_u32(&x395, x389, x384, x370); fiat_p224_cmovznz_u32(&x396, x389, x386, x372); out1[0] = x390; out1[1] = x391; out1[2] = x392; out1[3] = x393; out1[4] = x394; out1[5] = x395; out1[6] = x396; } /* * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain. * Preconditions: * 0 ≤ eval arg1 < m * Postconditions: * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m * 0 ≤ eval out1 < m * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_from_montgomery(uint32_t out1[7], const uint32_t arg1[7]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; fiat_p224_uint1 x13; uint32_t x14; fiat_p224_uint1 x15; uint32_t x16; fiat_p224_uint1 x17; uint32_t x18; fiat_p224_uint1 x19; uint32_t x20; fiat_p224_uint1 x21; uint32_t x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint32_t x28; uint32_t x29; uint32_t x30; uint32_t x31; uint32_t x32; fiat_p224_uint1 x33; uint32_t x34; fiat_p224_uint1 x35; uint32_t x36; fiat_p224_uint1 x37; uint32_t x38; fiat_p224_uint1 x39; uint32_t x40; fiat_p224_uint1 x41; uint32_t x42; fiat_p224_uint1 x43; uint32_t x44; fiat_p224_uint1 x45; uint32_t x46; fiat_p224_uint1 x47; uint32_t x48; fiat_p224_uint1 x49; uint32_t x50; fiat_p224_uint1 x51; uint32_t x52; fiat_p224_uint1 x53; uint32_t x54; fiat_p224_uint1 x55; uint32_t x56; fiat_p224_uint1 x57; uint32_t x58; fiat_p224_uint1 x59; uint32_t x60; fiat_p224_uint1 x61; uint32_t x62; fiat_p224_uint1 x63; uint32_t x64; uint32_t x65; uint32_t x66; uint32_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; uint32_t x74; fiat_p224_uint1 x75; uint32_t x76; fiat_p224_uint1 x77; uint32_t x78; fiat_p224_uint1 x79; uint32_t x80; fiat_p224_uint1 x81; uint32_t x82; fiat_p224_uint1 x83; uint32_t x84; fiat_p224_uint1 x85; uint32_t x86; fiat_p224_uint1 x87; uint32_t x88; fiat_p224_uint1 x89; uint32_t x90; fiat_p224_uint1 x91; uint32_t x92; fiat_p224_uint1 x93; uint32_t x94; fiat_p224_uint1 x95; uint32_t x96; fiat_p224_uint1 x97; uint32_t x98; fiat_p224_uint1 x99; uint32_t x100; fiat_p224_uint1 x101; uint32_t x102; fiat_p224_uint1 x103; uint32_t x104; fiat_p224_uint1 x105; uint32_t x106; fiat_p224_uint1 x107; uint32_t x108; fiat_p224_uint1 x109; uint32_t x110; uint32_t x111; uint32_t x112; uint32_t x113; uint32_t x114; uint32_t x115; uint32_t x116; uint32_t x117; uint32_t x118; uint32_t x119; uint32_t x120; fiat_p224_uint1 x121; uint32_t x122; fiat_p224_uint1 x123; uint32_t x124; fiat_p224_uint1 x125; uint32_t x126; fiat_p224_uint1 x127; uint32_t x128; fiat_p224_uint1 x129; uint32_t x130; fiat_p224_uint1 x131; uint32_t x132; fiat_p224_uint1 x133; uint32_t x134; fiat_p224_uint1 x135; uint32_t x136; fiat_p224_uint1 x137; uint32_t x138; fiat_p224_uint1 x139; uint32_t x140; fiat_p224_uint1 x141; uint32_t x142; fiat_p224_uint1 x143; uint32_t x144; fiat_p224_uint1 x145; uint32_t x146; fiat_p224_uint1 x147; uint32_t x148; fiat_p224_uint1 x149; uint32_t x150; fiat_p224_uint1 x151; uint32_t x152; fiat_p224_uint1 x153; uint32_t x154; fiat_p224_uint1 x155; uint32_t x156; uint32_t x157; uint32_t x158; uint32_t x159; uint32_t x160; uint32_t x161; uint32_t x162; uint32_t x163; uint32_t x164; uint32_t x165; uint32_t x166; fiat_p224_uint1 x167; uint32_t x168; fiat_p224_uint1 x169; uint32_t x170; fiat_p224_uint1 x171; uint32_t x172; fiat_p224_uint1 x173; uint32_t x174; fiat_p224_uint1 x175; uint32_t x176; fiat_p224_uint1 x177; uint32_t x178; fiat_p224_uint1 x179; uint32_t x180; fiat_p224_uint1 x181; uint32_t x182; fiat_p224_uint1 x183; uint32_t x184; fiat_p224_uint1 x185; uint32_t x186; fiat_p224_uint1 x187; uint32_t x188; fiat_p224_uint1 x189; uint32_t x190; fiat_p224_uint1 x191; uint32_t x192; fiat_p224_uint1 x193; uint32_t x194; fiat_p224_uint1 x195; uint32_t x196; fiat_p224_uint1 x197; uint32_t x198; fiat_p224_uint1 x199; uint32_t x200; fiat_p224_uint1 x201; uint32_t x202; uint32_t x203; uint32_t x204; uint32_t x205; uint32_t x206; uint32_t x207; uint32_t x208; uint32_t x209; uint32_t x210; uint32_t x211; uint32_t x212; fiat_p224_uint1 x213; uint32_t x214; fiat_p224_uint1 x215; uint32_t x216; fiat_p224_uint1 x217; uint32_t x218; fiat_p224_uint1 x219; uint32_t x220; fiat_p224_uint1 x221; uint32_t x222; fiat_p224_uint1 x223; uint32_t x224; fiat_p224_uint1 x225; uint32_t x226; fiat_p224_uint1 x227; uint32_t x228; fiat_p224_uint1 x229; uint32_t x230; fiat_p224_uint1 x231; uint32_t x232; fiat_p224_uint1 x233; uint32_t x234; fiat_p224_uint1 x235; uint32_t x236; fiat_p224_uint1 x237; uint32_t x238; fiat_p224_uint1 x239; uint32_t x240; fiat_p224_uint1 x241; uint32_t x242; fiat_p224_uint1 x243; uint32_t x244; fiat_p224_uint1 x245; uint32_t x246; fiat_p224_uint1 x247; uint32_t x248; uint32_t x249; uint32_t x250; uint32_t x251; uint32_t x252; uint32_t x253; uint32_t x254; uint32_t x255; uint32_t x256; uint32_t x257; uint32_t x258; fiat_p224_uint1 x259; uint32_t x260; fiat_p224_uint1 x261; uint32_t x262; fiat_p224_uint1 x263; uint32_t x264; fiat_p224_uint1 x265; uint32_t x266; fiat_p224_uint1 x267; uint32_t x268; fiat_p224_uint1 x269; uint32_t x270; fiat_p224_uint1 x271; uint32_t x272; fiat_p224_uint1 x273; uint32_t x274; fiat_p224_uint1 x275; uint32_t x276; fiat_p224_uint1 x277; uint32_t x278; fiat_p224_uint1 x279; uint32_t x280; fiat_p224_uint1 x281; uint32_t x282; fiat_p224_uint1 x283; uint32_t x284; fiat_p224_uint1 x285; uint32_t x286; fiat_p224_uint1 x287; uint32_t x288; fiat_p224_uint1 x289; uint32_t x290; fiat_p224_uint1 x291; uint32_t x292; fiat_p224_uint1 x293; uint32_t x294; fiat_p224_uint1 x295; uint32_t x296; uint32_t x297; uint32_t x298; uint32_t x299; uint32_t x300; uint32_t x301; uint32_t x302; x1 = (arg1[0]); fiat_p224_mulx_u32(&x2, &x3, x1, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x4, &x5, x2, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x6, &x7, x2, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x8, &x9, x2, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x10, &x11, x2, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x12, &x13, 0x0, x11, x8); fiat_p224_addcarryx_u32(&x14, &x15, x13, x9, x6); fiat_p224_addcarryx_u32(&x16, &x17, x15, x7, x4); fiat_p224_addcarryx_u32(&x18, &x19, 0x0, x1, x2); fiat_p224_addcarryx_u32(&x20, &x21, 0x0, x19, (arg1[1])); fiat_p224_mulx_u32(&x22, &x23, x20, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x24, &x25, x22, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x26, &x27, x22, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x28, &x29, x22, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x30, &x31, x22, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x32, &x33, 0x0, x31, x28); fiat_p224_addcarryx_u32(&x34, &x35, x33, x29, x26); fiat_p224_addcarryx_u32(&x36, &x37, x35, x27, x24); fiat_p224_addcarryx_u32(&x38, &x39, 0x0, x12, x30); fiat_p224_addcarryx_u32(&x40, &x41, x39, x14, x32); fiat_p224_addcarryx_u32(&x42, &x43, x41, x16, x34); fiat_p224_addcarryx_u32(&x44, &x45, x43, (x17 + x5), x36); fiat_p224_addcarryx_u32(&x46, &x47, x45, 0x0, (x37 + x25)); fiat_p224_addcarryx_u32(&x48, &x49, 0x0, x20, x22); fiat_p224_addcarryx_u32(&x50, &x51, 0x0, ((uint32_t)x49 + x21), (arg1[2])); fiat_p224_addcarryx_u32(&x52, &x53, x51, x10, 0x0); fiat_p224_addcarryx_u32(&x54, &x55, x53, x38, 0x0); fiat_p224_addcarryx_u32(&x56, &x57, x55, x40, 0x0); fiat_p224_addcarryx_u32(&x58, &x59, x57, x42, 0x0); fiat_p224_addcarryx_u32(&x60, &x61, x59, x44, 0x0); fiat_p224_addcarryx_u32(&x62, &x63, x61, x46, 0x0); fiat_p224_mulx_u32(&x64, &x65, x50, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x66, &x67, x64, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x68, &x69, x64, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x70, &x71, x64, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x72, &x73, x64, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x74, &x75, 0x0, x73, x70); fiat_p224_addcarryx_u32(&x76, &x77, x75, x71, x68); fiat_p224_addcarryx_u32(&x78, &x79, x77, x69, x66); fiat_p224_addcarryx_u32(&x80, &x81, 0x0, x50, x64); fiat_p224_addcarryx_u32(&x82, &x83, x81, x52, 0x0); fiat_p224_addcarryx_u32(&x84, &x85, x83, x54, 0x0); fiat_p224_addcarryx_u32(&x86, &x87, x85, x56, x72); fiat_p224_addcarryx_u32(&x88, &x89, x87, x58, x74); fiat_p224_addcarryx_u32(&x90, &x91, x89, x60, x76); fiat_p224_addcarryx_u32(&x92, &x93, x91, x62, x78); fiat_p224_addcarryx_u32(&x94, &x95, x93, ((uint32_t)x63 + x47), (x79 + x67)); fiat_p224_addcarryx_u32(&x96, &x97, 0x0, x82, (arg1[3])); fiat_p224_addcarryx_u32(&x98, &x99, x97, x84, 0x0); fiat_p224_addcarryx_u32(&x100, &x101, x99, x86, 0x0); fiat_p224_addcarryx_u32(&x102, &x103, x101, x88, 0x0); fiat_p224_addcarryx_u32(&x104, &x105, x103, x90, 0x0); fiat_p224_addcarryx_u32(&x106, &x107, x105, x92, 0x0); fiat_p224_addcarryx_u32(&x108, &x109, x107, x94, 0x0); fiat_p224_mulx_u32(&x110, &x111, x96, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x112, &x113, x110, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x114, &x115, x110, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x116, &x117, x110, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x118, &x119, x110, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x120, &x121, 0x0, x119, x116); fiat_p224_addcarryx_u32(&x122, &x123, x121, x117, x114); fiat_p224_addcarryx_u32(&x124, &x125, x123, x115, x112); fiat_p224_addcarryx_u32(&x126, &x127, 0x0, x96, x110); fiat_p224_addcarryx_u32(&x128, &x129, x127, x98, 0x0); fiat_p224_addcarryx_u32(&x130, &x131, x129, x100, 0x0); fiat_p224_addcarryx_u32(&x132, &x133, x131, x102, x118); fiat_p224_addcarryx_u32(&x134, &x135, x133, x104, x120); fiat_p224_addcarryx_u32(&x136, &x137, x135, x106, x122); fiat_p224_addcarryx_u32(&x138, &x139, x137, x108, x124); fiat_p224_addcarryx_u32(&x140, &x141, x139, ((uint32_t)x109 + x95), (x125 + x113)); fiat_p224_addcarryx_u32(&x142, &x143, 0x0, x128, (arg1[4])); fiat_p224_addcarryx_u32(&x144, &x145, x143, x130, 0x0); fiat_p224_addcarryx_u32(&x146, &x147, x145, x132, 0x0); fiat_p224_addcarryx_u32(&x148, &x149, x147, x134, 0x0); fiat_p224_addcarryx_u32(&x150, &x151, x149, x136, 0x0); fiat_p224_addcarryx_u32(&x152, &x153, x151, x138, 0x0); fiat_p224_addcarryx_u32(&x154, &x155, x153, x140, 0x0); fiat_p224_mulx_u32(&x156, &x157, x142, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x158, &x159, x156, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x160, &x161, x156, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x162, &x163, x156, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x164, &x165, x156, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x166, &x167, 0x0, x165, x162); fiat_p224_addcarryx_u32(&x168, &x169, x167, x163, x160); fiat_p224_addcarryx_u32(&x170, &x171, x169, x161, x158); fiat_p224_addcarryx_u32(&x172, &x173, 0x0, x142, x156); fiat_p224_addcarryx_u32(&x174, &x175, x173, x144, 0x0); fiat_p224_addcarryx_u32(&x176, &x177, x175, x146, 0x0); fiat_p224_addcarryx_u32(&x178, &x179, x177, x148, x164); fiat_p224_addcarryx_u32(&x180, &x181, x179, x150, x166); fiat_p224_addcarryx_u32(&x182, &x183, x181, x152, x168); fiat_p224_addcarryx_u32(&x184, &x185, x183, x154, x170); fiat_p224_addcarryx_u32(&x186, &x187, x185, ((uint32_t)x155 + x141), (x171 + x159)); fiat_p224_addcarryx_u32(&x188, &x189, 0x0, x174, (arg1[5])); fiat_p224_addcarryx_u32(&x190, &x191, x189, x176, 0x0); fiat_p224_addcarryx_u32(&x192, &x193, x191, x178, 0x0); fiat_p224_addcarryx_u32(&x194, &x195, x193, x180, 0x0); fiat_p224_addcarryx_u32(&x196, &x197, x195, x182, 0x0); fiat_p224_addcarryx_u32(&x198, &x199, x197, x184, 0x0); fiat_p224_addcarryx_u32(&x200, &x201, x199, x186, 0x0); fiat_p224_mulx_u32(&x202, &x203, x188, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x204, &x205, x202, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x206, &x207, x202, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x208, &x209, x202, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x210, &x211, x202, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x212, &x213, 0x0, x211, x208); fiat_p224_addcarryx_u32(&x214, &x215, x213, x209, x206); fiat_p224_addcarryx_u32(&x216, &x217, x215, x207, x204); fiat_p224_addcarryx_u32(&x218, &x219, 0x0, x188, x202); fiat_p224_addcarryx_u32(&x220, &x221, x219, x190, 0x0); fiat_p224_addcarryx_u32(&x222, &x223, x221, x192, 0x0); fiat_p224_addcarryx_u32(&x224, &x225, x223, x194, x210); fiat_p224_addcarryx_u32(&x226, &x227, x225, x196, x212); fiat_p224_addcarryx_u32(&x228, &x229, x227, x198, x214); fiat_p224_addcarryx_u32(&x230, &x231, x229, x200, x216); fiat_p224_addcarryx_u32(&x232, &x233, x231, ((uint32_t)x201 + x187), (x217 + x205)); fiat_p224_addcarryx_u32(&x234, &x235, 0x0, x220, (arg1[6])); fiat_p224_addcarryx_u32(&x236, &x237, x235, x222, 0x0); fiat_p224_addcarryx_u32(&x238, &x239, x237, x224, 0x0); fiat_p224_addcarryx_u32(&x240, &x241, x239, x226, 0x0); fiat_p224_addcarryx_u32(&x242, &x243, x241, x228, 0x0); fiat_p224_addcarryx_u32(&x244, &x245, x243, x230, 0x0); fiat_p224_addcarryx_u32(&x246, &x247, x245, x232, 0x0); fiat_p224_mulx_u32(&x248, &x249, x234, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x250, &x251, x248, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x252, &x253, x248, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x254, &x255, x248, UINT32_C(0xffffffff)); fiat_p224_mulx_u32(&x256, &x257, x248, UINT32_C(0xffffffff)); fiat_p224_addcarryx_u32(&x258, &x259, 0x0, x257, x254); fiat_p224_addcarryx_u32(&x260, &x261, x259, x255, x252); fiat_p224_addcarryx_u32(&x262, &x263, x261, x253, x250); fiat_p224_addcarryx_u32(&x264, &x265, 0x0, x234, x248); fiat_p224_addcarryx_u32(&x266, &x267, x265, x236, 0x0); fiat_p224_addcarryx_u32(&x268, &x269, x267, x238, 0x0); fiat_p224_addcarryx_u32(&x270, &x271, x269, x240, x256); fiat_p224_addcarryx_u32(&x272, &x273, x271, x242, x258); fiat_p224_addcarryx_u32(&x274, &x275, x273, x244, x260); fiat_p224_addcarryx_u32(&x276, &x277, x275, x246, x262); fiat_p224_addcarryx_u32(&x278, &x279, x277, ((uint32_t)x247 + x233), (x263 + x251)); fiat_p224_subborrowx_u32(&x280, &x281, 0x0, x266, 0x1); fiat_p224_subborrowx_u32(&x282, &x283, x281, x268, 0x0); fiat_p224_subborrowx_u32(&x284, &x285, x283, x270, 0x0); fiat_p224_subborrowx_u32(&x286, &x287, x285, x272, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x288, &x289, x287, x274, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x290, &x291, x289, x276, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x292, &x293, x291, x278, UINT32_C(0xffffffff)); fiat_p224_subborrowx_u32(&x294, &x295, x293, x279, 0x0); fiat_p224_cmovznz_u32(&x296, x295, x280, x266); fiat_p224_cmovznz_u32(&x297, x295, x282, x268); fiat_p224_cmovznz_u32(&x298, x295, x284, x270); fiat_p224_cmovznz_u32(&x299, x295, x286, x272); fiat_p224_cmovznz_u32(&x300, x295, x288, x274); fiat_p224_cmovznz_u32(&x301, x295, x290, x276); fiat_p224_cmovznz_u32(&x302, x295, x292, x278); out1[0] = x296; out1[1] = x297; out1[2] = x298; out1[3] = x299; out1[4] = x300; out1[5] = x301; out1[6] = x302; } /* * The function fiat_p224_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order. * Preconditions: * 0 ≤ eval arg1 < m * Postconditions: * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..27] * * Input Bounds: * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * 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]] */ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint8_t x8; uint32_t x9; uint8_t x10; uint32_t x11; uint8_t x12; uint8_t x13; uint8_t x14; uint32_t x15; uint8_t x16; uint32_t x17; uint8_t x18; uint8_t x19; uint8_t x20; uint32_t x21; uint8_t x22; uint32_t x23; uint8_t x24; uint8_t x25; uint8_t x26; uint32_t x27; uint8_t x28; uint32_t x29; uint8_t x30; uint8_t x31; uint8_t x32; uint32_t x33; uint8_t x34; uint32_t x35; uint8_t x36; uint8_t x37; uint8_t x38; uint32_t x39; uint8_t x40; uint32_t x41; uint8_t x42; uint8_t x43; uint8_t x44; uint32_t x45; uint8_t x46; uint32_t x47; uint8_t x48; uint8_t x49; x1 = (arg1[6]); x2 = (arg1[5]); x3 = (arg1[4]); x4 = (arg1[3]); x5 = (arg1[2]); x6 = (arg1[1]); x7 = (arg1[0]); x8 = (uint8_t)(x7 & UINT8_C(0xff)); x9 = (x7 >> 8); x10 = (uint8_t)(x9 & UINT8_C(0xff)); x11 = (x9 >> 8); x12 = (uint8_t)(x11 & UINT8_C(0xff)); x13 = (uint8_t)(x11 >> 8); x14 = (uint8_t)(x6 & UINT8_C(0xff)); x15 = (x6 >> 8); x16 = (uint8_t)(x15 & UINT8_C(0xff)); x17 = (x15 >> 8); x18 = (uint8_t)(x17 & UINT8_C(0xff)); x19 = (uint8_t)(x17 >> 8); x20 = (uint8_t)(x5 & UINT8_C(0xff)); x21 = (x5 >> 8); x22 = (uint8_t)(x21 & UINT8_C(0xff)); x23 = (x21 >> 8); x24 = (uint8_t)(x23 & UINT8_C(0xff)); x25 = (uint8_t)(x23 >> 8); x26 = (uint8_t)(x4 & UINT8_C(0xff)); x27 = (x4 >> 8); x28 = (uint8_t)(x27 & UINT8_C(0xff)); x29 = (x27 >> 8); x30 = (uint8_t)(x29 & UINT8_C(0xff)); x31 = (uint8_t)(x29 >> 8); x32 = (uint8_t)(x3 & UINT8_C(0xff)); x33 = (x3 >> 8); x34 = (uint8_t)(x33 & UINT8_C(0xff)); x35 = (x33 >> 8); x36 = (uint8_t)(x35 & UINT8_C(0xff)); x37 = (uint8_t)(x35 >> 8); x38 = (uint8_t)(x2 & UINT8_C(0xff)); x39 = (x2 >> 8); x40 = (uint8_t)(x39 & UINT8_C(0xff)); x41 = (x39 >> 8); x42 = (uint8_t)(x41 & UINT8_C(0xff)); x43 = (uint8_t)(x41 >> 8); x44 = (uint8_t)(x1 & UINT8_C(0xff)); x45 = (x1 >> 8); x46 = (uint8_t)(x45 & UINT8_C(0xff)); x47 = (x45 >> 8); x48 = (uint8_t)(x47 & UINT8_C(0xff)); x49 = (uint8_t)(x47 >> 8); out1[0] = x8; out1[1] = x10; out1[2] = x12; out1[3] = x13; out1[4] = x14; out1[5] = x16; out1[6] = x18; out1[7] = x19; out1[8] = x20; out1[9] = x22; out1[10] = x24; out1[11] = x25; out1[12] = x26; out1[13] = x28; out1[14] = x30; out1[15] = x31; out1[16] = x32; out1[17] = x34; out1[18] = x36; out1[19] = x37; out1[20] = x38; out1[21] = x40; out1[22] = x42; out1[23] = x43; out1[24] = x44; out1[25] = x46; out1[26] = x48; out1[27] = x49; } /* * The function fiat_p224_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order. * Preconditions: * 0 ≤ bytes_eval arg1 < m * Postconditions: * eval out1 mod m = bytes_eval arg1 mod m * 0 ≤ eval out1 < m * * Input Bounds: * 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]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p224_from_bytes(uint32_t out1[7], const uint8_t arg1[28]) { uint32_t x1; uint32_t x2; uint32_t x3; uint8_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint8_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint8_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint8_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint8_t x20; uint32_t x21; uint32_t x22; uint32_t x23; uint8_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint8_t x28; uint32_t x29; uint32_t x30; uint32_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; uint32_t x46; uint32_t x47; uint32_t x48; uint32_t x49; x1 = ((uint32_t)(arg1[27]) << 24); x2 = ((uint32_t)(arg1[26]) << 16); x3 = ((uint32_t)(arg1[25]) << 8); x4 = (arg1[24]); x5 = ((uint32_t)(arg1[23]) << 24); x6 = ((uint32_t)(arg1[22]) << 16); x7 = ((uint32_t)(arg1[21]) << 8); x8 = (arg1[20]); x9 = ((uint32_t)(arg1[19]) << 24); x10 = ((uint32_t)(arg1[18]) << 16); x11 = ((uint32_t)(arg1[17]) << 8); x12 = (arg1[16]); x13 = ((uint32_t)(arg1[15]) << 24); x14 = ((uint32_t)(arg1[14]) << 16); x15 = ((uint32_t)(arg1[13]) << 8); x16 = (arg1[12]); x17 = ((uint32_t)(arg1[11]) << 24); x18 = ((uint32_t)(arg1[10]) << 16); x19 = ((uint32_t)(arg1[9]) << 8); x20 = (arg1[8]); x21 = ((uint32_t)(arg1[7]) << 24); x22 = ((uint32_t)(arg1[6]) << 16); x23 = ((uint32_t)(arg1[5]) << 8); x24 = (arg1[4]); x25 = ((uint32_t)(arg1[3]) << 24); x26 = ((uint32_t)(arg1[2]) << 16); x27 = ((uint32_t)(arg1[1]) << 8); x28 = (arg1[0]); x29 = (x27 + (uint32_t)x28); x30 = (x26 + x29); x31 = (x25 + x30); x32 = (x23 + (uint32_t)x24); x33 = (x22 + x32); x34 = (x21 + x33); x35 = (x19 + (uint32_t)x20); x36 = (x18 + x35); x37 = (x17 + x36); x38 = (x15 + (uint32_t)x16); x39 = (x14 + x38); x40 = (x13 + x39); x41 = (x11 + (uint32_t)x12); x42 = (x10 + x41); x43 = (x9 + x42); x44 = (x7 + (uint32_t)x8); x45 = (x6 + x44); x46 = (x5 + x45); x47 = (x3 + (uint32_t)x4); x48 = (x2 + x47); x49 = (x1 + x48); out1[0] = x31; out1[1] = x34; out1[2] = x37; out1[3] = x40; out1[4] = x43; out1[5] = x46; out1[6] = x49; }