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
Iris
Tutorial POPL18
Commits
5fc7f232
Commit
5fc7f232
authored
Feb 18, 2020
by
Robbert Krebbers
Browse files
Make demo compile with recent Iris, and add to _CoqProject (and thus CI).
parent
fc782dc4
Pipeline
#24335
passed with stage
in 3 minutes and 18 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
5fc7f232
-Q exercises exercises
-Q solutions solutions
-Q talks/demo demo
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
...
...
@@ -7,6 +8,10 @@
# Can be triggered when importing some Iris files.
-arg -w -arg -notation-overridden
talks/demo/part1.v
talks/demo/part2.v
talks/demo/part3.v
talks/demo/part4.v
exercises/ex_01_swap.v
exercises/ex_02_sumlist.v
exercises/ex_03_spinlock.v
...
...
talks/demo/part2.v
View file @
5fc7f232
...
...
@@ -9,7 +9,7 @@ Definition strange_inc : val := λ: "p",
Lemma
strange_inc_spec1
`
{
heapG
Σ
}
l
(
x
:
Z
)
:
l
↦
#
x
-
∗
WP
strange_inc
#
l
{{
v
,
⌜
v
=
#()
⌝
∧
l
↦
#(
1
+
x
)
}}.
Proof
.
iIntros
"?"
.
wp_l
et
.
wp_alloc
k
.
wp_let
.
iIntros
"?"
.
wp_l
am
.
wp_alloc
k
.
wp_let
.
wp_load
.
wp_op
.
wp_store
.
wp_load
.
auto
.
Qed
.
...
...
@@ -21,7 +21,7 @@ Lemma strange_inc_twice_spec1 `{heapG Σ} l (x : Z) :
l
↦
#
x
-
∗
WP
strange_inc_twice
#
l
{{
v
,
⌜
v
=
#()
⌝
∧
l
↦
#(
2
+
x
)
}}.
Proof
.
iIntros
"Hl"
.
wp_l
et
.
wp_bind
(
strange_inc
_
).
iIntros
"Hl"
.
wp_l
am
.
wp_bind
(
strange_inc
_
).
(* now what? *)
Abort
.
...
...
@@ -30,14 +30,14 @@ Lemma strange_inc_spec2 `{heapG Σ} Φ l (x : Z) :
(
l
↦
#(
1
+
x
)
-
∗
Φ
#())
-
∗
WP
strange_inc
#
l
{{
Φ
}}.
Proof
.
iIntros
"Hl Post"
.
wp_l
et
.
wp_alloc
k
.
wp_let
.
iIntros
"Hl Post"
.
wp_l
am
.
wp_alloc
k
.
wp_let
.
wp_load
.
wp_op
.
wp_store
.
wp_load
.
by
iApply
"Post"
.
Qed
.
Lemma
strange_inc_spec
`
{
heapG
Σ
}
l
(
x
:
Z
)
:
{{{
l
↦
#
x
}}}
strange_inc
#
l
{{{
RET
#()
;
l
↦
#(
1
+
x
)
}}}.
Proof
.
iIntros
(
Φ
)
"? Post"
.
wp_l
et
.
wp_alloc
k
.
wp_let
.
iIntros
(
Φ
)
"? Post"
.
wp_l
am
.
wp_alloc
k
.
wp_let
.
wp_load
.
wp_op
.
wp_store
.
wp_load
.
by
iApply
"Post"
.
Qed
.
...
...
@@ -45,7 +45,7 @@ Lemma strange_inc_twice_spec2 `{heapG Σ} l (x : Z) :
l
↦
#
x
-
∗
WP
strange_inc_twice
#
l
{{
v
,
⌜
v
=
#()
⌝
∧
l
↦
#(
2
+
x
)
}}.
Proof
.
iIntros
"Hl"
.
wp_l
et
.
iIntros
"Hl"
.
wp_l
am
.
wp_apply
(
strange_inc_spec
with
"Hl"
)
;
iIntros
"Hl"
;
wp_seq
.
wp_apply
(
strange_inc_spec
with
"Hl"
)
;
iIntros
"Hl"
.
rewrite
(
_
:
2
+
x
=
1
+
(
1
+
x
))
;
last
lia
.
auto
.
...
...
@@ -54,7 +54,7 @@ Qed.
Lemma
strange_inc_twice_spec
`
{
heapG
Σ
}
l
(
x
:
Z
)
:
{{{
l
↦
#
x
}}}
strange_inc_twice
#
l
{{{
RET
#()
;
l
↦
#(
2
+
x
)
}}}.
Proof
.
iIntros
(
Φ
)
"Hl Post"
.
wp_l
et
.
iIntros
(
Φ
)
"Hl Post"
.
wp_l
am
.
wp_apply
(
strange_inc_spec
with
"Hl"
)
;
iIntros
"Hl"
;
wp_seq
.
wp_apply
(
strange_inc_spec
with
"Hl"
)
;
iIntros
"Hl"
.
iApply
"Post"
.
rewrite
(
_
:
2
+
x
=
1
+
(
1
+
x
))
;
last
lia
.
done
.
...
...
talks/demo/part3.v
View file @
5fc7f232
...
...
@@ -11,7 +11,7 @@ Definition coin_flip : val := λ: <>,
Lemma
test2_spec
`
{
heapG
Σ
,
spawnG
Σ
}
:
{{{
True
}}}
coin_flip
#()
{{{
n
,
RET
#
n
;
⌜
n
=
0
∨
n
=
1
⌝
}}}.
Proof
.
iIntros
(
Φ
)
"_ Post"
.
wp_l
et
.
wp_alloc
l
as
"Hl"
.
wp_let
.
iIntros
(
Φ
)
"_ Post"
.
wp_l
am
.
wp_alloc
l
as
"Hl"
.
wp_let
.
iMod
(
inv_alloc
N
_
(
∃
x
:
Z
,
l
↦
#
x
∧
⌜
x
=
0
∨
x
=
1
⌝
)%
I
with
"[Hl]"
)
as
"#?"
.
{
eauto
10
.
}
...
...
talks/demo/part4.v
View file @
5fc7f232
...
...
@@ -14,7 +14,7 @@ Section proof1.
Lemma
Zeven_2
:
Zeven
2
.
Proof
.
done
.
Qed
.
Hint
Resolve
Zeven_2
Zeven_plus_Zeven
.
Hint
Resolve
Zeven_2
Zeven_plus_Zeven
:
core
.
Lemma
par_inc_even_spec
:
{{{
True
}}}
par_inc
#()
{{{
n
,
RET
#
n
;
⌜
Zeven
n
⌝
}}}.
...
...
@@ -56,8 +56,8 @@ Section proof2.
Lemma
frac_auth_alloc
n
:
(|==>
∃
γ
,
own
γ
(
●
F
n
)
∗
own
γ
(
◯
F
{
1
}
n
))%
I
.
Proof
.
by
iMod
(
own_alloc
(
●
F
n
⋅
◯
F
n
))
as
(
γ
)
"[??]"
;
eauto
with
iFrame
.
iMod
(
own_alloc
(
●
F
n
⋅
◯
F
n
))
as
(
γ
)
"[??]"
;
eauto
with
iFrame
.
by
apply
frac_auth_valid
.
Qed
.
Lemma
frac_auth_update
n
n1
n2
q
γ
:
...
...
@@ -123,14 +123,14 @@ Section proof2.
Proof
.
iIntros
(
Φ
)
"[#? Hγ] Post /="
.
iInduction
n
as
[|
n
]
"IH"
forall
(
q
Φ
).
{
do
2
wp_l
et
.
wp_
op
.
wp_if
.
by
iApply
"Post"
.
}
rewrite
Nat2Z
.
inj_succ
.
do
2
wp_let
.
wp_op
.
case_bool_decide
;
first
lia
.
wp_if
.
{
wp_l
am
.
wp_
pures
.
by
iApply
"Post"
.
}
rewrite
Nat2Z
.
inj_succ
.
wp_lam
.
wp_pures
.
case_bool_decide
;
first
(
simplify_eq
/=
;
lia
)
.
wp_if
.
iDestruct
"Hγ"
as
"[Hγ1 Hγ2]"
.
wp_apply
(
wp_par
(
λ
_
,
own
γ
(
◯
F
{
q
/
2
}
2
%
nat
))
(
λ
_
,
own
γ
(
◯
F
{
q
/
2
}
(
n
*
2
)%
nat
))
with
"[Hγ1] [Hγ2]"
).
-
iApply
(
par_inc_FAA_spec
0
2
with
"[$]"
)
;
auto
.
-
wp_op
.
rewrite
(
_
:
Z
.
succ
n
-
1
=
n
)
;
last
lia
.
-
wp_op
.
rewrite
(
_
:
Z
.
succ
n
-
1
=
n
)
%
Z
;
last
lia
.
iApply
(
"IH"
with
"Hγ2"
)
;
auto
.
-
iIntros
(
v1
v2
)
"[Hγ1 Hγ2] !>"
.
iCombine
"Hγ1 Hγ2"
as
"Hγ"
.
by
iApply
"Post"
.
...
...
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