Commit c66ccdc5 authored by Ralf Jung's avatar Ralf Jung

tweak direct proof

parent e65f78d2
...@@ -58,16 +58,16 @@ Section increment. ...@@ -58,16 +58,16 @@ Section increment.
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam. iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_apply load_spec; first by iAccu. wp_apply load_spec; first by iAccu.
(* Prove the atomic update for load *) (* Prove the atomic update for load *)
iAuIntro. rewrite /atomic_acc. iMod "AU" as (v) "[Hl [Hclose _]]". iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
iModIntro. iExists _, _. iFrame "Hl". iSplit. iModIntro. iExists _, _. iFrame "Hl". iSplit.
{ (* proving abort case *) done. } { (* abort case *) done. }
iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iIntros "!> _". iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iIntros "!> _".
(* Now go on *) (* Now go on *)
wp_apply cas_spec; [done|iAccu|]. wp_apply cas_spec; [done|iAccu|].
(* Prove the atomic update for CAS *) (* Prove the atomic update for CAS *)
iAuIntro. rewrite /atomic_acc. iMod "AU" as (w) "[Hl Hclose]". iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
iModIntro. iExists _. iFrame "Hl". iSplit. iModIntro. iExists _. iFrame "Hl". iSplit.
{ iDestruct "Hclose" as "[? _]". done. } { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx]. iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
- iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ". - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iIntros "!> _". wp_if. by iApply "HΦ". iIntros "!> _". wp_if. by iApply "HΦ".
......
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