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
Jonas Kastberg
iris
Commits
8ec972e7
Commit
8ec972e7
authored
Jan 12, 2017
by
Ralf Jung
Browse files
Merge branch 'master' of
https://gitlab.mpi-sws.org/FP/iris-coq
parents
927dd1a0
f632b27f
Changes
5
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/lib/counter.v
View file @
8ec972e7
...
...
@@ -85,10 +85,10 @@ End mono_proof.
Class
ccounterG
Σ
:
=
CCounterG
{
ccounter_inG
:
>
inG
Σ
(
authR
(
optionUR
(
prodR
fracR
natR
)))
}.
Definition
ccounter
Σ
:
gFunctors
:
=
#[
GFunctor
(
constRF
(
authR
(
optionUR
(
prodR
fracR
natR
)))
)
].
#[
GFunctor
(
authR
(
optionUR
(
prodR
fracR
natR
)))].
Instance
subG_ccounter
Σ
{
Σ
}
:
subG
ccounter
Σ
Σ
→
ccounterG
Σ
.
Proof
.
intros
[?%
subG_inG
_
]%
subG_inv
.
split
;
apply
_
.
Qed
.
Proof
.
solve_inG
.
Qed
.
Section
contrib_spec
.
Context
`
{!
heapG
Σ
,
!
ccounterG
Σ
}
(
N
:
namespace
).
...
...
theories/program_logic/adequacy.v
View file @
8ec972e7
...
...
@@ -72,12 +72,11 @@ Lemma wp_step e1 σ1 e2 σ2 efs Φ :
prim_step
e1
σ
1 e2
σ
2
efs
→
world
σ
1
∗
WP
e1
{{
Φ
}}
==
∗
▷
|==>
◇
(
world
σ
2
∗
WP
e2
{{
Φ
}}
∗
wptp
efs
).
Proof
.
rewrite
{
1
}
wp_unfold
/
wp_pre
.
iIntros
(
Hstep
)
"[(Hw & HE & Hσ) [H|[_ H]]]"
.
{
iDestruct
"H"
as
(
v
)
"[% _]"
.
apply
val_stuck
in
Hstep
;
simplify_eq
.
}
rewrite
fupd_eq
/
fupd_def
.
rewrite
{
1
}
wp_unfold
/
wp_pre
.
iIntros
(?)
"[(Hw & HE & Hσ) H]"
.
rewrite
(
val_stuck
e1
σ
1 e2
σ
2
efs
)
//
fupd_eq
/
fupd_def
.
iMod
(
"H"
$!
σ
1
with
"Hσ [Hw HE]"
)
as
">(Hw & HE & _ & H)"
;
first
by
iFrame
.
iModIntro
;
iNext
.
by
iMod
(
"H"
$!
e2
σ
2
efs
with
"[%] [$Hw $HE]"
)
as
">($ & $ & $ & $)"
.
iMod
(
"H"
$!
e2
σ
2
efs
with
"[%] [$Hw $HE]"
)
as
">($ & $ & $ & $)"
;
auto
.
Qed
.
Lemma
wptp_step
e1
t1
t2
σ
1
σ
2
Φ
:
...
...
@@ -133,8 +132,8 @@ Qed.
Lemma
wp_safe
e
σ
Φ
:
world
σ
∗
WP
e
{{
Φ
}}
==
∗
▷
⌜
is_Some
(
to_val
e
)
∨
reducible
e
σ⌝
.
Proof
.
rewrite
wp_unfold
/
wp_pre
.
iIntros
"[(Hw&HE&Hσ)
[H|[_ H]]
]"
.
{
iD
estruct
"H"
as
(
v
)
"[% _]"
;
eauto
10
.
}
rewrite
wp_unfold
/
wp_pre
.
iIntros
"[(Hw&HE&Hσ)
H
]"
.
d
estruct
(
to_val
e
)
as
[
v
|]
eqn
:
?
;
[
eauto
10
|].
rewrite
fupd_eq
.
iMod
(
"H"
with
"* Hσ [-]"
)
as
">(?&?&%&?)"
;
first
by
iFrame
.
eauto
10
.
Qed
.
...
...
theories/program_logic/lifting.v
View file @
8ec972e7
...
...
@@ -18,7 +18,7 @@ Lemma wp_lift_step E Φ e1 :
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
state_interp
σ
2
∗
WP
e2
@
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
{{
_
,
True
}})
⊢
WP
e1
@
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
rewrite
wp_unfold
/
wp_pre
;
auto
.
Qed
.
Proof
.
by
rewrite
wp_unfold
/
wp_pre
=>
->
.
Qed
.
(** Derived lifting lemmas. *)
Lemma
wp_lift_pure_step
`
{
Inhabited
(
state
Λ
)}
E
Φ
e1
:
...
...
theories/program_logic/weakestpre.v
View file @
8ec972e7
...
...
@@ -13,15 +13,15 @@ Notation irisG Λ Σ := (irisG' (state Λ) Σ).
Definition
wp_pre
`
{
irisG
Λ
Σ
}
(
wp
:
coPset
-
c
>
expr
Λ
-
c
>
(
val
Λ
-
c
>
iProp
Σ
)
-
c
>
iProp
Σ
)
:
coPset
-
c
>
expr
Λ
-
c
>
(
val
Λ
-
c
>
iProp
Σ
)
-
c
>
iProp
Σ
:
=
λ
E
e1
Φ
,
(
(* value case *)
(
∃
v
,
⌜
to_val
e1
=
Some
v
⌝
∧
|={
E
}=>
Φ
v
)
∨
(* step case *)
(
⌜
to_val
e1
=
None
⌝
∧
∀
σ
1
,
coPset
-
c
>
expr
Λ
-
c
>
(
val
Λ
-
c
>
iProp
Σ
)
-
c
>
iProp
Σ
:
=
λ
E
e1
Φ
,
match
to_val
e1
with
|
Some
v
=>
|={
E
}=>
Φ
v
|
None
=>
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
reducible
e1
σ
1
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
state_interp
σ
2
∗
wp
E
e2
Φ
∗
[
∗
list
]
ef
∈
efs
,
wp
⊤
ef
(
λ
_
,
True
)))%
I
.
[
∗
list
]
ef
∈
efs
,
wp
⊤
ef
(
λ
_
,
True
)
end
%
I
.
Local
Instance
wp_pre_contractive
`
{
irisG
Λ
Σ
}
:
Contractive
wp_pre
.
Proof
.
...
...
@@ -110,7 +110,7 @@ Proof.
(* FIXME: figure out a way to properly automate this proof *)
(* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
is very slow here *)
do
1
8
(
f_contractive
||
f_equiv
).
apply
IH
;
first
lia
.
do
1
7
(
f_contractive
||
f_equiv
).
apply
IH
;
first
lia
.
intros
v
.
eapply
dist_le
;
eauto
with
omega
.
Qed
.
Global
Instance
wp_proper
E
e
:
...
...
@@ -120,25 +120,17 @@ Proof.
Qed
.
Lemma
wp_value'
E
Φ
v
:
Φ
v
⊢
WP
of_val
v
@
E
{{
Φ
}}.
Proof
.
iIntros
"HΦ"
.
rewrite
wp_unfold
/
wp_pre
.
iLeft
;
iExists
v
;
rewrite
to_of_val
;
auto
.
Qed
.
Proof
.
iIntros
"HΦ"
.
rewrite
wp_unfold
/
wp_pre
to_of_val
.
auto
.
Qed
.
Lemma
wp_value_inv
E
Φ
v
:
WP
of_val
v
@
E
{{
Φ
}}
={
E
}=
∗
Φ
v
.
Proof
.
rewrite
wp_unfold
/
wp_pre
to_of_val
.
iIntros
"[H|[% _]]"
;
[|
done
].
by
iDestruct
"H"
as
(
v'
)
"[% ?]"
;
simplify_eq
.
Qed
.
Proof
.
by
rewrite
wp_unfold
/
wp_pre
to_of_val
.
Qed
.
Lemma
wp_strong_mono
E1
E2
e
Φ
Ψ
:
E1
⊆
E2
→
(
∀
v
,
Φ
v
={
E2
}=
∗
Ψ
v
)
∗
WP
e
@
E1
{{
Φ
}}
⊢
WP
e
@
E2
{{
Ψ
}}.
Proof
.
iIntros
(?)
"[HΦ H]"
.
iL
ö
b
as
"IH"
forall
(
e
).
rewrite
!
wp_unfold
/
wp_pre
.
iDestruct
"H"
as
"[Hv|[% H]]"
;
[
iLeft
|
iRight
].
{
iDestruct
"Hv"
as
(
v
)
"[% Hv]"
.
iExists
v
;
iSplit
;
first
done
.
iApply
(
"HΦ"
with
">[-]"
).
by
iApply
(
fupd_mask_mono
E1
_
).
}
iSplit
;
[
done
|]
;
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
fupd_intro_mask'
E2
E1
)
as
"Hclose"
;
first
done
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
?.
{
iApply
(
"HΦ"
with
">[-]"
).
by
iApply
(
fupd_mask_mono
E1
_
).
}
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
fupd_intro_mask'
E2
E1
)
as
"Hclose"
;
first
done
.
iMod
(
"H"
$!
σ
1
with
"Hσ"
)
as
"[$ H]"
.
iModIntro
.
iNext
.
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
$!
_
σ
2
efs
with
"[#]"
)
as
"($ & H & $)"
;
auto
.
...
...
@@ -148,11 +140,8 @@ Qed.
Lemma
fupd_wp
E
e
Φ
:
(|={
E
}=>
WP
e
@
E
{{
Φ
}})
⊢
WP
e
@
E
{{
Φ
}}.
Proof
.
rewrite
wp_unfold
/
wp_pre
.
iIntros
"H"
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
?.
{
iLeft
.
iExists
v
;
iSplit
;
first
done
.
by
iMod
"H"
as
"[H|[% ?]]"
;
[
iDestruct
"H"
as
(
v'
)
"[% ?]"
|]
;
simplify_eq
.
}
iRight
;
iSplit
;
[
done
|]
;
iIntros
(
σ
1
)
"Hσ1"
.
iMod
"H"
as
"[H|[% H]]"
;
last
by
iApply
"H"
.
iDestruct
"H"
as
(
v'
)
"[% ?]"
;
simplify_eq
.
{
by
iMod
"H"
.
}
iIntros
(
σ
1
)
"Hσ1"
.
iMod
"H"
.
by
iApply
"H"
.
Qed
.
Lemma
wp_fupd
E
e
Φ
:
WP
e
@
E
{{
v
,
|={
E
}=>
Φ
v
}}
⊢
WP
e
@
E
{{
Φ
}}.
Proof
.
iIntros
"H"
.
iApply
(
wp_strong_mono
E
)
;
try
iFrame
;
auto
.
Qed
.
...
...
@@ -161,32 +150,24 @@ Lemma wp_atomic E1 E2 e Φ :
atomic
e
→
(|={
E1
,
E2
}=>
WP
e
@
E2
{{
v
,
|={
E2
,
E1
}=>
Φ
v
}})
⊢
WP
e
@
E1
{{
Φ
}}.
Proof
.
iIntros
(
Hatomic
)
"H"
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
He
.
{
apply
of_to_val
in
He
as
<-.
iApply
wp_fupd
.
iApply
wp_value'
.
iMod
"H"
.
by
iMod
(
wp_value_inv
with
"H"
).
}
setoid_rewrite
wp_unfold
;
rewrite
/
wp_pre
.
iRight
;
iSplit
;
auto
.
iIntros
(
σ
1
)
"Hσ"
.
iMod
"H"
as
"[H|[_ H]]"
.
{
iDestruct
"H"
as
(
v'
)
"[% ?]"
;
simplify_eq
.
}
iMod
(
"H"
$!
σ
1
with
"Hσ"
)
as
"[$ H]"
.
iIntros
(
Hatomic
)
"H"
.
rewrite
!
wp_unfold
/
wp_pre
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
He
.
{
by
iDestruct
"H"
as
">>> $"
.
}
iIntros
(
σ
1
)
"Hσ"
.
iMod
"H"
.
iMod
(
"H"
$!
σ
1
with
"Hσ"
)
as
"[$ H]"
.
iModIntro
.
iNext
.
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
with
"* []"
)
as
"(Hphy & H & $)"
;
first
done
.
rewrite
wp_unfold
/
wp_pre
.
iDestruct
"H"
as
"[H|H]"
.
-
iDestruct
"H"
as
(
v
)
"[% >>?]"
.
iModIntro
.
iFrame
.
rewrite
-(
of_to_val
e2
v
)
//.
by
iApply
wp_value'
.
-
iDestruct
"H"
as
"[_ H]"
.
iMod
(
"H"
with
"* Hphy"
)
as
"[H _]"
.
iDestruct
"H"
as
%(?
&
?
&
?
&
?).
exfalso
.
by
eapply
(
Hatomic
_
_
_
_
Hstep
).
rewrite
!
wp_unfold
/
wp_pre
.
destruct
(
to_val
e2
)
as
[
v2
|]
eqn
:
He2
.
-
iDestruct
"H"
as
">> $"
.
iFrame
.
eauto
.
-
iMod
(
"H"
with
"* Hphy"
)
as
"[H _]"
.
iDestruct
"H"
as
%(?
&
?
&
?
&
?).
by
edestruct
(
Hatomic
_
_
_
_
Hstep
).
Qed
.
Lemma
wp_fupd_step
E1
E2
e
P
Φ
:
to_val
e
=
None
→
E2
⊆
E1
→
(|={
E1
,
E2
}
▷
=>
P
)
-
∗
WP
e
@
E2
{{
v
,
P
={
E1
}=
∗
Φ
v
}}
-
∗
WP
e
@
E1
{{
Φ
}}.
Proof
.
rewrite
!
wp_unfold
/
wp_pre
.
iIntros
(??)
"HR [Hv|[_ H]]"
.
{
iDestruct
"Hv"
as
(
v
)
"[% Hv]"
;
simplify_eq
.
}
iRight
;
iSplit
;
[
done
|].
iIntros
(
σ
1
)
"Hσ"
.
iMod
"HR"
.
iMod
(
"H"
$!
_
with
"Hσ"
)
as
"[$ H]"
.
rewrite
!
wp_unfold
/
wp_pre
.
iIntros
(->
?)
"HR H"
.
iIntros
(
σ
1
)
"Hσ"
.
iMod
"HR"
.
iMod
(
"H"
$!
_
with
"Hσ"
)
as
"[$ H]"
.
iModIntro
;
iNext
;
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
$!
e2
σ
2
efs
with
"[%]"
)
as
"($ & H & $)"
;
auto
.
iMod
"HR"
.
iModIntro
.
iApply
(
wp_strong_mono
E2
)
;
first
done
.
...
...
@@ -197,12 +178,10 @@ Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
WP
e
@
E
{{
v
,
WP
K
(
of_val
v
)
@
E
{{
Φ
}}
}}
⊢
WP
K
e
@
E
{{
Φ
}}.
Proof
.
iIntros
"H"
.
iL
ö
b
as
"IH"
forall
(
E
e
Φ
).
rewrite
wp_unfold
/
wp_pre
.
iDestruct
"H"
as
"[Hv|[% H]]"
.
{
iDestruct
"Hv"
as
(
v
)
"[Hev Hv]"
;
iDestruct
"Hev"
as
%
<-%
of_to_val
.
by
iApply
fupd_wp
.
}
rewrite
wp_unfold
/
wp_pre
.
iRight
;
iSplit
;
eauto
using
fill_not_val
.
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
"H"
$!
_
with
"Hσ"
)
as
"[% H]"
.
iModIntro
;
iSplit
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
He
.
{
apply
of_to_val
in
He
as
<-.
by
iApply
fupd_wp
.
}
rewrite
wp_unfold
/
wp_pre
fill_not_val
//.
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
"H"
$!
_
with
"Hσ"
)
as
"[% H]"
.
iModIntro
;
iSplit
.
{
iPureIntro
.
unfold
reducible
in
*.
naive_solver
eauto
using
fill_step
.
}
iNext
;
iIntros
(
e2
σ
2
efs
Hstep
).
destruct
(
fill_step_inv
e
σ
1 e2
σ
2
efs
)
as
(
e2'
&->&?)
;
auto
.
...
...
theories/proofmode/tactics.v
View file @
8ec972e7
...
...
@@ -819,6 +819,27 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
")"
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
)
;
iIntro
(
x8
).
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
")"
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
;
iIntro
(
x9
).
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
simple_intropattern
(
x10
)
")"
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
;
iIntro
(
x10
).
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
simple_intropattern
(
x10
)
simple_intropattern
(
x11
)
")"
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
;
iIntro
(
x11
).
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
simple_intropattern
(
x10
)
simple_intropattern
(
x11
)
simple_intropattern
(
x12
)
")"
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
;
iIntro
(
x12
).
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
")"
constr
(
p
)
:
=
iIntros
(
x1
)
;
iIntros
p
.
...
...
@@ -848,6 +869,28 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
")"
constr
(
p
)
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
;
iIntros
p
.
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
")"
constr
(
p
)
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
;
iIntros
p
.
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
simple_intropattern
(
x10
)
")"
constr
(
p
)
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
;
iIntros
p
.
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
simple_intropattern
(
x10
)
simple_intropattern
(
x11
)
")"
constr
(
p
)
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
;
iIntros
p
.
Tactic
Notation
"iIntros"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
simple_intropattern
(
x10
)
simple_intropattern
(
x11
)
simple_intropattern
(
x12
)
")"
constr
(
p
)
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
;
iIntros
p
.
(* Used for generalization in iInduction and iLöb *)
Tactic
Notation
"iRevertIntros"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
...
...
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