.
.
.
.
.
.
.
.
.
.
.
.
Proof.
.
Proof.
.
Proof.
.
Proof.
.
Proof.
.
Proof.
>>).
Proof.
).
Next Obligation.
Proof.
i. destruct x; try econs. destruct v; try econs. Qed.
Lemma def_match_refl A V (
g:
globdef A V):
def_match g g.
Proof.
refl. Qed.
Hint Resolve def_match_refl.
Inductive meminj_match_globals F V (
R:
globdef F V ->
globdef F V ->
Prop)
(
ge_src ge_tgt:
Genv.t F V) (
j:
meminj) :
Prop :=
|
meminj_match_globals_intro
(
DEFLE:
forall
b_src b_tgt delta d_src
(
FINDSRC:
Genv.find_def ge_src b_src =
Some d_src)
(
INJ:
j b_src =
Some (
b_tgt,
delta)),
exists d_tgt,
(<<
FINDTGT:
Genv.find_def ge_tgt b_tgt =
Some d_tgt>>) /\
(<<
DELTA:
delta = 0>>) /\
(<<
DEFMATCH:
R d_src d_tgt>>))
(
SYMBLE:
forall
i b_src
(
FINDSRC:
Genv.find_symbol ge_src i =
Some b_src),
exists b_tgt,
(<<
FINDTGT:
Genv.find_symbol ge_tgt i =
Some b_tgt>>) /\
(<<
INJ:
j b_src =
Some (
b_tgt, 0)>>)).
Lemma SimSymbDrop_match_globals F `{
HasExternal F}
V sm0 skenv_src skenv_tgt (
p:
program F V)
(
SIMSKE:
SimSymbDrop.sim_skenv sm0 bot1 skenv_src skenv_tgt):
meminj_match_globals
eq
(
SkEnv.revive skenv_src p)
(
SkEnv.revive skenv_tgt p)
(
SimMemInj.inj sm0).
Proof.
inv SIMSKE.
econs.
-
i.
unfold SkEnv.revive in *.
exists d_src.
apply Genv_map_defs_def in FINDSRC.
des.
unfold o_bind,
o_bind2,
o_join,
o_map,
curry2,
fst in MAP.
des_ifs_safe.
apply Genv.invert_find_symbol in Heq0.
exploit SIMDEF;
try apply FIND;
eauto.
i.
des.
clarify.
esplits;
eauto.
exploit Genv_map_defs_def_inv;
try apply DEFTGT.
i.
rewrite H0.
unfold o_bind,
o_bind2,
o_join,
o_map,
curry2,
fst.
erewrite Genv.find_invert_symbol.
+
rewrite Heq1;
eauto.
+
exploit SIMSYMB1;
eauto.
i.
des.
eauto.
-
i.
unfold SkEnv.revive in *.
rewrite Genv_map_defs_symb in FINDSRC.
exploit SIMSYMB2;
try apply FINDSRC;
eauto.
Qed.
Lemma SimSymbDrop_symbols_inject sm0 ss_link skenv_src skenv_tgt
(
SIMSKELINK:
SimSymbDrop.sim_skenv sm0 ss_link skenv_src skenv_tgt):
symbols_inject (
SimMemInj.inj sm0)
skenv_src skenv_tgt.
Proof.
inv SIMSKELINK.
econs;
esplits;
ss;
i.
-
unfold Genv.public_symbol,
proj_sumbool.
rewrite PUB in *.
des_ifs;
ss.
+
exploit SIMSYMB3;
eauto.
i.
des.
clarify.
+
exploit SIMSYMB2;
eauto.
i.
des.
clarify.
-
exploit SIMSYMB1;
eauto.
i.
des.
eauto.
-
exploit SIMSYMB2;
eauto.
{
unfold Genv.public_symbol,
proj_sumbool in *.
des_ifs.
eauto. }
i.
des.
eauto.
-
unfold Genv.block_is_volatile,
Genv.find_var_info.
destruct (
Genv.find_def skenv_src b1)
eqn:
DEQ.
+
exploit SIMDEF;
eauto.
i.
des.
clarify.
rewrite DEFTGT.
eauto.
+
des_ifs_safe.
exfalso.
exploit SIMDEFINV;
eauto.
i.
des.
clarify.
Qed.
Lemma match_globals_find_funct F V (
ge_src ge_tgt:
Genv.t F V)
j fptr_src fptr_tgt d
(
FINDSRC:
Genv.find_funct ge_src fptr_src =
Some d)
(
GENV:
meminj_match_globals eq ge_src ge_tgt j)
(
FPTR:
Val.inject j fptr_src fptr_tgt):
Genv.find_funct ge_tgt fptr_tgt =
Some d.
Proof.
Lemma SimSymbDrop_find_None F `{
HasExternal F}
V (
p:
program F V)
sm0 skenv_src skenv_tgt fptr_src fptr_tgt
(
FINDSRC:
Genv.find_funct (
SkEnv.revive skenv_src p)
fptr_src =
None)
(
SIMSKE:
SimSymbDrop.sim_skenv sm0 bot1 skenv_src skenv_tgt)
(
FPTR:
Val.inject (
SimMemInj.inj sm0)
fptr_src fptr_tgt)
(
FPTRDEF:
fptr_src <>
Vundef):
Genv.find_funct (
SkEnv.revive skenv_tgt p)
fptr_tgt =
None.
Proof.
Require MatchSimModSem.
Lemma any_id
(
md:
Mod.t)
(
WF:
Sk.wf md):
exists mp,
(<<
SIM: @
ModPair.sim SimMemId.SimMemId SimMemId.SimSymbId SoundTop.Top mp>>)
/\ (<<
SRC:
mp.(
ModPair.src) =
md>>)
/\ (<<
TGT:
mp.(
ModPair.tgt) =
md>>).
Proof.
eexists (
ModPair.mk _ _ _);
s.
esplits;
eauto.
instantiate (1:=
tt).
econs;
ss;
i.
rewrite SIMSKENVLINK in *.
inv SIMSKENVLINK.
inv SSLE.
eapply MatchSimModSem.match_states_sim;
ss.
-
apply unit_ord_wf.
-
eapply SoundTop.sound_state_local_preservation.
-
instantiate (1:=
fun sm_arg _ st_src st_tgt sm0 =>
(<<
EQ:
st_src =
st_tgt>>) /\
(<<
MWF:
sm0.(
SimMemId.src) =
sm0.(
SimMemId.tgt)>>)).
ss.
i.
inv SIMARGS;
ss;
esplits;
eauto;
try congruence.
assert(
rs_tgt =
rs_src)
by (
eapply functional_extensionality;
r in RS;
ss).
congruence.
-
ii.
destruct args_src,
args_tgt,
sm_arg;
inv SIMARGS;
ss;
clarify.
assert(
rs_tgt =
rs_src)
by (
eapply functional_extensionality;
r in RS;
ss).
subst.
eauto.
-
ii.
ss.
des.
clarify.
-
i.
ss.
des.
clarify.
destruct args_src,
sm0;
ss;
clarify.
+
eexists _, (
SimMemId.mk _ _).
ss.
esplits;
eauto.
*
econs;
ss;
eauto.
*
instantiate (1:=
top4).
ss.
+
eexists _, (
SimMemId.mk _ _).
ss.
esplits;
eauto.
*
econs 2;
ss;
eauto.
-
i.
clear HISTORY.
ss.
destruct sm_ret,
retv_src,
retv_tgt;
inv SIMRET;
des;
ss;
clarify;
eexists (
SimMemId.mk _ _);
esplits;
eauto.
assert(
rs_tgt =
rs_src)
by (
eapply functional_extensionality;
r in RS;
ss).
congruence.
-
i.
ss.
des.
destruct sm0.
ss.
clarify.
destruct retv_src;
ss;
eexists (
SimMemId.mk m m);
esplits;
eauto.
+
econs;
ss;
eauto.
+
econs 2;
ss;
eauto.
-
right.
ii.
des.
destruct sm0.
ss.
clarify.
esplits;
eauto.
+
i.
exploit H;
ss.
*
econs 1.
*
i.
des;
clarify.
econs;
eauto.
+
i.
exists tt,
st_tgt1.
eexists (
SimMemId.mk _ _).
ss.
esplits;
eauto.
left.
econs;
eauto; [
econs 1|].
symmetry.
apply E0_right.
Unshelve.
all:
ss.
Qed.