From 8076fe3995be78f76e6eaa73b96713e09f403198 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Oct 2017 11:28:11 +0900
Subject: [PATCH] Total weakest preconditions for heap_lang.

---
 _CoqProject                         |   1 +
 theories/heap_lang/lifting.v        | 137 +++++++++++++-----
 theories/heap_lang/proofmode.v      | 211 +++++++++++++++++++++++++---
 theories/heap_lang/total_adequacy.v |  15 ++
 4 files changed, 308 insertions(+), 56 deletions(-)
 create mode 100644 theories/heap_lang/total_adequacy.v

diff --git a/_CoqProject b/_CoqProject
index e82f46f95..338f805ac 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -79,6 +79,7 @@ theories/heap_lang/lib/ticket_lock.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
+theories/heap_lang/total_adequacy.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 5369e0a9a..94c8b1e89 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,14 +1,11 @@
 From iris.base_logic Require Export gen_heap.
-From iris.program_logic Require Export weakestpre lifting.
-From iris.program_logic Require Import ectx_lifting.
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
-Import uPred.
-
-(** Basic rules for language operations. *)
 
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
@@ -39,8 +36,6 @@ Ltac inv_head_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | H : _ = of_val ?v |- _ =>
-     is_var v; destruct v; first[discriminate H|injection H as H]
   | H : head_step ?e _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
      and can thus better be avoided. *)
@@ -54,22 +49,6 @@ Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Section lifting.
-Context `{heapG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types efs : list expr.
-Implicit Types σ : state.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork s E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
-Proof.
-  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id.
-  - 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_pure_exec :=
@@ -79,48 +58,69 @@ Local Ltac solve_pure_exec :=
 
 Class AsRec (e : expr) (f x : binder) (erec : expr) :=
   as_rec : e = Rec f x erec.
-Global Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
-Global Instance AsRec_rec_locked_val v f x e :
+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.
 
-Global Instance pure_rec f x (erec e1 e2 : expr)
+Instance pure_rec f x (erec e1 e2 : expr)
     `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
   PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
 Proof. unfold AsRec in *; solve_pure_exec. Qed.
 
-Global Instance pure_unop op e v v' `{!IntoVal e v} :
+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_pure_exec. Qed.
 
-Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
+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_pure_exec. Qed.
 
-Global Instance pure_if_true e1 e2 :
-  PureExec True (If (Lit (LitBool true)) e1 e2) e1.
+Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_if_false e1 e2 :
-  PureExec True (If (Lit (LitBool false)) e1 e2) e2.
+Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
+Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
   PureExec True (Fst (Pair e1 e2)) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
+Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
+Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
+Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
 Proof. solve_pure_exec. Qed.
 
