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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.Lists.List.
Local Open Scope Z_scope.
Require Import Crypto.Arithmetic.Core.
Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.Tactics.PoseTermWithName.
Require Import Crypto.Util.Tactics.CacheTerm.
Ltac pose_local_limb_widths wt sz limb_widths :=
pose_term_with
ltac:(fun _ => (eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz))))
limb_widths.
Ltac get_b_of upper_bound_of_exponent :=
constr:(fun exp => {| lower := 0 ; upper := upper_bound_of_exponent exp |}%Z). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
(* The definition [bounds_exp] is a tuple-version of the limb-widths,
which are the [exp] argument in [b_of] above, i.e., the approximate
base-2 exponent of the bounds on the limb in that position. *)
Ltac pose_local_bounds_exp sz limb_widths bounds_exp :=
pose_term_with_type
(Tuple.tuple Z sz)
ltac:(fun _ => eval compute in
(Tuple.from_list sz limb_widths eq_refl))
bounds_exp.
Ltac internal_pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds :=
let b_of := get_b_of upper_bound_of_exponent in
pose_term_with_type
(Tuple.tuple zrange sz)
ltac:(fun _ => eval compute in
(Tuple.map (fun e => b_of e) bounds_exp))
bounds.
Ltac pose_local_bounds_tight sz upper_bound_of_exponent_tight bounds_exp bounds_tight :=
internal_pose_local_bounds sz upper_bound_of_exponent_tight bounds_exp bounds_tight.
Ltac pose_local_bounds_loose sz upper_bound_of_exponent_loose bounds_exp bounds_loose :=
internal_pose_local_bounds sz upper_bound_of_exponent_loose bounds_exp bounds_loose.
Ltac pose_local_bounds_limbwidths sz bounds_exp bounds_limbwidths :=
internal_pose_local_bounds sz (fun exp => (2^exp - 1)%Z) bounds_exp bounds_limbwidths.
Ltac pose_bound1 r bound1 :=
cache_term_with_type_by
zrange
ltac:(exact {| lower := 0 ; upper := Z.pos r-1 |})
bound1.
Ltac pose_local_lgbitwidth bitwidth lgbitwidth :=
pose_term_with
ltac:(fun _ => eval compute in (Z.to_nat (Z.log2_up bitwidth)))
lgbitwidth.
Ltac pose_local_adjusted_bitwidth' lgbitwidth adjusted_bitwidth' :=
pose_term_with
ltac:(fun _ => eval compute in (2^lgbitwidth)%nat)
adjusted_bitwidth'.
Ltac pose_adjusted_bitwidth adjusted_bitwidth' adjusted_bitwidth :=
cache_term adjusted_bitwidth' adjusted_bitwidth.
Ltac pose_local_feZ sz feZ :=
pose_term_with
ltac:(fun _ => constr:(tuple Z sz))
feZ.
Ltac pose_feW sz lgbitwidth feW :=
cache_term_with_type_by
Type
ltac:(let v := eval cbv [lgbitwidth] in (tuple (wordT lgbitwidth) sz) in exact v)
feW.
Ltac internal_pose_feW_bounded feW bounds feW_bounded :=
cache_term_with_type_by
(feW -> Prop)
ltac:(let v := eval cbv [bounds] in (fun w : feW => is_bounded_by None bounds (map wordToZ w)) in exact_no_check v)
feW_bounded.
Ltac pose_feW_tight_bounded feW bounds_tight feW_tight_bounded :=
internal_pose_feW_bounded feW bounds_tight feW_tight_bounded.
Ltac pose_feW_loose_bounded feW bounds_loose feW_loose_bounded :=
internal_pose_feW_bounded feW bounds_loose feW_loose_bounded.
Ltac pose_feW_limbwidths_bounded feW bounds_limbwidths feW_limbwidths_bounded :=
internal_pose_feW_bounded feW bounds_limbwidths feW_limbwidths_bounded.
Ltac internal_pose_feBW sz adjusted_bitwidth' bounds feBW :=
cache_term_with_type_by
Type
ltac:(let v := eval cbv [adjusted_bitwidth' bounds] in (BoundedWord sz adjusted_bitwidth' bounds) in exact v)
feBW.
Ltac pose_feBW_tight sz adjusted_bitwidth' bounds_tight feBW_tight :=
internal_pose_feBW sz adjusted_bitwidth' bounds_tight feBW_tight.
Ltac pose_feBW_loose sz adjusted_bitwidth' bounds_loose feBW_loose :=
internal_pose_feBW sz adjusted_bitwidth' bounds_loose feBW_loose.
Ltac pose_feBW_limbwidths sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths :=
internal_pose_feBW sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths.
Lemma relax'_pf {sz in_bounds out_bounds} {v : tuple Z sz}
(Htight : fieldwiseb is_tighter_than_bool in_bounds out_bounds = true)
: is_bounded_by None in_bounds v -> is_bounded_by None out_bounds v.
Proof.
destruct sz as [|sz]; simpl in *; trivial.
induction sz as [|sz IHsz]; simpl in *;
repeat first [ exact I
| progress destruct_head'_prod
| progress destruct_head' zrange
| progress cbv [is_tighter_than_bool] in *
| progress split_andb
| progress Z.ltb_to_lt
| progress cbn [fst snd ZRange.lower ZRange.upper] in *
| progress destruct_head_hnf' and
| progress intros
| apply conj
| omega
| solve [ eauto ] ].
Qed.
Definition relax' {sz adjusted_bitwidth'} {in_bounds out_bounds}
(Htight : Tuple.fieldwiseb ZRange.is_tighter_than_bool in_bounds out_bounds = true)
: BoundedWord sz adjusted_bitwidth' in_bounds
-> BoundedWord sz adjusted_bitwidth' out_bounds
:= fun w => exist _ (proj1_sig w) (relax'_pf Htight (proj2_sig w)).
Ltac internal_pose_feBW_relax sz feBW_in feBW_out feBW_relax :=
cache_term_with_type_by
(feBW_in -> feBW_out)
ltac:(refine (@relax' sz _ _ _ _);
lazymatch goal with
| [ |- fieldwiseb is_tighter_than_bool ?in_bounds ?out_bounds = true ]
=> try cbv [in_bounds];
try cbv [out_bounds]
end;
abstract vm_cast_no_check (eq_refl true))
feBW_relax.
Ltac pose_feBW_relax sz feBW_tight feBW_loose feBW_relax :=
internal_pose_feBW_relax sz feBW_tight feBW_loose feBW_relax.
Ltac pose_feBW_relax_limbwidths_to_tight sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight :=
internal_pose_feBW_relax sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight.
Ltac pose_feBW_relax_limbwidths_to_loose sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose :=
internal_pose_feBW_relax sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose.
Lemma feBW_bounded_helper'
sz adjusted_bitwidth' bounds
(feBW := BoundedWord sz adjusted_bitwidth' bounds)
(wt : nat -> Z)
(Hwt : forall i, 0 <= wt i)
: forall (a : feBW),
B.Positional.eval wt (map lower bounds)
<= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a)
<= B.Positional.eval wt (map upper bounds).
Proof.
let a := fresh "a" in
intro a;
destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
destruct sz as [|sz].
{ cbv -[Z.le Z.lt Z.mul]; lia. }
{ cbn [tuple map] in *.
revert dependent wt; induction sz as [|sz IHsz]; intros.
{ cbv -[Z.le Z.lt wordToZ Z.mul Z.pow Z.add lower upper Nat.log2 wordT] in *.
repeat match goal with
| [ |- context[@wordToZ ?n ?x] ]
=> generalize dependent (@wordToZ n x); intros
| [ H : forall j, 0 <= wt j |- context[wt ?i] ]
=> pose proof (H i); generalize dependent (wt i); intros
end.
nia. }
{ pose proof (Hwt 0%nat).
cbn [tuple' map'] in *.
destruct a as [a' a], bounds as [bounds b], H as [H [H' _]].
cbn [fst snd] in *.
setoid_rewrite (@B.Positional.eval_step (S _)).
specialize (IHsz bounds a' H (fun i => wt (S i)) (fun i => Hwt _)).
nia. } }
Qed.
Lemma feBW_bounded_helper
sz adjusted_bitwidth' bounds
(feBW := BoundedWord sz adjusted_bitwidth' bounds)
(wt : nat -> Z)
(Hwt : forall i, 0 <= wt i)
l u
: l <= B.Positional.eval wt (map lower bounds)
/\ B.Positional.eval wt (map upper bounds) < u
-> forall (a : feBW),
l <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < u.
Proof.
intros [Hl Hu] a; split;
[ eapply Z.le_trans | eapply Z.le_lt_trans ];
[ | eapply feBW_bounded_helper' | eapply feBW_bounded_helper' | ];
assumption.
Qed.
Ltac internal_pose_feBW_bounded freeze wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded :=
lazymatch (eval vm_compute in freeze) with
| true
=> cache_proof_with_type_by
(forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < 2 * Z.pos m)
ltac:(apply (@feBW_bounded_helper sz adjusted_bitwidth' bounds wt wt_nonneg);
cbv -[Z.lt Z.le];
clear; vm_decide)
feBW_bounded
| false
=> cache_term tt feBW_bounded
end.
Ltac pose_feBW_tight_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded :=
internal_pose_feBW_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded.
Ltac pose_feBW_limbwidths_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded :=
internal_pose_feBW_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded.
Ltac pose_phiW feW m wt phiW :=
cache_term_with_type_by
(feW -> F m)
ltac:(exact (fun x : feW => B.Positional.Fdecode wt (Tuple.map wordToZ x)))
phiW.
Ltac internal_pose_phiBW feBW m wt phiBW :=
cache_term_with_type_by
(feBW -> F m)
ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x)))
phiBW.
Ltac pose_phiBW_tight feBW_tight m wt phiBW_tight :=
internal_pose_phiBW feBW_tight m wt phiBW_tight.
Ltac pose_phiBW_loose feBW_loose m wt phiBW_loose :=
internal_pose_phiBW feBW_loose m wt phiBW_loose.
Ltac pose_phiBW_limbwidths feBW_limbwidths m wt phiBW_limbwidths :=
internal_pose_phiBW feBW_limbwidths m wt phiBW_limbwidths.
|
