The `PureExec` typeclass for performing pure symbolic executions.

Instead of writing a separate tactic lemma for each pure reduction,
there is a single tactic lemma for performing all of them.

The instances of PureExec can be shared between WP tactics and, e.g.
symbolic execution in the ghost  threadpool

_CoqProject

@@ -55,6 +55,7 @@ theories/base_logic/lib/core.v
 theories/base_logic/lib/fancy_updates_from_vs.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
+theories/program_logic/pure.v
 theories/program_logic/weakestpre.v
 theories/program_logic/hoare.v
 theories/program_logic/language.v

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 pure.
 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,56 @@ 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.
-
-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.
-
-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.
-
-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.
-
-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.
-
-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.
-
-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.
-
-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.
-
-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.
+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 :=
+  intros; split; intros ?; destruct_and?; [ solve_exec_safe | solve_exec_puredet ].
+
+Global Instance pure_rec f x erec e1 e2 v2 :
+  PureExec (to_val e2 = Some v2 ∧ e1 = Rec f x erec ∧ Closed (f :b: x :b: []) erec)
+           (App e1 e2)
+           (subst' x e2 (subst' f e1 erec)).
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_unop op e v v' :
+  PureExec (to_val e = Some v ∧ un_op_eval op v = Some v')
+           (UnOp op e)
+           (of_val v').
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_binop op e1 e2 v1 v2 v' :
+  PureExec (to_val e1 = Some v1 ∧ to_val e2 = Some v2 ∧ bin_op_eval op v1 v2 = Some v')
+           (BinOp op e1 e2)
+           (of_val v').
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_if_true e1 e2 :
+  PureExec True (If (Lit (LitBool true)) e1 e2) e1.
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_if_false e1 e2 :
+  PureExec True (If (Lit (LitBool false)) e1 e2) e2.
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_fst e1 e2 v1 v2 :
+  PureExec (to_val e1 = Some v1 ∧ to_val e2 = Some v2)
+           (Fst (Pair e1 e2))
+           e1.
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_snd e1 e2 v1 v2 :
+  PureExec (to_val e1 = Some v1 ∧ to_val e2 = Some v2)
+           (Snd (Pair e1 e2))
+           e2.
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_case_inl e0 v e1 e2  :
+  PureExec (to_val e0 = Some v) (Case (InjL e0) e1 e2) (App e1 e0).
+Proof. solve_pureexec. Qed.
+
+Global Instance pure_case_inr e0 v e1 e2  :
+  PureExec (to_val e0 = Some v) (Case (InjR e0) e1 e2) (App e2 e0).
+Proof. solve_pureexec. Qed.
 
 (** Heap *)
 Lemma wp_alloc E e v :
@@ -221,22 +191,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' []); 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 +202,11 @@ 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 ([? ?] ?) "?". do 2 (iApply (wp_pure' []); 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.
+Proof. iIntros ([? ?] ?) "?". do 2 (iApply (wp_pure' []); eauto). 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.
 End lifting.

theories/heap_lang/proofmode.v

@@ -54,76 +54,55 @@ Proof. by unlock. Qed.
    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.
 
-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.
-
-Tactic Notation "wp_lam" :=
-  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.
 
-Tactic Notation "wp_let" := wp_lam.
-Tactic Notation "wp_seq" := wp_let.
-
-Tactic Notation "wp_op" :=
-  iStartProof;
+(* Solves side-conditions generated specifically by wp_pure *)
+Ltac wp_pure_done :=
+  split_and?;
   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'"
+  | |- of_val _ = _ => solve_of_val_unlock
+  | _ => wp_done
   end.
 
-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.
+Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
+  IntoLaterNEnvs 1 Δ Δ' →
+  PureExec φ e1 e2 →
+  φ →
+  (Δ' ⊢ WP fill K e2 @ E {{ Φ }}) →
+  (Δ ⊢ WP fill K e1 @ E {{ Φ }}).
+Proof.
+  intros ??? HΔ'.
+  rewrite into_laterN_env_sound /=.
+  rewrite HΔ' -wp_pure' //.
+Qed.
 
-Tactic Notation "wp_if" :=
+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
-    | 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'"
+    let e'' := eval hnf in e' in
+    unify e'' efoc;
+    wp_bind_core K;
+    eapply (tac_wp_pure []);
+    [apply _                  (* IntoLaters *)
+    |unlock; simpl; apply _   (* PureExec *)
+    |wp_pure_done             (* The pure condition for PureExec *)
+    |simpl_subst; wp_finish   (* 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_lam.
+Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
+Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" :=
   iStartProof;
   lazymatch goal with

theories/program_logic/pure.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Import ectx_lifting.
+Set Default Proof Using "Type".
+
+Section pure.
+Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
+Context `{irisG (ectx_lang expr) Σ}.
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types v : val.
+Implicit Types e : expr.
+
+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;
+  }.
+
+Lemma wp_pure `{Inhabited state} K E E' e1 e2 φ Φ :
+  PureExec φ e1 e2 →
+  φ →
+  (|={E,E'}▷=> WP fill K e2 @ E {{ Φ }}) ⊢ WP fill K e1 @ E {{ Φ }}.
+Proof.
+  iIntros (? Hφ) "HWP".
+  iApply wp_bind.
+  iApply (wp_lift_pure_det_head_step_no_fork with "[HWP]").
+  { destruct (pure_exec_safe Hφ inhabitant) as (? & ? & ? & Hst).
+    eapply ectx_language.val_stuck.
+    apply Hst. }
+  { apply (pure_exec_safe Hφ). }
+  { apply (pure_exec_puredet Hφ). }
+  iApply wp_bind_inv.
+  iExact "HWP".
+Qed.
+
+
+Lemma wp_pure' `{Inhabited state} K E e1 e2 φ Φ :
+  PureExec φ e1 e2 →
+  φ →
+  (▷ WP fill K e2 @ E {{ Φ }}) ⊢ WP fill K e1 @ E {{ Φ }}.
+Proof. 
+  intros ? ?.
+  rewrite -wp_pure //.
+  rewrite -step_fupd_intro //.
+Qed.
+
+End pure.

theories/tests/heap_lang.v

@@ -44,14 +44,16 @@ Section LiftingTests.
     Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
     iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
-    wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
+    wp_rec. wp_let. wp_op. wp_let.
+    wp_op; case_bool_decide; wp_if.
     - iApply ("IH" with "[%] HΦ"). omega.
     - by assert (n1 = n2 - 1) as -> by omega.
   Qed.
 
   Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) -∗ WP Pred #n @ E {{ Φ }}.
   Proof.
-    iIntros "HΦ". wp_lam. wp_op=> ?; wp_if.
+    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.

theories/tests/one_shot.v

@@ -80,7 +80,8 @@ Proof.
     iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
     iMod ("Hclose" with "[Hl]") as "_".
     { iNext; iRight; by eauto. }
-    iModIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
+    iModIntro. wp_match. iApply wp_assert.
+    wp_op. by case_bool_decide.
 Qed.
 
 Lemma ht_one_shot (Φ : val → iProp Σ) :