Refactored & compiles

snu-sf · Mar 18, 2020 · 6f329db · 6f329db
1 parent 2563b4c
commit 6f329db
Show file tree

Hide file tree

Showing 8 changed files with 228 additions and 187 deletions.
diff --git 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
@@ -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; 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
@@ -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),
+      <<SAFE: safe (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
@@ -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
@@ -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
@@ -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)