Require Import Events.
Require Import Values.
Require Import AST.
Require Import MemoryC.
Require Import Globalenvs.
Require Import Smallstep.
Require Import CoqlibC.
Require Import Skeleton.
Require Import IntegersC.
Require Import ASTC.
Require Import LinkingC.
Require Import SimSymb.
Require Import MapsC.
Set Implicit Arguments.
Require Import SimSymb.
Require Import SimMem.
Require Import SimMemInjInvC.
Require Import ModSem.
Definition ref_init (
il :
list init_data) (
id :
ident):
Prop :=
exists ofs,
In (
Init_addrof id ofs)
il
.
Section MEMINJ.
Definition SimMemInvTop:
SimMem.class :=
SimMemInjInvC.SimMemInjInv SimMemInjInv.top_inv SimMemInjInv.top_inv.
Local Existing Instance SimMemInvTop.
Definition t':
Type :=
ident ->
Prop.
Inductive sim_sk (
ss:
t') (
sk_src sk_tgt:
Sk.t):
Prop :=
|
sim_sk_intro
(
KEPT:
forall
id
(
KEPT: ~
ss id)
,
sk_tgt.(
prog_defmap) !
id =
sk_src.(
prog_defmap) !
id)
(
DROP:
forall
id
(
DROP:
ss id)
,
sk_tgt.(
prog_defmap) !
id =
None)
(
CLOSED:
ss <1=
sk_src.(
privs))
(
PUB:
sk_src.(
prog_public) =
sk_tgt.(
prog_public))
(
MAIN:
sk_src.(
prog_main) =
sk_tgt.(
prog_main))
(
NOREF:
forall
id gv
(
PROG:
sk_tgt.(
prog_defmap) !
id =
Some (
Gvar gv))
,
<<
NOREF:
forall id_drop (
DROP:
ss id_drop), ~
ref_init gv.(
gvar_init)
id_drop>>)
(
NODUP:
NoDup (
prog_defs_names sk_tgt))
(
NOMAIN: ~
ss sk_src.(
prog_main))
.
Inductive sim_skenv (
sm0:
SimMem.t) (
ss:
t') (
skenv_src skenv_tgt:
SkEnv.t):
Prop :=
|
sim_skenv_intro
(
SIMSYMB1:
forall
id blk_src blk_tgt delta
(
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src)
,
(<<
DELTA:
delta = 0>>) /\
(<<
BLKTGT:
skenv_tgt.(
Genv.find_symbol)
id =
Some blk_tgt>>) /\
(<<
KEPT: ~
ss id>>)
)
(
SIMSYMB2:
forall
id
(
KEPT: ~
ss id)
blk_src
(
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src)
,
exists blk_tgt,
(<<
BLKTGT:
skenv_tgt.(
Genv.find_symbol)
id =
Some blk_tgt>>) /\
(<<
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt, 0)>>))
(
SIMSYMB3:
forall
id blk_tgt
(
BLKTGT:
skenv_tgt.(
Genv.find_symbol)
id =
Some blk_tgt)
,
exists blk_src,
(<<
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src>>) /\
(<<
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt, 0)>>)
)
(
SSINV:
forall
id blk_src
(
KEPT:
ss id)
(
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src)
,
sm0.(
SimMemInjInv.mem_inv_src)
blk_src)
(
SIMDEF:
forall
blk_src blk_tgt delta def_src
(
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
DEFSRC:
skenv_src.(
Genv.find_def)
blk_src =
Some def_src)
,
exists def_tgt, (<<
DEFTGT:
skenv_tgt.(
Genv.find_def)
blk_tgt =
Some def_tgt>>) /\
(<<
DELTA:
delta = 0>>) /\
(<<
SIM:
def_src =
def_tgt>>))
(
DISJ:
forall
id blk_src0 blk_src1 blk_tgt
(
SYMBSRC:
Genv.find_symbol skenv_src id =
Some blk_src0)
(
SIMVAL0:
sm0.(
SimMemInj.inj)
blk_src0 =
Some (
blk_tgt, 0))
(
SIMVAL1:
sm0.(
SimMemInj.inj)
blk_src1 =
Some (
blk_tgt, 0))
,
blk_src0 =
blk_src1)
(
SIMDEFINV:
forall
blk_src blk_tgt delta def_tgt
(
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
DEFTGT:
skenv_tgt.(
Genv.find_def)
blk_tgt =
Some def_tgt)
,
exists def_src, (<<
DEFSRC:
skenv_src.(
Genv.find_def)
blk_src =
Some def_src>>) /\
(<<
DELTA:
delta = 0>>) /\
(<<
SIM:
def_src =
def_tgt>>))
(
PUBKEPT: (
fun id =>
In id skenv_src.(
Genv.genv_public)) <1= ~1
ss)
(
PUB:
skenv_src.(
Genv.genv_public) =
skenv_tgt.(
Genv.genv_public))
(
NBSRC:
skenv_src.(
Genv.genv_next) =
sm0.(
SimMemInj.src_ge_nb))
(
NBTGT:
skenv_tgt.(
Genv.genv_next) =
sm0.(
SimMemInj.tgt_ge_nb))
.
Theorem sim_skenv_symbols_inject
sm0 ss0 skenv_src skenv_tgt
(
SIMSKENV:
sim_skenv sm0 ss0 skenv_src skenv_tgt)
:
<<
SINJ:
symbols_inject sm0.(
SimMemInj.inj)
skenv_src skenv_tgt>>
.
Proof.
{
clear -
SIMSKENV.
inv SIMSKENV;
ss.
rr.
esplits;
ii;
ss.
-
unfold Genv.public_symbol.
rewrite <-
PUB.
destruct (
Genv.find_symbol skenv_tgt id)
eqn:
T.
+
exploit SIMSYMB3;
et.
i;
des.
rewrite BLKSRC.
ss.
+
des_ifs.
des_sumbool.
ii.
exploit PUBKEPT;
et.
apply NNPP.
ii.
exploit SIMSYMB2;
et.
i;
des.
clarify.
-
exploit SIMSYMB1;
eauto.
i;
des.
esplits;
et.
-
exploit SIMSYMB2;
eauto.
{
ii.
eapply PUBKEPT;
eauto.
unfold Genv.public_symbol in H.
des_ifs.
des_sumbool.
ss. }
i;
des.
esplits;
eauto.
-
unfold Genv.block_is_volatile,
Genv.find_var_info.
destruct (
Genv.find_def skenv_src b1)
eqn:
T0.
{
exploit SIMDEF;
try eassumption.
i;
des.
des_ifs.
}
destruct (
Genv.find_def skenv_tgt b2)
eqn:
T1.
{
exploit SIMDEFINV;
try eassumption.
i;
des.
des_ifs.
}
ss.
}
Qed.
Definition sim_skenv_splittable (
sm0:
SimMem.t) (
ss:
t') (
skenv_src skenv_tgt:
SkEnv.t):
Prop :=
(<<
SIMSYMB1:
forall
id blk_src blk_tgt delta
(
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src)
,
(<<
DELTA:
delta = 0>>) /\
(<<
BLKTGT:
skenv_tgt.(
Genv.find_symbol)
id =
Some blk_tgt>>) /\
(<<
KEPT: ~
ss id>>)
>>)
/\
(<<
SIMSYMB2:
forall
id
(
KEPT: ~
ss id)
blk_src
(
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src)
,
exists blk_tgt,
(<<
BLKTGT:
skenv_tgt.(
Genv.find_symbol)
id =
Some blk_tgt>>) /\
(<<
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt, 0)>>)>>)
/\
(<<
SIMSYMB3:
forall
id blk_tgt
(
BLKTGT:
skenv_tgt.(
Genv.find_symbol)
id =
Some blk_tgt)
,
exists blk_src,
(<<
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src>>) /\
(<<
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt, 0)>>)
>>)
/\
(<<
SSINV:
forall
id blk_src
(
KEPT:
ss id)
(
BLKSRC:
skenv_src.(
Genv.find_symbol)
id =
Some blk_src)
,
sm0.(
SimMemInjInv.mem_inv_src)
blk_src>>)
/\
(<<
SIMDEF:
forall
blk_src blk_tgt delta def_src
(
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
DEFSRC:
skenv_src.(
Genv.find_def)
blk_src =
Some def_src)
,
exists def_tgt, (<<
DEFTGT:
skenv_tgt.(
Genv.find_def)
blk_tgt =
Some def_tgt>>) /\
(<<
DELTA:
delta = 0>>) /\
(<<
SIM:
def_src =
def_tgt>>)>>)
/\
(<<
DISJ:
forall
id blk_src0 blk_src1 blk_tgt
(
SYMBSRC:
Genv.find_symbol skenv_src id =
Some blk_src0)
(
SIMVAL0:
sm0.(
SimMemInj.inj)
blk_src0 =
Some (
blk_tgt, 0))
(
SIMVAL1:
sm0.(
SimMemInj.inj)
blk_src1 =
Some (
blk_tgt, 0))
,
blk_src0 =
blk_src1>>)
/\
(<<
SIMDEFINV:
forall
blk_src blk_tgt delta def_tgt
(
SIMVAL:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
DEFTGT:
skenv_tgt.(
Genv.find_def)
blk_tgt =
Some def_tgt)
,
exists def_src, (<<
DEFSRC:
skenv_src.(
Genv.find_def)
blk_src =
Some def_src>>) /\
(<<
DELTA:
delta = 0>>) /\
(<<
SIM:
def_src =
def_tgt>>)>>)
/\
(<<
PUBKEPT: (
fun id =>
In id skenv_src.(
Genv.genv_public)) <1= ~1
ss>>)
/\
(<<
PUB:
skenv_src.(
Genv.genv_public) =
skenv_tgt.(
Genv.genv_public)>>)
/\ (<<
NBSRC:
skenv_src.(
Genv.genv_next) =
sm0.(
SimMemInj.src_ge_nb)>>)
/\ (<<
NBTGT:
skenv_tgt.(
Genv.genv_next) =
sm0.(
SimMemInj.tgt_ge_nb)>>)
.
Theorem sim_skenv_splittable_spec
:
(
sim_skenv_splittable <4=
sim_skenv) /\ (
sim_skenv <4=
sim_skenv_splittable)
.
Proof.
split; ii; inv PR; ss; des; econs; eauto.
splits; ss.
Qed.
Inductive le (
ss0:
t') (
sk_src sk_tgt:
Sk.t) (
ss1:
t'):
Prop :=
|
le_intro
(
LE:
ss0 <1=
ss1)
(
OUTSIDE:
forall
id
(
IN: (
ss1 -1
ss0)
id)
,
<<
OUTSIDESRC: ~
sk_src.(
defs)
id>> /\ <<
OUTSIDETGT: ~
sk_tgt.(
defs)
id>>)
.
Global Program Definition link_ss (
ss0 ss1:
t'):
option t' :=
Some (
ss0 \1/
ss1)
.
Global Program Instance Linker_t:
Linker t' := {|
link :=
link_ss;
linkorder (
ss0 ss1:
t') :=
ss0 <1=
ss1;
|}.
Lemma linkorder_defs
F V
`{
Linker F} `{
Linker V}
(
p0 p1:
AST.program F V)
(
LINKORD:
linkorder p0 p1)
:
<<
DEFS:
p0.(
defs) <1=
p1.(
defs)>>
.
Proof.
inv LINKORD.
ii.
u in *.
des.
simpl_bool.
des_sumbool.
apply prog_defmap_spec in PR.
des.
exploit H3;
try eassumption.
i;
des.
apply prog_defmap_spec.
esplits;
eauto.
Qed.
Lemma Genv_invert_symbol_none_spec
F V
(
ge:
Genv.t F V)
b
:
<<
INV:
Genv.invert_symbol ge b =
None>> <-> <<
FIND:
forall id,
Genv.find_symbol ge id <>
Some b>>
.
Proof.
Lemma or_des A B (
OR:
A \/
B):
(
A /\
B) \/ (
A /\ ~
B) \/ (~
A /\
B).
Proof.
tauto. Qed.
Let init_meminj (
sk_src sk_tgt:
Sk.t) :
meminj :=
fun b =>
match Genv.invert_symbol (
Sk.load_skenv sk_src)
b with
|
Some id =>
match Genv.find_symbol (
Sk.load_skenv sk_tgt)
id with
|
Some b' =>
Some (
b', 0)
|
None =>
None
end
|
None =>
None
end.
Remark init_meminj_invert
sk_src sk_tgt ss
b b'
delta
(
INJ: (
init_meminj sk_src sk_tgt)
b =
Some(
b',
delta))
(
SIMSK :
sim_sk ss sk_src sk_tgt)
:
delta = 0 /\
exists id,
Genv.find_symbol (
Sk.load_skenv sk_src)
id =
Some b /\
Genv.find_symbol (
Sk.load_skenv sk_tgt)
id =
Some b' /\ ~
ss id.
Proof.
Remark init_meminj_eq
sk_src sk_tgt ss
id b b'
(
SYMBOL:
Genv.find_symbol (
Sk.load_skenv sk_src)
id =
Some b)
(
SYMBOL2:
Genv.find_symbol (
Sk.load_skenv sk_tgt)
id =
Some b')
(
SIMSK:
sim_sk ss sk_src sk_tgt)
:
(
init_meminj sk_src sk_tgt)
b =
Some(
b', 0).
Proof.
Lemma init_mem_exists
sk_src sk_tgt
ss m_src
(
SIMSK:
sim_sk ss sk_src sk_tgt)
(
LOADMEMSRC:
Sk.load_mem sk_src =
Some m_src)
:
exists m_tgt,
Sk.load_mem sk_tgt =
Some m_tgt.
Proof.
Lemma init_meminj_simskenv
sk_src sk_tgt ss
m_src m_tgt
(
LOADMEMSRC:
Sk.load_mem sk_src =
Some m_src)
(
LOADMEMTGT:
Sk.load_mem sk_tgt =
Some m_tgt)
(
SIMSK:
sim_sk ss sk_src sk_tgt)
:
sim_skenv
(
mk (
SimMemInj.mk m_src m_tgt (
init_meminj sk_src sk_tgt)
bot2 bot2 (
Mem.nextblock m_src) (
Mem.nextblock m_tgt) (
Mem.nextblock m_src) (
Mem.nextblock m_tgt))
(
fun blk =>
forall ofs,
loc_unmapped (
init_meminj sk_src sk_tgt)
blk ofs /\
Mem.valid_block m_src blk)
bot1)
ss (
Sk.load_skenv sk_src) (
Sk.load_skenv sk_tgt).
Proof.
Lemma init_meminj_invert_strong
sk_src sk_tgt ss
b b'
delta
(
INJ: (
init_meminj sk_src sk_tgt)
b =
Some(
b',
delta))
(
SIMSK :
sim_sk ss sk_src sk_tgt)
:
delta = 0 /\
exists id gd,
Genv.find_symbol (
Sk.load_skenv sk_src)
id =
Some b
/\
Genv.find_symbol (
Sk.load_skenv sk_tgt)
id =
Some b'
/\
Genv.find_def (
Sk.load_skenv sk_src)
b =
Some gd
/\
Genv.find_def (
Sk.load_skenv sk_tgt)
b' =
Some gd.
Proof.
Lemma bytes_of_init_inject
sk_src sk_tgt ss
m_src il
(
SIMSK:
sim_sk ss sk_src sk_tgt)
(
LOADMEMSRC:
Sk.load_mem sk_src =
Some m_src)
(
REF:
forall id,
ref_init il id -> ~
ss id)
:
list_forall2 (
memval_inject (
init_meminj sk_src sk_tgt)) (
Genv.bytes_of_init_data_list (
Sk.load_skenv sk_src)
il) (
Genv.bytes_of_init_data_list (
Sk.load_skenv sk_tgt)
il).
Proof.
Lemma Mem_getN_forall2:
forall (
P:
memval ->
memval ->
Prop)
c1 c2 i n p,
list_forall2 P (
Mem.getN n p c1) (
Mem.getN n p c2) ->
p <=
i ->
i <
p +
Z.of_nat n ->
P (
ZMap.get i c1) (
ZMap.get i c2).
Proof.
induction n;
simpl Mem.getN;
intros.
-
simpl in H1.
omegaContradiction.
-
inv H.
rewrite Nat2Z.inj_succ in H1.
destruct (
zeq i p).
+
congruence.
+
apply IHn with (
p + 1);
auto.
omega.
omega.
Qed.
Lemma SimSymbDropInv_func_bisim sm ss skenv_src skenv_tgt
(
SIMSKENV:
sim_skenv sm ss skenv_src skenv_tgt)
:
SimSymb.skenv_func_bisim (
Val.inject (
SimMemInj.inj sm))
skenv_src skenv_tgt.
Proof.
inv SIMSKENV.
econs;
eauto;
ii;
ss.
inv SIMFPTR;
ss.
des_ifs_safe;
ss.
unfold Genv.find_funct_ptr in *.
des_ifs_safe.
exploit SIMDEF;
eauto.
i;
des.
inv SIM.
rewrite DEFTGT.
esplits;
eauto.
des_ifs.
Qed.
Global Program Instance SimSymbDropInv:
SimSymb.class SimMemInvTop := {
t :=
t';
le :=
le;
sim_sk :=
sim_sk;
sim_skenv :=
sim_skenv;
}.
Next Obligation.
econs; eauto. ii. des; ss.
Qed.
Next Obligation.
inv LE0.
inv LE1.
econs;
eauto.
ii;
des.
specialize (
OUTSIDE id).
specialize (
OUTSIDE0 id).
destruct (
classic (
ss1 id)).
-
exploit OUTSIDE;
eauto.
-
exploit OUTSIDE0;
eauto.
i;
des.
hexploit (
linkorder_defs LINKORD0);
eauto.
i;
des.
hexploit (
linkorder_defs LINKORD1);
eauto.
i;
des.
esplits;
eauto.
Qed.
Next Obligation.
Next Obligation.
inv SIMSK.
inv SIMSK0.
exploit (
link_prog_inv sk_src0 sk_src1);
eauto.
i;
des.
assert(
AUX1:
forall id,
ss1 id -> ~
ss0 id -> (
prog_defmap sk_src0) !
id =
None).
{
i.
destruct ((
prog_defmap sk_src0) !
id)
eqn:
T;
ss.
apply CLOSED0 in H2.
unfold privs,
defs,
NW in *.
bsimpl.
des.
des_sumbool.
exploit prog_defmap_dom;
eauto.
i;
des.
exploit H0;
eauto.
i;
des.
clarify.
}
assert(
AUX2:
forall id,
ss0 id -> ~
ss1 id -> (
prog_defmap sk_src1) !
id =
None).
{
i.
destruct ((
prog_defmap sk_src1) !
id)
eqn:
T;
ss.
apply CLOSED in H2.
unfold privs,
defs,
NW in *.
bsimpl.
des.
des_sumbool.
exploit prog_defmap_dom;
eauto.
i;
des.
exploit H0;
eauto.
i;
des.
clarify.
}
i.
exists (
ss0 \1/
ss1).
eexists.
esplits;
eauto.
-
eapply (
link_prog_succeeds sk_tgt0 sk_tgt1);
eauto;
try congruence.
i.
exploit H0.
{
erewrite <-
KEPT;
et.
ii.
eapply DROP in H4.
congruence. }
{
erewrite <-
KEPT0;
et.
ii.
eapply DROP0 in H4.
congruence. }
i;
des.
esplits;
congruence.
-
econs;
ii;
et.
des;
des_ifs.
esplits;
et.
+
ii.
eapply defs_prog_defmap in H1.
des.
exploit AUX1;
eauto.
congruence.
+
ii.
eapply defs_prog_defmap in H1.
des.
exploit AUX1;
eauto.
i.
exploit KEPT;
eauto.
congruence.
-
econs;
ii;
et.
des;
des_ifs.
esplits;
et.
+
ii.
eapply defs_prog_defmap in H1.
des.
exploit AUX2;
eauto.
congruence.
+
ii.
eapply defs_prog_defmap in H1.
des.
exploit AUX2;
eauto.
i.
exploit KEPT0;
eauto.
congruence.
-
subst.
econs;
ss;
ii;
try congruence.
+
eapply not_or_and in KEPT1.
des.
rewrite !
prog_defmap_elements, !
PTree.gcombine by auto.
rewrite KEPT;
ss.
rewrite KEPT0;
ss.
+
rewrite prog_defmap_elements.
rewrite PTree.gcombine;
ss.
apply or_des in DROP1.
des.
*
rewrite DROP;
ss.
rewrite DROP0;
ss.
*
rewrite DROP;
ss.
rewrite KEPT0;
ss.
apply AUX2;
ss.
*
rewrite DROP0;
ss.
rewrite KEPT;
ss.
rewrite AUX1;
ss.
+
rr.
unfold privs.
ss.
bsimpl.
split.
{
assert(
T:
exists x1,
link_prog_merge (
prog_defmap sk_src0) !
x0 (
prog_defmap sk_src1) !
x0 =
Some x1).
{
des.
-
exploit CLOSED;
et.
intro T.
unfold privs in T.
unfold NW in *.
bsimpl.
des_safe.
des_sumbool.
apply defs_prog_defmap in T.
des.
rewrite T.
destruct ((
prog_defmap sk_src1) !
x0)
eqn:
EQN.
+
exploit H0;
et.
i;
des.
ss.
+
eexists.
ss.
-
exploit CLOSED0;
et.
intro T.
unfold privs in T.
unfold NW in *.
bsimpl.
des_safe.
des_sumbool.
apply defs_prog_defmap in T.
des.
rewrite T.
destruct ((
prog_defmap sk_src0) !
x0)
eqn:
EQN.
+
exploit H0;
et.
i;
des.
ss.
+
eexists.
ss.
}
clear PR.
des_safe.
rr.
unfold defs.
unfold NW.
des_sumbool.
unfold prog_defs_names.
ss.
rewrite in_map_iff.
eexists (
_,
_).
s.
esplits;
eauto.
eapply PTree.elements_correct;
eauto.
rewrite PTree.gcombine;
ss.
eauto.
}
unfold NW.
bsimpl.
des_sumbool.
intro T.
rewrite in_app_iff in T.
destruct PR.
*
exploit CLOSED;
eauto.
intro TT.
unfold privs,
NW in TT.
bsimpl.
des_safe.
des_sumbool.
des;
ss.
apply defs_prog_defmap in TT.
inv WFSRC1.
apply PUBINCL in T.
apply prog_defmap_dom in T.
des.
exploit H0;
et.
i;
des.
ss.
*
exploit CLOSED0;
eauto.
intro TT.
unfold privs,
NW in TT.
bsimpl.
des_safe.
des_sumbool.
des;
ss.
apply defs_prog_defmap in TT.
inv WFSRC0.
apply PUBINCL in T.
apply prog_defmap_dom in T.
des.
exploit H0;
et.
i;
des.
ss.
+
assert(
T: (
In (
id,
Gvar gv) (
prog_defs sk_tgt0))
\/ (
In (
id,
Gvar gv) (
prog_defs sk_tgt1))).
{
unfold prog_defmap in PROG.
ss.
rewrite PTree_Properties.of_list_elements in *.
rewrite PTree.gcombine in *;
ss.
unfold link_prog_merge in PROG.
clear -
PROG.
des_ifs.
-
apply PTree_Properties.in_of_list in Heq.
apply PTree_Properties.in_of_list in Heq0.
exploit (
link_unit_same g g0);
et.
i;
des;
clarify;
et.
-
apply PTree_Properties.in_of_list in Heq.
eauto.
-
apply PTree_Properties.in_of_list in PROG.
eauto.
}
assert(
U: ~
In id_drop (
prog_defs_names sk_tgt0) /\ ~
In id_drop (
prog_defs_names sk_tgt1)).
{
split.
-
destruct (
classic (
ss0 id_drop)).
+
exploit DROP;
eauto.
intro V.
intro W.
exploit prog_defmap_dom;
et.
i;
des;
clarify.
+
desH DROP1;
et.
exploit KEPT;
et.
intro V.
exploit AUX1;
eauto.
i.
ii.
exploit prog_defmap_dom;
et.
i;
des_safe;
clarify.
congruence.
-
destruct (
classic (
ss1 id_drop)).
+
exploit DROP0;
eauto.
intro V.
intro W.
exploit prog_defmap_dom;
et.
i;
des;
clarify.
+
desH DROP1;
et.
exploit KEPT0;
et.
intro V.
exploit AUX2;
eauto.
i.
ii.
exploit prog_defmap_dom;
et.
i;
des_safe;
clarify.
congruence.
}
desH T.
*
inv WFTGT0.
rr in H1.
des_safe.
exploit WFPTR;
eauto.
*
inv WFTGT1.
rr in H1.
des_safe.
exploit WFPTR;
eauto.
+
apply NoDup_norepet.
apply PTree.elements_keys_norepet.
+
des;
congruence.
Qed.
Next Obligation.
inv SIMSKE.
unfold Genv.public_symbol.
apply func_ext1.
intro i0.
destruct (
Genv.find_symbol skenv_tgt i0)
eqn:
T.
-
exploit SIMSYMB3;
et.
i;
des.
des_ifs.
rewrite PUB.
ss.
-
des_ifs.
des_sumbool.
ii.
eapply PUBKEPT in H.
exploit SIMSYMB2;
et.
i;
des.
clarify.
Qed.
Next Obligation.
Next Obligation.
inv MLE.
inv SIMSKENV.
assert (
SAME:
forall b b'
delta,
Plt b (
Genv.genv_next skenv_src) ->
SimMemInj.inj sm1 b =
Some(
b',
delta) ->
SimMemInj.inj sm0 b =
Some(
b',
delta)).
{
i.
destruct (
SimMemInj.inj sm0 b)
eqn:
T;
ss.
-
destruct p;
ss.
exploit INCR;
eauto.
i;
clarify.
-
inv FROZEN.
exploit NEW_IMPLIES_OUTSIDE;
eauto.
i.
des.
unfold Mem.valid_block in *.
rewrite <-
NBSRC in *.
xomega. }
apply sim_skenv_splittable_spec.
rr.
dsplits;
eauto;
try congruence; [..|
M|
M];
Mskip ii.
-
i.
eapply SIMSYMB1;
eauto.
eapply SAME;
try eapply Genv.genv_symb_range;
eauto.
-
i.
exploit SIMSYMB2;
eauto.
i;
des.
eexists.
splits;
eauto.
-
i.
exploit SIMSYMB3;
eauto.
i;
des.
eexists.
splits;
eauto.
-
rewrite <-
INVSRC.
eauto.
-
i.
exploit SIMDEF;
eauto.
eapply SAME;
try eapply Genv.genv_defs_range;
eauto.
-
ii.
eapply DISJ;
eauto.
eapply SAME;
try eapply Genv.genv_symb_range;
eauto.
destruct (
SimMemInj.inj sm0 blk_src1)
eqn:
T;
ss.
{
destruct p;
ss.
exploit INCR;
et.
i;
clarify. }
exfalso.
inv FROZEN.
exploit NEW_IMPLIES_OUTSIDE;
eauto.
i;
des.
exploit SPLITHINT;
try apply SYMBSRC;
eauto.
i;
des.
clear_tac.
exploit Genv.genv_symb_range;
eauto.
i.
unfold Mem.valid_block in *.
rewrite <-
NBTGT in *.
xomega.
-
ii.
eapply SIMDEFINV;
eauto.
destruct (
SimMemInj.inj sm0 blk_src)
as [[
b1 delta1] | ]
eqn:
J.
+
exploit INCR;
eauto.
congruence.
+
inv FROZEN.
exploit NEW_IMPLIES_OUTSIDE;
eauto.
i;
des.
exploit Genv.genv_defs_range;
eauto.
i.
unfold Mem.valid_block in *.
rewrite <-
NBTGT in *.
xomega.
Qed.
Next Obligation.
set (
SkEnv.project skenv_link_src sk_src)
as skenv_src.
generalize (
SkEnv.project_impl_spec INCLSRC);
intro LESRC.
set (
SkEnv.project skenv_link_tgt sk_tgt)
as skenv_tgt.
generalize (
SkEnv.project_impl_spec INCLTGT);
intro LETGT.
exploit SkEnv.project_spec_preserves_wf;
try apply LESRC;
eauto.
intro WFSMALLSRC.
exploit SkEnv.project_spec_preserves_wf;
try apply LETGT;
eauto.
intro WFSMALLTGT.
inv SIMSKENV.
ss.
apply sim_skenv_splittable_spec.
folder.
dsplits;
eauto;
ii;
ss.
-
inv LESRC.
destruct (
classic (
defs sk_src id));
cycle 1.
{
exfalso.
exploit SYMBDROP;
eauto.
i;
des.
clarify. }
exploit SYMBKEEP;
eauto.
intro KEEP;
des.
exploit SIMSYMB1;
eauto. {
rewrite <-
KEEP.
ss. }
i;
des.
inv LETGT.
destruct (
classic (
defs sk_tgt id));
cycle 1.
{
erewrite SYMBDROP0;
ss.
exfalso.
clear -
LE KEPT H H0 SIMSK.
apply H0.
clear H0.
inv SIMSK.
u in *.
simpl_bool.
des_sumbool.
rewrite prog_defmap_spec in *.
des.
destruct (
classic (
ss id));
cycle 1.
-
erewrite KEPT0;
ss.
esplits;
eauto.
-
exfalso.
apply KEPT.
inv LE.
eauto.
}
erewrite SYMBKEEP0;
ss.
esplits;
eauto.
{
clear -
LE H0 KEPT.
inv LE.
ii.
apply KEPT.
apply NNPP.
ii.
exploit OUTSIDE;
eauto. {
split;
eauto. }
}
-
inv LESRC.
destruct (
classic (
defs sk_src id));
cycle 1.
{
exfalso.
exploit SYMBDROP;
eauto.
i;
des.
clarify. }
exploit SYMBKEEP;
eauto.
intro KEEP;
des.
rewrite KEEP in *.
exploit (
SIMSYMB2 id);
eauto.
{
inv LE.
ii.
eapply KEPT.
specialize (
OUTSIDE id).
exploit OUTSIDE;
eauto.
i;
des.
ss.
}
i;
des.
esplits;
eauto.
inv LETGT.
erewrite SYMBKEEP0;
ss.
destruct (
classic (
defs sk_tgt id));
ss.
{
exfalso.
clear -
LE KEPT H H0 SIMSK.
apply H0.
clear H0.
inv SIMSK.
u in *.
simpl_bool.
des_sumbool.
rewrite prog_defmap_spec in *.
destruct (
classic (
ss id));
cycle 1.
-
erewrite KEPT0;
ss.
-
exfalso.
apply KEPT.
ss.
}
-
inv LETGT.
destruct (
classic (
defs sk_tgt id));
cycle 1.
{
exploit SYMBDROP;
eauto.
i;
des.
clarify. }
erewrite SYMBKEEP in *;
ss.
exploit SIMSYMB3;
eauto.
i;
des.
esplits;
eauto.
inv LESRC.
erewrite SYMBKEEP0;
ss.
{
clear -
H SIMSK.
inv SIMSK.
u in *.
simpl_bool.
des_sumbool.
rewrite prog_defmap_spec in *.
des.
destruct (
classic (
ss id));
ss.
{
erewrite DROP in *;
ss. }
exploit KEPT;
eauto.
i;
des.
rewrite <-
H1.
esplits;
eauto.
}
-
eapply SSINV;
eauto.
+
inv LE.
eauto.
+
unfold skenv_src,
Genv.find_symbol in *.
ss.
rewrite PTree_filter_key_spec in BLKSRC.
des_ifs.
-
inv LESRC.
inv WFSMALLSRC.
exploit DEFSYMB;
eauto.
intro SYMBSMALL;
des.
rename SYMB into SYMBSMALL.
destruct (
classic (
defs sk_src id));
cycle 1.
{
exploit SYMBDROP;
eauto.
i;
des.
clarify. }
exploit SYMBKEEP;
eauto.
intro SYMBBIG;
des.
rewrite SYMBSMALL in *.
symmetry in SYMBBIG.
inv WFSRC.
exploit SYMBDEF;
eauto.
i;
des.
exploit SIMDEF;
eauto.
i;
des.
clarify.
exploit SPLITHINT;
eauto.
i;
des.
move DEFSRC at bottom.
move H0 at bottom.
exploit DEFKEPT;
eauto.
{
eapply Genv.find_invert_symbol;
eauto. }
i;
des.
rename H1 into KEEP.
clarify.
esplits;
eauto.
inv LETGT.
exploit SIMSYMB1;
eauto.
i;
des.
destruct (
Genv.find_def skenv_tgt blk_tgt)
eqn:
T.
{
exploit DEFKEPT0;
eauto.
{
eapply Genv.find_invert_symbol;
eauto. }
i;
des.
clarify.
inv SIMSK.
specialize (
KEPT1 id).
destruct (
classic (
ss id)).
{
exploit DROP;
et.
i;
clarify. }
exploit KEPT1;
et.
i;
clarify.
congruence.
}
exploit DEFKEEP0;
eauto.
{
eapply Genv.find_invert_symbol;
eauto. }
{
inv SIMSK.
exploit (
KEPT1 id);
eauto.
i.
unfold internals in *.
des_ifs.
}
i;
des.
clarify.
-
inv LESRC.
destruct (
classic (
defs sk_src id));
cycle 1.
{
exploit SYMBDROP;
et.
i;
des.
clarify. }
eapply DISJ;
et.
erewrite <-
SYMBKEEP;
et.
-
assert(
exists gd_big, <<
DEFBIG:
Genv.find_def skenv_link_tgt blk_tgt =
Some gd_big>>
/\ <<
LO:
linkorder def_tgt gd_big>>).
{
inv LETGT.
destruct (
Genv.invert_symbol skenv_link_tgt blk_tgt)
eqn:
T.
-
exploit DEFKEPT;
eauto.
i;
des.
ss.
esplits;
et.
-
exploit DEFORPHAN;
eauto.
i;
des.
clarify.
}
des.
exploit SIMDEFINV;
eauto.
i;
des.
clarify.
esplits;
eauto.
inv WFSMALLTGT.
exploit DEFSYMB;
eauto.
intro SYMBSMALLTGT;
des.
rename SYMB into SYMBSMALLTGT.
exploit SPLITHINT1;
eauto.
i;
des.
Fail clears blk_src.
assert(
blk_src =
blk_src0).
{
symmetry.
eapply SPLITHINT4;
et. }
clarify.
inv LESRC.
inv WFSRC.
exploit DEFSYMB;
eauto.
i;
des.
assert(
id =
id0). {
eapply Genv.genv_vars_inj.
apply SYMBSMALLTGT.
eauto. }
clarify.
assert(
DSRC:
defs sk_src id0).
{
apply NNPP.
ii.
erewrite SYMBDROP in *;
eauto.
ss. }
exploit SYMBKEEP;
eauto.
i;
des.
rewrite BLKSRC in *.
symmetry in H.
assert(
DTGT:
defs sk_tgt id0).
{
apply NNPP.
ii.
inv LETGT.
erewrite SYMBDROP0 in *;
eauto.
ss. }
assert(
ITGT:
internals sk_tgt id0).
{
dup DTGT.
unfold defs in DTGT.
des_sumbool.
apply prog_defmap_spec in DTGT.
des.
inv INCLTGT.
exploit DEFS;
et.
i;
des.
assert(
blk =
blk_tgt).
{
inv LETGT.
exploit SYMBKEEP0;
et.
i;
des.
congruence. }
clarify.
inv LETGT.
exploit DEFKEPT0;
et.
{
apply Genv.find_invert_symbol;
eauto. }
i;
des.
ss.
}
assert(
ISRC:
internals sk_src id0).
{
inv SIMSK.
unfold internals in *.
des_ifs_safe.
exploit SPLITHINT;
et.
i;
des.
clear_tac.
hexploit (
KEPT id0);
et.
intro T.
rewrite Heq in *.
des_ifs.
}
exploit DEFKEEP;
et.
{
apply Genv.find_invert_symbol;
eauto. }
i;
des.
rewrite DEFSMALL.
{
inv LETGT.
exploit DEFKEPT0;
eauto.
{
eapply Genv.find_invert_symbol;
eauto.
rewrite <-
SYMBKEEP0;
et. }
i;
des.
clarify.
inv SIMSK.
specialize (
KEPT id0).
destruct (
classic (
ss id0)).
{
exploit DROP;
et.
i;
clarify. }
exploit KEPT;
et.
i;
clarify.
congruence.
}
-
exploit PUBKEPT;
eauto.
{
eapply INCLSRC;
et. }
inv LE.
eauto.
-
inv SIMSK.
ss.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
End MEMINJ.