diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-03-20 18:59:20 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-03-20 18:59:20 -0400 |
commit | 5f3561d6de74183448ceaf03685b0a1aaa1d6e0a (patch) | |
tree | 6e888baf161d5e88f466787ef203463cd0a51e68 /src | |
parent | b2de1ea79a9b0499d3931b936fda7e3289061285 (diff) |
Ed25519: d is nonsquare
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 12 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 30 |
2 files changed, 30 insertions, 12 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 91ac63d26..77d84c455 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -294,7 +294,7 @@ Section VariousModPrime. } Qed. - Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q), + Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q), if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1)) then (isSquare a) else (forall b, b ^ 2 <> a). Proof. @@ -309,6 +309,16 @@ Section VariousModPrime. apply euler_criterion_F in a_square; auto. Qed. + Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q), + if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1) + then (isSquare a) else (forall b, b ^ 2 <> a). + 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. + Qed. + Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. Proof. intros ? ? squares_eq. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 92c36b56c..d6d02b93f 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -43,11 +43,26 @@ Proof. rewrite Z.mod_small; q_bound. Qed. -(* TODO *) -(* d = .*) +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. Admitted. -(* Definition nonsquare_d : (forall x, x^2 <> d) := euler_criterion_if d. <-- currently not computable in reasonable time *) +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 TEParams : TwistedEdwardsParams := { q := q; @@ -117,13 +132,6 @@ Definition FlEncoding : encoding of F (Z.of_nat l) as word b := Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed. -Hint Rewrite - @FieldToZ_pow_efficient - @FieldToZ_ZToField - @FieldToZ_opp - @FieldToZ_ZToField : ZToField - . - Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F. Proof. apply F_eq. |