Use Iris' PureExec typeclass

theories/F_mu_ref_conc/lang.v

@@ -373,7 +373,7 @@ Module lang.
   Lemma alloc_fresh e v σ :
     let l := fresh (dom (gset loc) σ) in
     to_val e = Some v → head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) [].
-  Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
+  Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 End lang.
 
 (** Language instance for Iris *)

theories/F_mu_ref_conc/pureexec.v

 From iris_logrel.prelude Require Export hax.
 From iris_logrel.F_mu_ref_conc Require Export lang subst notation.
 
-Class PureExec (P : Prop) (e1 e2 : expr) := {
-  pure_exec_safe : P -> ∀ σ, head_reducible e1 σ;
-  pure_exec_puredet : P -> ∀ σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs;
-}.
-
-(* DF: Some tactics will loop pretty badly and consume lots of memory if you make this an instance *)
-Lemma PureExec_Closed P e1 e2 `{HP: PureExec P e1 e2} `{Hcl : Closed X e1} : P -> Closed X e2.
-Proof.
-destruct HP as [Hpure Hstep].
-intros p. specialize (Hpure p). specialize (Hstep p).
-specialize (Hpure inhabitant).
-unfold head_reducible in *.
-destruct Hpure as (e' & σ' & efs & Hst).
-destruct (Hstep inhabitant e' σ' efs Hst) as (? & ? & ?); subst.
-destruct e1; inv_head_step;
-  unfold Closed in *; simpl in Hcl; simpl;
-  destruct_and?; split_and?; eauto.
-- apply Closed_mono with ∅; [ | set_solver ].
-  destruct f, x; simpl in *; eauto;
-    repeat apply is_closed_subst_preserve; eauto;
-    try apply of_val_closed.
-- apply of_val_closed'.
-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 :=
+  apply hoist_pred_pureexec; intros; destruct_and?;
+  apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
 
 Instance pure_binop op e1 v1 e2 v2 v `(to_val e1 = Some v1) `(to_val e2 = Some v2):
   PureExec (binop_eval op v1 v2 = Some v)
            (BinOp op e1 e2)
            (of_val v).
-Proof.
-split; intros Hval.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_rec f x e1 e2 v2 `{Closed ∅ (Rec f x e1)} `(to_val e2 = Some v2) :
   PureExec True
            (App (Rec f x e1) e2)
            (subst' f (Rec f x e1) (subst' x e2 e1)).
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 (* TODO: give this one a correct priority? *)
 Instance pure_rec_locked e f x e1 e2 v2 `(to_val e2 = Some v2) `(e = Rec f x e1) `{Closed (x :b: f :b: ∅) e1} :
@@ -51,81 +25,46 @@ Instance pure_rec_locked e f x e1 e2 v2 `(to_val e2 = Some v2) `(e = Rec f x e1)
            (App e e2)
            (e $/ v2) | 100.
 Proof.
-split; intros ?; subst.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. destruct f; by inv_head_step.
+  apply hoist_pred_pureexec; intros; destruct_and?;
+  apply det_head_step_pureexec. 
+  - solve_exec_safe.
+  - destruct f; solve_exec_puredet.
 Qed.
 
 Instance pure_fst e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
   PureExec True (Fst (Pair e1 e2)) e1.
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_snd e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
   PureExec True (Snd (Pair e1 e2)) e2.
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_unfold e1 v1 `(to_val e1 = Some v1) :
   PureExec True (Unfold (Fold e1)) e1.
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_unpack e1 e2 v1 `(to_val e1 = Some v1) :
   PureExec True (Unpack (Pack e1) e2) (e2 e1).
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_if_true e1 e2 :
   PureExec True (If #true e1 e2) e1.
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_if_false e1 e2 :
   PureExec True (If #false e1 e2) e2.
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_case_inl e0 v `(to_val e0 = Some v) e1 e2  :
   PureExec True (Case (InjL e0) e1 e2) (e1 e0).
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_case_inr e0 v `(to_val e0 = Some v) e1 e2  :
   PureExec True (Case (InjR e0) e1 e2) (e2 e0).
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.
 
 Instance pure_tlam e `{Closed ∅ e} :
   PureExec True
            (TApp (TLam e))
            e.
