Skip to content
GitLab
Commit d4942fbf authored by Ralf Jung's avatar Ralf Jung
Browse files

introduce awp_apply tactic for applying atomic WP

parent 6de240cc
Hide whitespace changes
Inline Side-by-side
tests/atomic.8.8.ref
View file @ d4942fbf
......@@ -10,11 +10,9 @@
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -23,14 +21,12 @@
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >>
<< ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -46,11 +42,9 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -59,14 +53,11 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >>
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -82,11 +73,9 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -95,14 +84,12 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
<< ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -118,11 +105,9 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -131,13 +116,11 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >>
@ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -155,12 +138,10 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -178,12 +159,10 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
@ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -202,14 +181,12 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Q -∗ Φ #() >>
COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -227,12 +204,10 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >>
<< l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -252,12 +227,10 @@
heapG0 : heapG Σ
l : loc
x : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -277,12 +250,10 @@
heapG0 : heapG Σ
l : loc
x : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ #(), COMM Q -∗ Φ #() >>
<< l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -302,12 +273,10 @@
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
@ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -328,31 +297,16 @@
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Q -∗ Φ #() >>
COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
"Prettification"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
--------------------------------------∗
∀ Φ : language.val heap_lang → iProp Σ, AU << ∀
x : val,
P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
-∗ WP ! #0 {{ v, Φ v }}
1 subgoal
Σ : gFunctors
......
tests/atomic.v
View file @ d4942fbf
......@@ -13,28 +13,28 @@ Section printing.
Lemma print_both_quant (P : val → iProp Σ) :
<<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_first_quant l :
<<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_second_quant l :
<<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_no_quant l :
<<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
......@@ -43,49 +43,49 @@ Section printing.
Lemma print_both_quant_long l :
<<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpre l :
<<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpost l :
<<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? ?". Show.
Show. iIntros (Φ) "?". Show.
Abort.
Lemma print_first_quant_long l :
<<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_second_quant_long l x :
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_long l x :
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpre l xx yyyy :
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpost l xx yyyy :
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
Proof.
Show. iIntros (Q Φ) "? AU". Show.
Show. iIntros (Φ) "AU". Show.
Abort.
Check "Prettification".
......@@ -93,7 +93,6 @@ Section printing.
Lemma iMod_prettify (P : val → iProp Σ) :
<<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
Proof.
iApply wp_atomic_intro. Show.
iIntros (Φ) "AU". iMod "AU". Show.
Abort.
......
theories/heap_lang/lib/atomic_heap.v
View file @ d4942fbf
......@@ -81,18 +81,18 @@ Section proof.
<<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
<<< l ↦{q} v, RET v >>>.
Proof.
iIntros (Q Φ) "? AU". wp_lam.
iIntros (Φ) "AU". wp_lam.
iMod "AU" as (v q) "[H↦ [_ Hclose]]".
wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
wp_load. iMod ("Hclose" with "H↦") as "HΦ". done.
Qed.
Lemma primitive_store_spec (l : loc) (w : val) :
<<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
<<< l ↦ w, RET #() >>>.
Proof.
iIntros (Q Φ) "? AU". wp_lam. wp_let.
iIntros (Φ) "AU". wp_lam. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
Qed.
Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
......@@ -102,10 +102,10 @@ Section proof.
<<< if decide (v = w1) then l ↦ w2 else l ↦ v,
RET #(if decide (v = w1) then true else false) >>>.
Proof.
iIntros (? Q Φ) "? AU". wp_lam. wp_let. wp_let.
iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
iMod ("Hclose" with "H↦") as "HΦ"; done.
Qed.
End proof.
......
theories/heap_lang/lib/coin_flip.v
View file @ d4942fbf
......@@ -50,7 +50,7 @@ Section coinflip.
@ ⊤
<<< ∃ (b: bool), x ↦ #0, RET #b >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
iIntros (Φ) "AU". wp_lam.
wp_apply rand_spec; first done.
iIntros (b) "_". wp_let.
wp_bind (_ <- _)%E.
......@@ -73,7 +73,7 @@ Section coinflip.
@ ⊤
<<< ∃ (b: bool), x ↦ #0, RET #b >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
iIntros (Φ) "AU". wp_lam.
wp_apply wp_new_proph; first done.
iIntros (v p) "Hp".
wp_let.
......
theories/heap_lang/lib/increment.v
View file @ d4942fbf
......@@ -23,7 +23,7 @@ Section increment_physical.
Lemma incr_phy_spec (l: loc) :
<<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
wp_load. iMod ("Hclose" with "Hl") as "AU". iModIntro.
wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
......@@ -55,24 +55,24 @@ Section increment.
Lemma incr_spec_direct (l: loc) :
<<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_apply load_spec; first by iAccu.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
awp_apply load_spec.
(* Prove the atomic update for load *)
iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
iModIntro. iExists _, _. iFrame "Hl". iSplit.
{ (* abort case *) done. }
iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iIntros "!> _".
iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro.
(* Now go on *)
wp_apply cas_spec; [done|iAccu|].
awp_apply cas_spec; first done.
(* Prove the atomic update for CAS *)
iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
iModIntro. iExists _. iFrame "Hl". iSplit.
{ (* abort case *) iDestruct "Hclose" as "[? _]". done. }
iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
- iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iIntros "!> _". wp_if. by iApply "HΦ".
iIntros "!>". wp_if. by iApply "HΦ".
- iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
iIntros "!> _". wp_if. iApply "IH". done.
iIntros "!>". wp_if. iApply "IH". done.
Qed.
(** A proof of the incr specification that uses lemmas to avoid reasining
......@@ -80,22 +80,22 @@ Section increment.
Lemma incr_spec (l: loc) :
<<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_apply load_spec; first by iAccu.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
awp_apply load_spec.
(* Prove the atomic update for load *)
iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
iApply (aacc_aupd_abort with "AU"); first done.
iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> AU !> _".
iIntros "$ !> AU !>".
(* Now go on *)
wp_apply cas_spec; [done|iAccu|].
awp_apply cas_spec; first done.
(* Prove the atomic update for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "H↦ !>".
destruct (decide (#x' = #x)) as [[= ->]|Hx].
- iRight. iFrame. iIntros "HΦ !> _".
- iRight. iFrame. iIntros "HΦ !>".
wp_if. by iApply "HΦ".
- iLeft. iFrame. iIntros "AU !> _".
- iLeft. iFrame. iIntros "AU !>".
wp_if. iApply "IH". done.
Qed.
......@@ -116,17 +116,17 @@ Section increment.
weak_incr #l @ ⊤
<<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
iIntros "Hl" (Φ) "AU". wp_lam.
wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
iIntros "Hl". wp_apply store_spec; first by iAccu.
iIntros "Hl". awp_apply store_spec.
(* Prove the atomic update for store *)
iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
iApply (aacc_aupd_commit with "AU"); first done.
iIntros (x) "H↦".
iDestruct (mapsto_agree with "Hl H↦") as %[= <-].
iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
{ iIntros "[$ $]"; eauto. }
iIntros "$ !>". iSplit; first done.
iIntros "HΦ !> _". wp_seq. done.
iIntros "HΦ !>". wp_seq. done.
Qed.
End increment.
......@@ -149,8 +149,8 @@ Section increment_client.
(* FIXME: I am only using persistent stuff, so I should be allowed
to move this to the persisten context even without the additional □. *)
iAssert (□ WP incr #l {{ _, True }})%I as "#Aupd".
{ iAlways. wp_apply incr_spec; first by iAccu. clear x.
iAuIntro. iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
{ iAlways. awp_apply incr_spec. clear x.
iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
(* The continuation: From after the atomic triple to the postcondition of the WP *)
done.
......
theories/heap_lang/proofmode.v
View file @ d4942fbf
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import atomic.
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export tactics lifting.
......@@ -354,24 +355,31 @@ Proof.
Qed.
End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
wp_pures;
iPoseProofCore lem as false true (fun H =>
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
wp_bind_core K; tac H) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
twp_bind_core K; tac H) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
| _ => fail "wp_apply: not a 'wp'"
end).
Tactic Notation "wp_apply" open_constr(lem) :=
wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl).
(* Tactic tailored for atomic triples *)
Tactic Notation "awp_apply" open_constr(lem) :=
wp_apply_core lem (fun H => iApplyHyp H; iAuIntro).
Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H; iAuIntro]).
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
let Htmp := iFresh in
......
theories/program_logic/atomic.v
View file @ d4942fbf
......@@ -14,8 +14,8 @@ Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
(β: TA → TB → iProp Σ) (* atomic post-condition *)
(f: TA → TB → val Λ) (* Turn the return data into the return value *)
: iProp Σ :=
(∀ Q (Φ : val Λ → iProp Σ), Q -∗
atomic_update Eo ∅ α β (λ.. x y, Q -∗ Φ (f x y)) -∗
(∀ (Φ : val Λ → iProp Σ),
atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
WP e {{ Φ }})%I.
(* Note: To add a private postcondition, use
atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
......@@ -102,8 +102,8 @@ Section lemmas.
atomic_wp e Eo α β f -∗
∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
Proof.
rewrite ->tforall_forall in HL.
iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
......@@ -116,23 +116,12 @@ Section lemmas.
(∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}) -∗
atomic_wp e Eo α β f.
Proof.
simpl in HP. iIntros "Hwp" (Q Φ) "HQ HΦ". iApply fupd_wp.
simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iApply "HΦ". done.
rewrite ->!tele_app_bind. done.
Qed.
(* Way to prove an atomic triple without seeing the Q *)
Lemma wp_atomic_intro e Eo α β f :
(∀ (Φ : val Λ → iProp),