Crypto_Scalarmult.v 9.61 KB
Newer Older
1
2
3
4
5
From Tweetnacl.Libs Require Import Export.
From Tweetnacl.ListsOp Require Import Export.
From stdpp Require Import list.
Require Import ssreflect.

6
From Tweetnacl.Low Require Import AMZubSqSel_Correct.
7
From Tweetnacl.Gen Require Import AMZubSqSel_Prop.
Benoit Viguier's avatar
Benoit Viguier committed
8
From Tweetnacl.Gen Require Import AMZubSqSel_List.
9
10
11
12
From Tweetnacl.Gen Require Import ABCDEF.
From Tweetnacl.Gen Require Import abstract_fn_rev.
From Tweetnacl.Gen Require Import abstract_fn_rev_eq.
From Tweetnacl.Gen Require Import abstract_fn_rev_abcdef.
Benoit Viguier's avatar
Benoit Viguier committed
13
14
From Tweetnacl.Gen Require Import montgomery_rec.
From Tweetnacl.Gen Require Import montgomery_rec_eq.
Benoit Viguier's avatar
Benoit Viguier committed
15
From Tweetnacl.Low Require Import M.
16
17
18
19
20
21
From Tweetnacl.Low Require Import Pack25519.
From Tweetnacl.Low Require Import Unpack25519.
From Tweetnacl.Low Require Import Inv25519.
From Tweetnacl.Low Require Import ScalarMult_rev.
From Tweetnacl.Low Require Import Constant.
From Tweetnacl.Low Require Import Prep_n.
22
From Tweetnacl.Low Require Import GetBit.
23
From Tweetnacl.Low Require Import Get_abcdef.
Benoit Viguier's avatar
Benoit Viguier committed
24
From Tweetnacl.Low Require Import List16.
25
From Tweetnacl.Low Require Import ScalarMult_gen_small.
26
27
28
29
From Tweetnacl.Mid Require Import Unpack25519.
From Tweetnacl.Mid Require Import Pack25519.
From Tweetnacl.Mid Require Import Inv25519.
From Tweetnacl.Mid Require Import Prep_n.
30
From Tweetnacl.Mid Require Import GetBit.
31
From Tweetnacl.Mid Require Import Crypto_Scalarmult.
Benoit Viguier's avatar
Benoit Viguier committed
32
From Tweetnacl.Mid Require Import AMZubSqSel.
33
From Tweetnacl.Mid Require Import ScalarMult.
34
From Tweetnacl.Low Require Import Crypto_Scalarmult_lemmas.
Benoit Viguier's avatar
Benoit Viguier committed
35
From Tweetnacl.Mid Require Import Mod.
Benoit Viguier's avatar
Benoit Viguier committed
36
From Tweetnacl.Mid Require Import Instances.
37

38
Open Scope Z.
39

Benoit Viguier's avatar
Benoit Viguier committed
40
41
(* Real version for proof *)
Definition Crypto_Scalarmult_proof n p :=
Benoit Viguier's avatar
Benoit Viguier committed
42
43
44
  let a := get_a (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p)) in
  let c := get_c (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p)) in
  Pack25519 (Low.M a (Inv25519 c)).
45

Benoit Viguier's avatar
Benoit Viguier committed
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(* Pretty version for Paper *)
Definition Crypto_Scalarmult n p :=
  let a := get_a (montgomery_rec 255 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p)) in
  let c := get_c (montgomery_rec 255 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p)) in
  Pack25519 (Low.M a (Inv25519 c)).

(* Proof of equivalence between the two *)
Lemma Crypto_Scalarmult_eq : forall n p, 
  Crypto_Scalarmult_proof n p = Crypto_Scalarmult n p.
Proof.
  move => n p.
  rewrite /Crypto_Scalarmult_proof /Crypto_Scalarmult.
  apply f_equal.
  apply f_equal2.
  2: apply f_equal.
  all: apply f_equal.
  all: rewrite /montgomery_fn.
  all: change 255 with (254+1).
  all: rewrite -montgomery_rec_eq_fn_rev ; f_equal; omega.
Qed.

