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

auto-generate exercises from solutions

parent ae3bead2
...@@ -26,7 +26,10 @@ _*_.tex ...@@ -26,7 +26,10 @@ _*_.tex
*.glob *.glob
*.v.d *.v.d
*.vio *.vio
*.vos
*.vok
Makefile.coq* Makefile.coq*
.Makefile.coq.d
*.crashcoqide *.crashcoqide
.coqdeps.d .coqdeps.d
build-dep build-dep
......
...@@ -40,7 +40,7 @@ build-coq.8.10.1: ...@@ -40,7 +40,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
......
...@@ -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γ◯".
iDestruct (own_valid_2 with "Hγ● Hγ◯") as %->%frac_auth_agreeL. iDestruct (own_valid_2 with "Hγ● Hγ◯") as %->%frac_auth_agreeL.
by iApply "Post". by iApply "Post".
Qed. Qed.
(* END SOLUTION BEGIN TEMPLATE
- (* exercise *)
admit.
- (* exercise *)
admit.
Admitted.
END TEMPLATE *)
End proof3. End proof3.
...@@ -59,6 +59,7 @@ Section proof. ...@@ -59,6 +59,7 @@ Section proof.
and the rules for those as given above. You are allowed to use any number of and the rules for those as given above. You are allowed to use any number of
Boolean ghost variables. *) Boolean ghost variables. *)
Definition parallel_add_mul_inv (r : loc) (γ1 γ2 : gname) : iProp Σ := Definition parallel_add_mul_inv (r : loc) (γ1 γ2 : gname) : iProp Σ :=
(* BEGIN SOLUTION *)
( (b1 b2 : bool) (z : Z), ( (b1 b2 : bool) (z : Z),
own γ1 (E b1) own γ2 (E b2) r #z own γ1 (E b1) own γ2 (E b2) r #z
match b1, b2 with match b1, b2 with
...@@ -66,10 +67,14 @@ Section proof. ...@@ -66,10 +67,14 @@ Section proof.
| true, false => z = 2 | true, false => z = 2
| false, _ => z = 0 | false, _ => z = 0
end)%I. end)%I.
(* END SOLUTION BEGIN TEMPLATE
True%I. (* exercise: replace [True] with something meaningful. *)
END TEMPLATE *)
Lemma parallel_add_mul_spec : Lemma parallel_add_mul_spec :
{{{ True }}} parallel_add_mul {{{ z, RET #z; z = 2%Z z = 4%Z }}}. {{{ True }}} parallel_add_mul {{{ z, RET #z; z = 2%Z z = 4%Z }}}.
Proof. Proof.
(* BEGIN SOLUTION *)
iIntros (Φ) "_ Post". iIntros (Φ) "_ Post".
unfold parallel_add_mul. wp_alloc r as "Hr". wp_let. unfold parallel_add_mul. wp_alloc r as "Hr". wp_let.
iMod (ghost_var_alloc false) as (γ1) "[Hγ1● Hγ1◯]". iMod (ghost_var_alloc false) as (γ1) "[Hγ1● Hγ1◯]".
...@@ -102,4 +107,5 @@ Section proof. ...@@ -102,4 +107,5 @@ Section proof.
iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->. iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->.
auto. auto.
Qed. Qed.
(* END SOLUTION *)
End proof. End proof.