Allow `IntoVal` to take pure steps.

tests/one_shot.v

@@ -47,7 +47,7 @@ Proof.
   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.
+  iModIntro. iApply "Hf"; iSplit.
   - iIntros (n) "!#". wp_lam. wp_inj. wp_inj.
     iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + iMod (own_update with "Hγ") as "Hγ".
@@ -70,7 +70,7 @@ 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.
+    iModIntro. wp_let. iIntros "!#". wp_lam.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     { by wp_match. }
     wp_match. wp_bind (! _)%E.

theories/heap_lang/lib/assert.v

@@ -12,13 +12,13 @@ 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 [{ Φ }].
 Proof.
-  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
+  iIntros "HΦ". rewrite /assert. wp_lam. 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 {{ Φ }}.
 Proof.
-  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
+  iIntros "HΦ". rewrite /assert. wp_lam. wp_lam.
   wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.

theories/heap_lang/lib/par.v

@@ -32,7 +32,7 @@ Proof.
   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_let.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :

theories/heap_lang/lib/spawn.v

@@ -48,7 +48,7 @@ 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 /=.
+  iIntros (? Φ) "Hf HΦ". rewrite /spawn /=.
   wp_lam. wp_inj. 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

@@ -80,7 +80,7 @@ Section proof.
     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.
+    iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
   Lemma wait_loop_spec γ lk x R :

theories/heap_lang/lifting.v

@@ -47,11 +47,6 @@ Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Instance into_val_val v : IntoVal (Val v) v.
-Proof. done. Qed.
-Instance as_val_val v : AsVal (Val v).
-Proof. by eexists. Qed.
-
 Local Ltac solve_atomic :=
   apply strongly_atomic_atomic, ectx_language_atomic;
     [inversion 1; naive_solver
@@ -72,10 +67,19 @@ Proof. solve_atomic. Qed.
 Instance skip_atomic s  : Atomic s Skip.
 Proof. solve_atomic. Qed.
 
+Local Ltac pure_exec_step :=
+  lazymatch goal with
+  | |- PureExec _ _ ?e _ => eapply pure_exec_0_l;
+     [reshape_expr e ltac:(fun K e' =>
+        eapply (pure_exec_fill K); eassumption)
+     |simpl]
+  end.
 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_pure_exec :=
-  subst;
+  intros; unfold IntoVal;
+  repeat pure_exec_step;
+  eapply pure_exec_mono_steps with 1%nat; [lia|];
   apply mk_pure_exec; intros ?;
   apply nsteps_once, pure_head_step_pure_step;
     constructor; [solve_exec_safe | solve_exec_puredet].
@@ -87,51 +91,78 @@ Instance AsRecV_recv_locked v f x e :
   AsRecV v f x e → AsRecV (locked v) f x e.
 Proof. by unlock. Qed.
 
-Instance pure_recc f x (erec : expr) :
+Instance into_val_val v : IntoVal (Val v) v.
+Proof. apply pure_exec_refl. Qed.
+Instance into_val_recc f x erec :
+  IntoVal (Rec f x erec) (RecV f x erec).
+Proof. solve_pure_exec. Qed.
+Instance into_val_pairc e1 e2 v1 v2 :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  IntoVal (Pair e1 e2) (PairV v1 v2).
+Proof. solve_pure_exec. Qed.
+Instance into_val_injlc v :
+  IntoVal e v → IntoVal (InjL e) (InjLV v).
+Proof. solve_pure_exec. Qed.
+Instance into_val_injrc e v :
+  IntoVal e v → IntoVal (InjR e) (InjRV v).
+Proof. solve_pure_exec. Qed.
+
+Instance pure_recc f x erec :
   PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
 Proof. solve_pure_exec. Qed.
-Instance pure_pairc (v1 v2 : val) :
-  PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
+Instance pure_pairc v1 v2 :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  PureExec True 1 (Pair e1 e2) (Val $ PairV v1 v2).
 Proof. solve_pure_exec. Qed.
-Instance pure_injlc (v : val) :
-  PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
+Instance pure_injlc v :
+  IntoVal e v → PureExec True 1 (InjL e) (Val $ InjLV v).
 Proof. solve_pure_exec. Qed.
 Instance pure_injrc (v : val) :
-  PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
+  IntoVal e v → PureExec True 1 (InjR e) (Val $ InjRV v).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
-  PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
-Proof. unfold AsRecV in *. solve_pure_exec. Qed.
+Instance pure_beta e1 e2 f x (erec : expr) (v1 v2 : val)  :
+  IntoVal e1 v1 → AsRecV v1 f x erec →
+  IntoVal e2 v2 →
+  PureExec True 1 (App e1 e2) (subst' x v2 (subst' f v1 erec)).
+Proof. unfold AsRecV. solve_pure_exec. Qed.
 