Benoit Viguier's avatar
WIP    
Benoit Viguier committed
67
Local Lemma impl_omega_simpl_0 :  x : , (λ x0 : , 0  x0  x0 < 2 ^ 16) x  -38  x  x < 2 ^ 16 + 38.
68
69
70
71
72
73
74
Proof.
  intros ; simpl in *.
  change (2^16 + 38) with 65574.
  change (2^16) with 65536 in H.
  omega.
Qed.

Benoit Viguier's avatar
WIP    
Benoit Viguier committed
75
Local Lemma impl_omega_simpl_1 :  x : , (λ x0 : , -38  x0  x0 < 2 ^ 16 + 38) x  - 2 ^ 26 < x  x < 2 ^ 26.
76
77
78
79
80
81
82
Proof.
  intros ; simpl in *.
  change (2^16 + 38) with 65574 in H.
  change (2^26) with 67108864.
  omega.
Qed.

Benoit Viguier's avatar
WIP    
Benoit Viguier committed
83
Local Lemma impl_omega_simpl_2 :  x : , (λ x0 : , -38  x0  x0 < 2 ^ 16 + 38) x  - 2 ^ 62 < x  x < 2 ^ 62.
84
85
86
87
88
89
90
Proof.
  intros ; simpl in *.
  change (2^16 + 38) with 65574 in H.
  change (2^62) with 4611686018427387904.
  omega.
Qed.

Benoit Viguier's avatar
Benoit Viguier committed
91
92
93
Local Lemma Zlength_a : forall n p,
  Zlength n = 32 ->
  Zlength p = 32 ->
Benoit Viguier's avatar
Benoit Viguier committed
94
Zlength (get_a (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p))) = 16.
Benoit Viguier's avatar
Benoit Viguier committed
95
96
Proof.
  intros.
Benoit Viguier's avatar
Benoit Viguier committed
97
98
99
  apply get_a_montgomery_fn_Zlength => //.
  apply List_Z_Ops_Prop.
  all: apply Unpack25519_Zlength => //.
Benoit Viguier's avatar
Benoit Viguier committed
100
Qed.
Benoit Viguier's avatar
Benoit Viguier committed
101

Benoit Viguier's avatar
Benoit Viguier committed
102
103
104
Local Lemma Zlength_c : forall n p,
  Zlength n = 32 ->
  Zlength p = 32 ->
Benoit Viguier's avatar
Benoit Viguier committed
105
Zlength (get_c (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p))) = 16.
Benoit Viguier's avatar
Benoit Viguier committed
106
107
Proof.
  intros.
Benoit Viguier's avatar
Benoit Viguier committed
108
109
110
  apply get_c_montgomery_fn_Zlength => //.
  apply List_Z_Ops_Prop.
  all: apply Unpack25519_Zlength => //.
Benoit Viguier's avatar
Benoit Viguier committed
111
112
Qed.

Benoit Viguier's avatar
Benoit Viguier committed
113
Local Lemma C_1_bound_ext: Forall (λ x : , -38  x  x < 2 ^ 16 + 38) Low.C_1.
Benoit Viguier's avatar
Benoit Viguier committed
114
115
116
Proof.
repeat rewrite Forall_cons ; jauto_set ; try apply Forall_nil ; compute ; go.
Qed.
Benoit Viguier's avatar
Benoit Viguier committed
117
Local Lemma C_0_bound_ext: Forall (λ x : , -38  x  x < 2 ^ 16 + 38) Low.C_0.
Benoit Viguier's avatar
Benoit Viguier committed
118
119
120
121
122
Proof.
repeat rewrite Forall_cons ; jauto_set ; try apply Forall_nil ; compute ; go.
Qed.

Local Lemma M_bounded :  forall (n p:list Z),
123
124
125
126
  Zlength n = 32 ->
  Zlength p = 32 ->
  Forall (λ x : , 0  x  x < 2 ^ 8) n ->
  Forall (λ x : , 0  x  x < 2 ^ 8) p ->
Benoit Viguier's avatar
Benoit Viguier committed
127
Forall (λ x : , - 2 ^ 62 < x  x < 2 ^ 62)
Benoit Viguier's avatar
Benoit Viguier committed
128
  (Low.M
Benoit Viguier's avatar
Benoit Viguier committed
129
     (get_a
Benoit Viguier's avatar
Benoit Viguier committed
130
        (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p)))
