-
Notifications
You must be signed in to change notification settings - Fork 5
/
Simulation.v
1395 lines (1225 loc) · 54.8 KB
/
Simulation.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
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Export Smallstep.
Require Import Values.
Require Import Globalenvs.
Require Import Memory.
Require Import Integers.
Require Import Events.
Require Import AST.
From Paco Require Import paco.
Require Import sflib.
Require Import CoqlibC.
Require Import Axioms.
Require Import Relations.
Require Import Wellfounded.
Require Import Program.Equality.
Set Implicit Arguments.
(**********************************************************************************************************)
(**********************************************************************************************************)
(**********************************************************************************************************)
Lemma well_founded_clos_trans
index
(order: index -> index -> Prop)
(WF: well_founded order):
<<WF: well_founded (clos_trans index order)>>.
Proof.
hnf in WF. hnf. i. eapply Acc_clos_trans. eauto.
Qed.
Lemma clos_t_rt:
forall (A : Type) (R : relation A) (x y z : A),
clos_trans A R x y -> clos_refl_trans A R y z -> clos_trans A R x z.
Proof.
i. induction H0; ss.
- eapply t_trans; eauto.
- eapply IHclos_refl_trans2; eauto.
Qed.
(**********************************************************************************************************)
(**********************************************************************************************************)
(**********************************************************************************************************)
(* DO NOT USE THIS MODULE DIRECTLY. THIS IS ONLY FOR PROVING "bsim => compcert bsim". *)
Module NOSTUTTER.
Section BACKWARD_SIM.
Variables L1 L2: semantics.
Variable index: Type.
Variable order: index -> index -> Prop.
Inductive _bsim bsim (i0: index) (st_src0: state L1) (st_tgt0: state L2): Prop :=
| bsim_intro
(FINAL: forall retv
(FINALTGT: final_state L2 st_tgt0 retv)
(SAFESRC: safe L1 st_src0),
exists st_src1, <<STEPSRC: Star L1 st_src0 E0 st_src1>> /\
<<FINALSRC: final_state L1 st_src1 retv>>)
(STEP: forall st_tgt1 tr
(STEPTGT: Step L2 st_tgt0 tr st_tgt1)
(SAFESRC: safe L1 st_src0),
exists i1 st_src1,
(<<PLUS: Plus L1 st_src0 tr st_src1>> \/ <<STAR: Star L1 st_src0 tr st_src1 /\ order i1 i0>>)
/\ <<BSIM: bsim i1 st_src1 st_tgt1>>)
(PROGRESS: forall
(SAFESRC: safe L1 st_src0),
<<FINAL: exists retv, final_state L2 st_tgt0 retv>> \/
<<STEP: exists tr st_tgt1, Step L2 st_tgt0 tr st_tgt1>>).
Definition bsim: _ -> _ -> _ -> Prop := paco3 _bsim bot3.
Lemma bsim_mon: monotone3 _bsim.
Proof.
ii. inv IN. econs; eauto. i. exploit STEP; eauto. i; des_safe. esplits; eauto.
Qed.
End BACKWARD_SIM.
Hint Unfold bsim.
Hint Resolve bsim_mon: paco.
Record bsim_properties (L1 L2: semantics) (index: Type)
(order: index -> index -> Prop): Prop := {
bsim_order_wf: <<WF: well_founded order>>;
bsim_initial_states_exist: forall st_init_src
(INITSRC: initial_state L1 st_init_src),
exists st_init_tgt, <<INITTGT: initial_state L2 st_init_tgt>>;
bsim_match_initial_states: forall st_init_src_
(INITSRC: initial_state L1 st_init_src_)
st_init_tgt
(INITTGT: initial_state L2 st_init_tgt),
exists i0 st_init_src, <<INITSRC: initial_state L1 st_init_src>> /\
<<BSIM: bsim L1 L2 order i0 st_init_src st_init_tgt>>;
}.
Arguments bsim_properties: clear implicits.
Inductive backward_simulation (L1 L2: semantics) : Prop :=
Backward_simulation (index: Type)
(order: index -> index -> Prop)
(props: bsim_properties L1 L2 index order).
Arguments Backward_simulation {L1 L2 index} order props.
Lemma to_compcert_backward_simulation
L1 L2
(BSIM: backward_simulation L1 L2):
<<BSIM: Smallstep.backward_simulation L1 L2>>.
Proof.
inv BSIM. inv props.
econs. econs; eauto.
- i. exploit bsim_initial_states_exist0; eauto. exploit bsim_match_initial_states0; eauto.
- i. punfold H. inv H. exploit FINAL; eauto.
- (* progress *)
i. rename H into BSIM. rename H0 into SAFE. punfold BSIM. inv BSIM. exploit PROGRESS; eauto.
- i. rename H into STEP. rename H0 into BSIM. rename H1 into SAFE.
punfold BSIM. inv BSIM. exploit STEP0; eauto. i; des_safe. esplits; eauto. pclearbot. ss.
Qed.
End NOSTUTTER.
(**********************************************************************************************************)
(**********************************************************************************************************)
(**********************************************************************************************************)
Section BACKWARD_SIM.
Variables L1 L2: semantics.
Variable index: Type.
Variable order: index -> index -> Prop.
Inductive bsim_step bsim (i0: index) (st_src0: L1.(state)) (st_tgt0: L2.(state)): Prop :=
| bsim_step_step
(STEP: forall st_tgt1 tr
(STEPTGT: Step L2 st_tgt0 tr st_tgt1),
exists i1 st_src1,
(<<PLUS: Plus L1 st_src0 tr st_src1>> \/ <<STAR: Star L1 st_src0 tr st_src1 /\ order i1 i0>>)
/\ <<BSIM: bsim i1 st_src1 st_tgt1>>)
(PROGRESS: forall
(SAFESRC: safe L1 st_src0),
<<FINAL: exists retv, final_state L2 st_tgt0 retv>> \/
<<STEP: exists tr st_tgt1, Step L2 st_tgt0 tr st_tgt1>>)
(FINAL: forall retv
(FINALTGT: final_state L2 st_tgt0 retv),
exists st_src1, <<STEPSRC: Star L1 st_src0 E0 st_src1>> /\
<<FINALSRC: final_state L1 st_src1 retv>>)
| bsim_step_stutter
i1 st_src1
(STAR: Star L1 st_src0 nil st_src1 /\ order i1 i0)
(BSIM: bsim i1 st_src1 st_tgt0).
Inductive _bsim bsim (i0: index) (st_src0: state L1) (st_tgt0: state L2): Prop :=
| bsim_intro
(STEP: forall
(SAFESRC: safe L1 st_src0),
<<STEP: bsim_step bsim i0 st_src0 st_tgt0>>).
Definition bsim: _ -> _ -> _ -> Prop := paco3 _bsim bot3.
Lemma bsim_mon: monotone3 _bsim.
Proof.
ii. inv IN. econs; eauto. i. exploit STEP; eauto. i; des_safe. inv H.
- eleft; eauto. i. exploit STEP0; eauto. i; des_safe. esplits; eauto.
- eright; eauto.
Qed.
End BACKWARD_SIM.
Hint Unfold bsim.
Hint Resolve bsim_mon: paco.
Record bsim_properties (L1 L2: semantics) (index: Type)
(order: index -> index -> Prop): Prop := {
bsim_order_wf: <<WF: well_founded order>>;
bsim_initial_states_exist: forall st_init_src
(INITSRC: initial_state L1 st_init_src),
exists st_init_tgt, <<INITTGT: initial_state L2 st_init_tgt>>;
bsim_match_initial_states: forall st_init_src_
(INITSRC: initial_state L1 st_init_src_)
st_init_tgt
(INITTGT: initial_state L2 st_init_tgt),
exists i0 st_init_src, <<INITSRC: initial_state L1 st_init_src>> /\
<<BSIM: bsim L1 L2 order i0 st_init_src st_init_tgt>>;
}.
Arguments bsim_properties: clear implicits.
Inductive backward_simulation (L1 L2: semantics) : Prop :=
Backward_simulation (index: Type)
(order: index -> index -> Prop)
(props: bsim_properties L1 L2 index order).
Arguments Backward_simulation {L1 L2 index} order props.
Lemma bsim_to_nostutter_bsim
(L1 L2: semantics)
index i0 st_src0 st_tgt0
(ord: index -> index -> Prop)
(WF: well_founded ord)
(BSIM: bsim L1 L2 ord i0 st_src0 st_tgt0):
<<BSIM: NOSTUTTER.bsim L1 L2 (clos_trans _ ord) i0 st_src0 st_tgt0>>.
Proof.
red. generalize dependent i0. generalize dependent st_src0. generalize dependent st_tgt0.
pcofix CIH. i. pfold. econs; eauto.
- generalize dependent BSIM. generalize dependent st_src0. generalize dependent st_tgt0. pattern i0.
eapply (well_founded_ind WF); eauto. i. rename H into IH. clear i0.
punfold BSIM. inv BSIM. hexploit1 STEP; eauto. inv STEP.
+ eapply FINAL; eauto.
+ pclearbot. des. exploit IH; eauto. { eapply star_safe; eauto. } i; des. esplits; try apply FINALSRC.
eapply star_trans; eauto.
- generalize dependent st_src0. generalize dependent st_tgt0. pattern i0.
eapply (well_founded_ind WF); eauto. i. rename H into IH.
punfold BSIM. inv BSIM. exploit STEP; eauto. i; des_safe. inv H.
+ exploit STEP0; eauto. i; des_safe. pclearbot. esplits; eauto. des.
* left; ss.
* right; ss. esplits; eauto.
+ pclearbot. des. specialize (IH _ STAR0).
exploit IH; eauto.
{ ii. eapply SAFESRC. eapply star_trans; eauto. }
i; des_safe. esplits; eauto. des.
* left. eapply star_plus_trans; eauto.
* right. esplits; eauto. eapply star_trans; eauto.
apply clos_trans_tn1_iff. econs 2; eauto. apply clos_trans_tn1_iff. ss.
- generalize dependent BSIM. generalize dependent st_src0. generalize dependent st_tgt0. pattern i0.
eapply (well_founded_ind WF); eauto. i. rename H into IH. clear i0.
punfold BSIM. inv BSIM. specialize (STEP SAFESRC). inv STEP.
+ exploit PROGRESS; eauto.
+ des. pclearbot. exploit IH; eauto. eapply star_safe; eauto.
Qed.
Lemma backward_to_nostutter_backward_simulation
L1 L2
(BS: backward_simulation L1 L2):
<<BS: NOSTUTTER.backward_simulation L1 L2>>.
Proof.
inv BS. inv props. econs; eauto.
instantiate (1:= (clos_trans _ order)). econs; eauto.
{ eapply well_founded_clos_trans. eauto. }
i. exploit bsim_match_initial_states0; eauto. i; des.
esplits; eauto. eapply bsim_to_nostutter_bsim; eauto.
Qed.
Lemma backward_to_compcert_backward_simulation
L1 L2
(BSIM: backward_simulation L1 L2):
<<BSIM: Smallstep.backward_simulation L1 L2>>
.
Proof.
eapply NOSTUTTER.to_compcert_backward_simulation; eauto.
eapply backward_to_nostutter_backward_simulation; eauto.
Qed.
(**********************************************************************************************************)
(**********************************************************************************************************)
(**********************************************************************************************************)
Definition single_events_at (L: semantics) (s:L.(state)) : Prop :=
forall t s', Step L s t s' -> (length t <= 1)%nat.
(* These "strict_determinate" definitions are merely for convenience. *)
Record strict_determinate_at (L: semantics) (s:L.(state)) : Prop :=
Strict_determinate_at {
ssd_determ_at: forall t1 s1 t2 s2
(STEP0: Step L s t1 s1)
(STEP1 :Step L s t2 s2),
<<EQ: t1 = t2>> /\ <<EQ: s1 = s2>>;
ssd_determ_at_final: forall tr s' retv
(FINAL: final_state L s retv)
(STEP: Step L s tr s'),
False;
ssd_traces_at:
single_events_at L s
}.
Definition SDStep (L: semantics) :=
(fun s1 t s2 => strict_determinate_at L s1 /\ Step L s1 t s2).
Definition SDStar (L: semantics) :=
(star (fun _ _ => SDStep L)) L.(symbolenv) L.(globalenv).
Definition SDStarN (L: semantics) :=
(starN (fun _ _ => SDStep L)) L.(symbolenv) L.(globalenv).
Definition SDPlus (L: semantics) :=
(plus (fun _ _ => SDStep L)) L.(symbolenv) L.(globalenv).
Hint Unfold SDStep SDStar SDStarN SDPlus.
Inductive Dfinal_state (L: semantics) (st: L.(state)) (retv: int): Prop :=
| Dfinal_state_intro
(FINAL: final_state L st retv)
(DTM: forall retv0 retv1
(FINAL0: final_state L st retv0)
(FINAL1: final_state L st retv1),
retv0 = retv1)
(DTM: forall retv0
(FINAL: final_state L st retv0),
Nostep L st).
Inductive Dinitial_state (L: semantics) (st: L.(state)): Prop :=
| Dinitial_state_intro
(INIT: initial_state L st)
(DTM: forall st0 st1
(INIT0: initial_state L st0)
(INIT1: initial_state L st1),
st0 = st1).
Record preservation {L: semantics} (sound_state: L.(state) -> Prop): Prop :=
{
prsv_initial: forall st (INIT: L.(initial_state) st), (<<SS: sound_state st>>);
prsv_step: forall st0 tr st1 (SS: sound_state st0) (STEP: Step L st0 tr st1), (<<SS: sound_state st1>>);
}
.
Theorem preservation_top: forall {L}, <<PRSV: @preservation L top1>>.
Proof. ii. econs; eauto. Qed.
Theorem prsv_star
L sound_state
(PRSV: preservation sound_state)
:
(<<PRSVSTAR: forall st0 tr st1 (SS: sound_state st0) (STAR: Star L st0 tr st1), (<<SS: sound_state st1>>)>>)
.
Proof.
ii. ginduction STAR; ii; ss. eapply IHSTAR; eauto. eapply prsv_step; eauto.
Qed.
Module GENMT.
Record match_traces: Type := {
mt_match :> trace -> trace -> Prop;
mt_nil_left: forall x (NIL: mt_match E0 x), x = E0;
mt_nil_right: forall x (NIL: mt_match x E0), x = E0;
}.
Record receptive_at (mt: match_traces) (L: semantics) (s:L.(state)) : Prop :=
Receptive_at {
sr_receptive_at: forall t1 s1 t2,
Step L s t1 s1 -> mt t1 t2 -> exists s2, Step L s t2 s2;
sr_traces_at:
single_events_at L s
}.
Record determinate_at (mt: match_traces) (L: semantics) (s:L.(state)) : Prop :=
Determinate_at {
sd_determ_at: forall t1 s1 t2 s2,
Step L s t1 s1 -> Step L s t2 s2 ->
mt t1 t2 /\ (t1 = t2 -> s1 = s2);
sd_determ_at_final: forall
tr s' retv
(FINAL: final_state L s retv)
(STEP: Step L s tr s'),
False;
sd_traces_at:
single_events_at L s
}.
Program Definition match_traces_default (se: Senv.t): match_traces :=
Build_match_traces (Events.match_traces se) _ _.
Next Obligation. inv NIL. ss. Qed.
Next Obligation. inv NIL. ss. Qed.
Program Definition match_traces_strict: match_traces :=
Build_match_traces eq _ _.
Lemma no_event_receptive L s mt
(DETERM: forall t1 s1, Step L s t1 s1 -> t1 = E0):
receptive_at mt L s.
Proof.
econstructor; intros.
- exploit DETERM; eauto. intro. subst.
exploit mt_nil_left; eauto. i; clarify. exists s1. auto.
- repeat intro. exploit DETERM; eauto. intro. subst. auto.
Qed.
Definition DStep (mt: match_traces) (L: semantics) :=
(fun s1 t s2 => determinate_at mt L s1 /\ Step L s1 t s2).
Definition DStar (mt: match_traces) (L: semantics) :=
(star (fun _ _ => DStep mt L)) L.(symbolenv) L.(globalenv).
Definition DStarN (mt: match_traces) (L: semantics) :=
(starN (fun _ _ => DStep mt L)) L.(symbolenv) L.(globalenv).
Definition DPlus (mt: match_traces) (L: semantics) :=
(plus (fun _ _ => DStep mt L)) L.(symbolenv) L.(globalenv).
Hint Unfold DStep DStar DStarN DPlus.
Remark strict_fsim_src:
(<<SRC: forall L st0, single_events_at L st0 <-> receptive_at match_traces_strict L st0>>).
Proof.
- split; i.
+ econs; eauto. intros. ss. clarify. eauto.
+ inv H. ss.
Qed.
Remark strict_fsim_tgt:
(<<TGT: forall L st0, strict_determinate_at L st0 <-> determinate_at match_traces_strict L st0>>).
Proof.
- split; i.
+ inv H. econs; eauto. i. ss.
exploit ssd_determ_at0.
{ apply H. }
{ apply H0. }
i; des. clarify.
+ inv H. econs; eauto. i. ss.
exploit sd_determ_at0.
{ apply STEP0. }
{ apply STEP1. }
i; des. clarify. exploit H0; eauto.
Qed.
Remark strict_fsim_tgt_step:
(<<TGT: forall L st0 tr st1, SDStep L st0 tr st1 <-> DStep match_traces_strict L st0 tr st1>>).
Proof.
unfold DStep. unfold SDStep. split; i; des; econs; eauto; apply strict_fsim_tgt; ss.
Qed.
Remark strict_fsim_tgt_star:
(<<TGT: forall L st0 tr st1, SDStar L st0 tr st1 <-> DStar match_traces_strict L st0 tr st1>>).
Proof.
split; i; induction H; ii; ss; try apply star_refl; econs; eauto; apply strict_fsim_tgt_step; eauto.
Qed.
Remark strict_fsim_tgt_plus:
(<<TGT: forall L st0 tr st1, SDPlus L st0 tr st1 <-> DPlus match_traces_strict L st0 tr st1>>).
Proof.
split; i; inv H; econs; eauto; try apply strict_fsim_tgt_star; eauto; try apply strict_fsim_tgt_step; eauto.
Qed.
Lemma DStep_E0_SDStep
L st0 st1 mt_at
(STEP: DStep mt_at L st0 E0 st1):
SDStep L st0 E0 st1.
Proof.
r in STEP. des. econs; eauto. inv STEP. econs; eauto. intros.
exploit sd_determ_at0.
{ apply STEP0. }
{ apply STEP1. }
i; des. apply mt_nil_left in H. clarify. exploit H0; eauto. i; des. clarify.
exploit sd_determ_at0.
{ apply STEP0. }
{ apply STEP2. }
i; des. apply mt_nil_left in H. clarify. exploit H1; eauto.
Qed.
Lemma DStarN_E0_SDStarN
L st0 st1 mt_at n
(STEP: DStarN mt_at L n st0 E0 st1):
SDStarN L n st0 E0 st1.
Proof.
dependent induction STEP; ii; ss.
{ econs; eauto. }
destruct t1, t2; ss. econs; eauto.
{ eapply DStep_E0_SDStep; eauto. }
{ eapply IHSTEP. ss. }
ss.
Qed.
Section MIXED_SIM.
Variables L1 L2: semantics.
Variable index: Type.
Variable order: index -> index -> Prop.
Variable ss_src: L1.(state) -> Prop.
Variable ss_tgt: L2.(state) -> Prop.
Hypothesis (PRSVSRC: preservation ss_src).
Hypothesis (PRSVTGT: preservation ss_tgt).
Inductive fsim_step xsim (i0: index) (st_src0: L1.(state)) (st_tgt0: L2.(state)): Prop :=
| fsim_step_step
(mt: match_traces)
(STEP: forall st_src1 tr
(STEPSRC: Step L1 st_src0 tr st_src1),
exists i1 st_tgt1,
((<<PLUS: DPlus mt L2 st_tgt0 tr st_tgt1 /\ (<<RECEPTIVE: receptive_at mt L1 st_src0>>)>>) \/
<<STUTTER: st_tgt0 = st_tgt1 /\ tr = E0 /\ order i1 i0>>)
/\ <<XSIM: xsim i1 st_src1 st_tgt1>>)
(FINAL: forall retv
(FINALSRC: final_state L1 st_src0 retv),
<<FINALTGT: Dfinal_state L2 st_tgt0 retv>>)
| fsim_step_stutter
i1 st_tgt1
(PLUS: SDPlus L2 st_tgt0 nil st_tgt1 /\ order i1 i0)
(XSIM: xsim i1 st_src0 st_tgt1).
Inductive _xsim_forward xsim (i0: index) (st_src0: state L1) (st_tgt0: state L2): Prop :=
| _xsim_forward_intro
(STEP: fsim_step xsim i0 st_src0 st_tgt0).
Let bsim_step := bsim_step L1 L2 order.
Inductive _xsim_backward xsim (i0: index) (st_src0: state L1) (st_tgt0: state L2): Prop :=
| _xsim_backward_intro
(STEP: forall
(SAFESRC: safe L1 st_src0),
<<STEP: bsim_step xsim i0 st_src0 st_tgt0>>).
Definition _xsim xsim (i0: index) (st_src0: state L1) (st_tgt0: state L2): Prop := forall
(SSSRC: forall tr st_src1 (STAR: Star L1 st_src0 tr st_src1), <<SSSRC: ss_src st_src1>>)
(SSTGT: forall tr st_tgt1 (STAR: Star L2 st_tgt0 tr st_tgt1), <<SSTGT: ss_tgt st_tgt1>>)
,
(<<XSIM: (_xsim_forward \4/ _xsim_backward) xsim i0 st_src0 st_tgt0>>)
.
Definition xsim: _ -> _ -> _ -> Prop := paco3 _xsim bot3.
Lemma _xsim_forward_mon: monotone3 (_xsim_forward).
Proof.
ii. inv IN. econs; eauto. inv STEP.
- econs 1; eauto. i. exploit STEP0; eauto. i; des_safe. esplits; eauto.
- econs 2; eauto.
Qed.
Lemma _xsim_backward_mon: monotone3 (_xsim_backward).
Proof.
ii. inv IN. econs; eauto. i. exploit STEP; eauto. i; des_safe. inv H.
- eleft; eauto. i. exploit STEP0; eauto. i; des_safe. esplits; eauto.
- eright; eauto.
Qed.
Lemma xsim_mon: monotone3 _xsim.
Proof.
ii. repeat spc IN. inv IN.
- econs 1; eauto. eapply _xsim_forward_mon; eauto.
- econs 2; eauto. eapply _xsim_backward_mon; eauto.
Qed.
End MIXED_SIM.
Hint Unfold xsim.
Hint Resolve xsim_mon: paco.
Hint Resolve _xsim_forward_mon: paco.
Hint Resolve _xsim_backward_mon: paco.
Inductive xsim_init_sim (L1 L2: semantics) (index: Type) (order: index -> index -> Prop)
(ss_src: L1.(state) -> Prop) (ss_tgt: L2.(state) -> Prop): Prop :=
| xsim_init_forward
(INITSIM: forall st_init_src
(INITSRC: initial_state L1 st_init_src),
exists i0 st_init_tgt,
(<<INITTGT: Dinitial_state L2 st_init_tgt>>) /\
(<<XSIM: xsim L1 L2 order ss_src ss_tgt i0 st_init_src st_init_tgt>>))
| xsim_init_backward
(INITEXISTS: forall st_init_src
(INITSRC: initial_state L1 st_init_src),
exists st_init_tgt, <<INITTGT: initial_state L2 st_init_tgt>>)
(INITSIM: forall st_init_src_
(INITSRC: initial_state L1 st_init_src_)
st_init_tgt
(INITTGT: initial_state L2 st_init_tgt),
exists i0 st_init_src,
(<<INITSRC: initial_state L1 st_init_src>>) /\
(<<XSIM: xsim L1 L2 order ss_src ss_tgt i0 st_init_src st_init_tgt>>)).
Record xsim_properties (L1 L2: semantics) (index: Type)
(order: index -> index -> Prop): Type := {
xsim_ss_src: L1.(state) -> Prop;
xsim_ss_tgt: L2.(state) -> Prop;
xsim_prsv_src: preservation xsim_ss_src;
xsim_prsv_tgt: preservation xsim_ss_tgt;
xsim_order_wf: <<WF: well_founded order>>;
xsim_initial_states_sim: <<INIT: xsim_init_sim L1 L2 order xsim_ss_src xsim_ss_tgt>>;
}.
Arguments xsim_properties: clear implicits.
Inductive mixed_simulation (L1 L2: semantics) : Prop :=
Mixed_simulation (index: Type)
(order: index -> index -> Prop)
(props: xsim_properties L1 L2 index order).
Arguments Mixed_simulation {L1 L2 index} order props.
(**********************************************************************************************************)
(**********************************************************************************************************)
(**********************************************************************************************************)
Section MIXED_TO_BACKWARD.
Variables L1 L2: semantics.
Variable index: Type.
Variable order: index -> index -> Prop.
Hypothesis XSIM: xsim_properties L1 L2 index order.
Let match_states := xsim L1 L2 order XSIM.(xsim_ss_src) XSIM.(xsim_ss_tgt).
(** Orders *)
Inductive x2b_index : Type :=
| X2BI_before (n: nat)
| X2BI_after (n: nat) (i: index).
Inductive x2b_order: x2b_index -> x2b_index -> Prop :=
| x2b_order_before: forall n n',
(n' < n)%nat ->
x2b_order (X2BI_before n') (X2BI_before n)
| x2b_order_after: forall n n' i,
(n' < n)%nat ->
x2b_order (X2BI_after n' i) (X2BI_after n i)
| x2b_order_after': forall n m i' i,
clos_trans _ order i' i ->
x2b_order (X2BI_after m i') (X2BI_after n i)
| x2b_order_switch: forall n n' i,
x2b_order (X2BI_before n') (X2BI_after n i).
Lemma wf_x2b_order:
well_founded x2b_order.
Proof.
assert (ACC1: forall n, Acc x2b_order (X2BI_before n)).
{ intros n0; pattern n0; apply lt_wf_ind; intros.
constructor; intros. inv H0. auto.
}
assert (ACC2: forall i n, Acc x2b_order (X2BI_after n i)).
{ intros i; pattern i. eapply well_founded_ind.
{ apply wf_clos_trans. eapply xsim_order_wf; eauto. }
i. pattern n. apply lt_wf_ind; i. clear n. econs; eauto. i. inv H1; eauto.
}
red; intros. destruct a; auto.
Qed.
(** Constructing the backward simulation *)
Inductive x2b_match_states: x2b_index -> state L1 -> state L2 -> Prop :=
| x2b_match_at: forall i s1 s2,
match_states i s1 s2 ->
x2b_match_states (X2BI_after O i) s1 s2
| x2b_match_before: forall s1 t s1' s2b s2 n s2a mt,
Step L1 s1 t s1' -> t <> E0 ->
DStar mt L2 s2b E0 s2 ->
DStarN mt L2 n s2 t s2a ->
(forall t s1', Step L1 s1 t s1' ->
exists i', exists s2',
((<<PLUS: DPlus mt L2 s2b t s2' /\ (<<RECEPTIVE: receptive_at mt L1 s1>>)>>) \/
<<STUTTER: s2b = s2' /\ t = E0>>)
/\ match_states i' s1' s2') ->
x2b_match_states (X2BI_before n) s1 s2
| x2b_match_after: forall n s2 s2a s1 i,
SDStarN L2 (S n) s2 E0 s2a ->
match_states i s1 s2a ->
x2b_match_states (X2BI_after (S n) i) s1 s2.
Remark x2b_match_after':
forall n s2 s2a s1 i,
SDStarN L2 n s2 E0 s2a ->
match_states i s1 s2a ->
x2b_match_states (X2BI_after n i) s1 s2.
Proof.
intros. inv H. econstructor; eauto. econstructor; eauto. econstructor; eauto.
Qed.
Lemma _xsim_backward_mon_x2b
i0 st_src0 st_tgt0
(BSIM: _xsim_backward L1 L2 order match_states i0 st_src0 st_tgt0):
<<BSIM: _xsim_backward L1 L2 x2b_order x2b_match_states (X2BI_after 0 i0) st_src0 st_tgt0>>.
Proof.
red. inv BSIM. econs; eauto. i. exploit STEP; eauto. i; des. inv H.
- econs 1; eauto. i. exploit STEP0; eauto. i; des; pclearbot; esplits; eauto.
econs; eauto. right. esplits; eauto. econs 3; eauto. econs; eauto.
- pclearbot. des. econs 2; eauto. esplits; eauto. econs 3; eauto. econs; eauto.
Qed.
(** Exploiting mixed simulation *)
Inductive x2b_transitions: index -> state L1 -> state L2 -> Prop :=
| x2b_trans_forward_final
i st_src0 st_src1 st_tgt0 r
(TAU: Star L1 st_src0 E0 st_src1)
(FINALSRC: final_state L1 st_src1 r)
(FINALTGT: Dfinal_state L2 st_tgt0 r):
x2b_transitions i st_src0 st_tgt0
| x2b_trans_forward_step: forall i s1 s2 s1' t s1'' s2' i' i'' mt,
Star L1 s1 E0 s1' ->
Step L1 s1' t s1'' ->
DPlus mt L2 s2 t s2' ->
forall (STEP: forall st_src1 tr
(STEPSRC: Step L1 s1' tr st_src1),
exists i1 st_tgt1,
((<<PLUS: DPlus mt L2 s2 tr st_tgt1 /\ (<<RECEPTIVE: receptive_at mt L1 s1'>>)>>) \/
<<STUTTER: s2 = st_tgt1 /\ tr = E0 /\ order i1 i'>>)
/\ <<FSIM: match_states i1 st_src1 st_tgt1>>),
match_states i'' s1'' s2' ->
x2b_transitions i s1 s2
| x2b_trans_forward_stutter: forall i s1 s2 s1' s2' i' i'',
Star L1 s1 E0 s1' ->
True ->
SDPlus L2 s2 E0 s2' ->
match_states i'' s1' s2' ->
forall (ORD0: clos_refl_trans _ order i' i)
(ORD1: order i'' i'),
x2b_transitions i s1 s2
| x2b_trans_backward
i0 st_src0 st_tgt0
(BSIM: _xsim_backward L1 L2 x2b_order x2b_match_states (X2BI_after 0 i0) st_src0 st_tgt0):
x2b_transitions i0 st_src0 st_tgt0.
Lemma x2b_transitions_src_tau_rev
s1 s1' i i' s2
(STEPSRC: Star L1 s1 E0 s1')
(ORDER: order i' i)
(TRANS: x2b_transitions i' s1' s2):
<<TRANS: x2b_transitions i s1 s2>>.
Proof.
inv TRANS.
* eapply x2b_trans_forward_final; try eapply star_trans; eauto.
* eapply x2b_trans_forward_step; cycle 1; eauto. eapply star_trans; eauto.
* eapply x2b_trans_forward_stutter; cycle 1; eauto.
eapply rt_trans; eauto. constructor. auto. eapply star_trans; eauto.
* eapply x2b_trans_backward; cycle 1; eauto. inv BSIM. econs; eauto. i. hexploit1 STEP.
{ eapply star_safe; eauto. }
inv STEP.
- econs 1; eauto.
+ i. exploit STEP0; eauto. i; des.
{ esplits; eauto. left. eapply star_plus_trans; eauto. }
{ esplits; eauto. right. split. eapply star_trans; eauto. inv STAR0; econs; eauto. eapply t_trans; eauto. }
+ { i. eapply PROGRESS. eapply star_safe; eauto. }
+ i. exploit FINAL; eauto. ii. des. esplits; try eapply FINALSRC; eauto. eapply star_trans; eauto.
- econs 2; try apply BSIM; eauto. des. esplits; eauto. { eapply star_trans; eauto. } inv STAR0; econs; eauto.
{ eapply t_trans; eauto. }
Qed.
Lemma x2b_progress:
forall i s1 s2
(SSSRC: forall tr s1' (STAR: Star L1 s1 tr s1'), <<SSSRC: XSIM.(xsim_ss_src) s1'>>)
(SSTGT: forall tr s2' (STAR: Star L2 s2 tr s2'), <<SSTGT: XSIM.(xsim_ss_tgt) s2'>>)
,
match_states i s1 s2 -> safe L1 s1 -> x2b_transitions i s1 s2.
Proof.
intros i0; pattern i0. apply well_founded_ind with (R := order). eapply xsim_order_wf; eauto.
intros i REC s1 s2 ? ? MATCH SAFE. dup MATCH. punfold MATCH0. repeat spc MATCH0. des.
{ (* forward *)
inversion MATCH0; subst. unfold NW in *. destruct (SAFE s1) as [[r FINAL1] | [t [s1' STEP1]]]. apply star_refl.
- (* final state reached *)
inv STEP.
+ eapply x2b_trans_forward_final; try eapply star_refl; eauto. eapply FINAL; eauto.
+ des. pclearbot. inv PLUS.
eapply x2b_trans_forward_stutter; try apply STAR0; try eapply star_refl; eauto.
{ econs; eauto. }
econs 2; eauto.
- inv STEP.
+ (* L1 can make one step *)
hexploit STEP0; eauto. intros [i' [s2' [A MATCH']]]. pclearbot.
assert (B: DPlus mt L2 s2 t s2' \/ (s2 = s2' /\ t = E0 /\ order i' i)).
{ des; eauto. }
clear A. destruct B as [PLUS2 | [EQ1 [EQ2 ORDER]]].
{ eapply x2b_trans_forward_step; eauto. apply star_refl.
i. exploit STEP0; eauto. i; des_safe. pclearbot. esplits; eauto.
}
subst. exploit REC; try apply MATCH'; eauto.
{ ii. eapply SSSRC; eauto. eapply star_left; eauto. }
{ eapply star_safe; eauto. apply star_one; auto. }
i. eapply x2b_transitions_src_tau_rev; eauto. apply star_one; ss.
+ des. pclearbot. clears t. clear t. inv PLUS.
destruct t1, t2; ss. clear_tac.
eapply x2b_trans_forward_stutter; eauto. apply star_refl. econs; eauto. apply rt_refl.
}
{ (* backward *)
econs 4. eapply _xsim_backward_mon_x2b; eauto. eapply _xsim_backward_mon; eauto. i. pclearbot. ss.
}
Qed.
Lemma xsim_simulation_not_E0:
forall s1 t s1', Step L1 s1 t s1' -> t <> E0 ->
forall s2 mt,
receptive_at mt L1 s1 ->
(forall t s1', Step L1 s1 t s1' ->
exists i', exists s2',
(DPlus mt L2 s2 t s2' \/ (s2 = s2' /\ t = E0))
/\ match_states i' s1' s2') ->
exists i', exists s2', DPlus mt L2 s2 t s2' /\ match_states i' s1' s2'.
Proof.
intros. exploit H2; eauto. intros [i' [s2' [A B]]].
exists i'; exists s2'; split; auto. destruct A. auto. des. clarify.
Qed.
(** Exploiting determinacy *)
Lemma determinacy_inv:
forall s2 t' s2' t'' s2'' (mt: match_traces),
determinate_at mt L2 s2 ->
Step L2 s2 t' s2' -> Step L2 s2 t'' s2'' ->
(t' = E0 /\ t'' = E0 /\ s2' = s2'')
\/ (t' <> E0 /\ t'' <> E0 /\ mt t' t'').
Proof.
intros.
assert (mt t' t'').
eapply sd_determ_at; eauto.
destruct (silent_or_not_silent t').
- subst. eapply mt_nil_left in H2. clarify. left; intuition. eapply sd_determ_at; eauto.
- destruct (silent_or_not_silent t'').
+ subst. eapply mt_nil_right in H2. clarify.
+ right; intuition.
Qed.
Lemma determinacy_star:
forall s s1 mt_at, DStar mt_at L2 s E0 s1 ->
forall t s2 s3,
DStep mt_at L2 s1 t s2 -> t <> E0 ->
DStar mt_at L2 s t s3 ->
DStar mt_at L2 s1 t s3.
Proof.
intros s0 s01 mt_at ST0. pattern s0, s01. eapply star_E0_ind; eauto.
intros. inv H3. congruence. destruct H, H1, H4.
exploit determinacy_inv. eexact H. eexact H3. eexact H7.
intros [[EQ1 [EQ2 EQ3]] | [NEQ1 [NEQ2 MT]]].
subst. simpl in *. eauto. congruence.
Qed.
(** Backward simulation of L2 steps *)
Lemma x2b_match_states_bsim
i0_x2b st_src0 st_tgt0
(SSSRC: forall tr st_src1 (STAR: Star L1 st_src0 tr st_src1), <<SSSRC: XSIM.(xsim_ss_src) st_src1>>)
(SSTGT: forall tr st_tgt1 (STAR: Star L2 st_tgt0 tr st_tgt1), <<SSTGT: XSIM.(xsim_ss_tgt) st_tgt1>>)
(MATCH: x2b_match_states i0_x2b st_src0 st_tgt0):
<<BSIM: bsim L1 L2 x2b_order i0_x2b st_src0 st_tgt0>>.
Proof.
red. revert_until match_states.
pcofix CIH. i. rename r into rr. pfold.
assert(PROGRESS: safe L1 st_src0 ->
<<FINAL: exists retv : int, final_state L2 st_tgt0 retv >> \/
<<STEP: exists (tr : trace) (st_tgt1 : state L2), Step L2 st_tgt0 tr st_tgt1 >>).
{ (* PROGRESS *)
generalize dependent st_src0. generalize dependent st_tgt0. pattern i0_x2b.
eapply (well_founded_ind wf_x2b_order). clear i0_x2b. intros ? IH ? ? ? ? ? SAFE. i. inv MATCH.
+ exploit x2b_progress; eauto. intros TRANS; inv TRANS.
* left. esplits; eauto. apply FINALTGT.
* rename H2 into PLUS. inv PLUS. unfold DStep in *. des. right; econstructor; econstructor; eauto.
* right. rename H2 into PLUS. inv PLUS. rename H2 into STEP. inv STEP. esplits; eauto.
* inv BSIM. specialize (STEP SAFE). inv STEP.
{ exploit PROGRESS; eauto. }
{ des. exploit IH; try apply BSIM; eauto.
{ ii. eapply SSSRC; eauto. eapply star_trans; eauto. }
eapply star_safe; eauto. }
+ rename H2 into STARN. inv STARN. congruence. unfold DStep in *. des. right; econstructor; econstructor; eauto.
+ rename H into STARN. inv STARN. unfold SDStep in *. des. right; econstructor; econstructor; eauto.
}
econs; eauto.
assert(FINALLEMMA: forall retv (SAFESRC: safe L1 st_src0) (FINALTGT: final_state L2 st_tgt0 retv),
exists st_src1, <<STAR: Star L1 st_src0 E0 st_src1 >> /\ <<FINAL: final_state L1 st_src1 retv >>).
{ (* FINAL *)
clear - MATCH CIH XSIM SSSRC SSTGT.
generalize dependent MATCH. generalize dependent st_src0. generalize dependent st_tgt0. pattern i0_x2b.
eapply (well_founded_ind wf_x2b_order); eauto. i. rename H into IH. clear i0_x2b.
i. inv MATCH.
+ exploit x2b_progress; eauto. intro TRANS. inv TRANS.
* assert(retv = r). { inv FINALTGT0. eapply DTM; eauto. } clarify. esplits; eauto.
* rename H2 into PLUS. inv PLUS. unfold DStep in *. des. exploit sd_determ_at_final; eauto. contradiction.
* rename H2 into PLUS. inv PLUS. unfold SDStep in *. des. exploit ssd_determ_at_final; eauto. contradiction.
* inv BSIM. hexploit1 STEP; eauto. inv STEP; eauto. des. exploit IH; try apply BSIM; eauto.
{ ii. eapply SSSRC; eauto. eapply star_trans; eauto. }
{ eapply star_safe; eauto. } i; des. esplits; try apply FINAL. eapply star_trans; eauto.
+ rename H2 into STARN. inv STARN. congruence. unfold DStep in *. des. exploit sd_determ_at_final; eauto. contradiction.
+ rename H into STARN. inv STARN. unfold SDStep in *. des. exploit ssd_determ_at_final; eauto. contradiction.
}
{ (* STEP *)
i. inv MATCH.
- (* 1. At matching states *)
exploit x2b_progress; eauto. intros TRANS; inv TRANS.
{ (* final *)
(* 1.1 L1 can reach final state and L2 is at final state: impossible! *)
econs 1; ss; eauto.
i. inv FINALTGT. exploit DTM0; eauto. i; ss.
}
{ (* forward *)
(* 1.2 L1 can make 0 or several steps; L2 can make 1 or several matching steps. *)
econs 1; ss; eauto.
i. rename H3 into H4. inv H2.
exploit STEP; eauto. intros [i''' [s2''' [STEP''' MATCH''']]].
destruct H3. exploit determinacy_inv. eexact H2. eexact H3. eexact STEPTGT.
intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
(* 1.2.1 L2 makes a silent transition *)
+ destruct (silent_or_not_silent t2).
* (* 1.2.1.1 L1 makes a silent transition too: perform transition now and go to "after" state *)
subst. simpl in *. destruct (star_starN H5) as [n STEPS2].
exists (X2BI_after n i''); exists s1''; split.
left. eapply plus_right; eauto. right. eapply CIH.
{ ii. eapply SSSRC; eauto. eapply star_trans; eauto. eapply star_left; eauto. }
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
eapply x2b_match_after'; eauto. eapply DStarN_E0_SDStarN; eauto.
* (* 1.2.1.2 L1 makes a non-silent transition: keep it for later and go to "before" state *)
subst. simpl in *. destruct (star_starN H5) as [n STEPS2].
exists (X2BI_before n); exists s1'; split. right; split. auto. constructor. right. eapply CIH.
{ ii. eapply SSSRC; eauto. eapply star_trans; eauto. }
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
econstructor. eauto. auto. apply star_one; eauto. eauto. eauto.
intros. exploit STEP; eauto. intros [i'''' [s2'''' [A MATCH'''']]].
exists i''''. exists s2''''. destruct A as [?|[? ?]]; auto.
des; clarify. esplits; eauto.
+ (* 1.2.2 L2 makes a non-silent transition, and so does L1 *)
des; cycle 1.
{ clarify. destruct t1; ss. }
exploit not_silent_length. eapply (sr_traces_at RECEPTIVE); eauto. intros [EQ | EQ]. congruence.
subst t2. rewrite E0_right in H1.
(* Use receptiveness to equate the traces *)
exploit (sr_receptive_at RECEPTIVE); eauto. intros [s1''' STEP1].
exploit xsim_simulation_not_E0. eexact STEP1. auto. eauto.
intros. exploit STEP; eauto. intros [i'''' [s2'''' [A MATCH'''']]].
exists i''''. exists s2''''. destruct A as [?|[? ?]]; split; eauto.
{ des. left. eauto. }
{ des. clarify. right. esplits; eauto. }
intros [i'''' [s2'''' [P Q]]]. inv P.
(* Exploit determinacy *)
destruct H6. exploit sd_determ_at. eauto. eexact STEPTGT. eexact H8.
exploit not_silent_length. eapply (sr_traces_at RECEPTIVE); eauto. intros [EQ | EQ].
subst t0. simpl in *. intros. elim NOT2. destruct H9. eapply mt_nil_right in H9. clarify.
subst t2. rewrite E0_right in *. intros [_ TRACES]. assert (s0 = st_tgt1). symmetry. eapply TRACES. auto. subst s0.
(* Perform transition now and go to "after" state *)
destruct (star_starN H7) as [n STEPS2]. exists (X2BI_after n i''''); exists s1'''; split. left. eapply plus_right; eauto.
right. eapply CIH.
{ ii. eapply SSSRC; eauto. eapply star_trans; eauto. eapply star_left; eauto. }
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
eapply x2b_match_after'; eauto. eapply DStarN_E0_SDStarN; eauto.
}
{ econs 1; ss; eauto.
i. inv H2.
- destruct t1, t2; ss. clear_tac.
exploit ssd_determ_at. apply H4. apply H4. apply STEPTGT. i; des. clarify.
destruct H4. clear_tac. destruct (star_starN H5) as [n STEPS2]. destruct n.
+ inv STEPS2. ss. exists (X2BI_after 0 i''). esplits; eauto.
* right. esplits; eauto. econs; eauto. eapply clos_t_rt; eauto.
* right. eapply CIH.
{ ii. eapply SSSRC; eauto. eapply star_trans; eauto. }
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
econs; eauto.
+ exists (X2BI_after (S n) i''). esplits; eauto.
* right. esplits; eauto. econs; eauto. eapply clos_t_rt; eauto.
* right. eapply CIH.
{ ii. eapply SSSRC; eauto. eapply star_trans; eauto. }
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
econs 3; eauto.
}
{ (* backward *)
inv BSIM. exploit STEP; eauto. i. inv H0.
- econs 1; eauto. i. exploit STEP0; eauto. i; des_safe.
esplits; eauto. right. eapply CIH; eauto.
{ ii. eapply SSSRC; eauto. des.
- eapply plus_star. eapply plus_star_trans; eauto. - eapply star_trans; eauto. }
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
- econs 2; eauto.
right. eapply CIH; et.
{ ii. eapply SSSRC; eauto. des. eapply star_trans; eauto. }
}
- (* 2. Before *)
econs 1; ss; eauto.
i. assert(DUMMY_PROP) by ss. inv H2. congruence. destruct H5.
exploit determinacy_inv. eauto. eexact H5. eexact STEPTGT.
intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
+ (* 2.1 L2 makes a silent transition: remain in "before" state *)
subst. simpl in *. exists (X2BI_before n0); exists st_src0; split.
right; split. apply star_refl. constructor. omega. right. eapply CIH; et.
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
econstructor; eauto. eapply star_right; eauto.
+ (* 2.2 L2 make a non-silent transition *)
assert(RECEPTIVE : receptive_at mt L1 st_src0).
{ exploit H3; eauto. i; des; clarify. }
exploit not_silent_length. eapply (sr_traces_at RECEPTIVE); eauto. intros [EQ | EQ]. congruence.
subst. rewrite E0_right in *.
(* Use receptiveness to equate the traces *)
exploit (sr_receptive_at RECEPTIVE); eauto. intros [s1''' STEP1].
exploit xsim_simulation_not_E0. eexact STEP1. auto. eauto.
{ i. exploit H3; eauto. i; des; eauto. clarify. esplits; eauto. }
intros [i''' [s2''' [P Q]]].
(* Exploit determinacy *)
exploit determinacy_star. eauto. split; auto. eexact STEPTGT. auto. apply plus_star; eauto.
intro R. inv R. congruence.
exploit not_silent_length. eapply (sr_traces_at RECEPTIVE); eauto. intros [EQ | EQ].
subst. simpl in *. destruct H7. exploit sd_determ_at. eauto. eexact STEPTGT. eexact H9.
intros. elim NOT2. destruct H10. eapply mt_nil_right in H10. clarify.
subst. rewrite E0_right in *. destruct H7.
assert (s2 = st_tgt1). eapply sd_determ_at; eauto. subst s2.
(* Perform transition now and go to "after" state *)
destruct (star_starN H8) as [n STEPS2]. exists (X2BI_after n i'''); exists s1'''; split.
left. apply plus_one; auto. right. eapply CIH; et.
{ ii. eapply SSSRC; eauto. eapply star_left; eauto. }
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
eapply x2b_match_after'; eauto. eapply DStarN_E0_SDStarN; eauto.
- (* 3. After *)
econs 1; ss; eauto.
i. inv H. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst.
destruct H2. exploit ssd_determ_at. eapply H. eexact H1. eexact STEPTGT. i; des. clarify.
exists (X2BI_after n i); exists st_src0; split.
right; split. apply star_refl. constructor. constructor; omega. right. eapply CIH; et.
{ ii. eapply SSTGT; eauto. eapply star_left; eauto. }
eapply x2b_match_after'; eauto.
}
Qed.