Module AdequacySound
Let WFSKLINKTGT: Sk.wf sk_link_tgt. eapply link_list_preserves_wf_sk; et. Qed.
Inductive sound_ge (su0: Sound.t) (m0: mem): Prop :=
| sound_ge_intro
(GE: Forall (fun ms => su0.(Sound.skenv) m0 ms.(ModSem.skenv)) sem_src.(Smallstep.globalenv).(fst)).
Lemma lepriv_preserves_sound_ge
m0 su0 su1
(GE: sound_ge su0 m0)
(LE: Sound.lepriv su0 su1):
<<GE: sound_ge su1 m0>>.
Proof.
Lemma hle_preserves_sound_ge
m0 su0 su1
(WF: Sound.wf su0)
(GE: sound_ge su0 m0)
(LE: Sound.hle su0 su1):
<<GE: sound_ge su1 m0>>.
Proof.
Lemma mle_preserves_sound_ge
m0 m1 su0
(GE: sound_ge su0 m0)
(LE: Sound.mle su0 m0 m1):
<<GE: sound_ge su0 m1>>.
Proof.
Inductive sound_stack (args: Args.t): list Frame.t -> Prop :=
| sound_stack_nil
(EXSU: exists su_ex, Sound.args su_ex args /\ sound_ge su_ex args.(Args.get_m)):
sound_stack args []
| sound_stack_cons
args_tail tail ms lst0
(TL: sound_stack args_tail tail)
(FORALLSU: forall su0
(SUARGS: Sound.args su0 args_tail)
(SUGE: sound_ge su0 args_tail.(Args.get_m)),
(<<HD: forall
sound_state_all
(PRSV: local_preservation_noguarantee ms sound_state_all),
<<SUST: sound_state_all su0 args_tail.(Args.get_m) lst0>>>>)
/\
(<<K: forall
sound_state_all
(PRSV: local_preservation_noguarantee ms sound_state_all),
exists su_gr,
(<<ARGS: Sound.args su_gr args>>) /\
(<<LE: Sound.lepriv su0 su_gr>>) /\
(<<K: forall retv lst1 su_ret
(LE: Sound.hle su_gr su_ret)
(SURETV: Sound.retv su_ret retv)
(MLE: Sound.mle su_gr args.(Args.get_m) retv.(Retv.get_m))
(AFTER: ms.(ModSem.after_external) lst0 retv lst1),
sound_state_all su0 args_tail.(Args.get_m) lst1>>)
>>)
/\
(<<MLE: Sound.mle su0 args_tail.(Args.get_m) args.(Args.get_m)>>)
)
(EXSU: exists su_ex, Sound.args su_ex args_tail /\ sound_ge su_ex args_tail.(Args.get_m))
(EX: exists sound_state_ex, local_preservation ms sound_state_ex):
sound_stack args ((Frame.mk ms lst0) :: tail).
Inductive sound_state: mem -> state -> Prop :=
| sound_state_normal
args_tail tail ms lst0 m_arg
(TL: sound_stack args_tail tail)
(EXSU: exists su_ex, Sound.args su_ex args_tail /\ sound_ge su_ex m_arg)
(FORALLSU: forall su0
(SUARGS: Sound.args su0 args_tail)
(SUGE: sound_ge su0 args_tail.(Args.get_m)),
(<<HD: forall
sound_state_all
(PRSV: local_preservation_noguarantee ms sound_state_all),
<<SUST: sound_state_all su0 m_arg lst0>>>>))
(EX: exists sound_state_ex, local_preservation ms sound_state_ex)
(ABCD: args_tail.(Args.get_m) = m_arg)
:
sound_state m_arg (State ((Frame.mk ms lst0) :: tail))
| sound_state_call
m_tail frs args
(STK: sound_stack args frs)
(EQ: args.(Args.get_m) = m_tail)
(EXSU: exists su_ex, Sound.args su_ex args /\ sound_ge su_ex m_tail):
sound_state m_tail (Callstate args frs).
Lemma sound_init
st0
(INIT: sem_src.(Smallstep.initial_state) st0):
exists m_init0, <<MEM: Sk.load_mem sk_link_src = Some m_init0>> /\ <<SU: sound_state m_init0 st0>>.
Proof.
Lemma sound_progress
st0 m_arg0 tr st1
(SUST: sound_state m_arg0 st0)
(STEP: Step sem_src st0 tr st1):
<<SUST: exists m_arg1, sound_state m_arg1 st1>>.
Proof.
inv STEP.
-
inv SUST.
ss.
des.
exploit FORALLSU;
eauto. {
eapply local_preservation_noguarantee_weak;
eauto. }
intro T;
des.
inv EX.
exploit CALL;
eauto.
i;
des.
esplits;
eauto.
econs;
eauto;
cycle 1.
+
esplits;
eauto.
eapply lepriv_preserves_sound_ge;
eauto.
{
eapply mle_preserves_sound_ge;
eauto. }
+
econs;
eauto;
cycle 1.
{
esplits;
eauto.
econs;
eauto. }
ii.
esplits;
eauto.
*
ii.
exploit FORALLSU;
try apply SUARGS;
eauto.
*
ii.
exploit FORALLSU;
try apply SUARGS;
eauto.
intro U;
des.
inv PRSV.
exploit CALL0;
eauto.
i;
des.
esplits;
eauto.
ii.
eapply K0;
eauto.
*
exploit FORALLSU;
eauto.
{
eapply local_preservation_noguarantee_weak;
eauto.
econs;
eauto. }
i;
des.
exploit CALL;
eauto.
i;
des.
ss.
-
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.
+
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.
assert(
exists mp,
In mp pp /\
mp.(
ModPair.src) =
md_src).
{
clear -
MODSEM0.
rr in pp.
rr in p_src.
subst p_src.
rewrite in_map_iff in *.
des.
eauto. }
des.
exploit SIMPROG;
eauto.
intros MPSIM.
inv MPSIM.
destruct SIMSKENV.
exploit SIMMS.
{
eapply INCLSRC;
et. }
{
eapply INCLTGT;
et. }
{
eapply SkEnv.load_skenv_wf;
et. }
{
eapply SkEnv.load_skenv_wf;
et. }
{
eapply SSLE;
eauto. }
{
eauto. }
intro SIM;
des.
inv SIM.
ss.
esplits;
eauto.
-
inv SUST.
ss.
esplits;
eauto.
econs;
eauto.
i.
des.
exploit FORALLSU;
eauto. {
eapply local_preservation_noguarantee_weak;
eauto. }
intro U;
des.
esplits;
eauto.
i.
ss.
inv PRSV.
eapply STEP;
eauto.
+
eapply FORALLSU;
eauto.
econs;
eauto.
+
split;
ii;
ModSem.tac.
-
inv SUST.
ss.
rename ms into ms_top.
rename args_tail into args_tail_top.
inv TL.
ss.
unfold Frame.update_st.
s.
des.
esplits;
eauto.
econs;
eauto.
ii.
esplits;
eauto.
+
ii.
exploit FORALLSU0;
eauto.
i;
des.
exploit K;
eauto.
i;
des.
inv EX.
exploit RET;
eauto.
{
eapply FORALLSU;
eauto.
{
eapply lepriv_preserves_sound_ge. {
eapply mle_preserves_sound_ge;
eauto. }
eauto. }
{
eapply local_preservation_noguarantee_weak;
eauto.
econs;
et. } }
i;
des.
eapply K0;
eauto.
Unshelve.
all:
ss.
Qed.
Lemma sound_progress_star
st0 m_arg0 tr st1
(SUST: sound_state m_arg0 st0)
(STEP: Star sem_src st0 tr st1):
<<SUST: exists m_arg1, sound_state m_arg1 st1>>.
Proof.
generalize dependent m_arg0.
induction STEP.
-
esplits;
eauto.
-
clarify.
i.
exploit sound_progress;
eauto.
i;
des.
eapply IHSTEP;
eauto.
Qed.
Lemma sound_progress_plus
st0 m_arg0 tr st1
(SUST: sound_state m_arg0 st0)
(STEP: Plus sem_src st0 tr st1):
<<SUST: exists m_arg1, sound_state m_arg1 st1>>.
Proof.
End ADQSOUND.