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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.Lists.List.
Require Import Coq.Classes.Morphisms.
Require Import Coq.MSets.MSetPositive.
Require Import Coq.FSets.FMapPositive.
Require Import Crypto.Language.
Require Import Crypto.LanguageInversion.
Require Import Crypto.LanguageWf.
Require Import Crypto.UnderLetsProofs.
Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs.
Require Import Crypto.Rewriter.
Require Import Crypto.RewriterWf1.
Require Import Crypto.RewriterWf2.
Require Import Crypto.RewriterInterpProofs1.
Require Import Crypto.RewriterRulesGood.
Require Import Crypto.RewriterRulesInterpGood.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.SplitInContext.
Require Import Crypto.Util.Tactics.SpecializeAllWays.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.RewriteHyp.
Require Import Crypto.Util.Tactics.Head.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.CPSNotations.
Require Import Crypto.Util.HProp.
Require Import Crypto.Util.Decidable.
Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
Local Open Scope Z_scope.
Import EqNotations.
Module Compilers.
Import Language.Compilers.
Import LanguageInversion.Compilers.
Import LanguageWf.Compilers.
Import UnderLetsProofs.Compilers.
Import GENERATEDIdentifiersWithoutTypesProofs.Compilers.
Import Rewriter.Compilers.
Import RewriterWf1.Compilers.
Import RewriterWf2.Compilers.
Import RewriterInterpProofs1.Compilers.
Import RewriterRulesGood.Compilers.
Import RewriterRulesInterpGood.Compilers.
Import expr.Notations.
Import defaults.
Import Rewriter.Compilers.RewriteRules.
Import RewriterWf1.Compilers.RewriteRules.
Import RewriterWf2.Compilers.RewriteRules.
Import RewriterInterpProofs1.Compilers.RewriteRules.
Import RewriterRulesGood.Compilers.RewriteRules.
Import RewriterRulesInterpGood.Compilers.RewriteRules.
Module Import RewriteRules.
Local Ltac start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
let Rewrite := lazymatch goal with
| [ |- Wf ?e ] => head e
| [ |- expr.Interp _ ?e == _ ] => head e
end in
cbv [Rewrite]; rewrite rewrite_head_eq; cbv [rewrite_head0]; rewrite all_rewrite_rules_eq.
Local Ltac start_Wf_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0;
apply Compile.Wf_Rewrite; [ | assumption ];
let wf_do_again := fresh "wf_do_again" in
(intros ? ? ? ? wf_do_again ? ?);
eapply @Compile.wf_assemble_identifier_rewriters;
eauto using
pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct
with nocore;
try reflexivity.
Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0;
eapply Compile.InterpRewrite; [ | assumption ];
intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed);
eauto using
pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed,
@ident.gen_interp_Proper, eq_refl
with nocore.
Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e).
Proof.
start_Wf_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0).
apply nbe_rewrite_rules_good.
Qed.
Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e).
Proof.
start_Wf_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0).
apply arith_rewrite_rules_good.
Qed.
Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e).
Proof.
start_Wf_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0).
apply arith_with_casts_rewrite_rules_good.
Qed.
Lemma Wf_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Wf (@RewriteStripLiteralCasts t e).
Proof.
start_Wf_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0).
apply strip_literal_casts_rewrite_rules_good.
Qed.
Lemma Wf_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z)
(Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
(Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
{t} e (Hwf : Wf e) : Wf (@RewriteToFancy invert_low invert_high t e).
Proof.
start_Wf_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0).
eapply fancy_rewrite_rules_good; eassumption.
Qed.
Lemma Wf_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z)
(value_range flag_range : ZRange.zrange)
(Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
(Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
{t} e (Hwf : Wf e) : Wf (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e).
Proof.
start_Wf_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0).
eapply fancy_with_casts_rewrite_rules_good; eassumption.
Qed.
Lemma Interp_gen_RewriteNBE {cast_outside_of_range t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteNBE t e)
== expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof.
start_Interp_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0).
apply nbe_rewrite_rules_interp_good.
Qed.
Lemma Interp_gen_RewriteArith {cast_outside_of_range} (max_const_val : Z) {t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArith max_const_val t e)
== expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof.
start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0).
apply arith_rewrite_rules_interp_good.
Qed.
Lemma Interp_gen_RewriteArithWithCasts {cast_outside_of_range} {t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArithWithCasts t e)
== expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof.
start_Interp_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0).
apply arith_with_casts_rewrite_rules_interp_good.
Qed.
Lemma Interp_gen_RewriteStripLiteralCasts {cast_outside_of_range} {t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteStripLiteralCasts t e)
== expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof.
start_Interp_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0).
apply strip_literal_casts_rewrite_rules_interp_good.
Qed.
Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z)
(Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
(Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
{t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancy invert_low invert_high t e)
== expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof.
start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0).
eapply fancy_rewrite_rules_interp_good; eassumption.
Qed.
Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z)
(value_range flag_range : ZRange.zrange)
(Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
(Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
{t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e)
== expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof.
start_Interp_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0).
eapply fancy_with_casts_rewrite_rules_interp_good; eassumption.
Qed.
Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e.
Proof. apply Interp_gen_RewriteNBE; assumption. Qed.
Lemma Interp_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e)
: Interp (@RewriteArith max_const_val t e) == Interp e.
Proof. apply Interp_gen_RewriteArith; assumption. Qed.
Lemma Interp_RewriteArithWithCasts {t} e (Hwf : Wf e)
: Interp (@RewriteArithWithCasts t e) == Interp e.
Proof. apply Interp_gen_RewriteArithWithCasts; assumption. Qed.
Lemma Interp_RewriteStripLiteralCasts {t} e (Hwf : Wf e)
: Interp (@RewriteStripLiteralCasts t e) == Interp e.
Proof. apply Interp_gen_RewriteStripLiteralCasts; assumption. Qed.
Lemma Interp_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z)
(Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
(Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
{t} e (Hwf : Wf e)
: Interp (@RewriteToFancy invert_low invert_high t e) == Interp e.
Proof. apply Interp_gen_RewriteToFancy; assumption. Qed.
Lemma Interp_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z)
(value_range flag_range : ZRange.zrange)
(Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
(Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
{t} e (Hwf : Wf e)
: Interp (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e) == Interp e.
Proof. apply Interp_gen_RewriteToFancyWithCasts; assumption. Qed.
End RewriteRules.
Lemma Wf_PartialEvaluate {t} e (Hwf : Wf e) : Wf (@PartialEvaluate t e).
Proof. apply Wf_RewriteNBE, Hwf. Qed.
Lemma Interp_gen_PartialEvaluate {cast_outside_of_range} {t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@PartialEvaluate t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof. apply Interp_gen_RewriteNBE, Hwf. Qed.
Lemma Interp_PartialEvaluate {t} e (Hwf : Wf e)
: Interp (@PartialEvaluate t e) == Interp e.
Proof. apply Interp_gen_PartialEvaluate; assumption. Qed.
Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy Wf_RewriteArithWithCasts Wf_RewriteStripLiteralCasts Wf_RewriteToFancyWithCasts : wf.
Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_gen_RewriteArithWithCasts @Interp_gen_RewriteStripLiteralCasts @Interp_gen_RewriteToFancyWithCasts @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy @Interp_RewriteArithWithCasts @Interp_RewriteStripLiteralCasts @Interp_RewriteToFancyWithCasts : interp.
End Compilers.
|
