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
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics.
Require Import Crypto.Spec.ModularArithmetic.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Local Open Scope F_scope.
Section Pre.
Context {q : BinInt.Z}.
Context {a : F q}.
Context {d : F q}.
Context {prime_q : Znumtheory.prime q}.
Context {two_lt_q : 2 < q}.
Context {a_nonzero : a <> 0}.
Context {a_square : exists sqrt_a, sqrt_a^2 = a}.
Context {d_nonsquare : forall x, x^2 <> d}.
Add Field Ffield_Z : (@Ffield_theory q _)
(morphism (@Fring_morph q),
preprocess [Fpreprocess],
postprocess [Fpostprocess],
constants [Fconstant],
div (@Fmorph_div_theory q),
power_tac (@Fpower_theory q) [Fexp_tac]).
(* the canonical definitions are in Spec *)
Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
Local Notation unifiedAdd' P1' P2' := (
let '(x1, y1) := P1' in
let '(x2, y2) := P2' in
(((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
).
Lemma char_gt_2 : ZToField 2 <> (0: F q).
intro; find_injection.
pose proof two_lt_q.
rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega.
Qed.
Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
Ltac whatsNotZero :=
repeat match goal with
| [H: ?lhs = ?rhs |- _ ] =>
match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end;
assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
| [H: ?lhs = ?rhs |- _ ] =>
match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end;
assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
| [H: (?a^?p)%F <> 0 |- _ ] =>
match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
let Y:=fresh in let Z:=fresh in try (
assert (p <> 0%N) as Z by (intro Y; inversion Y);
assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0);
clear Z)
| [H: (?a*?b)%F <> 0 |- _ ] =>
match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0)
| [H: (?a*?b)%F <> 0 |- _ ] =>
match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end;
assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0)
end.
Lemma edwardsAddComplete' x1 y1 x2 y2 :
onCurve (x1, y1) ->
onCurve (x2, y2) ->
(d*x1*x2*y1*y2)^2 <> 1.
Proof.
intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero.
destruct a_square as [sqrt_a a_square'].
rewrite <-a_square' in *.
(* Furthermore... *)
pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
rewrite Hc2 in Heqt at 2.
replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2))
with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field.
rewrite Hcontra in Heqt.
replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
rewrite <-Hc1 in Heqt.
(* main equation for both potentially nonzero denominators *)
destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
try lazymatch goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] =>
assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 =
f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2)
(d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field;
rewrite Hcontra in Heqw1;
replace (1 * y1^2) with (y1^2) in * by field;
rewrite <- Heqt in *;
assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 /
(x1 * y1 * (f (sqrt_a * x2) y2))^2)
by (rewriteAny; field; auto);
match goal with [H: d = (?n^2)/(?l^2) |- _ ] =>
destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
end
end.
assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
(* contradiction: product of nonzero things is zero *)
destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
apply Ha_nonzero; field.
Qed.
Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
onCurve (x1, y1) ->
onCurve (x2, y2) ->
(1 + d*x1*x2*y1*y2) <> 0.
Proof.
intros Hc1 Hc2; simpl in Hc1, Hc2.
intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H].
- assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
- replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
intro Hz; rewrite Hz in H; intuition.
Qed.
Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
onCurve (x1, y1) ->
onCurve (x2, y2) ->
(1 - d*x1*x2*y1*y2) <> 0.
Proof.
intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H].
- assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
- replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
intro Hz; rewrite Hz in H; apply H; field.
Qed.
Definition zeroOnCurve : onCurve (0, 1).
simpl. field.
Qed.
Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
(H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
Proof.
(* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
* c=1 and an extra a in front of x^2 *)
injection H; clear H; intros.
Ltac t x1 y1 x2 y2 :=
assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
= (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
= 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
t x1 y1 x2 y2; t x2 y2 x1 y1.
remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
(a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +(
(y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
match goal with [ |- ?x = 1 ] => replace x with
((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/
((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end.
- rewrite <-HT1, <-HT2; field; rewrite HT1.
replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field.
auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
edwardsAddCompleteMinus, edwardsAddCompletePlus.
- field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
by field;
auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
edwardsAddCompleteMinus, edwardsAddCompletePlus.
Qed.
Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
onCurve (unifiedAdd' P1 P2).
Proof.
intros; destruct P1, P2.
remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
eapply unifiedAdd'_onCurve'; eauto.
Qed.
End Pre.
|
