Commit 35826abd authored by Ralf Jung's avatar Ralf Jung
Browse files

update to more automatic solution syntax

parent d00179c4
...@@ -69,12 +69,13 @@ macOS). ...@@ -69,12 +69,13 @@ macOS).
The syntax for the solution files is as follows: The syntax for the solution files is as follows:
``` ```
(* BEGIN SOLUTION *) (* SOLUTION *) Proof.
solution here. solution here.
(* END SOLUTION *) Qed.
``` ```
is replaced by is replaced by
``` ```
Proof.
(* exercise *) (* exercise *)
Admitted. Admitted.
``` ```
......
...@@ -102,7 +102,8 @@ Section proof. ...@@ -102,7 +102,8 @@ Section proof.
- 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. iModIntro. wp_proj.
(* exercise *) (* exercise *) admit.
- (* exercise *) admit.
Admitted. Admitted.
(** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive
......
BEGIN { BEGIN {
in_solution = 0; in_solution = 0; # for the advanced solution syntax
in_auto_solution = 0; # for the simple solution syntax that recognizes `Qed.`
} }
{ # on every line of the input { # on every line of the input
if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) { if (match($0, /^( *)\(\* *SOLUTION *\*\) *Proof.$/, groups)) {
in_solution = 1 print groups[1] "Proof."
} else if (match($0, /^( *)\(\* *END SOLUTION *\*\)$/, groups)) { in_auto_solution = 1
} else if (in_auto_solution == 1 && match($0, /^( *)Qed.$/, groups)) {
print groups[1] " (* exercise *)" print groups[1] " (* exercise *)"
print groups[1] "Admitted." print groups[1] "Admitted."
in_solution = 0 in_auto_solution = 0
} else if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) {
in_solution = 1
} else if (match($0, /^( *)\(\* *END SOLUTION BEGIN TEMPLATE *$/, groups)) { } else if (match($0, /^( *)\(\* *END SOLUTION BEGIN TEMPLATE *$/, groups)) {
in_solution = 0 in_solution = 0
} else if (match($0, /^( *)END TEMPLATE *\*\)$/, groups)) { } else if (match($0, /^( *)END TEMPLATE *\*\)$/, groups)) {
# Nothing to do, just do not print this line. # Nothing to do, just do not print this line.
} else if (in_solution == 0) { } else if (in_solution == 0 && in_auto_solution == 0) {
gsub("From solutions Require", "From exercises Require") gsub("From solutions Require", "From exercises Require")
print print
} }
......
...@@ -136,12 +136,10 @@ Lemma rotate_l_spec x y z v1 v2 v3 : ...@@ -136,12 +136,10 @@ Lemma rotate_l_spec x y z v1 v2 v3 :
{{{ x v1 y v2 z v3 }}} {{{ x v1 y v2 z 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. (* SOLUTION *) 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.
...@@ -116,8 +116,7 @@ Lemma inc_list_spec_induction n l v : ...@@ -116,8 +116,7 @@ Lemma inc_list_spec_induction n l v :
{{{ is_list l v }}} {{{ is_list 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. (* SOLUTION *) 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 %->.
...@@ -134,15 +133,13 @@ Proof. ...@@ -134,15 +133,13 @@ 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 :
{{{ is_list l v }}} {{{ is_list 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. (* SOLUTION *) 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".
...@@ -151,7 +148,6 @@ Proof. ...@@ -151,7 +148,6 @@ 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]. *)
...@@ -159,13 +155,11 @@ Lemma sum_inc_list_spec n l v : ...@@ -159,13 +155,11 @@ Lemma sum_inc_list_spec n l v :
{{{ is_list l v }}} {{{ is_list 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. (* SOLUTION *) 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
...@@ -173,8 +167,7 @@ pure, if you like, you can try to make it more general. *) ...@@ -173,8 +167,7 @@ pure, if you like, you can try to make it more general. *)
Lemma map_list_spec_induction (f : val) (f_coq : Z Z) l v : 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. (* SOLUTION *) 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".
...@@ -185,5 +178,4 @@ Proof. ...@@ -185,5 +178,4 @@ 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.
...@@ -109,21 +109,23 @@ Section proof. ...@@ -109,21 +109,23 @@ Section proof.
{ 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 *) (* END SOLUTION BEGIN TEMPLATE
(* exercise *) admit.
- (* exercise *) admit.
Admitted.
END TEMPLATE *)
(** *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
[wp_apply] to use [try_acquire_spec] when appropriate. *) [wp_apply] to use [try_acquire_spec] when appropriate. *)
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. (* SOLUTION *) 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:
...@@ -134,12 +136,10 @@ Section proof. ...@@ -134,12 +136,10 @@ Section proof.
invariant. *) invariant. *)
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. (* SOLUTION *) 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.
...@@ -73,8 +73,7 @@ Section proof. ...@@ -73,8 +73,7 @@ Section proof.
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. (* SOLUTION *) 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◯]".
...@@ -107,5 +106,4 @@ Section proof. ...@@ -107,5 +106,4 @@ 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.
Supports Markdown
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