Commit 22a8451e authored by Rodolphe Lepigre's avatar Rodolphe Lepigre

Fix the examples / solution files for latest Iris.

parent 0d7e5abd
......@@ -12,7 +12,7 @@ For the tutorial material you need to have the following dependencies installed:
- Coq 8.6.1 / 8.7.0 / 8.7.1
- Ssreflect 1.6.4
- 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,22 +21,23 @@ 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`.
Then you can do `opam install coq-iris`.
## Installing Iris from source
If you are unable to use opam, you can also build Iris from source. For this,
make sure to `git checkout` the correct versions, and run `make; make install`
for all of:
run `make; make install` for all of:
* ssreflect: <https://github.com/math-comp/math-comp/archive/mathcomp-1.6.4.tar.gz>
(`cd mathcomp/ssreflect` to only compile and install what is needed)
* std++: <https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/repository/coq-stdpp-1.1.0/archive.tar.gz>
* Iris: <https://gitlab.mpi-sws.org/FP/iris-coq/repository/iris-3.1.0/archive.tar.gz>
* Iris: <https://gitlab.mpi-sws.org/FP/iris-coq/-/archive/master/iris-coq-master.tar.gz>
## Compiling the exercises
......
......@@ -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,9 @@ Section proof1.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
(*wp_apply (wp_par (λ _, True%I) (λ _, True%I)).*)
(* FIXME previous tactic fails (replaced by the following two). *)
wp_bind (_ ||| _)%E. iApply (wp_par (λ _, 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 +110,11 @@ Section proof2.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
(*wp_apply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
with "[Hγ1◯] [Hγ2◯]").*)
(* FIXME previous tactic fails (replaced by the following two). *)
wp_bind (_ ||| _)%E.
iApply (wp_par (λ _, 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 +148,11 @@ 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 (wp_par (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]").*)
(* FIXME previous tactic fails (replaced by the following two). *)
wp_bind (_ ||| _)%E.
iApply (wp_par (λ _, 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.
......
......@@ -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,9 @@ 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 (wp_par (λ _, True%I) (λ _, True%I)).*)
(* FIXME previous tactic fails (replaced by the following two). *)
wp_bind (_ ||| _)%E. iApply (wp_par (λ _, 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 +113,11 @@ 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 (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
with "[Hγ1◯] [Hγ2◯]").*)
(* FIXME previous tactic fails (replaced by the following two). *)
wp_bind (_ ||| _)%E.
iApply (wp_par (λ _, 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 +160,11 @@ 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 (wp_par (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]").*)
(* FIXME previous tactic fails (replaced by the following two). *)
wp_bind (_ ||| _)%E.
iApply (wp_par (λ _, 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,11 @@ 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 (wp_par (λ _, own γ1 (◯ Excl' true)) (λ _, own γ2 (◯ Excl' true))
with "[Hγ1◯] [Hγ2◯]").*)
(* FIXME previous tactic fails (replaced by the following two). *)
wp_bind (_ ||| _)%E.
iApply (wp_par (λ _, 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