blob: cc6234762b1db6706f3b3e793092ec6bbc2f3784 (
plain)
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
|
Require Export Crypto.Spec.CompleteEdwardsCurve.
Require Import Crypto.Algebra Crypto.Algebra.
Require Import Crypto.CompleteEdwardsCurve.Pre.
Require Import Coq.Logic.Eqdep_dec.
Require Import Crypto.Tactics.VerdiTactics.
Require Import Coq.Classes.Morphisms.
Require Import Relation_Definitions.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Notations.
Module E.
Import Group ScalarMult 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).
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) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q).
Infix "=" := eq : E_scope.
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.
Local Obligation Tactic := intros; destruct_points; simpl; field_algebra.
Program Definition opp (P:point) : point :=
exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _.
Ltac bash_step :=
match goal with
| |- _ => progress intros
| [H: _ /\ _ |- _ ] => destruct H
| |- _ => progress destruct_points
| |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in *
| |- _ => split
| |- Feq _ _ => field_algebra
end.
Ltac bash := repeat bash_step.
Global Instance Proper_add : Proper (eq==>eq==>eq) add.
Proof. bash.
pose proof edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a) as Hxy.
specialize (Hxy _ _ _ _ pfx pfy).
pose proof (edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a) _ _ _ _ pfx pfy).
Qed.
Global Instance Proper_opp : Proper (eq==>eq) opp. Proof. bash. Qed.
Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. bash. Qed.
Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
Proof.
bash.
(* 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.
Admitted.
Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul.
Proof.
intros n m Hnm P Q HPQ. rewrite <-Hnm; clear Hnm m.
induction n; simpl; rewrite ?IHn, ?HPQ; reflexivity.
Qed.
Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul.
Proof. split; intros; reflexivity || typeclasses eauto. 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.
Section Homomorphism.
Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd}
{fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
{Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}.
Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd}
{fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
{Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}.
Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul
K Keq Kone Kadd Kmul phi}.
Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}.
Local Notation Fpoint := (@point F Feq Fone Fadd Fmul Fa Fd).
Local Notation Kpoint := (@point K Keq Kone Kadd Kmul Ka Kd).
Create HintDb field_homomorphism discriminated.
Hint Rewrite <-
homomorphism_one
homomorphism_add
homomorphism_sub
homomorphism_mul
homomorphism_div
Ha
Hd
: field_homomorphism.
Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ (
let (x, y) := coordinates P in (phi x, phi y)) _.
Next Obligation.
destruct P as [[? ?] ?]; simpl.
rewrite_strat bottomup hints field_homomorphism.
eauto using is_homomorphism_phi_proper; assumption.
Qed.
Context {point_phi:Fpoint->Kpoint}
{point_phi_Proper:Proper (eq==>eq) point_phi}
{point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}.
Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi.
Proof.
repeat match goal with
| |- Group.is_homomorphism => split
| |- _ => intro
| |- _ /\ _ => split
| [H: _ /\ _ |- _ ] => destruct H
| [p: point |- _ ] => destruct p as [[??]?]
| |- context[point_phi] => setoid_rewrite point_phi_correct
| |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp ref_phi] in *
| |- Keq ?x ?x => reflexivity
| |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism
| [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition]
end.
Qed.
End Homomorphism.
End E.
|