Benoit Viguier's avatar
Benoit Viguier committed
131
132
     (Inv25519
        (get_c
Benoit Viguier's avatar
Benoit Viguier committed
133
           (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0
Benoit Viguier's avatar
Benoit Viguier committed
134
              (Unpack25519 p))))).
135
136
Proof.
  intros n p Hln Hlp Hbn Hbp.
Benoit Viguier's avatar
Benoit Viguier committed
137
138
139
  have HUnpack:= Unpack25519_bounded p Hbp.
  have HUnpackEx: Forall (λ x : , -38  x  x < 2 ^ 16 + 38) (Unpack25519 p).
    eapply list.Forall_impl => //.
140
141
    eassumption.
    apply impl_omega_simpl_0.
Benoit Viguier's avatar
Benoit Viguier committed
142
143
  have HlUnpackP: Zlength (Unpack25519 p) = 16.
    apply Unpack25519_Zlength => //.
144
145
146
147
  eapply list.Forall_impl.
  apply M_bound_Zlength.
  5: apply impl_omega_simpl_2.
  2: apply Inv25519_Zlength.
Benoit Viguier's avatar
Benoit Viguier committed
148
149
150
151
152
153
154
  2: apply Zlength_c => //.
  1: apply Zlength_a => //.
  all: eapply list.Forall_impl.
  3: apply Inv25519_bound_Zlength.
  3: apply Zlength_c => //.
  3: apply get_c_montgomery_fn_bound => //.
  apply get_a_montgomery_fn_bound => //.
Benoit Viguier's avatar
Benoit Viguier committed
155
  1, 6: apply List_Z_Ops_Prop.
Benoit Viguier's avatar
Benoit Viguier committed
156
157
158
  all: try apply C_0_bound_ext.
  all: try apply C_1_bound_ext.
  all: apply impl_omega_simpl_1.
Benoit Viguier's avatar
Benoit Viguier committed
159
160
Qed.

Benoit Viguier's avatar
Benoit Viguier committed
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
Local Lemma get_a_abstract_fn_montgomery_fn n p:
Zlength n = 32 ->
Zlength p = 32 ->
Forall (λ x : , 0  x  x < 2 ^ 8) n ->
Forall (λ x : , 0  x  x < 2 ^ 8) p ->
Forall (λ x : , 0  x  x < 2 ^ 16) (Unpack25519 p) ->
Forall (λ x : , 0  x  x < 2 ^ 8) (clamp n) ->
Forall (λ x : , -38  x  x < 2 ^ 16 + 38) (Unpack25519 p) ->
Zlength (Unpack25519 p) = 16 ->
get_a
  (abstract_fn_rev 255 254 (Zclamp (ZofList 8 n)) 1 (ZUnpack25519 (ZofList 8 p)) 0 1 0 0
     (ZUnpack25519 (ZofList 8 p))) `mod` (2 ^ 255 - 19) =
(16.lst get_a
           (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0
              (Unpack25519 p))) `mod` (2 ^ 255 - 19).
Proof.
move => Hln Hlp Hbn Hbp HUnpack HCn HUnpackEx HlUnpackP.
rewrite /Zmontgomery_fn /montgomery_fn.
have H255: 0 <= 255 by omega.
rewrite Zlength_correct in Hln.
rewrite Zlength_correct in Hlp.
rewrite clamp_ZofList_eq ?Unpack25519_eq_ZUnpack25519 => // ; try omega.
symmetry.
apply (abstract_fn_rev_eq_List_Z_a (fun x => Z.modulo x (Z.pow 2 255 - 19)) Z_Ops List_Z_Ops List_Z_Ops_Prop List_Z_Ops_Prop_Correct) => //.
Qed.

Local Lemma get_c_abstract_fn_montgomery_fn n p:
Zlength n = 32 ->
Zlength p = 32 ->
Forall (λ x : , 0  x  x < 2 ^ 8) n ->
Forall (λ x : , 0  x  x < 2 ^ 8) p ->
Forall (λ x : , 0  x  x < 2 ^ 16) (Unpack25519 p) ->
Forall (λ x : , 0  x  x < 2 ^ 8) (clamp n) ->
Forall (λ x : , -38  x  x < 2 ^ 16 + 38) (Unpack25519 p) ->
Zlength (Unpack25519 p) = 16 ->
ZInv25519
  (get_c
     (abstract_fn_rev 255 254 (Zclamp (ZofList 8 n)) 1 (ZUnpack25519 (ZofList 8 p)) 0 1 0 0
        (ZUnpack25519 (ZofList 8 p)))) `mod` (2 ^ 255 - 19) =
