diff --git a/base_logic/derived.v b/base_logic/derived.v
index d3debb15f99b56d654520ada30b32adf88fc1df7..5432b0b1e677cc5bb253f615801b46b43c7a19f3 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -352,14 +352,8 @@ Lemma wand_elim_r P Q : P ★ (P -★ Q) ⊢ Q.
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
Lemma wand_elim_r' P Q R : (Q ⊢ P -★ R) → P ★ Q ⊢ R.
Proof. intros ->; apply wand_elim_r. Qed.
-Lemma wand_apply_l P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_r. Qed.
-Lemma wand_apply_l' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> <-; apply wand_elim_r. Qed.
+Lemma wand_apply P Q R S : (P ⊢ Q -★ R) → (S ⊢ P ★ Q) → S ⊢ R.
+Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R.
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P.
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index cd65d6692e343290e2165cd6d0b448a70f0daba3..9a95ee5c896a723d668ce27a506ab672fcae09cb 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -46,8 +46,8 @@ Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
Lemma wp_le E (n1 n2 : Z) P Φ :
- (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
- (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
+ (n1 ≤ n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+ (n2 < n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
@@ -55,8 +55,8 @@ Proof.
Qed.
Lemma wp_lt E (n1 n2 : Z) P Φ :
- (n1 < n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
- (n2 ≤ n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
+ (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+ (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
@@ -65,8 +65,8 @@ Qed.
Lemma wp_eq E e1 e2 v1 v2 P Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- (v1 = v2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
- (v1 ≠v2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
+ (v1 = v2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+ (v1 ≠v2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
P ⊢ WP BinOp EqOp e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 7f0dea5253dcbb2524ccb21068d1f56cc2fa1ed4..43d374169f01ec1b650edd8de9058a0b02b15a8a 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -122,12 +122,12 @@ Section heap.
(** Weakest precondition *)
Lemma wp_alloc E e v :
to_val e = Some v → nclose heapN ⊆ E →
- {{{ heap_ctx }}} Alloc e @ E {{{ l; LitV (LitLoc l), l ↦ v }}}.
+ {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
Proof.
- iIntros (<-%of_to_val ? Φ) "[#Hinv HΦ]". rewrite /heap_ctx.
+ iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
iMod (auth_empty heap_name) as "Ha".
iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
- iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !>".
+ iApply (wp_alloc_pst with "Hσ"). iNext. iIntros (l) "[% Hσ]".
iMod ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert.
eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
@@ -137,26 +137,26 @@ Section heap.
Lemma wp_load E l q v :
nclose heapN ⊆ E →
{{{ heap_ctx ★ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E
- {{{; v, l ↦{q} v }}}.
+ {{{ RET v; l ↦{q} v }}}.
Proof.
- iIntros (? Φ) "[[#Hinv >Hl] HΦ]".
+ iIntros (? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
- iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
+ iApply (wp_load_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
+ iNext; iIntros "Hσ".
iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed.
Lemma wp_store E l v' e v :
to_val e = Some v → nclose heapN ⊆ E →
{{{ heap_ctx ★ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E
- {{{; LitV LitUnit, l ↦ v }}}.
+ {{{ RET LitV LitUnit; l ↦ v }}}.
Proof.
- iIntros (<-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
+ iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
- iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("Hcl" with "* [Hσ]") as "Ha".
+ iApply (wp_store_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
+ iNext; iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert.
eapply singleton_local_update, exclusive_local_update; last done.
by eapply heap_singleton_included'. }
@@ -166,26 +166,26 @@ Section heap.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠v1 → nclose heapN ⊆ E →
{{{ heap_ctx ★ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
- {{{; LitV (LitBool false), l ↦{q} v' }}}.
+ {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
Proof.
- iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[[#Hinv >Hl] HΦ]".
+ iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
- iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
- iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
+ iApply (wp_cas_fail_pst _ σ with "Hσ"); [eauto using heap_singleton_included|done|].
+ iNext; iIntros "Hσ".
iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E →
{{{ heap_ctx ★ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
- {{{; LitV (LitBool true), l ↦ v2 }}}.
+ {{{ RET LitV (LitBool true); l ↦ v2 }}}.
Proof.
- iIntros (<-%of_to_val <-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
+ iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
- iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("Hcl" with "* [Hσ]") as "Ha".
+ iApply (wp_cas_suc_pst _ σ with "Hσ"); first by eauto using heap_singleton_included.
+ iNext. iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert.
eapply singleton_local_update, exclusive_local_update; last done.
by eapply heap_singleton_included'. }
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 9436c07e1bd22d0433797b8262ffab1a4d2682e9..764fa2347341f2acc3f1a3f010cd5555ef9f3815 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -92,10 +92,10 @@ Qed.
(** Actual proofs *)
Lemma newbarrier_spec (P : iProp Σ) :
heapN ⊥ N →
- {{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P ★ send l P }}}.
+ {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P ★ send l P }}}.
Proof.
- iIntros (HN Φ) "[#? HΦ]".
- rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
+ iIntros (HN Φ) "#? HΦ".
+ rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with ">[-]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
@@ -117,10 +117,10 @@ Proof.
Qed.
Lemma signal_spec l P :
- {{{ send l P ★ P }}} signal #l {{{; #(), True }}}.
+ {{{ send l P ★ P }}} signal #l {{{ RET #(); True }}}.
Proof.
rewrite /signal /send /barrier_ctx /=.
- iIntros (Φ) "((Hs&HP)&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
+ iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store.
@@ -133,10 +133,10 @@ Proof.
Qed.
Lemma wait_spec l P:
- {{{ recv l P }}} wait #l {{{ ; #(), P }}}.
+ {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
Proof.
rename P into R; rewrite /recv /barrier_ctx.
- iIntros (Φ) "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+ iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_bind (! _)%E.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
@@ -158,7 +158,7 @@ Proof.
iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
iModIntro. wp_if.
- iModIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
+ iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
Lemma recv_split E l P1 P2 :
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index 319dd0be941307eabc4823e1bf0b6d677ca40116..c0de6dd97b73b9b7fcb0d23bc392441152673cd3 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -20,10 +20,10 @@ Proof.
intros HN.
exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
split_and?; simpl.
- - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); first done.
- iSplit; first done. iNext. eauto.
- - iIntros (l P) "!# [Hl HP]". iApply signal_spec; iFrame "Hl HP"; by eauto.
- - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto.
+ - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
+ iNext. eauto.
+ - iIntros (l P) "!# [Hl HP]". iApply (signal_spec with "[$Hl $HP]"). by eauto.
+ - iIntros (l P) "!# Hl". iApply (wait_spec with "Hl"). eauto.
- iIntros (l P Q) "!#". by iApply recv_split.
- apply recv_weaken.
Qed.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 60f534434f849879387697fc8566c238d9c4e878..16a4967301f07a33b4341755c147a9337cc96397 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -35,9 +35,9 @@ Section mono_proof.
Lemma newcounter_mono_spec (R : iProp Σ) :
heapN ⊥ N →
- {{{ heap_ctx }}} newcounter #() {{{ l; #l, mcounter l 0 }}}.
+ {{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
- iIntros (? Φ) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+ iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
@@ -45,9 +45,9 @@ Section mono_proof.
Qed.
Lemma inc_mono_spec l n :
- {{{ mcounter l n }}} inc #l {{{; #(), mcounter l (S n) }}}.
+ {{{ mcounter l n }}} inc #l {{{ RET #(); mcounter l (S n) }}}.
Proof.
- iIntros (Φ) "[Hl HΦ]". iLöb as "IH". wp_rec.
+ iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
@@ -70,9 +70,9 @@ Section mono_proof.
Qed.
Lemma read_mono_spec l j :
- {{{ mcounter l j }}} read #l {{{ i; #i, ■(j ≤ i)%nat ∧ mcounter l i }}}.
+ {{{ mcounter l j }}} read #l {{{ i, RET #i; ■(j ≤ i)%nat ∧ mcounter l i }}}.
Proof.
- iIntros (ϕ) "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
+ iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[?%mnat_included _]%auth_valid_discrete_2.
@@ -112,9 +112,9 @@ Section contrib_spec.
Lemma newcounter_contrib_spec (R : iProp Σ) :
heapN ⊥ N →
{{{ heap_ctx }}} newcounter #()
- {{{ γ l; #l, ccounter_ctx γ l ★ ccounter γ 1 0 }}}.
+ {{{ γ l, RET #l; ccounter_ctx γ l ★ ccounter γ 1 0 }}}.
Proof.
- iIntros (? Φ) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+ iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (â— (Some (1%Qp, O%nat)) â‹… â—¯ (Some (1%Qp, 0%nat))))
as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
@@ -124,9 +124,9 @@ Section contrib_spec.
Lemma inc_contrib_spec γ l q n :
{{{ ccounter_ctx γ l ★ ccounter γ q n }}} inc #l
- {{{; #(), ccounter γ q (S n) }}}.
+ {{{ RET #(); ccounter γ q (S n) }}}.
Proof.
- iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)". iLöb as "IH". wp_rec.
+ iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op.
@@ -145,9 +145,9 @@ Section contrib_spec.
Lemma read_contrib_spec γ l q n :
{{{ ccounter_ctx γ l ★ ccounter γ q n }}} read #l
- {{{ c; #c, ■(n ≤ c)%nat ∧ ccounter γ q n }}}.
+ {{{ c, RET #c; ■(n ≤ c)%nat ∧ ccounter γ q n }}}.
Proof.
- iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
+ iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
@@ -157,9 +157,9 @@ Section contrib_spec.
Lemma read_contrib_spec_1 γ l n :
{{{ ccounter_ctx γ l ★ ccounter γ 1 n }}} read #l
- {{{ n; #n, ccounter γ 1 n }}}.
+ {{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
- iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
+ iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2.
apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 42bc6a572dcdb160d017b0476184733b4f147a94..43f81ecb517a61995abe5797328987b1f0344588 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -18,11 +18,11 @@ Structure lock Σ `{!heapG Σ} := Lock {
(* -- operation specs -- *)
newlock_spec N (R : iProp Σ) :
heapN ⊥ N →
- {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock N γ lk R }}};
+ {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
acquire_spec N γ lk R :
- {{{ is_lock N γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}};
+ {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}};
release_spec N γ lk R :
- {{{ is_lock N γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}
+ {{{ is_lock N γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}
}.
Arguments newlock {_ _} _.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index bae873a2327d28d564a6b690f1c3f448a1cf53f1..5efd170e7884bd36fd559a0530ccc5dba22e8a46 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -16,6 +16,10 @@ Global Opaque par.
Section proof.
Context `{!heapG Σ, !spawnG Σ}.
+(* Notice that this allows us to strip a later *after* the two Ψ have been
+ brought together. That is strictly stronger than first stripping a later
+ and then merging them, as demonstrated by [tests/joining_existentials.v].
+ This is why these are not Texan triples. *)
Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) :
to_val e = Some (f1,f2)%V →
(heap_ctx ★ WP f1 #() {{ Ψ1 }} ★ WP f2 #() {{ Ψ2 }} ★
@@ -23,11 +27,11 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
⊢ WP par e {{ Φ }}.
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
- rewrite /par. wp_value. iModIntro. wp_let. wp_proj.
- wp_apply (spawn_spec parN with "[- $Hh $Hf1]"); try wp_done; try solve_ndisj.
+ rewrite /par. wp_value. wp_let. wp_proj.
+ wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand_r with "[- $Hf2]"); iIntros (v) "H2". wp_let.
- wp_apply (join_spec with "[- $Hl]"). iIntros (w) "H1".
+ wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Qed.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 9c4bb70c3aa9baf8e9213251fc55fd1ea3689106..54053ad1b2c77989ddb5fb5fbf17a270da244ac0 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -49,31 +49,31 @@ Proof. solve_proper. Qed.
Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
to_val e = Some f →
heapN ⊥ N →
- {{{ heap_ctx ★ WP f #() {{ Ψ }} }}} spawn e {{{ l; #l, join_handle l Ψ }}}.
+ {{{ heap_ctx ★ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
- iIntros (<-%of_to_val ? Φ) "((#Hh & Hf) & HΦ)". rewrite /spawn /=.
+ iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork; simpl. iSplitR "Hf".
- - iModIntro. wp_seq. iModIntro. iApply "HΦ". rewrite /join_handle. eauto.
+ - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply (wp_wand_r with "[ $Hf]"); iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
Lemma join_spec (Ψ : val → iProp Σ) l :
- {{{ join_handle l Ψ }}} join #l {{{ v; v, Ψ v }}}.
+ {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
Proof.
- rewrite /join_handle; iIntros (Φ) "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
+ rewrite /join_handle; iIntros (Φ) "[% H] HΦ". iDestruct "H" as (γ) "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
- iModIntro. wp_match. iApply ("IH" with "Hγ [Hv]"). auto.
+ iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
- iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
- iModIntro. wp_match. by iApply "Hv".
+ iModIntro. wp_match. by iApply "HΦ".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed.
End proof.
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 34b5b22c352803a5a7fda785a797b86184f3b7fa..44443f4f66b634ddfa680dfbd231b61e67be6317 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -47,9 +47,9 @@ Section proof.
Lemma newlock_spec (R : iProp Σ):
heapN ⊥ N →
- {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
+ {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
- iIntros (? Φ) "[[#Hh HR] HΦ]". rewrite /newlock /=.
+ iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
@@ -59,9 +59,9 @@ Section proof.
Lemma try_acquire_spec γ lk R :
{{{ is_lock γ lk R }}} try_acquire lk
- {{{b; #b, if b is true then locked γ ★ R else True }}}.
+ {{{ b, RET #b; if b is true then locked γ ★ R else True }}}.
Proof.
- iIntros (Φ) "[#Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
+ iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). done.
@@ -71,18 +71,18 @@ Section proof.
Qed.
Lemma acquire_spec γ lk R :
- {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
+ {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}}.
Proof.
- iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec.
- wp_apply (try_acquire_spec with "[- $Hl]"). iIntros ([]).
- - iIntros "[Hlked HR]". wp_if. iModIntro. iApply "HΦ"; iFrame.
+ iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
+ wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
+ - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
- iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
Lemma release_spec γ lk R :
- {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}.
+ {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}.
Proof.
- iIntros (Φ) "((Hlock & Hlocked & HR) & HΦ)".
+ iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 3846ddebefa8f41ff6bab1ada82abb1c695bb7d7..5300485fcc6ef81e7e75f321a8451c104c8321ff 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -76,9 +76,9 @@ Section proof.
Lemma newlock_spec (R : iProp Σ) :
heapN ⊥ N →
- {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
+ {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
- iIntros (HN Φ) "((#Hh & HR) & HΦ)". rewrite /newlock /=.
+ iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
iMod (own_alloc (◠(Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
@@ -89,9 +89,9 @@ Section proof.
Qed.
Lemma wait_loop_spec γ lk x R :
- {{{ issued γ lk x R }}} wait_loop #x lk {{{; #(), locked γ ★ R }}}.
+ {{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ ★ R }}}.
Proof.
- iIntros (Φ) "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
+ iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -99,7 +99,7 @@ Section proof.
+ iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
{ iNext. iExists o, n. iFrame. eauto. }
iModIntro. wp_let. wp_op=>[_|[]] //.
- wp_if. iModIntro.
+ wp_if.
iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
+ iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
set_solver.
@@ -110,9 +110,9 @@ Section proof.
Qed.
Lemma acquire_spec γ lk R :
- {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
+ {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}}.
Proof.
- iIntros (ϕ) "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
+ iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
@@ -131,8 +131,9 @@ Section proof.
{ iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
iModIntro. wp_if.
- iApply (wait_loop_spec γ (#lo, #ln)).
- iFrame "HΦ". rewrite /issued; eauto 10.
+ iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+ + rewrite /issued; eauto 10.
+ + by iNext.
- wp_cas_fail.
iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
{ iNext. iExists o', n'. by iFrame. }
@@ -140,9 +141,9 @@ Section proof.
Qed.
Lemma release_spec γ lk R :
- {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}.
+ {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}.
Proof.
- iIntros (Φ) "((Hl & Hγ & HR) & HΦ)".
+ iIntros (Φ) "(Hl & Hγ & HR) HΦ".
iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
iDestruct "Hγ" as (o) "Hγo".
rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 2d2e5be870f440c0c6c28cf9719b6546ee6e2a1a..71ce9d61655dd367d747d5f57388522078ca6c3c 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -46,59 +46,59 @@ Lemma wp_bind_ctxi {E e} Ki Φ :
Proof. exact: weakestpre.wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ v Φ :
- ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
- ⊢ WP Alloc (of_val v) @ E {{ Φ }}.
+Lemma wp_alloc_pst E σ v :
+ {{{ ▷ ownP σ }}} Alloc (of_val v) @ E
+ {{{ l, RET LitV (LitLoc l); σ !! l = None ∧ ownP (<[l:=v]>σ) }}}.
Proof.
- iIntros "[HP HΦ]".
+ iIntros (Φ) "HP HΦ".
iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
subst v2. iSplit. iApply "HΦ"; by iSplit. by iApply big_sepL_nil.
Qed.
-Lemma wp_load_pst E σ l v Φ :
+Lemma wp_load_pst E σ l v :
σ !! l = Some v →
- ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+ {{{ ▷ ownP σ }}} Load (Lit (LitLoc l)) @ E {{{ RET v; ownP σ }}}.
Proof.
- intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto.
+ intros ? Φ. apply (wp_lift_atomic_det_head_step' σ v σ); eauto.
intros; inv_head_step; eauto.
Qed.
-Lemma wp_store_pst E σ l v v' Φ :
+Lemma wp_store_pst E σ l v v' :
σ !! l = Some v' →
- ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
- ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
+ {{{ ▷ ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E
+ {{{ RET LitV LitUnit; ownP (<[l:=v]>σ) }}}.
Proof.
- intros. rewrite-(wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
+ intros. apply (wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
intros; inv_head_step; eauto.
Qed.
-Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
+Lemma wp_cas_fail_pst E σ l v1 v2 v' :
σ !! l = Some v' → v' ≠v1 →
- ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
- ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
+ {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
+ {{{ RET LitV $ LitBool false; ownP σ }}}.
Proof.
- intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
+ intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
intros; inv_head_step; eauto.
Qed.
-Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
+Lemma wp_cas_suc_pst E σ l v1 v2 :
σ !! l = Some v1 →
- ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
- ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
+ {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
+ {{{ RET LitV $ LitBool true; ownP (<[l:=v2]>σ) }}}.
Proof.
- intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
+ intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
(<[l:=v2]>σ)); eauto.
intros; inv_head_step; eauto.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e Φ :
- ▷ (|={E}=> Φ (LitV LitUnit)) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
+ ▷ Φ (LitV LitUnit) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
- - by rewrite later_sep -(wp_value_fupd _ _ (Lit _)) // big_sepL_singleton.
+ - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
- intros; inv_head_step; eauto.
Qed.
@@ -116,20 +116,20 @@ Qed.
Lemma wp_un_op E op e v v' Φ :
to_val e = Some v →
un_op_eval op v = Some v' →
- ▷ (|={E}=> Φ v') ⊢ WP UnOp op e @ E {{ Φ }}.
+ ▷ Φ v' ⊢ WP UnOp op e @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
- -?wp_value_fupd'; eauto.
+ -?wp_value'; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
bin_op_eval op v1 v2 = Some v' →
- ▷ (|={E}=> Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
+ ▷ (Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
- -?wp_value_fupd'; eauto.
+ -?wp_value'; eauto.
intros; inv_head_step; eauto.
Qed.
@@ -149,19 +149,19 @@ Qed.
Lemma wp_fst E e1 v1 e2 Φ :
to_val e1 = Some v1 → is_Some (to_val e2) →
- ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
+ ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ? [v2 ?].
- rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value_fupd; eauto.
+ rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_snd E e1 e2 v2 Φ :
is_Some (to_val e1) → to_val e2 = Some v2 →
- ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
+ ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros [v1 ?] ?.
- rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value_fupd; eauto.
+ rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value; eauto.
intros; inv_head_step; eauto.
Qed.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 83e5f27d00ba2390f98a71e38b4ac89dc6ccb3d6..e0fba481b36dda57309490ba0a88933cc8ab127b 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -22,10 +22,10 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
IntoLaterEnvs Δ Δ' →
(∀ l, ∃ Δ'',
envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
- (Δ'' ⊢ |={E}=> Φ (LitV (LitLoc l)))) →
+ (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
Δ ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
- intros ???? HΔ. rewrite -wp_fupd -wp_alloc // -always_and_sep_l.
+ intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
@@ -36,10 +36,10 @@ Lemma tac_wp_load Δ Δ' E i l q v Φ :
(Δ ⊢ heap_ctx) → nclose heapN ⊆ E →
IntoLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
- (Δ' ⊢ |={E}=> Φ v) →
+ (Δ' ⊢ Φ v) →
Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
- intros. rewrite -wp_fupd -wp_load // -assoc -always_and_sep_l.
+ intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
@@ -51,10 +51,10 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
IntoLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
- (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
+ (Δ'' ⊢ Φ (LitV LitUnit)) →
Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
- intros. rewrite -wp_fupd -wp_store // -assoc -always_and_sep_l.
+ intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
@@ -65,10 +65,10 @@ Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
(Δ ⊢ heap_ctx) → nclose heapN ⊆ E →
IntoLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠v1 →
- (Δ' ⊢ |={E}=> Φ (LitV (LitBool false))) →
+ (Δ' ⊢ Φ (LitV (LitBool false))) →
Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
- intros. rewrite -wp_fupd -wp_cas_fail // -assoc -always_and_sep_l.
+ intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
@@ -80,10 +80,10 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
IntoLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
- (Δ'' ⊢ |={E}=> Φ (LitV (LitBool true))) →
+ (Δ'' ⊢ Φ (LitV (LitBool true))) →
Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
- intros; subst. rewrite -wp_fupd -wp_cas_suc // -assoc -always_and_sep_l.
+ intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 4f7309555bbfc5606058cedeb1615d816dbdd867..26856a3a1c5bdf5314a02b82dbc404df9d86b90d 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -18,20 +18,7 @@ Ltac wp_done :=
| _ => fast_done
end.
-(* sometimes, we want to keep the update modality, so only apply [fupd_intro]
-if we obtain a consecutive wp *)
-Ltac wp_strip_fupd :=
- lazymatch goal with
- | |- _ ⊢ |={?E}=> _ =>
- etrans; [|apply fupd_intro];
- match goal with
- | |- _ ⊢ wp E _ _ => simpl
- | |- _ ⊢ |={E,_}=> _ => simpl
- | _ => fail
- end
- end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value_fupd; wp_done]; lazy beta.
+Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
@@ -48,7 +35,6 @@ Ltac wp_finish := intros_revert ltac:(
| |- _ ⊢ wp ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; wp_strip_later
| |- _ ⊢ wp ?E _ ?Q => wp_value_head
- | |- _ ⊢ |={_,_}=> _ => wp_strip_fupd
end).
Tactic Notation "wp_value" :=
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 99df308b6349a696739113de8675c689a07faef9..28a3e76362232b50d58a109c386771279b0163cd 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -43,7 +43,7 @@ Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
head_reducible e1 σ1 →
▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
■head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★
- (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+ Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
@@ -56,19 +56,19 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
(∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ ownP σ1 ★ ▷ (ownP σ2 -★
- (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+ Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_atomic_det_step. Qed.
-Lemma wp_lift_atomic_det_head_step' {E Φ e1} σ1 v2 σ2 :
+Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 :
atomic e1 →
head_reducible e1 σ1 →
(∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
- ▷ ownP σ1 ★ ▷ (ownP σ2 ={E}=★ Φ v2) ⊢ WP e1 @ E {{ Φ }}.
+ {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
Proof.
- intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 [])
- ?big_sepL_nil ?right_id; eauto.
+ intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
+ rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
Qed.
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 8b05a82900fd167ef8c0e56d1d29d2fe362867e4..a3335b346e5a4aea35d697cf96decfc8b6e78206 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -48,7 +48,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
atomic e1 →
reducible e1 σ1 →
(▷ ownP σ1 ★ ▷ ∀ v2 σ2 efs, ■prim_step e1 σ1 (of_val v2) σ2 efs ★ ownP σ2 -★
- (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+ Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
@@ -57,7 +57,7 @@ Proof.
iNext; iIntros (e2 σ2 efs) "[% Hσ]".
edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
- iMod "Hclose". iMod "HΦ". iApply wp_value; auto using to_of_val.
+ iMod "Hclose". iApply wp_value; auto using to_of_val.
Qed.
Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
@@ -66,7 +66,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
(∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ ownP σ1 ★ ▷ (ownP σ2 -★
- (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+ Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 6b98efa4d050cbbc1f0b58d1f8b81a40dc897dcc..d5f94f1c4b34ddf051e6c31fc16143f02f5acc62 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -68,43 +68,43 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
format "'WP' e {{ v , Q } }") : uPred_scope.
(* Texan triples *)
-Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
- P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
+ P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
+ format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
- P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
+ P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ E {{{ x .. y ; pat , Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
- (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
+ format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
+ (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
(at level 20,
- format "{{{ P } } } e {{{ ; pat , Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
- (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
+ format "{{{ P } } } e {{{ RET pat ; Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
+ (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
(at level 20,
- format "{{{ P } } } e @ E {{{ ; pat , Q } } }") : uPred_scope.
+ format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
- P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e {{ Φ }})
+ P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : C_scope.
-Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
+ format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
- P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e @ E {{ Φ }})
+ P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ E {{{ x .. y ; pat , Q } } }") : C_scope.
-Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
- (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e {{ Φ }})
+ format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : C_scope.
+Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
+ (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})
(at level 20,
- format "{{{ P } } } e {{{ ; pat , Q } } }") : C_scope.
-Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
- (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e @ E {{ Φ }})
+ format "{{{ P } } } e {{{ RET pat ; Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
+ (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})
(at level 20,
- format "{{{ P } } } e @ E {{{ ; pat , Q } } }") : C_scope.
+ format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : C_scope.
Section wp.
Context `{irisG Λ Σ}.
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 71071bc05d5319c5e3d7440e580f613c146939e7..e29e8cbb59ad1e391f54c422550a8c0d4b74f3b3 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -37,11 +37,12 @@ Section client.
Lemma client_safe : heapN ⊥ N → heap_ctx ⊢ WP client {{ _, True }}.
Proof.
iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
- wp_apply (newbarrier_spec N (y_inv 1 y) with "[- $Hh]"); first done.
+ wp_apply (newbarrier_spec N (y_inv 1 y) with "Hh"); first done.
iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[-$Hh]"). iSplitL "Hy Hs".
- (* The original thread, the sender. *)
- wp_store. iApply (signal_spec with "[- $Hs]"). iSplitL "Hy"; [|by eauto].
+ wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
+ iSplitR "Hy"; first by eauto.
iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
- (* The two spawned threads, the waiters. *)
iSplitL; [|by iIntros (_ _) "_ !>"].
diff --git a/tests/counter.v b/tests/counter.v
index 8986a132626462a7db31da9255fd4a2963d53c4b..7056e303ccc6b4ec6ecbc956399033ab881d68bd 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -95,7 +95,7 @@ Lemma newcounter_spec N :
heapN ⊥ N →
heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, v = #l ∧ C l 0 }}.
Proof.
- iIntros (?) "#Hh !# _ /=". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+ iIntros (?) "#Hh !# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
@@ -119,7 +119,7 @@ Proof.
rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]").
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iModIntro. wp_if. iModIntro; rewrite {3}/C; eauto 10.
+ iModIntro. wp_if. rewrite {3}/C; eauto 10.
- wp_cas_fail; first (intros [=]; abstract omega).
iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 5f05dd6f3f0bc60d80101eed65f9f1d9b464df96..4cd2dd065c4d698c85de78cea753d0904c4db8fa 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -46,7 +46,7 @@ Section LiftingTests.
iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
- iApply ("IH" with "[%] HΦ"). omega.
- - iApply fupd_intro. by assert (n1 = n2 - 1) as -> by omega.
+ - by assert (n1 = n2 - 1) as -> by omega.
Qed.
Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index b2351a1ab107d335f34f2f0ab1db0a16693034e1..2abc3576672b5ddb0a36598748fef86e839f4068 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -76,7 +76,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
Proof.
iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
- wp_apply (newbarrier_spec N (barrier_res γ Φ) with "[- $Hh]"); auto.
+ wp_apply (newbarrier_spec N (barrier_res γ Φ) with "Hh"); auto.
iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par (λ _, True)%I workers_post with "[- $Hh]").
@@ -85,7 +85,7 @@ Proof.
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iMod (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). }
- iApply (signal_spec with "[- $Hs]"). iSplitR ""; last auto.
+ iApply (signal_spec with "[- $Hs]"); last auto.
iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iMod (recv_split with "Hr") as "[H1 H2]"; first done.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index aaeeaf2b20d2ae5b5136bfbfb8ab35b661abdd88..cfdaecc0d7d65d69725a09230f3fe2f357d05cc1 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -42,7 +42,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
⊢ WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "[#? Hf] /=".
- rewrite /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
+ rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
iMod (own_alloc Pending) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
@@ -69,7 +69,7 @@ Proof.
+ iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iMod ("Hclose" with "[Hinv]") as "_"; eauto; iModIntro.
- wp_let. iModIntro. iIntros "!#". wp_seq.
+ wp_let. iIntros "!#". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_bind (! _)%E.