From 3ca227f1137e6a3b65bc33f5689e1c230d591595 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Tue, 8 Jan 2019 04:21:38 -0500
Subject: remove old pipeline

---
 .../solinas64_2e512m569_10limbs/CurveParameters.v  | 39 -----------
 .../solinas64_2e512m569_10limbs/Synthesis.v        |  9 ---
 .../solinas64_2e512m569_10limbs/compiler.sh        |  4 --
 .../solinas64_2e512m569_10limbs/compilerxx.sh      |  4 --
 src/Specific/solinas64_2e512m569_10limbs/feadd.c   | 33 ---------
 src/Specific/solinas64_2e512m569_10limbs/feadd.v   | 14 ----
 .../solinas64_2e512m569_10limbs/feaddDisplay.log   |  7 --
 .../solinas64_2e512m569_10limbs/feaddDisplay.v     |  4 --
 src/Specific/solinas64_2e512m569_10limbs/fecarry.v | 14 ----
 .../solinas64_2e512m569_10limbs/fecarryDisplay.v   |  4 --
 src/Specific/solinas64_2e512m569_10limbs/femul.c   | 78 ----------------------
 src/Specific/solinas64_2e512m569_10limbs/femul.v   | 14 ----
 .../solinas64_2e512m569_10limbs/femulDisplay.log   | 52 ---------------
 .../solinas64_2e512m569_10limbs/femulDisplay.v     |  4 --
 .../solinas64_2e512m569_10limbs/fesquare.c         | 68 -------------------
 .../solinas64_2e512m569_10limbs/fesquare.v         | 14 ----
 .../fesquareDisplay.log                            | 52 ---------------
 .../solinas64_2e512m569_10limbs/fesquareDisplay.v  |  4 --
 src/Specific/solinas64_2e512m569_10limbs/fesub.c   | 33 ---------
 src/Specific/solinas64_2e512m569_10limbs/fesub.v   | 14 ----
 .../solinas64_2e512m569_10limbs/fesubDisplay.log   |  7 --
 .../solinas64_2e512m569_10limbs/fesubDisplay.v     |  4 --
 src/Specific/solinas64_2e512m569_10limbs/freeze.c  | 54 ---------------
 src/Specific/solinas64_2e512m569_10limbs/freeze.v  | 14 ----
 .../solinas64_2e512m569_10limbs/freezeDisplay.log  | 38 -----------
 .../solinas64_2e512m569_10limbs/freezeDisplay.v    |  4 --
 .../solinas64_2e512m569_10limbs/py_interpreter.sh  |  4 --
 27 files changed, 590 deletions(-)
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/CurveParameters.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/Synthesis.v
 delete mode 100755 src/Specific/solinas64_2e512m569_10limbs/compiler.sh
 delete mode 100755 src/Specific/solinas64_2e512m569_10limbs/compilerxx.sh
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/feadd.c
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/feadd.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/feaddDisplay.log
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/feaddDisplay.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fecarry.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fecarryDisplay.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/femul.c
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/femul.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/femulDisplay.log
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/femulDisplay.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesquare.c
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesquare.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesquareDisplay.log
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesquareDisplay.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesub.c
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesub.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesubDisplay.log
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/fesubDisplay.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/freeze.c
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/freeze.v
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/freezeDisplay.log
 delete mode 100644 src/Specific/solinas64_2e512m569_10limbs/freezeDisplay.v
 delete mode 100755 src/Specific/solinas64_2e512m569_10limbs/py_interpreter.sh

(limited to 'src/Specific/solinas64_2e512m569_10limbs')

