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
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
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
|
Require Import Coq.micromega.Lia.
Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Proofs.
Require Import Crypto.Arithmetic.Core. Import B.
Require Import Crypto.Util.Sigma.Lift.
Require Import Coq.ZArith.BinInt.
Require Import Coq.PArith.BinPos.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.ZUtil.ModInv.
Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.BreakMatch.
Definition wt (i:nat) : Z := Z.shiftl 1 (64*Z.of_nat i).
Definition r := Eval compute in (2^64)%positive.
Definition sz := 4%nat.
Definition m : positive := 2^256-2^224+2^192+2^96-1.
Definition p256 :=
Eval vm_compute in
((Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m))).
Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m).
Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z.
Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)).
Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z.
Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = Saturated.eval (n:=sz) (Z.pos r) p256.
Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod Saturated.eval (n:=sz) (Z.pos r) p256 = 1)%Z.
Proof. vm_compute; reflexivity. Qed.
Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| forall (A B : Tuple.tuple Z sz),
f A B =
(redc (r:=r)(R_numlimbs:=sz) p256 A B m')
}.
Proof.
eapply (lift2_sig (fun A B c => c = _)); eexists.
cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
(*
cbv [
r wt sz p256
CPSUtil.Tuple.tl_cps CPSUtil.Tuple.hd_cps
CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' CPSUtil.flat_map_cps CPSUtil.fold_right_cps
CPSUtil.map_cps CPSUtil.Tuple.left_append_cps CPSUtil.firstn_cps CPSUtil.combine_cps CPSUtil.on_tuple_cps CPSUtil.update_nth_cps CPSUtil.from_list_default_cps CPSUtil.from_list_default'_cps
fst snd length List.seq List.hd List.app
redc redc_cps redc_loop_cps redc_body_cps
Positional.to_associational_cps
Saturated.divmod_cps
Saturated.scmul_cps
Saturated.uweight
Saturated.Columns.mul_cps
Saturated.Associational.mul_cps
(*Z.of_nat Pos.of_succ_nat Nat.pred
Z.pow Z.pow_pos Z.mul Pos.iter Pos.mul Pos.succ*)
Tuple.hd Tuple.append Tuple.tl Tuple.hd' Tuple.tl' CPSUtil.Tuple.left_tl_cps CPSUtil.Tuple.left_hd_cps CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps
Saturated.Columns.from_associational_cps
Saturated.Associational.multerm_cps
Saturated.Columns.compact_cps
Saturated.Columns.compact_step_cps
Saturated.Columns.compact_digit_cps
Saturated.drop_high_cps
Saturated.add_cps
Saturated.Columns.add_cps
Saturated.Columns.cons_to_nth_cps
Nat.pred
Saturated.join0
Saturated.join0_cps CPSUtil.Tuple.left_append_cps
CPSUtil.Tuple.mapi_with_cps
id
Positional.zeros Saturated.zero Saturated.Columns.nils Tuple.repeat Tuple.append
Positional.place_cps
CPSUtil.Tuple.mapi_with'_cps Tuple.hd Tuple.hd' Tuple.tl Tuple.tl' CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps fst snd
Z.of_nat fst snd Z.pow Z.pow_pos Pos.of_succ_nat Z.div Z.mul Pos.mul Z.modulo Z.div_eucl Z.pos_div_eucl Z.leb Z.compare Pos.compare_cont Pos.compare Z.pow_pos Pos.iter Z.mul Pos.succ Z.ltb Z.gtb Z.geb Z.div Z.sub Z.pos_sub Z.add Z.opp Z.double
Decidable.dec Decidable.dec_eq_Z Z.eq_dec Z_rec Z_rec Z_rect
Positional.zeros Saturated.zero Saturated.Columns.nils Tuple.repeat Tuple.append
(*
Saturated.Associational.multerm_cps
Saturated.Columns.from_associational_cps Positional.place_cps Saturated.Columns.cons_to_nth_cps Saturated.Columns.nils
Tuple.append
Tuple.from_list Tuple.from_list'
Tuple.from_list_default Tuple.from_list_default'
Tuple.hd
Tuple.repeat
Tuple.tl
Tuple.tuple *)
(* Saturated.add_cps Saturated.divmod_cps Saturated.drop_high_cps Saturated.scmul_cps Saturated.zero Saturated.Columns.mul_cps Saturated.Columns.add_cps Saturated.uweight Saturated.T *)
(*
CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps'
Positional.zeros
Tuple.to_list
Tuple.to_list'
List.hd
List.tl
Nat.max
Positional.to_associational_cps
Z.of_nat *)
].
Unset Printing Notations.
(* cbv -[runtime_add runtime_mul LetIn.Let_In Definitions.Z.add_get_carry_full Definitions.Z.mul_split]. *)
(* basesystem_partial_evaluation_RHS. *)
*)
reflexivity.
Defined.
Definition mulmod_256'' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| forall (A B : Tuple.tuple Z sz),
Saturated.small (Z.pos r) A -> Saturated.small (Z.pos r) B ->
let eval := Saturated.eval (Z.pos r) in
(Saturated.small (Z.pos r) (f A B)
/\ (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)
/\ (eval (f A B) mod Z.pos m
= (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
}.
Proof.
exists (proj1_sig mulmod_256').
abstract (
intros; rewrite (proj2_sig mulmod_256');
split; [ | split ];
[ apply small_redc with (ri:=r') | apply redc_bound_N with (ri:=r') | apply redc_mod_N ];
try match goal with
| _ => assumption
| [ |- _ = _ :> Z ] => vm_compute; reflexivity
| _ => reflexivity
| [ |- Saturated.small (Z.pos r) p256 ]
=> hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
subst; try lia
| [ |- Saturated.eval (Z.pos r) p256 <> 0%Z ]
=> vm_compute; lia
end
).
Defined.
Definition add' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| forall (A B : Tuple.tuple Z sz),
f A B =
(add (r:=r)(R_numlimbs:=sz) p256 A B)
}.
Proof.
eapply (lift2_sig (fun A B c => c = _)); eexists.
cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
reflexivity.
Defined.
Definition sub' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| forall (A B : Tuple.tuple Z sz),
f A B =
(sub (r:=r) (R_numlimbs:=sz) p256 A B)
}.
Proof.
eapply (lift2_sig (fun A B c => c = _)); eexists.
cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
reflexivity.
Defined.
Definition opp' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
| forall (A : Tuple.tuple Z sz),
f A =
(opp (r:=r) (R_numlimbs:=sz) p256 A)
}.
Proof.
eapply (lift1_sig (fun A c => c = _)); eexists.
cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
reflexivity.
Defined.
Definition nonzero' : { f:Tuple.tuple Z sz -> Z
| forall (A : Tuple.tuple Z sz),
f A =
(nonzero (R_numlimbs:=sz) A)
}.
Proof.
eapply (lift1_sig (fun A c => c = _)); eexists.
cbv -[runtime_lor Let_In].
reflexivity.
Defined.
Import ModularArithmetic.
(*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
(B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
Saturated.small (Z.pos r) (f A B)
/\ (let eval := Saturated.eval (Z.pos r) in
0 <= eval (f A B) < Z.pos r^Z.of_nat sz
/\ (eval (f A B) mod Z.pos m
= (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
}.
Proof.*)
(** TODO: MOVE ME *)
Definition montgomery_to_F (v : Z) : F m
:= (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| let eval := Saturated.eval (Z.pos r) in
(forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
(B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
montgomery_to_F (eval (f A B))
= (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
/\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
(B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
(eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
Proof.
exists (proj1_sig mulmod_256'').
abstract (
split; intros A Asm B Bsm;
pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H;
cbv zeta in *;
try solve [ destruct_head'_and; assumption ];
rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H;
unfold montgomery_to_F;
destruct H as [H1 [H2 H3]];
rewrite H3;
rewrite <- !ModularArithmeticTheorems.F.of_Z_mul;
f_equal; nia
).
Defined.
Local Ltac t_fin :=
[ > reflexivity
| repeat match goal with
| _ => assumption
| [ |- _ = _ :> Z ] => vm_compute; reflexivity
| _ => reflexivity
| [ |- Saturated.small (Z.pos r) p256 ]
=> hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
subst; try lia
| [ |- Saturated.eval (Z.pos r) p256 <> 0%Z ]
=> vm_compute; lia
| [ |- and _ _ ] => split
| [ |- (0 <= Saturated.eval (Z.pos r) _)%Z ] => apply Saturated.eval_small
end.. ].
Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| let eval := Saturated.eval (Z.pos r) in
((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
(B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
(eval A < eval p256
-> eval B < eval p256
-> montgomery_to_F (eval (f A B))
= (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
/\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
(B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
(eval A < eval p256
-> eval B < eval p256
-> 0 <= eval (f A B) < eval p256)))%Z }.
Proof.
exists (proj1_sig add').
abstract (
split; intros; rewrite (proj2_sig add');
unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_add;
rewrite <- ?Z.mul_add_distr_r;
[ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_add_mod_N; pull_Zmod
| apply add_bound ];
t_fin
).
Defined.
Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
| let eval := Saturated.eval (Z.pos r) in
((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
(B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
(eval A < eval p256
-> eval B < eval p256
-> montgomery_to_F (eval (f A B))
= (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
/\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
(B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
(eval A < eval p256
-> eval B < eval p256
-> 0 <= eval (f A B) < eval p256)))%Z }.
Proof.
exists (proj1_sig sub').
abstract (
split; intros; rewrite (proj2_sig sub');
unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_sub;
rewrite <- ?Z.mul_sub_distr_r;
[ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_sub_mod_N; pull_Zmod
| apply sub_bound ];
t_fin
).
Defined.
Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
| let eval := Saturated.eval (Z.pos r) in
((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
(eval A < eval p256
-> montgomery_to_F (eval (f A))
= (F.opp (montgomery_to_F (eval A)))%F))
/\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
(eval A < eval p256
-> 0 <= eval (f A) < eval p256)))%Z }.
Proof.
exists (proj1_sig opp').
abstract (
split; intros; rewrite (proj2_sig opp');
unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?F_of_Z_opp;
rewrite <- ?Z.mul_opp_l;
[ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_opp_mod_N; pull_Zmod
| apply opp_bound ];
t_fin
).
Defined.
Definition nonzero : { f:Tuple.tuple Z sz -> Z
| let eval := Saturated.eval (Z.pos r) in
forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
(eval A < eval p256
-> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
Proof.
exists (proj1_sig nonzero').
abstract (
intros eval A H **; rewrite (proj2_sig nonzero'), (@eval_nonzero r) by (eassumption || reflexivity);
subst eval;
unfold montgomery_to_F, Saturated.uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256;
let H := fresh in
split; intro H;
[ rewrite H; autorewrite with zsimplify_const; reflexivity
| cut ((Saturated.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod Saturated.eval (n:=sz) (Z.pos r) p256 = 0)%Z;
[ rewrite Z.mul_mod, r'_pow_correct; autorewrite with zsimplify_const; pull_Zmod; [ | vm_compute; congruence ];
rewrite Z.mod_small; [ trivial | split; try assumption; apply Saturated.eval_small; try assumption; lia ]
| rewrite Z.mul_assoc, Z.mul_mod, H by (vm_compute; congruence); autorewrite with zsimplify_const; reflexivity ] ]
).
Defined.
Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero).
Print Assumptions for_assumptions.
|
