1 files changed, 0 insertions, 58 deletions
diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v
deleted file mode 100644
index 8474a05c9..000000000
--- a/src/Specific/IntegrationTestKaratsubaMul.v
+++ /dev/null
@@ -1,58 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.Karatsuba.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Import ListNotations.
-
-Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
-
-Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
-
-  Local Notation b_of exp := {| lower := 0 ; upper := 2^exp + 2^(exp-3) |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition mul :
-    { mul : feBW -> feBW -> feBW
-    | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
-  Proof.
-    start_preglue.
-    do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
-    all:fin_preglue.
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively.
-    (*Show Ltac Profile.*)
-  Time Defined.
-
-End BoundedField25p5.