Module CstrategyproofC
Require
Import
Axioms
.
Require
Import
Classical
.
Require
Import
CoqlibC
.
Require
Import
ErrorsC
.
Require
Import
MapsC
.
Require
Import
IntegersC
.
Require
Import
Floats
.
Require
Import
ValuesC
.
Require
Import
ASTC
.
Require
Import
MemoryC
.
Require
Import
EventsC
.
Require
Import
GlobalenvsC
.
Require
Import
SmallstepC
.
Require
Import
CtypesC
.
Require
Import
CopC
.
Require
Import
Csyntax
.
Require
Import
CsemC
.
Require
Import
sflib
.
Require
Import
CstrategyC
Cstrategyproof
.
newly added
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
AsmregsC
MatchSimModSem
.
Require
SimMemId
.
Require
SoundTop
.
Set
Implicit
Arguments
.
Section
SIMMODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variables
prog
:
program
.
Let
md_src
:
Mod.t
:= (
CsemC.module
prog
).
Let
md_tgt
:
Mod.t
:= (
module
prog
).
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
).
Let
ge
:
genv
:=
Build_genv
(
SkEnv.revive
(
SkEnv.project
skenv_link
md_src
.(
Mod.sk
))
prog
)
prog
.(
prog_comp_env
).
Let
tge
:
genv
:=
Build_genv
(
SkEnv.revive
(
SkEnv.project
skenv_link
md_tgt
.(
Mod.sk
))
prog
)
prog
.(
prog_comp_env
).
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
:
Csem.state
) (
st_tgt0
:
Csem.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
st_src0
=
st_tgt0
)
(
MWF
:
SimMem.wf
sm0
).
Require
Import
Classes.Equivalence
.
Ltac
inv
H
:=
inversion
H
;
clear
H
;
subst
*.
Theorem
sim_modsem
:
ModSemPair.sim
msp
.
Proof.
eapply
match_states_sim
with
(
match_states
:=
match_states
) (
match_states_at
:=
top4
) (
sound_state
:=
SoundTop.sound_state
);
eauto
;
ii
;
ss
.
-
instantiate
(1:=
Nat.lt
).
apply
lt_wf
.
-
eapply
SoundTop.sound_state_local_preservation
.
-
(* init bsim *)
destruct
sm_arg
;
ss
.
clarify
.
inv
INITTGT
.
inv
SIMARGS
;
ss
.
subst
*.
eexists
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
eauto
;
cycle
1.
+
econs
;
ss
;
eauto
.
+
econs
;
eauto
;
ss
.
-
(* init progress *)
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
subst
*.
inv
TYP
.
esplits
;
eauto
.
econs
;
eauto
.
ss
.
-
(* call wf *)
inv
MATCH
;
ss
.
-
(* call fsim *)
inv
MATCH
;
ss
.
destruct
sm0
;
ss
.
clarify
.
inv
CALLSRC
.
ss
.
des
;
ss
.
clarify
.
folder
.
eexists
_
, (
SimMemId.mk
_
_
).
esplits
;
ss
;
eauto
.
+
econs
;
eauto
.
+
econs
;
ss
;
eauto
.
-
(* after fsim *)
inv
AFTERSRC
.
inv
SIMRET
;
ss
.
exists
sm_ret
.
destruct
sm_ret
;
ss
.
clarify
.
inv
MATCH
;
ss
.
des
;
ss
.
clarify
.
esplits
;
eauto
.
+
econs
;
eauto
.
+
econs
;
ss
;
eauto
.
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
.
ss
.
des
;
ss
.
clarify
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
ss
;
eauto
.
econs
;
ss
;
eauto
.
-
(* step *)
right
;
i
.
inv
MATCH
;
ss
.
splits
.
{
ii
.
exploit
Cstrategyproof.progress
;
eauto
.
{
instantiate
(1:=
ModSem.is_call
(
CsemC.modsem
skenv_link
prog
) \1/
ModSem.is_return
(
CsemC.modsem
skenv_link
prog
)).
ss
.
intro
T
.
des
;
inv
T
;
inv
H0
;
ss
.
}
{
ii
.
exploit
H
;
eauto
.
i
;
des
;
eauto
. }
i
;
des
;
eauto
.
-
inv
H0
.
contradict
NOTRET
.
rr
.
esplits
.
econs
;
eauto
.
-
inv
H0
.
contradict
NOTCALL
.
rr
.
esplits
.
eauto
.
-
inv
H0
.
contradict
NOTRET
.
rr
.
esplits
.
eauto
.
}
i
.
folder
.
exploit
Cstrategyproof.step_simulation
;
eauto
.
i
.
esplits
;
eauto
.
{
econs
;
eauto
.
instantiate
(1:=
sm0
).
ss
. }
Unshelve
.
all
:
ss
;
try
(
by
econs
).
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variables
prog
:
program
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
CsemC.module
prog
) (
module
prog
).(
Mod.Atomic.trans
)
tt
.
Theorem
sim_mod
:
ModPair.sim
mp
.
Proof.
econs
;
ss
.
-
ii
.
inv
SIMSKENVLINK
.
eapply
factor_simmodsem_target
;
eauto
.
{
ii
.
eapply
CsemC.single_events_at
;
eauto
.
ss
.
eauto
. }
{
ii
.
ss
.
hexploit
(@
modsem_strongly_receptive
skenv_link_tgt
prog
s
);
eauto
.
intro
SR
.
inv
SR
.
exploit
ssr_traces_at
;
eauto
.
}
eapply
sim_modsem
;
eauto
.
Qed.
End
SIMMOD
.