From 918d8707fac5c087565972c93ce2c9c79d4f7b61 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 21 Jul 2016 09:49:44 -0400 Subject: ed25519 spec: small cleanup --- src/Experiments/SpecEd25519.v | 92 ++++++++++++++++--------------------------- 1 file changed, 35 insertions(+), 57 deletions(-) (limited to 'src') 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 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)). -- cgit v1.2.3