Skip to content
GitLab
Menu
Projects
Groups
Snippets
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
261e8146
Commit
261e8146
authored
Jul 03, 2019
by
Hai Dang
Browse files
WIP: public read
parent
d8608ad6
Changes
2
Hide whitespace changes
Inline
Sidebyside
theories/sim/cmra.v
View file @
261e8146
...
...
@@ 182,8 +182,5 @@ Qed.
Lemma
ptrmap_lookup_core_pub
(
pm
:
ptrmapUR
)
t
h
:
pm
!!
t
≡
Some
(
to_tagKindR
tkPub
,
h
)
→
(
pm
⋅
core
pm
)
!!
t
≡
Some
(
to_tagKindR
tkPub
,
h
).
Proof
.
intros
Eq
.
rewrite
lookup_op
lookup_core
Eq
/
core
/=
.
rewrite
core_id
.
by
rewrite

Some_op
pair_op
Cinr_op
agree_idemp

(
heaplet_core
h
)

cmra_core_dup
.
Qed
.
core
pm
!!
t
≡
Some
(
to_tagKindR
tkPub
,
h
).
Proof
.
intros
Eq
.
rewrite
lookup_core
Eq
/
core
/=
core_id
//. Qed.
theories/sim/one_step.v
View file @
261e8146
...
...
@@ 270,7 +270,7 @@ Proof.
destruct
SREL
as
(
Eqst
&
Eqnp
&
Eqcs
&
Eqnc
&
PRIV
).
destruct
(
read_mem_values
_
_
_
_
Eqvs
)
as
[
Eqls
HLs
].
destruct
(
read_mem_values
_
_
_
_
Eqvt
)
as
[
Eqlt
HLt
].
(
*
apply
Forall2_same_length_lookup
.
split
;
[
by
rewrite
Eqls
Eqlt

].
apply
Forall2_same_length_lookup
.
split
;
[
by
rewrite
Eqls
Eqlt

].
intros
i
ss
st
Hss
Hst
.
have
HLLs
:=
lookup_lt_Some
_
_
_
Hss
.
have
HLLt
:=
lookup_lt_Some
_
_
_
Hst
.
rewrite

Eqls
in
HLs
.
specialize
(
HLs
_
HLLs
).
rewrite
Hss
in
HLs
.
...
...
@@ 279,8 +279,10 @@ Proof.
{
rewrite
HLs
in
Eqss
'
.
symmetry
in
Eqss
'
.
simplify_eq
.
move
:
AREL
.
destruct
ss
as
[


l1
[
t1

]

],
st
as
[


l2
[
t2

]

];
auto
;
simpl
;
[

by
intros
[
?
[]]].
intros
[
?
[
?
[
h
'
Eqh
'
]]].
simplify_eq
.
do
2
(
split
;
[
done

]).
admit
.
}
destruct
PV
as
(
c
'
&
T
'
&
h
'
&
Eqci
&
InT
'
).
*
)
exists
h
'
.
by
apply
ptrmap_lookup_core_pub
.
}
destruct
PV
as
(
c
'
&
T
'
&
h
'
&
Eqci
&
InT
'
).
(
*
impossible
:
t
'
is
protected
by
c
'
which
is
still
active
.
So
t
≠
t
'
and
protected
(
t
'
,
c
'
)
is
on
top
of
(
l
+
ₗ
i
),
so
access
with
t
is
UB
*
)
admit
.
}
exists
(
Val
vs
),
σ
s
'
,
(
r
⋅
(
core
(
r_f
⋅
r
))),
(
S
n
).
split
;
last
split
.
...
...
Write
Preview
Supports
Markdown
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