Module CminorgenproofC
Require
Import
Coq.Program.Equality
FSets
Permutation
.
Require
Import
FSets
FSetAVL
Orders
Mergesort
.
Require
Import
CoqlibC
Maps
Ordered
Errors
IntegersC
Floats
.
Require
Intv
.
Require
Import
AST
Linking
.
Require
Import
ValuesC
Memory
Events
GlobalenvsC
Smallstep
.
Require
Import
CsharpminorC
Switch
CminorC
Cminorgen
.
Require
Import
sflib
.
Require
SimMemInj
.
newly added *
Require
Export
Cminorgenproof
.
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
AsmregsC
MatchSimModSem
.
Require
SimMemInjC
.
Require
SoundTop
.
Require
Import
CtypingC
.
Require
Import
ModSemProps
.
Set
Implicit
Arguments
.
Section
SIMMODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variable
prog
:
Csharpminor.program
.
Variable
tprog
:
Cminor.program
.
Let
md_src
:
Mod.t
:= (
CsharpminorC.module
prog
).
Let
md_tgt
:
Mod.t
:= (
CminorC.module
tprog
).
Hypothesis
(
INCLSRC
:
SkEnv.includes
skenv_link
md_src
.(
Mod.sk
)).
Hypothesis
(
INCLTGT
:
SkEnv.includes
skenv_link
md_tgt
.(
Mod.sk
)).
Hypothesis
(
WF
:
SkEnv.wf
skenv_link
).
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Let
ge
:
Csharpminor.genv
:= (
SkEnv.revive
(
SkEnv.project
skenv_link
md_src
.(
Mod.sk
))
prog
).
Let
tge
:
Cminor.genv
:= (
SkEnv.revive
(
SkEnv.project
skenv_link
md_tgt
.(
Mod.sk
))
tprog
).
Definition
msp
:
ModSemPair.t
:=
ModSemPair.mk
(
md_src
skenv_link
) (
md_tgt
skenv_link
)
tt
sm_link
.
Inductive
match_states
(
sm_init
:
SimMem.t
)
(
idx
:
nat
) (
st_src0
:
Csharpminor.state
) (
st_tgt0
:
Cminor.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
Cminorgenproof.match_states
skenv_link
skenv_link
ge
st_src0
st_tgt0
sm0
)
(
MCOMPATIDX
:
idx
=
Cminorgenproof.measure
st_src0
).
Theorem
make_match_genvs
:
SimSymbId.sim_skenv
(
SkEnv.project
skenv_link
md_src
.(
Mod.sk
)) (
SkEnv.project
skenv_link
md_tgt
.(
Mod.sk
)) ->
Genv.match_genvs
(
match_globdef
(
fun
cu
f
tf
=>
transl_fundef
f
=
OK
tf
)
eq
prog
)
ge
tge
.
Proof.
subst_locals
.
ss
.
eapply
SimSymbId.sim_skenv_revive
;
eauto
. Qed.
Theorem
sim_modsem
:
ModSemPair.sim
msp
.
Proof.
eapply
match_states_sim
with
(
match_states
:=
match_states
)
(
match_states_at
:=
fun
_
_
=>
eq
)
(
sound_state
:=
SoundTop.sound_state
);
eauto
;
ii
;
ss
.
-
eapply
Nat.lt_wf_0
.
-
eapply
SoundTop.sound_state_local_preservation
.
-
(* init bsim *)
(* destruct sm_arg; ss. clarify. *)
inv
INITTGT
.
des
.
inv
SAFESRC
.
destruct
args_src
,
args_tgt
;
ss
.
inv
SIMARGS
;
ss
.
clarify
.
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
eexists
.
exists
sm_arg
.
esplits
;
eauto
;
try
refl
;
econs
;
eauto
.
+
inv
TYP
.
folder
.
ss
.
exploit
(
Genv.find_funct_transf_partial_genv
SIMGE
);
eauto
.
intro
FINDFTGT
;
des
.
ss
.
assert
(
MGE
:
match_globalenvs
ge
(
SimMemInj.inj
sm_arg
) (
Genv.genv_next
skenv_link
)).
{
inv
SIMSKENV
.
inv
SIMSKE
.
ss
.
inv
INJECT
.
ss
.
econs
;
eauto
.
+
ii
.
ss
.
eapply
Plt_Ple_trans
. {
genext
. }
ss
.
refl
.
+
ii
.
ss
.
uge
.
des_ifs
.
eapply
Plt_Ple_trans
. {
genext
. }
ss
.
refl
.
+
ii
.
ss
.
uge
.
des_ifs
.
eapply
Plt_Ple_trans
. {
genext
. }
ss
.
refl
.
}
hexploit
fsim_external_inject_eq
;
try
apply
FINDF0
;
et
.
i
;
clarify
.
rpapply
match_callstate
;
ss
;
eauto
.
{
apply
MWF
. }
{
i
.
inv
SIMSKENV
.
inv
SIMSKE
.
ss
.
inv
INJECT
.
ss
.
econs
;
eauto
.
-
eapply
SimMemInjC.sim_skenv_symbols_inject
;
et
.
-
etrans
;
try
apply
MWF
.
ss
.
etrans
;
try
apply
MWF
.
rewrite
NBSRC
.
xomega
.
-
etrans
;
try
apply
MWF
.
ss
.
etrans
;
try
apply
MWF
.
rewrite
NBTGT
.
xomega
.
}
{
econs
;
et
. }
{
inv
TYP0
.
eapply
inject_list_typify_list
;
eauto
. }
assert
(
fn_sig
fd
=
Csharpminor.fn_sig
fd0
).
{
unfold
transl_function
in
*.
unfold
bind
in
*.
des_ifs
.
eapply
sig_preserved_body
;
eauto
. }
f_equal
;
try
congruence
.
-
(* init progress *)
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
exploit
(
Genv.find_funct_match_genv
SIMGE
);
eauto
.
i
;
des
.
ss
.
clarify
.
folder
.
hexploit
(@
fsim_external_inject_eq
);
try
apply
FINDF
;
eauto
.
clear
FPTR
.
intro
FPTR
.
(* unfold transf_function, bind in *. des_ifs. *)
unfold
bind
in
*.
des_ifs
.
assert
(
FN_SIG
:
fn_sig
f
=
Csharpminor.fn_sig
fd
).
{
unfold
transl_function
in
*.
unfold
bind
in
*.
des_ifs
.
eapply
sig_preserved_body
;
eauto
. }
esplits
;
eauto
.
econs
;
eauto
;
rewrite
FN_SIG
;
ss
.
+
inv
TYP
.
econs
;
ss
.
exploit
inject_list_length
;
et
.
congruence
.
(* inv TYP. econs. eapply typecheck_inject; et. congruence. *)
+
ss
.
exploit
inject_list_length
;
et
.
congruence
.
-
(* call wf *)
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
-
(* call fsim *)
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
inv
MATCH
;
ss
.
destruct
sm0
;
ss
.
clarify
.
inv
CALLSRC
.
inv
MATCHST
;
ss
.
folder
.
inv
MCOMPAT
;
ss
.
clear_tac
.
exploit
(
fsim_external_funct_inject
SIMGE
);
eauto
. {
ii
;
clarify
;
ss
.
des
;
ss
. }
intro
EXTTGT
.
esplits
;
eauto
.
+
econs
;
eauto
.
*
des
.
clarify
.
esplits
;
eauto
.
(* exploit (sim_internal_funct_inject SIMGE); try apply SIG; et. *)
(* Arguments sim_internal_funct_inject [_]. *)
(* destruct SIMSKENVLINK. inv H. rr in SIMSKENV1. clarify. *)
(* exploit (sim_internal_funct_inject); try apply VAL; try apply SIG; et. *)
(* { erewrite match_globdef_eq. eapply Global_match_genvs_refl. } *)
(* { inv SIMSKENV. ss. } *)
(***************** TODO: Add as a lemma in GlobalenvsC. *******************)
inv
SIMSKENV
.
assert
(
fptr_arg
=
tfptr
).
{
inv
FPTR
;
ss
.
des_ifs_safe
.
apply
Genv.find_funct_ptr_iff
in
SIG
.
unfold
Genv.find_def
in
*.
inv
SIMSKE
.
ss
.
inv
INJECT
;
ss
.
exploit
(
DOMAIN
b1
);
eauto
.
{
eapply
Genv.genv_defs_range
;
et
. }
i
;
clarify
.
}
clarify
.
+
econs
;
ss
.
+
reflexivity
.
-
(* after fsim *)
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
inv
AFTERSRC
.
inv
SIMRET
;
ss
.
exists
(
SimMemInj.unlift
'
sm_arg
sm_ret
).
destruct
sm_ret
;
ss
.
clarify
.
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
inv
HISTORY
.
ss
.
clear_tac
.
esplits
;
eauto
.
+
econs
;
eauto
.
+
econs
;
ss
;
eauto
.
inv
MLE0
;
ss
.
inv
MCOMPAT
.
clear_tac
.
rpapply
match_returnstate
;
ss
;
eauto
;
ss
.
{
eapply
MWFAFTR
. }
{
eapply
match_callstack_le
;
eauto
.
eapply
match_callstack_incr_bound
;
try
eapply
Mem.unchanged_on_nextblock
;
eauto
.
eapply
match_callstack_external_call
;
try
eapply
MCS
;
et
;
try
xomega
.
-
eapply
SkEnv.senv_genv_compat
;
ss
.
-
eapply
SkEnv.senv_genv_compat
;
ss
.
-
eapply
Mem.unchanged_on_implies
;
try
eassumption
.
ss
.
-
eapply
Mem.unchanged_on_implies
;
try
eassumption
.
ss
.
-
eapply
SimMemInj.inject_separated_frozen
;
et
.
-
ii
.
eapply
MAXSRC
;
ss
.
}
{
eapply
inject_typify
;
eauto
. }
+
refl
.
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
;
inv
MATCHST
;
ss
.
inv
MK
.
inv
MCOMPAT
;
ss
.
eexists
sm0
.
esplits
;
ss
;
eauto
;
try
refl
.
econs
;
eauto
.
-
left
;
i
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
esplits
;
eauto
.
{
apply
CsharpminorC.modsem_receptive
. }
inv
MATCH
.
ii
.
hexploit
(@
transl_step_correct
prog
tprog
TRANSL
skenv_link
skenv_link
);
eauto
;
ss
.
{
eapply
SkEnv.senv_genv_compat
;
ss
. }
{
eapply
SkEnv.senv_genv_compat
;
ss
. }
i
;
des
.
+
esplits
;
eauto
.
*
left
.
eapply
spread_dplus
;
eauto
.
eapply
modsem_determinate
;
eauto
.
*
econs
;
ss
.
+
esplits
;
eauto
.
*
right
.
subst
tr
.
split
.
econs
.
eauto
.
*
assert
(
MCOMPAT
:
CsharpminorC.get_mem
st_src1
=
SimMem.src
sm1
/\
get_mem
st_tgt0
=
SimMem.tgt
sm1
).
{
inv
H1
;
inv
MCOMPAT
;
ss
. }
des
.
econs
;
eauto
;
ss
.
Unshelve
.
all
:
ss
;
try
(
by
econs
).
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variable
prog
:
Csharpminor.program
.
Variable
tprog
:
Cminor.program
.
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
CsharpminorC.module
prog
) (
CminorC.module
tprog
)
tt
.
Theorem
sim_mod
:
ModPair.sim
mp
.
Proof.
econs
;
ss
.
-
r
.
eapply
Sk.match_program_eq
;
eauto
.
ii
.
destruct
f1
;
ss
.
+
clarify
.
right
.
unfold
bind
in
MATCH
.
des_ifs
.
esplits
;
eauto
.
unfold
transl_function
in
*.
des_ifs
.
unfold
transl_funbody
in
*.
unfold
bind
in
Heq
.
des_ifs
.
+
clarify
.
left
.
esplits
;
eauto
.
-
ii
.
inv
SIMSKENVLINK
.
inv
SIMSKENV
.
eapply
sim_modsem
;
eauto
.
Qed.
End
SIMMOD
.