Module RUSC
Libraries.
Require
Import
String
.
Require
Import
CoqlibC
Errors
ErrorsC
.
Require
Import
AST
Linking
Smallstep
.
Command-line flags.
Require
Import
Compopts
.
newly added *
Require
Import
BehaviorsC
.
Require
Export
Compiler
.
Require
Import
Simulation
.
Require
Import
Sem
SimProg
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
Sound
SimSymb
.
Require
Import
SemProps
AdequacyLocal
.
Module
program_relation
.
Record
t
:=
mk
{
rel
:>
program
->
program
->
Prop
;
horizontal
:
forall
p0_src
p1_src
p0_tgt
p1_tgt
(
REL0
:
rel
p0_src
p0_tgt
)
(
REL1
:
rel
p1_src
p1_tgt
),
rel
(
p0_src
++
p1_src
) (
p0_tgt
++
p1_tgt
);
adequacy
:
forall
p_src
p_tgt
(
REL
:
rel
p_src
p_tgt
),
improves
(
sem
p_src
) (
sem
p_tgt
);
empty
:
rel
[] [];
}.
End
program_relation
.
Hint
Resolve
program_relation.horizontal
.
Hint
Resolve
program_relation.adequacy
.
Hint
Resolve
program_relation.empty
.
Coercion
program_relation.rel
:
program_relation.t
>->
Funclass
.
Section
RUSC
.
Variable
R
:
program_relation.t
->
Prop
.
Definition
relate_R
(
p_src
p_tgt
:
program
) :=
forall
r
(
RELIN
:
R
r
),
r
p_src
p_tgt
.
Definition
self_related
(
p
:
program
) :=
relate_R
p
p
.
Lemma
empty_self_related
:
self_related
[].
Proof.
ii
.
eauto
. Qed.
Lemma
self_related_horizontal
(
p0
p1
:
program
)
(
SELF0
:
self_related
p0
)
(
SELF1
:
self_related
p1
):
self_related
(
p0
++
p1
).
Proof.
ii
.
eauto
. Qed.
Definition
rusc
(
p_src
p_tgt
:
program
):=
forall
(
ctx0
ctx1
:
program
)
(
SELF0
:
self_related
ctx0
)
(
SELF1
:
self_related
ctx1
),
improves
(
sem
(
ctx0
++
p_src
++
ctx1
))
(
sem
(
ctx0
++
p_tgt
++
ctx1
)).
Global
Program
Instance
rusc_PreOrder
:
RelationClasses.PreOrder
rusc
.
Next Obligation.
unfold
rusc
,
Reflexive
.
i
.
refl
. Qed.
Next Obligation.
unfold
rusc
,
Transitive
.
i
.
etrans
;
eauto
. Qed.
Lemma
rusc_incl
(
p_src
p_tgt
:
program
) (
r
:
program_relation.t
)
(
REL
:
r
p_src
p_tgt
)
(
RELIN
:
R
r
):
rusc
p_src
p_tgt
.
Proof.
unfold
rusc
.
i
.
eapply
program_relation.adequacy
.
eauto
. Qed.
Lemma
rusc_adequacy_left_ctx
ctx
(
p_src
p_tgt
:
program
)
(
RUSC
:
rusc
p_src
p_tgt
)
(
SELF
:
self_related
ctx
):
improves
(
sem
(
ctx
++
p_src
))
(
sem
(
ctx
++
p_tgt
)).
Proof.
specialize
(
RUSC
ctx
[]).
rewrite
app_nil_r
in
*.
rewrite
app_nil_r
in
*.
eapply
RUSC
;
eauto
.
eapply
empty_self_related
.
Qed.
Lemma
rusc_adequacy_right_ctx
ctx
(
p_src
p_tgt
:
program
)
(
RUSC
:
rusc
p_src
p_tgt
)
(
SELF
:
self_related
ctx
):
improves
(
sem
(
p_src
++
ctx
))
(
sem
(
p_tgt
++
ctx
)).
Proof.
specialize
(
RUSC
[]
ctx
).
eapply
RUSC
;
eauto
.
eapply
empty_self_related
.
Qed.
Lemma
rusc_adequacy
(
p_src
p_tgt
:
program
)
(
RUSC
:
rusc
p_src
p_tgt
):
improves
(
sem
p_src
) (
sem
p_tgt
).
Proof.
specialize
(
RUSC
[] []).
ss
.
rewrite
app_nil_r
in
*.
rewrite
app_nil_r
in
*.
eapply
RUSC
;
eapply
empty_self_related
.
Qed.
Lemma
rusc_horizontal
(
p0_src
p1_src
p0_tgt
p1_tgt
:
program
)
(
RUSC0
:
rusc
p0_src
p0_tgt
)
(
RUSC1
:
rusc
p1_src
p1_tgt
)
(
SELFSRC0
:
self_related
p0_src
)
(
SELFSRC1
:
self_related
p1_src
)
(
SELFTGT0
:
self_related
p0_tgt
)
(
SELFTGT1
:
self_related
p1_tgt
):
rusc
(
p0_src
++
p1_src
) (
p0_tgt
++
p1_tgt
).
Proof.
unfold
rusc
in
*.
i
.
erewrite
<-
app_assoc
.
erewrite
<-
app_assoc
.
transitivity
(
sem
(
ctx0
++
p0_tgt
++
p1_src
++
ctx1
));
eauto
.
{
eapply
RUSC0
;
eauto
.
eapply
self_related_horizontal
;
eauto
. }
rewrite
app_assoc
.
replace
(
ctx0
++
p0_tgt
++
p1_tgt
++
ctx1
)
with
((
ctx0
++
p0_tgt
) ++
p1_tgt
++
ctx1
);
eauto
.
{
eapply
RUSC1
;
eauto
.
eapply
self_related_horizontal
;
eauto
. }
rewrite
<-
app_assoc
;
auto
.
Qed.
Lemma
rusc_vertical
(
p0
p1
p2
:
program
)
(
RUSC0
:
rusc
p0
p1
)
(
RUSC1
:
rusc
p1
p2
):
rusc
p0
p2
.
Proof.
unfold
rusc
in
*.
i
.
etrans
;
eauto
. Qed.
End
RUSC
.
Hint
Resolve
self_related_horizontal
.
Hint
Resolve
empty_self_related
.
Lemma
self_related_mon
R0
R1
(
LE
:
R0
<1=
R1
):
self_related
R1
<1=
self_related
R0
.
Proof.
ii
.
eauto
. Qed.
Hint
Resolve
self_related_mon
.
Lemma
rusc_mon
R0
R1
(
LE
:
R0
<1=
R1
):
rusc
R0
<2=
rusc
R1
.
Proof.
intros
p_src
p_tgt
RU
ctx0
ctx1
.
i
.
eapply
RU
;
eauto
;
eapply
self_related_mon
;
eauto
.
Qed.
Hint
Resolve
rusc_mon
.
Program
Definition
mkPR
(
MR
:
SimMem.class
) (
SR
:
SimSymb.class
MR
) (
MP
:
Sound.class
)
:
program_relation.t
:=
program_relation.mk
(
fun
(
p_src
p_tgt
:
program
) =>
forall
(
WF
:
forall
x
(
IN
:
In
x
p_src
),
Sk.wf
x
),
exists
pp
,
(<<
SIMS
: @
ProgPair.sim
MR
SR
MP
pp
>>)
/\ (<<
SRCS
:
pp
.(
ProgPair.src
) =
p_src
>>)
/\ (<<
TGTS
:
pp
.(
ProgPair.tgt
) =
p_tgt
>>))
_
_
_
.
Next Obligation.
exploit
REL0
;
eauto
. {
i
.
eapply
WF
.
rewrite
in_app_iff
.
eauto
. }
intro
T0
;
des
.
exploit
REL1
;
eauto
. {
i
.
eapply
WF
.
rewrite
in_app_iff
.
eauto
. }
intro
T1
;
des
.
clarify
.
unfold
ProgPair.sim
in
*.
rewrite
Forall_forall
in
*.
eexists
(
_
++
_
).
esplits
;
eauto
.
-
rewrite
Forall_forall
in
*.
i
.
rewrite
in_app_iff
in
*.
des
; [
apply
SIMS
|
apply
SIMS0
];
eauto
.
-
unfold
ProgPair.src
.
rewrite
map_app
.
ss
.
-
unfold
ProgPair.tgt
.
rewrite
map_app
.
ss
.
Qed.
Next Obligation.
destruct
(
classic
(
forall
x
(
IN
:
In
x
p_src
),
Sk.wf
x
))
as
[
WF
|
NWF
];
cycle
1.
{
eapply
sk_nwf_improves
;
auto
. }
eapply
bsim_improves
.
eapply
mixed_to_backward_simulation
.
specialize
(
REL
WF
).
des
.
clarify
.
eapply
(@
adequacy_local
MR
SR
MP
).
auto
.
Qed.
Next Obligation.
exists
[].
splits
;
ss
. Qed.
Definition
relate_single
(
MR
:
SimMem.class
) (
SR
:
SimSymb.class
MR
) (
MP
:
Sound.class
)
(
p_src
p_tgt
:
Mod.t
) :
Prop
:=
forall
(
WF
:
Sk.wf
p_src
),
exists
mp
,
(<<
SIM
: @
ModPair.sim
MR
SR
MP
mp
>>)
/\ (<<
SRC
:
mp
.(
ModPair.src
) =
p_src
>>)
/\ (<<
TGT
:
mp
.(
ModPair.tgt
) =
p_tgt
>>).
Arguments
relate_single
:
clear
implicits
.
Lemma
relate_single_program
MR
SR
MP
p_src
p_tgt
(
REL
:
relate_single
MR
SR
MP
p_src
p_tgt
):
(
mkPR
MR
SR
MP
) [
p_src
] [
p_tgt
].
Proof.
unfold
relate_single
.
ss
.
i
.
exploit
REL
; [
ss
;
eauto
|].
i
.
des
.
clarify
.
exists
[
mp
].
esplits
;
ss
;
eauto
.
Qed.
Arguments
relate_single_program
:
clear
implicits
.
Lemma
relate_each_program
MR
SR
MP
(
p_src
p_tgt
:
program
)
(
REL
:
Forall2
(
relate_single
MR
SR
MP
)
p_src
p_tgt
):
(
mkPR
MR
SR
MP
)
p_src
p_tgt
.
Proof.
revert
p_tgt
REL
.
induction
p_src
;
ss
;
i
.
-
inv
REL
.
exists
[];
splits
;
ss
.
-
inv
REL
.
exploit
IHp_src
;
eauto
.
i
.
des
.
exploit
H1
;
eauto
.
i
.
des
.
clarify
.
exists
(
mp
::
pp
);
splits
;
ss
.
econs
;
eauto
.
Qed.
Arguments
relate_each_program
:
clear
implicits
.
Lemma
relate_single_rtc_rusc
(
R
:
program_relation.t
->
Prop
)
MR
SR
MP
(
p_src
p_tgt
:
Mod.t
)
(
REL
:
rtc
(
relate_single
MR
SR
MP
)
p_src
p_tgt
)
(
RELIN
:
R
(
mkPR
MR
SR
MP
)):
rusc
R
[
p_src
] [
p_tgt
].
Proof.
induction
REL
;
try
refl
.
-
etrans
;
eauto
.
eapply
rusc_incl
;
eauto
.
eapply
relate_single_program
;
eauto
.
Qed.
Arguments
relate_single_program
:
clear
implicits
.
Lemma
relate_single_rusc
(
R
:
program_relation.t
->
Prop
)
MR
SR
MP
(
p_src
p_tgt
:
Mod.t
)
(
REL
: (
relate_single
MR
SR
MP
)
p_src
p_tgt
)
(
RELIN
:
R
(
mkPR
MR
SR
MP
)):
rusc
R
[
p_src
] [
p_tgt
].
Proof.
eapply
relate_single_rtc_rusc
;
eauto
.
eapply
rtc_once
.
eauto
.
Qed.
Arguments
relate_single_program
:
clear
implicits
.