diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index cbc8d7cc1a406dac24be2cb44f8dd0bfcfb00e52..04d36e80abf6b87c5db6d6f00297bcbedffc71a3 100644
--- a/heap_lang/lib/counter.v
+++ b/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|].
@@ -69,18 +69,17 @@ Section mono_proof.
       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.
@@ -144,24 +143,23 @@ Section contrib_spec.
       iModIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
   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.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 0b764bb1ae480cc818132982ccc78cfc95589d17..42bc6a572dcdb160d017b0476184733b4f147a94 100644
--- a/heap_lang/lib/lock.v
+++ b/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 {_ _} _.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 435ed807349bc4d15ddffaff2d00c5506fec3195..fc9b2acf10174d6d883300846146bcde9971ba97 100644
--- a/heap_lang/lib/spawn.v
+++ b/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,10 +63,10 @@ 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|].
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 21bedd2cdbd5058324e8831e4f368f64d6f576b3..7d402e8615157ae11dec4b8e8f393a6736cc333d 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/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").
+    - iIntros "Hlked HR". wp_if. iModIntro. iApply "HΦ"; iFrame.
     - wp_if. iApply ("IH" with "HΦ").
   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.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 6bda146dae67c747dcee2990f58a0e866e7c6aae..1d68f5ec0a242977468e4ef69c12379a362a8f3e 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/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 "_".
@@ -139,10 +139,10 @@ Section proof.
       iModIntro. wp_if. by iApply "IH".
   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.