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
|
(** * Reflective Pipeline: Glue Code *)
(** This file defines the tactics that transform a non-reflective goal
into a goal the that the reflective machinery can handle. *)
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Reify.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.Z.Syntax.Util.
Require Import Crypto.Reflection.Z.Reify.
Require Import Crypto.Reflection.Z.Bounds.Interpretation.
Require Import Crypto.Util.Tactics.Head.
Require Import Crypto.Util.Curry.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.SigmaAssoc.
Require Import Crypto.Util.Tactics.EvarExists.
Module Export Exports.
Export Crypto.Reflection.Z.Reify. (* export for the tactic redefinitions *)
End Exports.
(** The [reassoc_sig_and_eexists] tactic operates on a goal convertible with
<<
{ f : { a | is_bounded_by bounds a }
| BoundedWordToZ f = rexprZ (BoundedWordToZ a) ... (BoundedWordToZ z) }
>>
and leaves a goal of the form
<<
is_bounded_by bounds (map wordToZ ?f)
/\ map wordToZ ?f = rexprZ (map wordToZ (proj1_sig a)) ... (map wordToZ (proj1_sig z))
>>
where [?f] is a context variable set to a new evar. This tactic
relies on the exact definition of [BoundedWordToZ]. *)
Ltac reassoc_sig_and_eexists :=
cbv [BoundedWordToZ];
sig_sig_assoc;
evar_exists.
(** The [do_curry] tactic takes a goal of the form
<<
_ /\ BoundedWordToZ (?f a b ... z) = F A B ... Z
>>
and turns it into a goal of the form
<<
_ /\ BoundedWordToZ (f' (a, b, ..., z)) = F' (A, B, ..., Z)
>>
Note that the number of arguments on the left and on the right DO
NOT need to be the same. *)
Ltac do_curry :=
lazymatch goal with
| [ |- _ /\ ?BWtoZ ?f_bw = ?f_Z ]
=> let f_bw := head f_bw in
let f_Z := head f_Z in
change_with_curried f_Z;
change_with_curried f_bw
end.
(** The [split_BoundedWordToZ] tactic takes a goal of the form
<<
_ /\ map wordToZ (proj1_sig f) = F ARGS
>>
and splits [f] and any arguments in ARGS into two parts, part
about the computational behavior, and another part about the
boundedness.
This pipeline relies on the specific definition of [BoundedWordToZ],
and requires [f] to be a context variable which is set to a single
evar. *)
Ltac check_precondition _ :=
lazymatch goal with
| [ |- @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (map wordToZ ?f)
/\ map wordToZ ?f = _ ]
=> first [ is_var f | fail 1 "The argument to BoundedWordToZ must be a bare context-definition set to an evar, not"
f "which is not a variable" ];
match goal with
| [ f' := ?f_evar |- _ ]
=> constr_eq f f';
first [ is_evar f_evar | fail 2 "The argument to BoundedWordToZ must be a context-definition set to an evar, not"
f' "which is defined as" f_evar ]
| [ f' : _ |- _ ]
=> constr_eq f f';
fail 1 "The argument to BoundedWordToZ must be a context-definition set to an evar, not"
f' "which has no body"
| _ => fail 1 "The argument to BoundedWordToZ must be a context-definition, not" f "which does not appear in the context"
end
| [ |- ?G ]
=> let expected := uconstr:(@ZRange.is_bounded_by _ _ _ (map wordToZ ?[f])
/\ map wordToZ ?[f] = _) in
fail "The post-processed goal should have the form"
expected
"not"
G
end.
Ltac split_BoundedWordToZ :=
(** first revert the context definition which is an evar named [f]
in the docs above, so that it becomes evar 1 (for
[instantiate]), and so that [make_evar_for_first_projection]
works *)
check_precondition ();
lazymatch goal with
| [ |- _ /\ map wordToZ ?f = _ ]
=> revert f
end;
repeat match goal with
| [ |- context[map wordToZ (proj1_sig ?x)] ]
=> is_var x;
first [ clearbody x; fail 1
| (** we want to keep the same context variable in
the evar that we reverted above, and in the
current goal; hence the instantiate trick *)
instantiate (1:=ltac:(destruct x)); destruct x ]
end;
cbv beta iota; intro; (* put [f] back in the context so that [cbn] doesn't remove this let-in *)
cbn [proj1_sig].
(** The [zrange_to_reflective] tactic takes a goal of the form
<<
is_bounded_by _ bounds (map wordToZ (?fW args)) /\ map wordToZ (?fW args) = fZ argsZ
>>
and uses [cut] and a small lemma to turn it into a goal that the
reflective machinery can handle. The goal left by this tactic
should be fully solvable by the reflective pipeline. *)
Ltac const_tuple T val :=
lazymatch T with
| (?A * ?B)%type => let a := const_tuple A val in
let b := const_tuple B val in
constr:((a, b)%core)
| _ => val
end.
Lemma adjust_goal_for_reflective {T P} (LHS RHS : T)
: P RHS /\ LHS = RHS -> P LHS /\ LHS = RHS.
Proof. intros [? ?]; subst; tauto. Qed.
Ltac adjust_goal_for_reflective := apply adjust_goal_for_reflective.
Ltac unmap_wordToZ_tuple term :=
lazymatch term with
| (?x, ?y) => let x' := unmap_wordToZ_tuple x in
let y' := unmap_wordToZ_tuple y in
constr:((x', y'))
| map wordToZ ?x => x
end.
Ltac zrange_to_reflective_hyps_step :=
match goal with
| [ H : @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (Tuple.map wordToZ ?arg) |- _ ]
=> let rT := constr:(Syntax.tuple (Tbase TZ) count) in
let is_bounded_by' := constr:(@Bounds.is_bounded_by rT) in
let map' := constr:(@cast_back_flat_const (@Bounds.interp_base_type) rT (fun _ => Bounds.bounds_to_base_type) bounds) in
(* we use [assert] and [abstract] rather than [change] to catch
inefficiencies in conversion early, rather than allowing
[Defined] to take forever *)
let H' := fresh H in
rename H into H';
assert (H : is_bounded_by' bounds (map' arg)) by (clear -H'; abstract exact H');
clear H'; move H at top
end.
Ltac zrange_to_reflective_hyps := repeat zrange_to_reflective_hyps_step.
Ltac zrange_to_reflective_goal :=
lazymatch goal with
| [ |- @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (Tuple.map wordToZ ?reified_f_evar)
/\ Tuple.map wordToZ ?reified_f_evar = ?f ?Zargs ]
=> let T := type of f in
let f_domain := lazymatch T with ?A -> ?B => A end in
let T := (eval compute in T) in
let rT := reify_type T in
let is_bounded_by' := constr:(@Bounds.is_bounded_by (codomain rT)) in
let input_bounds := const_tuple f_domain bounds in
let map_t := constr:(fun t bs => @cast_back_flat_const (@Bounds.interp_base_type) t (fun _ => Bounds.bounds_to_base_type) bs) in
let map_output := constr:(map_t (codomain rT) bounds) in
let map_input := constr:(map_t (domain rT) input_bounds) in
let args := unmap_wordToZ_tuple Zargs in
(* we use [cut] and [abstract] rather than [change] to catch
inefficiencies in conversion early, rather than allowing
[Defined] to take forever *)
cut (is_bounded_by' bounds (map_output reified_f_evar) /\ map_output reified_f_evar = f (map_input args));
[ generalize reified_f_evar; clear; clearbody f; clear; let x := fresh in intros ? x; abstract exact x
| ];
cbv beta
end;
adjust_goal_for_reflective.
Ltac zrange_to_reflective := zrange_to_reflective_hyps; zrange_to_reflective_goal.
(** The tactic [refine_to_reflective_glue] is the public-facing one;
it takes a goal of the form
<<
BoundedWordToZ ?f = F (BoundedWordToZ A) (BoundedWordToZ B) ... (BoundedWordToZ Z)
>>
where [?f] is an evar, and turns it into a goal the that
reflective automation pipeline can handle. *)
Ltac refine_to_reflective_glue :=
reassoc_sig_and_eexists;
do_curry;
split_BoundedWordToZ;
zrange_to_reflective_goal.
|