(16.lst Inv25519
           (get_c
              (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0
                 Low.C_0 (Unpack25519 p)))) `mod` (2 ^ 255 - 19).
Proof.
move => Hln Hlp Hbn Hbp HUnpack HCn HUnpackEx HlUnpackP.
rewrite Inv25519_Z_GF.
2: by apply Zlength_c.
rewrite Inv25519_Z_correct /ZInv25519 pow_mod.
symmetry.
rewrite pow_mod.
2,3: by compute.
f_equal ; f_equal.
have H255: 0 <= 255 by omega.
rewrite Zlength_correct in Hln.
rewrite Zlength_correct in Hlp.
rewrite /Zmontgomery_fn /montgomery_fn clamp_ZofList_eq ?Unpack25519_eq_ZUnpack25519 => // ; try omega.
apply (abstract_fn_rev_eq_List_Z_c (fun x => Z.modulo x (Z.pow 2 255 - 19)) Z_Ops List_Z_Ops List_Z_Ops_Prop List_Z_Ops_Prop_Correct) => //.
Qed.

220
Theorem Crypto_Scalarmult_Eq : forall (n p:list Z),
Benoit Viguier's avatar
Benoit Viguier committed
221
222
223
224
  Zlength n = 32 ->
  Zlength p = 32 ->
  Forall (λ x : , 0  x  x < 2 ^ 8) n ->
  Forall (λ x : , 0  x  x < 2 ^ 8) p ->
Benoit Viguier's avatar
Benoit Viguier committed
225
  ZofList 8 (Crypto_Scalarmult_proof n p) = ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
Benoit Viguier's avatar
Benoit Viguier committed
226
Proof.
227
  intros n p Hln Hlp Hbn Hbp.
Benoit Viguier's avatar
Benoit Viguier committed
228
  rewrite /Crypto_Scalarmult_proof ZCrypto_Scalarmult_eq /ZCrypto_Scalarmult_rev_gen.
Benoit Viguier's avatar
Benoit Viguier committed
229
230
231
232
233
234
  have HUnpack:= Unpack25519_bounded p Hbp.
  have HCn:= clamp_bound n Hbn.
  have HUnpackEx: Forall (λ x : , -38  x  x < 2 ^ 16 + 38) (Unpack25519 p)
    by eapply list.Forall_impl ; [eassumption | apply impl_omega_simpl_0].
  have HlUnpackP: Zlength (Unpack25519 p) = 16
    by apply Unpack25519_Zlength.
Benoit Viguier's avatar
Benoit Viguier committed
235
236
237
238
239
240
  rewrite Pack25519_mod_25519.
  2: {
  apply M_Zlength.
  2: apply Inv25519_Zlength.
  2: apply Zlength_c ; assumption.
  1: apply Zlength_a ; assumption.
241
  }
Benoit Viguier's avatar
Benoit Viguier committed
242
  2: apply M_bounded ; assumption.
243
244
245
  rewrite /ZPack25519.
  rewrite mult_GF_Zlengh.
  3: apply Inv25519_Zlength.
Benoit Viguier's avatar
Benoit Viguier committed
246
247
  2: apply Zlength_a ; assumption.
  2: apply Zlength_c ; assumption.
248
249
250
251
252
  rewrite -Zmult_mod_idemp_l.
  rewrite -Zmult_mod_idemp_r.
  symmetry.
  rewrite -Zmult_mod_idemp_l.
  rewrite -Zmult_mod_idemp_r.
Benoit Viguier's avatar
Benoit Viguier committed
253
254
  Opaque abstract_fn_rev.
  Opaque montgomery_fn.
255
256
  f_equal.
  f_equal.
Benoit Viguier's avatar
Benoit Viguier committed
257
258
  apply get_a_abstract_fn_montgomery_fn => //.
  apply get_c_abstract_fn_montgomery_fn => //.
Benoit Viguier's avatar
Benoit Viguier committed
259
Qed.
Benoit Viguier's avatar
Benoit Viguier committed
260
261

Close Scope Z.