Remove anything incompatible with new algebraic hierarcy

- PointEncoding (these will hopefully come back soon)
- EdDSAProofs (not a priority to bring back, but not hard either)
- Ed25519 spec bits and pieces which were not finished anyway

1 files changed, 0 insertions, 30 deletions

diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v
deleted file mode 100644
index 50027349d..000000000
--- a/src/CompleteEdwardsCurve/DoubleAndAdd.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Util.IterAssocOp.
-Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith.
-
-Section EdwardsDoubleAndAdd.
-  Context {prm:TwistedEdwardsParams}.
-  Definition doubleAndAdd (bound n : nat) (P : E.point) : E.point :=
-    iter_op E.add E.zero N.testbit_nat (N.of_nat n) P bound.
-
-  Lemma scalarMult_double : forall n P, E.mul (n + n) P = E.mul n (P + P)%E.
-  Proof.
-    intros.
-    replace (n + n)%nat with (n * 2)%nat by omega.
-    induction n; simpl; auto.
-    rewrite E.add_assoc.
-    f_equal; auto.
-  Qed.
-
-  Lemma doubleAndAdd_spec : forall bound n P, N.size_nat (N.of_nat n) <= bound ->
-    E.mul n P = doubleAndAdd bound n P.
-  Proof.
-    induction n; auto; intros; unfold doubleAndAdd;
-      rewrite iter_op_spec with (scToN := fun x => x); (
-        unfold Morphisms.Proper, Morphisms.respectful, Equivalence.equiv;
-        intros; subst; try rewrite Nat2N.id;
-        reflexivity || assumption || apply E.add_assoc
-        || rewrite E.add_comm; apply E.add_0_r).
-  Qed.
-End EdwardsDoubleAndAdd.
\ No newline at end of file