Require Import CoqlibC.
Require Import MemoryC.
Require Import Values.
Require Import Maps.
Require Import Events.
Require Import Globalenvs.
Require Import AST.
Require Import IntegersC LinkingC.
Require Import SimSymb Skeleton Mod ModSem.
Require Import SimMem SimMemLift.
Require SimSymbId.
Require Export SimMemInjInv.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.ClassicalChoice.
Require Import Coq.Logic.ChoiceFacts.
Set Implicit Arguments.
Section MEMINJINV.
Variable P_src :
memblk_invariant.
Variable P_tgt :
memblk_invariant.
Inductive lepriv (
sm0 sm1:
t'):
Prop :=
|
lepriv_intro
(
INCR:
inject_incr sm0.(
SimMemInj.inj)
sm1.(
SimMemInj.inj))
(
SRCGENB:
sm0.(
SimMemInj.src_ge_nb) =
sm1.(
SimMemInj.src_ge_nb))
(
TGTGENB:
sm0.(
SimMemInj.tgt_ge_nb) =
sm1.(
SimMemInj.tgt_ge_nb))
(
FROZEN:
SimMemInj.frozen sm0.(
SimMemInj.inj)
sm1.(
SimMemInj.inj) (
sm0.(
SimMemInj.src_ge_nb)) (
sm0.(
SimMemInj.tgt_ge_nb)))
(
INVSRC:
sm0.(
mem_inv_src) =
sm1.(
mem_inv_src))
(
INVTGT:
sm0.(
mem_inv_tgt) =
sm1.(
mem_inv_tgt))
.
Global Program Instance SimMemInjInv :
SimMem.class :=
{
t :=
t';
src :=
SimMemInj.src;
tgt :=
SimMemInj.tgt;
wf :=
wf'
P_src P_tgt;
le :=
le';
lepriv :=
lepriv;
sim_val :=
fun (
mrel:
t') =>
Val.inject mrel.(
SimMemInj.inj);
sim_val_list :=
fun (
mrel:
t') =>
Val.inject_list mrel.(
SimMemInj.inj);
}.
Next Obligation.
inv H. inv MLE. econs; eauto.
Qed.
Next Obligation.
inv MLE. inv MLE0. eauto.
Qed.
Next Obligation.
extensionality l0.
extensionality l1.
eapply prop_ext2.
induction x0;
ss;
i;
split;
intros H;
inv H;
econs;
eauto.
-
eapply IHx0;
eauto.
-
eapply IHx0;
eauto.
Qed.
Next Obligation.
inv H. ss.
Qed.
Lemma unchanged_on_mle (
sm0:
t')
m_src1 m_tgt1 j1
(
WF:
SimMemInjInv.wf'
P_src P_tgt sm0)
(
INJECT:
Mem.inject j1 m_src1 m_tgt1)
(
INCR:
inject_incr sm0.(
SimMemInj.inj)
j1)
(
SEP:
inject_separated sm0.(
SimMemInj.inj)
j1 sm0.(
SimMemInj.src)
sm0.(
SimMemInj.tgt))
(
UNCHSRC:
Mem.unchanged_on
(
loc_unmapped sm0.(
SimMemInj.inj))
sm0.(
SimMemInj.src)
m_src1)
(
UNCHTGT:
Mem.unchanged_on
(
loc_out_of_reach sm0.(
SimMemInj.inj)
sm0.(
SimMemInj.src))
sm0.(
SimMemInj.tgt)
m_tgt1)
(
MAXSRC:
forall
b ofs
(
VALID:
Mem.valid_block sm0.(
SimMemInj.src)
b)
,
<<
MAX:
Mem.perm m_src1 b ofs Max <1=
Mem.perm sm0.(
SimMemInj.src)
b ofs Max>>)
(
MAXTGT:
forall
b ofs
(
VALID:
Mem.valid_block sm0.(
SimMemInj.tgt)
b)
,
<<
MAX:
Mem.perm m_tgt1 b ofs Max <1=
Mem.perm sm0.(
SimMemInj.tgt)
b ofs Max>>)
:
(<<
MLE:
SimMemInjInv.le'
sm0 (
mk (
SimMemInj.mk
m_src1 m_tgt1 j1
(
SimMemInj.src_external sm0)
(
SimMemInj.tgt_external sm0)
(
SimMemInj.src_parent_nb sm0)
(
SimMemInj.tgt_parent_nb sm0)
(
SimMemInj.src_ge_nb sm0)
(
SimMemInj.tgt_ge_nb sm0))
sm0.(
mem_inv_src)
sm0.(
mem_inv_tgt))>>) /\
(<<
MWF:
SimMemInjInv.wf'
P_src P_tgt
(
mk (
SimMemInj.mk
m_src1 m_tgt1 j1
(
SimMemInj.src_external sm0)
(
SimMemInj.tgt_external sm0)
(
SimMemInj.src_parent_nb sm0)
(
SimMemInj.tgt_parent_nb sm0)
(
SimMemInj.src_ge_nb sm0)
(
SimMemInj.tgt_ge_nb sm0))
sm0.(
mem_inv_src)
sm0.(
mem_inv_tgt))>>).
Proof.
Definition lift' (
mrel0:
t'):
t' :=
mk (
SimMemInj.mk
(
SimMemInj.src mrel0)
(
SimMemInj.tgt mrel0)
(
SimMemInj.inj mrel0)
(
SimMemInj.src_private mrel0 /2\
fun blk _ => ~
mrel0.(
mem_inv_src)
blk)
(
SimMemInj.tgt_private mrel0 /2\
fun blk _ => ~
mrel0.(
mem_inv_tgt)
blk)
((
SimMemInj.src mrel0).(
Mem.nextblock))
((
SimMemInj.tgt mrel0).(
Mem.nextblock))
((
SimMemInj.src_ge_nb mrel0))
((
SimMemInj.tgt_ge_nb mrel0)))
(
mem_inv_src mrel0)
(
mem_inv_tgt mrel0)
.
Definition unlift' (
mrel0 mrel1:
t'):
t' :=
mk (
SimMemInj.mk
(
SimMemInj.src mrel1)
(
SimMemInj.tgt mrel1)
(
SimMemInj.inj mrel1)
(
SimMemInj.src_external mrel0)
(
SimMemInj.tgt_external mrel0)
(
SimMemInj.src_parent_nb mrel0)
(
SimMemInj.tgt_parent_nb mrel0)
(
SimMemInj.src_ge_nb mrel0)
(
SimMemInj.tgt_ge_nb mrel0)) (
mem_inv_src mrel0) (
mem_inv_tgt mrel0).
Lemma unlift_spec :
forall mrel0 mrel1 :
t',
le' (
lift'
mrel0)
mrel1 ->
wf'
P_src P_tgt mrel0 ->
le'
mrel0 (
unlift'
mrel0 mrel1).
Proof.
Lemma lift_wf :
forall mrel0 :
t',
wf'
P_src P_tgt mrel0 ->
wf'
P_src P_tgt (
lift'
mrel0).
Proof.
i.
inv H.
inv WF.
econs;
ss;
eauto.
-
econs;
ss;
eauto.
+
ii.
des.
destruct PR.
split;
ss.
+
ii.
des.
destruct PR.
split;
ss.
+
reflexivity.
+
reflexivity.
+
xomega.
+
xomega.
-
ii.
exploit INVRANGESRC;
eauto.
i.
des.
splits;
eauto.
+
ii.
des.
clarify.
+
eapply Plt_Ple_trans;
eauto.
-
ii.
exploit INVRANGETGT;
eauto.
i.
des.
splits;
eauto.
+
ii.
des.
clarify.
+
eapply Plt_Ple_trans;
eauto.
Qed.
Lemma unlift_wf :
forall mrel0 mrel1 :
t',
wf'
P_src P_tgt mrel0 ->
wf'
P_src P_tgt mrel1 ->
le' (
lift'
mrel0)
mrel1 ->
wf'
P_src P_tgt (
unlift'
mrel0 mrel1).
Proof.
i.
inv H.
inv H0.
inv H1.
inv WF.
inv WF0.
inv MLE.
econs;
ss;
eauto.
-
econs;
ss;
try etransitivity;
eauto.
+
ii.
destruct (
classic (
mem_inv_src mrel0 x0)).
*
rewrite MINVEQSRC in *.
exploit INVRANGESRC0;
eauto.
i.
des.
split;
eauto.
ss.
destruct PR.
eapply Mem.valid_block_unchanged_on;
eauto.
*
eapply SRCEXT0.
rewrite <-
SRCPARENTEQ.
auto.
+
ii.
destruct (
classic (
mem_inv_tgt mrel0 x0)).
*
rewrite MINVEQTGT in *.
exploit INVRANGETGT0;
eauto.
i.
des.
split;
eauto.
ss.
destruct PR.
eapply Mem.valid_block_unchanged_on;
eauto.
*
eapply TGTEXT0.
rewrite <-
TGTPARENTEQ.
auto.
+
inv SRCUNCHANGED;
ss.
+
inv TGTUNCHANGED;
ss.
-
rewrite MINVEQSRC.
eauto.
-
rewrite MINVEQTGT.
eauto.
-
ii.
split.
+
eapply INVRANGESRC0.
rewrite <-
MINVEQSRC.
auto.
+
eapply INVRANGESRC;
eauto.
-
ii.
split.
+
eapply INVRANGETGT0.
rewrite <-
MINVEQTGT.
auto.
+
eapply INVRANGETGT;
eauto.
Qed.
Global Program Instance lepriv_PreOrder:
RelationClasses.PreOrder lepriv.
Next Obligation.
Next Obligation.
ii.
inv H;
inv H0.
des;
clarify.
econs;
eauto with mem congruence.
+
eapply inject_incr_trans;
eauto.
+
econs;
eauto.
ii;
des.
destruct (
SimMemInj.inj y b_src)
eqn:
T.
*
destruct p.
exploit INCR0;
eauto.
i;
clarify.
inv FROZEN.
hexploit NEW_IMPLIES_OUTSIDE;
eauto.
*
inv FROZEN0.
hexploit NEW_IMPLIES_OUTSIDE;
eauto; [];
i;
des.
esplits;
congruence.
Qed.
Global Program Instance SimMemInjInvLift :
SimMemLift.class SimMemInjInv :=
{
lift :=
lift';
unlift :=
unlift';
}.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
inv MWF.
inv MLE.
inv MLE0.
inv MLIFT.
econs;
ss;
et;
try congruence.
-
eapply SimMemInj.frozen_refl.
Qed.
End MEMINJINV.
Definition ref_init (
il :
list init_data) (
id :
ident):
Prop :=
exists ofs,
In (
Init_addrof id ofs)
il
.
Section SIMSYMBINV.
Variable P :
memblk_invariant.
Inductive le (
ss0:
ident ->
Prop) (
sk_src sk_tgt:
Sk.t) (
ss1:
ident ->
Prop):
Prop :=
|
symb_le_intro
(
LE:
ss0 <1=
ss1)
(
OUTSIDE:
forall
id
(
IN: (
ss1 -1
ss0)
id)
,
<<
OUTSIDESRC: ~
sk_src.(
defs)
id>> /\ <<
OUTSIDETGT: ~
sk_tgt.(
defs)
id>>)
.
Inductive invariant_globvar F V:
globdef F V ->
Prop :=
|
invariant_globvar_intro
v
(
NVOL:
v.(
gvar_volatile) =
false)
(
WRITABLE:
v.(
gvar_readonly) =
false)
(
INITD:
forall
(
ge:
Genv.t F V)
m b
(
INIT:
Genv.load_store_init_data ge m b 0 (
gvar_init v))
(
PERM:
Mem.range_perm
m b 0 (
init_data_list_size (
gvar_init v))
Cur
(
Genv.perm_globvar v))
,
inv_sat_blk P b m)
:
invariant_globvar (
Gvar v)
.
Inductive sim_sk (
ss:
ident ->
Prop) (
sk_src sk_tgt:
Sk.t):
Prop :=
|
sim_sk_intro
(
SKSAME:
sk_src =
sk_tgt)
(
CLOSED:
forall id (
SS:
ss id),
exists g,
(<<
DEF:
sk_tgt.(
prog_defmap) !
id =
Some g>>) /\
(<<
INV:
invariant_globvar g>>) /\
(<<
PRVT: ~
In id (
prog_public sk_tgt)>>))
(
NOMAIN: ~
ss sk_src.(
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>>)
.
Inductive skenv_inject {
F V} (
ge:
Genv.t F V) (
j:
meminj)
(
invar:
block ->
Prop) :
Prop :=
|
sken_inject_intro
(
DOMAIN:
forall b i (
SYMB:
Genv.find_symbol ge i =
Some b),
Plt b ge.(
Genv.genv_next) ->
forall (
NINV: ~
invar b),
j b =
Some(
b, 0))
(
NDOMAIN:
forall b i (
SYMB:
Genv.find_symbol ge i =
Some b),
Plt b ge.(
Genv.genv_next) ->
forall (
NINV:
invar b),
j b =
None)
(
IMAGE:
forall b1 b2 delta,
j b1 =
Some(
b2,
delta) ->
(
Plt b1 ge.(
Genv.genv_next) \/
Plt b2 ge.(
Genv.genv_next)) ->
(<<
BLK:
b1 =
b2>> /\ <<
DELTA:
delta = 0>>))
.
Inductive sim_skenv_inj (
sm:
t') (
ss:
ident ->
Prop) (
skenv_src skenv_tgt:
SkEnv.t):
Prop :=
|
sim_skenv_inj_intro
(
INVCOMPAT:
forall id blk (
FIND:
skenv_tgt.(
Genv.find_symbol)
id =
Some blk),
ss id <->
sm.(
mem_inv_tgt)
blk)
(
PUBKEPT: (
fun id =>
In id skenv_src.(
Genv.genv_public)) <1= ~1
ss)
(
INJECT:
skenv_inject skenv_src sm.(
SimMemInj.inj)
sm.(
mem_inv_tgt))
(
SIMSKENV:
SimSymbId.sim_skenv skenv_src skenv_tgt)
(
NBSRC:
skenv_src.(
Genv.genv_next) =
sm.(
SimMemInj.src_ge_nb))
(
NBTGT:
skenv_tgt.(
Genv.genv_next) =
sm.(
SimMemInj.tgt_ge_nb))
.
Lemma skenv_inject_symbols_inject sm ss skenv_src skenv_tgt
(
SKENVINJ:
sim_skenv_inj sm ss skenv_src skenv_tgt)
:
symbols_inject sm.(
SimMemInj.inj)
skenv_src skenv_tgt.
Proof.
Lemma SimSymbIdInv_skenv_func_bisim sm ss skenv_src skenv_tgt
(
SIMSKENV:
sim_skenv_inj sm ss skenv_src skenv_tgt)
:
SimSymb.skenv_func_bisim (
Val.inject (
SimMemInj.inj sm))
skenv_src skenv_tgt.
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 init_mem_inject ss sk sk_tgt j m
(
SIMSK:
sim_sk ss sk sk_tgt)
(
LOADMEM:
Genv.init_mem sk =
Some m)
(
SS:
forall id, {
ss id} + {~
ss id})
(
J:
j =
fun blk :
positive =>
if plt blk (
Mem.nextblock m)
then
match Genv.invert_symbol (
Genv.globalenv sk)
blk with
|
Some id =>
if SS id then None else Some (
blk, 0)
|
None =>
None
end
else None)
:
Mem.inject j m m.
Proof.
Lemma sim_skenv_inj_lepriv ss sm0 sm1 skenv_src skenv_tgt
(
MLE:
lepriv sm0 sm1)
(
SIMSKENV :
sim_skenv_inj sm0 ss skenv_src skenv_tgt)
:
sim_skenv_inj sm1 ss skenv_src skenv_tgt.
Proof.
inv MLE.
inv SIMSKENV.
destruct sm0,
sm1.
destruct minj.
destruct minj0.
ss.
clarify.
rename inj0 into inj1.
rename inj into inj0.
econs;
ss;
eauto.
-
inv INJECT.
econs;
ss;
eauto.
+
i.
destruct (
inj1 b)
as [[
b0 delta]|]
eqn:
BLK;
auto.
exfalso.
inv FROZEN.
hexploit NEW_IMPLIES_OUTSIDE;
eauto.
i.
des.
eapply (
Plt_strict b).
eapply Plt_Ple_trans;
eauto.
+
i.
destruct (
inj0 b1)
as [[
b0 delta0]|]
eqn:
BLK;
auto.
*
dup BLK.
eapply INCR in BLK.
clarify.
eapply IMAGE;
eauto.
*
inv FROZEN.
exploit NEW_IMPLIES_OUTSIDE;
eauto.
i.
des.
{
exfalso.
eapply (
Plt_strict b1).
eapply Plt_Ple_trans;
eauto. }
{
inv SIMSKENV0.
exfalso.
eapply (
Plt_strict b2).
eapply Plt_Ple_trans;
eauto. }
Qed.
Global Program Instance SimSymbIdInv:
SimSymb.class (
SimMemInjInv top_inv P) :=
{
t :=
ident ->
Prop;
le :=
le;
sim_sk :=
sim_sk;
sim_skenv :=
sim_skenv_inj;
}
.
Next Obligation.
econs; eauto. i. des. clarify.
Qed.
Next Obligation.
inv LE0.
inv LE1.
econs;
eauto.
i.
des.
destruct (
classic (
ss1 id)).
-
exploit OUTSIDE;
eauto.
-
exploit OUTSIDE0;
eauto.
i.
des.
inv LINKORD0.
inv LINKORD1.
des.
split;
eauto.
+
ii.
eapply OUTSIDESRC.
eapply defs_prog_defmap in H6.
des.
eapply defs_prog_defmap.
exploit H5;
eauto.
i.
des.
eauto.
+
ii.
eapply OUTSIDETGT.
eapply defs_prog_defmap in H6.
des.
eapply defs_prog_defmap.
exploit H4;
eauto.
i.
des.
eauto.
Qed.
Next Obligation.
inv SIMSK. eauto.
Qed.
Next Obligation.
Next Obligation.
inv SIMSKE. inv SIMSKENV. eauto.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
inv LE.
inv SIMSKENV.
econs;
ss;
eauto.
-
i.
assert (
Genv.find_symbol skenv_link_tgt id =
Some blk).
{
exploit SkEnv.project_impl_spec.
{
eapply INCLTGT. }
i.
inv H.
ss.
erewrite <-
SYMBKEEP;
eauto.
apply NNPP.
ii.
exploit SYMBDROP;
eauto.
i.
red in H0.
clarify. }
exploit INVCOMPAT;
eauto.
i.
des.
split;
eauto;
i.
apply NNPP.
intros n.
exploit OUTSIDE;
eauto.
i.
des.
apply OUTSIDETGT.
unfold SkEnv.project in FIND.
erewrite Genv_map_defs_symb in FIND.
ss.
unfold Genv.find_symbol in FIND.
ss.
rewrite MapsC.PTree_filter_key_spec in FIND.
des_ifs.
-
ii.
eapply PUBKEPT;
eauto.
inv INCLSRC.
eauto.
-
inv INJECT.
clear INCLTGT.
exploit SkEnv.project_impl_spec;
eauto.
i.
inv H.
econs;
ss;
eauto.
+
i.
eapply DOMAIN;
eauto.
instantiate (1:=
i).
destruct (
classic (
defs sk_src i)).
*
rewrite <-
SYMBKEEP;
eauto.
*
rewrite SYMBDROP in SYMB;
eauto.
clarify.
+
i.
eapply NDOMAIN;
eauto.
instantiate (1:=
i).
destruct (
classic (
defs sk_src i)).
*
rewrite <-
SYMBKEEP;
eauto.
*
rewrite SYMBDROP in SYMB;
eauto.
clarify.
-
inv SIMSKENV0.
inv SIMSK.
ss.
Qed.
Next Obligation.
Next Obligation.
inv SIMSKENV. econs; eauto.
- inv INJECT. econs; eauto.
- inv SIMSKENV0. ss.
Qed.
Next Obligation.
End SIMSYMBINV.