Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
FP
Stacked Borrows Coq
Commits
2bc85deb
Commit
2bc85deb
authored
Jul 09, 2019
by
Hai Dang
Browse files
complete copy public
parent
0c31420a
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
40 additions
and
322 deletions
+40
322
theories/lang/steps_retag.v
theories/lang/steps_retag.v
+23
0
theories/sim/refl_mem_step.v
theories/sim/refl_mem_step.v
+17
322
No files found.
theories/lang/steps_retag.v
View file @
2bc85deb
...
@@ 99,6 +99,29 @@ Proof.
...
@@ 99,6 +99,29 @@ Proof.
intros
i
Lt
Eq
.
apply
NEql
.
by
rewrite
Eq
.
intros
i
Lt
Eq
.
apply
NEql
.
by
rewrite
Eq
.
Qed
.
Qed
.
Lemma
for_each_access1_lookup_inv
α
cids
l
n
tg
kind
α'
:
for_each
α
l
n
false
(
λ
stk
,
nstk
'
←
access1
stk
kind
tg
cids
;
Some
nstk
'
.2
)
=
Some
α'
→
∀
l
stk
,
α
!!
l
=
Some
stk
→
∃
stk
'
,
α'
!!
l
=
Some
stk
'
∧
((
∃
n
'
,
access1
stk
kind
tg
cids
=
Some
(
n
'
,
stk
'
))
∨
α'
!!
l
=
α
!!
l
).
Proof
.
intros
EQ
.
destruct
(
for_each_lookup
_
_
_
_
_
EQ
)
as
[
EQ1
[
EQ2
EQ3
]].
intros
l1
stk1
Eq1
.
case
(
decide
(
l1
.1
=
l
.1
))
=>
[
Eql

NEql
];
[
case
(
decide
(
l
.2
≤
l1
.2
<
l
.2
+
n
))
=>
[[
Le
Lt
]

NIN
]

].

have
Eql2
:
l1
=
l
+
ₗ
Z
.
of_nat
(
Z
.
to_nat
(
l1
.2

l
.2
)).
{
destruct
l
,
l1
.
move
:
Eql
Le
=>
/=
>
?
.
rewrite
/
shift_loc
/=
Z2Nat
.
id
;
[

lia
].
f_equal
.
lia
.
}
destruct
(
EQ1
(
Z
.
to_nat
(
l1
.2

l
.2
))
stk1
)
as
[
stk
[
Eq
[[
n1
stk
'
]
[
Eq
'
Eq0
]]
%
bind_Some
]];
[
rewrite

(
Nat2Z
.
id
n
)

Z2Nat
.
inj_lt
;
lia

by
rewrite

Eql2

].
simpl
in
Eq0
.
simplify_eq
.
rewrite

Eql2
in
Eq
.
naive_solver
.

rewrite
EQ3
;
[
naive_solver

].
intros
i
Lt
Eq
.
apply
NIN
.
rewrite
Eq
/=
.
lia
.

