Merge branch 'pureexec' into 'master'

Common tactic machinery for symbolic execution of pure reductions

See merge request FP/iris-coq!64

theories/heap_lang/lang.v

-From iris.program_logic Require Export ectx_language ectxi_language.
+From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
 From stdpp Require Export strings.
 From stdpp Require Import gmap.
@@ -109,6 +109,14 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 
+Class AsRec (e : expr) (f x : binder) (erec : expr) :=
+  as_rec : e = Rec f x erec.
+
+Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
+Instance AsRec_rec_locked_val v f x e :
+  AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
+Proof. by unlock. Qed.
+
 (** The state: heaps of vals. *)
 Definition state := gmap loc val.
 
@@ -411,6 +419,9 @@ Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
 Lemma is_closed_of_val X v : is_closed X (of_val v).
 Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
+Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
+Proof. intros Hev; rewrite -(of_to_val e v Hev); apply is_closed_of_val. Qed.
+
 Lemma is_closed_subst X e x es :
   is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
 Proof.

theories/heap_lang/lib/assert.v

@@ -13,5 +13,5 @@ Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
-  iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
+  wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.

theories/heap_lang/lib/par.v

@@ -21,15 +21,15 @@ Context `{!heapG Σ, !spawnG Σ}.
    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 →
+Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ)
+    `{Hef : !IntoVal e (f1,f2)} :
   WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
   (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP par e {{ Φ }}.
 Proof.
-  iIntros (?) "Hf1 Hf2 HΦ".
-  rewrite /par. wp_value. wp_let. wp_proj.
-  wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
+  apply of_to_val in Hef as <-. iIntros "Hf1 Hf2 HΦ".
+  rewrite /par /=. wp_let. wp_proj.
+  wp_apply (spawn_spec parN with "Hf1").
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
   wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
@@ -42,7 +42,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
   (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP e1 ||| e2 {{ Φ }}.
 Proof.
-  iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); try wp_done.
+  iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]").
   by wp_let. by wp_let. auto.
 Qed.
 End proof.

theories/heap_lang/lib/spawn.v

@@ -44,11 +44,10 @@ Global Instance join_handle_ne n l :
 Proof. solve_proper. Qed.
 
 (** The main proofs. *)
-Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
-  to_val e = Some f →
+Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) `{Hef : !IntoVal e f} :
   {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=.
+  apply of_to_val in Hef as <-. iIntros (Φ) "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 "#?".

theories/heap_lang/lib/ticket_lock.v

@@ -93,14 +93,15 @@ Section proof.
     - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
       + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
         { iNext. iExists o, n. iFrame. eauto. }
-        iModIntro. wp_let. wp_op=>[_|[]] //.
+        iModIntro. wp_let. wp_op. 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.
     - iMod ("Hclose" with "[Hlo Hln Ha]").
       { iNext. iExists o, n. by iFrame. }
-      iModIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
+      iModIntro. wp_let.
+      wp_op. case_bool_decide; [simplify_eq |].
       wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
   Qed.
 

theories/heap_lang/lifting.v

 From iris.base_logic Require Export gen_heap.
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre lifting.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
@@ -80,86 +80,52 @@ Proof.
   - intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_rec E f x erec e1 e2 Φ :
-  e1 = Rec f x erec →
-  is_Some (to_val e2) →
-  Closed (f :b: x :b: []) erec →
-  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof.
-  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork' (App _ _)
-    (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
+Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
+Local Ltac solve_pureexec :=
+  repeat lazymatch goal with
+  | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
+  | H: AsRec _ _ _ _ |- _ => rewrite H; clear H
+  end;
+  apply hoist_pred_pureexec; intros; destruct_and?;
+  apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
 
-Lemma wp_un_op E op e v v' Φ :
-  to_val e = Some v →
-  un_op_eval op v = Some v' →
-  ▷ Φ v' ⊢ WP UnOp op e @ E {{ Φ }}.
-Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step_no_fork' (UnOp op _) (of_val v'))
-    -?wp_value'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val)
+    `{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
+  PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
+Proof. solve_pureexec. 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' →
-  ▷ (Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step_no_fork' (BinOp op _ _) (of_val v'))
-    -?wp_value'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_unop op e v v' `{!IntoVal e v} :
+  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
+Proof. solve_pureexec. Qed.
 
-Lemma wp_if_true E e1 e2 Φ :
-  ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
-Proof.
-  apply wp_lift_pure_det_head_step_no_fork'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
+  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
+Proof. solve_pureexec. Qed.
 
-Lemma wp_if_false E e1 e2 Φ :
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
-Proof.
-  apply wp_lift_pure_det_head_step_no_fork'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_if_true e1 e2 :
+  PureExec True (If (Lit (LitBool true)) e1 e2) e1.
+Proof. solve_pureexec. Qed.
 
-Lemma wp_fst E e1 v1 e2 Φ :
-  to_val e1 = Some v1 → is_Some (to_val e2) →
-  ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
-Proof.
-  intros ? [v2 ?].
-  rewrite -(wp_lift_pure_det_head_step_no_fork' (Fst _) e1) -?wp_value; eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_if_false e1 e2 :
+  PureExec True (If (Lit (LitBool false)) e1 e2) e2.
+Proof. solve_pureexec. Qed.
 
-Lemma wp_snd E e1 e2 v2 Φ :
-  is_Some (to_val e1) → to_val e2 = Some v2 →
-  ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
-Proof.
-  intros [v1 ?] ?.
-  rewrite -(wp_lift_pure_det_head_step_no_fork' (Snd _) e2) -?wp_value; eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+  PureExec True (Fst (Pair e1 e2)) e1.
+Proof. solve_pureexec. Qed.
 
-Lemma wp_case_inl E e0 e1 e2 Φ :
-  is_Some (to_val e0) →
-  ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
-Proof.
-  intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step_no_fork' (Case _ _ _) (App e1 e0)); eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+  PureExec True (Snd (Pair e1 e2)) e2.
+Proof. solve_pureexec. Qed.
 
-Lemma wp_case_inr E e0 e1 e2 Φ :
-  is_Some (to_val e0) →
-  ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
-Proof.
-  intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step_no_fork' (Case _ _ _) (App e2 e0)); eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
+  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
+  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
+Proof. solve_pureexec. Qed.
 
 (** Heap *)
 Lemma wp_alloc E e v :
@@ -221,22 +187,10 @@ Proof.
 Qed.
 
 (** Proof rules for derived constructs *)
-Lemma wp_lam E x elam e1 e2 Φ :
-  e1 = Lam x elam →
-  is_Some (to_val e2) →
-  Closed (x :b: []) elam →
-  ▷ WP subst' x e2 elam @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
-
-Lemma wp_let E x e1 e2 Φ :
-  is_Some (to_val e1) → Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. by apply wp_lam. Qed.
-
 Lemma wp_seq E e1 e2 Φ :
   is_Some (to_val e1) → Closed [] e2 →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. intros ??. by rewrite -wp_let. Qed.
+Proof. iIntros ([? ?] ?). rewrite -wp_pure_step_later; by eauto. Qed.
 
 Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
 Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
@@ -244,38 +198,10 @@ Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
 Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
   is_Some (to_val e0) → Closed (x1 :b: []) e1 →
   ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
+Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
 
 Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
   is_Some (to_val e0) → Closed (x2 :b: []) e2 →
   ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-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 ⊢ ▷ Φ (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 //; [].
-  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
-Qed.
-
-Lemma wp_lt E (n1 n2 : Z) P Φ :
-  (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 //; [].
-  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
-Qed.
-
-Lemma wp_eq E e1 e2 v1 v2 P Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (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 //; [].
-  destruct (bool_decide_reflect (v1 = v2)); by eauto.
-Qed.
+Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
 End lifting.

theories/heap_lang/proofmode.v

@@ -5,136 +5,52 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-(** wp-specific helper tactics *)
-Ltac wp_bind_core K :=
-  lazymatch eval hnf in K with
-  | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
-  end.
-
-(* Solves side-conditions generated by the wp tactics *)
-Ltac wp_done :=
-  match goal with
-  | |- Closed _ _ => solve_closed
-  | |- is_Some (to_val _) => solve_to_val
-  | |- to_val _ = Some _ => solve_to_val
-  | |- language.to_val _ = Some _ => solve_to_val
-  | _ => fast_done
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; simpl.
-
-Ltac wp_seq_head :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-    etrans; [|eapply wp_seq; wp_done]; iNext
-  end.
-
-Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val;
-  try iNext;
-  repeat lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-     etrans; [|eapply wp_seq; wp_done]; iNext
-  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
-  end).
-
-Tactic Notation "wp_value" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
-  | _ => fail "wp_value: not a wp"
-  end.
-
-Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
-Proof. by unlock. Qed.
-
-(* Applied to goals that are equalities of expressions. Will try to unlock the
-   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
-Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
+Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
+  PureExec φ e1 e2 →
+  φ →
+  IntoLaterNEnvs 1 Δ Δ' →
+  (Δ' ⊢ WP fill K e2 @ E {{ Φ }}) →
+  (Δ ⊢ WP fill K e1 @ E {{ Φ }}).
+Proof.
+  intros ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
+  by rewrite -ectx_lifting.wp_ectx_bind_inv.
+Qed.
 
-Tactic Notation "wp_rec" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with App ?e1 _ =>
-(* hnf does not reduce through an of_val *)
-(*      match eval hnf in e1 with Rec _ _ _ => *)
-    wp_bind_core K; etrans;
-      [|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
-(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
-  | _ => fail "wp_rec: not a 'wp'"
-  end.
+Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
 
-Tactic Notation "wp_lam" :=
+Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with App ?e1 _ =>
-(*    match eval hnf in e1 with Rec BAnon _ _ => *)
-    wp_bind_core K; etrans;
-      [|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
-(*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
-  | _ => fail "wp_lam: not a 'wp'"
-  end.
-
+    unify e' efoc;
+    eapply (tac_wp_pure K);
+    [simpl; apply _                 (* PureExec *)
+    |try fast_done                  (* The pure condition for PureExec *)
+    |apply _                        (* IntoLaters *)
+    |simpl_subst; try wp_value_head (* new goal *)])
+   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+
+Tactic Notation "wp_if" := wp_pure (If _ _ _).
+Tactic Notation "wp_if_true" := wp_pure (If (Lit (LitBool true)) _ _).
+Tactic Notation "wp_if_false" := wp_pure (If (Lit (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_lam.
-Tactic Notation "wp_seq" := wp_let.
-
-Tactic Notation "wp_op" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    lazymatch eval hnf in e' with
-    | BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
-    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
-    | BinOp EqOp _ _ =>
-       wp_bind_core K; eapply wp_eq; [wp_done|wp_done|wp_finish|wp_finish]
-    | BinOp _ _ _ =>
-       wp_bind_core K; etrans;
-         [|eapply wp_bin_op; [wp_done|wp_done|try fast_done]]; wp_finish
-    | UnOp _ _ =>
-       wp_bind_core K; etrans;
-         [|eapply wp_un_op; [wp_done|try fast_done]]; wp_finish
-    end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
-  | _ => fail "wp_op: not a 'wp'"
-  end.
+Tactic Notation "wp_seq" := wp_lam.
+Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
+Tactic Notation "wp_case" := wp_pure (Case _ _ _).
+Tactic Notation "wp_match" := wp_case; wp_let.
 
-Tactic Notation "wp_proj" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
-    | Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
-    end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
-  | _ => fail "wp_proj: not a 'wp'"
-  end.
-
-Tactic Notation "wp_if" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | If _ _ _ =>
-      wp_bind_core K;
-      etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
-    end) || fail "wp_if: cannot find 'If' in" e
-  | _ => fail "wp_if: not a 'wp'"
-  end.
-
-Tactic Notation "wp_match" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Case _ _ _ =>
-      wp_bind_core K;
-      etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]];
-      simpl_subst; wp_finish
-    end) || fail "wp_match: cannot find 'Match' in" e
-  | _ => fail "wp_match: not a 'wp'"
+Ltac wp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
 Tactic Notation "wp_bind" open_constr(efoc) :=
@@ -154,65 +70,65 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
-Lemma tac_wp_alloc Δ Δ' E j e v Φ :
-  to_val e = Some v →
+Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
+  IntoVal e v →
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
-  Δ ⊢ WP Alloc e @ E {{ Φ }}.
+    (Δ'' ⊢ WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
+  Δ ⊢ WP fill K (Alloc e) @ E {{ Φ }}.
 Proof.
-  intros ?? HΔ. eapply wand_apply; first exact: wp_alloc.
+  intros ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
 
-Lemma tac_wp_load Δ Δ' E i l q v Φ :
+Lemma tac_wp_load Δ Δ' E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ Φ v) →
-  Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+  (Δ' ⊢ WP fill K (of_val v) @ E {{ Φ }}) →
+  Δ ⊢ WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first exact: wp_load.
+  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
-  to_val e = Some v' →
+Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
+  IntoVal e v' →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ Φ (LitV LitUnit)) →
-  Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  (Δ'' ⊢ WP fill K (Lit LitUnit) @ E {{ Φ }}) →
+  Δ ⊢ WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first by eapply wp_store.
+  intros. rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.