diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-20 18:33:02 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-20 18:53:43 -0400 |
| commit | d7f30db5fe04b11fa22a3b3b79eb0e63a72cb0f1 (patch) | |
| tree | d815bfbadaf6681593f778667e961be51443a2aa /src/Experiments | |
| parent | a5caf332df39f57bf25829cf5c127aa54fb8d3e4 (diff) | |
compute on [F q]!
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/SpecEd25519.v | 19 |
1 files changed, 11 insertions, 8 deletions
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<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. +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 := { |