-
Notifications
You must be signed in to change notification settings - Fork 5
/
SimModSem.v
308 lines (266 loc) · 12.2 KB
/
SimModSem.v
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
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
Require Import SimMem.
Require Import Simulation.
Require Import AST.
From Paco Require Import paco.
Require Import sflib.
Require Import Basics.
Require Import CoqlibC.
Require Import Values Integers.
Require Import Globalenvs.
Require Import Program.
Require Import MemoryC.
Require Import Skeleton SimSymb Ord.
Require Import ModSem.
Require Import Sound Preservation.
Import ModSem.
Require Import ModSemProps.
Require Import Events.
Require Import SmallstepC.
Set Implicit Arguments.
Section SIMMODSEM.
Variables ms_src ms_tgt: ModSem.t.
Context {SM: SimMem.class}.
Context {SS: SimSymb.class SM}.
Variable sound_states: ms_src.(state) -> Prop.
Inductive fsim_step (fsim: idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop)
(i0: idx) (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop :=
| fsim_step_step
(SAFESRC: ~ ms_src.(ModSem.is_call) st_src0 /\ ~ ms_src.(ModSem.is_return) st_src0)
(STEP: forall st_src1 tr
(STEPSRC: Step ms_src st_src0 tr st_src1),
exists i1 st_tgt1 sm1,
(<<PLUS: DPlus ms_tgt st_tgt0 tr st_tgt1>> \/ <<STAR: DStar ms_tgt st_tgt0 tr st_tgt1 /\ ord i1 i0>>)
/\ <<MLE: SimMem.le sm0 sm1>>
/\ <<FSIM: fsim i1 st_src1 st_tgt1 sm1>>)
(RECEP: receptive_at ms_src st_src0)
| fsim_step_stutter
i1 st_tgt1 sm1
(PLUS: DPlus ms_tgt st_tgt0 nil st_tgt1 /\ ord i1 i0)
(MLE: SimMem.le sm0 sm1)
(BSIM: fsim i1 st_src0 st_tgt1 sm1).
Inductive bsim_step (bsim: idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop)
(i0: idx) (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop :=
| bsim_step_step
(STEP: forall st_tgt1 tr
(STEPTGT: Step ms_tgt st_tgt0 tr st_tgt1),
exists i1 st_src1 sm1,
(<<PLUS: Plus ms_src st_src0 tr st_src1>> \/ <<STAR: Star ms_src st_src0 tr st_src1 /\ ord i1 i0>>)
/\ <<MLE: SimMem.le sm0 sm1>>
/\ <<BSIM: bsim i1 st_src1 st_tgt1 sm1>>)
(PROGRESS: <<STEPTGT: exists tr st_tgt1, Step ms_tgt st_tgt0 tr st_tgt1>>)
| bsim_step_stutter
i1 st_src1 sm1
(STAR: Star ms_src st_src0 nil st_src1 /\ ord i1 i0)
(MLE: SimMem.le sm0 sm1)
(BSIM: bsim i1 st_src1 st_tgt0 sm1).
Inductive _lxsim_pre (lxsim: idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop)
(i0: idx) (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop :=
| lxsim_step_forward
(SU: forall (SU: DUMMY_PROP),
<<FSTEP: fsim_step lxsim i0 st_src0 st_tgt0 sm0>>)
| lxsim_step_backward
(SU: forall (SU: DUMMY_PROP),
(<<BSTEP: forall
(SAFESRC: safe_modsem ms_src st_src0),
(<<BSTEP: bsim_step lxsim i0 st_src0 st_tgt0 sm0>>)>>))
| lxsim_at_external
(MWF: SimMem.wf sm0)
(SAFESRC: ms_src.(is_call) st_src0)
(SU: forall (SU: DUMMY_PROP),
<<CALLFSIM: forall args_src
(ATSRC: ms_src.(at_external) st_src0 args_src),
exists args_tgt sm_arg,
(<<SIMARGS: SimMem.sim_args args_src args_tgt sm_arg>>
/\ (<<MWF: SimMem.wf sm_arg>>)
/\ (<<MLE: SimMem.lepriv sm0 sm_arg>>)
/\ (<<ATTGT: ms_tgt.(at_external) st_tgt0 args_tgt>>)
/\ (<<K: forall sm_ret retv_src retv_tgt st_src1
(MLE: SimMem.le sm_arg sm_ret)
(MWF: SimMem.wf sm_ret)
(SIMRETV: SimMem.sim_retv retv_src retv_tgt sm_ret)
(AFTERSRC: ms_src.(after_external) st_src0 retv_src st_src1),
exists st_tgt1 sm_after i1,
(<<AFTERTGT: ms_tgt.(after_external) st_tgt0 retv_tgt st_tgt1>>) /\
(<<MLEPUB: SimMem.le sm0 sm_after>>) /\
(<<MLEPRIV: SimMem.lepriv sm_ret sm_after>>) /\
(<<LXSIM: lxsim i1 st_src1 st_tgt1 sm_after>>)>>))>>)
| lxsim_final
sm_ret retv_src retv_tgt
(MLE: SimMem.le sm0 sm_ret)
(MWF: SimMem.wf sm_ret)
(FINALSRC: ms_src.(final_frame) st_src0 retv_src)
(FINALTGT: ms_tgt.(final_frame) st_tgt0 retv_tgt)
(SIMRETV: SimMem.sim_retv retv_src retv_tgt sm_ret).
Definition _lxsim (lxsim: idx -> state ms_src -> state ms_tgt -> SimMem.t -> Prop)
(i0: idx) (st_src0: ms_src.(state)) (st_tgt0: ms_tgt.(state)) (sm0: SimMem.t): Prop :=
(forall (SUSTAR: forall st_src1 tr (STAR: Star ms_src st_src0 tr st_src1), sound_states st_src1),
<<LXSIM: _lxsim_pre lxsim i0 st_src0 st_tgt0 sm0>>).
Definition lxsim: _ -> _ -> _ -> _ -> Prop := paco4 _lxsim bot4.
Lemma lxsim_mon: monotone4 _lxsim.
Proof.
repeat intro. rr in IN. hexploit1 IN; eauto. inv IN; eauto.
- econs 1; ss. ii. spc SU. des. esplits; eauto. inv SU.
+ econs 1; eauto. i; des_safe. exploit STEP; eauto. i; des_safe. esplits; eauto.
+ econs 2; eauto.
- econs 2; ss. ii. exploit SU; eauto. i; des.
inv H.
+ econs 1; eauto. i; des_safe. exploit STEP; eauto. i; des_safe. esplits; eauto.
+ econs 2; eauto.
- econs 3; eauto. ii; ss. exploit SU; eauto. i; des.
esplits; eauto. ii. exploit K; eauto. i; des. esplits; eauto.
- econs 4; eauto.
Qed.
End SIMMODSEM.
Hint Unfold lxsim.
Hint Resolve lxsim_mon: paco.
Module ModSemPair.
Section MODSEMPAIR.
Context {SM: SimMem.class} {SS: SimSymb.class SM} {SU: Sound.class}.
Record t: Type := mk {
src: ModSem.t;
tgt: ModSem.t;
ss: SimSymb.t;
sm: SimMem.t;
}.
Inductive sim_skenv (msp: t) (sm0: SimMem.t): Prop :=
| sim_skenv_intro
(SIMSKE: SimSymb.sim_skenv sm0 msp.(ss) msp.(src).(ModSem.skenv) msp.(tgt).(ModSem.skenv))
ss_link
(SIMSKELINK: SimSymb.sim_skenv sm0 ss_link msp.(src).(ModSem.skenv_link) msp.(tgt).(ModSem.skenv_link)).
Lemma mfuture_preserves_sim_skenv
msp sm0 sm1
(MFUTURE: SimMem.future sm0 sm1)
(SIMSKENV: sim_skenv msp sm0):
<<SIMSKENV: sim_skenv msp sm1>>.
Proof.
inv SIMSKENV. econs; eapply SimSymb.mfuture_preserves_sim_skenv; eauto.
Qed.
Inductive sim (msp: t): Prop :=
| sim_intro
sidx sound_states sound_state_ex
(PRSV: local_preservation msp.(src) sound_state_ex)
(PRSVNOGR: forall (si: sidx), local_preservation_noguarantee msp.(src) (sound_states si))
(SIM: forall
sm_arg args_src args_tgt
sg_init_src sg_init_tgt
(FINDFSRC: (Genv.find_funct msp.(src).(ModSem.skenv)) (Args.get_fptr args_src) =
Some (Internal sg_init_src))
(FINDFTGT: (Genv.find_funct msp.(tgt).(ModSem.skenv)) (Args.get_fptr args_tgt) =
Some (Internal sg_init_tgt))
(SIMARGS: SimMem.sim_args args_src args_tgt sm_arg)
(SIMSKENV: sim_skenv msp sm_arg)
(MFUTURE: SimMem.future msp.(sm) sm_arg)
(MWF: SimMem.wf sm_arg),
(<<INITBSIM: forall st_init_tgt
(INITTGT: msp.(tgt).(initial_frame) args_tgt st_init_tgt)
(SAFESRC: exists _st_init_src, msp.(src).(initial_frame) args_src _st_init_src),
exists st_init_src sm_init idx_init,
(<<MLE: SimMem.le sm_arg sm_init>>) /\
(<<INITSRC: msp.(src).(initial_frame) args_src st_init_src>>) /\
(<<SIM: lxsim msp.(src) msp.(tgt) (fun st => forall si, exists su m_init, sound_states si su m_init st)
idx_init st_init_src st_init_tgt sm_init>>)>>) /\
(<<INITPROGRESS: forall
(SAFESRC: exists st_init_src, msp.(src).(initial_frame) args_src st_init_src),
exists st_init_tgt, (<<INITTGT: msp.(tgt).(initial_frame) args_tgt st_init_tgt>>)>>)).
End MODSEMPAIR.
End ModSemPair.
Hint Constructors ModSemPair.sim_skenv.
Section FACTORTARGET.
Context {SM: SimMem.class} {SS: SimSymb.class SM} {SU: Sound.class}.
Variable ms_src ms_tgt: ModSem.t.
Variable ss: SimSymb.t.
Variable sm: SimMem.t.
Hypothesis SINGLE: single_events ms_src.
Hypothesis WBT: well_behaved_traces ms_tgt.
Section LXSIM.
Variable sound_states: state ms_src -> Prop.
Inductive fbs_match: idx -> state ms_src -> (trace * state ms_tgt) -> SimMem.t -> Prop :=
| fbs_match_intro
idx0 st_src0 tr st_src1 st_tgt0 sm0
(STAR: (st_src0 = st_src1 /\ tr = E0) \/ ((Plus ms_src st_src0 tr st_src1) /\ output_trace tr /\ tr <> []))
(MATCH: lxsim ms_src ms_tgt sound_states idx0 st_src1 st_tgt0 sm0):
fbs_match idx0 st_src0 (tr, st_tgt0) sm0.
Lemma factor_lxsim_target: forall idx0 st_src0 tr st_tgt0 sm0
(SIM: fbs_match idx0 st_src0 (tr, st_tgt0) sm0),
<<SIM: lxsim ms_src (Atomic.trans ms_tgt) sound_states idx0 st_src0 (tr, st_tgt0) sm0>>.
Proof.
clear_tac. unfold NW. pcofix CIH.
i. pfold. inv SIM. punfold MATCH. des; clarify; cycle 1.
{ rename st_src2 into st_src1. econs 2; eauto. ii. econs 1; ii.
- (* bsim *)
econs; eauto.
exploit star_non_E0_split'_strong; eauto.
{ apply plus_star; eauto. }
intro P; des. des_ifs. des_safe. i. inv STEPTGT. esplits; eauto.
{ refl. }
pclearbot. right. eapply CIH; eauto. econs; eauto. ss. des; ss.
{ right. esplits; eauto. }
{ left. clarify. }
- (* progress *)
destruct tr; ss. ii. esplits; eauto. econs; eauto.
}
ii. rr in MATCH. hexploit1 MATCH.
{ ii. eapply SUSTAR; et. }
inv MATCH.
- econs 1. i. exploit SU; eauto. i; des_safe. esplits; eauto.
clear - SINGLE WBT CIH H. inv H.
+ econs 1; eauto. i. exploit STEP; eauto. i; des_safe. esplits; eauto.
{ des.
- left. exploit dplus_atomic_dplus; eauto.
- right. esplits; eauto. exploit dstar_atomic_dstar; eauto.
}
pclearbot. right. eapply CIH; eauto. econs; eauto.
+ econs 2; eauto.
{ des. esplits; eauto. exploit dplus_atomic_dplus; eauto. }
pclearbot. right. eapply CIH; eauto. econs; eauto.
- econs 2. ii. exploit SU; eauto. i; des. inv H; ii.
+ (* bsim *)
econs 1; eauto; cycle 1.
{ (* progress *)
des. destruct tr.
* esplits; eauto. instantiate (1:= (_, _)). econs 1; eauto.
* esplits; eauto. instantiate (1:= (_, _)). econs 2; eauto.
}
clear - SINGLE WBT CIH STEP.
* i. destruct tr; ss.
{ inv STEPTGT.
exploit STEP; eauto. i; des_safe. esplits; eauto.
pclearbot. right. eapply CIH; eauto. econs; eauto.
}
inv STEPTGT. destruct tr0; ss.
{ exploit STEP; eauto. i; des_safe. esplits; eauto.
pclearbot. right. eapply CIH; eauto. econs; eauto.
}
exploit WBT; eauto. intro WBT0. ss.
exploit STEP; eauto. i; des_safe. des.
-- exploit star_non_E0_split'; eauto.
{ apply plus_star; eauto. }
intro P. ss. des. esplits; eauto.
pclearbot. right. eapply CIH; eauto. econs.
{ right. esplits; eauto; ss. eapply star_inv in P0. des; clarify; ss. eauto. }
eauto.
-- exploit star_non_E0_split'; eauto. intro P. ss. des. esplits; eauto.
pclearbot. right. eapply CIH; eauto. econs.
{ right. esplits; eauto; ss. eapply star_inv in P0. des; clarify; ss. eauto. }
eauto.
+ econs 2; eauto. pclearbot. right. eapply CIH; eauto. econs; eauto.
- econs 3; eauto. ii. exploit SU; eauto. i; des. esplits; eauto.
{ rr. ss. }
i. exploit K; eauto. i; des. eexists (_, _). esplits; eauto.
{ rr. ss. esplits; eauto. }
pclearbot. right. eapply CIH; eauto. econs; eauto.
- econs 4; eauto. rr. esplits; eauto.
Qed.
End LXSIM.
Theorem factor_simmodsem_target
(SIM: ModSemPair.sim (ModSemPair.mk ms_src ms_tgt ss sm)):
ModSemPair.sim (ModSemPair.mk ms_src (ModSem.Atomic.trans ms_tgt) ss sm).
Proof.
inv SIM. ss. econs; eauto. ss. i. exploit SIM0; eauto.
{ inv SIMSKENV. ss. econs; eauto. }
i; des. split; ss.
- ii. rr in INITTGT. des. destruct st_init_tgt; ss. clarify. exploit INITBSIM; eauto. i; des.
esplits; eauto. eapply factor_lxsim_target; eauto. econs; eauto.
- ii. des. exploit INITPROGRESS; eauto. i ;des. eexists (_, _). esplits; eauto. rr. ss. econs; eauto.
Qed.
End FACTORTARGET.