Module SimMemInjInv
Require
Import
Coqlib
.
Require
Import
Memory
.
Require
Import
Values
.
Require
Import
Maps
.
Require
Import
Events
.
Require
Import
Globalenvs
.
Require
Import
AST
.
Require
Import
sflib
.
Require
Import
Integers
Linking
.
Require
Import
Coq.Logic.FunctionalExtensionality
.
Require
Import
Coq.Logic.ClassicalChoice
.
Require
Import
Coq.Logic.ChoiceFacts
.
Require
Import
SimMemInj
.
Set
Implicit
Arguments
.
Record
memblk_invariant
:=
memblk_invarant_mk
{
load_values
: (
memory_chunk
->
Z
->
option
val
) ->
Prop
;
permissions
:
memory_chunk
->
Z
->
permission
->
Prop
;
}.
Section
MEMINJINV
.
Variable
P_src
:
memblk_invariant
.
Variable
P_tgt
:
memblk_invariant
.
Record
t
' :=
mk
{
minj
:>
SimMemInj.t
';
mem_inv_src
:
block
->
Prop
;
mem_inv_tgt
:
block
->
Prop
;
}.
Inductive
inv_sat_blk
(
P
:
memblk_invariant
)
blk
(
m
:
mem
):
Prop
:=
|
inv_sat_blk_intro
(
PERMISSIONS
:
forall
chunk
ofs
p
(
INVAR
:
P
.(
permissions
)
chunk
ofs
p
),
Mem.valid_access
m
chunk
blk
ofs
p
)
(
LOADVALS
:
P
.(
load_values
) (
fun
chunk
=>
Mem.load
chunk
m
blk
))
.
Definition
inv_sat_mem
(
P
:
memblk_invariant
) (
invar
:
block
->
Prop
) (
m
:
mem
) :
Prop
:=
forall
blk
(
INVAR
:
invar
blk
),
inv_sat_blk
P
blk
m
.
Inductive
wf
' (
sm0
:
t
'):
Prop
:=
|
wf_intro
(
WF
:
SimMemInj.wf
'
sm0
)
(
SATSRC
:
inv_sat_mem
P_src
sm0
.(
mem_inv_src
)
sm0
.(
src
))
(
SATTGT
:
inv_sat_mem
P_tgt
sm0
.(
mem_inv_tgt
)
sm0
.(
tgt
))
(
INVRANGESRC
:
forall
blk
ofs
(
INV
:
sm0
.(
mem_inv_src
)
blk
),
loc_unmapped
(
inj
sm0
)
blk
ofs
/\ ~
sm0
.(
src_external
)
blk
ofs
/\
Plt
blk
sm0
.(
src_parent_nb
))
(
INVRANGETGT
:
forall
blk
ofs
(
INV
:
sm0
.(
mem_inv_tgt
)
blk
),
loc_out_of_reach
(
inj
sm0
) (
src
sm0
)
blk
ofs
/\ ~
sm0
.(
tgt_external
)
blk
ofs
/\
Plt
blk
sm0
.(
tgt_parent_nb
))
.
Lemma
private_unchanged_on_invariant
P
invar
m0
m1
(
INVAR
:
inv_sat_mem
P
invar
m0
)
(
INVRANGE
:
invar
<1=
Mem.valid_block
m0
)
(
UNCH
:
Mem.unchanged_on
(
fun
blk
_
=>
invar
blk
)
m0
m1
)
:
inv_sat_mem
P
invar
m1
.
Proof.
ii
.
exploit
INVAR
;
eauto
.
intros
SAT
.
inv
SAT
.
econs
.
-
ii
.
exploit
PERMISSIONS
;
eauto
.
i
.
unfold
Mem.valid_access
in
*.
des
.
split
;
auto
.
ii
.
eapply
Mem.perm_unchanged_on
;
eauto
.
-
rpapply
LOADVALS
.
extensionality
chunk
.
extensionality
ofs
.
eapply
Mem.load_unchanged_on_1
;
eauto
.
Qed.
Inductive
le
' (
mrel0
mrel1
:
t
'):
Prop
:=
|
le_intro
(
MLE
:
SimMemInj.le
'
mrel0
mrel1
)
(
MINVEQSRC
:
mrel0
.(
mem_inv_src
) =
mrel1
.(
mem_inv_src
))
(
MINVEQTGT
:
mrel0
.(
mem_inv_tgt
) =
mrel1
.(
mem_inv_tgt
))
.
Global
Program
Instance
le
'
_PreOrder
:
RelationClasses.PreOrder
le
'.
Next Obligation.
econs
;
ss
;
eauto
.
reflexivity
.
Qed.
Next Obligation.
ii
.
inv
H
.
inv
H0
.
econs
;
eauto
.
-
etransitivity
;
eauto
.
-
etransitivity
;
eauto
.
-
etransitivity
;
eauto
.
Qed.
Lemma
le_inj_wf_wf
minj_old
minj_new
inv_src
inv_tgt
(
MLE
:
SimMemInj.le
'
minj_old
minj_new
)
(
WF
:
wf
' (
mk
minj_old
inv_src
inv_tgt
))
(
MWF
:
SimMemInj.wf
'
minj_new
)
(
SATSRC
:
inv_sat_mem
P_src
inv_src
minj_new
.(
src
))
(
SATTGT
:
inv_sat_mem
P_tgt
inv_tgt
minj_new
.(
tgt
))
:
wf
' (
mk
minj_new
inv_src
inv_tgt
)
.
Proof.
inv
WF
.
inv
WF0
.
econs
;
ss
;
eauto
.
-
ii
.
inv
MLE
.
exploit
INVRANGESRC
;
eauto
.
rewrite
SRCPARENTEQ
.
rewrite
SRCPARENTEQNB
in
*.
i
.
des
.
splits
;
eauto
.
destruct
(
inj
minj_new
blk
)
eqn
:
BLK
;
auto
.
destruct
p
.
inv
FROZEN
.
exploit
NEW_IMPLIES_OUTSIDE
;
eauto
.
i
.
des
.
exfalso
.
eapply
(
Plt_strict
blk
).
eapply
Plt_Ple_trans
;
eauto
.
-
ii
.
inv
MLE
.
exploit
INVRANGETGT
;
eauto
.
rewrite
TGTPARENTEQ
.
rewrite
TGTPARENTEQNB
in
*.
i
.
des
.
splits
;
eauto
.
ii
.
destruct
(
inj
minj_old
b0
)
eqn
:
BLK
;
auto
.
+
destruct
p
.
dup
BLK
.
eapply
INCR
in
BLK
.
clarify
.
exploit
H
;
eauto
.
eapply
MAXSRC
;
eauto
.
eapply
Mem.valid_block_inject_1
;
eauto
.
+
inv
FROZEN
.
exploit
NEW_IMPLIES_OUTSIDE
;
eauto
.
i
.
des
.
eapply
(
Plt_strict
blk
);
eauto
.
eapply
Plt_Ple_trans
;
eauto
.
Qed.
End
MEMINJINV
.
Definition
top_inv
:
memblk_invariant
:=
memblk_invarant_mk
(
fun
_
=>
True
) (
fun
_
_
_
=>
False
).
Lemma
top_inv_satisfied_always
m
minv
:
inv_sat_mem
top_inv
minv
m
.
Proof.
econs
;
ss
. Qed.
Hint
Resolve
top_inv_satisfied_always
.
Record
mcompat
(
sm0
:
t
') (
m_src0
m_tgt0
:
mem
) (
F
:
meminj
):
Prop
:=
mkmcompat
{
mcompat_src
:
sm0
.(
src
) =
m_src0
;
mcompat_tgt
:
sm0
.(
tgt
) =
m_tgt0
;
mcompat_inj
:
sm0
.(
inj
) =
F
;
}.
Ltac
compat_tac
:=
ss
;
econs
;
eauto
;
try
congruence
.
Ltac
spl
:=
esplits
; [|
reflexivity
].
Ltac
spl_approx
sm
:=
eexists
(
mk
(
SimMemInj.mk
_
_
_
sm
.(
src_external
)
sm
.(
tgt_external
)
sm
.(
src_parent_nb
)
sm
.(
tgt_parent_nb
))
sm
.(
mem_inv_src
)
sm
.(
mem_inv_tgt
));
splits
;
eauto
.
Ltac
spl_approx2
sm
:=
eexists
(
mk
_
sm
.(
mem_inv_src
)
sm
.(
mem_inv_tgt
));
splits
;
eauto
.
Ltac
spl_exact
sm
:=
exists
sm
;
splits
; [|
try
etransitivity
;
eauto
;
try
reflexivity
;
eauto
].
Ltac
spl_exact2
sm
:=
eexists
(
mk
sm
_
_
);
splits
; [|
try
etransitivity
;
eauto
;
try
reflexivity
;
eauto
].