Consolidate all the pure tactics

theories/F_mu_ref_conc/pureexec.v

@@ -119,3 +119,13 @@ split; intros ?.
 - intros. do 3 eexists. econstructor; eauto using to_of_val.
 - intros. by inv_head_step.
 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.

theories/F_mu_ref_conc/tactics.v

@@ -4,22 +4,24 @@ From iris_logrel.F_mu_ref_conc Require Export rules lang reflection.
 Set Default Proof Using "Type".
 Import lang.
 
-(* * Tactics for solving specific goals *)
+(** * General tactics *)
 
-(* 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. *)
+(** 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; fast_done.
 Hint Extern 0 (of_val _ = _) => solve_of_val_unlock : typeclass_instances.
 
+(** A "finisher" tactic *)
 Ltac tac_rel_done := split_and?; try
   lazymatch goal with
   | [ |- of_val _ = _ ] => solve_of_val_unlock
   | [ |- Closed _ _ ] => solve_closed
   | [ |- to_val _ = Some _ ] => solve_to_val
+  | [ |- language.to_val _ = Some _ ] => solve_to_val
   | [ |- is_Some (to_val _)] => solve_to_val
   end.
 
-(* * WP tactics *)
+(** ** Bending and binding *)
 (** The tactic [reshape_expr e tac] decomposes the expression [e] into an
 evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
 for each possible decomposition until [tac] succeeds. *)
@@ -92,6 +94,8 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
+(** * Symbolic execution WP tactics *)
+(** ** Pure reductions *)
 Lemma tac_wp_pure `{heapG Σ} K φ e1 e2 ℶ1 ℶ2 E Φ :
   IntoLaterNEnvs 1 ℶ1 ℶ2 →
   PureExec φ e1 e2 →
@@ -130,14 +134,191 @@ Tactic Notation "wp_let" := wp_rec.
 Tactic Notation "wp_fst" := wp_pure (Fst (Pair _ _)).
 Tactic Notation "wp_snd" := wp_pure (Snd (Pair _ _)).
 Tactic Notation "wp_proj" := wp_pure (_ (Pair _ _)).
-Tactic Notation "wp_unfold" := wp_pure (Unfold (Fold _)).
-Tactic Notation "wp_fold" := wp_unfold.
-Tactic Notation "wp_if" := wp_pure (If _ _ _).
-Tactic Notation "wp_if_true" := wp_pure (If #true _ _).
-Tactic Notation "wp_if_false" := wp_pure (If #false _ _).
 Tactic Notation "wp_case_inl" := wp_pure (Case (InjL _) _ _).
-Tactic Notation "wp_case_inr" := wp_pure (Case (InjL _) _ _).
+Tactic Notation "wp_case_inr" := wp_pure (Case (InjR _) _ _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
-Tactic Notation "wp_op" := wp_pure (BinOp _ _ _).
+Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _).
+Tactic Notation "wp_op" := wp_binop.
+Tactic Notation "wp_if_true" := wp_pure (If #true _ _).
+Tactic Notation "wp_if_false" := wp_pure (If #false _ _).
+Tactic Notation "wp_if" := wp_pure (If _ _ _).
+Tactic Notation "wp_unfold" := wp_pure (Unfold (Fold _)).
+Tactic Notation "wp_fold" := wp_unfold.
+Tactic Notation "wp_tlam" := wp_pure (TApp (TLam _)).
+Tactic Notation "wp_unpack" := wp_pure (Unpack (Pack _) _).
+Tactic Notation "wp_pack" := wp_unpack.
+
+Ltac wp_value := etrans; [| eapply wp_value; tac_rel_done]; lazy beta.
+
+(** ** Stateful reductions *)
+(* WARNING: Most of the code below is copypasta from heap_lang *)
+
+Section heap.
+Context `{heapG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types Δ : envs (iResUR Σ).
+Import uPred.
+Lemma tac_wp_alloc Δ Δ' E j e v Φ :
+  to_val e = Some v →
+  IntoLaterNEnvs 1 Δ Δ' →
+  (∀ l, ∃ Δ'',
+    envs_app false (Esnoc Enil j (l ↦ᵢ v)) Δ' = Some Δ'' ∧
+    (Δ'' ⊢ Φ (LitV (Loc l)))) →
+  Δ ⊢ WP Alloc e @ E {{ Φ }}.
+Proof.
+  intros ?? HΔ. 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 Φ :
+  IntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ᵢ{q} v)%I →
+  (Δ' ⊢ Φ v) →
+  Δ ⊢ WP Load (Lit (Loc l)) @ E {{ Φ }}.
+Proof.
+  intros. 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' →
+  IntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ᵢ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ᵢ v')) Δ' = Some Δ'' →
+  (Δ'' ⊢ Φ (LitV Unit)) →
+  Δ ⊢ WP Store (Lit (Loc l)) e @ E {{ Φ }}.
+Proof.
+  intros. 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.
+Qed.
+
+Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  IntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ᵢ{q} v)%I → v ≠ v1 →
+  (Δ' ⊢ Φ (LitV (Bool false))) →
+  Δ ⊢ WP CAS (Lit (Loc l)) e1 e2 @ E {{ Φ }}.
+Proof.
+  intros. eapply wand_apply; first exact: wp_cas_fail.
+  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
+  by apply later_mono, sep_mono_r, wand_mono.
+Qed.
 
-Ltac wp_value := iApply wp_value; eauto.
+Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  IntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ᵢ v)%I → v = v1 →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ᵢ v2)) Δ' = Some Δ'' →
+  (Δ'' ⊢ Φ (LitV (Bool true))) →
+  Δ ⊢ WP CAS (Lit (Loc l)) e1 e2 @ E {{ Φ }}.
+Proof.
+  intros; subst. eapply wand_apply; first exact: wp_cas_suc.
+  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+End heap.
+
+Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with Alloc _ => wp_bind_core K end)
+      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+    eapply tac_wp_alloc with _ H _;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       tac_rel_done || fail "wp_alloc:" e' "not a value"
+      |apply _
+      |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
+        eexists; split;
+          [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
+          |]]
+  | _ => fail "wp_alloc: not a 'wp'"
+  end.
+
+Tactic Notation "wp_alloc" ident(l) :=
+  let H := iFresh in wp_alloc l as H.
+
+Tactic Notation "wp_load" :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with Load _ => wp_bind_core K end)
+      |fail 1 "wp_load: cannot find 'Load' in" e];
+    eapply tac_wp_load;
+      [apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦ᵢ{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
+      |]
+  | _ => fail "wp_load: not a 'wp'"
+  end.
+
+Tactic Notation "wp_store" :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with Store _ _ => wp_bind_core K end)
+      |fail 1 "wp_store: cannot find 'Store' in" e];
+    eapply tac_wp_store;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       tac_rel_done || fail "wp_store:" e' "not a value"
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦ᵢ{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
+      |env_cbv; reflexivity
+      |]
+  | _ => fail "wp_store: not a 'wp'"
+  end.
+
+Tactic Notation "wp_cas_fail" :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
+      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+    eapply tac_wp_cas_fail;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       tac_rel_done || fail "wp_cas_fail:" e' "not a value"
+      |let e' := match goal with |- to_val ?e' = _ => e' end in
+       tac_rel_done || fail "wp_cas_fail:" e' "not a value"
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦ᵢ{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
+      |try congruence
+      |]
+  | _ => fail "wp_cas_fail: not a 'wp'"
+  end.
+
+Tactic Notation "wp_cas_suc" :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
+      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+    eapply tac_wp_cas_suc;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       tac_rel_done || fail "wp_cas_suc:" e' "not a value"
+      |let e' := match goal with |- to_val ?e' = _ => e' end in
+       tac_rel_done || fail "wp_cas_suc:" e' "not a value"
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦ᵢ{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+      |try congruence
+      |env_cbv; reflexivity
+      |]
+  | _ => fail "wp_cas_suc: not a 'wp'"
+  end.

