Commit 20534ab1 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/awp_apply' into 'master'

simplify wp_atomic, add awp_apply tactic to apply atomic updates

See merge request FP/iris-coq!209
parents 9e2e8f0a e8f25c81
Pipeline #14071 canceled with stage
in 8 minutes and 20 seconds
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
aheap : atomic_heap Σ
Q : iProp Σ
l : loc
v : val
============================
"Hl" : l ↦ v
--------------------------------------∗
AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
<< l ↦{q} v0, COMM Q -∗ Q >>
1 subgoal
Σ : gFunctors
......@@ -10,11 +24,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 +35,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 +56,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 +67,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 +87,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 +98,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 +119,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 +130,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 +152,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 +173,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 +195,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 +218,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 +241,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 +264,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 +287,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 +311,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
......
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import proofmode notation atomic_heap.
Set Default Proof Using "Type".
Section tests.
Context `{!heapG Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation.
(* FIXME: removing the `val` type annotation breaks printing. *)
Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
Q - l v - WP !#l {{ _, Q }}.
Proof.
iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
iAaccIntro with "Hl"; eauto with iFrame.
Qed.
End tests.
(* Test if AWP and the AU obtained from AWP print. *)
Section printing.
Context `{!heapG Σ}.
......@@ -13,28 +26,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 +56,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 +106,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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
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,40 @@ Proof.
Qed.
End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
(** Evaluate [lem] to a hypothesis [H] that can be applied, and then run
[wp_bind K; tac H] for every possible evaluation context. [tac] can do
[iApplyHyp H] to actually apply the hypothesis. TC resolution of [lem] premises
happens *after* [tac H] got executed. *)
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: the first, simple one just runs
[iAuIntro] on the goal, as atomic triples always have an atomic update as their
premise. The second one additionaly does some framing: it gets rid of [Hs] from
the context, which is intended to be the non-laterable assertions that iAuIntro
would choke on. You get them all back in the continuation of the atomic
operation. *)
Tactic Notation "awp_apply" open_constr(lem) :=
wp_apply_core lem (fun H => iApplyHyp H; last 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; last iAuIntro]).
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
let Htmp := iFresh in
......
......@@ -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Φ";