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 /secp256k1_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 'secp256k1_32.c')
| -rw-r--r-- | secp256k1_32.c | 794 |
1 files changed, 390 insertions, 404 deletions
diff --git a/secp256k1_32.c b/secp256k1_32.c index 94744d26a..a4015f134 100644 --- a/secp256k1_32.c +++ b/secp256k1_32.c @@ -2991,781 +2991,781 @@ static void fiat_secp256k1_from_montgomery(uint32_t out1[8], const uint32_t arg1 fiat_secp256k1_uint1 x69; fiat_secp256k1_addcarryx_u32(&x68, &x69, x67, 0x0, x52); uint32_t x70; - fiat_secp256k1_uint1 x71; - fiat_secp256k1_addcarryx_u32(&x70, &x71, x53, 0x0, 0x0); + uint32_t x71; + fiat_secp256k1_mulx_u32(&x70, &x71, x54, UINT32_C(0xd2253531)); uint32_t x72; - fiat_secp256k1_uint1 x73; - fiat_secp256k1_addcarryx_u32(&x72, &x73, x69, 0x0, (fiat_secp256k1_uint1)x70); + uint32_t x73; + fiat_secp256k1_mulx_u32(&x72, &x73, x70, UINT32_C(0xffffffff)); uint32_t x74; uint32_t x75; - fiat_secp256k1_mulx_u32(&x74, &x75, x54, UINT32_C(0xd2253531)); + fiat_secp256k1_mulx_u32(&x74, &x75, x70, UINT32_C(0xffffffff)); uint32_t x76; uint32_t x77; - fiat_secp256k1_mulx_u32(&x76, &x77, x74, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x76, &x77, x70, UINT32_C(0xffffffff)); uint32_t x78; uint32_t x79; - fiat_secp256k1_mulx_u32(&x78, &x79, x74, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x78, &x79, x70, UINT32_C(0xffffffff)); uint32_t x80; uint32_t x81; - fiat_secp256k1_mulx_u32(&x80, &x81, x74, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x80, &x81, x70, UINT32_C(0xffffffff)); uint32_t x82; uint32_t x83; - fiat_secp256k1_mulx_u32(&x82, &x83, x74, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x82, &x83, x70, UINT32_C(0xffffffff)); uint32_t x84; uint32_t x85; - fiat_secp256k1_mulx_u32(&x84, &x85, x74, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x84, &x85, x70, UINT32_C(0xfffffffe)); uint32_t x86; uint32_t x87; - fiat_secp256k1_mulx_u32(&x86, &x87, x74, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x86, &x87, x70, UINT32_C(0xfffffc2f)); uint32_t x88; - uint32_t x89; - fiat_secp256k1_mulx_u32(&x88, &x89, x74, UINT32_C(0xfffffffe)); + fiat_secp256k1_uint1 x89; + fiat_secp256k1_addcarryx_u32(&x88, &x89, 0x0, x84, x87); uint32_t x90; - uint32_t x91; - fiat_secp256k1_mulx_u32(&x90, &x91, x74, UINT32_C(0xfffffc2f)); + fiat_secp256k1_uint1 x91; + fiat_secp256k1_addcarryx_u32(&x90, &x91, x89, x82, x85); uint32_t x92; fiat_secp256k1_uint1 x93; - fiat_secp256k1_addcarryx_u32(&x92, &x93, 0x0, x88, x91); + fiat_secp256k1_addcarryx_u32(&x92, &x93, x91, x80, x83); uint32_t x94; fiat_secp256k1_uint1 x95; - fiat_secp256k1_addcarryx_u32(&x94, &x95, x93, x86, x89); + fiat_secp256k1_addcarryx_u32(&x94, &x95, x93, x78, x81); uint32_t x96; fiat_secp256k1_uint1 x97; - fiat_secp256k1_addcarryx_u32(&x96, &x97, x95, x84, x87); + fiat_secp256k1_addcarryx_u32(&x96, &x97, x95, x76, x79); uint32_t x98; fiat_secp256k1_uint1 x99; - fiat_secp256k1_addcarryx_u32(&x98, &x99, x97, x82, x85); + fiat_secp256k1_addcarryx_u32(&x98, &x99, x97, x74, x77); uint32_t x100; fiat_secp256k1_uint1 x101; - fiat_secp256k1_addcarryx_u32(&x100, &x101, x99, x80, x83); + fiat_secp256k1_addcarryx_u32(&x100, &x101, x99, x72, x75); uint32_t x102; fiat_secp256k1_uint1 x103; - fiat_secp256k1_addcarryx_u32(&x102, &x103, x101, x78, x81); + fiat_secp256k1_addcarryx_u32(&x102, &x103, 0x0, x86, x54); uint32_t x104; fiat_secp256k1_uint1 x105; - fiat_secp256k1_addcarryx_u32(&x104, &x105, x103, x76, x79); + fiat_secp256k1_addcarryx_u32(&x104, &x105, x103, x88, x56); uint32_t x106; fiat_secp256k1_uint1 x107; - fiat_secp256k1_addcarryx_u32(&x106, &x107, 0x0, x90, x54); + fiat_secp256k1_addcarryx_u32(&x106, &x107, x105, x90, x58); uint32_t x108; fiat_secp256k1_uint1 x109; - fiat_secp256k1_addcarryx_u32(&x108, &x109, x107, x92, x56); + fiat_secp256k1_addcarryx_u32(&x108, &x109, x107, x92, x60); uint32_t x110; fiat_secp256k1_uint1 x111; - fiat_secp256k1_addcarryx_u32(&x110, &x111, x109, x94, x58); + fiat_secp256k1_addcarryx_u32(&x110, &x111, x109, x94, x62); uint32_t x112; fiat_secp256k1_uint1 x113; - fiat_secp256k1_addcarryx_u32(&x112, &x113, x111, x96, x60); + fiat_secp256k1_addcarryx_u32(&x112, &x113, x111, x96, x64); uint32_t x114; fiat_secp256k1_uint1 x115; - fiat_secp256k1_addcarryx_u32(&x114, &x115, x113, x98, x62); + fiat_secp256k1_addcarryx_u32(&x114, &x115, x113, x98, x66); uint32_t x116; fiat_secp256k1_uint1 x117; - fiat_secp256k1_addcarryx_u32(&x116, &x117, x115, x100, x64); + fiat_secp256k1_addcarryx_u32(&x116, &x117, x115, x100, x68); uint32_t x118; fiat_secp256k1_uint1 x119; - fiat_secp256k1_addcarryx_u32(&x118, &x119, x117, x102, x66); + fiat_secp256k1_addcarryx_u32(&x118, &x119, x53, 0x0, 0x0); uint32_t x120; fiat_secp256k1_uint1 x121; - fiat_secp256k1_addcarryx_u32(&x120, &x121, x119, x104, x68); + fiat_secp256k1_addcarryx_u32(&x120, &x121, x69, 0x0, (fiat_secp256k1_uint1)x118); uint32_t x122; fiat_secp256k1_uint1 x123; - fiat_secp256k1_addcarryx_u32(&x122, &x123, x105, 0x0, x77); + fiat_secp256k1_addcarryx_u32(&x122, &x123, x101, 0x0, x73); uint32_t x124; fiat_secp256k1_uint1 x125; - fiat_secp256k1_addcarryx_u32(&x124, &x125, x121, x122, x72); + fiat_secp256k1_addcarryx_u32(&x124, &x125, x117, x122, x120); uint32_t x126; fiat_secp256k1_uint1 x127; - fiat_secp256k1_addcarryx_u32(&x126, &x127, 0x0, (arg1[2]), x108); + fiat_secp256k1_addcarryx_u32(&x126, &x127, 0x0, (arg1[2]), x104); uint32_t x128; fiat_secp256k1_uint1 x129; - fiat_secp256k1_addcarryx_u32(&x128, &x129, x127, 0x0, x110); + fiat_secp256k1_addcarryx_u32(&x128, &x129, x127, 0x0, x106); uint32_t x130; fiat_secp256k1_uint1 x131; - fiat_secp256k1_addcarryx_u32(&x130, &x131, x129, 0x0, x112); + fiat_secp256k1_addcarryx_u32(&x130, &x131, x129, 0x0, x108); uint32_t x132; fiat_secp256k1_uint1 x133; - fiat_secp256k1_addcarryx_u32(&x132, &x133, x131, 0x0, x114); + fiat_secp256k1_addcarryx_u32(&x132, &x133, x131, 0x0, x110); uint32_t x134; fiat_secp256k1_uint1 x135; - fiat_secp256k1_addcarryx_u32(&x134, &x135, x133, 0x0, x116); + fiat_secp256k1_addcarryx_u32(&x134, &x135, x133, 0x0, x112); uint32_t x136; fiat_secp256k1_uint1 x137; - fiat_secp256k1_addcarryx_u32(&x136, &x137, x135, 0x0, x118); + fiat_secp256k1_addcarryx_u32(&x136, &x137, x135, 0x0, x114); uint32_t x138; fiat_secp256k1_uint1 x139; - fiat_secp256k1_addcarryx_u32(&x138, &x139, x137, 0x0, x120); + fiat_secp256k1_addcarryx_u32(&x138, &x139, x137, 0x0, x116); uint32_t x140; fiat_secp256k1_uint1 x141; fiat_secp256k1_addcarryx_u32(&x140, &x141, x139, 0x0, x124); uint32_t x142; - fiat_secp256k1_uint1 x143; - fiat_secp256k1_addcarryx_u32(&x142, &x143, x125, 0x0, x73); + uint32_t x143; + fiat_secp256k1_mulx_u32(&x142, &x143, x126, UINT32_C(0xd2253531)); uint32_t x144; - fiat_secp256k1_uint1 x145; - fiat_secp256k1_addcarryx_u32(&x144, &x145, x141, 0x0, (fiat_secp256k1_uint1)x142); + uint32_t x145; + fiat_secp256k1_mulx_u32(&x144, &x145, x142, UINT32_C(0xffffffff)); uint32_t x146; uint32_t x147; - fiat_secp256k1_mulx_u32(&x146, &x147, x126, UINT32_C(0xd2253531)); + fiat_secp256k1_mulx_u32(&x146, &x147, x142, UINT32_C(0xffffffff)); uint32_t x148; uint32_t x149; - fiat_secp256k1_mulx_u32(&x148, &x149, x146, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x148, &x149, x142, UINT32_C(0xffffffff)); uint32_t x150; uint32_t x151; - fiat_secp256k1_mulx_u32(&x150, &x151, x146, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x150, &x151, x142, UINT32_C(0xffffffff)); uint32_t x152; uint32_t x153; - fiat_secp256k1_mulx_u32(&x152, &x153, x146, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x152, &x153, x142, UINT32_C(0xffffffff)); uint32_t x154; uint32_t x155; - fiat_secp256k1_mulx_u32(&x154, &x155, x146, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x154, &x155, x142, UINT32_C(0xffffffff)); uint32_t x156; uint32_t x157; - fiat_secp256k1_mulx_u32(&x156, &x157, x146, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x156, &x157, x142, UINT32_C(0xfffffffe)); uint32_t x158; uint32_t x159; - fiat_secp256k1_mulx_u32(&x158, &x159, x146, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x158, &x159, x142, UINT32_C(0xfffffc2f)); uint32_t x160; - uint32_t x161; - fiat_secp256k1_mulx_u32(&x160, &x161, x146, UINT32_C(0xfffffffe)); + fiat_secp256k1_uint1 x161; + fiat_secp256k1_addcarryx_u32(&x160, &x161, 0x0, x156, x159); uint32_t x162; - uint32_t x163; - fiat_secp256k1_mulx_u32(&x162, &x163, x146, UINT32_C(0xfffffc2f)); + fiat_secp256k1_uint1 x163; + fiat_secp256k1_addcarryx_u32(&x162, &x163, x161, x154, x157); uint32_t x164; fiat_secp256k1_uint1 x165; - fiat_secp256k1_addcarryx_u32(&x164, &x165, 0x0, x160, x163); + fiat_secp256k1_addcarryx_u32(&x164, &x165, x163, x152, x155); uint32_t x166; fiat_secp256k1_uint1 x167; - fiat_secp256k1_addcarryx_u32(&x166, &x167, x165, x158, x161); + fiat_secp256k1_addcarryx_u32(&x166, &x167, x165, x150, x153); uint32_t x168; fiat_secp256k1_uint1 x169; - fiat_secp256k1_addcarryx_u32(&x168, &x169, x167, x156, x159); + fiat_secp256k1_addcarryx_u32(&x168, &x169, x167, x148, x151); uint32_t x170; fiat_secp256k1_uint1 x171; - fiat_secp256k1_addcarryx_u32(&x170, &x171, x169, x154, x157); + fiat_secp256k1_addcarryx_u32(&x170, &x171, x169, x146, x149); uint32_t x172; fiat_secp256k1_uint1 x173; - fiat_secp256k1_addcarryx_u32(&x172, &x173, x171, x152, x155); + fiat_secp256k1_addcarryx_u32(&x172, &x173, x171, x144, x147); uint32_t x174; fiat_secp256k1_uint1 x175; - fiat_secp256k1_addcarryx_u32(&x174, &x175, x173, x150, x153); + fiat_secp256k1_addcarryx_u32(&x174, &x175, 0x0, x158, x126); uint32_t x176; fiat_secp256k1_uint1 x177; - fiat_secp256k1_addcarryx_u32(&x176, &x177, x175, x148, x151); + fiat_secp256k1_addcarryx_u32(&x176, &x177, x175, x160, x128); uint32_t x178; fiat_secp256k1_uint1 x179; - fiat_secp256k1_addcarryx_u32(&x178, &x179, 0x0, x162, x126); + fiat_secp256k1_addcarryx_u32(&x178, &x179, x177, x162, x130); uint32_t x180; fiat_secp256k1_uint1 x181; - fiat_secp256k1_addcarryx_u32(&x180, &x181, x179, x164, x128); + fiat_secp256k1_addcarryx_u32(&x180, &x181, x179, x164, x132); uint32_t x182; fiat_secp256k1_uint1 x183; - fiat_secp256k1_addcarryx_u32(&x182, &x183, x181, x166, x130); + fiat_secp256k1_addcarryx_u32(&x182, &x183, x181, x166, x134); uint32_t x184; fiat_secp256k1_uint1 x185; - fiat_secp256k1_addcarryx_u32(&x184, &x185, x183, x168, x132); + fiat_secp256k1_addcarryx_u32(&x184, &x185, x183, x168, x136); uint32_t x186; fiat_secp256k1_uint1 x187; - fiat_secp256k1_addcarryx_u32(&x186, &x187, x185, x170, x134); + fiat_secp256k1_addcarryx_u32(&x186, &x187, x185, x170, x138); uint32_t x188; fiat_secp256k1_uint1 x189; - fiat_secp256k1_addcarryx_u32(&x188, &x189, x187, x172, x136); + fiat_secp256k1_addcarryx_u32(&x188, &x189, x187, x172, x140); uint32_t x190; fiat_secp256k1_uint1 x191; - fiat_secp256k1_addcarryx_u32(&x190, &x191, x189, x174, x138); + fiat_secp256k1_addcarryx_u32(&x190, &x191, x125, 0x0, 0x0); uint32_t x192; fiat_secp256k1_uint1 x193; - fiat_secp256k1_addcarryx_u32(&x192, &x193, x191, x176, x140); + fiat_secp256k1_addcarryx_u32(&x192, &x193, x141, 0x0, (fiat_secp256k1_uint1)x190); uint32_t x194; fiat_secp256k1_uint1 x195; - fiat_secp256k1_addcarryx_u32(&x194, &x195, x177, 0x0, x149); + fiat_secp256k1_addcarryx_u32(&x194, &x195, x173, 0x0, x145); uint32_t x196; fiat_secp256k1_uint1 x197; - fiat_secp256k1_addcarryx_u32(&x196, &x197, x193, x194, x144); + fiat_secp256k1_addcarryx_u32(&x196, &x197, x189, x194, x192); uint32_t x198; fiat_secp256k1_uint1 x199; - fiat_secp256k1_addcarryx_u32(&x198, &x199, 0x0, (arg1[3]), x180); + fiat_secp256k1_addcarryx_u32(&x198, &x199, 0x0, (arg1[3]), x176); uint32_t x200; fiat_secp256k1_uint1 x201; - fiat_secp256k1_addcarryx_u32(&x200, &x201, x199, 0x0, x182); + fiat_secp256k1_addcarryx_u32(&x200, &x201, x199, 0x0, x178); uint32_t x202; fiat_secp256k1_uint1 x203; - fiat_secp256k1_addcarryx_u32(&x202, &x203, x201, 0x0, x184); + fiat_secp256k1_addcarryx_u32(&x202, &x203, x201, 0x0, x180); uint32_t x204; fiat_secp256k1_uint1 x205; - fiat_secp256k1_addcarryx_u32(&x204, &x205, x203, 0x0, x186); + fiat_secp256k1_addcarryx_u32(&x204, &x205, x203, 0x0, x182); uint32_t x206; fiat_secp256k1_uint1 x207; - fiat_secp256k1_addcarryx_u32(&x206, &x207, x205, 0x0, x188); + fiat_secp256k1_addcarryx_u32(&x206, &x207, x205, 0x0, x184); uint32_t x208; fiat_secp256k1_uint1 x209; - fiat_secp256k1_addcarryx_u32(&x208, &x209, x207, 0x0, x190); + fiat_secp256k1_addcarryx_u32(&x208, &x209, x207, 0x0, x186); uint32_t x210; fiat_secp256k1_uint1 x211; - fiat_secp256k1_addcarryx_u32(&x210, &x211, x209, 0x0, x192); + fiat_secp256k1_addcarryx_u32(&x210, &x211, x209, 0x0, x188); uint32_t x212; fiat_secp256k1_uint1 x213; fiat_secp256k1_addcarryx_u32(&x212, &x213, x211, 0x0, x196); uint32_t x214; - fiat_secp256k1_uint1 x215; - fiat_secp256k1_addcarryx_u32(&x214, &x215, x197, 0x0, x145); + uint32_t x215; + fiat_secp256k1_mulx_u32(&x214, &x215, x198, UINT32_C(0xd2253531)); uint32_t x216; - fiat_secp256k1_uint1 x217; - fiat_secp256k1_addcarryx_u32(&x216, &x217, x213, 0x0, (fiat_secp256k1_uint1)x214); + uint32_t x217; + fiat_secp256k1_mulx_u32(&x216, &x217, x214, UINT32_C(0xffffffff)); uint32_t x218; uint32_t x219; - fiat_secp256k1_mulx_u32(&x218, &x219, x198, UINT32_C(0xd2253531)); + fiat_secp256k1_mulx_u32(&x218, &x219, x214, UINT32_C(0xffffffff)); uint32_t x220; uint32_t x221; - fiat_secp256k1_mulx_u32(&x220, &x221, x218, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x220, &x221, x214, UINT32_C(0xffffffff)); uint32_t x222; uint32_t x223; - fiat_secp256k1_mulx_u32(&x222, &x223, x218, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x222, &x223, x214, UINT32_C(0xffffffff)); uint32_t x224; uint32_t x225; - fiat_secp256k1_mulx_u32(&x224, &x225, x218, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x224, &x225, x214, UINT32_C(0xffffffff)); uint32_t x226; uint32_t x227; - fiat_secp256k1_mulx_u32(&x226, &x227, x218, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x226, &x227, x214, UINT32_C(0xffffffff)); uint32_t x228; uint32_t x229; - fiat_secp256k1_mulx_u32(&x228, &x229, x218, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x228, &x229, x214, UINT32_C(0xfffffffe)); uint32_t x230; uint32_t x231; - fiat_secp256k1_mulx_u32(&x230, &x231, x218, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x230, &x231, x214, UINT32_C(0xfffffc2f)); uint32_t x232; - uint32_t x233; - fiat_secp256k1_mulx_u32(&x232, &x233, x218, UINT32_C(0xfffffffe)); + fiat_secp256k1_uint1 x233; + fiat_secp256k1_addcarryx_u32(&x232, &x233, 0x0, x228, x231); uint32_t x234; - uint32_t x235; - fiat_secp256k1_mulx_u32(&x234, &x235, x218, UINT32_C(0xfffffc2f)); + fiat_secp256k1_uint1 x235; + fiat_secp256k1_addcarryx_u32(&x234, &x235, x233, x226, x229); uint32_t x236; fiat_secp256k1_uint1 x237; - fiat_secp256k1_addcarryx_u32(&x236, &x237, 0x0, x232, x235); + fiat_secp256k1_addcarryx_u32(&x236, &x237, x235, x224, x227); uint32_t x238; fiat_secp256k1_uint1 x239; - fiat_secp256k1_addcarryx_u32(&x238, &x239, x237, x230, x233); + fiat_secp256k1_addcarryx_u32(&x238, &x239, x237, x222, x225); uint32_t x240; fiat_secp256k1_uint1 x241; - fiat_secp256k1_addcarryx_u32(&x240, &x241, x239, x228, x231); + fiat_secp256k1_addcarryx_u32(&x240, &x241, x239, x220, x223); uint32_t x242; fiat_secp256k1_uint1 x243; - fiat_secp256k1_addcarryx_u32(&x242, &x243, x241, x226, x229); + fiat_secp256k1_addcarryx_u32(&x242, &x243, x241, x218, x221); uint32_t x244; fiat_secp256k1_uint1 x245; - fiat_secp256k1_addcarryx_u32(&x244, &x245, x243, x224, x227); + fiat_secp256k1_addcarryx_u32(&x244, &x245, x243, x216, x219); uint32_t x246; fiat_secp256k1_uint1 x247; - fiat_secp256k1_addcarryx_u32(&x246, &x247, x245, x222, x225); + fiat_secp256k1_addcarryx_u32(&x246, &x247, 0x0, x230, x198); uint32_t x248; fiat_secp256k1_uint1 x249; - fiat_secp256k1_addcarryx_u32(&x248, &x249, x247, x220, x223); + fiat_secp256k1_addcarryx_u32(&x248, &x249, x247, x232, x200); uint32_t x250; fiat_secp256k1_uint1 x251; - fiat_secp256k1_addcarryx_u32(&x250, &x251, 0x0, x234, x198); + fiat_secp256k1_addcarryx_u32(&x250, &x251, x249, x234, x202); uint32_t x252; fiat_secp256k1_uint1 x253; - fiat_secp256k1_addcarryx_u32(&x252, &x253, x251, x236, x200); + fiat_secp256k1_addcarryx_u32(&x252, &x253, x251, x236, x204); uint32_t x254; fiat_secp256k1_uint1 x255; - fiat_secp256k1_addcarryx_u32(&x254, &x255, x253, x238, x202); + fiat_secp256k1_addcarryx_u32(&x254, &x255, x253, x238, x206); uint32_t x256; fiat_secp256k1_uint1 x257; - fiat_secp256k1_addcarryx_u32(&x256, &x257, x255, x240, x204); + fiat_secp256k1_addcarryx_u32(&x256, &x257, x255, x240, x208); uint32_t x258; fiat_secp256k1_uint1 x259; - fiat_secp256k1_addcarryx_u32(&x258, &x259, x257, x242, x206); + fiat_secp256k1_addcarryx_u32(&x258, &x259, x257, x242, x210); uint32_t x260; fiat_secp256k1_uint1 x261; - fiat_secp256k1_addcarryx_u32(&x260, &x261, x259, x244, x208); + fiat_secp256k1_addcarryx_u32(&x260, &x261, x259, x244, x212); uint32_t x262; fiat_secp256k1_uint1 x263; - fiat_secp256k1_addcarryx_u32(&x262, &x263, x261, x246, x210); + fiat_secp256k1_addcarryx_u32(&x262, &x263, x197, 0x0, 0x0); uint32_t x264; fiat_secp256k1_uint1 x265; - fiat_secp256k1_addcarryx_u32(&x264, &x265, x263, x248, x212); + fiat_secp256k1_addcarryx_u32(&x264, &x265, x213, 0x0, (fiat_secp256k1_uint1)x262); uint32_t x266; fiat_secp256k1_uint1 x267; - fiat_secp256k1_addcarryx_u32(&x266, &x267, x249, 0x0, x221); + fiat_secp256k1_addcarryx_u32(&x266, &x267, x245, 0x0, x217); uint32_t x268; fiat_secp256k1_uint1 x269; - fiat_secp256k1_addcarryx_u32(&x268, &x269, x265, x266, x216); + fiat_secp256k1_addcarryx_u32(&x268, &x269, x261, x266, x264); uint32_t x270; fiat_secp256k1_uint1 x271; - fiat_secp256k1_addcarryx_u32(&x270, &x271, 0x0, (arg1[4]), x252); + fiat_secp256k1_addcarryx_u32(&x270, &x271, 0x0, (arg1[4]), x248); uint32_t x272; fiat_secp256k1_uint1 x273; - fiat_secp256k1_addcarryx_u32(&x272, &x273, x271, 0x0, x254); + fiat_secp256k1_addcarryx_u32(&x272, &x273, x271, 0x0, x250); uint32_t x274; fiat_secp256k1_uint1 x275; - fiat_secp256k1_addcarryx_u32(&x274, &x275, x273, 0x0, x256); + fiat_secp256k1_addcarryx_u32(&x274, &x275, x273, 0x0, x252); uint32_t x276; fiat_secp256k1_uint1 x277; - fiat_secp256k1_addcarryx_u32(&x276, &x277, x275, 0x0, x258); + fiat_secp256k1_addcarryx_u32(&x276, &x277, x275, 0x0, x254); uint32_t x278; fiat_secp256k1_uint1 x279; - fiat_secp256k1_addcarryx_u32(&x278, &x279, x277, 0x0, x260); + fiat_secp256k1_addcarryx_u32(&x278, &x279, x277, 0x0, x256); uint32_t x280; fiat_secp256k1_uint1 x281; - fiat_secp256k1_addcarryx_u32(&x280, &x281, x279, 0x0, x262); + fiat_secp256k1_addcarryx_u32(&x280, &x281, x279, 0x0, x258); uint32_t x282; fiat_secp256k1_uint1 x283; - fiat_secp256k1_addcarryx_u32(&x282, &x283, x281, 0x0, x264); + fiat_secp256k1_addcarryx_u32(&x282, &x283, x281, 0x0, x260); uint32_t x284; fiat_secp256k1_uint1 x285; fiat_secp256k1_addcarryx_u32(&x284, &x285, x283, 0x0, x268); uint32_t x286; - fiat_secp256k1_uint1 x287; - fiat_secp256k1_addcarryx_u32(&x286, &x287, x269, 0x0, x217); + uint32_t x287; + fiat_secp256k1_mulx_u32(&x286, &x287, x270, UINT32_C(0xd2253531)); uint32_t x288; - fiat_secp256k1_uint1 x289; - fiat_secp256k1_addcarryx_u32(&x288, &x289, x285, 0x0, (fiat_secp256k1_uint1)x286); + uint32_t x289; + fiat_secp256k1_mulx_u32(&x288, &x289, x286, UINT32_C(0xffffffff)); uint32_t x290; uint32_t x291; - fiat_secp256k1_mulx_u32(&x290, &x291, x270, UINT32_C(0xd2253531)); + fiat_secp256k1_mulx_u32(&x290, &x291, x286, UINT32_C(0xffffffff)); uint32_t x292; uint32_t x293; - fiat_secp256k1_mulx_u32(&x292, &x293, x290, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x292, &x293, x286, UINT32_C(0xffffffff)); uint32_t x294; uint32_t x295; - fiat_secp256k1_mulx_u32(&x294, &x295, x290, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x294, &x295, x286, UINT32_C(0xffffffff)); uint32_t x296; uint32_t x297; - fiat_secp256k1_mulx_u32(&x296, &x297, x290, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x296, &x297, x286, UINT32_C(0xffffffff)); uint32_t x298; uint32_t x299; - fiat_secp256k1_mulx_u32(&x298, &x299, x290, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x298, &x299, x286, UINT32_C(0xffffffff)); uint32_t x300; uint32_t x301; - fiat_secp256k1_mulx_u32(&x300, &x301, x290, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x300, &x301, x286, UINT32_C(0xfffffffe)); uint32_t x302; uint32_t x303; - fiat_secp256k1_mulx_u32(&x302, &x303, x290, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x302, &x303, x286, UINT32_C(0xfffffc2f)); uint32_t x304; - uint32_t x305; - fiat_secp256k1_mulx_u32(&x304, &x305, x290, UINT32_C(0xfffffffe)); + fiat_secp256k1_uint1 x305; + fiat_secp256k1_addcarryx_u32(&x304, &x305, 0x0, x300, x303); uint32_t x306; - uint32_t x307; - fiat_secp256k1_mulx_u32(&x306, &x307, x290, UINT32_C(0xfffffc2f)); + fiat_secp256k1_uint1 x307; + fiat_secp256k1_addcarryx_u32(&x306, &x307, x305, x298, x301); uint32_t x308; fiat_secp256k1_uint1 x309; - fiat_secp256k1_addcarryx_u32(&x308, &x309, 0x0, x304, x307); + fiat_secp256k1_addcarryx_u32(&x308, &x309, x307, x296, x299); uint32_t x310; fiat_secp256k1_uint1 x311; - fiat_secp256k1_addcarryx_u32(&x310, &x311, x309, x302, x305); + fiat_secp256k1_addcarryx_u32(&x310, &x311, x309, x294, x297); uint32_t x312; fiat_secp256k1_uint1 x313; - fiat_secp256k1_addcarryx_u32(&x312, &x313, x311, x300, x303); + fiat_secp256k1_addcarryx_u32(&x312, &x313, x311, x292, x295); uint32_t x314; fiat_secp256k1_uint1 x315; - fiat_secp256k1_addcarryx_u32(&x314, &x315, x313, x298, x301); + fiat_secp256k1_addcarryx_u32(&x314, &x315, x313, x290, x293); uint32_t x316; fiat_secp256k1_uint1 x317; - fiat_secp256k1_addcarryx_u32(&x316, &x317, x315, x296, x299); + fiat_secp256k1_addcarryx_u32(&x316, &x317, x315, x288, x291); uint32_t x318; fiat_secp256k1_uint1 x319; - fiat_secp256k1_addcarryx_u32(&x318, &x319, x317, x294, x297); + fiat_secp256k1_addcarryx_u32(&x318, &x319, 0x0, x302, x270); uint32_t x320; fiat_secp256k1_uint1 x321; - fiat_secp256k1_addcarryx_u32(&x320, &x321, x319, x292, x295); + fiat_secp256k1_addcarryx_u32(&x320, &x321, x319, x304, x272); uint32_t x322; fiat_secp256k1_uint1 x323; - fiat_secp256k1_addcarryx_u32(&x322, &x323, 0x0, x306, x270); + fiat_secp256k1_addcarryx_u32(&x322, &x323, x321, x306, x274); uint32_t x324; fiat_secp256k1_uint1 x325; - fiat_secp256k1_addcarryx_u32(&x324, &x325, x323, x308, x272); + fiat_secp256k1_addcarryx_u32(&x324, &x325, x323, x308, x276); uint32_t x326; fiat_secp256k1_uint1 x327; - fiat_secp256k1_addcarryx_u32(&x326, &x327, x325, x310, x274); + fiat_secp256k1_addcarryx_u32(&x326, &x327, x325, x310, x278); uint32_t x328; fiat_secp256k1_uint1 x329; - fiat_secp256k1_addcarryx_u32(&x328, &x329, x327, x312, x276); + fiat_secp256k1_addcarryx_u32(&x328, &x329, x327, x312, x280); uint32_t x330; fiat_secp256k1_uint1 x331; - fiat_secp256k1_addcarryx_u32(&x330, &x331, x329, x314, x278); + fiat_secp256k1_addcarryx_u32(&x330, &x331, x329, x314, x282); uint32_t x332; fiat_secp256k1_uint1 x333; - fiat_secp256k1_addcarryx_u32(&x332, &x333, x331, x316, x280); + fiat_secp256k1_addcarryx_u32(&x332, &x333, x331, x316, x284); uint32_t x334; fiat_secp256k1_uint1 x335; - fiat_secp256k1_addcarryx_u32(&x334, &x335, x333, x318, x282); + fiat_secp256k1_addcarryx_u32(&x334, &x335, x269, 0x0, 0x0); uint32_t x336; fiat_secp256k1_uint1 x337; - fiat_secp256k1_addcarryx_u32(&x336, &x337, x335, x320, x284); + fiat_secp256k1_addcarryx_u32(&x336, &x337, x285, 0x0, (fiat_secp256k1_uint1)x334); uint32_t x338; fiat_secp256k1_uint1 x339; - fiat_secp256k1_addcarryx_u32(&x338, &x339, x321, 0x0, x293); + fiat_secp256k1_addcarryx_u32(&x338, &x339, x317, 0x0, x289); uint32_t x340; fiat_secp256k1_uint1 x341; - fiat_secp256k1_addcarryx_u32(&x340, &x341, x337, x338, x288); + fiat_secp256k1_addcarryx_u32(&x340, &x341, x333, x338, x336); uint32_t x342; fiat_secp256k1_uint1 x343; - fiat_secp256k1_addcarryx_u32(&x342, &x343, 0x0, (arg1[5]), x324); + fiat_secp256k1_addcarryx_u32(&x342, &x343, 0x0, (arg1[5]), x320); uint32_t x344; fiat_secp256k1_uint1 x345; - fiat_secp256k1_addcarryx_u32(&x344, &x345, x343, 0x0, x326); + fiat_secp256k1_addcarryx_u32(&x344, &x345, x343, 0x0, x322); uint32_t x346; fiat_secp256k1_uint1 x347; - fiat_secp256k1_addcarryx_u32(&x346, &x347, x345, 0x0, x328); + fiat_secp256k1_addcarryx_u32(&x346, &x347, x345, 0x0, x324); uint32_t x348; fiat_secp256k1_uint1 x349; - fiat_secp256k1_addcarryx_u32(&x348, &x349, x347, 0x0, x330); + fiat_secp256k1_addcarryx_u32(&x348, &x349, x347, 0x0, x326); uint32_t x350; fiat_secp256k1_uint1 x351; - fiat_secp256k1_addcarryx_u32(&x350, &x351, x349, 0x0, x332); + fiat_secp256k1_addcarryx_u32(&x350, &x351, x349, 0x0, x328); uint32_t x352; fiat_secp256k1_uint1 x353; - fiat_secp256k1_addcarryx_u32(&x352, &x353, x351, 0x0, x334); + fiat_secp256k1_addcarryx_u32(&x352, &x353, x351, 0x0, x330); uint32_t x354; fiat_secp256k1_uint1 x355; - fiat_secp256k1_addcarryx_u32(&x354, &x355, x353, 0x0, x336); + fiat_secp256k1_addcarryx_u32(&x354, &x355, x353, 0x0, x332); uint32_t x356; fiat_secp256k1_uint1 x357; fiat_secp256k1_addcarryx_u32(&x356, &x357, x355, 0x0, x340); uint32_t x358; - fiat_secp256k1_uint1 x359; - fiat_secp256k1_addcarryx_u32(&x358, &x359, x341, 0x0, x289); + uint32_t x359; + fiat_secp256k1_mulx_u32(&x358, &x359, x342, UINT32_C(0xd2253531)); uint32_t x360; - fiat_secp256k1_uint1 x361; - fiat_secp256k1_addcarryx_u32(&x360, &x361, x357, 0x0, (fiat_secp256k1_uint1)x358); + uint32_t x361; + fiat_secp256k1_mulx_u32(&x360, &x361, x358, UINT32_C(0xffffffff)); uint32_t x362; uint32_t x363; - fiat_secp256k1_mulx_u32(&x362, &x363, x342, UINT32_C(0xd2253531)); + fiat_secp256k1_mulx_u32(&x362, &x363, x358, UINT32_C(0xffffffff)); uint32_t x364; uint32_t x365; - fiat_secp256k1_mulx_u32(&x364, &x365, x362, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x364, &x365, x358, UINT32_C(0xffffffff)); uint32_t x366; uint32_t x367; - fiat_secp256k1_mulx_u32(&x366, &x367, x362, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x366, &x367, x358, UINT32_C(0xffffffff)); uint32_t x368; uint32_t x369; - fiat_secp256k1_mulx_u32(&x368, &x369, x362, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x368, &x369, x358, UINT32_C(0xffffffff)); uint32_t x370; uint32_t x371; - fiat_secp256k1_mulx_u32(&x370, &x371, x362, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x370, &x371, x358, UINT32_C(0xffffffff)); uint32_t x372; uint32_t x373; - fiat_secp256k1_mulx_u32(&x372, &x373, x362, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x372, &x373, x358, UINT32_C(0xfffffffe)); uint32_t x374; uint32_t x375; - fiat_secp256k1_mulx_u32(&x374, &x375, x362, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x374, &x375, x358, UINT32_C(0xfffffc2f)); uint32_t x376; - uint32_t x377; - fiat_secp256k1_mulx_u32(&x376, &x377, x362, UINT32_C(0xfffffffe)); + fiat_secp256k1_uint1 x377; + fiat_secp256k1_addcarryx_u32(&x376, &x377, 0x0, x372, x375); uint32_t x378; - uint32_t x379; - fiat_secp256k1_mulx_u32(&x378, &x379, x362, UINT32_C(0xfffffc2f)); + fiat_secp256k1_uint1 x379; + fiat_secp256k1_addcarryx_u32(&x378, &x379, x377, x370, x373); uint32_t x380; fiat_secp256k1_uint1 x381; - fiat_secp256k1_addcarryx_u32(&x380, &x381, 0x0, x376, x379); + fiat_secp256k1_addcarryx_u32(&x380, &x381, x379, x368, x371); uint32_t x382; fiat_secp256k1_uint1 x383; - fiat_secp256k1_addcarryx_u32(&x382, &x383, x381, x374, x377); + fiat_secp256k1_addcarryx_u32(&x382, &x383, x381, x366, x369); uint32_t x384; fiat_secp256k1_uint1 x385; - fiat_secp256k1_addcarryx_u32(&x384, &x385, x383, x372, x375); + fiat_secp256k1_addcarryx_u32(&x384, &x385, x383, x364, x367); uint32_t x386; fiat_secp256k1_uint1 x387; - fiat_secp256k1_addcarryx_u32(&x386, &x387, x385, x370, x373); + fiat_secp256k1_addcarryx_u32(&x386, &x387, x385, x362, x365); uint32_t x388; fiat_secp256k1_uint1 x389; - fiat_secp256k1_addcarryx_u32(&x388, &x389, x387, x368, x371); + fiat_secp256k1_addcarryx_u32(&x388, &x389, x387, x360, x363); uint32_t x390; fiat_secp256k1_uint1 x391; - fiat_secp256k1_addcarryx_u32(&x390, &x391, x389, x366, x369); + fiat_secp256k1_addcarryx_u32(&x390, &x391, 0x0, x374, x342); uint32_t x392; fiat_secp256k1_uint1 x393; - fiat_secp256k1_addcarryx_u32(&x392, &x393, x391, x364, x367); + fiat_secp256k1_addcarryx_u32(&x392, &x393, x391, x376, x344); uint32_t x394; fiat_secp256k1_uint1 x395; - fiat_secp256k1_addcarryx_u32(&x394, &x395, 0x0, x378, x342); + fiat_secp256k1_addcarryx_u32(&x394, &x395, x393, x378, x346); uint32_t x396; fiat_secp256k1_uint1 x397; - fiat_secp256k1_addcarryx_u32(&x396, &x397, x395, x380, x344); + fiat_secp256k1_addcarryx_u32(&x396, &x397, x395, x380, x348); uint32_t x398; fiat_secp256k1_uint1 x399; - fiat_secp256k1_addcarryx_u32(&x398, &x399, x397, x382, x346); + fiat_secp256k1_addcarryx_u32(&x398, &x399, x397, x382, x350); uint32_t x400; fiat_secp256k1_uint1 x401; - fiat_secp256k1_addcarryx_u32(&x400, &x401, x399, x384, x348); + fiat_secp256k1_addcarryx_u32(&x400, &x401, x399, x384, x352); uint32_t x402; fiat_secp256k1_uint1 x403; - fiat_secp256k1_addcarryx_u32(&x402, &x403, x401, x386, x350); + fiat_secp256k1_addcarryx_u32(&x402, &x403, x401, x386, x354); uint32_t x404; fiat_secp256k1_uint1 x405; - fiat_secp256k1_addcarryx_u32(&x404, &x405, x403, x388, x352); + fiat_secp256k1_addcarryx_u32(&x404, &x405, x403, x388, x356); uint32_t x406; fiat_secp256k1_uint1 x407; - fiat_secp256k1_addcarryx_u32(&x406, &x407, x405, x390, x354); + fiat_secp256k1_addcarryx_u32(&x406, &x407, x341, 0x0, 0x0); uint32_t x408; fiat_secp256k1_uint1 x409; - fiat_secp256k1_addcarryx_u32(&x408, &x409, x407, x392, x356); + fiat_secp256k1_addcarryx_u32(&x408, &x409, x357, 0x0, (fiat_secp256k1_uint1)x406); uint32_t x410; fiat_secp256k1_uint1 x411; - fiat_secp256k1_addcarryx_u32(&x410, &x411, x393, 0x0, x365); + fiat_secp256k1_addcarryx_u32(&x410, &x411, x389, 0x0, x361); uint32_t x412; fiat_secp256k1_uint1 x413; - fiat_secp256k1_addcarryx_u32(&x412, &x413, x409, x410, x360); + fiat_secp256k1_addcarryx_u32(&x412, &x413, x405, x410, x408); uint32_t x414; fiat_secp256k1_uint1 x415; - fiat_secp256k1_addcarryx_u32(&x414, &x415, 0x0, (arg1[6]), x396); + fiat_secp256k1_addcarryx_u32(&x414, &x415, 0x0, (arg1[6]), x392); uint32_t x416; fiat_secp256k1_uint1 x417; - fiat_secp256k1_addcarryx_u32(&x416, &x417, x415, 0x0, x398); + fiat_secp256k1_addcarryx_u32(&x416, &x417, x415, 0x0, x394); uint32_t x418; fiat_secp256k1_uint1 x419; - fiat_secp256k1_addcarryx_u32(&x418, &x419, x417, 0x0, x400); + fiat_secp256k1_addcarryx_u32(&x418, &x419, x417, 0x0, x396); uint32_t x420; fiat_secp256k1_uint1 x421; - fiat_secp256k1_addcarryx_u32(&x420, &x421, x419, 0x0, x402); + fiat_secp256k1_addcarryx_u32(&x420, &x421, x419, 0x0, x398); uint32_t x422; fiat_secp256k1_uint1 x423; - fiat_secp256k1_addcarryx_u32(&x422, &x423, x421, 0x0, x404); + fiat_secp256k1_addcarryx_u32(&x422, &x423, x421, 0x0, x400); uint32_t x424; fiat_secp256k1_uint1 x425; - fiat_secp256k1_addcarryx_u32(&x424, &x425, x423, 0x0, x406); + fiat_secp256k1_addcarryx_u32(&x424, &x425, x423, 0x0, x402); uint32_t x426; fiat_secp256k1_uint1 x427; - fiat_secp256k1_addcarryx_u32(&x426, &x427, x425, 0x0, x408); + fiat_secp256k1_addcarryx_u32(&x426, &x427, x425, 0x0, x404); uint32_t x428; fiat_secp256k1_uint1 x429; fiat_secp256k1_addcarryx_u32(&x428, &x429, x427, 0x0, x412); uint32_t x430; - fiat_secp256k1_uint1 x431; - fiat_secp256k1_addcarryx_u32(&x430, &x431, x413, 0x0, x361); + uint32_t x431; + fiat_secp256k1_mulx_u32(&x430, &x431, x414, UINT32_C(0xd2253531)); uint32_t x432; - fiat_secp256k1_uint1 x433; - fiat_secp256k1_addcarryx_u32(&x432, &x433, x429, 0x0, (fiat_secp256k1_uint1)x430); + uint32_t x433; + fiat_secp256k1_mulx_u32(&x432, &x433, x430, UINT32_C(0xffffffff)); uint32_t x434; uint32_t x435; - fiat_secp256k1_mulx_u32(&x434, &x435, x414, UINT32_C(0xd2253531)); + fiat_secp256k1_mulx_u32(&x434, &x435, x430, UINT32_C(0xffffffff)); uint32_t x436; uint32_t x437; - fiat_secp256k1_mulx_u32(&x436, &x437, x434, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x436, &x437, x430, UINT32_C(0xffffffff)); uint32_t x438; uint32_t x439; - fiat_secp256k1_mulx_u32(&x438, &x439, x434, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x438, &x439, x430, UINT32_C(0xffffffff)); uint32_t x440; uint32_t x441; - fiat_secp256k1_mulx_u32(&x440, &x441, x434, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x440, &x441, x430, UINT32_C(0xffffffff)); uint32_t x442; uint32_t x443; - fiat_secp256k1_mulx_u32(&x442, &x443, x434, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x442, &x443, x430, UINT32_C(0xffffffff)); uint32_t x444; uint32_t x445; - fiat_secp256k1_mulx_u32(&x444, &x445, x434, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x444, &x445, x430, UINT32_C(0xfffffffe)); uint32_t x446; uint32_t x447; - fiat_secp256k1_mulx_u32(&x446, &x447, x434, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x446, &x447, x430, UINT32_C(0xfffffc2f)); uint32_t x448; - uint32_t x449; - fiat_secp256k1_mulx_u32(&x448, &x449, x434, UINT32_C(0xfffffffe)); + fiat_secp256k1_uint1 x449; + fiat_secp256k1_addcarryx_u32(&x448, &x449, 0x0, x444, x447); uint32_t x450; - uint32_t x451; - fiat_secp256k1_mulx_u32(&x450, &x451, x434, UINT32_C(0xfffffc2f)); + fiat_secp256k1_uint1 x451; + fiat_secp256k1_addcarryx_u32(&x450, &x451, x449, x442, x445); uint32_t x452; fiat_secp256k1_uint1 x453; - fiat_secp256k1_addcarryx_u32(&x452, &x453, 0x0, x448, x451); + fiat_secp256k1_addcarryx_u32(&x452, &x453, x451, x440, x443); uint32_t x454; fiat_secp256k1_uint1 x455; - fiat_secp256k1_addcarryx_u32(&x454, &x455, x453, x446, x449); + fiat_secp256k1_addcarryx_u32(&x454, &x455, x453, x438, x441); uint32_t x456; fiat_secp256k1_uint1 x457; - fiat_secp256k1_addcarryx_u32(&x456, &x457, x455, x444, x447); + fiat_secp256k1_addcarryx_u32(&x456, &x457, x455, x436, x439); uint32_t x458; fiat_secp256k1_uint1 x459; - fiat_secp256k1_addcarryx_u32(&x458, &x459, x457, x442, x445); + fiat_secp256k1_addcarryx_u32(&x458, &x459, x457, x434, x437); uint32_t x460; fiat_secp256k1_uint1 x461; - fiat_secp256k1_addcarryx_u32(&x460, &x461, x459, x440, x443); + fiat_secp256k1_addcarryx_u32(&x460, &x461, x459, x432, x435); uint32_t x462; fiat_secp256k1_uint1 x463; - fiat_secp256k1_addcarryx_u32(&x462, &x463, x461, x438, x441); + fiat_secp256k1_addcarryx_u32(&x462, &x463, 0x0, x446, x414); uint32_t x464; fiat_secp256k1_uint1 x465; - fiat_secp256k1_addcarryx_u32(&x464, &x465, x463, x436, x439); + fiat_secp256k1_addcarryx_u32(&x464, &x465, x463, x448, x416); uint32_t x466; fiat_secp256k1_uint1 x467; - fiat_secp256k1_addcarryx_u32(&x466, &x467, 0x0, x450, x414); + fiat_secp256k1_addcarryx_u32(&x466, &x467, x465, x450, x418); uint32_t x468; fiat_secp256k1_uint1 x469; - fiat_secp256k1_addcarryx_u32(&x468, &x469, x467, x452, x416); + fiat_secp256k1_addcarryx_u32(&x468, &x469, x467, x452, x420); uint32_t x470; fiat_secp256k1_uint1 x471; - fiat_secp256k1_addcarryx_u32(&x470, &x471, x469, x454, x418); + fiat_secp256k1_addcarryx_u32(&x470, &x471, x469, x454, x422); uint32_t x472; fiat_secp256k1_uint1 x473; - fiat_secp256k1_addcarryx_u32(&x472, &x473, x471, x456, x420); + fiat_secp256k1_addcarryx_u32(&x472, &x473, x471, x456, x424); uint32_t x474; fiat_secp256k1_uint1 x475; - fiat_secp256k1_addcarryx_u32(&x474, &x475, x473, x458, x422); + fiat_secp256k1_addcarryx_u32(&x474, &x475, x473, x458, x426); uint32_t x476; fiat_secp256k1_uint1 x477; - fiat_secp256k1_addcarryx_u32(&x476, &x477, x475, x460, x424); + fiat_secp256k1_addcarryx_u32(&x476, &x477, x475, x460, x428); uint32_t x478; fiat_secp256k1_uint1 x479; - fiat_secp256k1_addcarryx_u32(&x478, &x479, x477, x462, x426); + fiat_secp256k1_addcarryx_u32(&x478, &x479, x413, 0x0, 0x0); uint32_t x480; fiat_secp256k1_uint1 x481; - fiat_secp256k1_addcarryx_u32(&x480, &x481, x479, x464, x428); + fiat_secp256k1_addcarryx_u32(&x480, &x481, x429, 0x0, (fiat_secp256k1_uint1)x478); uint32_t x482; fiat_secp256k1_uint1 x483; - fiat_secp256k1_addcarryx_u32(&x482, &x483, x465, 0x0, x437); + fiat_secp256k1_addcarryx_u32(&x482, &x483, x461, 0x0, x433); uint32_t x484; fiat_secp256k1_uint1 x485; - fiat_secp256k1_addcarryx_u32(&x484, &x485, x481, x482, x432); + fiat_secp256k1_addcarryx_u32(&x484, &x485, x477, x482, x480); uint32_t x486; fiat_secp256k1_uint1 x487; - fiat_secp256k1_addcarryx_u32(&x486, &x487, 0x0, (arg1[7]), x468); + fiat_secp256k1_addcarryx_u32(&x486, &x487, 0x0, (arg1[7]), x464); uint32_t x488; fiat_secp256k1_uint1 x489; - fiat_secp256k1_addcarryx_u32(&x488, &x489, x487, 0x0, x470); + fiat_secp256k1_addcarryx_u32(&x488, &x489, x487, 0x0, x466); uint32_t x490; fiat_secp256k1_uint1 x491; - fiat_secp256k1_addcarryx_u32(&x490, &x491, x489, 0x0, x472); + fiat_secp256k1_addcarryx_u32(&x490, &x491, x489, 0x0, x468); uint32_t x492; fiat_secp256k1_uint1 x493; - fiat_secp256k1_addcarryx_u32(&x492, &x493, x491, 0x0, x474); + fiat_secp256k1_addcarryx_u32(&x492, &x493, x491, 0x0, x470); uint32_t x494; fiat_secp256k1_uint1 x495; - fiat_secp256k1_addcarryx_u32(&x494, &x495, x493, 0x0, x476); + fiat_secp256k1_addcarryx_u32(&x494, &x495, x493, 0x0, x472); uint32_t x496; fiat_secp256k1_uint1 x497; - fiat_secp256k1_addcarryx_u32(&x496, &x497, x495, 0x0, x478); + fiat_secp256k1_addcarryx_u32(&x496, &x497, x495, 0x0, x474); uint32_t x498; fiat_secp256k1_uint1 x499; - fiat_secp256k1_addcarryx_u32(&x498, &x499, x497, 0x0, x480); + fiat_secp256k1_addcarryx_u32(&x498, &x499, x497, 0x0, x476); uint32_t x500; fiat_secp256k1_uint1 x501; fiat_secp256k1_addcarryx_u32(&x500, &x501, x499, 0x0, x484); uint32_t x502; - fiat_secp256k1_uint1 x503; - fiat_secp256k1_addcarryx_u32(&x502, &x503, x485, 0x0, x433); + uint32_t x503; + fiat_secp256k1_mulx_u32(&x502, &x503, x486, UINT32_C(0xd2253531)); uint32_t x504; - fiat_secp256k1_uint1 x505; - fiat_secp256k1_addcarryx_u32(&x504, &x505, x501, 0x0, (fiat_secp256k1_uint1)x502); + uint32_t x505; + fiat_secp256k1_mulx_u32(&x504, &x505, x502, UINT32_C(0xffffffff)); uint32_t x506; uint32_t x507; - fiat_secp256k1_mulx_u32(&x506, &x507, x486, UINT32_C(0xd2253531)); + fiat_secp256k1_mulx_u32(&x506, &x507, x502, UINT32_C(0xffffffff)); uint32_t x508; uint32_t x509; - fiat_secp256k1_mulx_u32(&x508, &x509, x506, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x508, &x509, x502, UINT32_C(0xffffffff)); uint32_t x510; uint32_t x511; - fiat_secp256k1_mulx_u32(&x510, &x511, x506, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x510, &x511, x502, UINT32_C(0xffffffff)); uint32_t x512; uint32_t x513; - fiat_secp256k1_mulx_u32(&x512, &x513, x506, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x512, &x513, x502, UINT32_C(0xffffffff)); uint32_t x514; uint32_t x515; - fiat_secp256k1_mulx_u32(&x514, &x515, x506, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x514, &x515, x502, UINT32_C(0xffffffff)); uint32_t x516; uint32_t x517; - fiat_secp256k1_mulx_u32(&x516, &x517, x506, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x516, &x517, x502, UINT32_C(0xfffffffe)); uint32_t x518; uint32_t x519; - fiat_secp256k1_mulx_u32(&x518, &x519, x506, UINT32_C(0xffffffff)); + fiat_secp256k1_mulx_u32(&x518, &x519, x502, UINT32_C(0xfffffc2f)); uint32_t x520; - uint32_t x521; - fiat_secp256k1_mulx_u32(&x520, &x521, x506, UINT32_C(0xfffffffe)); + fiat_secp256k1_uint1 x521; + fiat_secp256k1_addcarryx_u32(&x520, &x521, 0x0, x516, x519); uint32_t x522; - uint32_t x523; - fiat_secp256k1_mulx_u32(&x522, &x523, x506, UINT32_C(0xfffffc2f)); + fiat_secp256k1_uint1 x523; + fiat_secp256k1_addcarryx_u32(&x522, &x523, x521, x514, x517); uint32_t x524; fiat_secp256k1_uint1 x525; - fiat_secp256k1_addcarryx_u32(&x524, &x525, 0x0, x520, x523); + fiat_secp256k1_addcarryx_u32(&x524, &x525, x523, x512, x515); uint32_t x526; fiat_secp256k1_uint1 x527; - fiat_secp256k1_addcarryx_u32(&x526, &x527, x525, x518, x521); + fiat_secp256k1_addcarryx_u32(&x526, &x527, x525, x510, x513); uint32_t x528; fiat_secp256k1_uint1 x529; - fiat_secp256k1_addcarryx_u32(&x528, &x529, x527, x516, x519); + fiat_secp256k1_addcarryx_u32(&x528, &x529, x527, x508, x511); uint32_t x530; fiat_secp256k1_uint1 x531; - fiat_secp256k1_addcarryx_u32(&x530, &x531, x529, x514, x517); + fiat_secp256k1_addcarryx_u32(&x530, &x531, x529, x506, x509); uint32_t x532; fiat_secp256k1_uint1 x533; - fiat_secp256k1_addcarryx_u32(&x532, &x533, x531, x512, x515); + fiat_secp256k1_addcarryx_u32(&x532, &x533, x531, x504, x507); uint32_t x534; fiat_secp256k1_uint1 x535; - fiat_secp256k1_addcarryx_u32(&x534, &x535, x533, x510, x513); + fiat_secp256k1_addcarryx_u32(&x534, &x535, 0x0, x518, x486); uint32_t x536; fiat_secp256k1_uint1 x537; - fiat_secp256k1_addcarryx_u32(&x536, &x537, x535, x508, x511); + fiat_secp256k1_addcarryx_u32(&x536, &x537, x535, x520, x488); uint32_t x538; fiat_secp256k1_uint1 x539; - fiat_secp256k1_addcarryx_u32(&x538, &x539, 0x0, x522, x486); + fiat_secp256k1_addcarryx_u32(&x538, &x539, x537, x522, x490); uint32_t x540; fiat_secp256k1_uint1 x541; - fiat_secp256k1_addcarryx_u32(&x540, &x541, x539, x524, x488); + fiat_secp256k1_addcarryx_u32(&x540, &x541, x539, x524, x492); uint32_t x542; fiat_secp256k1_uint1 x543; - fiat_secp256k1_addcarryx_u32(&x542, &x543, x541, x526, x490); + fiat_secp256k1_addcarryx_u32(&x542, &x543, x541, x526, x494); uint32_t x544; fiat_secp256k1_uint1 x545; - fiat_secp256k1_addcarryx_u32(&x544, &x545, x543, x528, x492); + fiat_secp256k1_addcarryx_u32(&x544, &x545, x543, x528, x496); uint32_t x546; fiat_secp256k1_uint1 x547; - fiat_secp256k1_addcarryx_u32(&x546, &x547, x545, x530, x494); + fiat_secp256k1_addcarryx_u32(&x546, &x547, x545, x530, x498); uint32_t x548; fiat_secp256k1_uint1 x549; - fiat_secp256k1_addcarryx_u32(&x548, &x549, x547, x532, x496); + fiat_secp256k1_addcarryx_u32(&x548, &x549, x547, x532, x500); uint32_t x550; fiat_secp256k1_uint1 x551; - fiat_secp256k1_addcarryx_u32(&x550, &x551, x549, x534, x498); + fiat_secp256k1_addcarryx_u32(&x550, &x551, x485, 0x0, 0x0); uint32_t x552; fiat_secp256k1_uint1 x553; - fiat_secp256k1_addcarryx_u32(&x552, &x553, x551, x536, x500); + fiat_secp256k1_addcarryx_u32(&x552, &x553, x501, 0x0, (fiat_secp256k1_uint1)x550); uint32_t x554; fiat_secp256k1_uint1 x555; - fiat_secp256k1_addcarryx_u32(&x554, &x555, x537, 0x0, x509); + fiat_secp256k1_addcarryx_u32(&x554, &x555, x533, 0x0, x505); uint32_t x556; fiat_secp256k1_uint1 x557; - fiat_secp256k1_addcarryx_u32(&x556, &x557, x553, x554, x504); + fiat_secp256k1_addcarryx_u32(&x556, &x557, x549, x554, x552); uint32_t x558; fiat_secp256k1_uint1 x559; - fiat_secp256k1_subborrowx_u32(&x558, &x559, 0x0, x540, UINT32_C(0xfffffc2f)); + fiat_secp256k1_subborrowx_u32(&x558, &x559, 0x0, x536, UINT32_C(0xfffffc2f)); uint32_t x560; fiat_secp256k1_uint1 x561; - fiat_secp256k1_subborrowx_u32(&x560, &x561, x559, x542, UINT32_C(0xfffffffe)); + fiat_secp256k1_subborrowx_u32(&x560, &x561, x559, x538, UINT32_C(0xfffffffe)); uint32_t x562; fiat_secp256k1_uint1 x563; - fiat_secp256k1_subborrowx_u32(&x562, &x563, x561, x544, UINT32_C(0xffffffff)); + fiat_secp256k1_subborrowx_u32(&x562, &x563, x561, x540, UINT32_C(0xffffffff)); uint32_t x564; fiat_secp256k1_uint1 x565; - fiat_secp256k1_subborrowx_u32(&x564, &x565, x563, x546, UINT32_C(0xffffffff)); + fiat_secp256k1_subborrowx_u32(&x564, &x565, x563, x542, UINT32_C(0xffffffff)); uint32_t x566; fiat_secp256k1_uint1 x567; - fiat_secp256k1_subborrowx_u32(&x566, &x567, x565, x548, UINT32_C(0xffffffff)); + fiat_secp256k1_subborrowx_u32(&x566, &x567, x565, x544, UINT32_C(0xffffffff)); uint32_t x568; fiat_secp256k1_uint1 x569; - fiat_secp256k1_subborrowx_u32(&x568, &x569, x567, x550, UINT32_C(0xffffffff)); + fiat_secp256k1_subborrowx_u32(&x568, &x569, x567, x546, UINT32_C(0xffffffff)); uint32_t x570; fiat_secp256k1_uint1 x571; - fiat_secp256k1_subborrowx_u32(&x570, &x571, x569, x552, UINT32_C(0xffffffff)); + fiat_secp256k1_subborrowx_u32(&x570, &x571, x569, x548, UINT32_C(0xffffffff)); uint32_t x572; fiat_secp256k1_uint1 x573; fiat_secp256k1_subborrowx_u32(&x572, &x573, x571, x556, UINT32_C(0xffffffff)); uint32_t x574; fiat_secp256k1_uint1 x575; - fiat_secp256k1_addcarryx_u32(&x574, &x575, x557, 0x0, x505); + fiat_secp256k1_addcarryx_u32(&x574, &x575, x557, 0x0, 0x0); uint32_t x576; fiat_secp256k1_uint1 x577; fiat_secp256k1_subborrowx_u32(&x576, &x577, x573, (fiat_secp256k1_uint1)x574, 0x0); uint32_t x578; - fiat_secp256k1_cmovznz_u32(&x578, x577, x558, x540); + fiat_secp256k1_cmovznz_u32(&x578, x577, x558, x536); uint32_t x579; - fiat_secp256k1_cmovznz_u32(&x579, x577, x560, x542); + fiat_secp256k1_cmovznz_u32(&x579, x577, x560, x538); uint32_t x580; - fiat_secp256k1_cmovznz_u32(&x580, x577, x562, x544); + fiat_secp256k1_cmovznz_u32(&x580, x577, x562, x540); uint32_t x581; - fiat_secp256k1_cmovznz_u32(&x581, x577, x564, x546); + fiat_secp256k1_cmovznz_u32(&x581, x577, x564, x542); uint32_t x582; - fiat_secp256k1_cmovznz_u32(&x582, x577, x566, x548); + fiat_secp256k1_cmovznz_u32(&x582, x577, x566, x544); uint32_t x583; - fiat_secp256k1_cmovznz_u32(&x583, x577, x568, x550); + fiat_secp256k1_cmovznz_u32(&x583, x577, x568, x546); uint32_t x584; - fiat_secp256k1_cmovznz_u32(&x584, x577, x570, x552); + fiat_secp256k1_cmovznz_u32(&x584, x577, x570, x548); uint32_t x585; fiat_secp256k1_cmovznz_u32(&x585, x577, x572, x556); out1[0] = x578; @@ -3845,101 +3845,94 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff)); uint8_t x13 = (uint8_t)(x11 >> 8); uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); - fiat_secp256k1_uint1 x15 = (fiat_secp256k1_uint1)(x13 >> 8); - uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff)); - uint32_t x17 = (x15 + x7); - uint32_t x18 = (x17 >> 8); - uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); - uint32_t x20 = (x18 >> 8); - uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); - uint8_t x22 = (uint8_t)(x20 >> 8); - uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); - fiat_secp256k1_uint1 x24 = (fiat_secp256k1_uint1)(x22 >> 8); - uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); - uint32_t x26 = (x24 + x6); - uint32_t x27 = (x26 >> 8); - uint8_t x28 = (uint8_t)(x26 & UINT8_C(0xff)); - uint32_t x29 = (x27 >> 8); + uint8_t x15 = (uint8_t)(x13 & UINT8_C(0xff)); + uint32_t x16 = (0x0 + x7); + uint32_t x17 = (x16 >> 8); + uint8_t x18 = (uint8_t)(x16 & UINT8_C(0xff)); + uint32_t x19 = (x17 >> 8); + uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); + uint8_t x21 = (uint8_t)(x19 >> 8); + uint8_t x22 = (uint8_t)(x19 & UINT8_C(0xff)); + uint8_t x23 = (uint8_t)(x21 & UINT8_C(0xff)); + uint32_t x24 = (0x0 + x6); + uint32_t x25 = (x24 >> 8); + uint8_t x26 = (uint8_t)(x24 & UINT8_C(0xff)); + uint32_t x27 = (x25 >> 8); + uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); + uint8_t x29 = (uint8_t)(x27 >> 8); uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); - uint8_t x31 = (uint8_t)(x29 >> 8); - uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); - fiat_secp256k1_uint1 x33 = (fiat_secp256k1_uint1)(x31 >> 8); - uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); - uint32_t x35 = (x33 + x5); - uint32_t x36 = (x35 >> 8); - uint8_t x37 = (uint8_t)(x35 & UINT8_C(0xff)); - uint32_t x38 = (x36 >> 8); - uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff)); - uint8_t x40 = (uint8_t)(x38 >> 8); - uint8_t x41 = (uint8_t)(x38 & UINT8_C(0xff)); - fiat_secp256k1_uint1 x42 = (fiat_secp256k1_uint1)(x40 >> 8); - uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff)); - uint32_t x44 = (x42 + x4); - 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)); - fiat_secp256k1_uint1 x51 = (fiat_secp256k1_uint1)(x49 >> 8); + uint8_t x31 = (uint8_t)(x29 & UINT8_C(0xff)); + uint32_t x32 = (0x0 + x5); + uint32_t x33 = (x32 >> 8); + uint8_t x34 = (uint8_t)(x32 & UINT8_C(0xff)); + uint32_t x35 = (x33 >> 8); + uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff)); + uint8_t x37 = (uint8_t)(x35 >> 8); + uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); + uint8_t x39 = (uint8_t)(x37 & UINT8_C(0xff)); + uint32_t x40 = (0x0 + x4); + uint32_t x41 = (x40 >> 8); + uint8_t x42 = (uint8_t)(x40 & UINT8_C(0xff)); + uint32_t x43 = (x41 >> 8); + uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); + uint8_t x45 = (uint8_t)(x43 >> 8); + uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); + uint8_t x47 = (uint8_t)(x45 & UINT8_C(0xff)); + uint32_t x48 = (0x0 + x3); + 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)); - uint32_t x53 = (x51 + x3); - uint32_t x54 = (x53 >> 8); + uint8_t x53 = (uint8_t)(x51 >> 8); + uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff)); uint8_t x55 = (uint8_t)(x53 & UINT8_C(0xff)); - uint32_t x56 = (x54 >> 8); - uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); - uint8_t x58 = (uint8_t)(x56 >> 8); - uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); - fiat_secp256k1_uint1 x60 = (fiat_secp256k1_uint1)(x58 >> 8); - uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); - uint32_t x62 = (x60 + x2); - uint32_t x63 = (x62 >> 8); - uint8_t x64 = (uint8_t)(x62 & UINT8_C(0xff)); - uint32_t x65 = (x63 >> 8); - uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); - uint8_t x67 = (uint8_t)(x65 >> 8); + uint32_t x56 = (0x0 + x2); + uint32_t x57 = (x56 >> 8); + uint8_t x58 = (uint8_t)(x56 & UINT8_C(0xff)); + uint32_t x59 = (x57 >> 8); + uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); + uint8_t x61 = (uint8_t)(x59 >> 8); + uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); + uint8_t x63 = (uint8_t)(x61 & UINT8_C(0xff)); + uint32_t x64 = (0x0 + x1); + uint32_t x65 = (x64 >> 8); + uint8_t x66 = (uint8_t)(x64 & UINT8_C(0xff)); + uint32_t x67 = (x65 >> 8); uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff)); - fiat_secp256k1_uint1 x69 = (fiat_secp256k1_uint1)(x67 >> 8); + uint8_t x69 = (uint8_t)(x67 >> 8); uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); - uint32_t x71 = (x69 + x1); - uint32_t x72 = (x71 >> 8); - uint8_t x73 = (uint8_t)(x71 & UINT8_C(0xff)); - uint32_t x74 = (x72 >> 8); - uint8_t x75 = (uint8_t)(x72 & UINT8_C(0xff)); - uint8_t x76 = (uint8_t)(x74 >> 8); - uint8_t x77 = (uint8_t)(x74 & UINT8_C(0xff)); out1[0] = x10; out1[1] = x12; out1[2] = x14; - out1[3] = x16; - out1[4] = x19; - out1[5] = x21; - out1[6] = x23; - out1[7] = x25; - out1[8] = x28; - out1[9] = x30; - out1[10] = x32; - out1[11] = x34; - out1[12] = x37; - out1[13] = x39; - out1[14] = x41; - out1[15] = x43; - out1[16] = x46; - out1[17] = x48; - out1[18] = x50; - out1[19] = x52; - out1[20] = x55; - out1[21] = x57; - out1[22] = x59; - out1[23] = x61; - out1[24] = x64; - out1[25] = x66; - out1[26] = x68; - out1[27] = x70; - out1[28] = x73; - out1[29] = x75; - out1[30] = x77; - out1[31] = x76; + out1[3] = x15; + out1[4] = x18; + out1[5] = x20; + out1[6] = x22; + out1[7] = x23; + out1[8] = x26; + out1[9] = x28; + out1[10] = x30; + out1[11] = x31; + out1[12] = x34; + out1[13] = x36; + out1[14] = x38; + out1[15] = x39; + out1[16] = x42; + out1[17] = x44; + out1[18] = x46; + out1[19] = x47; + out1[20] = x50; + out1[21] = x52; + out1[22] = x54; + out1[23] = x55; + out1[24] = x58; + out1[25] = x60; + out1[26] = x62; + out1[27] = x63; + out1[28] = x66; + out1[29] = x68; + out1[30] = x70; + out1[31] = x69; } /* @@ -3982,41 +3975,34 @@ static void fiat_secp256k1_from_bytes(uint32_t out1[8], const uint8_t arg1[32]) uint32_t x31 = ((uint32_t)(arg1[1]) << 8); uint8_t x32 = (arg1[0]); uint32_t x33 = (x32 + (x31 + (x30 + x29))); - fiat_secp256k1_uint1 x34 = (fiat_secp256k1_uint1)((uint64_t)x33 >> 32); - uint32_t x35 = (x33 & UINT32_C(0xffffffff)); - uint32_t x36 = (x4 + (x3 + (x2 + x1))); - uint32_t x37 = (x8 + (x7 + (x6 + x5))); - uint32_t x38 = (x12 + (x11 + (x10 + x9))); - uint32_t x39 = (x16 + (x15 + (x14 + x13))); - uint32_t x40 = (x20 + (x19 + (x18 + x17))); - uint32_t x41 = (x24 + (x23 + (x22 + x21))); - uint32_t x42 = (x28 + (x27 + (x26 + x25))); - uint32_t x43 = (x34 + x42); - fiat_secp256k1_uint1 x44 = (fiat_secp256k1_uint1)((uint64_t)x43 >> 32); - uint32_t x45 = (x43 & UINT32_C(0xffffffff)); - uint32_t x46 = (x44 + x41); - fiat_secp256k1_uint1 x47 = (fiat_secp256k1_uint1)((uint64_t)x46 >> 32); - uint32_t x48 = (x46 & UINT32_C(0xffffffff)); - uint32_t x49 = (x47 + x40); - fiat_secp256k1_uint1 x50 = (fiat_secp256k1_uint1)((uint64_t)x49 >> 32); - uint32_t x51 = (x49 & UINT32_C(0xffffffff)); - uint32_t x52 = (x50 + x39); - fiat_secp256k1_uint1 x53 = (fiat_secp256k1_uint1)((uint64_t)x52 >> 32); - uint32_t x54 = (x52 & UINT32_C(0xffffffff)); - uint32_t x55 = (x53 + x38); - fiat_secp256k1_uint1 x56 = (fiat_secp256k1_uint1)((uint64_t)x55 >> 32); - uint32_t x57 = (x55 & UINT32_C(0xffffffff)); - uint32_t x58 = (x56 + x37); - fiat_secp256k1_uint1 x59 = (fiat_secp256k1_uint1)((uint64_t)x58 >> 32); - uint32_t x60 = (x58 & UINT32_C(0xffffffff)); - uint32_t x61 = (x59 + x36); - out1[0] = x35; - out1[1] = x45; - out1[2] = x48; - out1[3] = x51; - out1[4] = x54; - out1[5] = x57; - out1[6] = x60; - out1[7] = x61; + uint32_t x34 = (x33 & UINT32_C(0xffffffff)); + uint32_t x35 = (x4 + (x3 + (x2 + x1))); + uint32_t x36 = (x8 + (x7 + (x6 + x5))); + uint32_t x37 = (x12 + (x11 + (x10 + x9))); + uint32_t x38 = (x16 + (x15 + (x14 + x13))); + uint32_t x39 = (x20 + (x19 + (x18 + x17))); + uint32_t x40 = (x24 + (x23 + (x22 + x21))); + uint32_t x41 = (x28 + (x27 + (x26 + x25))); + uint32_t x42 = (0x0 + x41); + uint32_t x43 = (x42 & UINT32_C(0xffffffff)); + uint32_t x44 = (0x0 + x40); + uint32_t x45 = (x44 & UINT32_C(0xffffffff)); + uint32_t x46 = (0x0 + x39); + uint32_t x47 = (x46 & UINT32_C(0xffffffff)); + uint32_t x48 = (0x0 + x38); + uint32_t x49 = (x48 & UINT32_C(0xffffffff)); + uint32_t x50 = (0x0 + x37); + uint32_t x51 = (x50 & UINT32_C(0xffffffff)); + uint32_t x52 = (0x0 + x36); + uint32_t x53 = (x52 & UINT32_C(0xffffffff)); + uint32_t x54 = (0x0 + x35); + out1[0] = x34; + out1[1] = x43; + out1[2] = x45; + out1[3] = x47; + out1[4] = x49; + out1[5] = x51; + out1[6] = x53; + out1[7] = x54; } |