-Proof.
-split; intros ?.
-- intros. do 3 eexists. econstructor; eauto using to_of_val.
-- intros. by inv_head_step.
-Qed.
+Proof. solve_pureexec. Qed.

theories/F_mu_ref_conc/reflection.v

@@ -231,12 +231,16 @@ Ltac solve_to_val :=
   | |- to_val ?e = Some ?v =>
      let e' := R.of_expr e in change (to_val (R.to_expr e') = Some v);
      apply R.to_val_Some; simpl; unfold R.to_expr; unlock; reflexivity
+  | |- IntoVal ?e ?v =>
+     let e' := R.of_expr e in change (to_val (R.to_expr e') = Some v);
+     apply R.to_val_Some; simpl; unfold R.to_expr; reflexivity
   | |- is_Some (to_val ?e) =>
      let e' := R.of_expr e in change (is_Some (to_val (R.to_expr e')));
      apply R.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
 Hint Extern 0 (to_val _ = Some _) => solve_to_val : typeclass_instances.
 Hint Extern 0 (is_Some (to_val _)) => solve_to_val : typeclass_instances.
+Hint Extern 0 (IntoVal _ _) => solve_to_val : typeclass_instances.
 
 Ltac solve_closed :=
   match goal with

theories/F_mu_ref_conc/rules.v

@@ -4,7 +4,7 @@ From iris.base_logic Require Export invariants big_op.
 From iris.algebra Require Import auth frac agree gmap.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export gen_heap.
