Commit 53a92a4e authored by Ralf Jung's avatar Ralf Jung

Merge branch 'latest_iris' into 'master'

Fix the examples / solution files for latest Iris.

Closes #2

See merge request !1
parents c4ae02c0 7e44373e
Pipeline #14570 failed with stage
in 8 minutes and 45 seconds
......@@ -8,7 +8,6 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
......
......@@ -12,7 +12,7 @@ For the tutorial material you need to have the following dependencies installed:
- Coq 8.6.1 / 8.7.2 / 8.8.2
- Ssreflect 1.7.0
- Coq-std++ 1.1
- Iris 3.1
- Iris (latest version)
*Note:* the tutorial material will not work with earlier versions of Iris, it
is important to install the exact versions as given above.
......@@ -21,11 +21,13 @@ is important to install the exact versions as given above.
The easiest, and recommend, way of installing Iris and its dependencies is via
the OCaml package manager opam (1.2.2 or newer). You first have to add the Coq
opam repository if you have not already done so earlier:
opam repository and the Iris development repository (if you have not already
done so earlier):
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
Then you can do `opam install coq-iris.3.1.0`.
Then you can do `opam install coq-iris`.
## Installing Iris from source
......
......@@ -55,7 +55,7 @@ Lemma swap_spec x y v1 v2 :
Proof.
iIntros (Φ) "[Hx Hy] Post".
unfold swap.
wp_lam. wp_lam.
wp_lam. wp_let.
wp_load. wp_let.
wp_load. wp_store.
wp_store.
......@@ -70,13 +70,13 @@ Lemma swap_spec_2 x y v1 v2 :
{{{ x v1 y v2 }}} swap #x #y {{{ RET #(); x v2 y v1 }}}.
Proof.
iIntros (Φ) "[??] Post".
wp_lam. wp_lam. wp_load. wp_let. wp_load. wp_store. wp_store.
wp_lam. wp_let. wp_load. wp_let. wp_load. wp_store. wp_store.
iApply "Post". iFrame.
Qed.
(* We can further automate the lemma by defining a simple Ltac tactic for
symbolic executing. *)
Ltac wp_exec := repeat (wp_pure _ || wp_load || wp_store).
Ltac wp_exec := repeat (wp_lam || wp_pure _ || wp_load || wp_store).
(* This tactic repeatedly tries to symbolically execute pure redexes, loads and
stores. It makes use of the tactic [wp_pure t], which tries to find the redex
......@@ -100,7 +100,7 @@ Proof.
(* As in Coq, the IPM introduction pattern (p1 & p2 & .. & pn) ] is syntactic
sugar for [ [p1 [p2 [... pn]]] ]. *)
iIntros (Φ) "(Hx & Hy & Hz) Post".
unfold rotate_r. do 3 wp_lam.
unfold rotate_r. wp_lam. do 2 wp_let.
wp_bind (swap _ _).
iApply (swap_spec with "[Hy Hz]").
{ iFrame. }
......@@ -117,7 +117,7 @@ Lemma rotate_r_spec_again x y z v1 v2 v3 :
rotate_r #x #y #z
{{{ RET #(); x v3 y v1 z v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
iIntros (Φ) "(Hx & Hy & Hz) Post". wp_lam.
(* We can shorten the above a bit: Instead of using the [iApply] tactic, we
can use [wp_apply] which automatically uses [wp_bind] first. Also, it strips
the later [▷] by calling [iNext] afterwards. *)
......
......@@ -39,7 +39,7 @@ Section proof1.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
wp_apply (par_spec (λ _, True%I) (λ _, True%I)).
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. wp_op. wp_store.
wp_apply (release_spec with "[Hr $Hl]"); [|done].
......@@ -108,7 +108,7 @@ Section proof2.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
wp_apply (par_spec (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
wp_seq. wp_load. wp_op. wp_store.
......@@ -142,7 +142,7 @@ Section proof3.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
wp_apply (par_spec (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store.
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [] # This repo does not install
remove: []
depends: [
"coq-iris" { (= "3.1.0") }
"coq-iris" { (= "dev.2019-01-22.0.b85a3cfc") | (= "dev") }
]
......@@ -55,7 +55,7 @@ Lemma swap_spec x y v1 v2 :
Proof.
iIntros (Φ) "[Hx Hy] Post".
unfold swap.
wp_lam. wp_lam.
wp_lam. wp_let.
wp_load. wp_let.
wp_load. wp_store.
wp_store.
......@@ -70,13 +70,13 @@ Lemma swap_spec_2 x y v1 v2 :
{{{ x v1 y v2 }}} swap #x #y {{{ RET #(); x v2 y v1 }}}.
Proof.
iIntros (Φ) "[??] Post".
wp_lam. wp_lam. wp_load. wp_let. wp_load. wp_store. wp_store.
wp_lam. wp_let. wp_load. wp_let. wp_load. wp_store. wp_store.
iApply "Post". iFrame.
Qed.
(* We can further automate the lemma by defining a simple Ltac tactic for
symbolic executing. *)
Ltac wp_exec := repeat (wp_pure _ || wp_load || wp_store).
Ltac wp_exec := repeat (wp_lam || wp_pure _ || wp_load || wp_store).
(* This tactic repeatedly tries to symbolically execute pure redexes, loads and
stores. It makes use of the tactic [wp_pure t], which tries to find the redex
......@@ -100,7 +100,7 @@ Proof.
(* As in Coq, the IPM introduction pattern (p1 & p2 & .. & pn) ] is syntactic
sugar for [ [p1 [p2 [... pn]]] ]. *)
iIntros (Φ) "(Hx & Hy & Hz) Post".
unfold rotate_r. do 3 wp_lam.
unfold rotate_r. wp_lam. do 2 wp_let.
wp_bind (swap _ _).
iApply (swap_spec with "[Hy Hz]").
{ iFrame. }
......@@ -117,7 +117,7 @@ Lemma rotate_r_spec_again x y z v1 v2 v3 :
rotate_r #x #y #z
{{{ RET #(); x v3 y v1 z v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
iIntros (Φ) "(Hx & Hy & Hz) Post". wp_lam. do 2 wp_let.
(* We can shorten the above a bit: Instead of using the [iApply] tactic, we
can use [wp_apply] which automatically uses [wp_bind] first. Also, it strips
the later [▷] by calling [iNext] afterwards. *)
......@@ -137,7 +137,7 @@ Lemma rotate_l_spec x y z v1 v2 v3 :
rotate_l #x #y #z
{{{ RET #(); x v2 y v3 z v1 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". unfold rotate_l. do 3 wp_lam.
iIntros (Φ) "(Hx & Hy & Hz) Post". unfold rotate_l. wp_lam. do 2 wp_let.
wp_apply (swap_spec with "[$Hx $Hy]"); iIntros "[Hx Hy]"; wp_seq.
wp_apply (swap_spec with "[$Hy $Hz]"); iIntros "[Hy Hz]".
iApply ("Post" with "[$]").
......
......@@ -156,7 +156,7 @@ Lemma sum_inc_list_spec n l v :
sum_inc_list #n v
{{{ RET #(sum_list_coq (map (Z.add n) l)); is_list (map (Z.add n) l) v }}}.
Proof.
iIntros (Φ) "Hl Post". do 2 wp_let.
iIntros (Φ) "Hl Post". wp_lam. wp_let.
wp_apply (inc_list_spec_induction with "Hl"); iIntros "Hl /="; wp_seq.
wp_apply (sum_list_spec_induction with "Hl"); auto.
Qed.
......
......@@ -38,7 +38,7 @@ Section proof1.
wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]").
{ (* exercise *) iExists 0. iFrame. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
wp_apply (par_spec (λ _, True%I) (λ _, True%I)).
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. wp_op. wp_store.
wp_apply (release_spec with "[Hr $Hl]"); [|done].
......@@ -111,7 +111,7 @@ Section proof2.
wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
{ (* exercise *) iExists 0, 0. iFrame. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
wp_apply (par_spec (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
wp_seq. wp_load. wp_op. wp_store.
......@@ -154,7 +154,7 @@ Section proof3.
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) iExists 0%nat. iFrame. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
wp_apply (par_spec (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store.
......
......@@ -77,7 +77,7 @@ Section proof.
wp_apply (newlock_spec (parallel_add_mul_inv r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
{ iExists false, false, 0. iFrame. done. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 ( Excl' true)) (λ _, own γ2 ( Excl' true))
wp_apply (par_spec (λ _, own γ1 ( Excl' true)) (λ _, own γ2 ( Excl' true))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl").
iDestruct 1 as (b1 b2 z) "(Hγ1● & Hγ2● & Hr & %)".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment