diff --git a/proof/AdequacySound.v b/proof/AdequacySound.v index 526b9f0c..6c57548c 100644 --- a/proof/AdequacySound.v +++ b/proof/AdequacySound.v @@ -55,7 +55,9 @@ 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 @@ -63,7 +65,7 @@ Section ADQSOUND. (LE: Sound.lepriv su0 su1): <>. 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): <>. 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 index ed2fb75c..8d97cab7 100644 --- 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) -> <>) (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. <>) (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, (<>) /\ @@ -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 index d4565dfa..9bcba321 100644 --- a/proof/Sound.v +++ b/proof/Sound.v @@ -113,8 +113,9 @@ Module Sound. (INCL: SkEnv.includes skenv_link sk), <>; - 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), + <>; system_axiom: forall ef skenv0 su0 args0 diff --git a/proof/SoundProduct.v b/proof/SoundProduct.v index 76295fed..61c75628 100644 --- 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 index 22c23315..11283959 100644 --- 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: <> /\ <> /\ <> /\ <>).