rewrite
EQ3
;
[
naive_solver

].
intros
i
Lt
Eq
.
apply
NEql
.
by
rewrite
Eq
.
Qed
.
(
**
Head
preserving
*
)
(
**
Head
preserving
*
)
Definition
is_stack_head
(
it
:
item
)
(
stk
:
stack
)
:=
Definition
is_stack_head
(
it
:
item
)
(
stk
:
stack
)
:=
...
...
theories/sim/refl_mem_step.v
View file @
2bc85deb
...
@@ 320,18 +320,22 @@ Proof.
...
@@ 320,18 +320,22 @@ Proof.
intros
[
Eq1
?
]
%
Some_equiv_inj
.
by
inversion
Eq1
.
intros
[
Eq1
?
]
%
Some_equiv_inj
.
by
inversion
Eq1
.
Qed
.
Qed
.
Lemma
local_access_eq
r
l
t
t
'
stk
kind
σ
s
σ
t
:
Lemma
local_access_eq
r
l
t
t
'
stk
n
stk
'
kind
σ
s
σ
t
:
σ
t
.(
sst
)
!!
l
=
Some
stk
→
σ
t
.(
sst
)
!!
l
=
Some
stk
→
is_Some
(
access1
stk
kind
t
'
σ
t
.(
scs
))
→
access1
stk
kind
t
'
σ
t
.(
scs
)
=
Some
(
n
,
stk
'
)
→
wsat
r
σ
s
σ
t
→
wsat
r
σ
s
σ
t
→
(
r
.(
rlm
)
!!
l
:
optionR
tagR
)
≡
Some
(
to_tagR
t
)
→
(
r
.(
rlm
)
!!
l
:
optionR
tagR
)
≡
Some
(
to_tagR
t
)
→
t
'
=
Tagged
t
.
t
'
=
Tagged
t
∧
stk
'
=
stk
.
Proof
.
Proof
.
intros
Eql
[[
n
stk
'
]
Eqstk
]
WSAT
Eqt
'
.
intros
Eql
Eqstk
WSAT
Eqt
'
.
destruct
WSAT
as
(
WFS
&
WFT
&
VALID
&
PINV
&
CINV
&
SREL
&
LINV
).
destruct
WSAT
as
(
WFS
&
WFT
&
VALID
&
PINV
&
CINV
&
SREL
&
LINV
).
specialize
(
LINV
_
_
Eqt
'
)
as
[
?
[
Eqs
?
]].
rewrite
Eql
in
Eqs
.
simplify_eq
.
specialize
(
LINV
_
_
Eqt
'
)
as
[
?
[
Eqs
?
]].
rewrite
Eql
in
Eqs
.
simplify_eq
.
apply
access1_in_stack
in
Eqstk
as
[
it
[
?%
elem_of_list_singleton
Eqt
]].
destruct
(
access1_in_stack
_
_
_
_
_
_
Eqstk
)
by
subst
.
as
[
it
[
?%
elem_of_list_singleton
Eqt
]].
subst
.
split
;
[
done

].
destruct
(
tag_unique_head_access
σ
t
.(
scs
)
(
init_stack
(
Tagged
t
))
t
None
kind
)
as
[
stk1
Eq1
];
[
by
exists
[]

].
rewrite
Eq1
in
Eqstk
.
by
simplify_eq
.
Qed
.
Qed
.
Lemma
priv_loc_UB_access_eq
r
l
kind
σ
s
σ
t
t
t
'
stk
:
Lemma
priv_loc_UB_access_eq
r
l
kind
σ
s
σ
t
t
t
'
stk
:
...
@@ 342,7 +346,7 @@ Lemma priv_loc_UB_access_eq r l kind σs σt t t' stk :
...
@@ 342,7 +346,7 @@ Lemma priv_loc_UB_access_eq r l kind σs σt t t' stk :
t
'
=
Tagged
t
.
t
'
=
Tagged
t
.
Proof
.
Proof
.
intros
Eql
ACC
WSAT
(
h
&
Eqh
&
[
LOC

PRO
]).
intros
Eql
ACC
WSAT
(
h
&
Eqh
&
[
LOC

PRO
]).
{
eapply
local_access_eq
;
eauto
.
}
{
destruct
ACC
as
[[]].
eapply
local_access_eq
;
eauto
.
}
destruct
WSAT
as
(
WFS
&
WFT
&
VALID
&
PINV
&
CINV
&
SREL
&
LINV
).
destruct
WSAT
as
(
WFS
&
WFT
&
VALID
&
PINV
&
CINV
&
SREL
&
LINV
).
specialize
(
PINV
_
_
_
Eqh
)
as
[
Lt
PINV
].
specialize
(
PINV
_
_
_
Eqh
)
as
[
Lt
PINV
].
destruct
PRO
as
(
c
&
T
&
Eqc
&
InT
&
Inl
).
have
Inl
'
:=
Inl
.
destruct
PRO
as
(
c
&
T
&
Eqc
&
InT
&
Inl
).
have
Inl
'
:=
Inl
.
...
@@ 494,15 +498,17 @@ Proof.
...
@@ 494,15 +498,17 @@ Proof.

intros
l1
t1
.
simpl
.
intros
Eqs
.