-Instance pure_unop op v v' :
-  PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
+Instance pure_unop op e v v' :
+  IntoVal e v →
+  PureExec (un_op_eval op v = Some v') 1 (UnOp op e) (Val v').
 Proof. solve_pure_exec. Qed.
 
-Instance pure_binop op v1 v2 v' :
-  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
+Instance pure_binop op e1 e2 v1 v2 v' :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op e1 e2) (Val v').
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
+Instance pure_if_true e1 e2 :
+  PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
+Instance pure_if_false e1 e2 :
+  PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
-Instance pure_fst v1 v2 :
-  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
+Instance pure_fst e v1 v2 :
+  IntoVal e (PairV v1 v2) →
+  PureExec True 1 (Fst e) (Val v1).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_snd v1 v2 :
-  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
+Instance pure_snd e v1 v2 :
+  IntoVal e (PairV v1 v2) →
+  PureExec True 1 (Snd e) (Val v2).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_case_inl v e1 e2 :
-  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
+Instance pure_case_inl e v e1 e2 :
+  IntoVal e (InjLV v) →
+  PureExec True 1 (Case e e1 e2) (App e1 (Val v)).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_case_inr v e1 e2 :
-  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
+Instance pure_case_inr e v e1 e2 :
+  IntoVal e (InjRV v) →
+  PureExec True 1 (Case e e1 e2) (App e2 (Val v)).
 Proof. solve_pure_exec. Qed.
 
 Section lifting.

theories/heap_lang/proofmode.v

@@ -48,15 +48,19 @@ Proof.
   rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
 Qed.
 
