diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-15 15:53:34 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-16 16:51:11 -0500 |
| commit | 60bade02ccd577550bfcd5974d3c62a3d40e751a (patch) | |
| tree | 46a9e9ef505704bdff47f0c794c163ecd5d7fd76 /p384_32.c | |
| parent | 538e541709d70caaa78104739cb965c6523d89a8 (diff) | |
Add a rewrite rule to collapse constant casts
If, e.g., we know from bounds analysis that the result of an operation
fits in the range r[0~>0], we now just replace it with the literal
constant.
Fixes #493
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
21m22.14s | Total | 21m22.79s || -0m00.65s | -0.05%
--------------------------------------------------------------------------------------------
4m09.97s | PushButtonSynthesis.vo | 4m10.56s || -0m00.59s | -0.23%
3m09.12s | p384_32.c | 3m08.91s || +0m00.21s | +0.11%
2m05.94s | Rewriter.vo | 2m06.30s || -0m00.35s | -0.28%
1m56.58s | RewriterWf2.vo | 1m56.09s || +0m00.48s | +0.42%
1m52.39s | RewriterRulesGood.vo | 1m52.04s || +0m00.35s | +0.31%
1m46.01s | RewriterRulesInterpGood.vo | 1m45.79s || +0m00.21s | +0.20%
0m46.44s | RewriterInterpProofs1.vo | 0m46.47s || -0m00.03s | -0.06%
0m44.96s | ExtractionHaskell/word_by_word_montgomery | 0m45.59s || -0m00.63s | -1.38%
0m39.18s | p521_32.c | 0m39.33s || -0m00.14s | -0.38%
0m32.41s | p521_64.c | 0m32.54s || -0m00.13s | -0.39%
0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m30.67s || +0m00.19s | +0.65%
0m24.32s | ExtractionHaskell/saturated_solinas | 0m24.44s || -0m00.12s | -0.49%
0m23.59s | RewriterWf1.vo | 0m24.10s || -0m00.51s | -2.11%
0m17.01s | ExtractionOCaml/word_by_word_montgomery | 0m17.14s || -0m00.12s | -0.75%
0m13.48s | secp256k1_32.c | 0m13.30s || +0m00.17s | +1.35%
0m13.11s | p256_32.c | 0m13.37s || -0m00.25s | -1.94%
0m11.34s | p484_64.c | 0m11.34s || +0m00.00s | +0.00%
0m10.78s | ExtractionOCaml/unsaturated_solinas | 0m10.79s || -0m00.00s | -0.09%
0m10.27s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.06s || +0m00.20s | +2.08%
0m08.11s | ExtractionOCaml/saturated_solinas | 0m07.92s || +0m00.18s | +2.39%
0m06.92s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.02s || -0m00.09s | -1.42%
0m06.18s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s || -0m00.10s | -1.59%
0m06.13s | BoundsPipeline.vo | 0m05.98s || +0m00.14s | +2.50%
0m05.90s | p224_32.c | 0m05.92s || -0m00.01s | -0.33%
0m05.29s | p384_64.c | 0m05.33s || -0m00.04s | -0.75%
0m05.17s | ExtractionOCaml/saturated_solinas.ml | 0m05.20s || -0m00.03s | -0.57%
0m04.91s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.93s || -0m00.01s | -0.40%
0m04.06s | ExtractionHaskell/saturated_solinas.hs | 0m04.00s || +0m00.05s | +1.49%
0m02.21s | curve25519_32.c | 0m02.22s || -0m00.01s | -0.45%
0m01.52s | curve25519_64.c | 0m01.50s || +0m00.02s | +1.33%
0m01.38s | CLI.vo | 0m01.42s || -0m00.04s | -2.81%
0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88%
0m01.14s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.17s | +18.74%
0m01.12s | StandaloneHaskellMain.vo | 0m01.03s || +0m00.09s | +8.73%
0m01.12s | secp256k1_64.c | 0m01.00s || +0m00.12s | +12.00%
0m01.05s | p256_64.c | 0m00.98s || +0m00.07s | +7.14%
0m01.03s | p224_64.c | 0m01.15s || -0m00.11s | -10.43%
Diffstat (limited to 'p384_32.c')
| -rw-r--r-- | p384_32.c | 1906 |
1 files changed, 924 insertions, 982 deletions
@@ -5620,1601 +5620,1565 @@ static void fiat_p384_from_montgomery(uint32_t out1[12], const uint32_t arg1[12] fiat_p384_uint1 x43; fiat_p384_addcarryx_u32(&x42, &x43, 0x0, (arg1[1]), x40); uint32_t x44; - fiat_p384_uint1 x45; - fiat_p384_addcarryx_u32(&x44, &x45, x41, 0x0, 0x0); + uint32_t x45; + fiat_p384_mulx_u32(&x44, &x45, x42, UINT32_C(0xffffffff)); uint32_t x46; - fiat_p384_uint1 x47; - fiat_p384_addcarryx_u32(&x46, &x47, x43, 0x0, (fiat_p384_uint1)x44); + uint32_t x47; + fiat_p384_mulx_u32(&x46, &x47, x42, UINT32_C(0xffffffff)); uint32_t x48; - fiat_p384_uint1 x49; - fiat_p384_addcarryx_u32(&x48, &x49, x47, 0x0, x18); + uint32_t x49; + fiat_p384_mulx_u32(&x48, &x49, x42, UINT32_C(0xffffffff)); uint32_t x50; - fiat_p384_uint1 x51; - fiat_p384_addcarryx_u32(&x50, &x51, x49, 0x0, x22); + uint32_t x51; + fiat_p384_mulx_u32(&x50, &x51, x42, UINT32_C(0xffffffff)); uint32_t x52; - fiat_p384_uint1 x53; - fiat_p384_addcarryx_u32(&x52, &x53, x51, 0x0, x24); + uint32_t x53; + fiat_p384_mulx_u32(&x52, &x53, x42, UINT32_C(0xffffffff)); uint32_t x54; - fiat_p384_uint1 x55; - fiat_p384_addcarryx_u32(&x54, &x55, x53, 0x0, x26); + uint32_t x55; + fiat_p384_mulx_u32(&x54, &x55, x42, UINT32_C(0xffffffff)); uint32_t x56; - fiat_p384_uint1 x57; - fiat_p384_addcarryx_u32(&x56, &x57, x55, 0x0, x28); + uint32_t x57; + fiat_p384_mulx_u32(&x56, &x57, x42, UINT32_C(0xffffffff)); uint32_t x58; - fiat_p384_uint1 x59; - fiat_p384_addcarryx_u32(&x58, &x59, x57, 0x0, x30); + uint32_t x59; + fiat_p384_mulx_u32(&x58, &x59, x42, UINT32_C(0xfffffffe)); uint32_t x60; - fiat_p384_uint1 x61; - fiat_p384_addcarryx_u32(&x60, &x61, x59, 0x0, x32); + uint32_t x61; + fiat_p384_mulx_u32(&x60, &x61, x42, UINT32_C(0xffffffff)); uint32_t x62; - fiat_p384_uint1 x63; - fiat_p384_addcarryx_u32(&x62, &x63, x61, 0x0, x34); + uint32_t x63; + fiat_p384_mulx_u32(&x62, &x63, x42, UINT32_C(0xffffffff)); uint32_t x64; fiat_p384_uint1 x65; - fiat_p384_addcarryx_u32(&x64, &x65, x63, 0x0, x36); + fiat_p384_addcarryx_u32(&x64, &x65, 0x0, x58, x61); uint32_t x66; fiat_p384_uint1 x67; - fiat_p384_addcarryx_u32(&x66, &x67, x37, 0x0, x3); + fiat_p384_addcarryx_u32(&x66, &x67, x65, x56, x59); uint32_t x68; fiat_p384_uint1 x69; - fiat_p384_addcarryx_u32(&x68, &x69, x65, 0x0, x66); + fiat_p384_addcarryx_u32(&x68, &x69, x67, x54, x57); uint32_t x70; - uint32_t x71; - fiat_p384_mulx_u32(&x70, &x71, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x71; + fiat_p384_addcarryx_u32(&x70, &x71, x69, x52, x55); uint32_t x72; - uint32_t x73; - fiat_p384_mulx_u32(&x72, &x73, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x73; + fiat_p384_addcarryx_u32(&x72, &x73, x71, x50, x53); uint32_t x74; - uint32_t x75; - fiat_p384_mulx_u32(&x74, &x75, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x75; + fiat_p384_addcarryx_u32(&x74, &x75, x73, x48, x51); uint32_t x76; - uint32_t x77; - fiat_p384_mulx_u32(&x76, &x77, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x77; + fiat_p384_addcarryx_u32(&x76, &x77, x75, x46, x49); uint32_t x78; - uint32_t x79; - fiat_p384_mulx_u32(&x78, &x79, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x79; + fiat_p384_addcarryx_u32(&x78, &x79, x77, x44, x47); uint32_t x80; - uint32_t x81; - fiat_p384_mulx_u32(&x80, &x81, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x81; + fiat_p384_addcarryx_u32(&x80, &x81, x43, 0x0, 0x0); uint32_t x82; - uint32_t x83; - fiat_p384_mulx_u32(&x82, &x83, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x83; + fiat_p384_addcarryx_u32(&x82, &x83, 0x0, x62, x42); uint32_t x84; - uint32_t x85; - fiat_p384_mulx_u32(&x84, &x85, x42, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x85; + fiat_p384_addcarryx_u32(&x84, &x85, x83, x63, (fiat_p384_uint1)x80); uint32_t x86; - uint32_t x87; - fiat_p384_mulx_u32(&x86, &x87, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x87; + fiat_p384_addcarryx_u32(&x86, &x87, x85, 0x0, x18); uint32_t x88; - uint32_t x89; - fiat_p384_mulx_u32(&x88, &x89, x42, UINT32_C(0xffffffff)); + fiat_p384_uint1 x89; + fiat_p384_addcarryx_u32(&x88, &x89, x87, x60, x22); uint32_t x90; fiat_p384_uint1 x91; - fiat_p384_addcarryx_u32(&x90, &x91, 0x0, x84, x87); + fiat_p384_addcarryx_u32(&x90, &x91, x89, x64, x24); uint32_t x92; fiat_p384_uint1 x93; - fiat_p384_addcarryx_u32(&x92, &x93, x91, x82, x85); + fiat_p384_addcarryx_u32(&x92, &x93, x91, x66, x26); uint32_t x94; fiat_p384_uint1 x95; - fiat_p384_addcarryx_u32(&x94, &x95, x93, x80, x83); + fiat_p384_addcarryx_u32(&x94, &x95, x93, x68, x28); uint32_t x96; fiat_p384_uint1 x97; - fiat_p384_addcarryx_u32(&x96, &x97, x95, x78, x81); + fiat_p384_addcarryx_u32(&x96, &x97, x95, x70, x30); uint32_t x98; fiat_p384_uint1 x99; - fiat_p384_addcarryx_u32(&x98, &x99, x97, x76, x79); + fiat_p384_addcarryx_u32(&x98, &x99, x97, x72, x32); uint32_t x100; fiat_p384_uint1 x101; - fiat_p384_addcarryx_u32(&x100, &x101, x99, x74, x77); + fiat_p384_addcarryx_u32(&x100, &x101, x99, x74, x34); uint32_t x102; fiat_p384_uint1 x103; - fiat_p384_addcarryx_u32(&x102, &x103, x101, x72, x75); + fiat_p384_addcarryx_u32(&x102, &x103, x101, x76, x36); uint32_t x104; fiat_p384_uint1 x105; - fiat_p384_addcarryx_u32(&x104, &x105, x103, x70, x73); + fiat_p384_addcarryx_u32(&x104, &x105, x37, 0x0, x3); uint32_t x106; fiat_p384_uint1 x107; - fiat_p384_addcarryx_u32(&x106, &x107, 0x0, x88, x42); + fiat_p384_addcarryx_u32(&x106, &x107, x103, x78, x104); uint32_t x108; fiat_p384_uint1 x109; - fiat_p384_addcarryx_u32(&x108, &x109, x107, x89, (fiat_p384_uint1)x46); + fiat_p384_addcarryx_u32(&x108, &x109, x79, 0x0, x45); uint32_t x110; fiat_p384_uint1 x111; - fiat_p384_addcarryx_u32(&x110, &x111, x109, 0x0, x48); + fiat_p384_addcarryx_u32(&x110, &x111, x107, x108, 0x0); uint32_t x112; fiat_p384_uint1 x113; - fiat_p384_addcarryx_u32(&x112, &x113, x111, x86, x50); + fiat_p384_addcarryx_u32(&x112, &x113, 0x0, (arg1[2]), x84); uint32_t x114; fiat_p384_uint1 x115; - fiat_p384_addcarryx_u32(&x114, &x115, x113, x90, x52); + fiat_p384_addcarryx_u32(&x114, &x115, x113, 0x0, x86); uint32_t x116; fiat_p384_uint1 x117; - fiat_p384_addcarryx_u32(&x116, &x117, x115, x92, x54); + fiat_p384_addcarryx_u32(&x116, &x117, x115, 0x0, x88); uint32_t x118; fiat_p384_uint1 x119; - fiat_p384_addcarryx_u32(&x118, &x119, x117, x94, x56); + fiat_p384_addcarryx_u32(&x118, &x119, x117, 0x0, x90); uint32_t x120; fiat_p384_uint1 x121; - fiat_p384_addcarryx_u32(&x120, &x121, x119, x96, x58); + fiat_p384_addcarryx_u32(&x120, &x121, x119, 0x0, x92); uint32_t x122; fiat_p384_uint1 x123; - fiat_p384_addcarryx_u32(&x122, &x123, x121, x98, x60); + fiat_p384_addcarryx_u32(&x122, &x123, x121, 0x0, x94); uint32_t x124; fiat_p384_uint1 x125; - fiat_p384_addcarryx_u32(&x124, &x125, x123, x100, x62); + fiat_p384_addcarryx_u32(&x124, &x125, x123, 0x0, x96); uint32_t x126; fiat_p384_uint1 x127; - fiat_p384_addcarryx_u32(&x126, &x127, x125, x102, x64); + fiat_p384_addcarryx_u32(&x126, &x127, x125, 0x0, x98); uint32_t x128; fiat_p384_uint1 x129; - fiat_p384_addcarryx_u32(&x128, &x129, x127, x104, x68); + fiat_p384_addcarryx_u32(&x128, &x129, x127, 0x0, x100); uint32_t x130; fiat_p384_uint1 x131; - fiat_p384_addcarryx_u32(&x130, &x131, x69, 0x0, 0x0); + fiat_p384_addcarryx_u32(&x130, &x131, x129, 0x0, x102); uint32_t x132; fiat_p384_uint1 x133; - fiat_p384_addcarryx_u32(&x132, &x133, x105, 0x0, x71); + fiat_p384_addcarryx_u32(&x132, &x133, x131, 0x0, x106); uint32_t x134; fiat_p384_uint1 x135; - fiat_p384_addcarryx_u32(&x134, &x135, x129, x132, (fiat_p384_uint1)x130); + fiat_p384_addcarryx_u32(&x134, &x135, x133, 0x0, x110); uint32_t x136; - fiat_p384_uint1 x137; - fiat_p384_addcarryx_u32(&x136, &x137, 0x0, (arg1[2]), x108); + uint32_t x137; + fiat_p384_mulx_u32(&x136, &x137, x112, UINT32_C(0xffffffff)); uint32_t x138; - fiat_p384_uint1 x139; - fiat_p384_addcarryx_u32(&x138, &x139, x137, 0x0, x110); + uint32_t x139; + fiat_p384_mulx_u32(&x138, &x139, x112, UINT32_C(0xffffffff)); uint32_t x140; - fiat_p384_uint1 x141; - fiat_p384_addcarryx_u32(&x140, &x141, x139, 0x0, x112); + uint32_t x141; + fiat_p384_mulx_u32(&x140, &x141, x112, UINT32_C(0xffffffff)); uint32_t x142; - fiat_p384_uint1 x143; - fiat_p384_addcarryx_u32(&x142, &x143, x141, 0x0, x114); + uint32_t x143; + fiat_p384_mulx_u32(&x142, &x143, x112, UINT32_C(0xffffffff)); uint32_t x144; - fiat_p384_uint1 x145; - fiat_p384_addcarryx_u32(&x144, &x145, x143, 0x0, x116); + uint32_t x145; + fiat_p384_mulx_u32(&x144, &x145, x112, UINT32_C(0xffffffff)); uint32_t x146; - fiat_p384_uint1 x147; - fiat_p384_addcarryx_u32(&x146, &x147, x145, 0x0, x118); + uint32_t x147; + fiat_p384_mulx_u32(&x146, &x147, x112, UINT32_C(0xffffffff)); uint32_t x148; - fiat_p384_uint1 x149; - fiat_p384_addcarryx_u32(&x148, &x149, x147, 0x0, x120); + uint32_t x149; + fiat_p384_mulx_u32(&x148, &x149, x112, UINT32_C(0xffffffff)); uint32_t x150; - fiat_p384_uint1 x151; - fiat_p384_addcarryx_u32(&x150, &x151, x149, 0x0, x122); + uint32_t x151; + fiat_p384_mulx_u32(&x150, &x151, x112, UINT32_C(0xfffffffe)); uint32_t x152; - fiat_p384_uint1 x153; - fiat_p384_addcarryx_u32(&x152, &x153, x151, 0x0, x124); + uint32_t x153; + fiat_p384_mulx_u32(&x152, &x153, x112, UINT32_C(0xffffffff)); uint32_t x154; - fiat_p384_uint1 x155; - fiat_p384_addcarryx_u32(&x154, &x155, x153, 0x0, x126); + uint32_t x155; + fiat_p384_mulx_u32(&x154, &x155, x112, UINT32_C(0xffffffff)); uint32_t x156; fiat_p384_uint1 x157; - fiat_p384_addcarryx_u32(&x156, &x157, x155, 0x0, x128); + fiat_p384_addcarryx_u32(&x156, &x157, 0x0, x150, x153); uint32_t x158; fiat_p384_uint1 x159; - fiat_p384_addcarryx_u32(&x158, &x159, x157, 0x0, x134); + fiat_p384_addcarryx_u32(&x158, &x159, x157, x148, x151); uint32_t x160; fiat_p384_uint1 x161; - fiat_p384_addcarryx_u32(&x160, &x161, x135, 0x0, 0x0); + fiat_p384_addcarryx_u32(&x160, &x161, x159, x146, x149); uint32_t x162; fiat_p384_uint1 x163; - fiat_p384_addcarryx_u32(&x162, &x163, x159, 0x0, (fiat_p384_uint1)x160); + fiat_p384_addcarryx_u32(&x162, &x163, x161, x144, x147); uint32_t x164; - uint32_t x165; - fiat_p384_mulx_u32(&x164, &x165, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x165; + fiat_p384_addcarryx_u32(&x164, &x165, x163, x142, x145); uint32_t x166; - uint32_t x167; - fiat_p384_mulx_u32(&x166, &x167, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x167; + fiat_p384_addcarryx_u32(&x166, &x167, x165, x140, x143); uint32_t x168; - uint32_t x169; - fiat_p384_mulx_u32(&x168, &x169, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x169; + fiat_p384_addcarryx_u32(&x168, &x169, x167, x138, x141); uint32_t x170; - uint32_t x171; - fiat_p384_mulx_u32(&x170, &x171, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x171; + fiat_p384_addcarryx_u32(&x170, &x171, x169, x136, x139); uint32_t x172; - uint32_t x173; - fiat_p384_mulx_u32(&x172, &x173, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x173; + fiat_p384_addcarryx_u32(&x172, &x173, 0x0, x154, x112); uint32_t x174; - uint32_t x175; - fiat_p384_mulx_u32(&x174, &x175, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x175; + fiat_p384_addcarryx_u32(&x174, &x175, x173, x155, x114); uint32_t x176; - uint32_t x177; - fiat_p384_mulx_u32(&x176, &x177, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x177; + fiat_p384_addcarryx_u32(&x176, &x177, x175, 0x0, x116); uint32_t x178; - uint32_t x179; - fiat_p384_mulx_u32(&x178, &x179, x136, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x179; + fiat_p384_addcarryx_u32(&x178, &x179, x177, x152, x118); uint32_t x180; - uint32_t x181; - fiat_p384_mulx_u32(&x180, &x181, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x181; + fiat_p384_addcarryx_u32(&x180, &x181, x179, x156, x120); uint32_t x182; - uint32_t x183; - fiat_p384_mulx_u32(&x182, &x183, x136, UINT32_C(0xffffffff)); + fiat_p384_uint1 x183; + fiat_p384_addcarryx_u32(&x182, &x183, x181, x158, x122); uint32_t x184; fiat_p384_uint1 x185; - fiat_p384_addcarryx_u32(&x184, &x185, 0x0, x178, x181); + fiat_p384_addcarryx_u32(&x184, &x185, x183, x160, x124); uint32_t x186; fiat_p384_uint1 x187; - fiat_p384_addcarryx_u32(&x186, &x187, x185, x176, x179); + fiat_p384_addcarryx_u32(&x186, &x187, x185, x162, x126); uint32_t x188; fiat_p384_uint1 x189; - fiat_p384_addcarryx_u32(&x188, &x189, x187, x174, x177); + fiat_p384_addcarryx_u32(&x188, &x189, x187, x164, x128); uint32_t x190; fiat_p384_uint1 x191; - fiat_p384_addcarryx_u32(&x190, &x191, x189, x172, x175); + fiat_p384_addcarryx_u32(&x190, &x191, x189, x166, x130); uint32_t x192; fiat_p384_uint1 x193; - fiat_p384_addcarryx_u32(&x192, &x193, x191, x170, x173); + fiat_p384_addcarryx_u32(&x192, &x193, x191, x168, x132); uint32_t x194; fiat_p384_uint1 x195; - fiat_p384_addcarryx_u32(&x194, &x195, x193, x168, x171); + fiat_p384_addcarryx_u32(&x194, &x195, x193, x170, x134); uint32_t x196; fiat_p384_uint1 x197; - fiat_p384_addcarryx_u32(&x196, &x197, x195, x166, x169); + fiat_p384_addcarryx_u32(&x196, &x197, x111, 0x0, 0x0); uint32_t x198; fiat_p384_uint1 x199; - fiat_p384_addcarryx_u32(&x198, &x199, x197, x164, x167); + fiat_p384_addcarryx_u32(&x198, &x199, x135, 0x0, (fiat_p384_uint1)x196); uint32_t x200; fiat_p384_uint1 x201; - fiat_p384_addcarryx_u32(&x200, &x201, 0x0, x182, x136); + fiat_p384_addcarryx_u32(&x200, &x201, x171, 0x0, x137); uint32_t x202; fiat_p384_uint1 x203; - fiat_p384_addcarryx_u32(&x202, &x203, x201, x183, x138); + fiat_p384_addcarryx_u32(&x202, &x203, x195, x200, x198); uint32_t x204; fiat_p384_uint1 x205; - fiat_p384_addcarryx_u32(&x204, &x205, x203, 0x0, x140); + fiat_p384_addcarryx_u32(&x204, &x205, 0x0, (arg1[3]), x174); uint32_t x206; fiat_p384_uint1 x207; - fiat_p384_addcarryx_u32(&x206, &x207, x205, x180, x142); + fiat_p384_addcarryx_u32(&x206, &x207, x205, 0x0, x176); uint32_t x208; fiat_p384_uint1 x209; - fiat_p384_addcarryx_u32(&x208, &x209, x207, x184, x144); + fiat_p384_addcarryx_u32(&x208, &x209, x207, 0x0, x178); uint32_t x210; fiat_p384_uint1 x211; - fiat_p384_addcarryx_u32(&x210, &x211, x209, x186, x146); + fiat_p384_addcarryx_u32(&x210, &x211, x209, 0x0, x180); uint32_t x212; fiat_p384_uint1 x213; - fiat_p384_addcarryx_u32(&x212, &x213, x211, x188, x148); + fiat_p384_addcarryx_u32(&x212, &x213, x211, 0x0, x182); uint32_t x214; fiat_p384_uint1 x215; - fiat_p384_addcarryx_u32(&x214, &x215, x213, x190, x150); + fiat_p384_addcarryx_u32(&x214, &x215, x213, 0x0, x184); uint32_t x216; fiat_p384_uint1 x217; - fiat_p384_addcarryx_u32(&x216, &x217, x215, x192, x152); + fiat_p384_addcarryx_u32(&x216, &x217, x215, 0x0, x186); uint32_t x218; fiat_p384_uint1 x219; - fiat_p384_addcarryx_u32(&x218, &x219, x217, x194, x154); + fiat_p384_addcarryx_u32(&x218, &x219, x217, 0x0, x188); uint32_t x220; fiat_p384_uint1 x221; - fiat_p384_addcarryx_u32(&x220, &x221, x219, x196, x156); + fiat_p384_addcarryx_u32(&x220, &x221, x219, 0x0, x190); uint32_t x222; fiat_p384_uint1 x223; - fiat_p384_addcarryx_u32(&x222, &x223, x221, x198, x158); + fiat_p384_addcarryx_u32(&x222, &x223, x221, 0x0, x192); uint32_t x224; fiat_p384_uint1 x225; - fiat_p384_addcarryx_u32(&x224, &x225, x199, 0x0, x165); + fiat_p384_addcarryx_u32(&x224, &x225, x223, 0x0, x194); uint32_t x226; fiat_p384_uint1 x227; - fiat_p384_addcarryx_u32(&x226, &x227, x223, x224, x162); + fiat_p384_addcarryx_u32(&x226, &x227, x225, 0x0, x202); uint32_t x228; - fiat_p384_uint1 x229; - fiat_p384_addcarryx_u32(&x228, &x229, 0x0, (arg1[3]), x202); + uint32_t x229; + fiat_p384_mulx_u32(&x228, &x229, x204, UINT32_C(0xffffffff)); uint32_t x230; - fiat_p384_uint1 x231; - fiat_p384_addcarryx_u32(&x230, &x231, x229, 0x0, x204); + uint32_t x231; + fiat_p384_mulx_u32(&x230, &x231, x204, UINT32_C(0xffffffff)); uint32_t x232; - fiat_p384_uint1 x233; - fiat_p384_addcarryx_u32(&x232, &x233, x231, 0x0, x206); + uint32_t x233; + fiat_p384_mulx_u32(&x232, &x233, x204, UINT32_C(0xffffffff)); uint32_t x234; - fiat_p384_uint1 x235; - fiat_p384_addcarryx_u32(&x234, &x235, x233, 0x0, x208); + uint32_t x235; + fiat_p384_mulx_u32(&x234, &x235, x204, UINT32_C(0xffffffff)); uint32_t x236; - fiat_p384_uint1 x237; - fiat_p384_addcarryx_u32(&x236, &x237, x235, 0x0, x210); + uint32_t x237; + fiat_p384_mulx_u32(&x236, &x237, x204, UINT32_C(0xffffffff)); uint32_t x238; - fiat_p384_uint1 x239; - fiat_p384_addcarryx_u32(&x238, &x239, x237, 0x0, x212); + uint32_t x239; + fiat_p384_mulx_u32(&x238, &x239, x204, UINT32_C(0xffffffff)); uint32_t x240; - fiat_p384_uint1 x241; - fiat_p384_addcarryx_u32(&x240, &x241, x239, 0x0, x214); + uint32_t x241; + fiat_p384_mulx_u32(&x240, &x241, x204, UINT32_C(0xffffffff)); uint32_t x242; - fiat_p384_uint1 x243; - fiat_p384_addcarryx_u32(&x242, &x243, x241, 0x0, x216); + uint32_t x243; + fiat_p384_mulx_u32(&x242, &x243, x204, UINT32_C(0xfffffffe)); uint32_t x244; - fiat_p384_uint1 x245; - fiat_p384_addcarryx_u32(&x244, &x245, x243, 0x0, x218); + uint32_t x245; + fiat_p384_mulx_u32(&x244, &x245, x204, UINT32_C(0xffffffff)); uint32_t x246; - fiat_p384_uint1 x247; - fiat_p384_addcarryx_u32(&x246, &x247, x245, 0x0, x220); + uint32_t x247; + fiat_p384_mulx_u32(&x246, &x247, x204, UINT32_C(0xffffffff)); uint32_t x248; fiat_p384_uint1 x249; - fiat_p384_addcarryx_u32(&x248, &x249, x247, 0x0, x222); + fiat_p384_addcarryx_u32(&x248, &x249, 0x0, x242, x245); uint32_t x250; fiat_p384_uint1 x251; - fiat_p384_addcarryx_u32(&x250, &x251, x249, 0x0, x226); + fiat_p384_addcarryx_u32(&x250, &x251, x249, x240, x243); uint32_t x252; fiat_p384_uint1 x253; - fiat_p384_addcarryx_u32(&x252, &x253, x227, 0x0, x163); + fiat_p384_addcarryx_u32(&x252, &x253, x251, x238, x241); uint32_t x254; fiat_p384_uint1 x255; - fiat_p384_addcarryx_u32(&x254, &x255, x251, 0x0, (fiat_p384_uint1)x252); + fiat_p384_addcarryx_u32(&x254, &x255, x253, x236, x239); uint32_t x256; - uint32_t x257; - fiat_p384_mulx_u32(&x256, &x257, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x257; + fiat_p384_addcarryx_u32(&x256, &x257, x255, x234, x237); uint32_t x258; - uint32_t x259; - fiat_p384_mulx_u32(&x258, &x259, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x259; + fiat_p384_addcarryx_u32(&x258, &x259, x257, x232, x235); uint32_t x260; - uint32_t x261; - fiat_p384_mulx_u32(&x260, &x261, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x261; + fiat_p384_addcarryx_u32(&x260, &x261, x259, x230, x233); uint32_t x262; - uint32_t x263; - fiat_p384_mulx_u32(&x262, &x263, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x263; + fiat_p384_addcarryx_u32(&x262, &x263, x261, x228, x231); uint32_t x264; - uint32_t x265; - fiat_p384_mulx_u32(&x264, &x265, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x265; + fiat_p384_addcarryx_u32(&x264, &x265, 0x0, x246, x204); uint32_t x266; - uint32_t x267; - fiat_p384_mulx_u32(&x266, &x267, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x267; + fiat_p384_addcarryx_u32(&x266, &x267, x265, x247, x206); uint32_t x268; - uint32_t x269; - fiat_p384_mulx_u32(&x268, &x269, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x269; + fiat_p384_addcarryx_u32(&x268, &x269, x267, 0x0, x208); uint32_t x270; - uint32_t x271; - fiat_p384_mulx_u32(&x270, &x271, x228, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x271; + fiat_p384_addcarryx_u32(&x270, &x271, x269, x244, x210); uint32_t x272; - uint32_t x273; - fiat_p384_mulx_u32(&x272, &x273, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x273; + fiat_p384_addcarryx_u32(&x272, &x273, x271, x248, x212); uint32_t x274; - uint32_t x275; - fiat_p384_mulx_u32(&x274, &x275, x228, UINT32_C(0xffffffff)); + fiat_p384_uint1 x275; + fiat_p384_addcarryx_u32(&x274, &x275, x273, x250, x214); uint32_t x276; fiat_p384_uint1 x277; - fiat_p384_addcarryx_u32(&x276, &x277, 0x0, x270, x273); + fiat_p384_addcarryx_u32(&x276, &x277, x275, x252, x216); uint32_t x278; fiat_p384_uint1 x279; - fiat_p384_addcarryx_u32(&x278, &x279, x277, x268, x271); + fiat_p384_addcarryx_u32(&x278, &x279, x277, x254, x218); uint32_t x280; fiat_p384_uint1 x281; - fiat_p384_addcarryx_u32(&x280, &x281, x279, x266, x269); + fiat_p384_addcarryx_u32(&x280, &x281, x279, x256, x220); uint32_t x282; fiat_p384_uint1 x283; - fiat_p384_addcarryx_u32(&x282, &x283, x281, x264, x267); + fiat_p384_addcarryx_u32(&x282, &x283, x281, x258, x222); uint32_t x284; fiat_p384_uint1 x285; - fiat_p384_addcarryx_u32(&x284, &x285, x283, x262, x265); + fiat_p384_addcarryx_u32(&x284, &x285, x283, x260, x224); uint32_t x286; fiat_p384_uint1 x287; - fiat_p384_addcarryx_u32(&x286, &x287, x285, x260, x263); + fiat_p384_addcarryx_u32(&x286, &x287, x285, x262, x226); uint32_t x288; fiat_p384_uint1 x289; - fiat_p384_addcarryx_u32(&x288, &x289, x287, x258, x261); + fiat_p384_addcarryx_u32(&x288, &x289, x203, 0x0, 0x0); uint32_t x290; fiat_p384_uint1 x291; - fiat_p384_addcarryx_u32(&x290, &x291, x289, x256, x259); + fiat_p384_addcarryx_u32(&x290, &x291, x227, 0x0, (fiat_p384_uint1)x288); uint32_t x292; fiat_p384_uint1 x293; - fiat_p384_addcarryx_u32(&x292, &x293, 0x0, x274, x228); + fiat_p384_addcarryx_u32(&x292, &x293, x263, 0x0, x229); uint32_t x294; fiat_p384_uint1 x295; - fiat_p384_addcarryx_u32(&x294, &x295, x293, x275, x230); + fiat_p384_addcarryx_u32(&x294, &x295, x287, x292, x290); uint32_t x296; fiat_p384_uint1 x297; - fiat_p384_addcarryx_u32(&x296, &x297, x295, 0x0, x232); + fiat_p384_addcarryx_u32(&x296, &x297, 0x0, (arg1[4]), x266); uint32_t x298; fiat_p384_uint1 x299; - fiat_p384_addcarryx_u32(&x298, &x299, x297, x272, x234); + fiat_p384_addcarryx_u32(&x298, &x299, x297, 0x0, x268); uint32_t x300; fiat_p384_uint1 x301; - fiat_p384_addcarryx_u32(&x300, &x301, x299, x276, x236); + fiat_p384_addcarryx_u32(&x300, &x301, x299, 0x0, x270); uint32_t x302; fiat_p384_uint1 x303; - fiat_p384_addcarryx_u32(&x302, &x303, x301, x278, x238); + fiat_p384_addcarryx_u32(&x302, &x303, x301, 0x0, x272); uint32_t x304; fiat_p384_uint1 x305; - fiat_p384_addcarryx_u32(&x304, &x305, x303, x280, x240); + fiat_p384_addcarryx_u32(&x304, &x305, x303, 0x0, x274); uint32_t x306; fiat_p384_uint1 x307; - fiat_p384_addcarryx_u32(&x306, &x307, x305, x282, x242); + fiat_p384_addcarryx_u32(&x306, &x307, x305, 0x0, x276); uint32_t x308; fiat_p384_uint1 x309; - fiat_p384_addcarryx_u32(&x308, &x309, x307, x284, x244); + fiat_p384_addcarryx_u32(&x308, &x309, x307, 0x0, x278); uint32_t x310; fiat_p384_uint1 x311; - fiat_p384_addcarryx_u32(&x310, &x311, x309, x286, x246); + fiat_p384_addcarryx_u32(&x310, &x311, x309, 0x0, x280); uint32_t x312; fiat_p384_uint1 x313; - fiat_p384_addcarryx_u32(&x312, &x313, x311, x288, x248); + fiat_p384_addcarryx_u32(&x312, &x313, x311, 0x0, x282); uint32_t x314; fiat_p384_uint1 x315; - fiat_p384_addcarryx_u32(&x314, &x315, x313, x290, x250); + fiat_p384_addcarryx_u32(&x314, &x315, x313, 0x0, x284); uint32_t x316; fiat_p384_uint1 x317; - fiat_p384_addcarryx_u32(&x316, &x317, x291, 0x0, x257); + fiat_p384_addcarryx_u32(&x316, &x317, x315, 0x0, x286); uint32_t x318; fiat_p384_uint1 x319; - fiat_p384_addcarryx_u32(&x318, &x319, x315, x316, x254); + fiat_p384_addcarryx_u32(&x318, &x319, x317, 0x0, x294); uint32_t x320; - fiat_p384_uint1 x321; - fiat_p384_addcarryx_u32(&x320, &x321, 0x0, (arg1[4]), x294); + uint32_t x321; + fiat_p384_mulx_u32(&x320, &x321, x296, UINT32_C(0xffffffff)); uint32_t x322; - fiat_p384_uint1 x323; - fiat_p384_addcarryx_u32(&x322, &x323, x321, 0x0, x296); + uint32_t x323; + fiat_p384_mulx_u32(&x322, &x323, x296, UINT32_C(0xffffffff)); uint32_t x324; - fiat_p384_uint1 x325; - fiat_p384_addcarryx_u32(&x324, &x325, x323, 0x0, x298); + uint32_t x325; + fiat_p384_mulx_u32(&x324, &x325, x296, UINT32_C(0xffffffff)); uint32_t x326; - fiat_p384_uint1 x327; - fiat_p384_addcarryx_u32(&x326, &x327, x325, 0x0, x300); + uint32_t x327; + fiat_p384_mulx_u32(&x326, &x327, x296, UINT32_C(0xffffffff)); uint32_t x328; - fiat_p384_uint1 x329; - fiat_p384_addcarryx_u32(&x328, &x329, x327, 0x0, x302); + uint32_t x329; + fiat_p384_mulx_u32(&x328, &x329, x296, UINT32_C(0xffffffff)); uint32_t x330; - fiat_p384_uint1 x331; - fiat_p384_addcarryx_u32(&x330, &x331, x329, 0x0, x304); + uint32_t x331; + fiat_p384_mulx_u32(&x330, &x331, x296, UINT32_C(0xffffffff)); uint32_t x332; - fiat_p384_uint1 x333; - fiat_p384_addcarryx_u32(&x332, &x333, x331, 0x0, x306); + uint32_t x333; + fiat_p384_mulx_u32(&x332, &x333, x296, UINT32_C(0xffffffff)); uint32_t x334; - fiat_p384_uint1 x335; - fiat_p384_addcarryx_u32(&x334, &x335, x333, 0x0, x308); + uint32_t x335; + fiat_p384_mulx_u32(&x334, &x335, x296, UINT32_C(0xfffffffe)); uint32_t x336; - fiat_p384_uint1 x337; - fiat_p384_addcarryx_u32(&x336, &x337, x335, 0x0, x310); + uint32_t x337; + fiat_p384_mulx_u32(&x336, &x337, x296, UINT32_C(0xffffffff)); uint32_t x338; - fiat_p384_uint1 x339; - fiat_p384_addcarryx_u32(&x338, &x339, x337, 0x0, x312); + uint32_t x339; + fiat_p384_mulx_u32(&x338, &x339, x296, UINT32_C(0xffffffff)); uint32_t x340; fiat_p384_uint1 x341; - fiat_p384_addcarryx_u32(&x340, &x341, x339, 0x0, x314); + fiat_p384_addcarryx_u32(&x340, &x341, 0x0, x334, x337); uint32_t x342; fiat_p384_uint1 x343; - fiat_p384_addcarryx_u32(&x342, &x343, x341, 0x0, x318); + fiat_p384_addcarryx_u32(&x342, &x343, x341, x332, x335); uint32_t x344; fiat_p384_uint1 x345; - fiat_p384_addcarryx_u32(&x344, &x345, x319, 0x0, x255); + fiat_p384_addcarryx_u32(&x344, &x345, x343, x330, x333); uint32_t x346; fiat_p384_uint1 x347; - fiat_p384_addcarryx_u32(&x346, &x347, x343, 0x0, (fiat_p384_uint1)x344); + fiat_p384_addcarryx_u32(&x346, &x347, x345, x328, x331); uint32_t x348; - uint32_t x349; - fiat_p384_mulx_u32(&x348, &x349, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x349; + fiat_p384_addcarryx_u32(&x348, &x349, x347, x326, x329); uint32_t x350; - uint32_t x351; - fiat_p384_mulx_u32(&x350, &x351, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x351; + fiat_p384_addcarryx_u32(&x350, &x351, x349, x324, x327); uint32_t x352; - uint32_t x353; - fiat_p384_mulx_u32(&x352, &x353, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x353; + fiat_p384_addcarryx_u32(&x352, &x353, x351, x322, x325); uint32_t x354; - uint32_t x355; - fiat_p384_mulx_u32(&x354, &x355, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x355; + fiat_p384_addcarryx_u32(&x354, &x355, x353, x320, x323); uint32_t x356; - uint32_t x357; - fiat_p384_mulx_u32(&x356, &x357, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x357; + fiat_p384_addcarryx_u32(&x356, &x357, 0x0, x338, x296); uint32_t x358; - uint32_t x359; - fiat_p384_mulx_u32(&x358, &x359, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x359; + fiat_p384_addcarryx_u32(&x358, &x359, x357, x339, x298); uint32_t x360; - uint32_t x361; - fiat_p384_mulx_u32(&x360, &x361, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x361; + fiat_p384_addcarryx_u32(&x360, &x361, x359, 0x0, x300); uint32_t x362; - uint32_t x363; - fiat_p384_mulx_u32(&x362, &x363, x320, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x363; + fiat_p384_addcarryx_u32(&x362, &x363, x361, x336, x302); uint32_t x364; - uint32_t x365; - fiat_p384_mulx_u32(&x364, &x365, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x365; + fiat_p384_addcarryx_u32(&x364, &x365, x363, x340, x304); uint32_t x366; - uint32_t x367; - fiat_p384_mulx_u32(&x366, &x367, x320, UINT32_C(0xffffffff)); + fiat_p384_uint1 x367; + fiat_p384_addcarryx_u32(&x366, &x367, x365, x342, x306); uint32_t x368; fiat_p384_uint1 x369; - fiat_p384_addcarryx_u32(&x368, &x369, 0x0, x362, x365); + fiat_p384_addcarryx_u32(&x368, &x369, x367, x344, x308); uint32_t x370; fiat_p384_uint1 x371; - fiat_p384_addcarryx_u32(&x370, &x371, x369, x360, x363); + fiat_p384_addcarryx_u32(&x370, &x371, x369, x346, x310); uint32_t x372; fiat_p384_uint1 x373; - fiat_p384_addcarryx_u32(&x372, &x373, x371, x358, x361); + fiat_p384_addcarryx_u32(&x372, &x373, x371, x348, x312); uint32_t x374; fiat_p384_uint1 x375; - fiat_p384_addcarryx_u32(&x374, &x375, x373, x356, x359); + fiat_p384_addcarryx_u32(&x374, &x375, x373, x350, x314); uint32_t x376; fiat_p384_uint1 x377; - fiat_p384_addcarryx_u32(&x376, &x377, x375, x354, x357); + fiat_p384_addcarryx_u32(&x376, &x377, x375, x352, x316); uint32_t x378; fiat_p384_uint1 x379; - fiat_p384_addcarryx_u32(&x378, &x379, x377, x352, x355); + fiat_p384_addcarryx_u32(&x378, &x379, x377, x354, x318); uint32_t x380; fiat_p384_uint1 x381; - fiat_p384_addcarryx_u32(&x380, &x381, x379, x350, x353); + fiat_p384_addcarryx_u32(&x380, &x381, x295, 0x0, 0x0); uint32_t x382; fiat_p384_uint1 x383; - fiat_p384_addcarryx_u32(&x382, &x383, x381, x348, x351); + fiat_p384_addcarryx_u32(&x382, &x383, x319, 0x0, (fiat_p384_uint1)x380); uint32_t x384; fiat_p384_uint1 x385; - fiat_p384_addcarryx_u32(&x384, &x385, 0x0, x366, x320); + fiat_p384_addcarryx_u32(&x384, &x385, x355, 0x0, x321); uint32_t x386; fiat_p384_uint1 x387; - fiat_p384_addcarryx_u32(&x386, &x387, x385, x367, x322); + fiat_p384_addcarryx_u32(&x386, &x387, x379, x384, x382); uint32_t x388; fiat_p384_uint1 x389; - fiat_p384_addcarryx_u32(&x388, &x389, x387, 0x0, x324); + fiat_p384_addcarryx_u32(&x388, &x389, 0x0, (arg1[5]), x358); uint32_t x390; fiat_p384_uint1 x391; - fiat_p384_addcarryx_u32(&x390, &x391, x389, x364, x326); + fiat_p384_addcarryx_u32(&x390, &x391, x389, 0x0, x360); uint32_t x392; fiat_p384_uint1 x393; - fiat_p384_addcarryx_u32(&x392, &x393, x391, x368, x328); + fiat_p384_addcarryx_u32(&x392, &x393, x391, 0x0, x362); uint32_t x394; fiat_p384_uint1 x395; - fiat_p384_addcarryx_u32(&x394, &x395, x393, x370, x330); + fiat_p384_addcarryx_u32(&x394, &x395, x393, 0x0, x364); uint32_t x396; fiat_p384_uint1 x397; - fiat_p384_addcarryx_u32(&x396, &x397, x395, x372, x332); + fiat_p384_addcarryx_u32(&x396, &x397, x395, 0x0, x366); uint32_t x398; fiat_p384_uint1 x399; - fiat_p384_addcarryx_u32(&x398, &x399, x397, x374, x334); + fiat_p384_addcarryx_u32(&x398, &x399, x397, 0x0, x368); uint32_t x400; fiat_p384_uint1 x401; - fiat_p384_addcarryx_u32(&x400, &x401, x399, x376, x336); + fiat_p384_addcarryx_u32(&x400, &x401, x399, 0x0, x370); uint32_t x402; fiat_p384_uint1 x403; - fiat_p384_addcarryx_u32(&x402, &x403, x401, x378, x338); + fiat_p384_addcarryx_u32(&x402, &x403, x401, 0x0, x372); uint32_t x404; fiat_p384_uint1 x405; - fiat_p384_addcarryx_u32(&x404, &x405, x403, x380, x340); + fiat_p384_addcarryx_u32(&x404, &x405, x403, 0x0, x374); uint32_t x406; fiat_p384_uint1 x407; - fiat_p384_addcarryx_u32(&x406, &x407, x405, x382, x342); + fiat_p384_addcarryx_u32(&x406, &x407, x405, 0x0, x376); uint32_t x408; fiat_p384_uint1 x409; - fiat_p384_addcarryx_u32(&x408, &x409, x383, 0x0, x349); + fiat_p384_addcarryx_u32(&x408, &x409, x407, 0x0, x378); uint32_t x410; fiat_p384_uint1 x411; - fiat_p384_addcarryx_u32(&x410, &x411, x407, x408, x346); + fiat_p384_addcarryx_u32(&x410, &x411, x409, 0x0, x386); uint32_t x412; - fiat_p384_uint1 x413; - fiat_p384_addcarryx_u32(&x412, &x413, 0x0, (arg1[5]), x386); + uint32_t x413; + fiat_p384_mulx_u32(&x412, &x413, x388, UINT32_C(0xffffffff)); uint32_t x414; - fiat_p384_uint1 x415; - fiat_p384_addcarryx_u32(&x414, &x415, x413, 0x0, x388); + uint32_t x415; + fiat_p384_mulx_u32(&x414, &x415, x388, UINT32_C(0xffffffff)); uint32_t x416; - fiat_p384_uint1 x417; - fiat_p384_addcarryx_u32(&x416, &x417, x415, 0x0, x390); + uint32_t x417; + fiat_p384_mulx_u32(&x416, &x417, x388, UINT32_C(0xffffffff)); uint32_t x418; - fiat_p384_uint1 x419; - fiat_p384_addcarryx_u32(&x418, &x419, x417, 0x0, x392); + uint32_t x419; + fiat_p384_mulx_u32(&x418, &x419, x388, UINT32_C(0xffffffff)); uint32_t x420; - fiat_p384_uint1 x421; - fiat_p384_addcarryx_u32(&x420, &x421, x419, 0x0, x394); + uint32_t x421; + fiat_p384_mulx_u32(&x420, &x421, x388, UINT32_C(0xffffffff)); uint32_t x422; - fiat_p384_uint1 x423; - fiat_p384_addcarryx_u32(&x422, &x423, x421, 0x0, x396); + uint32_t x423; + fiat_p384_mulx_u32(&x422, &x423, x388, UINT32_C(0xffffffff)); uint32_t x424; - fiat_p384_uint1 x425; - fiat_p384_addcarryx_u32(&x424, &x425, x423, 0x0, x398); + uint32_t x425; + fiat_p384_mulx_u32(&x424, &x425, x388, UINT32_C(0xffffffff)); uint32_t x426; - fiat_p384_uint1 x427; - fiat_p384_addcarryx_u32(&x426, &x427, x425, 0x0, x400); + uint32_t x427; + fiat_p384_mulx_u32(&x426, &x427, x388, UINT32_C(0xfffffffe)); uint32_t x428; - fiat_p384_uint1 x429; - fiat_p384_addcarryx_u32(&x428, &x429, x427, 0x0, x402); + uint32_t x429; + fiat_p384_mulx_u32(&x428, &x429, x388, UINT32_C(0xffffffff)); uint32_t x430; - fiat_p384_uint1 x431; - fiat_p384_addcarryx_u32(&x430, &x431, x429, 0x0, x404); + uint32_t x431; + fiat_p384_mulx_u32(&x430, &x431, x388, UINT32_C(0xffffffff)); uint32_t x432; fiat_p384_uint1 x433; - fiat_p384_addcarryx_u32(&x432, &x433, x431, 0x0, x406); + fiat_p384_addcarryx_u32(&x432, &x433, 0x0, x426, x429); uint32_t x434; fiat_p384_uint1 x435; - fiat_p384_addcarryx_u32(&x434, &x435, x433, 0x0, x410); + fiat_p384_addcarryx_u32(&x434, &x435, x433, x424, x427); uint32_t x436; fiat_p384_uint1 x437; - fiat_p384_addcarryx_u32(&x436, &x437, x411, 0x0, x347); + fiat_p384_addcarryx_u32(&x436, &x437, x435, x422, x425); uint32_t x438; fiat_p384_uint1 x439; - fiat_p384_addcarryx_u32(&x438, &x439, x435, 0x0, (fiat_p384_uint1)x436); + fiat_p384_addcarryx_u32(&x438, &x439, x437, x420, x423); uint32_t x440; - uint32_t x441; - fiat_p384_mulx_u32(&x440, &x441, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x441; + fiat_p384_addcarryx_u32(&x440, &x441, x439, x418, x421); uint32_t x442; - uint32_t x443; - fiat_p384_mulx_u32(&x442, &x443, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x443; + fiat_p384_addcarryx_u32(&x442, &x443, x441, x416, x419); uint32_t x444; - uint32_t x445; - fiat_p384_mulx_u32(&x444, &x445, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x445; + fiat_p384_addcarryx_u32(&x444, &x445, x443, x414, x417); uint32_t x446; - uint32_t x447; - fiat_p384_mulx_u32(&x446, &x447, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x447; + fiat_p384_addcarryx_u32(&x446, &x447, x445, x412, x415); uint32_t x448; - uint32_t x449; - fiat_p384_mulx_u32(&x448, &x449, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x449; + fiat_p384_addcarryx_u32(&x448, &x449, 0x0, x430, x388); uint32_t x450; - uint32_t x451; - fiat_p384_mulx_u32(&x450, &x451, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x451; + fiat_p384_addcarryx_u32(&x450, &x451, x449, x431, x390); uint32_t x452; - uint32_t x453; - fiat_p384_mulx_u32(&x452, &x453, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x453; + fiat_p384_addcarryx_u32(&x452, &x453, x451, 0x0, x392); uint32_t x454; - uint32_t x455; - fiat_p384_mulx_u32(&x454, &x455, x412, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x455; + fiat_p384_addcarryx_u32(&x454, &x455, x453, x428, x394); uint32_t x456; - uint32_t x457; - fiat_p384_mulx_u32(&x456, &x457, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x457; + fiat_p384_addcarryx_u32(&x456, &x457, x455, x432, x396); uint32_t x458; - uint32_t x459; - fiat_p384_mulx_u32(&x458, &x459, x412, UINT32_C(0xffffffff)); + fiat_p384_uint1 x459; + fiat_p384_addcarryx_u32(&x458, &x459, x457, x434, x398); uint32_t x460; fiat_p384_uint1 x461; - fiat_p384_addcarryx_u32(&x460, &x461, 0x0, x454, x457); + fiat_p384_addcarryx_u32(&x460, &x461, x459, x436, x400); uint32_t x462; fiat_p384_uint1 x463; - fiat_p384_addcarryx_u32(&x462, &x463, x461, x452, x455); + fiat_p384_addcarryx_u32(&x462, &x463, x461, x438, x402); uint32_t x464; fiat_p384_uint1 x465; - fiat_p384_addcarryx_u32(&x464, &x465, x463, x450, x453); + fiat_p384_addcarryx_u32(&x464, &x465, x463, x440, x404); uint32_t x466; fiat_p384_uint1 x467; - fiat_p384_addcarryx_u32(&x466, &x467, x465, x448, x451); + fiat_p384_addcarryx_u32(&x466, &x467, x465, x442, x406); uint32_t x468; fiat_p384_uint1 x469; - fiat_p384_addcarryx_u32(&x468, &x469, x467, x446, x449); + fiat_p384_addcarryx_u32(&x468, &x469, x467, x444, x408); uint32_t x470; fiat_p384_uint1 x471; - fiat_p384_addcarryx_u32(&x470, &x471, x469, x444, x447); + fiat_p384_addcarryx_u32(&x470, &x471, x469, x446, x410); uint32_t x472; fiat_p384_uint1 x473; - fiat_p384_addcarryx_u32(&x472, &x473, x471, x442, x445); + fiat_p384_addcarryx_u32(&x472, &x473, x387, 0x0, 0x0); uint32_t x474; fiat_p384_uint1 x475; - fiat_p384_addcarryx_u32(&x474, &x475, x473, x440, x443); + fiat_p384_addcarryx_u32(&x474, &x475, x411, 0x0, (fiat_p384_uint1)x472); uint32_t x476; fiat_p384_uint1 x477; - fiat_p384_addcarryx_u32(&x476, &x477, 0x0, x458, x412); + fiat_p384_addcarryx_u32(&x476, &x477, x447, 0x0, x413); uint32_t x478; fiat_p384_uint1 x479; - fiat_p384_addcarryx_u32(&x478, &x479, x477, x459, x414); + fiat_p384_addcarryx_u32(&x478, &x479, x471, x476, x474); uint32_t x480; fiat_p384_uint1 x481; - fiat_p384_addcarryx_u32(&x480, &x481, x479, 0x0, x416); + fiat_p384_addcarryx_u32(&x480, &x481, 0x0, (arg1[6]), x450); uint32_t x482; fiat_p384_uint1 x483; - fiat_p384_addcarryx_u32(&x482, &x483, x481, x456, x418); + fiat_p384_addcarryx_u32(&x482, &x483, x481, 0x0, x452); uint32_t x484; fiat_p384_uint1 x485; - fiat_p384_addcarryx_u32(&x484, &x485, x483, x460, x420); + fiat_p384_addcarryx_u32(&x484, &x485, x483, 0x0, x454); uint32_t x486; fiat_p384_uint1 x487; - fiat_p384_addcarryx_u32(&x486, &x487, x485, x462, x422); + fiat_p384_addcarryx_u32(&x486, &x487, x485, 0x0, x456); uint32_t x488; fiat_p384_uint1 x489; - fiat_p384_addcarryx_u32(&x488, &x489, x487, x464, x424); + fiat_p384_addcarryx_u32(&x488, &x489, x487, 0x0, x458); uint32_t x490; fiat_p384_uint1 x491; - fiat_p384_addcarryx_u32(&x490, &x491, x489, x466, x426); + fiat_p384_addcarryx_u32(&x490, &x491, x489, 0x0, x460); uint32_t x492; fiat_p384_uint1 x493; - fiat_p384_addcarryx_u32(&x492, &x493, x491, x468, x428); + fiat_p384_addcarryx_u32(&x492, &x493, x491, 0x0, x462); uint32_t x494; fiat_p384_uint1 x495; - fiat_p384_addcarryx_u32(&x494, &x495, x493, x470, x430); + fiat_p384_addcarryx_u32(&x494, &x495, x493, 0x0, x464); uint32_t x496; fiat_p384_uint1 x497; - fiat_p384_addcarryx_u32(&x496, &x497, x495, x472, x432); + fiat_p384_addcarryx_u32(&x496, &x497, x495, 0x0, x466); uint32_t x498; fiat_p384_uint1 x499; - fiat_p384_addcarryx_u32(&x498, &x499, x497, x474, x434); + fiat_p384_addcarryx_u32(&x498, &x499, x497, 0x0, x468); uint32_t x500; fiat_p384_uint1 x501; - fiat_p384_addcarryx_u32(&x500, &x501, x475, 0x0, x441); + fiat_p384_addcarryx_u32(&x500, &x501, x499, 0x0, x470); uint32_t x502; fiat_p384_uint1 x503; - fiat_p384_addcarryx_u32(&x502, &x503, x499, x500, x438); + fiat_p384_addcarryx_u32(&x502, &x503, x501, 0x0, x478); uint32_t x504; - fiat_p384_uint1 x505; - fiat_p384_addcarryx_u32(&x504, &x505, 0x0, (arg1[6]), x478); + uint32_t x505; + fiat_p384_mulx_u32(&x504, &x505, x480, UINT32_C(0xffffffff)); uint32_t x506; - fiat_p384_uint1 x507; - fiat_p384_addcarryx_u32(&x506, &x507, x505, 0x0, x480); + uint32_t x507; + fiat_p384_mulx_u32(&x506, &x507, x480, UINT32_C(0xffffffff)); uint32_t x508; - fiat_p384_uint1 x509; - fiat_p384_addcarryx_u32(&x508, &x509, x507, 0x0, x482); + uint32_t x509; + fiat_p384_mulx_u32(&x508, &x509, x480, UINT32_C(0xffffffff)); uint32_t x510; - fiat_p384_uint1 x511; - fiat_p384_addcarryx_u32(&x510, &x511, x509, 0x0, x484); + uint32_t x511; + fiat_p384_mulx_u32(&x510, &x511, x480, UINT32_C(0xffffffff)); uint32_t x512; - fiat_p384_uint1 x513; - fiat_p384_addcarryx_u32(&x512, &x513, x511, 0x0, x486); + uint32_t x513; + fiat_p384_mulx_u32(&x512, &x513, x480, UINT32_C(0xffffffff)); uint32_t x514; - fiat_p384_uint1 x515; - fiat_p384_addcarryx_u32(&x514, &x515, x513, 0x0, x488); + uint32_t x515; + fiat_p384_mulx_u32(&x514, &x515, x480, UINT32_C(0xffffffff)); uint32_t x516; - fiat_p384_uint1 x517; - fiat_p384_addcarryx_u32(&x516, &x517, x515, 0x0, x490); + uint32_t x517; + fiat_p384_mulx_u32(&x516, &x517, x480, UINT32_C(0xffffffff)); uint32_t x518; - fiat_p384_uint1 x519; - fiat_p384_addcarryx_u32(&x518, &x519, x517, 0x0, x492); + uint32_t x519; + fiat_p384_mulx_u32(&x518, &x519, x480, UINT32_C(0xfffffffe)); uint32_t x520; - fiat_p384_uint1 x521; - fiat_p384_addcarryx_u32(&x520, &x521, x519, 0x0, x494); + uint32_t x521; + fiat_p384_mulx_u32(&x520, &x521, x480, UINT32_C(0xffffffff)); uint32_t x522; - fiat_p384_uint1 x523; - fiat_p384_addcarryx_u32(&x522, &x523, x521, 0x0, x496); + uint32_t x523; + fiat_p384_mulx_u32(&x522, &x523, x480, UINT32_C(0xffffffff)); uint32_t x524; fiat_p384_uint1 x525; - fiat_p384_addcarryx_u32(&x524, &x525, x523, 0x0, x498); + fiat_p384_addcarryx_u32(&x524, &x525, 0x0, x518, x521); uint32_t x526; fiat_p384_uint1 x527; - fiat_p384_addcarryx_u32(&x526, &x527, x525, 0x0, x502); + fiat_p384_addcarryx_u32(&x526, &x527, x525, x516, x519); uint32_t x528; fiat_p384_uint1 x529; - fiat_p384_addcarryx_u32(&x528, &x529, x503, 0x0, x439); + fiat_p384_addcarryx_u32(&x528, &x529, x527, x514, x517); uint32_t x530; fiat_p384_uint1 x531; - fiat_p384_addcarryx_u32(&x530, &x531, x527, 0x0, (fiat_p384_uint1)x528); + fiat_p384_addcarryx_u32(&x530, &x531, x529, x512, x515); uint32_t x532; - uint32_t x533; - fiat_p384_mulx_u32(&x532, &x533, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x533; + fiat_p384_addcarryx_u32(&x532, &x533, x531, x510, x513); uint32_t x534; - uint32_t x535; - fiat_p384_mulx_u32(&x534, &x535, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x535; + fiat_p384_addcarryx_u32(&x534, &x535, x533, x508, x511); uint32_t x536; - uint32_t x537; - fiat_p384_mulx_u32(&x536, &x537, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x537; + fiat_p384_addcarryx_u32(&x536, &x537, x535, x506, x509); uint32_t x538; - uint32_t x539; - fiat_p384_mulx_u32(&x538, &x539, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x539; + fiat_p384_addcarryx_u32(&x538, &x539, x537, x504, x507); uint32_t x540; - uint32_t x541; - fiat_p384_mulx_u32(&x540, &x541, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x541; + fiat_p384_addcarryx_u32(&x540, &x541, 0x0, x522, x480); uint32_t x542; - uint32_t x543; - fiat_p384_mulx_u32(&x542, &x543, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x543; + fiat_p384_addcarryx_u32(&x542, &x543, x541, x523, x482); uint32_t x544; - uint32_t x545; - fiat_p384_mulx_u32(&x544, &x545, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x545; + fiat_p384_addcarryx_u32(&x544, &x545, x543, 0x0, x484); uint32_t x546; - uint32_t x547; - fiat_p384_mulx_u32(&x546, &x547, x504, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x547; + fiat_p384_addcarryx_u32(&x546, &x547, x545, x520, x486); uint32_t x548; - uint32_t x549; - fiat_p384_mulx_u32(&x548, &x549, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x549; + fiat_p384_addcarryx_u32(&x548, &x549, x547, x524, x488); uint32_t x550; - uint32_t x551; - fiat_p384_mulx_u32(&x550, &x551, x504, UINT32_C(0xffffffff)); + fiat_p384_uint1 x551; + fiat_p384_addcarryx_u32(&x550, &x551, x549, x526, x490); uint32_t x552; fiat_p384_uint1 x553; - fiat_p384_addcarryx_u32(&x552, &x553, 0x0, x546, x549); + fiat_p384_addcarryx_u32(&x552, &x553, x551, x528, x492); uint32_t x554; fiat_p384_uint1 x555; - fiat_p384_addcarryx_u32(&x554, &x555, x553, x544, x547); + fiat_p384_addcarryx_u32(&x554, &x555, x553, x530, x494); uint32_t x556; fiat_p384_uint1 x557; - fiat_p384_addcarryx_u32(&x556, &x557, x555, x542, x545); + fiat_p384_addcarryx_u32(&x556, &x557, x555, x532, x496); uint32_t x558; fiat_p384_uint1 x559; - fiat_p384_addcarryx_u32(&x558, &x559, x557, x540, x543); + fiat_p384_addcarryx_u32(&x558, &x559, x557, x534, x498); uint32_t x560; fiat_p384_uint1 x561; - fiat_p384_addcarryx_u32(&x560, &x561, x559, x538, x541); + fiat_p384_addcarryx_u32(&x560, &x561, x559, x536, x500); uint32_t x562; fiat_p384_uint1 x563; - fiat_p384_addcarryx_u32(&x562, &x563, x561, x536, x539); + fiat_p384_addcarryx_u32(&x562, &x563, x561, x538, x502); uint32_t x564; fiat_p384_uint1 x565; - fiat_p384_addcarryx_u32(&x564, &x565, x563, x534, x537); + fiat_p384_addcarryx_u32(&x564, &x565, x479, 0x0, 0x0); uint32_t x566; fiat_p384_uint1 x567; - fiat_p384_addcarryx_u32(&x566, &x567, x565, x532, x535); + fiat_p384_addcarryx_u32(&x566, &x567, x503, 0x0, (fiat_p384_uint1)x564); uint32_t x568; fiat_p384_uint1 x569; - fiat_p384_addcarryx_u32(&x568, &x569, 0x0, x550, x504); + fiat_p384_addcarryx_u32(&x568, &x569, x539, 0x0, x505); uint32_t x570; fiat_p384_uint1 x571; - fiat_p384_addcarryx_u32(&x570, &x571, x569, x551, x506); + fiat_p384_addcarryx_u32(&x570, &x571, x563, x568, x566); uint32_t x572; fiat_p384_uint1 x573; - fiat_p384_addcarryx_u32(&x572, &x573, x571, 0x0, x508); + fiat_p384_addcarryx_u32(&x572, &x573, 0x0, (arg1[7]), x542); uint32_t x574; fiat_p384_uint1 x575; - fiat_p384_addcarryx_u32(&x574, &x575, x573, x548, x510); + fiat_p384_addcarryx_u32(&x574, &x575, x573, 0x0, x544); uint32_t x576; fiat_p384_uint1 x577; - fiat_p384_addcarryx_u32(&x576, &x577, x575, x552, x512); + fiat_p384_addcarryx_u32(&x576, &x577, x575, 0x0, x546); uint32_t x578; fiat_p384_uint1 x579; - fiat_p384_addcarryx_u32(&x578, &x579, x577, x554, x514); + fiat_p384_addcarryx_u32(&x578, &x579, x577, 0x0, x548); uint32_t x580; fiat_p384_uint1 x581; - fiat_p384_addcarryx_u32(&x580, &x581, x579, x556, x516); + fiat_p384_addcarryx_u32(&x580, &x581, x579, 0x0, x550); uint32_t x582; fiat_p384_uint1 x583; - fiat_p384_addcarryx_u32(&x582, &x583, x581, x558, x518); + fiat_p384_addcarryx_u32(&x582, &x583, x581, 0x0, x552); uint32_t x584; fiat_p384_uint1 x585; - fiat_p384_addcarryx_u32(&x584, &x585, x583, x560, x520); + fiat_p384_addcarryx_u32(&x584, &x585, x583, 0x0, x554); uint32_t x586; fiat_p384_uint1 x587; - fiat_p384_addcarryx_u32(&x586, &x587, x585, x562, x522); + fiat_p384_addcarryx_u32(&x586, &x587, x585, 0x0, x556); uint32_t x588; fiat_p384_uint1 x589; - fiat_p384_addcarryx_u32(&x588, &x589, x587, x564, x524); + fiat_p384_addcarryx_u32(&x588, &x589, x587, 0x0, x558); uint32_t x590; fiat_p384_uint1 x591; - fiat_p384_addcarryx_u32(&x590, &x591, x589, x566, x526); + fiat_p384_addcarryx_u32(&x590, &x591, x589, 0x0, x560); uint32_t x592; fiat_p384_uint1 x593; - fiat_p384_addcarryx_u32(&x592, &x593, x567, 0x0, x533); + fiat_p384_addcarryx_u32(&x592, &x593, x591, 0x0, x562); uint32_t x594; fiat_p384_uint1 x595; - fiat_p384_addcarryx_u32(&x594, &x595, x591, x592, x530); + fiat_p384_addcarryx_u32(&x594, &x595, x593, 0x0, x570); uint32_t x596; - fiat_p384_uint1 x597; - fiat_p384_addcarryx_u32(&x596, &x597, 0x0, (arg1[7]), x570); + uint32_t x597; + fiat_p384_mulx_u32(&x596, &x597, x572, UINT32_C(0xffffffff)); uint32_t x598; - fiat_p384_uint1 x599; - fiat_p384_addcarryx_u32(&x598, &x599, x597, 0x0, x572); + uint32_t x599; + fiat_p384_mulx_u32(&x598, &x599, x572, UINT32_C(0xffffffff)); uint32_t x600; - fiat_p384_uint1 x601; - fiat_p384_addcarryx_u32(&x600, &x601, x599, 0x0, x574); + uint32_t x601; + fiat_p384_mulx_u32(&x600, &x601, x572, UINT32_C(0xffffffff)); uint32_t x602; - fiat_p384_uint1 x603; - fiat_p384_addcarryx_u32(&x602, &x603, x601, 0x0, x576); + uint32_t x603; + fiat_p384_mulx_u32(&x602, &x603, x572, UINT32_C(0xffffffff)); uint32_t x604; - fiat_p384_uint1 x605; - fiat_p384_addcarryx_u32(&x604, &x605, x603, 0x0, x578); + uint32_t x605; + fiat_p384_mulx_u32(&x604, &x605, x572, UINT32_C(0xffffffff)); uint32_t x606; - fiat_p384_uint1 x607; - fiat_p384_addcarryx_u32(&x606, &x607, x605, 0x0, x580); + uint32_t x607; + fiat_p384_mulx_u32(&x606, &x607, x572, UINT32_C(0xffffffff)); uint32_t x608; - fiat_p384_uint1 x609; - fiat_p384_addcarryx_u32(&x608, &x609, x607, 0x0, x582); + uint32_t x609; + fiat_p384_mulx_u32(&x608, &x609, x572, UINT32_C(0xffffffff)); uint32_t x610; - fiat_p384_uint1 x611; - fiat_p384_addcarryx_u32(&x610, &x611, x609, 0x0, x584); + uint32_t x611; + fiat_p384_mulx_u32(&x610, &x611, x572, UINT32_C(0xfffffffe)); uint32_t x612; - fiat_p384_uint1 x613; - fiat_p384_addcarryx_u32(&x612, &x613, x611, 0x0, x586); + uint32_t x613; + fiat_p384_mulx_u32(&x612, &x613, x572, UINT32_C(0xffffffff)); uint32_t x614; - fiat_p384_uint1 x615; - fiat_p384_addcarryx_u32(&x614, &x615, x613, 0x0, x588); + uint32_t x615; + fiat_p384_mulx_u32(&x614, &x615, x572, UINT32_C(0xffffffff)); uint32_t x616; fiat_p384_uint1 x617; - fiat_p384_addcarryx_u32(&x616, &x617, x615, 0x0, x590); + fiat_p384_addcarryx_u32(&x616, &x617, 0x0, x610, x613); uint32_t x618; fiat_p384_uint1 x619; - fiat_p384_addcarryx_u32(&x618, &x619, x617, 0x0, x594); + fiat_p384_addcarryx_u32(&x618, &x619, x617, x608, x611); uint32_t x620; fiat_p384_uint1 x621; - fiat_p384_addcarryx_u32(&x620, &x621, x595, 0x0, x531); + fiat_p384_addcarryx_u32(&x620, &x621, x619, x606, x609); uint32_t x622; fiat_p384_uint1 x623; - fiat_p384_addcarryx_u32(&x622, &x623, x619, 0x0, (fiat_p384_uint1)x620); + fiat_p384_addcarryx_u32(&x622, &x623, x621, x604, x607); uint32_t x624; - uint32_t x625; - fiat_p384_mulx_u32(&x624, &x625, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x625; + fiat_p384_addcarryx_u32(&x624, &x625, x623, x602, x605); uint32_t x626; - uint32_t x627; - fiat_p384_mulx_u32(&x626, &x627, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x627; + fiat_p384_addcarryx_u32(&x626, &x627, x625, x600, x603); uint32_t x628; - uint32_t x629; - fiat_p384_mulx_u32(&x628, &x629, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x629; + fiat_p384_addcarryx_u32(&x628, &x629, x627, x598, x601); uint32_t x630; - uint32_t x631; - fiat_p384_mulx_u32(&x630, &x631, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x631; + fiat_p384_addcarryx_u32(&x630, &x631, x629, x596, x599); uint32_t x632; - uint32_t x633; - fiat_p384_mulx_u32(&x632, &x633, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x633; + fiat_p384_addcarryx_u32(&x632, &x633, 0x0, x614, x572); uint32_t x634; - uint32_t x635; - fiat_p384_mulx_u32(&x634, &x635, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x635; + fiat_p384_addcarryx_u32(&x634, &x635, x633, x615, x574); uint32_t x636; - uint32_t x637; - fiat_p384_mulx_u32(&x636, &x637, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x637; + fiat_p384_addcarryx_u32(&x636, &x637, x635, 0x0, x576); uint32_t x638; - uint32_t x639; - fiat_p384_mulx_u32(&x638, &x639, x596, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x639; + fiat_p384_addcarryx_u32(&x638, &x639, x637, x612, x578); uint32_t x640; - uint32_t x641; - fiat_p384_mulx_u32(&x640, &x641, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x641; + fiat_p384_addcarryx_u32(&x640, &x641, x639, x616, x580); uint32_t x642; - uint32_t x643; - fiat_p384_mulx_u32(&x642, &x643, x596, UINT32_C(0xffffffff)); + fiat_p384_uint1 x643; + fiat_p384_addcarryx_u32(&x642, &x643, x641, x618, x582); uint32_t x644; fiat_p384_uint1 x645; - fiat_p384_addcarryx_u32(&x644, &x645, 0x0, x638, x641); + fiat_p384_addcarryx_u32(&x644, &x645, x643, x620, x584); uint32_t x646; fiat_p384_uint1 x647; - fiat_p384_addcarryx_u32(&x646, &x647, x645, x636, x639); + fiat_p384_addcarryx_u32(&x646, &x647, x645, x622, x586); uint32_t x648; fiat_p384_uint1 x649; - fiat_p384_addcarryx_u32(&x648, &x649, x647, x634, x637); + fiat_p384_addcarryx_u32(&x648, &x649, x647, x624, x588); uint32_t x650; fiat_p384_uint1 x651; - fiat_p384_addcarryx_u32(&x650, &x651, x649, x632, x635); + fiat_p384_addcarryx_u32(&x650, &x651, x649, x626, x590); uint32_t x652; fiat_p384_uint1 x653; - fiat_p384_addcarryx_u32(&x652, &x653, x651, x630, x633); + fiat_p384_addcarryx_u32(&x652, &x653, x651, x628, x592); uint32_t x654; fiat_p384_uint1 x655; - fiat_p384_addcarryx_u32(&x654, &x655, x653, x628, x631); + fiat_p384_addcarryx_u32(&x654, &x655, x653, x630, x594); uint32_t x656; fiat_p384_uint1 x657; - fiat_p384_addcarryx_u32(&x656, &x657, x655, x626, x629); + fiat_p384_addcarryx_u32(&x656, &x657, x571, 0x0, 0x0); uint32_t x658; fiat_p384_uint1 x659; - fiat_p384_addcarryx_u32(&x658, &x659, x657, x624, x627); + fiat_p384_addcarryx_u32(&x658, &x659, x595, 0x0, (fiat_p384_uint1)x656); uint32_t x660; fiat_p384_uint1 x661; - fiat_p384_addcarryx_u32(&x660, &x661, 0x0, x642, x596); + fiat_p384_addcarryx_u32(&x660, &x661, x631, 0x0, x597); uint32_t x662; fiat_p384_uint1 x663; - fiat_p384_addcarryx_u32(&x662, &x663, x661, x643, x598); + fiat_p384_addcarryx_u32(&x662, &x663, x655, x660, x658); uint32_t x664; fiat_p384_uint1 x665; - fiat_p384_addcarryx_u32(&x664, &x665, x663, 0x0, x600); + fiat_p384_addcarryx_u32(&x664, &x665, 0x0, (arg1[8]), x634); uint32_t x666; fiat_p384_uint1 x667; - fiat_p384_addcarryx_u32(&x666, &x667, x665, x640, x602); + fiat_p384_addcarryx_u32(&x666, &x667, x665, 0x0, x636); uint32_t x668; fiat_p384_uint1 x669; - fiat_p384_addcarryx_u32(&x668, &x669, x667, x644, x604); + fiat_p384_addcarryx_u32(&x668, &x669, x667, 0x0, x638); uint32_t x670; fiat_p384_uint1 x671; - fiat_p384_addcarryx_u32(&x670, &x671, x669, x646, x606); + fiat_p384_addcarryx_u32(&x670, &x671, x669, 0x0, x640); uint32_t x672; fiat_p384_uint1 x673; - fiat_p384_addcarryx_u32(&x672, &x673, x671, x648, x608); + fiat_p384_addcarryx_u32(&x672, &x673, x671, 0x0, x642); uint32_t x674; fiat_p384_uint1 x675; - fiat_p384_addcarryx_u32(&x674, &x675, x673, x650, x610); + fiat_p384_addcarryx_u32(&x674, &x675, x673, 0x0, x644); uint32_t x676; fiat_p384_uint1 x677; - fiat_p384_addcarryx_u32(&x676, &x677, x675, x652, x612); + fiat_p384_addcarryx_u32(&x676, &x677, x675, 0x0, x646); uint32_t x678; fiat_p384_uint1 x679; - fiat_p384_addcarryx_u32(&x678, &x679, x677, x654, x614); + fiat_p384_addcarryx_u32(&x678, &x679, x677, 0x0, x648); uint32_t x680; fiat_p384_uint1 x681; - fiat_p384_addcarryx_u32(&x680, &x681, x679, x656, x616); + fiat_p384_addcarryx_u32(&x680, &x681, x679, 0x0, x650); uint32_t x682; fiat_p384_uint1 x683; - fiat_p384_addcarryx_u32(&x682, &x683, x681, x658, x618); + fiat_p384_addcarryx_u32(&x682, &x683, x681, 0x0, x652); uint32_t x684; fiat_p384_uint1 x685; - fiat_p384_addcarryx_u32(&x684, &x685, x659, 0x0, x625); + fiat_p384_addcarryx_u32(&x684, &x685, x683, 0x0, x654); uint32_t x686; fiat_p384_uint1 x687; - fiat_p384_addcarryx_u32(&x686, &x687, x683, x684, x622); + fiat_p384_addcarryx_u32(&x686, &x687, x685, 0x0, x662); uint32_t x688; - fiat_p384_uint1 x689; - fiat_p384_addcarryx_u32(&x688, &x689, 0x0, (arg1[8]), x662); + uint32_t x689; + fiat_p384_mulx_u32(&x688, &x689, x664, UINT32_C(0xffffffff)); uint32_t x690; - fiat_p384_uint1 x691; - fiat_p384_addcarryx_u32(&x690, &x691, x689, 0x0, x664); + uint32_t x691; + fiat_p384_mulx_u32(&x690, &x691, x664, UINT32_C(0xffffffff)); uint32_t x692; - fiat_p384_uint1 x693; - fiat_p384_addcarryx_u32(&x692, &x693, x691, 0x0, x666); + uint32_t x693; + fiat_p384_mulx_u32(&x692, &x693, x664, UINT32_C(0xffffffff)); uint32_t x694; - fiat_p384_uint1 x695; - fiat_p384_addcarryx_u32(&x694, &x695, x693, 0x0, x668); + uint32_t x695; + fiat_p384_mulx_u32(&x694, &x695, x664, UINT32_C(0xffffffff)); uint32_t x696; - fiat_p384_uint1 x697; - fiat_p384_addcarryx_u32(&x696, &x697, x695, 0x0, x670); + uint32_t x697; + fiat_p384_mulx_u32(&x696, &x697, x664, UINT32_C(0xffffffff)); uint32_t x698; - fiat_p384_uint1 x699; - fiat_p384_addcarryx_u32(&x698, &x699, x697, 0x0, x672); + uint32_t x699; + fiat_p384_mulx_u32(&x698, &x699, x664, UINT32_C(0xffffffff)); uint32_t x700; - fiat_p384_uint1 x701; - fiat_p384_addcarryx_u32(&x700, &x701, x699, 0x0, x674); + uint32_t x701; + fiat_p384_mulx_u32(&x700, &x701, x664, UINT32_C(0xffffffff)); uint32_t x702; - fiat_p384_uint1 x703; - fiat_p384_addcarryx_u32(&x702, &x703, x701, 0x0, x676); + uint32_t x703; + fiat_p384_mulx_u32(&x702, &x703, x664, UINT32_C(0xfffffffe)); uint32_t x704; - fiat_p384_uint1 x705; - fiat_p384_addcarryx_u32(&x704, &x705, x703, 0x0, x678); + uint32_t x705; + fiat_p384_mulx_u32(&x704, &x705, x664, UINT32_C(0xffffffff)); uint32_t x706; - fiat_p384_uint1 x707; - fiat_p384_addcarryx_u32(&x706, &x707, x705, 0x0, x680); + uint32_t x707; + fiat_p384_mulx_u32(&x706, &x707, x664, UINT32_C(0xffffffff)); uint32_t x708; fiat_p384_uint1 x709; - fiat_p384_addcarryx_u32(&x708, &x709, x707, 0x0, x682); + fiat_p384_addcarryx_u32(&x708, &x709, 0x0, x702, x705); uint32_t x710; fiat_p384_uint1 x711; - fiat_p384_addcarryx_u32(&x710, &x711, x709, 0x0, x686); + fiat_p384_addcarryx_u32(&x710, &x711, x709, x700, x703); uint32_t x712; fiat_p384_uint1 x713; - fiat_p384_addcarryx_u32(&x712, &x713, x687, 0x0, x623); + fiat_p384_addcarryx_u32(&x712, &x713, x711, x698, x701); uint32_t x714; fiat_p384_uint1 x715; - fiat_p384_addcarryx_u32(&x714, &x715, x711, 0x0, (fiat_p384_uint1)x712); + fiat_p384_addcarryx_u32(&x714, &x715, x713, x696, x699); uint32_t x716; - uint32_t x717; - fiat_p384_mulx_u32(&x716, &x717, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x717; + fiat_p384_addcarryx_u32(&x716, &x717, x715, x694, x697); uint32_t x718; - uint32_t x719; - fiat_p384_mulx_u32(&x718, &x719, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x719; + fiat_p384_addcarryx_u32(&x718, &x719, x717, x692, x695); uint32_t x720; - uint32_t x721; - fiat_p384_mulx_u32(&x720, &x721, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x721; + fiat_p384_addcarryx_u32(&x720, &x721, x719, x690, x693); uint32_t x722; - uint32_t x723; - fiat_p384_mulx_u32(&x722, &x723, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x723; + fiat_p384_addcarryx_u32(&x722, &x723, x721, x688, x691); uint32_t x724; - uint32_t x725; - fiat_p384_mulx_u32(&x724, &x725, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x725; + fiat_p384_addcarryx_u32(&x724, &x725, 0x0, x706, x664); uint32_t x726; - uint32_t x727; - fiat_p384_mulx_u32(&x726, &x727, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x727; + fiat_p384_addcarryx_u32(&x726, &x727, x725, x707, x666); uint32_t x728; - uint32_t x729; - fiat_p384_mulx_u32(&x728, &x729, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x729; + fiat_p384_addcarryx_u32(&x728, &x729, x727, 0x0, x668); uint32_t x730; - uint32_t x731; - fiat_p384_mulx_u32(&x730, &x731, x688, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x731; + fiat_p384_addcarryx_u32(&x730, &x731, x729, x704, x670); uint32_t x732; - uint32_t x733; - fiat_p384_mulx_u32(&x732, &x733, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x733; + fiat_p384_addcarryx_u32(&x732, &x733, x731, x708, x672); uint32_t x734; - uint32_t x735; - fiat_p384_mulx_u32(&x734, &x735, x688, UINT32_C(0xffffffff)); + fiat_p384_uint1 x735; + fiat_p384_addcarryx_u32(&x734, &x735, x733, x710, x674); uint32_t x736; fiat_p384_uint1 x737; - fiat_p384_addcarryx_u32(&x736, &x737, 0x0, x730, x733); + fiat_p384_addcarryx_u32(&x736, &x737, x735, x712, x676); uint32_t x738; fiat_p384_uint1 x739; - fiat_p384_addcarryx_u32(&x738, &x739, x737, x728, x731); + fiat_p384_addcarryx_u32(&x738, &x739, x737, x714, x678); uint32_t x740; fiat_p384_uint1 x741; - fiat_p384_addcarryx_u32(&x740, &x741, x739, x726, x729); + fiat_p384_addcarryx_u32(&x740, &x741, x739, x716, x680); uint32_t x742; fiat_p384_uint1 x743; - fiat_p384_addcarryx_u32(&x742, &x743, x741, x724, x727); + fiat_p384_addcarryx_u32(&x742, &x743, x741, x718, x682); uint32_t x744; fiat_p384_uint1 x745; - fiat_p384_addcarryx_u32(&x744, &x745, x743, x722, x725); + fiat_p384_addcarryx_u32(&x744, &x745, x743, x720, x684); uint32_t x746; fiat_p384_uint1 x747; - fiat_p384_addcarryx_u32(&x746, &x747, x745, x720, x723); + fiat_p384_addcarryx_u32(&x746, &x747, x745, x722, x686); uint32_t x748; fiat_p384_uint1 x749; - fiat_p384_addcarryx_u32(&x748, &x749, x747, x718, x721); + fiat_p384_addcarryx_u32(&x748, &x749, x663, 0x0, 0x0); uint32_t x750; fiat_p384_uint1 x751; - fiat_p384_addcarryx_u32(&x750, &x751, x749, x716, x719); + fiat_p384_addcarryx_u32(&x750, &x751, x687, 0x0, (fiat_p384_uint1)x748); uint32_t x752; fiat_p384_uint1 x753; - fiat_p384_addcarryx_u32(&x752, &x753, 0x0, x734, x688); + fiat_p384_addcarryx_u32(&x752, &x753, x723, 0x0, x689); uint32_t x754; fiat_p384_uint1 x755; - fiat_p384_addcarryx_u32(&x754, &x755, x753, x735, x690); + fiat_p384_addcarryx_u32(&x754, &x755, x747, x752, x750); uint32_t x756; fiat_p384_uint1 x757; - fiat_p384_addcarryx_u32(&x756, &x757, x755, 0x0, x692); + fiat_p384_addcarryx_u32(&x756, &x757, 0x0, (arg1[9]), x726); uint32_t x758; fiat_p384_uint1 x759; - fiat_p384_addcarryx_u32(&x758, &x759, x757, x732, x694); + fiat_p384_addcarryx_u32(&x758, &x759, x757, 0x0, x728); uint32_t x760; fiat_p384_uint1 x761; - fiat_p384_addcarryx_u32(&x760, &x761, x759, x736, x696); + fiat_p384_addcarryx_u32(&x760, &x761, x759, 0x0, x730); uint32_t x762; fiat_p384_uint1 x763; - fiat_p384_addcarryx_u32(&x762, &x763, x761, x738, x698); + fiat_p384_addcarryx_u32(&x762, &x763, x761, 0x0, x732); uint32_t x764; fiat_p384_uint1 x765; - fiat_p384_addcarryx_u32(&x764, &x765, x763, x740, x700); + fiat_p384_addcarryx_u32(&x764, &x765, x763, 0x0, x734); uint32_t x766; fiat_p384_uint1 x767; - fiat_p384_addcarryx_u32(&x766, &x767, x765, x742, x702); + fiat_p384_addcarryx_u32(&x766, &x767, x765, 0x0, x736); uint32_t x768; fiat_p384_uint1 x769; - fiat_p384_addcarryx_u32(&x768, &x769, x767, x744, x704); + fiat_p384_addcarryx_u32(&x768, &x769, x767, 0x0, x738); uint32_t x770; fiat_p384_uint1 x771; - fiat_p384_addcarryx_u32(&x770, &x771, x769, x746, x706); + fiat_p384_addcarryx_u32(&x770, &x771, x769, 0x0, x740); uint32_t x772; fiat_p384_uint1 x773; - fiat_p384_addcarryx_u32(&x772, &x773, x771, x748, x708); + fiat_p384_addcarryx_u32(&x772, &x773, x771, 0x0, x742); uint32_t x774; fiat_p384_uint1 x775; - fiat_p384_addcarryx_u32(&x774, &x775, x773, x750, x710); + fiat_p384_addcarryx_u32(&x774, &x775, x773, 0x0, x744); uint32_t x776; fiat_p384_uint1 x777; - fiat_p384_addcarryx_u32(&x776, &x777, x751, 0x0, x717); + fiat_p384_addcarryx_u32(&x776, &x777, x775, 0x0, x746); uint32_t x778; fiat_p384_uint1 x779; - fiat_p384_addcarryx_u32(&x778, &x779, x775, x776, x714); + fiat_p384_addcarryx_u32(&x778, &x779, x777, 0x0, x754); uint32_t x780; - fiat_p384_uint1 x781; - fiat_p384_addcarryx_u32(&x780, &x781, 0x0, (arg1[9]), x754); + uint32_t x781; + fiat_p384_mulx_u32(&x780, &x781, x756, UINT32_C(0xffffffff)); uint32_t x782; - fiat_p384_uint1 x783; - fiat_p384_addcarryx_u32(&x782, &x783, x781, 0x0, x756); + uint32_t x783; + fiat_p384_mulx_u32(&x782, &x783, x756, UINT32_C(0xffffffff)); uint32_t x784; - fiat_p384_uint1 x785; - fiat_p384_addcarryx_u32(&x784, &x785, x783, 0x0, x758); + uint32_t x785; + fiat_p384_mulx_u32(&x784, &x785, x756, UINT32_C(0xffffffff)); uint32_t x786; - fiat_p384_uint1 x787; - fiat_p384_addcarryx_u32(&x786, &x787, x785, 0x0, x760); + uint32_t x787; + fiat_p384_mulx_u32(&x786, &x787, x756, UINT32_C(0xffffffff)); uint32_t x788; - fiat_p384_uint1 x789; - fiat_p384_addcarryx_u32(&x788, &x789, x787, 0x0, x762); + uint32_t x789; + fiat_p384_mulx_u32(&x788, &x789, x756, UINT32_C(0xffffffff)); uint32_t x790; - fiat_p384_uint1 x791; - fiat_p384_addcarryx_u32(&x790, &x791, x789, 0x0, x764); + uint32_t x791; + fiat_p384_mulx_u32(&x790, &x791, x756, UINT32_C(0xffffffff)); uint32_t x792; - fiat_p384_uint1 x793; - fiat_p384_addcarryx_u32(&x792, &x793, x791, 0x0, x766); + uint32_t x793; + fiat_p384_mulx_u32(&x792, &x793, x756, UINT32_C(0xffffffff)); uint32_t x794; - fiat_p384_uint1 x795; - fiat_p384_addcarryx_u32(&x794, &x795, x793, 0x0, x768); + uint32_t x795; + fiat_p384_mulx_u32(&x794, &x795, x756, UINT32_C(0xfffffffe)); uint32_t x796; - fiat_p384_uint1 x797; - fiat_p384_addcarryx_u32(&x796, &x797, x795, 0x0, x770); + uint32_t x797; + fiat_p384_mulx_u32(&x796, &x797, x756, UINT32_C(0xffffffff)); uint32_t x798; - fiat_p384_uint1 x799; - fiat_p384_addcarryx_u32(&x798, &x799, x797, 0x0, x772); + uint32_t x799; + fiat_p384_mulx_u32(&x798, &x799, x756, UINT32_C(0xffffffff)); uint32_t x800; fiat_p384_uint1 x801; - fiat_p384_addcarryx_u32(&x800, &x801, x799, 0x0, x774); + fiat_p384_addcarryx_u32(&x800, &x801, 0x0, x794, x797); uint32_t x802; fiat_p384_uint1 x803; - fiat_p384_addcarryx_u32(&x802, &x803, x801, 0x0, x778); + fiat_p384_addcarryx_u32(&x802, &x803, x801, x792, x795); uint32_t x804; fiat_p384_uint1 x805; - fiat_p384_addcarryx_u32(&x804, &x805, x779, 0x0, x715); + fiat_p384_addcarryx_u32(&x804, &x805, x803, x790, x793); uint32_t x806; fiat_p384_uint1 x807; - fiat_p384_addcarryx_u32(&x806, &x807, x803, 0x0, (fiat_p384_uint1)x804); + fiat_p384_addcarryx_u32(&x806, &x807, x805, x788, x791); uint32_t x808; - uint32_t x809; - fiat_p384_mulx_u32(&x808, &x809, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x809; + fiat_p384_addcarryx_u32(&x808, &x809, x807, x786, x789); uint32_t x810; - uint32_t x811; - fiat_p384_mulx_u32(&x810, &x811, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x811; + fiat_p384_addcarryx_u32(&x810, &x811, x809, x784, x787); uint32_t x812; - uint32_t x813; - fiat_p384_mulx_u32(&x812, &x813, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x813; + fiat_p384_addcarryx_u32(&x812, &x813, x811, x782, x785); uint32_t x814; - uint32_t x815; - fiat_p384_mulx_u32(&x814, &x815, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x815; + fiat_p384_addcarryx_u32(&x814, &x815, x813, x780, x783); uint32_t x816; - uint32_t x817; - fiat_p384_mulx_u32(&x816, &x817, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x817; + fiat_p384_addcarryx_u32(&x816, &x817, 0x0, x798, x756); uint32_t x818; - uint32_t x819; - fiat_p384_mulx_u32(&x818, &x819, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x819; + fiat_p384_addcarryx_u32(&x818, &x819, x817, x799, x758); uint32_t x820; - uint32_t x821; - fiat_p384_mulx_u32(&x820, &x821, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x821; + fiat_p384_addcarryx_u32(&x820, &x821, x819, 0x0, x760); uint32_t x822; - uint32_t x823; - fiat_p384_mulx_u32(&x822, &x823, x780, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x823; + fiat_p384_addcarryx_u32(&x822, &x823, x821, x796, x762); uint32_t x824; - uint32_t x825; - fiat_p384_mulx_u32(&x824, &x825, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x825; + fiat_p384_addcarryx_u32(&x824, &x825, x823, x800, x764); uint32_t x826; - uint32_t x827; - fiat_p384_mulx_u32(&x826, &x827, x780, UINT32_C(0xffffffff)); + fiat_p384_uint1 x827; + fiat_p384_addcarryx_u32(&x826, &x827, x825, x802, x766); uint32_t x828; fiat_p384_uint1 x829; - fiat_p384_addcarryx_u32(&x828, &x829, 0x0, x822, x825); + fiat_p384_addcarryx_u32(&x828, &x829, x827, x804, x768); uint32_t x830; fiat_p384_uint1 x831; - fiat_p384_addcarryx_u32(&x830, &x831, x829, x820, x823); + fiat_p384_addcarryx_u32(&x830, &x831, x829, x806, x770); uint32_t x832; fiat_p384_uint1 x833; - fiat_p384_addcarryx_u32(&x832, &x833, x831, x818, x821); + fiat_p384_addcarryx_u32(&x832, &x833, x831, x808, x772); uint32_t x834; fiat_p384_uint1 x835; - fiat_p384_addcarryx_u32(&x834, &x835, x833, x816, x819); + fiat_p384_addcarryx_u32(&x834, &x835, x833, x810, x774); uint32_t x836; fiat_p384_uint1 x837; - fiat_p384_addcarryx_u32(&x836, &x837, x835, x814, x817); + fiat_p384_addcarryx_u32(&x836, &x837, x835, x812, x776); uint32_t x838; fiat_p384_uint1 x839; - fiat_p384_addcarryx_u32(&x838, &x839, x837, x812, x815); + fiat_p384_addcarryx_u32(&x838, &x839, x837, x814, x778); uint32_t x840; fiat_p384_uint1 x841; - fiat_p384_addcarryx_u32(&x840, &x841, x839, x810, x813); + fiat_p384_addcarryx_u32(&x840, &x841, x755, 0x0, 0x0); uint32_t x842; fiat_p384_uint1 x843; - fiat_p384_addcarryx_u32(&x842, &x843, x841, x808, x811); + fiat_p384_addcarryx_u32(&x842, &x843, x779, 0x0, (fiat_p384_uint1)x840); uint32_t x844; fiat_p384_uint1 x845; - fiat_p384_addcarryx_u32(&x844, &x845, 0x0, x826, x780); + fiat_p384_addcarryx_u32(&x844, &x845, x815, 0x0, x781); uint32_t x846; fiat_p384_uint1 x847; - fiat_p384_addcarryx_u32(&x846, &x847, x845, x827, x782); + fiat_p384_addcarryx_u32(&x846, &x847, x839, x844, x842); uint32_t x848; fiat_p384_uint1 x849; - fiat_p384_addcarryx_u32(&x848, &x849, x847, 0x0, x784); + fiat_p384_addcarryx_u32(&x848, &x849, 0x0, (arg1[10]), x818); uint32_t x850; fiat_p384_uint1 x851; - fiat_p384_addcarryx_u32(&x850, &x851, x849, x824, x786); + fiat_p384_addcarryx_u32(&x850, &x851, x849, 0x0, x820); uint32_t x852; fiat_p384_uint1 x853; - fiat_p384_addcarryx_u32(&x852, &x853, x851, x828, x788); + fiat_p384_addcarryx_u32(&x852, &x853, x851, 0x0, x822); uint32_t x854; fiat_p384_uint1 x855; - fiat_p384_addcarryx_u32(&x854, &x855, x853, x830, x790); + fiat_p384_addcarryx_u32(&x854, &x855, x853, 0x0, x824); uint32_t x856; fiat_p384_uint1 x857; - fiat_p384_addcarryx_u32(&x856, &x857, x855, x832, x792); + fiat_p384_addcarryx_u32(&x856, &x857, x855, 0x0, x826); uint32_t x858; fiat_p384_uint1 x859; - fiat_p384_addcarryx_u32(&x858, &x859, x857, x834, x794); + fiat_p384_addcarryx_u32(&x858, &x859, x857, 0x0, x828); uint32_t x860; fiat_p384_uint1 x861; - fiat_p384_addcarryx_u32(&x860, &x861, x859, x836, x796); + fiat_p384_addcarryx_u32(&x860, &x861, x859, 0x0, x830); uint32_t x862; fiat_p384_uint1 x863; - fiat_p384_addcarryx_u32(&x862, &x863, x861, x838, x798); + fiat_p384_addcarryx_u32(&x862, &x863, x861, 0x0, x832); uint32_t x864; fiat_p384_uint1 x865; - fiat_p384_addcarryx_u32(&x864, &x865, x863, x840, x800); + fiat_p384_addcarryx_u32(&x864, &x865, x863, 0x0, x834); uint32_t x866; fiat_p384_uint1 x867; - fiat_p384_addcarryx_u32(&x866, &x867, x865, x842, x802); + fiat_p384_addcarryx_u32(&x866, &x867, x865, 0x0, x836); uint32_t x868; fiat_p384_uint1 x869; - fiat_p384_addcarryx_u32(&x868, &x869, x843, 0x0, x809); + fiat_p384_addcarryx_u32(&x868, &x869, x867, 0x0, x838); uint32_t x870; fiat_p384_uint1 x871; - fiat_p384_addcarryx_u32(&x870, &x871, x867, x868, x806); + fiat_p384_addcarryx_u32(&x870, &x871, x869, 0x0, x846); uint32_t x872; - fiat_p384_uint1 x873; - fiat_p384_addcarryx_u32(&x872, &x873, 0x0, (arg1[10]), x846); + uint32_t x873; + fiat_p384_mulx_u32(&x872, &x873, x848, UINT32_C(0xffffffff)); uint32_t x874; - fiat_p384_uint1 x875; - fiat_p384_addcarryx_u32(&x874, &x875, x873, 0x0, x848); + uint32_t x875; + fiat_p384_mulx_u32(&x874, &x875, x848, UINT32_C(0xffffffff)); uint32_t x876; - fiat_p384_uint1 x877; - fiat_p384_addcarryx_u32(&x876, &x877, x875, 0x0, x850); + uint32_t x877; + fiat_p384_mulx_u32(&x876, &x877, x848, UINT32_C(0xffffffff)); uint32_t x878; - fiat_p384_uint1 x879; - fiat_p384_addcarryx_u32(&x878, &x879, x877, 0x0, x852); + uint32_t x879; + fiat_p384_mulx_u32(&x878, &x879, x848, UINT32_C(0xffffffff)); uint32_t x880; - fiat_p384_uint1 x881; - fiat_p384_addcarryx_u32(&x880, &x881, x879, 0x0, x854); + uint32_t x881; + fiat_p384_mulx_u32(&x880, &x881, x848, UINT32_C(0xffffffff)); uint32_t x882; - fiat_p384_uint1 x883; - fiat_p384_addcarryx_u32(&x882, &x883, x881, 0x0, x856); + uint32_t x883; + fiat_p384_mulx_u32(&x882, &x883, x848, UINT32_C(0xffffffff)); uint32_t x884; - fiat_p384_uint1 x885; - fiat_p384_addcarryx_u32(&x884, &x885, x883, 0x0, x858); + uint32_t x885; + fiat_p384_mulx_u32(&x884, &x885, x848, UINT32_C(0xffffffff)); uint32_t x886; - fiat_p384_uint1 x887; - fiat_p384_addcarryx_u32(&x886, &x887, x885, 0x0, x860); + uint32_t x887; + fiat_p384_mulx_u32(&x886, &x887, x848, UINT32_C(0xfffffffe)); uint32_t x888; - fiat_p384_uint1 x889; - fiat_p384_addcarryx_u32(&x888, &x889, x887, 0x0, x862); + uint32_t x889; + fiat_p384_mulx_u32(&x888, &x889, x848, UINT32_C(0xffffffff)); uint32_t x890; - fiat_p384_uint1 x891; - fiat_p384_addcarryx_u32(&x890, &x891, x889, 0x0, x864); + uint32_t x891; + fiat_p384_mulx_u32(&x890, &x891, x848, UINT32_C(0xffffffff)); uint32_t x892; fiat_p384_uint1 x893; - fiat_p384_addcarryx_u32(&x892, &x893, x891, 0x0, x866); + fiat_p384_addcarryx_u32(&x892, &x893, 0x0, x886, x889); uint32_t x894; fiat_p384_uint1 x895; - fiat_p384_addcarryx_u32(&x894, &x895, x893, 0x0, x870); + fiat_p384_addcarryx_u32(&x894, &x895, x893, x884, x887); uint32_t x896; fiat_p384_uint1 x897; - fiat_p384_addcarryx_u32(&x896, &x897, x871, 0x0, x807); + fiat_p384_addcarryx_u32(&x896, &x897, x895, x882, x885); uint32_t x898; fiat_p384_uint1 x899; - fiat_p384_addcarryx_u32(&x898, &x899, x895, 0x0, (fiat_p384_uint1)x896); + fiat_p384_addcarryx_u32(&x898, &x899, x897, x880, x883); uint32_t x900; - uint32_t x901; - fiat_p384_mulx_u32(&x900, &x901, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x901; + fiat_p384_addcarryx_u32(&x900, &x901, x899, x878, x881); uint32_t x902; - uint32_t x903; - fiat_p384_mulx_u32(&x902, &x903, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x903; + fiat_p384_addcarryx_u32(&x902, &x903, x901, x876, x879); uint32_t x904; - uint32_t x905; - fiat_p384_mulx_u32(&x904, &x905, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x905; + fiat_p384_addcarryx_u32(&x904, &x905, x903, x874, x877); uint32_t x906; - uint32_t x907; - fiat_p384_mulx_u32(&x906, &x907, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x907; + fiat_p384_addcarryx_u32(&x906, &x907, x905, x872, x875); uint32_t x908; - uint32_t x909; - fiat_p384_mulx_u32(&x908, &x909, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x909; + fiat_p384_addcarryx_u32(&x908, &x909, 0x0, x890, x848); uint32_t x910; - uint32_t x911; - fiat_p384_mulx_u32(&x910, &x911, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x911; + fiat_p384_addcarryx_u32(&x910, &x911, x909, x891, x850); uint32_t x912; - uint32_t x913; - fiat_p384_mulx_u32(&x912, &x913, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x913; + fiat_p384_addcarryx_u32(&x912, &x913, x911, 0x0, x852); uint32_t x914; - uint32_t x915; - fiat_p384_mulx_u32(&x914, &x915, x872, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x915; + fiat_p384_addcarryx_u32(&x914, &x915, x913, x888, x854); uint32_t x916; - uint32_t x917; - fiat_p384_mulx_u32(&x916, &x917, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x917; + fiat_p384_addcarryx_u32(&x916, &x917, x915, x892, x856); uint32_t x918; - uint32_t x919; - fiat_p384_mulx_u32(&x918, &x919, x872, UINT32_C(0xffffffff)); + fiat_p384_uint1 x919; + fiat_p384_addcarryx_u32(&x918, &x919, x917, x894, x858); uint32_t x920; fiat_p384_uint1 x921; - fiat_p384_addcarryx_u32(&x920, &x921, 0x0, x914, x917); + fiat_p384_addcarryx_u32(&x920, &x921, x919, x896, x860); uint32_t x922; fiat_p384_uint1 x923; - fiat_p384_addcarryx_u32(&x922, &x923, x921, x912, x915); + fiat_p384_addcarryx_u32(&x922, &x923, x921, x898, x862); uint32_t x924; fiat_p384_uint1 x925; - fiat_p384_addcarryx_u32(&x924, &x925, x923, x910, x913); + fiat_p384_addcarryx_u32(&x924, &x925, x923, x900, x864); uint32_t x926; fiat_p384_uint1 x927; - fiat_p384_addcarryx_u32(&x926, &x927, x925, x908, x911); + fiat_p384_addcarryx_u32(&x926, &x927, x925, x902, x866); uint32_t x928; fiat_p384_uint1 x929; - fiat_p384_addcarryx_u32(&x928, &x929, x927, x906, x909); + fiat_p384_addcarryx_u32(&x928, &x929, x927, x904, x868); uint32_t x930; fiat_p384_uint1 x931; - fiat_p384_addcarryx_u32(&x930, &x931, x929, x904, x907); + fiat_p384_addcarryx_u32(&x930, &x931, x929, x906, x870); uint32_t x932; fiat_p384_uint1 x933; - fiat_p384_addcarryx_u32(&x932, &x933, x931, x902, x905); + fiat_p384_addcarryx_u32(&x932, &x933, x847, 0x0, 0x0); uint32_t x934; fiat_p384_uint1 x935; - fiat_p384_addcarryx_u32(&x934, &x935, x933, x900, x903); + fiat_p384_addcarryx_u32(&x934, &x935, x871, 0x0, (fiat_p384_uint1)x932); uint32_t x936; fiat_p384_uint1 x937; - fiat_p384_addcarryx_u32(&x936, &x937, 0x0, x918, x872); + fiat_p384_addcarryx_u32(&x936, &x937, x907, 0x0, x873); uint32_t x938; fiat_p384_uint1 x939; - fiat_p384_addcarryx_u32(&x938, &x939, x937, x919, x874); + fiat_p384_addcarryx_u32(&x938, &x939, x931, x936, x934); uint32_t x940; fiat_p384_uint1 x941; - fiat_p384_addcarryx_u32(&x940, &x941, x939, 0x0, x876); + fiat_p384_addcarryx_u32(&x940, &x941, 0x0, (arg1[11]), x910); uint32_t x942; fiat_p384_uint1 x943; - fiat_p384_addcarryx_u32(&x942, &x943, x941, x916, x878); + fiat_p384_addcarryx_u32(&x942, &x943, x941, 0x0, x912); uint32_t x944; fiat_p384_uint1 x945; - fiat_p384_addcarryx_u32(&x944, &x945, x943, x920, x880); + fiat_p384_addcarryx_u32(&x944, &x945, x943, 0x0, x914); uint32_t x946; fiat_p384_uint1 x947; - fiat_p384_addcarryx_u32(&x946, &x947, x945, x922, x882); + fiat_p384_addcarryx_u32(&x946, &x947, x945, 0x0, x916); uint32_t x948; fiat_p384_uint1 x949; - fiat_p384_addcarryx_u32(&x948, &x949, x947, x924, x884); + fiat_p384_addcarryx_u32(&x948, &x949, x947, 0x0, x918); uint32_t x950; fiat_p384_uint1 x951; - fiat_p384_addcarryx_u32(&x950, &x951, x949, x926, x886); + fiat_p384_addcarryx_u32(&x950, &x951, x949, 0x0, x920); uint32_t x952; fiat_p384_uint1 x953; - fiat_p384_addcarryx_u32(&x952, &x953, x951, x928, x888); + fiat_p384_addcarryx_u32(&x952, &x953, x951, 0x0, x922); uint32_t x954; fiat_p384_uint1 x955; - fiat_p384_addcarryx_u32(&x954, &x955, x953, x930, x890); + fiat_p384_addcarryx_u32(&x954, &x955, x953, 0x0, x924); uint32_t x956; fiat_p384_uint1 x957; - fiat_p384_addcarryx_u32(&x956, &x957, x955, x932, x892); + fiat_p384_addcarryx_u32(&x956, &x957, x955, 0x0, x926); uint32_t x958; fiat_p384_uint1 x959; - fiat_p384_addcarryx_u32(&x958, &x959, x957, x934, x894); + fiat_p384_addcarryx_u32(&x958, &x959, x957, 0x0, x928); uint32_t x960; fiat_p384_uint1 x961; - fiat_p384_addcarryx_u32(&x960, &x961, x935, 0x0, x901); + fiat_p384_addcarryx_u32(&x960, &x961, x959, 0x0, x930); uint32_t x962; fiat_p384_uint1 x963; - fiat_p384_addcarryx_u32(&x962, &x963, x959, x960, x898); + fiat_p384_addcarryx_u32(&x962, &x963, x961, 0x0, x938); uint32_t x964; - fiat_p384_uint1 x965; - fiat_p384_addcarryx_u32(&x964, &x965, 0x0, (arg1[11]), x938); + uint32_t x965; + fiat_p384_mulx_u32(&x964, &x965, x940, UINT32_C(0xffffffff)); uint32_t x966; - fiat_p384_uint1 x967; - fiat_p384_addcarryx_u32(&x966, &x967, x965, 0x0, x940); + uint32_t x967; + fiat_p384_mulx_u32(&x966, &x967, x940, UINT32_C(0xffffffff)); uint32_t x968; - fiat_p384_uint1 x969; - fiat_p384_addcarryx_u32(&x968, &x969, x967, 0x0, x942); + uint32_t x969; + fiat_p384_mulx_u32(&x968, &x969, x940, UINT32_C(0xffffffff)); uint32_t x970; - fiat_p384_uint1 x971; - fiat_p384_addcarryx_u32(&x970, &x971, x969, 0x0, x944); + uint32_t x971; + fiat_p384_mulx_u32(&x970, &x971, x940, UINT32_C(0xffffffff)); uint32_t x972; - fiat_p384_uint1 x973; - fiat_p384_addcarryx_u32(&x972, &x973, x971, 0x0, x946); + uint32_t x973; + fiat_p384_mulx_u32(&x972, &x973, x940, UINT32_C(0xffffffff)); uint32_t x974; - fiat_p384_uint1 x975; - fiat_p384_addcarryx_u32(&x974, &x975, x973, 0x0, x948); + uint32_t x975; + fiat_p384_mulx_u32(&x974, &x975, x940, UINT32_C(0xffffffff)); uint32_t x976; - fiat_p384_uint1 x977; - fiat_p384_addcarryx_u32(&x976, &x977, x975, 0x0, x950); + uint32_t x977; + fiat_p384_mulx_u32(&x976, &x977, x940, UINT32_C(0xffffffff)); uint32_t x978; - fiat_p384_uint1 x979; - fiat_p384_addcarryx_u32(&x978, &x979, x977, 0x0, x952); + uint32_t x979; + fiat_p384_mulx_u32(&x978, &x979, x940, UINT32_C(0xfffffffe)); uint32_t x980; - fiat_p384_uint1 x981; - fiat_p384_addcarryx_u32(&x980, &x981, x979, 0x0, x954); + uint32_t x981; + fiat_p384_mulx_u32(&x980, &x981, x940, UINT32_C(0xffffffff)); uint32_t x982; - fiat_p384_uint1 x983; - fiat_p384_addcarryx_u32(&x982, &x983, x981, 0x0, x956); + uint32_t x983; + fiat_p384_mulx_u32(&x982, &x983, x940, UINT32_C(0xffffffff)); uint32_t x984; fiat_p384_uint1 x985; - fiat_p384_addcarryx_u32(&x984, &x985, x983, 0x0, x958); + fiat_p384_addcarryx_u32(&x984, &x985, 0x0, x978, x981); uint32_t x986; fiat_p384_uint1 x987; - fiat_p384_addcarryx_u32(&x986, &x987, x985, 0x0, x962); + fiat_p384_addcarryx_u32(&x986, &x987, x985, x976, x979); uint32_t x988; fiat_p384_uint1 x989; - fiat_p384_addcarryx_u32(&x988, &x989, x963, 0x0, x899); + fiat_p384_addcarryx_u32(&x988, &x989, x987, x974, x977); uint32_t x990; fiat_p384_uint1 x991; - fiat_p384_addcarryx_u32(&x990, &x991, x987, 0x0, (fiat_p384_uint1)x988); + fiat_p384_addcarryx_u32(&x990, &x991, x989, x972, x975); uint32_t x992; - uint32_t x993; - fiat_p384_mulx_u32(&x992, &x993, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x993; + fiat_p384_addcarryx_u32(&x992, &x993, x991, x970, x973); uint32_t x994; - uint32_t x995; - fiat_p384_mulx_u32(&x994, &x995, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x995; + fiat_p384_addcarryx_u32(&x994, &x995, x993, x968, x971); uint32_t x996; - uint32_t x997; - fiat_p384_mulx_u32(&x996, &x997, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x997; + fiat_p384_addcarryx_u32(&x996, &x997, x995, x966, x969); uint32_t x998; - uint32_t x999; - fiat_p384_mulx_u32(&x998, &x999, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x999; + fiat_p384_addcarryx_u32(&x998, &x999, x997, x964, x967); uint32_t x1000; - uint32_t x1001; - fiat_p384_mulx_u32(&x1000, &x1001, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x1001; + fiat_p384_addcarryx_u32(&x1000, &x1001, 0x0, x982, x940); uint32_t x1002; - uint32_t x1003; - fiat_p384_mulx_u32(&x1002, &x1003, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x1003; + fiat_p384_addcarryx_u32(&x1002, &x1003, x1001, x983, x942); uint32_t x1004; - uint32_t x1005; - fiat_p384_mulx_u32(&x1004, &x1005, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x1005; + fiat_p384_addcarryx_u32(&x1004, &x1005, x1003, 0x0, x944); uint32_t x1006; - uint32_t x1007; - fiat_p384_mulx_u32(&x1006, &x1007, x964, UINT32_C(0xfffffffe)); + fiat_p384_uint1 x1007; + fiat_p384_addcarryx_u32(&x1006, &x1007, x1005, x980, x946); uint32_t x1008; - uint32_t x1009; - fiat_p384_mulx_u32(&x1008, &x1009, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x1009; + fiat_p384_addcarryx_u32(&x1008, &x1009, x1007, x984, x948); uint32_t x1010; - uint32_t x1011; - fiat_p384_mulx_u32(&x1010, &x1011, x964, UINT32_C(0xffffffff)); + fiat_p384_uint1 x1011; + fiat_p384_addcarryx_u32(&x1010, &x1011, x1009, x986, x950); uint32_t x1012; fiat_p384_uint1 x1013; - fiat_p384_addcarryx_u32(&x1012, &x1013, 0x0, x1006, x1009); + fiat_p384_addcarryx_u32(&x1012, &x1013, x1011, x988, x952); uint32_t x1014; fiat_p384_uint1 x1015; - fiat_p384_addcarryx_u32(&x1014, &x1015, x1013, x1004, x1007); + fiat_p384_addcarryx_u32(&x1014, &x1015, x1013, x990, x954); uint32_t x1016; fiat_p384_uint1 x1017; - fiat_p384_addcarryx_u32(&x1016, &x1017, x1015, x1002, x1005); + fiat_p384_addcarryx_u32(&x1016, &x1017, x1015, x992, x956); uint32_t x1018; fiat_p384_uint1 x1019; - fiat_p384_addcarryx_u32(&x1018, &x1019, x1017, x1000, x1003); + fiat_p384_addcarryx_u32(&x1018, &x1019, x1017, x994, x958); uint32_t x1020; fiat_p384_uint1 x1021; - fiat_p384_addcarryx_u32(&x1020, &x1021, x1019, x998, x1001); + fiat_p384_addcarryx_u32(&x1020, &x1021, x1019, x996, x960); uint32_t x1022; fiat_p384_uint1 x1023; - fiat_p384_addcarryx_u32(&x1022, &x1023, x1021, x996, x999); + fiat_p384_addcarryx_u32(&x1022, &x1023, x1021, x998, x962); uint32_t x1024; fiat_p384_uint1 x1025; - fiat_p384_addcarryx_u32(&x1024, &x1025, x1023, x994, x997); + fiat_p384_addcarryx_u32(&x1024, &x1025, x939, 0x0, 0x0); uint32_t x1026; fiat_p384_uint1 x1027; - fiat_p384_addcarryx_u32(&x1026, &x1027, x1025, x992, x995); + fiat_p384_addcarryx_u32(&x1026, &x1027, x963, 0x0, (fiat_p384_uint1)x1024); uint32_t x1028; fiat_p384_uint1 x1029; - fiat_p384_addcarryx_u32(&x1028, &x1029, 0x0, x1010, x964); + fiat_p384_addcarryx_u32(&x1028, &x1029, x999, 0x0, x965); uint32_t x1030; fiat_p384_uint1 x1031; - fiat_p384_addcarryx_u32(&x1030, &x1031, x1029, x1011, x966); + fiat_p384_addcarryx_u32(&x1030, &x1031, x1023, x1028, x1026); uint32_t x1032; fiat_p384_uint1 x1033; - fiat_p384_addcarryx_u32(&x1032, &x1033, x1031, 0x0, x968); + fiat_p384_subborrowx_u32(&x1032, &x1033, 0x0, x1002, UINT32_C(0xffffffff)); uint32_t x1034; fiat_p384_uint1 x1035; - fiat_p384_addcarryx_u32(&x1034, &x1035, x1033, x1008, x970); + fiat_p384_subborrowx_u32(&x1034, &x1035, x1033, x1004, 0x0); uint32_t x1036; fiat_p384_uint1 x1037; - fiat_p384_addcarryx_u32(&x1036, &x1037, x1035, x1012, x972); + fiat_p384_subborrowx_u32(&x1036, &x1037, x1035, x1006, 0x0); uint32_t x1038; fiat_p384_uint1 x1039; - fiat_p384_addcarryx_u32(&x1038, &x1039, x1037, x1014, x974); + fiat_p384_subborrowx_u32(&x1038, &x1039, x1037, x1008, UINT32_C(0xffffffff)); uint32_t x1040; fiat_p384_uint1 x1041; - fiat_p384_addcarryx_u32(&x1040, &x1041, x1039, x1016, x976); + fiat_p384_subborrowx_u32(&x1040, &x1041, x1039, x1010, UINT32_C(0xfffffffe)); uint32_t x1042; fiat_p384_uint1 x1043; - fiat_p384_addcarryx_u32(&x1042, &x1043, x1041, x1018, x978); + fiat_p384_subborrowx_u32(&x1042, &x1043, x1041, x1012, UINT32_C(0xffffffff)); uint32_t x1044; fiat_p384_uint1 x1045; - fiat_p384_addcarryx_u32(&x1044, &x1045, x1043, x1020, x980); + fiat_p384_subborrowx_u32(&x1044, &x1045, x1043, x1014, UINT32_C(0xffffffff)); uint32_t x1046; fiat_p384_uint1 x1047; - fiat_p384_addcarryx_u32(&x1046, &x1047, x1045, x1022, x982); + fiat_p384_subborrowx_u32(&x1046, &x1047, x1045, x1016, UINT32_C(0xffffffff)); uint32_t x1048; fiat_p384_uint1 x1049; - fiat_p384_addcarryx_u32(&x1048, &x1049, x1047, x1024, x984); + fiat_p384_subborrowx_u32(&x1048, &x1049, x1047, x1018, UINT32_C(0xffffffff)); uint32_t x1050; fiat_p384_uint1 x1051; - fiat_p384_addcarryx_u32(&x1050, &x1051, x1049, x1026, x986); + fiat_p384_subborrowx_u32(&x1050, &x1051, x1049, x1020, UINT32_C(0xffffffff)); uint32_t x1052; fiat_p384_uint1 x1053; - fiat_p384_addcarryx_u32(&x1052, &x1053, x1027, 0x0, x993); + fiat_p384_subborrowx_u32(&x1052, &x1053, x1051, x1022, UINT32_C(0xffffffff)); uint32_t x1054; fiat_p384_uint1 x1055; - fiat_p384_addcarryx_u32(&x1054, &x1055, x1051, x1052, x990); + fiat_p384_subborrowx_u32(&x1054, &x1055, x1053, x1030, UINT32_C(0xffffffff)); uint32_t x1056; fiat_p384_uint1 x1057; - fiat_p384_subborrowx_u32(&x1056, &x1057, 0x0, x1030, UINT32_C(0xffffffff)); + fiat_p384_addcarryx_u32(&x1056, &x1057, x1031, 0x0, 0x0); uint32_t x1058; fiat_p384_uint1 x1059; - fiat_p384_subborrowx_u32(&x1058, &x1059, x1057, x1032, 0x0); + fiat_p384_subborrowx_u32(&x1058, &x1059, x1055, (fiat_p384_uint1)x1056, 0x0); uint32_t x1060; - fiat_p384_uint1 x1061; - fiat_p384_subborrowx_u32(&x1060, &x1061, x1059, x1034, 0x0); + fiat_p384_cmovznz_u32(&x1060, x1059, x1032, x1002); + uint32_t x1061; + fiat_p384_cmovznz_u32(&x1061, x1059, x1034, x1004); uint32_t x1062; - fiat_p384_uint1 x1063; - fiat_p384_subborrowx_u32(&x1062, &x1063, x1061, x1036, UINT32_C(0xffffffff)); + fiat_p384_cmovznz_u32(&x1062, x1059, x1036, x1006); + uint32_t x1063; + fiat_p384_cmovznz_u32(&x1063, x1059, x1038, x1008); uint32_t x1064; - fiat_p384_uint1 x1065; - fiat_p384_subborrowx_u32(&x1064, &x1065, x1063, x1038, UINT32_C(0xfffffffe)); + fiat_p384_cmovznz_u32(&x1064, x1059, x1040, x1010); + uint32_t x1065; + fiat_p384_cmovznz_u32(&x1065, x1059, x1042, x1012); uint32_t x1066; - fiat_p384_uint1 x1067; - fiat_p384_subborrowx_u32(&x1066, &x1067, x1065, x1040, UINT32_C(0xffffffff)); + fiat_p384_cmovznz_u32(&x1066, x1059, x1044, x1014); + uint32_t x1067; + fiat_p384_cmovznz_u32(&x1067, x1059, x1046, x1016); uint32_t x1068; - fiat_p384_uint1 x1069; - fiat_p384_subborrowx_u32(&x1068, &x1069, x1067, x1042, UINT32_C(0xffffffff)); + fiat_p384_cmovznz_u32(&x1068, x1059, x1048, x1018); + uint32_t x1069; + fiat_p384_cmovznz_u32(&x1069, x1059, x1050, x1020); uint32_t x1070; - fiat_p384_uint1 x1071; - fiat_p384_subborrowx_u32(&x1070, &x1071, x1069, x1044, UINT32_C(0xffffffff)); - uint32_t x1072; - fiat_p384_uint1 x1073; - fiat_p384_subborrowx_u32(&x1072, &x1073, x1071, x1046, UINT32_C(0xffffffff)); - uint32_t x1074; - fiat_p384_uint1 x1075; - fiat_p384_subborrowx_u32(&x1074, &x1075, x1073, x1048, UINT32_C(0xffffffff)); - uint32_t x1076; - fiat_p384_uint1 x1077; - fiat_p384_subborrowx_u32(&x1076, &x1077, x1075, x1050, UINT32_C(0xffffffff)); - uint32_t x1078; - fiat_p384_uint1 x1079; - fiat_p384_subborrowx_u32(&x1078, &x1079, x1077, x1054, UINT32_C(0xffffffff)); - uint32_t x1080; - fiat_p384_uint1 x1081; - fiat_p384_addcarryx_u32(&x1080, &x1081, x1055, 0x0, x991); - uint32_t x1082; - fiat_p384_uint1 x1083; - fiat_p384_subborrowx_u32(&x1082, &x1083, x1079, (fiat_p384_uint1)x1080, 0x0); - uint32_t x1084; - fiat_p384_cmovznz_u32(&x1084, x1083, x1056, x1030); - uint32_t x1085; - fiat_p384_cmovznz_u32(&x1085, x1083, x1058, x1032); - uint32_t x1086; - fiat_p384_cmovznz_u32(&x1086, x1083, x1060, x1034); - uint32_t x1087; - fiat_p384_cmovznz_u32(&x1087, x1083, x1062, x1036); - uint32_t x1088; - fiat_p384_cmovznz_u32(&x1088, x1083, x1064, x1038); - uint32_t x1089; - fiat_p384_cmovznz_u32(&x1089, x1083, x1066, x1040); - uint32_t x1090; - fiat_p384_cmovznz_u32(&x1090, x1083, x1068, x1042); - uint32_t x1091; - fiat_p384_cmovznz_u32(&x1091, x1083, x1070, x1044); - uint32_t x1092; - fiat_p384_cmovznz_u32(&x1092, x1083, x1072, x1046); - uint32_t x1093; - fiat_p384_cmovznz_u32(&x1093, x1083, x1074, x1048); - uint32_t x1094; - fiat_p384_cmovznz_u32(&x1094, x1083, x1076, x1050); - uint32_t x1095; - fiat_p384_cmovznz_u32(&x1095, x1083, x1078, x1054); - out1[0] = x1084; - out1[1] = x1085; - out1[2] = x1086; - out1[3] = x1087; - out1[4] = x1088; - out1[5] = x1089; - out1[6] = x1090; - out1[7] = x1091; - out1[8] = x1092; - out1[9] = x1093; - out1[10] = x1094; - out1[11] = x1095; + fiat_p384_cmovznz_u32(&x1070, x1059, x1052, x1022); + uint32_t x1071; + fiat_p384_cmovznz_u32(&x1071, x1059, x1054, x1030); + out1[0] = x1060; + out1[1] = x1061; + out1[2] = x1062; + out1[3] = x1063; + out1[4] = x1064; + out1[5] = x1065; + out1[6] = x1066; + out1[7] = x1067; + out1[8] = x1068; + out1[9] = x1069; + out1[10] = x1070; + out1[11] = x1071; } /* @@ -7300,153 +7264,142 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) { uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff)); uint8_t x17 = (uint8_t)(x15 >> 8); uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); - fiat_p384_uint1 x19 = (fiat_p384_uint1)(x17 >> 8); - uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); - uint32_t x21 = (x19 + x11); - uint32_t x22 = (x21 >> 8); - uint8_t x23 = (uint8_t)(x21 & UINT8_C(0xff)); - uint32_t x24 = (x22 >> 8); - uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); - uint8_t x26 = (uint8_t)(x24 >> 8); - uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); - fiat_p384_uint1 x28 = (fiat_p384_uint1)(x26 >> 8); - uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); - uint32_t x30 = (x28 + x10); - uint32_t x31 = (x30 >> 8); - uint8_t x32 = (uint8_t)(x30 & UINT8_C(0xff)); - uint32_t x33 = (x31 >> 8); + uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); + uint32_t x20 = (0x0 + x11); + uint32_t x21 = (x20 >> 8); + uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); + uint32_t x23 = (x21 >> 8); + uint8_t x24 = (uint8_t)(x21 & UINT8_C(0xff)); + uint8_t x25 = (uint8_t)(x23 >> 8); + uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); + uint8_t x27 = (uint8_t)(x25 & UINT8_C(0xff)); + uint32_t x28 = (0x0 + x10); + uint32_t x29 = (x28 >> 8); + uint8_t x30 = (uint8_t)(x28 & UINT8_C(0xff)); + uint32_t x31 = (x29 >> 8); + uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); + uint8_t x33 = (uint8_t)(x31 >> 8); uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); - uint8_t x35 = (uint8_t)(x33 >> 8); - uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff)); - fiat_p384_uint1 x37 = (fiat_p384_uint1)(x35 >> 8); - uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); - uint32_t x39 = (x37 + x9); - uint32_t x40 = (x39 >> 8); - uint8_t x41 = (uint8_t)(x39 & UINT8_C(0xff)); - uint32_t x42 = (x40 >> 8); - uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff)); - uint8_t x44 = (uint8_t)(x42 >> 8); - uint8_t x45 = (uint8_t)(x42 & UINT8_C(0xff)); - fiat_p384_uint1 x46 = (fiat_p384_uint1)(x44 >> 8); - uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff)); - uint32_t x48 = (x46 + x8); - uint32_t x49 = (x48 >> 8); - uint8_t x50 = (uint8_t)(x48 & UINT8_C(0xff)); - uint32_t x51 = (x49 >> 8); - uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff)); - uint8_t x53 = (uint8_t)(x51 >> 8); - uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff)); - fiat_p384_uint1 x55 = (fiat_p384_uint1)(x53 >> 8); + uint8_t x35 = (uint8_t)(x33 & UINT8_C(0xff)); + uint32_t x36 = (0x0 + x9); + uint32_t x37 = (x36 >> 8); + uint8_t x38 = (uint8_t)(x36 & UINT8_C(0xff)); + uint32_t x39 = (x37 >> 8); + uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); + uint8_t x41 = (uint8_t)(x39 >> 8); + uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); + uint8_t x43 = (uint8_t)(x41 & UINT8_C(0xff)); + uint32_t x44 = (0x0 + x8); + uint32_t x45 = (x44 >> 8); + uint8_t x46 = (uint8_t)(x44 & UINT8_C(0xff)); + uint32_t x47 = (x45 >> 8); + uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); + uint8_t x49 = (uint8_t)(x47 >> 8); + uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); + uint8_t x51 = (uint8_t)(x49 & UINT8_C(0xff)); + uint32_t x52 = (0x0 + x7); + uint32_t x53 = (x52 >> 8); + uint8_t x54 = (uint8_t)(x52 & UINT8_C(0xff)); + uint32_t x55 = (x53 >> 8); uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); - uint32_t x57 = (x55 + x7); - uint32_t x58 = (x57 >> 8); + uint8_t x57 = (uint8_t)(x55 >> 8); + uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff)); uint8_t x59 = (uint8_t)(x57 & UINT8_C(0xff)); - uint32_t x60 = (x58 >> 8); - uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); - uint8_t x62 = (uint8_t)(x60 >> 8); - uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); - fiat_p384_uint1 x64 = (fiat_p384_uint1)(x62 >> 8); - uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff)); - uint32_t x66 = (x64 + x6); - uint32_t x67 = (x66 >> 8); - uint8_t x68 = (uint8_t)(x66 & UINT8_C(0xff)); - uint32_t x69 = (x67 >> 8); - uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); - uint8_t x71 = (uint8_t)(x69 >> 8); + uint32_t x60 = (0x0 + x6); + uint32_t x61 = (x60 >> 8); + uint8_t x62 = (uint8_t)(x60 & UINT8_C(0xff)); + uint32_t x63 = (x61 >> 8); + uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff)); + uint8_t x65 = (uint8_t)(x63 >> 8); + uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); + uint8_t x67 = (uint8_t)(x65 & UINT8_C(0xff)); + uint32_t x68 = (0x0 + x5); + uint32_t x69 = (x68 >> 8); + uint8_t x70 = (uint8_t)(x68 & UINT8_C(0xff)); + uint32_t x71 = (x69 >> 8); uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff)); - fiat_p384_uint1 x73 = (fiat_p384_uint1)(x71 >> 8); + uint8_t x73 = (uint8_t)(x71 >> 8); uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff)); - uint32_t x75 = (x73 + x5); - uint32_t x76 = (x75 >> 8); - uint8_t x77 = (uint8_t)(x75 & UINT8_C(0xff)); - uint32_t x78 = (x76 >> 8); - uint8_t x79 = (uint8_t)(x76 & UINT8_C(0xff)); - uint8_t x80 = (uint8_t)(x78 >> 8); - uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff)); - fiat_p384_uint1 x82 = (fiat_p384_uint1)(x80 >> 8); - uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff)); - uint32_t x84 = (x82 + x4); + uint8_t x75 = (uint8_t)(x73 & UINT8_C(0xff)); + uint32_t x76 = (0x0 + x4); + uint32_t x77 = (x76 >> 8); + uint8_t x78 = (uint8_t)(x76 & UINT8_C(0xff)); + uint32_t x79 = (x77 >> 8); + uint8_t x80 = (uint8_t)(x77 & UINT8_C(0xff)); + uint8_t x81 = (uint8_t)(x79 >> 8); + uint8_t x82 = (uint8_t)(x79 & UINT8_C(0xff)); + uint8_t x83 = (uint8_t)(x81 & UINT8_C(0xff)); + uint32_t x84 = (0x0 + x3); uint32_t x85 = (x84 >> 8); uint8_t x86 = (uint8_t)(x84 & UINT8_C(0xff)); uint32_t x87 = (x85 >> 8); uint8_t x88 = (uint8_t)(x85 & UINT8_C(0xff)); uint8_t x89 = (uint8_t)(x87 >> 8); uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff)); - fiat_p384_uint1 x91 = (fiat_p384_uint1)(x89 >> 8); - uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff)); - uint32_t x93 = (x91 + x3); - uint32_t x94 = (x93 >> 8); - uint8_t x95 = (uint8_t)(x93 & UINT8_C(0xff)); - uint32_t x96 = (x94 >> 8); - uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff)); - uint8_t x98 = (uint8_t)(x96 >> 8); - uint8_t x99 = (uint8_t)(x96 & UINT8_C(0xff)); - fiat_p384_uint1 x100 = (fiat_p384_uint1)(x98 >> 8); - uint8_t x101 = (uint8_t)(x98 & UINT8_C(0xff)); - uint32_t x102 = (x100 + x2); - uint32_t x103 = (x102 >> 8); - uint8_t x104 = (uint8_t)(x102 & UINT8_C(0xff)); - uint32_t x105 = (x103 >> 8); + uint8_t x91 = (uint8_t)(x89 & UINT8_C(0xff)); + uint32_t x92 = (0x0 + x2); + uint32_t x93 = (x92 >> 8); + uint8_t x94 = (uint8_t)(x92 & UINT8_C(0xff)); + uint32_t x95 = (x93 >> 8); + uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff)); + uint8_t x97 = (uint8_t)(x95 >> 8); + uint8_t x98 = (uint8_t)(x95 & UINT8_C(0xff)); + uint8_t x99 = (uint8_t)(x97 & UINT8_C(0xff)); + uint32_t x100 = (0x0 + x1); + uint32_t x101 = (x100 >> 8); + uint8_t x102 = (uint8_t)(x100 & UINT8_C(0xff)); + uint32_t x103 = (x101 >> 8); + uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff)); + uint8_t x105 = (uint8_t)(x103 >> 8); uint8_t x106 = (uint8_t)(x103 & UINT8_C(0xff)); - uint8_t x107 = (uint8_t)(x105 >> 8); - uint8_t x108 = (uint8_t)(x105 & UINT8_C(0xff)); - fiat_p384_uint1 x109 = (fiat_p384_uint1)(x107 >> 8); - uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff)); - uint32_t x111 = (x109 + x1); - uint32_t x112 = (x111 >> 8); - uint8_t x113 = (uint8_t)(x111 & UINT8_C(0xff)); - uint32_t x114 = (x112 >> 8); - uint8_t x115 = (uint8_t)(x112 & UINT8_C(0xff)); - uint8_t x116 = (uint8_t)(x114 >> 8); - uint8_t x117 = (uint8_t)(x114 & UINT8_C(0xff)); out1[0] = x14; out1[1] = x16; out1[2] = x18; - out1[3] = x20; - out1[4] = x23; - out1[5] = x25; - out1[6] = x27; - out1[7] = x29; - out1[8] = x32; - out1[9] = x34; - out1[10] = x36; - out1[11] = x38; - out1[12] = x41; - out1[13] = x43; - out1[14] = x45; - out1[15] = x47; - out1[16] = x50; - out1[17] = x52; - out1[18] = x54; - out1[19] = x56; - out1[20] = x59; - out1[21] = x61; - out1[22] = x63; - out1[23] = x65; - out1[24] = x68; - out1[25] = x70; - out1[26] = x72; - out1[27] = x74; - out1[28] = x77; - out1[29] = x79; - out1[30] = x81; - out1[31] = x83; - out1[32] = x86; - out1[33] = x88; - out1[34] = x90; - out1[35] = x92; - out1[36] = x95; - out1[37] = x97; - out1[38] = x99; - out1[39] = x101; - out1[40] = x104; - out1[41] = x106; - out1[42] = x108; - out1[43] = x110; - out1[44] = x113; - out1[45] = x115; - out1[46] = x117; - out1[47] = x116; + out1[3] = x19; + out1[4] = x22; + out1[5] = x24; + out1[6] = x26; + out1[7] = x27; + out1[8] = x30; + out1[9] = x32; + out1[10] = x34; + out1[11] = x35; + out1[12] = x38; + out1[13] = x40; + out1[14] = x42; + out1[15] = x43; + out1[16] = x46; + out1[17] = x48; + out1[18] = x50; + out1[19] = x51; + out1[20] = x54; + out1[21] = x56; + out1[22] = x58; + out1[23] = x59; + out1[24] = x62; + out1[25] = x64; + out1[26] = x66; + out1[27] = x67; + out1[28] = x70; + out1[29] = x72; + out1[30] = x74; + out1[31] = x75; + out1[32] = x78; + out1[33] = x80; + out1[34] = x82; + out1[35] = x83; + out1[36] = x86; + out1[37] = x88; + out1[38] = x90; + out1[39] = x91; + out1[40] = x94; + out1[41] = x96; + out1[42] = x98; + out1[43] = x99; + out1[44] = x102; + out1[45] = x104; + out1[46] = x106; + out1[47] = x105; } /* @@ -7505,61 +7458,50 @@ static void fiat_p384_from_bytes(uint32_t out1[12], const uint8_t arg1[48]) { uint32_t x47 = ((uint32_t)(arg1[1]) << 8); uint8_t x48 = (arg1[0]); uint32_t x49 = (x48 + (x47 + (x46 + x45))); - fiat_p384_uint1 x50 = (fiat_p384_uint1)((uint64_t)x49 >> 32); - uint32_t x51 = (x49 & UINT32_C(0xffffffff)); - uint32_t x52 = (x4 + (x3 + (x2 + x1))); - uint32_t x53 = (x8 + (x7 + (x6 + x5))); - uint32_t x54 = (x12 + (x11 + (x10 + x9))); - uint32_t x55 = (x16 + (x15 + (x14 + x13))); - uint32_t x56 = (x20 + (x19 + (x18 + x17))); - uint32_t x57 = (x24 + (x23 + (x22 + x21))); - uint32_t x58 = (x28 + (x27 + (x26 + x25))); - uint32_t x59 = (x32 + (x31 + (x30 + x29))); - uint32_t x60 = (x36 + (x35 + (x34 + x33))); - uint32_t x61 = (x40 + (x39 + (x38 + x37))); - uint32_t x62 = (x44 + (x43 + (x42 + x41))); - uint32_t x63 = (x50 + x62); - fiat_p384_uint1 x64 = (fiat_p384_uint1)((uint64_t)x63 >> 32); - uint32_t x65 = (x63 & UINT32_C(0xffffffff)); - uint32_t x66 = (x64 + x61); - fiat_p384_uint1 x67 = (fiat_p384_uint1)((uint64_t)x66 >> 32); - uint32_t x68 = (x66 & UINT32_C(0xffffffff)); - uint32_t x69 = (x67 + x60); - fiat_p384_uint1 x70 = (fiat_p384_uint1)((uint64_t)x69 >> 32); - uint32_t x71 = (x69 & UINT32_C(0xffffffff)); - uint32_t x72 = (x70 + x59); - fiat_p384_uint1 x73 = (fiat_p384_uint1)((uint64_t)x72 >> 32); - uint32_t x74 = (x72 & UINT32_C(0xffffffff)); - uint32_t x75 = (x73 + x58); - fiat_p384_uint1 x76 = (fiat_p384_uint1)((uint64_t)x75 >> 32); - uint32_t x77 = (x75 & UINT32_C(0xffffffff)); - uint32_t x78 = (x76 + x57); - fiat_p384_uint1 x79 = (fiat_p384_uint1)((uint64_t)x78 >> 32); - uint32_t x80 = (x78 & UINT32_C(0xffffffff)); - uint32_t x81 = (x79 + x56); - fiat_p384_uint1 x82 = (fiat_p384_uint1)((uint64_t)x81 >> 32); - uint32_t x83 = (x81 & UINT32_C(0xffffffff)); - uint32_t x84 = (x82 + x55); - fiat_p384_uint1 x85 = (fiat_p384_uint1)((uint64_t)x84 >> 32); - uint32_t x86 = (x84 & UINT32_C(0xffffffff)); - uint32_t x87 = (x85 + x54); - fiat_p384_uint1 x88 = (fiat_p384_uint1)((uint64_t)x87 >> 32); - uint32_t x89 = (x87 & UINT32_C(0xffffffff)); - uint32_t x90 = (x88 + x53); - fiat_p384_uint1 x91 = (fiat_p384_uint1)((uint64_t)x90 >> 32); - uint32_t x92 = (x90 & UINT32_C(0xffffffff)); - uint32_t x93 = (x91 + x52); - out1[0] = x51; - out1[1] = x65; - out1[2] = x68; - out1[3] = x71; - out1[4] = x74; - out1[5] = x77; - out1[6] = x80; - out1[7] = x83; - out1[8] = x86; - out1[9] = x89; - out1[10] = x92; - out1[11] = x93; + uint32_t x50 = (x49 & UINT32_C(0xffffffff)); + uint32_t x51 = (x4 + (x3 + (x2 + x1))); + uint32_t x52 = (x8 + (x7 + (x6 + x5))); + uint32_t x53 = (x12 + (x11 + (x10 + x9))); + uint32_t x54 = (x16 + (x15 + (x14 + x13))); + uint32_t x55 = (x20 + (x19 + (x18 + x17))); + uint32_t x56 = (x24 + (x23 + (x22 + x21))); + uint32_t x57 = (x28 + (x27 + (x26 + x25))); + uint32_t x58 = (x32 + (x31 + (x30 + x29))); + uint32_t x59 = (x36 + (x35 + (x34 + x33))); + uint32_t x60 = (x40 + (x39 + (x38 + x37))); + uint32_t x61 = (x44 + (x43 + (x42 + x41))); + uint32_t x62 = (0x0 + x61); + uint32_t x63 = (x62 & UINT32_C(0xffffffff)); + uint32_t x64 = (0x0 + x60); + uint32_t x65 = (x64 & UINT32_C(0xffffffff)); + uint32_t x66 = (0x0 + x59); + uint32_t x67 = (x66 & UINT32_C(0xffffffff)); + uint32_t x68 = (0x0 + x58); + uint32_t x69 = (x68 & UINT32_C(0xffffffff)); + uint32_t x70 = (0x0 + x57); + uint32_t x71 = (x70 & UINT32_C(0xffffffff)); + uint32_t x72 = (0x0 + x56); + uint32_t x73 = (x72 & UINT32_C(0xffffffff)); + uint32_t x74 = (0x0 + x55); + uint32_t x75 = (x74 & UINT32_C(0xffffffff)); + uint32_t x76 = (0x0 + x54); + uint32_t x77 = (x76 & UINT32_C(0xffffffff)); + uint32_t x78 = (0x0 + x53); + uint32_t x79 = (x78 & UINT32_C(0xffffffff)); + uint32_t x80 = (0x0 + x52); + uint32_t x81 = (x80 & UINT32_C(0xffffffff)); + uint32_t x82 = (0x0 + x51); + out1[0] = x50; + out1[1] = x63; + out1[2] = x65; + out1[3] = x67; + out1[4] = x69; + out1[5] = x71; + out1[6] = x73; + out1[7] = x75; + out1[8] = x77; + out1[9] = x79; + out1[10] = x81; + out1[11] = x82; } |