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
|
(** * Push-Button Synthesis of Saturated Solinas *)
Require Import Coq.Strings.String.
Require Import Coq.micromega.Lia.
Require Import Coq.ZArith.ZArith.
Require Import Coq.MSets.MSetPositive.
Require Import Coq.Lists.List.
Require Import Coq.QArith.QArith_base Coq.QArith.Qround.
Require Import Coq.derive.Derive.
Require Import Crypto.Util.ErrorT.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.ListUtil.FoldBool.
Require Import Crypto.Util.Strings.Decimal.
Require Import Crypto.Util.Strings.Equality.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.Zselect.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.Tactics.HasBody.
Require Import Crypto.Util.Tactics.Head.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.LanguageWf.
Require Import Crypto.Language.
Require Import Crypto.AbstractInterpretation.
Require Import Crypto.CStringification.
Require Import Crypto.Arithmetic.
Require Import Crypto.BoundsPipeline.
Require Import Crypto.COperationSpecifications.
Require Import Crypto.PushButtonSynthesis.ReificationCache.
Require Import Crypto.PushButtonSynthesis.Primitives.
Require Import Crypto.PushButtonSynthesis.SaturatedSolinasReificationCache.
Import ListNotations.
Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope.
Import
LanguageWf.Compilers
Language.Compilers
AbstractInterpretation.Compilers
CStringification.Compilers.
Import Compilers.defaults.
Import COperationSpecifications.Primitives.
Import COperationSpecifications.Solinas.
Import COperationSpecifications.SaturatedSolinas.
Import Associational Positional.
Local Coercion Z.of_nat : nat >-> Z.
Local Coercion QArith_base.inject_Z : Z >-> Q.
Local Coercion Z.pos : positive >-> Z.
Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *)
Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *)
(* needed for making [autorewrite] with [Set Keyed Unification] fast *)
Local Opaque expr.Interp.
Section __.
Context (s : Z)
(c : list (Z * Z))
(machine_wordsize : Z).
(* We include [0], so that even after bounds relaxation, we can
notice where the constant 0s are, and remove them. *)
Definition possible_values_of_machine_wordsize
:= [0; 1; machine_wordsize]%Z.
Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)).
Let m := s - Associational.eval c.
(* Number of reductions is calculated as follows :
Let i be the highest limb index of c. Then, each reduction
decreases the number of extra limbs by (n-i). So, to go from
the n extra limbs we have post-multiplication down to 0, we
need ceil (n / (n - i)) reductions. *)
Let nreductions : nat :=
let i := fold_right Z.max 0 (map (fun t => Z.log2 (fst t) / machine_wordsize) c) in
Z.to_nat (Qceiling (Z.of_nat n / (Z.of_nat n - i))).
Let possible_values := possible_values_of_machine_wordsize.
Let bound := Some r[0 ~> (2^machine_wordsize - 1)]%zrange.
Let boundsn : list (ZRange.type.option.interp base.type.Z)
:= repeat bound n.
(** Note: If you change the name or type signature of this
function, you will need to update the code in CLI.v *)
Definition check_args {T} (res : Pipeline.ErrorT T)
: Pipeline.ErrorT T
:= fold_right
(fun '(b, e) k => if b:bool then Error e else k)
res
[((negb (0 <? s - Associational.eval c))%Z, Pipeline.Value_not_ltZ "s - Associational.eval c ≤ 0" 0 (s - Associational.eval c));
((s =? 0)%Z, Pipeline.Values_not_provably_distinctZ "s ≠ 0" s 0);
((n =? 0)%nat, Pipeline.Values_not_provably_distinctZ "n ≠ 0" n 0);
((negb (0 <? machine_wordsize)), Pipeline.Value_not_ltZ "0 < machine_wordsize" 0 machine_wordsize)].
Local Ltac use_curve_good_t :=
repeat first [ assumption
| progress rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *
| reflexivity
| lia
| rewrite expr.interp_reify_list, ?map_map
| rewrite map_ext with (g:=id), map_id
| progress distr_length
| progress cbv [Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *
| progress cbv [Qle] in *
| progress cbn -[reify_list] in *
| progress intros
| solve [ auto ] ].
Context (curve_good : check_args (Success tt) = Success tt).
Lemma use_curve_good
: 0 < s - Associational.eval c
/\ s - Associational.eval c <> 0
/\ s <> 0
/\ 0 < machine_wordsize
/\ n <> 0%nat.
Proof using curve_good.
clear -curve_good.
cbv [check_args fold_right] in curve_good.
break_innermost_match_hyps; try discriminate.
rewrite negb_false_iff in *.
Z.ltb_to_lt.
rewrite NPeano.Nat.eqb_neq in *.
intros.
rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *.
specialize_by lia.
repeat match goal with H := _ |- _ => subst H end.
repeat match goal with
| [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ]
end.
repeat apply conj.
{ destruct (s - Associational.eval c) eqn:?; cbn; lia. }
{ use_curve_good_t. }
{ use_curve_good_t. }
{ use_curve_good_t. }
{ use_curve_good_t. }
Qed.
Local Notation weightf := (weight machine_wordsize 1).
Local Notation evalf := (eval weightf n).
Local Notation notations_for_docstring
:= (CorrectnessStringification.dyn_context.cons
weightf "weight"
(CorrectnessStringification.dyn_context.cons
evalf "eval"
CorrectnessStringification.dyn_context.nil))%string.
Local Notation "'docstring_with_summary_from_lemma!' summary correctness"
:= (docstring_with_summary_from_lemma_with_ctx!
notations_for_docstring
summary
correctness)
(only parsing, at level 10, summary at next level, correctness at next level).
Definition mul
:= Pipeline.BoundsPipeline
false (* subst01 *)
None (* fancy *)
possible_values
(reified_mul_gen
@ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify nreductions)
(Some boundsn, (Some boundsn, tt))
(Some boundsn, None (* Should be: Some r[0~>0]%zrange, but bounds analysis is not good enough *) ).
Definition smul (prefix : string)
: string * (Pipeline.ErrorT (list string * ToString.C.ident_infos))
:= Eval cbv beta in
FromPipelineToString
prefix "mul" mul
(docstring_with_summary_from_lemma!
(fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string)
(mul_correct weightf n m boundsn)).
Local Ltac solve_extra_bounds_side_conditions :=
cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia.
Hint Rewrite
(fun pf => @Rows.eval_mulmod (weight machine_wordsize 1) (@wprops _ _ pf))
using solve [ auto with zarith | congruence | solve_extra_bounds_side_conditions ] : push_eval.
Hint Unfold mulmod : push_eval.
Local Ltac prove_correctness _ := Primitives.prove_correctness use_curve_good.
Lemma mul_correct res
(Hres : mul = Success res)
: mul_correct (weight machine_wordsize 1) n m boundsn (Interp res).
Proof using curve_good. prove_correctness (). Qed.
Section for_stringification.
Local Open Scope string_scope.
Local Open Scope list_scope.
Definition known_functions
:= [("mul", smul)].
Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions).
(** Note: If you change the name or type signature of this
function, you will need to update the code in CLI.v *)
Definition Synthesize (function_name_prefix : string) (requests : list string)
: list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
:= Primitives.Synthesize
machine_wordsize valid_names known_functions (fun _ => nil)
[] function_name_prefix requests.
End for_stringification.
End __.
|