-Lemma tac_wp_value `{heapG Σ} Δ s E Φ v :
-  envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
-Lemma tac_twp_value `{heapG Σ} Δ s E Φ v :
-  envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
-Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
+Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
+Proof. rewrite envs_entails_eq=> ? ->. by apply lifting.wp_value. Qed.
+Lemma tac_twp_value `{heapG Σ} Δ s E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E [{ Φ }]).
+Proof. rewrite envs_entails_eq=> ? ->. by apply total_lifting.twp_value. Qed.
 
 Ltac wp_value_head :=
-  first [eapply tac_wp_value || eapply tac_twp_value]; reduction.pm_prettify.
+  first [eapply tac_wp_value || eapply tac_twp_value];
+    [iSolveTC
+    |reduction.pm_prettify].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;

theories/program_logic/language.v

@@ -198,8 +198,9 @@ Section language.
 
   (* This is a family of frequent assumptions for PureExec *)
   Class IntoVal (e : expr Λ) (v : val Λ) :=
-    into_val : of_val v = e.
+    into_val : PureExec True 0 e (of_val v).
 
+  (* TODO: either drop this class, or change it so that it matches IntoVal *)
   Class AsVal (e : expr Λ) := as_val : ∃ v, of_val v = e.
   (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
   efficiently since no witness has to be computed. *)

theories/program_logic/lifting.v

@@ -93,8 +93,8 @@ Proof.
   iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
-  destruct (to_val e2) eqn:?; last by iExFalso.
-  iApply wp_value; last done. by apply of_to_val.
+  destruct (to_val e2) eqn:He2; last by iExFalso.
+  apply of_to_val in He2 as <-. by iApply wp_value'.
 Qed.
 
 Lemma wp_lift_atomic_step {s E Φ} e1 :
@@ -150,4 +150,14 @@ Proof.
   intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
   induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
 Qed.
+
+Lemma wp_value `{Inhabited (state Λ)} s E Φ e v :
+  IntoVal e v → Φ v ⊢ WP e @ s; E {{ Φ }}.
+Proof.
+  rewrite /IntoVal. iIntros (?) "?". iApply wp_pure_step_later=> //=.
+  by iApply wp_value'.
+Qed.
+Lemma wp_value_fupd `{Inhabited (state Λ)} s E Φ e v :
+  IntoVal e v → (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}.
+Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
 End lifting.

theories/program_logic/ownp.v

@@ -146,8 +146,8 @@ Section lifting.
     iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
     iNext; iIntros (e2 σ2 efs) "% Hσ".
     iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
-    destruct (to_val e2) eqn:?; last by iExFalso.
-    iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
+    destruct (to_val e2) eqn:He2; last by iExFalso.
+    iMod "Hclose". apply of_to_val in He2 as <-. by iApply wp_value'.
   Qed.
 
   Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :

theories/program_logic/total_lifting.v

@@ -53,8 +53,8 @@ Proof.
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
   iIntros "!>" (e2 σ2 efs) "%". iMod "Hclose" as "_".
   iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
-  destruct (to_val e2) eqn:?; last by iExFalso.
-  iApply twp_value; last done. by apply of_to_val.
+  destruct (to_val e2) eqn:He2; last by iExFalso.
+  apply of_to_val in He2 as <-. by iApply twp_value'.
 Qed.
 
 Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
@@ -78,4 +78,14 @@ Proof.
   iApply twp_lift_pure_det_step; [done|naive_solver|].
   iModIntro. rewrite /= right_id. by iApply "IH".
 Qed.
+
+Lemma twp_value `{Inhabited (state Λ)} s E Φ e v :
+  IntoVal e v → Φ v -∗ WP e @ s; E [{ Φ }].
+Proof.
+  rewrite /IntoVal. iIntros (?) "?". iApply twp_pure_step=> //=.
+  by iApply twp_value'.
+Qed.
+Lemma twp_value_fupd `{Inhabited (state Λ)} s E Φ e v :
+  IntoVal e v → (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
+Proof. intros ?. rewrite -twp_fupd -twp_value //. Qed.
 End lifting.

theories/program_logic/total_weakestpre.v

@@ -213,14 +213,8 @@ Global Instance twp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (twp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply twp_mono. Qed.
 
-Lemma twp_value s E Φ e v : IntoVal e v → Φ v -∗ WP e @ s; E [{ Φ }].
-Proof. intros <-. by apply twp_value'. Qed.
 Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }].
 Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
-Lemma twp_value_fupd s E Φ e v : IntoVal e v → (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
-Proof. intros ?. rewrite -twp_fupd -twp_value //. Qed.
-Lemma twp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E [{ Φ }] ={E}=∗ Φ v.
-Proof. intros <-. by apply twp_value_inv'. Qed.
 
 Lemma twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, R ∗ Φ v }].
 Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.

theories/program_logic/weakestpre.v

@@ -175,15 +175,8 @@ Global Instance wp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (wp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
 
-Lemma wp_value s E Φ e v : IntoVal e v → Φ v ⊢ WP e @ s; E {{ Φ }}.
-Proof. intros <-. by apply wp_value'. Qed.
 Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ s; E {{ Φ }}.
 Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
-Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
-  (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}.
-Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
-Lemma wp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E {{ Φ }} ={E}=∗ Φ v.
-Proof. intros <-. by apply wp_value_inv'. Qed.
 
 Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.