Merge pull request #10 from alxest/sim-preservation

Sim preservation
snu-sf · Mar 18, 2020 · 5ff6d1d · 5ff6d1d
2 parents da173b6 + 11d0ef1
commit 5ff6d1d
Show file tree

Hide file tree

Showing 9 changed files with 341 additions and 174 deletions.
diff --git a/bound/LowerBound.v b/bound/LowerBound.v
@@ -2299,7 +2299,7 @@ Section PRESERVATION.
 
   Lemma match_state_xsim:
       forall st_src st_tgt n (MTCHST: match_states st_src st_tgt n),
-        xsim (sem prog) (semantics tprog) lt n st_src st_tgt.
+        xsim (sem prog) (semantics tprog) lt top1 top1 n st_src st_tgt.
   Proof.
     pcofix CIH. i. pfold. destruct st_src.
     - exploit init_case; ss.
@@ -2364,7 +2364,7 @@ Section PRESERVATION.
   Lemma transf_xsim_properties:
         xsim_properties (sem prog) (semantics tprog) nat lt.
   Proof.
-    econs; [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
@@ -732,7 +732,7 @@ Section PRESERVATION.
         (STEP: Csem.step skenv_link ge_cp_link st0 tr st1) :
       <<WT: wt_state cp_link ge_cp_link st1>>.
   Proof.
-    eapply preservation; try apply STEP; try refl; et; destruct cp_link_precise.
+    eapply Ctyping.preservation; try apply STEP; try refl; et; destruct cp_link_precise.
     - ii. red. unfold ge_cp_link in *. ss.
       exploit GE2P; eauto. i. des.
       eapply Genv.find_invert_symbol in SYMB. eapply Genv.find_invert_symbol in SYMB0.
@@ -750,7 +750,7 @@ Section PRESERVATION.
   Proof.
     exploit is_focus_precise; eauto. i. inv H.
     r in FOC.
-    eapply preservation; try apply STEP; try refl; et.
+    eapply Ctyping.preservation; try apply STEP; try refl; et.
     - ii. ss. exploit GE2P; eauto. i. des.
       eapply Genv.find_invert_symbol in SYMB. eapply Genv.find_invert_symbol in SYMB0.
       unfold Genv.invert_symbol in *. ss. rewrite SYMB in *. clarify.
@@ -802,7 +802,7 @@ Section PRESERVATION.
   Lemma match_xsim
         st_src0 st_tgt0
         (MATCH: match_states st_src0 st_tgt0) :
-      <<XSIM: xsim (sem prog_src) (sem prog_tgt) (fun _ _ => False) tt st_src0 st_tgt0>>
+      <<XSIM: xsim (sem prog_src) (sem prog_tgt) (fun _ _ => False) top1 top1 tt st_src0 st_tgt0>>
   .
   Proof.
     revert_until sum_cont. revert INCL_FOCUS INCL.
@@ -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 :
       <<XSIM: mixed_simulation (Sem.sem prog_src) (Sem.sem prog_tgt)>>.
   Proof.
-    econs; ss; eauto. econs; 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; 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
@@ -953,7 +953,7 @@ Section PRESERVATION.
         (STEP: Csem.step skenv_link ge st0 tr st1):
       <<WT: wt_state prog ge st1>>.
   Proof.
-    eapply preservation; try apply STEP; try refl; eauto; et; destruct prog_precise.
+    eapply Ctyping.preservation; try apply STEP; try refl; eauto; et; destruct prog_precise.
     - ii. eapply Genv.find_def_symbol. esplits; eauto.
     - i. rewrite Genv.find_def_symbol in MAP. des; eauto.
     - i.
@@ -970,8 +970,8 @@ Section PRESERVATION.
   Qed.
 
   Lemma match_state_xsim:
-      forall st_src st_tgt n (MTCHST: match_states st_src st_tgt n) (WTST: wt_state prog ge st_src),
-        xsim (Csem.semantics prog) (Sem.sem tprog) lt n%nat st_src st_tgt.
+      forall st_src st_tgt n (MTCHST: match_states st_src st_tgt n),
+        xsim (Csem.semantics prog) (Sem.sem tprog) lt (wt_state prog ge) top1 n%nat st_src st_tgt.
   Proof.
     pcofix CIH. i. pfold.
     destruct match_ge_skenv_link.
@@ -1092,7 +1092,6 @@ Section PRESERVATION.
                 ** traceEq.
              ++ right. eapply CIH.
                 { econs. ss. }
-                { ss. eapply preservation_prog; eauto. rewrite <- senv_same. et. }
       (* initial state *)
       + inversion INITSRC; subst; ss.
         left. right. econs; i. econs; i; cycle 1.
@@ -1212,7 +1211,6 @@ Section PRESERVATION.
                    --- right. eapply CIH.
                        { ss. instantiate (1:= 1%nat). inv INITTGT.
                          eapply match_states_intro. ss. }
-                       { ss. eapply preservation_prog; eauto. rewrite <- senv_same; et. }
              (* main is syscall *)
              ++ inv SYSMOD. inv INITTGT. ss.
                 assert (SAME: sk_tgt = sk_link) by (Eq; auto). clear INITSK.
@@ -1241,15 +1239,13 @@ Section PRESERVATION.
                 splits; auto. eapply star_refl.
              ++ right. eapply CIH.
                 { econs; eauto. }
-                { ss. }
           (* step_internal *)
           -- assert(STEPSRC: Csem.step skenv_link (globalenv prog) st_src tr st0).
              { exploit cstep_same; eauto. }
              esplits.
              ++ left. eapply plus_one. unfold fundef in *. rewrite senv_same. eauto.
              ++ right. eapply CIH.
                 { econs; eauto. }
-                { ss. eapply preservation_prog; eauto. }
         (* progress *)
         * specialize (SAFESRC _ (star_refl _ _ _ _)). des.
           (* final *)
@@ -1285,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 WTST; 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.
@@ -1296,43 +1292,45 @@ Section PRESERVATION.
           { inv INITTGT. }
   Qed.
 
+  Hypothesis INITSAFE: forall st (INIT: Smallstep.initial_state (semantics prog) st),
+      <<SAFE: safe (semantics prog) st>>.
+
   Lemma transf_xsim_properties:
       xsim_properties (Csem.semantics prog) (Sem.sem tprog) nat lt.
   Proof.
-    econs; [apply lt_wf| |i; apply symb_preserved].
+    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.
+    }
     econs. i.
     exploit (transf_initial_states); eauto.
     i. des. esplits. econs; eauto.
     - i. inv INIT0. inv INIT1. clarify.
