Module SoundProduct
Require
Import
CoqlibC
.
Require
Import
MemoryC
.
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
ModSem
.
Require
Import
Skeleton
.
Require
Import
System
.
Require
Import
Sound
Preservation
.
Set
Implicit
Arguments
.
Section
SOUNDPRODUCT
.
Variable
SU0
SU1
:
Sound.class
.
Global
Program
Instance
sound_class_product
:
Sound.class
:=
{
Sound.t
:=
SU0
.(@
Sound.t
) *
SU1
.(@
Sound.t
);
Sound.mle
su0
m0
m1
:=
SU0
.(@
Sound.mle
)
su0
.(
fst
)
m0
m1
/\
SU1
.(@
Sound.mle
)
su0
.(
snd
)
m0
m1
;
Sound.lepriv
su0
su1
:=
SU0
.(@
Sound.lepriv
)
su0
.(
fst
)
su1
.(
fst
) /\
SU1
.(@
Sound.lepriv
)
su0
.(
snd
)
su1
.(
snd
);
Sound.hle
su0
su1
:=
SU0
.(@
Sound.hle
)
su0
.(
fst
)
su1
.(
fst
) /\
SU1
.(@
Sound.hle
)
su0
.(
snd
)
su1
.(
snd
);
Sound.wf
su0
:=
SU0
.(@
Sound.wf
)
su0
.(
fst
) /\
SU1
.(@
Sound.wf
)
su0
.(
snd
);
Sound.val
su0
v
:=
SU0
.(@
Sound.val
)
su0
.(
fst
)
v
/\
SU1
.(@
Sound.val
)
su0
.(
snd
)
v
;
Sound.mem
su0
m
:=
SU0
.(@
Sound.mem
)
su0
.(
fst
)
m
/\
SU1
.(@
Sound.mem
)
su0
.(
snd
)
m
;
Sound.skenv
su0
m
ske
:=
SU0
.(@
Sound.skenv
)
su0
.(
fst
)
m
ske
/\
SU1
.(@
Sound.skenv
)
su0
.(
snd
)
m
ske
}
.
Next Obligation.
econs
;
eauto
;
ii
;
ss
;
des
.
-
esplits
;
eauto
;
refl
.
-
esplits
;
eauto
;
etrans
;
eauto
.
Qed.
Next Obligation.
econs
;
eauto
;
ii
;
ss
;
des
.
-
esplits
;
eauto
;
refl
.
-
esplits
;
eauto
;
etrans
;
eauto
.
Qed.
Next Obligation.
econs
;
eauto
;
ii
;
ss
;
des
.
-
esplits
;
eauto
;
refl
.
-
esplits
;
eauto
;
etrans
;
eauto
.
Qed.
Next Obligation.
ii
;
ss
.
esplits
;
ss
;
eauto
;
eapply
Sound.hle_lepriv
;
et
.
Qed.
Next Obligation.
ii
;
ss
.
esplits
;
ss
;
eauto
;
eapply
Sound.hle_mle
;
et
.
Qed.
Next Obligation.
ii
;
ss
.
des
.
esplits
;
ss
;
eauto
;
eapply
Sound.hle_val
;
et
.
Qed.
Next Obligation.
exploit
(@
Sound.init_spec
SU0
);
eauto
.
i
;
des
.
exploit
(@
Sound.init_spec
SU1
);
eauto
.
i
;
des
.
exists
(
su_init
,
su_init0
);
eauto
.
inv
SUARGS
.
inv
SUARGS0
.
ss
.
des
.
esplits
;
ss
;
eauto
.
Qed.
Next Obligation.
ss
.
esplits
;
eauto
;
eapply
Sound.skenv_lepriv
;
eauto
.
Qed.
Next Obligation.
ss
.
esplits
;
eauto
;
eapply
Sound.skenv_mle
;
eauto
.
Qed.
Next Obligation.
ss
.
esplits
;
eauto
;
eapply
Sound.skenv_project
;
eauto
.
Qed.
Next Obligation.
ss
.
rr
.
esplits
;
ii
;
des
.
-
erewrite
<- ! (
Sound.system_skenv
)
in
*;
eauto
.
-
erewrite
<- (
Sound.system_skenv
)
in
H
;
eauto
.
erewrite
<- (
Sound.system_skenv
)
in
H0
;
eauto
.
Qed.
Next Obligation.
ss
.
des
.
exploit
(@
Sound.system_axiom
SU0
);
et
.
{
des_ifs
;
ss
.
des
.
rr
.
esplits
;
eauto
.
rr
.
rewrite
Forall_forall
in
*.
ii
;
ss
;
eauto
.
eapply
VALS
;
eauto
. }
intro
T
.
exploit
(@
Sound.system_axiom
SU1
);
et
.
{
des_ifs
;
ss
.
des
.
rr
.
esplits
;
eauto
.
rr
.
rewrite
Forall_forall
in
*.
ii
;
ss
;
eauto
.
eapply
VALS
;
eauto
. }
intro
T0
.
des
.
unfold
Sound.retv
in
*.
ss
.
des
.
eexists
(
su0
,
su1
).
esplits
;
ss
;
eauto
.
Qed.
Lemma
sound_args_iff
su0
su1
args
:
(@
Sound.args
SU0
su0
args
) /\ (@
Sound.args
SU1
su1
args
) <-> (@
Sound.args
sound_class_product
(
su0
,
su1
)
args
)
.
Proof.
unfold
Sound.args
.
unfold
Sound.vals
.
ss
.
des_ifs
.
-
split
;
ii
;
des
;
esplits
;
eauto
;
rewrite
Forall_forall
in
*;
ii
;
ss
;
eauto
.
+
eapply
VALS
;
eauto
.
+
eapply
VALS
;
eauto
.
-
split
;
ii
;
des
;
esplits
;
eauto
;
ii
;
ss
;
eauto
.
+
eapply
REGSET
;
eauto
.
+
eapply
REGSET
;
eauto
.
Qed.
Lemma
sound_skenv_iff
su0
su1
m
ske
:
(@
Sound.skenv
SU0
su0
m
ske
) /\ (@
Sound.skenv
SU1
su1
m
ske
) <-> (@
Sound.skenv
sound_class_product
(
su0
,
su1
)
m
ske
)
.
Proof.
split
;
ii
;
des
;
esplits
;
ss
;
des
;
eauto
.
Qed.
Lemma
sound_retv_iff
su0
su1
args
:
(@
Sound.retv
SU0
su0
args
) /\ (@
Sound.retv
SU1
su1
args
) <-> (@
Sound.retv
sound_class_product
(
su0
,
su1
)
args
)
.
Proof.
unfold
Sound.retv
.
ss
.
des_ifs
.
-
split
;
ii
;
des
;
esplits
;
eauto
;
rewrite
Forall_forall
in
*;
ii
;
ss
;
eauto
.
-
split
;
ii
;
des
;
esplits
;
eauto
;
ii
;
ss
;
eauto
.
+
eapply
REGSET
.
+
eapply
REGSET
.
Qed.
Theorem
preservation_product
ms
sound_state0
sound_state1
(
PRSV0
: @
local_preservation
SU0
ms
sound_state0
)
(
PRSV1
: @
local_preservation
SU1
ms
sound_state1
):
<<
PRSV
: @
local_preservation
sound_class_product
ms
(
fun
su
m
st
=>
sound_state0
su
.(
fst
)
m
st
/\
sound_state1
su
.(
snd
)
m
st
)>>.
Proof.
inv
PRSV0
.
inv
PRSV1
.
econs
;
eauto
.
-
clear
-
INIT
INIT0
.
ii
.
ss
.
specialize
(
INIT
su_init
.(
fst
)).
specialize
(
INIT0
su_init
.(
snd
)).
split
;
ss
.
+
eapply
INIT
;
eauto
.
{
destruct
su_init
;
ss
.
eapply
sound_args_iff
in
SUARG
;
eauto
.
ss
;
des
;
ss
. }
{
destruct
su_init
;
ss
.
eapply
sound_skenv_iff
in
SKENV
;
eauto
.
ss
;
des
;
ss
. }
+
eapply
INIT0
;
eauto
.
{
destruct
su_init
;
ss
.
eapply
sound_args_iff
in
SUARG
;
eauto
.
des
.
ss
. }
{
destruct
su_init
;
ss
.
eapply
sound_skenv_iff
in
SKENV
;
eauto
.
ss
;
des
;
ss
. }
-
clear
-
STEP
STEP0
.
ii
.
ss
.
des
.
specialize
(
STEP
m_arg
su0
.(
fst
)).
specialize
(
STEP0
m_arg
su0
.(
snd
)).
split
;
ss
.
+
eapply
STEP
;
eauto
.
+
eapply
STEP0
;
eauto
.
-
clear
-
CALL
CALL0
.
ii
.
ss
.
des
.
exploit
CALL
;
eauto
.
i
;
des
.
exploit
CALL0
;
eauto
.
i
;
des
.
esplits
;
eauto
.
{
instantiate
(1:= (
su_gr
,
su_gr0
)).
eapply
sound_args_iff
;
eauto
. }
{
ss
. }
{
ss
. }
i
.
ss
.
des
.
split
;
ss
.
+
eapply
K
;
eauto
.
destruct
su_ret
;
ss
.
eapply
sound_retv_iff
in
RETV
.
des
;
ss
.
+
eapply
K0
;
eauto
.
destruct
su_ret
;
ss
.
eapply
sound_retv_iff
in
RETV
.
des
;
ss
.
-
clear
-
RET
RET0
.
ii
.
ss
.
des
.
specialize
(
RET
m_arg
su0
.(
fst
)).
specialize
(
RET0
m_arg
su0
.(
snd
)).
exploit
RET
;
eauto
.
i
;
des
.
exploit
RET0
;
eauto
.
i
;
des
.
exists
(
su_ret
,
su_ret0
).
esplits
;
eauto
.
eapply
sound_retv_iff
.
ss
.
Qed.
End
SOUNDPRODUCT
.