1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
Require Export Crypto.Spec.CompleteEdwardsCurve.
Require Import Crypto.Algebra Crypto.Nsatz.
Require Import Crypto.CompleteEdwardsCurve.Pre.
Require Import Coq.Logic.Eqdep_dec.
Require Import Crypto.Tactics.VerdiTactics.
Module E.
Import Group Ring Field CompleteEdwardsCurve.E.
Section CompleteEdwardsCurveTheorems.
Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
{field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
{prm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}.
Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
Local Notation "0" := Fzero. Local Notation "1" := Fone.
Local Infix "+" := Fadd. Local Infix "*" := Fmul.
Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
Local Notation "x ^2" := (x*x) (at level 30).
Local Notation point := (@point F Feq Fone Fadd Fmul a d).
Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d).
Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)).
Definition eq (P Q:point) :=
let Feq2 (ab xy:F*F) := fst ab = fst xy /\ snd ab = snd xy in
Feq2 (coordinates P) (coordinates Q).
Infix "=" := eq : E_scope.
(* TODO:port
Local Ltac t :=
unfold point_eqb;
repeat match goal with
| _ => progress intros
| _ => progress simpl in *
| _ => progress subst
| [P:E.point |- _ ] => destruct P
| [x: (F q * F q)%type |- _ ] => destruct x
| [H: _ /\ _ |- _ ] => destruct H
| [H: _ |- _ ] => rewrite Bool.andb_true_iff in H
| [H: _ |- _ ] => apply F_eqb_eq in H
| _ => rewrite F_eqb_refl
end; eauto.
Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2.
Proof.
t.
Qed.
Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true.
Proof.
t.
Qed.
Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2.
Proof.
intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
apply point_eqb_complete in H0; congruence.
Qed.
Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false.
Proof.
intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
apply point_eqb_sound in Hneq. congruence.
Qed.
Lemma point_eqb_refl : forall p, point_eqb p p = true.
Proof.
t.
Qed.
Definition point_eq_dec (p1 p2:E.point) : {p1 = p2} + {p1 <> p2}.
destruct (point_eqb p1 p2) eqn:H; match goal with
| [ H: _ |- _ ] => apply point_eqb_sound in H
| [ H: _ |- _ ] => apply point_eqb_neq in H
end; eauto.
Qed.
Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false.
Proof.
intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete.
Qed.
*)
(* TODO: move to util *)
Lemma decide_and : forall P Q, {P}+{not P} -> {Q}+{not Q} -> {P/\Q}+{not(P/\Q)}.
Proof. intros; repeat match goal with [H:{_}+{_}|-_] => destruct H end; intuition. Qed.
Ltac destruct_points :=
repeat match goal with
| [ p : point |- _ ] =>
let x := fresh "x" p in
let y := fresh "y" p in
let pf := fresh "pf" p in
destruct p as [[x y] pf]
end.
Ltac expand_opp :=
rewrite ?mul_opp_r, ?mul_opp_l, ?ring_sub_definition, ?inv_inv, <-?ring_sub_definition.
Local Hint Resolve char_gt_2.
Local Hint Resolve nonzero_a.
Local Hint Resolve square_a.
Local Hint Resolve nonsquare_d.
Local Hint Resolve @edwardsAddCompletePlus.
Local Hint Resolve @edwardsAddCompleteMinus.
Program Definition opp (P:point) : point :=
exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _.
Solve All Obligations using intros; destruct_points; simpl; field_algebra.
Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
Proof.
repeat match goal with
| |- _ => progress intros
| [H: _ /\ _ |- _ ] => destruct H
| |- _ => progress destruct_points
| |- _ => progress cbv [fst snd coordinates proj1_sig eq add zero opp] in *
| |- _ => split
| |- Feq _ _ => common_denominator_all; try nsatz
| |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto]
| |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances
end.
(* TODO: port denominator-nonzero proofs for associativity *)
match goal with | |- _ <> 0 => admit end.
match goal with | |- _ <> 0 => admit end.
match goal with | |- _ <> 0 => admit end.
match goal with | |- _ <> 0 => admit end.
Qed.
(* TODO: move to [Group] and [AbelianGroup] as appropriate *)
Lemma mul_0_l : forall P, (0 * P = zero)%E.
Proof. intros; reflexivity. Qed.
Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E.
Proof. intros; reflexivity. Qed.
Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E.
Proof.
induction n; intros;
rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
Qed.
Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E.
Proof.
induction n; intros; [reflexivity|].
rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity.
Qed.
Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed.
(*
Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E.
Proof.
induction n. intros. simpl. admit.
Qed.
*)
Section PointCompression.
Local Notation "x ^2" := (x*x).
Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)).
Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0.
Proof.
intros ? eq_zero.
destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero.
destruct (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; field_algebra.
Qed.
Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y).
Proof.
unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero.
Qed.
End PointCompression.
End CompleteEdwardsCurveTheorems.
End E.
|
