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
|
Require Import Coq.Bool.Bool.
Require Import Coq.derive.Derive.
Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
Require Import Coq.Lists.List. Import ListNotations.
Require Import Crypto.Fancy.Compiler.
Require Import Crypto.Fancy.Prod.
Require Import Crypto.Fancy.Spec.
Require Import Crypto.Language. Import Language.Compilers.
Require Import Crypto.LanguageWf.
Require Import Crypto.Arithmetic.FancyMontgomeryReduction.
Require Import Crypto.PushButtonSynthesis.FancyMontgomeryReduction.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.ZUtil.EquivModulo.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.Notations.
Local Open Scope Z_scope.
Module Montgomery256.
Definition N := Eval lazy in (2^256-2^224+2^192+2^96-1).
Definition N':= (115792089210356248768974548684794254293921932838497980611635986753331132366849).
Definition R := Eval lazy in (2^256).
Definition R' := 115792089183396302114378112356516095823261736990586219612555396166510339686400.
Definition machine_wordsize := 256.
Derive montred256
SuchThat (montred N R N' machine_wordsize = ErrorT.Success montred256)
As montred256_eq.
Proof. lazy; reflexivity. Qed.
Lemma montred256_correct :
COperationSpecifications.MontgomeryReduction.montred_correct N R R' (expr.Interp (@ident.gen_interp cast_oor) montred256).
Proof.
apply montred_correct with (n:=2%nat) (machine_wordsize:=machine_wordsize) (N':=N').
{ lazy. reflexivity. }
{ apply montred256_eq. }
Qed.
Lemma montred'_correct_specialized R' (R'_correct : Z.equiv_modulo N (R * R') 1) :
forall (lo hi : Z),
0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N ->
MontgomeryReduction.montred' N R N' (Z.log2 R) lo hi = ((lo + R * hi) * R') mod N.
Proof.
intros.
apply MontgomeryReduction.montred'_correct with (T:=lo + R * hi) (R':=R') (n:=2%nat);
try match goal with
| |- context[R'] => assumption
| |- context [lo] =>
try assumption; progress autorewrite with zsimplify cancel_pair; reflexivity
end; lazy; try split; congruence.
Qed.
Definition montred256_fancy' (RegMod RegPInv RegZero lo hi error : positive) :=
of_Expr 6%positive
(make_consts [(RegMod, N); (RegZero, 0); (RegPInv, N')])
montred256
(lo, (hi, tt))
error.
Derive montred256_fancy
SuchThat (forall RegMod RegPInv RegZero,
montred256_fancy RegMod RegPInv RegZero = montred256_fancy' RegMod RegPInv RegZero)
As montred256_fancy_eq.
Proof.
intros.
cbv [montred256_fancy'].
lazy - [ADD ADDC SUB MUL128LL MUL128LU MUL128UL MUL128UU RSHI SELC SELM SELL ADDM].
reflexivity.
Qed.
(* TODO: these tactics are duplicated; move them elsewhere (probably translation *)
Local Ltac wf_subgoal :=
repeat match goal with
| _ => progress cbn [fst snd]
| |- LanguageWf.Compilers.expr.wf _ _ _ =>
econstructor; try solve [econstructor]; [ ]
| |- LanguageWf.Compilers.expr.wf _ _ _ =>
solve [econstructor]
| |- In _ _ => auto 50 using in_eq, in_cons
end.
Local Ltac valid_expr_subgoal :=
repeat match goal with
| _ => progress intros
| |- context [valid_ident] => econstructor
| |- context[valid_scalar] => econstructor
| |- context [valid_carry] => econstructor
| _ => reflexivity
| |- _ <> None => cbn; congruence
| |- of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto]
end.
Lemma montred256_fancy_correct :
forall lo hi error,
0 <= lo < R ->
0 <= hi < R ->
0 <= lo + R * hi < R * N ->
let RegZero := 1%positive in
let RegMod := 2%positive in
let RegPInv := 3%positive in
let RegHi := 4%positive in
let RegLo := 5%positive in
let consts_list := [(RegMod, N); (RegZero, 0); (RegPInv, N')] in
let arg_list := [(RegHi, hi); (RegLo, lo)] in
let ctx := make_ctx (consts_list ++ arg_list) in
let carry_flag := false in
let last_wrote := (fun x : CC.code => RegZero) in
let cc := make_cc last_wrote ctx carry_flag in
interp Pos.eqb wordmax cc_spec (montred256_fancy RegMod RegPInv RegZero RegLo RegHi error) cc ctx = ((lo + R * hi) * R') mod N.
Proof.
intros.
rewrite montred256_fancy_eq.
cbv [montred256_fancy'].
rewrite <-montred256_correct by (auto; reflexivity).
eapply of_Expr_correct with (x2 := (lo, (hi, tt))).
{ cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
intuition; Prod.inversion_prod; subst; cbv. break_innermost_match; congruence. }
{ cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
intuition; Prod.inversion_prod; subst; cbv; congruence. }
{ cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo. tauto. }
{ cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
intuition; Prod.inversion_prod; subst; cbv; congruence. }
{ cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
match goal with |- context [_ mod ?m] => change m with (2 ^ machine_wordsize) end.
intuition; Prod.inversion_prod; subst; apply Z.mod_small; cbv; try split; congruence. }
{ cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
match goal with |- context [_ mod ?m] => change m with (2 ^ machine_wordsize) end.
assert (R <= 2 ^ machine_wordsize) by (cbv; congruence).
intuition; Prod.inversion_prod; subst; apply Z.mod_small; omega. }
{ cbn.
repeat match goal with
| _ => apply Compilers.expr.WfLetIn
| _ => progress wf_subgoal
| _ => econstructor
end. }
{ cbn. cbv [N' N].
repeat (econstructor; [ solve [valid_expr_subgoal] | intros ]).
econstructor. valid_expr_subgoal. }
{ reflexivity. }
Qed.
Import Spec.Registers.
Definition montred256_alloc' lo hi RegPInv :=
fun errorP errorR =>
allocate register
positive Pos.eqb
errorR
(montred256_fancy 1000%positive 1001%positive 1002%positive 1003%positive 1004%positive errorP)
[r2;r3;r4;r5;r6;r7;r8;r9;r10;r11;r12;r13;r14;r15;r16;r17;r18;r19;r20]
(fun n => if n =? 1000 then RegMod
else if n =? 1001 then RegPInv
else if n =? 1002 then RegZero
else if n =? 1003 then lo
else if n =? 1004 then hi
else errorR)%positive.
Derive montred256_alloc
SuchThat (montred256_alloc = montred256_alloc')
As montred256_alloc_eq.
Proof.
intros.
cbv [montred256_alloc' montred256_fancy].
cbn. subst montred256_alloc.
reflexivity.
Qed.
Local Notation interp := (interp reg_eqb wordmax cc_spec).
Lemma montred256_alloc_equivalent errorP errorR cc_start_state start_context :
forall lo hi y t1 t2 scratch RegPInv extra_reg,
NoDup [lo; hi; y; t1; t2; scratch; RegPInv; extra_reg; RegMod; RegZero] ->
0 <= start_context lo < R ->
0 <= start_context hi < R ->
0 <= start_context RegPInv < R ->
interp
(montred256_alloc r0 r1 r30 errorP errorR) cc_start_state
(fun r => if reg_eqb r r0
then start_context lo
else if reg_eqb r r1
then start_context hi
else if reg_eqb r r30
then start_context RegPInv
else start_context r)
= interp (Prod.MontRed256 lo hi y t1 t2 scratch RegPInv) cc_start_state start_context.
Proof.
intros. cbv [R] in *.
cbv [Prod.MontRed256 montred256_alloc].
(* Extract proofs that no registers are equal to each other *)
repeat match goal with
| H : NoDup _ |- _ => inversion H; subst; clear H
| H : ~ In _ _ |- _ => cbv [In] in H
| H : ~ (_ \/ _) |- _ => apply Decidable.not_or in H; destruct H
| H : ~ False |- _ => clear H
end.
Time repeat match goal with
| _ => progress prove_programs_equivalent
| _ => rewrite interp_Mul256 with (tmp2 := extra_reg) by
(match goal with
| |- _ <> _ => assumption || congruence
| _ => push_value_unused
end)
| _ => rewrite interp_Mul256x256 with (tmp2 := extra_reg) by
(match goal with
| |- _ <> _ => assumption || congruence
| _ => push_value_unused
end)
end.
cbn [Spec.interp]; simplify_with_register_properties.
reflexivity.
Qed.
Lemma prod_montred256_correct :
forall (cc_start_state : CC.state) (* starting carry flags can be anything *)
(start_context : register -> Z) (* starting register values *)
(lo hi y t1 t2 scratch RegPInv extra_reg : register), (* registers to use in computation *)
NoDup [lo; hi; y; t1; t2; scratch; RegPInv; extra_reg; RegMod; RegZero] -> (* registers must be distinct *)
start_context RegPInv = N' -> (* RegPInv needs to hold the inverse of the modulus *)
start_context RegMod = N -> (* RegMod needs to hold the modulus *)
start_context RegZero = 0 -> (* RegZero needs to hold zero *)
(0 <= start_context lo < R) -> (* low half of the input is in bounds (R=2^256) *)
(0 <= start_context hi < R) -> (* high half of the input is in bounds (R=2^256) *)
let x := (start_context lo) + R * (start_context hi) in (* x is the input (split into two registers) *)
(0 <= x < R * N) -> (* input precondition *)
(interp (Prod.MontRed256 lo hi y t1 t2 scratch RegPInv) cc_start_state start_context = (x * R') mod N).
Proof.
intros. subst x.
erewrite <-montred256_fancy_correct with (error:=100000%positive) by eauto.
rewrite <-montred256_alloc_equivalent with (errorR := RegZero) (errorP := 1%positive) (extra_reg:=extra_reg)
by (cbv [R N N'] in *; auto with omega).
(* TODO: factor out this tactic *)
match goal with
|- context [make_cc ?last_wrote ?ctx ?carry] =>
let e := fresh in
let He := fresh in
remember (make_cc last_wrote ctx carry) as e eqn:He;
cbv [make_ctx app make_cc] in He;
cbn [Pos.eqb] in He; autorewrite with zsimplify in He;
subst e
end.
cbv [montred256_alloc montred256_fancy].
repeat match goal with
H : context [start_context] |- _ =>
rewrite <-H end.
repeat step.
reflexivity.
Qed.
End Montgomery256.
Import Registers.
(* Notations to make code more readable *)
Local Notation "i rd x y ; cont" := (Instr i rd (x, y) cont) (at level 40, cont at level 200, format "i rd x y ; '//' cont").
Local Notation "i rd x y z ; cont" := (Instr i rd (x, y, z) cont) (at level 40, cont at level 200, format "i rd x y z ; '//' cont").
(* Montgomery reference code : *)
Eval cbv beta iota delta [Prod.MontRed256 Prod.Mul256 Prod.Mul256x256] in Prod.MontRed256.
(*
= fun lo hi y t1 t2 scratch RegPInv : register =>
MUL128LL y lo RegPInv;
MUL128UL t1 lo RegPInv;
ADD 128 y y t1;
MUL128LU t1 lo RegPInv;
ADD 128 y y t1;
MUL128LL t1 y RegMod;
MUL128UU t2 y RegMod;
MUL128UL scratch y RegMod;
ADD 128 t1 t1 scratch;
ADDC (-128) t2 t2 scratch;
MUL128LU scratch y RegMod;
ADD 128 t1 t1 scratch;
ADDC (-128) t2 t2 scratch;
ADD 0 lo lo t1;
ADDC 0 hi hi t2;
SELC y RegMod RegZero;
SUB 0 lo hi y;
ADDM lo lo RegZero RegMod;
Ret lo
*)
(* Uncomment to see proof statement and remaining admitted statements,
or search for "prod_montred256_correct" to see comments on the proof
preconditions. *)
(*
Check Montgomery256.prod_montred256_correct.
Print Assumptions Montgomery256.prod_montred256_correct.
*)
|
