Module SoundTop
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
ModSem
Skeleton
.
Require
Import
Sound
.
Require
Import
SemiLattice
.
Require
Import
FinFun
.
Set
Implicit
Arguments
.
Global
Program
Instance
Top
:
Sound.class
:= {
t
:=
unit
;
lepriv
:=
top2
;
wf
:=
top1
;
val
:=
top2
;
mem
:=
top2
;
mle
:=
top3
;
skenv
:=
top3
;
}.
Next Obligation.
esplits
;
eauto
.
econs
;
eauto
. Qed.
Next Obligation.
esplits
;
eauto
. Qed.
Require
Import
Preservation
.
Definition
sound_state
{
STATE
:
Type
}:
Sound.t
->
mem
->
STATE
->
Prop
:=
top3
.
Lemma
sound_state_local_preservation
:
forall
ms
,
<<
PRSV
:
local_preservation
ms
sound_state
>>.
Proof.
econs
;
ii
;
ss
;
eauto
.
{
esplits
;
eauto
.
rr
.
des_ifs
.
esplits
;
eauto
.
rr
.
rewrite
Forall_forall
.
ii
;
ss
. }
{
esplits
;
eauto
.
rr
.
des_ifs
. }
Unshelve
.
all
:
ss
.
Qed.