Merge branch 'janno/hoare-notation' into 'master'

Add triple notation for generalized post-condition

This changeset defines notation for the Iris style of writing Hoare triples:

`{{{ P }}} e {{{ v1 .. vn; T, Q }}} := P ★ (∀ v1 .. vn, Q → Φ T) ⊢ WP e {{ Φ }}`

For no good reason the notation is parsing only, although I do not declare it as such. We might want to do that though, since it might be too hard to understand a Hoare triple goal without unfolding it.

I have changed the barrier specifications to use the new notation in an attempt to demonstrate their usefulness (or, at a minimum, their applicability). The changes are rather minimal, as you can see.

## Changes

First and foremost, the specifications change. (Duh!)
Then, there are three kinds of changes to the proofs:
1. The first `iIntros` needs to take care of introducing `Φ`. No big deal, in my opinion.
2. Introducing the spatial assumptions needs one additional level of structure since we go from

    ```P1 ★ P2 ★ (∀ v, Q v -★ Φ v)```
to
   ```(P1 ★ P2) ★ (∀ v, Q v -★ Φ v)```

3. A post-condition of `True` leads to the rather annoying hypothesis `True -★ Φ v`, which (as far as I can tell) cannot be made to behave the same as just (Φ v) in the context of `iFrame`.

## Applicability

I have also looked at most other examples of specifications in heap_lang/lib.  The notation seems to be applicable to almost all of them. The only place where I spotted an obvious mismatch is par.v, where the current lemmas have a later before the generalized post-condition, as in `... ★ (∀ .., ... -★ ▷ Φ ..) ⊢ WP ..`. We could always add another pair of notations for this special case, I suppose.

## Nomenclature
I think "Texan triple" would be a good name, seeing how everything is bigger in Texas, including the number of curly braces.

See merge request !9

base_logic/primitive.v

@@ -171,9 +171,11 @@ Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
 Notation "P -★ Q" := (uPred_wand P Q)
   (at level 99, Q at level 200, right associativity) : uPred_scope.
 Notation "∀ x .. y , P" :=
-  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
+  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I)
+  (at level 200, x binder, y binder, right associativity) : uPred_scope.
 Notation "∃ x .. y , P" :=
-  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
+  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I)
+  (at level 200, x binder, y binder, right associativity) : uPred_scope.
 Notation "□ P" := (uPred_always P)
   (at level 20, right associativity) : uPred_scope.
 Notation "▷ P" := (uPred_later P)

heap_lang/heap.v

@@ -104,11 +104,11 @@ Section heap.
   Proof. by rewrite heap_mapsto_op_half. Qed.
 
   (** Weakest precondition *)
-  Lemma wp_alloc E e v Φ :
+  Lemma wp_alloc E e v :
     to_val e = Some v → nclose heapN ⊆ E →
