Merge pull request #11 from alxest/refactor-sound

Weaken Sound.v
snu-sf · Mar 20, 2020 · 829f24a · 829f24a
2 parents 5ff6d1d + 2f44e8d
commit 829f24a
Show file tree

Hide file tree

Showing 5 changed files with 31 additions and 19 deletions.
diff --git a/proof/AdequacySound.v b/proof/AdequacySound.v
@@ -55,15 +55,17 @@ Section ADQSOUND.
 
   Inductive sound_ge (su0: Sound.t) (m0: mem): Prop :=
   | sound_ge_intro
-      (GE: Forall (fun ms => su0.(Sound.skenv) m0 ms.(ModSem.skenv)) (fst sem_src.(Smallstep.globalenv))).
+      (GE: Forall (fun ms => su0.(Sound.skenv) m0 ms.(ModSem.skenv) /\ su0.(Sound.skenv) m0 ms.(ModSem.skenv_link))
+                  (fst sem_src.(Smallstep.globalenv)))
+  .
 
   Lemma lepriv_preserves_sound_ge
         m0 su0 su1
         (GE: sound_ge su0 m0)
         (LE: Sound.lepriv su0 su1):
       <<GE: sound_ge su1 m0>>.
   Proof.
-    inv GE. econs; eauto. rewrite Forall_forall in *. ii. eapply Sound.skenv_lepriv; eauto.
+    inv GE. econs; eauto. rewrite Forall_forall in *. ii. split; eapply Sound.skenv_lepriv; try apply GE0; eauto.
   Qed.
 
   Lemma hle_preserves_sound_ge
@@ -82,7 +84,7 @@ Section ADQSOUND.
         (LE: Sound.mle su0 m0 m1):
       <<GE: sound_ge su0 m1>>.
   Proof.
-    inv GE. econs; eauto. rewrite Forall_forall in *. ii. eapply Sound.skenv_mle; eauto.
+    inv GE. econs; eauto. rewrite Forall_forall in *. ii. split; eapply Sound.skenv_mle; try apply GE0; eauto.
   Qed.
 
   (* stack can go preservation when su0 is given *)
@@ -161,12 +163,14 @@ Section ADQSOUND.
     assert(GE: sound_ge su_init m_init).
     { econs. rewrite Forall_forall. intros ? IN. ss. des_ifs. u in IN.
       rewrite in_map_iff in IN. des; ss; clarify.
-      + s. rewrite <- Sound.system_skenv; eauto.
+      + s. split; try eapply Sound.system_skenv; eauto.
       + assert(INCL: SkEnv.includes (Sk.load_skenv sk_link_src) (Mod.sk x0)).
         { unfold p_src in IN0. unfold ProgPair.src in *. rewrite in_map_iff in IN0. des. clarify. eapply INCLSRC; et. }
-        eapply Sound.skenv_project; eauto.
-        { eapply link_load_skenv_wf_mem; et. }
-        rewrite <- Mod.get_modsem_skenv_spec; ss. eapply SkEnv.project_impl_spec; et.
+        split; ss.
+        * eapply Sound.skenv_project; eauto.
+          { eapply link_load_skenv_wf_mem; et. }
+          rewrite <- Mod.get_modsem_skenv_spec; ss. eapply SkEnv.project_impl_spec; et.
+        * rewrite Mod.get_modsem_skenv_link_spec. ss.
     }
     econs; eauto. econs; eauto.
     (* - eapply Sound.greatest_adq; eauto. *)
@@ -201,7 +205,8 @@ Section ADQSOUND.
     - (* INIT *)
       inv SUST. ss. des_ifs. esplits; eauto. econs; eauto.
       + ii. esplits; eauto.
-        * ii. inv PRSV. eapply INIT0; eauto. inv SUGE. rewrite Forall_forall in *. eapply GE. inv MSFIND. ss. des_ifs.
+        * ii. inv PRSV. inv SUGE. rewrite Forall_forall in *.
+          exploit GE; eauto. { ss. des_ifs. eapply MSFIND. } intro T; des. eapply INIT0; et.
       + inv MSFIND. ss. rr in SIMPROG. rewrite Forall_forall in *. des; clarify.
         { eapply system_local_preservation. }
         u in MODSEM. rewrite in_map_iff in MODSEM. des; clarify. rename x into md_src.

diff --git a/proof/Preservation.v b/proof/Preservation.v
@@ -29,6 +29,7 @@ Inductive local_preservation (sound_state: Sound.t -> mem -> ms.(state) -> Prop)
 | local_preservation_intro
     (INIT: forall su_init args st_init
         (SUARG: Sound.args su_init args)
+        (SKENVLINK: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv_link))
         (SKENV: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv))
         (INIT: ms.(ModSem.initial_frame) args st_init)
       ,
@@ -65,6 +66,7 @@ Inductive local_preservation_noguarantee (sound_state: Sound.t -> mem -> ms.(sta
 | local_preservation_noguarantee_intro
     (INIT: forall su_init args st_init
         (SUARG: Sound.args su_init args)
+        (SKENVLINK: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv_link))
         (SKENV: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv))
         (INIT: ms.(ModSem.initial_frame) args st_init)
       ,
@@ -103,6 +105,7 @@ Inductive local_preservation_standard (sound_state: Sound.t -> ms.(state) -> Pro
 | local_preservation_standard_intro
     (INIT: forall su_arg args st_init
         (SUARG: Sound.args su_arg args)
+        (SKENVLINK: Sound.skenv su_arg (Args.get_m args) ms.(ModSem.skenv_link))
         (SKENV: Sound.skenv su_arg (Args.get_m args) ms.(ModSem.skenv))
         (INIT: ms.(ModSem.initial_frame) args st_init)
       ,
@@ -169,6 +172,7 @@ Inductive local_preservation_strong (sound_state: Sound.t -> ms.(state) -> Prop)
     (LIFTPRIV: lift <2= Sound.lepriv)
     (INIT: forall su_init args st_init
         (SUARG: Sound.args su_init args)
+        (SKENVLINK: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv_link))
         (SKENV: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv))
         (INIT: ms.(ModSem.initial_frame) args st_init)
       ,
@@ -236,6 +240,7 @@ Inductive local_preservation_strong_horizontal (sound_state: Sound.t -> ms.(stat
     (LIFTPRIV: lift <2= Sound.lepriv)
     (INIT: forall su_arg args st_init
         (SUARG: Sound.args su_arg args)
+        (SKENVLINK: Sound.skenv su_arg (Args.get_m args) ms.(ModSem.skenv_link))
         (SKENV: Sound.skenv su_arg (Args.get_m args) ms.(ModSem.skenv))
         (INIT: ms.(ModSem.initial_frame) args st_init)
       ,
@@ -307,6 +312,7 @@ Inductive local_preservation_strong_excl (sound_state: Sound.t -> ms.(state) ->
         <<MLE: Sound.mle su0 m0 m2>>)
     (INIT: forall su_init args st_init
         (SUARG: Sound.args su_init args)
+        (SKENVLINK: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv_link))
         (SKENV: Sound.skenv su_init (Args.get_m args) ms.(ModSem.skenv))
         (INIT: ms.(ModSem.initial_frame) args st_init)
       ,
@@ -365,6 +371,7 @@ Inductive local_preservation_strong_horizontal_excl (sound_state: Sound.t -> ms.
         <<MLE: Sound.mle su0 m0 m2>>)
     (INIT: forall su_arg args st_init
         (SUARG: Sound.args su_arg args)
+        (SKENVLINK: Sound.skenv su_arg (Args.get_m args) ms.(ModSem.skenv_link))
         (SKENV: Sound.skenv su_arg (Args.get_m args) ms.(ModSem.skenv))
         (INIT: ms.(ModSem.initial_frame) args st_init),
         exists su_init, (<<LE: Sound.hle su_arg su_init>>) /\
@@ -432,10 +439,10 @@ Definition system_sound_state `{SU: Sound.class} (ms: ModSem.t): Sound.t -> mem
   fun su m_arg st =>
     match st with
     | System.Callstate fptr vs m => su.(Sound.args) (Args.Cstyle fptr vs m) /\ su.(Sound.mle) m_arg m
-                               /\ su.(Sound.skenv) m_arg ms.(ModSem.skenv)
+                               /\ su.(Sound.skenv) m_arg ms.(ModSem.skenv_link)
     | System.Returnstate v m =>
       exists su_ret, Sound.hle su su_ret /\ su_ret.(Sound.retv) (Retv.Cstyle v m) /\ su.(Sound.mle) m_arg m
-        /\ su.(Sound.skenv) m ms.(ModSem.skenv)
+        /\ su.(Sound.skenv) m ms.(ModSem.skenv_link)
     end.
 
 Lemma system_local_preservation
@@ -449,7 +456,7 @@ Proof.
   - inv STEP. ss. inv SUST. des. exploit Sound.system_axiom; try apply EXTCALL; eauto.
     { instantiate (1:= Args.Cstyle _ _ _). ss. }
     { rr. esplits; eauto. }
-    { eapply Sound.system_skenv; eauto. eapply Sound.skenv_mle; eauto. }
+    { eapply Sound.skenv_mle; eauto. }
     { eauto. }
     i; des. r in RETV. ss. des. ss. esplits; eauto.
     + etrans; eauto.

diff --git a/proof/Sound.v b/proof/Sound.v
@@ -113,8 +113,9 @@ Module Sound.
         (INCL: SkEnv.includes skenv_link sk),
         <<SKE: su.(skenv) m0 skenv0>>;
 
-    system_skenv: forall su m0 skenv_link,
-        su.(skenv) m0 skenv_link <-> su.(skenv) m0 (System.skenv skenv_link);
+    system_skenv: forall su m0 skenv_link
+        (SKELINK: su.(skenv) m0 skenv_link),
+        <<SKE: su.(skenv) m0 (System.skenv skenv_link)>>;
 
     system_axiom: forall
         ef skenv0 su0 args0

diff --git a/proof/SoundProduct.v b/proof/SoundProduct.v
@@ -81,9 +81,7 @@ Section SOUNDPRODUCT.
     ss. esplits; eauto; eapply Sound.skenv_project; eauto.
   Qed.
   Next Obligation.
-    ss. rr. esplits; ii; des.
-    - erewrite <- ! (Sound.system_skenv) in *; eauto.
-    - erewrite <- (Sound.system_skenv) in H; eauto. erewrite <- (Sound.system_skenv) in H0; eauto.
+    ss. esplits; eauto; eapply Sound.system_skenv; eauto.
   Qed.
   Next Obligation.
     ss. des.
@@ -148,9 +146,11 @@ Section SOUNDPRODUCT.
       + eapply INIT; eauto.
         { destruct su_init; ss. eapply sound_args_iff in SUARG; eauto. ss; des; ss. }
         { destruct su_init; ss. eapply sound_skenv_iff in SKENV; eauto. ss; des; ss. }
+        { destruct su_init; ss. eapply sound_skenv_iff in SKENV; eauto. ss; des; ss. }
       + eapply INIT0; eauto.
         { destruct su_init; ss. eapply sound_args_iff in SUARG; eauto. des. ss. }
         { destruct su_init; ss. eapply sound_skenv_iff in SKENV; eauto. ss; des; ss. }
+        { destruct su_init; ss. eapply sound_skenv_iff in SKENV; eauto. ss; des; ss. }
     - clear - STEP STEP0. ii. ss. des.
       specialize (STEP m_arg (fst su0)). specialize (STEP0 m_arg (snd su0)).
       split; ss.

diff --git a/proof/UnreachC.v b/proof/UnreachC.v
@@ -720,9 +720,8 @@ Next Obligation.
     - unfold Genv.find_var_info in *. des_ifs_safe. erewrite Genv_map_defs_def_inv; et. ss.
     - unfold Genv.find_var_info in *. des_ifs_safe. exploit Genv_map_defs_def; et. i; des. des_ifs.
   }
-  split; i; inv H; ss.
-  - econs; eauto. rpapply ROMATCH; ss.
-  - econs; eauto. rpapply ROMATCH; ss.
+  inv SKELINK.
+  econs; eauto. rpapply ROMATCH; ss.
 Qed.
 Next Obligation.
   assert(T: <<VAL: val' su0 (Args.fptr args0)>> /\ <<VALS: Forall (val' su0) (Args.vs args0)>> /\ <<MEM: mem' su0 (Args.m args0)>> /\ <<WF: wf su0 >>).