Module IdSimClight
Require
Import
Sem
SimProg
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
Sound
SimSymb
.
Require
Import
Cop
Ctypes
ClightC
.
Require
SimMemId
SimMemExt
SimMemInj
.
Require
SoundTop
UnreachC
.
Require
SimSymbId
SimSymbDrop
.
Require
Import
CoqlibC
.
Require
Import
ValuesC
.
Require
Import
LinkingC
.
Require
Import
MapsC
.
Require
Import
AxiomsC
.
Require
Import
Ord
.
Require
Import
MemoryC
.
Require
Import
SmallstepC
.
Require
Import
Events
.
Require
Import
Preservation
.
Require
Import
Integers
.
Require
Import
LocationsC
Conventions
.
Require
Import
MatchSimModSem
.
Require
Import
ClightStepInj
ClightStepExt
.
Require
Import
IdSimExtra
IdSimClightExtra
.
Require
Import
CtypingC
.
Require
Import
CopC
.
Set
Implicit
Arguments
.
Local
Opaque
Z.mul
Z.add
Z.sub
Z.div
.
Lemma
clight_id
(
clight
:
Clight.program
)
(
WF
:
Sk.wf
clight
.(
module2
)):
exists
mp
,
(<<
SIM
: @
ModPair.sim
SimMemId.SimMemId
SimMemId.SimSymbId
SoundTop.Top
mp
>>)
/\ (<<
SRC
:
mp
.(
ModPair.src
) =
clight
.(
module2
)>>)
/\ (<<
TGT
:
mp
.(
ModPair.tgt
) =
clight
.(
module2
)>>).
Proof.
eapply
any_id
;
eauto
.
Qed.
Lemma
clight_ext_unreach
(
clight
:
Clight.program
)
(
WF
:
Sk.wf
clight
.(
module2
)):
exists
mp
,
(<<
SIM
: @
ModPair.sim
SimMemExt.SimMemExt
SimMemExt.SimSymbExtends
UnreachC.Unreach
mp
>>)
/\ (<<
SRC
:
mp
.(
ModPair.src
) =
clight
.(
module2
)>>)
/\ (<<
TGT
:
mp
.(
ModPair.tgt
) =
clight
.(
module2
)>>).
Proof.
eexists
(
ModPair.mk
_
_
_
);
s
.
esplits
;
eauto
.
instantiate
(1:=
tt
).
econs
;
ss
;
i
.
destruct
SIMSKENVLINK
.
exploit
clight_unreach_local_preservation
.
i
.
des
.
eapply
match_states_sim
with
(
match_states
:=
match_states_ext_clight
);
ss
;
eauto
.
-
apply
unit_ord_wf
.
-
i
.
ss
.
inv
INITTGT
.
inv
SAFESRC
.
inv
H
.
inv
SIMARGS
;
ss
.
assert
(
FD
:
fd
=
fd0
).
{
inv
FPTR
;
ss
.
rewrite
FINDF
in
FINDF0
.
clarify
. }
esplits
;
eauto
.
+
econs
;
eauto
.
+
ss
.
subst
.
econs
2;
eauto
.
*
inv
TYP
.
inv
TYP0
.
eapply
lessdef_list_typify_list
;
et
.
*
econs
;
et
.
-
i
.
ss
.
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
esplits
.
econs
;
ss
.
+
inv
FPTR
;
ss
.
eauto
.
+
inv
TYP
.
econs
;
ss
;
eauto
.
erewrite
<-
lessdef_list_length
;
eauto
.
-
i
.
ss
.
inv
MATCH
;
eauto
.
-
i
.
ss
.
clear
SOUND
.
inv
CALLSRC
.
inv
MATCH
.
ss
.
esplits
;
eauto
.
+
des
.
inv
INJ
;
ss
;
clarify
.
econs
;
ss
;
eauto
.
+
econs
;
ss
.
+
instantiate
(1:=
top4
).
ss
.
-
i
.
ss
.
clear
SOUND
HISTORY
.
exists
sm_ret
.
inv
AFTERSRC
.
inv
MATCH
.
esplits
;
eauto
.
+
econs
;
eauto
.
inv
SIMRET
;
ss
.
+
inv
SIMRET
;
ss
.
econs
;
eauto
.
eapply
lessdef_typify
;
eauto
.
-
i
.
ss
.
inv
FINALSRC
.
inv
MATCH
.
inv
CONT
.
esplits
;
eauto
;
econs
;
eauto
.
-
left
.
i
.
split
.
{
eapply
modsem2_receptive
. }
ii
.
exploit
clight_step_preserve_extension
;
eauto
.
{
eapply
function_entry2_extends
. }
i
.
des
.
esplits
;
eauto
.
left
.
apply
plus_one
.
econs
;
ss
;
eauto
.
eapply
modsem2_determinate
.
Qed.
Lemma
clight_ext_top
(
clight
:
Clight.program
)
(
WF
:
Sk.wf
clight
.(
module2
)):
exists
mp
,
(<<
SIM
: @
ModPair.sim
SimMemExt.SimMemExt
SimMemExt.SimSymbExtends
SoundTop.Top
mp
>>)
/\ (<<
SRC
:
mp
.(
ModPair.src
) =
clight
.(
module2
)>>)
/\ (<<
TGT
:
mp
.(
ModPair.tgt
) =
clight
.(
module2
)>>).
Proof.
eexists
(
ModPair.mk
_
_
_
);
s
.
esplits
;
eauto
.
instantiate
(1:=
tt
).
econs
;
ss
;
i
.
destruct
SIMSKENVLINK
.
eapply
match_states_sim
with
(
match_states
:=
match_states_ext_clight
);
ss
.
-
apply
unit_ord_wf
.
-
eapply
SoundTop.sound_state_local_preservation
.
-
i
.
ss
.
inv
INITTGT
.
inv
SAFESRC
.
inv
H
.
inv
SIMARGS
;
ss
.
assert
(
FD
:
fd
=
fd0
).
{
inv
FPTR
;
ss
.
rewrite
FINDF
in
FINDF0
.
clarify
. }
esplits
;
eauto
.
+
econs
;
eauto
.
+
ss
.
subst
.
econs
;
eauto
.
*
inv
TYP
.
inv
TYP0
.
eapply
lessdef_list_typify_list
;
eauto
.
*
econs
;
eauto
.
-
i
.
ss
.
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
esplits
.
econs
;
ss
.
+
inv
FPTR
;
ss
.
eauto
.
+
inv
TYP
.
econs
;
ss
;
eauto
.
erewrite
<-
lessdef_list_length
;
eauto
.
-
i
.
ss
.
inv
MATCH
;
eauto
.
-
i
.
ss
.
clear
SOUND
.
inv
CALLSRC
.
inv
MATCH
.
ss
.
esplits
;
eauto
.
+
des
.
inv
INJ
;
ss
;
clarify
.
econs
;
ss
;
eauto
.
+
econs
;
ss
.
+
instantiate
(1:=
top4
).
ss
.
-
i
.
ss
.
clear
SOUND
HISTORY
.
exists
sm_ret
.
inv
AFTERSRC
.
inv
MATCH
.
esplits
;
eauto
.
+
econs
;
eauto
.
inv
SIMRET
;
ss
.
+
inv
SIMRET
;
ss
.
econs
;
eauto
.
eapply
lessdef_typify
;
eauto
.
-
i
.
ss
.
inv
FINALSRC
.
inv
MATCH
.
inv
CONT
.
esplits
;
eauto
;
econs
;
eauto
.
-
left
.
i
.
split
.
{
eapply
modsem2_receptive
. }
ii
.
exploit
clight_step_preserve_extension
;
eauto
.
{
eapply
function_entry2_extends
. }
i
.
des
.
esplits
;
eauto
.
left
.
apply
plus_one
.
econs
;
ss
;
eauto
.
eapply
modsem2_determinate
.
Qed.
Lemma
clight_inj_drop_bot
(
clight
:
Clight.program
)
(
WF
:
Sk.wf
clight
.(
module2
)):
exists
mp
,
(<<
SIM
: @
ModPair.sim
SimMemInjC.SimMemInj
SimSymbDrop.SimSymbDrop
SoundTop.Top
mp
>>)
/\ (<<
SRC
:
mp
.(
ModPair.src
) =
clight
.(
module2
)>>)
/\ (<<
TGT
:
mp
.(
ModPair.tgt
) =
clight
.(
module2
)>>)
/\ (<<
SSBOT
:
mp
.(
ModPair.ss
) =
bot1
>>).
Proof.
eexists
(
ModPair.mk
_
_
_
);
s
.
esplits
;
eauto
.
econs
;
ss
;
i
.
{
econs
;
ss
;
i
;
clarify
.
inv
WF
.
auto
. }
eapply
match_states_sim
with
(
match_states
:=
match_states_clight
);
ss
.
-
apply
unit_ord_wf
.
-
eapply
SoundTop.sound_state_local_preservation
.
-
i
.
ss
.
exploit
SimSymbDrop_match_globals
.
{
inv
SIMSKENV
.
ss
.
eauto
. }
intros
GEMATCH
.
inv
INITTGT
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
inv
H
.
ss
.
exploit
match_globals_find_funct
;
eauto
.
i
.
clarify
.
esplits
;
eauto
;
try
refl
;
econs
;
eauto
.
+
econs
;
eauto
;
try
econs
.
inv
TYP
.
inv
TYP0
.
eapply
inject_list_typify_list
;
eauto
.
-
i
.
ss
.
exploit
SimSymbDrop_match_globals
.
{
inv
SIMSKENV
.
ss
.
eauto
. }
intros
GEMATCH
.
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
esplits
.
econs
;
ss
.
+
eapply
match_globals_find_funct
;
eauto
.
+
inv
TYP
.
econs
;
eauto
.
erewrite
<-
inject_list_length
;
eauto
.
-
i
.
ss
.
inv
MATCH
;
eauto
.
-
i
.
ss
.
clear
SOUND
.
inv
CALLSRC
.
inv
MATCH
.
inv
MATCHST
.
inv
SIMSKENV
.
ss
.
esplits
;
eauto
;
try
refl
.
+
econs
;
ss
;
eauto
.
*
eapply
SimSymbDrop_find_None
;
eauto
.
ii
.
clarify
.
ss
.
des
.
clarify
.
*
des
.
clear
EXTERNAL
.
unfold
Genv.find_funct
,
Genv.find_funct_ptr
in
*.
des_ifs_safe
.
inv
INJ
.
inv
SIMSKELINK
.
exploit
SIMDEF
;
eauto
.
i
.
des
.
clarify
.
des_ifs
.
esplits
;
eauto
.
+
econs
;
ss
.
+
instantiate
(1:=
top4
).
ss
.
-
i
.
ss
.
clear
SOUND
HISTORY
.
exists
(
SimMemInj.unlift
'
sm_arg
sm_ret
).
inv
AFTERSRC
.
inv
MATCH
.
inv
MATCHST
.
esplits
;
eauto
.
+
econs
;
eauto
.
inv
SIMRET
;
ss
.
+
inv
SIMRET
;
ss
.
econs
;
eauto
.
econs
;
eauto
.
{
eapply
inject_typify
;
et
. }
ss
.
eapply
match_cont_incr
;
try
eassumption
.
inv
MLE
.
inv
MLE0
.
etrans
;
eauto
.
+
refl
.
-
i
.
ss
.
inv
FINALSRC
.
inv
MATCH
.
inv
MATCHST
.
inv
CONT
.
esplits
;
eauto
;
try
refl
;
econs
;
eauto
.
-
left
.
i
.
split
.
+
eapply
modsem2_receptive
.
+
ii
.
exploit
clight_step_preserve_injection
;
try
eassumption
.
{
instantiate
(1:=
cgenv
skenv_link_tgt
clight
).
ss
. }
{
eapply
function_entry2_inject
.
ss
. }
{
inv
SIMSKENV
.
ss
.
eapply
SimSymbDrop_symbols_inject
;
eauto
. }
{
inv
SIMSKENV
.
ss
.
eapply
SimSymbDrop_match_globals
;
eauto
. }
i
.
des
.
esplits
;
eauto
.
left
.
apply
plus_one
.
econs
;
ss
;
eauto
.
eapply
modsem2_determinate
.
Qed.
Lemma
clight_inj_drop
(
clight
:
Clight.program
)
(
WF
:
Sk.wf
clight
.(
module2
)):
exists
mp
,
(<<
SIM
: @
ModPair.sim
SimMemInjC.SimMemInj
SimSymbDrop.SimSymbDrop
SoundTop.Top
mp
>>)
/\ (<<
SRC
:
mp
.(
ModPair.src
) =
clight
.(
module2
)>>)
/\ (<<
TGT
:
mp
.(
ModPair.tgt
) =
clight
.(
module2
)>>).
Proof.
exploit
clight_inj_drop_bot
;
eauto
.
i
.
des
.
eauto
.
Qed.
Lemma
clight_inj_id
(
clight
:
Clight.program
)
(
WF
:
Sk.wf
clight
.(
module2
)):
exists
mp
,
(<<
SIM
: @
ModPair.sim
SimMemInjC.SimMemInj
SimMemInjC.SimSymbId
SoundTop.Top
mp
>>)
/\ (<<
SRC
:
mp
.(
ModPair.src
) =
clight
.(
module2
)>>)
/\ (<<
TGT
:
mp
.(
ModPair.tgt
) =
clight
.(
module2
)>>).
Proof.
apply
sim_inj_drop_bot_id
.
apply
clight_inj_drop_bot
;
auto
.
Qed.