-    - ss. inv INITSRC.
-      destruct (classic (exists fd, Genv.find_funct (globalenv prog) (Vptr b Ptrofs.zero) = Some (Internal fd))).
-      + apply match_state_xsim; eauto.
-        eapply wt_initial_state; 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 H7. Eq. }
-           ss. unfold Genv.find_def in DEF. unfold fundef, genv_genv in *. ss.
-          symmetry in H6. Eq.
-          symmetry in H7. exploit DEFSYMB; eauto. i. des.
-          unfold Genv.find_symbol in *. rewrite mge_symb in H6. eauto. }
-        { des_ifs. }
-      + assert(NOSTEP: Nostep (semantics prog) (Csem.Callstate (Vptr b Ptrofs.zero)
-                                                               (Tfunction Tnil type_int32s cc_default) [] Kstop m0)).
-        { ii. rr in H6. des; inv H6; ss; des_ifs.
-           - contradict H5; eauto.
-           - exploit MAIN_INTERNAL; eauto.
-             { econs; eauto. }
-             i; des. ss. des_ifs. }
-        assert(UB: ~safe (semantics prog) (Csem.Callstate (Vptr b Ptrofs.zero)
-                                                          (Tfunction Tnil type_int32s cc_default) [] Kstop m0)).
-        { ii; ss. specialize (H6 _ (star_refl _ _ _ _)). des; ss.
-          - inv H6; ss.
-          - rr in NOSTEP. contradict NOSTEP; eauto. }
-        pfold. right. econs; ii; ss.
+    - apply match_state_xsim; eauto.
   Qed.
 
   Lemma transf_program_correct:
@@ -1382,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
@@ -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)):
+    <<INITUB: 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)):
+    <<INITUB: program_behaves sem0 (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, <<INIT: Smallstep.initial_state L1 st>>)
+          (INITSAFE: forall st (INIT: Smallstep.initial_state L1 st),
+              <<SAFE: safe L1 st>>)
+        ,
+          improves L1 L2)
+  :
+    <<IMPRV: improves L1 L2>>
+.
+Proof.
+  destruct (classic (exists st, <<INIT: Smallstep.initial_state L1 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), <<SAFE: safe 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
@@ -603,7 +603,7 @@ Section LXSIM.
   Lemma match_states_xsim
         i st_src0 st_tgt0
         (MATCH: match_states i st_src0 st_tgt0):
-    xsim (sem (ctx1 ++ [module] ++ ctx2)) (sem (ctx1 ++ [MutrecAspec.module; MutrecBspec.module] ++ ctx2)) (Zwf.Zwf 0) i st_src0 st_tgt0.
+    xsim (sem (ctx1 ++ [module] ++ ctx2)) (sem (ctx1 ++ [MutrecAspec.module; MutrecBspec.module] ++ ctx2)) (Zwf.Zwf 0) top1 top1 i st_src0 st_tgt0.
   Proof.
     revert_until SKEWF. pcofix CIH. i.
     inv MATCH.
@@ -1064,7 +1064,7 @@ Proof.
   eapply bsim_improves.
   eapply mixed_to_backward_simulation.
   econs; eauto.
-  econs; 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
@@ -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)):
-    <<INITUB: 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)):
-    <<INITUB: program_behaves sem0 (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)