From 2b9a48be7bd9c288b78306f992eacf9b858554b6 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 24 Jan 2017 10:45:50 +0100
Subject: [PATCH] Try to stay up to date wrt heaplang's proofmode.v.

---
 _CoqProject                      |   1 -
 theories/lang/derived.v          |  21 ++--
 theories/lang/lifting.v          |   2 +-
 theories/lang/proofmode.v        | 162 ++++++++++++++++++++++++++++---
 theories/lang/wp_tactics.v       | 129 ------------------------
 theories/typing/borrow.v         |   9 +-
 theories/typing/programs.v       |   6 +-
 theories/typing/soundness.v      |   2 +-
 theories/typing/type_sum.v       |  12 +--
 theories/typing/unsafe/refcell.v |  50 ++++++++++
 10 files changed, 224 insertions(+), 170 deletions(-)
 delete mode 100644 theories/lang/wp_tactics.v

diff --git a/_CoqProject b/_CoqProject
index 60996da1..16db149f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -23,7 +23,6 @@ theories/lang/notation.v
 theories/lang/proofmode.v
 theories/lang/races.v
 theories/lang/tactics.v
-theories/lang/wp_tactics.v
 theories/typing/type.v
 theories/typing/lft_contexts.v
 theories/typing/type_context.v
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index c3c5be5e..f72861cf 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -67,13 +67,14 @@ Proof.
 Qed.
 
 (** Proof rules for the sugar *)
-Lemma wp_lam E xl e e' el Φ :
+Lemma wp_lam E xl e eb e' el Φ :
+  e = Lam xl eb →
   Forall (λ ei, is_Some (to_val ei)) el →
-  Closed (xl +b+ []) e →
-  subst_l xl el e = Some e' →
-  ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
+  Closed (xl +b+ []) eb →
+  subst_l xl el eb = Some e' →
+  ▷ WP e' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
 Proof.
-  iIntros (???) "?". iApply (wp_rec _ _ BAnon)=>//.
+  iIntros (-> ???) "?". iApply (wp_rec _ _ BAnon)=>//.
     by rewrite /= option_fmap_id.
 Qed.
 
@@ -99,8 +100,8 @@ Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
 Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P -∗ ▷ |={E}=> Φ (LitV true)) →
-  (n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
+  (n1 ≤ n2 → P -∗ ▷ Φ (LitV true)) →
+  (n2 < n1 → P -∗ ▷ Φ (LitV false)) →
   P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   iIntros (Hl Hg) "HP". iApply wp_fupd.
@@ -110,7 +111,7 @@ Proof.
 Qed.
 
 Lemma wp_offset E l z Φ :
-  ▷ (|={E}=> Φ (LitV $ LitLoc $ shift_loc l z)) -∗
+  ▷ Φ (LitV $ LitLoc $ shift_loc l z) -∗
     WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
 Proof.
   iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
@@ -118,7 +119,7 @@ Proof.
 Qed.
 
 Lemma wp_plus E z1 z2 Φ :
-  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 + z2)) -∗
+  ▷ Φ (LitV $ LitInt $ z1 + z2) -∗
     WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
 Proof.
   iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
@@ -126,7 +127,7 @@ Proof.
 Qed.
 
 Lemma wp_minus E z1 z2 Φ :
-  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 - z2)) -∗
+  ▷ Φ (LitV $ LitInt $ z1 - z2) -∗
     WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
 Proof.
   iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index ede4cd0f..b8f0cab8 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -144,7 +144,7 @@ Proof.
 Qed.
 
 Lemma wp_rec E e f xl erec erec' el Φ :
-  e = Rec f xl erec → (* to avoids recursive calls being unfolded *)
+  e = Rec f xl erec →
   Forall (λ ei, is_Some (to_val ei)) el →
   Closed (f :b: xl +b+ []) erec →
   subst_l (f::xl) (e::el) erec = Some erec' →
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 44a89ce8..c606d13e 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,11 +1,140 @@
+From iris.base_logic Require Import namespaces.
+From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
-From iris.base_logic Require Import namespaces.
-From lrust.lang Require Export wp_tactics heap.
+From lrust.lang Require Export tactics derived heap.
 Set Default Proof Using "Type".
 Import uPred.
 