+Section lifting.
+Context `{heapG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types efs : list expr.
+Implicit Types σ : state.
+
+(** Base axioms for core primitives of the language: Stateless reductions *)
+Lemma wp_fork s E e Φ :
+  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
+Proof.
+  iIntros "[HΦ He]".
+  iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
+Qed.
+Lemma twp_fork s E e Φ :
+  Φ (LitV LitUnit) ∗ WP e @ s; ⊤ [{ _, True }] ⊢ WP Fork e @ s; E [{ Φ }].
+Proof.
+  iIntros "[HΦ He]".
+  iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iIntros "!> /= {$He}". by iApply twp_value.
+Qed.
+
 (** Heap *)
 Lemma wp_alloc s E e v :
   IntoVal e v →
@@ -132,6 +132,16 @@ Proof.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_alloc s E e v :
+  IntoVal e v →
+  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>"; iSplit; first by auto.
+  iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_load s E l q v :
   {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
@@ -142,6 +152,15 @@ Proof.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_load s E l q v :
+  [[{ l ↦{q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l ↦{q} v }]].
+Proof.
+  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto.
+  iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_store s E l v' e v :
   IntoVal e v →
@@ -154,6 +173,17 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_store s E l v' e v :
+  IntoVal e v →
+  [[{ l ↦ v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l ↦ v }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 
 Lemma wp_cas_fail s E l q v' e1 v1 e2 :
   IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
@@ -166,6 +196,17 @@ Proof.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_cas_fail s E l q v' e1 v1 e2 :
+  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
+  [[{ l ↦{q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+  [[{ RET LitV (LitBool false); l ↦{q} v' }]].
+Proof.
+  iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 → IntoVal e2 v2 →
@@ -179,6 +220,18 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_cas_suc s E l e1 v1 e2 v2 :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  [[{ l ↦ v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+  [[{ RET LitV (LitBool true); l ↦ v2 }]].
+Proof.
+  iIntros (<-%of_to_val <-%of_to_val Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 
 Lemma wp_faa s E l i1 e2 i2 :
   IntoVal e2 (LitV (LitInt i2)) →
@@ -192,4 +245,16 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_faa s E l i1 e2 i2 :
+  IntoVal e2 (LitV (LitInt i2)) →
+  [[{ l ↦ LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
+  [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 End lifting.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a88e47559..24a22025c 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
@@ -9,10 +9,15 @@ Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
   e = e' →
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
+Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
+  e = e' →
+  envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
+Proof. by intros ->. Qed.
 
 Tactic Notation "wp_expr_eval" tactic(t) :=
   try iStartProof;
-  try (eapply tac_wp_expr_eval; [t; reflexivity|]).
+  try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
+       [t; reflexivity|]).
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
@@ -25,16 +30,28 @@ Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
   envs_entails Δ (WP e1 @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
-  rewrite HΔ' -wp_pure_step_later //.
+  rewrite HΔ' -lifting.wp_pure_step_later //.
+Qed.
+Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
+  PureExec φ e1 e2 →
+  φ →
+  envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
+  envs_entails Δ (WP e1 @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ?? ->. rewrite -total_lifting.twp_pure_step //.
 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=> ? ->. by apply 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=> ? ->. by apply twp_value. Qed.
 
 Ltac wp_value_head :=
-  eapply tac_wp_value;
+  first [eapply tac_wp_value || eapply tac_twp_value];
     [apply _
     |iEval (lazy beta; simpl of_val)].
 
@@ -51,7 +68,17 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       |apply _                        (* IntoLaters *)
       |wp_expr_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: cannot find" efoc "in" e "or" efoc "is not a reduct"
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    let e := eval simpl in e in
+    reshape_expr e ltac:(fun K e' =>
+      unify e' efoc;
+      eapply (tac_twp_pure _ _ _ (fill K e'));
+      [apply _                        (* PureExec *)
+      |try fast_done                  (* The pure condition for PureExec *)
+      |wp_expr_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.
 
@@ -74,12 +101,22 @@ Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
   envs_entails Δ (WP e @ s; E {{ v, WP f (of_val v) @ s; E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
+Lemma tac_twp_bind `{heapG Σ} K Δ s E Φ e f :
+  f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
+  envs_entails Δ (WP e @ s; E [{ v, WP f (of_val v) @ s; E [{ Φ }] }])%I →
+  envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
+Proof. rewrite /envs_entails=> -> ->. by apply: twp_bind. Qed.
 
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
   | [] => idtac
   | _ => eapply (tac_wp_bind K); [simpl; reflexivity|lazy beta]
   end.
+Ltac twp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|lazy beta]
+  end.
 
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
@@ -87,6 +124,9 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
     || fail "wp_bind: cannot find" efoc "in" e
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
+    || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
@@ -111,6 +151,19 @@ Proof.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
+Lemma tac_twp_alloc Δ s E j K e v Φ :
+  IntoVal e v →
+  (∀ l, ∃ Δ',
+    envs_app false (Esnoc Enil j (l ↦ v)) Δ = Some Δ' ∧
+    envs_entails Δ' (WP fill K (Lit (LitLoc l)) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (Alloc e) @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ? HΔ.
+  rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
+  rewrite left_id. apply forall_intro=> l.
+  destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
+  by rewrite right_id HΔ'.
+Qed.
 
 Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
@@ -123,6 +176,16 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+Lemma tac_twp_load Δ s E i K l q v Φ :
+  envs_lookup i Δ = Some (false, l ↦{q} v)%I →
+  envs_entails Δ (WP fill K (of_val v) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ??.
+  rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
+  rewrite envs_lookup_split //; simpl.
+  by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
   IntoVal e v' →
@@ -137,6 +200,17 @@ Proof.
   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_twp_store Δ Δ' s E i K l v e v' Φ :
+  IntoVal e v' →
+  envs_lookup i Δ = Some (false, l ↦ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ = Some Δ' →
+  envs_entails Δ' (WP fill K (Lit LitUnit) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E [{ Φ }]).
+Proof.
+  intros. rewrite -twp_bind. eapply wand_apply; first by eapply twp_store.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
@@ -150,6 +224,15 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
+  IntoVal e1 v1 → AsVal e2 →
+  envs_lookup i Δ = Some (false, l ↦{q} v)%I → v ≠ v1 →
+  envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+Proof.
+  intros. rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_fail.
+  rewrite envs_lookup_split //; simpl. by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
@@ -164,6 +247,17 @@ Proof.
   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_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  envs_lookup i Δ = Some (false, l ↦ v)%I → v = v1 →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
+  envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+Proof.
+  intros; subst. rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
   IntoVal e2 (LitV (LitInt i2)) →
@@ -178,6 +272,18 @@ Proof.
   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_twp_faa Δ Δ' s E i K l i1 e2 i2 Φ :
+  IntoVal e2 (LitV (LitInt i2)) →
+  envs_lookup i Δ = Some (false, l ↦ LitV (LitInt i1))%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (i1 + i2)))) Δ = Some Δ' →
+  envs_entails Δ' (WP fill K (Lit (LitInt i1)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ????; subst.
+  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ i1 _ i2).
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
@@ -189,10 +295,21 @@ Tactic Notation "wp_apply" open_constr(lem) :=
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
+    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+      reshape_expr e ltac:(fun K e' =>
+        twp_bind_core K; iApplyHyp H; wp_expr_simpl) ||
+      lazymatch iTypeOf H with
+      | Some (_,?P) => fail "wp_apply: cannot apply" P
+      end
     | _ => fail "wp_apply: not a 'wp'"
     end).
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
+  let finish _ :=
+    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
+      eexists; split;
+        [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
+        |wp_expr_simpl; try wp_value_head] in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -201,10 +318,13 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
          eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     [apply _
-    |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
-      eexists; split;
-        [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
-        |wp_expr_simpl; try wp_value_head]]
+    |finish ()]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_alloc _ _ _ H K); [apply _|..])
+      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+    finish ()
   | _ => fail "wp_alloc: not a 'wp'"
   end.
 
