ed25519 spec: small cleanup

1 files changed, 35 insertions, 57 deletions

diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index 9ecb06f2f..f107e4497 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -11,42 +11,15 @@ 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.
-
-Lemma nonzero_a : a <> 0%F. Proof. rewrite F_eq; compute; discriminate. Qed.
-
-Ltac q_bound := pose proof two_lt_q; omega.
-Lemma square_a : isSquare a.
-Proof.
-  assert (q_1mod4 : (q mod 4 = 1)%Z) by abstract reflexivity.
-  intros.
-  pose proof (minus1_square_1mod4 q prime_q q_1mod4) as minus1_square.
-  destruct minus1_square as [b b_id].
+(* TODO: move to PrimeFieldTheorems *)
+Lemma minus1_is_square {q} :  prime q -> (q mod 4)%Z = 1%Z -> isSquare (opp 1 : F q)%F.
+  intros; pose proof prime_ge_2 q _.
   apply square_Zmod_F.
+  destruct (minus1_square_1mod4 q) as [b b_id]; trivial.
   exists b; rewrite b_id.
-  unfold a.
-  rewrite opp_ZToField.
-  rewrite FieldToZ_ZToField.
-  rewrite Z.mod_small; q_bound.
+  rewrite opp_ZToField, !FieldToZ_ZToField, !Z.mod_small; omega.
 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 euler_criterion_nonsquare {q} (prime_q:prime q) (two_lt_q:(2<q)%Z) (d:F q) : 
   ((d =? 0)%Z || (Pre.powmod q d (Z.to_N (q / 2)) =? 1)%Z)%bool = false -> 
    forall x : F q, (x ^ 2)%F <> d.
@@ -55,52 +28,62 @@ Proof.
     break_if; intros; try discriminate; eauto.
 Qed.
 
-Lemma nonsquare_d : forall x, (x^2 <> d)%F.
+Definition q : Z := (2 ^ 255 - 19)%Z.
+Global Instance prime_q : prime q. Admitted.
+Lemma two_lt_q : (2 < q)%Z. Proof. reflexivity. Qed.
+Lemma char_gt_2 : (1 + 1 <> (0:F q))%F. Proof. rewrite F_eq; compute; discriminate. Qed.
+
+Definition a : F q := opp 1%F.
+Lemma nonzero_a : a <> 0%F. Proof. rewrite F_eq; compute; discriminate. Qed.
+Lemma square_a : exists b, (b*b=a)%F.
+Proof. setoid_rewrite <-F_pow_2_r. apply (minus1_is_square _); reflexivity. Qed.
+
+Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F.
+Lemma nonsquare_d : forall x, (x*x <> d)%F.
+Proof.
+  intros; rewrite <-F_pow_2_r.
   apply (euler_criterion_nonsquare prime_q two_lt_q); vm_cast_no_check (eq_refl false).
 Qed. (* 3s *)
 
 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 }
-                    *)
+    nonzero_a := nonzero_a;
+    char_gt_2 := char_gt_2;
+    square_a := square_a;
+    nonsquare_d := nonsquare_d
   }.
-Admitted.
 
-Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = 2 ^ n.
+Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = (2 ^ n)%nat.
 Admitted.
 
-Definition b := 256.
+Definition b := 256%nat.
 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))))
+  replace (2 ^ (b - 1))%nat 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.
+Definition c := 3%nat.
+Lemma c_valid : (c = 2 \/ c = 3)%nat.
 Proof.
   right; auto.
 Qed.
 
-Definition n := b - 2.
-Lemma n_ge_c : n >= c.
+Definition n := (b - 2)%nat.
+Lemma n_ge_c : (n >= c)%nat.
 Proof.
   unfold n, c, b; omega.
 Qed.
-Lemma n_le_b : n <= b.
+Lemma n_le_b : (n <= b)%nat.
 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.
+Lemma l_odd : (l > 2)%nat.
 Proof.
   unfold l, proj1_sig.
   rewrite Z2Nat.inj_add; try omega.
@@ -110,12 +93,12 @@ Qed.
 
 Require Import Crypto.Spec.Encoding.
 
-Lemma q_pos : (0 < q)%Z. q_bound. Qed.
+Lemma q_pos : (0 < q)%Z. pose proof prime_ge_2 q _; omega. 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.
+Lemma l_bound : (Z.to_nat (Z.of_nat l) < 2 ^ b)%nat.
 Proof.
   rewrite Nat2Z.id.
   rewrite <- pow2_id.
@@ -129,12 +112,7 @@ Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b :=
 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.
+Proof. apply F_eq; 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)).