diff options
Diffstat (limited to 'src/Specific/montgomery64_2e510m290x2e496m1_8limbs')
22 files changed, 0 insertions, 1140 deletions
diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/CurveParameters.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/CurveParameters.v deleted file mode 100644 index d8cf3d25f..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/CurveParameters.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Import Crypto.Specific.Framework.RawCurveParameters. -Require Import Crypto.Util.LetIn. - -(*** -Modulus : 2^510 - 290*2^496 - 1 -Base: 64 -***) - -Definition curve : CurveParameters := - {| - sz := 8%nat; - base := 64; - bitwidth := 64; - s := 2^510; - c := [(1, 1); (290, 2^496)]; - carry_chains := None; - - a24 := None; - coef_div_modulus := None; - - goldilocks := None; - karatsuba := None; - montgomery := true; - freeze := Some false; - ladderstep := false; - - mul_code := None; - - square_code := None; - - upper_bound_of_exponent_loose := None; - upper_bound_of_exponent_tight := None; - allowable_bit_widths := None; - freeze_extra_allowable_bit_widths := None; - modinv_fuel := None - |}. - -Ltac extra_prove_mul_eq _ := idtac. -Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/Synthesis.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/Synthesis.v deleted file mode 100644 index d3c4e871f..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/Synthesis.v +++ /dev/null @@ -1,9 +0,0 @@ -Require Import Crypto.Specific.Framework.SynthesisFramework. -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.CurveParameters. - -Module P <: PrePackage. - Definition package : Tag.Context. - Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. -End P. - -Module Export S := PackageSynthesis P. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/compiler.sh b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/compiler.sh deleted file mode 100755 index 231fd60e3..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/compiler.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh -set -eu - -clang -fbracket-depth=999999 -march=native -mbmi2 -mtune=native -std=gnu11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{64,64,64,64,64,64,64,64}' -Dmodulus_array='{0x3e,0xdd,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='8' -Dq_mpz='(1_mpz<<510) - 290*(1_mpz<<496) - 1' "$@" diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/compilerxx.sh b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/compilerxx.sh deleted file mode 100755 index 20f1dedb0..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/compilerxx.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh -set -eu - -clang++ -fbracket-depth=999999 -march=native -mbmi2 -mtune=native -std=gnu++11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{64,64,64,64,64,64,64,64}' -Dmodulus_array='{0x3e,0xdd,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='8' -Dq_mpz='(1_mpz<<510) - 290*(1_mpz<<496) - 1' "$@" diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feadd.c b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feadd.c deleted file mode 100644 index 9851fdab2..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feadd.c +++ /dev/null @@ -1,52 +0,0 @@ -static void feadd(uint64_t out[8], const uint64_t in1[8], const uint64_t in2[8]) { - { const uint64_t x16 = in1[7]; - { const uint64_t x17 = in1[6]; - { const uint64_t x15 = in1[5]; - { const uint64_t x13 = in1[4]; - { const uint64_t x11 = in1[3]; - { const uint64_t x9 = in1[2]; - { const uint64_t x7 = in1[1]; - { const uint64_t x5 = in1[0]; - { const uint64_t x30 = in2[7]; - { const uint64_t x31 = in2[6]; - { const uint64_t x29 = in2[5]; - { const uint64_t x27 = in2[4]; - { const uint64_t x25 = in2[3]; - { const uint64_t x23 = in2[2]; - { const uint64_t x21 = in2[1]; - { const uint64_t x19 = in2[0]; - { uint64_t x33; uint8_t x34 = _addcarryx_u64(0x0, x5, x19, &x33); - { uint64_t x36; uint8_t x37 = _addcarryx_u64(x34, x7, x21, &x36); - { uint64_t x39; uint8_t x40 = _addcarryx_u64(x37, x9, x23, &x39); - { uint64_t x42; uint8_t x43 = _addcarryx_u64(x40, x11, x25, &x42); - { uint64_t x45; uint8_t x46 = _addcarryx_u64(x43, x13, x27, &x45); - { uint64_t x48; uint8_t x49 = _addcarryx_u64(x46, x15, x29, &x48); - { uint64_t x51; uint8_t x52 = _addcarryx_u64(x49, x17, x31, &x51); - { uint64_t x54; uint8_t x55 = _addcarryx_u64(x52, x16, x30, &x54); - { uint64_t x57; uint8_t x58 = _subborrow_u64(0x0, x33, 0xffffffffffffffffL, &x57); - { uint64_t x60; uint8_t x61 = _subborrow_u64(x58, x36, 0xffffffffffffffffL, &x60); - { uint64_t x63; uint8_t x64 = _subborrow_u64(x61, x39, 0xffffffffffffffffL, &x63); - { uint64_t x66; uint8_t x67 = _subborrow_u64(x64, x42, 0xffffffffffffffffL, &x66); - { uint64_t x69; uint8_t x70 = _subborrow_u64(x67, x45, 0xffffffffffffffffL, &x69); - { uint64_t x72; uint8_t x73 = _subborrow_u64(x70, x48, 0xffffffffffffffffL, &x72); - { uint64_t x75; uint8_t x76 = _subborrow_u64(x73, x51, 0xffffffffffffffffL, &x75); - { uint64_t x78; uint8_t x79 = _subborrow_u64(x76, x54, 0x3eddffffffffffff, &x78); - { uint64_t _; uint8_t x82 = _subborrow_u64(x79, x55, 0x0, &_); - { uint64_t x83 = cmovznz64(x82, x78, x54); - { uint64_t x84 = cmovznz64(x82, x75, x51); - { uint64_t x85 = cmovznz64(x82, x72, x48); - { uint64_t x86 = cmovznz64(x82, x69, x45); - { uint64_t x87 = cmovznz64(x82, x66, x42); - { uint64_t x88 = cmovznz64(x82, x63, x39); - { uint64_t x89 = cmovznz64(x82, x60, x36); - { uint64_t x90 = cmovznz64(x82, x57, x33); - out[0] = x90; - out[1] = x89; - out[2] = x88; - out[3] = x87; - out[4] = x86; - out[5] = x85; - out[6] = x84; - out[7] = x83; - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feadd.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feadd.v deleted file mode 100644 index a3d8a0922..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feadd.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition add : - { add : feBW_small -> feBW_small -> feBW_small - | forall a b, phiM_small (add a b) = F.add (phiM_small a) (phiM_small b) }. -Proof. - Set Ltac Profiling. - Time synthesize_add (). - Show Ltac Profile. -Time Defined. - -Print Assumptions add. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feaddDisplay.log b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feaddDisplay.log deleted file mode 100644 index 57c9fad62..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feaddDisplay.log +++ /dev/null @@ -1,32 +0,0 @@ -λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core, - uint64_t x33, uint8_t x34 = addcarryx_u64(0x0, x5, x19); - uint64_t x36, uint8_t x37 = addcarryx_u64(x34, x7, x21); - uint64_t x39, uint8_t x40 = addcarryx_u64(x37, x9, x23); - uint64_t x42, uint8_t x43 = addcarryx_u64(x40, x11, x25); - uint64_t x45, uint8_t x46 = addcarryx_u64(x43, x13, x27); - uint64_t x48, uint8_t x49 = addcarryx_u64(x46, x15, x29); - uint64_t x51, uint8_t x52 = addcarryx_u64(x49, x17, x31); - uint64_t x54, uint8_t x55 = addcarryx_u64(x52, x16, x30); - uint64_t x57, uint8_t x58 = subborrow_u64(0x0, x33, 0xffffffffffffffffL); - uint64_t x60, uint8_t x61 = subborrow_u64(x58, x36, 0xffffffffffffffffL); - uint64_t x63, uint8_t x64 = subborrow_u64(x61, x39, 0xffffffffffffffffL); - uint64_t x66, uint8_t x67 = subborrow_u64(x64, x42, 0xffffffffffffffffL); - uint64_t x69, uint8_t x70 = subborrow_u64(x67, x45, 0xffffffffffffffffL); - uint64_t x72, uint8_t x73 = subborrow_u64(x70, x48, 0xffffffffffffffffL); - uint64_t x75, uint8_t x76 = subborrow_u64(x73, x51, 0xffffffffffffffffL); - uint64_t x78, uint8_t x79 = subborrow_u64(x76, x54, 0x3eddffffffffffff); - uint64_t _, uint8_t x82 = subborrow_u64(x79, x55, 0x0); - uint64_t x83 = cmovznz64(x82, x78, x54); - uint64_t x84 = cmovznz64(x82, x75, x51); - uint64_t x85 = cmovznz64(x82, x72, x48); - uint64_t x86 = cmovznz64(x82, x69, x45); - uint64_t x87 = cmovznz64(x82, x66, x42); - uint64_t x88 = cmovznz64(x82, x63, x39); - uint64_t x89 = cmovznz64(x82, x60, x36); - uint64_t x90 = cmovznz64(x82, x57, x33); - return (x83, x84, x85, x86, x87, x88, x89, x90)) -(x, x0)%core - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feaddDisplay.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feaddDisplay.v deleted file mode 100644 index e6939a00b..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feaddDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.feadd. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display add. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.c b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.c deleted file mode 100644 index 193eb0c44..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.c +++ /dev/null @@ -1,443 +0,0 @@ -static void femul(uint64_t out[8], const uint64_t in1[8], const uint64_t in2[8]) { - { const uint64_t x16 = in1[7]; - { const uint64_t x17 = in1[6]; - { const uint64_t x15 = in1[5]; - { const uint64_t x13 = in1[4]; - { const uint64_t x11 = in1[3]; - { const uint64_t x9 = in1[2]; - { const uint64_t x7 = in1[1]; - { const uint64_t x5 = in1[0]; - { const uint64_t x30 = in2[7]; - { const uint64_t x31 = in2[6]; - { const uint64_t x29 = in2[5]; - { const uint64_t x27 = in2[4]; - { const uint64_t x25 = in2[3]; - { const uint64_t x23 = in2[2]; - { const uint64_t x21 = in2[1]; - { const uint64_t x19 = in2[0]; - { uint64_t x34; uint64_t x33 = _mulx_u64(x5, x19, &x34); - { uint64_t x37; uint64_t x36 = _mulx_u64(x5, x21, &x37); - { uint64_t x40; uint64_t x39 = _mulx_u64(x5, x23, &x40); - { uint64_t x43; uint64_t x42 = _mulx_u64(x5, x25, &x43); - { uint64_t x46; uint64_t x45 = _mulx_u64(x5, x27, &x46); - { uint64_t x49; uint64_t x48 = _mulx_u64(x5, x29, &x49); - { uint64_t x52; uint64_t x51 = _mulx_u64(x5, x31, &x52); - { uint64_t x55; uint64_t x54 = _mulx_u64(x5, x30, &x55); - { uint64_t x57; uint8_t x58 = _addcarryx_u64(0x0, x34, x36, &x57); - { uint64_t x60; uint8_t x61 = _addcarryx_u64(x58, x37, x39, &x60); - { uint64_t x63; uint8_t x64 = _addcarryx_u64(x61, x40, x42, &x63); - { uint64_t x66; uint8_t x67 = _addcarryx_u64(x64, x43, x45, &x66); - { uint64_t x69; uint8_t x70 = _addcarryx_u64(x67, x46, x48, &x69); - { uint64_t x72; uint8_t x73 = _addcarryx_u64(x70, x49, x51, &x72); - { uint64_t x75; uint8_t x76 = _addcarryx_u64(x73, x52, x54, &x75); - { uint64_t x78; uint8_t _ = _addcarryx_u64(0x0, x76, x55, &x78); - { uint64_t x82; uint64_t x81 = _mulx_u64(x33, 0xffffffffffffffffL, &x82); - { uint64_t x85; uint64_t x84 = _mulx_u64(x33, 0xffffffffffffffffL, &x85); - { uint64_t x88; uint64_t x87 = _mulx_u64(x33, 0xffffffffffffffffL, &x88); - { uint64_t x91; uint64_t x90 = _mulx_u64(x33, 0xffffffffffffffffL, &x91); - { uint64_t x94; uint64_t x93 = _mulx_u64(x33, 0xffffffffffffffffL, &x94); - { uint64_t x97; uint64_t x96 = _mulx_u64(x33, 0xffffffffffffffffL, &x97); - { uint64_t x100; uint64_t x99 = _mulx_u64(x33, 0xffffffffffffffffL, &x100); - { uint64_t x103; uint64_t x102 = _mulx_u64(x33, 0x3eddffffffffffff, &x103); - { uint64_t x105; uint8_t x106 = _addcarryx_u64(0x0, x82, x84, &x105); - { uint64_t x108; uint8_t x109 = _addcarryx_u64(x106, x85, x87, &x108); - { uint64_t x111; uint8_t x112 = _addcarryx_u64(x109, x88, x90, &x111); - { uint64_t x114; uint8_t x115 = _addcarryx_u64(x112, x91, x93, &x114); - { uint64_t x117; uint8_t x118 = _addcarryx_u64(x115, x94, x96, &x117); - { uint64_t x120; uint8_t x121 = _addcarryx_u64(x118, x97, x99, &x120); - { uint64_t x123; uint8_t x124 = _addcarryx_u64(x121, x100, x102, &x123); - { uint64_t x126; uint8_t _ = _addcarryx_u64(0x0, x124, x103, &x126); - { uint64_t _; uint8_t x130 = _addcarryx_u64(0x0, x33, x81, &_); - { uint64_t x132; uint8_t x133 = _addcarryx_u64(x130, x57, x105, &x132); - { uint64_t x135; uint8_t x136 = _addcarryx_u64(x133, x60, x108, &x135); - { uint64_t x138; uint8_t x139 = _addcarryx_u64(x136, x63, x111, &x138); - { uint64_t x141; uint8_t x142 = _addcarryx_u64(x139, x66, x114, &x141); - { uint64_t x144; uint8_t x145 = _addcarryx_u64(x142, x69, x117, &x144); - { uint64_t x147; uint8_t x148 = _addcarryx_u64(x145, x72, x120, &x147); - { uint64_t x150; uint8_t x151 = _addcarryx_u64(x148, x75, x123, &x150); - { uint64_t x153; uint8_t x154 = _addcarryx_u64(x151, x78, x126, &x153); - { uint8_t x155 = (x154 + 0x0); - { uint64_t x158; uint64_t x157 = _mulx_u64(x7, x19, &x158); - { uint64_t x161; uint64_t x160 = _mulx_u64(x7, x21, &x161); - { uint64_t x164; uint64_t x163 = _mulx_u64(x7, x23, &x164); - { uint64_t x167; uint64_t x166 = _mulx_u64(x7, x25, &x167); - { uint64_t x170; uint64_t x169 = _mulx_u64(x7, x27, &x170); - { uint64_t x173; uint64_t x172 = _mulx_u64(x7, x29, &x173); - { uint64_t x176; uint64_t x175 = _mulx_u64(x7, x31, &x176); - { uint64_t x179; uint64_t x178 = _mulx_u64(x7, x30, &x179); - { uint64_t x181; uint8_t x182 = _addcarryx_u64(0x0, x158, x160, &x181); - { uint64_t x184; uint8_t x185 = _addcarryx_u64(x182, x161, x163, &x184); - { uint64_t x187; uint8_t x188 = _addcarryx_u64(x185, x164, x166, &x187); - { uint64_t x190; uint8_t x191 = _addcarryx_u64(x188, x167, x169, &x190); - { uint64_t x193; uint8_t x194 = _addcarryx_u64(x191, x170, x172, &x193); - { uint64_t x196; uint8_t x197 = _addcarryx_u64(x194, x173, x175, &x196); - { uint64_t x199; uint8_t x200 = _addcarryx_u64(x197, x176, x178, &x199); - { uint64_t x202; uint8_t _ = _addcarryx_u64(0x0, x200, x179, &x202); - { uint64_t x205; uint8_t x206 = _addcarryx_u64(0x0, x132, x157, &x205); - { uint64_t x208; uint8_t x209 = _addcarryx_u64(x206, x135, x181, &x208); - { uint64_t x211; uint8_t x212 = _addcarryx_u64(x209, x138, x184, &x211); - { uint64_t x214; uint8_t x215 = _addcarryx_u64(x212, x141, x187, &x214); - { uint64_t x217; uint8_t x218 = _addcarryx_u64(x215, x144, x190, &x217); - { uint64_t x220; uint8_t x221 = _addcarryx_u64(x218, x147, x193, &x220); - { uint64_t x223; uint8_t x224 = _addcarryx_u64(x221, x150, x196, &x223); - { uint64_t x226; uint8_t x227 = _addcarryx_u64(x224, x153, x199, &x226); - { uint64_t x229; uint8_t x230 = _addcarryx_u64(x227, x155, x202, &x229); - { uint64_t x233; uint64_t x232 = _mulx_u64(x205, 0xffffffffffffffffL, &x233); - { uint64_t x236; uint64_t x235 = _mulx_u64(x205, 0xffffffffffffffffL, &x236); - { uint64_t x239; uint64_t x238 = _mulx_u64(x205, 0xffffffffffffffffL, &x239); - { uint64_t x242; uint64_t x241 = _mulx_u64(x205, 0xffffffffffffffffL, &x242); - { uint64_t x245; uint64_t x244 = _mulx_u64(x205, 0xffffffffffffffffL, &x245); - { uint64_t x248; uint64_t x247 = _mulx_u64(x205, 0xffffffffffffffffL, &x248); - { uint64_t x251; uint64_t x250 = _mulx_u64(x205, 0xffffffffffffffffL, &x251); - { uint64_t x254; uint64_t x253 = _mulx_u64(x205, 0x3eddffffffffffff, &x254); - { uint64_t x256; uint8_t x257 = _addcarryx_u64(0x0, x233, x235, &x256); - { uint64_t x259; uint8_t x260 = _addcarryx_u64(x257, x236, x238, &x259); - { uint64_t x262; uint8_t x263 = _addcarryx_u64(x260, x239, x241, &x262); - { uint64_t x265; uint8_t x266 = _addcarryx_u64(x263, x242, x244, &x265); - { uint64_t x268; uint8_t x269 = _addcarryx_u64(x266, x245, x247, &x268); - { uint64_t x271; uint8_t x272 = _addcarryx_u64(x269, x248, x250, &x271); - { uint64_t x274; uint8_t x275 = _addcarryx_u64(x272, x251, x253, &x274); - { uint64_t x277; uint8_t _ = _addcarryx_u64(0x0, x275, x254, &x277); - { uint64_t _; uint8_t x281 = _addcarryx_u64(0x0, x205, x232, &_); - { uint64_t x283; uint8_t x284 = _addcarryx_u64(x281, x208, x256, &x283); - { uint64_t x286; uint8_t x287 = _addcarryx_u64(x284, x211, x259, &x286); - { uint64_t x289; uint8_t x290 = _addcarryx_u64(x287, x214, x262, &x289); - { uint64_t x292; uint8_t x293 = _addcarryx_u64(x290, x217, x265, &x292); - { uint64_t x295; uint8_t x296 = _addcarryx_u64(x293, x220, x268, &x295); - { uint64_t x298; uint8_t x299 = _addcarryx_u64(x296, x223, x271, &x298); - { uint64_t x301; uint8_t x302 = _addcarryx_u64(x299, x226, x274, &x301); - { uint64_t x304; uint8_t x305 = _addcarryx_u64(x302, x229, x277, &x304); - { uint8_t x306 = (x305 + x230); - { uint64_t x309; uint64_t x308 = _mulx_u64(x9, x19, &x309); - { uint64_t x312; uint64_t x311 = _mulx_u64(x9, x21, &x312); - { uint64_t x315; uint64_t x314 = _mulx_u64(x9, x23, &x315); - { uint64_t x318; uint64_t x317 = _mulx_u64(x9, x25, &x318); - { uint64_t x321; uint64_t x320 = _mulx_u64(x9, x27, &x321); - { uint64_t x324; uint64_t x323 = _mulx_u64(x9, x29, &x324); - { uint64_t x327; uint64_t x326 = _mulx_u64(x9, x31, &x327); - { uint64_t x330; uint64_t x329 = _mulx_u64(x9, x30, &x330); - { uint64_t x332; uint8_t x333 = _addcarryx_u64(0x0, x309, x311, &x332); - { uint64_t x335; uint8_t x336 = _addcarryx_u64(x333, x312, x314, &x335); - { uint64_t x338; uint8_t x339 = _addcarryx_u64(x336, x315, x317, &x338); - { uint64_t x341; uint8_t x342 = _addcarryx_u64(x339, x318, x320, &x341); - { uint64_t x344; uint8_t x345 = _addcarryx_u64(x342, x321, x323, &x344); - { uint64_t x347; uint8_t x348 = _addcarryx_u64(x345, x324, x326, &x347); - { uint64_t x350; uint8_t x351 = _addcarryx_u64(x348, x327, x329, &x350); - { uint64_t x353; uint8_t _ = _addcarryx_u64(0x0, x351, x330, &x353); - { uint64_t x356; uint8_t x357 = _addcarryx_u64(0x0, x283, x308, &x356); - { uint64_t x359; uint8_t x360 = _addcarryx_u64(x357, x286, x332, &x359); - { uint64_t x362; uint8_t x363 = _addcarryx_u64(x360, x289, x335, &x362); - { uint64_t x365; uint8_t x366 = _addcarryx_u64(x363, x292, x338, &x365); - { uint64_t x368; uint8_t x369 = _addcarryx_u64(x366, x295, x341, &x368); - { uint64_t x371; uint8_t x372 = _addcarryx_u64(x369, x298, x344, &x371); - { uint64_t x374; uint8_t x375 = _addcarryx_u64(x372, x301, x347, &x374); - { uint64_t x377; uint8_t x378 = _addcarryx_u64(x375, x304, x350, &x377); - { uint64_t x380; uint8_t x381 = _addcarryx_u64(x378, x306, x353, &x380); - { uint64_t x384; uint64_t x383 = _mulx_u64(x356, 0xffffffffffffffffL, &x384); - { uint64_t x387; uint64_t x386 = _mulx_u64(x356, 0xffffffffffffffffL, &x387); - { uint64_t x390; uint64_t x389 = _mulx_u64(x356, 0xffffffffffffffffL, &x390); - { uint64_t x393; uint64_t x392 = _mulx_u64(x356, 0xffffffffffffffffL, &x393); - { uint64_t x396; uint64_t x395 = _mulx_u64(x356, 0xffffffffffffffffL, &x396); - { uint64_t x399; uint64_t x398 = _mulx_u64(x356, 0xffffffffffffffffL, &x399); - { uint64_t x402; uint64_t x401 = _mulx_u64(x356, 0xffffffffffffffffL, &x402); - { uint64_t x405; uint64_t x404 = _mulx_u64(x356, 0x3eddffffffffffff, &x405); - { uint64_t x407; uint8_t x408 = _addcarryx_u64(0x0, x384, x386, &x407); - { uint64_t x410; uint8_t x411 = _addcarryx_u64(x408, x387, x389, &x410); - { uint64_t x413; uint8_t x414 = _addcarryx_u64(x411, x390, x392, &x413); - { uint64_t x416; uint8_t x417 = _addcarryx_u64(x414, x393, x395, &x416); - { uint64_t x419; uint8_t x420 = _addcarryx_u64(x417, x396, x398, &x419); - { uint64_t x422; uint8_t x423 = _addcarryx_u64(x420, x399, x401, &x422); - { uint64_t x425; uint8_t x426 = _addcarryx_u64(x423, x402, x404, &x425); - { uint64_t x428; uint8_t _ = _addcarryx_u64(0x0, x426, x405, &x428); - { uint64_t _; uint8_t x432 = _addcarryx_u64(0x0, x356, x383, &_); - { uint64_t x434; uint8_t x435 = _addcarryx_u64(x432, x359, x407, &x434); - { uint64_t x437; uint8_t x438 = _addcarryx_u64(x435, x362, x410, &x437); - { uint64_t x440; uint8_t x441 = _addcarryx_u64(x438, x365, x413, &x440); - { uint64_t x443; uint8_t x444 = _addcarryx_u64(x441, x368, x416, &x443); - { uint64_t x446; uint8_t x447 = _addcarryx_u64(x444, x371, x419, &x446); - { uint64_t x449; uint8_t x450 = _addcarryx_u64(x447, x374, x422, &x449); - { uint64_t x452; uint8_t x453 = _addcarryx_u64(x450, x377, x425, &x452); - { uint64_t x455; uint8_t x456 = _addcarryx_u64(x453, x380, x428, &x455); - { uint8_t x457 = (x456 + x381); - { uint64_t x460; uint64_t x459 = _mulx_u64(x11, x19, &x460); - { uint64_t x463; uint64_t x462 = _mulx_u64(x11, x21, &x463); - { uint64_t x466; uint64_t x465 = _mulx_u64(x11, x23, &x466); - { uint64_t x469; uint64_t x468 = _mulx_u64(x11, x25, &x469); - { uint64_t x472; uint64_t x471 = _mulx_u64(x11, x27, &x472); - { uint64_t x475; uint64_t x474 = _mulx_u64(x11, x29, &x475); - { uint64_t x478; uint64_t x477 = _mulx_u64(x11, x31, &x478); - { uint64_t x481; uint64_t x480 = _mulx_u64(x11, x30, &x481); - { uint64_t x483; uint8_t x484 = _addcarryx_u64(0x0, x460, x462, &x483); - { uint64_t x486; uint8_t x487 = _addcarryx_u64(x484, x463, x465, &x486); - { uint64_t x489; uint8_t x490 = _addcarryx_u64(x487, x466, x468, &x489); - { uint64_t x492; uint8_t x493 = _addcarryx_u64(x490, x469, x471, &x492); - { uint64_t x495; uint8_t x496 = _addcarryx_u64(x493, x472, x474, &x495); - { uint64_t x498; uint8_t x499 = _addcarryx_u64(x496, x475, x477, &x498); - { uint64_t x501; uint8_t x502 = _addcarryx_u64(x499, x478, x480, &x501); - { uint64_t x504; uint8_t _ = _addcarryx_u64(0x0, x502, x481, &x504); - { uint64_t x507; uint8_t x508 = _addcarryx_u64(0x0, x434, x459, &x507); - { uint64_t x510; uint8_t x511 = _addcarryx_u64(x508, x437, x483, &x510); - { uint64_t x513; uint8_t x514 = _addcarryx_u64(x511, x440, x486, &x513); - { uint64_t x516; uint8_t x517 = _addcarryx_u64(x514, x443, x489, &x516); - { uint64_t x519; uint8_t x520 = _addcarryx_u64(x517, x446, x492, &x519); - { uint64_t x522; uint8_t x523 = _addcarryx_u64(x520, x449, x495, &x522); - { uint64_t x525; uint8_t x526 = _addcarryx_u64(x523, x452, x498, &x525); - { uint64_t x528; uint8_t x529 = _addcarryx_u64(x526, x455, x501, &x528); - { uint64_t x531; uint8_t x532 = _addcarryx_u64(x529, x457, x504, &x531); - { uint64_t x535; uint64_t x534 = _mulx_u64(x507, 0xffffffffffffffffL, &x535); - { uint64_t x538; uint64_t x537 = _mulx_u64(x507, 0xffffffffffffffffL, &x538); - { uint64_t x541; uint64_t x540 = _mulx_u64(x507, 0xffffffffffffffffL, &x541); - { uint64_t x544; uint64_t x543 = _mulx_u64(x507, 0xffffffffffffffffL, &x544); - { uint64_t x547; uint64_t x546 = _mulx_u64(x507, 0xffffffffffffffffL, &x547); - { uint64_t x550; uint64_t x549 = _mulx_u64(x507, 0xffffffffffffffffL, &x550); - { uint64_t x553; uint64_t x552 = _mulx_u64(x507, 0xffffffffffffffffL, &x553); - { uint64_t x556; uint64_t x555 = _mulx_u64(x507, 0x3eddffffffffffff, &x556); - { uint64_t x558; uint8_t x559 = _addcarryx_u64(0x0, x535, x537, &x558); - { uint64_t x561; uint8_t x562 = _addcarryx_u64(x559, x538, x540, &x561); - { uint64_t x564; uint8_t x565 = _addcarryx_u64(x562, x541, x543, &x564); - { uint64_t x567; uint8_t x568 = _addcarryx_u64(x565, x544, x546, &x567); - { uint64_t x570; uint8_t x571 = _addcarryx_u64(x568, x547, x549, &x570); - { uint64_t x573; uint8_t x574 = _addcarryx_u64(x571, x550, x552, &x573); - { uint64_t x576; uint8_t x577 = _addcarryx_u64(x574, x553, x555, &x576); - { uint64_t x579; uint8_t _ = _addcarryx_u64(0x0, x577, x556, &x579); - { uint64_t _; uint8_t x583 = _addcarryx_u64(0x0, x507, x534, &_); - { uint64_t x585; uint8_t x586 = _addcarryx_u64(x583, x510, x558, &x585); - { uint64_t x588; uint8_t x589 = _addcarryx_u64(x586, x513, x561, &x588); - { uint64_t x591; uint8_t x592 = _addcarryx_u64(x589, x516, x564, &x591); - { uint64_t x594; uint8_t x595 = _addcarryx_u64(x592, x519, x567, &x594); - { uint64_t x597; uint8_t x598 = _addcarryx_u64(x595, x522, x570, &x597); - { uint64_t x600; uint8_t x601 = _addcarryx_u64(x598, x525, x573, &x600); - { uint64_t x603; uint8_t x604 = _addcarryx_u64(x601, x528, x576, &x603); - { uint64_t x606; uint8_t x607 = _addcarryx_u64(x604, x531, x579, &x606); - { uint8_t x608 = (x607 + x532); - { uint64_t x611; uint64_t x610 = _mulx_u64(x13, x19, &x611); - { uint64_t x614; uint64_t x613 = _mulx_u64(x13, x21, &x614); - { uint64_t x617; uint64_t x616 = _mulx_u64(x13, x23, &x617); - { uint64_t x620; uint64_t x619 = _mulx_u64(x13, x25, &x620); - { uint64_t x623; uint64_t x622 = _mulx_u64(x13, x27, &x623); - { uint64_t x626; uint64_t x625 = _mulx_u64(x13, x29, &x626); - { uint64_t x629; uint64_t x628 = _mulx_u64(x13, x31, &x629); - { uint64_t x632; uint64_t x631 = _mulx_u64(x13, x30, &x632); - { uint64_t x634; uint8_t x635 = _addcarryx_u64(0x0, x611, x613, &x634); - { uint64_t x637; uint8_t x638 = _addcarryx_u64(x635, x614, x616, &x637); - { uint64_t x640; uint8_t x641 = _addcarryx_u64(x638, x617, x619, &x640); - { uint64_t x643; uint8_t x644 = _addcarryx_u64(x641, x620, x622, &x643); - { uint64_t x646; uint8_t x647 = _addcarryx_u64(x644, x623, x625, &x646); - { uint64_t x649; uint8_t x650 = _addcarryx_u64(x647, x626, x628, &x649); - { uint64_t x652; uint8_t x653 = _addcarryx_u64(x650, x629, x631, &x652); - { uint64_t x655; uint8_t _ = _addcarryx_u64(0x0, x653, x632, &x655); - { uint64_t x658; uint8_t x659 = _addcarryx_u64(0x0, x585, x610, &x658); - { uint64_t x661; uint8_t x662 = _addcarryx_u64(x659, x588, x634, &x661); - { uint64_t x664; uint8_t x665 = _addcarryx_u64(x662, x591, x637, &x664); - { uint64_t x667; uint8_t x668 = _addcarryx_u64(x665, x594, x640, &x667); - { uint64_t x670; uint8_t x671 = _addcarryx_u64(x668, x597, x643, &x670); - { uint64_t x673; uint8_t x674 = _addcarryx_u64(x671, x600, x646, &x673); - { uint64_t x676; uint8_t x677 = _addcarryx_u64(x674, x603, x649, &x676); - { uint64_t x679; uint8_t x680 = _addcarryx_u64(x677, x606, x652, &x679); - { uint64_t x682; uint8_t x683 = _addcarryx_u64(x680, x608, x655, &x682); - { uint64_t x686; uint64_t x685 = _mulx_u64(x658, 0xffffffffffffffffL, &x686); - { uint64_t x689; uint64_t x688 = _mulx_u64(x658, 0xffffffffffffffffL, &x689); - { uint64_t x692; uint64_t x691 = _mulx_u64(x658, 0xffffffffffffffffL, &x692); - { uint64_t x695; uint64_t x694 = _mulx_u64(x658, 0xffffffffffffffffL, &x695); - { uint64_t x698; uint64_t x697 = _mulx_u64(x658, 0xffffffffffffffffL, &x698); - { uint64_t x701; uint64_t x700 = _mulx_u64(x658, 0xffffffffffffffffL, &x701); - { uint64_t x704; uint64_t x703 = _mulx_u64(x658, 0xffffffffffffffffL, &x704); - { uint64_t x707; uint64_t x706 = _mulx_u64(x658, 0x3eddffffffffffff, &x707); - { uint64_t x709; uint8_t x710 = _addcarryx_u64(0x0, x686, x688, &x709); - { uint64_t x712; uint8_t x713 = _addcarryx_u64(x710, x689, x691, &x712); - { uint64_t x715; uint8_t x716 = _addcarryx_u64(x713, x692, x694, &x715); - { uint64_t x718; uint8_t x719 = _addcarryx_u64(x716, x695, x697, &x718); - { uint64_t x721; uint8_t x722 = _addcarryx_u64(x719, x698, x700, &x721); - { uint64_t x724; uint8_t x725 = _addcarryx_u64(x722, x701, x703, &x724); - { uint64_t x727; uint8_t x728 = _addcarryx_u64(x725, x704, x706, &x727); - { uint64_t x730; uint8_t _ = _addcarryx_u64(0x0, x728, x707, &x730); - { uint64_t _; uint8_t x734 = _addcarryx_u64(0x0, x658, x685, &_); - { uint64_t x736; uint8_t x737 = _addcarryx_u64(x734, x661, x709, &x736); - { uint64_t x739; uint8_t x740 = _addcarryx_u64(x737, x664, x712, &x739); - { uint64_t x742; uint8_t x743 = _addcarryx_u64(x740, x667, x715, &x742); - { uint64_t x745; uint8_t x746 = _addcarryx_u64(x743, x670, x718, &x745); - { uint64_t x748; uint8_t x749 = _addcarryx_u64(x746, x673, x721, &x748); - { uint64_t x751; uint8_t x752 = _addcarryx_u64(x749, x676, x724, &x751); - { uint64_t x754; uint8_t x755 = _addcarryx_u64(x752, x679, x727, &x754); - { uint64_t x757; uint8_t x758 = _addcarryx_u64(x755, x682, x730, &x757); - { uint8_t x759 = (x758 + x683); - { uint64_t x762; uint64_t x761 = _mulx_u64(x15, x19, &x762); - { uint64_t x765; uint64_t x764 = _mulx_u64(x15, x21, &x765); - { uint64_t x768; uint64_t x767 = _mulx_u64(x15, x23, &x768); - { uint64_t x771; uint64_t x770 = _mulx_u64(x15, x25, &x771); - { uint64_t x774; uint64_t x773 = _mulx_u64(x15, x27, &x774); - { uint64_t x777; uint64_t x776 = _mulx_u64(x15, x29, &x777); - { uint64_t x780; uint64_t x779 = _mulx_u64(x15, x31, &x780); - { uint64_t x783; uint64_t x782 = _mulx_u64(x15, x30, &x783); - { uint64_t x785; uint8_t x786 = _addcarryx_u64(0x0, x762, x764, &x785); - { uint64_t x788; uint8_t x789 = _addcarryx_u64(x786, x765, x767, &x788); - { uint64_t x791; uint8_t x792 = _addcarryx_u64(x789, x768, x770, &x791); - { uint64_t x794; uint8_t x795 = _addcarryx_u64(x792, x771, x773, &x794); - { uint64_t x797; uint8_t x798 = _addcarryx_u64(x795, x774, x776, &x797); - { uint64_t x800; uint8_t x801 = _addcarryx_u64(x798, x777, x779, &x800); - { uint64_t x803; uint8_t x804 = _addcarryx_u64(x801, x780, x782, &x803); - { uint64_t x806; uint8_t _ = _addcarryx_u64(0x0, x804, x783, &x806); - { uint64_t x809; uint8_t x810 = _addcarryx_u64(0x0, x736, x761, &x809); - { uint64_t x812; uint8_t x813 = _addcarryx_u64(x810, x739, x785, &x812); - { uint64_t x815; uint8_t x816 = _addcarryx_u64(x813, x742, x788, &x815); - { uint64_t x818; uint8_t x819 = _addcarryx_u64(x816, x745, x791, &x818); - { uint64_t x821; uint8_t x822 = _addcarryx_u64(x819, x748, x794, &x821); - { uint64_t x824; uint8_t x825 = _addcarryx_u64(x822, x751, x797, &x824); - { uint64_t x827; uint8_t x828 = _addcarryx_u64(x825, x754, x800, &x827); - { uint64_t x830; uint8_t x831 = _addcarryx_u64(x828, x757, x803, &x830); - { uint64_t x833; uint8_t x834 = _addcarryx_u64(x831, x759, x806, &x833); - { uint64_t x837; uint64_t x836 = _mulx_u64(x809, 0xffffffffffffffffL, &x837); - { uint64_t x840; uint64_t x839 = _mulx_u64(x809, 0xffffffffffffffffL, &x840); - { uint64_t x843; uint64_t x842 = _mulx_u64(x809, 0xffffffffffffffffL, &x843); - { uint64_t x846; uint64_t x845 = _mulx_u64(x809, 0xffffffffffffffffL, &x846); - { uint64_t x849; uint64_t x848 = _mulx_u64(x809, 0xffffffffffffffffL, &x849); - { uint64_t x852; uint64_t x851 = _mulx_u64(x809, 0xffffffffffffffffL, &x852); - { uint64_t x855; uint64_t x854 = _mulx_u64(x809, 0xffffffffffffffffL, &x855); - { uint64_t x858; uint64_t x857 = _mulx_u64(x809, 0x3eddffffffffffff, &x858); - { uint64_t x860; uint8_t x861 = _addcarryx_u64(0x0, x837, x839, &x860); - { uint64_t x863; uint8_t x864 = _addcarryx_u64(x861, x840, x842, &x863); - { uint64_t x866; uint8_t x867 = _addcarryx_u64(x864, x843, x845, &x866); - { uint64_t x869; uint8_t x870 = _addcarryx_u64(x867, x846, x848, &x869); - { uint64_t x872; uint8_t x873 = _addcarryx_u64(x870, x849, x851, &x872); - { uint64_t x875; uint8_t x876 = _addcarryx_u64(x873, x852, x854, &x875); - { uint64_t x878; uint8_t x879 = _addcarryx_u64(x876, x855, x857, &x878); - { uint64_t x881; uint8_t _ = _addcarryx_u64(0x0, x879, x858, &x881); - { uint64_t _; uint8_t x885 = _addcarryx_u64(0x0, x809, x836, &_); - { uint64_t x887; uint8_t x888 = _addcarryx_u64(x885, x812, x860, &x887); - { uint64_t x890; uint8_t x891 = _addcarryx_u64(x888, x815, x863, &x890); - { uint64_t x893; uint8_t x894 = _addcarryx_u64(x891, x818, x866, &x893); - { uint64_t x896; uint8_t x897 = _addcarryx_u64(x894, x821, x869, &x896); - { uint64_t x899; uint8_t x900 = _addcarryx_u64(x897, x824, x872, &x899); - { uint64_t x902; uint8_t x903 = _addcarryx_u64(x900, x827, x875, &x902); - { uint64_t x905; uint8_t x906 = _addcarryx_u64(x903, x830, x878, &x905); - { uint64_t x908; uint8_t x909 = _addcarryx_u64(x906, x833, x881, &x908); - { uint8_t x910 = (x909 + x834); - { uint64_t x913; uint64_t x912 = _mulx_u64(x17, x19, &x913); - { uint64_t x916; uint64_t x915 = _mulx_u64(x17, x21, &x916); - { uint64_t x919; uint64_t x918 = _mulx_u64(x17, x23, &x919); - { uint64_t x922; uint64_t x921 = _mulx_u64(x17, x25, &x922); - { uint64_t x925; uint64_t x924 = _mulx_u64(x17, x27, &x925); - { uint64_t x928; uint64_t x927 = _mulx_u64(x17, x29, &x928); - { uint64_t x931; uint64_t x930 = _mulx_u64(x17, x31, &x931); - { uint64_t x934; uint64_t x933 = _mulx_u64(x17, x30, &x934); - { uint64_t x936; uint8_t x937 = _addcarryx_u64(0x0, x913, x915, &x936); - { uint64_t x939; uint8_t x940 = _addcarryx_u64(x937, x916, x918, &x939); - { uint64_t x942; uint8_t x943 = _addcarryx_u64(x940, x919, x921, &x942); - { uint64_t x945; uint8_t x946 = _addcarryx_u64(x943, x922, x924, &x945); - { uint64_t x948; uint8_t x949 = _addcarryx_u64(x946, x925, x927, &x948); - { uint64_t x951; uint8_t x952 = _addcarryx_u64(x949, x928, x930, &x951); - { uint64_t x954; uint8_t x955 = _addcarryx_u64(x952, x931, x933, &x954); - { uint64_t x957; uint8_t _ = _addcarryx_u64(0x0, x955, x934, &x957); - { uint64_t x960; uint8_t x961 = _addcarryx_u64(0x0, x887, x912, &x960); - { uint64_t x963; uint8_t x964 = _addcarryx_u64(x961, x890, x936, &x963); - { uint64_t x966; uint8_t x967 = _addcarryx_u64(x964, x893, x939, &x966); - { uint64_t x969; uint8_t x970 = _addcarryx_u64(x967, x896, x942, &x969); - { uint64_t x972; uint8_t x973 = _addcarryx_u64(x970, x899, x945, &x972); - { uint64_t x975; uint8_t x976 = _addcarryx_u64(x973, x902, x948, &x975); - { uint64_t x978; uint8_t x979 = _addcarryx_u64(x976, x905, x951, &x978); - { uint64_t x981; uint8_t x982 = _addcarryx_u64(x979, x908, x954, &x981); - { uint64_t x984; uint8_t x985 = _addcarryx_u64(x982, x910, x957, &x984); - { uint64_t x988; uint64_t x987 = _mulx_u64(x960, 0xffffffffffffffffL, &x988); - { uint64_t x991; uint64_t x990 = _mulx_u64(x960, 0xffffffffffffffffL, &x991); - { uint64_t x994; uint64_t x993 = _mulx_u64(x960, 0xffffffffffffffffL, &x994); - { uint64_t x997; uint64_t x996 = _mulx_u64(x960, 0xffffffffffffffffL, &x997); - { uint64_t x1000; uint64_t x999 = _mulx_u64(x960, 0xffffffffffffffffL, &x1000); - { uint64_t x1003; uint64_t x1002 = _mulx_u64(x960, 0xffffffffffffffffL, &x1003); - { uint64_t x1006; uint64_t x1005 = _mulx_u64(x960, 0xffffffffffffffffL, &x1006); - { uint64_t x1009; uint64_t x1008 = _mulx_u64(x960, 0x3eddffffffffffff, &x1009); - { uint64_t x1011; uint8_t x1012 = _addcarryx_u64(0x0, x988, x990, &x1011); - { uint64_t x1014; uint8_t x1015 = _addcarryx_u64(x1012, x991, x993, &x1014); - { uint64_t x1017; uint8_t x1018 = _addcarryx_u64(x1015, x994, x996, &x1017); - { uint64_t x1020; uint8_t x1021 = _addcarryx_u64(x1018, x997, x999, &x1020); - { uint64_t x1023; uint8_t x1024 = _addcarryx_u64(x1021, x1000, x1002, &x1023); - { uint64_t x1026; uint8_t x1027 = _addcarryx_u64(x1024, x1003, x1005, &x1026); - { uint64_t x1029; uint8_t x1030 = _addcarryx_u64(x1027, x1006, x1008, &x1029); - { uint64_t x1032; uint8_t _ = _addcarryx_u64(0x0, x1030, x1009, &x1032); - { uint64_t _; uint8_t x1036 = _addcarryx_u64(0x0, x960, x987, &_); - { uint64_t x1038; uint8_t x1039 = _addcarryx_u64(x1036, x963, x1011, &x1038); - { uint64_t x1041; uint8_t x1042 = _addcarryx_u64(x1039, x966, x1014, &x1041); - { uint64_t x1044; uint8_t x1045 = _addcarryx_u64(x1042, x969, x1017, &x1044); - { uint64_t x1047; uint8_t x1048 = _addcarryx_u64(x1045, x972, x1020, &x1047); - { uint64_t x1050; uint8_t x1051 = _addcarryx_u64(x1048, x975, x1023, &x1050); - { uint64_t x1053; uint8_t x1054 = _addcarryx_u64(x1051, x978, x1026, &x1053); - { uint64_t x1056; uint8_t x1057 = _addcarryx_u64(x1054, x981, x1029, &x1056); - { uint64_t x1059; uint8_t x1060 = _addcarryx_u64(x1057, x984, x1032, &x1059); - { uint8_t x1061 = (x1060 + x985); - { uint64_t x1064; uint64_t x1063 = _mulx_u64(x16, x19, &x1064); - { uint64_t x1067; uint64_t x1066 = _mulx_u64(x16, x21, &x1067); - { uint64_t x1070; uint64_t x1069 = _mulx_u64(x16, x23, &x1070); - { uint64_t x1073; uint64_t x1072 = _mulx_u64(x16, x25, &x1073); - { uint64_t x1076; uint64_t x1075 = _mulx_u64(x16, x27, &x1076); - { uint64_t x1079; uint64_t x1078 = _mulx_u64(x16, x29, &x1079); - { uint64_t x1082; uint64_t x1081 = _mulx_u64(x16, x31, &x1082); - { uint64_t x1085; uint64_t x1084 = _mulx_u64(x16, x30, &x1085); - { uint64_t x1087; uint8_t x1088 = _addcarryx_u64(0x0, x1064, x1066, &x1087); - { uint64_t x1090; uint8_t x1091 = _addcarryx_u64(x1088, x1067, x1069, &x1090); - { uint64_t x1093; uint8_t x1094 = _addcarryx_u64(x1091, x1070, x1072, &x1093); - { uint64_t x1096; uint8_t x1097 = _addcarryx_u64(x1094, x1073, x1075, &x1096); - { uint64_t x1099; uint8_t x1100 = _addcarryx_u64(x1097, x1076, x1078, &x1099); - { uint64_t x1102; uint8_t x1103 = _addcarryx_u64(x1100, x1079, x1081, &x1102); - { uint64_t x1105; uint8_t x1106 = _addcarryx_u64(x1103, x1082, x1084, &x1105); - { uint64_t x1108; uint8_t _ = _addcarryx_u64(0x0, x1106, x1085, &x1108); - { uint64_t x1111; uint8_t x1112 = _addcarryx_u64(0x0, x1038, x1063, &x1111); - { uint64_t x1114; uint8_t x1115 = _addcarryx_u64(x1112, x1041, x1087, &x1114); - { uint64_t x1117; uint8_t x1118 = _addcarryx_u64(x1115, x1044, x1090, &x1117); - { uint64_t x1120; uint8_t x1121 = _addcarryx_u64(x1118, x1047, x1093, &x1120); - { uint64_t x1123; uint8_t x1124 = _addcarryx_u64(x1121, x1050, x1096, &x1123); - { uint64_t x1126; uint8_t x1127 = _addcarryx_u64(x1124, x1053, x1099, &x1126); - { uint64_t x1129; uint8_t x1130 = _addcarryx_u64(x1127, x1056, x1102, &x1129); - { uint64_t x1132; uint8_t x1133 = _addcarryx_u64(x1130, x1059, x1105, &x1132); - { uint64_t x1135; uint8_t x1136 = _addcarryx_u64(x1133, x1061, x1108, &x1135); - { uint64_t x1139; uint64_t x1138 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1139); - { uint64_t x1142; uint64_t x1141 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1142); - { uint64_t x1145; uint64_t x1144 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1145); - { uint64_t x1148; uint64_t x1147 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1148); - { uint64_t x1151; uint64_t x1150 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1151); - { uint64_t x1154; uint64_t x1153 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1154); - { uint64_t x1157; uint64_t x1156 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1157); - { uint64_t x1160; uint64_t x1159 = _mulx_u64(x1111, 0x3eddffffffffffff, &x1160); - { uint64_t x1162; uint8_t x1163 = _addcarryx_u64(0x0, x1139, x1141, &x1162); - { uint64_t x1165; uint8_t x1166 = _addcarryx_u64(x1163, x1142, x1144, &x1165); - { uint64_t x1168; uint8_t x1169 = _addcarryx_u64(x1166, x1145, x1147, &x1168); - { uint64_t x1171; uint8_t x1172 = _addcarryx_u64(x1169, x1148, x1150, &x1171); - { uint64_t x1174; uint8_t x1175 = _addcarryx_u64(x1172, x1151, x1153, &x1174); - { uint64_t x1177; uint8_t x1178 = _addcarryx_u64(x1175, x1154, x1156, &x1177); - { uint64_t x1180; uint8_t x1181 = _addcarryx_u64(x1178, x1157, x1159, &x1180); - { uint64_t x1183; uint8_t _ = _addcarryx_u64(0x0, x1181, x1160, &x1183); - { uint64_t _; uint8_t x1187 = _addcarryx_u64(0x0, x1111, x1138, &_); - { uint64_t x1189; uint8_t x1190 = _addcarryx_u64(x1187, x1114, x1162, &x1189); - { uint64_t x1192; uint8_t x1193 = _addcarryx_u64(x1190, x1117, x1165, &x1192); - { uint64_t x1195; uint8_t x1196 = _addcarryx_u64(x1193, x1120, x1168, &x1195); - { uint64_t x1198; uint8_t x1199 = _addcarryx_u64(x1196, x1123, x1171, &x1198); - { uint64_t x1201; uint8_t x1202 = _addcarryx_u64(x1199, x1126, x1174, &x1201); - { uint64_t x1204; uint8_t x1205 = _addcarryx_u64(x1202, x1129, x1177, &x1204); - { uint64_t x1207; uint8_t x1208 = _addcarryx_u64(x1205, x1132, x1180, &x1207); - { uint64_t x1210; uint8_t x1211 = _addcarryx_u64(x1208, x1135, x1183, &x1210); - { uint8_t x1212 = (x1211 + x1136); - { uint64_t x1214; uint8_t x1215 = _subborrow_u64(0x0, x1189, 0xffffffffffffffffL, &x1214); - { uint64_t x1217; uint8_t x1218 = _subborrow_u64(x1215, x1192, 0xffffffffffffffffL, &x1217); - { uint64_t x1220; uint8_t x1221 = _subborrow_u64(x1218, x1195, 0xffffffffffffffffL, &x1220); - { uint64_t x1223; uint8_t x1224 = _subborrow_u64(x1221, x1198, 0xffffffffffffffffL, &x1223); - { uint64_t x1226; uint8_t x1227 = _subborrow_u64(x1224, x1201, 0xffffffffffffffffL, &x1226); - { uint64_t x1229; uint8_t x1230 = _subborrow_u64(x1227, x1204, 0xffffffffffffffffL, &x1229); - { uint64_t x1232; uint8_t x1233 = _subborrow_u64(x1230, x1207, 0xffffffffffffffffL, &x1232); - { uint64_t x1235; uint8_t x1236 = _subborrow_u64(x1233, x1210, 0x3eddffffffffffff, &x1235); - { uint64_t _; uint8_t x1239 = _subborrow_u64(x1236, x1212, 0x0, &_); - { uint64_t x1240 = cmovznz64(x1239, x1235, x1210); - { uint64_t x1241 = cmovznz64(x1239, x1232, x1207); - { uint64_t x1242 = cmovznz64(x1239, x1229, x1204); - { uint64_t x1243 = cmovznz64(x1239, x1226, x1201); - { uint64_t x1244 = cmovznz64(x1239, x1223, x1198); - { uint64_t x1245 = cmovznz64(x1239, x1220, x1195); - { uint64_t x1246 = cmovznz64(x1239, x1217, x1192); - { uint64_t x1247 = cmovznz64(x1239, x1214, x1189); - out[0] = x1247; - out[1] = x1246; - out[2] = x1245; - out[3] = x1244; - out[4] = x1243; - out[5] = x1242; - out[6] = x1241; - out[7] = x1240; - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.v deleted file mode 100644 index f374b9e73..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition mul : - { mul : feBW_small -> feBW_small -> feBW_small - | forall a b, phiM_small (mul a b) = F.mul (phiM_small a) (phiM_small b) }. -Proof. - Set Ltac Profiling. - Time synthesize_mul (). - Show Ltac Profile. -Time Defined. - -Print Assumptions mul. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femulDisplay.log b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femulDisplay.log deleted file mode 100644 index f5fee1792..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femulDisplay.log +++ /dev/null @@ -1,423 +0,0 @@ -λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core, - uint64_t x33, uint64_t x34 = mulx_u64(x5, x19); - uint64_t x36, uint64_t x37 = mulx_u64(x5, x21); - uint64_t x39, uint64_t x40 = mulx_u64(x5, x23); - uint64_t x42, uint64_t x43 = mulx_u64(x5, x25); - uint64_t x45, uint64_t x46 = mulx_u64(x5, x27); - uint64_t x48, uint64_t x49 = mulx_u64(x5, x29); - uint64_t x51, uint64_t x52 = mulx_u64(x5, x31); - uint64_t x54, uint64_t x55 = mulx_u64(x5, x30); - uint64_t x57, uint8_t x58 = addcarryx_u64(0x0, x34, x36); - uint64_t x60, uint8_t x61 = addcarryx_u64(x58, x37, x39); - uint64_t x63, uint8_t x64 = addcarryx_u64(x61, x40, x42); - uint64_t x66, uint8_t x67 = addcarryx_u64(x64, x43, x45); - uint64_t x69, uint8_t x70 = addcarryx_u64(x67, x46, x48); - uint64_t x72, uint8_t x73 = addcarryx_u64(x70, x49, x51); - uint64_t x75, uint8_t x76 = addcarryx_u64(x73, x52, x54); - uint64_t x78, uint8_t _ = addcarryx_u64(0x0, x76, x55); - uint64_t x81, uint64_t x82 = mulx_u64(x33, 0xffffffffffffffffL); - uint64_t x84, uint64_t x85 = mulx_u64(x33, 0xffffffffffffffffL); - uint64_t x87, uint64_t x88 = mulx_u64(x33, 0xffffffffffffffffL); - uint64_t x90, uint64_t x91 = mulx_u64(x33, 0xffffffffffffffffL); - uint64_t x93, uint64_t x94 = mulx_u64(x33, 0xffffffffffffffffL); - uint64_t x96, uint64_t x97 = mulx_u64(x33, 0xffffffffffffffffL); - uint64_t x99, uint64_t x100 = mulx_u64(x33, 0xffffffffffffffffL); - uint64_t x102, uint64_t x103 = mulx_u64(x33, 0x3eddffffffffffff); - uint64_t x105, uint8_t x106 = addcarryx_u64(0x0, x82, x84); - uint64_t x108, uint8_t x109 = addcarryx_u64(x106, x85, x87); - uint64_t x111, uint8_t x112 = addcarryx_u64(x109, x88, x90); - uint64_t x114, uint8_t x115 = addcarryx_u64(x112, x91, x93); - uint64_t x117, uint8_t x118 = addcarryx_u64(x115, x94, x96); - uint64_t x120, uint8_t x121 = addcarryx_u64(x118, x97, x99); - uint64_t x123, uint8_t x124 = addcarryx_u64(x121, x100, x102); - uint64_t x126, uint8_t _ = addcarryx_u64(0x0, x124, x103); - uint64_t _, uint8_t x130 = addcarryx_u64(0x0, x33, x81); - uint64_t x132, uint8_t x133 = addcarryx_u64(x130, x57, x105); - uint64_t x135, uint8_t x136 = addcarryx_u64(x133, x60, x108); - uint64_t x138, uint8_t x139 = addcarryx_u64(x136, x63, x111); - uint64_t x141, uint8_t x142 = addcarryx_u64(x139, x66, x114); - uint64_t x144, uint8_t x145 = addcarryx_u64(x142, x69, x117); - uint64_t x147, uint8_t x148 = addcarryx_u64(x145, x72, x120); - uint64_t x150, uint8_t x151 = addcarryx_u64(x148, x75, x123); - uint64_t x153, uint8_t x154 = addcarryx_u64(x151, x78, x126); - uint8_t x155 = (x154 + 0x0); - uint64_t x157, uint64_t x158 = mulx_u64(x7, x19); - uint64_t x160, uint64_t x161 = mulx_u64(x7, x21); - uint64_t x163, uint64_t x164 = mulx_u64(x7, x23); - uint64_t x166, uint64_t x167 = mulx_u64(x7, x25); - uint64_t x169, uint64_t x170 = mulx_u64(x7, x27); - uint64_t x172, uint64_t x173 = mulx_u64(x7, x29); - uint64_t x175, uint64_t x176 = mulx_u64(x7, x31); - uint64_t x178, uint64_t x179 = mulx_u64(x7, x30); - uint64_t x181, uint8_t x182 = addcarryx_u64(0x0, x158, x160); - uint64_t x184, uint8_t x185 = addcarryx_u64(x182, x161, x163); - uint64_t x187, uint8_t x188 = addcarryx_u64(x185, x164, x166); - uint64_t x190, uint8_t x191 = addcarryx_u64(x188, x167, x169); - uint64_t x193, uint8_t x194 = addcarryx_u64(x191, x170, x172); - uint64_t x196, uint8_t x197 = addcarryx_u64(x194, x173, x175); - uint64_t x199, uint8_t x200 = addcarryx_u64(x197, x176, x178); - uint64_t x202, uint8_t _ = addcarryx_u64(0x0, x200, x179); - uint64_t x205, uint8_t x206 = addcarryx_u64(0x0, x132, x157); - uint64_t x208, uint8_t x209 = addcarryx_u64(x206, x135, x181); - uint64_t x211, uint8_t x212 = addcarryx_u64(x209, x138, x184); - uint64_t x214, uint8_t x215 = addcarryx_u64(x212, x141, x187); - uint64_t x217, uint8_t x218 = addcarryx_u64(x215, x144, x190); - uint64_t x220, uint8_t x221 = addcarryx_u64(x218, x147, x193); - uint64_t x223, uint8_t x224 = addcarryx_u64(x221, x150, x196); - uint64_t x226, uint8_t x227 = addcarryx_u64(x224, x153, x199); - uint64_t x229, uint8_t x230 = addcarryx_u64(x227, x155, x202); - uint64_t x232, uint64_t x233 = mulx_u64(x205, 0xffffffffffffffffL); - uint64_t x235, uint64_t x236 = mulx_u64(x205, 0xffffffffffffffffL); - uint64_t x238, uint64_t x239 = mulx_u64(x205, 0xffffffffffffffffL); - uint64_t x241, uint64_t x242 = mulx_u64(x205, 0xffffffffffffffffL); - uint64_t x244, uint64_t x245 = mulx_u64(x205, 0xffffffffffffffffL); - uint64_t x247, uint64_t x248 = mulx_u64(x205, 0xffffffffffffffffL); - uint64_t x250, uint64_t x251 = mulx_u64(x205, 0xffffffffffffffffL); - uint64_t x253, uint64_t x254 = mulx_u64(x205, 0x3eddffffffffffff); - uint64_t x256, uint8_t x257 = addcarryx_u64(0x0, x233, x235); - uint64_t x259, uint8_t x260 = addcarryx_u64(x257, x236, x238); - uint64_t x262, uint8_t x263 = addcarryx_u64(x260, x239, x241); - uint64_t x265, uint8_t x266 = addcarryx_u64(x263, x242, x244); - uint64_t x268, uint8_t x269 = addcarryx_u64(x266, x245, x247); - uint64_t x271, uint8_t x272 = addcarryx_u64(x269, x248, x250); - uint64_t x274, uint8_t x275 = addcarryx_u64(x272, x251, x253); - uint64_t x277, uint8_t _ = addcarryx_u64(0x0, x275, x254); - uint64_t _, uint8_t x281 = addcarryx_u64(0x0, x205, x232); - uint64_t x283, uint8_t x284 = addcarryx_u64(x281, x208, x256); - uint64_t x286, uint8_t x287 = addcarryx_u64(x284, x211, x259); - uint64_t x289, uint8_t x290 = addcarryx_u64(x287, x214, x262); - uint64_t x292, uint8_t x293 = addcarryx_u64(x290, x217, x265); - uint64_t x295, uint8_t x296 = addcarryx_u64(x293, x220, x268); - uint64_t x298, uint8_t x299 = addcarryx_u64(x296, x223, x271); - uint64_t x301, uint8_t x302 = addcarryx_u64(x299, x226, x274); - uint64_t x304, uint8_t x305 = addcarryx_u64(x302, x229, x277); - uint8_t x306 = (x305 + x230); - uint64_t x308, uint64_t x309 = mulx_u64(x9, x19); - uint64_t x311, uint64_t x312 = mulx_u64(x9, x21); - uint64_t x314, uint64_t x315 = mulx_u64(x9, x23); - uint64_t x317, uint64_t x318 = mulx_u64(x9, x25); - uint64_t x320, uint64_t x321 = mulx_u64(x9, x27); - uint64_t x323, uint64_t x324 = mulx_u64(x9, x29); - uint64_t x326, uint64_t x327 = mulx_u64(x9, x31); - uint64_t x329, uint64_t x330 = mulx_u64(x9, x30); - uint64_t x332, uint8_t x333 = addcarryx_u64(0x0, x309, x311); - uint64_t x335, uint8_t x336 = addcarryx_u64(x333, x312, x314); - uint64_t x338, uint8_t x339 = addcarryx_u64(x336, x315, x317); - uint64_t x341, uint8_t x342 = addcarryx_u64(x339, x318, x320); - uint64_t x344, uint8_t x345 = addcarryx_u64(x342, x321, x323); - uint64_t x347, uint8_t x348 = addcarryx_u64(x345, x324, x326); - uint64_t x350, uint8_t x351 = addcarryx_u64(x348, x327, x329); - uint64_t x353, uint8_t _ = addcarryx_u64(0x0, x351, x330); - uint64_t x356, uint8_t x357 = addcarryx_u64(0x0, x283, x308); - uint64_t x359, uint8_t x360 = addcarryx_u64(x357, x286, x332); - uint64_t x362, uint8_t x363 = addcarryx_u64(x360, x289, x335); - uint64_t x365, uint8_t x366 = addcarryx_u64(x363, x292, x338); - uint64_t x368, uint8_t x369 = addcarryx_u64(x366, x295, x341); - uint64_t x371, uint8_t x372 = addcarryx_u64(x369, x298, x344); - uint64_t x374, uint8_t x375 = addcarryx_u64(x372, x301, x347); - uint64_t x377, uint8_t x378 = addcarryx_u64(x375, x304, x350); - uint64_t x380, uint8_t x381 = addcarryx_u64(x378, x306, x353); - uint64_t x383, uint64_t x384 = mulx_u64(x356, 0xffffffffffffffffL); - uint64_t x386, uint64_t x387 = mulx_u64(x356, 0xffffffffffffffffL); - uint64_t x389, uint64_t x390 = mulx_u64(x356, 0xffffffffffffffffL); - uint64_t x392, uint64_t x393 = mulx_u64(x356, 0xffffffffffffffffL); - uint64_t x395, uint64_t x396 = mulx_u64(x356, 0xffffffffffffffffL); - uint64_t x398, uint64_t x399 = mulx_u64(x356, 0xffffffffffffffffL); - uint64_t x401, uint64_t x402 = mulx_u64(x356, 0xffffffffffffffffL); - uint64_t x404, uint64_t x405 = mulx_u64(x356, 0x3eddffffffffffff); - uint64_t x407, uint8_t x408 = addcarryx_u64(0x0, x384, x386); - uint64_t x410, uint8_t x411 = addcarryx_u64(x408, x387, x389); - uint64_t x413, uint8_t x414 = addcarryx_u64(x411, x390, x392); - uint64_t x416, uint8_t x417 = addcarryx_u64(x414, x393, x395); - uint64_t x419, uint8_t x420 = addcarryx_u64(x417, x396, x398); - uint64_t x422, uint8_t x423 = addcarryx_u64(x420, x399, x401); - uint64_t x425, uint8_t x426 = addcarryx_u64(x423, x402, x404); - uint64_t x428, uint8_t _ = addcarryx_u64(0x0, x426, x405); - uint64_t _, uint8_t x432 = addcarryx_u64(0x0, x356, x383); - uint64_t x434, uint8_t x435 = addcarryx_u64(x432, x359, x407); - uint64_t x437, uint8_t x438 = addcarryx_u64(x435, x362, x410); - uint64_t x440, uint8_t x441 = addcarryx_u64(x438, x365, x413); - uint64_t x443, uint8_t x444 = addcarryx_u64(x441, x368, x416); - uint64_t x446, uint8_t x447 = addcarryx_u64(x444, x371, x419); - uint64_t x449, uint8_t x450 = addcarryx_u64(x447, x374, x422); - uint64_t x452, uint8_t x453 = addcarryx_u64(x450, x377, x425); - uint64_t x455, uint8_t x456 = addcarryx_u64(x453, x380, x428); - uint8_t x457 = (x456 + x381); - uint64_t x459, uint64_t x460 = mulx_u64(x11, x19); - uint64_t x462, uint64_t x463 = mulx_u64(x11, x21); - uint64_t x465, uint64_t x466 = mulx_u64(x11, x23); - uint64_t x468, uint64_t x469 = mulx_u64(x11, x25); - uint64_t x471, uint64_t x472 = mulx_u64(x11, x27); - uint64_t x474, uint64_t x475 = mulx_u64(x11, x29); - uint64_t x477, uint64_t x478 = mulx_u64(x11, x31); - uint64_t x480, uint64_t x481 = mulx_u64(x11, x30); - uint64_t x483, uint8_t x484 = addcarryx_u64(0x0, x460, x462); - uint64_t x486, uint8_t x487 = addcarryx_u64(x484, x463, x465); - uint64_t x489, uint8_t x490 = addcarryx_u64(x487, x466, x468); - uint64_t x492, uint8_t x493 = addcarryx_u64(x490, x469, x471); - uint64_t x495, uint8_t x496 = addcarryx_u64(x493, x472, x474); - uint64_t x498, uint8_t x499 = addcarryx_u64(x496, x475, x477); - uint64_t x501, uint8_t x502 = addcarryx_u64(x499, x478, x480); - uint64_t x504, uint8_t _ = addcarryx_u64(0x0, x502, x481); - uint64_t x507, uint8_t x508 = addcarryx_u64(0x0, x434, x459); - uint64_t x510, uint8_t x511 = addcarryx_u64(x508, x437, x483); - uint64_t x513, uint8_t x514 = addcarryx_u64(x511, x440, x486); - uint64_t x516, uint8_t x517 = addcarryx_u64(x514, x443, x489); - uint64_t x519, uint8_t x520 = addcarryx_u64(x517, x446, x492); - uint64_t x522, uint8_t x523 = addcarryx_u64(x520, x449, x495); - uint64_t x525, uint8_t x526 = addcarryx_u64(x523, x452, x498); - uint64_t x528, uint8_t x529 = addcarryx_u64(x526, x455, x501); - uint64_t x531, uint8_t x532 = addcarryx_u64(x529, x457, x504); - uint64_t x534, uint64_t x535 = mulx_u64(x507, 0xffffffffffffffffL); - uint64_t x537, uint64_t x538 = mulx_u64(x507, 0xffffffffffffffffL); - uint64_t x540, uint64_t x541 = mulx_u64(x507, 0xffffffffffffffffL); - uint64_t x543, uint64_t x544 = mulx_u64(x507, 0xffffffffffffffffL); - uint64_t x546, uint64_t x547 = mulx_u64(x507, 0xffffffffffffffffL); - uint64_t x549, uint64_t x550 = mulx_u64(x507, 0xffffffffffffffffL); - uint64_t x552, uint64_t x553 = mulx_u64(x507, 0xffffffffffffffffL); - uint64_t x555, uint64_t x556 = mulx_u64(x507, 0x3eddffffffffffff); - uint64_t x558, uint8_t x559 = addcarryx_u64(0x0, x535, x537); - uint64_t x561, uint8_t x562 = addcarryx_u64(x559, x538, x540); - uint64_t x564, uint8_t x565 = addcarryx_u64(x562, x541, x543); - uint64_t x567, uint8_t x568 = addcarryx_u64(x565, x544, x546); - uint64_t x570, uint8_t x571 = addcarryx_u64(x568, x547, x549); - uint64_t x573, uint8_t x574 = addcarryx_u64(x571, x550, x552); - uint64_t x576, uint8_t x577 = addcarryx_u64(x574, x553, x555); - uint64_t x579, uint8_t _ = addcarryx_u64(0x0, x577, x556); - uint64_t _, uint8_t x583 = addcarryx_u64(0x0, x507, x534); - uint64_t x585, uint8_t x586 = addcarryx_u64(x583, x510, x558); - uint64_t x588, uint8_t x589 = addcarryx_u64(x586, x513, x561); - uint64_t x591, uint8_t x592 = addcarryx_u64(x589, x516, x564); - uint64_t x594, uint8_t x595 = addcarryx_u64(x592, x519, x567); - uint64_t x597, uint8_t x598 = addcarryx_u64(x595, x522, x570); - uint64_t x600, uint8_t x601 = addcarryx_u64(x598, x525, x573); - uint64_t x603, uint8_t x604 = addcarryx_u64(x601, x528, x576); - uint64_t x606, uint8_t x607 = addcarryx_u64(x604, x531, x579); - uint8_t x608 = (x607 + x532); - uint64_t x610, uint64_t x611 = mulx_u64(x13, x19); - uint64_t x613, uint64_t x614 = mulx_u64(x13, x21); - uint64_t x616, uint64_t x617 = mulx_u64(x13, x23); - uint64_t x619, uint64_t x620 = mulx_u64(x13, x25); - uint64_t x622, uint64_t x623 = mulx_u64(x13, x27); - uint64_t x625, uint64_t x626 = mulx_u64(x13, x29); - uint64_t x628, uint64_t x629 = mulx_u64(x13, x31); - uint64_t x631, uint64_t x632 = mulx_u64(x13, x30); - uint64_t x634, uint8_t x635 = addcarryx_u64(0x0, x611, x613); - uint64_t x637, uint8_t x638 = addcarryx_u64(x635, x614, x616); - uint64_t x640, uint8_t x641 = addcarryx_u64(x638, x617, x619); - uint64_t x643, uint8_t x644 = addcarryx_u64(x641, x620, x622); - uint64_t x646, uint8_t x647 = addcarryx_u64(x644, x623, x625); - uint64_t x649, uint8_t x650 = addcarryx_u64(x647, x626, x628); - uint64_t x652, uint8_t x653 = addcarryx_u64(x650, x629, x631); - uint64_t x655, uint8_t _ = addcarryx_u64(0x0, x653, x632); - uint64_t x658, uint8_t x659 = addcarryx_u64(0x0, x585, x610); - uint64_t x661, uint8_t x662 = addcarryx_u64(x659, x588, x634); - uint64_t x664, uint8_t x665 = addcarryx_u64(x662, x591, x637); - uint64_t x667, uint8_t x668 = addcarryx_u64(x665, x594, x640); - uint64_t x670, uint8_t x671 = addcarryx_u64(x668, x597, x643); - uint64_t x673, uint8_t x674 = addcarryx_u64(x671, x600, x646); - uint64_t x676, uint8_t x677 = addcarryx_u64(x674, x603, x649); - uint64_t x679, uint8_t x680 = addcarryx_u64(x677, x606, x652); - uint64_t x682, uint8_t x683 = addcarryx_u64(x680, x608, x655); - uint64_t x685, uint64_t x686 = mulx_u64(x658, 0xffffffffffffffffL); - uint64_t x688, uint64_t x689 = mulx_u64(x658, 0xffffffffffffffffL); - uint64_t x691, uint64_t x692 = mulx_u64(x658, 0xffffffffffffffffL); - uint64_t x694, uint64_t x695 = mulx_u64(x658, 0xffffffffffffffffL); - uint64_t x697, uint64_t x698 = mulx_u64(x658, 0xffffffffffffffffL); - uint64_t x700, uint64_t x701 = mulx_u64(x658, 0xffffffffffffffffL); - uint64_t x703, uint64_t x704 = mulx_u64(x658, 0xffffffffffffffffL); - uint64_t x706, uint64_t x707 = mulx_u64(x658, 0x3eddffffffffffff); - uint64_t x709, uint8_t x710 = addcarryx_u64(0x0, x686, x688); - uint64_t x712, uint8_t x713 = addcarryx_u64(x710, x689, x691); - uint64_t x715, uint8_t x716 = addcarryx_u64(x713, x692, x694); - uint64_t x718, uint8_t x719 = addcarryx_u64(x716, x695, x697); - uint64_t x721, uint8_t x722 = addcarryx_u64(x719, x698, x700); - uint64_t x724, uint8_t x725 = addcarryx_u64(x722, x701, x703); - uint64_t x727, uint8_t x728 = addcarryx_u64(x725, x704, x706); - uint64_t x730, uint8_t _ = addcarryx_u64(0x0, x728, x707); - uint64_t _, uint8_t x734 = addcarryx_u64(0x0, x658, x685); - uint64_t x736, uint8_t x737 = addcarryx_u64(x734, x661, x709); - uint64_t x739, uint8_t x740 = addcarryx_u64(x737, x664, x712); - uint64_t x742, uint8_t x743 = addcarryx_u64(x740, x667, x715); - uint64_t x745, uint8_t x746 = addcarryx_u64(x743, x670, x718); - uint64_t x748, uint8_t x749 = addcarryx_u64(x746, x673, x721); - uint64_t x751, uint8_t x752 = addcarryx_u64(x749, x676, x724); - uint64_t x754, uint8_t x755 = addcarryx_u64(x752, x679, x727); - uint64_t x757, uint8_t x758 = addcarryx_u64(x755, x682, x730); - uint8_t x759 = (x758 + x683); - uint64_t x761, uint64_t x762 = mulx_u64(x15, x19); - uint64_t x764, uint64_t x765 = mulx_u64(x15, x21); - uint64_t x767, uint64_t x768 = mulx_u64(x15, x23); - uint64_t x770, uint64_t x771 = mulx_u64(x15, x25); - uint64_t x773, uint64_t x774 = mulx_u64(x15, x27); - uint64_t x776, uint64_t x777 = mulx_u64(x15, x29); - uint64_t x779, uint64_t x780 = mulx_u64(x15, x31); - uint64_t x782, uint64_t x783 = mulx_u64(x15, x30); - uint64_t x785, uint8_t x786 = addcarryx_u64(0x0, x762, x764); - uint64_t x788, uint8_t x789 = addcarryx_u64(x786, x765, x767); - uint64_t x791, uint8_t x792 = addcarryx_u64(x789, x768, x770); - uint64_t x794, uint8_t x795 = addcarryx_u64(x792, x771, x773); - uint64_t x797, uint8_t x798 = addcarryx_u64(x795, x774, x776); - uint64_t x800, uint8_t x801 = addcarryx_u64(x798, x777, x779); - uint64_t x803, uint8_t x804 = addcarryx_u64(x801, x780, x782); - uint64_t x806, uint8_t _ = addcarryx_u64(0x0, x804, x783); - uint64_t x809, uint8_t x810 = addcarryx_u64(0x0, x736, x761); - uint64_t x812, uint8_t x813 = addcarryx_u64(x810, x739, x785); - uint64_t x815, uint8_t x816 = addcarryx_u64(x813, x742, x788); - uint64_t x818, uint8_t x819 = addcarryx_u64(x816, x745, x791); - uint64_t x821, uint8_t x822 = addcarryx_u64(x819, x748, x794); - uint64_t x824, uint8_t x825 = addcarryx_u64(x822, x751, x797); - uint64_t x827, uint8_t x828 = addcarryx_u64(x825, x754, x800); - uint64_t x830, uint8_t x831 = addcarryx_u64(x828, x757, x803); - uint64_t x833, uint8_t x834 = addcarryx_u64(x831, x759, x806); - uint64_t x836, uint64_t x837 = mulx_u64(x809, 0xffffffffffffffffL); - uint64_t x839, uint64_t x840 = mulx_u64(x809, 0xffffffffffffffffL); - uint64_t x842, uint64_t x843 = mulx_u64(x809, 0xffffffffffffffffL); - uint64_t x845, uint64_t x846 = mulx_u64(x809, 0xffffffffffffffffL); - uint64_t x848, uint64_t x849 = mulx_u64(x809, 0xffffffffffffffffL); - uint64_t x851, uint64_t x852 = mulx_u64(x809, 0xffffffffffffffffL); - uint64_t x854, uint64_t x855 = mulx_u64(x809, 0xffffffffffffffffL); - uint64_t x857, uint64_t x858 = mulx_u64(x809, 0x3eddffffffffffff); - uint64_t x860, uint8_t x861 = addcarryx_u64(0x0, x837, x839); - uint64_t x863, uint8_t x864 = addcarryx_u64(x861, x840, x842); - uint64_t x866, uint8_t x867 = addcarryx_u64(x864, x843, x845); - uint64_t x869, uint8_t x870 = addcarryx_u64(x867, x846, x848); - uint64_t x872, uint8_t x873 = addcarryx_u64(x870, x849, x851); - uint64_t x875, uint8_t x876 = addcarryx_u64(x873, x852, x854); - uint64_t x878, uint8_t x879 = addcarryx_u64(x876, x855, x857); - uint64_t x881, uint8_t _ = addcarryx_u64(0x0, x879, x858); - uint64_t _, uint8_t x885 = addcarryx_u64(0x0, x809, x836); - uint64_t x887, uint8_t x888 = addcarryx_u64(x885, x812, x860); - uint64_t x890, uint8_t x891 = addcarryx_u64(x888, x815, x863); - uint64_t x893, uint8_t x894 = addcarryx_u64(x891, x818, x866); - uint64_t x896, uint8_t x897 = addcarryx_u64(x894, x821, x869); - uint64_t x899, uint8_t x900 = addcarryx_u64(x897, x824, x872); - uint64_t x902, uint8_t x903 = addcarryx_u64(x900, x827, x875); - uint64_t x905, uint8_t x906 = addcarryx_u64(x903, x830, x878); - uint64_t x908, uint8_t x909 = addcarryx_u64(x906, x833, x881); - uint8_t x910 = (x909 + x834); - uint64_t x912, uint64_t x913 = mulx_u64(x17, x19); - uint64_t x915, uint64_t x916 = mulx_u64(x17, x21); - uint64_t x918, uint64_t x919 = mulx_u64(x17, x23); - uint64_t x921, uint64_t x922 = mulx_u64(x17, x25); - uint64_t x924, uint64_t x925 = mulx_u64(x17, x27); - uint64_t x927, uint64_t x928 = mulx_u64(x17, x29); - uint64_t x930, uint64_t x931 = mulx_u64(x17, x31); - uint64_t x933, uint64_t x934 = mulx_u64(x17, x30); - uint64_t x936, uint8_t x937 = addcarryx_u64(0x0, x913, x915); - uint64_t x939, uint8_t x940 = addcarryx_u64(x937, x916, x918); - uint64_t x942, uint8_t x943 = addcarryx_u64(x940, x919, x921); - uint64_t x945, uint8_t x946 = addcarryx_u64(x943, x922, x924); - uint64_t x948, uint8_t x949 = addcarryx_u64(x946, x925, x927); - uint64_t x951, uint8_t x952 = addcarryx_u64(x949, x928, x930); - uint64_t x954, uint8_t x955 = addcarryx_u64(x952, x931, x933); - uint64_t x957, uint8_t _ = addcarryx_u64(0x0, x955, x934); - uint64_t x960, uint8_t x961 = addcarryx_u64(0x0, x887, x912); - uint64_t x963, uint8_t x964 = addcarryx_u64(x961, x890, x936); - uint64_t x966, uint8_t x967 = addcarryx_u64(x964, x893, x939); - uint64_t x969, uint8_t x970 = addcarryx_u64(x967, x896, x942); - uint64_t x972, uint8_t x973 = addcarryx_u64(x970, x899, x945); - uint64_t x975, uint8_t x976 = addcarryx_u64(x973, x902, x948); - uint64_t x978, uint8_t x979 = addcarryx_u64(x976, x905, x951); - uint64_t x981, uint8_t x982 = addcarryx_u64(x979, x908, x954); - uint64_t x984, uint8_t x985 = addcarryx_u64(x982, x910, x957); - uint64_t x987, uint64_t x988 = mulx_u64(x960, 0xffffffffffffffffL); - uint64_t x990, uint64_t x991 = mulx_u64(x960, 0xffffffffffffffffL); - uint64_t x993, uint64_t x994 = mulx_u64(x960, 0xffffffffffffffffL); - uint64_t x996, uint64_t x997 = mulx_u64(x960, 0xffffffffffffffffL); - uint64_t x999, uint64_t x1000 = mulx_u64(x960, 0xffffffffffffffffL); - uint64_t x1002, uint64_t x1003 = mulx_u64(x960, 0xffffffffffffffffL); - uint64_t x1005, uint64_t x1006 = mulx_u64(x960, 0xffffffffffffffffL); - uint64_t x1008, uint64_t x1009 = mulx_u64(x960, 0x3eddffffffffffff); - uint64_t x1011, uint8_t x1012 = addcarryx_u64(0x0, x988, x990); - uint64_t x1014, uint8_t x1015 = addcarryx_u64(x1012, x991, x993); - uint64_t x1017, uint8_t x1018 = addcarryx_u64(x1015, x994, x996); - uint64_t x1020, uint8_t x1021 = addcarryx_u64(x1018, x997, x999); - uint64_t x1023, uint8_t x1024 = addcarryx_u64(x1021, x1000, x1002); - uint64_t x1026, uint8_t x1027 = addcarryx_u64(x1024, x1003, x1005); - uint64_t x1029, uint8_t x1030 = addcarryx_u64(x1027, x1006, x1008); - uint64_t x1032, uint8_t _ = addcarryx_u64(0x0, x1030, x1009); - uint64_t _, uint8_t x1036 = addcarryx_u64(0x0, x960, x987); - uint64_t x1038, uint8_t x1039 = addcarryx_u64(x1036, x963, x1011); - uint64_t x1041, uint8_t x1042 = addcarryx_u64(x1039, x966, x1014); - uint64_t x1044, uint8_t x1045 = addcarryx_u64(x1042, x969, x1017); - uint64_t x1047, uint8_t x1048 = addcarryx_u64(x1045, x972, x1020); - uint64_t x1050, uint8_t x1051 = addcarryx_u64(x1048, x975, x1023); - uint64_t x1053, uint8_t x1054 = addcarryx_u64(x1051, x978, x1026); - uint64_t x1056, uint8_t x1057 = addcarryx_u64(x1054, x981, x1029); - uint64_t x1059, uint8_t x1060 = addcarryx_u64(x1057, x984, x1032); - uint8_t x1061 = (x1060 + x985); - uint64_t x1063, uint64_t x1064 = mulx_u64(x16, x19); - uint64_t x1066, uint64_t x1067 = mulx_u64(x16, x21); - uint64_t x1069, uint64_t x1070 = mulx_u64(x16, x23); - uint64_t x1072, uint64_t x1073 = mulx_u64(x16, x25); - uint64_t x1075, uint64_t x1076 = mulx_u64(x16, x27); - uint64_t x1078, uint64_t x1079 = mulx_u64(x16, x29); - uint64_t x1081, uint64_t x1082 = mulx_u64(x16, x31); - uint64_t x1084, uint64_t x1085 = mulx_u64(x16, x30); - uint64_t x1087, uint8_t x1088 = addcarryx_u64(0x0, x1064, x1066); - uint64_t x1090, uint8_t x1091 = addcarryx_u64(x1088, x1067, x1069); - uint64_t x1093, uint8_t x1094 = addcarryx_u64(x1091, x1070, x1072); - uint64_t x1096, uint8_t x1097 = addcarryx_u64(x1094, x1073, x1075); - uint64_t x1099, uint8_t x1100 = addcarryx_u64(x1097, x1076, x1078); - uint64_t x1102, uint8_t x1103 = addcarryx_u64(x1100, x1079, x1081); - uint64_t x1105, uint8_t x1106 = addcarryx_u64(x1103, x1082, x1084); - uint64_t x1108, uint8_t _ = addcarryx_u64(0x0, x1106, x1085); - uint64_t x1111, uint8_t x1112 = addcarryx_u64(0x0, x1038, x1063); - uint64_t x1114, uint8_t x1115 = addcarryx_u64(x1112, x1041, x1087); - uint64_t x1117, uint8_t x1118 = addcarryx_u64(x1115, x1044, x1090); - uint64_t x1120, uint8_t x1121 = addcarryx_u64(x1118, x1047, x1093); - uint64_t x1123, uint8_t x1124 = addcarryx_u64(x1121, x1050, x1096); - uint64_t x1126, uint8_t x1127 = addcarryx_u64(x1124, x1053, x1099); - uint64_t x1129, uint8_t x1130 = addcarryx_u64(x1127, x1056, x1102); - uint64_t x1132, uint8_t x1133 = addcarryx_u64(x1130, x1059, x1105); - uint64_t x1135, uint8_t x1136 = addcarryx_u64(x1133, x1061, x1108); - uint64_t x1138, uint64_t x1139 = mulx_u64(x1111, 0xffffffffffffffffL); - uint64_t x1141, uint64_t x1142 = mulx_u64(x1111, 0xffffffffffffffffL); - uint64_t x1144, uint64_t x1145 = mulx_u64(x1111, 0xffffffffffffffffL); - uint64_t x1147, uint64_t x1148 = mulx_u64(x1111, 0xffffffffffffffffL); - uint64_t x1150, uint64_t x1151 = mulx_u64(x1111, 0xffffffffffffffffL); - uint64_t x1153, uint64_t x1154 = mulx_u64(x1111, 0xffffffffffffffffL); - uint64_t x1156, uint64_t x1157 = mulx_u64(x1111, 0xffffffffffffffffL); - uint64_t x1159, uint64_t x1160 = mulx_u64(x1111, 0x3eddffffffffffff); - uint64_t x1162, uint8_t x1163 = addcarryx_u64(0x0, x1139, x1141); - uint64_t x1165, uint8_t x1166 = addcarryx_u64(x1163, x1142, x1144); - uint64_t x1168, uint8_t x1169 = addcarryx_u64(x1166, x1145, x1147); - uint64_t x1171, uint8_t x1172 = addcarryx_u64(x1169, x1148, x1150); - uint64_t x1174, uint8_t x1175 = addcarryx_u64(x1172, x1151, x1153); - uint64_t x1177, uint8_t x1178 = addcarryx_u64(x1175, x1154, x1156); - uint64_t x1180, uint8_t x1181 = addcarryx_u64(x1178, x1157, x1159); - uint64_t x1183, uint8_t _ = addcarryx_u64(0x0, x1181, x1160); - uint64_t _, uint8_t x1187 = addcarryx_u64(0x0, x1111, x1138); - uint64_t x1189, uint8_t x1190 = addcarryx_u64(x1187, x1114, x1162); - uint64_t x1192, uint8_t x1193 = addcarryx_u64(x1190, x1117, x1165); - uint64_t x1195, uint8_t x1196 = addcarryx_u64(x1193, x1120, x1168); - uint64_t x1198, uint8_t x1199 = addcarryx_u64(x1196, x1123, x1171); - uint64_t x1201, uint8_t x1202 = addcarryx_u64(x1199, x1126, x1174); - uint64_t x1204, uint8_t x1205 = addcarryx_u64(x1202, x1129, x1177); - uint64_t x1207, uint8_t x1208 = addcarryx_u64(x1205, x1132, x1180); - uint64_t x1210, uint8_t x1211 = addcarryx_u64(x1208, x1135, x1183); - uint8_t x1212 = (x1211 + x1136); - uint64_t x1214, uint8_t x1215 = subborrow_u64(0x0, x1189, 0xffffffffffffffffL); - uint64_t x1217, uint8_t x1218 = subborrow_u64(x1215, x1192, 0xffffffffffffffffL); - uint64_t x1220, uint8_t x1221 = subborrow_u64(x1218, x1195, 0xffffffffffffffffL); - uint64_t x1223, uint8_t x1224 = subborrow_u64(x1221, x1198, 0xffffffffffffffffL); - uint64_t x1226, uint8_t x1227 = subborrow_u64(x1224, x1201, 0xffffffffffffffffL); - uint64_t x1229, uint8_t x1230 = subborrow_u64(x1227, x1204, 0xffffffffffffffffL); - uint64_t x1232, uint8_t x1233 = subborrow_u64(x1230, x1207, 0xffffffffffffffffL); - uint64_t x1235, uint8_t x1236 = subborrow_u64(x1233, x1210, 0x3eddffffffffffff); - uint64_t _, uint8_t x1239 = subborrow_u64(x1236, x1212, 0x0); - uint64_t x1240 = cmovznz64(x1239, x1235, x1210); - uint64_t x1241 = cmovznz64(x1239, x1232, x1207); - uint64_t x1242 = cmovznz64(x1239, x1229, x1204); - uint64_t x1243 = cmovznz64(x1239, x1226, x1201); - uint64_t x1244 = cmovznz64(x1239, x1223, x1198); - uint64_t x1245 = cmovznz64(x1239, x1220, x1195); - uint64_t x1246 = cmovznz64(x1239, x1217, x1192); - uint64_t x1247 = cmovznz64(x1239, x1214, x1189); - return (x1240, x1241, x1242, x1243, x1244, x1245, x1246, x1247)) -(x, x0)%core - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femulDisplay.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femulDisplay.v deleted file mode 100644 index c859c108e..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femulDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.femul. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display mul. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenz.c b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenz.c deleted file mode 100644 index a07b0df9c..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenz.c +++ /dev/null @@ -1,19 +0,0 @@ -static void fenz(ReturnType uint64_t out[1], const uint64_t in1[8]) { - { const uint64_t x13 = in1[7]; - { const uint64_t x14 = in1[6]; - { const uint64_t x12 = in1[5]; - { const uint64_t x10 = in1[4]; - { const uint64_t x8 = in1[3]; - { const uint64_t x6 = in1[2]; - { const uint64_t x4 = in1[1]; - { const uint64_t x2 = in1[0]; - { uint64_t x15 = (x14 | x13); - { uint64_t x16 = (x12 | x15); - { uint64_t x17 = (x10 | x16); - { uint64_t x18 = (x8 | x17); - { uint64_t x19 = (x6 | x18); - { uint64_t x20 = (x4 | x19); - { uint64_t x21 = (x2 | x20); - out[0] = x21; - }}}}}}}}}}}}}}} -} diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenz.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenz.v deleted file mode 100644 index d877bb15e..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenz.v +++ /dev/null @@ -1,16 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.Synthesis. -Local Open Scope Z_scope. - -(* TODO : change this to field once field isomorphism happens *) -Definition nonzero : - { nonzero : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1 - | forall a, (BoundedWord.BoundedWordToZ _ _ _ (nonzero a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }. -Proof. - Set Ltac Profiling. - Time synthesize_nonzero (). - Show Ltac Profile. -Time Defined. - -Print Assumptions nonzero. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenzDisplay.log b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenzDisplay.log deleted file mode 100644 index a05fc22ab..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenzDisplay.log +++ /dev/null @@ -1,14 +0,0 @@ -λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x13, x14, x12, x10, x8, x6, x4, x2)%core, - uint64_t x15 = (x14 | x13); - uint64_t x16 = (x12 | x15); - uint64_t x17 = (x10 | x16); - uint64_t x18 = (x8 | x17); - uint64_t x19 = (x6 | x18); - uint64_t x20 = (x4 | x19); - uint64_t x21 = (x2 | x20); - return x21) -x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenzDisplay.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenzDisplay.v deleted file mode 100644 index f4b23c2be..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fenzDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.fenz. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display nonzero. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feopp.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feopp.v deleted file mode 100644 index 6f2297ff1..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feopp.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition opp : - { opp : feBW_small -> feBW_small - | forall a, phiM_small (opp a) = F.opp (phiM_small a) }. -Proof. - Set Ltac Profiling. - Time synthesize_opp (). - Show Ltac Profile. -Time Defined. - -Print Assumptions opp. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feoppDisplay.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feoppDisplay.v deleted file mode 100644 index e61efd6b4..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/feoppDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.feopp. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display opp. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesquare.c b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesquare.c deleted file mode 100644 index 7bd8db166..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesquare.c +++ /dev/null @@ -1,5 +0,0 @@ -/* WARNING: This file was copied from Specific/CurveParameters/montgomery64/fesquare.c. - If you edit it here, changes will be erased the next time remake_curves.sh is run. */ -static void fesquare(uint64_t *out, const uint64_t *in) { - femul(out, in, in); -} diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesub.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesub.v deleted file mode 100644 index 0e6ddc0f4..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesub.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition sub : - { sub : feBW_small -> feBW_small -> feBW_small - | forall a b, phiM_small (sub a b) = F.sub (phiM_small a) (phiM_small b) }. -Proof. - Set Ltac Profiling. - Time synthesize_sub (). - Show Ltac Profile. -Time Defined. - -Print Assumptions sub. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesubDisplay.v b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesubDisplay.v deleted file mode 100644 index f0a751a19..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/fesubDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery64_2e510m290x2e496m1_8limbs.fesub. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display sub. diff --git a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/py_interpreter.sh b/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/py_interpreter.sh deleted file mode 100755 index ff7ce7905..000000000 --- a/src/Specific/montgomery64_2e510m290x2e496m1_8limbs/py_interpreter.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh -set -eu - -/usr/bin/env python3 "$@" -Dq='2**510 - 290*2**496 - 1' -Dmodulus_bytes='64' -Da24='121665' |