blob: e5796b8f2f48e54fbbf0c02e4d602d467eb0650e (
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
|
Require Import ZArith.ZArith Zpower ZArith Znumtheory.
Require Import NPeano NArith.
Require Import Crypto.Spec.Encoding.
Require Import Crypto.Spec.EdDSA.
Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
Require Import Crypto.Curves.PointFormats.
Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil.
Require Import Bedrock.Word.
Require Import VerdiTactics.
Require Import Decidable.
Require Import Omega.
Local Open Scope nat_scope.
Definition q : Z := (2 ^ 255 - 19)%Z.
Lemma 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.
Lemma q_1mod4 : (q mod 4 = 1)%Z. reflexivity. Qed.
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.
(* TODO *)
(* d = .*)
Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F.
Lemma nonsquare_d : forall x, (x^2 <> d)%F. Admitted.
(* Definition nonsquare_d : (forall x, x^2 <> d) := euler_criterion_if d. <-- currently not computable in reasonable time *)
Instance TEParams : TwistedEdwardsParams := {
q := q;
prime_q := prime_q;
two_lt_q := two_lt_q;
a := a;
nonzero_a := nonzero_a;
square_a := square_a;
d := d;
nonsquare_d := nonsquare_d
}.
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 CompleteEdwardsCurve.q)%nat.
Proof.
replace (CompleteEdwardsCurve.q) with q by reflexivity.
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.
Lemma l_bound : l < pow2 b.
Proof.
rewrite Zpow_pow2.
unfold l.
rewrite <- Z2Nat.inj_lt; compute; congruence.
Qed.
Lemma q_pos : (0 < q)%Z. q_bound. Qed.
Definition FqEncoding : encoding of (F q) as word (b-1) :=
@modular_word_encoding q (b - 1) q_pos b_valid.
Check @modular_word_encoding.
Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed.
(* form of l_bound needed for FlEncoding *)
Lemma l_bound_encoding : Z.to_nat (Z.of_nat l) < 2 ^ b.
Proof.
rewrite Nat2Z.id.
rewrite <- pow2_id.
exact l_bound.
Qed.
Definition FlEncoding : encoding of F (Z.of_nat l) as word b :=
@modular_word_encoding (Z.of_nat l) b l_pos l_bound_encoding.
Definition H : forall n : nat, word n -> word (b + b). Admitted.
Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
Definition B_nonzero : B <> zero. Admitted.
Definition l_order_B : scalarMult l B = zero. Admitted.
Definition PointEncoding : encoding of point as word b. Admitted.
Instance x : EdDSAParams := {
E := TEParams;
b := b;
H := H;
c := c;
n := n;
B := B;
l := l;
FqEncoding := FqEncoding;
FlEncoding := FlEncoding;
PointEncoding := PointEncoding;
b_valid := b_valid;
c_valid := c_valid;
n_ge_c := n_ge_c;
n_le_b := n_le_b;
B_not_identity := B_nonzero;
l_prime := prime_l;
l_odd := l_odd;
l_order_B := l_order_B
}.
|
