27 files changed, 0 insertions, 380 deletions
diff --git a/src/Specific/solinas64_2e230m27_4limbs/CurveParameters.v b/src/Specific/solinas64_2e230m27_4limbs/CurveParameters.v
deleted file mode 100644
index c6ea3202b..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/CurveParameters.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^230 - 27
-Base: 57.5
-***)
-
-Definition curve : CurveParameters :=
-  {|
-    sz := 4%nat;
-    base := 57 + 1/2;
-    bitwidth := 64;
-    s := 2^230;
-    c := [(1, 27)];
-    carry_chains := Some [seq 0 (pred 4); [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_2e230m27_4limbs/Synthesis.v b/src/Specific/solinas64_2e230m27_4limbs/Synthesis.v
deleted file mode 100644
index f0a7c8050..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.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_2e230m27_4limbs/compiler.sh b/src/Specific/solinas64_2e230m27_4limbs/compiler.sh
deleted file mode 100755
index fc1cb69cd..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/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,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{58,57,58,57}' -Dmodulus_array='{0x3f,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,0xe5}' -Dmodulus_bytes_val='29' -Dmodulus_limbs='4' -Dq_mpz='(1_mpz<<230) - 27' "$@"
diff --git a/src/Specific/solinas64_2e230m27_4limbs/compilerxx.sh b/src/Specific/solinas64_2e230m27_4limbs/compilerxx.sh
deleted file mode 100755
index 3aa34c029..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/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,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{58,57,58,57}' -Dmodulus_array='{0x3f,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,0xe5}' -Dmodulus_bytes_val='29' -Dmodulus_limbs='4' -Dq_mpz='(1_mpz<<230) - 27' "$@"
diff --git a/src/Specific/solinas64_2e230m27_4limbs/feadd.c b/src/Specific/solinas64_2e230m27_4limbs/feadd.c
deleted file mode 100644
index d304c298a..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/feadd.c
+++ /dev/null
@@ -1,15 +0,0 @@
-static void feadd(uint64_t out[4], const uint64_t in1[4], const uint64_t in2[4]) {
-  { const uint64_t x8 = in1[3];
-  { const uint64_t x9 = in1[2];
-  { const uint64_t x7 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x14 = in2[3];
-  { const uint64_t x15 = in2[2];
-  { const uint64_t x13 = in2[1];
-  { const uint64_t x11 = in2[0];
-  out[0] = (x5 + x11);
-  out[1] = (x7 + x13);
-  out[2] = (x9 + x15);
-  out[3] = (x8 + x14);
-  }}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e230m27_4limbs/feadd.v b/src/Specific/solinas64_2e230m27_4limbs/feadd.v
deleted file mode 100644
index 61975391f..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/feadd.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.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_2e230m27_4limbs/feaddDisplay.log b/src/Specific/solinas64_2e230m27_4limbs/feaddDisplay.log
deleted file mode 100644
index d42ef91c3..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/feaddDisplay.log
+++ /dev/null
@@ -1,7 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core,
- ((x8 + x14), (x9 + x15), (x7 + x13), (x5 + x11)))
-(x, x0)%core
-     : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e230m27_4limbs/feaddDisplay.v b/src/Specific/solinas64_2e230m27_4limbs/feaddDisplay.v
deleted file mode 100644
index b927d4e1a..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/feaddDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.feadd.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display add.
diff --git a/src/Specific/solinas64_2e230m27_4limbs/fecarry.v b/src/Specific/solinas64_2e230m27_4limbs/fecarry.v
deleted file mode 100644
index 28f2ed91a..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fecarry.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.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_2e230m27_4limbs/fecarryDisplay.v b/src/Specific/solinas64_2e230m27_4limbs/fecarryDisplay.v
deleted file mode 100644
index 823e87cf3..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fecarryDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.fecarry.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display carry.
diff --git a/src/Specific/solinas64_2e230m27_4limbs/femul.c b/src/Specific/solinas64_2e230m27_4limbs/femul.c
deleted file mode 100644
index ffb6b77cd..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/femul.c
+++ /dev/null
@@ -1,36 +0,0 @@
-static void femul(uint64_t out[4], const uint64_t in1[4], const uint64_t in2[4]) {
-  { const uint64_t x8 = in1[3];
-  { const uint64_t x9 = in1[2];
-  { const uint64_t x7 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x14 = in2[3];
-  { const uint64_t x15 = in2[2];
-  { const uint64_t x13 = in2[1];
-  { const uint64_t x11 = in2[0];
-  { uint128_t x16 = (((uint128_t)x5 * x14) + (((uint128_t)x7 * x15) + (((uint128_t)x9 * x13) + ((uint128_t)x8 * x11))));
-  { uint128_t x17 = ((((uint128_t)x5 * x15) + ((0x2 * ((uint128_t)x7 * x13)) + ((uint128_t)x9 * x11))) + (0x1b * (0x2 * ((uint128_t)x8 * x14))));
-  { uint128_t x18 = ((((uint128_t)x5 * x13) + ((uint128_t)x7 * x11)) + (0x1b * (((uint128_t)x9 * x14) + ((uint128_t)x8 * x15))));
-  { uint128_t x19 = (((uint128_t)x5 * x11) + (0x1b * ((0x2 * ((uint128_t)x7 * x14)) + (((uint128_t)x9 * x15) + (0x2 * ((uint128_t)x8 * x13))))));
-  { uint128_t x20 = (x19 >> 0x3a);
-  { uint64_t x21 = ((uint64_t)x19 & 0x3ffffffffffffff);
-  { uint128_t x22 = (x20 + x18);
-  { uint128_t x23 = (x22 >> 0x39);
-  { uint64_t x24 = ((uint64_t)x22 & 0x1ffffffffffffff);
-  { uint128_t x25 = (x23 + x17);
-  { uint128_t x26 = (x25 >> 0x3a);
-  { uint64_t x27 = ((uint64_t)x25 & 0x3ffffffffffffff);
-  { uint128_t x28 = (x26 + x16);
-  { uint64_t x29 = (uint64_t) (x28 >> 0x39);
-  { uint64_t x30 = ((uint64_t)x28 & 0x1ffffffffffffff);
-  { uint128_t x31 = (x21 + ((uint128_t)0x1b * x29));
-  { uint64_t x32 = (uint64_t) (x31 >> 0x3a);
-  { uint64_t x33 = ((uint64_t)x31 & 0x3ffffffffffffff);
-  { uint64_t x34 = (x32 + x24);
-  { uint64_t x35 = (x34 >> 0x39);
-  { uint64_t x36 = (x34 & 0x1ffffffffffffff);
-  out[0] = x33;
-  out[1] = x36;
-  out[2] = (x35 + x27);
-  out[3] = x30;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e230m27_4limbs/femul.v b/src/Specific/solinas64_2e230m27_4limbs/femul.v
deleted file mode 100644
index be6fe19f7..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/femul.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.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_2e230m27_4limbs/femulDisplay.log b/src/Specific/solinas64_2e230m27_4limbs/femulDisplay.log
deleted file mode 100644
index c3853896e..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/femulDisplay.log
+++ /dev/null
@@ -1,28 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core,
- uint128_t x16 = (((uint128_t)x5 * x14) + (((uint128_t)x7 * x15) + (((uint128_t)x9 * x13) + ((uint128_t)x8 * x11))));
- uint128_t x17 = ((((uint128_t)x5 * x15) + ((0x2 * ((uint128_t)x7 * x13)) + ((uint128_t)x9 * x11))) + (0x1b * (0x2 * ((uint128_t)x8 * x14))));
- uint128_t x18 = ((((uint128_t)x5 * x13) + ((uint128_t)x7 * x11)) + (0x1b * (((uint128_t)x9 * x14) + ((uint128_t)x8 * x15))));
- uint128_t x19 = (((uint128_t)x5 * x11) + (0x1b * ((0x2 * ((uint128_t)x7 * x14)) + (((uint128_t)x9 * x15) + (0x2 * ((uint128_t)x8 * x13))))));
- uint128_t x20 = (x19 >> 0x3a);
- uint64_t x21 = ((uint64_t)x19 & 0x3ffffffffffffff);
- uint128_t x22 = (x20 + x18);
- uint128_t x23 = (x22 >> 0x39);
- uint64_t x24 = ((uint64_t)x22 & 0x1ffffffffffffff);
- uint128_t x25 = (x23 + x17);
- uint128_t x26 = (x25 >> 0x3a);
- uint64_t x27 = ((uint64_t)x25 & 0x3ffffffffffffff);
- uint128_t x28 = (x26 + x16);
- uint64_t x29 = (uint64_t) (x28 >> 0x39);
- uint64_t x30 = ((uint64_t)x28 & 0x1ffffffffffffff);
- uint128_t x31 = (x21 + ((uint128_t)0x1b * x29));
- uint64_t x32 = (uint64_t) (x31 >> 0x3a);
- uint64_t x33 = ((uint64_t)x31 & 0x3ffffffffffffff);
- uint64_t x34 = (x32 + x24);
- uint64_t x35 = (x34 >> 0x39);
- uint64_t x36 = (x34 & 0x1ffffffffffffff);
- return (Return x30, (x35 + x27), Return x36, Return x33))
-(x, x0)%core
-     : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e230m27_4limbs/femulDisplay.v b/src/Specific/solinas64_2e230m27_4limbs/femulDisplay.v
deleted file mode 100644
index 5325cbe45..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/femulDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.femul.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display mul.
diff --git a/src/Specific/solinas64_2e230m27_4limbs/fesquare.c b/src/Specific/solinas64_2e230m27_4limbs/fesquare.c
deleted file mode 100644
index daf47328b..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesquare.c
+++ /dev/null
@@ -1,32 +0,0 @@
-static void fesquare(uint64_t out[4], const uint64_t in1[4]) {
-  { const uint64_t x5 = in1[3];
-  { const uint64_t x6 = in1[2];
-  { const uint64_t x4 = in1[1];
-  { const uint64_t x2 = in1[0];
-  { uint128_t x7 = (((uint128_t)x2 * x5) + (((uint128_t)x4 * x6) + (((uint128_t)x6 * x4) + ((uint128_t)x5 * x2))));
-  { uint128_t x8 = ((((uint128_t)x2 * x6) + ((0x2 * ((uint128_t)x4 * x4)) + ((uint128_t)x6 * x2))) + (0x1b * (0x2 * ((uint128_t)x5 * x5))));
-  { uint128_t x9 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x1b * (((uint128_t)x6 * x5) + ((uint128_t)x5 * x6))));
-  { uint128_t x10 = (((uint128_t)x2 * x2) + (0x1b * ((0x2 * ((uint128_t)x4 * x5)) + (((uint128_t)x6 * x6) + (0x2 * ((uint128_t)x5 * x4))))));
-  { uint128_t x11 = (x10 >> 0x3a);
-  { uint64_t x12 = ((uint64_t)x10 & 0x3ffffffffffffff);
-  { uint128_t x13 = (x11 + x9);
-  { uint128_t x14 = (x13 >> 0x39);
-  { uint64_t x15 = ((uint64_t)x13 & 0x1ffffffffffffff);
-  { uint128_t x16 = (x14 + x8);
-  { uint128_t x17 = (x16 >> 0x3a);
-  { uint64_t x18 = ((uint64_t)x16 & 0x3ffffffffffffff);
-  { uint128_t x19 = (x17 + x7);
-  { uint64_t x20 = (uint64_t) (x19 >> 0x39);
-  { uint64_t x21 = ((uint64_t)x19 & 0x1ffffffffffffff);
-  { uint128_t x22 = (x12 + ((uint128_t)0x1b * x20));
-  { uint64_t x23 = (uint64_t) (x22 >> 0x3a);
-  { uint64_t x24 = ((uint64_t)x22 & 0x3ffffffffffffff);
-  { uint64_t x25 = (x23 + x15);
-  { uint64_t x26 = (x25 >> 0x39);
-  { uint64_t x27 = (x25 & 0x1ffffffffffffff);
-  out[0] = x24;
-  out[1] = x27;
-  out[2] = (x26 + x18);
-  out[3] = x21;
-  }}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e230m27_4limbs/fesquare.v b/src/Specific/solinas64_2e230m27_4limbs/fesquare.v
deleted file mode 100644
index 7fde088c1..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesquare.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.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_2e230m27_4limbs/fesquareDisplay.log b/src/Specific/solinas64_2e230m27_4limbs/fesquareDisplay.log
deleted file mode 100644
index 936d27885..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesquareDisplay.log
+++ /dev/null
@@ -1,28 +0,0 @@
-λ x : word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x5, x6, x4, x2)%core,
- uint128_t x7 = (((uint128_t)x2 * x5) + (((uint128_t)x4 * x6) + (((uint128_t)x6 * x4) + ((uint128_t)x5 * x2))));
- uint128_t x8 = ((((uint128_t)x2 * x6) + ((0x2 * ((uint128_t)x4 * x4)) + ((uint128_t)x6 * x2))) + (0x1b * (0x2 * ((uint128_t)x5 * x5))));
- uint128_t x9 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x1b * (((uint128_t)x6 * x5) + ((uint128_t)x5 * x6))));
- uint128_t x10 = (((uint128_t)x2 * x2) + (0x1b * ((0x2 * ((uint128_t)x4 * x5)) + (((uint128_t)x6 * x6) + (0x2 * ((uint128_t)x5 * x4))))));
- uint128_t x11 = (x10 >> 0x3a);
- uint64_t x12 = ((uint64_t)x10 & 0x3ffffffffffffff);
- uint128_t x13 = (x11 + x9);
- uint128_t x14 = (x13 >> 0x39);
- uint64_t x15 = ((uint64_t)x13 & 0x1ffffffffffffff);
- uint128_t x16 = (x14 + x8);
- uint128_t x17 = (x16 >> 0x3a);
- uint64_t x18 = ((uint64_t)x16 & 0x3ffffffffffffff);
- uint128_t x19 = (x17 + x7);
- uint64_t x20 = (uint64_t) (x19 >> 0x39);
- uint64_t x21 = ((uint64_t)x19 & 0x1ffffffffffffff);
- uint128_t x22 = (x12 + ((uint128_t)0x1b * x20));
- uint64_t x23 = (uint64_t) (x22 >> 0x3a);
- uint64_t x24 = ((uint64_t)x22 & 0x3ffffffffffffff);
- uint64_t x25 = (x23 + x15);
- uint64_t x26 = (x25 >> 0x39);
- uint64_t x27 = (x25 & 0x1ffffffffffffff);
- return (Return x21, (x26 + x18), Return x27, Return x24))
-x
-     : word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e230m27_4limbs/fesquareDisplay.v b/src/Specific/solinas64_2e230m27_4limbs/fesquareDisplay.v
deleted file mode 100644
index 79abb33d5..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesquareDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.fesquare.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display square.
diff --git a/src/Specific/solinas64_2e230m27_4limbs/fesub.c b/src/Specific/solinas64_2e230m27_4limbs/fesub.c
deleted file mode 100644
index babe8ab41..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesub.c
+++ /dev/null
@@ -1,15 +0,0 @@
-static void fesub(uint64_t out[4], const uint64_t in1[4], const uint64_t in2[4]) {
-  { const uint64_t x8 = in1[3];
-  { const uint64_t x9 = in1[2];
-  { const uint64_t x7 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x14 = in2[3];
-  { const uint64_t x15 = in2[2];
-  { const uint64_t x13 = in2[1];
-  { const uint64_t x11 = in2[0];
-  out[0] = ((0x7ffffffffffffca + x5) - x11);
-  out[1] = ((0x3fffffffffffffe + x7) - x13);
-  out[2] = ((0x7fffffffffffffe + x9) - x15);
-  out[3] = ((0x3fffffffffffffe + x8) - x14);
-  }}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e230m27_4limbs/fesub.v b/src/Specific/solinas64_2e230m27_4limbs/fesub.v
deleted file mode 100644
index 6d078a910..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesub.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.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_2e230m27_4limbs/fesubDisplay.log b/src/Specific/solinas64_2e230m27_4limbs/fesubDisplay.log
deleted file mode 100644
index db7ef6c5d..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesubDisplay.log
+++ /dev/null
@@ -1,7 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core,
- (((0x3fffffffffffffe + x8) - x14), ((0x7fffffffffffffe + x9) - x15), ((0x3fffffffffffffe + x7) - x13), ((0x7ffffffffffffca + x5) - x11)))
-(x, x0)%core
-     : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e230m27_4limbs/fesubDisplay.v b/src/Specific/solinas64_2e230m27_4limbs/fesubDisplay.v
deleted file mode 100644
index e1cc9a650..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/fesubDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.fesub.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display sub.
diff --git a/src/Specific/solinas64_2e230m27_4limbs/freeze.c b/src/Specific/solinas64_2e230m27_4limbs/freeze.c
deleted file mode 100644
index 038500201..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/freeze.c
+++ /dev/null
@@ -1,24 +0,0 @@
-static void freeze(uint64_t out[4], const uint64_t in1[4]) {
-  { const uint64_t x5 = in1[3];
-  { const uint64_t x6 = in1[2];
-  { const uint64_t x4 = in1[1];
-  { const uint64_t x2 = in1[0];
-  { uint64_t x8, uint8_t x9 = Op (Syntax.SubWithGetBorrow 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0x3ffffffffffffe5);
-  { uint64_t x11, uint8_t x12 = Op (Syntax.SubWithGetBorrow 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x9, Return x4, 0x1ffffffffffffff);
-  { uint64_t x14, uint8_t x15 = Op (Syntax.SubWithGetBorrow 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x12, Return x6, 0x3ffffffffffffff);
-  { uint64_t x17, uint8_t x18 = Op (Syntax.SubWithGetBorrow 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x15, Return x5, 0x1ffffffffffffff);
-  { uint64_t x19 = cmovznz64(x18, 0x0, 0xffffffffffffffffL);
-  { uint64_t x20 = (x19 & 0x3ffffffffffffe5);
-  { uint64_t x22, uint8_t x23 = Op (Syntax.AddWithGetCarry 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x8, Return x20);
-  { uint64_t x24 = (x19 & 0x1ffffffffffffff);
-  { uint64_t x26, uint8_t x27 = Op (Syntax.AddWithGetCarry 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x23, Return x11, Return x24);
-  { uint64_t x28 = (x19 & 0x3ffffffffffffff);
-  { uint64_t x30, uint8_t x31 = Op (Syntax.AddWithGetCarry 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x27, Return x14, Return x28);
-  { uint64_t x32 = (x19 & 0x1ffffffffffffff);
-  { uint64_t x34, uint8_t _ = Op (Syntax.AddWithGetCarry 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x31, Return x17, Return x32);
-  out[0] = x22;
-  out[1] = x26;
-  out[2] = x30;
-  out[3] = x34;
-  }}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e230m27_4limbs/freeze.v b/src/Specific/solinas64_2e230m27_4limbs/freeze.v
deleted file mode 100644
index e2779468e..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/freeze.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.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_2e230m27_4limbs/freezeDisplay.log b/src/Specific/solinas64_2e230m27_4limbs/freezeDisplay.log
deleted file mode 100644
index 11aac547b..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/freezeDisplay.log
+++ /dev/null
@@ -1,20 +0,0 @@
-λ x : word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x5, x6, x4, x2)%core,
- uint64_t x8, uint8_t x9 = Op (Syntax.SubWithGetBorrow 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0x3ffffffffffffe5);
- uint64_t x11, uint8_t x12 = Op (Syntax.SubWithGetBorrow 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x9, Return x4, 0x1ffffffffffffff);
- uint64_t x14, uint8_t x15 = Op (Syntax.SubWithGetBorrow 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x12, Return x6, 0x3ffffffffffffff);
- uint64_t x17, uint8_t x18 = Op (Syntax.SubWithGetBorrow 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x15, Return x5, 0x1ffffffffffffff);
- uint64_t x19 = cmovznz64(x18, 0x0, 0xffffffffffffffffL);
- uint64_t x20 = (x19 & 0x3ffffffffffffe5);
- uint64_t x22, uint8_t x23 = Op (Syntax.AddWithGetCarry 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x8, Return x20);
- uint64_t x24 = (x19 & 0x1ffffffffffffff);
- uint64_t x26, uint8_t x27 = Op (Syntax.AddWithGetCarry 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x23, Return x11, Return x24);
- uint64_t x28 = (x19 & 0x3ffffffffffffff);
- uint64_t x30, uint8_t x31 = Op (Syntax.AddWithGetCarry 58 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x27, Return x14, Return x28);
- uint64_t x32 = (x19 & 0x1ffffffffffffff);
- uint64_t x34, uint8_t _ = Op (Syntax.AddWithGetCarry 57 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x31, Return x17, Return x32);
- (Return x34, Return x30, Return x26, Return x22))
-x
-     : word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e230m27_4limbs/freezeDisplay.v b/src/Specific/solinas64_2e230m27_4limbs/freezeDisplay.v
deleted file mode 100644
index e39e3fb1a..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/freezeDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e230m27_4limbs.freeze.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display freeze.
diff --git a/src/Specific/solinas64_2e230m27_4limbs/py_interpreter.sh b/src/Specific/solinas64_2e230m27_4limbs/py_interpreter.sh
deleted file mode 100755
index 37bed5d95..000000000
--- a/src/Specific/solinas64_2e230m27_4limbs/py_interpreter.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-/usr/bin/env python3 "$@" -Dq='2**230 - 27' -Dmodulus_bytes='57.5' -Da24='121665'