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
|
Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
Require Import Crypto.Algebra Crypto.Algebra.
Require Import Crypto.Util.Notations.
Generalizable All Variables.
Section Pre.
Context {F eq zero one opp add sub mul inv div}
`{field F eq zero one opp add sub mul inv div}.
Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
Local Notation "0" := zero. Local Notation "1" := one.
Local Infix "+" := add. Local Infix "*" := mul.
Local Infix "-" := sub. Local Infix "/" := div.
Local Notation "x ^ 2" := (x*x).
Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}.
Context {d:F} {d_nonsquare : forall sqrt_d, sqrt_d^2 <> d}.
Context {char_gt_2 : 1+1 <> 0}.
(* the canonical definitions are in Spec *)
Definition onCurve (P:F*F) := let (x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
Definition unifiedAdd' (P1' P2':F*F) : F*F :=
let (x1, y1) := P1' in
let (x2, y2) := P2' in
pair (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *.
Lemma onCurve_subst : forall x1 x2 y1 y2, and (eq x1 y1) (eq x2 y2) -> onCurve (x1, x2) ->
onCurve (y1, y2).
Proof.
unfold onCurve.
intros ? ? ? ? [eq_1 eq_2] ?.
rewrite eq_1, eq_2 in *.
assumption.
Qed.
Lemma edwardsAddComplete' x1 y1 x2 y2 :
onCurve (pair x1 y1) ->
onCurve (pair x2 y2) ->
(d*x1*x2*y1*y2)^2 <> 1.
Proof.
unfold onCurve, not; use_sqrt_a; intros.
destruct (eq_dec (sqrt_a*x2 + y2) 0); destruct (eq_dec (sqrt_a*x2 - y2) 0);
lazymatch goal with
| [H: not (eq (?f (sqrt_a * x2) y2) 0) |- _ ]
=> apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))
/(f (sqrt_a * x2) y2 * x1 * y1 ))
| _ => apply a_nonzero
end; super_nsatz.
Qed.
Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0.
Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed.
Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0.
Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed.
Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. super_nsatz. Qed.
Lemma unifiedAdd'_onCurve : forall P1 P2,
onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2).
Proof.
unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] ? ?.
common_denominator; [ | auto using edwardsAddCompleteMinus, edwardsAddCompletePlus..].
nsatz.
Qed.
End Pre.
Import Group Ring Field.
(* TODO: move -- this does not need to be defined before [point] *)
Section RespectsFieldHomomorphism.
Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}.
Context {K eq zero one opp add mul sub inv div} `{@field K eq zero one opp add sub mul inv div}.
Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
Context {phi:F->K} `{@is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}.
Context {A D:F} {a d:K} {a_ok:phi A=a} {d_ok:phi D=d}.
Let phip := fun (P':F*F) => let (x, y) := P' in (phi x, phi y).
Let eqp := fun (P1' P2':K*K) =>
let (x1, y1) := P1' in
let (x2, y2) := P2' in
and (eq x1 x2) (eq y1 y2).
Create HintDb field_homomorphism discriminated.
Hint Rewrite
homomorphism_one
homomorphism_add
homomorphism_sub
homomorphism_mul
homomorphism_div
a_ok
d_ok
: field_homomorphism.
Lemma morphism_unifiedAdd' : forall P Q:F*F,
(~ EQ (ADD ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) ->
(~ EQ (SUB ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) ->
eqp
(phip (unifiedAdd'(F:=F)(one:=ONE)(add:=ADD)(sub:=SUB)(mul:=MUL)(div:=DIV)(a:=A)(d:=D) P Q))
(unifiedAdd'(F:=K)(one:=one)(add:=add)(sub:=sub)(mul:=mul)(div:=div)(a:=a)(d:=d) (phip P) (phip Q)).
Proof.
intros [x1 y1] [x2 y2] Hnonzero1 Hnonzero2;
cbv [unifiedAdd' phip eqp];
apply conj;
(rewrite_strat topdown hints field_homomorphism); try assumption; reflexivity.
Qed.
End RespectsFieldHomomorphism.
|
