wp_pures.

tests/heap_lang.ref

@@ -50,6 +50,8 @@
   --------------------------------------∗
   True
   
+"wp_nonclosed_value"
+     : string
 The command has indeed failed with message:
 Ltac call to "wp_pure (open_constr)" failed.
 Tactic failure: wp_pure: cannot find ?y in (Var "x") or 
@@ -116,4 +118,4 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
      : string
 The command has indeed failed with message:
 Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: cannot find 'CAS' in (Val #()).
+Tactic failure: wp_cas_suc: not a 'wp'.

tests/heap_lang.v

@@ -27,8 +27,8 @@ Section tests.
   Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
   Proof.
     iIntros "". rewrite /heap_e. Show.
-    wp_alloc l as "?". wp_let. wp_load. Show.
-    wp_op. wp_store. by wp_load.
+    wp_alloc l as "?". wp_load. Show.
+    wp_store. by wp_load.
   Qed.
 
   Definition heap_e2 : expr :=
@@ -39,8 +39,8 @@ Section tests.
   Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, ⌜v = #2⌝ }]%I.
   Proof.
     iIntros "". rewrite /heap_e2.
-    wp_alloc l as "Hl". Show. wp_let. wp_alloc l'. wp_let.
-    wp_load. wp_op. wp_store. wp_load. done.
+    wp_alloc l as "Hl". Show. wp_alloc l'.
+    wp_load. wp_store. wp_load. done.
   Qed.
 
   Definition heap_e3 : expr :=
@@ -60,8 +60,8 @@ Section tests.
 
   Lemma heap_e4_spec : WP heap_e4 [{ v, ⌜ v = #1 ⌝ }]%I.
   Proof.
-    rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
-    wp_alloc l''. wp_let. by repeat wp_load.
+    rewrite /heap_e4. wp_alloc l. wp_alloc l'.
+    wp_alloc l''. by repeat wp_load.
   Qed.
 
   Definition heap_e5 : expr :=
@@ -69,8 +69,8 @@ Section tests.
 
   Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, ⌜v = #13⌝ }]%I.
   Proof.
-    rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
-    wp_op. wp_load. wp_faa. do 2 wp_load. wp_op. done.
+    rewrite /heap_e5. wp_alloc l. wp_alloc l'.
+    wp_load. wp_faa. do 2 wp_load. by wp_pures.
   Qed.
 
   Definition heap_e6 : val := λ: "v", "v" = "v".
@@ -92,8 +92,7 @@ Section tests.
   Proof.
     iIntros (Hn) "HΦ".
     iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
-    wp_rec. wp_let. wp_op. wp_let.
-    wp_op; case_bool_decide; wp_if.
+    wp_rec. wp_pures. case_bool_decide; wp_if.
     - iApply ("IH" with "[%] [%] HΦ"); omega.
     - by assert (n1' = n2 - 1) as -> by omega.
   Qed.
@@ -101,16 +100,15 @@ Section tests.
   Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
   Proof.
     iIntros "HΦ". wp_lam.
-    wp_op. case_bool_decide; wp_if.
-    - wp_op. wp_op.
-      wp_apply FindPred_spec; first omega.
-      wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
+    wp_op. case_bool_decide.
+    - wp_apply FindPred_spec; first omega. wp_pures.
+      by replace (n - 1) with (- (-n + 2 - 1)) by omega.
     - wp_apply FindPred_spec; eauto with omega.
   Qed.
 
   Lemma Pred_user E :
     WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]%I.
-  Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
+  Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
 
   Lemma wp_apply_evar e P :
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
@@ -131,6 +129,7 @@ Section tests.
     WP Alloc #0 {{ _, True }}%I.
   Proof. wp_alloc l as "_". Show. done. Qed.
 
+  Check "wp_nonclosed_value".
   Lemma wp_nonclosed_value :
     WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
   Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.

tests/ipm_paper.v

@@ -82,7 +82,7 @@ Section list_reverse.
     destruct xs as [|x xs]; iSimplifyEq.
     - (* nil *) by wp_match.
     - (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
-      wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_pair. wp_store.
+      wp_match. wp_load. wp_load. wp_store.
       rewrite reverse_cons -assoc.
       iApply ("IH" $! hd' (InjRV #l) xs (x :: ys) with "Hxs [Hx Hys]").
       iExists l, acc; by iFrame.

tests/list_reverse.v

@@ -36,7 +36,7 @@ Proof.
     iSimplifyEq; wp_rec; wp_let.
   - Show. wp_match. by iApply "HΦ".
   - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
-    wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_pair. wp_store.
+    wp_load. wp_load. wp_store.
     iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
     { iExists l, acc; by iFrame. }
     iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".

tests/one_shot.v

@@ -43,12 +43,12 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
-  rewrite -wp_fupd /one_shot_example /=. wp_lam. wp_inj. wp_alloc l as "Hl". wp_let.
+  rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
   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". }
-  wp_closure. wp_closure. wp_pair. iModIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!#". wp_lam. wp_inj. wp_inj.
+  wp_pures. iModIntro. iApply "Hf"; iSplit.
+  - iIntros (n) "!#". wp_lam. wp_pures.
     iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
@@ -70,18 +70,17 @@ Proof.
       + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iSplitL "Hinv"; first by eauto.
-    iModIntro. wp_let. wp_closure. iIntros "!#". wp_lam.
-    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
-    { by wp_match. }
-    wp_match. wp_bind (! _)%E.
+    iModIntro. wp_pures. iIntros "!#". wp_lam.
+    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
+      subst; wp_match; [done|].
+    wp_bind (! _)%E.
     iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
     { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
     wp_load. Show.
     iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
     iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
-    wp_match. iApply wp_assert.
-    wp_op. by case_bool_decide.
+    wp_apply wp_assert. wp_pures. by case_bool_decide.
 Qed.
 
 Lemma ht_one_shot (Φ : val → iProp Σ) :
@@ -92,8 +91,7 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
     }}.
 Proof.
   iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
-  - iIntros (n) "!# _". wp_proj. iApply "Hf1".
-  - iIntros "!# _". wp_proj.
-    iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
+  - iIntros (n) "!# _". wp_apply "Hf1".
+  - iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
 Qed.
 End proof.

tests/tree_sum.v

@@ -42,13 +42,11 @@ Proof.
   iIntros (Φ) "[Hl Ht] HΦ".
   iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
   - iDestruct "Ht" as "%"; subst.
-    wp_match. wp_load. wp_op. wp_store.
+    wp_load. wp_store.
     by iApply ("HΦ" with "[$Hl]").
   - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
-    wp_match. wp_proj. wp_load.
-    wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
-    wp_seq. wp_proj. wp_load.
-    wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
+    wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
+    wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
     iApply "HΦ". iSplitL "Hl".
     { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
     iExists ll, lr, vl, vr. by iFrame.
@@ -58,8 +56,8 @@ Lemma sum_wp `{!heapG Σ} v t :
   [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
 Proof.
   iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
-  wp_lam. wp_alloc l as "Hl". wp_let.
+  wp_lam. wp_alloc l as "Hl".
   wp_apply (sum_loop_wp with "[$Hl $Ht]").
   rewrite Z.add_0_r.
-  iIntros "[Hl Ht]". wp_seq. wp_load. by iApply "HΦ".
+  iIntros "[Hl Ht]". wp_load. by iApply "HΦ".
 Qed.

theories/heap_lang/lib/assert.v

@@ -10,15 +10,17 @@ Definition assert : val :=
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
 Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
-  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗ WP assert: e @ E [{ Φ }].
+  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
+  WP assert (LamV BAnon e)%V @ E [{ Φ }].
 Proof.
-  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
+  iIntros "HΦ". wp_lam.
   wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
 
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
-  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
+  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
+  WP assert (LamV BAnon e)%V @ E {{ Φ }}.
 Proof.
-  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
+  iIntros "HΦ". wp_lam.
   wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.

theories/heap_lang/lib/coin_flip.v

@@ -36,11 +36,11 @@ Section coinflip.
   Lemma rand_spec :
     {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
   Proof.
-    iIntros (Φ) "_ HP". wp_lam. wp_alloc l as "Hl". wp_let.
+    iIntros (Φ) "_ HP". wp_lam. wp_alloc l as "Hl".
     iMod (inv_alloc N _ (∃ (b: bool), l ↦ #b)%I with "[Hl]") as "#Hinv"; first by eauto.
     wp_apply wp_fork.
     - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
-    - wp_seq. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
+    - wp_pures. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
       iApply "HP". done.
   Qed.
 
@@ -82,8 +82,8 @@ Section coinflip.
     iDestruct "Hl" as (v') "Hl".
     wp_store.
     iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
-    iModIntro. wp_seq. wp_apply rand_spec; try done.
-    iIntros (b') "_". wp_let.
+    iModIntro. wp_apply rand_spec; try done.
+    iIntros (b') "_".
     wp_apply (wp_resolve_proph with "Hp").
     iIntros (->). wp_seq. done.
   Qed.

theories/heap_lang/lib/counter.v

@@ -49,7 +49,7 @@ Section mono_proof.
     iDestruct "Hl" as (γ) "[#? Hγf]".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_let. wp_op.
+    wp_pures.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
@@ -126,7 +126,7 @@ Section contrib_spec.
     iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_let. wp_op.
+    wp_pures.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".

theories/heap_lang/lib/increment.v

@@ -30,7 +30,7 @@ Section increment.
     iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
     iIntros "$ !> AU !> _".
     (* Now go on *)
-    wp_let. wp_op. wp_apply cas_spec; [done|iAccu|].
+    wp_apply cas_spec; [done|iAccu|].
     (* Prove the atomic update for CAS *)
     iAuIntro. iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
@@ -58,8 +58,7 @@ Section increment.
   Proof.
     iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
     wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
-    iIntros "Hl". wp_let. wp_op.
-    wp_apply store_spec; first by iAccu.
+    iIntros "Hl". wp_apply store_spec; first by iAccu.
     (* Prove the atomic update for store *)
     iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
     iIntros (x) "H↦".
@@ -85,7 +84,7 @@ Section increment_client.
   Lemma incr_client_safe (x: Z):
     WP incr_client #x {{ _, True }}%I.
   Proof using Type*.
-    wp_lam. wp_alloc l as "Hl". wp_let.
+    wp_lam. wp_alloc l as "Hl".
     iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
     (* FIXME: I am only using persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional □. *)
@@ -96,7 +95,7 @@ Section increment_client.
       (* The continuation: From after the atomic triple to the postcondition of the WP *)
       done.
     }
-    wp_apply wp_par.
+    wp_apply par_spec; wp_pures.
     - iAssumption.
     - iAssumption.
     - iIntros (??) "_ !>". done.

theories/heap_lang/lib/par.v

@@ -26,13 +26,12 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) (f1 f2 : val) (Φ : val → iProp Σ
   (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP par f1 f2 {{ Φ }}.
 Proof.
-  iIntros "Hf1 Hf2 HΦ".
-  rewrite /par /=. wp_lam. wp_let.
+  iIntros "Hf1 Hf2 HΦ". wp_lam. wp_let.
   wp_apply (spawn_spec parN with "Hf1").
   iIntros (l) "Hl". wp_let. wp_bind (f2 _).
   wp_apply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
   wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
-  iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". wp_let. by wp_pair.
+  iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". by wp_pures.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
@@ -40,7 +39,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ)
   (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP e1 ||| e2 {{ Φ }}.
 Proof.
-  iIntros "H1 H2 H". do 2 wp_closure.
-  iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
+  iIntros "H1 H2 H".
+  wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
 Qed.
 End proof.

theories/heap_lang/lib/spawn.v

@@ -48,8 +48,8 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   IntoVal e f →
   {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
-  wp_lam. wp_inj. wp_alloc l as "Hl". wp_let.
+  iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=. wp_lam.
+  wp_alloc l as "Hl".
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
   { iNext. iExists NONEV. iFrame; eauto. }
@@ -57,7 +57,7 @@ Proof.
   - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
     wp_inj. iInv N as (v') "[Hl _]".
     wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
-  - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
+  - wp_pures. iApply "HΦ". rewrite /join_handle. eauto.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp Σ) l :
@@ -67,10 +67,10 @@ Proof.
   iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
-    wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
+    wp_apply ("IH" with "Hγ [HΦ]"). auto.
   - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
     + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
-      wp_match. by iApply "HΦ".
+      wp_pures. by iApply "HΦ".
     + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
 Qed.
 End proof.

theories/heap_lang/lib/ticket_lock.v

@@ -73,33 +73,33 @@ Section proof.
   Lemma newlock_spec (R : iProp Σ) :
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=. repeat wp_proj.
-    wp_lam. wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
+    wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
       iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
-    wp_pair. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
+    wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
   Lemma wait_loop_spec γ lk x R :
     {{{ is_lock γ lk R ∗ issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
   Proof.
     iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
-    iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
+    iLöb as "IH". wp_rec. subst. wp_pures. wp_bind (! _)%E.
     iInv N as (o n) "(Hlo & Hln & Ha)".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
     - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
       + iModIntro. iSplitL "Hlo Hln Hainv Ht".
         { iNext. iExists o, n. iFrame. }
-        wp_let. wp_op. case_bool_decide; [|done]. wp_if.
+        wp_pures. case_bool_decide; [|done]. wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
     - iModIntro. iSplitL "Hlo Hln Ha".
       { iNext. iExists o, n. by iFrame. }
-      wp_let. wp_op. case_bool_decide; [simplify_eq |].
+      wp_pures. case_bool_decide; [simplify_eq |].
       wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
   Qed.
 
@@ -111,7 +111,7 @@ Section proof.
     iInv N as (o n) "[Hlo [Hln Ha]]".
     wp_load. iModIntro. iSplitL "Hlo Hln Ha".
     { iNext. iExists o, n. by iFrame. }
-    wp_let. wp_op. wp_proj. wp_bind (CAS _ _ _).
+    wp_pures. wp_bind (CAS _ _ _).
     iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
     - iMod (own_update with "Hauth") as "[Hauth Hofull]".
@@ -144,7 +144,7 @@ Section proof.
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
     iModIntro. iSplitL "Hlo Hln Hauth Haown".
     { iNext. iExists o, n. by iFrame. }
-    wp_op. wp_proj.
+    wp_pures.
     iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
     iApply wp_fupd. wp_store.
     iDestruct (own_valid_2 with "Hauth Hγo") as

theories/heap_lang/lifting.v

@@ -93,7 +93,13 @@ Local Ltac solve_pure_exec :=
 Class AsRecV (v : val) (f x : binder) (erec : expr) :=
   as_recv : v = RecV f x erec.
 Instance AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
-Instance AsRecV_recv_locked v f x e :
+
+(* Pure reductions are automatically performed before any wp_ tactics
+   handling impure operations. Since we do not want these tactics to
+   unfold locked terms, we do not register this instance explicitely,
+   but only activate it by hand in the `wp_rec` tactic, where we
+   *actually* want it to unlock. *)
+Lemma AsRecV_recv_locked v f x e :
   AsRecV v f x e → AsRecV (locked v) f x e.
 Proof. by unlock. Qed.
 

theories/heap_lang/metatheory.v

@@ -88,31 +88,16 @@ Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
 (* The stepping relation preserves closedness *)
 Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
   is_closed_expr [] e1 →
-  (∀ x v, σ1.(heap) !! x = Some v → is_closed_val v) →
+  map_Forall (λ _ v, is_closed_val v) σ1.(heap) →
   head_step e1 σ1 obs e2 σ2 es →
 
   is_closed_expr [] e2 ∧ Forall (is_closed_expr []) es ∧
-  (∀ x v, σ2.(heap) !! x = Some v → is_closed_val v).
+  map_Forall (λ _ v, is_closed_val v) σ2.(heap).
 Proof.
   intros Cl1 Clσ1 STEP.
-  destruct STEP; simpl in *; split_and!; try by naive_solver.
+  destruct STEP; simpl in *; split_and!;
+    try apply map_Forall_insert_2; try by naive_solver.
   - subst. repeat apply is_closed_subst'; naive_solver.
   - unfold un_op_eval in *. repeat case_match; naive_solver.
   - unfold bin_op_eval, bin_op_eval_bool in *. repeat case_match; naive_solver.
-  - intros ??.
-    match goal with
-    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
-    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
-  - intros ??.
-    match goal with
-    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
-    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
-  - intros ??.
-    match goal with
-    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
-    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
-  - intros ??.
-    match goal with
-    | |- context [<[?l1 := _]>_!! ?l2] => destruct (decide (l1 = l2)) as [->|]
-    end; rewrite ?lookup_insert ?lookup_insert_ne; naive_solver.
 Qed.

theories/heap_lang/proofmode.v

@@ -85,13 +85,29 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
+(* The `;[]` makes sure that no side-condition magically spawns. *)
+Ltac wp_pures := repeat (wp_pure _; []).
+
+(* The handling of beta-reductions with wp_rec needs special care in
+  order to allow it to unlock locked `RecV` values: We first put
+  `AsRecV_recv_locked` in the current environment so that it can be
+  used as an instance by the typeclass resolution system, then we
+  perform the reduction, and finally we clear this new hypothesis.
+
+  The reason is that we do not want impure wp_ tactics to unfold
+  locked terms, while we want them to execute arbitrary pure steps. *)
+Tactic Notation "wp_rec" :=
+  let H := fresh in
+  assert (H := AsRecV_recv_locked);
+  wp_pure (App _ _);
+  clear H.
+
 Tactic Notation "wp_if" := wp_pure (If _ _ _).
 Tactic Notation "wp_if_true" := wp_pure (If (LitV (LitBool true)) _ _).
 Tactic Notation "wp_if_false" := wp_pure (If (LitV (LitBool false)) _ _).
 Tactic Notation "wp_unop" := wp_pure (UnOp _ _).
 Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _).
 Tactic Notation "wp_op" := wp_unop || wp_binop.
-Tactic Notation "wp_rec" := wp_pure (App _ _).
 Tactic Notation "wp_lam" := wp_rec.
 Tactic Notation "wp_let" := wp_pure (Rec BAnon (BNamed _) _); wp_lam.
 Tactic Notation "wp_seq" := wp_pure (Rec BAnon BAnon _); wp_lam.
@@ -330,6 +346,7 @@ Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
+  wp_pures;
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -354,7 +371,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
       eexists; split;
         [pm_reflexivity || fail "wp_alloc:" H "not fresh"
         |iDestructHyp Htmp as H; wp_expr_simpl; try wp_value_head] in
-  iStartProof;
+  wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
@@ -377,7 +394,7 @@ Tactic Notation "wp_load" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
     iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
-  iStartProof;
+  wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
@@ -401,7 +418,7 @@ Tactic Notation "wp_store" :=
     iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
   let finish _ :=
     wp_expr_simpl; try first [wp_seq|wp_value_head] in
-  iStartProof;
+  wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
@@ -425,7 +442,7 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
     iAssumptionCore || fail "wp_cas: cannot find" l "↦ ?" in
-  iStartProof;
+  wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>