1 files changed, 0 insertions, 74 deletions
diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/CurveParameters.v b/src/Specific/solinas64_2e255m19_5limbs_donna/CurveParameters.v
deleted file mode 100644
index e128a8a09..000000000
--- a/src/Specific/solinas64_2e255m19_5limbs_donna/CurveParameters.v
+++ /dev/null
@@ -1,74 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^255 - 19
-Base: 51
-***)
-
-Definition curve : CurveParameters :=
-  {|
-    sz := 5%nat;
-    base := 51;
-    bitwidth := 64;
-    s := 2^255;
-    c := [(1, 19)];
-    carry_chains := Some [seq 0 (pred 5); [0; 1]]%nat;
-
-    a24 := None;
-    coef_div_modulus := Some 2%nat;
-
-    goldilocks := None;
-    karatsuba := None;
-    montgomery := false;
-    freeze := Some true;
-    ladderstep := false;
-
-    mul_code := Some (fun a b =>
-      (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(r4, r3, r2, r1, r0) := a in
-      let '(s4, s3, s2, s1, s0) := b in
-      dlet t0  :=  r0 * s0 in
-      dlet t1  :=  r0 * s1 + r1 * s0 in
-      dlet t2  :=  r0 * s2 + r2 * s0 + r1 * s1 in
-      dlet t3  :=  r0 * s3 + r3 * s0 + r1 * s2 + r2 * s1 in
-      dlet t4  :=  r0 * s4 + r4 * s0 + r3 * s1 + r1 * s3 + r2 * s2 in
-
-      dlet r4 := r4 * 19 in
-      dlet r1 := r1 * 19 in
-      dlet r2 := r2 * 19 in
-      dlet r3 := r3 * 19 in
-
-      dlet t0 := t0 + r4 * s1 + r1 * s4 + r2 * s3 + r3 * s2 in
-      dlet t1 := t1 + r4 * s2 + r2 * s4 + r3 * s3 in
-      dlet t2 := t2 + r4 * s3 + r3 * s4 in
-      dlet t3 := t3 + r4 * s4 in
-      (t4, t3, t2, t1, t0)
-            );
-
-    square_code := Some (fun a =>
-      (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(r4, r3, r2, r1, r0) := a in
-      dlet d0 := r0 * 2 in
-      dlet d1 := r1 * 2 in
-      dlet d2 := r2 * 2 * 19 in
-      dlet d419 := r4 * 19 in
-      dlet d4 := d419 * 2 in
-
-      dlet t0 := r0 * r0 + d4 * r1 + (d2 * (r3     )) in
-      dlet t1 := d0 * r1 + d4 * r2 + (r3 * (r3 * 19)) in
-      dlet t2 := d0 * r2 + r1 * r1 + (d4 * (r3     )) in
-      dlet t3 := d0 * r3 + d1 * r2 + (r4 * (d419   )) in
-      dlet t4 := d0 * r4 + d1 * r3 + (r2 * (r2     )) in
-      (t4, t3, t2, t1, t0)
-            );
-
-    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.