new autogenerated files

21 files changed, 0 insertions, 574 deletions

diff --git a/src/Specific/solinas32_2e511m187/CurveParameters.v b/src/Specific/solinas32_2e511m187/CurveParameters.v
deleted file mode 100644
index 257c04523..000000000
--- a/src/Specific/solinas32_2e511m187/CurveParameters.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^511 - 187
-Base: 18.25
-***)
-
-Definition curve : CurveParameters :=
-  {|
-    sz := 28%nat;
-    base := 18 + 1/4;
-    bitwidth := 32;
-    s := 2^511;
-    c := [(1, 187)];
-    carry_chains := Some [seq 0 (pred 28); [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_2e511m187/Synthesis.v b/src/Specific/solinas32_2e511m187/Synthesis.v
deleted file mode 100644
index e2ccddf39..000000000
--- a/src/Specific/solinas32_2e511m187/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.solinas32_2e511m187.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_2e511m187/compiler.sh b/src/Specific/solinas32_2e511m187/compiler.sh
deleted file mode 100755
index be5a225ed..000000000
--- a/src/Specific/solinas32_2e511m187/compiler.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-clang -fbracket-depth=999999 -march=native -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='{19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18}' -Dmodulus_array='{0x7f,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,0x45}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='28' -Dq_mpz='(1_mpz<<511) - 187' "$@"
diff --git a/src/Specific/solinas32_2e511m187/compilerxx.sh b/src/Specific/solinas32_2e511m187/compilerxx.sh
deleted file mode 100755
index cdb584f20..000000000
--- a/src/Specific/solinas32_2e511m187/compilerxx.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-clang++ -fbracket-depth=999999 -march=native -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='{19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18,19,18,18,18}' -Dmodulus_array='{0x7f,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,0x45}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='28' -Dq_mpz='(1_mpz<<511) - 187' "$@"
diff --git a/src/Specific/solinas32_2e511m187/feadd.c b/src/Specific/solinas32_2e511m187/feadd.c
deleted file mode 100644
index ea5a0de71..000000000
--- a/src/Specific/solinas32_2e511m187/feadd.c
+++ /dev/null
@@ -1,87 +0,0 @@
-static void feadd(uint32_t out[28], const uint32_t in1[28], const uint32_t in2[28]) {
-  { const uint32_t x56 = in1[27];
-  { const uint32_t x57 = in1[26];
-  { const uint32_t x55 = in1[25];
-  { const uint32_t x53 = 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 x110 = in2[27];
-  { const uint32_t x111 = in2[26];
-  { const uint32_t x109 = in2[25];
-  { const uint32_t x107 = in2[24];
-  { const uint32_t x105 = in2[23];
-  { const uint32_t x103 = in2[22];
-  { const uint32_t x101 = in2[21];
-  { const uint32_t x99 = in2[20];
-  { const uint32_t x97 = in2[19];
-  { const uint32_t x95 = in2[18];
-  { const uint32_t x93 = in2[17];
-  { const uint32_t x91 = in2[16];
-  { const uint32_t x89 = in2[15];
-  { const uint32_t x87 = in2[14];
-  { const uint32_t x85 = in2[13];
-  { const uint32_t x83 = in2[12];
-  { const uint32_t x81 = in2[11];
-  { const uint32_t x79 = in2[10];
-  { const uint32_t x77 = in2[9];
-  { const uint32_t x75 = in2[8];
-  { const uint32_t x73 = in2[7];
-  { const uint32_t x71 = in2[6];
-  { const uint32_t x69 = in2[5];
-  { const uint32_t x67 = in2[4];
-  { const uint32_t x65 = in2[3];
-  { const uint32_t x63 = in2[2];
-  { const uint32_t x61 = in2[1];
-  { const uint32_t x59 = in2[0];
-  out[0] = (x5 + x59);
-  out[1] = (x7 + x61);
-  out[2] = (x9 + x63);
-  out[3] = (x11 + x65);
-  out[4] = (x13 + x67);
-  out[5] = (x15 + x69);
-  out[6] = (x17 + x71);
-  out[7] = (x19 + x73);
-  out[8] = (x21 + x75);
-  out[9] = (x23 + x77);
-  out[10] = (x25 + x79);
-  out[11] = (x27 + x81);
-  out[12] = (x29 + x83);
-  out[13] = (x31 + x85);
-  out[14] = (x33 + x87);
-  out[15] = (x35 + x89);
-  out[16] = (x37 + x91);
-  out[17] = (x39 + x93);
-  out[18] = (x41 + x95);
-  out[19] = (x43 + x97);
-  out[20] = (x45 + x99);
-  out[21] = (x47 + x101);
-  out[22] = (x49 + x103);
-  out[23] = (x51 + x105);
-  out[24] = (x53 + x107);
-  out[25] = (x55 + x109);
-  out[26] = (x57 + x111);
-  out[27] = (x56 + x110);
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas32_2e511m187/feadd.v b/src/Specific/solinas32_2e511m187/feadd.v
deleted file mode 100644
index 4fe376c50..000000000
--- a/src/Specific/solinas32_2e511m187/feadd.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas32_2e511m187.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_2e511m187/feaddDisplay.log b/src/Specific/solinas32_2e511m187/feaddDisplay.log
deleted file mode 100644
index 881e72050..000000000
--- a/src/Specific/solinas32_2e511m187/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 * word32 * word32 * word32,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x56, x57, x55, x53, x51, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x110, x111, x109, x107, x105, x103, x101, x99, x97, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59))%core,
- ((x56 + x110), (x57 + x111), (x55 + x109), (x53 + x107), (x51 + x105), (x49 + x103), (x47 + x101), (x45 + x99), (x43 + x97), (x41 + x95), (x39 + x93), (x37 + x91), (x35 + x89), (x33 + x87), (x31 + x85), (x29 + x83), (x27 + x81), (x25 + x79), (x23 + x77), (x21 + x75), (x19 + x73), (x17 + x71), (x15 + x69), (x13 + x67), (x11 + x65), (x9 + x63), (x7 + x61), (x5 + x59)))
-(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 * 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 * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e511m187/feaddDisplay.v b/src/Specific/solinas32_2e511m187/feaddDisplay.v
deleted file mode 100644
index 881420fcc..000000000
--- a/src/Specific/solinas32_2e511m187/feaddDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas32_2e511m187.feadd.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display add.
diff --git a/src/Specific/solinas32_2e511m187/femul.v b/src/Specific/solinas32_2e511m187/femul.v
deleted file mode 100644
index f369e47bc..000000000
--- a/src/Specific/solinas32_2e511m187/femul.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas32_2e511m187.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_2e511m187/femulDisplay.v b/src/Specific/solinas32_2e511m187/femulDisplay.v
deleted file mode 100644
index 37c22439a..000000000
--- a/src/Specific/solinas32_2e511m187/femulDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas32_2e511m187.femul.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display mul.
diff --git a/src/Specific/solinas32_2e511m187/fesquare.v b/src/Specific/solinas32_2e511m187/fesquare.v
deleted file mode 100644
index 6ca547cd9..000000000
--- a/src/Specific/solinas32_2e511m187/fesquare.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas32_2e511m187.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_2e511m187/fesquareDisplay.v b/src/Specific/solinas32_2e511m187/fesquareDisplay.v
deleted file mode 100644
index 6735a28b4..000000000
--- a/src/Specific/solinas32_2e511m187/fesquareDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas32_2e511m187.fesquare.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display square.
diff --git a/src/Specific/solinas32_2e511m187/fesub.c b/src/Specific/solinas32_2e511m187/fesub.c
deleted file mode 100644
index 3aed6811f..000000000
--- a/src/Specific/solinas32_2e511m187/fesub.c
+++ /dev/null
@@ -1,87 +0,0 @@
-static void fesub(uint32_t out[28], const uint32_t in1[28], const uint32_t in2[28]) {
-  { const uint32_t x56 = in1[27];
-  { const uint32_t x57 = in1[26];
-  { const uint32_t x55 = in1[25];
-  { const uint32_t x53 = 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 x110 = in2[27];
-  { const uint32_t x111 = in2[26];
-  { const uint32_t x109 = in2[25];
-  { const uint32_t x107 = in2[24];
-  { const uint32_t x105 = in2[23];
-  { const uint32_t x103 = in2[22];
-  { const uint32_t x101 = in2[21];
-  { const uint32_t x99 = in2[20];
-  { const uint32_t x97 = in2[19];
-  { const uint32_t x95 = in2[18];
-  { const uint32_t x93 = in2[17];
-  { const uint32_t x91 = in2[16];
-  { const uint32_t x89 = in2[15];
-  { const uint32_t x87 = in2[14];
-  { const uint32_t x85 = in2[13];
-  { const uint32_t x83 = in2[12];
-  { const uint32_t x81 = in2[11];
-  { const uint32_t x79 = in2[10];
-  { const uint32_t x77 = in2[9];
-  { const uint32_t x75 = in2[8];
-  { const uint32_t x73 = in2[7];
-  { const uint32_t x71 = in2[6];
-  { const uint32_t x69 = in2[5];
-  { const uint32_t x67 = in2[4];
-  { const uint32_t x65 = in2[3];
-  { const uint32_t x63 = in2[2];
-  { const uint32_t x61 = in2[1];
-  { const uint32_t x59 = in2[0];
-  out[0] = ((0xffe8a + x5) - x59);
-  out[1] = ((0x7fffe + x7) - x61);
-  out[2] = ((0x7fffe + x9) - x63);
-  out[3] = ((0x7fffe + x11) - x65);
-  out[4] = ((0xffffe + x13) - x67);
-  out[5] = ((0x7fffe + x15) - x69);
-  out[6] = ((0x7fffe + x17) - x71);
-  out[7] = ((0x7fffe + x19) - x73);
-  out[8] = ((0xffffe + x21) - x75);
-  out[9] = ((0x7fffe + x23) - x77);
-  out[10] = ((0x7fffe + x25) - x79);
-  out[11] = ((0x7fffe + x27) - x81);
-  out[12] = ((0xffffe + x29) - x83);
-  out[13] = ((0x7fffe + x31) - x85);
-  out[14] = ((0x7fffe + x33) - x87);
-  out[15] = ((0x7fffe + x35) - x89);
-  out[16] = ((0xffffe + x37) - x91);
-  out[17] = ((0x7fffe + x39) - x93);
-  out[18] = ((0x7fffe + x41) - x95);
-  out[19] = ((0x7fffe + x43) - x97);
-  out[20] = ((0xffffe + x45) - x99);
-  out[21] = ((0x7fffe + x47) - x101);
-  out[22] = ((0x7fffe + x49) - x103);
-  out[23] = ((0x7fffe + x51) - x105);
-  out[24] = ((0xffffe + x53) - x107);
-  out[25] = ((0x7fffe + x55) - x109);
-  out[26] = ((0x7fffe + x57) - x111);
-  out[27] = ((0x7fffe + x56) - x110);
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas32_2e511m187/fesub.v b/src/Specific/solinas32_2e511m187/fesub.v
deleted file mode 100644
index a65634a5e..000000000
--- a/src/Specific/solinas32_2e511m187/fesub.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas32_2e511m187.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_2e511m187/fesubDisplay.log b/src/Specific/solinas32_2e511m187/fesubDisplay.log
deleted file mode 100644
index 6f251e609..000000000
--- a/src/Specific/solinas32_2e511m187/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 * word32 * word32 * word32,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x56, x57, x55, x53, x51, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x110, x111, x109, x107, x105, x103, x101, x99, x97, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59))%core,
- (((0x7fffe + x56) - x110), ((0x7fffe + x57) - x111), ((0x7fffe + x55) - x109), ((0xffffe + x53) - x107), ((0x7fffe + x51) - x105), ((0x7fffe + x49) - x103), ((0x7fffe + x47) - x101), ((0xffffe + x45) - x99), ((0x7fffe + x43) - x97), ((0x7fffe + x41) - x95), ((0x7fffe + x39) - x93), ((0xffffe + x37) - x91), ((0x7fffe + x35) - x89), ((0x7fffe + x33) - x87), ((0x7fffe + x31) - x85), ((0xffffe + x29) - x83), ((0x7fffe + x27) - x81), ((0x7fffe + x25) - x79), ((0x7fffe + x23) - x77), ((0xffffe + x21) - x75), ((0x7fffe + x19) - x73), ((0x7fffe + x17) - x71), ((0x7fffe + x15) - x69), ((0xffffe + x13) - x67), ((0x7fffe + x11) - x65), ((0x7fffe + x9) - x63), ((0x7fffe + x7) - x61), ((0xffe8a + x5) - x59)))
-(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 * 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 * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e511m187/fesubDisplay.v b/src/Specific/solinas32_2e511m187/fesubDisplay.v
deleted file mode 100644
index f06160816..000000000
--- a/src/Specific/solinas32_2e511m187/fesubDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas32_2e511m187.fesub.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display sub.
diff --git a/src/Specific/solinas32_2e511m187/freeze.c b/src/Specific/solinas32_2e511m187/freeze.c
deleted file mode 100644
index 245df8444..000000000
--- a/src/Specific/solinas32_2e511m187/freeze.c
+++ /dev/null
@@ -1,144 +0,0 @@
-static void freeze(uint32_t out[28], const uint32_t in1[28]) {
-  { const uint32_t x53 = in1[27];
-  { const uint32_t x54 = in1[26];
-  { const uint32_t x52 = in1[25];
-  { const uint32_t x50 = 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 x56, uint8_t x57 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, 0x7ff45);
-  { uint32_t x59, uint8_t x60 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x57, Return x4, 0x3ffff);
-  { uint32_t x62, uint8_t x63 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x60, Return x6, 0x3ffff);
-  { uint32_t x65, uint8_t x66 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x63, Return x8, 0x3ffff);
-  { uint32_t x68, uint8_t x69 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x66, Return x10, 0x7ffff);
-  { uint32_t x71, uint8_t x72 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x69, Return x12, 0x3ffff);
-  { uint32_t x74, uint8_t x75 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x72, Return x14, 0x3ffff);
-  { uint32_t x77, uint8_t x78 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x75, Return x16, 0x3ffff);
-  { uint32_t x80, uint8_t x81 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x78, Return x18, 0x7ffff);
-  { uint32_t x83, uint8_t x84 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x81, Return x20, 0x3ffff);
-  { uint32_t x86, uint8_t x87 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x84, Return x22, 0x3ffff);
-  { uint32_t x89, uint8_t x90 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x87, Return x24, 0x3ffff);
-  { uint32_t x92, uint8_t x93 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x90, Return x26, 0x7ffff);
-  { uint32_t x95, uint8_t x96 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x93, Return x28, 0x3ffff);
-  { uint32_t x98, uint8_t x99 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x96, Return x30, 0x3ffff);
-  { uint32_t x101, uint8_t x102 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x99, Return x32, 0x3ffff);
-  { uint32_t x104, uint8_t x105 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x102, Return x34, 0x7ffff);
-  { uint32_t x107, uint8_t x108 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x105, Return x36, 0x3ffff);
-  { uint32_t x110, uint8_t x111 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x108, Return x38, 0x3ffff);
-  { uint32_t x113, uint8_t x114 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x111, Return x40, 0x3ffff);
-  { uint32_t x116, uint8_t x117 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x114, Return x42, 0x7ffff);
-  { uint32_t x119, uint8_t x120 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x117, Return x44, 0x3ffff);
-  { uint32_t x122, uint8_t x123 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x120, Return x46, 0x3ffff);
-  { uint32_t x125, uint8_t x126 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x123, Return x48, 0x3ffff);
-  { uint32_t x128, uint8_t x129 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x126, Return x50, 0x7ffff);
-  { uint32_t x131, uint8_t x132 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x129, Return x52, 0x3ffff);
-  { uint32_t x134, uint8_t x135 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x132, Return x54, 0x3ffff);
-  { uint32_t x137, uint8_t x138 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x135, Return x53, 0x3ffff);
-  { uint32_t x139 = cmovznz32(x138, 0x0, 0xffffffff);
-  { uint32_t x140 = (x139 & 0x7ff45);
-  { uint32_t x142, uint8_t x143 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x56, Return x140);
-  { uint32_t x144 = (x139 & 0x3ffff);
-  { uint32_t x146, uint8_t x147 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x143, Return x59, Return x144);
-  { uint32_t x148 = (x139 & 0x3ffff);
-  { uint32_t x150, uint8_t x151 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x147, Return x62, Return x148);
-  { uint32_t x152 = (x139 & 0x3ffff);
-  { uint32_t x154, uint8_t x155 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x151, Return x65, Return x152);
-  { uint32_t x156 = (x139 & 0x7ffff);
-  { uint32_t x158, uint8_t x159 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x155, Return x68, Return x156);
-  { uint32_t x160 = (x139 & 0x3ffff);
-  { uint32_t x162, uint8_t x163 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x159, Return x71, Return x160);
-  { uint32_t x164 = (x139 & 0x3ffff);
-  { uint32_t x166, uint8_t x167 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x163, Return x74, Return x164);
-  { uint32_t x168 = (x139 & 0x3ffff);
-  { uint32_t x170, uint8_t x171 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x167, Return x77, Return x168);
-  { uint32_t x172 = (x139 & 0x7ffff);
-  { uint32_t x174, uint8_t x175 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x171, Return x80, Return x172);
-  { uint32_t x176 = (x139 & 0x3ffff);
-  { uint32_t x178, uint8_t x179 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x175, Return x83, Return x176);
-  { uint32_t x180 = (x139 & 0x3ffff);
-  { uint32_t x182, uint8_t x183 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x179, Return x86, Return x180);
-  { uint32_t x184 = (x139 & 0x3ffff);
-  { uint32_t x186, uint8_t x187 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x183, Return x89, Return x184);
-  { uint32_t x188 = (x139 & 0x7ffff);
-  { uint32_t x190, uint8_t x191 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x187, Return x92, Return x188);
-  { uint32_t x192 = (x139 & 0x3ffff);
-  { uint32_t x194, uint8_t x195 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x191, Return x95, Return x192);
-  { uint32_t x196 = (x139 & 0x3ffff);
-  { uint32_t x198, uint8_t x199 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x195, Return x98, Return x196);
-  { uint32_t x200 = (x139 & 0x3ffff);
-  { uint32_t x202, uint8_t x203 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x199, Return x101, Return x200);
-  { uint32_t x204 = (x139 & 0x7ffff);
-  { uint32_t x206, uint8_t x207 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x203, Return x104, Return x204);
-  { uint32_t x208 = (x139 & 0x3ffff);
-  { uint32_t x210, uint8_t x211 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x207, Return x107, Return x208);
-  { uint32_t x212 = (x139 & 0x3ffff);
-  { uint32_t x214, uint8_t x215 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x211, Return x110, Return x212);
-  { uint32_t x216 = (x139 & 0x3ffff);
-  { uint32_t x218, uint8_t x219 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x215, Return x113, Return x216);
-  { uint32_t x220 = (x139 & 0x7ffff);
-  { uint32_t x222, uint8_t x223 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x219, Return x116, Return x220);
-  { uint32_t x224 = (x139 & 0x3ffff);
-  { uint32_t x226, uint8_t x227 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x223, Return x119, Return x224);
-  { uint32_t x228 = (x139 & 0x3ffff);
-  { uint32_t x230, uint8_t x231 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x227, Return x122, Return x228);
-  { uint32_t x232 = (x139 & 0x3ffff);
-  { uint32_t x234, uint8_t x235 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x231, Return x125, Return x232);
-  { uint32_t x236 = (x139 & 0x7ffff);
-  { uint32_t x238, uint8_t x239 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x235, Return x128, Return x236);
-  { uint32_t x240 = (x139 & 0x3ffff);
-  { uint32_t x242, uint8_t x243 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x239, Return x131, Return x240);
-  { uint32_t x244 = (x139 & 0x3ffff);
-  { uint32_t x246, uint8_t x247 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x243, Return x134, Return x244);
-  { uint32_t x248 = (x139 & 0x3ffff);
-  { uint32_t x250, uint8_t _ = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x247, Return x137, Return x248);
-  out[0] = x142;
-  out[1] = x146;
-  out[2] = x150;
-  out[3] = x154;
-  out[4] = x158;
-  out[5] = x162;
-  out[6] = x166;
-  out[7] = x170;
-  out[8] = x174;
-  out[9] = x178;
-  out[10] = x182;
-  out[11] = x186;
-  out[12] = x190;
-  out[13] = x194;
-  out[14] = x198;
-  out[15] = x202;
-  out[16] = x206;
-  out[17] = x210;
-  out[18] = x214;
-  out[19] = x218;
-  out[20] = x222;
-  out[21] = x226;
-  out[22] = x230;
-  out[23] = x234;
-  out[24] = x238;
-  out[25] = x242;
-  out[26] = x246;
-  out[27] = x250;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas32_2e511m187/freeze.v b/src/Specific/solinas32_2e511m187/freeze.v
deleted file mode 100644
index 7c748465a..000000000
--- a/src/Specific/solinas32_2e511m187/freeze.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas32_2e511m187.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_2e511m187/freezeDisplay.log b/src/Specific/solinas32_2e511m187/freezeDisplay.log
deleted file mode 100644
index 8d9b7d049..000000000
--- a/src/Specific/solinas32_2e511m187/freezeDisplay.log
+++ /dev/null
@@ -1,92 +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 * word32 * word32 * word32,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x53, x54, x52, x50, 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 x56, uint8_t x57 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, 0x7ff45);
- uint32_t x59, uint8_t x60 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x57, Return x4, 0x3ffff);
- uint32_t x62, uint8_t x63 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x60, Return x6, 0x3ffff);
- uint32_t x65, uint8_t x66 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x63, Return x8, 0x3ffff);
- uint32_t x68, uint8_t x69 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x66, Return x10, 0x7ffff);
- uint32_t x71, uint8_t x72 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x69, Return x12, 0x3ffff);
- uint32_t x74, uint8_t x75 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x72, Return x14, 0x3ffff);
- uint32_t x77, uint8_t x78 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x75, Return x16, 0x3ffff);
- uint32_t x80, uint8_t x81 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x78, Return x18, 0x7ffff);
- uint32_t x83, uint8_t x84 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x81, Return x20, 0x3ffff);
- uint32_t x86, uint8_t x87 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x84, Return x22, 0x3ffff);
- uint32_t x89, uint8_t x90 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x87, Return x24, 0x3ffff);
- uint32_t x92, uint8_t x93 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x90, Return x26, 0x7ffff);
- uint32_t x95, uint8_t x96 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x93, Return x28, 0x3ffff);
- uint32_t x98, uint8_t x99 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x96, Return x30, 0x3ffff);
- uint32_t x101, uint8_t x102 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x99, Return x32, 0x3ffff);
- uint32_t x104, uint8_t x105 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x102, Return x34, 0x7ffff);
- uint32_t x107, uint8_t x108 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x105, Return x36, 0x3ffff);
- uint32_t x110, uint8_t x111 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x108, Return x38, 0x3ffff);
- uint32_t x113, uint8_t x114 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x111, Return x40, 0x3ffff);
- uint32_t x116, uint8_t x117 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x114, Return x42, 0x7ffff);
- uint32_t x119, uint8_t x120 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x117, Return x44, 0x3ffff);
- uint32_t x122, uint8_t x123 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x120, Return x46, 0x3ffff);
- uint32_t x125, uint8_t x126 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x123, Return x48, 0x3ffff);
- uint32_t x128, uint8_t x129 = Op (Syntax.SubWithGetBorrow 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x126, Return x50, 0x7ffff);
- uint32_t x131, uint8_t x132 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x129, Return x52, 0x3ffff);
- uint32_t x134, uint8_t x135 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x132, Return x54, 0x3ffff);
- uint32_t x137, uint8_t x138 = Op (Syntax.SubWithGetBorrow 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x135, Return x53, 0x3ffff);
- uint32_t x139 = cmovznz32(x138, 0x0, 0xffffffff);
- uint32_t x140 = (x139 & 0x7ff45);
- uint32_t x142, uint8_t x143 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x56, Return x140);
- uint32_t x144 = (x139 & 0x3ffff);
- uint32_t x146, uint8_t x147 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x143, Return x59, Return x144);
- uint32_t x148 = (x139 & 0x3ffff);
- uint32_t x150, uint8_t x151 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x147, Return x62, Return x148);
- uint32_t x152 = (x139 & 0x3ffff);
- uint32_t x154, uint8_t x155 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x151, Return x65, Return x152);
- uint32_t x156 = (x139 & 0x7ffff);
- uint32_t x158, uint8_t x159 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x155, Return x68, Return x156);
- uint32_t x160 = (x139 & 0x3ffff);
- uint32_t x162, uint8_t x163 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x159, Return x71, Return x160);
- uint32_t x164 = (x139 & 0x3ffff);
- uint32_t x166, uint8_t x167 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x163, Return x74, Return x164);
- uint32_t x168 = (x139 & 0x3ffff);
- uint32_t x170, uint8_t x171 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x167, Return x77, Return x168);
- uint32_t x172 = (x139 & 0x7ffff);
- uint32_t x174, uint8_t x175 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x171, Return x80, Return x172);
- uint32_t x176 = (x139 & 0x3ffff);
- uint32_t x178, uint8_t x179 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x175, Return x83, Return x176);
- uint32_t x180 = (x139 & 0x3ffff);
- uint32_t x182, uint8_t x183 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x179, Return x86, Return x180);
- uint32_t x184 = (x139 & 0x3ffff);
- uint32_t x186, uint8_t x187 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x183, Return x89, Return x184);
- uint32_t x188 = (x139 & 0x7ffff);
- uint32_t x190, uint8_t x191 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x187, Return x92, Return x188);
- uint32_t x192 = (x139 & 0x3ffff);
- uint32_t x194, uint8_t x195 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x191, Return x95, Return x192);
- uint32_t x196 = (x139 & 0x3ffff);
- uint32_t x198, uint8_t x199 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x195, Return x98, Return x196);
- uint32_t x200 = (x139 & 0x3ffff);
- uint32_t x202, uint8_t x203 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x199, Return x101, Return x200);
- uint32_t x204 = (x139 & 0x7ffff);
- uint32_t x206, uint8_t x207 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x203, Return x104, Return x204);
- uint32_t x208 = (x139 & 0x3ffff);
- uint32_t x210, uint8_t x211 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x207, Return x107, Return x208);
- uint32_t x212 = (x139 & 0x3ffff);
- uint32_t x214, uint8_t x215 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x211, Return x110, Return x212);
- uint32_t x216 = (x139 & 0x3ffff);
- uint32_t x218, uint8_t x219 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x215, Return x113, Return x216);
- uint32_t x220 = (x139 & 0x7ffff);
- uint32_t x222, uint8_t x223 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x219, Return x116, Return x220);
- uint32_t x224 = (x139 & 0x3ffff);
- uint32_t x226, uint8_t x227 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x223, Return x119, Return x224);
- uint32_t x228 = (x139 & 0x3ffff);
- uint32_t x230, uint8_t x231 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x227, Return x122, Return x228);
- uint32_t x232 = (x139 & 0x3ffff);
- uint32_t x234, uint8_t x235 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x231, Return x125, Return x232);
- uint32_t x236 = (x139 & 0x7ffff);
- uint32_t x238, uint8_t x239 = Op (Syntax.AddWithGetCarry 19 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x235, Return x128, Return x236);
- uint32_t x240 = (x139 & 0x3ffff);
- uint32_t x242, uint8_t x243 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x239, Return x131, Return x240);
- uint32_t x244 = (x139 & 0x3ffff);
- uint32_t x246, uint8_t x247 = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x243, Return x134, Return x244);
- uint32_t x248 = (x139 & 0x3ffff);
- uint32_t x250, uint8_t _ = Op (Syntax.AddWithGetCarry 18 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x247, Return x137, Return x248);
- (Return x250, Return x246, Return x242, Return x238, Return x234, Return x230, Return x226, Return x222, Return x218, Return x214, Return x210, Return x206, Return x202, Return x198, Return x194, Return x190, Return x186, Return x182, Return x178, Return x174, Return x170, Return x166, Return x162, Return x158, Return x154, Return x150, Return x146, Return x142))
-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 * 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 * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e511m187/freezeDisplay.v b/src/Specific/solinas32_2e511m187/freezeDisplay.v
deleted file mode 100644
index 1e93eb9be..000000000
--- a/src/Specific/solinas32_2e511m187/freezeDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas32_2e511m187.freeze.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display freeze.
diff --git a/src/Specific/solinas32_2e511m187/py_interpreter.sh b/src/Specific/solinas32_2e511m187/py_interpreter.sh
deleted file mode 100755
index 6900eaec6..000000000
--- a/src/Specific/solinas32_2e511m187/py_interpreter.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-/usr/bin/env python3 "$@" -Dq='2**511 - 187' -Dmodulus_bytes='18.25' -Da24='121665'