-From iris_logrel.F_mu_ref_conc Require Export lang notation pureexec.
+From iris_logrel.F_mu_ref_conc Require Export lang notation pureexec reflection.
 Import uPred.
 
 (** The CMRA for the heap of the implementation. This is linked to the
@@ -108,15 +108,7 @@ Section lang_rules.
     PureExec φ e1 e2 →
     φ →
     ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-  Proof.
-    iIntros (? Hφ) "HWP".
-    iApply (wp_lift_pure_det_head_step_no_fork' with "HWP").
-    { destruct (pure_exec_safe Hφ ∅) as (e' & σ' & efs & Hst).
-      eapply val_stuck.
-      apply Hst. }
-    { apply (pure_exec_safe Hφ). }
-    { apply (pure_exec_puredet Hφ). }
-  Qed.
+  Proof. apply wp_pure_step_later. Qed.
 
   Lemma wp_rec E f x erec e1 e2 Φ :
     e1 = Rec f x erec →
@@ -125,7 +117,7 @@ Section lang_rules.
     ▷ WP subst' f e1 (subst' x e2 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
   Proof.
     iIntros (? [v ?] ?) "HWP". subst.
-    iApply (wp_pure with "HWP"); [ eapply pure_rec | exact I ]; eauto.
+    iApply (wp_pure with "HWP"); eauto.
   Qed.
 
   Lemma wp_tlam E e Φ {Hcl: Closed ∅ e} : ▷ WP e @ E {{ Φ }} ⊢ WP TApp (TLam e) @ E {{ Φ }}.
@@ -133,90 +125,15 @@ Section lang_rules.
     rewrite -(wp_lift_pure_det_head_step_no_fork (TApp _) e); eauto.
     intros; inv_head_step; eauto.
   Qed.
-
-  Lemma wp_fold E e v Φ :
-    to_val e = Some v → ▷ (|={E}=> Φ v) ⊢ WP Unfold (Fold e) @ E {{ Φ }}.
-  Proof.
-    intros <-%of_to_val.
-    rewrite -(wp_lift_pure_det_head_step_no_fork (Unfold _) (of_val v))
-      -?wp_value_fupd; eauto.
-    intros; inv_head_step; eauto.
-  Qed.
-
-  Lemma wp_pack E e1 e2 v Φ :
-    to_val e1 = Some v →
-    ▷ WP (App e2 e1) @ E {{ Φ }} ⊢ WP Unpack (Pack e1) e2 @ E {{ Φ }}.
-  Proof.
-    intros <-%of_to_val. 
-    rewrite -(wp_lift_pure_det_head_step_no_fork (Unpack _ _) _); eauto.
-    intros; inv_head_step; eauto.
-  Qed.
-
-  Lemma wp_fst E e1 v1 e2 v2 Φ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 →
-    ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
-  Proof.
-    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1)
-      -?wp_value_fupd; eauto.
-    intros; inv_head_step; eauto.
-  Qed.
-
-  Lemma wp_snd E e1 v1 e2 v2 Φ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 →
-    ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
-  Proof.
-    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2)
-      -?wp_value_fupd; eauto.
-    intros; inv_head_step; eauto.
-  Qed.
-
-  Lemma wp_case_inl E e0 v0 e1 e2 Φ :
-    to_val e0 = Some v0 →
-    ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
-  Proof.
-    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) _); eauto.
-    intros; inv_head_step; eauto.
-  Qed.
-
-  Lemma wp_case_inr E e0 v0 e1 e2 Φ :
-    to_val e0 = Some v0 →
-    ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
-  Proof.
-    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _)); eauto.
-    intros; inv_head_step; eauto.
-  Qed.
-
+  
   Lemma wp_fork E e Φ :
     ▷ (|={E}=> Φ #()) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
   Proof.
-  rewrite -(wp_lift_pure_det_head_step (Fork e) #() [e]) //=; eauto.
-  - rewrite -(wp_value_fupd _ _ #()); auto.
-    by rewrite -step_fupd_intro // right_id later_sep. 
-  - intros; inv_head_step; eauto.
-  Qed.
-
-  Lemma wp_if_true E e1 e2 Φ :
-    ▷ WP e1 @ E {{ Φ }} ⊢ WP If #true e1 e2 @ E {{ Φ }}.
-  Proof.
-    rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e1); eauto.
-    intros; inv_head_step; eauto.
-  Qed.
-
-  Lemma wp_if_false E e1 e2 Φ :
-    ▷ WP e2 @ E {{ Φ }} ⊢ WP If #false e1 e2 @ E {{ Φ }}.
-  Proof.
-    rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e2); eauto.
-    intros; inv_head_step; eauto.
+    rewrite -(wp_lift_pure_det_head_step (Fork e) #() [e]) //=; eauto.
+    - (* TODO typeclass inference fail *)
+      erewrite <-(wp_value_fupd _ _ #()); eauto; last solve_to_val.
+      by rewrite -step_fupd_intro // right_id later_sep. 
+    - intros; inv_head_step; eauto.
   Qed.
 
-  Lemma wp_nat_binop E op e1 e2 v1 v2 v Φ :
-    to_val e1 = Some v1 →
-    to_val e2 = Some v2 →
-    binop_eval op v1 v2 = Some v →
-    ▷ (|={E}=> Φ v) ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
-  Proof.
-    intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val _))
-      -?wp_value_fupd'; eauto.
-    intros; inv_head_step; eauto.
-  Qed.
 End lang_rules.

theories/F_mu_ref_conc/subst.v

@@ -413,6 +413,26 @@ Proof.
       [ apply lookup_delete | rewrite delete_commute ; apply lookup_delete ].
 Qed.
 
+(** Properties of the context substitution *)
+Lemma fill_item_subst_p (es : stringmap val) (Ki : ectx_item) (e : expr)  :
+  subst_p es (fill_item Ki e) = fill_item (subst_ctx_item es Ki) (subst_p es e).
+Proof.
+  induction Ki; simpl;
+  rewrite ?of_val_subst_p; eauto.
+Qed.
+
+Lemma fill_subst (es : stringmap val) (K : list ectx_item) (e : expr) :
+  subst_p es (fill K e) = fill (subst_ctx es K) (subst_p es e).
+Proof.
+  generalize dependent e. generalize dependent es.
+  induction K as [|Ki K]; eauto.
+  intros es e. simpl.
+  rewrite IHK.
+    by rewrite ?fill_item_subst_p.
+Qed.
+
+(** Substitutions and reductions *)
+
 Lemma subst_p_head_step e e' vs efs σ σ' :
   head_step e σ e' σ' efs →
   head_step (subst_p vs e) σ (subst_p vs e') σ' (subst_p vs <$> efs).
@@ -438,7 +458,18 @@ Proof.
   - econstructor. by rewrite Closed_subst_p_id.
 Qed.
 
-Lemma subst_p_safe e es :
+Lemma subst_p_prim_step e e' vs efs σ σ' :
+  prim_step e σ e' σ' efs →
+  prim_step (subst_p vs e) σ (subst_p vs e') σ' (subst_p vs <$> efs).
+Proof.
+  intros Hst.
+  destruct Hst as [K e1 e2 ?? Hst]; subst.
+  rewrite !fill_subst.
+  eapply Ectx_step with (subst_ctx vs K) (subst_p vs e1) (subst_p vs e2); eauto.
+  simpl. by apply subst_p_head_step.
+Qed.
+
+Lemma subst_p_safe_head e es :
   (∀ σ, head_reducible e σ) → (∀ σ, head_reducible (subst_p es e) σ).
 Proof.
   rewrite /head_reducible.
@@ -447,7 +478,19 @@ Proof.
   do 3 eexists. apply subst_p_head_step; eauto.
 Qed.
 
-Lemma subst_p_det e e' es :
+Lemma subst_p_safe e es :
+  (∀ σ, reducible e σ) → (∀ σ, reducible (subst_p es e) σ).
+Proof.
+  rewrite /reducible.
+  intros Hsafe.
+  intros σ. destruct (Hsafe σ) as (e' & σ' & efs & Hstep).
+  destruct Hstep as [K ? ? ? ? Hstep]. subst.
+  do 3 eexists. rewrite fill_subst.
+  eapply Ectx_step; eauto.
+  apply subst_p_head_step; eauto.
+Qed.
+
+Lemma subst_p_det_head e e' es :
   (∀ σ, head_step e σ e' σ []) →
   (∀ σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) →
   (∀ σ1 e2 σ2 efs, head_step (subst_p es e) σ1 e2 σ2 efs -> σ1=σ2 /\ (subst_p es e')=e2 /\ [] = efs).
@@ -482,20 +525,71 @@ Proof.
     by simplify_eq.
 Qed.
 
-(** Properties of the context substitution *)
-Lemma fill_item_subst_p (es : stringmap val) (Ki : ectx_item) (e : expr)  :
-  subst_p es (fill_item Ki e) = fill_item (subst_ctx_item es Ki) (subst_p es e).
-Proof.
-  induction Ki; simpl;
-  rewrite ?of_val_subst_p; eauto.
-Qed.
+Lemma subst_p_det e e' es :
+  (∀ σ, prim_step e σ e' σ []) →
+  (∀ σ1 e2 σ2 efs, prim_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) →
+  (∀ σ1 e2 σ2 efs, prim_step (subst_p es e) σ1 e2 σ2 efs -> σ1=σ2 /\ (subst_p es e')=e2 /\ [] = efs).
+Proof. admit. Admitted.
+  (* intros Hstep Hdet σ1 e2 σ2 efs Hst. *)
+  (* assert (Hstep' := Hstep). *)
+  (* specialize (Hdet σ1). *)
+  (* specialize (Hstep σ1). *)
+  (* destruct Hstep as [K0 e0 e0' ?? Hstep]. subst. simpl in *. *)
+  (* rewrite fill_subst in Hst. *)
+  (* rewrite fill_subst. *)
+  (* destruct Hst as [K1 t0 t2 Hfill ? Hst]. subst. simpl in *. *)
+  (* assert (to_val (subst_p es e0) = None) as Hnoval. *)
+  (* { pose (Hstuck:=val_prim_stuck). *)
+  (*   simpl in Hstuck. *)
+  (*   eapply Hstuck. *)
+  (*   apply head_prim_step. *)
+  (*   by apply subst_p_head_step. } *)
+  (* destruct (step_by_val _ _ _ _ _ _ _ _ Hfill Hnoval Hst) *)
+  (*   as [K2 Hctx]. subst. clear Hnoval. *)
+  (* rewrite fill_app in Hfill. *)
+  (* apply fill_inj in Hfill. *)
+  (* rewrite fill_app.     *)
+  (* inversion Hstep; subst; simplify_eq/=. *)
+  (* Focus 3. *)
+  (* inversion Hst; subst; simplify_eq/=. *)
+  (* split_and!; eauto. *)
+  (* f_equal. *)
+  (* rewrite -(of_to_val _ _ H0). *)
+  (* rewrite -(of_to_val _ _ H1). *)
+  
+  (* inversion Hstep; subst; simplify_eq/=. *)
+  (* inversion Hfill. *)
+  (* apply fill_inj. *)
+  (* repeat (split; eauto). *)
+  (* apply *)
+  (* simpl in Hst. *)
+  (* simpl in Hst. *)
+  (*   simpl in Hst; inversion Hst; simplify_eq/=; eauto; *)
 
-Lemma fill_subst (es : stringmap val) (K : list ectx_item) (e : expr) :
-  subst_p es (fill K e) = fill (subst_ctx es K) (subst_p es e).
-Proof.
-  generalize dependent e. generalize dependent es.
-  induction K as [|Ki K]; eauto.
-  intros es e. simpl.
-  rewrite IHK.
-    by rewrite ?fill_item_subst_p.
-Qed.
+  (* inversion Hstep; subst; simplify_eq/=; *)
+  (*   simpl in Hst; inversion Hst; simplify_eq/=; eauto; *)
+  (* repeat lazymatch goal with *)
+  (* | [ H : to_val ?e = Some ?v, H' : to_val (subst_p es ?e) = Some ?v2 |- _ ] => *)
+  (*   rewrite -(of_to_val _ _ H) in H'; *)
+  (*   rewrite of_val_subst_p in H'; *)
+  (*   rewrite to_of_val in H' *)
+  (* | [ H : to_val ?e = Some ?v, H' : context[subst_p _ ?e] |- _ ] => *)
+  (*   rewrite -(of_to_val _ _ H) in H'; *)
+  (*   rewrite of_val_subst_p in H'; *)
+  (*   rewrite (of_to_val _ _ H) in H' *)
+  (* end; simplify_eq/=; *)
+  (* rewrite ?of_val_subst_p; *)
+  (* split_and !; eauto. *)
+  (* - rewrite !subst_p_delete. *)
+  (*   rewrite !(delete_commute_binder _ f x). *)
+  (*   rewrite (Closed_subst_p_id' _ _ e1); eauto. *)
+  (*   rewrite (to_val_subst_p e0 v0 _); eauto. *)
+  (*   apply elem_of_rec_lookup. *)
+  (* - destruct (Hdet _ _ _ Hst) as (?&?&?). *)
+  (*   by simplify_eq. *)
+  (* - destruct (Hdet _ _ _ Hst) as (?&?&?). *)
+  (*   by simplify_eq. *)
+  (* - destruct (Hdet _ _ _ Hst) as (?&?&?). *)
+  (*   by simplify_eq. *)
+
+  (* apply subst_p_det_head. *)

theories/F_mu_ref_conc/tactics.v

-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre lifting.
 From iris.proofmode Require Export tactics coq_tactics.
 From iris_logrel.F_mu_ref_conc Require Export rules lang reflection.
 Set Default Proof Using "Type".
@@ -97,9 +97,9 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
 (** * Symbolic execution WP tactics *)
 (** ** Pure reductions *)
 Lemma tac_wp_pure `{heapG Σ} K φ e1 e2 ℶ1 ℶ2 E Φ :
-  IntoLaterNEnvs 1 ℶ1 ℶ2 →
   PureExec φ e1 e2 →
   φ →
+  IntoLaterNEnvs 1 ℶ1 ℶ2 →
   (ℶ2 ⊢ WP fill K e2 @ E {{ Φ }}) →
   (ℶ1 ⊢ WP fill K e1 @ E {{ Φ }}).
 Proof.
@@ -108,7 +108,7 @@ Proof.
   rewrite Hgoal.
   iIntros "HWP".
   wp_bind_core K.
-  iApply wp_pure; eauto.
+  iApply wp_pure_step_later; eauto.
   iApply (wp_bind_inv with "HWP").
   { (* TODO: how to get rid of this? *)
     change lang with (ectx_lang expr).
@@ -122,9 +122,9 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
-    [apply _ (* IntoLaters *)
-    |apply _ (* PureExec *)
+    [apply _ (* PureExec *)
     |try (exact I || reflexivity || tac_rel_done)
+    |apply _ (* IntoLaters *)
     |simpl_subst/= (* new goal *)])
   end.
 

theories/examples/counter.v

@@ -86,7 +86,7 @@ Section CG_Counter.
     unfold FG_increment. unlock.
     iApply wp_rec; eauto.
     iNext. simpl.
-    iApply wp_value; eauto. simpl. by rewrite decide_left.
+    iApply wp_value; eauto.
     iApply wp_rec; eauto.
     iNext. simpl.
     wp_bind (Load (# x)).
@@ -95,11 +95,12 @@ Section CG_Counter.
     iApply wp_rec; eauto.
     iNext. simpl.
     wp_bind (BinOp _ _ _).
-    iApply (wp_nat_binop);eauto. iNext. iModIntro. simpl.    
+    wp_binop.
+    iApply wp_value.
     wp_bind (CAS _ _ _).    
     iApply (wp_cas_suc with "[Hx]"); auto.
     iNext. iIntros "Hx".
-    iApply wp_if_true. iNext.
+    wp_if.
     iApply wp_value; auto.
     by iApply "Hlog".
   Qed.

theories/examples/lock.v

@@ -67,6 +67,17 @@ Section proof.
     iApply ("Hlog" with "Hl").
   Qed.
 
+  Lemma bin_log_related_newlock_l Γ K t τ :
+    (∀ l : loc, l ↦ᵢ #false -∗ {E1,E1;Δ;Γ} ⊨ fill K #l ≤log≤ t : τ) -∗
+    {E1,E1;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t : τ.
+  Proof.
+    iIntros "Hlog".
+    unfold newlock. unlock.
+    rel_rec_l.
+    rel_alloc_l as l "Hl".
+    iApply ("Hlog" with "Hl").
+  Qed.
+
   Global Opaque newlock.
   
   Transparent acquire. 
@@ -96,7 +107,42 @@ Section proof.
     rel_if_r.
     by iApply "Hlog".
   Qed.
-  
+
+  Lemma bin_log_related_acquire_suc_l Γ K l t τ :
+    l ↦ᵢ #false -∗
+    (l ↦ᵢ #true -∗ {E1,E1;Δ;Γ} ⊨ fill K (#()) ≤log≤ t : τ) -∗
+    {E1,E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ.
+  Proof.
+    iIntros "Hl Hlog".
+    unfold acquire. unlock.
+    rel_rec_l.
+    rel_cas_l_atomic. iModIntro.
+    iExists _; iFrame "Hl".
+    iSplitR.
+    { iIntros (Hfoo). congruence. }
+    iIntros (_). iNext. iIntros "Hl".
+    rel_if_l.
+    by iApply "Hlog".
+  Qed.
+
+  Lemma bin_log_related_acquire_fail_l Γ K l t τ :
+    l ↦ᵢ #true -∗
+    (l ↦ᵢ #false -∗ {E1,E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ) -∗
+    {E1,E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ.
+  Proof.
+    iIntros "Hl Hlog".
+    iLöb as "IH".
+    unfold acquire. unlock.
+    rel_rec_l.