Crypto_Scalarmult.v 8.71 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
From Tweetnacl.Low Require Import M.
14
15
16
17
18
19
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.
20
From Tweetnacl.Low Require Import GetBit.
21
From Tweetnacl.Low Require Import Get_abcdef.
Benoit Viguier's avatar
Benoit Viguier committed
22
From Tweetnacl.Low Require Import List16.
23
From Tweetnacl.Low Require Import ScalarMult_gen_small.
24
25
26
27
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.
28
From Tweetnacl.Mid Require Import GetBit.
29
From Tweetnacl.Mid Require Import Crypto_Scalarmult.
Benoit Viguier's avatar
Benoit Viguier committed
30
From Tweetnacl.Mid Require Import AMZubSqSel.
31
From Tweetnacl.Mid Require Import ScalarMult.
32
From Tweetnacl.Low Require Import Crypto_Scalarmult_lemmas.
Benoit Viguier's avatar
Benoit Viguier committed
33
From Tweetnacl.Mid Require Import Mod.
Benoit Viguier's avatar
Benoit Viguier committed
34
From Tweetnacl.Mid Require Import Instances.
35

36
Open Scope Z.
37

Benoit Viguier's avatar
typo...    
Benoit Viguier committed
38
Definition Crypto_Scalarmult n p :=
Benoit Viguier's avatar
Benoit Viguier committed
39
40
41
  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)).
42

Benoit Viguier's avatar
WIP    
Benoit Viguier committed
43
Local Lemma impl_omega_simpl_0 :  x : , (λ x0 : , 0  x0  x0 < 2 ^ 16) x  -38  x  x < 2 ^ 16 + 38.
44
45
46
47
48
49
50
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
51
Local Lemma impl_omega_simpl_1 :  x : , (λ x0 : , -38  x0  x0 < 2 ^ 16 + 38) x  - 2 ^ 26 < x  x < 2 ^ 26.
52
53
54
55
56
57
58
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
59
Local Lemma impl_omega_simpl_2 :  x : , (λ x0 : , -38  x0  x0 < 2 ^ 16 + 38) x  - 2 ^ 62 < x  x < 2 ^ 62.
60
61
62
63
64
65
66
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
67
68
69
Local Lemma Zlength_a : forall n p,
  Zlength n = 32 ->
  Zlength p = 32 ->
Benoit Viguier's avatar
Benoit Viguier committed
70
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
71
72
Proof.
  intros.
Benoit Viguier's avatar
Benoit Viguier committed
73
74
75
  apply get_a_montgomery_fn_Zlength => //.
  apply List_Z_Ops_Prop.
  all: apply Unpack25519_Zlength => //.
Benoit Viguier's avatar
Benoit Viguier committed
76
Qed.
Benoit Viguier's avatar
Benoit Viguier committed
77

Benoit Viguier's avatar
Benoit Viguier committed
78
79
80
Local Lemma Zlength_c : forall n p,
  Zlength n = 32 ->
  Zlength p = 32 ->
Benoit Viguier's avatar
Benoit Viguier committed
81
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
82
83
Proof.
  intros.
Benoit Viguier's avatar
Benoit Viguier committed
84
85
86
  apply get_c_montgomery_fn_Zlength => //.
  apply List_Z_Ops_Prop.
  all: apply Unpack25519_Zlength => //.
Benoit Viguier's avatar
Benoit Viguier committed
87
88
Qed.

Benoit Viguier's avatar
Benoit Viguier committed
89
Local Lemma C_1_bound_ext: Forall (λ x : , -38  x  x < 2 ^ 16 + 38) Low.C_1.
Benoit Viguier's avatar
Benoit Viguier committed
90
91
92
Proof.
repeat rewrite Forall_cons ; jauto_set ; try apply Forall_nil ; compute ; go.
Qed.
Benoit Viguier's avatar
Benoit Viguier committed
93
Local Lemma C_0_bound_ext: Forall (λ x : , -38  x  x < 2 ^ 16 + 38) Low.C_0.
Benoit Viguier's avatar
Benoit Viguier committed
94
95
96
97
98
Proof.
repeat rewrite Forall_cons ; jauto_set ; try apply Forall_nil ; compute ; go.
Qed.

Local Lemma M_bounded :  forall (n p:list Z),
99
100
101
102
  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
103
Forall (λ x : , - 2 ^ 62 < x  x < 2 ^ 62)
Benoit Viguier's avatar
Benoit Viguier committed
104
  (Low.M
Benoit Viguier's avatar
Benoit Viguier committed
105
     (get_a
Benoit Viguier's avatar
Benoit Viguier committed
106
        (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
107
108
     (Inv25519
        (get_c
Benoit Viguier's avatar
Benoit Viguier committed
109
           (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
110
              (Unpack25519 p))))).
111
112
Proof.
  intros n p Hln Hlp Hbn Hbp.
Benoit Viguier's avatar
Benoit Viguier committed
113
114
115
  have HUnpack:= Unpack25519_bounded p Hbp.
  have HUnpackEx: Forall (λ x : , -38  x  x < 2 ^ 16 + 38) (Unpack25519 p).
    eapply list.Forall_impl => //.
116
117
    eassumption.
    apply impl_omega_simpl_0.
Benoit Viguier's avatar
Benoit Viguier committed
118
119
  have HlUnpackP: Zlength (Unpack25519 p) = 16.
    apply Unpack25519_Zlength => //.
120
121
122
123
  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
124
125
126
127
128
129
130
  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
131
  1, 6: apply List_Z_Ops_Prop.
Benoit Viguier's avatar
Benoit Viguier committed
132
133
134
  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
135
136
Qed.

Benoit Viguier's avatar
Benoit Viguier committed
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
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
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.

196
Theorem Crypto_Scalarmult_Eq : forall (n p:list Z),
Benoit Viguier's avatar
Benoit Viguier committed
197
198
199
200
  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
201
  ZofList 8 (Crypto_Scalarmult n p) = ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
Benoit Viguier's avatar
Benoit Viguier committed
202
Proof.
203
  intros n p Hln Hlp Hbn Hbp.
Benoit Viguier's avatar
Benoit Viguier committed
204
  rewrite /Crypto_Scalarmult ZCrypto_Scalarmult_eq /ZCrypto_Scalarmult_rev_gen.
Benoit Viguier's avatar
Benoit Viguier committed
205
206
207
208
209
210
  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
211
212
213
214
215
216
  rewrite Pack25519_mod_25519.
  2: {
  apply M_Zlength.
  2: apply Inv25519_Zlength.
  2: apply Zlength_c ; assumption.
  1: apply Zlength_a ; assumption.
217
  }
Benoit Viguier's avatar
Benoit Viguier committed
218
  2: apply M_bounded ; assumption.
219
220
221
  rewrite /ZPack25519.
  rewrite mult_GF_Zlengh.
  3: apply Inv25519_Zlength.
Benoit Viguier's avatar
Benoit Viguier committed
222
223
  2: apply Zlength_a ; assumption.
  2: apply Zlength_c ; assumption.
224
225
226
227
228
  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
229
230
  Opaque abstract_fn_rev.
  Opaque montgomery_fn.
231
232
  f_equal.
  f_equal.
Benoit Viguier's avatar
Benoit Viguier committed
233
234
  apply get_a_abstract_fn_montgomery_fn => //.
  apply get_c_abstract_fn_montgomery_fn => //.
Benoit Viguier's avatar
Benoit Viguier committed
235
Qed.
Benoit Viguier's avatar
Benoit Viguier committed
236
237

Close Scope Z.