Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Rodolphe Lepigre
Iris
Commits
ed3b7e73
Commit
ed3b7e73
authored
Oct 28, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'robbert/invariant'
parents
e71c3257
b9413b6f
Changes
24
Hide whitespace changes
Inline
Side-by-side
Showing
24 changed files
with
194 additions
and
168 deletions
+194
-168
_CoqProject
_CoqProject
+11
-12
base_logic/lib/auth.v
base_logic/lib/auth.v
+5
-5
base_logic/lib/boxes.v
base_logic/lib/boxes.v
+7
-8
base_logic/lib/cancelable_invariants.v
base_logic/lib/cancelable_invariants.v
+4
-4
base_logic/lib/counter_examples.v
base_logic/lib/counter_examples.v
+0
-0
base_logic/lib/fancy_updates.v
base_logic/lib/fancy_updates.v
+13
-11
base_logic/lib/invariants.v
base_logic/lib/invariants.v
+6
-8
base_logic/lib/namespaces.v
base_logic/lib/namespaces.v
+0
-0
base_logic/lib/sts.v
base_logic/lib/sts.v
+7
-7
base_logic/lib/thread_local.v
base_logic/lib/thread_local.v
+4
-4
base_logic/lib/viewshifts.v
base_logic/lib/viewshifts.v
+5
-5
base_logic/lib/wsat.v
base_logic/lib/wsat.v
+27
-56
heap_lang/adequacy.v
heap_lang/adequacy.v
+2
-2
heap_lang/heap.v
heap_lang/heap.v
+2
-2
heap_lang/lib/barrier/proof.v
heap_lang/lib/barrier/proof.v
+1
-2
heap_lang/lifting.v
heap_lang/lifting.v
+1
-1
program_logic/adequacy.v
program_logic/adequacy.v
+57
-1
program_logic/ectx_lifting.v
program_logic/ectx_lifting.v
+0
-1
program_logic/hoare.v
program_logic/hoare.v
+2
-1
program_logic/iris.v
program_logic/iris.v
+0
-31
program_logic/lifting.v
program_logic/lifting.v
+0
-1
program_logic/weakestpre.v
program_logic/weakestpre.v
+38
-3
tests/heap_lang.v
tests/heap_lang.v
+0
-1
tests/proofmode.v
tests/proofmode.v
+2
-2
No files found.
_CoqProject
View file @
ed3b7e73
...
...
@@ -70,26 +70,25 @@ base_logic/double_negation.v
base_logic/lib/iprop.v
base_logic/lib/own.v
base_logic/lib/saved_prop.v
base_logic/lib/namespaces.v
base_logic/lib/wsat.v
base_logic/lib/invariants.v
base_logic/lib/fancy_updates.v
base_logic/lib/viewshifts.v
base_logic/lib/auth.v
base_logic/lib/sts.v
base_logic/lib/boxes.v
base_logic/lib/thread_local.v
base_logic/lib/cancelable_invariants.v
base_logic/lib/counter_examples.v
program_logic/adequacy.v
program_logic/lifting.v
program_logic/invariants.v
program_logic/wsat.v
program_logic/weakestpre.v
program_logic/fancy_updates.v
program_logic/hoare.v
program_logic/viewshifts.v
program_logic/language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_lifting.v
program_logic/auth.v
program_logic/sts.v
program_logic/namespaces.v
program_logic/boxes.v
program_logic/counter_examples.v
program_logic/iris.v
program_logic/thread_local.v
program_logic/cancelable_invariants.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
...
...
program
_logic/auth.v
→
base
_logic/
lib/
auth.v
View file @
ed3b7e73
From
iris
.
program
_logic
Require
Export
invariants
.
From
iris
.
base
_logic
.
lib
Require
Export
invariants
.
From
iris
.
algebra
Require
Export
auth
.
From
iris
.
algebra
Require
Import
gmap
.
From
iris
.
base_logic
Require
Import
big_op
.
...
...
@@ -16,7 +16,7 @@ Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A
Proof
.
intros
?%
subG_inG
?.
by
split
.
Qed
.
Section
definitions
.
Context
`
{
i
risG
Λ
Σ
,
authG
Σ
A
}
{
T
:
Type
}
(
γ
:
gname
).
Context
`
{
i
nvG
Σ
,
authG
Σ
A
}
{
T
:
Type
}
(
γ
:
gname
).
Definition
auth_own
(
a
:
A
)
:
iProp
Σ
:
=
own
γ
(
◯
a
).
...
...
@@ -57,10 +57,10 @@ End definitions.
Typeclasses
Opaque
auth_own
auth_inv
auth_ctx
.
Instance
:
Params
(@
auth_own
)
4
.
Instance
:
Params
(@
auth_inv
)
5
.
Instance
:
Params
(@
auth_ctx
)
8
.
Instance
:
Params
(@
auth_ctx
)
7
.
Section
auth
.
Context
`
{
i
risG
Λ
Σ
,
authG
Σ
A
}.
Context
`
{
i
nvG
Σ
,
authG
Σ
A
}.
Context
{
T
:
Type
}
`
{!
Inhabited
T
}.
Context
(
f
:
T
→
A
)
(
φ
:
T
→
iProp
Σ
).
Implicit
Types
N
:
namespace
.
...
...
@@ -146,4 +146,4 @@ Section auth.
Qed
.
End
auth
.
Arguments
auth_open
{
_
_
_
_
}
[
_
]
{
_
}
[
_
]
_
_
_
_
_
_
_
.
Arguments
auth_open
{
_
_
_
}
[
_
]
{
_
}
[
_
]
_
_
_
_
_
_
_
.
program
_logic/boxes.v
→
base
_logic/
lib/
boxes.v
View file @
ed3b7e73
From
iris
.
program
_logic
Require
Export
invariants
.
From
iris
.
base
_logic
.
lib
Require
Export
invariants
.
From
iris
.
algebra
Require
Import
auth
gmap
agree
.
From
iris
.
base_logic
Require
Import
big_op
.
From
iris
.
proofmode
Require
Import
tactics
.
...
...
@@ -11,7 +11,7 @@ Class boxG Σ :=
(
optionR
(
agreeR
(
laterC
(
iPreProp
Σ
))))).
Section
box_defs
.
Context
`
{
i
risG
Λ
Σ
,
boxG
Σ
}
(
N
:
namespace
).
Context
`
{
i
nvG
Σ
,
boxG
Σ
}
(
N
:
namespace
).
Definition
slice_name
:
=
gname
.
...
...
@@ -34,14 +34,13 @@ Section box_defs.
inv
N
(
slice_inv
γ
(
Φ
γ
)))%
I
.
End
box_defs
.
Instance
:
Params
(@
box_own_auth
)
5
.
Instance
:
Params
(@
box_own_prop
)
5
.
Instance
:
Params
(@
slice_inv
)
5
.
Instance
:
Params
(@
slice
)
6
.
Instance
:
Params
(@
box
)
6
.
Instance
:
Params
(@
box_own_prop
)
3
.
Instance
:
Params
(@
slice_inv
)
3
.
Instance
:
Params
(@
slice
)
5
.
Instance
:
Params
(@
box
)
5
.
Section
box
.
Context
`
{
i
risG
Λ
Σ
,
boxG
Σ
}
(
N
:
namespace
).
Context
`
{
i
nvG
Σ
,
boxG
Σ
}
(
N
:
namespace
).
Implicit
Types
P
Q
:
iProp
Σ
.
Global
Instance
box_own_prop_ne
n
γ
:
Proper
(
dist
n
==>
dist
n
)
(
box_own_prop
γ
).
...
...
program
_logic/cancelable_invariants.v
→
base
_logic/
lib/
cancelable_invariants.v
View file @
ed3b7e73
From
iris
.
program
_logic
Require
Export
invariants
.
From
iris
.
base
_logic
.
lib
Require
Export
invariants
.
From
iris
.
algebra
Require
Export
frac
.
From
iris
.
proofmode
Require
Import
tactics
.
Import
uPred
.
...
...
@@ -6,7 +6,7 @@ Import uPred.
Class
cinvG
Σ
:
=
cinv_inG
:
>
inG
Σ
fracR
.
Section
defs
.
Context
`
{
i
risG
Λ
Σ
,
cinvG
Σ
}.
Context
`
{
i
nvG
Σ
,
cinvG
Σ
}.
Definition
cinv_own
(
γ
:
gname
)
(
p
:
frac
)
:
iProp
Σ
:
=
own
γ
p
.
...
...
@@ -14,11 +14,11 @@ Section defs.
inv
N
(
P
∨
cinv_own
γ
1
%
Qp
)%
I
.
End
defs
.
Instance
:
Params
(@
cinv
)
6
.
Instance
:
Params
(@
cinv
)
5
.
Typeclasses
Opaque
cinv_own
cinv
.
Section
proofs
.
Context
`
{
i
risG
Λ
Σ
,
cinvG
Σ
}.
Context
`
{
i
nvG
Σ
,
cinvG
Σ
}.
Global
Instance
cinv_own_timeless
γ
p
:
TimelessP
(
cinv_own
γ
p
).
Proof
.
rewrite
/
cinv_own
;
apply
_
.
Qed
.
...
...
program
_logic/counter_examples.v
→
base
_logic/
lib/
counter_examples.v
View file @
ed3b7e73
File moved
program
_logic/fancy_updates.v
→
base
_logic/
lib/
fancy_updates.v
View file @
ed3b7e73
From
iris
.
program_logic
Require
Export
iris
.
From
iris
.
program_logic
Require
Import
wsat
.
From
iris
.
base_logic
.
lib
Require
Export
own
.
From
iris
.
prelude
Require
Export
coPset
.
From
iris
.
base_logic
.
lib
Require
Import
wsat
.
From
iris
.
algebra
Require
Import
gmap
.
From
iris
.
base_logic
Require
Import
big_op
.
From
iris
.
proofmode
Require
Import
tactics
classes
.
Export
invG
.
Import
uPred
.
Program
Definition
fupd_def
`
{
i
risG
Λ
Σ
}
Program
Definition
fupd_def
`
{
i
nvG
Σ
}
(
E1
E2
:
coPset
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
(
wsat
★
ownE
E1
==
★
◇
(
wsat
★
ownE
E2
★
P
))%
I
.
Definition
fupd_aux
:
{
x
|
x
=
@
fupd_def
}.
by
eexists
.
Qed
.
Definition
fupd
:
=
proj1_sig
fupd_aux
.
Definition
fupd_eq
:
@
fupd
=
@
fupd_def
:
=
proj2_sig
fupd_aux
.
Arguments
fupd
{
_
_
_
}
_
_
_
%
I
.
Instance
:
Params
(@
fupd
)
5
.
Arguments
fupd
{
_
_
}
_
_
_
%
I
.
Instance
:
Params
(@
fupd
)
4
.
Notation
"|={ E1 , E2 }=> Q"
:
=
(
fupd
E1
E2
Q
)
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
...
...
@@ -46,12 +48,12 @@ Notation "P ={ E }▷=★ Q" := (P ={E,E}▷=★ Q)%I
format
"P ={ E }▷=★ Q"
)
:
uPred_scope
.
Section
fupd
.
Context
`
{
i
risG
Λ
Σ
}.
Context
`
{
i
nvG
Σ
}.
Implicit
Types
P
Q
:
iProp
Σ
.
Global
Instance
fupd_ne
E1
E2
n
:
Proper
(
dist
n
==>
dist
n
)
(@
fupd
Λ
Σ
_
E1
E2
).
Global
Instance
fupd_ne
E1
E2
n
:
Proper
(
dist
n
==>
dist
n
)
(@
fupd
Σ
_
E1
E2
).
Proof
.
rewrite
fupd_eq
.
solve_proper
.
Qed
.
Global
Instance
fupd_proper
E1
E2
:
Proper
((
≡
)
==>
(
≡
))
(@
fupd
Λ
Σ
_
E1
E2
).
Global
Instance
fupd_proper
E1
E2
:
Proper
((
≡
)
==>
(
≡
))
(@
fupd
Σ
_
E1
E2
).
Proof
.
apply
ne_proper
,
_
.
Qed
.
Lemma
fupd_intro_mask
E1
E2
P
:
E2
⊆
E1
→
P
⊢
|={
E1
,
E2
}=>
|={
E2
,
E1
}=>
P
.
...
...
@@ -92,10 +94,10 @@ Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q.
Proof
.
rewrite
fupd_eq
/
fupd_def
.
by
iIntros
"[HwP $]"
.
Qed
.
(** * Derived rules *)
Global
Instance
fupd_mono'
E1
E2
:
Proper
((
⊢
)
==>
(
⊢
))
(@
fupd
Λ
Σ
_
E1
E2
).
Global
Instance
fupd_mono'
E1
E2
:
Proper
((
⊢
)
==>
(
⊢
))
(@
fupd
Σ
_
E1
E2
).
Proof
.
intros
P
Q
;
apply
fupd_mono
.
Qed
.
Global
Instance
fupd_flip_mono'
E1
E2
:
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
fupd
Λ
Σ
_
E1
E2
).
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
fupd
Σ
_
E1
E2
).
Proof
.
intros
P
Q
;
apply
fupd_mono
.
Qed
.
Lemma
fupd_intro
E
P
:
P
={
E
}=
★
P
.
...
...
@@ -148,7 +150,7 @@ End fupd.
(** Proofmode class instances *)
Section
proofmode_classes
.
Context
`
{
i
risG
Λ
Σ
}.
Context
`
{
i
nvG
Σ
}.
Implicit
Types
P
Q
:
iProp
Σ
.
Global
Instance
from_pure_fupd
E
P
φ
:
FromPure
P
φ
→
FromPure
(|={
E
}=>
P
)
φ
.
...
...
program
_logic/invariants.v
→
base
_logic/
lib/
invariants.v
View file @
ed3b7e73
From
iris
.
program_logic
Require
Export
fancy_updates
.
From
iris
.
program_logic
Require
Export
namespaces
.
From
iris
.
program_logic
Require
Import
wsat
.
From
iris
.
base_logic
.
lib
Require
Export
fancy_updates
namespaces
.
From
iris
.
base_logic
.
lib
Require
Import
wsat
.
From
iris
.
algebra
Require
Import
gmap
.
From
iris
.
proofmode
Require
Import
tactics
coq_tactics
intro_patterns
.
Import
uPred
.
(** Derived forms and lemmas about them. *)
Definition
inv_def
`
{
i
risG
Λ
Σ
}
(
N
:
namespace
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
Definition
inv_def
`
{
i
nvG
Σ
}
(
N
:
namespace
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
(
∃
i
,
■
(
i
∈
nclose
N
)
∧
ownI
i
P
)%
I
.
Definition
inv_aux
:
{
x
|
x
=
@
inv_def
}.
by
eexists
.
Qed
.
Definition
inv
{
Λ
Σ
i
}
:
=
proj1_sig
inv_aux
Λ
Σ
i
.
Definition
inv
{
Σ
i
}
:
=
proj1_sig
inv_aux
Σ
i
.
Definition
inv_eq
:
@
inv
=
@
inv_def
:
=
proj2_sig
inv_aux
.
Instance
:
Params
(@
inv
)
4
.
Instance
:
Params
(@
inv
)
3
.
Typeclasses
Opaque
inv
.
Section
inv
.
Context
`
{
i
risG
Λ
Σ
}.
Context
`
{
i
nvG
Σ
}.
Implicit
Types
i
:
positive
.
Implicit
Types
N
:
namespace
.
Implicit
Types
P
Q
R
:
iProp
Σ
.
Implicit
Types
Φ
:
val
Λ
→
iProp
Σ
.
Global
Instance
inv_contractive
N
:
Contractive
(
inv
N
).
Proof
.
...
...
program
_logic/namespaces.v
→
base
_logic/
lib/
namespaces.v
View file @
ed3b7e73
File moved
program
_logic/sts.v
→
base
_logic/
lib/
sts.v
View file @
ed3b7e73
From
iris
.
program
_logic
Require
Export
invariants
.
From
iris
.
base
_logic
.
lib
Require
Export
invariants
.
From
iris
.
algebra
Require
Export
sts
.
From
iris
.
proofmode
Require
Import
tactics
.
Import
uPred
.
...
...
@@ -15,7 +15,7 @@ Instance subG_stsΣ Σ sts :
Proof
.
intros
?%
subG_inG
?.
by
split
.
Qed
.
Section
definitions
.
Context
`
{
i
risG
Λ
Σ
,
stsG
Σ
sts
}
(
γ
:
gname
).
Context
`
{
i
nvG
Σ
,
stsG
Σ
sts
}
(
γ
:
gname
).
Definition
sts_ownS
(
S
:
sts
.
states
sts
)
(
T
:
sts
.
tokens
sts
)
:
iProp
Σ
:
=
own
γ
(
sts_frag
S
T
).
...
...
@@ -51,13 +51,13 @@ Section definitions.
End
definitions
.
Typeclasses
Opaque
sts_own
sts_ownS
sts_inv
sts_ctx
.
Instance
:
Params
(@
sts_inv
)
5
.
Instance
:
Params
(@
sts_ownS
)
5
.
Instance
:
Params
(@
sts_own
)
6
.
Instance
:
Params
(@
sts_inv
)
4
.
Instance
:
Params
(@
sts_ownS
)
4
.
Instance
:
Params
(@
sts_own
)
5
.
Instance
:
Params
(@
sts_ctx
)
6
.
Section
sts
.
Context
`
{
i
risG
Λ
Σ
,
stsG
Σ
sts
}
(
φ
:
sts
.
state
sts
→
iProp
Σ
).
Context
`
{
i
nvG
Σ
,
stsG
Σ
sts
}
(
φ
:
sts
.
state
sts
→
iProp
Σ
).
Implicit
Types
N
:
namespace
.
Implicit
Types
P
Q
R
:
iProp
Σ
.
Implicit
Types
γ
:
gname
.
...
...
@@ -115,7 +115,7 @@ Section sts.
■
sts
.
frame_steps
T
s0
s
★
▷
φ
s
★
∀
s'
T'
,
■
sts
.
steps
(
s
,
T
)
(
s'
,
T'
)
★
▷
φ
s'
={
E
}=
★
▷
sts_inv
γ
φ
★
sts_own
γ
s'
T'
.
Proof
.
by
apply
sts_accS
.
Qed
.
Lemma
sts_openS
E
N
γ
S
T
:
nclose
N
⊆
E
→
sts_ctx
γ
N
φ
★
sts_ownS
γ
S
T
={
E
,
E
∖
N
}=
★
∃
s
,
...
...
program
_logic/thread_local.v
→
base
_logic/
lib/
thread_local.v
View file @
ed3b7e73
From
iris
.
program
_logic
Require
Export
invariants
.
From
iris
.
base
_logic
.
lib
Require
Export
invariants
.
From
iris
.
algebra
Require
Export
gmap
gset
coPset
.
From
iris
.
proofmode
Require
Import
tactics
.
Import
uPred
.
...
...
@@ -10,7 +10,7 @@ Class thread_localG Σ :=
tl_inG
:
>
inG
Σ
(
prodR
coPset_disjR
(
gset_disjR
positive
)).
Section
defs
.
Context
`
{
i
risG
Λ
Σ
,
thread_localG
Σ
}.
Context
`
{
i
nvG
Σ
,
thread_localG
Σ
}.
Definition
tl_own
(
tid
:
thread_id
)
(
E
:
coPset
)
:
iProp
Σ
:
=
own
tid
(
CoPset
E
,
∅
).
...
...
@@ -20,11 +20,11 @@ Section defs.
inv
tlN
(
P
★
own
tid
(
∅
,
GSet
{[
i
]})
∨
tl_own
tid
{[
i
]}))%
I
.
End
defs
.
Instance
:
Params
(@
tl_inv
)
4
.
Instance
:
Params
(@
tl_inv
)
3
.
Typeclasses
Opaque
tl_own
tl_inv
.
Section
proofs
.
Context
`
{
i
risG
Λ
Σ
,
thread_localG
Σ
}.
Context
`
{
i
nvG
Σ
,
thread_localG
Σ
}.
Global
Instance
tl_own_timeless
tid
E
:
TimelessP
(
tl_own
tid
E
).
Proof
.
rewrite
/
tl_own
;
apply
_
.
Qed
.
...
...
program
_logic/viewshifts.v
→
base
_logic/
lib/
viewshifts.v
View file @
ed3b7e73
From
iris
.
program
_logic
Require
Export
invariants
.
From
iris
.
base
_logic
.
lib
Require
Export
invariants
.
From
iris
.
proofmode
Require
Import
tactics
.
Definition
vs
`
{
i
risG
Λ
Σ
}
(
E1
E2
:
coPset
)
(
P
Q
:
iProp
Σ
)
:
iProp
Σ
:
=
Definition
vs
`
{
i
nvG
Σ
}
(
E1
E2
:
coPset
)
(
P
Q
:
iProp
Σ
)
:
iProp
Σ
:
=
(
□
(
P
-
★
|={
E1
,
E2
}=>
Q
))%
I
.
Arguments
vs
{
_
_
_
}
_
_
_
%
I
_
%
I
.
Arguments
vs
{
_
_
}
_
_
_
%
I
_
%
I
.
Instance
:
Params
(@
vs
)
5
.
Instance
:
Params
(@
vs
)
4
.
Notation
"P ={ E1 , E2 }=> Q"
:
=
(
vs
E1
E2
P
Q
)
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
format
"P ={ E1 , E2 }=> Q"
)
:
uPred_scope
.
...
...
@@ -21,7 +21,7 @@ Notation "P ={ E }=> Q" := (True ⊢ P ={E}=> Q)%I
format
"P ={ E }=> Q"
)
:
C_scope
.
Section
vs
.
Context
`
{
i
risG
Λ
Σ
}.
Context
`
{
i
nvG
Σ
}.
Implicit
Types
P
Q
R
:
iProp
Σ
.
Implicit
Types
N
:
namespace
.
...
...
program
_logic/wsat.v
→
base
_logic/
lib/
wsat.v
View file @
ed3b7e73
From
iris
.
program_logic
Require
Export
iris
.
From
iris
.
base_logic
.
lib
Require
Export
own
.
From
iris
.
prelude
Require
Export
coPset
.
From
iris
.
algebra
Require
Import
gmap
auth
agree
gset
coPset
.
From
iris
.
base_logic
Require
Import
big_op
.
From
iris
.
proofmode
Require
Import
tactics
.
Module
invG
.
Class
invG
(
Σ
:
gFunctors
)
:
Set
:
=
WsatG
{
inv_inG
:
>
inG
Σ
(
authR
(
gmapUR
positive
(
agreeR
(
laterC
(
iPreProp
Σ
)))))
;
enabled_inG
:
>
inG
Σ
coPset_disjR
;
disabled_inG
:
>
inG
Σ
(
gset_disjR
positive
)
;
invariant_name
:
gname
;
enabled_name
:
gname
;
disabled_name
:
gname
;
}.
End
invG
.
Import
invG
.
Definition
invariant_unfold
{
Σ
}
(
P
:
iProp
Σ
)
:
agree
(
later
(
iPreProp
Σ
))
:
=
to_agree
(
Next
(
iProp_unfold
P
)).
Definition
ownI
`
{
i
risG
Λ
Σ
}
(
i
:
positive
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
Definition
ownI
`
{
i
nvG
Σ
}
(
i
:
positive
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
own
invariant_name
(
◯
{[
i
:
=
invariant_unfold
P
]}).
Arguments
ownI
{
_
_
_
}
_
_
%
I
.
Arguments
ownI
{
_
_
}
_
_
%
I
.
Typeclasses
Opaque
ownI
.
Instance
:
Params
(@
ownI
)
4
.
Definition
ownP
`
{
irisG
Λ
Σ
}
(
σ
:
state
Λ
)
:
iProp
Σ
:
=
own
state_name
(
◯
(
Excl'
σ
)).
Typeclasses
Opaque
ownP
.
Instance
:
Params
(@
ownP
)
4
.
Definition
ownP_auth
`
{
irisG
Λ
Σ
}
(
σ
:
state
Λ
)
:
iProp
Σ
:
=
own
state_name
(
●
(
Excl'
σ
)).
Typeclasses
Opaque
ownP_auth
.
Instance
:
Params
(@
ownP_auth
)
4
.
Instance
:
Params
(@
ownI
)
3
.
Definition
ownE
`
{
i
risG
Λ
Σ
}
(
E
:
coPset
)
:
iProp
Σ
:
=
Definition
ownE
`
{
i
nvG
Σ
}
(
E
:
coPset
)
:
iProp
Σ
:
=
own
enabled_name
(
CoPset
E
).
Typeclasses
Opaque
ownE
.
Instance
:
Params
(@
ownE
)
4
.
Instance
:
Params
(@
ownE
)
3
.
Definition
ownD
`
{
i
risG
Λ
Σ
}
(
E
:
gset
positive
)
:
iProp
Σ
:
=
Definition
ownD
`
{
i
nvG
Σ
}
(
E
:
gset
positive
)
:
iProp
Σ
:
=
own
disabled_name
(
GSet
E
).
Typeclasses
Opaque
ownD
.
Instance
:
Params
(@
ownD
)
4
.
Instance
:
Params
(@
ownD
)
3
.
Definition
wsat
`
{
i
risG
Λ
Σ
}
:
iProp
Σ
:
=
Definition
wsat
`
{
i
nvG
Σ
}
:
iProp
Σ
:
=
(
∃
I
:
gmap
positive
(
iProp
Σ
),
own
invariant_name
(
●
(
invariant_unfold
<$>
I
:
gmap
_
_
))
★
[
★
map
]
i
↦
Q
∈
I
,
▷
Q
★
ownD
{[
i
]}
∨
ownE
{[
i
]})%
I
.
Section
ownership
.
Context
`
{
irisG
Λ
Σ
}.
Implicit
Types
σ
:
state
Λ
.
Section
wsat
.
Context
`
{
invG
Σ
}.
Implicit
Types
P
:
iProp
Σ
.
(* Allocation *)
Lemma
iris_alloc
`
{
irisPreG
Λ
Σ
}
σ
:
True
==
★
∃
_
:
irisG
Λ
Σ
,
wsat
★
ownE
⊤
★
ownP_auth
σ
★
ownP
σ
.
Proof
.
iIntros
.
iMod
(
own_alloc
(
●
(
Excl'
σ
)
⋅
◯
(
Excl'
σ
)))
as
(
γσ
)
"[Hσ Hσ']"
;
first
done
.
iMod
(
own_alloc
(
●
(
∅
:
gmap
_
_
)))
as
(
γ
I
)
"HI"
;
first
done
.
iMod
(
own_alloc
(
CoPset
⊤
))
as
(
γ
E
)
"HE"
;
first
done
.
iMod
(
own_alloc
(
GSet
∅
))
as
(
γ
D
)
"HD"
;
first
done
.
iModIntro
;
iExists
(
IrisG
_
_
_
γσ
γ
I
γ
E
γ
D
).
rewrite
/
wsat
/
ownE
/
ownP_auth
/
ownP
;
iFrame
.
iExists
∅
.
rewrite
fmap_empty
big_sepM_empty
.
by
iFrame
.
Qed
.
(* Physical state *)
Lemma
ownP_twice
σ
1
σ
2
:
ownP
σ
1
★
ownP
σ
2
⊢
False
.
Proof
.
rewrite
/
ownP
own_valid_2
.
by
iIntros
(?).
Qed
.
Global
Instance
ownP_timeless
σ
:
TimelessP
(@
ownP
Λ
Σ
_
σ
).
Proof
.
rewrite
/
ownP
;
apply
_
.
Qed
.
Lemma
ownP_agree
σ
1
σ
2
:
ownP_auth
σ
1
★
ownP
σ
2
⊢
σ
1
=
σ
2
.
Proof
.
rewrite
/
ownP
/
ownP_auth
own_valid_2
-
auth_both_op
.
by
iIntros
([[[]
[=]%
leibniz_equiv
]
_
]%
auth_valid_discrete
).
Qed
.
Lemma
ownP_update
σ
1
σ
2
:
ownP_auth
σ
1
★
ownP
σ
1
==
★
ownP_auth
σ
2
★
ownP
σ
2
.
Proof
.
rewrite
/
ownP
-!
own_op
.
by
apply
own_update
,
auth_update
,
option_local_update
,
exclusive_local_update
.
Qed
.
(* Invariants *)
Global
Instance
ownI_contractive
i
:
Contractive
(@
ownI
Λ
Σ
_
i
).
Global
Instance
ownI_contractive
i
:
Contractive
(@
ownI
Σ
_
i
).
Proof
.
intros
n
P
Q
HPQ
.
rewrite
/
ownI
/
invariant_unfold
.
do
4
f_equiv
.
apply
Next_contractive
=>
j
?
;
by
rewrite
(
HPQ
j
).
...
...
@@ -111,7 +82,7 @@ Qed.
Lemma
ownD_singleton_twice
i
:
ownD
{[
i
]}
★
ownD
{[
i
]}
⊢
False
.
Proof
.
rewrite
ownD_disjoint
.
iIntros
(?)
;
set_solver
.
Qed
.
Lemma
invariant_lookup
`
{
irisG
Λ
Σ
}
(
I
:
gmap
positive
(
iProp
Σ
))
i
P
:
Lemma
invariant_lookup
(
I
:
gmap
positive
(
iProp
Σ
))
i
P
:
own
invariant_name
(
●
(
invariant_unfold
<$>
I
:
gmap
_
_
))
★
own
invariant_name
(
◯
{[
i
:
=
invariant_unfold
P
]})
⊢
∃
Q
,
I
!!
i
=
Some
Q
★
▷
(
Q
≡
P
).
...
...
@@ -171,4 +142,4 @@ Proof.
iApply
(
big_sepM_insert
_
I
)
;
first
done
.
iFrame
"HI"
.
iLeft
.
by
rewrite
/
ownD
;
iFrame
.
Qed
.
End
ownership
.
End
wsat
.
heap_lang/adequacy.v
View file @
ed3b7e73
From
iris
.
program_logic
Require
Export
weakestpre
adequacy
.
From
iris
.
heap_lang
Require
Export
heap
.
From
iris
.
algebra
Require
Import
auth
.
From
iris
.
program
_logic
Require
Import
wsat
auth
.
From
iris
.
base
_logic
.
lib
Require
Import
wsat
auth
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
proofmode
Require
Import
tactics
.
...
...
@@ -11,7 +11,7 @@ Class heapPreG Σ := HeapPreG {
}.
Definition
heap
Σ
:
gFunctors
:
=
#[
iris
Σ
heap_lang
;
auth
Σ
heapUR
].
#[
iris
Σ
state
;
auth
Σ
heapUR
].
Instance
subG_heapPreG
{
Σ
}
:
subG
heap
Σ
Σ
→
heapPreG
Σ
.
Proof
.
intros
[?
?]%
subG_inv
.
split
;
apply
_
.
Qed
.
...
...
heap_lang/heap.v
View file @
ed3b7e73
From
iris
.
heap_lang
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
auth
gmap
frac
dec_agree
.
From
iris
.
program
_logic
Require
Export
invariants
.
From
iris
.
program
_logic
Require
Import
wsat
auth
.
From
iris
.
base
_logic
.
lib
Require
Export
invariants
.
From
iris
.
base
_logic
.
lib
Require
Import
wsat
auth
.
From
iris
.
proofmode
Require
Import
tactics
.
Import
uPred
.
(* TODO: The entire construction could be generalized to arbitrary languages that have
...
...
heap_lang/lib/barrier/proof.v
View file @
ed3b7e73
...
...
@@ -2,8 +2,7 @@ From iris.program_logic Require Export weakestpre.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Export
barrier
.
From
iris
.
prelude
Require
Import
functions
.
From
iris
.
base_logic
Require
Import
big_op
lib
.
saved_prop
.
From
iris
.
program_logic
Require
Import
sts
.
From
iris
.
base_logic
Require
Import
big_op
lib
.
saved_prop
lib
.
sts
.
From
iris
.
heap_lang
Require
Import
proofmode
.
From
iris
.
heap_lang
.
lib
.
barrier
Require
Import
protocol
.
...
...
heap_lang/lifting.v
View file @
ed3b7e73
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
program_logic
Require
Import
wsat
ectx_lifting
.
(* for ownP *)
From
iris
.
program_logic
Require
Import
ectx_lifting
.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
Require
Import
tactics
.
From
iris
.
proofmode
Require
Import
tactics
.
...
...
program_logic/adequacy.v
View file @
ed3b7e73
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
algebra
Require
Import
gmap
auth
agree
gset
coPset
.
From
iris
.
base_logic
Require
Import
big_op
soundness
.
From
iris
.
program
_logic
Require
Import
wsat
.
From
iris
.
base
_logic
.
lib
Require
Import
wsat
.
From
iris
.
proofmode
Require
Import
tactics
.
Import
uPred
.
(* Global functor setup *)
Definition
inv
Σ
:
gFunctors
:
=
#[
GFunctor
(
authRF
(
gmapURF
positive
(
agreeRF
(
laterCF
idCF
))))
;
GFunctor
(
constRF
coPset_disjUR
)
;
GFunctor
(
constRF
(
gset_disjUR
positive
))].
Class
invPreG
(
Σ
:
gFunctors
)
:
Set
:
=
WsatPreG
{
inv_inPreG
:
>
inG
Σ
(
authR
(
gmapUR
positive
(
agreeR
(
laterC
(
iPreProp
Σ
)))))
;
enabled_inPreG
:
>
inG
Σ
coPset_disjR
;
disabled_inPreG
:
>
inG
Σ
(
gset_disjR
positive
)
;
}.
Instance
subG_inv
Σ
{
Σ
}
:
subG
inv
Σ
Σ
→
invPreG
Σ
.
Proof
.
intros
[?%
subG_inG
[?%
subG_inG
?%
subG_inG
]%
subG_inv
]%
subG_inv
;
by
constructor
.
Qed
.
Definition
iris
Σ
(
Λ
state
:
Type
)
:
gFunctors
:
=
#[
inv
Σ
;
GFunctor
(
constRF
(
authUR
(
optionUR
(
exclR
(
leibnizC
Λ
state
)))))].
Class
irisPreG'
(
Λ
state
:
Type
)
(
Σ
:
gFunctors
)
:
Set
:
=
IrisPreG
{
inv_inG
:
>
invPreG
Σ
;
state_inG
:
>
inG
Σ
(
authR
(
optionUR
(
exclR
(
leibnizC
Λ
state
))))
}.
Notation
irisPreG
Λ
Σ
:
=
(
irisPreG'
(
state
Λ
)
Σ
).
Instance
subG_iris
Σ
{
Λ
state
Σ
}
:
subG
(
iris
Σ
Λ
state
)
Σ
→
irisPreG'
Λ
state
Σ
.
Proof
.
intros
[??%
subG_inG
]%
subG_inv
;
constructor
;
apply
_
.
Qed
.
(* Allocation *)
Lemma
wsat_alloc
`
{
invPreG
Σ
}
:
True
==
★
∃
_
:
invG
Σ
,
wsat
★
ownE
⊤
.
Proof
.
iIntros
.
iMod
(
own_alloc
(
●
(
∅
:
gmap
_
_
)))
as
(
γ
I
)
"HI"
;
first
done
.
iMod
(
own_alloc
(
CoPset
⊤
))
as
(
γ
E
)
"HE"
;
first
done
.
iMod
(
own_alloc
(
GSet
∅
))
as
(
γ
D
)
"HD"
;
first
done
.
iModIntro
;
iExists
(
WsatG
_
_
_
_
γ
I
γ
E
γ
D
).
rewrite
/
wsat
/
ownE
;
iFrame
.
iExists
∅
.
rewrite
fmap_empty
big_sepM_empty
.
by
iFrame
.
Qed
.
Lemma
iris_alloc
`
{
irisPreG'
Λ
state
Σ
}
σ
:
True
==
★
∃
_
:
irisG'
Λ
state
Σ
,
wsat
★
ownE
⊤
★
ownP_auth
σ
★
ownP
σ
.
Proof
.
iIntros
.
iMod