diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-25 16:19:49 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-26 18:12:06 -0500 |
| commit | 90c59282be5ba1f2cd7c2561d17f0559c140c597 (patch) | |
| tree | 2aa4a1b468c3a848ffb44a46e2b6c5b3cc1630fc /p448_solinas_64.c | |
| parent | 299aec51224743bea006460af8edc37525a48baa (diff) | |
Reduce more in mulmod and squaremod
After some debugging with Andres, the issue seems to be that when we
have multiple TAPs, the first reduction will leave some of the partial
products past the end of the table, because it "folds over" the partial
products table at the location of each TAP. In the worst case, if we
have a TAP at 1 and a TAP at the second-highest limb, we will have to
reduce as many times as there are limbs. To prevent quadratic blowup,
we short-circuit the repeat_reduce calculation whenever the list of high
terms is nil. We deliberately do not support primes with a TAP in the
highest limb.
After | File Name | Before || Change | % Change
-----------------------------------------------------------------------------------------------------------
17m49.68s | Total | 17m34.83s || +0m14.84s | +1.40%
-----------------------------------------------------------------------------------------------------------
2m22.88s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m21.60s || +0m01.28s | +0.90%
2m19.62s | Arithmetic.vo | 2m17.66s || +0m01.96s | +1.42%
0m34.02s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m32.24s || +0m01.78s | +5.52%
0m32.06s | ExtractionHaskell/unsaturated_solinas | 0m30.99s || +0m01.07s | +3.45%
0m19.95s | SlowPrimeSynthesisExamples.vo | 0m18.40s || +0m01.55s | +8.42%
3m12.02s | p384_32.c | 3m12.03s || -0m00.00s | -0.00%
1m02.14s | Fancy/Montgomery256.vo | 1m02.09s || +0m00.04s | +0.08%
0m51.24s | Fancy/Barrett256.vo | 0m51.28s || -0m00.03s | -0.07%
0m45.72s | ExtractionHaskell/word_by_word_montgomery | 0m45.05s || +0m00.67s | +1.48%
0m38.67s | p521_32.c | 0m38.24s || +0m00.42s | +1.12%
0m31.94s | p521_64.c | 0m31.38s || +0m00.56s | +1.78%
0m24.85s | ExtractionHaskell/saturated_solinas | 0m24.45s || +0m00.40s | +1.63%
0m23.53s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m22.79s || +0m00.74s | +3.24%
0m21.96s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m21.88s || +0m00.08s | +0.36%
0m19.60s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.56s || +0m00.04s | +0.20%
0m17.76s | ExtractionOCaml/word_by_word_montgomery | 0m17.26s || +0m00.50s | +2.89%
0m14.90s | p448_solinas_64.c | 0m14.91s || -0m00.00s | -0.06%
0m13.55s | secp256k1_32.c | 0m13.39s || +0m00.16s | +1.19%
0m13.31s | p256_32.c | 0m13.06s || +0m00.25s | +1.91%
0m13.30s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m12.44s || +0m00.86s | +6.91%
0m11.47s | p484_64.c | 0m11.31s || +0m00.16s | +1.41%
0m11.43s | ExtractionOCaml/unsaturated_solinas | 0m11.15s || +0m00.27s | +2.51%
0m10.55s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.66s || -0m00.10s | -1.03%
0m08.42s | ExtractionOCaml/saturated_solinas | 0m08.24s || +0m00.17s | +2.18%
0m07.07s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.04s || +0m00.03s | +0.42%
0m06.66s | COperationSpecifications.vo | 0m06.31s || +0m00.35s | +5.54%
0m06.50s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.39s || +0m00.11s | +1.72%
0m06.19s | p224_32.c | 0m05.99s || +0m00.20s | +3.33%
0m05.35s | p384_64.c | 0m05.24s || +0m00.10s | +2.09%
0m05.26s | ExtractionOCaml/saturated_solinas.ml | 0m05.24s || +0m00.01s | +0.38%
0m05.24s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.17s || +0m00.07s | +1.35%
0m04.23s | ExtractionHaskell/saturated_solinas.hs | 0m04.12s || +0m00.11s | +2.66%
0m04.14s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m03.89s || +0m00.24s | +6.42%
0m03.68s | PushButtonSynthesis/Primitives.vo | 0m03.62s || +0m00.06s | +1.65%
0m03.58s | PushButtonSynthesis/SmallExamples.vo | 0m03.30s || +0m00.28s | +8.48%
0m03.49s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.25s || +0m00.24s | +7.38%
0m02.38s | curve25519_32.c | 0m02.28s || +0m00.10s | +4.38%
0m01.66s | PushButtonSynthesis/BarrettReduction.vo | 0m01.39s || +0m00.27s | +19.42%
0m01.47s | curve25519_64.c | 0m01.42s || +0m00.05s | +3.52%
0m01.34s | CLI.vo | 0m01.45s || -0m00.10s | -7.58%
0m01.32s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.30s || +0m00.02s | +1.53%
0m01.08s | secp256k1_64.c | 0m01.04s || +0m00.04s | +3.84%
0m01.07s | StandaloneOCamlMain.vo | 0m01.10s || -0m00.03s | -2.72%
0m01.04s | StandaloneHaskellMain.vo | 0m01.12s || -0m00.08s | -7.14%
0m01.04s | p224_64.c | 0m01.14s || -0m00.09s | -8.77%
0m01.00s | p256_64.c | 0m00.98s || +0m00.02s | +2.04%
Diffstat (limited to 'p448_solinas_64.c')
| -rw-r--r-- | p448_solinas_64.c | 500 |
1 files changed, 255 insertions, 245 deletions
diff --git a/p448_solinas_64.c b/p448_solinas_64.c index 37cb13e10..8604acca6 100644 --- a/p448_solinas_64.c +++ b/p448_solinas_64.c @@ -76,149 +76,155 @@ static void fiat_p448_carry_mul(uint64_t out1[8], const uint64_t arg1[8], const fiat_p448_uint128 x1 = ((fiat_p448_uint128)(arg1[7]) * (arg2[7])); fiat_p448_uint128 x2 = ((fiat_p448_uint128)(arg1[7]) * (arg2[6])); fiat_p448_uint128 x3 = ((fiat_p448_uint128)(arg1[7]) * (arg2[5])); - fiat_p448_uint128 x4 = ((fiat_p448_uint128)(arg1[7]) * (arg2[4])); - fiat_p448_uint128 x5 = ((fiat_p448_uint128)(arg1[7]) * (arg2[3])); - fiat_p448_uint128 x6 = ((fiat_p448_uint128)(arg1[7]) * (arg2[2])); - fiat_p448_uint128 x7 = ((fiat_p448_uint128)(arg1[7]) * (arg2[1])); - fiat_p448_uint128 x8 = ((fiat_p448_uint128)(arg1[6]) * (arg2[7])); - fiat_p448_uint128 x9 = ((fiat_p448_uint128)(arg1[6]) * (arg2[6])); - fiat_p448_uint128 x10 = ((fiat_p448_uint128)(arg1[6]) * (arg2[5])); - fiat_p448_uint128 x11 = ((fiat_p448_uint128)(arg1[6]) * (arg2[4])); - fiat_p448_uint128 x12 = ((fiat_p448_uint128)(arg1[6]) * (arg2[3])); - fiat_p448_uint128 x13 = ((fiat_p448_uint128)(arg1[6]) * (arg2[2])); - fiat_p448_uint128 x14 = ((fiat_p448_uint128)(arg1[5]) * (arg2[7])); - fiat_p448_uint128 x15 = ((fiat_p448_uint128)(arg1[5]) * (arg2[6])); - fiat_p448_uint128 x16 = ((fiat_p448_uint128)(arg1[5]) * (arg2[5])); - fiat_p448_uint128 x17 = ((fiat_p448_uint128)(arg1[5]) * (arg2[4])); - fiat_p448_uint128 x18 = ((fiat_p448_uint128)(arg1[5]) * (arg2[3])); - fiat_p448_uint128 x19 = ((fiat_p448_uint128)(arg1[4]) * (arg2[7])); - fiat_p448_uint128 x20 = ((fiat_p448_uint128)(arg1[4]) * (arg2[6])); - fiat_p448_uint128 x21 = ((fiat_p448_uint128)(arg1[4]) * (arg2[5])); - fiat_p448_uint128 x22 = ((fiat_p448_uint128)(arg1[4]) * (arg2[4])); - fiat_p448_uint128 x23 = ((fiat_p448_uint128)(arg1[3]) * (arg2[7])); - fiat_p448_uint128 x24 = ((fiat_p448_uint128)(arg1[3]) * (arg2[6])); - fiat_p448_uint128 x25 = ((fiat_p448_uint128)(arg1[3]) * (arg2[5])); - fiat_p448_uint128 x26 = ((fiat_p448_uint128)(arg1[2]) * (arg2[7])); - fiat_p448_uint128 x27 = ((fiat_p448_uint128)(arg1[2]) * (arg2[6])); - fiat_p448_uint128 x28 = ((fiat_p448_uint128)(arg1[1]) * (arg2[7])); - fiat_p448_uint512 x29 = ((fiat_p448_uint512)((fiat_p448_uint128)(arg1[7]) * (arg2[7])) << 168); - fiat_p448_uint256 x30 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[7]) * (arg2[6])) << 112); - fiat_p448_uint256 x31 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[7]) * (arg2[5])) << 56); - fiat_p448_uint128 x32 = ((fiat_p448_uint128)(arg1[7]) * (arg2[4])); - fiat_p448_uint128 x33 = ((fiat_p448_uint128)(arg1[7]) * (arg2[3])); - fiat_p448_uint128 x34 = ((fiat_p448_uint128)(arg1[7]) * (arg2[2])); - fiat_p448_uint128 x35 = ((fiat_p448_uint128)(arg1[7]) * (arg2[1])); - fiat_p448_uint256 x36 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[6]) * (arg2[7])) << 112); - fiat_p448_uint256 x37 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[6]) * (arg2[6])) << 56); - fiat_p448_uint128 x38 = ((fiat_p448_uint128)(arg1[6]) * (arg2[5])); - fiat_p448_uint128 x39 = ((fiat_p448_uint128)(arg1[6]) * (arg2[4])); - fiat_p448_uint128 x40 = ((fiat_p448_uint128)(arg1[6]) * (arg2[3])); - fiat_p448_uint128 x41 = ((fiat_p448_uint128)(arg1[6]) * (arg2[2])); - fiat_p448_uint256 x42 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[5]) * (arg2[7])) << 56); - fiat_p448_uint128 x43 = ((fiat_p448_uint128)(arg1[5]) * (arg2[6])); - fiat_p448_uint128 x44 = ((fiat_p448_uint128)(arg1[5]) * (arg2[5])); - fiat_p448_uint128 x45 = ((fiat_p448_uint128)(arg1[5]) * (arg2[4])); - fiat_p448_uint128 x46 = ((fiat_p448_uint128)(arg1[5]) * (arg2[3])); - fiat_p448_uint128 x47 = ((fiat_p448_uint128)(arg1[4]) * (arg2[7])); - fiat_p448_uint128 x48 = ((fiat_p448_uint128)(arg1[4]) * (arg2[6])); - fiat_p448_uint128 x49 = ((fiat_p448_uint128)(arg1[4]) * (arg2[5])); - fiat_p448_uint128 x50 = ((fiat_p448_uint128)(arg1[4]) * (arg2[4])); - fiat_p448_uint128 x51 = ((fiat_p448_uint128)(arg1[3]) * (arg2[7])); - fiat_p448_uint128 x52 = ((fiat_p448_uint128)(arg1[3]) * (arg2[6])); - fiat_p448_uint128 x53 = ((fiat_p448_uint128)(arg1[3]) * (arg2[5])); - fiat_p448_uint128 x54 = ((fiat_p448_uint128)(arg1[2]) * (arg2[7])); - fiat_p448_uint128 x55 = ((fiat_p448_uint128)(arg1[2]) * (arg2[6])); - fiat_p448_uint128 x56 = ((fiat_p448_uint128)(arg1[1]) * (arg2[7])); - fiat_p448_uint128 x57 = ((fiat_p448_uint128)(arg1[7]) * (arg2[0])); - fiat_p448_uint128 x58 = ((fiat_p448_uint128)(arg1[6]) * (arg2[1])); - fiat_p448_uint128 x59 = ((fiat_p448_uint128)(arg1[6]) * (arg2[0])); - fiat_p448_uint128 x60 = ((fiat_p448_uint128)(arg1[5]) * (arg2[2])); - fiat_p448_uint128 x61 = ((fiat_p448_uint128)(arg1[5]) * (arg2[1])); - fiat_p448_uint128 x62 = ((fiat_p448_uint128)(arg1[5]) * (arg2[0])); - fiat_p448_uint128 x63 = ((fiat_p448_uint128)(arg1[4]) * (arg2[3])); - fiat_p448_uint128 x64 = ((fiat_p448_uint128)(arg1[4]) * (arg2[2])); - fiat_p448_uint128 x65 = ((fiat_p448_uint128)(arg1[4]) * (arg2[1])); - fiat_p448_uint128 x66 = ((fiat_p448_uint128)(arg1[4]) * (arg2[0])); - fiat_p448_uint128 x67 = ((fiat_p448_uint128)(arg1[3]) * (arg2[4])); - fiat_p448_uint128 x68 = ((fiat_p448_uint128)(arg1[3]) * (arg2[3])); - fiat_p448_uint128 x69 = ((fiat_p448_uint128)(arg1[3]) * (arg2[2])); - fiat_p448_uint128 x70 = ((fiat_p448_uint128)(arg1[3]) * (arg2[1])); - fiat_p448_uint128 x71 = ((fiat_p448_uint128)(arg1[3]) * (arg2[0])); - fiat_p448_uint128 x72 = ((fiat_p448_uint128)(arg1[2]) * (arg2[5])); - fiat_p448_uint128 x73 = ((fiat_p448_uint128)(arg1[2]) * (arg2[4])); - fiat_p448_uint128 x74 = ((fiat_p448_uint128)(arg1[2]) * (arg2[3])); - fiat_p448_uint128 x75 = ((fiat_p448_uint128)(arg1[2]) * (arg2[2])); - fiat_p448_uint128 x76 = ((fiat_p448_uint128)(arg1[2]) * (arg2[1])); - fiat_p448_uint128 x77 = ((fiat_p448_uint128)(arg1[2]) * (arg2[0])); - fiat_p448_uint128 x78 = ((fiat_p448_uint128)(arg1[1]) * (arg2[6])); - fiat_p448_uint128 x79 = ((fiat_p448_uint128)(arg1[1]) * (arg2[5])); - fiat_p448_uint128 x80 = ((fiat_p448_uint128)(arg1[1]) * (arg2[4])); - fiat_p448_uint128 x81 = ((fiat_p448_uint128)(arg1[1]) * (arg2[3])); - fiat_p448_uint128 x82 = ((fiat_p448_uint128)(arg1[1]) * (arg2[2])); - fiat_p448_uint128 x83 = ((fiat_p448_uint128)(arg1[1]) * (arg2[1])); - fiat_p448_uint128 x84 = ((fiat_p448_uint128)(arg1[1]) * (arg2[0])); - fiat_p448_uint128 x85 = ((fiat_p448_uint128)(arg1[0]) * (arg2[7])); - fiat_p448_uint128 x86 = ((fiat_p448_uint128)(arg1[0]) * (arg2[6])); - fiat_p448_uint128 x87 = ((fiat_p448_uint128)(arg1[0]) * (arg2[5])); - fiat_p448_uint128 x88 = ((fiat_p448_uint128)(arg1[0]) * (arg2[4])); - fiat_p448_uint128 x89 = ((fiat_p448_uint128)(arg1[0]) * (arg2[3])); - fiat_p448_uint128 x90 = ((fiat_p448_uint128)(arg1[0]) * (arg2[2])); - fiat_p448_uint128 x91 = ((fiat_p448_uint128)(arg1[0]) * (arg2[1])); - fiat_p448_uint128 x92 = ((fiat_p448_uint128)(arg1[0]) * (arg2[0])); - fiat_p448_uint128 x93 = (x89 + (x82 + (x76 + (x71 + (x19 + (x15 + (x10 + x4))))))); - uint64_t x94 = (uint64_t)(x93 >> 56); - uint64_t x95 = (uint64_t)(x93 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint512 x96 = (x85 + (x78 + (x72 + (x67 + (x63 + (x60 + (x58 + (x57 + (x47 + (x43 + (x42 + (x38 + (x37 + (x36 + (x32 + (x31 + (x30 + x29))))))))))))))))); - fiat_p448_uint128 x97 = (x86 + (x79 + (x73 + (x68 + (x64 + (x61 + (x59 + (x51 + (x48 + (x44 + (x39 + (x33 + x1)))))))))))); - fiat_p448_uint128 x98 = (x87 + (x80 + (x74 + (x69 + (x65 + (x62 + (x54 + (x52 + (x49 + (x45 + (x40 + (x34 + (x8 + x2))))))))))))); - fiat_p448_uint128 x99 = (x88 + (x81 + (x75 + (x70 + (x66 + (x56 + (x55 + (x53 + (x50 + (x46 + (x41 + (x35 + (x14 + (x9 + x3)))))))))))))); - fiat_p448_uint128 x100 = (x90 + (x83 + (x77 + (x23 + (x20 + (x16 + (x11 + x5))))))); - fiat_p448_uint128 x101 = (x91 + (x84 + (x26 + (x24 + (x21 + (x17 + (x12 + x6))))))); - fiat_p448_uint128 x102 = (x92 + (x28 + (x27 + (x25 + (x22 + (x18 + (x13 + x7))))))); - fiat_p448_uint128 x103 = (x94 + x99); - fiat_p448_uint256 x104 = (fiat_p448_uint256)(x96 >> 56); - uint64_t x105 = (uint64_t)(x96 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint256 x106 = (x103 + x104); - fiat_p448_uint256 x107 = (x106 >> 56); - uint64_t x108 = (uint64_t)(x106 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint256 x109 = (x102 + x104); - fiat_p448_uint256 x110 = (x107 + x98); - fiat_p448_uint256 x111 = (x109 >> 56); - uint64_t x112 = (uint64_t)(x109 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint256 x113 = (x111 + x101); - fiat_p448_uint128 x114 = (fiat_p448_uint128)(x110 >> 56); - uint64_t x115 = (uint64_t)(x110 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint128 x116 = (x114 + x97); - fiat_p448_uint128 x117 = (fiat_p448_uint128)(x113 >> 56); - uint64_t x118 = (uint64_t)(x113 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint128 x119 = (x117 + x100); + fiat_p448_uint128 x4 = ((fiat_p448_uint128)(arg1[6]) * (arg2[7])); + fiat_p448_uint128 x5 = ((fiat_p448_uint128)(arg1[6]) * (arg2[6])); + fiat_p448_uint128 x6 = ((fiat_p448_uint128)(arg1[5]) * (arg2[7])); + fiat_p448_uint128 x7 = ((fiat_p448_uint128)(arg1[7]) * (arg2[7])); + fiat_p448_uint128 x8 = ((fiat_p448_uint128)(arg1[7]) * (arg2[6])); + fiat_p448_uint128 x9 = ((fiat_p448_uint128)(arg1[7]) * (arg2[5])); + fiat_p448_uint128 x10 = ((fiat_p448_uint128)(arg1[6]) * (arg2[7])); + fiat_p448_uint128 x11 = ((fiat_p448_uint128)(arg1[6]) * (arg2[6])); + fiat_p448_uint128 x12 = ((fiat_p448_uint128)(arg1[5]) * (arg2[7])); + fiat_p448_uint128 x13 = ((fiat_p448_uint128)(arg1[7]) * (arg2[7])); + fiat_p448_uint128 x14 = ((fiat_p448_uint128)(arg1[7]) * (arg2[6])); + fiat_p448_uint128 x15 = ((fiat_p448_uint128)(arg1[7]) * (arg2[5])); + fiat_p448_uint128 x16 = ((fiat_p448_uint128)(arg1[7]) * (arg2[4])); + fiat_p448_uint128 x17 = ((fiat_p448_uint128)(arg1[7]) * (arg2[3])); + fiat_p448_uint128 x18 = ((fiat_p448_uint128)(arg1[7]) * (arg2[2])); + fiat_p448_uint128 x19 = ((fiat_p448_uint128)(arg1[7]) * (arg2[1])); + fiat_p448_uint128 x20 = ((fiat_p448_uint128)(arg1[6]) * (arg2[7])); + fiat_p448_uint128 x21 = ((fiat_p448_uint128)(arg1[6]) * (arg2[6])); + fiat_p448_uint128 x22 = ((fiat_p448_uint128)(arg1[6]) * (arg2[5])); + fiat_p448_uint128 x23 = ((fiat_p448_uint128)(arg1[6]) * (arg2[4])); + fiat_p448_uint128 x24 = ((fiat_p448_uint128)(arg1[6]) * (arg2[3])); + fiat_p448_uint128 x25 = ((fiat_p448_uint128)(arg1[6]) * (arg2[2])); + fiat_p448_uint128 x26 = ((fiat_p448_uint128)(arg1[5]) * (arg2[7])); + fiat_p448_uint128 x27 = ((fiat_p448_uint128)(arg1[5]) * (arg2[6])); + fiat_p448_uint128 x28 = ((fiat_p448_uint128)(arg1[5]) * (arg2[5])); + fiat_p448_uint128 x29 = ((fiat_p448_uint128)(arg1[5]) * (arg2[4])); + fiat_p448_uint128 x30 = ((fiat_p448_uint128)(arg1[5]) * (arg2[3])); + fiat_p448_uint128 x31 = ((fiat_p448_uint128)(arg1[4]) * (arg2[7])); + fiat_p448_uint128 x32 = ((fiat_p448_uint128)(arg1[4]) * (arg2[6])); + fiat_p448_uint128 x33 = ((fiat_p448_uint128)(arg1[4]) * (arg2[5])); + fiat_p448_uint128 x34 = ((fiat_p448_uint128)(arg1[4]) * (arg2[4])); + fiat_p448_uint128 x35 = ((fiat_p448_uint128)(arg1[3]) * (arg2[7])); + fiat_p448_uint128 x36 = ((fiat_p448_uint128)(arg1[3]) * (arg2[6])); + fiat_p448_uint128 x37 = ((fiat_p448_uint128)(arg1[3]) * (arg2[5])); + fiat_p448_uint128 x38 = ((fiat_p448_uint128)(arg1[2]) * (arg2[7])); + fiat_p448_uint128 x39 = ((fiat_p448_uint128)(arg1[2]) * (arg2[6])); + fiat_p448_uint128 x40 = ((fiat_p448_uint128)(arg1[1]) * (arg2[7])); + fiat_p448_uint128 x41 = ((fiat_p448_uint128)(arg1[7]) * (arg2[4])); + fiat_p448_uint128 x42 = ((fiat_p448_uint128)(arg1[7]) * (arg2[3])); + fiat_p448_uint128 x43 = ((fiat_p448_uint128)(arg1[7]) * (arg2[2])); + fiat_p448_uint128 x44 = ((fiat_p448_uint128)(arg1[7]) * (arg2[1])); + fiat_p448_uint128 x45 = ((fiat_p448_uint128)(arg1[6]) * (arg2[5])); + fiat_p448_uint128 x46 = ((fiat_p448_uint128)(arg1[6]) * (arg2[4])); + fiat_p448_uint128 x47 = ((fiat_p448_uint128)(arg1[6]) * (arg2[3])); + fiat_p448_uint128 x48 = ((fiat_p448_uint128)(arg1[6]) * (arg2[2])); + fiat_p448_uint128 x49 = ((fiat_p448_uint128)(arg1[5]) * (arg2[6])); + fiat_p448_uint128 x50 = ((fiat_p448_uint128)(arg1[5]) * (arg2[5])); + fiat_p448_uint128 x51 = ((fiat_p448_uint128)(arg1[5]) * (arg2[4])); + fiat_p448_uint128 x52 = ((fiat_p448_uint128)(arg1[5]) * (arg2[3])); + fiat_p448_uint128 x53 = ((fiat_p448_uint128)(arg1[4]) * (arg2[7])); + fiat_p448_uint128 x54 = ((fiat_p448_uint128)(arg1[4]) * (arg2[6])); + fiat_p448_uint128 x55 = ((fiat_p448_uint128)(arg1[4]) * (arg2[5])); + fiat_p448_uint128 x56 = ((fiat_p448_uint128)(arg1[4]) * (arg2[4])); + fiat_p448_uint128 x57 = ((fiat_p448_uint128)(arg1[3]) * (arg2[7])); + fiat_p448_uint128 x58 = ((fiat_p448_uint128)(arg1[3]) * (arg2[6])); + fiat_p448_uint128 x59 = ((fiat_p448_uint128)(arg1[3]) * (arg2[5])); + fiat_p448_uint128 x60 = ((fiat_p448_uint128)(arg1[2]) * (arg2[7])); + fiat_p448_uint128 x61 = ((fiat_p448_uint128)(arg1[2]) * (arg2[6])); + fiat_p448_uint128 x62 = ((fiat_p448_uint128)(arg1[1]) * (arg2[7])); + fiat_p448_uint128 x63 = ((fiat_p448_uint128)(arg1[7]) * (arg2[0])); + fiat_p448_uint128 x64 = ((fiat_p448_uint128)(arg1[6]) * (arg2[1])); + fiat_p448_uint128 x65 = ((fiat_p448_uint128)(arg1[6]) * (arg2[0])); + fiat_p448_uint128 x66 = ((fiat_p448_uint128)(arg1[5]) * (arg2[2])); + fiat_p448_uint128 x67 = ((fiat_p448_uint128)(arg1[5]) * (arg2[1])); + fiat_p448_uint128 x68 = ((fiat_p448_uint128)(arg1[5]) * (arg2[0])); + fiat_p448_uint128 x69 = ((fiat_p448_uint128)(arg1[4]) * (arg2[3])); + fiat_p448_uint128 x70 = ((fiat_p448_uint128)(arg1[4]) * (arg2[2])); + fiat_p448_uint128 x71 = ((fiat_p448_uint128)(arg1[4]) * (arg2[1])); + fiat_p448_uint128 x72 = ((fiat_p448_uint128)(arg1[4]) * (arg2[0])); + fiat_p448_uint128 x73 = ((fiat_p448_uint128)(arg1[3]) * (arg2[4])); + fiat_p448_uint128 x74 = ((fiat_p448_uint128)(arg1[3]) * (arg2[3])); + fiat_p448_uint128 x75 = ((fiat_p448_uint128)(arg1[3]) * (arg2[2])); + fiat_p448_uint128 x76 = ((fiat_p448_uint128)(arg1[3]) * (arg2[1])); + fiat_p448_uint128 x77 = ((fiat_p448_uint128)(arg1[3]) * (arg2[0])); + fiat_p448_uint128 x78 = ((fiat_p448_uint128)(arg1[2]) * (arg2[5])); + fiat_p448_uint128 x79 = ((fiat_p448_uint128)(arg1[2]) * (arg2[4])); + fiat_p448_uint128 x80 = ((fiat_p448_uint128)(arg1[2]) * (arg2[3])); + fiat_p448_uint128 x81 = ((fiat_p448_uint128)(arg1[2]) * (arg2[2])); + fiat_p448_uint128 x82 = ((fiat_p448_uint128)(arg1[2]) * (arg2[1])); + fiat_p448_uint128 x83 = ((fiat_p448_uint128)(arg1[2]) * (arg2[0])); + fiat_p448_uint128 x84 = ((fiat_p448_uint128)(arg1[1]) * (arg2[6])); + fiat_p448_uint128 x85 = ((fiat_p448_uint128)(arg1[1]) * (arg2[5])); + fiat_p448_uint128 x86 = ((fiat_p448_uint128)(arg1[1]) * (arg2[4])); + fiat_p448_uint128 x87 = ((fiat_p448_uint128)(arg1[1]) * (arg2[3])); + fiat_p448_uint128 x88 = ((fiat_p448_uint128)(arg1[1]) * (arg2[2])); + fiat_p448_uint128 x89 = ((fiat_p448_uint128)(arg1[1]) * (arg2[1])); + fiat_p448_uint128 x90 = ((fiat_p448_uint128)(arg1[1]) * (arg2[0])); + fiat_p448_uint128 x91 = ((fiat_p448_uint128)(arg1[0]) * (arg2[7])); + fiat_p448_uint128 x92 = ((fiat_p448_uint128)(arg1[0]) * (arg2[6])); + fiat_p448_uint128 x93 = ((fiat_p448_uint128)(arg1[0]) * (arg2[5])); + fiat_p448_uint128 x94 = ((fiat_p448_uint128)(arg1[0]) * (arg2[4])); + fiat_p448_uint128 x95 = ((fiat_p448_uint128)(arg1[0]) * (arg2[3])); + fiat_p448_uint128 x96 = ((fiat_p448_uint128)(arg1[0]) * (arg2[2])); + fiat_p448_uint128 x97 = ((fiat_p448_uint128)(arg1[0]) * (arg2[1])); + fiat_p448_uint128 x98 = ((fiat_p448_uint128)(arg1[0]) * (arg2[0])); + fiat_p448_uint128 x99 = (x95 + (x88 + (x82 + (x77 + (x31 + (x27 + (x22 + x16))))))); + uint64_t x100 = (uint64_t)(x99 >> 56); + uint64_t x101 = (uint64_t)(x99 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x102 = (x91 + (x84 + (x78 + (x73 + (x69 + (x66 + (x64 + (x63 + (x53 + (x49 + (x45 + x41))))))))))); + fiat_p448_uint128 x103 = (x92 + (x85 + (x79 + (x74 + (x70 + (x67 + (x65 + (x57 + (x54 + (x50 + (x46 + (x42 + (x13 + x7))))))))))))); + fiat_p448_uint128 x104 = (x93 + (x86 + (x80 + (x75 + (x71 + (x68 + (x60 + (x58 + (x55 + (x51 + (x47 + (x43 + (x20 + (x14 + (x10 + x8))))))))))))))); + fiat_p448_uint128 x105 = (x94 + (x87 + (x81 + (x76 + (x72 + (x62 + (x61 + (x59 + (x56 + (x52 + (x48 + (x44 + (x26 + (x21 + (x15 + (x12 + (x11 + x9))))))))))))))))); + fiat_p448_uint128 x106 = (x96 + (x89 + (x83 + (x35 + (x32 + (x28 + (x23 + (x17 + x1)))))))); + fiat_p448_uint128 x107 = (x97 + (x90 + (x38 + (x36 + (x33 + (x29 + (x24 + (x18 + (x4 + x2))))))))); + fiat_p448_uint128 x108 = (x98 + (x40 + (x39 + (x37 + (x34 + (x30 + (x25 + (x19 + (x6 + (x5 + x3)))))))))); + fiat_p448_uint128 x109 = (x100 + x105); + uint64_t x110 = (uint64_t)(x102 >> 56); + uint64_t x111 = (uint64_t)(x102 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x112 = (x109 + x110); + uint64_t x113 = (uint64_t)(x112 >> 56); + uint64_t x114 = (uint64_t)(x112 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x115 = (x108 + x110); + fiat_p448_uint128 x116 = (x113 + x104); + uint64_t x117 = (uint64_t)(x115 >> 56); + uint64_t x118 = (uint64_t)(x115 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x119 = (x117 + x107); uint64_t x120 = (uint64_t)(x116 >> 56); uint64_t x121 = (uint64_t)(x116 & UINT64_C(0xffffffffffffff)); - uint64_t x122 = (x120 + x105); + fiat_p448_uint128 x122 = (x120 + x103); uint64_t x123 = (uint64_t)(x119 >> 56); uint64_t x124 = (uint64_t)(x119 & UINT64_C(0xffffffffffffff)); - uint64_t x125 = (x123 + x95); - uint64_t x126 = (x122 >> 56); - uint64_t x127 = (x122 & UINT64_C(0xffffffffffffff)); - uint64_t x128 = (x125 >> 56); - uint64_t x129 = (x125 & UINT64_C(0xffffffffffffff)); - uint64_t x130 = (x108 + x126); - uint64_t x131 = (x112 + x126); - uint64_t x132 = (x128 + x130); - uint64_t x133 = (x132 >> 56); - uint64_t x134 = (x132 & UINT64_C(0xffffffffffffff)); - uint64_t x135 = (x133 + x115); - uint64_t x136 = (x131 >> 56); - uint64_t x137 = (x131 & UINT64_C(0xffffffffffffff)); - uint64_t x138 = (x136 + x118); - out1[0] = x137; - out1[1] = x138; - out1[2] = x124; - out1[3] = x129; - out1[4] = x134; - out1[5] = x135; - out1[6] = x121; - out1[7] = x127; + fiat_p448_uint128 x125 = (x123 + x106); + uint64_t x126 = (uint64_t)(x122 >> 56); + uint64_t x127 = (uint64_t)(x122 & UINT64_C(0xffffffffffffff)); + uint64_t x128 = (x126 + x111); + uint64_t x129 = (uint64_t)(x125 >> 56); + uint64_t x130 = (uint64_t)(x125 & UINT64_C(0xffffffffffffff)); + uint64_t x131 = (x129 + x101); + uint64_t x132 = (x128 >> 56); + uint64_t x133 = (x128 & UINT64_C(0xffffffffffffff)); + uint64_t x134 = (x131 >> 56); + uint64_t x135 = (x131 & UINT64_C(0xffffffffffffff)); + uint64_t x136 = (x114 + x132); + uint64_t x137 = (x118 + x132); + uint64_t x138 = (x134 + x136); + uint64_t x139 = (x138 >> 56); + uint64_t x140 = (x138 & UINT64_C(0xffffffffffffff)); + uint64_t x141 = (x139 + x121); + uint64_t x142 = (x137 >> 56); + uint64_t x143 = (x137 & UINT64_C(0xffffffffffffff)); + uint64_t x144 = (x142 + x124); + out1[0] = x143; + out1[1] = x144; + out1[2] = x130; + out1[3] = x135; + out1[4] = x140; + out1[5] = x141; + out1[6] = x127; + out1[7] = x133; } /* @@ -249,112 +255,116 @@ static void fiat_p448_carry_square(uint64_t out1[8], const uint64_t arg1[8]) { uint64_t x19 = ((arg1[3]) * (uint64_t)0x2); uint64_t x20 = ((arg1[2]) * (uint64_t)0x2); uint64_t x21 = ((arg1[1]) * (uint64_t)0x2); - fiat_p448_uint128 x22 = ((fiat_p448_uint128)(arg1[7]) * x2); - fiat_p448_uint512 x23 = ((fiat_p448_uint512)((fiat_p448_uint128)(arg1[7]) * x1) << 168); - fiat_p448_uint128 x24 = ((fiat_p448_uint128)(arg1[6]) * x4); - fiat_p448_uint256 x25 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[6]) * x3) << 112); - fiat_p448_uint128 x26 = ((fiat_p448_uint128)(arg1[6]) * x7); - fiat_p448_uint256 x27 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[6]) * x6) << 56); - fiat_p448_uint128 x28 = ((fiat_p448_uint128)(arg1[5]) * x4); - fiat_p448_uint256 x29 = ((fiat_p448_uint256)((fiat_p448_uint128)(arg1[5]) * x3) << 56); - fiat_p448_uint128 x30 = ((fiat_p448_uint128)(arg1[5]) * x9); - fiat_p448_uint128 x31 = ((fiat_p448_uint128)(arg1[5]) * x8); - fiat_p448_uint128 x32 = ((fiat_p448_uint128)(arg1[5]) * x12); - fiat_p448_uint128 x33 = ((fiat_p448_uint128)(arg1[5]) * x11); - fiat_p448_uint128 x34 = ((fiat_p448_uint128)(arg1[4]) * x4); - fiat_p448_uint128 x35 = ((fiat_p448_uint128)(arg1[4]) * x3); - fiat_p448_uint128 x36 = ((fiat_p448_uint128)(arg1[4]) * x9); - fiat_p448_uint128 x37 = ((fiat_p448_uint128)(arg1[4]) * x8); - fiat_p448_uint128 x38 = ((fiat_p448_uint128)(arg1[4]) * x14); - fiat_p448_uint128 x39 = ((fiat_p448_uint128)(arg1[4]) * x13); - fiat_p448_uint128 x40 = ((fiat_p448_uint128)(arg1[4]) * x17); - fiat_p448_uint128 x41 = ((fiat_p448_uint128)(arg1[4]) * x16); - fiat_p448_uint128 x42 = ((fiat_p448_uint128)(arg1[3]) * x4); - fiat_p448_uint128 x43 = ((fiat_p448_uint128)(arg1[3]) * x3); - fiat_p448_uint128 x44 = ((fiat_p448_uint128)(arg1[3]) * x9); - fiat_p448_uint128 x45 = ((fiat_p448_uint128)(arg1[3]) * x8); - fiat_p448_uint128 x46 = ((fiat_p448_uint128)(arg1[3]) * x14); - fiat_p448_uint128 x47 = ((fiat_p448_uint128)(arg1[3]) * x13); - fiat_p448_uint128 x48 = ((fiat_p448_uint128)(arg1[3]) * x18); - fiat_p448_uint128 x49 = ((fiat_p448_uint128)(arg1[3]) * (arg1[3])); - fiat_p448_uint128 x50 = ((fiat_p448_uint128)(arg1[2]) * x4); - fiat_p448_uint128 x51 = ((fiat_p448_uint128)(arg1[2]) * x3); - fiat_p448_uint128 x52 = ((fiat_p448_uint128)(arg1[2]) * x9); - fiat_p448_uint128 x53 = ((fiat_p448_uint128)(arg1[2]) * x8); - fiat_p448_uint128 x54 = ((fiat_p448_uint128)(arg1[2]) * x15); - fiat_p448_uint128 x55 = ((fiat_p448_uint128)(arg1[2]) * x18); - fiat_p448_uint128 x56 = ((fiat_p448_uint128)(arg1[2]) * x19); - fiat_p448_uint128 x57 = ((fiat_p448_uint128)(arg1[2]) * (arg1[2])); - fiat_p448_uint128 x58 = ((fiat_p448_uint128)(arg1[1]) * x4); - fiat_p448_uint128 x59 = ((fiat_p448_uint128)(arg1[1]) * x3); - fiat_p448_uint128 x60 = ((fiat_p448_uint128)(arg1[1]) * x10); - fiat_p448_uint128 x61 = ((fiat_p448_uint128)(arg1[1]) * x15); - fiat_p448_uint128 x62 = ((fiat_p448_uint128)(arg1[1]) * x18); - fiat_p448_uint128 x63 = ((fiat_p448_uint128)(arg1[1]) * x19); - fiat_p448_uint128 x64 = ((fiat_p448_uint128)(arg1[1]) * x20); - fiat_p448_uint128 x65 = ((fiat_p448_uint128)(arg1[1]) * (arg1[1])); - fiat_p448_uint128 x66 = ((fiat_p448_uint128)(arg1[0]) * x5); - fiat_p448_uint128 x67 = ((fiat_p448_uint128)(arg1[0]) * x10); - fiat_p448_uint128 x68 = ((fiat_p448_uint128)(arg1[0]) * x15); - fiat_p448_uint128 x69 = ((fiat_p448_uint128)(arg1[0]) * x18); - fiat_p448_uint128 x70 = ((fiat_p448_uint128)(arg1[0]) * x19); - fiat_p448_uint128 x71 = ((fiat_p448_uint128)(arg1[0]) * x20); - fiat_p448_uint128 x72 = ((fiat_p448_uint128)(arg1[0]) * x21); - fiat_p448_uint128 x73 = ((fiat_p448_uint128)(arg1[0]) * (arg1[0])); - fiat_p448_uint128 x74 = (x70 + (x64 + (x34 + x30))); - uint64_t x75 = (uint64_t)(x74 >> 56); - uint64_t x76 = (uint64_t)(x74 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint512 x77 = (x66 + (x60 + (x54 + (x48 + (x35 + (x31 + (x29 + (x27 + (x25 + x23))))))))); - fiat_p448_uint128 x78 = (x67 + (x61 + (x55 + (x49 + (x43 + (x37 + (x33 + x22))))))); - fiat_p448_uint128 x79 = (x68 + (x62 + (x56 + (x51 + (x45 + (x39 + x24)))))); - fiat_p448_uint128 x80 = (x69 + (x63 + (x59 + (x57 + (x53 + (x47 + (x41 + (x28 + x26)))))))); - fiat_p448_uint128 x81 = (x71 + (x65 + (x42 + (x36 + x32)))); - fiat_p448_uint128 x82 = (x72 + (x50 + (x44 + x38))); - fiat_p448_uint128 x83 = (x73 + (x58 + (x52 + (x46 + x40)))); - fiat_p448_uint128 x84 = (x75 + x80); - fiat_p448_uint256 x85 = (fiat_p448_uint256)(x77 >> 56); - uint64_t x86 = (uint64_t)(x77 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint256 x87 = (x84 + x85); - fiat_p448_uint256 x88 = (x87 >> 56); - uint64_t x89 = (uint64_t)(x87 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint256 x90 = (x83 + x85); - fiat_p448_uint256 x91 = (x88 + x79); - fiat_p448_uint256 x92 = (x90 >> 56); - uint64_t x93 = (uint64_t)(x90 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint256 x94 = (x92 + x82); - fiat_p448_uint128 x95 = (fiat_p448_uint128)(x91 >> 56); - uint64_t x96 = (uint64_t)(x91 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint128 x97 = (x95 + x78); - fiat_p448_uint128 x98 = (fiat_p448_uint128)(x94 >> 56); - uint64_t x99 = (uint64_t)(x94 & UINT64_C(0xffffffffffffff)); - fiat_p448_uint128 x100 = (x98 + x81); - uint64_t x101 = (uint64_t)(x97 >> 56); - uint64_t x102 = (uint64_t)(x97 & UINT64_C(0xffffffffffffff)); - uint64_t x103 = (x101 + x86); - uint64_t x104 = (uint64_t)(x100 >> 56); - uint64_t x105 = (uint64_t)(x100 & UINT64_C(0xffffffffffffff)); - uint64_t x106 = (x104 + x76); - uint64_t x107 = (x103 >> 56); - uint64_t x108 = (x103 & UINT64_C(0xffffffffffffff)); - uint64_t x109 = (x106 >> 56); - uint64_t x110 = (x106 & UINT64_C(0xffffffffffffff)); - uint64_t x111 = (x89 + x107); - uint64_t x112 = (x93 + x107); - uint64_t x113 = (x109 + x111); - uint64_t x114 = (x113 >> 56); - uint64_t x115 = (x113 & UINT64_C(0xffffffffffffff)); - uint64_t x116 = (x114 + x96); - uint64_t x117 = (x112 >> 56); - uint64_t x118 = (x112 & UINT64_C(0xffffffffffffff)); - uint64_t x119 = (x117 + x99); - out1[0] = x118; - out1[1] = x119; - out1[2] = x105; - out1[3] = x110; - out1[4] = x115; - out1[5] = x116; - out1[6] = x102; - out1[7] = x108; + fiat_p448_uint128 x22 = ((fiat_p448_uint128)(arg1[7]) * x1); + fiat_p448_uint128 x23 = ((fiat_p448_uint128)(arg1[6]) * x3); + fiat_p448_uint128 x24 = ((fiat_p448_uint128)(arg1[6]) * x6); + fiat_p448_uint128 x25 = ((fiat_p448_uint128)(arg1[5]) * x3); + fiat_p448_uint128 x26 = ((fiat_p448_uint128)(arg1[7]) * x1); + fiat_p448_uint128 x27 = ((fiat_p448_uint128)(arg1[6]) * x3); + fiat_p448_uint128 x28 = ((fiat_p448_uint128)(arg1[6]) * x6); + fiat_p448_uint128 x29 = ((fiat_p448_uint128)(arg1[5]) * x3); + fiat_p448_uint128 x30 = ((fiat_p448_uint128)(arg1[7]) * x2); + fiat_p448_uint128 x31 = ((fiat_p448_uint128)(arg1[6]) * x4); + fiat_p448_uint128 x32 = ((fiat_p448_uint128)(arg1[6]) * x7); + fiat_p448_uint128 x33 = ((fiat_p448_uint128)(arg1[5]) * x4); + fiat_p448_uint128 x34 = ((fiat_p448_uint128)(arg1[5]) * x9); + fiat_p448_uint128 x35 = ((fiat_p448_uint128)(arg1[5]) * x8); + fiat_p448_uint128 x36 = ((fiat_p448_uint128)(arg1[5]) * x12); + fiat_p448_uint128 x37 = ((fiat_p448_uint128)(arg1[5]) * x11); + fiat_p448_uint128 x38 = ((fiat_p448_uint128)(arg1[4]) * x4); + fiat_p448_uint128 x39 = ((fiat_p448_uint128)(arg1[4]) * x3); + fiat_p448_uint128 x40 = ((fiat_p448_uint128)(arg1[4]) * x9); + fiat_p448_uint128 x41 = ((fiat_p448_uint128)(arg1[4]) * x8); + fiat_p448_uint128 x42 = ((fiat_p448_uint128)(arg1[4]) * x14); + fiat_p448_uint128 x43 = ((fiat_p448_uint128)(arg1[4]) * x13); + fiat_p448_uint128 x44 = ((fiat_p448_uint128)(arg1[4]) * x17); + fiat_p448_uint128 x45 = ((fiat_p448_uint128)(arg1[4]) * x16); + fiat_p448_uint128 x46 = ((fiat_p448_uint128)(arg1[3]) * x4); + fiat_p448_uint128 x47 = ((fiat_p448_uint128)(arg1[3]) * x3); + fiat_p448_uint128 x48 = ((fiat_p448_uint128)(arg1[3]) * x9); + fiat_p448_uint128 x49 = ((fiat_p448_uint128)(arg1[3]) * x8); + fiat_p448_uint128 x50 = ((fiat_p448_uint128)(arg1[3]) * x14); + fiat_p448_uint128 x51 = ((fiat_p448_uint128)(arg1[3]) * x13); + fiat_p448_uint128 x52 = ((fiat_p448_uint128)(arg1[3]) * x18); + fiat_p448_uint128 x53 = ((fiat_p448_uint128)(arg1[3]) * (arg1[3])); + fiat_p448_uint128 x54 = ((fiat_p448_uint128)(arg1[2]) * x4); + fiat_p448_uint128 x55 = ((fiat_p448_uint128)(arg1[2]) * x3); + fiat_p448_uint128 x56 = ((fiat_p448_uint128)(arg1[2]) * x9); + fiat_p448_uint128 x57 = ((fiat_p448_uint128)(arg1[2]) * x8); + fiat_p448_uint128 x58 = ((fiat_p448_uint128)(arg1[2]) * x15); + fiat_p448_uint128 x59 = ((fiat_p448_uint128)(arg1[2]) * x18); + fiat_p448_uint128 x60 = ((fiat_p448_uint128)(arg1[2]) * x19); + fiat_p448_uint128 x61 = ((fiat_p448_uint128)(arg1[2]) * (arg1[2])); + fiat_p448_uint128 x62 = ((fiat_p448_uint128)(arg1[1]) * x4); + fiat_p448_uint128 x63 = ((fiat_p448_uint128)(arg1[1]) * x3); + fiat_p448_uint128 x64 = ((fiat_p448_uint128)(arg1[1]) * x10); + fiat_p448_uint128 x65 = ((fiat_p448_uint128)(arg1[1]) * x15); + fiat_p448_uint128 x66 = ((fiat_p448_uint128)(arg1[1]) * x18); + fiat_p448_uint128 x67 = ((fiat_p448_uint128)(arg1[1]) * x19); + fiat_p448_uint128 x68 = ((fiat_p448_uint128)(arg1[1]) * x20); + fiat_p448_uint128 x69 = ((fiat_p448_uint128)(arg1[1]) * (arg1[1])); + fiat_p448_uint128 x70 = ((fiat_p448_uint128)(arg1[0]) * x5); + fiat_p448_uint128 x71 = ((fiat_p448_uint128)(arg1[0]) * x10); + fiat_p448_uint128 x72 = ((fiat_p448_uint128)(arg1[0]) * x15); + fiat_p448_uint128 x73 = ((fiat_p448_uint128)(arg1[0]) * x18); + fiat_p448_uint128 x74 = ((fiat_p448_uint128)(arg1[0]) * x19); + fiat_p448_uint128 x75 = ((fiat_p448_uint128)(arg1[0]) * x20); + fiat_p448_uint128 x76 = ((fiat_p448_uint128)(arg1[0]) * x21); + fiat_p448_uint128 x77 = ((fiat_p448_uint128)(arg1[0]) * (arg1[0])); + fiat_p448_uint128 x78 = (x74 + (x68 + (x38 + x34))); + uint64_t x79 = (uint64_t)(x78 >> 56); + uint64_t x80 = (uint64_t)(x78 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x81 = (x70 + (x64 + (x58 + (x52 + (x39 + x35))))); + fiat_p448_uint128 x82 = (x71 + (x65 + (x59 + (x53 + (x47 + (x41 + (x37 + (x30 + x26)))))))); + fiat_p448_uint128 x83 = (x72 + (x66 + (x60 + (x55 + (x49 + (x43 + (x31 + x27))))))); + fiat_p448_uint128 x84 = (x73 + (x67 + (x63 + (x61 + (x57 + (x51 + (x45 + (x33 + (x32 + (x29 + x28)))))))))); + fiat_p448_uint128 x85 = (x75 + (x69 + (x46 + (x40 + (x36 + x22))))); + fiat_p448_uint128 x86 = (x76 + (x54 + (x48 + (x42 + x23)))); + fiat_p448_uint128 x87 = (x77 + (x62 + (x56 + (x50 + (x44 + (x25 + x24)))))); + fiat_p448_uint128 x88 = (x79 + x84); + uint64_t x89 = (uint64_t)(x81 >> 56); + uint64_t x90 = (uint64_t)(x81 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x91 = (x88 + x89); + uint64_t x92 = (uint64_t)(x91 >> 56); + uint64_t x93 = (uint64_t)(x91 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x94 = (x87 + x89); + fiat_p448_uint128 x95 = (x92 + x83); + uint64_t x96 = (uint64_t)(x94 >> 56); + uint64_t x97 = (uint64_t)(x94 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x98 = (x96 + x86); + uint64_t x99 = (uint64_t)(x95 >> 56); + uint64_t x100 = (uint64_t)(x95 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x101 = (x99 + x82); + uint64_t x102 = (uint64_t)(x98 >> 56); + uint64_t x103 = (uint64_t)(x98 & UINT64_C(0xffffffffffffff)); + fiat_p448_uint128 x104 = (x102 + x85); + uint64_t x105 = (uint64_t)(x101 >> 56); + uint64_t x106 = (uint64_t)(x101 & UINT64_C(0xffffffffffffff)); + uint64_t x107 = (x105 + x90); + uint64_t x108 = (uint64_t)(x104 >> 56); + uint64_t x109 = (uint64_t)(x104 & UINT64_C(0xffffffffffffff)); + uint64_t x110 = (x108 + x80); + uint64_t x111 = (x107 >> 56); + uint64_t x112 = (x107 & UINT64_C(0xffffffffffffff)); + uint64_t x113 = (x110 >> 56); + uint64_t x114 = (x110 & UINT64_C(0xffffffffffffff)); + uint64_t x115 = (x93 + x111); + uint64_t x116 = (x97 + x111); + uint64_t x117 = (x113 + x115); + uint64_t x118 = (x117 >> 56); + uint64_t x119 = (x117 & UINT64_C(0xffffffffffffff)); + uint64_t x120 = (x118 + x100); + uint64_t x121 = (x116 >> 56); + uint64_t x122 = (x116 & UINT64_C(0xffffffffffffff)); + uint64_t x123 = (x121 + x103); + out1[0] = x122; + out1[1] = x123; + out1[2] = x109; + out1[3] = x114; + out1[4] = x119; + out1[5] = x120; + out1[6] = x106; + out1[7] = x112; } /* |