From 6f329db7c258b95e2e78e7b4faef946967302778 Mon Sep 17 00:00:00 2001 From: alxest Date: Wed, 18 Mar 2020 15:32:22 +0900 Subject: [PATCH] Refactored & compiles --- bound/LowerBound.v | 2 +- bound/UpperBound_A.v | 7 +- bound/UpperBound_B.v | 59 +++++++------ common/BehaviorsC.v | 54 ++++++++++++ demo/mutrec/MutrecABproof.v | 2 +- driver/SepComp.v | 19 ---- proof/AdequacyLocal.v | 102 ++++++++++++++-------- proof/Simulation.v | 170 +++++++++++++++--------------------- 8 files changed, 228 insertions(+), 187 deletions(-) diff --git a/bound/LowerBound.v b/bound/LowerBound.v index a8f5fb48..755fbb34 100644 --- a/bound/LowerBound.v +++ b/bound/LowerBound.v @@ -2364,7 +2364,7 @@ Section PRESERVATION. Lemma transf_xsim_properties: xsim_properties (sem prog) (semantics tprog) nat lt. Proof. - econs; try apply progress_top; ss; [apply lt_wf| |i; apply symb_preserved]. + econs; try apply preservation_top; ss; [apply lt_wf| |i; apply symb_preserved]. econs. i. exploit (transf_initial_states); eauto. i. des. esplits. econs; eauto. diff --git a/bound/UpperBound_A.v b/bound/UpperBound_A.v index 51cdacb2..3c658e3a 100644 --- a/bound/UpperBound_A.v +++ b/bound/UpperBound_A.v @@ -822,6 +822,7 @@ Section PRESERVATION. destruct frs_tgt; ss. { exploit match_stacks_right_nil; et. i; des. clarify. } rename t into fr_tgt. + ii. clear SSSRC SSTGT. destruct (classic (fr_tgt.(Frame.ms).(ModSem.is_call) fr_tgt.(Frame.st))). (* tgt call *) (* fsim *) @@ -1527,7 +1528,7 @@ i. des_safe. inv H0. unfold is_call_cont_strong. auto. } exploit preservation_cp_focus; eauto. } exploit match_stacks_focus; eauto. } (* call state *) - - right. econs; ss; et. + - right. clear SSSRC SSTGT. econs; ss; et. i. econs; cycle 1. { i. specialize (SAFESRC _ (star_refl _ _ _ _)). des; ss. @@ -1595,7 +1596,7 @@ i. des_safe. inv H0. unfold is_call_cont_strong. auto. } Theorem upperbound_a_xsim : <>. Proof. - econs; ss; eauto. econs; try apply progress_top; ss; eauto. + econs; ss; eauto. econs; try apply preservation_top; ss; eauto. { eapply unit_ord_wf. } { econs 1. ii. inversion INITSRC. exploit init_fsim; eauto. i; des. esplits; eauto. @@ -1624,7 +1625,7 @@ Proof. eapply mixed_to_backward_simulation. destruct (link_sk (ctx ++ [module cp_link])) eqn:LINKSK; cycle 1. { econs; et. - econs; try apply progress_top; et. + econs; try apply preservation_top; et. { eapply unit_ord_wf. } { econs; et. i. ss. inv INITSRC. clarify. } i; des. ss. des_ifs. diff --git a/bound/UpperBound_B.v b/bound/UpperBound_B.v index adc89352..f8efb3af 100644 --- a/bound/UpperBound_B.v +++ b/bound/UpperBound_B.v @@ -1281,7 +1281,7 @@ Section PRESERVATION. subst. ss. } exploit Genv.find_funct_inversion; eauto. i; des. f_equal. inv WTPROG. exploit CSTYLE_EXTERN; eauto. i. des_ifs. f_equal. eapply H3; eauto. } - { inv SSSRC; ss. exploit WTKS; eauto. { ii. clarify. } esplits; ss; eauto. rr. des. des_ifs. } + { specialize (SSSRC _ _ (star_refl _ _ _ _)). inv SSSRC; ss. exploit WTKS; eauto. { ii. clarify. } esplits; ss; eauto. rr. des. des_ifs. } (* internal *) ++ exploit progress_step; eauto. * inv MTCHST. @@ -1292,36 +1292,40 @@ Section PRESERVATION. { inv INITTGT. } Qed. + Hypothesis INITSAFE: forall st (INIT: Smallstep.initial_state (semantics prog) st), + <>. + Lemma transf_xsim_properties: xsim_properties (Csem.semantics prog) (Sem.sem tprog) nat lt. Proof. - econstructor 1 with (ss_src := wt_state prog ge) (ss_tgt := top1); - ss; [| |apply lt_wf| |i; apply symb_preserved]. - { clear - MAIN_INTERNAL tprog WTPROG SKEWF LINK_SK_TGT. - ii. inv INIT. - destruct (classic (exists fd, Genv.find_funct (globalenv prog) (Vptr b Ptrofs.zero) = Some (Internal fd))). - - eapply wt_initial_state; ss; eauto. - { i. rr. rewrite Genv.find_def_symbol. esplits; eauto. } - { des. ii. - destruct SKEWF. - destruct match_ge_skenv_link. - specialize (mge_defs blk). inv mge_defs. - { ss. unfold Genv.find_def in DEF. unfold fundef, genv_genv in *. ss. - symmetry in H5. Eq. } - ss. unfold Genv.find_def in DEF. unfold fundef, genv_genv in *. ss. - symmetry in H4. Eq. - symmetry in H5. exploit DEFSYMB; eauto. i. des. - unfold Genv.find_symbol in *. rewrite mge_symb in H4. eauto. } - - ss. des_ifs. - specialize (SAFE _ (star_refl _ _ _ _)). des; inv SAFE; ss. - { inv H4. } - { contradict H3. inv H4; ss; des_ifs; rewrite FPTR in *; eauto. - exploit MAIN_INTERNAL; eauto. - { econs; eauto. } - i; des. ss. des_ifs. - } + econstructor 1 with (xsim_ss_src := wt_state prog ge) (xsim_ss_tgt := top1); + ss; [|apply lt_wf| |i; apply symb_preserved]. + { clear - MAIN_INTERNAL tprog WTPROG SKEWF LINK_SK_TGT INITSAFE WTSK WT_EXTERNAL INCL. + econs. + - ii. hexploit INITSAFE; eauto. intro SAFE. inv INIT. + destruct (classic (exists fd, Genv.find_funct (globalenv prog) (Vptr b Ptrofs.zero) = Some (Internal fd))). + + eapply wt_initial_state; ss; eauto. + { i. rr. rewrite Genv.find_def_symbol. esplits; eauto. } + { des. ii. + destruct SKEWF. + destruct match_ge_skenv_link. + specialize (mge_defs blk). inv mge_defs. + { ss. unfold Genv.find_def in DEF. unfold fundef, genv_genv in *. ss. + symmetry in H5. Eq. } + ss. unfold Genv.find_def in DEF. unfold fundef, genv_genv in *. ss. + symmetry in H4. Eq. + symmetry in H5. exploit DEFSYMB; eauto. i. des. + unfold Genv.find_symbol in *. rewrite mge_symb in H4. eauto. } + + ss. des_ifs. + specialize (SAFE _ (star_refl _ _ _ _)). des; inv SAFE; ss. + { inv H4. } + { contradict H3. inv H4; ss; des_ifs; rewrite FPTR in *; eauto. + exploit MAIN_INTERNAL; eauto. + { econs; eauto. } + i; des. ss. des_ifs. + } + - ii. eapply preservation_prog; eauto. rewrite <- senv_same; et. } - { ii. eapply preservation_prog; eauto. rewrite <- senv_same; et. } econs. i. exploit (transf_initial_states); eauto. i. des. esplits. econs; eauto. @@ -1376,6 +1380,7 @@ Proof. + exploit IHl; eauto. - split; unfold link_sk, link_list in *; ss; unfold link_prog in *; des_ifs. } rewrite T2 in H0. clarify. } + eapply improves_free_theorem; i. eapply bsim_improves. eapply mixed_to_backward_simulation. inv TYPED. diff --git a/common/BehaviorsC.v b/common/BehaviorsC.v index 84aeb4d9..17a5333b 100644 --- a/common/BehaviorsC.v +++ b/common/BehaviorsC.v @@ -34,3 +34,57 @@ Proof. eapply backward_to_compcert_backward_simulation; eauto. Qed. +Lemma back_propagate_ub_behav + beh0 + (INITUB: behavior_improves beh0 (Goes_wrong E0)): + <>. +Proof. + rr in INITUB. des; clarify; et. + rr in INITUB0. des. unfold behavior_app in *. des_ifs. destruct t; ss. +Qed. + +Lemma back_propagate_ub_program + sem0 sem1 + (IMPR: improves sem0 sem1) + (INITUB: program_behaves sem1 (Goes_wrong E0)): + <>. +Proof. + exploit IMPR; eauto. i; des. + hexploit back_propagate_ub_behav; et. i ;des. clarify. +Qed. + +Lemma improves_free_theorem + L1 L2 + (IMPRV: forall + (INITSAFE: exists st, <>) + (INITSAFE: forall st (INIT: Smallstep.initial_state L1 st), + <>) + , + improves L1 L2) + : + <> +. +Proof. + destruct (classic (exists st, <>)); cycle 1. + { clear - H. + ii. + exists (Goes_wrong []). esplits; ss; eauto using behavior_improves_bot. + econs 2; eauto. + } + destruct (classic (forall st (INIT: Smallstep.initial_state L1 st), <>)); cycle 1. + { clear - H0. rename H0 into H. + ii. + exists (Goes_wrong []). esplits; ss; eauto. + - apply Classical_Pred_Type.not_all_ex_not in H. des. + apply Classical_Prop.imply_to_and in H. des. + econs 1; eauto. + clear - H0. + apply Classical_Pred_Type.not_all_ex_not in H0. des. + repeat (apply_all_once Classical_Prop.imply_to_and; des). + apply Classical_Prop.not_or_and in H1. des. + econs 4; eauto. + ii. eapply H2; eauto. + - eapply behavior_improves_bot; eauto. + } + eauto. +Qed. diff --git a/demo/mutrec/MutrecABproof.v b/demo/mutrec/MutrecABproof.v index 08573e99..32c84cca 100644 --- a/demo/mutrec/MutrecABproof.v +++ b/demo/mutrec/MutrecABproof.v @@ -1064,7 +1064,7 @@ Proof. eapply bsim_improves. eapply mixed_to_backward_simulation. econs; eauto. - econs; try apply progress_top; eauto; swap 2 3. + econs; try apply preservation_top; eauto; swap 2 3. { instantiate (1:= Zwf.Zwf 0%Z). eapply Zwf.Zwf_well_founded. } { i; des. ss. inv SAFESRC. rewrite INITSK. exploit link_sk_same; ss. i. erewrite H. des_ifs. } diff --git a/driver/SepComp.v b/driver/SepComp.v index 161811c8..77f1e428 100644 --- a/driver/SepComp.v +++ b/driver/SepComp.v @@ -4,25 +4,6 @@ Require Import CoqlibC. Require Import BehaviorsC LinkingC EventsC MapsC ASTC CtypesC. -Lemma back_propagate_ub_behav - beh0 - (INITUB: behavior_improves beh0 (Goes_wrong E0)): - <>. -Proof. - rr in INITUB. des; clarify; et. - rr in INITUB0. des. unfold behavior_app in *. des_ifs. destruct t; ss. -Qed. - -Lemma back_propagate_ub_program - sem0 sem1 - (IMPR: improves sem0 sem1) - (INITUB: program_behaves sem1 (Goes_wrong E0)): - <>. -Proof. - exploit IMPR; eauto. i; des. - hexploit back_propagate_ub_behav; et. i ;des. clarify. -Qed. - Theorem separate_compilation_correct (srcs: list Csyntax.program) (tgts: list Asm.program) builtins src_link (TYPECHECKS: Forall (fun src => CsemC.typechecked builtins src) srcs) diff --git a/proof/AdequacyLocal.v b/proof/AdequacyLocal.v index 14c2e61b..7a6f6a7a 100644 --- a/proof/AdequacyLocal.v +++ b/proof/AdequacyLocal.v @@ -493,8 +493,9 @@ Section ADQSTEP. Theorem lxsim_lift_xsim i0 st_src0 st_tgt0 sm0 (LXSIM: lxsim_lift sk_link_src sk_link_tgt i0 st_src0 st_tgt0 sm0) - (SUST: sound_state pp st_src0): - <>. + : + <> + . Proof. generalize dependent sm0. generalize dependent st_src0. generalize dependent st_tgt0. generalize dependent i0. pcofix CIH. i. pfold. inv LXSIM; ss; cycle 1. @@ -532,9 +533,6 @@ Section ADQSTEP. clears st_init0; clear st_init0. esplits; eauto. - left. apply plus_one. econs; eauto. econs; eauto. - right. eapply CIH. - { unsguard SUST. unfold __GUARD__. des. eapply sound_progress; eauto. - ss. folder. des_ifs. econs 2; eauto. econs; eauto. - } instantiate (1:= sm_init). econs; try apply SIM0; eauto. + ss. folder. des_ifs. eapply mfuture_preserves_sim_ge; eauto. apply rtc_once. et. + etrans; eauto. @@ -544,10 +542,9 @@ Section ADQSTEP. } sguard in SESRC. sguard in SETGT. folder. rewrite LINKSRC in *. rewrite LINKTGT in *. - punfold TOP. rr in TOP. hexploit1 TOP; eauto. - { unsguard SUST. des. - ii. exploit sound_progress_star; eauto. { eapply lift_star; eauto. } intro SUST0; des. inv SUST0. des. - simpl_depind. clarify. i. hexploit FORALLSU; eauto. i; des. + punfold TOP. rr in TOP. ii. hexploit1 TOP; eauto. + { ii. exploit SSSRC. { eapply lift_star; eauto. } intro SUST0; des. inv SUST0. des. + simpl_depind. clarify. hexploit FORALLSU; eauto. i; des. specialize (H (sound_states_local si)). esplits; eauto. eapply H; eauto. } inv TOP. @@ -573,7 +570,6 @@ Section ADQSTEP. - right. esplits; eauto. clarify. } pclearbot. right. eapply CIH with (sm0 := sm1); eauto. - { unsguard SUST. des_safe. eapply sound_progress; eauto. eapply lift_step; eauto. } econs; eauto. { ss. folder. des_ifs. eapply mfuture_preserves_sim_ge; eauto. apply rtc_once; eauto. } { etransitivity; eauto. } @@ -602,17 +598,12 @@ Section ADQSTEP. - right. esplits; eauto. eapply lift_star; eauto. } pclearbot. right. eapply CIH with (sm0 := sm1); eauto. - { unsguard SUST. des_safe. destruct H. - - eapply sound_progress_plus; eauto. eapply lift_plus; eauto. - - des_safe. eapply sound_progress_star; eauto. eapply lift_star; eauto. - } econs; eauto. { folder. ss; des_ifs. eapply mfuture_preserves_sim_ge; eauto. apply rtc_once; eauto. } etransitivity; eauto. + des. pclearbot. econs 2. { esplits; eauto. eapply lift_star; eauto. } right. eapply CIH; eauto. - { unsguard SUST. des_safe. eapply sound_progress_star; eauto. eapply lift_star; eauto. } instantiate (1:=sm1). econs; eauto. { folder. ss; des_ifs. eapply mfuture_preserves_sim_ge; eauto. eapply rtc_once; eauto. } { etrans; eauto. } @@ -631,7 +622,6 @@ Section ADQSTEP. { eapply lift_determinate_at; et. { unsguard SETGT. ss. des_ifs. } eapply at_external_determinate_at; et. } des_ifs. econs 1; eauto. + right. eapply CIH; eauto. - { unsguard SUST. des_safe. eapply sound_progress; eauto. ss. folder. des_ifs_safe. econs; eauto. } { instantiate (1:= sm_arg). econs 2; eauto. * ss. folder. des_ifs. eapply mfuture_preserves_sim_ge; eauto. econs 2; et. * instantiate (1:= sm_arg). econs; [eassumption|..]; revgoals; ss. @@ -664,7 +654,8 @@ Section ADQSTEP. determ_tac ModSem.final_frame_dtm. clear_tac. exploit K; try apply SIMRETV; eauto. { etransitivity; eauto. etrans; eauto. } - { unsguard SUST. des_safe. inv SUST. des. simpl_depind. clarify. i. inv TL. simpl_depind. clarify. des. + { exploit SSSRC. { eapply star_refl. } intro T; des. inv T. des. simpl_depind. clarify. + inv TL. simpl_depind. clarify. des. exploit FORALLSU0; eauto. i; des. esplits; eauto. eapply HD; eauto. } i; des. esplits; eauto. @@ -674,8 +665,6 @@ Section ADQSTEP. { eapply lift_determinate_at. { unsguard SETGT. ss. des_ifs. } eapply final_frame_determinate_at; et. } econs 4; ss; eauto. + right. eapply CIH; eauto. - { unsguard SUST. des_safe. eapply sound_progress; eauto. - ss. folder. des_ifs_safe. econs; eauto. } instantiate (1:= sm_after). econs; ss; cycle 3; eauto. { folder. des_ifs. eapply mfuture_preserves_sim_ge; et. econs 2; et. } { etrans; eauto. } @@ -700,22 +689,38 @@ Section ADQ. Let sem_src := Sem.sem p_src. Let sem_tgt := Sem.sem p_tgt. - Theorem adequacy_local: mixed_simulation sem_src sem_tgt. + Variable sk_link_src sk_link_tgt: Sk.t. + Hypothesis LINKSRC: (link_sk p_src) = Some sk_link_src. + Hypothesis LINKTGT: (link_sk p_tgt) = Some sk_link_tgt. + + Let lxsim_lift := (lxsim_lift pp). + Hint Unfold lxsim_lift. + + Let skenv_link_src := (Sk.load_skenv sk_link_src). + Let skenv_link_tgt := (Sk.load_skenv sk_link_tgt). + Variable ss_link: SimSymb.t. + Hypothesis (SIMSKENV: exists sm, SimSymb.sim_skenv sm ss_link skenv_link_src skenv_link_tgt). + + Hypothesis (INCLSRC: forall mp (IN: In mp pp), SkEnv.includes skenv_link_src (Mod.sk mp.(ModPair.src))). + Hypothesis (INCLTGT: forall mp (IN: In mp pp), SkEnv.includes skenv_link_tgt (Mod.sk mp.(ModPair.tgt))). + Hypothesis (SSLE: forall mp (IN: In mp pp), SimSymb.le mp.(ModPair.ss) ss_link). + + Hypothesis (WFSKSRC: forall md (IN: In md (ProgPair.src pp)), <>). + Hypothesis (WFSKTGT: forall md (IN: In md (ProgPair.tgt pp)), <>). + + Theorem adequacy_local_aux: mixed_simulation sem_src sem_tgt. Proof. subst_locals. econstructor 1 with (order := ord); eauto. generalize wf_ord; intro WF. - destruct (classic (pp <> [])); cycle 1. - { apply NNPP in H. clarify. ss. econs; try apply progress_top; eauto. - econs; eauto. ii. ss. inv INITSRC. ss. } - rename H into NOTNIL. econs; try apply progress_top; eauto. - - econs 1; ss; eauto. ii. inv INITSRC. - exploit sim_link_sk; eauto. i; des. - exploit init_lxsim_lift_forward; eauto. { econs; eauto. } i; des. + econstructor; eauto. + - instantiate (1:= sound_state pp). econs. + + eapply sound_init; ss; eauto. + + eapply sound_progress; eauto. + - apply preservation_top. + - econs 1; ss; eauto. ii. + exploit init_lxsim_lift_forward; eauto. { destruct pp; ss. } i; des. assert(WFTGT: forall md, In md (ProgPair.tgt pp) -> <>). { inv INITTGT. inv INIT. ss. } hexploit lxsim_lift_xsim; eauto. - { exploit SimSymb.wf_load_sim_skenv; et. { rewrite SKSRC; et. } i; des. esplits. rp; et; try congruence. } - { rewrite Forall_forall in *. eauto. } - eapply sound_init; eauto. econs; eauto. - ss. i; des. inv SAFESRC. exploit sim_link_sk; eauto. i; des. des_ifs. exploit SimSymb.wf_load_sim_skenv; eauto. i; des. clarify. @@ -724,11 +729,40 @@ Section ADQ. all: ss. Qed. - Goal BehaviorsC.improves sem_src sem_tgt. - Proof. eapply bsim_improves; eauto. eapply mixed_to_backward_simulation; eauto. eapply adequacy_local. Qed. - End ADQ. + + +Section BEH. + + Context `{SM: SimMem.class}. + Context {SS: SimSymb.class SM}. + Context `{SU: Sound.class}. + + Variable pp: ProgPair.t. + Hypothesis SIMPROG: ProgPair.sim pp. + Let p_src := (ProgPair.src pp). + Let p_tgt := (ProgPair.tgt pp). + Let sem_src := Sem.sem p_src. + Let sem_tgt := Sem.sem p_tgt. + + Theorem adequacy_local: BehaviorsC.improves sem_src sem_tgt. + Proof. + eapply improves_free_theorem; i. + eapply bsim_improves; eauto. eapply mixed_to_backward_simulation; eauto. + + des. inv INIT. ss. exploit sim_link_sk; eauto. i; des. clarify. + exploit init_lxsim_lift_forward; eauto. { destruct pp; ss. } { econs; eauto. } i; des. + exploit SimSymb.wf_load_sim_skenv; eauto. i; des. clarify. + eapply adequacy_local_aux; ss; eauto. + { rewrite Forall_forall in *. ss. } + { inv INITTGT. inv INIT. ss. } + Qed. + +End BEH. + + + Program Definition mkPR (MR: SimMem.class) (SR: SimSymb.class MR) (MP: Sound.class) : program_relation.t := program_relation.mk (fun (p_src p_tgt: program) => @@ -750,8 +784,6 @@ Next Obligation. (* adequacy *) destruct (classic (forall x (IN: In x p_src), Sk.wf x)) as [WF|NWF]; cycle 1. { eapply sk_nwf_improves; auto. } - eapply bsim_improves. - eapply mixed_to_backward_simulation. specialize (REL WF). des. clarify. eapply (@adequacy_local MR SR MP). auto. Qed. diff --git a/proof/Simulation.v b/proof/Simulation.v index 16e967db..b5ba8227 100644 --- a/proof/Simulation.v +++ b/proof/Simulation.v @@ -313,21 +313,24 @@ Inductive Dinitial_state (L: semantics) (st: L.(state)): Prop := st0 = st1). -Lemma progress_top - {L} - : - forall st0 tr st1 (SS: top1 st0) (STEP: Step L st0 tr st1), (<>) +Record preservation {L: semantics} (sound_state: L.(state) -> Prop): Prop := +{ + prsv_initial: forall st (INIT: L.(initial_state) st), (<>); + prsv_step: forall st0 tr st1 (SS: sound_state st0) (STEP: Step L st0 tr st1), (<>); +} . -Proof. ss. Qed. -Theorem progress_star - {L} {sound_state: _ -> Prop} - (PRSVSTEP: forall st0 tr st1 (SS: sound_state st0) (STEP: Step L st0 tr st1), (<>)) +Theorem preservation_top: forall {L}, <>. +Proof. ii. econs; eauto. Qed. + +Theorem prsv_star + L sound_state + (PRSV: preservation sound_state) : (<>)>>) . Proof. - ii. ginduction STAR; ii; ss. eapply IHSTAR; eauto. eapply PRSVSTEP; eauto. + ii. ginduction STAR; ii; ss. eapply IHSTAR; eauto. eapply prsv_step; eauto. Qed. Module GENMT. @@ -470,8 +473,8 @@ Section MIXED_SIM. Variable order: index -> index -> Prop. Variable ss_src: L1.(state) -> Prop. Variable ss_tgt: L2.(state) -> Prop. - Hypothesis (PRSVSRC: forall st0 tr st1 (SS: ss_src st0) (STEP: Step L1 st0 tr st1), (<>)). - Hypothesis (PRSVTGT: forall st0 tr st1 (SS: ss_tgt st0) (STEP: Step L2 st0 tr st1), (<>)). + 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 @@ -503,8 +506,8 @@ Section MIXED_SIM. <>). Definition _xsim xsim (i0: index) (st_src0: state L1) (st_tgt0: state L2): Prop := forall - (SSSRC: ss_src st_src0) - (SSTGT: ss_tgt st_tgt0) + (SSSRC: forall tr st_src1 (STAR: Star L1 st_src0 tr st_src1), <>) + (SSTGT: forall tr st_tgt1 (STAR: Star L2 st_tgt0 tr st_tgt1), <>) , (<>) . @@ -532,36 +535,6 @@ Section MIXED_SIM. - econs 2; eauto. eapply _xsim_backward_mon; eauto. Qed. - Section TEST. - Definition xsim2: _ -> _ -> _ -> Prop := paco3 (_xsim_forward \4/ _xsim_backward) bot3. - Goal xsim2 <3= xsim. - pcofix CIH. ii. pfold. ii. exploit CIH; eauto. i. - rr in PR. punfold PR; cycle 1. - { ii. des; eauto using _xsim_forward_mon, _xsim_backward_mon. } - des. - - left. eapply _xsim_forward_mon; eauto. ii. pclearbot. right. eauto. - - right. eapply _xsim_backward_mon; eauto. ii. pclearbot. right. eauto. - Qed. - Definition xsim3: _ -> _ -> _ -> Prop := fun i st_src st_tgt => - forall (SSSRC: ss_src st_src) (SSTGT: ss_tgt st_tgt), - (paco3 (_xsim_forward \4/ _xsim_backward) bot3) i st_src st_tgt. - Goal xsim3 <3= xsim. - pcofix CIH. ii. pfold. ii. exploit CIH; eauto. i. - rr in PR. repeat spc PR. punfold PR; cycle 1. - { ii. des; eauto using _xsim_forward_mon, _xsim_backward_mon. } - des. - - left. eapply _xsim_forward_mon; eauto. ii. pclearbot. right. eapply CIH; ii; eauto. - - right. eapply _xsim_backward_mon; eauto. ii. pclearbot. right. eapply CIH; ii; eauto. - Qed. - Goal xsim <3= xsim3. - pcofix CIH. ii. pfold. ii. exploit CIH; eauto. i. - rr in PR. punfold PR; cycle 1. - { eapply xsim_mon. } - rr in PR. repeat spc PR. des. - - left. eapply _xsim_forward_mon; eauto. ii. pclearbot. right. - Abort. - End TEST. - End MIXED_SIM. Hint Unfold xsim. @@ -591,14 +564,12 @@ Inductive xsim_init_sim (L1 L2: semantics) (index: Type) (order: index -> index Record xsim_properties (L1 L2: semantics) (index: Type) (order: index -> index -> Prop): Type := { - ss_src: L1.(state) -> Prop; - ss_tgt: L2.(state) -> Prop; - xsim_initial_sound_src: forall st (INIT: initial_state L1 st) (SAFE: safe L1 st), <>; - xsim_initial_sound_tgt: forall st (INIT: initial_state L2 st), <>; - xsim_progress_src: forall st0 tr st1 (SS: ss_src st0) (STEP: Step L1 st0 tr st1), (<>); - xsim_progress_tgt: forall st0 tr st1 (SS: ss_tgt st0) (STEP: Step L2 st0 tr st1), (<>); + 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: <>; - xsim_initial_states_sim: <>; + xsim_initial_states_sim: <>; }. Arguments xsim_properties: clear implicits. @@ -621,7 +592,7 @@ Variable index: Type. Variable order: index -> index -> Prop. Hypothesis XSIM: xsim_properties L1 L2 index order. -Let match_states := xsim L1 L2 order XSIM.(ss_src) XSIM.(ss_tgt). +Let match_states := xsim L1 L2 order XSIM.(xsim_ss_src) XSIM.(xsim_ss_tgt). (** Orders *) @@ -758,7 +729,10 @@ Proof. Qed. Lemma x2b_progress: - forall i s1 s2 (SSSRC: XSIM.(ss_src) s1) (SSTGT: XSIM.(ss_tgt) s2), + forall i s1 s2 + (SSSRC: forall tr s1' (STAR: Star L1 s1 tr s1'), <>) + (SSTGT: forall tr s2' (STAR: Star L2 s2 tr 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. @@ -783,7 +757,7 @@ Proof. i. exploit STEP0; eauto. i; des_safe. pclearbot. esplits; eauto. } subst. exploit REC; try apply MATCH'; eauto. - { eapply xsim_progress_src; 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. @@ -846,8 +820,8 @@ Qed. Lemma x2b_match_states_bsim i0_x2b st_src0 st_tgt0 - (SSSRC: XSIM.(ss_src) st_src0) - (SSTGT: XSIM.(ss_tgt) st_tgt0) + (SSSRC: forall tr st_src1 (STAR: Star L1 st_src0 tr st_src1), <>) + (SSTGT: forall tr st_tgt1 (STAR: Star L2 st_tgt0 tr st_tgt1), <>) (MATCH: x2b_match_states i0_x2b st_src0 st_tgt0): <>. Proof. @@ -866,7 +840,8 @@ Proof. * inv BSIM. specialize (STEP SAFE). inv STEP. { exploit PROGRESS; eauto. } { des. exploit IH; try apply BSIM; eauto. - eapply (progress_star XSIM.(xsim_progress_src)); eauto. eapply star_safe; 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. } @@ -883,7 +858,7 @@ Proof. * 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. - { eapply (progress_star XSIM.(xsim_progress_src)); 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. @@ -910,14 +885,14 @@ Proof. 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. - { eapply (progress_star XSIM.(xsim_progress_src)); eauto. eapply star_right; et. } - { eapply (xsim_progress_tgt); eauto. } + { 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. - { eapply (progress_star XSIM.(xsim_progress_src)); eauto. } - { eapply (xsim_progress_tgt); eauto. } + { 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. @@ -943,8 +918,8 @@ Proof. (* 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. - { eapply (progress_star XSIM.(xsim_progress_src)); eauto. eapply star_right; et. } - { eapply (xsim_progress_tgt); eauto. } + { 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. @@ -955,27 +930,26 @@ Proof. + inv STEPS2. ss. exists (X2BI_after 0 i''). esplits; eauto. * right. esplits; eauto. econs; eauto. eapply clos_t_rt; eauto. * right. eapply CIH. - { eapply (progress_star XSIM.(xsim_progress_src)); eauto. } - { eapply (xsim_progress_tgt); eauto. } + { 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. - { eapply (progress_star XSIM.(xsim_progress_src)); eauto. } - { eapply (xsim_progress_tgt); eauto. } + { 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. - assert(SSSRC1: XSIM.(ss_src) st_src1). - { des; eapply (progress_star XSIM.(xsim_progress_src)); eauto. eapply plus_star; et. } - assert(SSTGT1: XSIM.(ss_tgt) st_tgt1). - { eapply (xsim_progress_tgt); eauto. } - esplits; eauto. + 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. - { des; eapply (progress_star XSIM.(xsim_progress_src)); eauto. } + { ii. eapply SSSRC; eauto. des. eapply star_trans; eauto. } } - (* 2. Before *) @@ -986,7 +960,7 @@ Proof. + (* 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. - { eapply (xsim_progress_tgt); eauto. } + { 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). @@ -1009,8 +983,8 @@ Proof. (* 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. - { eapply (progress_star XSIM.(xsim_progress_src)); eauto. eapply star_right; et. eapply star_refl. } - { eapply (xsim_progress_tgt); eauto. } + { 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 *) @@ -1019,7 +993,7 @@ Proof. 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. - { eapply (xsim_progress_tgt); eauto. } + { ii. eapply SSTGT; eauto. eapply star_left; eauto. } eapply x2b_match_after'; eauto. } Qed. @@ -1051,21 +1025,14 @@ Proof. + exploit INITSIM; eauto. i; des. inv INITTGT0. assert(st_init_tgt = st_init_tgt0). { eapply DTM; eauto. } - destruct (classic (safe L1 st_init_src_)); cycle 1. - { esplits; eauto. rr. pfold. econs. ii; ss. } clarify. esplits; eauto. eapply x2b_match_states_bsim; eauto. - { eapply xsim_initial_sound_src; eauto. } - { eapply xsim_initial_sound_tgt; eauto. } + { ii. eapply prsv_star; try apply props; et. } + { ii. eapply prsv_star; try apply props; et. } econs; eauto. - + exploit INITSIM; eauto. i; des. - destruct (classic (safe L1 st_init_src)); cycle 1. - { esplits; eauto. rr. pfold. econs. ii; ss. } - esplits; eauto. eapply x2b_match_states_bsim; eauto. - { eapply xsim_initial_sound_src; eauto. } - { eapply xsim_initial_sound_tgt; eauto. } + + exploit INITSIM; eauto. i; des. esplits; eauto. eapply x2b_match_states_bsim; eauto. + { ii. eapply prsv_star; try apply props; et. } + { ii. eapply prsv_star; try apply props; et. } econs; eauto. -Unshelve. - all: by (repeat econs; eauto). Qed. Lemma mixed_to_compcert_backward_simulation @@ -1081,7 +1048,10 @@ Lemma backward_to_mixed_simulation (BSIM: backward_simulation L1 L2): <>. Proof. - inv BSIM. inv props. econs; eauto. econs; try apply progress_top; eauto. econs 2; eauto. + inv BSIM. inv props. econs; eauto. econs; eauto. + { eapply preservation_top. } + { eapply preservation_top. } + econs 2; eauto. i. exploit bsim_match_initial_states0; eauto. i; des. esplits; eauto. eapply bsim_to_xsim; eauto. Qed. @@ -1164,8 +1134,8 @@ Section MIXED_SIM. Variable order: index -> index -> Prop. Variable ss_src: L1.(state) -> Prop. Variable ss_tgt: L2.(state) -> Prop. - Hypothesis (PRSVSRC: forall st0 tr st1 (SS: ss_src st0) (STEP: Step L1 st0 tr st1), (<>)). - Hypothesis (PRSVTGT: forall st0 tr st1 (SS: ss_tgt st0) (STEP: Step L2 st0 tr st1), (<>)). + Hypothesis (PRSVSRC: preservation ss_src). + Hypothesis (PRSVTGT: preservation ss_tgt). Inductive sfsim_step xsim (i0: index) (st_src0: L1.(state)) (st_tgt0: L2.(state)): Prop := | sfsim_step_step @@ -1216,8 +1186,8 @@ Section MIXED_SIM. <>). Definition _xsim xsim (i0: index) (st_src0: state L1) (st_tgt0: state L2): Prop := forall - (SSSRC: ss_src st_src0) - (SSTGT: ss_tgt st_tgt0) + (SSSRC: forall tr st_src1 (STAR: Star L1 st_src0 tr st_src1), <>) + (SSTGT: forall tr st_tgt1 (STAR: Star L2 st_tgt0 tr st_tgt1), <>) , (<>) @@ -1285,14 +1255,12 @@ Inductive xsim_init_sim (L1 L2: semantics) (index: Type) (order: index -> index Record xsim_properties (L1 L2: semantics) (index: Type) (order: index -> index -> Prop): Prop := { - ss_src: L1.(state) -> Prop; - ss_tgt: L2.(state) -> Prop; - xsim_initial_sound_src: forall st (INIT: initial_state L1 st) (SAFE: safe L1 st), <>; - xsim_initial_sound_tgt: forall st (INIT: initial_state L2 st), <>; - xsim_progress_src: forall st0 tr st1 (SS: ss_src st0) (STEP: Step L1 st0 tr st1), (<>); - xsim_progress_tgt: forall st0 tr st1 (SS: ss_tgt st0) (STEP: Step L2 st0 tr st1), (<>); + 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: <>; - xsim_initial_states_sim: <>; + xsim_initial_states_sim: <>; xsim_public_preserved: forall (SAFESRC: exists st_init_src, L1.(initial_state) st_init_src), forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id; }.