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
|
Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
Require Import Crypto.Spec.ModularWordEncoding.
Require Import Crypto.Encoding.ModularWordEncodingTheorems.
Require Import Crypto.Spec.EdDSA.
Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil.
Require Import Bedrock.Word.
Require Import Crypto.Tactics.VerdiTactics.
Require Import Coq.Logic.Decidable.
Require Import Coq.omega.Omega.
Local Open Scope nat_scope.
Definition q : Z := (2 ^ 255 - 19)%Z.
Global Instance prime_q : prime q. Admitted.
Lemma two_lt_q : (2 < q)%Z. reflexivity. Qed.
Definition a : F q := opp 1%F.
(* TODO (jadep) : make the proofs about a and d more general *)
Lemma nonzero_a : a <> 0%F.
Proof.
unfold a.
intro eq_opp1_0.
apply (@Fq_1_neq_0 q prime_q).
rewrite <- (F_opp_spec 1%F).
rewrite eq_opp1_0.
symmetry; apply F_add_0_r.
Qed.
Ltac q_bound := pose proof two_lt_q; omega.
Lemma square_a : isSquare a.
Proof.
assert (q_1mod4 : (q mod 4 = 1)%Z) by abstract reflexivity.
intros.
pose proof (minus1_square_1mod4 q prime_q q_1mod4) as minus1_square.
destruct minus1_square as [b b_id].
apply square_Zmod_F.
exists b; rewrite b_id.
unfold a.
rewrite opp_ZToField.
rewrite FieldToZ_ZToField.
rewrite Z.mod_small; q_bound.
Qed.
Hint Rewrite
@FieldToZ_add
@FieldToZ_mul
@FieldToZ_opp
@FieldToZ_inv_efficient
@FieldToZ_pow_efficient
@FieldToZ_ZToField
@Zmod_mod
: ZToField.
Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F.
Lemma nonsquare_d : forall x, (x^2 <> d)%F.
pose proof @euler_criterion_if q prime_q d two_lt_q.
match goal with
[H: if ?b then ?x else ?y |- ?y ] => replace b with false in H; [exact H|clear H]
end.
unfold d, div. autorewrite with ZToField; [|eauto using prime_q, two_lt_q..].
vm_compute. (* 10s *)
exact eq_refl.
Qed. (* 10s *)
Instance curve25519params : @E.twisted_edwards_params (F q) eq (ZToField 0) (ZToField 1) add mul a d :=
{
nonzero_a := nonzero_a
(* TODO:port
char_gt_2 : ~ Feq (Fadd Fone Fone) Fzero;
nonzero_a : ~ Feq a Fzero;
nonsquare_d : forall x : F, ~ Feq (Fmul x x) d }
*)
}.
Admitted.
Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = 2 ^ n.
Admitted.
Definition b := 256.
Lemma b_valid : (2 ^ (b - 1) > Z.to_nat q)%nat.
Proof.
unfold q, gt.
replace (2 ^ (b - 1)) with (Z.to_nat (2 ^ (Z.of_nat (b - 1))))
by (rewrite <- two_power_nat_equiv; apply two_power_nat_Z2Nat).
rewrite <- Z2Nat.inj_lt; compute; congruence.
Qed.
Definition c := 3.
Lemma c_valid : c = 2 \/ c = 3.
Proof.
right; auto.
Qed.
Definition n := b - 2.
Lemma n_ge_c : n >= c.
Proof.
unfold n, c, b; omega.
Qed.
Lemma n_le_b : n <= b.
Proof.
unfold n, b; omega.
Qed.
Definition l : nat := Z.to_nat (252 + 27742317777372353535851937790883648493)%Z.
Lemma prime_l : prime (Z.of_nat l). Admitted.
Lemma l_odd : l > 2.
Proof.
unfold l, proj1_sig.
rewrite Z2Nat.inj_add; try omega.
apply lt_plus_trans.
compute; omega.
Qed.
Require Import Crypto.Spec.Encoding.
Lemma q_pos : (0 < q)%Z. q_bound. Qed.
Definition FqEncoding : canonical encoding of (F q) as word (b-1) :=
@modular_word_encoding q (b - 1) q_pos b_valid.
Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed.
Lemma l_bound : Z.to_nat (Z.of_nat l) < 2 ^ b.
Proof.
rewrite Nat2Z.id.
rewrite <- pow2_id.
rewrite Zpow_pow2.
unfold l.
apply Z2Nat.inj_lt; compute; congruence.
Qed.
Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b :=
@modular_word_encoding (Z.of_nat l) b l_pos l_bound.
Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed.
Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F.
Proof.
apply F_eq.
autorewrite with ZToField.
vm_compute.
reflexivity.
Qed.
Local Notation point := (@E.point (F q) eq (ZToField 1) add mul a d).
Local Notation zero := (E.zero(H:=field_modulo)).
Local Notation add := (E.add(H0:=curve25519params)).
Local Infix "*" := (E.mul(H0:=curve25519params)).
Axiom H : forall n : nat, word n -> word (b + b).
Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *)
Axiom B_nonzero : B <> zero.
Axiom l_order_B : E.eq (l * B) zero.
Axiom Eenc : point -> word b.
Axiom Senc : nat -> word b.
Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B Eenc Senc :=
{
EdDSA_c_valid := c_valid;
EdDSA_n_ge_c := n_ge_c;
EdDSA_n_le_b := n_le_b;
EdDSA_B_not_identity := B_nonzero;
EdDSA_l_prime := prime_l;
EdDSA_l_odd := l_odd;
EdDSA_l_order_B := l_order_B
}.
|
