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
George Pirlea
Iris
Commits
843bf221
Commit
843bf221
authored
Feb 18, 2019
by
Dan Frumin
Browse files
Implement `own_alloc_infinite`
parent
da93f357
Changes
7
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
843bf221
...
...
@@ -100,6 +100,9 @@ Changes in Coq:
steps that would require unlocking subterms. Every impure wp_ tactic executes
this tactic before doing anything else.
*
Add
`big_sepM_insert_acc`
.
*
The
`_strong`
lemmas (e.g.
`own_alloc_strong`
) work for all infinite
sets, instead of just for cofinite sets. The versions with cofinite
sets have been renamed to use the
`_cofinite`
suffix.
## Iris 3.1.0 (released 2017-12-19)
...
...
theories/algebra/gmap.v
View file @
843bf221
From
iris
.
algebra
Require
Export
cmra
.
From
stdpp
Require
Export
gmap
.
From
stdpp
Require
Export
list
gmap
.
From
iris
.
algebra
Require
Import
updates
local_updates
.
From
iris
.
base_logic
Require
Import
base_logic
.
From
iris
.
algebra
Require
Import
proofmode_classes
.
...
...
@@ -354,29 +354,48 @@ Qed.
Section
freshness
.
Local
Set
Default
Proof
Using
"Type*"
.
Context
`
{!
Infinite
K
}.
Lemma
alloc_updateP_strong
(
Q
:
gmap
K
A
→
Prop
)
(
I
:
gset
K
)
m
x
:
✓
x
→
(
∀
i
,
m
!!
i
=
None
→
i
∉
I
→
Q
(<[
i
:
=
x
]>
m
))
→
m
~~>
:
Q
.
Lemma
alloc_updateP_strong
(
Q
:
gmap
K
A
→
Prop
)
(
I
:
K
→
Prop
)
m
x
:
pred_infinite
I
→
✓
x
→
(
∀
i
,
m
!!
i
=
None
→
I
i
→
Q
(<[
i
:
=
x
]>
m
))
→
m
~~>
:
Q
.
Proof
.
intros
?
HQ
.
apply
cmra_total_updateP
.
intros
n
mf
Hm
.
set
(
i
:
=
fresh
(
I
∪
dom
(
gset
K
)
(
m
⋅
mf
))).
assert
(
i
∉
I
∧
i
∉
dom
(
gset
K
)
m
∧
i
∉
dom
(
gset
K
)
mf
)
as
[?[??]].
{
rewrite
-
not_elem_of_union
-
dom_op
-
not_elem_of_union
;
apply
is_fresh
.
}
move
=>
/(
pred_infinite_set
I
(
C
:
=
gset
K
))
HP
?
HQ
.
apply
cmra_total_updateP
.
intros
n
mf
Hm
.
destruct
(
HP
(
dom
(
gset
K
)
(
m
⋅
mf
)))
as
[
i
[
Hi1
Hi2
]].
assert
(
m
!!
i
=
None
).
{
eapply
(
not_elem_of_dom
(
D
:
=
gset
K
)).
revert
Hi2
.
rewrite
dom_op
not_elem_of_union
.
naive_solver
.
}
exists
(<[
i
:
=
x
]>
m
)
;
split
.
{
apply
HQ
;
last
done
.
by
e
apply
not_elem_of_dom
.
}
rewrite
insert_singleton_op
;
last
by
eapply
not_elem_of_dom
.
rewrite
-
assoc
-
insert_singleton_op
;
last
by
eapply
(
not_elem_of_dom
(
D
:
=
gset
K
))
;
rewrite
dom_op
not_elem_of_union
.
-
by
apply
HQ
.
-
rewrite
insert_singleton_op
//
.
rewrite
-
assoc
-
insert_singleton_op
;
last
by
eapply
(
not_elem_of_dom
(
D
:
=
gset
K
)).
by
apply
insert_validN
;
[
apply
cmra_valid_validN
|].
Qed
.
Lemma
alloc_updateP
(
Q
:
gmap
K
A
→
Prop
)
m
x
:
✓
x
→
(
∀
i
,
m
!!
i
=
None
→
Q
(<[
i
:
=
x
]>
m
))
→
m
~~>
:
Q
.
Proof
.
move
=>??.
eapply
alloc_updateP_strong
with
(
I
:
=
∅
)
;
by
eauto
.
Qed
.
Lemma
alloc_updateP_strong'
m
x
(
I
:
gset
K
)
:
✓
x
→
m
~~>
:
λ
m'
,
∃
i
,
i
∉
I
∧
m'
=
<[
i
:
=
x
]>
m
∧
m
!!
i
=
None
.
Proof
.
move
=>??.
eapply
alloc_updateP_strong
with
(
I
:
=
λ
_
,
True
)
;
eauto
using
pred_infinite_True
.
Qed
.
Lemma
alloc_updateP_strong'
m
x
(
I
:
K
→
Prop
)
:
pred_infinite
I
→
✓
x
→
m
~~>
:
λ
m'
,
∃
i
,
I
i
∧
m'
=
<[
i
:
=
x
]>
m
∧
m
!!
i
=
None
.
Proof
.
eauto
using
alloc_updateP_strong
.
Qed
.
Lemma
alloc_updateP'
m
x
:
✓
x
→
m
~~>
:
λ
m'
,
∃
i
,
m'
=
<[
i
:
=
x
]>
m
∧
m
!!
i
=
None
.
Proof
.
eauto
using
alloc_updateP
.
Qed
.
Lemma
alloc_updateP_cofinite
(
Q
:
gmap
K
A
→
Prop
)
(
J
:
gset
K
)
m
x
:
✓
x
→
(
∀
i
,
m
!!
i
=
None
→
i
∉
J
→
Q
(<[
i
:
=
x
]>
m
))
→
m
~~>
:
Q
.
Proof
.
eapply
alloc_updateP_strong
.
apply
(
pred_infinite_set
(
C
:
=
gset
K
)).
intros
E
.
exists
(
fresh
(
J
∪
E
)).
apply
not_elem_of_union
,
is_fresh
.
Qed
.
Lemma
alloc_updateP_cofinite'
m
x
(
J
:
gset
K
)
:
✓
x
→
m
~~>
:
λ
m'
,
∃
i
,
i
∉
J
∧
m'
=
<[
i
:
=
x
]>
m
∧
m
!!
i
=
None
.
Proof
.
eauto
using
alloc_updateP_cofinite
.
Qed
.
End
freshness
.
Lemma
alloc_unit_singleton_updateP
(
P
:
A
→
Prop
)
(
Q
:
gmap
K
A
→
Prop
)
u
i
:
...
...
theories/base_logic/lib/auth.v
View file @
843bf221
...
...
@@ -102,22 +102,31 @@ Section auth.
Global
Instance
own_mono'
γ
:
Proper
(
flip
(
≼
)
==>
(
⊢
))
(
auth_own
γ
).
Proof
.
intros
a1
a2
.
apply
auth_own_mono
.
Qed
.
Lemma
auth_alloc_strong
N
E
t
(
G
:
gset
gname
)
:
✓
(
f
t
)
→
▷
φ
t
={
E
}=
∗
∃
γ
,
⌜γ
∉
G
⌝
∧
auth_ctx
γ
N
f
φ
∧
auth_own
γ
(
f
t
).
Lemma
auth_alloc_strong
N
E
t
(
I
:
gname
→
Prop
)
:
pred_infinite
I
→
✓
(
f
t
)
→
▷
φ
t
={
E
}=
∗
∃
γ
,
⌜
I
γ⌝
∧
auth_ctx
γ
N
f
φ
∧
auth_own
γ
(
f
t
).
Proof
.
iIntros
(?)
"Hφ"
.
rewrite
/
auth_own
/
auth_ctx
.
iMod
(
own_alloc_strong
(
Auth
(
Excl'
(
f
t
))
(
f
t
))
G
)
as
(
γ
)
"[% Hγ]"
;
first
done
.
iIntros
(?
?
)
"Hφ"
.
rewrite
/
auth_own
/
auth_ctx
.
iMod
(
own_alloc_strong
(
Auth
(
Excl'
(
f
t
))
(
f
t
))
I
)
as
(
γ
)
"[% Hγ]"
;
[
done
|
done
|]
.
iRevert
"Hγ"
;
rewrite
auth_both_op
;
iIntros
"[Hγ Hγ']"
.
iMod
(
inv_alloc
N
_
(
auth_inv
γ
f
φ
)
with
"[-Hγ']"
)
as
"#?"
.
{
iNext
.
rewrite
/
auth_inv
.
iExists
t
.
by
iFrame
.
}
eauto
.
Qed
.
Lemma
auth_alloc_cofinite
N
E
t
(
G
:
gset
gname
)
:
✓
(
f
t
)
→
▷
φ
t
={
E
}=
∗
∃
γ
,
⌜γ
∉
G
⌝
∧
auth_ctx
γ
N
f
φ
∧
auth_own
γ
(
f
t
).
Proof
.
intros
?.
apply
auth_alloc_strong
=>//.
apply
(
pred_infinite_set
(
C
:
=
gset
gname
))
=>
E'
.
exists
(
fresh
(
G
∪
E'
)).
apply
not_elem_of_union
,
is_fresh
.
Qed
.
Lemma
auth_alloc
N
E
t
:
✓
(
f
t
)
→
▷
φ
t
={
E
}=
∗
∃
γ
,
auth_ctx
γ
N
f
φ
∧
auth_own
γ
(
f
t
).
Proof
.
iIntros
(?)
"Hφ"
.
iMod
(
auth_alloc_
strong
N
E
t
∅
with
"Hφ"
)
as
(
γ
)
"[_ ?]"
;
eauto
.
iMod
(
auth_alloc_
cofinite
N
E
t
∅
with
"Hφ"
)
as
(
γ
)
"[_ ?]"
;
eauto
.
Qed
.
Lemma
auth_empty
γ
:
(|==>
auth_own
γ
ε
)%
I
.
...
...
theories/base_logic/lib/boxes.v
View file @
843bf221
...
...
@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P :
slice
N
γ
Q
∗
▷
?q
box
N
(<[
γ
:
=
false
]>
f
)
(
Q
∗
P
).
Proof
.
iDestruct
1
as
(
Φ
)
"[#HeqP Hf]"
.
iMod
(
own_alloc_
strong
(
●
Excl'
false
⋅
◯
Excl'
false
,
iMod
(
own_alloc_
cofinite
(
●
Excl'
false
⋅
◯
Excl'
false
,
Some
(
to_agree
(
Next
(
iProp_unfold
Q
))))
(
dom
_
f
))
as
(
γ
)
"[Hdom Hγ]"
;
first
done
.
rewrite
pair_split
.
iDestruct
"Hγ"
as
"[[Hγ Hγ'] #HγQ]"
.
...
...
theories/base_logic/lib/cancelable_invariants.v
View file @
843bf221
...
...
@@ -62,15 +62,23 @@ Section proofs.
-
iIntros
"?"
.
iApply
"HP'"
.
iApply
"HP''"
.
done
.
Qed
.
Lemma
cinv_alloc_strong
(
G
:
gset
gname
)
E
N
:
(|={
E
}=>
∃
γ
,
⌜
γ
∉
G
⌝
∧
cinv_own
γ
1
∗
∀
P
,
▷
P
={
E
}=
∗
cinv
N
γ
P
)%
I
.
Lemma
cinv_alloc_strong
(
I
:
gname
→
Prop
)
E
N
:
pred_infinite
I
→
(|={
E
}=>
∃
γ
,
⌜
I
γ
⌝
∧
cinv_own
γ
1
∗
∀
P
,
▷
P
={
E
}=
∗
cinv
N
γ
P
)%
I
.
Proof
.
iMod
(
own_alloc_strong
1
%
Qp
G
)
as
(
γ
)
"[Hfresh Hγ]"
;
first
done
.
iIntros
(?).
iMod
(
own_alloc_strong
1
%
Qp
I
)
as
(
γ
)
"[Hfresh Hγ]"
;
[
done
|
done
|]
.
iExists
γ
;
iIntros
"!> {$Hγ $Hfresh}"
(
P
)
"HP"
.
iMod
(
inv_alloc
N
_
(
P
∨
own
γ
1
%
Qp
)%
I
with
"[HP]"
)
;
first
by
eauto
.
iIntros
"!>"
.
iExists
P
.
iSplit
;
last
done
.
iIntros
"!# !>"
;
iSplit
;
auto
.
Qed
.
Lemma
cinv_alloc_cofinite
(
G
:
gset
gname
)
E
N
:
(|={
E
}=>
∃
γ
,
⌜
γ
∉
G
⌝
∧
cinv_own
γ
1
∗
∀
P
,
▷
P
={
E
}=
∗
cinv
N
γ
P
)%
I
.
Proof
.
apply
cinv_alloc_strong
.
apply
(
pred_infinite_set
(
C
:
=
gset
gname
))=>
E'
.
exists
(
fresh
(
G
∪
E'
)).
apply
not_elem_of_union
,
is_fresh
.
Qed
.
Lemma
cinv_open_strong
E
N
γ
p
P
:
↑
N
⊆
E
→
cinv
N
γ
P
-
∗
cinv_own
γ
p
={
E
,
E
∖↑
N
}=
∗
...
...
@@ -88,7 +96,7 @@ Section proofs.
Lemma
cinv_alloc
E
N
P
:
▷
P
={
E
}=
∗
∃
γ
,
cinv
N
γ
P
∗
cinv_own
γ
1
.
Proof
.
iIntros
"HP"
.
iMod
(
cinv_alloc_
strong
∅
E
N
)
as
(
γ
_
)
"[Hγ Halloc]"
.
iIntros
"HP"
.
iMod
(
cinv_alloc_
cofinite
∅
E
N
)
as
(
γ
_
)
"[Hγ Halloc]"
.
iExists
γ
.
iFrame
"Hγ"
.
by
iApply
"Halloc"
.
Qed
.
...
...
theories/base_logic/lib/own.v
View file @
843bf221
...
...
@@ -143,11 +143,12 @@ Qed.
(** ** Allocation *)
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma
own_alloc_strong
a
(
G
:
gset
gname
)
:
✓
a
→
(|==>
∃
γ
,
⌜γ
∉
G
⌝
∧
own
γ
a
)%
I
.
Lemma
own_alloc_strong
a
(
P
:
gname
→
Prop
)
:
pred_infinite
P
→
✓
a
→
(|==>
∃
γ
,
⌜
P
γ⌝
∧
own
γ
a
)%
I
.
Proof
.
intros
Ha
.
rewrite
-(
bupd_mono
(
∃
m
,
⌜
∃
γ
,
γ
∉
G
∧
m
=
iRes_singleton
γ
a
⌝
∧
uPred_ownM
m
)%
I
).
intros
HP
Ha
.
rewrite
-(
bupd_mono
(
∃
m
,
⌜
∃
γ
,
P
γ
∧
m
=
iRes_singleton
γ
a
⌝
∧
uPred_ownM
m
)%
I
).
-
rewrite
/
uPred_valid
/
bi_emp_valid
(
ownM_unit
emp
).
eapply
bupd_ownM_updateP
,
(
ofe_fun_singleton_updateP_empty
(
inG_id
_
))
;
first
(
eapply
alloc_updateP_strong'
,
cmra_transport_valid
,
Ha
)
;
...
...
@@ -155,9 +156,18 @@ Proof.
-
apply
exist_elim
=>
m
;
apply
pure_elim_l
=>-[
γ
[
Hfresh
->]].
by
rewrite
!
own_eq
/
own_def
-(
exist_intro
γ
)
pure_True
//
left_id
.
Qed
.
Lemma
own_alloc_cofinite
a
(
G
:
gset
gname
)
:
✓
a
→
(|==>
∃
γ
,
⌜γ
∉
G
⌝
∧
own
γ
a
)%
I
.
Proof
.
intros
Ha
.
apply
(
own_alloc_strong
a
(
λ
γ
,
γ
∉
G
))=>
//.
apply
(
pred_infinite_set
(
C
:
=
gset
gname
)).
intros
E
.
set
(
i
:
=
fresh
(
G
∪
E
)).
exists
i
.
apply
not_elem_of_union
,
is_fresh
.
Qed
.
Lemma
own_alloc
a
:
✓
a
→
(|==>
∃
γ
,
own
γ
a
)%
I
.
Proof
.
intros
Ha
.
rewrite
/
uPred_valid
/
bi_emp_valid
(
own_alloc_
strong
a
∅
)
//
;
[].
intros
Ha
.
rewrite
/
uPred_valid
/
bi_emp_valid
(
own_alloc_
cofinite
a
∅
)
//
;
[].
apply
bupd_mono
,
exist_mono
=>?.
eauto
using
and_elim_r
.
Qed
.
...
...
theories/base_logic/lib/saved_prop.v
View file @
843bf221
...
...
@@ -37,9 +37,14 @@ Section saved_anything.
Global
Instance
saved_anything_proper
γ
:
Proper
((
≡
)
==>
(
≡
))
(
saved_anything_own
γ
).
Proof
.
solve_proper
.
Qed
.
Lemma
saved_anything_alloc_strong
x
(
G
:
gset
gname
)
:
Lemma
saved_anything_alloc_strong
x
(
I
:
gname
→
Prop
)
:
pred_infinite
I
→
(|==>
∃
γ
,
⌜
I
γ⌝
∧
saved_anything_own
γ
x
)%
I
.
Proof
.
intros
?.
by
apply
own_alloc_strong
.
Qed
.
Lemma
saved_anything_alloc_cofinite
x
(
G
:
gset
gname
)
:
(|==>
∃
γ
,
⌜γ
∉
G
⌝
∧
saved_anything_own
γ
x
)%
I
.
Proof
.
by
apply
own_alloc_
strong
.
Qed
.
Proof
.
by
apply
own_alloc_
cofinite
.
Qed
.
Lemma
saved_anything_alloc
x
:
(|==>
∃
γ
,
saved_anything_own
γ
x
)%
I
.
Proof
.
by
apply
own_alloc
.
Qed
.
...
...
@@ -72,9 +77,14 @@ Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
Contractive
(
saved_prop_own
γ
).
Proof
.
solve_contractive
.
Qed
.
Lemma
saved_prop_alloc_strong
`
{!
savedPropG
Σ
}
(
G
:
gset
gname
)
(
P
:
iProp
Σ
)
:
Lemma
saved_prop_alloc_strong
`
{!
savedPropG
Σ
}
(
I
:
gname
→
Prop
)
(
P
:
iProp
Σ
)
:
pred_infinite
I
→
(|==>
∃
γ
,
⌜
I
γ⌝
∧
saved_prop_own
γ
P
)%
I
.
Proof
.
iIntros
(?).
by
iApply
saved_anything_alloc_strong
.
Qed
.
Lemma
saved_prop_alloc_cofinite
`
{!
savedPropG
Σ
}
(
G
:
gset
gname
)
(
P
:
iProp
Σ
)
:
(|==>
∃
γ
,
⌜γ
∉
G
⌝
∧
saved_prop_own
γ
P
)%
I
.
Proof
.
iApply
saved_anything_alloc_
strong
.
Qed
.
Proof
.
iApply
saved_anything_alloc_
cofinite
.
Qed
.
Lemma
saved_prop_alloc
`
{!
savedPropG
Σ
}
(
P
:
iProp
Σ
)
:
(|==>
∃
γ
,
saved_prop_own
γ
P
)%
I
.
...
...
@@ -99,9 +109,14 @@ Proof.
solve_proper_core
ltac
:
(
fun
_
=>
first
[
intros
?
;
progress
simpl
|
by
auto
|
f_contractive
|
f_equiv
]).
Qed
.
Lemma
saved_pred_alloc_strong
`
{!
savedPredG
Σ
A
}
(
G
:
gset
gname
)
(
Φ
:
A
→
iProp
Σ
)
:
Lemma
saved_pred_alloc_strong
`
{!
savedPredG
Σ
A
}
(
I
:
gname
→
Prop
)
(
Φ
:
A
→
iProp
Σ
)
:
pred_infinite
I
→
(|==>
∃
γ
,
⌜
I
γ⌝
∧
saved_pred_own
γ
Φ
)%
I
.
Proof
.
iIntros
(?).
by
iApply
saved_anything_alloc_strong
.
Qed
.
Lemma
saved_pred_alloc_cofinite
`
{!
savedPredG
Σ
A
}
(
G
:
gset
gname
)
(
Φ
:
A
→
iProp
Σ
)
:
(|==>
∃
γ
,
⌜γ
∉
G
⌝
∧
saved_pred_own
γ
Φ
)%
I
.
Proof
.
iApply
saved_anything_alloc_
strong
.
Qed
.
Proof
.
iApply
saved_anything_alloc_
cofinite
.
Qed
.
Lemma
saved_pred_alloc
`
{!
savedPredG
Σ
A
}
(
Φ
:
A
→
iProp
Σ
)
:
(|==>
∃
γ
,
saved_pred_own
γ
Φ
)%
I
.
...
...
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