Module SimSymbId
Require
Import
Events
.
Require
Import
Values
.
Require
Import
AST
.
Require
Import
Memory
.
Require
Import
GlobalenvsC
.
Require
Import
Smallstep
.
Require
Import
CoqlibC
.
Require
Import
Skeleton
.
Require
Import
Integers
.
Require
Import
ASTC
.
Require
Import
LinkingC
.
Require
Import
MapsC
.
Require
Import
SimSymb
.
Require
Import
System
.
Set
Implicit
Arguments
.
Definition
sim_skenv
(
skenv0
skenv1
:
SkEnv.t
):
Prop
:=
skenv0
=
skenv1
.
Lemma
sim_skenv_equiv
skenv_src
skenv_tgt
(
SIMSKENV
:
sim_skenv
skenv_src
skenv_tgt
):
<<
EQUIV
:
Senv.equiv
skenv_src
skenv_tgt
>>.
Proof.
rewrite
SIMSKENV
.
eapply
GlobalenvsC.Senv_eq_equiv_obligation_1
. Qed.
Lemma
system_sim_skenv
skenv_src
skenv_tgt
(
SIMSKENV
:
sim_skenv
skenv_src
skenv_tgt
):
<<
SIMSKENV
:
sim_skenv
(
skenv_src
).(
System.skenv
) (
skenv_tgt
).(
System.skenv
)>>.
Proof.
inv
SIMSKENV
.
econs
;
eauto
. Qed.
Definition
sim_sk
(
u
:
unit
) (
sk_src
sk_tgt
:
Sk.t
):
Prop
:=
sk_src
=
sk_tgt
.
Definition
le
:
unit
->
Sk.t
->
Sk.t
->
unit
->
Prop
:=
top4
.
Lemma
sim_sk_link
:
forall
ss0
(
sk_src0
sk_tgt0
:
Sk.t
)
ss1
sk_src1
sk_tgt1
sk_src
(
SIMSK
:
sim_sk
ss0
sk_src0
sk_tgt0
)
(
SIMSK
:
sim_sk
ss1
sk_src1
sk_tgt1
)
(
LINKSRC
:
link
sk_src0
sk_src1
=
Some
sk_src
),
exists
ss
sk_tgt
,
<<
LINKTGT
:
link
sk_tgt0
sk_tgt1
=
Some
sk_tgt
>> /\
<<
LE0
:
le
ss0
sk_src0
sk_tgt0
ss
>> /\
<<
LE1
:
le
ss1
sk_src1
sk_tgt1
ss
>> /\
<<
SIMSK
:
sim_sk
ss
sk_src
sk_tgt
>>.
Proof.
i
.
inv
SIMSK
.
inv
SIMSK0
.
esplits
;
ss
;
eauto
.
Unshelve
.
all
:
ss
.
Qed.
Lemma
sim_sk_load_sim_skenv
:
forall
ss
sk_src
sk_tgt
skenv_src
skenv_tgt
m_src
(
SIMSK
:
sim_sk
ss
sk_src
sk_tgt
)
(
LOADSRC
:
sk_src
.(
Sk.load_skenv
) =
skenv_src
)
(
LOADTGT
:
sk_tgt
.(
Sk.load_skenv
) =
skenv_tgt
)
(
LOADMEMSRC
:
sk_src
.(
Sk.load_mem
) =
Some
m_src
),
(<<
LOADMEMTGT
:
sk_tgt
.(
Sk.load_mem
) =
Some
m_src
>>) /\
(<<
SIMSKENV
:
sim_skenv
skenv_src
skenv_tgt
>>) /\
(<<
MAINSIM
: (
Genv.symbol_address
skenv_src
(
prog_main
sk_src
)
Ptrofs.zero
)
= (
Genv.symbol_address
skenv_tgt
(
prog_main
sk_tgt
)
Ptrofs.zero
)>>).
Proof.
i
.
u
in
*.
inv
SIMSK
.
esplits
;
eauto
.
rr
.
ss
. Qed.
Lemma
sim_skenv_monotone
:
forall
ss_link
skenv_link_src
skenv_link_tgt
ss
sk_src
sk_tgt
skenv_src
skenv_tgt
(
WFSRC
:
SkEnv.wf
skenv_link_src
)
(
WFTGT
:
SkEnv.wf
skenv_link_tgt
)
(
SIMSKENV
:
sim_skenv
skenv_link_src
skenv_link_tgt
)
(
SIMSK
:
sim_sk
ss
sk_src
sk_tgt
)
(
LE
:
le
ss
sk_src
sk_tgt
ss_link
)
(
LESRC
:
SkEnv.project
skenv_link_src
sk_src
=
skenv_src
)
(
LETGT
:
SkEnv.project
skenv_link_tgt
sk_tgt
=
skenv_tgt
),
<<
SIMSKENV
:
sim_skenv
skenv_src
skenv_tgt
>>.
Proof.
i
.
clarify
.
rr
.
inv
SIMSK
.
inv
SIMSKENV
.
ss
. Qed.
Lemma
sim_skenv_func_bisim
:
forall
skenv_src
skenv_tgt
(
SIMSKENV
:
sim_skenv
skenv_src
skenv_tgt
),
<<
DEF
:
SimSymb.skenv_func_bisim
eq
skenv_src
skenv_tgt
>>.
Proof.
i
.
inv
SIMSKENV
.
econs
;
eauto
;
ii
;
assert
(
fptr_src
=
fptr_tgt
)
by
ss
;
clarify
;
unfold
Genv.find_funct
,
Genv.find_funct_ptr
in
*;
des_ifs_safe
;
esplits
;
eauto
.
Qed.
Local
Opaque
prog_defmap
.
Section
REVIVE
.
Context
{
C
F1
V1
F2
V2
:
Type
} {
LC
:
Linker
C
} {
LF
:
Linker
F1
} {
LV
:
Linker
V1
}.
Context
`{
HasExternal
F1
} `{
HasExternal
F2
}.
Variable
match_fundef
:
C
->
F1
->
F2
->
Prop
.
Variable
match_varinfo
:
V1
->
V2
->
Prop
.
Variables
(
ctx
:
C
) (
p_src
:
AST.program
F1
V1
) (
p_tgt
:
AST.program
F2
V2
).
Hypothesis
(
MATCHPROG
:
match_program_gen
match_fundef
match_varinfo
ctx
p_src
p_tgt
).
Hypothesis
MATCH_FUNDEF_EXTERNAL
:
forall
ctx
f_src
f_tgt
(
MATCH
:
match_fundef
ctx
f_src
f_tgt
),
is_external
f_src
=
is_external
f_tgt
.
Lemma
sim_skenv_revive
skenv_proj_src
skenv_proj_tgt
ge_src
ge_tgt
(
REVIVESRC
:
ge_src
=
SkEnv.revive
skenv_proj_src
p_src
)
(
REVIVETGT
:
ge_tgt
=
SkEnv.revive
skenv_proj_tgt
p_tgt
)
(
SIMSKENV
:
sim_skenv
skenv_proj_src
skenv_proj_tgt
):
<<
SIMGE
:
Genv.match_genvs
(
match_globdef
match_fundef
match_varinfo
ctx
)
ge_src
ge_tgt
>>.
Proof.
clarify
.
inv
SIMSKENV
.
econs
;
eauto
.
ii
.
ss
.
rewrite
!
MapsC.PTree_filter_map_spec
.
rewrite
!
o_bind_ignore
.
unfold
Genv.find_def
in
*.
des_ifs
;
try
(
by
econs
).
destruct
(
Genv.invert_symbol
skenv_proj_tgt
b
)
eqn
:
T
;
cbn
;
try
(
by
econs
;
eauto
).
apply
match_program_defmap
with
(
id
:=
i
)
in
MATCHPROG
.
inv
MATCHPROG
;
cbn
;
try
(
by
econs
;
eauto
).
(* inv H3; ss; cycle 1. *)
(* { econs; eauto. econs; eauto. } *)
(* erewrite MATCH_FUNDEF_EXTERNAL; eauto. *)
(* des_ifs; try (by econs; eauto). *)
(* econs; eauto. econs; eauto. *)
Qed.
End
REVIVE
.