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
|
(*
* Vericert: Verified high-level synthesis.
* Copyright (C) 2023 Yann Herklotz <git@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Errors.
Require Import compcert.common.Linking.
Require Import compcert.common.Globalenvs.
Require Import compcert.common.Memory.
Require Import compcert.common.Values.
Require Import compcert.lib.Maps.
Require Import vericert.common.Vericertlib.
Require Import vericert.hls.GibleSeq.
Require Import vericert.hls.GiblePar.
Require Import vericert.hls.Gible.
Require Import vericert.hls.GiblePargenproofEquiv.
Require Import vericert.hls.GiblePargen.
Require Import vericert.hls.Predicate.
Require Import vericert.hls.Abstr.
Require Import vericert.hls.AbstrSemIdent.
Require Import vericert.common.Monad.
Module Import OptionExtra := MonadExtra(Option).
#[local] Open Scope positive.
#[local] Open Scope forest.
#[local] Open Scope pred_op.
#[local] Opaque simplify.
#[local] Opaque deep_simplify.
#[local] Ltac destr := destruct_match; try discriminate; [].
Lemma storev_valid_pointer1 :
forall chunk m m' s d b z,
Mem.storev chunk m s d = Some m' ->
Mem.valid_pointer m b z = true ->
Mem.valid_pointer m' b z = true.
Proof using.
intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
eapply Mem.perm_store_1; eauto.
Qed.
Lemma storev_valid_pointer2 :
forall chunk m m' s d b z,
Mem.storev chunk m s d = Some m' ->
Mem.valid_pointer m' b z = true ->
Mem.valid_pointer m b z = true.
Proof using.
intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
eapply Mem.perm_store_2; eauto.
Qed.
Definition valid_mem m m' :=
forall b z, Mem.valid_pointer m b z = Mem.valid_pointer m' b z.
#[global] Program Instance valid_mem_Equivalence : Equivalence valid_mem.
Next Obligation. unfold valid_mem; auto. Qed. (* Reflexivity *)
Next Obligation. unfold valid_mem; auto. Qed. (* Symmetry *)
Next Obligation. unfold valid_mem; eauto. Qed. (* Transitity *)
Lemma storev_valid_pointer :
forall chunk m m' s d,
Mem.storev chunk m s d = Some m' ->
valid_mem m m'.
Proof using.
unfold valid_mem. symmetry.
intros. destruct (Mem.valid_pointer m b z) eqn:?;
eauto using storev_valid_pointer1.
apply not_true_iff_false.
apply not_true_iff_false in Heqb0.
eauto using storev_valid_pointer2.
Qed.
Lemma storev_cmpu_bool :
forall m m' c v v0,
valid_mem m m' ->
Val.cmpu_bool (Mem.valid_pointer m) c v v0 = Val.cmpu_bool (Mem.valid_pointer m') c v v0.
Proof using.
unfold valid_mem.
intros. destruct v, v0; crush.
{ destruct_match; crush.
destruct_match; crush.
destruct_match; crush.
apply orb_true_iff in H1.
inv H1. rewrite H in H2. rewrite H2 in Heqb1.
simplify. rewrite H0 in Heqb1. crush.
rewrite H in H2. rewrite H2 in Heqb1.
rewrite H0 in Heqb1. crush.
destruct_match; auto. simplify.
apply orb_true_iff in H1.
inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
simplify. rewrite H0 in Heqb1. crush.
rewrite <- H in H2. rewrite H2 in Heqb1.
rewrite H0 in Heqb1. crush. }
{ destruct_match; crush.
destruct_match; crush.
destruct_match; crush.
apply orb_true_iff in H1.
inv H1. rewrite H in H2. rewrite H2 in Heqb1.
simplify. rewrite H0 in Heqb1. crush.
rewrite H in H2. rewrite H2 in Heqb1.
rewrite H0 in Heqb1. crush.
destruct_match; auto. simplify.
apply orb_true_iff in H1.
inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
simplify. rewrite H0 in Heqb1. crush.
rewrite <- H in H2. rewrite H2 in Heqb1.
rewrite H0 in Heqb1. crush. }
{ destruct_match; auto. destruct_match; auto; crush.
{ destruct_match; crush.
{ destruct_match; crush.
setoid_rewrite H in H0; eauto.
setoid_rewrite H in H1; eauto.
rewrite H0 in Heqb. rewrite H1 in Heqb; crush.
}
{ destruct_match; crush.
setoid_rewrite H in Heqb0; eauto.
rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } }
{ destruct_match; crush.
{ destruct_match; crush.
setoid_rewrite H in H0; eauto.
setoid_rewrite H in H1; eauto.
rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush.
}
{ destruct_match; crush.
setoid_rewrite H in Heqb0; eauto.
rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } }
Qed.
Lemma storev_eval_condition :
forall m m' c rs,
valid_mem m m' ->
Op.eval_condition c rs m = Op.eval_condition c rs m'.
Proof using.
intros. destruct c; crush.
destruct rs; crush.
destruct rs; crush.
destruct rs; crush.
eapply storev_cmpu_bool; eauto.
destruct rs; crush.
destruct rs; crush.
eapply storev_cmpu_bool; eauto.
Qed.
Lemma eval_operation_valid_pointer :
forall A B (ge: Genv.t A B) sp op args m m' v,
valid_mem m m' ->
Op.eval_operation ge sp op args m' = Some v ->
Op.eval_operation ge sp op args m = Some v.
Proof.
intros * VALID OP. destruct op; auto.
- destruct cond; auto; cbn in *.
+ repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
+ repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
- destruct c; auto; cbn in *.
+ repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
+ repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
Qed.
Lemma bb_memory_consistency_eval_operation :
forall A B (ge: Genv.t A B) sp state i state' args op v,
step_instr ge sp (Iexec state) i (Iexec state') ->
Op.eval_operation ge sp op args (is_mem state) = Some v ->
Op.eval_operation ge sp op args (is_mem state') = Some v.
Proof.
inversion_clear 1; intro EVAL; auto.
cbn in *.
eapply eval_operation_valid_pointer. unfold valid_mem. symmetry.
eapply storev_valid_pointer; eauto.
auto.
Qed.
Lemma truthy_dflt :
forall ps p,
truthy ps p -> eval_predf ps (dfltp p) = true.
Proof. intros. destruct p; cbn; inv H; auto. Qed.
Lemma exists_sem_pred :
forall A B C (ctx: @ctx A) s pr r v,
@sem_pred_expr A B C pr s ctx r v ->
exists r',
NE.In r' r /\ s ctx (snd r') v.
Proof.
induction r; crush.
- inv H. econstructor. split. constructor. auto.
- inv H.
+ econstructor. split. constructor. left; auto. auto.
+ exploit IHr; eauto. intros HH. inversion_clear HH as [x HH']. inv HH'.
econstructor. split. constructor. right. eauto. auto.
Qed.
Lemma truthy_dec:
forall ps a, truthy ps a \/ falsy ps a.
Proof.
destruct a; try case_eq (eval_predf ps p); intuition (constructor; auto).
Qed.
Definition all_mutexcl (f: forest) : Prop :=
forall x, predicated_mutexcl (f #r x).
Lemma all_mutexcl_set :
forall f n r,
all_mutexcl f ->
predicated_mutexcl n ->
all_mutexcl f #r r <- n.
Proof.
unfold all_mutexcl; intros.
destruct (resource_eq x r); subst.
{ now rewrite forest_reg_gss. }
now rewrite forest_reg_gso by auto.
Qed.
#[local] Hint Resolve all_mutexcl_set : mte.
Lemma pred_ret_mutexcl :
forall A (a: A), predicated_mutexcl (pred_ret a).
Proof.
unfold pred_ret. repeat constructor; intros. inv H. inv H0. contradiction.
Qed.
#[local] Hint Resolve pred_ret_mutexcl : mte.
|