theories/logrel/proofmode/tactics_rel.v

@@ -153,15 +153,19 @@ Tactic Notation "rel_let_l" := rel_rec_l.
 Tactic Notation "rel_fst_l" := rel_pure_l (Fst (Pair _ _)).
 Tactic Notation "rel_snd_l" := rel_pure_l (Snd (Pair _ _)).
 Tactic Notation "rel_proj_l" := rel_pure_l (_ (Pair _ _)).
-Tactic Notation "rel_unfold_l" := rel_pure_l (Unfold (Fold _)).
-Tactic Notation "rel_fold_l" := rel_unfold_l.
-Tactic Notation "rel_if_l" := rel_pure_l (If _ _ _).
-Tactic Notation "rel_if_true_l" := rel_pure_l (If #true _ _).
-Tactic Notation "rel_if_false_l" := rel_pure_l (If #false _ _).
 Tactic Notation "rel_case_inl_l" := rel_pure_l (Case (InjL _) _ _).
-Tactic Notation "rel_case_inr_l" := rel_pure_l (Case (InjL _) _ _).
+Tactic Notation "rel_case_inr_l" := rel_pure_l (Case (InjR _) _ _).
 Tactic Notation "rel_case_l" := rel_pure_l (Case _ _ _).
-Tactic Notation "rel_op_l" := rel_pure_l (BinOp _ _ _).
+Tactic Notation "rel_binop_l" := rel_pure_l (BinOp _ _ _).
+Tactic Notation "rel_op_l" := rel_binop_l.
+Tactic Notation "rel_if_true_l" := rel_pure_l (If #true _ _).
+Tactic Notation "rel_if_false_l" := rel_pure_l (If #false _ _).
+Tactic Notation "rel_if_l" := rel_pure_l (If _ _ _).
+Tactic Notation "rel_unfold_l" := rel_pure_l (Unfold (Fold _)).
+Tactic Notation "rel_fold_l" := rel_unfold_l.
+Tactic Notation "rel_tlam_l" := rel_pure_l (TApp (TLam _)).
+Tactic Notation "rel_unpack_l" := rel_pure_l (Unpack (Pack _) _).
+Tactic Notation "rel_pack_l" := rel_unpack_l.
 
 Lemma tac_rel_pure_r `{logrelG Σ} K e1 ℶ E1 E2 Δ Γ e e2 eres ϕ t τ :
   e = fill K e1 →
@@ -202,15 +206,19 @@ Tactic Notation "rel_ret_r" := rel_rec_r.
 Tactic Notation "rel_fst_r" := rel_pure_r (Fst (Pair _ _)).
 Tactic Notation "rel_snd_r" := rel_pure_r (Snd (Pair _ _)).
 Tactic Notation "rel_proj_r" := rel_pure_r (_ (Pair _ _)).
-Tactic Notation "rel_unfold_r" := rel_pure_r (Unfold (Fold _)).
-Tactic Notation "rel_fold_r" := rel_unfold_r.
-Tactic Notation "rel_if_r" := rel_pure_r (If _ _ _).
-Tactic Notation "rel_if_true_r" := rel_pure_r (If #true _ _).
-Tactic Notation "rel_if_false_r" := rel_pure_r (If #false _ _).
 Tactic Notation "rel_case_inl_r" := rel_pure_r (Case (InjL _) _ _).
 Tactic Notation "rel_case_inr_r" := rel_pure_r (Case (InjL _) _ _).
 Tactic Notation "rel_case_r" := rel_pure_r (Case _ _ _).
-Tactic Notation "rel_op_r" := rel_pure_r (BinOp _ _ _).
+Tactic Notation "rel_binop_r" := rel_pure_r (BinOp _ _ _).
+Tactic Notation "rel_op_r" := rel_binop_r.
+Tactic Notation "rel_if_true_r" := rel_pure_r (If #true _ _).
+Tactic Notation "rel_if_false_r" := rel_pure_r (If #false _ _).
+Tactic Notation "rel_if_r" := rel_pure_r (If _ _ _).
+Tactic Notation "rel_unfold_r" := rel_pure_r (Unfold (Fold _)).
+Tactic Notation "rel_fold_r" := rel_unfold_r.
+Tactic Notation "rel_tlam_r" := rel_pure_r (TApp (TLam _)).
+Tactic Notation "rel_unpack_r" := rel_pure_r (Unpack (Pack _) _).
+Tactic Notation "rel_pack_r" := rel_unpack_r.
 
 (** Stateful reductions *)
 

theories/logrel/proofmode/tactics_threadpool.v

@@ -212,19 +212,25 @@ Tactic Notation "tp_pure" constr(j) open_constr(ef) :=
     |simpl_subst (* new goal *)].
 
 Tactic Notation "tp_pure" constr(j) := tp_pure j _.
-(* TODO: All the pure reduction should be implemented like this *)
 Tactic Notation "tp_rec" constr(j) := tp_pure j (App (Rec _ _ _) _).
-Tactic Notation "tp_binop" constr(j) := tp_pure j (BinOp _ _ _).
-Tactic Notation "tp_op" constr(j) := tp_binop j.
-Tactic Notation "tp_fold" constr(j) := tp_pure j (Unfold (Fold _)).
+Tactic Notation "tp_seq" constr(j) := tp_rec j.
+Tactic Notation "tp_let" constr(j) := tp_rec j.
 Tactic Notation "tp_fst" constr(j) := tp_pure j (Fst (Pair _ _)).
 Tactic Notation "tp_snd" constr(j) := tp_pure j (Snd (Pair _ _)).
+Tactic Notation "tp_proj" constr(j) := tp_pure j (_ (Pair _ _)).
 Tactic Notation "tp_case_inl" constr(j) := tp_pure j (Case (InjL _) _ _).
 Tactic Notation "tp_case_inr" constr(j) := tp_pure j (Case (InjR _) _ _).
 Tactic Notation "tp_case" constr(j) := tp_pure j (Case _ _ _).
+Tactic Notation "tp_binop" constr(j) := tp_pure j (BinOp _ _ _).
+Tactic Notation "tp_op" constr(j) := tp_binop j.
 Tactic Notation "tp_if_true" constr(j) := tp_pure j (If #true _ _).
 Tactic Notation "tp_if_false" constr(j) := tp_pure j (If #false _ _).
 Tactic Notation "tp_if" constr(j) := tp_pure j (If _ _ _).
+Tactic Notation "tp_unfold" constr(j) := tp_pure j (Unfold (Fold _)).
+Tactic Notation "tp_fold" constr(j) := tp_unfold j.
+Tactic Notation "tp_tlam" constr(j) := tp_pure j (TApp (TLam _)).
+Tactic Notation "tp_unpack" constr(j) := tp_pure j (Unpack (Pack _) _).
+Tactic Notation "tp_pack" constr(j) := tp_unpack j.
 
 Lemma tac_tp_cas_fail `{logrelG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l e1 e2 v' v1 v2 Q q :
   nclose specN ⊆ E1 →

theories/tests/tactics.v

+From iris.proofmode Require Import tactics.
 From iris_logrel.F_mu_ref_conc Require Export tactics notation.
 
 Lemma wp_rec1 `{heapG Σ} Φ :
@@ -8,7 +9,7 @@ Proof.
   wp_rec.
   wp_rec.
   wp_op.
-  wp_value.
+  by wp_value.
 Qed.
 
 Lemma wp_proj2 `{heapG Σ} Φ :
@@ -18,6 +19,5 @@ Proof.
   iIntros "HΦ".
   wp_proj.
   wp_proj.
-  wp_value.
+  by wp_value.
 Qed.
-

theories/tests/tactics2.v

-From iris.proofmode Require Import coq_tactics sel_patterns.
+From iris.proofmode Require Import tactics. 
 From iris_logrel.logrel Require Export rules_threadpool proofmode.tactics_threadpool logrel_binary.
 Set Default Proof Using "Type".
 Import lang.