Commit fcc95c24 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/gen-exercises' into 'master'

Auto-generate exercise files

Closes #4

See merge request !4
parents ae3bead2 a6c95521
Pipeline #33203 failed with stage
in 1 minute and 59 seconds
...@@ -26,7 +26,11 @@ _*_.tex ...@@ -26,7 +26,11 @@ _*_.tex
*.glob *.glob
*.v.d *.v.d
*.vio *.vio
Makefile.coq* *.vos
*.vok
Makefile.coq
Makefile.coq.conf
.Makefile.coq.d
*.crashcoqide *.crashcoqide
.coqdeps.d .coqdeps.d
build-dep build-dep
......
...@@ -5,6 +5,7 @@ stages: ...@@ -5,6 +5,7 @@ stages:
variables: variables:
CPU_CORES: "10" CPU_CORES: "10"
MAKE_TARGET: "ci"
.template: &template .template: &template
stage: build stage: build
...@@ -40,7 +41,7 @@ build-coq.8.10.1: ...@@ -40,7 +41,7 @@ build-coq.8.10.1:
build-iris.dev: build-iris.dev:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.11.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV" OPAM_PINS: "coq version 8.12.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
except: except:
only: only:
- triggers - triggers
......
# Generate an exercise for each solution.
SOLUTIONS := $(wildcard solutions/*.v)
EXERCISES := $(addprefix exercises/,$(notdir $(SOLUTIONS)))
exercises: $(EXERCISES)
.PHONY: exercises
$(EXERCISES): exercises/%.v: solutions/%.v gen-exercises.awk
$(HIDE)echo "Generating exercise file $@ from $<"
$(HIDE)gawk -f gen-exercises.awk < $< > $@
# CI make target
ci: all
+@make -B exercises # force make (in case exercise files have been edited directly)
if [ -n "$$(git status --porcelain)" ]; then echo 'ERROR: Exercise files are not up-to-date with solutions.'; exit 1; fi
...@@ -58,3 +58,35 @@ If you would like to know more about Iris, we recommend to take a look at: ...@@ -58,3 +58,35 @@ If you would like to know more about Iris, we recommend to take a look at:
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars
Birkedal, Derek Dreyer. Birkedal, Derek Dreyer.
A detailed description of the Iris logic and its model A detailed description of the Iris logic and its model
## Generating the exercises
If you want to contribute to the tutorial, note that the files in `exercises/`
are generated from the corresponding files in `solutions/`. Run `make exercises`
to re-generate those files. This requires `gawk` to be installed (which should
usually be available on Linux but might have to be installed separately on
macOS).
The syntax for the solution files is as follows:
```
(* BEGIN SOLUTION *)
solution here.
(* END SOLUTION *)
```
is replaced by
```
(* exercise *)
Admitted.
```
and the more powerful
```
(* BEGIN SOLUTION *)
solution here.
(* END SOLUTION BEGIN TEMPLATE
exercise template here.
END TEMPLATE *)
```
is replaced by
```
exercise template here.
```
...@@ -117,7 +117,7 @@ Lemma rotate_r_spec_again x y z v1 v2 v3 : ...@@ -117,7 +117,7 @@ Lemma rotate_r_spec_again x y z v1 v2 v3 :
rotate_r #x #y #z rotate_r #x #y #z
{{{ RET #(); x v3 y v1 z v2 }}}. {{{ RET #(); x v3 y v1 z v2 }}}.
Proof. Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". 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 (* 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 can use [wp_apply] which automatically uses [wp_bind] first. Also, it strips
the later [▷] by calling [iNext] afterwards. *) the later [▷] by calling [iNext] afterwards. *)
......
...@@ -101,7 +101,8 @@ Section proof. ...@@ -101,7 +101,8 @@ Section proof.
destruct b. destruct b.
- wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_". - wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_".
{ iNext. iExists true. iFrame. } { iNext. iExists true. iFrame. }
iModIntro. wp_proj. (* exercise *) iModIntro. wp_proj.
(* exercise *)
Admitted. Admitted.
(** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive
......
...@@ -36,8 +36,7 @@ Section proof1. ...@@ -36,8 +36,7 @@ Section proof1.
iIntros (Φ) "_ Post". iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let. unfold parallel_add. wp_alloc r as "Hr". wp_let.
wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]"). wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]").
{ (* exercise *) { (* exercise *) admit. }
admit. }
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, True%I) (λ _, True%I)). wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]". - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
...@@ -105,8 +104,7 @@ Section proof2. ...@@ -105,8 +104,7 @@ Section proof2.
iMod (ghost_var_alloc 0) as (γ1) "[Hγ1● Hγ1◯]". iMod (ghost_var_alloc 0) as (γ1) "[Hγ1● Hγ1◯]".
iMod (ghost_var_alloc 0) as (γ2) "[Hγ2● Hγ2◯]". iMod (ghost_var_alloc 0) as (γ2) "[Hγ2● Hγ2◯]".
wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]"). wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
{ (* exercise *) { (* exercise *) admit. }
admit. }
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 (E 2%Z)) (λ _, own γ2 (E 2%Z)) wp_apply (wp_par (λ _, own γ1 (E 2%Z)) (λ _, own γ2 (E 2%Z))
with "[Hγ1◯] [Hγ2◯]"). with "[Hγ1◯] [Hγ2◯]").
...@@ -140,8 +138,7 @@ Section proof3. ...@@ -140,8 +138,7 @@ Section proof3.
iMod (own_alloc (F 0 F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]". iMod (own_alloc (F 0 F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. } { by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]"). wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) { (* exercise *) admit. }
admit. }
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2)) wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2))
with "[Hγ1◯] [Hγ2◯]"). with "[Hγ1◯] [Hγ2◯]").
......
...@@ -62,7 +62,7 @@ Section proof. ...@@ -62,7 +62,7 @@ Section proof.
True%I. (* exercise: replace [True] with something meaningful. *) True%I. (* exercise: replace [True] with something meaningful. *)
Lemma parallel_add_mul_spec : Lemma parallel_add_mul_spec :
{{{ True }}} parallel_add_mul {{{ z, RET #z; z = 2 z = 4 }}}. {{{ True }}} parallel_add_mul {{{ z, RET #z; z = 2%Z z = 4%Z }}}.
Proof. Proof.
(* exercise *) (* exercise *)
Admitted. Admitted.
......
BEGIN {
in_solution = 0;
}
{ # on every line of the input
if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) {
in_solution = 1
} else if (match($0, /^( *)\(\* *END SOLUTION *\*\)$/, groups)) {
print groups[1] " (* exercise *)"
print groups[1] "Admitted."
in_solution = 0
} else if (match($0, /^( *)\(\* *END SOLUTION BEGIN TEMPLATE *$/, groups)) {
in_solution = 0
} else if (match($0, /^( *)END TEMPLATE *\*\)$/, groups)) {
# Nothing to do, just do not print this line.
} else if (in_solution == 0) {
gsub("From solutions Require", "From exercises Require")
print
}
}
...@@ -137,9 +137,11 @@ Lemma rotate_l_spec x y z v1 v2 v3 : ...@@ -137,9 +137,11 @@ Lemma rotate_l_spec x y z v1 v2 v3 :
rotate_l #x #y #z rotate_l #x #y #z
{{{ RET #(); x v2 y v3 z v1 }}}. {{{ RET #(); x v2 y v3 z v1 }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros (Φ) "(Hx & Hy & Hz) Post". unfold rotate_l. wp_lam. do 2 wp_let. 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 "[$Hx $Hy]"); iIntros "[Hx Hy]"; wp_seq.
wp_apply (swap_spec with "[$Hy $Hz]"); iIntros "[Hy Hz]". wp_apply (swap_spec with "[$Hy $Hz]"); iIntros "[Hy Hz]".
iApply ("Post" with "[$]"). iApply ("Post" with "[$]").
Qed. Qed.
(* END SOLUTION *)
End proof. End proof.
...@@ -117,6 +117,7 @@ Lemma inc_list_spec_induction n l v : ...@@ -117,6 +117,7 @@ Lemma inc_list_spec_induction n l v :
inc_list #n v inc_list #n v
{{{ RET #(); is_list (map (Z.add n) l) v }}}. {{{ RET #(); is_list (map (Z.add n) l) v }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros (Φ) "Hl Post". iIntros (Φ) "Hl Post".
iInduction l as [|x l] "IH" forall (v Φ); simpl. iInduction l as [|x l] "IH" forall (v Φ); simpl.
- iDestruct "Hl" as %->. - iDestruct "Hl" as %->.
...@@ -133,6 +134,7 @@ Proof. ...@@ -133,6 +134,7 @@ Proof.
iExists p. iSplitR; [done|]. iExists p. iSplitR; [done|].
iExists v. iSplitR "Hl"; [iApply "Hp"|iApply "Hl"]. iExists v. iSplitR "Hl"; [iApply "Hp"|iApply "Hl"].
Qed. Qed.
(* END SOLUTION *)
(** *Exercise*: Now do the proof again using Löb induction. *) (** *Exercise*: Now do the proof again using Löb induction. *)
Lemma inc_list_spec_löb n l v : Lemma inc_list_spec_löb n l v :
...@@ -140,6 +142,7 @@ Lemma inc_list_spec_löb n l v : ...@@ -140,6 +142,7 @@ Lemma inc_list_spec_löb n l v :
inc_list #n v inc_list #n v
{{{ RET #(); is_list (map (Z.add n) l) v }}}. {{{ RET #(); is_list (map (Z.add n) l) v }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros (Φ) "Hl Post". iIntros (Φ) "Hl Post".
iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let. iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let.
- iDestruct "Hl" as %->. wp_match. by iApply "Post". - iDestruct "Hl" as %->. wp_match. by iApply "Post".
...@@ -148,6 +151,7 @@ Proof. ...@@ -148,6 +151,7 @@ Proof.
wp_apply ("IH" with "Hl"). iIntros "Hl". wp_apply ("IH" with "Hl"). iIntros "Hl".
iApply "Post". eauto with iFrame. iApply "Post". eauto with iFrame.
Qed. Qed.
(* END SOLUTION *)
(** *Exercise*: Do the proof of [sum_inc_list] by making use of the lemmas of (** *Exercise*: Do the proof of [sum_inc_list] by making use of the lemmas of
[sum_list] and [inc_list] we just proved. Make use of [wp_apply]. *) [sum_list] and [inc_list] we just proved. Make use of [wp_apply]. *)
...@@ -156,10 +160,12 @@ Lemma sum_inc_list_spec n l v : ...@@ -156,10 +160,12 @@ Lemma sum_inc_list_spec n l v :
sum_inc_list #n v sum_inc_list #n v
{{{ RET #(sum_list_coq (map (Z.add n) l)); is_list (map (Z.add n) l) v }}}. {{{ RET #(sum_list_coq (map (Z.add n) l)); is_list (map (Z.add n) l) v }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros (Φ) "Hl Post". wp_lam. wp_let. iIntros (Φ) "Hl Post". wp_lam. wp_let.
wp_apply (inc_list_spec_induction with "Hl"); iIntros "Hl /="; wp_seq. wp_apply (inc_list_spec_induction with "Hl"); iIntros "Hl /="; wp_seq.
wp_apply (sum_list_spec_induction with "Hl"); auto. wp_apply (sum_list_spec_induction with "Hl"); auto.
Qed. Qed.
(* END SOLUTION *)
(** *Optional exercise*: Prove the following spec of [map_list] which makes use (** *Optional exercise*: Prove the following spec of [map_list] which makes use
of a nested Texan triple, This spec is rather weak, as it requires [f] to be of a nested Texan triple, This spec is rather weak, as it requires [f] to be
...@@ -168,6 +174,7 @@ Lemma map_list_spec_induction (f : val) (f_coq : Z → Z) l v : ...@@ -168,6 +174,7 @@ Lemma map_list_spec_induction (f : val) (f_coq : Z → Z) l v :
( n, {{{ True }}} f #n {{{ RET #(f_coq n); True }}}) - ( n, {{{ True }}} f #n {{{ RET #(f_coq n); True }}}) -
{{{ is_list l v }}} map_list f v {{{ RET #(); is_list (map f_coq l) v }}}. {{{ is_list l v }}} map_list f v {{{ RET #(); is_list (map f_coq l) v }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros "#Hf" (Φ) "!# Hl Post". iIntros "#Hf" (Φ) "!# Hl Post".
iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let. iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let.
- iDestruct "Hl" as %->. wp_match. by iApply "Post". - iDestruct "Hl" as %->. wp_match. by iApply "Post".
...@@ -178,4 +185,5 @@ Proof. ...@@ -178,4 +185,5 @@ Proof.
wp_apply ("IH" with "Hl"). iIntros "Hl". wp_apply ("IH" with "Hl"). iIntros "Hl".
iApply "Post". eauto with iFrame. iApply "Post". eauto with iFrame.
Qed. Qed.
(* END SOLUTION *)
End proof. End proof.
...@@ -101,12 +101,15 @@ Section proof. ...@@ -101,12 +101,15 @@ Section proof.
destruct b. destruct b.
- wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_". - wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_".
{ iNext. iExists true. iFrame. } { iNext. iExists true. iFrame. }
iModIntro. wp_proj. iApply ("HΦ" $! false). done. iModIntro. wp_proj.
(* BEGIN SOLUTION *)
iApply ("HΦ" $! false). done.
- (* Exercise *) wp_cmpxchg_suc. - (* Exercise *) wp_cmpxchg_suc.
iMod ("Hclose" with "[Hl]") as "_". iMod ("Hclose" with "[Hl]") as "_".
{ iNext. iExists true. iFrame. } { iNext. iExists true. iFrame. }
iModIntro. wp_proj. by iApply ("HΦ" $! true with "HR"). iModIntro. wp_proj. by iApply ("HΦ" $! true with "HR").
Qed. Qed.
(* END SOLUTION *)
(** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive
function, you should use the tactic [iLöb] for Löb induction. Use the tactic function, you should use the tactic [iLöb] for Löb induction. Use the tactic
...@@ -114,11 +117,13 @@ Section proof. ...@@ -114,11 +117,13 @@ Section proof.
Lemma acquire_spec lk R : Lemma acquire_spec lk R :
{{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}}. {{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec. iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hl"). iIntros ([]). wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
- iIntros "HR". wp_if. by iApply "HΦ". - iIntros "HR". wp_if. by iApply "HΦ".
- iIntros "_". wp_if. iApply ("IH" with "HΦ"). - iIntros "_". wp_if. iApply ("IH" with "HΦ").
Qed. Qed.
(* END SOLUTION *)
(** *Exercise*: prove the spec of [release]. At a certain point in this proof, (** *Exercise*: prove the spec of [release]. At a certain point in this proof,
you need to open the invariant. For this you can use: you need to open the invariant. For this you can use:
...@@ -130,9 +135,11 @@ Section proof. ...@@ -130,9 +135,11 @@ Section proof.
Lemma release_spec lk R : Lemma release_spec lk R :
{{{ is_lock lk R R }}} release lk {{{ RET #(); True }}}. {{{ is_lock lk R R }}} release lk {{{ RET #(); True }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros (Φ) "(Hlock & HR) HΦ". iIntros (Φ) "(Hlock & HR) HΦ".
iDestruct "Hlock" as (l ->) "#Hinv /=". iDestruct "Hlock" as (l ->) "#Hinv /=".
wp_lam. iInv lockN as (b) "[Hl _]" "Hclose". wp_lam. iInv lockN as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. iFrame. wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. iFrame.
Qed. Qed.
(* END SOLUTION *)
End proof. End proof.
...@@ -36,23 +36,33 @@ Section proof1. ...@@ -36,23 +36,33 @@ Section proof1.
iIntros (Φ) "_ Post". iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let. unfold parallel_add. wp_alloc r as "Hr". wp_let.
wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]"). wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]").
{ (* exercise *) iExists 0. iFrame. } (* BEGIN SOLUTION *)
{ iExists 0. iFrame. }
(* END SOLUTION BEGIN TEMPLATE
{ (* exercise *) admit. }
END TEMPLATE *)
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, True%I) (λ _, True%I)). wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]". - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. wp_op. wp_store. wp_seq. wp_load. wp_op. wp_store.
wp_apply (release_spec with "[Hr $Hl]"); [|done]. wp_apply (release_spec with "[Hr $Hl]"); [|done].
iExists _. iFrame "Hr". iPureIntro. by apply Zeven_plus_Zeven. iExists _. iFrame "Hr". iPureIntro. by apply Zeven_plus_Zeven.
- (* exercise *) (* BEGIN SOLUTION *)
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]". - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. wp_op. wp_store. wp_seq. wp_load. wp_op. wp_store.
wp_apply (release_spec with "[Hr $Hl]"); [|done]. wp_apply (release_spec with "[Hr $Hl]"); [|done].
iExists _. iFrame "Hr". iPureIntro. by apply Zeven_plus_Zeven. iExists _. iFrame "Hr". iPureIntro. by apply Zeven_plus_Zeven.
- (* exercise *) - iIntros (v1 v2) "_ !>". wp_seq.
iIntros (v1 v2) "_ !>". wp_seq.
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]". wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. by iApply "Post". wp_seq. wp_load. by iApply "Post".
Qed. Qed.
(* END SOLUTION BEGIN TEMPLATE
- (* exercise *)
admit.
- (* exercise *)
admit.
Admitted.
END TEMPLATE *)
End proof1. End proof1.
(** 2nd proof : we prove that the program returns 4 exactly. (** 2nd proof : we prove that the program returns 4 exactly.
...@@ -62,7 +72,7 @@ Whereas we previously abstracted over an arbitrary "ghost state" [Σ] in the ...@@ -62,7 +72,7 @@ Whereas we previously abstracted over an arbitrary "ghost state" [Σ] in the
proofs, we now need to make sure that we can use integer ghost variables. For proofs, we now need to make sure that we can use integer ghost variables. For
this, we add the type class constraint: this, we add the type class constraint:
inG Σ (authR (optionUR (exclR ZO))) inG Σ (excl_authR ZO)
*) *)
...@@ -109,7 +119,11 @@ Section proof2. ...@@ -109,7 +119,11 @@ Section proof2.
iMod (ghost_var_alloc 0) as (γ1) "[Hγ1● Hγ1◯]". iMod (ghost_var_alloc 0) as (γ1) "[Hγ1● Hγ1◯]".
iMod (ghost_var_alloc 0) as (γ2) "[Hγ2● Hγ2◯]". iMod (ghost_var_alloc 0) as (γ2) "[Hγ2● Hγ2◯]".
wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]"). wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
{ (* exercise *) iExists 0, 0. iFrame. } (* BEGIN SOLUTION *)
{ iExists 0, 0. iFrame. }
(* END SOLUTION BEGIN TEMPLATE
{ (* exercise *) admit. }
END TEMPLATE *)
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 (E 2%Z)) (λ _, own γ2 (E 2%Z)) wp_apply (wp_par (λ _, own γ1 (E 2%Z)) (λ _, own γ2 (E 2%Z))
with "[Hγ1◯] [Hγ2◯]"). with "[Hγ1◯] [Hγ2◯]").
...@@ -119,21 +133,27 @@ Section proof2. ...@@ -119,21 +133,27 @@ Section proof2.
iMod (ghost_var_update γ1 2 with "Hγ1● Hγ1◯") as "[Hγ1● Hγ1◯]". iMod (ghost_var_update γ1 2 with "Hγ1● Hγ1◯") as "[Hγ1● Hγ1◯]".
wp_apply (release_spec with "[- $Hl Hγ1◯]"); [|by auto]. wp_apply (release_spec with "[- $Hl Hγ1◯]"); [|by auto].
iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2)%Z; [done|ring]. iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2)%Z; [done|ring].
- (* exercise *) (* BEGIN SOLUTION *)
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & 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. wp_seq. wp_load. wp_op. wp_store.
iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->. iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->.
iMod (ghost_var_update γ2 2 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]". iMod (ghost_var_update γ2 2 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]".
wp_apply (release_spec with "[- $Hl Hγ2◯]"); [|by auto]. wp_apply (release_spec with "[- $Hl Hγ2◯]"); [|by auto].
iExists _, _. iFrame "Hγ1● Hγ2●". by rewrite -Z.add_assoc. iExists _, _. iFrame "Hγ1● Hγ2●". by rewrite -Z.add_assoc.
- (* exercise *) - iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq.
iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq.
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & 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_seq. wp_load.
iDestruct (ghost_var_agree with "Hγ1● Hγ1◯") as %->. iDestruct (ghost_var_agree with "Hγ1● Hγ1◯") as %->.
iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->. iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->.
by iApply "Post". by iApply "Post".
Qed. Qed.
(* END SOLUTION BEGIN TEMPLATE
- (* exercise *)
admit.
- (* exercise *)
admit.
Admitted.
END TEMPLATE *)
End proof2. End proof2.
(** 3rd proof : we prove that the program returns 4 exactly, but using a (** 3rd proof : we prove that the program returns 4 exactly, but using a
...@@ -153,7 +173,11 @@ Section proof3. ...@@ -153,7 +173,11 @@ Section proof3.
iMod (own_alloc (F 0 F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]". iMod (own_alloc (F 0 F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. } { by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]"). wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) iExists 0. iFrame. } (* BEGIN SOLUTION *)
{ iExists 0. iFrame. }
(* END SOLUTION BEGIN TEMPLATE
{ (* exercise *) admit. }
END TEMPLATE *)
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2)) wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2))
with "[Hγ1◯] [Hγ2◯]"). with "[Hγ1◯] [Hγ2◯]").
...@@ -164,19 +188,25 @@ Section proof3. ...@@ -164,19 +188,25 @@ Section proof3.
by apply frac_auth_update, (op_local_update_discrete n 0 2). } by apply frac_auth_update, (op_local_update_discrete n 0 2). }
wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto]. wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto].
iExists _. iFrame. by rewrite Nat2Z.inj_add. iExists _. iFrame. by rewrite Nat2Z.inj_add.
- (* exercise *) (* BEGIN SOLUTION *)
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]". - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store. wp_seq. wp_load. wp_op. wp_store.
iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2) with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]". iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2) with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]".
{ rewrite (comm plus). { rewrite (comm plus).
by apply frac_auth_update, (op_local_update_discrete n 0 2). } by apply frac_auth_update, (op_local_update_discrete n 0 2). }
wp_apply (release_spec with "[- $Hl Hγ2◯]"); [|by auto]. wp_apply (release_spec with "[- $Hl Hγ2◯]"); [|by auto].
iExists _. iFrame. by rewrite Nat2Z.inj_add. iExists _. iFrame. by rewrite Nat2Z.inj_add.
- (* exercise *) - iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq.
iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq.
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "(Hr & Hγ●)". wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "(Hr & Hγ●)".
wp_seq. wp_load. iCombine "Hγ1◯ Hγ2◯" as "Hγ◯". wp_seq. wp_load. iCombine "Hγ1◯ Hγ2◯" as "Hγ◯".