new autogenerated files

26 files changed, 0 insertions, 338 deletions

diff --git a/src/Specific/montgomery64_2e127m1/CurveParameters.v b/src/Specific/montgomery64_2e127m1/CurveParameters.v
deleted file mode 100644
index fb2a5146e..000000000
--- a/src/Specific/montgomery64_2e127m1/CurveParameters.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^127 - 1
-Base: 64
-***)
-
-Definition curve : CurveParameters :=
-  {|
-    sz := 2%nat;
-    base := 64;
-    bitwidth := 64;
-    s := 2^127;
-    c := [(1, 1)];
-    carry_chains := None;
-
-    a24 := None;
-    coef_div_modulus := None;
-
-    goldilocks := None;
-    karatsuba := None;
-    montgomery := true;
-    freeze := Some false;
-    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/montgomery64_2e127m1/Synthesis.v b/src/Specific/montgomery64_2e127m1/Synthesis.v
deleted file mode 100644
index 19135e306..000000000
--- a/src/Specific/montgomery64_2e127m1/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.montgomery64_2e127m1.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/montgomery64_2e127m1/compiler.sh b/src/Specific/montgomery64_2e127m1/compiler.sh
deleted file mode 100755
index 0cd0a7d9a..000000000
--- a/src/Specific/montgomery64_2e127m1/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,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{64,64}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='16' -Dmodulus_limbs='2' -Dq_mpz='(1_mpz<<127) - 1' "$@"
diff --git a/src/Specific/montgomery64_2e127m1/compilerxx.sh b/src/Specific/montgomery64_2e127m1/compilerxx.sh
deleted file mode 100755
index 19dfd153a..000000000
--- a/src/Specific/montgomery64_2e127m1/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,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{64,64}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='16' -Dmodulus_limbs='2' -Dq_mpz='(1_mpz<<127) - 1' "$@"
diff --git a/src/Specific/montgomery64_2e127m1/feadd.c b/src/Specific/montgomery64_2e127m1/feadd.c
deleted file mode 100644
index 91fa60600..000000000
--- a/src/Specific/montgomery64_2e127m1/feadd.c
+++ /dev/null
@@ -1,16 +0,0 @@
-static void feadd(uint64_t out[2], const uint64_t in1[2], const uint64_t in2[2]) {
-  { const uint64_t x4 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x6 = in2[1];
-  { const uint64_t x7 = in2[0];
-  { uint64_t x9; uint8_t x10 = _addcarryx_u64(0x0, x5, x7, &x9);
-  { uint64_t x12; uint8_t x13 = _addcarryx_u64(x10, x4, x6, &x12);
-  { uint64_t x15; uint8_t x16 = _subborrow_u64(0x0, x9, 0xffffffffffffffffL, &x15);
-  { uint64_t x18; uint8_t x19 = _subborrow_u64(x16, x12, 0x7fffffffffffffffL, &x18);
-  { uint64_t _; uint8_t x22 = _subborrow_u64(x19, x13, 0x0, &_);
-  { uint64_t x23 = cmovznz64(x22, x18, x12);
-  { uint64_t x24 = cmovznz64(x22, x15, x9);
-  out[0] = x24;
-  out[1] = x23;
-  }}}}}}}}}}}
-}
diff --git a/src/Specific/montgomery64_2e127m1/feadd.v b/src/Specific/montgomery64_2e127m1/feadd.v
deleted file mode 100644
index c01f323bd..000000000
--- a/src/Specific/montgomery64_2e127m1/feadd.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.montgomery64_2e127m1.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition add :
-  { add : feBW_small -> feBW_small -> feBW_small
-  | forall a b, phiM_small (add a b) = F.add (phiM_small a) (phiM_small b) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_add ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions add.
diff --git a/src/Specific/montgomery64_2e127m1/feaddDisplay.log b/src/Specific/montgomery64_2e127m1/feaddDisplay.log
deleted file mode 100644
index a47056f6b..000000000
--- a/src/Specific/montgomery64_2e127m1/feaddDisplay.log
+++ /dev/null
@@ -1,14 +0,0 @@
-λ x x0 : word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x4, x5, (x6, x7))%core,
- uint64_t x9, uint8_t x10 = addcarryx_u64(0x0, x5, x7);
- uint64_t x12, uint8_t x13 = addcarryx_u64(x10, x4, x6);
- uint64_t x15, uint8_t x16 = subborrow_u64(0x0, x9, 0xffffffffffffffffL);
- uint64_t x18, uint8_t x19 = subborrow_u64(x16, x12, 0x7fffffffffffffffL);
- uint64_t _, uint8_t x22 = subborrow_u64(x19, x13, 0x0);
- uint64_t x23 = cmovznz64(x22, x18, x12);
- uint64_t x24 = cmovznz64(x22, x15, x9);
- return (x23, x24))
-(x, x0)%core
-     : word64 * word64 → word64 * word64 → ReturnType (uint64_t * uint64_t)
diff --git a/src/Specific/montgomery64_2e127m1/feaddDisplay.v b/src/Specific/montgomery64_2e127m1/feaddDisplay.v
deleted file mode 100644
index acc8bea07..000000000
--- a/src/Specific/montgomery64_2e127m1/feaddDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.montgomery64_2e127m1.feadd.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display add.
diff --git a/src/Specific/montgomery64_2e127m1/femul.c b/src/Specific/montgomery64_2e127m1/femul.c
deleted file mode 100644
index c6f5ef6fb..000000000
--- a/src/Specific/montgomery64_2e127m1/femul.c
+++ /dev/null
@@ -1,40 +0,0 @@
-static void femul(uint64_t out[2], const uint64_t in1[2], const uint64_t in2[2]) {
-  { const uint64_t x4 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x6 = in2[1];
-  { const uint64_t x7 = in2[0];
-  { uint64_t x10;  uint64_t x9 = _mulx_u64(x5, x7, &x10);
-  { uint64_t x13;  uint64_t x12 = _mulx_u64(x5, x6, &x13);
-  { uint64_t x15; uint8_t x16 = _addcarryx_u64(0x0, x10, x12, &x15);
-  { uint64_t x18; uint8_t _ = _addcarryx_u64(0x0, x16, x13, &x18);
-  { uint64_t x22;  uint64_t x21 = _mulx_u64(x9, 0xffffffffffffffffL, &x22);
-  { uint64_t x25;  uint64_t x24 = _mulx_u64(x9, 0x7fffffffffffffffL, &x25);
-  { uint64_t x27; uint8_t x28 = _addcarryx_u64(0x0, x22, x24, &x27);
-  { uint64_t x30; uint8_t _ = _addcarryx_u64(0x0, x28, x25, &x30);
-  { uint64_t _; uint8_t x34 = _addcarryx_u64(0x0, x9, x21, &_);
-  { uint64_t x36; uint8_t x37 = _addcarryx_u64(x34, x15, x27, &x36);
-  { uint64_t x39; uint8_t x40 = _addcarryx_u64(x37, x18, x30, &x39);
-  { uint64_t x43;  uint64_t x42 = _mulx_u64(x4, x7, &x43);
-  { uint64_t x46;  uint64_t x45 = _mulx_u64(x4, x6, &x46);
-  { uint64_t x48; uint8_t x49 = _addcarryx_u64(0x0, x43, x45, &x48);
-  { uint64_t x51; uint8_t _ = _addcarryx_u64(0x0, x49, x46, &x51);
-  { uint64_t x54; uint8_t x55 = _addcarryx_u64(0x0, x36, x42, &x54);
-  { uint64_t x57; uint8_t x58 = _addcarryx_u64(x55, x39, x48, &x57);
-  { uint64_t x60; uint8_t x61 = _addcarryx_u64(x58, x40, x51, &x60);
-  { uint64_t x64;  uint64_t x63 = _mulx_u64(x54, 0xffffffffffffffffL, &x64);
-  { uint64_t x67;  uint64_t x66 = _mulx_u64(x54, 0x7fffffffffffffffL, &x67);
-  { uint64_t x69; uint8_t x70 = _addcarryx_u64(0x0, x64, x66, &x69);
-  { uint64_t x72; uint8_t _ = _addcarryx_u64(0x0, x70, x67, &x72);
-  { uint64_t _; uint8_t x76 = _addcarryx_u64(0x0, x54, x63, &_);
-  { uint64_t x78; uint8_t x79 = _addcarryx_u64(x76, x57, x69, &x78);
-  { uint64_t x81; uint8_t x82 = _addcarryx_u64(x79, x60, x72, &x81);
-  { uint8_t x83 = (x82 + x61);
-  { uint64_t x85; uint8_t x86 = _subborrow_u64(0x0, x78, 0xffffffffffffffffL, &x85);
-  { uint64_t x88; uint8_t x89 = _subborrow_u64(x86, x81, 0x7fffffffffffffffL, &x88);
-  { uint64_t _; uint8_t x92 = _subborrow_u64(x89, x83, 0x0, &_);
-  { uint64_t x93 = cmovznz64(x92, x88, x81);
-  { uint64_t x94 = cmovznz64(x92, x85, x78);
-  out[0] = x94;
-  out[1] = x93;
-  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/montgomery64_2e127m1/femul.v b/src/Specific/montgomery64_2e127m1/femul.v
deleted file mode 100644
index db33b1ad3..000000000
--- a/src/Specific/montgomery64_2e127m1/femul.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.montgomery64_2e127m1.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition mul :
-  { mul : feBW_small -> feBW_small -> feBW_small
-  | forall a b, phiM_small (mul a b) = F.mul (phiM_small a) (phiM_small b) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_mul ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions mul.
diff --git a/src/Specific/montgomery64_2e127m1/femulDisplay.log b/src/Specific/montgomery64_2e127m1/femulDisplay.log
deleted file mode 100644
index ea19e6486..000000000
--- a/src/Specific/montgomery64_2e127m1/femulDisplay.log
+++ /dev/null
@@ -1,38 +0,0 @@
-λ x x0 : word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x4, x5, (x6, x7))%core,
- uint64_t x9, uint64_t x10 = mulx_u64(x5, x7);
- uint64_t x12, uint64_t x13 = mulx_u64(x5, x6);
- uint64_t x15, uint8_t x16 = addcarryx_u64(0x0, x10, x12);
- uint64_t x18, uint8_t _ = addcarryx_u64(0x0, x16, x13);
- uint64_t x21, uint64_t x22 = mulx_u64(x9, 0xffffffffffffffffL);
- uint64_t x24, uint64_t x25 = mulx_u64(x9, 0x7fffffffffffffffL);
- uint64_t x27, uint8_t x28 = addcarryx_u64(0x0, x22, x24);
- uint64_t x30, uint8_t _ = addcarryx_u64(0x0, x28, x25);
- uint64_t _, uint8_t x34 = addcarryx_u64(0x0, x9, x21);
- uint64_t x36, uint8_t x37 = addcarryx_u64(x34, x15, x27);
- uint64_t x39, uint8_t x40 = addcarryx_u64(x37, x18, x30);
- uint64_t x42, uint64_t x43 = mulx_u64(x4, x7);
- uint64_t x45, uint64_t x46 = mulx_u64(x4, x6);
- uint64_t x48, uint8_t x49 = addcarryx_u64(0x0, x43, x45);
- uint64_t x51, uint8_t _ = addcarryx_u64(0x0, x49, x46);
- uint64_t x54, uint8_t x55 = addcarryx_u64(0x0, x36, x42);
- uint64_t x57, uint8_t x58 = addcarryx_u64(x55, x39, x48);
- uint64_t x60, uint8_t x61 = addcarryx_u64(x58, x40, x51);
- uint64_t x63, uint64_t x64 = mulx_u64(x54, 0xffffffffffffffffL);
- uint64_t x66, uint64_t x67 = mulx_u64(x54, 0x7fffffffffffffffL);
- uint64_t x69, uint8_t x70 = addcarryx_u64(0x0, x64, x66);
- uint64_t x72, uint8_t _ = addcarryx_u64(0x0, x70, x67);
- uint64_t _, uint8_t x76 = addcarryx_u64(0x0, x54, x63);
- uint64_t x78, uint8_t x79 = addcarryx_u64(x76, x57, x69);
- uint64_t x81, uint8_t x82 = addcarryx_u64(x79, x60, x72);
- uint8_t x83 = (x82 + x61);
- uint64_t x85, uint8_t x86 = subborrow_u64(0x0, x78, 0xffffffffffffffffL);
- uint64_t x88, uint8_t x89 = subborrow_u64(x86, x81, 0x7fffffffffffffffL);
- uint64_t _, uint8_t x92 = subborrow_u64(x89, x83, 0x0);
- uint64_t x93 = cmovznz64(x92, x88, x81);
- uint64_t x94 = cmovznz64(x92, x85, x78);
- return (x93, x94))
-(x, x0)%core
-     : word64 * word64 → word64 * word64 → ReturnType (uint64_t * uint64_t)
diff --git a/src/Specific/montgomery64_2e127m1/femulDisplay.v b/src/Specific/montgomery64_2e127m1/femulDisplay.v
deleted file mode 100644
index 000d6ced6..000000000
--- a/src/Specific/montgomery64_2e127m1/femulDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.montgomery64_2e127m1.femul.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display mul.
diff --git a/src/Specific/montgomery64_2e127m1/fenz.c b/src/Specific/montgomery64_2e127m1/fenz.c
deleted file mode 100644
index 3b61c77b8..000000000
--- a/src/Specific/montgomery64_2e127m1/fenz.c
+++ /dev/null
@@ -1,7 +0,0 @@
-static void fenz(ReturnType uint64_t out[1], const uint64_t in1[2]) {
-  { const uint64_t x1 = in1[1];
-  { const uint64_t x2 = in1[0];
-  { uint64_t x3 = (x2 | x1);
-  out[0] = x3;
-  }}}
-}
diff --git a/src/Specific/montgomery64_2e127m1/fenz.v b/src/Specific/montgomery64_2e127m1/fenz.v
deleted file mode 100644
index 74a25c2db..000000000
--- a/src/Specific/montgomery64_2e127m1/fenz.v
+++ /dev/null
@@ -1,16 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.montgomery64_2e127m1.Synthesis.
-Local Open Scope Z_scope.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition nonzero :
-  { nonzero : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1
-  | forall a, (BoundedWord.BoundedWordToZ _ _ _ (nonzero a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_nonzero ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions nonzero.
diff --git a/src/Specific/montgomery64_2e127m1/fenzDisplay.log b/src/Specific/montgomery64_2e127m1/fenzDisplay.log
deleted file mode 100644
index 42367b877..000000000
--- a/src/Specific/montgomery64_2e127m1/fenzDisplay.log
+++ /dev/null
@@ -1,8 +0,0 @@
-λ x : word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x1, x2)%core,
- uint64_t x3 = (x2 | x1);
- return x3)
-x
-     : word64 * word64 → ReturnType uint64_t
diff --git a/src/Specific/montgomery64_2e127m1/fenzDisplay.v b/src/Specific/montgomery64_2e127m1/fenzDisplay.v
deleted file mode 100644
index 3645a8a57..000000000
--- a/src/Specific/montgomery64_2e127m1/fenzDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.montgomery64_2e127m1.fenz.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display nonzero.
diff --git a/src/Specific/montgomery64_2e127m1/feopp.c b/src/Specific/montgomery64_2e127m1/feopp.c
deleted file mode 100644
index 2982fec31..000000000
--- a/src/Specific/montgomery64_2e127m1/feopp.c
+++ /dev/null
@@ -1,14 +0,0 @@
-static void feopp(uint64_t out[2], const uint64_t in1[2]) {
-  { const uint64_t x1 = in1[1];
-  { const uint64_t x2 = in1[0];
-  { uint64_t x4; uint8_t x5 = _subborrow_u64(0x0, 0x0, x2, &x4);
-  { uint64_t x7; uint8_t x8 = _subborrow_u64(x5, 0x0, x1, &x7);
-  { uint64_t x9 = cmovznz64(x8, 0x0, 0xffffffffffffffffL);
-  { uint64_t x10 = (x9 & 0xffffffffffffffffL);
-  { uint64_t x12; uint8_t x13 = _addcarryx_u64(0x0, x4, x10, &x12);
-  { uint64_t x14 = (x9 & 0x7fffffffffffffffL);
-  { uint64_t x16; uint8_t _ = _addcarryx_u64(x13, x7, x14, &x16);
-  out[0] = x12;
-  out[1] = x16;
-  }}}}}}}}}
-}
diff --git a/src/Specific/montgomery64_2e127m1/feopp.v b/src/Specific/montgomery64_2e127m1/feopp.v
deleted file mode 100644
index 8c13a7efb..000000000
--- a/src/Specific/montgomery64_2e127m1/feopp.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.montgomery64_2e127m1.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition opp :
-  { opp : feBW_small -> feBW_small
-  | forall a, phiM_small (opp a) = F.opp (phiM_small a) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_opp ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions opp.
diff --git a/src/Specific/montgomery64_2e127m1/feoppDisplay.log b/src/Specific/montgomery64_2e127m1/feoppDisplay.log
deleted file mode 100644
index 2e861c851..000000000
--- a/src/Specific/montgomery64_2e127m1/feoppDisplay.log
+++ /dev/null
@@ -1,14 +0,0 @@
-λ x : word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x1, x2)%core,
- uint64_t x4, uint8_t x5 = subborrow_u64(0x0, 0x0, x2);
- uint64_t x7, uint8_t x8 = subborrow_u64(x5, 0x0, x1);
- uint64_t x9 = cmovznz64(x8, 0x0, 0xffffffffffffffffL);
- uint64_t x10 = (x9 & 0xffffffffffffffffL);
- uint64_t x12, uint8_t x13 = addcarryx_u64(0x0, x4, x10);
- uint64_t x14 = (x9 & 0x7fffffffffffffffL);
- uint64_t x16, uint8_t _ = addcarryx_u64(x13, x7, x14);
- (Return x16, Return x12))
-x
-     : word64 * word64 → ReturnType (uint64_t * uint64_t)
diff --git a/src/Specific/montgomery64_2e127m1/feoppDisplay.v b/src/Specific/montgomery64_2e127m1/feoppDisplay.v
deleted file mode 100644
index 752ff2ec7..000000000
--- a/src/Specific/montgomery64_2e127m1/feoppDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.montgomery64_2e127m1.feopp.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display opp.
diff --git a/src/Specific/montgomery64_2e127m1/fesquare.c b/src/Specific/montgomery64_2e127m1/fesquare.c
deleted file mode 100644
index 7bd8db166..000000000
--- a/src/Specific/montgomery64_2e127m1/fesquare.c
+++ /dev/null
@@ -1,5 +0,0 @@
-/* WARNING: This file was copied from Specific/CurveParameters/montgomery64/fesquare.c.
- If you edit it here, changes will be erased the next time remake_curves.sh is run. */
-static void fesquare(uint64_t *out, const uint64_t *in) {
-  femul(out, in, in);
-}
diff --git a/src/Specific/montgomery64_2e127m1/fesub.c b/src/Specific/montgomery64_2e127m1/fesub.c
deleted file mode 100644
index 45bb624d9..000000000
--- a/src/Specific/montgomery64_2e127m1/fesub.c
+++ /dev/null
@@ -1,16 +0,0 @@
-static void fesub(uint64_t out[2], const uint64_t in1[2], const uint64_t in2[2]) {
-  { const uint64_t x4 = in1[1];
-  { const uint64_t x5 = in1[0];
-  { const uint64_t x6 = in2[1];
-  { const uint64_t x7 = in2[0];
-  { uint64_t x9; uint8_t x10 = _subborrow_u64(0x0, x5, x7, &x9);
-  { uint64_t x12; uint8_t x13 = _subborrow_u64(x10, x4, x6, &x12);
-  { uint64_t x14 = cmovznz64(x13, 0x0, 0xffffffffffffffffL);
-  { uint64_t x15 = (x14 & 0xffffffffffffffffL);
-  { uint64_t x17; uint8_t x18 = _addcarryx_u64(0x0, x9, x15, &x17);
-  { uint64_t x19 = (x14 & 0x7fffffffffffffffL);
-  { uint64_t x21; uint8_t _ = _addcarryx_u64(x18, x12, x19, &x21);
-  out[0] = x17;
-  out[1] = x21;
-  }}}}}}}}}}}
-}
diff --git a/src/Specific/montgomery64_2e127m1/fesub.v b/src/Specific/montgomery64_2e127m1/fesub.v
deleted file mode 100644
index 09945c747..000000000
--- a/src/Specific/montgomery64_2e127m1/fesub.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.montgomery64_2e127m1.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition sub :
-  { sub : feBW_small -> feBW_small -> feBW_small
-  | forall a b, phiM_small (sub a b) = F.sub (phiM_small a) (phiM_small b) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_sub ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions sub.
diff --git a/src/Specific/montgomery64_2e127m1/fesubDisplay.log b/src/Specific/montgomery64_2e127m1/fesubDisplay.log
deleted file mode 100644
index ec41671f0..000000000
--- a/src/Specific/montgomery64_2e127m1/fesubDisplay.log
+++ /dev/null
@@ -1,14 +0,0 @@
-λ x x0 : word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x4, x5, (x6, x7))%core,
- uint64_t x9, uint8_t x10 = subborrow_u64(0x0, x5, x7);
- uint64_t x12, uint8_t x13 = subborrow_u64(x10, x4, x6);
- uint64_t x14 = cmovznz64(x13, 0x0, 0xffffffffffffffffL);
- uint64_t x15 = (x14 & 0xffffffffffffffffL);
- uint64_t x17, uint8_t x18 = addcarryx_u64(0x0, x9, x15);
- uint64_t x19 = (x14 & 0x7fffffffffffffffL);
- uint64_t x21, uint8_t _ = addcarryx_u64(x18, x12, x19);
- (Return x21, Return x17))
-(x, x0)%core
-     : word64 * word64 → word64 * word64 → ReturnType (uint64_t * uint64_t)
diff --git a/src/Specific/montgomery64_2e127m1/fesubDisplay.v b/src/Specific/montgomery64_2e127m1/fesubDisplay.v
deleted file mode 100644
index 91308f964..000000000
--- a/src/Specific/montgomery64_2e127m1/fesubDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.montgomery64_2e127m1.fesub.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display sub.
diff --git a/src/Specific/montgomery64_2e127m1/py_interpreter.sh b/src/Specific/montgomery64_2e127m1/py_interpreter.sh
deleted file mode 100755
index 83c4398b2..000000000
--- a/src/Specific/montgomery64_2e127m1/py_interpreter.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-/usr/bin/env python3 "$@" -Dq='2**127 - 1' -Dmodulus_bytes='64' -Da24='121665'