intros
l1
t1
.
simpl
.
intros
Eqs
.
specialize
(
LINV
_
_
Eqs
)
as
(
LTi
&
Eqst
&
Eqhs
).
specialize
(
LINV
_
_
Eqs
)
as
(
LTi
&
Eqst
&
Eqhs
).
split
;
[
done

].
split
;
[

done
].
split
;
[
done

].
split
;
[

done
].
admit
.
destruct
(
for_each_access1_lookup_inv
_
_
_
_
_
_
_
Eq
α'
_
_
Eqst
)
(
*
destruct
(
for_each_access1
_
_
_
_
_
_
_
Eq
α'
_
_
Eqstk
'
)
as
(
stk2
&
Eq2
&
LOR
).
as
(
stk
&
Eqstk
&
SUB
&
?
).
*
)
}
destruct
LOR
as
[[
n
'
ACC1
]

LOR
];
[

by
rewrite
LOR
].
destruct
(
local_access_eq
_
_
_
_
_
_
_
_
_
_
Eqst
ACC1
WSAT1
Eqs
)
as
[
?
Eqstk2
].
by
rewrite
Eq2
Eqstk2
.
}
left
.
left
.
apply:
sim_body_result
.
intros
.
apply:
sim_body_result
.
intros
.
have
VREL2
:
vrel
(
r
⋅
(
core
(
r_f
⋅
r
)))
vs
vt
.
have
VREL2
:
vrel
(
r
⋅
(
core
(
r_f
⋅
r
)))
vs
vt
.
{
eapply
vrel_mono
;
[
done


exact
VREL
'
].
apply
cmra_included_r
.
}
{
eapply
vrel_mono
;
[
done


exact
VREL
'
].
apply
cmra_included_r
.
}
eapply
POST
;
eauto
.
eapply
POST
;
eauto
.
Admitt
ed
.
Q
ed
.
(
**
Write
*
)
(
**
Write
*
)
(
*
Fixpoint
write_heaplet
(
l
:
loc
)
(
v
:
value
)
(
h
:
gmapR
loc
(
agreeR
scalarC
))
:=
(
*
Fixpoint
write_heaplet
(
l
:
loc
)
(
v
:
value
)
(
h
:
gmapR
loc
(
agreeR
scalarC
))
:=
...
@@ 1059,317 +1065,6 @@ Proof.
...
@@ 1059,317 +1065,6 @@ Proof.
intros
.
simpl
.
by
apply
POST
.
intros
.
simpl
.
by
apply
POST
.
Abort
.
Abort
.
Lemma
sim_body_write_related_values
fs
ft
(
r
:
resUR
)
k0
h0
n
l
tg
Ts
Tt
v
σ
s
σ
t
Φ
(
EQS
:
tsize
Ts
=
tsize
Tt
)
(
Eqtg
:
r
.(
rtm
)
!!
tg
=
Some
(
to_tagKindR
k0
,
h0
))
(
NONLOCAL
:
if
k0
then
∀
i
,
(
i
<
tsize
Tt
)
%
nat
→
r
.(
rlm
)
!!
(
l
+
ₗ
i
)
=
None
else
True
)
(
*
assuming
to

write
values
are
related
*
)
(
PUBWRITE
:
∀
s
,
s
∈
v
→
arel
r
s
s
)
:
let
r
'
:=
if
k0
then
((
<
[
tg
:=
(
to_tagKindR
tkUnique
,
write_heaplet
l
v
h0
)]
>
r
.(
rtm
),
r
.(
rcm
)),
r
.(
rlm
))
else
r
in
(
∀
α'
,
memory_written
σ
t
.(
sst
)
σ
t
.(
scs
)
l
(
Tagged
tg
)
(
tsize
Tt
)
=
Some
α'
→
let
σ
s
'
:=
mkState
(
write_mem
l
v
σ
s
.(
shp
))
α'
σ
s
.(
scs
)
σ
s
.(
snp
)
σ
s
.(
snc
)
in
let
σ
t
'
:=
mkState
(
write_mem
l
v
σ
t
.(
shp
))
α'
σ
t
.(
scs
)
σ
t
.(
snp
)
σ
t
.(
snc
)
in
Φ
r
'
n
(
ValR
[
☠
]
%
S
)
σ
s
'
(
ValR
[
☠
]
%
S
)
σ
t
'
:
Prop
)
→
r
⊨
{
n
,
fs
,
ft
}
(
Place
l
(
Tagged
tg
)
Ts
<
#
v
,
σ
s
)
≥
(
Place
l
(
Tagged
tg
)
Tt
<
#
v
,
σ
t
)
:
Φ
.
Proof
.
intros
r
'
POST
.
pfold
.
intros
NT
.
intros
.
have
WSAT1
:=
WSAT
.
destruct
WSAT
as
(
WFS
&
WFT
&
VALID
&
PINV
&
CINV
&
SREL
&
LINV
).
split
;
[

done

].
{
right
.
edestruct
NT
as
[[]

[
es
'
[
σ
s
'
STEPS
]]];
[
constructor
1

done

].
destruct
(
tstep_write_inv
_
(
PlaceR
_
_
_
)
(
ValR
_
)
_
_
_
STEPS
)
as
(
?&?&?&?&
α'
&
EqH
&
EqH
'
&
?
&
Eq
α'
&
EqD
&
IN
&
EQL
&
?
).
symmetry
in
EqH
,
EqH
'
.
simplify_eq
.
setoid_rewrite
<
(
srel_heap_dom
_
_
_
WFS
WFT
SREL
)
in
EqD
.
destruct
SREL
as
(
Eqst
&
Eqnp
&
Eqcs
&
Eqnc
&
AREL
).
rewrite
Eqst
Eqcs
EQS
in
Eq
α'
.
rewrite

EQL
in
EQS
.
rewrite
EQS
in
EqD
.
rewrite
Eqnp
in
IN
.
exists
(#[
☠
])
%
V
,
(
mkState
(
write_mem
l
v
σ
t
.(
shp
))
α'
σ
t
.(
scs
)
σ
t
.(
snp
)
σ
t
.(
snc
)).
by
eapply
(
head_step_fill_tstep
_
[]),
write_head_step
'
.
}
constructor
1.
intros
.
destruct
(
tstep_write_inv
_
(
PlaceR
_
_
_
)
(
ValR
_
)
_
_
_
STEPT
)
as
(
?&?&?&?&
α'
&
EqH
&
EqH
'
&
?
&
Eq
α'
&
EqD
&
IN
&
EQL
&
?
).
symmetry
in
EqH
,
EqH
'
.
simplify_eq
.
set
σ
s
'
:=
mkState
(
write_mem
l
v
σ
s
.(
shp
))
α'
σ
s
.(
scs
)
σ
s
.(
snp
)
σ
s
.(
snc
).
have
STEPS
:
((
Place
l
(
Tagged
tg
)
Ts
<
v
)
%
E
,
σ
s
)
~{
fs
}~>
((#[
☠
])
%
V
,
σ
s
'
).
{
setoid_rewrite
(
srel_heap_dom
_
_
_
WFS
WFT
SREL
)
in
EqD
.
destruct
SREL
as
(
Eqst
&
Eqnp
&
Eqcs
&
Eqnc
&
AREL
).
rewrite

Eqst

Eqcs

EQS
in
Eq
α'
.
rewrite

EQS
in
EQL
.
rewrite
EQL
in
EqD
.
rewrite

Eqnp
in
IN
.
eapply
(
head_step_fill_tstep
_
[]),
write_head_step
'
;
eauto
.
}
have
HL
:
if
k0
then
∀
kh
,
r_f
.(
rtm
)
⋅
<
[
tg
:=
kh
]
>
r
.(
rtm
)
=
<
[
tg
:=
kh
]
>
(
r_f
.(
rtm
)
⋅
r
.(
rtm
))
else
True
.
{
destruct
k0
;
[

done
].
intros
.
rewrite
(
tmap_insert_op_r
r_f
.(
rtm
)
r
.(
rtm
)
tg
h0
)
//. apply VALID. }
have
HL2
:
if
k0
then
(
r_f
.(
rtm
)
⋅
r
.(
rtm
))
!!
tg
=
Some
(
to_tagKindR
tkUnique
,
h0
)
else
True
.
{
destruct
k0
;
[

done
].
by
apply
(
tmap_lookup_op_r
_
_
_
_
(
proj1
(
proj1
VALID
))
Eqtg
).
}
have
SHR
:
∀
i
,
(
i
<
tsize
Tt
)
%
nat
→
(
r_f
⋅
r
).(
rlm
)
!!
(
l
+
ₗ
i
)
≡
Some
$
to_locStateR
lsShared
.
{
destruct
k0
.

intros
i
Lt
.
specialize
(
NONLOCAL
_
Lt
).
apply
lmap_lookup_op_r
;
[
apply
VALID

done
].

eapply
public_access_not_local
;
eauto
.
rewrite
Eqtg
.
by
eexists
.
}
clear
WSAT1
.
exists
(#[
☠
])
%
V
,
σ
s
'
,
r
'
,
n
.
split
;
last
split
.
{
left
.
by
constructor
1.
}
{
have
Eqrlm
:
(
r_f
⋅
r
'
).(
rlm
)
≡
(
r_f
⋅
r
).(
rlm
)
by
destruct
k0
.
destruct
(
for_each_lookup
_
_
_
_
_
Eq
α'
)
as
[
EQ1
EQ2
].
split
;
last
split
;
last
split
;
last
split
;
last
split
;
last
split
.

by
apply
(
tstep_wf
_
_
_
STEPS
WFS
).

by
apply
(
tstep_wf
_
_
_
STEPT
WFT
).

(
*
valid
*
)
rewrite
/
r
'
.
destruct
k0
;
[

done
].
do
2
(
split
;
[

apply
VALID
]).
eapply
tmap_valid
;
eauto
;
[

apply
VALID
].
split
;
[
done

].
apply
write_heaplet_valid
.
have
VL
:=
(
proj1
(
proj1
(
cmra_valid_op_r
_
_
VALID
))
tg
).
rewrite
Eqtg
in
VL
.
apply
VL
.

(
*
tmap_inv
*
)
intros
t
k
h
Eqt
.
have
Eqttg
:
t
=
tg
→
k0
=
tkUnique
→
k
=
k0
∧
h
≡
write_heaplet
l
v
h0
.
{
intros
.
subst
t
k0
.
move
:
Eqt
.
rewrite
/
rtm
/=
HL
lookup_insert
.
intros
[
Eq1
Eq2
]
%
Some_equiv_inj
.
simpl
in
Eq1
,
Eq2
.
rewrite
Eq2
.
repeat
split
;
[

done
].
destruct
k
;
[
done

inversion
Eq1
].
}
have
CASEt
:
(
t
=
tg
∧
k0
=
tkUnique
∧
k
=
k0
∧
h
≡
write_heaplet
l
v
h0
∨
(
r_f
⋅
r
).(
rtm
)
!!
t
≡
Some
(
to_tagKindR
k
,
h
)
∧
(
k
=
tkUnique
→
t
≠
tg
)).
{
move
:
Eqt
.
rewrite
/
r
'
.
destruct
k0
;
simpl
.

rewrite
/
rtm
/=
HL
.
case
(
decide
(
t
=
tg
))
=>
?
;
[
subst
t

rewrite
lookup_insert_ne
//].
+
left
.
by
destruct
Eqttg
.
+
right
.
naive_solver
.

case
(
decide
(
t
=
tg
))
=>
?
;
[
subst
t

].
+
intros
Eqt
.
right
.
split
;
[
done

].
intros
?
.
subst
k
.
move
:
Eqt
.
rewrite
lookup_op
Eqtg
.
by
move
=>
/
tagKindR_exclusive_2
.
+
right
.
naive_solver
.
}
split
.
{
simpl
.
destruct
CASEt
as
[(
?&?&?&?
Eqh
)

[
Eqh
NEQ
]].

subst
t
k
k0
.
apply
(
PINV
tg
tkUnique
h0
).
by
rewrite
HL2
.

move
:
Eqh
.
apply
PINV
.
}
intros
l
'
s
'
Eqk
'
.
split
.
{
destruct
CASEt
as
[(
?&?&?&?
Eqh
)

[
Eqh
NEQ
]].

subst
t
k
k0
.
destruct
(
PINV
tg
tkUnique
h0
)
as
[
?
PI
];
[
by
rewrite
HL2

].
have
InD
'
:
l
'
∈
dom
(
gset
loc
)
h
.
{
rewrite
elem_of_dom
.
destruct
(
h
!!
l
'
)
eqn
:
Eql
'
;
rewrite
Eql
'
;
[
by
eexists

by
inversion
Eqk
'
].
}
move
:
InD
'
.
rewrite
Eqh
write_heaplet_dom
elem_of_dom
.
intros
[
s0
Eqs0
].
have
VALS
:=
proj1
(
proj1
(
cmra_valid_op_r
_
_
VALID
))
tg
.
rewrite
Eqtg
in
VALS
.
have
VALs0
:
✓
s0
.
{
change
(
✓
(
Some
s0
)).
rewrite

Eqs0
.
apply
VALS
.
}
apply
to_agree_uninj
in
VALs0
as
[
ss0
Eqss0
].
destruct
(
PI
l
'
ss0
)
as
[
?
_
];
[

done
].
by
rewrite
Eqs0
Eqss0
.

specialize
(
PINV
_
_
_
Eqh
)
as
[
?
PINV
].
specialize
(
PINV
_
_
Eqk
'
)
as
[
EQ
_
].
rewrite
/
r
'
/=
.
by
destruct
k0
.
}
intros
stk
'
.
simpl
.
destruct
(
write_mem_lookup_case
l
v
σ
t
.(
shp
)
l
'
)
as
[[
i
[
Lti
[
Eqi
Eqmi
]]]

[
NEql
Eql
]];
last
first
.
{
(
*
l
'
is
NOT
written
to
*
)
destruct
(
for_each_lookup
_
_
_
_
_
Eq
α'
)
as
[
_
[
_
EQ
]].
rewrite
EQL
in
NEql
.
rewrite
(
EQ
_
NEql
)
Eql
.
destruct
CASEt
as
[(
?&?&?&?
Eqh
)

[
Eqh
?
]];
[

by
apply
(
PINV
t
k
h
Eqh
)].
subst
t
k
k0
.
apply
(
PINV
tg
tkUnique
h0
).

by
rewrite
HL2
.

move
:
Eqk
'
.
rewrite
Eqh
.
rewrite

EQL
in
NEql
.
by
rewrite
(
proj2
(
write_heaplet_lookup
l
v
h0
)
_
NEql
).
}
(
*
l
'
is
written
to
*
)
intros
Eqstk
'
pm
opro
In
'
NDIS
.
subst
l
'
.
destruct
(
for_each_access1
_
_
_
_
_
_
_
Eq
α'
_
_
Eqstk
'
)
as
(
stk
&
Eqstk
&
SUB
&
?
).
destruct
(
SUB
_
In
'
)
as
(
it2
&
In2
&
Eqt2
&
Eqp2
&
NDIS2
).
simpl
in
*
.
destruct
CASEt
as
[(
?&?&?&?
Eqh
)

[
Eqh
NEQ
]].
+
(
*
t
=
tg
*
)
subst
t
k
k0
.
rewrite
>
Eqh
in
Eqk
'
.
split
.
*
have
Eqs
'
:=
proj1
(
write_heaplet_lookup
l
v
h0
)
_
_
Lti
Eqk
'
.
rewrite
(
proj1
(
write_mem_lookup
l
v
σ
t
.(
shp
))
_
Lti
).
destruct
(
v
!!
i
)
as
[
s
''

]
eqn
:
Eq
''
;
[
rewrite
Eq
''

by
inversion
Eqs
'
].
apply
Some_equiv_inj
,
to_agree_inj
in
Eqs
'
.
by
inversion
Eqs
'
.
*
assert
(
∃
s0
:
scalar
,
h0
!!
(
l
+
ₗ
i
)
≡
Some
(
to_agree
s0
))
as
[
s0
Eq0
].
{
assert
(
is_Some
(
h0
!!
(
l
+
ₗ
i
)))
as
[
s0
Eqs0
].
{
rewrite

(
elem_of_dom
(
D
:=
gset
loc
))

(
write_heaplet_dom
l
v
h0
).
move
:
Eqk
'
.
destruct
(
write_heaplet
l
v
h0
!!
(
l
+
ₗ
i
))
eqn
:
Eq
''
;
rewrite
Eq
''
;
[
intros
_

by
inversion
1
].
apply
(
elem_of_dom_2
_
_
_
Eq
''
).
}
rewrite
Eqs0
.
destruct
(
to_agree_uninj
s0
)
as
[
s1
Eq1
];
[

by
exists
s1
;
rewrite

Eq1
].
apply
(
lookup_valid_Some
h0
(
l
+
ₗ
i
));
[

by
rewrite
Eqs0
].
apply
(
lookup_valid_Some
(
r_f
.(
rtm
)
⋅
r
.(
rtm
))
tg
(
to_tagKindR
tkUnique
,
h0
));
[
by
apply
(
proj1
VALID
)

by
rewrite
HL2
].
}
specialize
(
PINV
tg
tkUnique
h0
)
as
[
Lt
PI
];
[
by
rewrite
HL2

].
specialize
(
PI
_
_
Eq0
)
as
[
?
PI
].
specialize
(
PI
_
Eqstk
it2
.(
perm
)
opro
)
as
[
Eql
'
HTOP
].
{
rewrite
/=
Eqt2
Eqp2
.
by
destruct
it2
.
}
{
by
rewrite
(
NDIS2
NDIS
).
}
destruct
(
for_each_lookup_case
_
_
_
_
_
Eq
α'
_
_
_
Eqstk
Eqstk
'
)
as
[
?
[
MR
_
]];
[
by
subst

].
clear

In
'
MR
HTOP
Eqstk
WFT
NDIS
.
destruct
(
access1
stk
AccessWrite
(
Tagged
tg
)
σ
t
.(
scs
))
as
[[
n
stk1
]

]
eqn
:
Eqstk
'
;
[

done
].
simpl
in
MR
.
simplify_eq
.
destruct
(
state_wf_stack_item
_
WFT
_
_
Eqstk
).
move
:
Eqstk
'
HTOP
.
eapply
access1_head_preserving
;
eauto
.
+
(
*
invoke
PINV
for
t
*
)
exfalso
.
destruct
(
PINV
t
k
h
Eqh
)
as
[
Lt
PI
].
specialize
(
PI
_
_
Eqk
'
)
as
[
?
PI
].
specialize
(
PI
_
Eqstk
it2
.(
perm
)
opro
)
as
[
Eql
'
HTOP
].
{
rewrite
/=
Eqt2
Eqp2
.
by
destruct
it2
.
}
{
by
rewrite
(
NDIS2
NDIS
).
}
destruct
k
.
*
(
*
if
k
is
Unique
∧
t
≠
tg
,
writing
with
tg
must
have
popped
t
from
top
,
contradicting
In
'
.
*
)
rewrite
EQL
in
Lti
.
destruct
(
EQ1
_
_
Lti
Eqstk
)
as
[
ss
'
[
Eq
'
EQ3
]].
have
?:
ss
'
=
stk
'
.
{
rewrite
Eqstk
'
in
Eq
'
.
by
inversion
Eq
'
.
}
subst
ss
'
.
clear
Eq
'
.
move
:
EQ3
.
case
access1
as
[[
n1
stk1
]

]
eqn
:
EQ4
;
[

done
].
simpl
.
intros
?
.
simplify_eq
.
specialize
(
NEQ
eq_refl
).
have
ND
:=
proj2
(
state_wf_stack_item
_
WFT
_
_
Eqstk
).
move
:
In
'
.
eapply
(
access1_write_remove_incompatible_head
_
tg
t
_
_
_
ND
);
[
by
eexists

done
..].
*
(
*
if
k
is
Public
=>
t
is
for
SRO
,
and
must
also
have
been
popped
,
contradicting
In
'
.
*
)
rewrite
EQL
in
Lti
.
destruct
(
EQ1
_
_
Lti
Eqstk
)
as
[
ss
'
[
Eq
'
EQ3
]].
have
?:
ss
'
=
stk
'
.
{
rewrite
Eqstk
'
in
Eq
'
.
by
inversion
Eq
'
.
}
subst
ss
'
.
clear
Eq
'
.
move
:
EQ3
.
case
access1
as
[[
n1
stk1
]

]
eqn
:
EQ4
;
[

done
].
simpl
.
intros
?
.
simplify_eq
.
have
ND
:=
proj2
(
state_wf_stack_item
_
WFT
_
_
Eqstk
).
move
:
In
'
.
eapply
(
access1_write_remove_incompatible_active_SRO
_
tg
t
_
_
_
ND
);
eauto
.

(
*
cmap_inv
:
make
sure
tags
in
the
new
resource
are
still
on
top
*
)
intros
c
cs
Eqc
'
.
have
Eqc
:
(
r_f
⋅
r
).(
rcm
)
!!
c
≡
Some
cs
.
{
move
:
Eqc
'
.
rewrite
/
r
'
.
by
destruct
k0
.
}
specialize
(
CINV
_
_
Eqc
).
simpl
.
clear

Eq
α'
CINV
Eqtg
VALID
HL
HL2
.
destruct
cs
as
[[
T

]


];
[

done
..].
destruct
CINV
as
[
IN
CINV
].
split
;
[
done

].
intros
t
InT
.
specialize
(
CINV
_
InT
)
as
[
?
CINV
].
split
;
[
done

].
intros
k
h
.
(
*
TODO
:
duplicated
proofs
*
)
rewrite
/
r
'
.
destruct
k0
.
+
(
*
if
tg
was
unique
*
)
rewrite
/
rtm
/=
HL
.
case
(
decide
(
t
=
tg
))
=>
?
.
{
subst
tg
.
rewrite
lookup_insert
.
intros
[
Eqk
Eqh
]
%
Some_equiv_inj
.
simpl
in
Eqk
,
Eqh
.
have
Eqt
:
(
r_f
⋅
r
).(
rtm
)
!!
t
≡
Some
(
k
,
h0
)
by
rewrite
HL2

Eqk
.
intros
l
'
.
rewrite

Eqh
write_heaplet_dom
.
intros
Inh
.
destruct
(
CINV
_
_
Eqt
_
Inh
)
as
(
stk
'
&
pm
'
&
Eqstk
'
&
Instk
'
&
NDIS
).
destruct
(
for_each_access1_active_preserving
_
_
_
_
_
_
_
Eq
α'
_
_
Eqstk
'
)
as
[
stk
[
Eqstk
AS
]].
exists
stk
,
pm
'
.
split
;
last
split
;
[
done

by
apply
AS

done
].
}
{
rewrite
lookup_insert_ne
//.
intros
Eqt
l
'
Inh
.
destruct
(
CINV
_
_
Eqt
_
Inh
)
as
(
stk
'
&
pm
'
&
Eqstk
'
&
Instk
'
&
NDIS
).
destruct
(
for_each_access1_active_preserving
_
_
_
_
_
_
_
Eq
α'
_
_
Eqstk
'
)
as
[
stk
[
Eqstk
AS
]].
exists
stk
,
pm
'
.
split
;
last
split
;
[
done

by
apply
AS

done
].
}
+
(
*
if
tg
was
public
*
)
intros
Eqt
l
'
Inh
.
destruct
(
CINV
_
_
Eqt
_
Inh
)
as
(
stk
'
&
pm
'
&
Eqstk
'
&
Instk
'
&
NDIS
).
destruct
(
for_each_access1_active_preserving
_
_
_
_
_
_
_
Eq
α'
_
_
Eqstk
'
)
as
[
stk
[
Eqstk
AS
]].
exists
stk
,
pm
'
.
split
;
last
split
;
[
done

by
apply
AS

done
].

(
*
srel
*
)
rewrite
/
srel
/=
.
destruct
SREL
as
(
?&?&?&?&
EqDl
&
Eq
).
split
;
last
split
;
last
split
;
last
split
;
last
split
;
[
done
..


].
{
rewrite
write_mem_dom
// EqDl Eqrlm //. }
intros
l1
Eq1
.
destruct
(
write_mem_lookup
l
v
σ
s
.(
shp
))
as
[
EqN
EqO
].
rewrite
/
r
'
.
destruct
(
write_mem_lookup_case
l
v
σ
t
.(
shp
)
l1
)
as
[[
i
[
Lti
[
Eqi
Eqmi
]]]

[
NEql
Eql
]].
+
subst
l1
.
specialize
(
EqN
_
Lti
).
(
*
rewrite
EqN
.
*
)
have
InD
:=
(
EqD
_
Lti
).
rewrite
(
_
:
r_f
.2
⋅
r
'
.2
=
(
r_f
⋅
r
'
).(
rlm
))
// in Eq1.
rewrite
>
Eqrlm
in
Eq1
.
specialize
(
Eq
_
Eq1
).
destruct
(
lookup_lt_is_Some_2
_
_
Lti
)
as
[
s
Eqs
].
destruct
k0
.
*
(
*
tg
was
unique
,
and
(
l
+
ₗ
i
)
was
written
to
*
)
destruct
Eq
as
[
PB

[
t
PV
]].
{
left
.
intros
st
.
simpl
.
intros
Eqst
.
have
?:
st
=
s
.
{
rewrite
Eqmi
Eqs
in
Eqst
.
by
inversion
Eqst
.
}
subst
st
.
exists
s
.
rewrite
EqN
.
split
;
[
done

].
move
:
(
PUBWRITE
_
(
elem_of_list_lookup_2
_
_
_
Eqs
)).
rewrite
/
arel
/=
.
destruct
s
as
[


l0
t0

];
[
done
..


done
].
intros
[
?
[
?
Eqt0
]].
repeat
split
;
[
done
..

].
destruct
t0
as
[
t0

];
[

done
].
repeat
split
.
destruct
Eqt0
as
[
ht0
Eqt0
].
destruct
(
tmap_lookup_op_r_equiv_pub
r_f
.(
rtm
)
r
.(
rtm
)
_
_
(
proj1
(
proj1
VALID
))
Eqt0
)
as
[
h
'
Eq
'
].
exists
(
h
'
⋅
ht0
).
rewrite
/
rtm
/=
HL
lookup_insert_ne
//.
intros
?
;
subst
t0
.
rewrite
Eqtg
in
Eqt0
.
apply
Some_equiv_inj
in
Eqt0
as
[
Eqt0
_
].
inversion
Eqt0
.
}
{
destruct
PV
as
(
c
&
T
&
h
&
Eqc
&
InT
&
Eqt
&
Inh
).
right
.
exists
t
,
c
,
T
.
case
(
decide
(
t
=
tg
))
=>
?
;
[
subst
t

].

exists
(
write_heaplet
l
v
h0
).
do
2
(
split
;
[
done

]).
split
.
by
rewrite
/
rtm
/=
HL
lookup_insert
.
rewrite
write_heaplet_dom
.
rewrite
HL2
in
Eqt
.
apply
Some_equiv_inj
in
Eqt
as
[
?
Eqt
].
simpl
in
Eqt
.
by
rewrite
Eqt
.

exists
h
.
rewrite
/
rtm
/=
HL
.
do
2
(
split
;
[
done

]).
rewrite
lookup_insert_ne
//. }
*
(
*
tg
was
public
,
and
(
l
+
ₗ
i
)
was
written
to
*
)
left
.
intros
st
.
simpl
.
intros
Eqst
.
have
?:
st
=
s
.
{
rewrite
Eqmi
Eqs
in
Eqst
.
by
inversion
Eqst
.
}
subst
st
.
exists
s
.
rewrite
EqN
.
split
;
[
done

].
(
*
we
know
that
the
values
written
must
be
publicly
related
*
)
apply
(
arel_mono
r
_
VALID
).
{
apply
cmra_included_r
.
}
{
apply
PUBWRITE
,
(
elem_of_list_lookup_2
_
_
_
Eqs
).
}
+
specialize
(
EqO
_
NEql
).
(
*
have
InD1
'
:
l1
∈
dom
(
gset
loc
)
σ
t
.(
shp
)
by
rewrite
elem_of_dom

Eql

(
elem_of_dom
(
D
:=
gset
loc
)).
*
)
have
Eq1
'
:
(
r_f
⋅
r
).(
rlm
)
!!
l1
≡
Some
$
to_locStateR
lsShared
.
{
move
:
Eq1
.
by
destruct
k0
.
}
specialize
(
Eq
_
Eq1
'
).
rewrite
/
pub_loc
EqO
Eql
.
destruct
k0
;
[

done
].
destruct
Eq
as
[
PB

[
t
PV
]].
*
(
*
tg
was
unique
,
and
l1
was
NOT
written
to
*
)
left
.
intros
st
Eqst
.
destruct
(
PB
_
Eqst
)
as
[
ss
[
Eqss
AREL
]].
exists
ss
.
split
;
[
done

].
move
:
AREL
.
rewrite
/
arel
.
destruct
ss
as
[


l0
t0

],
st
as
[


l3
t3

];
try
done
.
intros
[
?
[
?
Eqt
]].
subst
l3
t3
.
repeat
split
.
destruct
t0
as
[
t0

];
[

done
].
destruct
Eqt
as
[
h
Eqt
].
exists
h
.
rewrite
/
rtm
/=
HL
(
lookup_insert_ne
_
tg
)
//.
intros
?
.
subst
t0
.
move
:
Eqt
.
rewrite
lookup_op
Eqtg
.
by
apply
tagKindR_exclusive
.
*
(
*
tg
was
public
,
and
l1
was
NOT
written
to
*
)
right
.
destruct
PV
as
(
c
&
T
&
h
&
Eqc
&
InT
&
Eqt
&
Inl
).
exists
t
,
c
,
T
.
simpl
.
case
(
decide
(
t
=
tg
))
=>
?
;
[
subst
t

].
{
eexists
(
write_heaplet
l
v
h0
).
rewrite
/
rtm
/=
HL
lookup_insert
.
repeat
split
;
[
done
..

].
rewrite
lookup_op
Eqtg
in
Eqt
.
by
rewrite
write_heaplet_dom
(
tagKindR_exclusive_heaplet
_
_
_
Eqt
).
}
{
exists
h
.
rewrite
/
rtm
/=
HL
lookup_insert_ne
//. }

intros
l
'
s
'
t
'
.
rewrite
Eqrlm
.
intros
Eq
.
rewrite
/=
.
specialize
(
LINV
_
_
_
Eq
)
as
(
?&?&?&?&
h
&
Eqh
).
destruct
(
write_mem_lookup
l
v
σ
s
.(
shp
))
as
[
_
HLs
].
destruct
(
write_mem_lookup
l
v
σ
t
.(
shp
))
as
[
_
HLt
].
have
NEQ
:
∀
i
,
(
i
<
length
v
)
%
nat
→
l
'
≠
l
+
ₗ
i
.
{
intros
i
Lti
EQ
.
rewrite
EQL
in
Lti
.
specialize
(
SHR
_
Lti
).
subst
l
'
.
move
:
Eq
.
rewrite
SHR
.
intros
Eqv
%
Some_equiv_inj
.
inversion
Eqv
.
}
destruct
EQ2
as
[
_
EQ2
].
rewrite
HLs
// HLt // EQ2 //; [rewrite EQL //].
do
4
(
split
;
[
done

]).
rewrite
/
r
'
.
destruct
k0
;
simpl
;
[

by
exists
h
].
setoid_rewrite
HL
.
case
(
decide
(
t
'
=
tg
))
=>
?
;
[
subst
t
'

].
rewrite
lookup_insert
.
by
eexists
.
rewrite
lookup_insert_ne
//. by eexists.
}
left
.
apply:
sim_body_result
.
intros
.
simpl
.
by
apply
POST
.
Qed
.
(
**
can
probably
be
derived
from
[
write_related_values
]
?
*
)
(
**
can
probably
be
derived
from
[
write_related_values
]
?
*
)
Lemma
sim_body_write_owned
Lemma
sim_body_write_owned
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment