From a5caf332df39f57bf25829cf5c127aa54fb8d3e4 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 20 Jul 2016 15:35:01 -0400 Subject: experiments wd25519: simplify proof for a --- src/Experiments/SpecEd25519.v | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) (limited to 'src') diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index 30d8ce13d..111aaff0b 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -18,16 +18,7 @@ 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. +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. -- cgit v1.2.3 From d7f30db5fe04b11fa22a3b3b79eb0e63a72cb0f1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 20 Jul 2016 18:33:02 -0400 Subject: compute on [F q]! --- src/Experiments/SpecEd25519.v | 19 +-- src/ModularArithmetic/ModularArithmeticTheorems.v | 38 +++-- src/ModularArithmetic/Pre.v | 160 ++++++---------------- src/ModularArithmetic/PrimeFieldTheorems.v | 4 +- src/Spec/ModularArithmetic.v | 17 +-- 5 files changed, 82 insertions(+), 156 deletions(-) (limited to 'src') diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index 111aaff0b..9ecb06f2f 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -46,15 +46,18 @@ Hint Rewrite : 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. +Proof. + pose proof @euler_criterion_if q prime_q d two_lt_q; + break_if; intros; try discriminate; eauto. +Qed. + 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 *) + 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 := { diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 951f848bf..a1d47ae8f 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -21,13 +21,6 @@ Section ModularArithmeticPreliminaries. eapply UIP_dec, Z.eq_dec. Qed. - Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0. - intros a. - pose (@opp_with_spec m) as H. - change (@opp m) with (proj1_sig H). - destruct H; eauto. - Qed. - Lemma F_pow_spec : forall (a:F m), pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x). Proof. @@ -85,7 +78,6 @@ end. Ltac Fdefn := intros; - rewrite ?F_opp_spec; repeat match goal with [ x : F _ |- _ ] => destruct x end; try eq_remove_proofs; demod; @@ -155,10 +147,13 @@ Section FandZ. Proof. repeat split; Fdefn; try apply F_eq_dec. { rewrite Z.add_0_r. auto. } - { rewrite <-Z.add_sub_swap, <-Z.add_sub_assoc, Z.sub_diag, Z.add_0_r. apply Z_mod_same_full. } { rewrite Z.mul_1_r. auto. } Qed. + Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0. + Fdefn. + Qed. + Lemma ZToField_0 : @ZToField m 0 = 0. Proof. Fdefn. @@ -270,7 +265,6 @@ Section FandZ. @ZToField m (x - y) = ZToField x - ZToField y. Proof. Fdefn. - apply sub_intersperse_modulus. Qed. (* Compatibility between inject and multiplication *) @@ -412,13 +406,30 @@ Section RingModuloPre. Fdefn; rewrite <-Z.quot_rem'; trivial. Qed. + Lemma Z_mul_mod_modulus_r : forall x m, ((x*m) mod m = 0)%Z. + intros. + rewrite Zmult_mod, Z_mod_same_full. + rewrite Z.mul_0_r, Zmod_0_l. + reflexivity. + Qed. + + Lemma Z_mod_opp_equiv : forall x y m, x mod m = (-y) mod m -> + (-x) mod m = y mod m. + Proof. + intros. + rewrite <-Z.sub_0_l. + rewrite Zminus_mod. rewrite H. + rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal. + destruct y; auto. + Qed. + Lemma Z_opp_opp : forall x : Z, (-(-x)) = x. destruct x; auto. Qed. Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m. intros. - apply Pre.mod_opp_equiv. + apply Z_mod_opp_equiv. rewrite Z_opp_opp. demod; auto. Qed. @@ -437,9 +448,7 @@ Section RingModuloPre. Proof. constructor; intros; try Fdefn; unfold id; try (apply gf_eq; simpl; intuition). - - - apply sub_intersperse_modulus. - - rewrite Zminus_mod, Z_mod_same_full; simpl. apply Z_mod_opp. + - apply Z_mod_opp_equiv; rewrite Z_opp_opp, Zmod_mod; reflexivity. - rewrite (proj1 (Z.eqb_eq x y)); trivial. Qed. @@ -620,6 +629,7 @@ Section VariousModulo. Lemma opp_ZToField : forall x : Z, opp (ZToField x) = @ZToField m (m - x). Proof. Fdefn. + rewrite Zminus_mod, Z_mod_same_full, (Z.sub_0_l (x mod m)); reflexivity. Qed. Lemma F_pow_2_r : forall x : F m, x^2 = x*x. diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index fca5576b7..47a38b867 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -3,6 +3,7 @@ Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Logic.EqdepFacts. Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.omega.Omega. +Require Import Crypto.Util.NumTheoryUtil. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. symmetry. @@ -21,29 +22,6 @@ Proof. eapply UIP_dec, Z.eq_dec. Qed. -Definition opp_impl: - forall {m : BinNums.Z}, - {opp0 : {z : BinNums.Z | z = z mod m} -> {z : BinNums.Z | z = z mod m} | - forall x : {z : BinNums.Z | z = z mod m}, - exist (fun z : BinNums.Z => z = z mod m) - ((proj1_sig x + proj1_sig (opp0 x)) mod m) - (Z_mod_mod (proj1_sig x + proj1_sig (opp0 x)) m) = - exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m)}. - intro m. - refine (exist _ (fun x => exist _ ((m-proj1_sig x) mod m) _) _); intros. - - destruct x; - simpl; - apply exist_reduced_eq; - rewrite Zdiv.Zplus_mod_idemp_r; - replace (x + (m - x)) with m by omega; - apply Zdiv.Z_mod_same_full. - - Grab Existential Variables. - destruct x; simpl. - rewrite Zdiv.Zmod_mod; reflexivity. -Defined. - Definition mulmod m := fun a b => a * b mod m. Definition powmod_pos m := Pos.iter_op (mulmod m). Definition powmod m a x := match x with N0 => 1 mod m | Npos p => powmod_pos m p (a mod m) end. @@ -93,17 +71,18 @@ Proof. rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal. Qed. -Definition pow_impl_sig {m} : {z : Z | z = z mod m} -> N -> {z : Z | z = z mod m}. - intros a x. - exists (powmod m (proj1_sig a) x). - destruct x; [simpl; rewrite Zmod_mod; reflexivity|]. +Local Obligation Tactic := idtac. + +Program Definition pow_impl_sig {m} (a:{z : Z | z = z mod m}) (x:N) : {z : Z | z = z mod m} + := powmod m (proj1_sig a) x. +Next Obligation. + intros; destruct x; [simpl; rewrite Zmod_mod; reflexivity|]. rewrite N_pos_1plus. rewrite powmod_1plus. rewrite Zmod_mod; reflexivity. -Defined. +Qed. -Definition pow_impl: - forall {m : BinNums.Z}, +Program Definition pow_impl {m} : {pow0 : {z : BinNums.Z | z = z mod m} -> BinNums.N -> {z : BinNums.Z | z = z mod m} | @@ -114,85 +93,23 @@ Definition pow_impl: pow0 a (1 + x)%N = exist (fun z : BinNums.Z => z = z mod m) ((proj1_sig a * proj1_sig (pow0 a x)) mod m) - (Z_mod_mod (proj1_sig a * proj1_sig (pow0 a x)) m))}. - intros m. exists pow_impl_sig. - split; [eauto using exist_reduced_eq|]; intros. - apply exist_reduced_eq. - rewrite powmod_1plus. - rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal. -Qed. - -Lemma mul_mod_modulus_r : forall x m, (x*m) mod m = 0. - intros. - rewrite Zmult_mod, Z_mod_same_full. - rewrite Z.mul_0_r, Zmod_0_l. - reflexivity. -Qed. - -Lemma mod_opp_equiv : forall x y m, x mod m = (-y) mod m -> - (-x) mod m = y mod m. -Proof. - intros. - rewrite <-Z.sub_0_l. - rewrite Zminus_mod. rewrite H. - rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal. - destruct y; auto. + (Z_mod_mod (proj1_sig a * proj1_sig (pow0 a x)) m))} := pow_impl_sig. +Next Obligation. + split; intros; apply exist_reduced_eq; + rewrite ?powmod_1plus, ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; reflexivity. Qed. -Definition mod_inv_eucl (a m:Z) : Z. - destruct (euclid a m). (* [euclid] is opaque. TODO: reimplement? *) - exact ((match a with Z0 => Z0 | _ => - (match d with Z.pos _ => u | _ => -u end) - end) mod m). -Defined. - -Lemma reduced_nonzero_pos: - forall a m : Z, m > 0 -> a <> 0 -> a = a mod m -> 0 < a. -Proof. - intros a m m_pos a_nonzero pfa. - destruct (Z.eq_dec 0 m); subst_max; try omega. - pose proof (Z_mod_lt a m) as H. - destruct (Z.eq_dec 0 a); subst_max; try omega. +Program Definition mod_inv_sig {m} (a:{z : Z | z = z mod m}) : {z : Z | z = z mod m} := + let (a, _) := a in + match a return _ with + | 0%Z => 0 (* m = 2 *) + | _ => powmod m a (Z.to_N (m-2)) + end. +Next Obligation. + abstract (destruct a; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity). Qed. -Lemma mod_inv_eucl_correct : forall a m, a <> 0 -> a = a mod m -> prime m -> - ((mod_inv_eucl a m) * a) mod m = 1 mod m. -Proof. - intros a m a_nonzero pfa prime_m. - pose proof (prime_ge_2 _ prime_m). - assert (0 < m) as m_pos by omega. - assert (0 <= m) as m_nonneg by omega. - assert (0 < a) as a_pos by (eapply reduced_nonzero_pos; eauto; omega). - unfold mod_inv_eucl. - destruct a as [|a'|a'] eqn:ha; try pose proof (Zlt_neg_0 a') as nnn; try omega; clear nnn. - rewrite<- ha in *. - lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end. - lazymatch goal with [H: Zis_gcd _ _ _ |- _ ] => destruct H end. - rewrite Z.add_move_r in e. - destruct (Z_mod_lt a m ); try omega; rewrite <- pfa in *. - destruct (prime_divisors _ prime_m _ H1) as [Ha|[Hb|[Hc|Hd]]]; subst d. - + assert ((u * a) mod m = (-1 - v * m) mod m) as Hx by (f_equal; trivial). - rewrite Zminus_mod, mul_mod_modulus_r, Z.sub_0_r, Zmod_mod in Hx. - rewrite Zmult_mod_idemp_l. - rewrite <-Zopp_mult_distr_l. - eauto using mod_opp_equiv. - + rewrite Zmult_mod_idemp_l. - rewrite e, Zminus_mod, mul_mod_modulus_r, Z.sub_0_r, Zmod_mod; reflexivity. - + pose proof (Zdivide_le _ _ m_nonneg a_pos H0); omega. - + apply Zdivide_opp_l_rev in H0. - pose proof (Zdivide_le _ _ m_nonneg a_pos H0); omega. -Qed. - -Lemma mod_inv_eucl_sig : forall {m}, {z : Z | z = z mod m} -> {z : Z | z = z mod m}. - intros m a. - exists (mod_inv_eucl (proj1_sig a) m). - destruct a; unfold mod_inv_eucl. - lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end. - rewrite Zmod_mod; reflexivity. -Defined. - -Definition inv_impl : - forall {m : BinNums.Z}, +Program Definition inv_impl {m : BinNums.Z} : {inv0 : {z : BinNums.Z | z = z mod m} -> {z : BinNums.Z | z = z mod m} | inv0 (exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m)) = exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m) /\ @@ -202,20 +119,21 @@ Definition inv_impl : exist (fun z : BinNums.Z => z = z mod m) ((proj1_sig a * proj1_sig (inv0 a)) mod m) (Z_mod_mod (proj1_sig a * proj1_sig (inv0 a)) m) = - exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))}. -Proof. - intros m. exists mod_inv_eucl_sig. split; intros. - - simpl. - apply exist_reduced_eq; simpl. - unfold mod_inv_eucl; simpl. - lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end. - auto. - - - destruct a. - cbv [proj1_sig mod_inv_eucl_sig]. - rewrite Z.mul_comm. - eapply exist_reduced_eq. - rewrite mod_inv_eucl_correct; eauto. - intro; destruct H0. - eapply exist_reduced_eq. congruence. + exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))} + := mod_inv_sig. +Next Obligation. + split. + { apply exist_reduced_eq; rewrite Zmod_0_l; reflexivity. } + intros Hm [a pfa] Ha'. apply exist_reduced_eq. + assert (Hm':0 <= m - 2) by (pose proof prime_ge_2 m Hm; omega). + assert (Ha:a mod m<>0) by (intro; apply Ha', exist_reduced_eq; congruence). + cbv [proj1_sig mod_inv_sig]. + transitivity ((a*powmod m a (Z.to_N (m - 2))) mod m); [destruct a; congruence|]. + rewrite !powmod_Zpow_mod. + rewrite Z2N.id by assumption. + rewrite Zmult_mod_idemp_r. + rewrite <-Z.pow_succ_r by assumption. + replace (Z.succ (m - 2)) with (m-1) by omega. + rewrite (Zmod_small 1) by omega. + apply (fermat_little m Hm a Ha). Qed. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index a2f606f30..8d594e8ce 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -346,8 +346,8 @@ Section VariousModPrime. Proof. intros. pose proof (euler_criterion_if' a q_odd) as H. - unfold F_eqb in *; simpl in *. - rewrite !Zmod_small, !@FieldToZ_pow_efficient in H by omega; eauto. + unfold F_eqb in H. + rewrite !FieldToZ_ZToField, !@FieldToZ_pow_efficient, !Zmod_small in H by omega; assumption. Qed. Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index 8ee07fe5d..fc506f61d 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -24,29 +24,24 @@ Coercion FieldToZ {m} (a:F m) : BinNums.Z := proj1_sig a. Section FieldOperations. Context {m : BinInt.Z}. - - (* Coercion without Context {m} --> non-uniform inheritance --> Anomalies *) - Let ZToFm := ZToField : BinNums.Z -> F m. Local Coercion ZToFm : BinNums.Z >-> F. + Definition zero : F m := ZToField 0. + Definition one : F m := ZToField 1. Definition add (a b:F m) : F m := ZToField (a + b). Definition mul (a b:F m) : F m := ZToField (a * b). - - Definition opp_with_spec : { opp : F m -> F m - | forall x, add x (opp x) = 0 - } := Pre.opp_impl. - Definition opp : F m -> F m := Eval hnf in proj1_sig opp_with_spec. + Definition opp (a : F m) : F m := ZToField (0 - a). Definition sub (a b:F m) : F m := add a (opp b). Definition inv_with_spec : { inv : F m -> F m - | inv 0 = 0 + | inv zero = zero /\ ( Znumtheory.prime m -> - forall (a:F m), a <> 0 -> mul a (inv a) = 1 ) + forall a, a <> zero -> mul a (inv a) = one ) } := Pre.inv_impl. Definition inv : F m -> F m := Eval hnf in proj1_sig inv_with_spec. Definition div (a b:F m) : F m := mul a (inv b). Definition pow_with_spec : { pow : F m -> BinNums.N -> F m - | forall a, pow a 0%N = 1 + | forall a, pow a 0%N = one /\ forall x, pow a (1 + x)%N = mul a (pow a x) } := Pre.pow_impl. Definition pow : F m -> BinNums.N -> F m := Eval hnf in proj1_sig pow_with_spec. -- cgit v1.2.3 From 980c92a3b46897b4e1b1d72bc552d3a48e27c673 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 20 Jul 2016 18:53:24 -0400 Subject: automate a proof --- src/ModularArithmetic/Pre.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 47a38b867..5e61278f6 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -4,6 +4,7 @@ Require Import Coq.Logic.EqdepFacts. Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.omega.Omega. Require Import Crypto.Util.NumTheoryUtil. +Require Import Crypto.Tactics.VerdiTactics. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. symmetry. @@ -106,7 +107,7 @@ Program Definition mod_inv_sig {m} (a:{z : Z | z = z mod m}) : {z : Z | z = z mo | _ => powmod m a (Z.to_N (m-2)) end. Next Obligation. - abstract (destruct a; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity). + intros; break_match; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity. Qed. Program Definition inv_impl {m : BinNums.Z} : -- cgit v1.2.3 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