-Ltac wp_strip_later ::= iNext.
+(** wp-specific helper tactics *)
+Ltac wp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
+  end.
+
+(* Solves side-conditions generated by the wp tactics *)
+Ltac wp_done :=
+  match goal with
+  | |- Closed _ _ => solve_closed
+  | |- is_Some (to_val _) => solve_to_val
+  | |- to_val _ = Some _ => solve_to_val
+  | |- language.to_val _ = Some _ => solve_to_val
+  | |- Forall _ [] => fast_by apply List.Forall_nil
+  | |- Forall _ (_ :: _) => apply List.Forall_cons; wp_done
+  | _ => fast_done
+  end.
+
+Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
+
+Ltac wp_seq_head :=
+  lazymatch goal with
+  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+    etrans; [|eapply wp_seq; wp_done]; iNext
+  end.
+
+Ltac wp_finish := intros_revert ltac:(
+  rewrite /= ?to_of_val;
+  try iNext;
+  repeat lazymatch goal with
+  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+     etrans; [|eapply wp_seq; wp_done]; iNext
+  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
+  end).
+
+Tactic Notation "wp_value" :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
+  | _ => fail "wp_value: not a wp"
+  end.
+
+Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
+Proof. by unlock. Qed.
+
+(* 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; 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;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with
+    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
+    | BinOp OffsetOp _ _ =>
+       wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
+    | BinOp PlusOp _ _ =>
+       wp_bind_core K; etrans; [|eapply wp_plus; try fast_done]; wp_finish
+    | BinOp MinusOp _ _ =>
+       wp_bind_core K; etrans; [|eapply wp_minus; try fast_done]; wp_finish
+    end) || fail "wp_op: cannot find 'BinOp' in" e
+  | _ => fail "wp_op: not a 'wp'"
+  end.
+
+Tactic Notation "wp_if" :=
+  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]; wp_finish
+    end) || fail "wp_if: cannot find 'If' in" e
+  | _ => fail "wp_if: not a 'wp'"
+  end.
+
+Tactic Notation "wp_case" :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with
+    | Case _ _ _ =>
+      wp_bind_core K;
+      etrans; [|eapply wp_case; wp_done];
+      simpl_subst; wp_finish
+    end) || fail "wp_case: cannot find 'Case' in" e
+  | _ => fail "wp_case: not a 'wp'"
+  end.
+
+Tactic Notation "wp_bind" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match e' with
+    | efoc => unify e' efoc; wp_bind_core K
+    end) || fail "wp_bind: cannot find" efoc "in" e
+  | _ => fail "wp_bind: not a 'wp'"
+  end.
 
 Section heap.
 Context `{heapG Σ}.
@@ -19,7 +148,7 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   (∀ l vl, n = length vl → ∃ Δ'',
     envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
       = Some Δ'' ∧
-    (Δ'' ⊢ |={E}=> Φ (LitV $ LitLoc l))) →
+    (Δ'' ⊢ Φ (LitV $ LitLoc l))) →
   Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
 Proof.
   intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
@@ -28,7 +157,7 @@ Proof.
   apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
   apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
   destruct (HΔ l vl) as (Δ''&?&HΔ'). done.
-  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ' -fupd_intro.
 Qed.
 
 Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
@@ -39,32 +168,32 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   envs_lookup i2 Δ'' = Some (false, †l…n')%I →
   envs_delete i2 false Δ'' = Δ''' →
   n' = length vl →
-  (Δ''' ⊢ |={E}=> Φ (LitV LitUnit)) →
+  (Δ''' ⊢ Φ (LitV LitUnit)) →
   Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
   eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_laterN_env_sound -!later_sep; apply later_mono.
-  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True.
+  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True -fupd_intro.
 Qed.
 
 Lemma tac_wp_read Δ Δ' E i l q v o Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ |={E}=> Φ v) →
+  (Δ' ⊢ Φ v) →
   Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   intros ??[->| ->]???.
   - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-      by apply later_mono, sep_mono_r, wand_mono.
+      rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
   - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-      by apply later_mono, sep_mono_r, wand_mono.
+      rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
@@ -73,29 +202,31 @@ Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
+  (Δ'' ⊢ Φ (LitV LitUnit)) →
   Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
 Proof.
   intros ???[->| ->]????.
   - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
-    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+    rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
   - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
-    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+    rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; iApply lem; try iNext)
+    wp_bind_core K; iApply lem; try iNext; simpl)
   | _ => fail "wp_apply: not a 'wp'"
   end.
 
 Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
@@ -118,6 +249,7 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) :=
   let H := iFresh in let Hf := iFresh in wp_alloc l vl as H Hf.
 
 Tactic Notation "wp_free" :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
@@ -141,6 +273,7 @@ Tactic Notation "wp_free" :=
   end.
 
 Tactic Notation "wp_read" :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
@@ -160,6 +293,7 @@ Tactic Notation "wp_read" :=
   end.
 
 Tactic Notation "wp_write" :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
diff --git a/theories/lang/wp_tactics.v b/theories/lang/wp_tactics.v
deleted file mode 100644
index f4d6c053..00000000
--- a/theories/lang/wp_tactics.v
+++ /dev/null
@@ -1,129 +0,0 @@
-From lrust.lang Require Export tactics derived.
-Set Default Proof Using "Type".
-Import uPred.
-
-(** wp-specific helper tactics *)
-Ltac wp_bind_core K :=
-  lazymatch eval hnf in K with
-  | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
-  end.
-
-(* FIXME : the [reflexivity] tactic is not able to solve trivial
-   reflexivity proofs, while [exact (reflexivity _)] does. *)
-Ltac wp_done :=
-  rewrite /= ?to_of_val;
-  match goal with
-  | |- _ = _ => exact (reflexivity _)
-  | |- Forall _ [] => fast_by apply List.Forall_nil
-  | |- Forall _ (_ :: _) => apply List.Forall_cons; wp_done
-  | |- is_Some (Some ?v) => exists v; reflexivity
-  | |- _ => fast_done
-  end.
-
-(* sometimes, we will have to do a final view shift, so only apply
-pvs_intro if we obtain a consecutive wp *)
-Ltac wp_strip_pvs :=
-  lazymatch goal with
-  | |- _ ⊢ |={?E}=> _ =>
-    etrans; [|apply fupd_intro];
-    match goal with |- _ ⊢ wp E _ _ => simpl | _ => fail end
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value_fupd; wp_done]; lazy beta.
-
-Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
-
-Ltac wp_seq_head :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-    etrans; [|eapply wp_seq; wp_done]; wp_strip_later
-  end.
-
-Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val;
-  try wp_strip_later;
-  repeat lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-     etrans; [|eapply wp_seq; wp_done]; wp_strip_later
-  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
-  | |- _ ⊢ |={_}=> _ => wp_strip_pvs
-  end).
-
-Tactic Notation "wp_value" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
-  | _ => fail "wp_value: not a wp"
-  end.
-
-Tactic Notation "wp_rec" :=
-  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; 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" :=
-  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; 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" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
-    | BinOp OffsetOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
-    | BinOp PlusOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_plus; try fast_done]; wp_finish
-    | BinOp MinusOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_minus; try fast_done]; wp_finish
-    end) || fail "wp_op: cannot find 'BinOp' in" e
-  | _ => fail "wp_op: not a 'wp'"
-  end.
-
-Tactic Notation "wp_if" :=
-  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]; wp_finish
-    end) || fail "wp_if: cannot find 'If' in" e
-  | _ => fail "wp_if: not a 'wp'"
-  end.
-
-Tactic Notation "wp_case" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Case _ _ _ =>
-      wp_bind_core K;
-      etrans; [|eapply wp_case; wp_done];
-      simpl_subst; wp_finish
-    end) || fail "wp_case: cannot find 'Case' in" e
-  | _ => fail "wp_case: not a 'wp'"
-  end.
-
-Tactic Notation "wp_bind" open_constr(efoc) :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match e' with
-    | efoc => unify e' efoc; wp_bind_core K
-    end) || fail "wp_bind: cannot find" efoc "in" e
-  | _ => fail "wp_bind: not a 'wp'"
-  end.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index cc94d5a1..f43fa84a 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -54,7 +54,7 @@ Section borrow.
       (try iDestruct "Hown" as "[]").
     iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
-      iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton. wp_read.
+      iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
     iMod ("Hclose'" $! (l↦#l' ∗ freeable_sz n (ty_size ty) l' ∗ _)%I
           with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
     - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
@@ -88,7 +88,7 @@ Section borrow.
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
     - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[#Hshr Htok2]".
+    - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
       iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
       iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
       rewrite tctx_interp_singleton tctx_hasty_val' //. auto.
@@ -123,7 +123,7 @@ Section borrow.
     rewrite heap_mapsto_vec_singleton.
     iApply (wp_fupd_step  _ (⊤∖↑lftN) with "[Hbor]"); try done.
       by iApply (bor_unnest with "LFT Hbor").
-    wp_read. iIntros "!> Hbor".
+    iApply wp_fupd. wp_read. iIntros "!> Hbor".
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
     iMod ("Hclose" with "Htok") as "($ & $)".
     rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -157,7 +157,8 @@ Section borrow.
     iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
     iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
     - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[#Hshr Htok2]". iMod ("Hclose''" with "Htok2") as "Htok2".
+    - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
+      iMod ("Hclose''" with "Htok2") as "Htok2".
       iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
       iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
       rewrite tctx_interp_singleton tctx_hasty_val' //.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index c35802f3..acd60687 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -154,7 +154,7 @@ Section typing_rules.
     iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_fupd_step with "Hend"); try done. wp_seq.
-    iIntros "!> #Hdead !>". wp_seq. iApply (He with "HEAP LFT Htl HE HL HC >").
+    iIntros "#Hdead !>". wp_seq. iApply (He with "HEAP LFT Htl HE HL HC >").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
 
@@ -186,7 +186,7 @@ Section typing_rules.
     iMod (Hwrt with "* [] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
     subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
-    rewrite heap_mapsto_vec_singleton. wp_write.
+    rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_write.
     rewrite -heap_mapsto_vec_singleton.
     iMod ("Hclose" with "* [Hl Hown2]") as "($ & $ & Hown)".
     { iExists _. iFrame. }
@@ -212,7 +212,7 @@ Section typing_rules.
         (l vl q) "(% & Hl & Hown & Hclose)"; first done.
     subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
     destruct vl as [|v [|]]; try done.
-    rewrite heap_mapsto_vec_singleton. wp_read.
+    rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
     iMod ("Hclose" with "Hl") as "($ & $ & Hown2)".
     rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
     by iFrame.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 674fdaa2..502f7efc 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -54,7 +54,7 @@ Section type_soundness.
     iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl HE HL []");
       last by rewrite tctx_interp_nil.
     iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
-    inv_vec args. iIntros (x) "_". by wp_seq.
+    inv_vec args. iIntros (x) "_ /=". by wp_lam.
   Qed.
 End type_soundness.
 
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 2d21fb76..92828b31 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -156,15 +156,14 @@ Section case.
     iMod (Hw with "* [] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
     destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
-    wp_write. iApply wp_seq. done. iNext. wp_bind p1.
-    iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
+    wp_write. wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
     iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2").
     iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
     destruct vl as [|? vl].
     { exfalso. revert i Hty. clear - Hlen Hlenty. induction tyl=>//= -[|i] /=.
       - intros [= ->]. simpl in *. lia.
       - apply IHtyl. simpl in *. lia. }
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
+    rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
     rewrite tctx_interp_singleton tctx_hasty_val' //. iApply "Hw". iNext.
     iExists (_::_::_). rewrite !heap_mapsto_vec_cons. iFrame.
     iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
@@ -192,7 +191,7 @@ Section case.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
     iMod (Hw with "* [] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
     simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
+    rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
     iApply "Hw". iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
     iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
@@ -225,9 +224,8 @@ Section case.
     iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
     iMod (Hw with "* [] LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
     destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
-    iApply wp_seq. done. iNext. wp_bind p1.
-    iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
+    rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
+    wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
     wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
     iMod (Hr with "* [] LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=.
     subst. assert (ty.(ty_size) ≤ length vl1).
diff --git a/theories/typing/unsafe/refcell.v b/theories/typing/unsafe/refcell.v
index d670fe96..ce50af70 100644
--- a/theories/typing/unsafe/refcell.v
+++ b/theories/typing/unsafe/refcell.v
@@ -391,3 +391,53 @@ End refmut.
 
 Hint Resolve refcell_mono' refcell_proper' ref_mono' ref_proper'
              refmut_mono' refmut_proper' : lrust_typing.
+
+(* Section refcell_functions. *)
+(*   Context `{typeG Σ, refcellG Σ}. *)
+
+(*   (* Constructing a cell. *) *)
+(*   Definition refcell_new ty : val := *)
+(*     funrec: <> ["x"] := *)
+(*       let: "r" := new [ #(S ty.(ty_size))] in *)
+(*       "r" +â‚— #0 <- #0;; *)
+(*       "r" +â‚— #1 <-{ty.(ty_size)} !"x";; *)
+(*       "k" ["r"] *)
+(*       cont: "k" ["r"] := *)
+(*         delete [ #ty.(ty_size) ; "x"];; "return" ["r"]. *)
+
+(*   Lemma refcell_new_type ty : *)
+(*     typed_instruction_ty [] [] [] (refcell_new ty) *)
+(*         (fn (λ _, [])%EL (λ _, [# ty]) (λ _:(), refcell ty)). *)
+(*   Proof. *)
+(*     apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst. *)
+(*     eapply (type_cont [_] [] *)
+(*          (λ r, [x ◁ box (uninit ty.(ty_size)); r!!!0 ◁ box (refcell ty)])%TC); *)
+(*       [solve_typing..| |]; last first. *)
+(*     - simpl. intros k arg. inv_vec arg=>r. simpl_subst. *)
+(*       eapply type_delete; [solve_typing..|]. *)
+(*       eapply (type_jump [_]); solve_typing. *)
+(*     - intros k. simpl_subst. eapply type_new; [solve_typing..|]. *)
+(*       iIntros (r) "!# * #HEAP #LFT Hna HE _ Hk HT". simpl_subst. *)
+(*       rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons *)
+(*               tctx_interp_singleton !tctx_hasty_val. *)
+(*       iDestruct "HT" as "[Hr Hx]". *)
+(*       destruct x as [[]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]". *)
+(*       destruct r as [[]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]". *)
+(*       iDestruct "Hr" as (vl) "Hr". rewrite uninit_own. iDestruct "Hr" as "[Hr↦ >%]". *)
+(*       destruct vl as [|]; try done. rewrite heap_mapsto_vec_cons. *)
+(*       iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op. rewrite shift_loc_0. wp_write. *)
+
+(* etrans. admit. apply wp_lam. wp_done. apply _. wp_done. *)
+(* wp_seq. *)
+
+(*  simpl *)
+
+(*  simpl. *)
+(* simpl. *)
+(*       simpl_subst. *)
+
+(*     eapply type_new; [solve_typing..|]=>r. simpl_subst. *)
+
+(*     eapply (type_jump [_]); first solve_typing. *)
+(*     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done. *)
+(*   Qed. *)
-- 
GitLab