diff --git a/src/Specific/solinas64_2e512m569_10limbs/CurveParameters.v b/src/Specific/solinas64_2e512m569_10limbs/CurveParameters.v
deleted file mode 100644
index 13d176bc4..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/CurveParameters.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^512 - 569
-Base: 51.2
-***)
-
-Definition curve : CurveParameters :=
-  {|
-    sz := 10%nat;
-    base := 51 + 1/5;
-    bitwidth := 64;
-    s := 2^512;
-    c := [(1, 569)];
-    carry_chains := Some [seq 0 (pred 10); [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/solinas64_2e512m569_10limbs/Synthesis.v b/src/Specific/solinas64_2e512m569_10limbs/Synthesis.v
deleted file mode 100644
index 414fbe02f..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.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/solinas64_2e512m569_10limbs/compiler.sh b/src/Specific/solinas64_2e512m569_10limbs/compiler.sh
deleted file mode 100755
index 139748419..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/compiler.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-clang -fbracket-depth=999999 -march=native -mbmi2 -mtune=native -std=gnu11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{52,51,51,51,51,52,51,51,51,51}' -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='10' -Dq_mpz='(1_mpz<<512) - 569' "$@"
diff --git a/src/Specific/solinas64_2e512m569_10limbs/compilerxx.sh b/src/Specific/solinas64_2e512m569_10limbs/compilerxx.sh
deleted file mode 100755
index d335d47c8..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/compilerxx.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-clang++ -fbracket-depth=999999 -march=native -mbmi2 -mtune=native -std=gnu++11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{52,51,51,51,51,52,51,51,51,51}' -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='10' -Dq_mpz='(1_mpz<<512) - 569' "$@"
diff --git a/src/Specific/solinas64_2e512m569_10limbs/feadd.c b/src/Specific/solinas64_2e512m569_10limbs/feadd.c
deleted file mode 100644
index df991e375..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/feadd.c
+++ /dev/null
@@ -1,33 +0,0 @@
-static void feadd(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[10]) {
-  { const uint64_t x20 = in1[9];
-  { const uint64_t x21 = in1[8];
-  { const uint64_t x19 = in1[7];
-  { const uint64_t x17 = in1[6];
-  { const uint64_t x15 = in1[5];
-  { const uint64_t x13 = in1[4];
-  { const uint64_t x11 = in1[3];
-  { const uint64_t x9 = in1[2];
-  { const uint64_t x7 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x38 = in2[9];
-  { const uint64_t x39 = in2[8];
-  { const uint64_t x37 = in2[7];
-  { const uint64_t x35 = in2[6];
-  { const uint64_t x33 = in2[5];
-  { const uint64_t x31 = in2[4];
-  { const uint64_t x29 = in2[3];
-  { const uint64_t x27 = in2[2];
-  { const uint64_t x25 = in2[1];
-  { const uint64_t x23 = in2[0];
-  out[0] = (x5 + x23);
-  out[1] = (x7 + x25);
-  out[2] = (x9 + x27);
-  out[3] = (x11 + x29);
-  out[4] = (x13 + x31);
-  out[5] = (x15 + x33);
-  out[6] = (x17 + x35);
-  out[7] = (x19 + x37);
-  out[8] = (x21 + x39);
-  out[9] = (x20 + x38);
-  }}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e512m569_10limbs/feadd.v b/src/Specific/solinas64_2e512m569_10limbs/feadd.v
deleted file mode 100644
index b5772a500..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/feadd.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.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/solinas64_2e512m569_10limbs/feaddDisplay.log b/src/Specific/solinas64_2e512m569_10limbs/feaddDisplay.log
deleted file mode 100644
index 04176128e..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/feaddDisplay.log
+++ /dev/null
@@ -1,7 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- ((x20 + x38), (x21 + x39), (x19 + x37), (x17 + x35), (x15 + x33), (x13 + x31), (x11 + x29), (x9 + x27), (x7 + x25), (x5 + x23)))
-(x, x0)%core
-     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e512m569_10limbs/feaddDisplay.v b/src/Specific/solinas64_2e512m569_10limbs/feaddDisplay.v
deleted file mode 100644
index b80f582f0..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/feaddDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.feadd.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display add.
diff --git a/src/Specific/solinas64_2e512m569_10limbs/fecarry.v b/src/Specific/solinas64_2e512m569_10limbs/fecarry.v
deleted file mode 100644
index 8e7f05aba..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fecarry.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.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/solinas64_2e512m569_10limbs/fecarryDisplay.v b/src/Specific/solinas64_2e512m569_10limbs/fecarryDisplay.v
deleted file mode 100644
index d6eafdcc8..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fecarryDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.fecarry.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display carry.
diff --git a/src/Specific/solinas64_2e512m569_10limbs/femul.c b/src/Specific/solinas64_2e512m569_10limbs/femul.c
deleted file mode 100644
index 46e0f261b..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/femul.c
+++ /dev/null
@@ -1,78 +0,0 @@
-static void femul(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[10]) {
-  { const uint64_t x20 = in1[9];
-  { const uint64_t x21 = in1[8];
-  { const uint64_t x19 = in1[7];
-  { const uint64_t x17 = in1[6];
-  { const uint64_t x15 = in1[5];
-  { const uint64_t x13 = in1[4];
-  { const uint64_t x11 = in1[3];
-  { const uint64_t x9 = in1[2];
-  { const uint64_t x7 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x38 = in2[9];
-  { const uint64_t x39 = in2[8];
-  { const uint64_t x37 = in2[7];
-  { const uint64_t x35 = in2[6];
-  { const uint64_t x33 = in2[5];
-  { const uint64_t x31 = in2[4];
-  { const uint64_t x29 = in2[3];
-  { const uint64_t x27 = in2[2];
-  { const uint64_t x25 = in2[1];
-  { const uint64_t x23 = in2[0];
-  { uint128_t x40 = (((uint128_t)x5 * x38) + ((0x2 * ((uint128_t)x7 * x39)) + ((0x2 * ((uint128_t)x9 * x37)) + ((0x2 * ((uint128_t)x11 * x35)) + (((uint128_t)x13 * x33) + (((uint128_t)x15 * x31) + ((0x2 * ((uint128_t)x17 * x29)) + ((0x2 * ((uint128_t)x19 * x27)) + ((0x2 * ((uint128_t)x21 * x25)) + ((uint128_t)x20 * x23))))))))));
-  { uint128_t x41 = ((((uint128_t)x5 * x39) + ((0x2 * ((uint128_t)x7 * x37)) + ((0x2 * ((uint128_t)x9 * x35)) + (((uint128_t)x11 * x33) + (((uint128_t)x13 * x31) + (((uint128_t)x15 * x29) + ((0x2 * ((uint128_t)x17 * x27)) + ((0x2 * ((uint128_t)x19 * x25)) + ((uint128_t)x21 * x23))))))))) + (0x239 * ((uint128_t)x20 * x38)));
-  { uint128_t x42 = ((((uint128_t)x5 * x37) + ((0x2 * ((uint128_t)x7 * x35)) + (((uint128_t)x9 * x33) + (((uint128_t)x11 * x31) + (((uint128_t)x13 * x29) + (((uint128_t)x15 * x27) + ((0x2 * ((uint128_t)x17 * x25)) + ((uint128_t)x19 * x23)))))))) + (0x239 * (((uint128_t)x21 * x38) + ((uint128_t)x20 * x39))));
-  { uint128_t x43 = ((((uint128_t)x5 * x35) + (((uint128_t)x7 * x33) + (((uint128_t)x9 * x31) + (((uint128_t)x11 * x29) + (((uint128_t)x13 * x27) + (((uint128_t)x15 * x25) + ((uint128_t)x17 * x23))))))) + (0x239 * (((uint128_t)x19 * x38) + (((uint128_t)x21 * x39) + ((uint128_t)x20 * x37)))));
-  { uint128_t x44 = ((((uint128_t)x5 * x33) + ((0x2 * ((uint128_t)x7 * x31)) + ((0x2 * ((uint128_t)x9 * x29)) + ((0x2 * ((uint128_t)x11 * x27)) + ((0x2 * ((uint128_t)x13 * x25)) + ((uint128_t)x15 * x23)))))) + (0x239 * ((0x2 * ((uint128_t)x17 * x38)) + ((0x2 * ((uint128_t)x19 * x39)) + ((0x2 * ((uint128_t)x21 * x37)) + (0x2 * ((uint128_t)x20 * x35)))))));
-  { uint128_t x45 = ((((uint128_t)x5 * x31) + ((0x2 * ((uint128_t)x7 * x29)) + ((0x2 * ((uint128_t)x9 * x27)) + ((0x2 * ((uint128_t)x11 * x25)) + ((uint128_t)x13 * x23))))) + (0x239 * (((uint128_t)x15 * x38) + ((0x2 * ((uint128_t)x17 * x39)) + ((0x2 * ((uint128_t)x19 * x37)) + ((0x2 * ((uint128_t)x21 * x35)) + ((uint128_t)x20 * x33)))))));
-  { uint128_t x46 = ((((uint128_t)x5 * x29) + ((0x2 * ((uint128_t)x7 * x27)) + ((0x2 * ((uint128_t)x9 * x25)) + ((uint128_t)x11 * x23)))) + (0x239 * (((uint128_t)x13 * x38) + (((uint128_t)x15 * x39) + ((0x2 * ((uint128_t)x17 * x37)) + ((0x2 * ((uint128_t)x19 * x35)) + (((uint128_t)x21 * x33) + ((uint128_t)x20 * x31))))))));
-  { uint128_t x47 = ((((uint128_t)x5 * x27) + ((0x2 * ((uint128_t)x7 * x25)) + ((uint128_t)x9 * x23))) + (0x239 * (((uint128_t)x11 * x38) + (((uint128_t)x13 * x39) + (((uint128_t)x15 * x37) + ((0x2 * ((uint128_t)x17 * x35)) + (((uint128_t)x19 * x33) + (((uint128_t)x21 * x31) + ((uint128_t)x20 * x29)))))))));
-  { uint128_t x48 = ((((uint128_t)x5 * x25) + ((uint128_t)x7 * x23)) + (0x239 * (((uint128_t)x9 * x38) + (((uint128_t)x11 * x39) + (((uint128_t)x13 * x37) + (((uint128_t)x15 * x35) + (((uint128_t)x17 * x33) + (((uint128_t)x19 * x31) + (((uint128_t)x21 * x29) + ((uint128_t)x20 * x27))))))))));
-  { uint128_t x49 = (((uint128_t)x5 * x23) + (0x239 * ((0x2 * ((uint128_t)x7 * x38)) + ((0x2 * ((uint128_t)x9 * x39)) + ((0x2 * ((uint128_t)x11 * x37)) + ((0x2 * ((uint128_t)x13 * x35)) + (((uint128_t)x15 * x33) + ((0x2 * ((uint128_t)x17 * x31)) + ((0x2 * ((uint128_t)x19 * x29)) + ((0x2 * ((uint128_t)x21 * x27)) + (0x2 * ((uint128_t)x20 * x25))))))))))));
-  { uint128_t x50 = (x49 >> 0x34);
-  { uint64_t x51 = ((uint64_t)x49 & 0xfffffffffffff);
-  { uint128_t x52 = (x50 + x48);
-  { uint128_t x53 = (x52 >> 0x33);
-  { uint64_t x54 = ((uint64_t)x52 & 0x7ffffffffffff);
-  { uint128_t x55 = (x53 + x47);
-  { uint128_t x56 = (x55 >> 0x33);
-  { uint64_t x57 = ((uint64_t)x55 & 0x7ffffffffffff);
-  { uint128_t x58 = (x56 + x46);
-  { uint128_t x59 = (x58 >> 0x33);
-  { uint64_t x60 = ((uint64_t)x58 & 0x7ffffffffffff);
-  { uint128_t x61 = (x59 + x45);
-  { uint128_t x62 = (x61 >> 0x33);
-  { uint64_t x63 = ((uint64_t)x61 & 0x7ffffffffffff);
-  { uint128_t x64 = (x62 + x44);
-  { uint128_t x65 = (x64 >> 0x34);
-  { uint64_t x66 = ((uint64_t)x64 & 0xfffffffffffff);
-  { uint128_t x67 = (x65 + x43);
-  { uint128_t x68 = (x67 >> 0x33);
-  { uint64_t x69 = ((uint64_t)x67 & 0x7ffffffffffff);
-  { uint128_t x70 = (x68 + x42);
-  { uint128_t x71 = (x70 >> 0x33);
-  { uint64_t x72 = ((uint64_t)x70 & 0x7ffffffffffff);
-  { uint128_t x73 = (x71 + x41);
-  { uint64_t x74 = (uint64_t) (x73 >> 0x33);
-  { uint64_t x75 = ((uint64_t)x73 & 0x7ffffffffffff);
-  { uint128_t x76 = (x74 + x40);
-  { uint64_t x77 = (uint64_t) (x76 >> 0x33);
-  { uint64_t x78 = ((uint64_t)x76 & 0x7ffffffffffff);
-  { uint128_t x79 = (x51 + ((uint128_t)0x239 * x77));
-  { uint64_t x80 = (uint64_t) (x79 >> 0x34);
-  { uint64_t x81 = ((uint64_t)x79 & 0xfffffffffffff);
-  { uint64_t x82 = (x80 + x54);
-  { uint64_t x83 = (x82 >> 0x33);
-  { uint64_t x84 = (x82 & 0x7ffffffffffff);
-  out[0] = x81;
-  out[1] = x84;
-  out[2] = (x83 + x57);
-  out[3] = x60;
-  out[4] = x63;
-  out[5] = x66;
-  out[6] = x69;
-  out[7] = x72;
-  out[8] = x75;
-  out[9] = x78;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e512m569_10limbs/femul.v b/src/Specific/solinas64_2e512m569_10limbs/femul.v
deleted file mode 100644
index ac9f5ccfa..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/femul.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.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/solinas64_2e512m569_10limbs/femulDisplay.log b/src/Specific/solinas64_2e512m569_10limbs/femulDisplay.log
deleted file mode 100644
index 0fdd49f6f..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/femulDisplay.log
+++ /dev/null
@@ -1,52 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- uint128_t x40 = (((uint128_t)x5 * x38) + ((0x2 * ((uint128_t)x7 * x39)) + ((0x2 * ((uint128_t)x9 * x37)) + ((0x2 * ((uint128_t)x11 * x35)) + (((uint128_t)x13 * x33) + (((uint128_t)x15 * x31) + ((0x2 * ((uint128_t)x17 * x29)) + ((0x2 * ((uint128_t)x19 * x27)) + ((0x2 * ((uint128_t)x21 * x25)) + ((uint128_t)x20 * x23))))))))));
- uint128_t x41 = ((((uint128_t)x5 * x39) + ((0x2 * ((uint128_t)x7 * x37)) + ((0x2 * ((uint128_t)x9 * x35)) + (((uint128_t)x11 * x33) + (((uint128_t)x13 * x31) + (((uint128_t)x15 * x29) + ((0x2 * ((uint128_t)x17 * x27)) + ((0x2 * ((uint128_t)x19 * x25)) + ((uint128_t)x21 * x23))))))))) + (0x239 * ((uint128_t)x20 * x38)));
- uint128_t x42 = ((((uint128_t)x5 * x37) + ((0x2 * ((uint128_t)x7 * x35)) + (((uint128_t)x9 * x33) + (((uint128_t)x11 * x31) + (((uint128_t)x13 * x29) + (((uint128_t)x15 * x27) + ((0x2 * ((uint128_t)x17 * x25)) + ((uint128_t)x19 * x23)))))))) + (0x239 * (((uint128_t)x21 * x38) + ((uint128_t)x20 * x39))));
- uint128_t x43 = ((((uint128_t)x5 * x35) + (((uint128_t)x7 * x33) + (((uint128_t)x9 * x31) + (((uint128_t)x11 * x29) + (((uint128_t)x13 * x27) + (((uint128_t)x15 * x25) + ((uint128_t)x17 * x23))))))) + (0x239 * (((uint128_t)x19 * x38) + (((uint128_t)x21 * x39) + ((uint128_t)x20 * x37)))));
- uint128_t x44 = ((((uint128_t)x5 * x33) + ((0x2 * ((uint128_t)x7 * x31)) + ((0x2 * ((uint128_t)x9 * x29)) + ((0x2 * ((uint128_t)x11 * x27)) + ((0x2 * ((uint128_t)x13 * x25)) + ((uint128_t)x15 * x23)))))) + (0x239 * ((0x2 * ((uint128_t)x17 * x38)) + ((0x2 * ((uint128_t)x19 * x39)) + ((0x2 * ((uint128_t)x21 * x37)) + (0x2 * ((uint128_t)x20 * x35)))))));
- uint128_t x45 = ((((uint128_t)x5 * x31) + ((0x2 * ((uint128_t)x7 * x29)) + ((0x2 * ((uint128_t)x9 * x27)) + ((0x2 * ((uint128_t)x11 * x25)) + ((uint128_t)x13 * x23))))) + (0x239 * (((uint128_t)x15 * x38) + ((0x2 * ((uint128_t)x17 * x39)) + ((0x2 * ((uint128_t)x19 * x37)) + ((0x2 * ((uint128_t)x21 * x35)) + ((uint128_t)x20 * x33)))))));
- uint128_t x46 = ((((uint128_t)x5 * x29) + ((0x2 * ((uint128_t)x7 * x27)) + ((0x2 * ((uint128_t)x9 * x25)) + ((uint128_t)x11 * x23)))) + (0x239 * (((uint128_t)x13 * x38) + (((uint128_t)x15 * x39) + ((0x2 * ((uint128_t)x17 * x37)) + ((0x2 * ((uint128_t)x19 * x35)) + (((uint128_t)x21 * x33) + ((uint128_t)x20 * x31))))))));
- uint128_t x47 = ((((uint128_t)x5 * x27) + ((0x2 * ((uint128_t)x7 * x25)) + ((uint128_t)x9 * x23))) + (0x239 * (((uint128_t)x11 * x38) + (((uint128_t)x13 * x39) + (((uint128_t)x15 * x37) + ((0x2 * ((uint128_t)x17 * x35)) + (((uint128_t)x19 * x33) + (((uint128_t)x21 * x31) + ((uint128_t)x20 * x29)))))))));
- uint128_t x48 = ((((uint128_t)x5 * x25) + ((uint128_t)x7 * x23)) + (0x239 * (((uint128_t)x9 * x38) + (((uint128_t)x11 * x39) + (((uint128_t)x13 * x37) + (((uint128_t)x15 * x35) + (((uint128_t)x17 * x33) + (((uint128_t)x19 * x31) + (((uint128_t)x21 * x29) + ((uint128_t)x20 * x27))))))))));
- uint128_t x49 = (((uint128_t)x5 * x23) + (0x239 * ((0x2 * ((uint128_t)x7 * x38)) + ((0x2 * ((uint128_t)x9 * x39)) + ((0x2 * ((uint128_t)x11 * x37)) + ((0x2 * ((uint128_t)x13 * x35)) + (((uint128_t)x15 * x33) + ((0x2 * ((uint128_t)x17 * x31)) + ((0x2 * ((uint128_t)x19 * x29)) + ((0x2 * ((uint128_t)x21 * x27)) + (0x2 * ((uint128_t)x20 * x25))))))))))));
- uint128_t x50 = (x49 >> 0x34);
- uint64_t x51 = ((uint64_t)x49 & 0xfffffffffffff);
- uint128_t x52 = (x50 + x48);
- uint128_t x53 = (x52 >> 0x33);
- uint64_t x54 = ((uint64_t)x52 & 0x7ffffffffffff);
- uint128_t x55 = (x53 + x47);
- uint128_t x56 = (x55 >> 0x33);
- uint64_t x57 = ((uint64_t)x55 & 0x7ffffffffffff);
- uint128_t x58 = (x56 + x46);
- uint128_t x59 = (x58 >> 0x33);
- uint64_t x60 = ((uint64_t)x58 & 0x7ffffffffffff);
- uint128_t x61 = (x59 + x45);
- uint128_t x62 = (x61 >> 0x33);
- uint64_t x63 = ((uint64_t)x61 & 0x7ffffffffffff);
- uint128_t x64 = (x62 + x44);
- uint128_t x65 = (x64 >> 0x34);
- uint64_t x66 = ((uint64_t)x64 & 0xfffffffffffff);
- uint128_t x67 = (x65 + x43);
- uint128_t x68 = (x67 >> 0x33);
- uint64_t x69 = ((uint64_t)x67 & 0x7ffffffffffff);
- uint128_t x70 = (x68 + x42);
- uint128_t x71 = (x70 >> 0x33);
- uint64_t x72 = ((uint64_t)x70 & 0x7ffffffffffff);
- uint128_t x73 = (x71 + x41);
- uint64_t x74 = (uint64_t) (x73 >> 0x33);
- uint64_t x75 = ((uint64_t)x73 & 0x7ffffffffffff);
- uint128_t x76 = (x74 + x40);
- uint64_t x77 = (uint64_t) (x76 >> 0x33);
- uint64_t x78 = ((uint64_t)x76 & 0x7ffffffffffff);
- uint128_t x79 = (x51 + ((uint128_t)0x239 * x77));
- uint64_t x80 = (uint64_t) (x79 >> 0x34);
- uint64_t x81 = ((uint64_t)x79 & 0xfffffffffffff);
- uint64_t x82 = (x80 + x54);
- uint64_t x83 = (x82 >> 0x33);
- uint64_t x84 = (x82 & 0x7ffffffffffff);
- return (Return x78, Return x75, Return x72, Return x69, Return x66, Return x63, Return x60, (x83 + x57), Return x84, Return x81))
-(x, x0)%core
-     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e512m569_10limbs/femulDisplay.v b/src/Specific/solinas64_2e512m569_10limbs/femulDisplay.v
deleted file mode 100644
index 7531c9c34..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/femulDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.femul.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display mul.
diff --git a/src/Specific/solinas64_2e512m569_10limbs/fesquare.c b/src/Specific/solinas64_2e512m569_10limbs/fesquare.c
deleted file mode 100644
index c8ecbdfda..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesquare.c
+++ /dev/null
@@ -1,68 +0,0 @@
-static void fesquare(uint64_t out[10], const uint64_t in1[10]) {
-  { const uint64_t x17 = in1[9];
-  { const uint64_t x18 = in1[8];
-  { const uint64_t x16 = in1[7];
-  { const uint64_t x14 = in1[6];
-  { const uint64_t x12 = in1[5];
-  { const uint64_t x10 = in1[4];
-  { const uint64_t x8 = in1[3];
-  { const uint64_t x6 = in1[2];
-  { const uint64_t x4 = in1[1];
-  { const uint64_t x2 = in1[0];
-  { uint128_t x19 = (((uint128_t)x2 * x17) + ((0x2 * ((uint128_t)x4 * x18)) + ((0x2 * ((uint128_t)x6 * x16)) + ((0x2 * ((uint128_t)x8 * x14)) + (((uint128_t)x10 * x12) + (((uint128_t)x12 * x10) + ((0x2 * ((uint128_t)x14 * x8)) + ((0x2 * ((uint128_t)x16 * x6)) + ((0x2 * ((uint128_t)x18 * x4)) + ((uint128_t)x17 * x2))))))))));
-  { uint128_t x20 = ((((uint128_t)x2 * x18) + ((0x2 * ((uint128_t)x4 * x16)) + ((0x2 * ((uint128_t)x6 * x14)) + (((uint128_t)x8 * x12) + (((uint128_t)x10 * x10) + (((uint128_t)x12 * x8) + ((0x2 * ((uint128_t)x14 * x6)) + ((0x2 * ((uint128_t)x16 * x4)) + ((uint128_t)x18 * x2))))))))) + (0x239 * ((uint128_t)x17 * x17)));
-  { uint128_t x21 = ((((uint128_t)x2 * x16) + ((0x2 * ((uint128_t)x4 * x14)) + (((uint128_t)x6 * x12) + (((uint128_t)x8 * x10) + (((uint128_t)x10 * x8) + (((uint128_t)x12 * x6) + ((0x2 * ((uint128_t)x14 * x4)) + ((uint128_t)x16 * x2)))))))) + (0x239 * (((uint128_t)x18 * x17) + ((uint128_t)x17 * x18))));
-  { uint128_t x22 = ((((uint128_t)x2 * x14) + (((uint128_t)x4 * x12) + (((uint128_t)x6 * x10) + (((uint128_t)x8 * x8) + (((uint128_t)x10 * x6) + (((uint128_t)x12 * x4) + ((uint128_t)x14 * x2))))))) + (0x239 * (((uint128_t)x16 * x17) + (((uint128_t)x18 * x18) + ((uint128_t)x17 * x16)))));
-  { uint128_t x23 = ((((uint128_t)x2 * x12) + ((0x2 * ((uint128_t)x4 * x10)) + ((0x2 * ((uint128_t)x6 * x8)) + ((0x2 * ((uint128_t)x8 * x6)) + ((0x2 * ((uint128_t)x10 * x4)) + ((uint128_t)x12 * x2)))))) + (0x239 * ((0x2 * ((uint128_t)x14 * x17)) + ((0x2 * ((uint128_t)x16 * x18)) + ((0x2 * ((uint128_t)x18 * x16)) + (0x2 * ((uint128_t)x17 * x14)))))));
-  { uint128_t x24 = ((((uint128_t)x2 * x10) + ((0x2 * ((uint128_t)x4 * x8)) + ((0x2 * ((uint128_t)x6 * x6)) + ((0x2 * ((uint128_t)x8 * x4)) + ((uint128_t)x10 * x2))))) + (0x239 * (((uint128_t)x12 * x17) + ((0x2 * ((uint128_t)x14 * x18)) + ((0x2 * ((uint128_t)x16 * x16)) + ((0x2 * ((uint128_t)x18 * x14)) + ((uint128_t)x17 * x12)))))));
-  { uint128_t x25 = ((((uint128_t)x2 * x8) + ((0x2 * ((uint128_t)x4 * x6)) + ((0x2 * ((uint128_t)x6 * x4)) + ((uint128_t)x8 * x2)))) + (0x239 * (((uint128_t)x10 * x17) + (((uint128_t)x12 * x18) + ((0x2 * ((uint128_t)x14 * x16)) + ((0x2 * ((uint128_t)x16 * x14)) + (((uint128_t)x18 * x12) + ((uint128_t)x17 * x10))))))));
-  { uint128_t x26 = ((((uint128_t)x2 * x6) + ((0x2 * ((uint128_t)x4 * x4)) + ((uint128_t)x6 * x2))) + (0x239 * (((uint128_t)x8 * x17) + (((uint128_t)x10 * x18) + (((uint128_t)x12 * x16) + ((0x2 * ((uint128_t)x14 * x14)) + (((uint128_t)x16 * x12) + (((uint128_t)x18 * x10) + ((uint128_t)x17 * x8)))))))));
-  { uint128_t x27 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x239 * (((uint128_t)x6 * x17) + (((uint128_t)x8 * x18) + (((uint128_t)x10 * x16) + (((uint128_t)x12 * x14) + (((uint128_t)x14 * x12) + (((uint128_t)x16 * x10) + (((uint128_t)x18 * x8) + ((uint128_t)x17 * x6))))))))));
-  { uint128_t x28 = (((uint128_t)x2 * x2) + (0x239 * ((0x2 * ((uint128_t)x4 * x17)) + ((0x2 * ((uint128_t)x6 * x18)) + ((0x2 * ((uint128_t)x8 * x16)) + ((0x2 * ((uint128_t)x10 * x14)) + (((uint128_t)x12 * x12) + ((0x2 * ((uint128_t)x14 * x10)) + ((0x2 * ((uint128_t)x16 * x8)) + ((0x2 * ((uint128_t)x18 * x6)) + (0x2 * ((uint128_t)x17 * x4))))))))))));
-  { uint128_t x29 = (x28 >> 0x34);
-  { uint64_t x30 = ((uint64_t)x28 & 0xfffffffffffff);
-  { uint128_t x31 = (x29 + x27);
-  { uint128_t x32 = (x31 >> 0x33);
-  { uint64_t x33 = ((uint64_t)x31 & 0x7ffffffffffff);
-  { uint128_t x34 = (x32 + x26);
-  { uint128_t x35 = (x34 >> 0x33);
-  { uint64_t x36 = ((uint64_t)x34 & 0x7ffffffffffff);
-  { uint128_t x37 = (x35 + x25);
-  { uint128_t x38 = (x37 >> 0x33);
-  { uint64_t x39 = ((uint64_t)x37 & 0x7ffffffffffff);
-  { uint128_t x40 = (x38 + x24);
-  { uint128_t x41 = (x40 >> 0x33);
-  { uint64_t x42 = ((uint64_t)x40 & 0x7ffffffffffff);
-  { uint128_t x43 = (x41 + x23);
-  { uint128_t x44 = (x43 >> 0x34);
-  { uint64_t x45 = ((uint64_t)x43 & 0xfffffffffffff);
-  { uint128_t x46 = (x44 + x22);
-  { uint128_t x47 = (x46 >> 0x33);
-  { uint64_t x48 = ((uint64_t)x46 & 0x7ffffffffffff);
-  { uint128_t x49 = (x47 + x21);
-  { uint128_t x50 = (x49 >> 0x33);
-  { uint64_t x51 = ((uint64_t)x49 & 0x7ffffffffffff);
-  { uint128_t x52 = (x50 + x20);
-  { uint64_t x53 = (uint64_t) (x52 >> 0x33);
-  { uint64_t x54 = ((uint64_t)x52 & 0x7ffffffffffff);
-  { uint128_t x55 = (x53 + x19);
-  { uint64_t x56 = (uint64_t) (x55 >> 0x33);
-  { uint64_t x57 = ((uint64_t)x55 & 0x7ffffffffffff);
-  { uint128_t x58 = (x30 + ((uint128_t)0x239 * x56));
-  { uint64_t x59 = (uint64_t) (x58 >> 0x34);
-  { uint64_t x60 = ((uint64_t)x58 & 0xfffffffffffff);
-  { uint64_t x61 = (x59 + x33);
-  { uint64_t x62 = (x61 >> 0x33);
-  { uint64_t x63 = (x61 & 0x7ffffffffffff);
-  out[0] = x60;
-  out[1] = x63;
-  out[2] = (x62 + x36);
-  out[3] = x39;
-  out[4] = x42;
-  out[5] = x45;
-  out[6] = x48;
-  out[7] = x51;
-  out[8] = x54;
-  out[9] = x57;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e512m569_10limbs/fesquare.v b/src/Specific/solinas64_2e512m569_10limbs/fesquare.v
deleted file mode 100644
index d673db48d..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesquare.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.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/solinas64_2e512m569_10limbs/fesquareDisplay.log b/src/Specific/solinas64_2e512m569_10limbs/fesquareDisplay.log
deleted file mode 100644
index 09790b996..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesquareDisplay.log
+++ /dev/null
@@ -1,52 +0,0 @@
-λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x17, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
- uint128_t x19 = (((uint128_t)x2 * x17) + ((0x2 * ((uint128_t)x4 * x18)) + ((0x2 * ((uint128_t)x6 * x16)) + ((0x2 * ((uint128_t)x8 * x14)) + (((uint128_t)x10 * x12) + (((uint128_t)x12 * x10) + ((0x2 * ((uint128_t)x14 * x8)) + ((0x2 * ((uint128_t)x16 * x6)) + ((0x2 * ((uint128_t)x18 * x4)) + ((uint128_t)x17 * x2))))))))));
- uint128_t x20 = ((((uint128_t)x2 * x18) + ((0x2 * ((uint128_t)x4 * x16)) + ((0x2 * ((uint128_t)x6 * x14)) + (((uint128_t)x8 * x12) + (((uint128_t)x10 * x10) + (((uint128_t)x12 * x8) + ((0x2 * ((uint128_t)x14 * x6)) + ((0x2 * ((uint128_t)x16 * x4)) + ((uint128_t)x18 * x2))))))))) + (0x239 * ((uint128_t)x17 * x17)));
- uint128_t x21 = ((((uint128_t)x2 * x16) + ((0x2 * ((uint128_t)x4 * x14)) + (((uint128_t)x6 * x12) + (((uint128_t)x8 * x10) + (((uint128_t)x10 * x8) + (((uint128_t)x12 * x6) + ((0x2 * ((uint128_t)x14 * x4)) + ((uint128_t)x16 * x2)))))))) + (0x239 * (((uint128_t)x18 * x17) + ((uint128_t)x17 * x18))));
- uint128_t x22 = ((((uint128_t)x2 * x14) + (((uint128_t)x4 * x12) + (((uint128_t)x6 * x10) + (((uint128_t)x8 * x8) + (((uint128_t)x10 * x6) + (((uint128_t)x12 * x4) + ((uint128_t)x14 * x2))))))) + (0x239 * (((uint128_t)x16 * x17) + (((uint128_t)x18 * x18) + ((uint128_t)x17 * x16)))));
- uint128_t x23 = ((((uint128_t)x2 * x12) + ((0x2 * ((uint128_t)x4 * x10)) + ((0x2 * ((uint128_t)x6 * x8)) + ((0x2 * ((uint128_t)x8 * x6)) + ((0x2 * ((uint128_t)x10 * x4)) + ((uint128_t)x12 * x2)))))) + (0x239 * ((0x2 * ((uint128_t)x14 * x17)) + ((0x2 * ((uint128_t)x16 * x18)) + ((0x2 * ((uint128_t)x18 * x16)) + (0x2 * ((uint128_t)x17 * x14)))))));
- uint128_t x24 = ((((uint128_t)x2 * x10) + ((0x2 * ((uint128_t)x4 * x8)) + ((0x2 * ((uint128_t)x6 * x6)) + ((0x2 * ((uint128_t)x8 * x4)) + ((uint128_t)x10 * x2))))) + (0x239 * (((uint128_t)x12 * x17) + ((0x2 * ((uint128_t)x14 * x18)) + ((0x2 * ((uint128_t)x16 * x16)) + ((0x2 * ((uint128_t)x18 * x14)) + ((uint128_t)x17 * x12)))))));
- uint128_t x25 = ((((uint128_t)x2 * x8) + ((0x2 * ((uint128_t)x4 * x6)) + ((0x2 * ((uint128_t)x6 * x4)) + ((uint128_t)x8 * x2)))) + (0x239 * (((uint128_t)x10 * x17) + (((uint128_t)x12 * x18) + ((0x2 * ((uint128_t)x14 * x16)) + ((0x2 * ((uint128_t)x16 * x14)) + (((uint128_t)x18 * x12) + ((uint128_t)x17 * x10))))))));
- uint128_t x26 = ((((uint128_t)x2 * x6) + ((0x2 * ((uint128_t)x4 * x4)) + ((uint128_t)x6 * x2))) + (0x239 * (((uint128_t)x8 * x17) + (((uint128_t)x10 * x18) + (((uint128_t)x12 * x16) + ((0x2 * ((uint128_t)x14 * x14)) + (((uint128_t)x16 * x12) + (((uint128_t)x18 * x10) + ((uint128_t)x17 * x8)))))))));
- uint128_t x27 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x239 * (((uint128_t)x6 * x17) + (((uint128_t)x8 * x18) + (((uint128_t)x10 * x16) + (((uint128_t)x12 * x14) + (((uint128_t)x14 * x12) + (((uint128_t)x16 * x10) + (((uint128_t)x18 * x8) + ((uint128_t)x17 * x6))))))))));
- uint128_t x28 = (((uint128_t)x2 * x2) + (0x239 * ((0x2 * ((uint128_t)x4 * x17)) + ((0x2 * ((uint128_t)x6 * x18)) + ((0x2 * ((uint128_t)x8 * x16)) + ((0x2 * ((uint128_t)x10 * x14)) + (((uint128_t)x12 * x12) + ((0x2 * ((uint128_t)x14 * x10)) + ((0x2 * ((uint128_t)x16 * x8)) + ((0x2 * ((uint128_t)x18 * x6)) + (0x2 * ((uint128_t)x17 * x4))))))))))));
- uint128_t x29 = (x28 >> 0x34);
- uint64_t x30 = ((uint64_t)x28 & 0xfffffffffffff);
- uint128_t x31 = (x29 + x27);
- uint128_t x32 = (x31 >> 0x33);
- uint64_t x33 = ((uint64_t)x31 & 0x7ffffffffffff);
- uint128_t x34 = (x32 + x26);
- uint128_t x35 = (x34 >> 0x33);
- uint64_t x36 = ((uint64_t)x34 & 0x7ffffffffffff);
- uint128_t x37 = (x35 + x25);
- uint128_t x38 = (x37 >> 0x33);
- uint64_t x39 = ((uint64_t)x37 & 0x7ffffffffffff);
- uint128_t x40 = (x38 + x24);
- uint128_t x41 = (x40 >> 0x33);
- uint64_t x42 = ((uint64_t)x40 & 0x7ffffffffffff);
- uint128_t x43 = (x41 + x23);
- uint128_t x44 = (x43 >> 0x34);
- uint64_t x45 = ((uint64_t)x43 & 0xfffffffffffff);
- uint128_t x46 = (x44 + x22);
- uint128_t x47 = (x46 >> 0x33);
- uint64_t x48 = ((uint64_t)x46 & 0x7ffffffffffff);
- uint128_t x49 = (x47 + x21);
- uint128_t x50 = (x49 >> 0x33);
- uint64_t x51 = ((uint64_t)x49 & 0x7ffffffffffff);
- uint128_t x52 = (x50 + x20);
- uint64_t x53 = (uint64_t) (x52 >> 0x33);
- uint64_t x54 = ((uint64_t)x52 & 0x7ffffffffffff);
- uint128_t x55 = (x53 + x19);
- uint64_t x56 = (uint64_t) (x55 >> 0x33);
- uint64_t x57 = ((uint64_t)x55 & 0x7ffffffffffff);
- uint128_t x58 = (x30 + ((uint128_t)0x239 * x56));
- uint64_t x59 = (uint64_t) (x58 >> 0x34);
- uint64_t x60 = ((uint64_t)x58 & 0xfffffffffffff);
- uint64_t x61 = (x59 + x33);
- uint64_t x62 = (x61 >> 0x33);
- uint64_t x63 = (x61 & 0x7ffffffffffff);
- return (Return x57, Return x54, Return x51, Return x48, Return x45, Return x42, Return x39, (x62 + x36), Return x63, Return x60))
-x
-     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e512m569_10limbs/fesquareDisplay.v b/src/Specific/solinas64_2e512m569_10limbs/fesquareDisplay.v
deleted file mode 100644
index 3629053ea..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesquareDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.fesquare.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display square.
diff --git a/src/Specific/solinas64_2e512m569_10limbs/fesub.c b/src/Specific/solinas64_2e512m569_10limbs/fesub.c
deleted file mode 100644
index b2dd293f5..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesub.c
+++ /dev/null
@@ -1,33 +0,0 @@
-static void fesub(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[10]) {
-  { const uint64_t x20 = in1[9];
-  { const uint64_t x21 = in1[8];
-  { const uint64_t x19 = in1[7];
-  { const uint64_t x17 = in1[6];
-  { const uint64_t x15 = in1[5];
-  { const uint64_t x13 = in1[4];
-  { const uint64_t x11 = in1[3];
-  { const uint64_t x9 = in1[2];
-  { const uint64_t x7 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x38 = in2[9];
-  { const uint64_t x39 = in2[8];
-  { const uint64_t x37 = in2[7];
-  { const uint64_t x35 = in2[6];
-  { const uint64_t x33 = in2[5];
-  { const uint64_t x31 = in2[4];
-  { const uint64_t x29 = in2[3];
-  { const uint64_t x27 = in2[2];
-  { const uint64_t x25 = in2[1];
-  { const uint64_t x23 = in2[0];
-  out[0] = ((0x1ffffffffffb8e + x5) - x23);
-  out[1] = ((0xffffffffffffe + x7) - x25);
-  out[2] = ((0xffffffffffffe + x9) - x27);
-  out[3] = ((0xffffffffffffe + x11) - x29);
-  out[4] = ((0xffffffffffffe + x13) - x31);
-  out[5] = ((0x1ffffffffffffe + x15) - x33);
-  out[6] = ((0xffffffffffffe + x17) - x35);
-  out[7] = ((0xffffffffffffe + x19) - x37);
-  out[8] = ((0xffffffffffffe + x21) - x39);
-  out[9] = ((0xffffffffffffe + x20) - x38);
-  }}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e512m569_10limbs/fesub.v b/src/Specific/solinas64_2e512m569_10limbs/fesub.v
deleted file mode 100644
index 792210dc5..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesub.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.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/solinas64_2e512m569_10limbs/fesubDisplay.log b/src/Specific/solinas64_2e512m569_10limbs/fesubDisplay.log
deleted file mode 100644
index 07b0161a8..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesubDisplay.log
+++ /dev/null
@@ -1,7 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0xffffffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0x1ffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0x1ffffffffffb8e + x5) - x23)))
-(x, x0)%core
-     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e512m569_10limbs/fesubDisplay.v b/src/Specific/solinas64_2e512m569_10limbs/fesubDisplay.v
deleted file mode 100644
index a977888de..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/fesubDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.fesub.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display sub.
diff --git a/src/Specific/solinas64_2e512m569_10limbs/freeze.c b/src/Specific/solinas64_2e512m569_10limbs/freeze.c
deleted file mode 100644
index 6f4db7541..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/freeze.c
+++ /dev/null
@@ -1,54 +0,0 @@
-static void freeze(uint64_t out[10], const uint64_t in1[10]) {
-  { const uint64_t x17 = in1[9];
-  { const uint64_t x18 = in1[8];
-  { const uint64_t x16 = in1[7];
-  { const uint64_t x14 = in1[6];
-  { const uint64_t x12 = in1[5];
-  { const uint64_t x10 = in1[4];
-  { const uint64_t x8 = in1[3];
-  { const uint64_t x6 = in1[2];
-  { const uint64_t x4 = in1[1];
-  { const uint64_t x2 = in1[0];
-  { uint64_t x20, uint8_t x21 = Op (Syntax.SubWithGetBorrow 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0xffffffffffdc7);
-  { uint64_t x23; uint8_t x24 = _subborrow_u51(x21, x4, 0x7ffffffffffff, &x23);
-  { uint64_t x26; uint8_t x27 = _subborrow_u51(x24, x6, 0x7ffffffffffff, &x26);
-  { uint64_t x29; uint8_t x30 = _subborrow_u51(x27, x8, 0x7ffffffffffff, &x29);
-  { uint64_t x32; uint8_t x33 = _subborrow_u51(x30, x10, 0x7ffffffffffff, &x32);
-  { uint64_t x35, uint8_t x36 = Op (Syntax.SubWithGetBorrow 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x33, Return x12, 0xfffffffffffff);
-  { uint64_t x38; uint8_t x39 = _subborrow_u51(x36, x14, 0x7ffffffffffff, &x38);
-  { uint64_t x41; uint8_t x42 = _subborrow_u51(x39, x16, 0x7ffffffffffff, &x41);
-  { uint64_t x44; uint8_t x45 = _subborrow_u51(x42, x18, 0x7ffffffffffff, &x44);
-  { uint64_t x47; uint8_t x48 = _subborrow_u51(x45, x17, 0x7ffffffffffff, &x47);
-  { uint64_t x49 = cmovznz64(x48, 0x0, 0xffffffffffffffffL);
-  { uint64_t x50 = (x49 & 0xffffffffffdc7);
-  { uint64_t x52, uint8_t x53 = Op (Syntax.AddWithGetCarry 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x20, Return x50);
-  { uint64_t x54 = (x49 & 0x7ffffffffffff);
-  { uint64_t x56; uint8_t x57 = _addcarryx_u51(x53, x23, x54, &x56);
-  { uint64_t x58 = (x49 & 0x7ffffffffffff);
-  { uint64_t x60; uint8_t x61 = _addcarryx_u51(x57, x26, x58, &x60);
-  { uint64_t x62 = (x49 & 0x7ffffffffffff);
-  { uint64_t x64; uint8_t x65 = _addcarryx_u51(x61, x29, x62, &x64);
-  { uint64_t x66 = (x49 & 0x7ffffffffffff);
-  { uint64_t x68; uint8_t x69 = _addcarryx_u51(x65, x32, x66, &x68);
-  { uint64_t x70 = (x49 & 0xfffffffffffff);
-  { uint64_t x72, uint8_t x73 = Op (Syntax.AddWithGetCarry 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x69, Return x35, Return x70);
-  { uint64_t x74 = (x49 & 0x7ffffffffffff);
-  { uint64_t x76; uint8_t x77 = _addcarryx_u51(x73, x38, x74, &x76);
-  { uint64_t x78 = (x49 & 0x7ffffffffffff);
-  { uint64_t x80; uint8_t x81 = _addcarryx_u51(x77, x41, x78, &x80);
-  { uint64_t x82 = (x49 & 0x7ffffffffffff);
-  { uint64_t x84; uint8_t x85 = _addcarryx_u51(x81, x44, x82, &x84);
-  { uint64_t x86 = (x49 & 0x7ffffffffffff);
-  { uint64_t x88; uint8_t _ = _addcarryx_u51(x85, x47, x86, &x88);
-  out[0] = x52;
-  out[1] = x56;
-  out[2] = x60;
-  out[3] = x64;
-  out[4] = x68;
-  out[5] = x72;
-  out[6] = x76;
-  out[7] = x80;
-  out[8] = x84;
-  out[9] = x88;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e512m569_10limbs/freeze.v b/src/Specific/solinas64_2e512m569_10limbs/freeze.v
deleted file mode 100644
index ef77d30c7..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/freeze.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.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/solinas64_2e512m569_10limbs/freezeDisplay.log b/src/Specific/solinas64_2e512m569_10limbs/freezeDisplay.log
deleted file mode 100644
index c78c962ee..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/freezeDisplay.log
+++ /dev/null
@@ -1,38 +0,0 @@
-λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x17, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
- uint64_t x20, uint8_t x21 = Op (Syntax.SubWithGetBorrow 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0xffffffffffdc7);
- uint64_t x23, uint8_t x24 = subborrow_u51(x21, x4, 0x7ffffffffffff);
- uint64_t x26, uint8_t x27 = subborrow_u51(x24, x6, 0x7ffffffffffff);
- uint64_t x29, uint8_t x30 = subborrow_u51(x27, x8, 0x7ffffffffffff);
- uint64_t x32, uint8_t x33 = subborrow_u51(x30, x10, 0x7ffffffffffff);
- uint64_t x35, uint8_t x36 = Op (Syntax.SubWithGetBorrow 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x33, Return x12, 0xfffffffffffff);
- uint64_t x38, uint8_t x39 = subborrow_u51(x36, x14, 0x7ffffffffffff);
- uint64_t x41, uint8_t x42 = subborrow_u51(x39, x16, 0x7ffffffffffff);
- uint64_t x44, uint8_t x45 = subborrow_u51(x42, x18, 0x7ffffffffffff);
- uint64_t x47, uint8_t x48 = subborrow_u51(x45, x17, 0x7ffffffffffff);
- uint64_t x49 = cmovznz64(x48, 0x0, 0xffffffffffffffffL);
- uint64_t x50 = (x49 & 0xffffffffffdc7);
- uint64_t x52, uint8_t x53 = Op (Syntax.AddWithGetCarry 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x20, Return x50);
- uint64_t x54 = (x49 & 0x7ffffffffffff);
- uint64_t x56, uint8_t x57 = addcarryx_u51(x53, x23, x54);
- uint64_t x58 = (x49 & 0x7ffffffffffff);
- uint64_t x60, uint8_t x61 = addcarryx_u51(x57, x26, x58);
- uint64_t x62 = (x49 & 0x7ffffffffffff);
- uint64_t x64, uint8_t x65 = addcarryx_u51(x61, x29, x62);
- uint64_t x66 = (x49 & 0x7ffffffffffff);
- uint64_t x68, uint8_t x69 = addcarryx_u51(x65, x32, x66);
- uint64_t x70 = (x49 & 0xfffffffffffff);
- uint64_t x72, uint8_t x73 = Op (Syntax.AddWithGetCarry 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x69, Return x35, Return x70);
- uint64_t x74 = (x49 & 0x7ffffffffffff);
- uint64_t x76, uint8_t x77 = addcarryx_u51(x73, x38, x74);
- uint64_t x78 = (x49 & 0x7ffffffffffff);
- uint64_t x80, uint8_t x81 = addcarryx_u51(x77, x41, x78);
- uint64_t x82 = (x49 & 0x7ffffffffffff);
- uint64_t x84, uint8_t x85 = addcarryx_u51(x81, x44, x82);
- uint64_t x86 = (x49 & 0x7ffffffffffff);
- uint64_t x88, uint8_t _ = addcarryx_u51(x85, x47, x86);
- (Return x88, Return x84, Return x80, Return x76, Return x72, Return x68, Return x64, Return x60, Return x56, Return x52))
-x
-     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e512m569_10limbs/freezeDisplay.v b/src/Specific/solinas64_2e512m569_10limbs/freezeDisplay.v
deleted file mode 100644
index 3a4855ab8..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/freezeDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e512m569_10limbs.freeze.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display freeze.
diff --git a/src/Specific/solinas64_2e512m569_10limbs/py_interpreter.sh b/src/Specific/solinas64_2e512m569_10limbs/py_interpreter.sh
deleted file mode 100755
index 711a90d28..000000000
--- a/src/Specific/solinas64_2e512m569_10limbs/py_interpreter.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-/usr/bin/env python3 "$@" -Dq='2**512 - 569' -Dmodulus_bytes='51.2' -Da24='121665'
-- 
cgit v1.2.3