@@ -212,6 +332,9 @@ Tactic Notation "wp_alloc" ident(l) :=
   let H := iFresh in wp_alloc l as H.
 
 Tactic Notation "wp_load" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -219,13 +342,23 @@ Tactic Notation "wp_load" :=
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |wp_expr_simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ _ K))
+      |fail 1 "wp_load: cannot find 'Load' in" e];
+    [solve_mapsto ()
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_load: not a 'wp'"
   end.
 
 Tactic Notation "wp_store" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
+  let finish _ :=
+    wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head] in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -234,14 +367,24 @@ Tactic Notation "wp_store" :=
          eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |env_cbv; reflexivity
+    |finish ()]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_store _ _ _ _ _ K); [apply _|..])
+      |fail 1 "wp_store: cannot find 'Store' in" e];
+    [solve_mapsto ()
     |env_cbv; reflexivity
-    |wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
+    |finish ()]
   | _ => fail "wp_store: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_fail" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -250,14 +393,24 @@ Tactic Notation "wp_cas_fail" :=
          eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |try congruence
+    |simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_cas_fail _ _ _ _ K); [apply _|apply _|..])
+      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+    [solve_mapsto ()
     |try congruence
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_fail: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_suc" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -266,8 +419,16 @@ Tactic Notation "wp_cas_suc" :=
          eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |try congruence
+    |env_cbv; reflexivity
+    |simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
+      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+    [solve_mapsto ()
     |try congruence
     |env_cbv; reflexivity
     |wp_expr_simpl; try wp_value_head]
@@ -275,6 +436,9 @@ Tactic Notation "wp_cas_suc" :=
   end.
 
 Tactic Notation "wp_faa" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -283,8 +447,15 @@ Tactic Notation "wp_faa" :=
          eapply (tac_wp_faa _ _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |env_cbv; reflexivity
+    |wp_expr_simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_faa _ _ _ _ _ K); [apply _|..])
+      |fail 1 "wp_faa: cannot find 'CAS' in" e];
+    [solve_mapsto ()
     |env_cbv; reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_faa: not a 'wp'"
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
new file mode 100644
index 000000000..55e7f5f5e
--- /dev/null
+++ b/theories/heap_lang/total_adequacy.v
@@ -0,0 +1,15 @@
+From iris.program_logic Require Export total_adequacy.
+From iris.heap_lang Require Export adequacy.
+From iris.heap_lang Require Import proofmode notation.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Definition heap_total Σ `{heapPreG Σ} s e σ φ :
+  (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
+  sn step ([e], σ).
+Proof.
+  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
+  iMod (gen_heap_init σ) as (?) "Hh".
+  iModIntro. iExists gen_heap_ctx; iFrame.
+  iApply (Hwp (HeapG _ _ _)).
+Qed.
-- 
GitLab