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_2e243m9_6limbs/CurveParameters.v     | 39 -----------------
 src/Specific/solinas64_2e243m9_6limbs/Synthesis.v  |  9 ----
 src/Specific/solinas64_2e243m9_6limbs/compiler.sh  |  4 --
 .../solinas64_2e243m9_6limbs/compilerxx.sh         |  4 --
 src/Specific/solinas64_2e243m9_6limbs/feadd.c      | 21 ---------
 src/Specific/solinas64_2e243m9_6limbs/feadd.v      | 14 ------
 .../solinas64_2e243m9_6limbs/feaddDisplay.log      |  7 ---
 .../solinas64_2e243m9_6limbs/feaddDisplay.v        |  4 --
 src/Specific/solinas64_2e243m9_6limbs/fecarry.v    | 14 ------
 .../solinas64_2e243m9_6limbs/fecarryDisplay.v      |  4 --
 src/Specific/solinas64_2e243m9_6limbs/femul.c      | 50 ----------------------
 src/Specific/solinas64_2e243m9_6limbs/femul.v      | 14 ------
 .../solinas64_2e243m9_6limbs/femulDisplay.log      | 36 ----------------
 .../solinas64_2e243m9_6limbs/femulDisplay.v        |  4 --
 src/Specific/solinas64_2e243m9_6limbs/fesquare.c   | 44 -------------------
 src/Specific/solinas64_2e243m9_6limbs/fesquare.v   | 14 ------
 .../solinas64_2e243m9_6limbs/fesquareDisplay.log   | 36 ----------------
 .../solinas64_2e243m9_6limbs/fesquareDisplay.v     |  4 --
 src/Specific/solinas64_2e243m9_6limbs/fesub.c      | 21 ---------
 src/Specific/solinas64_2e243m9_6limbs/fesub.v      | 14 ------
 .../solinas64_2e243m9_6limbs/fesubDisplay.log      |  7 ---
 .../solinas64_2e243m9_6limbs/fesubDisplay.v        |  4 --
 src/Specific/solinas64_2e243m9_6limbs/freeze.c     | 34 ---------------
 src/Specific/solinas64_2e243m9_6limbs/freeze.v     | 14 ------
 .../solinas64_2e243m9_6limbs/freezeDisplay.log     | 26 -----------
 .../solinas64_2e243m9_6limbs/freezeDisplay.v       |  4 --
 .../solinas64_2e243m9_6limbs/py_interpreter.sh     |  4 --
 27 files changed, 450 deletions(-)
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/CurveParameters.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/Synthesis.v
 delete mode 100755 src/Specific/solinas64_2e243m9_6limbs/compiler.sh
 delete mode 100755 src/Specific/solinas64_2e243m9_6limbs/compilerxx.sh
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/feadd.c
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/feadd.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/feaddDisplay.log
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/feaddDisplay.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fecarry.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fecarryDisplay.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/femul.c
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/femul.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/femulDisplay.log
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/femulDisplay.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesquare.c
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesquare.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesquareDisplay.log
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesquareDisplay.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesub.c
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesub.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesubDisplay.log
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/fesubDisplay.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/freeze.c
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/freeze.v
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/freezeDisplay.log
 delete mode 100644 src/Specific/solinas64_2e243m9_6limbs/freezeDisplay.v
 delete mode 100755 src/Specific/solinas64_2e243m9_6limbs/py_interpreter.sh

(limited to 'src/Specific/solinas64_2e243m9_6limbs')

