Module SimMemId
Require
Import
CoqlibC
.
Require
Import
Memory
.
Require
Import
Values
.
Require
Import
Maps
.
Require
Import
Events
.
Require
Import
Globalenvs
.
Require
Import
sflib
.
Require
Import
RelationClasses
.
Require
Import
FSets
.
Require
Import
Ordered
.
Require
Import
AST
.
Require
Import
Integers
.
Require
Import
IntegersC
LinkingC
.
Require
Import
SimSymb
Skeleton
Mod
ModSem
.
Require
SimSymbId
.
Require
Import
SimMemLift
.
Set
Implicit
Arguments
.
Record
t
' :=
mk
{
src
:
mem
;
tgt
:
mem
;
}.
Program
Instance
SimMemId
:
SimMem.class
:=
{
t
:=
t
';
src
:=
src
;
tgt
:=
tgt
;
wf
:=
fun
(
rel
:
t
') =>
rel
.(
src
) =
rel
.(
tgt
);
le
:=
fun
(
mrel0
mrel1
:
t
') =>
True
;
lepriv
:=
top2
;
sim_val
:=
fun
(
_
:
t
') =>
eq
;
sim_val_list
:=
fun
(
_
:
t
') =>
eq
;
}.
Next Obligation.
do
2 (
apply
Axioms.functional_extensionality
;
i
).
apply
prop_ext1
.
split
;
i
;
ss
;
clarify
.
-
ginduction
x
;
ii
;
inv
H
;
ss
.
erewrite
IHx
;
eauto
.
-
ginduction
x1
;
ii
;
ss
.
econs
;
eauto
.
Qed.
Program
Instance
SimMemIdLift
:
SimMemLift.class
SimMemId
:=
{
lift
:=
id
;
unlift
:=
fun
_
=>
id
;
}.
Global
Program
Instance
SimSymbId
:
SimSymb.class
SimMemId
:= {
t
:=
unit
;
le
:=
SimSymbId.le
;
sim_sk
:=
SimSymbId.sim_sk
;
sim_skenv
(
_
:
SimMem.t
) (
_
:
unit
) :=
SimSymbId.sim_skenv
;
}.
Next Obligation.
ss
. Qed.
Next Obligation.
rr
in
SIMSK
.
clarify
. Qed.
Next Obligation.
eapply
SimSymbId.sim_sk_link
;
eauto
. Qed.
Next Obligation.
rr
in
SIMSKE
.
clarify
. Qed.
Next Obligation.
exploit
SimSymbId.sim_sk_load_sim_skenv
;
eauto
.
i
;
des
.
eexists
.
eexists
(
mk
_
_
).
esplits
;
ss
;
eauto
.
Qed.
Next Obligation.
eapply
SimSymbId.sim_skenv_monotone
;
try
apply
SIMSKENV
;
eauto
. Qed.
Next Obligation.
eapply
SimSymbId.sim_skenv_func_bisim
;
eauto
. Qed.
Next Obligation.
esplits
;
eauto
.
eapply
SimSymbId.system_sim_skenv
;
eauto
. Qed.
Next Obligation.
inv
ARGS
;
ss
.
clarify
.
destruct
sm0
;
ss
.
clarify
.
destruct
retv_src
;
ss
.
esplits
;
eauto
.
-
eapply
external_call_symbols_preserved
;
eauto
.
{
eapply
SimSymbId.sim_skenv_equiv
;
eauto
. }
instantiate
(1:=
Retv.mk
_
_
).
ss
.
eauto
.
-
instantiate
(1:=
mk
_
_
).
econs
;
ss
;
eauto
.
-
ss
.
Qed.