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
|
Require Import Coq.Classes.Morphisms.
Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Curves.Edwards.AffineProofs.
Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings.
Require Export Crypto.Util.FixCoqMistakes.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.UniquePose.
Module Extended.
Section ExtendedCoordinates.
Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
{field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
{char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
{Feq_dec:DecidableRel Feq}.
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).
Context {a d: F}
{nonzero_a : a <> 0}
{square_a : exists sqrt_a, sqrt_a^2 = a}
{nonsquare_d : forall x, x^2 <> d}.
Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
(** [Extended.point] represents a point on an elliptic curve using extended projective
* Edwards coordinates 1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
Definition point := { P | let '(X,Y,Z,T) := P in
a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2
/\ X * Y = Z * T
/\ Z <> 0 }.
Definition coordinates (P:point) : F*F*F*F := proj1_sig P.
Definition eq (P1 P2:point) :=
let '(X1, Y1, Z1, _) := coordinates P1 in
let '(X2, Y2, Z2, _) := coordinates P2 in
Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.
Ltac t_step :=
match goal with
| |- Proper _ _ => intro
| _ => progress intros
| _ => progress destruct_head' prod
| _ => progress destruct_head' @E.point
| _ => progress destruct_head' point
| _ => progress destruct_head' and
| _ => progress cbv [eq CompleteEdwardsCurve.E.eq E.eq E.zero E.add E.opp fst snd coordinates E.coordinates proj1_sig] in *
| |- _ /\ _ => split | |- _ <-> _ => split
end.
Ltac t := repeat t_step; Field.fsatz.
Global Instance Equivalence_eq : Equivalence eq.
Proof using Feq_dec field nonzero_a. split; repeat intro; t. Qed.
Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
Proof. intros P Q; destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; exact _. Defined.
Program Definition from_twisted (P:Epoint) : point :=
let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy * snd xy).
Next Obligation. t. Qed.
Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted.
Proof using Type. cbv [from_twisted]; t. Qed.
Program Definition to_twisted (P:point) : Epoint :=
let XYZT := coordinates P in let T := snd XYZT in
let XYZ := fst XYZT in let Z := snd XYZ in
let XY := fst XYZ in let Y := snd XY in
let X := fst XY in
let iZ := Finv Z in ((X*iZ), (Y*iZ)).
Next Obligation. t. Qed.
Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted.
Proof using Type. cbv [to_twisted]; t. Qed.
Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P.
Proof using Type. cbv [to_twisted from_twisted]; t. Qed.
Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P.
Proof using Type. cbv [to_twisted from_twisted]; t. Qed.
Program Definition zero : point := (0, 1, 1, 0).
Next Obligation. t. Qed.
Program Definition opp P : point :=
match coordinates P return F*F*F*F with (X,Y,Z,T) => (Fopp X, Y, Z, Fopp T) end.
Next Obligation. t. Qed.
Section TwistMinusOne.
Context {a_eq_minus1:a = Fopp 1} {twice_d} {k_eq_2d:twice_d = d+d}.
Program Definition m1add
(P1 P2:point) : point :=
match coordinates P1, coordinates P2 return F*F*F*F with
(X1, Y1, Z1, T1), (X2, Y2, Z2, T2) =>
let A := (Y1-X1)*(Y2-X2) in
let B := (Y1+X1)*(Y2+X2) in
let C := T1*twice_d*T2 in
let D := Z1*(Z2+Z2) in
let E := B-A in
let F := D-C in
let G := D+C in
let H := B+A in
let X3 := E*F in
let Y3 := G*H in
let T3 := E*H in
let Z3 := F*G in
(X3, Y3, Z3, T3)
end.
Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))); t. Qed.
Global Instance isomorphic_commutative_group_m1 :
@Group.isomorphic_commutative_groups
Epoint E.eq
(E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d))
(E.zero(nonzero_a:=nonzero_a))
(E.opp(nonzero_a:=nonzero_a))
point eq m1add zero opp
from_twisted to_twisted.
Proof.
eapply Group.commutative_group_by_isomorphism; try exact _.
par: abstract
(cbv [to_twisted from_twisted zero opp m1add]; intros;
repeat match goal with
| |- context[E.add ?P ?Q] =>
unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q)) end;
t).
Qed.
End TwistMinusOne.
End ExtendedCoordinates.
End Extended.
|