Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Lennard Gäher
Iris
Commits
3b36c1fe
Commit
3b36c1fe
authored
Apr 07, 2020
by
Ralf Jung
Browse files
rename gc -> inv_heap
parent
c271fd9a
Changes
2
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
3b36c1fe
...
...
@@ -82,9 +82,9 @@ theories/base_logic/lib/boxes.v
theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/gen_inv_heap.v
theories/base_logic/lib/fancy_updates_from_vs.v
theories/base_logic/lib/proph_map.v
theories/base_logic/lib/gc.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/weakestpre.v
...
...
theories/base_logic/lib/g
c
.v
→
theories/base_logic/lib/g
en_inv_heap
.v
View file @
3b36c1fe
...
...
@@ -3,152 +3,152 @@ From iris.base_logic.lib Require Import own invariants gen_heap.
From
iris
.
proofmode
Require
Import
tactics
.
Set
Default
Proof
Using
"Type"
.
(** A "GC" location is a location that can never be deallocated explicitly by
the program. It provides a persistent witness that will always allow reading
the location. The location is moreover associated with a (pure, Coq-level)
invariant determining which values are allowed to be stored in that location.
The persistent witness cannot know the exact value that will be read, but it
*can* know that the value satisfies the invariant.
(** An "invariant" location is a location that has some invariant about its
value attached to it, and that can never be deallocated explicitly by the
program. It provides a persistent witness that will always allow reading the
location, guaranteeing that the value read will satisfy the invariant.
This is useful for data structures like RDCSS that need to read locations long
after their ownership has been passed back to the client, but do not care *what*
it is that they are reading in that case.
it is that they are reading in that case. In that extreme case, the invariant
may just be [True].
Note that heap_lang does not actually have explicit dealloaction. However, the
proof rules we provide for heap operations currently are conservative in the
sense that they do not expose this fact. By making "GC" locations a separate
assertion, we can keep all the other proofs that do not need it conservative.
*)
Since invariant locations cannot be deallocated, they only make sense when
modelling languages with garbage collection. Note that heap_lang does not
actually have explicit dealloaction. However, the proof rules we provide for
heap operations currently are conservative in the sense that they do not expose
this fact. By making "invariant" locations a separate assertion, we can keep
all the other proofs that do not need it conservative. *)
Definition
gc
N
:
namespace
:
=
nroot
.@
"
gc
"
.
Definition
inv_heap
N
:
namespace
:
=
nroot
.@
"
inv_heap
"
.
Local
Notation
"l ↦ v"
:
=
(
mapsto
l
1
v
)
(
at
level
20
)
:
bi_scope
.
Definition
gc
_mapUR
(
L
V
:
Type
)
`
{
Countable
L
}
:
ucmraT
:
=
gmapUR
L
$
prodR
Definition
inv_heap
_mapUR
(
L
V
:
Type
)
`
{
Countable
L
}
:
ucmraT
:
=
gmapUR
L
$
prodR
(
optionR
$
exclR
$
leibnizO
V
)
(
agreeR
(
V
-
d
>
PropO
)).
Definition
to_
gc_m
ap
{
L
V
:
Type
}
`
{
Countable
L
}
(
gcm
:
gmap
L
(
V
*
(
V
-
d
>
PropO
)))
:
gc
_mapUR
L
V
:
=
prod_map
(
λ
x
,
Excl'
x
)
to_agree
<$>
gcm
.
Definition
to_
inv_he
ap
{
L
V
:
Type
}
`
{
Countable
L
}
(
h
:
gmap
L
(
V
*
(
V
-
d
>
PropO
)))
:
inv_heap
_mapUR
L
V
:
=
prod_map
(
λ
x
,
Excl'
x
)
to_agree
<$>
h
.
Class
gc
G
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
Gc
G
{
gc
_inG
:
>
inG
Σ
(
authR
(
gc
_mapUR
L
V
))
;
gc
_name
:
gname
Class
inv_heap
G
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
Inv_Heap
G
{
inv_heap
_inG
:
>
inG
Σ
(
authR
(
inv_heap
_mapUR
L
V
))
;
inv_heap
_name
:
gname
}.
Arguments
Gc
G
_
_
{
_
_
_
_
}.
Arguments
gc
_name
{
_
_
_
_
_
}
_
:
assert
.
Arguments
Inv_Heap
G
_
_
{
_
_
_
_
}.
Arguments
inv_heap
_name
{
_
_
_
_
_
}
_
:
assert
.
Class
gc
PreG
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
{
gc
_preG_inG
:
>
inG
Σ
(
authR
(
gc
_mapUR
L
V
))
Class
inv_heap
PreG
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
{
inv_heap
_preG_inG
:
>
inG
Σ
(
authR
(
inv_heap
_mapUR
L
V
))
}.
Definition
gc
Σ
(
L
V
:
Type
)
`
{
Countable
L
}
:
gFunctors
:
=
#[
GFunctor
(
authR
(
gc
_mapUR
L
V
))
].
Definition
inv_heap
Σ
(
L
V
:
Type
)
`
{
Countable
L
}
:
gFunctors
:
=
#[
GFunctor
(
authR
(
inv_heap
_mapUR
L
V
))
].
Instance
subG_
gc
PreG
(
L
V
:
Type
)
`
{
Countable
L
}
{
Σ
}
:
subG
(
gc
Σ
L
V
)
Σ
→
gc
PreG
L
V
Σ
.
Instance
subG_
inv_heap
PreG
(
L
V
:
Type
)
`
{
Countable
L
}
{
Σ
}
:
subG
(
inv_heap
Σ
L
V
)
Σ
→
inv_heap
PreG
L
V
Σ
.
Proof
.
solve_inG
.
Qed
.
Section
defs
.
Context
{
L
V
:
Type
}
`
{
Countable
L
}.
Context
`
{!
invG
Σ
,
!
gen_heapG
L
V
Σ
,
gG
:
!
gc
G
L
V
Σ
}.
Context
`
{!
invG
Σ
,
!
gen_heapG
L
V
Σ
,
gG
:
!
inv_heap
G
L
V
Σ
}.
Definition
gc
_inv_P
:
iProp
Σ
:
=
(
∃
gcm
:
gmap
L
(
V
*
(
V
-
d
>
PropO
)),
own
(
gc
_name
gG
)
(
●
to_
gc_map
gcm
)
∗
[
∗
map
]
l
↦
p
∈
gcm
,
⌜
p
.
2
p
.
1
⌝
∗
l
↦
p
.
1
)%
I
.
Definition
inv_heap
_inv_P
:
iProp
Σ
:
=
(
∃
h
:
gmap
L
(
V
*
(
V
-
d
>
PropO
)),
own
(
inv_heap
_name
gG
)
(
●
to_
inv_heap
h
)
∗
[
∗
map
]
l
↦
p
∈
h
,
⌜
p
.
2
p
.
1
⌝
∗
l
↦
p
.
1
)%
I
.
Definition
gc
_inv
:
iProp
Σ
:
=
inv
gcN
gc
_inv_P
.
Definition
inv_heap
_inv
:
iProp
Σ
:
=
inv
inv_heapN
inv_heap
_inv_P
.
Definition
gc
_mapsto
(
l
:
L
)
(
v
:
V
)
(
I
:
V
→
Prop
)
:
iProp
Σ
:
=
own
(
gc
_name
gG
)
(
◯
{[
l
:
=
(
Excl'
v
,
to_agree
I
)
]}).
Definition
inv
_mapsto
_own
(
l
:
L
)
(
v
:
V
)
(
I
:
V
→
Prop
)
:
iProp
Σ
:
=
own
(
inv_heap
_name
gG
)
(
◯
{[
l
:
=
(
Excl'
v
,
to_agree
I
)
]}).
Definition
i
s_gc_loc
(
l
:
L
)
(
I
:
V
→
Prop
)
:
iProp
Σ
:
=
own
(
gc
_name
gG
)
(
◯
{[
l
:
=
(
None
,
to_agree
I
)]}).
Definition
i
nv_mapsto
(
l
:
L
)
(
I
:
V
→
Prop
)
:
iProp
Σ
:
=
own
(
inv_heap
_name
gG
)
(
◯
{[
l
:
=
(
None
,
to_agree
I
)]}).
End
defs
.
(* [
gc
_inv] has no parameters to infer the types from, so we need to
(* [
inv_heap
_inv] has no parameters to infer the types from, so we need to
make them explicit. *)
Arguments
gc
_inv
_
_
{
_
_
_
_
_
_
}.
Arguments
inv_heap
_inv
_
_
{
_
_
_
_
_
_
}.
Instance
:
Params
(@
gc
_mapsto
)
8
:
=
{}.
Instance
:
Params
(@
gc
_mapsto
)
7
:
=
{}.
Instance
:
Params
(@
inv
_mapsto
_own
)
8
:
=
{}.
Instance
:
Params
(@
inv
_mapsto
)
7
:
=
{}.
Section
to_
gc_m
ap
.
Section
to_
inv_he
ap
.
Context
{
L
V
:
Type
}
`
{
Countable
L
}.
Implicit
Types
(
gcm
:
gmap
L
(
V
*
(
V
-
d
>
PropO
))).
Implicit
Types
(
h
:
gmap
L
(
V
*
(
V
-
d
>
PropO
))).
Lemma
to_
gc_m
ap_valid
gcm
:
✓
to_
gc_map
gcm
.
Proof
.
intros
l
.
rewrite
lookup_fmap
.
by
case
(
gcm
!!
l
).
Qed
.
Lemma
to_
inv_he
ap_valid
h
:
✓
to_
inv_heap
h
.
Proof
.
intros
l
.
rewrite
lookup_fmap
.
by
case
(
h
!!
l
).
Qed
.
Lemma
to_
gc_m
ap_singleton
l
v
I
:
to_
gc_m
ap
{[
l
:
=
(
v
,
I
)]}
=@{
gc
_mapUR
L
V
}
{[
l
:
=
(
Excl'
v
,
to_agree
I
)]}.
Proof
.
by
rewrite
/
to_
gc_m
ap
fmap_insert
fmap_empty
.
Qed
.
Lemma
to_
inv_he
ap_singleton
l
v
I
:
to_
inv_he
ap
{[
l
:
=
(
v
,
I
)]}
=@{
inv_heap
_mapUR
L
V
}
{[
l
:
=
(
Excl'
v
,
to_agree
I
)]}.
Proof
.
by
rewrite
/
to_
inv_he
ap
fmap_insert
fmap_empty
.
Qed
.
Lemma
to_
gc_m
ap_insert
l
v
I
gcm
:
to_
gc_m
ap
(<[
l
:
=
(
v
,
I
)]>
gcm
)
=
<[
l
:
=
(
Excl'
v
,
to_agree
I
)]>
(
to_
gc_map
gcm
).
Proof
.
by
rewrite
/
to_
gc_m
ap
fmap_insert
.
Qed
.
Lemma
to_
inv_he
ap_insert
l
v
I
h
:
to_
inv_he
ap
(<[
l
:
=
(
v
,
I
)]>
h
)
=
<[
l
:
=
(
Excl'
v
,
to_agree
I
)]>
(
to_
inv_heap
h
).
Proof
.
by
rewrite
/
to_
inv_he
ap
fmap_insert
.
Qed
.
Lemma
lookup_to_
gc_m
ap_None
gcm
l
:
gcm
!!
l
=
None
→
to_
gc_map
gcm
!!
l
=
None
.
Proof
.
by
rewrite
/
to_
gc_m
ap
lookup_fmap
=>
->.
Qed
.
Lemma
lookup_to_
inv_he
ap_None
h
l
:
h
!!
l
=
None
→
to_
inv_heap
h
!!
l
=
None
.
Proof
.
by
rewrite
/
to_
inv_he
ap
lookup_fmap
=>
->.
Qed
.
Lemma
lookup_to_
gc_m
ap_Some
gcm
l
v
I
:
gcm
!!
l
=
Some
(
v
,
I
)
→
to_
gc_map
gcm
!!
l
=
Some
(
Excl'
v
,
to_agree
I
).
Proof
.
by
rewrite
/
to_
gc_m
ap
lookup_fmap
=>
->.
Qed
.
Lemma
lookup_to_
inv_he
ap_Some
h
l
v
I
:
h
!!
l
=
Some
(
v
,
I
)
→
to_
inv_heap
h
!!
l
=
Some
(
Excl'
v
,
to_agree
I
).
Proof
.
by
rewrite
/
to_
inv_he
ap
lookup_fmap
=>
->.
Qed
.
Lemma
lookup_to_
gc_m
ap_Some_2
gcm
l
v'
I'
:
to_
gc_map
gcm
!!
l
≡
Some
(
v'
,
I'
)
→
∃
v
I
,
v'
=
Excl'
v
∧
I'
≡
to_agree
I
∧
gcm
!!
l
=
Some
(
v
,
I
).
Lemma
lookup_to_
inv_he
ap_Some_2
h
l
v'
I'
:
to_
inv_heap
h
!!
l
≡
Some
(
v'
,
I'
)
→
∃
v
I
,
v'
=
Excl'
v
∧
I'
≡
to_agree
I
∧
h
!!
l
=
Some
(
v
,
I
).
Proof
.
rewrite
/
to_
gc_m
ap
/
prod_map
lookup_fmap
.
rewrite
fmap_Some_equiv
.
rewrite
/
to_
inv_he
ap
/
prod_map
lookup_fmap
.
rewrite
fmap_Some_equiv
.
intros
([]
&
Hsome
&
[
Heqv
HeqI
])
;
simplify_eq
/=
;
eauto
.
Qed
.
End
to_
gc_m
ap
.
End
to_
inv_he
ap
.
Lemma
gc
_init
{
L
V
:
Type
}
`
{
Countable
L
,
!
invG
Σ
,
!
gen_heapG
L
V
Σ
,
!
gc
PreG
L
V
Σ
}
E
:
⊢
|==>
∃
_
:
gc
G
L
V
Σ
,
|={
E
}=>
gc
_inv
L
V
.
Lemma
inv_heap
_init
{
L
V
:
Type
}
`
{
Countable
L
,
!
invG
Σ
,
!
gen_heapG
L
V
Σ
,
!
inv_heap
PreG
L
V
Σ
}
E
:
⊢
|==>
∃
_
:
inv_heap
G
L
V
Σ
,
|={
E
}=>
inv_heap
_inv
L
V
.
Proof
.
iMod
(
own_alloc
(
●
(
to_
gc_m
ap
∅
)))
as
(
γ
)
"H●"
.
{
rewrite
auth_auth_valid
.
exact
:
to_
gc_m
ap_valid
.
}
iMod
(
own_alloc
(
●
(
to_
inv_he
ap
∅
)))
as
(
γ
)
"H●"
.
{
rewrite
auth_auth_valid
.
exact
:
to_
inv_he
ap_valid
.
}
iModIntro
.
iExists
(
Gc
G
L
V
γ
).
iAssert
(
gc
_inv_P
(
gG
:
=
Gc
G
L
V
γ
))
with
"[H●]"
as
"P"
.
iExists
(
Inv_Heap
G
L
V
γ
).
iAssert
(
inv_heap
_inv_P
(
gG
:
=
Inv_Heap
G
L
V
γ
))
with
"[H●]"
as
"P"
.
{
iExists
_
.
iFrame
.
done
.
}
iApply
(
inv_alloc
gcN
E
gc
_inv_P
with
"P"
).
iApply
(
inv_alloc
inv_heapN
E
inv_heap
_inv_P
with
"P"
).
Qed
.
Section
gc
.
Section
inv_heap
.
Context
{
L
V
:
Type
}
`
{
Countable
L
}.
Context
`
{!
invG
Σ
,
!
gen_heapG
L
V
Σ
,
gG
:
!
gc
G
L
V
Σ
}.
Context
`
{!
invG
Σ
,
!
gen_heapG
L
V
Σ
,
gG
:
!
inv_heap
G
L
V
Σ
}.
Implicit
Types
(
l
:
L
)
(
v
:
V
)
(
I
:
V
→
Prop
).
Implicit
Types
(
gcm
:
gmap
L
(
V
*
(
V
-
d
>
PropO
))).
Implicit
Types
(
h
:
gmap
L
(
V
*
(
V
-
d
>
PropO
))).
(** * Helpers *)
Lemma
i
s_gc
_lookup_Some
l
gcm
I
:
i
s_gc_loc
l
I
-
∗
own
(
gc
_name
gG
)
(
●
to_
gc_map
gcm
)
-
∗
⌜
∃
v
I'
,
gcm
!!
l
=
Some
(
v
,
I'
)
∧
∀
w
,
I
w
↔
I'
w
⌝
.
Lemma
i
nv_mapsto
_lookup_Some
l
h
I
:
i
nv_mapsto
l
I
-
∗
own
(
inv_heap
_name
gG
)
(
●
to_
inv_heap
h
)
-
∗
⌜
∃
v
I'
,
h
!!
l
=
Some
(
v
,
I'
)
∧
∀
w
,
I
w
↔
I'
w
⌝
.
Proof
.
iIntros
"H
gc_l
H◯"
.
iDestruct
(
own_valid_2
with
"H◯ H
gc_l
"
)
as
%[
Hincl
Hvalid
]%
auth_both_valid
.
iIntros
"H
l_inv
H◯"
.
iDestruct
(
own_valid_2
with
"H◯ H
l_inv
"
)
as
%[
Hincl
Hvalid
]%
auth_both_valid
.
iPureIntro
.
move
:
Hincl
;
rewrite
singleton_included_l
;
intros
([
v'
I'
]
&
Hsome
&
Hincl
).
apply
lookup_to_
gc_m
ap_Some_2
in
Hsome
as
(
v''
&
I''
&
_
&
HI
&
H
gcm
).
apply
lookup_to_
inv_he
ap_Some_2
in
Hsome
as
(
v''
&
I''
&
_
&
HI
&
H
h
).
move
:
Hincl
;
rewrite
HI
Some_included_total
pair_included
to_agree_included
;
intros
[??]
;
eauto
.
Qed
.
Lemma
gc
_mapsto_lookup_Some
l
v
gcm
I
:
gc
_mapsto
l
v
I
-
∗
own
(
gc
_name
gG
)
(
●
to_
gc_map
gcm
)
-
∗
⌜
∃
I'
,
gcm
!!
l
=
Some
(
v
,
I'
)
∧
∀
w
,
I
w
↔
I'
w
⌝
.
Lemma
inv
_mapsto_
own_
lookup_Some
l
v
h
I
:
inv
_mapsto
_own
l
v
I
-
∗
own
(
inv_heap
_name
gG
)
(
●
to_
inv_heap
h
)
-
∗
⌜
∃
I'
,
h
!!
l
=
Some
(
v
,
I'
)
∧
∀
w
,
I
w
↔
I'
w
⌝
.
Proof
.
iIntros
"H
gc_l
H●"
.
iDestruct
(
own_valid_2
with
"H● H
gc_l
"
)
as
%[
Hincl
Hvalid
]%
auth_both_valid
.
iIntros
"H
l_inv
H●"
.
iDestruct
(
own_valid_2
with
"H● H
l_inv
"
)
as
%[
Hincl
Hvalid
]%
auth_both_valid
.
iPureIntro
.
move
:
Hincl
;
rewrite
singleton_included_l
;
intros
([
v'
I'
]
&
Hsome
&
Hincl
).
apply
lookup_to_
gc_m
ap_Some_2
in
Hsome
as
(
v''
&
I''
&
->
&
HI
&
H
gcm
).
apply
lookup_to_
inv_he
ap_Some_2
in
Hsome
as
(
v''
&
I''
&
->
&
HI
&
H
h
).
move
:
Hincl
;
rewrite
HI
Some_included_total
pair_included
Excl_included
to_agree_included
;
intros
[->
?]
;
eauto
.
Qed
.
...
...
@@ -158,113 +158,114 @@ Section gc.
(* FIXME(Coq #6294): needs new unification
The uses of [apply:] and [move: ..; rewrite ..] (by lack of [apply: .. in ..])
in this file are needed because Coq's default unification algorithm fails. *)
Global
Instance
gc
_mapsto_proper
l
v
:
Proper
(
pointwise_relation
_
iff
==>
(
≡
))
(
gc
_mapsto
l
v
).
Global
Instance
inv
_mapsto_
own_
proper
l
v
:
Proper
(
pointwise_relation
_
iff
==>
(
≡
))
(
inv
_mapsto
_own
l
v
).
Proof
.
intros
I1
I2
?.
rewrite
/
gc
_mapsto
.
do
2
f_equiv
.
intros
I1
I2
?.
rewrite
/
inv
_mapsto
_own
.
do
2
f_equiv
.
apply
:
singletonM_proper
.
f_equiv
.
by
apply
:
to_agree_proper
.
Qed
.
Global
Instance
i
s_gc_loc
_proper
l
:
Proper
(
pointwise_relation
_
iff
==>
(
≡
))
(
i
s_gc_loc
l
).
Global
Instance
i
nv_mapsto
_proper
l
:
Proper
(
pointwise_relation
_
iff
==>
(
≡
))
(
i
nv_mapsto
l
).
Proof
.
intros
I1
I2
?.
rewrite
/
i
s_gc_loc
.
do
2
f_equiv
.
intros
I1
I2
?.
rewrite
/
i
nv_mapsto
.
do
2
f_equiv
.
apply
:
singletonM_proper
.
f_equiv
.
by
apply
:
to_agree_proper
.
Qed
.
Global
Instance
i
s_gc_loc
_persistent
l
I
:
Persistent
(
i
s_gc_loc
l
I
).
Proof
.
rewrite
/
i
s_gc_loc
.
apply
_
.
Qed
.
Global
Instance
i
nv_mapsto
_persistent
l
I
:
Persistent
(
i
nv_mapsto
l
I
).
Proof
.
rewrite
/
i
nv_mapsto
.
apply
_
.
Qed
.
Global
Instance
i
s_gc_loc
_timeless
l
I
:
Timeless
(
i
s_gc_loc
l
I
).
Proof
.
rewrite
/
i
s_gc_loc
.
apply
_
.
Qed
.
Global
Instance
i
nv_mapsto
_timeless
l
I
:
Timeless
(
i
nv_mapsto
l
I
).
Proof
.
rewrite
/
i
nv_mapsto
.
apply
_
.
Qed
.
Global
Instance
gc
_mapsto_timeless
l
v
I
:
Timeless
(
gc
_mapsto
l
v
I
).
Proof
.
rewrite
/
i
s_gc_loc
.
apply
_
.
Qed
.
Global
Instance
inv
_mapsto_
own_
timeless
l
v
I
:
Timeless
(
inv
_mapsto
_own
l
v
I
).
Proof
.
rewrite
/
i
nv_mapsto
.
apply
_
.
Qed
.
(** * Public lemmas *)
Lemma
make_
gc
l
v
I
E
:
↑
gc
N
⊆
E
→
Lemma
make_
inv_mapsto
l
v
I
E
:
↑
inv_heap
N
⊆
E
→
I
v
→
gc
_inv
L
V
-
∗
l
↦
v
={
E
}=
∗
gc
_mapsto
l
v
I
.
inv_heap
_inv
L
V
-
∗
l
↦
v
={
E
}=
∗
inv
_mapsto
_own
l
v
I
.
Proof
.
iIntros
(
HN
HI
)
"#Hinv Hl"
.
iMod
(
inv_acc_timeless
_
gc
N
with
"Hinv"
)
as
"[HP Hclose]"
;
first
done
.
iDestruct
"HP"
as
(
gcm
)
"[H● HsepM]"
.
destruct
(
gcm
!!
l
)
as
[
v'
|
]
eqn
:
Hlookup
.
iMod
(
inv_acc_timeless
_
inv_heap
N
with
"Hinv"
)
as
"[HP Hclose]"
;
first
done
.
iDestruct
"HP"
as
(
h
)
"[H● HsepM]"
.
destruct
(
h
!!
l
)
as
[
v'
|
]
eqn
:
Hlookup
.
-
(* auth map contains l --> contradiction *)
iDestruct
(
big_sepM_lookup
with
"HsepM"
)
as
"[_ Hl']"
;
first
done
.
by
iDestruct
(
mapsto_valid_2
with
"Hl Hl'"
)
as
%?.
-
iMod
(
own_update
with
"H●"
)
as
"[H● H◯]"
.
{
apply
lookup_to_
gc_m
ap_None
in
Hlookup
.
{
apply
lookup_to_
inv_he
ap_None
in
Hlookup
.
apply
(
auth_update_alloc
_
(
to_
gc_m
ap
(<[
l
:
=(
v
,
I
)]>
gcm
))
(
to_
gc_m
ap
({[
l
:
=(
v
,
I
)]}))).
rewrite
to_
gc_m
ap_insert
to_
gc_m
ap_singleton
.
(
to_
inv_he
ap
(<[
l
:
=(
v
,
I
)]>
h
))
(
to_
inv_he
ap
({[
l
:
=(
v
,
I
)]}))).
rewrite
to_
inv_he
ap_insert
to_
inv_he
ap_singleton
.
by
apply
:
alloc_singleton_local_update
.
}
iMod
(
"Hclose"
with
"[H● HsepM Hl]"
).
+
iExists
_
.
iDestruct
(
big_sepM_insert
_
_
_
(
_
,
_
)
with
"[$HsepM $Hl]"
)
as
"HsepM"
;
auto
with
iFrame
.
+
iModIntro
.
by
rewrite
/
gc
_mapsto
to_gc_m
ap_singleton
.
+
iModIntro
.
by
rewrite
/
inv
_mapsto
_own
to_inv_he
ap_singleton
.
Qed
.
Lemma
gc_is_gc
l
v
I
:
gc
_mapsto
l
v
I
-
∗
i
s_gc_loc
l
I
.
Lemma
inv_mapsto_own_inv
l
v
I
:
inv
_mapsto
_own
l
v
I
-
∗
i
nv_mapsto
l
I
.
Proof
.
apply
own_mono
,
auth_frag_mono
.
rewrite
singleton_included
pair_included
.
right
.
split
;
[
apply
:
ucmra_unit_least
|
done
].
Qed
.
(** An accessor to make use of [gc_mapsto].
This opens the invariant *before* consuming [gc_mapsto] so that you can use
this before opening an atomic update that provides [gc_mapsto]!. *)
Lemma
gc_acc_strong
E
:
↑
gcN
⊆
E
→
gc_inv
L
V
={
E
,
E
∖
↑
gcN
}=
∗
∀
l
v
I
,
gc_mapsto
l
v
I
-
∗
(
⌜
I
v
⌝
∗
l
↦
v
∗
(
∀
w
,
⌜
I
w
⌝
-
∗
l
↦
w
==
∗
gc_mapsto
l
w
I
∗
|={
E
∖
↑
gcN
,
E
}=>
True
)).
(** An accessor to make use of [inv_mapsto_own].
This opens the invariant *before* consuming [inv_mapsto_own] so that you can use
this before opening an atomic update that provides [inv_mapsto_own]!. *)
Lemma
inv_mapsto_own_acc_strong
E
:
↑
inv_heapN
⊆
E
→
inv_heap_inv
L
V
={
E
,
E
∖
↑
inv_heapN
}=
∗
∀
l
v
I
,
inv_mapsto_own
l
v
I
-
∗
(
⌜
I
v
⌝
∗
l
↦
v
∗
(
∀
w
,
⌜
I
w
⌝
-
∗
l
↦
w
==
∗
inv_mapsto_own
l
w
I
∗
|={
E
∖
↑
inv_heapN
,
E
}=>
True
)).
Proof
.
iIntros
(
HN
)
"#Hinv"
.
iMod
(
inv_acc_timeless
_
gc
N
_
with
"Hinv"
)
as
"[HP Hclose]"
=>//.
iIntros
"!>"
(
l
v
I
)
"H
gc_l
"
.
iDestruct
"HP"
as
(
gcm
)
"[H● HsepM]"
.
iDestruct
(
gc
_mapsto_lookup_Some
with
"H
gc_l
H●"
)
as
%(
I'
&?&
HI'
).
iMod
(
inv_acc_timeless
_
inv_heap
N
_
with
"Hinv"
)
as
"[HP Hclose]"
=>//.
iIntros
"!>"
(
l
v
I
)
"H
l_inv
"
.
iDestruct
"HP"
as
(
h
)
"[H● HsepM]"
.
iDestruct
(
inv
_mapsto_
own_
lookup_Some
with
"H
l_inv
H●"
)
as
%(
I'
&?&
HI'
).
setoid_rewrite
HI'
.
iDestruct
(
big_sepM_delete
with
"HsepM"
)
as
"[[HI Hl] HsepM]"
;
first
done
.
iIntros
"{$HI $Hl}"
(
w
?)
"Hl"
.
iMod
(
own_update_2
with
"H● H
gc_l
"
)
as
"[H● H◯]"
.
{
apply
(
auth_update
_
_
(<[
l
:
=
(
Excl'
w
,
to_agree
I'
)]>
(
to_
gc_map
gcm
))
iMod
(
own_update_2
with
"H● H
l_inv
"
)
as
"[H● H◯]"
.
{
apply
(
auth_update
_
_
(<[
l
:
=
(
Excl'
w
,
to_agree
I'
)]>
(
to_
inv_heap
h
))
{[
l
:
=
(
Excl'
w
,
to_agree
I
)]}).
apply
:
singleton_local_update
.
{
by
apply
lookup_to_
gc_m
ap_Some
.
}
{
by
apply
lookup_to_
inv_he
ap_Some
.
}
apply
:
prod_local_update_1
.
apply
:
option_local_update
.
apply
:
exclusive_local_update
.
done
.
}
iDestruct
(
big_sepM_insert
_
_
_
(
w
,
I'
)
with
"[$HsepM $Hl //]"
)
as
"HsepM"
.
{
apply
lookup_delete
.
}
rewrite
insert_delete
-
to_
gc_m
ap_insert
.
iIntros
"!> {$H◯}"
.
rewrite
insert_delete
-
to_
inv_he
ap_insert
.
iIntros
"!> {$H◯}"
.
iApply
(
"Hclose"
with
"[H● HsepM]"
).
iExists
_;
by
iFrame
.
Qed
.
(** Derive a more standard accessor. *)
Lemma
gc
_acc
E
l
v
I
:
↑
gc
N
⊆
E
→
gc
_inv
L
V
-
∗
gc
_mapsto
l
v
I
={
E
,
E
∖
↑
gc
N
}=
∗
(
⌜
I
v
⌝
∗
l
↦
v
∗
(
∀
w
,
⌜
I
w
⌝
-
∗
l
↦
w
={
E
∖
↑
gc
N
,
E
}=
∗
gc
_mapsto
l
w
I
)).
Lemma
inv_mapsto_own
_acc
E
l
v
I
:
↑
inv_heap
N
⊆
E
→
inv_heap
_inv
L
V
-
∗
inv
_mapsto
_own
l
v
I
={
E
,
E
∖
↑
inv_heap
N
}=
∗
(
⌜
I
v
⌝
∗
l
↦
v
∗
(
∀
w
,
⌜
I
w
⌝
-
∗
l
↦
w
={
E
∖
↑
inv_heap
N
,
E
}=
∗
inv
_mapsto
_own
l
w
I
)).
Proof
.
iIntros
(?)
"#Hinv Hl"
.
iMod
(
gc
_acc_strong
with
"Hinv"
)
as
"Hacc"
;
first
done
.
iMod
(
inv_mapsto_own
_acc_strong
with
"Hinv"
)
as
"Hacc"
;
first
done
.
iDestruct
(
"Hacc"
with
"Hl"
)
as
"(HI & Hl & Hclose)"
.
iIntros
"!> {$HI $Hl}"
(
w
)
"HI Hl"
.
iMod
(
"Hclose"
with
"HI Hl"
)
as
"[$ $]"
.
Qed
.
Lemma
i
s_gc
_acc
l
I
E
:
↑
gc
N
⊆
E
→
gc
_inv
L
V
-
∗
i
s_gc_loc
l
I
={
E
,
E
∖
↑
gc
N
}=
∗
∃
v
,
⌜
I
v
⌝
∗
l
↦
v
∗
(
l
↦
v
={
E
∖
↑
gc
N
,
E
}=
∗
⌜
True
⌝
).
Lemma
i
nv_mapsto
_acc
l
I
E
:
↑
inv_heap
N
⊆
E
→
inv_heap
_inv
L
V
-
∗
i
nv_mapsto
l
I
={
E
,
E
∖
↑
inv_heap
N
}=
∗
∃
v
,
⌜
I
v
⌝
∗
l
↦
v
∗
(
l
↦
v
={
E
∖
↑
inv_heap
N
,
E
}=
∗
⌜
True
⌝
).
Proof
.
iIntros
(
HN
)
"#Hinv H
gc_l
"
.
iMod
(
inv_acc_timeless
_
gc
N
_
with
"Hinv"
)
as
"[HP Hclose]"
=>//.
iIntros
(
HN
)
"#Hinv H
l_inv
"
.
iMod
(
inv_acc_timeless
_
inv_heap
N
_
with
"Hinv"
)
as
"[HP Hclose]"
=>//.
iModIntro
.
iDestruct
"HP"
as
(
gcm
)
"[H● HsepM]"
.
iDestruct
(
i
s_gc
_lookup_Some
with
"H
gc_l
H●"
)
as
%(
v
&
I'
&?&
HI'
).
iDestruct
"HP"
as
(
h
)
"[H● HsepM]"
.
iDestruct
(
i
nv_mapsto
_lookup_Some
with
"H
l_inv
H●"
)
as
%(
v
&
I'
&?&
HI'
).
iDestruct
(
big_sepM_lookup_acc
with
"HsepM"
)
as
"[[#HI Hl] HsepM]"
=>//.
setoid_rewrite
HI'
.
iExists
_
.
iIntros
"{$HI $Hl} Hl"
.
...
...
@@ -272,6 +273,6 @@ Section gc.
iExists
_
.
iFrame
"H●"
.
iApply
(
"HsepM"
with
"[$Hl //]"
).
Qed
.
End
gc
.
End
inv_heap
.
Typeclasses
Opaque
i
s_gc_loc
gc
_mapsto
.
Typeclasses
Opaque
i
nv_mapsto
inv
_mapsto
_own
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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