Require Import CoqlibC.
Require Import Simulation.
Require Import LinkingC.
Require Import Skeleton.
Require Import Values.
Require Import JMeq.
Require Import SmallstepC.
Require Import Integers.
Require Import Events.
Require Import Skeleton ModSem Mod Sem.
Require Import SimSymb SimMem SimMod SimModSem SimProg SimProg.
Require Import ModSemProps SemProps Ord.
Require Import Sound Preservation AdequacySound.
Require Import Program.
Set Implicit Arguments.
Section SIMGE.
Context `{
SM:
SimMem.class}.
Context `{
SU:
Sound.class}.
Context {
SS:
SimSymb.class SM}.
Inductive sim_ge (
sm0:
SimMem.t):
Ge.t ->
Ge.t ->
Prop :=
|
sim_ge_src_stuck
ge_tgt skenv_link_src skenv_link_tgt:
sim_ge sm0 ([],
skenv_link_src) (
ge_tgt,
skenv_link_tgt)
|
sim_ge_intro
msps ge_src ge_tgt skenv_link_src skenv_link_tgt
(
SIMSKENV:
List.Forall (
fun msp =>
ModSemPair.sim_skenv msp sm0)
msps)
(
SIMMSS:
List.Forall (
ModSemPair.sim)
msps)
(
GESRC:
ge_src = (
map (
ModSemPair.src)
msps))
(
GETGT:
ge_tgt = (
map (
ModSemPair.tgt)
msps))
(
SIMSKENVLINK:
exists ss_link,
SimSymb.sim_skenv sm0 ss_link skenv_link_src skenv_link_tgt)
(
MFUTURE:
List.Forall (
fun msp =>
SimMem.future msp.(
ModSemPair.sm)
sm0)
msps)
(
SESRC:
List.Forall (
fun ms =>
ms.(
ModSem.to_semantics).(
symbolenv) =
skenv_link_src)
ge_src)
(
SETGT:
List.Forall (
fun ms =>
ms.(
ModSem.to_semantics).(
symbolenv) =
skenv_link_tgt)
ge_tgt):
sim_ge sm0 (
ge_src,
skenv_link_src) (
ge_tgt,
skenv_link_tgt).
Lemma find_fptr_owner_fsim
sm0 ge_src ge_tgt fptr_src fptr_tgt ms_src
(
SIMGE:
sim_ge sm0 ge_src ge_tgt)
(
SIMFPTR:
SimMem.sim_val sm0 fptr_src fptr_tgt)
(
FINDSRC:
Ge.find_fptr_owner ge_src fptr_src ms_src):
exists msp,
<<
SRC:
msp.(
ModSemPair.src) =
ms_src>>
/\ <<
FINDTGT:
Ge.find_fptr_owner ge_tgt fptr_tgt msp.(
ModSemPair.tgt)>>
/\ <<
SIMMS:
ModSemPair.sim msp>>
/\ <<
SIMSKENV:
ModSemPair.sim_skenv msp sm0>>
/\ <<
MFUTURE:
SimMem.future msp.(
ModSemPair.sm)
sm0>>.
Proof.
inv SIMGE.
{
inv FINDSRC;
ss. }
rewrite Forall_forall in *.
inv FINDSRC.
ss.
rewrite in_map_iff in MODSEM.
des.
rename x into msp.
esplits;
eauto.
clarify.
specialize (
SIMMSS msp).
exploit SIMMSS;
eauto.
clear SIMMSS.
intro SIMMS.
specialize (
SIMSKENV msp).
exploit SIMSKENV;
eauto.
clear SIMSKENV.
intro SIMSKENV.
exploit SimSymb.sim_skenv_func_bisim;
try apply SIMSKENV.
intro SIMFUNC;
des.
inv SIMFUNC.
exploit FUNCFSIM;
eauto.
i;
des.
clear_tac.
inv SIM.
econs;
eauto.
apply in_map_iff.
esplits;
eauto.
Qed.
Theorem mfuture_preserves_sim_ge
sm0 ge_src ge_tgt sm1
(
SIMGE:
sim_ge sm0 ge_src ge_tgt)
(
MFUTURE:
SimMem.future sm0 sm1):
<<
SIMGE:
sim_ge sm1 ge_src ge_tgt>>.
Proof.
Lemma sim_ge_cons
sm_init tl_src tl_tgt msp skenv_link_src skenv_link_tgt
(
SAFESRC:
tl_src <> [])
(
SIMMSP:
ModSemPair.sim msp)
(
SIMGETL:
sim_ge sm_init (
tl_src,
skenv_link_src) (
tl_tgt,
skenv_link_tgt))
(
SIMSKENV:
ModSemPair.sim_skenv msp sm_init)
(
MFUTURE:
SimMem.future (
ModSemPair.sm msp)
sm_init)
(
SESRC: (
symbolenv (
ModSemPair.src msp)) =
skenv_link_src)
(
SETGT: (
symbolenv (
ModSemPair.tgt msp)) =
skenv_link_tgt):
<<
SIMGE:
sim_ge sm_init (
msp.(
ModSemPair.src) ::
tl_src,
skenv_link_src)
(
msp.(
ModSemPair.tgt) ::
tl_tgt,
skenv_link_tgt)>>.
Proof.
red. inv SIMGETL; ss. econstructor 2 with (msps := msp :: msps); eauto. Qed.
Lemma to_msp_tgt:
forall skenv_tgt skenv_src pp sm_init,
map ModSemPair.tgt (
map (
ModPair.to_msp skenv_src skenv_tgt sm_init)
pp) =
map (
fun md =>
Mod.modsem md skenv_tgt) (
ProgPair.tgt pp).
Proof.
i. ginduction pp; ii; ss. f_equal. erewrite IHpp; eauto. Qed.
Lemma to_msp_src:
forall skenv_tgt skenv_src pp sm_init,
map ModSemPair.src (
map (
ModPair.to_msp skenv_src skenv_tgt sm_init)
pp) =
map (
fun md =>
Mod.modsem md skenv_src) (
ProgPair.src pp).
Proof.
i. ginduction pp; ii; ss. f_equal. erewrite IHpp; eauto. Qed.
Lemma to_msp_sim_skenv
sm_init mp skenv_src skenv_tgt ss_link
(
WFSRC:
SkEnv.wf skenv_src)
(
WFTGT:
SkEnv.wf skenv_tgt)
(
INCLSRC:
SkEnv.includes skenv_src mp.(
ModPair.src).(
Mod.sk))
(
INCLTGT:
SkEnv.includes skenv_tgt mp.(
ModPair.tgt).(
Mod.sk))
(
SIMMP:
ModPair.sim mp)
(
LESS:
SimSymb.le (
ModPair.ss mp) (
Mod.get_sk (
ModPair.src mp) (
Mod.data (
ModPair.src mp)))
(
Mod.get_sk (
ModPair.tgt mp) (
Mod.data (
ModPair.tgt mp)))
ss_link)
(
SIMSKENV:
SimSymb.sim_skenv sm_init ss_link skenv_src skenv_tgt):
<<
SIMSKENV:
ModSemPair.sim_skenv (
ModPair.to_msp skenv_src skenv_tgt sm_init mp)
sm_init>>.
Proof.
Theorem init_sim_ge_strong
pp p_src p_tgt sk_link_src sk_link_tgt ss_link skenv_link_src skenv_link_tgt m_src
(
NOTNIL:
pp <> [])
(
SIMPROG:
ProgPair.sim pp)
(
PSRC:
p_src =
pp.(
ProgPair.src))
(
PTGT:
p_tgt =
pp.(
ProgPair.tgt))
(
SSLE:
Forall (
fun mp =>
SimSymb.le (
ModPair.ss mp) (
ModPair.src mp) (
ModPair.tgt mp)
ss_link)
pp)
(
SIMSK:
SimSymb.sim_sk ss_link sk_link_src sk_link_tgt)
(
SKSRC:
link_sk p_src =
Some sk_link_src)
(
SKTGT:
link_sk p_tgt =
Some sk_link_tgt)
(
SKENVSRC:
Sk.load_skenv sk_link_src =
skenv_link_src)
(
SKENVTGT:
Sk.load_skenv sk_link_tgt =
skenv_link_tgt)
(
WFSKSRC:
forall mp (
IN:
In mp pp),
Sk.wf (
ModPair.src mp))
(
WFSKTGT:
forall mp (
IN:
In mp pp),
Sk.wf (
ModPair.tgt mp))
(
LOADSRC:
Sk.load_mem sk_link_src =
Some m_src):
exists sm_init ss_link, <<
SIMGE:
sim_ge sm_init
(
load_genv p_src (
Sk.load_skenv sk_link_src))
(
load_genv p_tgt (
Sk.load_skenv sk_link_tgt))>>
/\ <<
MWF:
SimMem.wf sm_init>>
/\ <<
LOADTGT:
Sk.load_mem sk_link_tgt =
Some sm_init.(
SimMem.tgt)>>
/\ <<
MSRC:
sm_init.(
SimMem.src) =
m_src>>
/\ (<<
SIMSKENV:
SimSymb.sim_skenv sm_init ss_link skenv_link_src skenv_link_tgt>>)
/\ (<<
INCLSRC:
forall mp (
IN:
In mp pp),
SkEnv.includes skenv_link_src mp.(
ModPair.src).(
Mod.sk)>>)
/\ (<<
INCLTGT:
forall mp (
IN:
In mp pp),
SkEnv.includes skenv_link_tgt mp.(
ModPair.tgt).(
Mod.sk)>>)
/\ (<<
SSLE:
forall mp (
IN:
In mp pp),
SimSymb.le mp.(
ModPair.ss)
mp.(
ModPair.src)
mp.(
ModPair.tgt)
ss_link>>)
/\ (<<
MAINSIM:
SimMem.sim_val sm_init (
Genv.symbol_address skenv_link_src sk_link_src.(
prog_main)
Ptrofs.zero)
(
Genv.symbol_address skenv_link_tgt sk_link_tgt.(
prog_main)
Ptrofs.zero)>>).
Proof.
End SIMGE.
Section ADQMATCH.
Context `{
SM:
SimMem.class}.
Context {
SS:
SimSymb.class SM}.
Context `{
SU:
Sound.class}.
Variable pp:
ProgPair.t.
Let p_src :=
pp.(
ProgPair.src).
Let p_tgt :=
pp.(
ProgPair.tgt).
Variable sk_link_src sk_link_tgt:
Sk.t.
Hypothesis LINKSRC: (
link_sk p_src) =
Some sk_link_src.
Hypothesis LINKTGT: (
link_sk p_tgt) =
Some sk_link_tgt.
Let sem_src :=
Sem.sem p_src.
Let sem_tgt :=
Sem.sem p_tgt.
Let skenv_link_src :=
sk_link_src.(
Sk.load_skenv).
Let skenv_link_tgt :=
sk_link_tgt.(
Sk.load_skenv).
Inductive lxsim_stack:
SimMem.t ->
list Frame.t ->
list Frame.t ->
Prop :=
|
lxsim_stack_nil
sm0:
lxsim_stack sm0 [] []
|
lxsim_stack_cons
tail_src tail_tgt tail_sm ms_src lst_src0 ms_tgt lst_tgt0 sm_at sm_arg sm_arg_lift sm_init sidx
(
STACK:
lxsim_stack tail_sm tail_src tail_tgt)
(
MWF:
SimMem.wf sm_arg)
(
GE:
sim_ge sm_at sem_src.(
globalenv)
sem_tgt.(
globalenv))
(
MLE:
SimMem.le tail_sm sm_at)
(
MLE:
SimMem.le sm_at sm_arg)
(
MLELIFT:
SimMem.lepriv sm_arg sm_arg_lift)
(
MLE:
SimMem.le sm_arg_lift sm_init)
(
sound_states_local:
sidx ->
Sound.t ->
Memory.Mem.mem ->
ms_src.(
ModSem.state) ->
Prop)
(
PRSV:
forall si,
local_preservation_noguarantee ms_src (
sound_states_local si))
(
K:
forall sm_ret retv_src retv_tgt lst_src1
(
MLE:
SimMem.le sm_arg_lift sm_ret)
(
MWF:
SimMem.wf sm_ret)
(
SIMRETV:
SimMem.sim_retv retv_src retv_tgt sm_ret)
(
SU:
forall si,
exists su m_arg, (
sound_states_local si)
su m_arg lst_src0)
(
AFTERSRC:
ms_src.(
ModSem.after_external)
lst_src0 retv_src lst_src1),
exists lst_tgt1 sm_after i1,
(<<
AFTERTGT:
ms_tgt.(
ModSem.after_external)
lst_tgt0 retv_tgt lst_tgt1>>)
/\ (<<
MLEPUB:
SimMem.le sm_at sm_after>>)
/\ (<<
LXSIM:
lxsim ms_src ms_tgt (
fun st =>
forall si,
exists su m_arg, (
sound_states_local si)
su m_arg st)
tail_sm i1 lst_src1 lst_tgt1 sm_after>>))
(
SESRC:
ms_src.(
ModSem.to_semantics).(
symbolenv) =
skenv_link_src)
(
SETGT:
ms_tgt.(
ModSem.to_semantics).(
symbolenv) =
skenv_link_tgt):
lxsim_stack sm_init
((
Frame.mk ms_src lst_src0) ::
tail_src)
((
Frame.mk ms_tgt lst_tgt0) ::
tail_tgt).
Lemma lxsim_stack_le
sm0 frs_src frs_tgt sm1
(
SIMSTACK:
lxsim_stack sm0 frs_src frs_tgt)
(
MLE:
SimMem.le sm0 sm1):
<<
SIMSTACK:
lxsim_stack sm1 frs_src frs_tgt>>.
Proof.
inv SIMSTACK.
{ econs 1; eauto. }
econs 2; eauto. etransitivity; eauto.
Qed.
Inductive lxsim_lift:
idx ->
sem_src.(
Smallstep.state) ->
sem_tgt.(
Smallstep.state) ->
SimMem.t ->
Prop :=
|
lxsim_lift_intro
sm0 tail_src tail_tgt tail_sm i0 ms_src lst_src ms_tgt lst_tgt sidx
(
GE:
sim_ge sm0 sem_src.(
globalenv)
sem_tgt.(
globalenv))
(
STACK:
lxsim_stack tail_sm tail_src tail_tgt)
(
MLE:
SimMem.le tail_sm sm0)
(
sound_states_local:
sidx ->
Sound.t ->
Memory.Mem.mem ->
ms_src.(
ModSem.state) ->
Prop)
(
PRSV:
forall si,
local_preservation_noguarantee ms_src (
sound_states_local si))
(
TOP:
lxsim ms_src ms_tgt (
fun st =>
forall si,
exists su m_arg, (
sound_states_local si)
su m_arg st)
tail_sm
i0 lst_src lst_tgt sm0)
(
SESRC:
ms_src.(
ModSem.to_semantics).(
symbolenv) =
skenv_link_src)
(
SETGT:
ms_tgt.(
ModSem.to_semantics).(
symbolenv) =
skenv_link_tgt):
lxsim_lift i0 (
State ((
Frame.mk ms_src lst_src) ::
tail_src)) (
State ((
Frame.mk ms_tgt lst_tgt) ::
tail_tgt))
sm0
|
lxsim_lift_callstate
sm_arg tail_src tail_tgt tail_sm args_src args_tgt
(
GE:
sim_ge sm_arg sem_src.(
globalenv)
sem_tgt.(
globalenv))
(
STACK:
lxsim_stack tail_sm tail_src tail_tgt)
(
MLE:
SimMem.le tail_sm sm_arg)
(
MWF:
SimMem.wf sm_arg)
(
SIMARGS:
SimMem.sim_args args_src args_tgt sm_arg):
lxsim_lift idx_bot (
Callstate args_src tail_src) (
Callstate args_tgt tail_tgt)
sm_arg.
End ADQMATCH.
Section ADQINIT.
Context `{
SM:
SimMem.class}.
Context {
SS:
SimSymb.class SM}.
Context `{
SU:
Sound.class}.
Variable pp:
ProgPair.t.
Hypothesis NOTNIL:
pp <> [].
Hypothesis SIMPROG:
ProgPair.sim pp.
Let p_src :=
pp.(
ProgPair.src).
Let p_tgt :=
pp.(
ProgPair.tgt).
Variable sk_link_src sk_link_tgt:
Sk.t.
Hypothesis LINKSRC: (
link_sk p_src) =
Some sk_link_src.
Hypothesis LINKTGT: (
link_sk p_tgt) =
Some sk_link_tgt.
Let lxsim_lift := (
lxsim_lift pp).
Hint Unfold lxsim_lift.
Let sem_src :=
Sem.sem p_src.
Let sem_tgt :=
Sem.sem p_tgt.
Let skenv_link_src :=
sk_link_src.(
Sk.load_skenv).
Let skenv_link_tgt :=
sk_link_tgt.(
Sk.load_skenv).
Theorem init_lxsim_lift_forward
st_init_src
(
INITSRC:
sem_src.(
Smallstep.initial_state)
st_init_src):
exists idx st_init_tgt sm_init,
<<
INITTGT:
sem_tgt.(
Dinitial_state)
st_init_tgt>>
/\ (<<
SIM:
lxsim_lift sk_link_src sk_link_tgt idx st_init_src st_init_tgt sm_init>>)
/\ (<<
INCLSRC:
forall mp (
IN:
In mp pp),
SkEnv.includes skenv_link_src mp.(
ModPair.src).(
Mod.sk)>>)
/\ (<<
INCLTGT:
forall mp (
IN:
In mp pp),
SkEnv.includes skenv_link_tgt mp.(
ModPair.tgt).(
Mod.sk)>>).
Proof.
End ADQINIT.
Section ADQSTEP.
Context `{
SM:
SimMem.class}.
Context {
SS:
SimSymb.class SM}.
Context `{
SU:
Sound.class}.
Variable pp:
ProgPair.t.
Hypothesis SIMPROG:
ProgPair.sim pp.
Let p_src :=
pp.(
ProgPair.src).
Let p_tgt :=
pp.(
ProgPair.tgt).
Variable sk_link_src sk_link_tgt:
Sk.t.
Hypothesis LINKSRC: (
link_sk p_src) =
Some sk_link_src.
Hypothesis LINKTGT: (
link_sk p_tgt) =
Some sk_link_tgt.
Let lxsim_lift := (
lxsim_lift pp).
Hint Unfold lxsim_lift.
Let sem_src :=
Sem.sem p_src.
Let sem_tgt :=
Sem.sem p_tgt.
Let skenv_link_src :=
sk_link_src.(
Sk.load_skenv).
Let skenv_link_tgt :=
sk_link_tgt.(
Sk.load_skenv).
Variable ss_link:
SimSymb.t.
Hypothesis (
SIMSKENV:
exists sm,
SimSymb.sim_skenv sm ss_link skenv_link_src skenv_link_tgt).
Hypothesis (
INCLSRC:
forall mp (
IN:
In mp pp),
SkEnv.includes skenv_link_src mp.(
ModPair.src).(
Mod.sk)).
Hypothesis (
INCLTGT:
forall mp (
IN:
In mp pp),
SkEnv.includes skenv_link_tgt mp.(
ModPair.tgt).(
Mod.sk)).
Hypothesis (
SSLE:
forall mp (
IN:
In mp pp),
SimSymb.le mp.(
ModPair.ss)
mp.(
ModPair.src)
mp.(
ModPair.tgt)
ss_link).
Hypothesis (
WFKSSRC:
forall md (
IN:
In md (
ProgPair.src pp)), <<
WF:
Sk.wf md >>).
Hypothesis (
WFKSTGT:
forall md (
IN:
In md (
ProgPair.tgt pp)), <<
WF:
Sk.wf md >>).
Theorem lxsim_lift_xsim
i0 st_src0 st_tgt0 sm0
(
LXSIM:
lxsim_lift sk_link_src sk_link_tgt i0 st_src0 st_tgt0 sm0)
(
SUST:
__GUARD__ (
exists m_arg,
sound_state pp m_arg st_src0)):
<<
XSIM:
xsim sem_src sem_tgt ord i0 st_src0 st_tgt0>>.
Proof.
generalize dependent sm0.
generalize dependent st_src0.
generalize dependent st_tgt0.
generalize dependent i0.
pcofix CIH.
i.
pfold.
inv LXSIM;
ss;
cycle 1.
{
folder.
des_ifs.
right.
econs;
eauto.
{
i.
ss.
inv FINALTGT. }
i.
econs;
eauto;
cycle 1.
{
ii.
specialize (
SAFESRC _ (
star_refl _ _ _ _)).
des;
ss.
-
inv SAFESRC.
-
des_ifs.
right.
inv SAFESRC.
exploit find_fptr_owner_fsim;
eauto. {
eapply SimMem.sim_args_sim_fptr;
eauto. }
i;
des.
clarify.
inv SIMMS.
inv MSFIND.
inv FINDTGT.
exploit SIM;
eauto.
i;
des.
exploit INITPROGRESS;
eauto.
i;
des.
esplits;
eauto.
econs;
eauto.
econs;
eauto.
}
i.
inv STEPTGT.
specialize (
SAFESRC _ (
star_refl _ _ _ _)).
des.
{
inv SAFESRC. }
bar.
inv SAFESRC.
ss.
des_ifs.
bar.
exploit find_fptr_owner_fsim;
eauto. {
eapply SimMem.sim_args_sim_fptr;
eauto. }
i;
des.
clarify.
exploit find_fptr_owner_determ;
ss;
eauto.
{
rewrite Heq.
apply FINDTGT. }
{
rewrite Heq.
apply MSFIND. }
i;
des.
clarify.
inv SIMMS.
specialize (
SIM sm0).
inv MSFIND.
inv MSFIND0.
exploit SIM;
eauto.
i;
des.
exploit INITBSIM;
eauto.
i;
des.
clears st_init0;
clear st_init0.
esplits;
eauto.
-
left.
apply plus_one.
econs;
eauto.
econs;
eauto.
-
right.
eapply CIH.
{
unsguard SUST.
unfold __GUARD__.
des.
eapply sound_progress;
eauto.
ss.
folder.
des_ifs.
econs 2;
eauto.
econs;
eauto.
}
instantiate (1:=
sm_init).
econs;
try apply SIM0;
eauto.
+
ss.
folder.
des_ifs.
eapply mfuture_preserves_sim_ge;
eauto.
apply rtc_once.
et.
+
eapply lxsim_stack_le;
eauto.
+
ss.
inv GE.
folder.
rewrite Forall_forall in *.
eapply SESRC;
et.
+
ss.
inv GE.
folder.
rewrite Forall_forall in *.
eapply SETGT;
et.
}
sguard in SESRC.
sguard in SETGT.
folder.
rewrite LINKSRC in *.
rewrite LINKTGT in *.
punfold TOP.
rr in TOP.
hexploit1 TOP;
eauto.
{
unsguard SUST.
des.
ii.
exploit sound_progress_star;
eauto. {
eapply lift_star;
eauto. }
intro SUST0;
des.
inv SUST0.
des.
simpl_depind.
clarify.
i.
hexploit FORALLSU;
eauto.
i;
des.
specialize (
H (
sound_states_local si)).
esplits;
eauto.
eapply H;
eauto. }
inv TOP.
-
left.
exploit SU0.
{
ss. }
i;
des.
clear SU0.
right.
econs;
ss;
eauto.
+
rename H into FSTEP.
inv FSTEP.
*
econs 1;
cycle 1.
{
ii.
des.
inv FINALSRC;
ss.
exfalso.
eapply SAFESRC0.
u.
eauto. }
ii.
ss.
rewrite LINKSRC in *.
des.
inv STEPSRC;
ss;
ModSem.tac;
swap 2 3.
{
exfalso.
eapply SAFESRC;
eauto. }
{
exfalso.
eapply SAFESRC0.
u.
eauto. }
exploit STEP;
eauto.
i;
des_safe.
exists i1, (
State ((
Frame.mk ms_tgt st_tgt1) ::
tail_tgt)).
esplits;
eauto.
{
assert(
T:
DPlus ms_tgt lst_tgt tr st_tgt1 \/ (
lst_tgt =
st_tgt1 /\
tr =
E0 /\
ord i1 i0)).
{
des;
et.
inv STAR;
et.
left.
econs;
et. }
clear H.
des.
-
left.
split;
cycle 1.
{
eapply lift_receptive_at;
eauto.
unsguard SESRC.
s.
des_ifs. }
eapply lift_dplus;
eauto.
{
unsguard SETGT.
ss.
des_ifs. }
-
right.
esplits;
eauto.
clarify.
}
pclearbot.
right.
eapply CIH with (
sm0 :=
sm1);
eauto.
{
unsguard SUST.
des_safe.
eapply sound_progress;
eauto.
eapply lift_step;
eauto. }
econs;
eauto.
{
ss.
folder.
des_ifs.
eapply mfuture_preserves_sim_ge;
eauto.
apply rtc_once;
eauto. }
{
etransitivity;
eauto. }
*
des.
pclearbot.
econs 2.
{
esplits;
eauto.
eapply lift_dplus;
eauto. {
unsguard SETGT.
ss.
des_ifs. } }
right.
eapply CIH;
eauto.
instantiate (1:=
sm1).
econs;
eauto.
{
folder.
ss;
des_ifs.
eapply mfuture_preserves_sim_ge;
eauto.
eapply rtc_once;
eauto. }
{
etrans;
eauto. }
-
right.
ss.
exploit SU0.
{
ss. }
i;
des.
clear SU0.
assert(
SAFESTEP:
safe sem_src (
State ({|
Frame.ms :=
ms_src;
Frame.st :=
lst_src |} ::
tail_src))
->
safe_modsem ms_src lst_src).
{
eapply safe_implies_safe_modsem;
eauto. }
econs;
ss;
eauto.
+
ii.
exploit PROGRESS;
eauto.
intro STEPTGT;
des.
clear -
FINALTGT STEPTGT.
inv FINALTGT.
ss.
ModSem.tac.
+
ii.
exploit PROGRESS;
eauto.
intro STEPTGT;
des.
hexploit BSTEP;
eauto.
intro T.
inv T.
*
econs 1;
eauto;
cycle 1.
{
ii.
right.
des.
esplits;
eauto.
eapply lift_step;
eauto. }
ii.
inv STEPTGT0;
ModSem.tac.
ss.
exploit STEP;
eauto.
i;
des_safe.
exists i1, (
State ((
Frame.mk ms_src st_src1) ::
tail_src)).
esplits;
eauto.
{
des.
-
left.
eapply lift_plus;
eauto.
-
right.
esplits;
eauto.
eapply lift_star;
eauto.
}
pclearbot.
right.
eapply CIH with (
sm0 :=
sm1);
eauto.
{
unsguard SUST.
des_safe.
destruct H.
-
eapply sound_progress_plus;
eauto.
eapply lift_plus;
eauto.
-
des_safe.
eapply sound_progress_star;
eauto.
eapply lift_star;
eauto.
}
econs;
eauto.
{
folder.
ss;
des_ifs.
eapply mfuture_preserves_sim_ge;
eauto.
apply rtc_once;
eauto. }
etransitivity;
eauto.
*
des.
pclearbot.
econs 2.
{
esplits;
eauto.
eapply lift_star;
eauto. }
right.
eapply CIH;
eauto.
{
unsguard SUST.
des_safe.
eapply sound_progress_star;
eauto.
eapply lift_star;
eauto. }
instantiate (1:=
sm1).
econs;
eauto.
{
folder.
ss;
des_ifs.
eapply mfuture_preserves_sim_ge;
eauto.
eapply rtc_once;
eauto. }
{
etrans;
eauto. }
-
left.
right.
econs;
eauto.
econs;
eauto;
cycle 1.
{
ii.
inv FINALSRC.
ss.
ModSem.tac. }
i.
inv STEPSRC;
ss;
ModSem.tac.
des_ifs.
hexploit1 SU0.
{
ss. }
rename SU0 into CALLFSIM.
exploit CALLFSIM;
eauto.
i;
des.
esplits;
eauto.
+
left.
split;
cycle 1.
{
eapply lift_receptive_at. {
unsguard SESRC.
ss.
des_ifs. }
eapply at_external_receptive_at;
et. }
apply plus_one.
econs;
ss;
eauto.
{
eapply lift_determinate_at;
et. {
unsguard SETGT.
ss.
des_ifs. }
eapply at_external_determinate_at;
et. }
des_ifs.
econs 1;
eauto.
+
right.
eapply CIH;
eauto.
{
unsguard SUST.
des_safe.
eapply sound_progress;
eauto.
ss.
folder.
des_ifs_safe.
econs;
eauto. }
{
instantiate (1:=
sm_arg).
econs 2;
eauto.
*
ss.
folder.
des_ifs.
eapply mfuture_preserves_sim_ge;
eauto.
econs 2;
et.
*
instantiate (1:=
sm_arg).
econs; [
eassumption|..];
revgoals;
ss.
{
ii.
exploit K;
eauto.
i;
des_safe.
pclearbot.
esplits;
try apply LXSIM;
eauto. }
{
reflexivity. }
{
et. }
{
refl. }
{
et. }
{
ss.
folder.
des_ifs. }
{
eauto. }
*
reflexivity.
}
-
left.
right.
econs;
eauto.
econs;
eauto;
cycle 1.
{
ii.
ss.
inv FINALSRC0.
ss.
determ_tac ModSem.final_frame_dtm.
clear_tac.
inv STACK.
econs;
ss;
eauto.
-
econs;
ss;
eauto.
inv SIMRETV;
ss.
eapply SimMem.sim_val_int;
et.
-
i.
inv FINAL0;
inv FINAL1;
ss.
exploit ModSem.final_frame_dtm; [
apply FINAL|
apply FINAL0|..].
i;
clarify.
congruence.
-
ii.
des_ifs.
inv H;
ss;
ModSem.tac.
}
i.
ss.
des_ifs.
inv STEPSRC;
ModSem.tac.
ss.
inv STACK;
ss.
folder.
sguard in SESRC0.
sguard in SETGT0.
des_ifs.
determ_tac ModSem.final_frame_dtm.
clear_tac.
exploit K;
try apply SIMRETV;
eauto.
{
etransitivity;
eauto. }
{
unsguard SUST.
des_safe.
inv SUST.
des.
simpl_depind.
clarify.
i.
inv TL.
simpl_depind.
clarify.
des.
exploit FORALLSU0;
eauto.
i;
des.
esplits;
eauto.
eapply HD;
eauto.
}
i;
des.
esplits;
eauto.
+
left.
split;
cycle 1.
{
eapply lift_receptive_at. {
unsguard SESRC.
ss.
des_ifs. }
eapply final_frame_receptive_at;
et. }
apply plus_one.
econs;
eauto.
{
eapply lift_determinate_at. {
unsguard SETGT.
ss.
des_ifs. }
eapply final_frame_determinate_at;
et. }
econs 4;
ss;
eauto.
+
right.
eapply CIH;
eauto.
{
unsguard SUST.
des_safe.
eapply sound_progress;
eauto.
ss.
folder.
des_ifs_safe.
econs;
eauto. }
instantiate (1:=
sm_after).
econs;
ss;
cycle 3;
eauto.
{
folder.
des_ifs.
eapply mfuture_preserves_sim_ge;
et.
econs 2;
et. }
{
etrans;
eauto. }
Qed.
End ADQSTEP.
Section ADQ.
Context `{
SM:
SimMem.class}.
Context {
SS:
SimSymb.class SM}.
Context `{
SU:
Sound.class}.
Variable pp:
ProgPair.t.
Hypothesis SIMPROG:
ProgPair.sim pp.
Let p_src :=
pp.(
ProgPair.src).
Let p_tgt :=
pp.(
ProgPair.tgt).
Let sem_src :=
Sem.sem p_src.
Let sem_tgt :=
Sem.sem p_tgt.
Theorem adequacy_local:
mixed_simulation sem_src sem_tgt.
Proof.
End ADQ.