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, 165 insertions, 0 deletions

diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
new file mode 100644
index 000000000..4e30313d9
--- /dev/null
+++ b/src/Experiments/SpecEd25519.v
@@ -0,0 +1,165 @@
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
+Require Import Crypto.Spec.ModularWordEncoding.
+Require Import Crypto.Encoding.ModularWordEncodingTheorems.
+Require Import Crypto.Spec.EdDSA.
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
+Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil.
+Require Import Bedrock.Word.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Coq.Logic.Decidable.
+Require Import Coq.omega.Omega.
+
+Local Open Scope nat_scope.
+Definition q : Z := (2 ^ 255 - 19)%Z.
+Global Instance prime_q : prime q. Admitted.
+Lemma two_lt_q : (2 < q)%Z. reflexivity. Qed.
+
+Definition a : F q := opp 1%F.
+
+(* TODO (jadep) : make the proofs about a and d more general *)
+Lemma nonzero_a : a <> 0%F.
+Proof.
+  unfold a.
+  intro eq_opp1_0.
+  apply (@Fq_1_neq_0 q prime_q).
+  rewrite <- (F_opp_spec 1%F).
+  rewrite eq_opp1_0.
+  symmetry; apply F_add_0_r.
+Qed.
+
+Ltac q_bound := pose proof two_lt_q; omega.
+Lemma square_a : isSquare a.
+Proof.
+  Lemma q_1mod4 : (q mod 4 = 1)%Z. reflexivity. Qed.
+  intros.
+  pose proof (minus1_square_1mod4 q prime_q q_1mod4) as minus1_square.
+  destruct minus1_square as [b b_id].
+  apply square_Zmod_F.
+  exists b; rewrite b_id.
+  unfold a.
+  rewrite opp_ZToField.
+  rewrite FieldToZ_ZToField.
+  rewrite Z.mod_small; q_bound.
+Qed.
+
+Hint Rewrite
+ @FieldToZ_add
+ @FieldToZ_mul
+ @FieldToZ_opp
+ @FieldToZ_inv_efficient
+ @FieldToZ_pow_efficient
+ @FieldToZ_ZToField
+ @Zmod_mod
+ : ZToField.
+
+Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F.
+Lemma nonsquare_d : forall x, (x^2 <> d)%F.
+  pose proof @euler_criterion_if q prime_q d two_lt_q.
+  match goal with
+    [H: if ?b then ?x else ?y |- ?y ] => replace b with false in H; [exact H|clear H]
+  end.
+  unfold d, div. autorewrite with ZToField; [|eauto using prime_q, two_lt_q..].
+  vm_compute. (* 10s *)
+  exact eq_refl.
+Qed. (* 10s *)
+
+Instance curve25519params : @E.twisted_edwards_params (F q) eq (ZToField 0) (ZToField 1) add mul a d :=
+  {
+    nonzero_a := nonzero_a
+                   (* TODO:port
+    char_gt_2 : ~ Feq (Fadd Fone Fone) Fzero;
+    nonzero_a : ~ Feq a Fzero;
+    nonsquare_d : forall x : F, ~ Feq (Fmul x x) d }
+                    *)
+  }.
+Admitted.
+
+Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = 2 ^ n.
+Admitted.
+
+Definition b := 256.
+Lemma b_valid : (2 ^ (b - 1) > Z.to_nat q)%nat.
+Proof.
+  unfold q, gt.
+  replace (2 ^ (b - 1)) with (Z.to_nat (2 ^ (Z.of_nat (b - 1))))
+    by (rewrite <- two_power_nat_equiv; apply two_power_nat_Z2Nat).
+  rewrite <- Z2Nat.inj_lt; compute; congruence.
+Qed.
+
+Definition c := 3.
+Lemma c_valid : c = 2 \/ c = 3.
+Proof.
+  right; auto.
+Qed.
+
+Definition n := b - 2.
+Lemma n_ge_c : n >= c.
+Proof.
+  unfold n, c, b; omega.
+Qed.
+Lemma n_le_b : n <= b.
+Proof.
+  unfold n, b; omega.
+Qed.
+
+Definition l : nat := Z.to_nat (252 + 27742317777372353535851937790883648493)%Z.
+Lemma prime_l : prime (Z.of_nat l). Admitted.
+Lemma l_odd : l > 2.
+Proof.
+  unfold l, proj1_sig.
+  rewrite Z2Nat.inj_add; try omega.
+  apply lt_plus_trans.
+  compute; omega.
+Qed.
+
+Require Import Crypto.Spec.Encoding.
+
+Lemma q_pos : (0 < q)%Z. q_bound. Qed.
+Definition FqEncoding : canonical encoding of (F q) as word (b-1) :=
+  @modular_word_encoding q (b - 1) q_pos b_valid.
+
+Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed.
+Lemma l_bound : Z.to_nat (Z.of_nat l) < 2 ^ b.
+Proof.
+  rewrite Nat2Z.id.
+  rewrite <- pow2_id.
+  rewrite Zpow_pow2.
+  unfold l.
+  apply Z2Nat.inj_lt; compute; congruence.
+Qed.
+Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b :=
+  @modular_word_encoding (Z.of_nat l) b l_pos l_bound.
+
+Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed.
+
+Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F.
+Proof.
+  apply F_eq.
+  autorewrite with ZToField.
+  vm_compute.
+  reflexivity.
+Qed.
+
+Local Notation point := (@E.point (F q) eq (ZToField 1) add mul a d).
+Local Notation zero := (E.zero(H:=field_modulo)).
+Local Notation add := (E.add(H0:=curve25519params)).
+Local Infix "*" := (E.mul(H0:=curve25519params)).
+Axiom H : forall n : nat, word n -> word (b + b).
+Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *)
+Axiom B_nonzero : B <> zero.
+Axiom l_order_B : l * B = zero.
+Axiom point_encoding : canonical encoding of point as word b.
+Axiom scalar_encoding : canonical encoding of {n : nat | n < l} as word b.
+
+Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B point_encoding scalar_encoding :=
+  {
+    EdDSA_c_valid := c_valid;
+    EdDSA_n_ge_c := n_ge_c;
+    EdDSA_n_le_b := n_le_b;
+    EdDSA_B_not_identity := B_nonzero;
+    EdDSA_l_prime := prime_l;
+    EdDSA_l_odd := l_odd;
+    EdDSA_l_order_B := l_order_B
+  }.
\ No newline at end of file