Commit 469c810a authored by Ralf Jung's avatar Ralf Jung

add lemma to prove atomic WP without seeing a Q

parent 35308b0f
...@@ -23,24 +23,24 @@ Section increment. ...@@ -23,24 +23,24 @@ Section increment.
Lemma incr_spec (l: loc) : Lemma incr_spec (l: loc) :
<<< (v : Z), l #v >>> incr #l @ <<< l #(v + 1), RET #v >>>. <<< (v : Z), l #v >>> incr #l @ <<< l #(v + 1), RET #v >>>.
Proof. Proof.
iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let. iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_let.
wp_apply (load_spec with "[HQ]"); first by iAccu. wp_apply load_spec; first by iAccu.
(* Prove the atomic update for load *) (* Prove the atomic update for load *)
iAuIntro. iApply (aacc_aupd_abort with "AU"); first done. iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> AU !> HQ". iIntros "$ !> AU !> _".
(* Now go on *) (* Now go on *)
wp_let. wp_op. wp_bind (CAS _ _ _)%I. wp_let. wp_op. wp_bind (CAS _ _ _)%I.
wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. wp_apply cas_spec; [done|iAccu|].
(* Prove the atomic update for CAS *) (* Prove the atomic update for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done. iAuIntro. iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "H↦ !>". iIntros "H↦ !>".
destruct (decide (#x' = #x)) as [[= ->]|Hx]. destruct (decide (#x' = #x)) as [[= ->]|Hx].
- iRight. iFrame. iIntros "HΦ !> HQ". - iRight. iFrame. iIntros "HΦ !> _".
wp_if. by iApply "HΦ". wp_if. by iApply "HΦ".
- iLeft. iFrame. iIntros "AU !> HQ". - iLeft. iFrame. iIntros "AU !> _".
wp_if. iApply ("IH" with "HQ"). done. wp_if. iApply "IH". done.
Qed. Qed.
Definition weak_incr: val := Definition weak_incr: val :=
...@@ -57,10 +57,10 @@ Section increment. ...@@ -57,10 +57,10 @@ Section increment.
weak_incr #l @ weak_incr #l @
<<< v = v' l #(v + 1), RET #v >>>. <<< v = v' l #(v + 1), RET #v >>>.
Proof. Proof.
iIntros "Hl" (Q Φ) "HQ AU". wp_let. iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_let.
wp_apply (atomic_wp_seq $! (load_spec _) with "Hl"). wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
iIntros "Hl". wp_let. wp_op. iIntros "Hl". wp_let. wp_op.
wp_apply (store_spec with "[HQ]"); first by iAccu. wp_apply store_spec; first by iAccu.
(* Prove the atomic update for store *) (* Prove the atomic update for store *)
iAuIntro. iApply (aacc_aupd_commit with "AU"); first done. iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
iIntros (x) "H↦". iIntros (x) "H↦".
...@@ -68,7 +68,7 @@ Section increment. ...@@ -68,7 +68,7 @@ Section increment.
iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl". iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
{ iIntros "[$ $]"; eauto. } { iIntros "[$ $]"; eauto. }
iIntros "$ !>". iSplit; first done. iIntros "$ !>". iSplit; first done.
iIntros "HΦ !> HQ". wp_seq. iApply "HΦ". done. iIntros "HΦ !> _". wp_seq. done.
Qed. Qed.
End increment. End increment.
......
...@@ -122,4 +122,16 @@ Section lemmas. ...@@ -122,4 +122,16 @@ Section lemmas.
iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ". iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
rewrite ->!tele_app_bind. iApply "HΦ". done. rewrite ->!tele_app_bind. iApply "HΦ". done.
Qed. Qed.
(* Way to prove an atomic triple without seeing the Q *)
Lemma wp_atomic_intro e Eo α β f :
( (Φ : val Λ iProp),
atomic_update Eo α β (λ.. x y, Φ (f x y)) -
WP e {{ Φ }}) -
atomic_wp e Eo α β f.
Proof.
iIntros "Hwp" (Q Φ) "HQ AU". iApply (wp_wand with "[-HQ]").
{ iApply ("Hwp" $! (λ v, Q - Φ v)%I). done. }
iIntros (v) "HΦ". iApply "HΦ". done.
Qed.
End lemmas. End lemmas.
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