diff options
Diffstat (limited to 'src/Specific/solinas32_2e512m569_25limbs')
25 files changed, 0 insertions, 820 deletions
diff --git a/src/Specific/solinas32_2e512m569_25limbs/CurveParameters.v b/src/Specific/solinas32_2e512m569_25limbs/CurveParameters.v deleted file mode 100644 index d3f7a5042..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/CurveParameters.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Import Crypto.Specific.Framework.RawCurveParameters. -Require Import Crypto.Util.LetIn. - -(*** -Modulus : 2^512 - 569 -Base: 20 + 12/25 -***) - -Definition curve : CurveParameters := - {| - sz := 25%nat; - base := 20 + 12/25; - bitwidth := 32; - s := 2^512; - c := [(1, 569)]; - carry_chains := Some [seq 0 (pred 25); [0; 1]]%nat; - - a24 := None; - coef_div_modulus := Some 2%nat; - - goldilocks := None; - karatsuba := None; - montgomery := false; - freeze := Some true; - 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/solinas32_2e512m569_25limbs/Synthesis.v b/src/Specific/solinas32_2e512m569_25limbs/Synthesis.v deleted file mode 100644 index 00691ffb7..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/Synthesis.v +++ /dev/null @@ -1,9 +0,0 @@ -Require Import Crypto.Specific.Framework.SynthesisFramework. -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.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/solinas32_2e512m569_25limbs/compiler.sh b/src/Specific/solinas32_2e512m569_25limbs/compiler.sh deleted file mode 100755 index 4094fb440..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/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='32' -Dlimb_weight_gaps_array='{21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,20}' -Dmodulus_array='{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,0xfd,0xc7}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='25' -Dq_mpz='(1_mpz<<512) - 569' "$@" diff --git a/src/Specific/solinas32_2e512m569_25limbs/compilerxx.sh b/src/Specific/solinas32_2e512m569_25limbs/compilerxx.sh deleted file mode 100755 index f8a05fc6b..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/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='32' -Dlimb_weight_gaps_array='{21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,21,20,20}' -Dmodulus_array='{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,0xfd,0xc7}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='25' -Dq_mpz='(1_mpz<<512) - 569' "$@" diff --git a/src/Specific/solinas32_2e512m569_25limbs/feadd.c b/src/Specific/solinas32_2e512m569_25limbs/feadd.c deleted file mode 100644 index f297d1eee..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/feadd.c +++ /dev/null @@ -1,78 +0,0 @@ -static void feadd(uint32_t out[25], const uint32_t in1[25], const uint32_t in2[25]) { - { const uint32_t x50 = in1[24]; - { const uint32_t x51 = in1[23]; - { const uint32_t x49 = in1[22]; - { const uint32_t x47 = in1[21]; - { const uint32_t x45 = in1[20]; - { const uint32_t x43 = in1[19]; - { const uint32_t x41 = in1[18]; - { const uint32_t x39 = in1[17]; - { const uint32_t x37 = in1[16]; - { const uint32_t x35 = in1[15]; - { const uint32_t x33 = in1[14]; - { const uint32_t x31 = in1[13]; - { const uint32_t x29 = in1[12]; - { const uint32_t x27 = in1[11]; - { const uint32_t x25 = in1[10]; - { const uint32_t x23 = in1[9]; - { const uint32_t x21 = in1[8]; - { const uint32_t x19 = in1[7]; - { const uint32_t x17 = in1[6]; - { const uint32_t x15 = in1[5]; - { const uint32_t x13 = in1[4]; - { const uint32_t x11 = in1[3]; - { const uint32_t x9 = in1[2]; - { const uint32_t x7 = in1[1]; - { const uint32_t x5 = in1[0]; - { const uint32_t x98 = in2[24]; - { const uint32_t x99 = in2[23]; - { const uint32_t x97 = in2[22]; - { const uint32_t x95 = in2[21]; - { const uint32_t x93 = in2[20]; - { const uint32_t x91 = in2[19]; - { const uint32_t x89 = in2[18]; - { const uint32_t x87 = in2[17]; - { const uint32_t x85 = in2[16]; - { const uint32_t x83 = in2[15]; - { const uint32_t x81 = in2[14]; - { const uint32_t x79 = in2[13]; - { const uint32_t x77 = in2[12]; - { const uint32_t x75 = in2[11]; - { const uint32_t x73 = in2[10]; - { const uint32_t x71 = in2[9]; - { const uint32_t x69 = in2[8]; - { const uint32_t x67 = in2[7]; - { const uint32_t x65 = in2[6]; - { const uint32_t x63 = in2[5]; - { const uint32_t x61 = in2[4]; - { const uint32_t x59 = in2[3]; - { const uint32_t x57 = in2[2]; - { const uint32_t x55 = in2[1]; - { const uint32_t x53 = in2[0]; - out[0] = (x5 + x53); - out[1] = (x7 + x55); - out[2] = (x9 + x57); - out[3] = (x11 + x59); - out[4] = (x13 + x61); - out[5] = (x15 + x63); - out[6] = (x17 + x65); - out[7] = (x19 + x67); - out[8] = (x21 + x69); - out[9] = (x23 + x71); - out[10] = (x25 + x73); - out[11] = (x27 + x75); - out[12] = (x29 + x77); - out[13] = (x31 + x79); - out[14] = (x33 + x81); - out[15] = (x35 + x83); - out[16] = (x37 + x85); - out[17] = (x39 + x87); - out[18] = (x41 + x89); - out[19] = (x43 + x91); - out[20] = (x45 + x93); - out[21] = (x47 + x95); - out[22] = (x49 + x97); - out[23] = (x51 + x99); - out[24] = (x50 + x98); - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/solinas32_2e512m569_25limbs/feadd.v b/src/Specific/solinas32_2e512m569_25limbs/feadd.v deleted file mode 100644 index 888acda1e..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/feadd.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition add : - { add : feBW_tight -> feBW_tight -> feBW_loose - | forall a b, phiBW_loose (add a b) = F.add (phiBW_tight a) (phiBW_tight b) }. -Proof. - Set Ltac Profiling. - Time synthesize_add (). - Show Ltac Profile. -Time Defined. - -Print Assumptions add. diff --git a/src/Specific/solinas32_2e512m569_25limbs/feaddDisplay.log b/src/Specific/solinas32_2e512m569_25limbs/feaddDisplay.log deleted file mode 100644 index a5f61c9b9..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/feaddDisplay.log +++ /dev/null @@ -1,7 +0,0 @@ -λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x50, x51, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x98, x99, x97, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59, x57, x55, x53))%core, - ((x50 + x98), (x51 + x99), (x49 + x97), (x47 + x95), (x45 + x93), (x43 + x91), (x41 + x89), (x39 + x87), (x37 + x85), (x35 + x83), (x33 + x81), (x31 + x79), (x29 + x77), (x27 + x75), (x25 + x73), (x23 + x71), (x21 + x69), (x19 + x67), (x17 + x65), (x15 + x63), (x13 + x61), (x11 + x59), (x9 + x57), (x7 + x55), (x5 + x53))) -(x, x0)%core - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e512m569_25limbs/feaddDisplay.v b/src/Specific/solinas32_2e512m569_25limbs/feaddDisplay.v deleted file mode 100644 index a0377aadf..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/feaddDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.feadd. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display add. diff --git a/src/Specific/solinas32_2e512m569_25limbs/fecarry.v b/src/Specific/solinas32_2e512m569_25limbs/fecarry.v deleted file mode 100644 index c7635653c..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fecarry.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition carry : - { carry : feBW_loose -> feBW_tight - | forall a, phiBW_tight (carry a) = (phiBW_loose a) }. -Proof. - Set Ltac Profiling. - Time synthesize_carry (). - Show Ltac Profile. -Time Defined. - -Print Assumptions carry. diff --git a/src/Specific/solinas32_2e512m569_25limbs/fecarryDisplay.v b/src/Specific/solinas32_2e512m569_25limbs/fecarryDisplay.v deleted file mode 100644 index 73792e5c2..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fecarryDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.fecarry. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display carry. diff --git a/src/Specific/solinas32_2e512m569_25limbs/femul.v b/src/Specific/solinas32_2e512m569_25limbs/femul.v deleted file mode 100644 index 54090d4de..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/femul.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition mul : - { mul : feBW_loose -> feBW_loose -> feBW_tight - | forall a b, phiBW_tight (mul a b) = F.mul (phiBW_loose a) (phiBW_loose b) }. -Proof. - Set Ltac Profiling. - Time synthesize_mul (). - Show Ltac Profile. -Time Defined. - -Print Assumptions mul. diff --git a/src/Specific/solinas32_2e512m569_25limbs/femulDisplay.v b/src/Specific/solinas32_2e512m569_25limbs/femulDisplay.v deleted file mode 100644 index 1f2a84bc8..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/femulDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.femul. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display mul. diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesquare.c b/src/Specific/solinas32_2e512m569_25limbs/fesquare.c deleted file mode 100644 index 7ec3e8d64..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesquare.c +++ /dev/null @@ -1,158 +0,0 @@ -static void fesquare(uint32_t out[25], const uint32_t in1[25]) { - { const uint32_t x47 = in1[24]; - { const uint32_t x48 = in1[23]; - { const uint32_t x46 = in1[22]; - { const uint32_t x44 = in1[21]; - { const uint32_t x42 = in1[20]; - { const uint32_t x40 = in1[19]; - { const uint32_t x38 = in1[18]; - { const uint32_t x36 = in1[17]; - { const uint32_t x34 = in1[16]; - { const uint32_t x32 = in1[15]; - { const uint32_t x30 = in1[14]; - { const uint32_t x28 = in1[13]; - { const uint32_t x26 = in1[12]; - { const uint32_t x24 = in1[11]; - { const uint32_t x22 = in1[10]; - { const uint32_t x20 = in1[9]; - { const uint32_t x18 = in1[8]; - { const uint32_t x16 = in1[7]; - { const uint32_t x14 = in1[6]; - { const uint32_t x12 = in1[5]; - { const uint32_t x10 = in1[4]; - { const uint32_t x8 = in1[3]; - { const uint32_t x6 = in1[2]; - { const uint32_t x4 = in1[1]; - { const uint32_t x2 = in1[0]; - { uint64_t x49 = (((uint64_t)x2 * x47) + ((0x2 * ((uint64_t)x4 * x48)) + (((uint64_t)x6 * x46) + ((0x2 * ((uint64_t)x8 * x44)) + (((uint64_t)x10 * x42) + ((0x2 * ((uint64_t)x12 * x40)) + (((uint64_t)x14 * x38) + ((0x2 * ((uint64_t)x16 * x36)) + (((uint64_t)x18 * x34) + ((0x2 * ((uint64_t)x20 * x32)) + (((uint64_t)x22 * x30) + ((0x2 * ((uint64_t)x24 * x28)) + (((uint64_t)x26 * x26) + ((0x2 * ((uint64_t)x28 * x24)) + (((uint64_t)x30 * x22) + ((0x2 * ((uint64_t)x32 * x20)) + (((uint64_t)x34 * x18) + ((0x2 * ((uint64_t)x36 * x16)) + (((uint64_t)x38 * x14) + ((0x2 * ((uint64_t)x40 * x12)) + (((uint64_t)x42 * x10) + ((0x2 * ((uint64_t)x44 * x8)) + (((uint64_t)x46 * x6) + ((0x2 * ((uint64_t)x48 * x4)) + ((uint64_t)x47 * x2))))))))))))))))))))))))); - { uint64_t x50 = ((((uint64_t)x2 * x48) + (((uint64_t)x4 * x46) + (((uint64_t)x6 * x44) + (((uint64_t)x8 * x42) + (((uint64_t)x10 * x40) + (((uint64_t)x12 * x38) + (((uint64_t)x14 * x36) + (((uint64_t)x16 * x34) + (((uint64_t)x18 * x32) + (((uint64_t)x20 * x30) + (((uint64_t)x22 * x28) + (((uint64_t)x24 * x26) + (((uint64_t)x26 * x24) + (((uint64_t)x28 * x22) + (((uint64_t)x30 * x20) + (((uint64_t)x32 * x18) + (((uint64_t)x34 * x16) + (((uint64_t)x36 * x14) + (((uint64_t)x38 * x12) + (((uint64_t)x40 * x10) + (((uint64_t)x42 * x8) + (((uint64_t)x44 * x6) + (((uint64_t)x46 * x4) + ((uint64_t)x48 * x2)))))))))))))))))))))))) + (0x239 * ((uint64_t)x47 * x47))); - { uint64_t x51 = ((((uint64_t)x2 * x46) + ((0x2 * ((uint64_t)x4 * x44)) + (((uint64_t)x6 * x42) + ((0x2 * ((uint64_t)x8 * x40)) + (((uint64_t)x10 * x38) + ((0x2 * ((uint64_t)x12 * x36)) + (((uint64_t)x14 * x34) + ((0x2 * ((uint64_t)x16 * x32)) + (((uint64_t)x18 * x30) + ((0x2 * ((uint64_t)x20 * x28)) + (((uint64_t)x22 * x26) + ((0x2 * ((uint64_t)x24 * x24)) + (((uint64_t)x26 * x22) + ((0x2 * ((uint64_t)x28 * x20)) + (((uint64_t)x30 * x18) + ((0x2 * ((uint64_t)x32 * x16)) + (((uint64_t)x34 * x14) + ((0x2 * ((uint64_t)x36 * x12)) + (((uint64_t)x38 * x10) + ((0x2 * ((uint64_t)x40 * x8)) + (((uint64_t)x42 * x6) + ((0x2 * ((uint64_t)x44 * x4)) + ((uint64_t)x46 * x2))))))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x48 * x47)) + (0x2 * ((uint64_t)x47 * x48))))); - { uint64_t x52 = ((((uint64_t)x2 * x44) + (((uint64_t)x4 * x42) + (((uint64_t)x6 * x40) + (((uint64_t)x8 * x38) + (((uint64_t)x10 * x36) + (((uint64_t)x12 * x34) + (((uint64_t)x14 * x32) + (((uint64_t)x16 * x30) + (((uint64_t)x18 * x28) + (((uint64_t)x20 * x26) + (((uint64_t)x22 * x24) + (((uint64_t)x24 * x22) + (((uint64_t)x26 * x20) + (((uint64_t)x28 * x18) + (((uint64_t)x30 * x16) + (((uint64_t)x32 * x14) + (((uint64_t)x34 * x12) + (((uint64_t)x36 * x10) + (((uint64_t)x38 * x8) + (((uint64_t)x40 * x6) + (((uint64_t)x42 * x4) + ((uint64_t)x44 * x2)))))))))))))))))))))) + (0x239 * (((uint64_t)x46 * x47) + ((0x2 * ((uint64_t)x48 * x48)) + ((uint64_t)x47 * x46))))); - { uint64_t x53 = ((((uint64_t)x2 * x42) + ((0x2 * ((uint64_t)x4 * x40)) + (((uint64_t)x6 * x38) + ((0x2 * ((uint64_t)x8 * x36)) + (((uint64_t)x10 * x34) + ((0x2 * ((uint64_t)x12 * x32)) + (((uint64_t)x14 * x30) + ((0x2 * ((uint64_t)x16 * x28)) + (((uint64_t)x18 * x26) + ((0x2 * ((uint64_t)x20 * x24)) + (((uint64_t)x22 * x22) + ((0x2 * ((uint64_t)x24 * x20)) + (((uint64_t)x26 * x18) + ((0x2 * ((uint64_t)x28 * x16)) + (((uint64_t)x30 * x14) + ((0x2 * ((uint64_t)x32 * x12)) + (((uint64_t)x34 * x10) + ((0x2 * ((uint64_t)x36 * x8)) + (((uint64_t)x38 * x6) + ((0x2 * ((uint64_t)x40 * x4)) + ((uint64_t)x42 * x2))))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x44 * x47)) + ((0x2 * ((uint64_t)x46 * x48)) + ((0x2 * ((uint64_t)x48 * x46)) + (0x2 * ((uint64_t)x47 * x44))))))); - { uint64_t x54 = ((((uint64_t)x2 * x40) + (((uint64_t)x4 * x38) + (((uint64_t)x6 * x36) + (((uint64_t)x8 * x34) + (((uint64_t)x10 * x32) + (((uint64_t)x12 * x30) + (((uint64_t)x14 * x28) + (((uint64_t)x16 * x26) + (((uint64_t)x18 * x24) + (((uint64_t)x20 * x22) + (((uint64_t)x22 * x20) + (((uint64_t)x24 * x18) + (((uint64_t)x26 * x16) + (((uint64_t)x28 * x14) + (((uint64_t)x30 * x12) + (((uint64_t)x32 * x10) + (((uint64_t)x34 * x8) + (((uint64_t)x36 * x6) + (((uint64_t)x38 * x4) + ((uint64_t)x40 * x2)))))))))))))))))))) + (0x239 * (((uint64_t)x42 * x47) + ((0x2 * ((uint64_t)x44 * x48)) + (((uint64_t)x46 * x46) + ((0x2 * ((uint64_t)x48 * x44)) + ((uint64_t)x47 * x42))))))); - { uint64_t x55 = ((((uint64_t)x2 * x38) + ((0x2 * ((uint64_t)x4 * x36)) + (((uint64_t)x6 * x34) + ((0x2 * ((uint64_t)x8 * x32)) + (((uint64_t)x10 * x30) + ((0x2 * ((uint64_t)x12 * x28)) + (((uint64_t)x14 * x26) + ((0x2 * ((uint64_t)x16 * x24)) + (((uint64_t)x18 * x22) + ((0x2 * ((uint64_t)x20 * x20)) + (((uint64_t)x22 * x18) + ((0x2 * ((uint64_t)x24 * x16)) + (((uint64_t)x26 * x14) + ((0x2 * ((uint64_t)x28 * x12)) + (((uint64_t)x30 * x10) + ((0x2 * ((uint64_t)x32 * x8)) + (((uint64_t)x34 * x6) + ((0x2 * ((uint64_t)x36 * x4)) + ((uint64_t)x38 * x2))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x40 * x47)) + ((0x2 * ((uint64_t)x42 * x48)) + ((0x2 * ((uint64_t)x44 * x46)) + ((0x2 * ((uint64_t)x46 * x44)) + ((0x2 * ((uint64_t)x48 * x42)) + (0x2 * ((uint64_t)x47 * x40))))))))); - { uint64_t x56 = ((((uint64_t)x2 * x36) + (((uint64_t)x4 * x34) + (((uint64_t)x6 * x32) + (((uint64_t)x8 * x30) + (((uint64_t)x10 * x28) + (((uint64_t)x12 * x26) + (((uint64_t)x14 * x24) + (((uint64_t)x16 * x22) + (((uint64_t)x18 * x20) + (((uint64_t)x20 * x18) + (((uint64_t)x22 * x16) + (((uint64_t)x24 * x14) + (((uint64_t)x26 * x12) + (((uint64_t)x28 * x10) + (((uint64_t)x30 * x8) + (((uint64_t)x32 * x6) + (((uint64_t)x34 * x4) + ((uint64_t)x36 * x2)))))))))))))))))) + (0x239 * (((uint64_t)x38 * x47) + ((0x2 * ((uint64_t)x40 * x48)) + (((uint64_t)x42 * x46) + ((0x2 * ((uint64_t)x44 * x44)) + (((uint64_t)x46 * x42) + ((0x2 * ((uint64_t)x48 * x40)) + ((uint64_t)x47 * x38))))))))); - { uint64_t x57 = ((((uint64_t)x2 * x34) + ((0x2 * ((uint64_t)x4 * x32)) + (((uint64_t)x6 * x30) + ((0x2 * ((uint64_t)x8 * x28)) + (((uint64_t)x10 * x26) + ((0x2 * ((uint64_t)x12 * x24)) + (((uint64_t)x14 * x22) + ((0x2 * ((uint64_t)x16 * x20)) + (((uint64_t)x18 * x18) + ((0x2 * ((uint64_t)x20 * x16)) + (((uint64_t)x22 * x14) + ((0x2 * ((uint64_t)x24 * x12)) + (((uint64_t)x26 * x10) + ((0x2 * ((uint64_t)x28 * x8)) + (((uint64_t)x30 * x6) + ((0x2 * ((uint64_t)x32 * x4)) + ((uint64_t)x34 * x2))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x36 * x47)) + ((0x2 * ((uint64_t)x38 * x48)) + ((0x2 * ((uint64_t)x40 * x46)) + ((0x2 * ((uint64_t)x42 * x44)) + ((0x2 * ((uint64_t)x44 * x42)) + ((0x2 * ((uint64_t)x46 * x40)) + ((0x2 * ((uint64_t)x48 * x38)) + (0x2 * ((uint64_t)x47 * x36))))))))))); - { uint64_t x58 = ((((uint64_t)x2 * x32) + (((uint64_t)x4 * x30) + (((uint64_t)x6 * x28) + (((uint64_t)x8 * x26) + (((uint64_t)x10 * x24) + (((uint64_t)x12 * x22) + (((uint64_t)x14 * x20) + (((uint64_t)x16 * x18) + (((uint64_t)x18 * x16) + (((uint64_t)x20 * x14) + (((uint64_t)x22 * x12) + (((uint64_t)x24 * x10) + (((uint64_t)x26 * x8) + (((uint64_t)x28 * x6) + (((uint64_t)x30 * x4) + ((uint64_t)x32 * x2)))))))))))))))) + (0x239 * (((uint64_t)x34 * x47) + ((0x2 * ((uint64_t)x36 * x48)) + (((uint64_t)x38 * x46) + ((0x2 * ((uint64_t)x40 * x44)) + (((uint64_t)x42 * x42) + ((0x2 * ((uint64_t)x44 * x40)) + (((uint64_t)x46 * x38) + ((0x2 * ((uint64_t)x48 * x36)) + ((uint64_t)x47 * x34))))))))))); - { uint64_t x59 = ((((uint64_t)x2 * x30) + ((0x2 * ((uint64_t)x4 * x28)) + (((uint64_t)x6 * x26) + ((0x2 * ((uint64_t)x8 * x24)) + (((uint64_t)x10 * x22) + ((0x2 * ((uint64_t)x12 * x20)) + (((uint64_t)x14 * x18) + ((0x2 * ((uint64_t)x16 * x16)) + (((uint64_t)x18 * x14) + ((0x2 * ((uint64_t)x20 * x12)) + (((uint64_t)x22 * x10) + ((0x2 * ((uint64_t)x24 * x8)) + (((uint64_t)x26 * x6) + ((0x2 * ((uint64_t)x28 * x4)) + ((uint64_t)x30 * x2))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x32 * x47)) + ((0x2 * ((uint64_t)x34 * x48)) + ((0x2 * ((uint64_t)x36 * x46)) + ((0x2 * ((uint64_t)x38 * x44)) + ((0x2 * ((uint64_t)x40 * x42)) + ((0x2 * ((uint64_t)x42 * x40)) + ((0x2 * ((uint64_t)x44 * x38)) + ((0x2 * ((uint64_t)x46 * x36)) + ((0x2 * ((uint64_t)x48 * x34)) + (0x2 * ((uint64_t)x47 * x32))))))))))))); - { uint64_t x60 = ((((uint64_t)x2 * x28) + (((uint64_t)x4 * x26) + (((uint64_t)x6 * x24) + (((uint64_t)x8 * x22) + (((uint64_t)x10 * x20) + (((uint64_t)x12 * x18) + (((uint64_t)x14 * x16) + (((uint64_t)x16 * x14) + (((uint64_t)x18 * x12) + (((uint64_t)x20 * x10) + (((uint64_t)x22 * x8) + (((uint64_t)x24 * x6) + (((uint64_t)x26 * x4) + ((uint64_t)x28 * x2)))))))))))))) + (0x239 * (((uint64_t)x30 * x47) + ((0x2 * ((uint64_t)x32 * x48)) + (((uint64_t)x34 * x46) + ((0x2 * ((uint64_t)x36 * x44)) + (((uint64_t)x38 * x42) + ((0x2 * ((uint64_t)x40 * x40)) + (((uint64_t)x42 * x38) + ((0x2 * ((uint64_t)x44 * x36)) + (((uint64_t)x46 * x34) + ((0x2 * ((uint64_t)x48 * x32)) + ((uint64_t)x47 * x30))))))))))))); - { uint64_t x61 = ((((uint64_t)x2 * x26) + ((0x2 * ((uint64_t)x4 * x24)) + (((uint64_t)x6 * x22) + ((0x2 * ((uint64_t)x8 * x20)) + (((uint64_t)x10 * x18) + ((0x2 * ((uint64_t)x12 * x16)) + (((uint64_t)x14 * x14) + ((0x2 * ((uint64_t)x16 * x12)) + (((uint64_t)x18 * x10) + ((0x2 * ((uint64_t)x20 * x8)) + (((uint64_t)x22 * x6) + ((0x2 * ((uint64_t)x24 * x4)) + ((uint64_t)x26 * x2))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x28 * x47)) + ((0x2 * ((uint64_t)x30 * x48)) + ((0x2 * ((uint64_t)x32 * x46)) + ((0x2 * ((uint64_t)x34 * x44)) + ((0x2 * ((uint64_t)x36 * x42)) + ((0x2 * ((uint64_t)x38 * x40)) + ((0x2 * ((uint64_t)x40 * x38)) + ((0x2 * ((uint64_t)x42 * x36)) + ((0x2 * ((uint64_t)x44 * x34)) + ((0x2 * ((uint64_t)x46 * x32)) + ((0x2 * ((uint64_t)x48 * x30)) + (0x2 * ((uint64_t)x47 * x28))))))))))))))); - { uint64_t x62 = ((((uint64_t)x2 * x24) + (((uint64_t)x4 * x22) + (((uint64_t)x6 * x20) + (((uint64_t)x8 * x18) + (((uint64_t)x10 * x16) + (((uint64_t)x12 * x14) + (((uint64_t)x14 * x12) + (((uint64_t)x16 * x10) + (((uint64_t)x18 * x8) + (((uint64_t)x20 * x6) + (((uint64_t)x22 * x4) + ((uint64_t)x24 * x2)))))))))))) + (0x239 * (((uint64_t)x26 * x47) + ((0x2 * ((uint64_t)x28 * x48)) + (((uint64_t)x30 * x46) + ((0x2 * ((uint64_t)x32 * x44)) + (((uint64_t)x34 * x42) + ((0x2 * ((uint64_t)x36 * x40)) + (((uint64_t)x38 * x38) + ((0x2 * ((uint64_t)x40 * x36)) + (((uint64_t)x42 * x34) + ((0x2 * ((uint64_t)x44 * x32)) + (((uint64_t)x46 * x30) + ((0x2 * ((uint64_t)x48 * x28)) + ((uint64_t)x47 * x26))))))))))))))); - { uint64_t x63 = ((((uint64_t)x2 * x22) + ((0x2 * ((uint64_t)x4 * x20)) + (((uint64_t)x6 * x18) + ((0x2 * ((uint64_t)x8 * x16)) + (((uint64_t)x10 * x14) + ((0x2 * ((uint64_t)x12 * x12)) + (((uint64_t)x14 * x10) + ((0x2 * ((uint64_t)x16 * x8)) + (((uint64_t)x18 * x6) + ((0x2 * ((uint64_t)x20 * x4)) + ((uint64_t)x22 * x2))))))))))) + (0x239 * ((0x2 * ((uint64_t)x24 * x47)) + ((0x2 * ((uint64_t)x26 * x48)) + ((0x2 * ((uint64_t)x28 * x46)) + ((0x2 * ((uint64_t)x30 * x44)) + ((0x2 * ((uint64_t)x32 * x42)) + ((0x2 * ((uint64_t)x34 * x40)) + ((0x2 * ((uint64_t)x36 * x38)) + ((0x2 * ((uint64_t)x38 * x36)) + ((0x2 * ((uint64_t)x40 * x34)) + ((0x2 * ((uint64_t)x42 * x32)) + ((0x2 * ((uint64_t)x44 * x30)) + ((0x2 * ((uint64_t)x46 * x28)) + ((0x2 * ((uint64_t)x48 * x26)) + (0x2 * ((uint64_t)x47 * x24))))))))))))))))); - { uint64_t x64 = ((((uint64_t)x2 * x20) + (((uint64_t)x4 * x18) + (((uint64_t)x6 * x16) + (((uint64_t)x8 * x14) + (((uint64_t)x10 * x12) + (((uint64_t)x12 * x10) + (((uint64_t)x14 * x8) + (((uint64_t)x16 * x6) + (((uint64_t)x18 * x4) + ((uint64_t)x20 * x2)))))))))) + (0x239 * (((uint64_t)x22 * x47) + ((0x2 * ((uint64_t)x24 * x48)) + (((uint64_t)x26 * x46) + ((0x2 * ((uint64_t)x28 * x44)) + (((uint64_t)x30 * x42) + ((0x2 * ((uint64_t)x32 * x40)) + (((uint64_t)x34 * x38) + ((0x2 * ((uint64_t)x36 * x36)) + (((uint64_t)x38 * x34) + ((0x2 * ((uint64_t)x40 * x32)) + (((uint64_t)x42 * x30) + ((0x2 * ((uint64_t)x44 * x28)) + (((uint64_t)x46 * x26) + ((0x2 * ((uint64_t)x48 * x24)) + ((uint64_t)x47 * x22))))))))))))))))); - { uint64_t x65 = ((((uint64_t)x2 * x18) + ((0x2 * ((uint64_t)x4 * x16)) + (((uint64_t)x6 * x14) + ((0x2 * ((uint64_t)x8 * x12)) + (((uint64_t)x10 * x10) + ((0x2 * ((uint64_t)x12 * x8)) + (((uint64_t)x14 * x6) + ((0x2 * ((uint64_t)x16 * x4)) + ((uint64_t)x18 * x2))))))))) + (0x239 * ((0x2 * ((uint64_t)x20 * x47)) + ((0x2 * ((uint64_t)x22 * x48)) + ((0x2 * ((uint64_t)x24 * x46)) + ((0x2 * ((uint64_t)x26 * x44)) + ((0x2 * ((uint64_t)x28 * x42)) + ((0x2 * ((uint64_t)x30 * x40)) + ((0x2 * ((uint64_t)x32 * x38)) + ((0x2 * ((uint64_t)x34 * x36)) + ((0x2 * ((uint64_t)x36 * x34)) + ((0x2 * ((uint64_t)x38 * x32)) + ((0x2 * ((uint64_t)x40 * x30)) + ((0x2 * ((uint64_t)x42 * x28)) + ((0x2 * ((uint64_t)x44 * x26)) + ((0x2 * ((uint64_t)x46 * x24)) + ((0x2 * ((uint64_t)x48 * x22)) + (0x2 * ((uint64_t)x47 * x20))))))))))))))))))); - { uint64_t x66 = ((((uint64_t)x2 * x16) + (((uint64_t)x4 * x14) + (((uint64_t)x6 * x12) + (((uint64_t)x8 * x10) + (((uint64_t)x10 * x8) + (((uint64_t)x12 * x6) + (((uint64_t)x14 * x4) + ((uint64_t)x16 * x2)))))))) + (0x239 * (((uint64_t)x18 * x47) + ((0x2 * ((uint64_t)x20 * x48)) + (((uint64_t)x22 * x46) + ((0x2 * ((uint64_t)x24 * x44)) + (((uint64_t)x26 * x42) + ((0x2 * ((uint64_t)x28 * x40)) + (((uint64_t)x30 * x38) + ((0x2 * ((uint64_t)x32 * x36)) + (((uint64_t)x34 * x34) + ((0x2 * ((uint64_t)x36 * x32)) + (((uint64_t)x38 * x30) + ((0x2 * ((uint64_t)x40 * x28)) + (((uint64_t)x42 * x26) + ((0x2 * ((uint64_t)x44 * x24)) + (((uint64_t)x46 * x22) + ((0x2 * ((uint64_t)x48 * x20)) + ((uint64_t)x47 * x18))))))))))))))))))); - { uint64_t x67 = ((((uint64_t)x2 * x14) + ((0x2 * ((uint64_t)x4 * x12)) + (((uint64_t)x6 * x10) + ((0x2 * ((uint64_t)x8 * x8)) + (((uint64_t)x10 * x6) + ((0x2 * ((uint64_t)x12 * x4)) + ((uint64_t)x14 * x2))))))) + (0x239 * ((0x2 * ((uint64_t)x16 * x47)) + ((0x2 * ((uint64_t)x18 * x48)) + ((0x2 * ((uint64_t)x20 * x46)) + ((0x2 * ((uint64_t)x22 * x44)) + ((0x2 * ((uint64_t)x24 * x42)) + ((0x2 * ((uint64_t)x26 * x40)) + ((0x2 * ((uint64_t)x28 * x38)) + ((0x2 * ((uint64_t)x30 * x36)) + ((0x2 * ((uint64_t)x32 * x34)) + ((0x2 * ((uint64_t)x34 * x32)) + ((0x2 * ((uint64_t)x36 * x30)) + ((0x2 * ((uint64_t)x38 * x28)) + ((0x2 * ((uint64_t)x40 * x26)) + ((0x2 * ((uint64_t)x42 * x24)) + ((0x2 * ((uint64_t)x44 * x22)) + ((0x2 * ((uint64_t)x46 * x20)) + ((0x2 * ((uint64_t)x48 * x18)) + (0x2 * ((uint64_t)x47 * x16))))))))))))))))))))); - { uint64_t x68 = ((((uint64_t)x2 * x12) + (((uint64_t)x4 * x10) + (((uint64_t)x6 * x8) + (((uint64_t)x8 * x6) + (((uint64_t)x10 * x4) + ((uint64_t)x12 * x2)))))) + (0x239 * (((uint64_t)x14 * x47) + ((0x2 * ((uint64_t)x16 * x48)) + (((uint64_t)x18 * x46) + ((0x2 * ((uint64_t)x20 * x44)) + (((uint64_t)x22 * x42) + ((0x2 * ((uint64_t)x24 * x40)) + (((uint64_t)x26 * x38) + ((0x2 * ((uint64_t)x28 * x36)) + (((uint64_t)x30 * x34) + ((0x2 * ((uint64_t)x32 * x32)) + (((uint64_t)x34 * x30) + ((0x2 * ((uint64_t)x36 * x28)) + (((uint64_t)x38 * x26) + ((0x2 * ((uint64_t)x40 * x24)) + (((uint64_t)x42 * x22) + ((0x2 * ((uint64_t)x44 * x20)) + (((uint64_t)x46 * x18) + ((0x2 * ((uint64_t)x48 * x16)) + ((uint64_t)x47 * x14))))))))))))))))))))); - { uint64_t x69 = ((((uint64_t)x2 * x10) + ((0x2 * ((uint64_t)x4 * x8)) + (((uint64_t)x6 * x6) + ((0x2 * ((uint64_t)x8 * x4)) + ((uint64_t)x10 * x2))))) + (0x239 * ((0x2 * ((uint64_t)x12 * x47)) + ((0x2 * ((uint64_t)x14 * x48)) + ((0x2 * ((uint64_t)x16 * x46)) + ((0x2 * ((uint64_t)x18 * x44)) + ((0x2 * ((uint64_t)x20 * x42)) + ((0x2 * ((uint64_t)x22 * x40)) + ((0x2 * ((uint64_t)x24 * x38)) + ((0x2 * ((uint64_t)x26 * x36)) + ((0x2 * ((uint64_t)x28 * x34)) + ((0x2 * ((uint64_t)x30 * x32)) + ((0x2 * ((uint64_t)x32 * x30)) + ((0x2 * ((uint64_t)x34 * x28)) + ((0x2 * ((uint64_t)x36 * x26)) + ((0x2 * ((uint64_t)x38 * x24)) + ((0x2 * ((uint64_t)x40 * x22)) + ((0x2 * ((uint64_t)x42 * x20)) + ((0x2 * ((uint64_t)x44 * x18)) + ((0x2 * ((uint64_t)x46 * x16)) + ((0x2 * ((uint64_t)x48 * x14)) + (0x2 * ((uint64_t)x47 * x12))))))))))))))))))))))); - { uint64_t x70 = ((((uint64_t)x2 * x8) + (((uint64_t)x4 * x6) + (((uint64_t)x6 * x4) + ((uint64_t)x8 * x2)))) + (0x239 * (((uint64_t)x10 * x47) + ((0x2 * ((uint64_t)x12 * x48)) + (((uint64_t)x14 * x46) + ((0x2 * ((uint64_t)x16 * x44)) + (((uint64_t)x18 * x42) + ((0x2 * ((uint64_t)x20 * x40)) + (((uint64_t)x22 * x38) + ((0x2 * ((uint64_t)x24 * x36)) + (((uint64_t)x26 * x34) + ((0x2 * ((uint64_t)x28 * x32)) + (((uint64_t)x30 * x30) + ((0x2 * ((uint64_t)x32 * x28)) + (((uint64_t)x34 * x26) + ((0x2 * ((uint64_t)x36 * x24)) + (((uint64_t)x38 * x22) + ((0x2 * ((uint64_t)x40 * x20)) + (((uint64_t)x42 * x18) + ((0x2 * ((uint64_t)x44 * x16)) + (((uint64_t)x46 * x14) + ((0x2 * ((uint64_t)x48 * x12)) + ((uint64_t)x47 * x10))))))))))))))))))))))); - { uint64_t x71 = ((((uint64_t)x2 * x6) + ((0x2 * ((uint64_t)x4 * x4)) + ((uint64_t)x6 * x2))) + (0x239 * ((0x2 * ((uint64_t)x8 * x47)) + ((0x2 * ((uint64_t)x10 * x48)) + ((0x2 * ((uint64_t)x12 * x46)) + ((0x2 * ((uint64_t)x14 * x44)) + ((0x2 * ((uint64_t)x16 * x42)) + ((0x2 * ((uint64_t)x18 * x40)) + ((0x2 * ((uint64_t)x20 * x38)) + ((0x2 * ((uint64_t)x22 * x36)) + ((0x2 * ((uint64_t)x24 * x34)) + ((0x2 * ((uint64_t)x26 * x32)) + ((0x2 * ((uint64_t)x28 * x30)) + ((0x2 * ((uint64_t)x30 * x28)) + ((0x2 * ((uint64_t)x32 * x26)) + ((0x2 * ((uint64_t)x34 * x24)) + ((0x2 * ((uint64_t)x36 * x22)) + ((0x2 * ((uint64_t)x38 * x20)) + ((0x2 * ((uint64_t)x40 * x18)) + ((0x2 * ((uint64_t)x42 * x16)) + ((0x2 * ((uint64_t)x44 * x14)) + ((0x2 * ((uint64_t)x46 * x12)) + ((0x2 * ((uint64_t)x48 * x10)) + (0x2 * ((uint64_t)x47 * x8))))))))))))))))))))))))); - { uint64_t x72 = ((((uint64_t)x2 * x4) + ((uint64_t)x4 * x2)) + (0x239 * (((uint64_t)x6 * x47) + ((0x2 * ((uint64_t)x8 * x48)) + (((uint64_t)x10 * x46) + ((0x2 * ((uint64_t)x12 * x44)) + (((uint64_t)x14 * x42) + ((0x2 * ((uint64_t)x16 * x40)) + (((uint64_t)x18 * x38) + ((0x2 * ((uint64_t)x20 * x36)) + (((uint64_t)x22 * x34) + ((0x2 * ((uint64_t)x24 * x32)) + (((uint64_t)x26 * x30) + ((0x2 * ((uint64_t)x28 * x28)) + (((uint64_t)x30 * x26) + ((0x2 * ((uint64_t)x32 * x24)) + (((uint64_t)x34 * x22) + ((0x2 * ((uint64_t)x36 * x20)) + (((uint64_t)x38 * x18) + ((0x2 * ((uint64_t)x40 * x16)) + (((uint64_t)x42 * x14) + ((0x2 * ((uint64_t)x44 * x12)) + (((uint64_t)x46 * x10) + ((0x2 * ((uint64_t)x48 * x8)) + ((uint64_t)x47 * x6))))))))))))))))))))))))); - { uint64_t x73 = (((uint64_t)x2 * x2) + (0x239 * ((0x2 * ((uint64_t)x4 * x47)) + ((0x2 * ((uint64_t)x6 * x48)) + ((0x2 * ((uint64_t)x8 * x46)) + ((0x2 * ((uint64_t)x10 * x44)) + ((0x2 * ((uint64_t)x12 * x42)) + ((0x2 * ((uint64_t)x14 * x40)) + ((0x2 * ((uint64_t)x16 * x38)) + ((0x2 * ((uint64_t)x18 * x36)) + ((0x2 * ((uint64_t)x20 * x34)) + ((0x2 * ((uint64_t)x22 * x32)) + ((0x2 * ((uint64_t)x24 * x30)) + ((0x2 * ((uint64_t)x26 * x28)) + ((0x2 * ((uint64_t)x28 * x26)) + ((0x2 * ((uint64_t)x30 * x24)) + ((0x2 * ((uint64_t)x32 * x22)) + ((0x2 * ((uint64_t)x34 * x20)) + ((0x2 * ((uint64_t)x36 * x18)) + ((0x2 * ((uint64_t)x38 * x16)) + ((0x2 * ((uint64_t)x40 * x14)) + ((0x2 * ((uint64_t)x42 * x12)) + ((0x2 * ((uint64_t)x44 * x10)) + ((0x2 * ((uint64_t)x46 * x8)) + ((0x2 * ((uint64_t)x48 * x6)) + (0x2 * ((uint64_t)x47 * x4))))))))))))))))))))))))))); - { uint64_t x74 = (x73 >> 0x15); - { uint32_t x75 = ((uint32_t)x73 & 0x1fffff); - { uint64_t x76 = (x74 + x72); - { uint64_t x77 = (x76 >> 0x14); - { uint32_t x78 = ((uint32_t)x76 & 0xfffff); - { uint64_t x79 = (x77 + x71); - { uint64_t x80 = (x79 >> 0x15); - { uint32_t x81 = ((uint32_t)x79 & 0x1fffff); - { uint64_t x82 = (x80 + x70); - { uint64_t x83 = (x82 >> 0x14); - { uint32_t x84 = ((uint32_t)x82 & 0xfffff); - { uint64_t x85 = (x83 + x69); - { uint64_t x86 = (x85 >> 0x15); - { uint32_t x87 = ((uint32_t)x85 & 0x1fffff); - { uint64_t x88 = (x86 + x68); - { uint64_t x89 = (x88 >> 0x14); - { uint32_t x90 = ((uint32_t)x88 & 0xfffff); - { uint64_t x91 = (x89 + x67); - { uint64_t x92 = (x91 >> 0x15); - { uint32_t x93 = ((uint32_t)x91 & 0x1fffff); - { uint64_t x94 = (x92 + x66); - { uint64_t x95 = (x94 >> 0x14); - { uint32_t x96 = ((uint32_t)x94 & 0xfffff); - { uint64_t x97 = (x95 + x65); - { uint64_t x98 = (x97 >> 0x15); - { uint32_t x99 = ((uint32_t)x97 & 0x1fffff); - { uint64_t x100 = (x98 + x64); - { uint64_t x101 = (x100 >> 0x14); - { uint32_t x102 = ((uint32_t)x100 & 0xfffff); - { uint64_t x103 = (x101 + x63); - { uint64_t x104 = (x103 >> 0x15); - { uint32_t x105 = ((uint32_t)x103 & 0x1fffff); - { uint64_t x106 = (x104 + x62); - { uint64_t x107 = (x106 >> 0x14); - { uint32_t x108 = ((uint32_t)x106 & 0xfffff); - { uint64_t x109 = (x107 + x61); - { uint64_t x110 = (x109 >> 0x15); - { uint32_t x111 = ((uint32_t)x109 & 0x1fffff); - { uint64_t x112 = (x110 + x60); - { uint64_t x113 = (x112 >> 0x14); - { uint32_t x114 = ((uint32_t)x112 & 0xfffff); - { uint64_t x115 = (x113 + x59); - { uint64_t x116 = (x115 >> 0x15); - { uint32_t x117 = ((uint32_t)x115 & 0x1fffff); - { uint64_t x118 = (x116 + x58); - { uint64_t x119 = (x118 >> 0x14); - { uint32_t x120 = ((uint32_t)x118 & 0xfffff); - { uint64_t x121 = (x119 + x57); - { uint64_t x122 = (x121 >> 0x15); - { uint32_t x123 = ((uint32_t)x121 & 0x1fffff); - { uint64_t x124 = (x122 + x56); - { uint64_t x125 = (x124 >> 0x14); - { uint32_t x126 = ((uint32_t)x124 & 0xfffff); - { uint64_t x127 = (x125 + x55); - { uint64_t x128 = (x127 >> 0x15); - { uint32_t x129 = ((uint32_t)x127 & 0x1fffff); - { uint64_t x130 = (x128 + x54); - { uint64_t x131 = (x130 >> 0x14); - { uint32_t x132 = ((uint32_t)x130 & 0xfffff); - { uint64_t x133 = (x131 + x53); - { uint64_t x134 = (x133 >> 0x15); - { uint32_t x135 = ((uint32_t)x133 & 0x1fffff); - { uint64_t x136 = (x134 + x52); - { uint64_t x137 = (x136 >> 0x14); - { uint32_t x138 = ((uint32_t)x136 & 0xfffff); - { uint64_t x139 = (x137 + x51); - { uint64_t x140 = (x139 >> 0x15); - { uint32_t x141 = ((uint32_t)x139 & 0x1fffff); - { uint64_t x142 = (x140 + x50); - { uint64_t x143 = (x142 >> 0x14); - { uint32_t x144 = ((uint32_t)x142 & 0xfffff); - { uint64_t x145 = (x143 + x49); - { uint32_t x146 = (uint32_t) (x145 >> 0x14); - { uint32_t x147 = ((uint32_t)x145 & 0xfffff); - { uint64_t x148 = (x75 + ((uint64_t)0x239 * x146)); - { uint32_t x149 = (uint32_t) (x148 >> 0x15); - { uint32_t x150 = ((uint32_t)x148 & 0x1fffff); - { uint32_t x151 = (x149 + x78); - { uint32_t x152 = (x151 >> 0x14); - { uint32_t x153 = (x151 & 0xfffff); - out[0] = x150; - out[1] = x153; - out[2] = (x152 + x81); - out[3] = x84; - out[4] = x87; - out[5] = x90; - out[6] = x93; - out[7] = x96; - out[8] = x99; - out[9] = x102; - out[10] = x105; - out[11] = x108; - out[12] = x111; - out[13] = x114; - out[14] = x117; - out[15] = x120; - out[16] = x123; - out[17] = x126; - out[18] = x129; - out[19] = x132; - out[20] = x135; - out[21] = x138; - out[22] = x141; - out[23] = x144; - out[24] = x147; - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesquare.v b/src/Specific/solinas32_2e512m569_25limbs/fesquare.v deleted file mode 100644 index 1bd784456..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesquare.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition square : - { square : feBW_loose -> feBW_tight - | forall a, phiBW_tight (square a) = F.mul (phiBW_loose a) (phiBW_loose a) }. -Proof. - Set Ltac Profiling. - Time synthesize_square (). - Show Ltac Profile. -Time Defined. - -Print Assumptions square. diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesquareDisplay.log b/src/Specific/solinas32_2e512m569_25limbs/fesquareDisplay.log deleted file mode 100644 index 656e9ee16..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesquareDisplay.log +++ /dev/null @@ -1,112 +0,0 @@ -λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x47, x48, x46, x44, x42, x40, x38, x36, x34, x32, x30, x28, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core, - uint64_t x49 = (((uint64_t)x2 * x47) + ((0x2 * ((uint64_t)x4 * x48)) + (((uint64_t)x6 * x46) + ((0x2 * ((uint64_t)x8 * x44)) + (((uint64_t)x10 * x42) + ((0x2 * ((uint64_t)x12 * x40)) + (((uint64_t)x14 * x38) + ((0x2 * ((uint64_t)x16 * x36)) + (((uint64_t)x18 * x34) + ((0x2 * ((uint64_t)x20 * x32)) + (((uint64_t)x22 * x30) + ((0x2 * ((uint64_t)x24 * x28)) + (((uint64_t)x26 * x26) + ((0x2 * ((uint64_t)x28 * x24)) + (((uint64_t)x30 * x22) + ((0x2 * ((uint64_t)x32 * x20)) + (((uint64_t)x34 * x18) + ((0x2 * ((uint64_t)x36 * x16)) + (((uint64_t)x38 * x14) + ((0x2 * ((uint64_t)x40 * x12)) + (((uint64_t)x42 * x10) + ((0x2 * ((uint64_t)x44 * x8)) + (((uint64_t)x46 * x6) + ((0x2 * ((uint64_t)x48 * x4)) + ((uint64_t)x47 * x2))))))))))))))))))))))))); - uint64_t x50 = ((((uint64_t)x2 * x48) + (((uint64_t)x4 * x46) + (((uint64_t)x6 * x44) + (((uint64_t)x8 * x42) + (((uint64_t)x10 * x40) + (((uint64_t)x12 * x38) + (((uint64_t)x14 * x36) + (((uint64_t)x16 * x34) + (((uint64_t)x18 * x32) + (((uint64_t)x20 * x30) + (((uint64_t)x22 * x28) + (((uint64_t)x24 * x26) + (((uint64_t)x26 * x24) + (((uint64_t)x28 * x22) + (((uint64_t)x30 * x20) + (((uint64_t)x32 * x18) + (((uint64_t)x34 * x16) + (((uint64_t)x36 * x14) + (((uint64_t)x38 * x12) + (((uint64_t)x40 * x10) + (((uint64_t)x42 * x8) + (((uint64_t)x44 * x6) + (((uint64_t)x46 * x4) + ((uint64_t)x48 * x2)))))))))))))))))))))))) + (0x239 * ((uint64_t)x47 * x47))); - uint64_t x51 = ((((uint64_t)x2 * x46) + ((0x2 * ((uint64_t)x4 * x44)) + (((uint64_t)x6 * x42) + ((0x2 * ((uint64_t)x8 * x40)) + (((uint64_t)x10 * x38) + ((0x2 * ((uint64_t)x12 * x36)) + (((uint64_t)x14 * x34) + ((0x2 * ((uint64_t)x16 * x32)) + (((uint64_t)x18 * x30) + ((0x2 * ((uint64_t)x20 * x28)) + (((uint64_t)x22 * x26) + ((0x2 * ((uint64_t)x24 * x24)) + (((uint64_t)x26 * x22) + ((0x2 * ((uint64_t)x28 * x20)) + (((uint64_t)x30 * x18) + ((0x2 * ((uint64_t)x32 * x16)) + (((uint64_t)x34 * x14) + ((0x2 * ((uint64_t)x36 * x12)) + (((uint64_t)x38 * x10) + ((0x2 * ((uint64_t)x40 * x8)) + (((uint64_t)x42 * x6) + ((0x2 * ((uint64_t)x44 * x4)) + ((uint64_t)x46 * x2))))))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x48 * x47)) + (0x2 * ((uint64_t)x47 * x48))))); - uint64_t x52 = ((((uint64_t)x2 * x44) + (((uint64_t)x4 * x42) + (((uint64_t)x6 * x40) + (((uint64_t)x8 * x38) + (((uint64_t)x10 * x36) + (((uint64_t)x12 * x34) + (((uint64_t)x14 * x32) + (((uint64_t)x16 * x30) + (((uint64_t)x18 * x28) + (((uint64_t)x20 * x26) + (((uint64_t)x22 * x24) + (((uint64_t)x24 * x22) + (((uint64_t)x26 * x20) + (((uint64_t)x28 * x18) + (((uint64_t)x30 * x16) + (((uint64_t)x32 * x14) + (((uint64_t)x34 * x12) + (((uint64_t)x36 * x10) + (((uint64_t)x38 * x8) + (((uint64_t)x40 * x6) + (((uint64_t)x42 * x4) + ((uint64_t)x44 * x2)))))))))))))))))))))) + (0x239 * (((uint64_t)x46 * x47) + ((0x2 * ((uint64_t)x48 * x48)) + ((uint64_t)x47 * x46))))); - uint64_t x53 = ((((uint64_t)x2 * x42) + ((0x2 * ((uint64_t)x4 * x40)) + (((uint64_t)x6 * x38) + ((0x2 * ((uint64_t)x8 * x36)) + (((uint64_t)x10 * x34) + ((0x2 * ((uint64_t)x12 * x32)) + (((uint64_t)x14 * x30) + ((0x2 * ((uint64_t)x16 * x28)) + (((uint64_t)x18 * x26) + ((0x2 * ((uint64_t)x20 * x24)) + (((uint64_t)x22 * x22) + ((0x2 * ((uint64_t)x24 * x20)) + (((uint64_t)x26 * x18) + ((0x2 * ((uint64_t)x28 * x16)) + (((uint64_t)x30 * x14) + ((0x2 * ((uint64_t)x32 * x12)) + (((uint64_t)x34 * x10) + ((0x2 * ((uint64_t)x36 * x8)) + (((uint64_t)x38 * x6) + ((0x2 * ((uint64_t)x40 * x4)) + ((uint64_t)x42 * x2))))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x44 * x47)) + ((0x2 * ((uint64_t)x46 * x48)) + ((0x2 * ((uint64_t)x48 * x46)) + (0x2 * ((uint64_t)x47 * x44))))))); - uint64_t x54 = ((((uint64_t)x2 * x40) + (((uint64_t)x4 * x38) + (((uint64_t)x6 * x36) + (((uint64_t)x8 * x34) + (((uint64_t)x10 * x32) + (((uint64_t)x12 * x30) + (((uint64_t)x14 * x28) + (((uint64_t)x16 * x26) + (((uint64_t)x18 * x24) + (((uint64_t)x20 * x22) + (((uint64_t)x22 * x20) + (((uint64_t)x24 * x18) + (((uint64_t)x26 * x16) + (((uint64_t)x28 * x14) + (((uint64_t)x30 * x12) + (((uint64_t)x32 * x10) + (((uint64_t)x34 * x8) + (((uint64_t)x36 * x6) + (((uint64_t)x38 * x4) + ((uint64_t)x40 * x2)))))))))))))))))))) + (0x239 * (((uint64_t)x42 * x47) + ((0x2 * ((uint64_t)x44 * x48)) + (((uint64_t)x46 * x46) + ((0x2 * ((uint64_t)x48 * x44)) + ((uint64_t)x47 * x42))))))); - uint64_t x55 = ((((uint64_t)x2 * x38) + ((0x2 * ((uint64_t)x4 * x36)) + (((uint64_t)x6 * x34) + ((0x2 * ((uint64_t)x8 * x32)) + (((uint64_t)x10 * x30) + ((0x2 * ((uint64_t)x12 * x28)) + (((uint64_t)x14 * x26) + ((0x2 * ((uint64_t)x16 * x24)) + (((uint64_t)x18 * x22) + ((0x2 * ((uint64_t)x20 * x20)) + (((uint64_t)x22 * x18) + ((0x2 * ((uint64_t)x24 * x16)) + (((uint64_t)x26 * x14) + ((0x2 * ((uint64_t)x28 * x12)) + (((uint64_t)x30 * x10) + ((0x2 * ((uint64_t)x32 * x8)) + (((uint64_t)x34 * x6) + ((0x2 * ((uint64_t)x36 * x4)) + ((uint64_t)x38 * x2))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x40 * x47)) + ((0x2 * ((uint64_t)x42 * x48)) + ((0x2 * ((uint64_t)x44 * x46)) + ((0x2 * ((uint64_t)x46 * x44)) + ((0x2 * ((uint64_t)x48 * x42)) + (0x2 * ((uint64_t)x47 * x40))))))))); - uint64_t x56 = ((((uint64_t)x2 * x36) + (((uint64_t)x4 * x34) + (((uint64_t)x6 * x32) + (((uint64_t)x8 * x30) + (((uint64_t)x10 * x28) + (((uint64_t)x12 * x26) + (((uint64_t)x14 * x24) + (((uint64_t)x16 * x22) + (((uint64_t)x18 * x20) + (((uint64_t)x20 * x18) + (((uint64_t)x22 * x16) + (((uint64_t)x24 * x14) + (((uint64_t)x26 * x12) + (((uint64_t)x28 * x10) + (((uint64_t)x30 * x8) + (((uint64_t)x32 * x6) + (((uint64_t)x34 * x4) + ((uint64_t)x36 * x2)))))))))))))))))) + (0x239 * (((uint64_t)x38 * x47) + ((0x2 * ((uint64_t)x40 * x48)) + (((uint64_t)x42 * x46) + ((0x2 * ((uint64_t)x44 * x44)) + (((uint64_t)x46 * x42) + ((0x2 * ((uint64_t)x48 * x40)) + ((uint64_t)x47 * x38))))))))); - uint64_t x57 = ((((uint64_t)x2 * x34) + ((0x2 * ((uint64_t)x4 * x32)) + (((uint64_t)x6 * x30) + ((0x2 * ((uint64_t)x8 * x28)) + (((uint64_t)x10 * x26) + ((0x2 * ((uint64_t)x12 * x24)) + (((uint64_t)x14 * x22) + ((0x2 * ((uint64_t)x16 * x20)) + (((uint64_t)x18 * x18) + ((0x2 * ((uint64_t)x20 * x16)) + (((uint64_t)x22 * x14) + ((0x2 * ((uint64_t)x24 * x12)) + (((uint64_t)x26 * x10) + ((0x2 * ((uint64_t)x28 * x8)) + (((uint64_t)x30 * x6) + ((0x2 * ((uint64_t)x32 * x4)) + ((uint64_t)x34 * x2))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x36 * x47)) + ((0x2 * ((uint64_t)x38 * x48)) + ((0x2 * ((uint64_t)x40 * x46)) + ((0x2 * ((uint64_t)x42 * x44)) + ((0x2 * ((uint64_t)x44 * x42)) + ((0x2 * ((uint64_t)x46 * x40)) + ((0x2 * ((uint64_t)x48 * x38)) + (0x2 * ((uint64_t)x47 * x36))))))))))); - uint64_t x58 = ((((uint64_t)x2 * x32) + (((uint64_t)x4 * x30) + (((uint64_t)x6 * x28) + (((uint64_t)x8 * x26) + (((uint64_t)x10 * x24) + (((uint64_t)x12 * x22) + (((uint64_t)x14 * x20) + (((uint64_t)x16 * x18) + (((uint64_t)x18 * x16) + (((uint64_t)x20 * x14) + (((uint64_t)x22 * x12) + (((uint64_t)x24 * x10) + (((uint64_t)x26 * x8) + (((uint64_t)x28 * x6) + (((uint64_t)x30 * x4) + ((uint64_t)x32 * x2)))))))))))))))) + (0x239 * (((uint64_t)x34 * x47) + ((0x2 * ((uint64_t)x36 * x48)) + (((uint64_t)x38 * x46) + ((0x2 * ((uint64_t)x40 * x44)) + (((uint64_t)x42 * x42) + ((0x2 * ((uint64_t)x44 * x40)) + (((uint64_t)x46 * x38) + ((0x2 * ((uint64_t)x48 * x36)) + ((uint64_t)x47 * x34))))))))))); - uint64_t x59 = ((((uint64_t)x2 * x30) + ((0x2 * ((uint64_t)x4 * x28)) + (((uint64_t)x6 * x26) + ((0x2 * ((uint64_t)x8 * x24)) + (((uint64_t)x10 * x22) + ((0x2 * ((uint64_t)x12 * x20)) + (((uint64_t)x14 * x18) + ((0x2 * ((uint64_t)x16 * x16)) + (((uint64_t)x18 * x14) + ((0x2 * ((uint64_t)x20 * x12)) + (((uint64_t)x22 * x10) + ((0x2 * ((uint64_t)x24 * x8)) + (((uint64_t)x26 * x6) + ((0x2 * ((uint64_t)x28 * x4)) + ((uint64_t)x30 * x2))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x32 * x47)) + ((0x2 * ((uint64_t)x34 * x48)) + ((0x2 * ((uint64_t)x36 * x46)) + ((0x2 * ((uint64_t)x38 * x44)) + ((0x2 * ((uint64_t)x40 * x42)) + ((0x2 * ((uint64_t)x42 * x40)) + ((0x2 * ((uint64_t)x44 * x38)) + ((0x2 * ((uint64_t)x46 * x36)) + ((0x2 * ((uint64_t)x48 * x34)) + (0x2 * ((uint64_t)x47 * x32))))))))))))); - uint64_t x60 = ((((uint64_t)x2 * x28) + (((uint64_t)x4 * x26) + (((uint64_t)x6 * x24) + (((uint64_t)x8 * x22) + (((uint64_t)x10 * x20) + (((uint64_t)x12 * x18) + (((uint64_t)x14 * x16) + (((uint64_t)x16 * x14) + (((uint64_t)x18 * x12) + (((uint64_t)x20 * x10) + (((uint64_t)x22 * x8) + (((uint64_t)x24 * x6) + (((uint64_t)x26 * x4) + ((uint64_t)x28 * x2)))))))))))))) + (0x239 * (((uint64_t)x30 * x47) + ((0x2 * ((uint64_t)x32 * x48)) + (((uint64_t)x34 * x46) + ((0x2 * ((uint64_t)x36 * x44)) + (((uint64_t)x38 * x42) + ((0x2 * ((uint64_t)x40 * x40)) + (((uint64_t)x42 * x38) + ((0x2 * ((uint64_t)x44 * x36)) + (((uint64_t)x46 * x34) + ((0x2 * ((uint64_t)x48 * x32)) + ((uint64_t)x47 * x30))))))))))))); - uint64_t x61 = ((((uint64_t)x2 * x26) + ((0x2 * ((uint64_t)x4 * x24)) + (((uint64_t)x6 * x22) + ((0x2 * ((uint64_t)x8 * x20)) + (((uint64_t)x10 * x18) + ((0x2 * ((uint64_t)x12 * x16)) + (((uint64_t)x14 * x14) + ((0x2 * ((uint64_t)x16 * x12)) + (((uint64_t)x18 * x10) + ((0x2 * ((uint64_t)x20 * x8)) + (((uint64_t)x22 * x6) + ((0x2 * ((uint64_t)x24 * x4)) + ((uint64_t)x26 * x2))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x28 * x47)) + ((0x2 * ((uint64_t)x30 * x48)) + ((0x2 * ((uint64_t)x32 * x46)) + ((0x2 * ((uint64_t)x34 * x44)) + ((0x2 * ((uint64_t)x36 * x42)) + ((0x2 * ((uint64_t)x38 * x40)) + ((0x2 * ((uint64_t)x40 * x38)) + ((0x2 * ((uint64_t)x42 * x36)) + ((0x2 * ((uint64_t)x44 * x34)) + ((0x2 * ((uint64_t)x46 * x32)) + ((0x2 * ((uint64_t)x48 * x30)) + (0x2 * ((uint64_t)x47 * x28))))))))))))))); - uint64_t x62 = ((((uint64_t)x2 * x24) + (((uint64_t)x4 * x22) + (((uint64_t)x6 * x20) + (((uint64_t)x8 * x18) + (((uint64_t)x10 * x16) + (((uint64_t)x12 * x14) + (((uint64_t)x14 * x12) + (((uint64_t)x16 * x10) + (((uint64_t)x18 * x8) + (((uint64_t)x20 * x6) + (((uint64_t)x22 * x4) + ((uint64_t)x24 * x2)))))))))))) + (0x239 * (((uint64_t)x26 * x47) + ((0x2 * ((uint64_t)x28 * x48)) + (((uint64_t)x30 * x46) + ((0x2 * ((uint64_t)x32 * x44)) + (((uint64_t)x34 * x42) + ((0x2 * ((uint64_t)x36 * x40)) + (((uint64_t)x38 * x38) + ((0x2 * ((uint64_t)x40 * x36)) + (((uint64_t)x42 * x34) + ((0x2 * ((uint64_t)x44 * x32)) + (((uint64_t)x46 * x30) + ((0x2 * ((uint64_t)x48 * x28)) + ((uint64_t)x47 * x26))))))))))))))); - uint64_t x63 = ((((uint64_t)x2 * x22) + ((0x2 * ((uint64_t)x4 * x20)) + (((uint64_t)x6 * x18) + ((0x2 * ((uint64_t)x8 * x16)) + (((uint64_t)x10 * x14) + ((0x2 * ((uint64_t)x12 * x12)) + (((uint64_t)x14 * x10) + ((0x2 * ((uint64_t)x16 * x8)) + (((uint64_t)x18 * x6) + ((0x2 * ((uint64_t)x20 * x4)) + ((uint64_t)x22 * x2))))))))))) + (0x239 * ((0x2 * ((uint64_t)x24 * x47)) + ((0x2 * ((uint64_t)x26 * x48)) + ((0x2 * ((uint64_t)x28 * x46)) + ((0x2 * ((uint64_t)x30 * x44)) + ((0x2 * ((uint64_t)x32 * x42)) + ((0x2 * ((uint64_t)x34 * x40)) + ((0x2 * ((uint64_t)x36 * x38)) + ((0x2 * ((uint64_t)x38 * x36)) + ((0x2 * ((uint64_t)x40 * x34)) + ((0x2 * ((uint64_t)x42 * x32)) + ((0x2 * ((uint64_t)x44 * x30)) + ((0x2 * ((uint64_t)x46 * x28)) + ((0x2 * ((uint64_t)x48 * x26)) + (0x2 * ((uint64_t)x47 * x24))))))))))))))))); - uint64_t x64 = ((((uint64_t)x2 * x20) + (((uint64_t)x4 * x18) + (((uint64_t)x6 * x16) + (((uint64_t)x8 * x14) + (((uint64_t)x10 * x12) + (((uint64_t)x12 * x10) + (((uint64_t)x14 * x8) + (((uint64_t)x16 * x6) + (((uint64_t)x18 * x4) + ((uint64_t)x20 * x2)))))))))) + (0x239 * (((uint64_t)x22 * x47) + ((0x2 * ((uint64_t)x24 * x48)) + (((uint64_t)x26 * x46) + ((0x2 * ((uint64_t)x28 * x44)) + (((uint64_t)x30 * x42) + ((0x2 * ((uint64_t)x32 * x40)) + (((uint64_t)x34 * x38) + ((0x2 * ((uint64_t)x36 * x36)) + (((uint64_t)x38 * x34) + ((0x2 * ((uint64_t)x40 * x32)) + (((uint64_t)x42 * x30) + ((0x2 * ((uint64_t)x44 * x28)) + (((uint64_t)x46 * x26) + ((0x2 * ((uint64_t)x48 * x24)) + ((uint64_t)x47 * x22))))))))))))))))); - uint64_t x65 = ((((uint64_t)x2 * x18) + ((0x2 * ((uint64_t)x4 * x16)) + (((uint64_t)x6 * x14) + ((0x2 * ((uint64_t)x8 * x12)) + (((uint64_t)x10 * x10) + ((0x2 * ((uint64_t)x12 * x8)) + (((uint64_t)x14 * x6) + ((0x2 * ((uint64_t)x16 * x4)) + ((uint64_t)x18 * x2))))))))) + (0x239 * ((0x2 * ((uint64_t)x20 * x47)) + ((0x2 * ((uint64_t)x22 * x48)) + ((0x2 * ((uint64_t)x24 * x46)) + ((0x2 * ((uint64_t)x26 * x44)) + ((0x2 * ((uint64_t)x28 * x42)) + ((0x2 * ((uint64_t)x30 * x40)) + ((0x2 * ((uint64_t)x32 * x38)) + ((0x2 * ((uint64_t)x34 * x36)) + ((0x2 * ((uint64_t)x36 * x34)) + ((0x2 * ((uint64_t)x38 * x32)) + ((0x2 * ((uint64_t)x40 * x30)) + ((0x2 * ((uint64_t)x42 * x28)) + ((0x2 * ((uint64_t)x44 * x26)) + ((0x2 * ((uint64_t)x46 * x24)) + ((0x2 * ((uint64_t)x48 * x22)) + (0x2 * ((uint64_t)x47 * x20))))))))))))))))))); - uint64_t x66 = ((((uint64_t)x2 * x16) + (((uint64_t)x4 * x14) + (((uint64_t)x6 * x12) + (((uint64_t)x8 * x10) + (((uint64_t)x10 * x8) + (((uint64_t)x12 * x6) + (((uint64_t)x14 * x4) + ((uint64_t)x16 * x2)))))))) + (0x239 * (((uint64_t)x18 * x47) + ((0x2 * ((uint64_t)x20 * x48)) + (((uint64_t)x22 * x46) + ((0x2 * ((uint64_t)x24 * x44)) + (((uint64_t)x26 * x42) + ((0x2 * ((uint64_t)x28 * x40)) + (((uint64_t)x30 * x38) + ((0x2 * ((uint64_t)x32 * x36)) + (((uint64_t)x34 * x34) + ((0x2 * ((uint64_t)x36 * x32)) + (((uint64_t)x38 * x30) + ((0x2 * ((uint64_t)x40 * x28)) + (((uint64_t)x42 * x26) + ((0x2 * ((uint64_t)x44 * x24)) + (((uint64_t)x46 * x22) + ((0x2 * ((uint64_t)x48 * x20)) + ((uint64_t)x47 * x18))))))))))))))))))); - uint64_t x67 = ((((uint64_t)x2 * x14) + ((0x2 * ((uint64_t)x4 * x12)) + (((uint64_t)x6 * x10) + ((0x2 * ((uint64_t)x8 * x8)) + (((uint64_t)x10 * x6) + ((0x2 * ((uint64_t)x12 * x4)) + ((uint64_t)x14 * x2))))))) + (0x239 * ((0x2 * ((uint64_t)x16 * x47)) + ((0x2 * ((uint64_t)x18 * x48)) + ((0x2 * ((uint64_t)x20 * x46)) + ((0x2 * ((uint64_t)x22 * x44)) + ((0x2 * ((uint64_t)x24 * x42)) + ((0x2 * ((uint64_t)x26 * x40)) + ((0x2 * ((uint64_t)x28 * x38)) + ((0x2 * ((uint64_t)x30 * x36)) + ((0x2 * ((uint64_t)x32 * x34)) + ((0x2 * ((uint64_t)x34 * x32)) + ((0x2 * ((uint64_t)x36 * x30)) + ((0x2 * ((uint64_t)x38 * x28)) + ((0x2 * ((uint64_t)x40 * x26)) + ((0x2 * ((uint64_t)x42 * x24)) + ((0x2 * ((uint64_t)x44 * x22)) + ((0x2 * ((uint64_t)x46 * x20)) + ((0x2 * ((uint64_t)x48 * x18)) + (0x2 * ((uint64_t)x47 * x16))))))))))))))))))))); - uint64_t x68 = ((((uint64_t)x2 * x12) + (((uint64_t)x4 * x10) + (((uint64_t)x6 * x8) + (((uint64_t)x8 * x6) + (((uint64_t)x10 * x4) + ((uint64_t)x12 * x2)))))) + (0x239 * (((uint64_t)x14 * x47) + ((0x2 * ((uint64_t)x16 * x48)) + (((uint64_t)x18 * x46) + ((0x2 * ((uint64_t)x20 * x44)) + (((uint64_t)x22 * x42) + ((0x2 * ((uint64_t)x24 * x40)) + (((uint64_t)x26 * x38) + ((0x2 * ((uint64_t)x28 * x36)) + (((uint64_t)x30 * x34) + ((0x2 * ((uint64_t)x32 * x32)) + (((uint64_t)x34 * x30) + ((0x2 * ((uint64_t)x36 * x28)) + (((uint64_t)x38 * x26) + ((0x2 * ((uint64_t)x40 * x24)) + (((uint64_t)x42 * x22) + ((0x2 * ((uint64_t)x44 * x20)) + (((uint64_t)x46 * x18) + ((0x2 * ((uint64_t)x48 * x16)) + ((uint64_t)x47 * x14))))))))))))))))))))); - uint64_t x69 = ((((uint64_t)x2 * x10) + ((0x2 * ((uint64_t)x4 * x8)) + (((uint64_t)x6 * x6) + ((0x2 * ((uint64_t)x8 * x4)) + ((uint64_t)x10 * x2))))) + (0x239 * ((0x2 * ((uint64_t)x12 * x47)) + ((0x2 * ((uint64_t)x14 * x48)) + ((0x2 * ((uint64_t)x16 * x46)) + ((0x2 * ((uint64_t)x18 * x44)) + ((0x2 * ((uint64_t)x20 * x42)) + ((0x2 * ((uint64_t)x22 * x40)) + ((0x2 * ((uint64_t)x24 * x38)) + ((0x2 * ((uint64_t)x26 * x36)) + ((0x2 * ((uint64_t)x28 * x34)) + ((0x2 * ((uint64_t)x30 * x32)) + ((0x2 * ((uint64_t)x32 * x30)) + ((0x2 * ((uint64_t)x34 * x28)) + ((0x2 * ((uint64_t)x36 * x26)) + ((0x2 * ((uint64_t)x38 * x24)) + ((0x2 * ((uint64_t)x40 * x22)) + ((0x2 * ((uint64_t)x42 * x20)) + ((0x2 * ((uint64_t)x44 * x18)) + ((0x2 * ((uint64_t)x46 * x16)) + ((0x2 * ((uint64_t)x48 * x14)) + (0x2 * ((uint64_t)x47 * x12))))))))))))))))))))))); - uint64_t x70 = ((((uint64_t)x2 * x8) + (((uint64_t)x4 * x6) + (((uint64_t)x6 * x4) + ((uint64_t)x8 * x2)))) + (0x239 * (((uint64_t)x10 * x47) + ((0x2 * ((uint64_t)x12 * x48)) + (((uint64_t)x14 * x46) + ((0x2 * ((uint64_t)x16 * x44)) + (((uint64_t)x18 * x42) + ((0x2 * ((uint64_t)x20 * x40)) + (((uint64_t)x22 * x38) + ((0x2 * ((uint64_t)x24 * x36)) + (((uint64_t)x26 * x34) + ((0x2 * ((uint64_t)x28 * x32)) + (((uint64_t)x30 * x30) + ((0x2 * ((uint64_t)x32 * x28)) + (((uint64_t)x34 * x26) + ((0x2 * ((uint64_t)x36 * x24)) + (((uint64_t)x38 * x22) + ((0x2 * ((uint64_t)x40 * x20)) + (((uint64_t)x42 * x18) + ((0x2 * ((uint64_t)x44 * x16)) + (((uint64_t)x46 * x14) + ((0x2 * ((uint64_t)x48 * x12)) + ((uint64_t)x47 * x10))))))))))))))))))))))); - uint64_t x71 = ((((uint64_t)x2 * x6) + ((0x2 * ((uint64_t)x4 * x4)) + ((uint64_t)x6 * x2))) + (0x239 * ((0x2 * ((uint64_t)x8 * x47)) + ((0x2 * ((uint64_t)x10 * x48)) + ((0x2 * ((uint64_t)x12 * x46)) + ((0x2 * ((uint64_t)x14 * x44)) + ((0x2 * ((uint64_t)x16 * x42)) + ((0x2 * ((uint64_t)x18 * x40)) + ((0x2 * ((uint64_t)x20 * x38)) + ((0x2 * ((uint64_t)x22 * x36)) + ((0x2 * ((uint64_t)x24 * x34)) + ((0x2 * ((uint64_t)x26 * x32)) + ((0x2 * ((uint64_t)x28 * x30)) + ((0x2 * ((uint64_t)x30 * x28)) + ((0x2 * ((uint64_t)x32 * x26)) + ((0x2 * ((uint64_t)x34 * x24)) + ((0x2 * ((uint64_t)x36 * x22)) + ((0x2 * ((uint64_t)x38 * x20)) + ((0x2 * ((uint64_t)x40 * x18)) + ((0x2 * ((uint64_t)x42 * x16)) + ((0x2 * ((uint64_t)x44 * x14)) + ((0x2 * ((uint64_t)x46 * x12)) + ((0x2 * ((uint64_t)x48 * x10)) + (0x2 * ((uint64_t)x47 * x8))))))))))))))))))))))))); - uint64_t x72 = ((((uint64_t)x2 * x4) + ((uint64_t)x4 * x2)) + (0x239 * (((uint64_t)x6 * x47) + ((0x2 * ((uint64_t)x8 * x48)) + (((uint64_t)x10 * x46) + ((0x2 * ((uint64_t)x12 * x44)) + (((uint64_t)x14 * x42) + ((0x2 * ((uint64_t)x16 * x40)) + (((uint64_t)x18 * x38) + ((0x2 * ((uint64_t)x20 * x36)) + (((uint64_t)x22 * x34) + ((0x2 * ((uint64_t)x24 * x32)) + (((uint64_t)x26 * x30) + ((0x2 * ((uint64_t)x28 * x28)) + (((uint64_t)x30 * x26) + ((0x2 * ((uint64_t)x32 * x24)) + (((uint64_t)x34 * x22) + ((0x2 * ((uint64_t)x36 * x20)) + (((uint64_t)x38 * x18) + ((0x2 * ((uint64_t)x40 * x16)) + (((uint64_t)x42 * x14) + ((0x2 * ((uint64_t)x44 * x12)) + (((uint64_t)x46 * x10) + ((0x2 * ((uint64_t)x48 * x8)) + ((uint64_t)x47 * x6))))))))))))))))))))))))); - uint64_t x73 = (((uint64_t)x2 * x2) + (0x239 * ((0x2 * ((uint64_t)x4 * x47)) + ((0x2 * ((uint64_t)x6 * x48)) + ((0x2 * ((uint64_t)x8 * x46)) + ((0x2 * ((uint64_t)x10 * x44)) + ((0x2 * ((uint64_t)x12 * x42)) + ((0x2 * ((uint64_t)x14 * x40)) + ((0x2 * ((uint64_t)x16 * x38)) + ((0x2 * ((uint64_t)x18 * x36)) + ((0x2 * ((uint64_t)x20 * x34)) + ((0x2 * ((uint64_t)x22 * x32)) + ((0x2 * ((uint64_t)x24 * x30)) + ((0x2 * ((uint64_t)x26 * x28)) + ((0x2 * ((uint64_t)x28 * x26)) + ((0x2 * ((uint64_t)x30 * x24)) + ((0x2 * ((uint64_t)x32 * x22)) + ((0x2 * ((uint64_t)x34 * x20)) + ((0x2 * ((uint64_t)x36 * x18)) + ((0x2 * ((uint64_t)x38 * x16)) + ((0x2 * ((uint64_t)x40 * x14)) + ((0x2 * ((uint64_t)x42 * x12)) + ((0x2 * ((uint64_t)x44 * x10)) + ((0x2 * ((uint64_t)x46 * x8)) + ((0x2 * ((uint64_t)x48 * x6)) + (0x2 * ((uint64_t)x47 * x4))))))))))))))))))))))))))); - uint64_t x74 = (x73 >> 0x15); - uint32_t x75 = ((uint32_t)x73 & 0x1fffff); - uint64_t x76 = (x74 + x72); - uint64_t x77 = (x76 >> 0x14); - uint32_t x78 = ((uint32_t)x76 & 0xfffff); - uint64_t x79 = (x77 + x71); - uint64_t x80 = (x79 >> 0x15); - uint32_t x81 = ((uint32_t)x79 & 0x1fffff); - uint64_t x82 = (x80 + x70); - uint64_t x83 = (x82 >> 0x14); - uint32_t x84 = ((uint32_t)x82 & 0xfffff); - uint64_t x85 = (x83 + x69); - uint64_t x86 = (x85 >> 0x15); - uint32_t x87 = ((uint32_t)x85 & 0x1fffff); - uint64_t x88 = (x86 + x68); - uint64_t x89 = (x88 >> 0x14); - uint32_t x90 = ((uint32_t)x88 & 0xfffff); - uint64_t x91 = (x89 + x67); - uint64_t x92 = (x91 >> 0x15); - uint32_t x93 = ((uint32_t)x91 & 0x1fffff); - uint64_t x94 = (x92 + x66); - uint64_t x95 = (x94 >> 0x14); - uint32_t x96 = ((uint32_t)x94 & 0xfffff); - uint64_t x97 = (x95 + x65); - uint64_t x98 = (x97 >> 0x15); - uint32_t x99 = ((uint32_t)x97 & 0x1fffff); - uint64_t x100 = (x98 + x64); - uint64_t x101 = (x100 >> 0x14); - uint32_t x102 = ((uint32_t)x100 & 0xfffff); - uint64_t x103 = (x101 + x63); - uint64_t x104 = (x103 >> 0x15); - uint32_t x105 = ((uint32_t)x103 & 0x1fffff); - uint64_t x106 = (x104 + x62); - uint64_t x107 = (x106 >> 0x14); - uint32_t x108 = ((uint32_t)x106 & 0xfffff); - uint64_t x109 = (x107 + x61); - uint64_t x110 = (x109 >> 0x15); - uint32_t x111 = ((uint32_t)x109 & 0x1fffff); - uint64_t x112 = (x110 + x60); - uint64_t x113 = (x112 >> 0x14); - uint32_t x114 = ((uint32_t)x112 & 0xfffff); - uint64_t x115 = (x113 + x59); - uint64_t x116 = (x115 >> 0x15); - uint32_t x117 = ((uint32_t)x115 & 0x1fffff); - uint64_t x118 = (x116 + x58); - uint64_t x119 = (x118 >> 0x14); - uint32_t x120 = ((uint32_t)x118 & 0xfffff); - uint64_t x121 = (x119 + x57); - uint64_t x122 = (x121 >> 0x15); - uint32_t x123 = ((uint32_t)x121 & 0x1fffff); - uint64_t x124 = (x122 + x56); - uint64_t x125 = (x124 >> 0x14); - uint32_t x126 = ((uint32_t)x124 & 0xfffff); - uint64_t x127 = (x125 + x55); - uint64_t x128 = (x127 >> 0x15); - uint32_t x129 = ((uint32_t)x127 & 0x1fffff); - uint64_t x130 = (x128 + x54); - uint64_t x131 = (x130 >> 0x14); - uint32_t x132 = ((uint32_t)x130 & 0xfffff); - uint64_t x133 = (x131 + x53); - uint64_t x134 = (x133 >> 0x15); - uint32_t x135 = ((uint32_t)x133 & 0x1fffff); - uint64_t x136 = (x134 + x52); - uint64_t x137 = (x136 >> 0x14); - uint32_t x138 = ((uint32_t)x136 & 0xfffff); - uint64_t x139 = (x137 + x51); - uint64_t x140 = (x139 >> 0x15); - uint32_t x141 = ((uint32_t)x139 & 0x1fffff); - uint64_t x142 = (x140 + x50); - uint64_t x143 = (x142 >> 0x14); - uint32_t x144 = ((uint32_t)x142 & 0xfffff); - uint64_t x145 = (x143 + x49); - uint32_t x146 = (uint32_t) (x145 >> 0x14); - uint32_t x147 = ((uint32_t)x145 & 0xfffff); - uint64_t x148 = (x75 + ((uint64_t)0x239 * x146)); - uint32_t x149 = (uint32_t) (x148 >> 0x15); - uint32_t x150 = ((uint32_t)x148 & 0x1fffff); - uint32_t x151 = (x149 + x78); - uint32_t x152 = (x151 >> 0x14); - uint32_t x153 = (x151 & 0xfffff); - return (Return x147, Return x144, Return x141, Return x138, Return x135, Return x132, Return x129, Return x126, Return x123, Return x120, Return x117, Return x114, Return x111, Return x108, Return x105, Return x102, Return x99, Return x96, Return x93, Return x90, Return x87, Return x84, (x152 + x81), Return x153, Return x150)) -x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesquareDisplay.v b/src/Specific/solinas32_2e512m569_25limbs/fesquareDisplay.v deleted file mode 100644 index 603896064..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesquareDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.fesquare. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display square. diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesub.c b/src/Specific/solinas32_2e512m569_25limbs/fesub.c deleted file mode 100644 index fb6b779e3..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesub.c +++ /dev/null @@ -1,78 +0,0 @@ -static void fesub(uint32_t out[25], const uint32_t in1[25], const uint32_t in2[25]) { - { const uint32_t x50 = in1[24]; - { const uint32_t x51 = in1[23]; - { const uint32_t x49 = in1[22]; - { const uint32_t x47 = in1[21]; - { const uint32_t x45 = in1[20]; - { const uint32_t x43 = in1[19]; - { const uint32_t x41 = in1[18]; - { const uint32_t x39 = in1[17]; - { const uint32_t x37 = in1[16]; - { const uint32_t x35 = in1[15]; - { const uint32_t x33 = in1[14]; - { const uint32_t x31 = in1[13]; - { const uint32_t x29 = in1[12]; - { const uint32_t x27 = in1[11]; - { const uint32_t x25 = in1[10]; - { const uint32_t x23 = in1[9]; - { const uint32_t x21 = in1[8]; - { const uint32_t x19 = in1[7]; - { const uint32_t x17 = in1[6]; - { const uint32_t x15 = in1[5]; - { const uint32_t x13 = in1[4]; - { const uint32_t x11 = in1[3]; - { const uint32_t x9 = in1[2]; - { const uint32_t x7 = in1[1]; - { const uint32_t x5 = in1[0]; - { const uint32_t x98 = in2[24]; - { const uint32_t x99 = in2[23]; - { const uint32_t x97 = in2[22]; - { const uint32_t x95 = in2[21]; - { const uint32_t x93 = in2[20]; - { const uint32_t x91 = in2[19]; - { const uint32_t x89 = in2[18]; - { const uint32_t x87 = in2[17]; - { const uint32_t x85 = in2[16]; - { const uint32_t x83 = in2[15]; - { const uint32_t x81 = in2[14]; - { const uint32_t x79 = in2[13]; - { const uint32_t x77 = in2[12]; - { const uint32_t x75 = in2[11]; - { const uint32_t x73 = in2[10]; - { const uint32_t x71 = in2[9]; - { const uint32_t x69 = in2[8]; - { const uint32_t x67 = in2[7]; - { const uint32_t x65 = in2[6]; - { const uint32_t x63 = in2[5]; - { const uint32_t x61 = in2[4]; - { const uint32_t x59 = in2[3]; - { const uint32_t x57 = in2[2]; - { const uint32_t x55 = in2[1]; - { const uint32_t x53 = in2[0]; - out[0] = ((0x3ffb8e + x5) - x53); - out[1] = ((0x1ffffe + x7) - x55); - out[2] = ((0x3ffffe + x9) - x57); - out[3] = ((0x1ffffe + x11) - x59); - out[4] = ((0x3ffffe + x13) - x61); - out[5] = ((0x1ffffe + x15) - x63); - out[6] = ((0x3ffffe + x17) - x65); - out[7] = ((0x1ffffe + x19) - x67); - out[8] = ((0x3ffffe + x21) - x69); - out[9] = ((0x1ffffe + x23) - x71); - out[10] = ((0x3ffffe + x25) - x73); - out[11] = ((0x1ffffe + x27) - x75); - out[12] = ((0x3ffffe + x29) - x77); - out[13] = ((0x1ffffe + x31) - x79); - out[14] = ((0x3ffffe + x33) - x81); - out[15] = ((0x1ffffe + x35) - x83); - out[16] = ((0x3ffffe + x37) - x85); - out[17] = ((0x1ffffe + x39) - x87); - out[18] = ((0x3ffffe + x41) - x89); - out[19] = ((0x1ffffe + x43) - x91); - out[20] = ((0x3ffffe + x45) - x93); - out[21] = ((0x1ffffe + x47) - x95); - out[22] = ((0x3ffffe + x49) - x97); - out[23] = ((0x1ffffe + x51) - x99); - out[24] = ((0x1ffffe + x50) - x98); - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesub.v b/src/Specific/solinas32_2e512m569_25limbs/fesub.v deleted file mode 100644 index 4b1c1bc8d..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesub.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition sub : - { sub : feBW_tight -> feBW_tight -> feBW_loose - | forall a b, phiBW_loose (sub a b) = F.sub (phiBW_tight a) (phiBW_tight b) }. -Proof. - Set Ltac Profiling. - Time synthesize_sub (). - Show Ltac Profile. -Time Defined. - -Print Assumptions sub. diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesubDisplay.log b/src/Specific/solinas32_2e512m569_25limbs/fesubDisplay.log deleted file mode 100644 index bb633ea33..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesubDisplay.log +++ /dev/null @@ -1,7 +0,0 @@ -λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x50, x51, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x98, x99, x97, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59, x57, x55, x53))%core, - (((0x1ffffe + x50) - x98), ((0x1ffffe + x51) - x99), ((0x3ffffe + x49) - x97), ((0x1ffffe + x47) - x95), ((0x3ffffe + x45) - x93), ((0x1ffffe + x43) - x91), ((0x3ffffe + x41) - x89), ((0x1ffffe + x39) - x87), ((0x3ffffe + x37) - x85), ((0x1ffffe + x35) - x83), ((0x3ffffe + x33) - x81), ((0x1ffffe + x31) - x79), ((0x3ffffe + x29) - x77), ((0x1ffffe + x27) - x75), ((0x3ffffe + x25) - x73), ((0x1ffffe + x23) - x71), ((0x3ffffe + x21) - x69), ((0x1ffffe + x19) - x67), ((0x3ffffe + x17) - x65), ((0x1ffffe + x15) - x63), ((0x3ffffe + x13) - x61), ((0x1ffffe + x11) - x59), ((0x3ffffe + x9) - x57), ((0x1ffffe + x7) - x55), ((0x3ffb8e + x5) - x53))) -(x, x0)%core - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e512m569_25limbs/fesubDisplay.v b/src/Specific/solinas32_2e512m569_25limbs/fesubDisplay.v deleted file mode 100644 index 310043be0..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/fesubDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.fesub. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display sub. diff --git a/src/Specific/solinas32_2e512m569_25limbs/freeze.c b/src/Specific/solinas32_2e512m569_25limbs/freeze.c deleted file mode 100644 index dc8d24656..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/freeze.c +++ /dev/null @@ -1,129 +0,0 @@ -static void freeze(uint32_t out[25], const uint32_t in1[25]) { - { const uint32_t x47 = in1[24]; - { const uint32_t x48 = in1[23]; - { const uint32_t x46 = in1[22]; - { const uint32_t x44 = in1[21]; - { const uint32_t x42 = in1[20]; - { const uint32_t x40 = in1[19]; - { const uint32_t x38 = in1[18]; - { const uint32_t x36 = in1[17]; - { const uint32_t x34 = in1[16]; - { const uint32_t x32 = in1[15]; - { const uint32_t x30 = in1[14]; - { const uint32_t x28 = in1[13]; - { const uint32_t x26 = in1[12]; - { const uint32_t x24 = in1[11]; - { const uint32_t x22 = in1[10]; - { const uint32_t x20 = in1[9]; - { const uint32_t x18 = in1[8]; - { const uint32_t x16 = in1[7]; - { const uint32_t x14 = in1[6]; - { const uint32_t x12 = in1[5]; - { const uint32_t x10 = in1[4]; - { const uint32_t x8 = in1[3]; - { const uint32_t x6 = in1[2]; - { const uint32_t x4 = in1[1]; - { const uint32_t x2 = in1[0]; - { uint32_t x50, uint8_t x51 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, 0x1ffdc7); - { uint32_t x53, uint8_t x54 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x51, Return x4, 0xfffff); - { uint32_t x56, uint8_t x57 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x54, Return x6, 0x1fffff); - { uint32_t x59, uint8_t x60 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x57, Return x8, 0xfffff); - { uint32_t x62, uint8_t x63 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x60, Return x10, 0x1fffff); - { uint32_t x65, uint8_t x66 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x63, Return x12, 0xfffff); - { uint32_t x68, uint8_t x69 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x66, Return x14, 0x1fffff); - { uint32_t x71, uint8_t x72 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x69, Return x16, 0xfffff); - { uint32_t x74, uint8_t x75 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x72, Return x18, 0x1fffff); - { uint32_t x77, uint8_t x78 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x75, Return x20, 0xfffff); - { uint32_t x80, uint8_t x81 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x78, Return x22, 0x1fffff); - { uint32_t x83, uint8_t x84 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x81, Return x24, 0xfffff); - { uint32_t x86, uint8_t x87 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x84, Return x26, 0x1fffff); - { uint32_t x89, uint8_t x90 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x87, Return x28, 0xfffff); - { uint32_t x92, uint8_t x93 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x90, Return x30, 0x1fffff); - { uint32_t x95, uint8_t x96 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x93, Return x32, 0xfffff); - { uint32_t x98, uint8_t x99 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x96, Return x34, 0x1fffff); - { uint32_t x101, uint8_t x102 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x99, Return x36, 0xfffff); - { uint32_t x104, uint8_t x105 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x102, Return x38, 0x1fffff); - { uint32_t x107, uint8_t x108 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x105, Return x40, 0xfffff); - { uint32_t x110, uint8_t x111 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x108, Return x42, 0x1fffff); - { uint32_t x113, uint8_t x114 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x111, Return x44, 0xfffff); - { uint32_t x116, uint8_t x117 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x114, Return x46, 0x1fffff); - { uint32_t x119, uint8_t x120 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x117, Return x48, 0xfffff); - { uint32_t x122, uint8_t x123 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x120, Return x47, 0xfffff); - { uint32_t x124 = cmovznz32(x123, 0x0, 0xffffffff); - { uint32_t x125 = (x124 & 0x1ffdc7); - { uint32_t x127, uint8_t x128 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x50, Return x125); - { uint32_t x129 = (x124 & 0xfffff); - { uint32_t x131, uint8_t x132 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x128, Return x53, Return x129); - { uint32_t x133 = (x124 & 0x1fffff); - { uint32_t x135, uint8_t x136 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x132, Return x56, Return x133); - { uint32_t x137 = (x124 & 0xfffff); - { uint32_t x139, uint8_t x140 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x136, Return x59, Return x137); - { uint32_t x141 = (x124 & 0x1fffff); - { uint32_t x143, uint8_t x144 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x140, Return x62, Return x141); - { uint32_t x145 = (x124 & 0xfffff); - { uint32_t x147, uint8_t x148 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x144, Return x65, Return x145); - { uint32_t x149 = (x124 & 0x1fffff); - { uint32_t x151, uint8_t x152 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x148, Return x68, Return x149); - { uint32_t x153 = (x124 & 0xfffff); - { uint32_t x155, uint8_t x156 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x152, Return x71, Return x153); - { uint32_t x157 = (x124 & 0x1fffff); - { uint32_t x159, uint8_t x160 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x156, Return x74, Return x157); - { uint32_t x161 = (x124 & 0xfffff); - { uint32_t x163, uint8_t x164 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x160, Return x77, Return x161); - { uint32_t x165 = (x124 & 0x1fffff); - { uint32_t x167, uint8_t x168 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x164, Return x80, Return x165); - { uint32_t x169 = (x124 & 0xfffff); - { uint32_t x171, uint8_t x172 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x168, Return x83, Return x169); - { uint32_t x173 = (x124 & 0x1fffff); - { uint32_t x175, uint8_t x176 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x172, Return x86, Return x173); - { uint32_t x177 = (x124 & 0xfffff); - { uint32_t x179, uint8_t x180 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x176, Return x89, Return x177); - { uint32_t x181 = (x124 & 0x1fffff); - { uint32_t x183, uint8_t x184 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x180, Return x92, Return x181); - { uint32_t x185 = (x124 & 0xfffff); - { uint32_t x187, uint8_t x188 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x184, Return x95, Return x185); - { uint32_t x189 = (x124 & 0x1fffff); - { uint32_t x191, uint8_t x192 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x188, Return x98, Return x189); - { uint32_t x193 = (x124 & 0xfffff); - { uint32_t x195, uint8_t x196 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x192, Return x101, Return x193); - { uint32_t x197 = (x124 & 0x1fffff); - { uint32_t x199, uint8_t x200 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x196, Return x104, Return x197); - { uint32_t x201 = (x124 & 0xfffff); - { uint32_t x203, uint8_t x204 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x200, Return x107, Return x201); - { uint32_t x205 = (x124 & 0x1fffff); - { uint32_t x207, uint8_t x208 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x204, Return x110, Return x205); - { uint32_t x209 = (x124 & 0xfffff); - { uint32_t x211, uint8_t x212 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x208, Return x113, Return x209); - { uint32_t x213 = (x124 & 0x1fffff); - { uint32_t x215, uint8_t x216 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x212, Return x116, Return x213); - { uint32_t x217 = (x124 & 0xfffff); - { uint32_t x219, uint8_t x220 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x216, Return x119, Return x217); - { uint32_t x221 = (x124 & 0xfffff); - { uint32_t x223, uint8_t _ = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x220, Return x122, Return x221); - out[0] = x127; - out[1] = x131; - out[2] = x135; - out[3] = x139; - out[4] = x143; - out[5] = x147; - out[6] = x151; - out[7] = x155; - out[8] = x159; - out[9] = x163; - out[10] = x167; - out[11] = x171; - out[12] = x175; - out[13] = x179; - out[14] = x183; - out[15] = x187; - out[16] = x191; - out[17] = x195; - out[18] = x199; - out[19] = x203; - out[20] = x207; - out[21] = x211; - out[22] = x215; - out[23] = x219; - out[24] = x223; - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/solinas32_2e512m569_25limbs/freeze.v b/src/Specific/solinas32_2e512m569_25limbs/freeze.v deleted file mode 100644 index 6e0180849..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/freeze.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.Synthesis. - -(* TODO : change this to field once field isomorphism happens *) -Definition freeze : - { freeze : feBW_tight -> feBW_limbwidths - | forall a, phiBW_limbwidths (freeze a) = phiBW_tight a }. -Proof. - Set Ltac Profiling. - Time synthesize_freeze (). - Show Ltac Profile. -Time Defined. - -Print Assumptions freeze. diff --git a/src/Specific/solinas32_2e512m569_25limbs/freezeDisplay.log b/src/Specific/solinas32_2e512m569_25limbs/freezeDisplay.log deleted file mode 100644 index 0e95dcf8e..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/freezeDisplay.log +++ /dev/null @@ -1,83 +0,0 @@ -λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x47, x48, x46, x44, x42, x40, x38, x36, x34, x32, x30, x28, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core, - uint32_t x50, uint8_t x51 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, 0x1ffdc7); - uint32_t x53, uint8_t x54 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x51, Return x4, 0xfffff); - uint32_t x56, uint8_t x57 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x54, Return x6, 0x1fffff); - uint32_t x59, uint8_t x60 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x57, Return x8, 0xfffff); - uint32_t x62, uint8_t x63 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x60, Return x10, 0x1fffff); - uint32_t x65, uint8_t x66 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x63, Return x12, 0xfffff); - uint32_t x68, uint8_t x69 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x66, Return x14, 0x1fffff); - uint32_t x71, uint8_t x72 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x69, Return x16, 0xfffff); - uint32_t x74, uint8_t x75 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x72, Return x18, 0x1fffff); - uint32_t x77, uint8_t x78 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x75, Return x20, 0xfffff); - uint32_t x80, uint8_t x81 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x78, Return x22, 0x1fffff); - uint32_t x83, uint8_t x84 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x81, Return x24, 0xfffff); - uint32_t x86, uint8_t x87 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x84, Return x26, 0x1fffff); - uint32_t x89, uint8_t x90 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x87, Return x28, 0xfffff); - uint32_t x92, uint8_t x93 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x90, Return x30, 0x1fffff); - uint32_t x95, uint8_t x96 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x93, Return x32, 0xfffff); - uint32_t x98, uint8_t x99 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x96, Return x34, 0x1fffff); - uint32_t x101, uint8_t x102 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x99, Return x36, 0xfffff); - uint32_t x104, uint8_t x105 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x102, Return x38, 0x1fffff); - uint32_t x107, uint8_t x108 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x105, Return x40, 0xfffff); - uint32_t x110, uint8_t x111 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x108, Return x42, 0x1fffff); - uint32_t x113, uint8_t x114 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x111, Return x44, 0xfffff); - uint32_t x116, uint8_t x117 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x114, Return x46, 0x1fffff); - uint32_t x119, uint8_t x120 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x117, Return x48, 0xfffff); - uint32_t x122, uint8_t x123 = Op (Syntax.SubWithGetBorrow 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x120, Return x47, 0xfffff); - uint32_t x124 = cmovznz32(x123, 0x0, 0xffffffff); - uint32_t x125 = (x124 & 0x1ffdc7); - uint32_t x127, uint8_t x128 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x50, Return x125); - uint32_t x129 = (x124 & 0xfffff); - uint32_t x131, uint8_t x132 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x128, Return x53, Return x129); - uint32_t x133 = (x124 & 0x1fffff); - uint32_t x135, uint8_t x136 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x132, Return x56, Return x133); - uint32_t x137 = (x124 & 0xfffff); - uint32_t x139, uint8_t x140 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x136, Return x59, Return x137); - uint32_t x141 = (x124 & 0x1fffff); - uint32_t x143, uint8_t x144 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x140, Return x62, Return x141); - uint32_t x145 = (x124 & 0xfffff); - uint32_t x147, uint8_t x148 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x144, Return x65, Return x145); - uint32_t x149 = (x124 & 0x1fffff); - uint32_t x151, uint8_t x152 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x148, Return x68, Return x149); - uint32_t x153 = (x124 & 0xfffff); - uint32_t x155, uint8_t x156 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x152, Return x71, Return x153); - uint32_t x157 = (x124 & 0x1fffff); - uint32_t x159, uint8_t x160 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x156, Return x74, Return x157); - uint32_t x161 = (x124 & 0xfffff); - uint32_t x163, uint8_t x164 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x160, Return x77, Return x161); - uint32_t x165 = (x124 & 0x1fffff); - uint32_t x167, uint8_t x168 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x164, Return x80, Return x165); - uint32_t x169 = (x124 & 0xfffff); - uint32_t x171, uint8_t x172 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x168, Return x83, Return x169); - uint32_t x173 = (x124 & 0x1fffff); - uint32_t x175, uint8_t x176 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x172, Return x86, Return x173); - uint32_t x177 = (x124 & 0xfffff); - uint32_t x179, uint8_t x180 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x176, Return x89, Return x177); - uint32_t x181 = (x124 & 0x1fffff); - uint32_t x183, uint8_t x184 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x180, Return x92, Return x181); - uint32_t x185 = (x124 & 0xfffff); - uint32_t x187, uint8_t x188 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x184, Return x95, Return x185); - uint32_t x189 = (x124 & 0x1fffff); - uint32_t x191, uint8_t x192 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x188, Return x98, Return x189); - uint32_t x193 = (x124 & 0xfffff); - uint32_t x195, uint8_t x196 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x192, Return x101, Return x193); - uint32_t x197 = (x124 & 0x1fffff); - uint32_t x199, uint8_t x200 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x196, Return x104, Return x197); - uint32_t x201 = (x124 & 0xfffff); - uint32_t x203, uint8_t x204 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x200, Return x107, Return x201); - uint32_t x205 = (x124 & 0x1fffff); - uint32_t x207, uint8_t x208 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x204, Return x110, Return x205); - uint32_t x209 = (x124 & 0xfffff); - uint32_t x211, uint8_t x212 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x208, Return x113, Return x209); - uint32_t x213 = (x124 & 0x1fffff); - uint32_t x215, uint8_t x216 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x212, Return x116, Return x213); - uint32_t x217 = (x124 & 0xfffff); - uint32_t x219, uint8_t x220 = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x216, Return x119, Return x217); - uint32_t x221 = (x124 & 0xfffff); - uint32_t x223, uint8_t _ = Op (Syntax.AddWithGetCarry 20 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x220, Return x122, Return x221); - (Return x223, Return x219, Return x215, Return x211, Return x207, Return x203, Return x199, Return x195, Return x191, Return x187, Return x183, Return x179, Return x175, Return x171, Return x167, Return x163, Return x159, Return x155, Return x151, Return x147, Return x143, Return x139, Return x135, Return x131, Return x127)) -x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e512m569_25limbs/freezeDisplay.v b/src/Specific/solinas32_2e512m569_25limbs/freezeDisplay.v deleted file mode 100644 index 38122eaa7..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/freezeDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas32_2e512m569_25limbs.freeze. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display freeze. diff --git a/src/Specific/solinas32_2e512m569_25limbs/py_interpreter.sh b/src/Specific/solinas32_2e512m569_25limbs/py_interpreter.sh deleted file mode 100755 index 9ad22d5c1..000000000 --- a/src/Specific/solinas32_2e512m569_25limbs/py_interpreter.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh -set -eu - -/usr/bin/env python3 "$@" -Dq='2**512 - 569' -Dmodulus_bytes='20 + 12/25' -Da24='121665' |