-    heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
+    {{{ heap_ctx }}} Alloc e @ E {{{ l; 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σ] !>".
@@ -118,12 +118,12 @@ Section heap.
     iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
-  Lemma wp_load E l q v Φ :
+  Lemma wp_load E l q v :
     nclose heapN ⊆ E →
-    heap_ctx ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v)
-    ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E
+    {{{; 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.
@@ -131,12 +131,12 @@ Section heap.
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
-  Lemma wp_store E l v' e v Φ :
+  Lemma wp_store E l v' e v :
     to_val e = Some v → nclose heapN ⊆ E →
-    heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
-    ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E
+    {{{; 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.
@@ -147,12 +147,12 @@ Section heap.
     by iApply "HΦ".
   Qed.
 
-  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
+  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' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
-    ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+    {{{; 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|].
@@ -160,12 +160,12 @@ Section heap.
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
-  Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
+  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 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
-    ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+    {{{; 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.

heap_lang/lib/barrier/proof.v

@@ -91,11 +91,11 @@ Proof.
 Qed.
 
 (** Actual proofs *)
-Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
+Lemma newbarrier_spec (P : iProp Σ) :
   heapN ⊥ N →
-  heap_ctx ★ (∀ l, recv l P ★ send l P -★ Φ #l) ⊢ WP newbarrier #() {{ Φ }}.
+  {{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P ★ send l P }}}.
 Proof.
-  iIntros (HN) "[#? HΦ]".
+  iIntros (HN Φ) "[#? HΦ]".
   rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with ">[-]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
@@ -117,14 +117,15 @@ Proof.
   - auto.
 Qed.
 
-Lemma signal_spec l P (Φ : val → iProp Σ) :
-  send l P ★ P ★ Φ #() ⊢ WP signal #l {{ Φ }}.
+Lemma signal_spec l P :
+  {{{ send l P ★ P }}} signal #l {{{; #(), 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. iFrame "HΦ".
+  destruct p; [|done]. wp_store.
+  iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
   iMod ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
   iSplit; [iPureIntro; by eauto using signal_step|].
   iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
@@ -132,11 +133,11 @@ Proof.
   iNext. iIntros "_"; by iApply "Hr".
 Qed.
 
-Lemma wait_spec l P (Φ : val → iProp Σ) :
-  recv l P ★ (P -★ Φ #()) ⊢ WP wait #l {{ Φ }}.
+Lemma wait_spec l P:
+  {{{ recv l P }}} wait #l {{{ ; #(), 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.
@@ -146,7 +147,7 @@ Proof.
     iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     iModIntro. wp_if.
-    iApply ("IH" with "Hγ [HQR] HΦ"). auto.
+    iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
   - (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
     iDestruct "Hr" as (Ψ) "[HΨ Hsp]".

heap_lang/lib/barrier/specification.v

@@ -20,8 +20,9 @@ Proof.
   intros HN.
   exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
   split_and?; simpl.
-  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto.
-  - iIntros (l P) "!# [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
+  - 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 (l P Q) "!#". by iApply recv_split.
   - apply recv_weaken.

heap_lang/lib/counter.v

@@ -33,21 +33,21 @@ Section mono_proof.
   Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
   Proof. apply _. Qed.
 
-  Lemma newcounter_mono_spec (R : iProp Σ) Φ :
+  Lemma newcounter_mono_spec (R : iProp Σ) :
     heapN ⊥ N →
-    heap_ctx ★ (∀ l, mcounter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
+    {{{ heap_ctx }}} newcounter #() {{{ l; #l, mcounter l 0 }}}.
   Proof.
-    iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "[#Hh HΦ]". rewrite /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. }
     iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
   Qed.
 
-  Lemma inc_mono_spec l n (Φ : val → iProp Σ) :
-    mcounter l n ★ (mcounter l (S n) -★ Φ #()) ⊢ WP inc #l {{ Φ }}.
+  Lemma inc_mono_spec l n :
+    {{{ mcounter l n }}} inc #l {{{; #(), 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|].
@@ -65,22 +65,21 @@ Section mono_proof.
       by apply mnat_included, le_n_S.
     - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
       iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. iApply ("IH" with "[Hγf] HΦ").
+      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
   Qed.
 
-  Lemma read_mono_spec l j (Φ : val → iProp Σ) :
-    mcounter l j ★ (∀ i, ■ (j ≤ i)%nat → mcounter l i -★ Φ #i)
-    ⊢ WP read #l {{ Φ }}.
+  Lemma read_mono_spec l j :
+    {{{ mcounter l j }}} read #l {{{ i; #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.
     iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
     { apply auth_update, (mnat_local_update _ _ c); auto. }
     iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
-    iApply ("HΦ" with "[%]"); rewrite /mcounter; eauto 10.
+    iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
   Qed.
 End mono_proof.
 
@@ -110,12 +109,12 @@ Section contrib_spec.
     ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1★ ccounter γ q2 n2.
   Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed.
 
-  Lemma newcounter_contrib_spec (R : iProp Σ) Φ :
+  Lemma newcounter_contrib_spec (R : iProp Σ) :
     heapN ⊥ N →
-    heap_ctx ★ (∀ γ l, ccounter_ctx γ l ★ ccounter γ 1 0 -★ Φ #l)
-    ⊢ WP newcounter #() {{ Φ }}.
+    {{{ heap_ctx }}} newcounter #()
+    {{{ γ l; #l, ccounter_ctx γ l ★ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "[#Hh HΦ]". rewrite /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γ]").
@@ -123,11 +122,11 @@ Section contrib_spec.
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
   Qed.
 
-  Lemma inc_contrib_spec γ l q n (Φ : val → iProp Σ) :
-    ccounter_ctx γ l ★ ccounter γ q n ★ (ccounter γ q (S n) -★ Φ #())
-    ⊢ WP inc #l {{ Φ }}.
+  Lemma inc_contrib_spec γ l q n :
+    {{{ ccounter_ctx γ l ★ ccounter γ q n }}} inc #l
+    {{{; #(), 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.
@@ -141,27 +140,26 @@ Section contrib_spec.
       iModIntro. wp_if. by iApply "HΦ".
     - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
       iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
+      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
 
-  Lemma read_contrib_spec γ l q n (Φ : val → iProp Σ) :
-    ccounter_ctx γ l ★ ccounter γ q n ★
-      (∀ c, ■ (n ≤ c)%nat → ccounter γ q n -★ Φ #c)
-    ⊢ WP read #l {{ Φ }}.
+  Lemma read_contrib_spec γ l q n :
+    {{{ ccounter_ctx γ l ★ ccounter γ q n }}} read #l
+    {{{ c; #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.
     iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
-    iApply ("HΦ" with "[%]"); rewrite /ccounter; eauto 10.
+    iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
   Qed.
 
-  Lemma read_contrib_spec_1 γ l n (Φ : val → iProp Σ) :
-    ccounter_ctx γ l ★ ccounter γ 1 n ★ (ccounter γ 1 n -★ Φ #n)
-    ⊢ WP read #l {{ Φ }}.
+  Lemma read_contrib_spec_1 γ l n :
+    {{{ ccounter_ctx γ l ★ ccounter γ 1 n }}} read #l
+    {{{ n; #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.

heap_lang/lib/lock.v

@@ -16,13 +16,13 @@ Structure lock Σ `{!heapG Σ} := Lock {
   locked_timeless γ : TimelessP (locked γ);
   locked_exclusive γ : locked γ ★ locked γ ⊢ False;
   (* -- operation specs -- *)
-  newlock_spec N (R : iProp Σ) Φ :
+  newlock_spec N (R : iProp Σ) :
     heapN ⊥ N →
-    heap_ctx ★ R ★ (∀ l γ, is_lock N γ l R -★ Φ l) ⊢ WP newlock #() {{ Φ }};
-  acquire_spec N γ lk R (Φ : val → iProp Σ) :
-    is_lock N γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
-  release_spec N γ lk R (Φ : val → iProp Σ) :
-    is_lock N γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
+    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock N γ lk R }}};
+  acquire_spec N γ lk R :
+    {{{ is_lock N γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}};
+  release_spec N γ lk R :
+    {{{ is_lock N γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}
 }.
 
 Arguments newlock {_ _} _.

heap_lang/lib/par.v

@@ -19,15 +19,15 @@ Context `{!heapG Σ, !spawnG Σ}.
 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 }} ★
-   ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
+   ▷ ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP par e {{ Φ }}.
 Proof.
   iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
   rewrite /par. wp_value. iModIntro. wp_let. wp_proj.
   wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
-  iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
+  iNext. iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
-  wp_apply join_spec; iFrame "Hl". iIntros (w) "H1".
+  wp_apply join_spec; iFrame "Hl". iNext. iIntros (w) "H1".
   iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
 Qed.
 

heap_lang/lib/spawn.v

@@ -46,13 +46,12 @@ Global Instance join_handle_ne n l :
 Proof. solve_proper. Qed.
 
 (** The main proofs. *)
-Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
+Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   to_val e = Some f →
   heapN ⊥ N →
-  heap_ctx ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l)
-  ⊢ WP spawn e {{ Φ }}.
+  {{{ heap_ctx ★ WP f #() {{ Ψ }} }}} spawn e {{{ l; #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 "#?".
@@ -64,14 +63,14 @@ Proof.
     wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
 Qed.
 
-Lemma join_spec (Ψ : val → iProp Σ) l (Φ : val → iProp Σ) :
-  join_handle l Ψ ★ (∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
+Lemma join_spec (Ψ : val → iProp Σ) l :
+  {{{ join_handle l Ψ }}} join #l {{{ v; v, Ψ v }}}.
 Proof.
-  rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
+  rewrite /join_handle; iIntros (Φ) "[[% H] Hv]". 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").
+    iModIntro. wp_match. iApply ("IH" with "Hγ [Hv]"). auto.
   - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
     + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
       iModIntro. wp_match. by iApply "Hv".

heap_lang/lib/spin_lock.v

@@ -45,11 +45,11 @@ Section proof.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
 
-  Lemma newlock_spec (R : iProp Σ) Φ :
+  Lemma newlock_spec (R : iProp Σ):
     heapN ⊥ N →
-    heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
   Proof.
-    iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
+    iIntros (? Φ) "[[#Hh HR] HΦ]". rewrite /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 "#?".
@@ -70,22 +70,22 @@ Section proof.
       iModIntro. iDestruct "HΦ" as "[HΦ _]". rewrite /locked. by iApply ("HΦ" with "Hγ HR").
   Qed.
 
-  Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
-    is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
+  Lemma acquire_spec γ lk R :
+    {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
   Proof.
-    iIntros "[#Hl HΦ]". iLöb as "IH". wp_rec. wp_bind (try_acquire _).
+    iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec. wp_bind (try_acquire _).
     iApply try_acquire_spec. iFrame "#". iSplit.
-    - iIntros "Hlked HR". wp_if. iModIntro. iApply ("HΦ" with "Hlked HR").
-    - wp_if. iApply ("IH" with "HΦ").
+    - iIntros "Hlked HR". wp_if. iModIntro. iApply "HΦ"; iFrame.
+    - wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
 
-  Lemma release_spec γ lk R (Φ : val → iProp Σ) :
-    is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
+  Lemma release_spec γ lk R :
+    {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), 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. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
+    wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
   Qed.
 
 End proof.

heap_lang/lib/ticket_lock.v

@@ -74,11 +74,11 @@ Section proof.
     iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _].
   Qed.
 
-  Lemma newlock_spec (R : iProp Σ) Φ :
+  Lemma newlock_spec (R : iProp Σ) :
     heapN ⊥ N →
-    heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
   Proof.
-    iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock /=.
+    iIntros (HN Φ) "((#Hh & HR) & HΦ)". rewrite /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,7 +89,7 @@ Section proof.
   Qed.
 
   Lemma wait_loop_spec γ lk x R (Φ : val → iProp Σ) :
-    issued γ lk x R ★ (locked γ -★ R -★ Φ #()) ⊢ WP wait_loop #x lk {{ Φ }}.
+    issued γ lk x R ★ (locked γ ★ R -★ Φ #()) ⊢ WP wait_loop #x lk {{ Φ }}.
   Proof.
     iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
@@ -100,7 +100,7 @@ Section proof.
         { iNext. iExists o, n. iFrame. eauto. }
         iModIntro. wp_let. wp_op=>[_|[]] //.
         wp_if. iModIntro.
-        iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto.
+        iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
         set_solver.
     - iMod ("Hclose" with "[Hlo Hln Ha]").
@@ -109,10 +109,10 @@ Section proof.
       wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
   Qed.
 
-  Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
-    is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
+  Lemma acquire_spec γ lk R :
+    {{{ is_lock γ lk R }}} acquire lk {{{; #(), 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 "_".
@@ -136,13 +136,13 @@ Section proof.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
       { iNext. iExists o', n'. by iFrame. }
-      iModIntro. wp_if. by iApply "IH".
+      iModIntro. wp_if. by iApply "IH"; auto.
   Qed.
 
-  Lemma release_spec γ lk R (Φ : val → iProp Σ):
-    is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
+  Lemma release_spec γ lk R :
+    {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), 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.
@@ -162,7 +162,7 @@ Section proof.
     iMod (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]".
     { apply auth_update, prod_local_update_1.
       by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
-    iMod ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
+    iMod ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last by iApply "HΦ".
     iNext. iExists (S o), n'.
     rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
   Qed.

heap_lang/proofmode.v

@@ -25,7 +25,7 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
     (Δ'' ⊢ |={E}=> Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
+  intros ???? HΔ. rewrite -wp_fupd -wp_alloc // -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.
@@ -39,7 +39,8 @@ Lemma tac_wp_load Δ Δ' E i l q v Φ :
   (Δ' ⊢ |={E}=> Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
+  intros. rewrite -wp_fupd -wp_load // -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.
 Qed.
@@ -53,7 +54,8 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
   Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
+  intros. rewrite -wp_fupd -wp_store // -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.
 Qed.
@@ -66,7 +68,8 @@ Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   (Δ' ⊢ |={E}=> Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
+  intros. rewrite -wp_fupd -wp_cas_fail // -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.
 Qed.
@@ -80,8 +83,8 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
   (Δ'' ⊢ |={E}=> Φ (LitV (LitBool true))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros; subst.
-  rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
+  intros; subst. rewrite -wp_fupd -wp_cas_suc // -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.
 Qed.

program_logic/weakestpre.v

@@ -50,6 +50,45 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
+(* Texan triples *)
+Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+  (□ ∀ Φ,
+      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 } } }" :=
+  (□ ∀ Φ,
+      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
+    (at level 20,
+     format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
+  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : uPred_scope.
+
+Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+  (∀ Φ : _ → uPred _,
+      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 } } }" :=
+  (∀ Φ : _ → uPred _,
+      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 {{ Φ }})
+    (at level 20,
+     format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
+  (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e @ E {{ Φ }})
+    (at level 20,
+     format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : C_scope.
+
 Section wp.
 Context `{irisG Λ Σ}.
 Implicit Types P : iProp Σ.

tests/barrier_client.v

@@ -30,7 +30,7 @@ Section client.
   Proof.
     iIntros "[#Hh Hrecv]". wp_lam. wp_let.
     wp_apply wait_spec; iFrame "Hrecv".
-    iDestruct 1 as (f) "[Hy #Hf]".
+    iNext. iDestruct 1 as (f) "[Hy #Hf]".
     wp_seq. wp_load.
     iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"].
   Qed.
@@ -39,11 +39,11 @@ Section client.
   Proof.
     iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
     wp_apply (newbarrier_spec N (y_inv 1 y)); first done.
-    iFrame "Hh". iIntros (l) "[Hr Hs]". wp_let.
+    iFrame "Hh". iNext. iIntros (l) "[Hr Hs]". wp_let.
     iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
     iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
+      wp_store. iApply signal_spec; iFrame "Hs"; iSplitL "Hy"; [|by eauto].
       iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros (_ _) "_ !>"].

tests/joining_existentials.v

@@ -36,7 +36,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
   ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
   iIntros "[Hl #He]". wp_apply wait_spec; simpl; iFrame "Hl".
-  iDestruct 1 as (x) "[#Hγ Hx]".
+  iNext. iDestruct 1 as (x) "[#Hγ Hx]".
   wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
   iIntros (v) "?"; iExists x; by iSplit.
 Qed.
@@ -77,7 +77,7 @@ 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 γ Φ)); auto.
-  iFrame "Hh". iIntros (l) "[Hr Hs]".
+  iFrame "Hh". iNext. 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); iFrame "Hh".
   iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
@@ -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; iFrame "Hs"; iSplit; last done.
+    iApply signal_spec; iFrame "Hs"; iSplitR ""; 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.