diff --git a/src/Specific/solinas64_2e243m9_6limbs/CurveParameters.v b/src/Specific/solinas64_2e243m9_6limbs/CurveParameters.v
deleted file mode 100644
index 60427d462..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/CurveParameters.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^243 - 9
-Base: 40.5
-***)
-
-Definition curve : CurveParameters :=
-  {|
-    sz := 6%nat;
-    base := 40 + 1/2;
-    bitwidth := 64;
-    s := 2^243;
-    c := [(1, 9)];
-    carry_chains := Some [seq 0 (pred 6); [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_2e243m9_6limbs/Synthesis.v b/src/Specific/solinas64_2e243m9_6limbs/Synthesis.v
deleted file mode 100644
index 07fd26c97..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.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_2e243m9_6limbs/compiler.sh b/src/Specific/solinas64_2e243m9_6limbs/compiler.sh
deleted file mode 100755
index 0791ed971..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/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,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{41,40,41,40,41,40}' -Dmodulus_array='{0x07,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xf7}' -Dmodulus_bytes_val='31' -Dmodulus_limbs='6' -Dq_mpz='(1_mpz<<243) - 9' "$@"
diff --git a/src/Specific/solinas64_2e243m9_6limbs/compilerxx.sh b/src/Specific/solinas64_2e243m9_6limbs/compilerxx.sh
deleted file mode 100755
index 8bcf69417..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/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,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{41,40,41,40,41,40}' -Dmodulus_array='{0x07,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xf7}' -Dmodulus_bytes_val='31' -Dmodulus_limbs='6' -Dq_mpz='(1_mpz<<243) - 9' "$@"
diff --git a/src/Specific/solinas64_2e243m9_6limbs/feadd.c b/src/Specific/solinas64_2e243m9_6limbs/feadd.c
deleted file mode 100644
index 4a6bfb999..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/feadd.c
+++ /dev/null
@@ -1,21 +0,0 @@
-static void feadd(uint64_t out[6], const uint64_t in1[6], const uint64_t in2[6]) {
-  { const uint64_t x12 = 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 x22 = in2[5];
-  { const uint64_t x23 = in2[4];
-  { const uint64_t x21 = in2[3];
-  { const uint64_t x19 = in2[2];
-  { const uint64_t x17 = in2[1];
-  { const uint64_t x15 = in2[0];
-  out[0] = (x5 + x15);
-  out[1] = (x7 + x17);
-  out[2] = (x9 + x19);
-  out[3] = (x11 + x21);
-  out[4] = (x13 + x23);
-  out[5] = (x12 + x22);
-  }}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e243m9_6limbs/feadd.v b/src/Specific/solinas64_2e243m9_6limbs/feadd.v
deleted file mode 100644
index 95f06fad0..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/feadd.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.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_2e243m9_6limbs/feaddDisplay.log b/src/Specific/solinas64_2e243m9_6limbs/feaddDisplay.log
deleted file mode 100644
index e32995a81..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/feaddDisplay.log
+++ /dev/null
@@ -1,7 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core,
- ((x12 + x22), (x13 + x23), (x11 + x21), (x9 + x19), (x7 + x17), (x5 + x15)))
-(x, x0)%core
-     : 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)
diff --git a/src/Specific/solinas64_2e243m9_6limbs/feaddDisplay.v b/src/Specific/solinas64_2e243m9_6limbs/feaddDisplay.v
deleted file mode 100644
index a63e71554..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/feaddDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.feadd.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display add.
diff --git a/src/Specific/solinas64_2e243m9_6limbs/fecarry.v b/src/Specific/solinas64_2e243m9_6limbs/fecarry.v
deleted file mode 100644
index 832dcd6b3..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fecarry.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.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_2e243m9_6limbs/fecarryDisplay.v b/src/Specific/solinas64_2e243m9_6limbs/fecarryDisplay.v
deleted file mode 100644
index 5d470ddea..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fecarryDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.fecarry.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display carry.
diff --git a/src/Specific/solinas64_2e243m9_6limbs/femul.c b/src/Specific/solinas64_2e243m9_6limbs/femul.c
deleted file mode 100644
index 1f3dd625a..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/femul.c
+++ /dev/null
@@ -1,50 +0,0 @@
-static void femul(uint64_t out[6], const uint64_t in1[6], const uint64_t in2[6]) {
-  { const uint64_t x12 = 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 x22 = in2[5];
-  { const uint64_t x23 = in2[4];
-  { const uint64_t x21 = in2[3];
-  { const uint64_t x19 = in2[2];
-  { const uint64_t x17 = in2[1];
-  { const uint64_t x15 = in2[0];
-  { uint128_t x24 = (((uint128_t)x5 * x22) + (((uint128_t)x7 * x23) + (((uint128_t)x9 * x21) + (((uint128_t)x11 * x19) + (((uint128_t)x13 * x17) + ((uint128_t)x12 * x15))))));
-  { uint128_t x25 = ((((uint128_t)x5 * x23) + ((0x2 * ((uint128_t)x7 * x21)) + (((uint128_t)x9 * x19) + ((0x2 * ((uint128_t)x11 * x17)) + ((uint128_t)x13 * x15))))) + (0x9 * (0x2 * ((uint128_t)x12 * x22))));
-  { uint128_t x26 = ((((uint128_t)x5 * x21) + (((uint128_t)x7 * x19) + (((uint128_t)x9 * x17) + ((uint128_t)x11 * x15)))) + (0x9 * (((uint128_t)x13 * x22) + ((uint128_t)x12 * x23))));
-  { uint128_t x27 = ((((uint128_t)x5 * x19) + ((0x2 * ((uint128_t)x7 * x17)) + ((uint128_t)x9 * x15))) + (0x9 * ((0x2 * ((uint128_t)x11 * x22)) + (((uint128_t)x13 * x23) + (0x2 * ((uint128_t)x12 * x21))))));
-  { uint128_t x28 = ((((uint128_t)x5 * x17) + ((uint128_t)x7 * x15)) + (0x9 * (((uint128_t)x9 * x22) + (((uint128_t)x11 * x23) + (((uint128_t)x13 * x21) + ((uint128_t)x12 * x19))))));
-  { uint128_t x29 = (((uint128_t)x5 * x15) + (0x9 * ((0x2 * ((uint128_t)x7 * x22)) + (((uint128_t)x9 * x23) + ((0x2 * ((uint128_t)x11 * x21)) + (((uint128_t)x13 * x19) + (0x2 * ((uint128_t)x12 * x17))))))));
-  { uint64_t x30 = (uint64_t) (x29 >> 0x29);
-  { uint64_t x31 = ((uint64_t)x29 & 0x1ffffffffff);
-  { uint128_t x32 = (x30 + x28);
-  { uint64_t x33 = (uint64_t) (x32 >> 0x28);
-  { uint64_t x34 = ((uint64_t)x32 & 0xffffffffff);
-  { uint128_t x35 = (x33 + x27);
-  { uint64_t x36 = (uint64_t) (x35 >> 0x29);
-  { uint64_t x37 = ((uint64_t)x35 & 0x1ffffffffff);
-  { uint128_t x38 = (x36 + x26);
-  { uint64_t x39 = (uint64_t) (x38 >> 0x28);
-  { uint64_t x40 = ((uint64_t)x38 & 0xffffffffff);
-  { uint128_t x41 = (x39 + x25);
-  { uint64_t x42 = (uint64_t) (x41 >> 0x29);
-  { uint64_t x43 = ((uint64_t)x41 & 0x1ffffffffff);
-  { uint128_t x44 = (x42 + x24);
-  { uint64_t x45 = (uint64_t) (x44 >> 0x28);
-  { uint64_t x46 = ((uint64_t)x44 & 0xffffffffff);
-  { uint64_t x47 = (x31 + (0x9 * x45));
-  { uint64_t x48 = (x47 >> 0x29);
-  { uint64_t x49 = (x47 & 0x1ffffffffff);
-  { uint64_t x50 = (x48 + x34);
-  { uint64_t x51 = (x50 >> 0x28);
-  { uint64_t x52 = (x50 & 0xffffffffff);
-  out[0] = x49;
-  out[1] = x52;
-  out[2] = (x51 + x37);
-  out[3] = x40;
-  out[4] = x43;
-  out[5] = x46;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e243m9_6limbs/femul.v b/src/Specific/solinas64_2e243m9_6limbs/femul.v
deleted file mode 100644
index 28872402d..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/femul.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.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_2e243m9_6limbs/femulDisplay.log b/src/Specific/solinas64_2e243m9_6limbs/femulDisplay.log
deleted file mode 100644
index 6b6b1ee55..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/femulDisplay.log
+++ /dev/null
@@ -1,36 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core,
- uint128_t x24 = (((uint128_t)x5 * x22) + (((uint128_t)x7 * x23) + (((uint128_t)x9 * x21) + (((uint128_t)x11 * x19) + (((uint128_t)x13 * x17) + ((uint128_t)x12 * x15))))));
- uint128_t x25 = ((((uint128_t)x5 * x23) + ((0x2 * ((uint128_t)x7 * x21)) + (((uint128_t)x9 * x19) + ((0x2 * ((uint128_t)x11 * x17)) + ((uint128_t)x13 * x15))))) + (0x9 * (0x2 * ((uint128_t)x12 * x22))));
- uint128_t x26 = ((((uint128_t)x5 * x21) + (((uint128_t)x7 * x19) + (((uint128_t)x9 * x17) + ((uint128_t)x11 * x15)))) + (0x9 * (((uint128_t)x13 * x22) + ((uint128_t)x12 * x23))));
- uint128_t x27 = ((((uint128_t)x5 * x19) + ((0x2 * ((uint128_t)x7 * x17)) + ((uint128_t)x9 * x15))) + (0x9 * ((0x2 * ((uint128_t)x11 * x22)) + (((uint128_t)x13 * x23) + (0x2 * ((uint128_t)x12 * x21))))));
- uint128_t x28 = ((((uint128_t)x5 * x17) + ((uint128_t)x7 * x15)) + (0x9 * (((uint128_t)x9 * x22) + (((uint128_t)x11 * x23) + (((uint128_t)x13 * x21) + ((uint128_t)x12 * x19))))));
- uint128_t x29 = (((uint128_t)x5 * x15) + (0x9 * ((0x2 * ((uint128_t)x7 * x22)) + (((uint128_t)x9 * x23) + ((0x2 * ((uint128_t)x11 * x21)) + (((uint128_t)x13 * x19) + (0x2 * ((uint128_t)x12 * x17))))))));
- uint64_t x30 = (uint64_t) (x29 >> 0x29);
- uint64_t x31 = ((uint64_t)x29 & 0x1ffffffffff);
- uint128_t x32 = (x30 + x28);
- uint64_t x33 = (uint64_t) (x32 >> 0x28);
- uint64_t x34 = ((uint64_t)x32 & 0xffffffffff);
- uint128_t x35 = (x33 + x27);
- uint64_t x36 = (uint64_t) (x35 >> 0x29);
- uint64_t x37 = ((uint64_t)x35 & 0x1ffffffffff);
- uint128_t x38 = (x36 + x26);
- uint64_t x39 = (uint64_t) (x38 >> 0x28);
- uint64_t x40 = ((uint64_t)x38 & 0xffffffffff);
- uint128_t x41 = (x39 + x25);
- uint64_t x42 = (uint64_t) (x41 >> 0x29);
- uint64_t x43 = ((uint64_t)x41 & 0x1ffffffffff);
- uint128_t x44 = (x42 + x24);
- uint64_t x45 = (uint64_t) (x44 >> 0x28);
- uint64_t x46 = ((uint64_t)x44 & 0xffffffffff);
- uint64_t x47 = (x31 + (0x9 * x45));
- uint64_t x48 = (x47 >> 0x29);
- uint64_t x49 = (x47 & 0x1ffffffffff);
- uint64_t x50 = (x48 + x34);
- uint64_t x51 = (x50 >> 0x28);
- uint64_t x52 = (x50 & 0xffffffffff);
- return (Return x46, Return x43, Return x40, (x51 + x37), Return x52, Return x49))
-(x, x0)%core
-     : 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)
diff --git a/src/Specific/solinas64_2e243m9_6limbs/femulDisplay.v b/src/Specific/solinas64_2e243m9_6limbs/femulDisplay.v
deleted file mode 100644
index 7431207de..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/femulDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.femul.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display mul.
diff --git a/src/Specific/solinas64_2e243m9_6limbs/fesquare.c b/src/Specific/solinas64_2e243m9_6limbs/fesquare.c
deleted file mode 100644
index c1d0d52c6..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesquare.c
+++ /dev/null
@@ -1,44 +0,0 @@
-static void fesquare(uint64_t out[6], const uint64_t in1[6]) {
-  { const uint64_t x9 = 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 x11 = (((uint128_t)x2 * x9) + (((uint128_t)x4 * x10) + (((uint128_t)x6 * x8) + (((uint128_t)x8 * x6) + (((uint128_t)x10 * x4) + ((uint128_t)x9 * x2))))));
-  { uint128_t x12 = ((((uint128_t)x2 * x10) + ((0x2 * ((uint128_t)x4 * x8)) + (((uint128_t)x6 * x6) + ((0x2 * ((uint128_t)x8 * x4)) + ((uint128_t)x10 * x2))))) + (0x9 * (0x2 * ((uint128_t)x9 * x9))));
-  { uint128_t x13 = ((((uint128_t)x2 * x8) + (((uint128_t)x4 * x6) + (((uint128_t)x6 * x4) + ((uint128_t)x8 * x2)))) + (0x9 * (((uint128_t)x10 * x9) + ((uint128_t)x9 * x10))));
-  { uint128_t x14 = ((((uint128_t)x2 * x6) + ((0x2 * ((uint128_t)x4 * x4)) + ((uint128_t)x6 * x2))) + (0x9 * ((0x2 * ((uint128_t)x8 * x9)) + (((uint128_t)x10 * x10) + (0x2 * ((uint128_t)x9 * x8))))));
-  { uint128_t x15 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x9 * (((uint128_t)x6 * x9) + (((uint128_t)x8 * x10) + (((uint128_t)x10 * x8) + ((uint128_t)x9 * x6))))));
-  { uint128_t x16 = (((uint128_t)x2 * x2) + (0x9 * ((0x2 * ((uint128_t)x4 * x9)) + (((uint128_t)x6 * x10) + ((0x2 * ((uint128_t)x8 * x8)) + (((uint128_t)x10 * x6) + (0x2 * ((uint128_t)x9 * x4))))))));
-  { uint64_t x17 = (uint64_t) (x16 >> 0x29);
-  { uint64_t x18 = ((uint64_t)x16 & 0x1ffffffffff);
-  { uint128_t x19 = (x17 + x15);
-  { uint64_t x20 = (uint64_t) (x19 >> 0x28);
-  { uint64_t x21 = ((uint64_t)x19 & 0xffffffffff);
-  { uint128_t x22 = (x20 + x14);
-  { uint64_t x23 = (uint64_t) (x22 >> 0x29);
-  { uint64_t x24 = ((uint64_t)x22 & 0x1ffffffffff);
-  { uint128_t x25 = (x23 + x13);
-  { uint64_t x26 = (uint64_t) (x25 >> 0x28);
-  { uint64_t x27 = ((uint64_t)x25 & 0xffffffffff);
-  { uint128_t x28 = (x26 + x12);
-  { uint64_t x29 = (uint64_t) (x28 >> 0x29);
-  { uint64_t x30 = ((uint64_t)x28 & 0x1ffffffffff);
-  { uint128_t x31 = (x29 + x11);
-  { uint64_t x32 = (uint64_t) (x31 >> 0x28);
-  { uint64_t x33 = ((uint64_t)x31 & 0xffffffffff);
-  { uint64_t x34 = (x18 + (0x9 * x32));
-  { uint64_t x35 = (x34 >> 0x29);
-  { uint64_t x36 = (x34 & 0x1ffffffffff);
-  { uint64_t x37 = (x35 + x21);
-  { uint64_t x38 = (x37 >> 0x28);
-  { uint64_t x39 = (x37 & 0xffffffffff);
-  out[0] = x36;
-  out[1] = x39;
-  out[2] = (x38 + x24);
-  out[3] = x27;
-  out[4] = x30;
-  out[5] = x33;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e243m9_6limbs/fesquare.v b/src/Specific/solinas64_2e243m9_6limbs/fesquare.v
deleted file mode 100644
index e5a459bfa..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesquare.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.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_2e243m9_6limbs/fesquareDisplay.log b/src/Specific/solinas64_2e243m9_6limbs/fesquareDisplay.log
deleted file mode 100644
index 5b9f6a27c..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesquareDisplay.log
+++ /dev/null
@@ -1,36 +0,0 @@
-λ x : word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x9, x10, x8, x6, x4, x2)%core,
- uint128_t x11 = (((uint128_t)x2 * x9) + (((uint128_t)x4 * x10) + (((uint128_t)x6 * x8) + (((uint128_t)x8 * x6) + (((uint128_t)x10 * x4) + ((uint128_t)x9 * x2))))));
- uint128_t x12 = ((((uint128_t)x2 * x10) + ((0x2 * ((uint128_t)x4 * x8)) + (((uint128_t)x6 * x6) + ((0x2 * ((uint128_t)x8 * x4)) + ((uint128_t)x10 * x2))))) + (0x9 * (0x2 * ((uint128_t)x9 * x9))));
- uint128_t x13 = ((((uint128_t)x2 * x8) + (((uint128_t)x4 * x6) + (((uint128_t)x6 * x4) + ((uint128_t)x8 * x2)))) + (0x9 * (((uint128_t)x10 * x9) + ((uint128_t)x9 * x10))));
- uint128_t x14 = ((((uint128_t)x2 * x6) + ((0x2 * ((uint128_t)x4 * x4)) + ((uint128_t)x6 * x2))) + (0x9 * ((0x2 * ((uint128_t)x8 * x9)) + (((uint128_t)x10 * x10) + (0x2 * ((uint128_t)x9 * x8))))));
- uint128_t x15 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x9 * (((uint128_t)x6 * x9) + (((uint128_t)x8 * x10) + (((uint128_t)x10 * x8) + ((uint128_t)x9 * x6))))));
- uint128_t x16 = (((uint128_t)x2 * x2) + (0x9 * ((0x2 * ((uint128_t)x4 * x9)) + (((uint128_t)x6 * x10) + ((0x2 * ((uint128_t)x8 * x8)) + (((uint128_t)x10 * x6) + (0x2 * ((uint128_t)x9 * x4))))))));
- uint64_t x17 = (uint64_t) (x16 >> 0x29);
- uint64_t x18 = ((uint64_t)x16 & 0x1ffffffffff);
- uint128_t x19 = (x17 + x15);
- uint64_t x20 = (uint64_t) (x19 >> 0x28);
- uint64_t x21 = ((uint64_t)x19 & 0xffffffffff);
- uint128_t x22 = (x20 + x14);
- uint64_t x23 = (uint64_t) (x22 >> 0x29);
- uint64_t x24 = ((uint64_t)x22 & 0x1ffffffffff);
- uint128_t x25 = (x23 + x13);
- uint64_t x26 = (uint64_t) (x25 >> 0x28);
- uint64_t x27 = ((uint64_t)x25 & 0xffffffffff);
- uint128_t x28 = (x26 + x12);
- uint64_t x29 = (uint64_t) (x28 >> 0x29);
- uint64_t x30 = ((uint64_t)x28 & 0x1ffffffffff);
- uint128_t x31 = (x29 + x11);
- uint64_t x32 = (uint64_t) (x31 >> 0x28);
- uint64_t x33 = ((uint64_t)x31 & 0xffffffffff);
- uint64_t x34 = (x18 + (0x9 * x32));
- uint64_t x35 = (x34 >> 0x29);
- uint64_t x36 = (x34 & 0x1ffffffffff);
- uint64_t x37 = (x35 + x21);
- uint64_t x38 = (x37 >> 0x28);
- uint64_t x39 = (x37 & 0xffffffffff);
- return (Return x33, Return x30, Return x27, (x38 + x24), Return x39, Return x36))
-x
-     : word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e243m9_6limbs/fesquareDisplay.v b/src/Specific/solinas64_2e243m9_6limbs/fesquareDisplay.v
deleted file mode 100644
index 097098540..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesquareDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.fesquare.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display square.
diff --git a/src/Specific/solinas64_2e243m9_6limbs/fesub.c b/src/Specific/solinas64_2e243m9_6limbs/fesub.c
deleted file mode 100644
index 50c317b29..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesub.c
+++ /dev/null
@@ -1,21 +0,0 @@
-static void fesub(uint64_t out[6], const uint64_t in1[6], const uint64_t in2[6]) {
-  { const uint64_t x12 = 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 x22 = in2[5];
-  { const uint64_t x23 = in2[4];
-  { const uint64_t x21 = in2[3];
-  { const uint64_t x19 = in2[2];
-  { const uint64_t x17 = in2[1];
-  { const uint64_t x15 = in2[0];
-  out[0] = ((0x3ffffffffee + x5) - x15);
-  out[1] = ((0x1fffffffffe + x7) - x17);
-  out[2] = ((0x3fffffffffe + x9) - x19);
-  out[3] = ((0x1fffffffffe + x11) - x21);
-  out[4] = ((0x3fffffffffe + x13) - x23);
-  out[5] = ((0x1fffffffffe + x12) - x22);
-  }}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e243m9_6limbs/fesub.v b/src/Specific/solinas64_2e243m9_6limbs/fesub.v
deleted file mode 100644
index 9745e8c81..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesub.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.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_2e243m9_6limbs/fesubDisplay.log b/src/Specific/solinas64_2e243m9_6limbs/fesubDisplay.log
deleted file mode 100644
index 22e0778d0..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesubDisplay.log
+++ /dev/null
@@ -1,7 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core,
- (((0x1fffffffffe + x12) - x22), ((0x3fffffffffe + x13) - x23), ((0x1fffffffffe + x11) - x21), ((0x3fffffffffe + x9) - x19), ((0x1fffffffffe + x7) - x17), ((0x3ffffffffee + x5) - x15)))
-(x, x0)%core
-     : 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)
diff --git a/src/Specific/solinas64_2e243m9_6limbs/fesubDisplay.v b/src/Specific/solinas64_2e243m9_6limbs/fesubDisplay.v
deleted file mode 100644
index c91eee1fa..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/fesubDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.fesub.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display sub.
diff --git a/src/Specific/solinas64_2e243m9_6limbs/freeze.c b/src/Specific/solinas64_2e243m9_6limbs/freeze.c
deleted file mode 100644
index 56fe99d55..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/freeze.c
+++ /dev/null
@@ -1,34 +0,0 @@
-static void freeze(uint64_t out[6], const uint64_t in1[6]) {
-  { const uint64_t x9 = 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 x12, uint8_t x13 = Op (Syntax.SubWithGetBorrow 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0x1fffffffff7);
-  { uint64_t x15, uint8_t x16 = Op (Syntax.SubWithGetBorrow 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x13, Return x4, 0xffffffffff);
-  { uint64_t x18, uint8_t x19 = Op (Syntax.SubWithGetBorrow 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x16, Return x6, 0x1ffffffffff);
-  { uint64_t x21, uint8_t x22 = Op (Syntax.SubWithGetBorrow 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x19, Return x8, 0xffffffffff);
-  { uint64_t x24, uint8_t x25 = Op (Syntax.SubWithGetBorrow 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x22, Return x10, 0x1ffffffffff);
-  { uint64_t x27, uint8_t x28 = Op (Syntax.SubWithGetBorrow 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x25, Return x9, 0xffffffffff);
-  { uint64_t x29 = cmovznz64(x28, 0x0, 0xffffffffffffffffL);
-  { uint64_t x30 = (x29 & 0x1fffffffff7);
-  { uint64_t x32, uint8_t x33 = Op (Syntax.AddWithGetCarry 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x12, Return x30);
-  { uint64_t x34 = (x29 & 0xffffffffff);
-  { uint64_t x36, uint8_t x37 = Op (Syntax.AddWithGetCarry 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x33, Return x15, Return x34);
-  { uint64_t x38 = (x29 & 0x1ffffffffff);
-  { uint64_t x40, uint8_t x41 = Op (Syntax.AddWithGetCarry 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x37, Return x18, Return x38);
-  { uint64_t x42 = (x29 & 0xffffffffff);
-  { uint64_t x44, uint8_t x45 = Op (Syntax.AddWithGetCarry 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x41, Return x21, Return x42);
-  { uint64_t x46 = (x29 & 0x1ffffffffff);
-  { uint64_t x48, uint8_t x49 = Op (Syntax.AddWithGetCarry 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x45, Return x24, Return x46);
-  { uint64_t x50 = (x29 & 0xffffffffff);
-  { uint64_t x52, uint8_t _ = Op (Syntax.AddWithGetCarry 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x49, Return x27, Return x50);
-  out[0] = x32;
-  out[1] = x36;
-  out[2] = x40;
-  out[3] = x44;
-  out[4] = x48;
-  out[5] = x52;
-  }}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e243m9_6limbs/freeze.v b/src/Specific/solinas64_2e243m9_6limbs/freeze.v
deleted file mode 100644
index 69c91e045..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/freeze.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.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_2e243m9_6limbs/freezeDisplay.log b/src/Specific/solinas64_2e243m9_6limbs/freezeDisplay.log
deleted file mode 100644
index 2240ec6b1..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/freezeDisplay.log
+++ /dev/null
@@ -1,26 +0,0 @@
-λ x : word64 * word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x9, x10, x8, x6, x4, x2)%core,
- uint64_t x12, uint8_t x13 = Op (Syntax.SubWithGetBorrow 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0x1fffffffff7);
- uint64_t x15, uint8_t x16 = Op (Syntax.SubWithGetBorrow 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x13, Return x4, 0xffffffffff);
- uint64_t x18, uint8_t x19 = Op (Syntax.SubWithGetBorrow 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x16, Return x6, 0x1ffffffffff);
- uint64_t x21, uint8_t x22 = Op (Syntax.SubWithGetBorrow 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x19, Return x8, 0xffffffffff);
- uint64_t x24, uint8_t x25 = Op (Syntax.SubWithGetBorrow 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x22, Return x10, 0x1ffffffffff);
- uint64_t x27, uint8_t x28 = Op (Syntax.SubWithGetBorrow 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x25, Return x9, 0xffffffffff);
- uint64_t x29 = cmovznz64(x28, 0x0, 0xffffffffffffffffL);
- uint64_t x30 = (x29 & 0x1fffffffff7);
- uint64_t x32, uint8_t x33 = Op (Syntax.AddWithGetCarry 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x12, Return x30);
- uint64_t x34 = (x29 & 0xffffffffff);
- uint64_t x36, uint8_t x37 = Op (Syntax.AddWithGetCarry 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x33, Return x15, Return x34);
- uint64_t x38 = (x29 & 0x1ffffffffff);
- uint64_t x40, uint8_t x41 = Op (Syntax.AddWithGetCarry 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x37, Return x18, Return x38);
- uint64_t x42 = (x29 & 0xffffffffff);
- uint64_t x44, uint8_t x45 = Op (Syntax.AddWithGetCarry 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x41, Return x21, Return x42);
- uint64_t x46 = (x29 & 0x1ffffffffff);
- uint64_t x48, uint8_t x49 = Op (Syntax.AddWithGetCarry 41 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x45, Return x24, Return x46);
- uint64_t x50 = (x29 & 0xffffffffff);
- uint64_t x52, uint8_t _ = Op (Syntax.AddWithGetCarry 40 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x49, Return x27, Return x50);
- (Return x52, Return x48, Return x44, Return x40, Return x36, Return x32))
-x
-     : word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e243m9_6limbs/freezeDisplay.v b/src/Specific/solinas64_2e243m9_6limbs/freezeDisplay.v
deleted file mode 100644
index d935e124e..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/freezeDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e243m9_6limbs.freeze.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display freeze.
diff --git a/src/Specific/solinas64_2e243m9_6limbs/py_interpreter.sh b/src/Specific/solinas64_2e243m9_6limbs/py_interpreter.sh
deleted file mode 100755
index 73df75d70..000000000
--- a/src/Specific/solinas64_2e243m9_6limbs/py_interpreter.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-/usr/bin/env python3 "$@" -Dq='2**243 - 9' -Dmodulus_bytes='40.5' -Da24='121665'
-- 
cgit v1.2.3