From 627509b934fd7363a97b2d6fee738c2bcf05e099 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 27 Oct 2016 23:29:20 +0200
Subject: [PATCH] Use Texan triples, and better treatement of valuable
 expressions. They are just expressions.

---
 _CoqProject |   1 -
 adequacy.v  |   4 +-
 heap.v      | 122 +++++++++---------
 lifting.v   |  92 +++++++-------
 memcpy.v    |   9 +-
 perm.v      |  45 ++++++-
 perm_incl.v |  62 +++++-----
 proofmode.v |  17 +--
 type_incl.v |   6 +-
 typing.v    | 350 ++++++++++++++++++++++++++--------------------------
 valuable.v  |  30 -----
 11 files changed, 374 insertions(+), 364 deletions(-)
 delete mode 100644 valuable.v

diff --git a/_CoqProject b/_CoqProject
index 6ef94ecd..9769f2a7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,7 +13,6 @@ wp_tactics.v
 lifetime.v
 type.v
 type_incl.v
-valuable.v
 perm.v
 perm_incl.v
 typing.v
diff --git a/adequacy.v b/adequacy.v
index a7936698..77e67483 100644
--- a/adequacy.v
+++ b/adequacy.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export weakestpre adequacy.
+From iris.program_logic Require Export hoare adequacy.
 From lrust Require Export heap.
 From iris.algebra Require Import auth.
 From lrust Require Import proofmode notation.
@@ -17,7 +17,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. intros [? [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv. split; apply _. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ■ φ v }}) →
+  (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ■ φ v }}) →
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ). iIntros (?) "Hσ".
diff --git a/heap.v b/heap.v
index 44d19463..60e29665 100644
--- a/heap.v
+++ b/heap.v
@@ -95,7 +95,6 @@ Notation "† l … n" := (heap_freeable l 1 n) (at level 20) : uPred_scope.
 Section heap.
   Context {Σ : gFunctors}.
   Implicit Types P Q : iProp Σ.
-  Implicit Types Φ : val → iProp Σ.
   Implicit Types σ : state.
 
   (** Allocation *)
@@ -105,7 +104,7 @@ Section heap.
   Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
   Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
 
-  Lemma to_heap_insert σ l x v : 
+  Lemma to_heap_insert σ l x v :
     to_heap (<[l:=(x, v)]> σ)
     = <[l:=(1%Qp, to_lock_stateR x, DecAgree v)]> (to_heap σ).
   Proof. by rewrite /to_heap fmap_insert. Qed.
@@ -324,17 +323,15 @@ Section heap.
     rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
   Qed.
 
-  Lemma wp_alloc E n Φ :
+  Lemma wp_alloc E n :
     nclose heapN ⊆ E → 0 < n →
-    heap_ctx ★
-    ▷ (∀ l vl, n = length vl ★ †l…(Z.to_nat n) ★ l ↦★ vl
-               ={E}=★ Φ (LitV $ LitLoc l))
-    ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
+    {{{ heap_ctx }}} Alloc (Lit $ LitInt n) @ E
+    {{{ l vl; LitV $ LitLoc l, n = length vl ★ †l…(Z.to_nat n) ★ l ↦★ vl }}}.
   Proof.
-    iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx /heap_inv.
+    iIntros (???) "[#Hinv HΦ]". rewrite /heap_ctx /heap_inv.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iApply wp_alloc_pst=> //. iNext.
-    iIntros "{$Hσ}"; iIntros (l σ') "(% & #Hσσ' & Hσ') !>".
+    iIntros "{$Hσ}". iIntros (l σ') "(% & #Hσσ' & Hσ')".
     iDestruct "Hσσ'" as %(vl & HvlLen & Hvl).
     assert (vl ≠ []) by (intros ->; simpl in *; lia).
     iMod (heap_alloc_vs with "[$Hvalσ]") as "[Hvalσ' Hmapsto]"; first done.
@@ -371,15 +368,15 @@ Section heap.
     setoid_rewrite <-shift_loc_assoc. apply IH.
   Qed.
 
-  Lemma wp_free E (n:Z) l vl Φ :
+  Lemma wp_free E (n:Z) l vl :
     nclose heapN ⊆ E →
     n = length vl →
-    heap_ctx ★ ▷ l ↦★ vl ★ ▷ †l…(length vl) ★ ▷ (|={E}=> Φ (LitV LitUnit))
-    ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦★ vl ★ ▷ †l…(length vl) }}}
+      Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
+    {{{ ; LitV LitUnit, True }}}.
   Proof.
-    iIntros (??) "(#Hinv & >Hmt & >Hf & HΦ)". rewrite /heap_ctx /heap_inv.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose".
-    iDestruct "REL" as %REL.
+    iIntros (???Φ) "[(#Hinv & >Hmt & >Hf) HΦ]". rewrite /heap_ctx /heap_inv.
+    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose". iDestruct "REL" as %REL.
     rewrite heap_freeable_eq /heap_freeable_def.
     iDestruct (own_valid_2 with "[$HhF $Hf]") as % [Hl Hv]%auth_valid_discrete_2.
     move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
@@ -390,12 +387,11 @@ Section heap.
     assert (0 < n) by (subst n; by destruct vl).
     iApply (wp_free_pst _ σ); auto.
     { intros i. subst n. eauto using heap_freeable_is_Some. }
-    iNext. iIntros "{$Hσ} Hσ !>".
-    iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
+    iNext. iIntros "{$Hσ} Hσ". iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
     { rewrite heap_mapsto_vec_combine //. iFrame. }
     iMod (own_update_2 with "[$HhF $Hf]") as "HhF".
     { apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
-    iMod ("Hclose" with "[-HΦ]") as "_"; last done.
+    iMod ("Hclose" with "[-HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, _. subst. rewrite Nat2Z.id. iFrame.
     eauto using heap_freeable_rel_free_mem.
   Qed.
@@ -431,16 +427,16 @@ Section heap.
     destruct ls, ls''; rewrite ?Nat.add_0_r; naive_solver.
   Qed.
 
-  Lemma wp_read_sc E l q v Φ :
+  Lemma wp_read_sc E l q v :
     nclose heapN ⊆ E →
-    heap_ctx ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v)
-    ⊢ WP Read ScOrd (Lit $ LitLoc l) @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
+    {{{; v, l ↦{q} v }}}.
   Proof.
-    iIntros (?) "(#Hinv & >Hv & HΦ)".
+    iIntros (??) "[[#Hinv >Hv] HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iApply wp_read_sc_pst; first done. iNext. iIntros "{$Hσ} Hσ !>".
+    iApply wp_read_sc_pst; first done. iNext. iIntros "{$Hσ} Hσ".
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
     iNext. iExists σ, hF. iFrame. eauto.
   Qed.
@@ -458,12 +454,12 @@ Section heap.
     apply nat_local_update; lia.
   Qed.
 
-  Lemma wp_read_na E l q v Φ :
+  Lemma wp_read_na E l q v :
     nclose heapN ⊆ E →
-    heap_ctx ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v)
-    ⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
+    {{{; v, l ↦{q} v }}}.
   Proof.
-    iIntros (?) "(#Hinv & >Hv & HΦ)".
+    iIntros (??Φ) "[[#Hinv >Hv] HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iApply (wp_read_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
@@ -476,7 +472,7 @@ Section heap.
     iModIntro. clear dependent n σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iApply wp_read_na2_pst; first done. iNext. iIntros "{$Hσ} Hσ !>".
+    iApply wp_read_na2_pst; first done. iNext. iIntros "{$Hσ} Hσ".
     iMod (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
@@ -494,27 +490,27 @@ Section heap.
     apply exclusive_local_update. by destruct st2.
   Qed.
 
-  Lemma wp_write_sc E l e v v' Φ :
+  Lemma wp_write_sc E l e v v' :
     nclose heapN ⊆ E → to_val e = Some v →
-    heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
-    ⊢ WP Write ScOrd (Lit $ LitLoc l) e @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
+    {{{; LitV LitUnit, l ↦ v }}}.
   Proof.
-    iIntros (? <-%of_to_val) "(#Hinv & >Hv & HΦ)".
+    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_write_sc_pst; [done|]. iNext. iIntros "{$Hσ} Hσ !>".
+    iApply wp_write_sc_pst; [done|]. iNext. iIntros "{$Hσ} Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
-  Lemma wp_write_na E l e v v' Φ :
+  Lemma wp_write_na E l e v v' :
     nclose heapN ⊆ E → to_val e = Some v →
-    heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
-    ⊢ WP Write Na1Ord (Lit $ LitLoc l) e @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
+    {{{; LitV LitUnit, l ↦ v }}}.
   Proof.
-    iIntros (? <-%of_to_val) "(#Hinv & >Hv & HΦ)".
+    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iApply (wp_write_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
@@ -527,37 +523,37 @@ Section heap.
     iModIntro. clear dependent σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_write_na2_pst; [done|]. iNext. iIntros "{$Hσ} Hσ !>".
+    iApply wp_write_na2_pst; [done|]. iNext. iIntros "{$Hσ} Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
-  Lemma wp_cas_int_fail E l q z1 e2 v2 zl Φ :
+  Lemma wp_cas_int_fail E l q z1 e2 v2 zl :
     nclose heapN ⊆ E → to_val e2 = Some v2 → z1 ≠ zl →
-    heap_ctx ★ ▷ l ↦{q} (LitV $ LitInt zl)
-             ★ ▷ (l ↦{q} (LitV $ LitInt zl) ={E}=★ Φ (LitV $ LitInt 0))
-    ⊢ WP CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦{q} (LitV $ LitInt zl) }}}
+      CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+    {{{;LitV $ LitInt 0, l ↦{q} (LitV $ LitInt zl) }}}.
   Proof.
-    iIntros (? <-%of_to_val ?) "(#Hinv & >Hv & HΦ)".
+    iIntros (? <-%of_to_val ??) "[[#Hinv >Hv] HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
     iApply wp_cas_fail_pst; eauto.
     { by rewrite /= bool_decide_false. }
-    iNext. iIntros "{$Hσ} Hσ !>".
+    iNext. iIntros "{$Hσ} Hσ".
     iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
-  Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 v2 l' vl' Φ :
+  Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 v2 l' vl' :
     nclose heapN ⊆ E → to_val e2 = Some v2 → l1 ≠ l' →
-    heap_ctx ★ ▷ l ↦{q} (LitV $ LitLoc l') ★ ▷ l' ↦{q'} vl' ★ ▷ l1 ↦{q1} v1'
-             ★ ▷ (l ↦{q} (LitV $ LitLoc l') ★ l' ↦{q'} vl' ★ l1 ↦{q1} v1'
-                  ={E}=★ Φ (LitV $ LitInt 0))
-    ⊢ WP CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦{q} (LitV $ LitLoc l') ★ ▷ l' ↦{q'} vl' ★ ▷ l1 ↦{q1} v1' }}}
+      CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+    {{{;LitV $ LitInt 0,
+        l ↦{q} (LitV $ LitLoc l') ★ l' ↦{q'} vl' ★ l1 ↦{q1} v1' }}}.
   Proof.
-    iIntros (? <-%of_to_val ?) "(#Hinv & >Hl & >Hl' & >Hl1 & HΦ)".
+    iIntros (? <-%of_to_val ??) "[(#Hinv & >Hl & >Hl' & >Hl1) HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl]") as %[n Hσl].
@@ -565,42 +561,42 @@ Section heap.
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl1]") as %[n1 Hσl1].
     iApply wp_cas_fail_pst; eauto.
     { by rewrite /= bool_decide_false // Hσl1 Hσl'. }
-    iNext. iIntros "{$Hσ} Hσ !>".
+    iNext. iIntros "{$Hσ} Hσ ".
     iMod ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. by iFrame.
   Qed.
 
-  Lemma wp_cas_int_suc E l z1 e2 v2 Φ :
+  Lemma wp_cas_int_suc E l z1 e2 v2 :
     nclose heapN ⊆ E → to_val e2 = Some v2 →
-    heap_ctx ★ ▷ l ↦ (LitV $ LitInt z1)
-             ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV $ LitInt 1))
-    ⊢ WP CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦ (LitV $ LitInt z1) }}}
+      CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+    {{{; LitV $ LitInt 1, l ↦ v2 }}}.
   Proof.
-    iIntros (? <-%of_to_val) "(#Hinv & >Hv & HΦ)".
+    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
     iApply wp_cas_suc_pst; eauto.
     { by rewrite /= bool_decide_true. }
-    iNext. iIntros "{$Hσ} Hσ !>".
+    iNext. iIntros "{$Hσ} Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
   Qed.
 
-  Lemma wp_cas_loc_suc E l l1 e2 v2 Φ :
+  Lemma wp_cas_loc_suc E l l1 e2 v2 :
     nclose heapN ⊆ E → to_val e2 = Some v2 →
-    heap_ctx ★ ▷ l ↦ (LitV $ LitLoc l1)
-             ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV $ LitInt 1))
-    ⊢ WP CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E {{ Φ }}.
+    {{{ heap_ctx ★ ▷ l ↦ (LitV $ LitLoc l1) }}}
+      CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+    {{{; LitV $ LitInt 1, l ↦ v2 }}}.
   Proof.
-    iIntros (? <-%of_to_val) "(#Hinv & >Hv & HΦ)".
+    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
     iApply wp_cas_suc_pst; eauto.
     { by rewrite /= bool_decide_true. }
-    iNext. iIntros "{$Hσ} Hσ !>".
+    iNext. iIntros "{$Hσ} Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
diff --git a/lifting.v b/lifting.v
index 80522fa2..3c3159dc 100644
--- a/lifting.v
+++ b/lifting.v
@@ -9,7 +9,6 @@ Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
 Section lifting.
 Context `{irisG lrust_lang Σ}.
 Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
 Implicit Types ef : option expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
@@ -23,48 +22,47 @@ Lemma wp_bindi {E e} Ki Φ :
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ n Φ :
+Lemma wp_alloc_pst E σ n:
   0 < n →
-  ▷ ownP σ ★
-  ▷ (∀ l σ', ■ (∀ m, σ !! (shift_loc l m) = None) ★
-             ■ (∃ vl, n = length vl ∧ init_mem l vl σ = σ') ★
-             ownP σ' ={E}=★ Φ (LitV $ LitLoc l))
-  ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
+  {{{ l σ'; LitV $ LitLoc l,
+      ■ (∀ m, σ !! (shift_loc l m) = None) ★
+      ■ (∃ vl, n = length vl ∧ init_mem l vl σ = σ') ★
+      ownP σ' }}}.
 Proof.
-  iIntros (?)  "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
+  iIntros (? Φ) "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
 Qed.
 
-Lemma wp_free_pst E σ l n Φ :
+Lemma wp_free_pst E σ l n :
   0 < n →
   (∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)) →
-  ▷ ownP σ ★
-  ▷ (ownP (free_mem l (Z.to_nat n) σ) ={E}=★ Φ (LitV $ LitUnit))
-  ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
+  {{{ ; LitV $ LitUnit, ownP (free_mem l (Z.to_nat n) σ) }}}.
 Proof.
-  iIntros (??)  "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
+  iIntros (???)  "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ".
 Qed.
 
-Lemma wp_read_sc_pst E σ l n v Φ :
+Lemma wp_read_sc_pst E σ l n v :
   σ !! l = Some (RSt n, v) →
-  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Read ScOrd (Lit $ LitLoc l) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ ; v, ownP σ }}}.
 Proof.
-  iIntros (?) "[??]". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto using to_of_val.
-  by rewrite big_sepL_nil right_id; iFrame.
+  rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
 Qed.
 
-Lemma wp_read_na2_pst E σ l n v Φ :
+Lemma wp_read_na2_pst E σ l n v :
   σ !! l = Some(RSt $ S n, v) →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=(RSt n, v)]>σ) ={E}=★ Φ v)
-  ⊢ WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Read Na2Ord (Lit $ LitLoc l) @ E
+  {{{ ; v, ownP (<[l:=(RSt n, v)]>σ) }}}.
 Proof.
-  iIntros (?) "[??]". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto using to_of_val.
-  by rewrite big_sepL_nil right_id; iFrame.
+  rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
 Qed.
 
 Lemma wp_read_na1_pst E l Φ :
@@ -80,22 +78,24 @@ Proof.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
 Qed.
 
-Lemma wp_write_sc_pst E σ l v v' Φ :
+Lemma wp_write_sc_pst E σ l v v' :
   σ !! l = Some (RSt 0, v') →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=(RSt 0, v)]>σ) ={E}=★ Φ (LitV LitUnit))
-  ⊢ WP Write ScOrd (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Write ScOrd (Lit $ LitLoc l) (of_val v) @ E
+  {{{ ; LitV LitUnit, ownP (<[l:=(RSt 0, v)]>σ) }}}.
 Proof.
-  iIntros (?) "[??]". iApply wp_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto. by rewrite big_sepL_nil right_id; iFrame.
+  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
+  by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
+  iNext. iIntros "?!>". by iApply "HΦ".
 Qed.
 
-Lemma wp_write_na2_pst E σ l v v' Φ :
+Lemma wp_write_na2_pst E σ l v v' :
   σ !! l = Some(WSt, v') →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=(RSt 0, v)]>σ) ={E}=★ Φ (LitV LitUnit))
-  ⊢ WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E
+  {{{ ; LitV LitUnit, ownP (<[l:=(RSt 0, v)]>σ) }}}.
 Proof.
-  iIntros (?) "[??]". iApply wp_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto. by rewrite big_sepL_nil right_id; iFrame.
+  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
+  by intros; inv_head_step; eauto.
+  rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
 Qed.
 
 Lemma wp_write_na1_pst E l v Φ :
@@ -111,37 +111,37 @@ Proof.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
 Qed.
 
-Lemma wp_cas_fail_pst E σ l n e1 v1 v2 vl Φ :
+Lemma wp_cas_fail_pst E σ l n e1 v1 v2 vl :
   to_val e1 = Some v1 →
   σ !! l = Some (RSt n, vl) →
   value_eq σ v1 vl = Some false →
-  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitInt 0))
-  ⊢ WP CAS (Lit $ LitLoc l) e1 (of_val v2) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
+  {{{ ; LitV $ LitInt 0, ownP σ }}}.
 Proof.
-  iIntros (?%of_to_val ??) "[HP HΦ]". subst.
+  iIntros (?%of_to_val ???) "[HP HΦ]". subst.
   iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
-  iFrame. iNext. by rewrite big_sepL_nil right_id.
+  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?!>". by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_suc_pst E σ l e1 v1 v2 vl Φ :
+Lemma wp_cas_suc_pst E σ l e1 v1 v2 vl :
   to_val e1 = Some v1 →
   σ !! l = Some (RSt 0, vl) →
   value_eq σ v1 vl = Some true →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=(RSt 0, v2)]>σ) ={E}=★ Φ (LitV $ LitInt 1))
-  ⊢ WP CAS (Lit $ LitLoc l) e1 (of_val v2) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
+  {{{ ; LitV $ LitInt 1, ownP (<[l:=(RSt 0, v2)]>σ) }}}.
 Proof.
-  iIntros (?%of_to_val ??) "[HP HΦ]". subst.
+  iIntros (?%of_to_val ???) "[HP HΦ]". subst.
   iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
-  iFrame. iNext. by rewrite big_sepL_nil right_id.
+  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?!>". by iApply "HΦ".
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e Φ :
-  ▷ Φ (LitV LitUnit) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
+Lemma wp_fork E e :
+  {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ ; LitV LitUnit, True }}}.
 Proof.
-  iIntros "[??]". iApply wp_lift_pure_det_head_step; eauto.
+  iIntros (?) "[?HΦ]". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iNext.
-  rewrite big_sepL_singleton. iFrame. by iApply wp_value.
+  rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
 Qed.
 
 Lemma wp_rec E e f xl erec erec' el Φ :
diff --git a/memcpy.v b/memcpy.v
index 253a17fc..d9046c30 100644
--- a/memcpy.v
+++ b/memcpy.v
@@ -16,13 +16,14 @@ Notation "e1 <-[ i ]{ n } ! e2" :=
   (at level 80, n, i at next level,
    format "e1  <-[ i ]{ n }  ! e2") : lrust_expr_scope.
 
-Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n Φ:
+Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
   nclose heapN ⊆ E →
   length vl1 = n → length vl2 = n →
-  heap_ctx ★ l1 ↦★ vl1 ★ l2 ↦★{q} vl2 ★
-  ▷ (l1 ↦★ vl2 ★ l2 ↦★{q} vl2 ={E}=★ Φ #()) ⊢ WP #l1 <-{n} !#l2 @ E {{ Φ }}.
+  {{{ heap_ctx ★ l1 ↦★ vl1 ★ l2 ↦★{q} vl2 }}}
+    #l1 <-{n} !#l2 @ E
+  {{{; #(), l1 ↦★ vl2 ★ l2 ↦★{q} vl2 }}}.
 Proof.
-  iIntros (? Hvl1 Hvl2) "(#Hinv&Hl1&Hl2&HΦ)".
+  iIntros (? Hvl1 Hvl2 Φ) "[(#Hinv & Hl1 & Hl2) HΦ]".
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
   - iApply "HΦ". assert (n = O) by lia; subst.
     destruct vl1, vl2; try discriminate. by iFrame.
diff --git a/perm.v b/perm.v
index 10d84185..a08f10b3 100644
--- a/perm.v
+++ b/perm.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import thread_local.
 From iris.proofmode Require Import tactics.
-From lrust Require Export type valuable.
+From lrust Require Export type proofmode.
 
 Delimit Scope perm_scope with P.
 Bind Scope perm_scope with perm.
@@ -11,8 +11,18 @@ Section perm.
 
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
-  Definition has_type (v : Valuable.t) (ty : type) : perm :=
-    λ tid, from_option (λ v, ty.(ty_own) tid [v]) False%I v.
+  Fixpoint eval_expr (ν : expr) : option val :=
+    match ν with
+    | BinOp ProjOp e (Lit (LitInt n)) =>
+      match eval_expr e with
+      | Some (#(LitLoc l)) => Some (#(shift_loc l n))
+      | _ => None
+      end
+    | e => to_val e
+    end.
+
+  Definition has_type (ν : expr) (ty : type) : perm := λ tid,
+    from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
 
   Definition extract (κ : lifetime) (ρ : perm) : perm :=
     λ tid, (κ ∋ ρ tid)%I.
@@ -75,3 +85,32 @@ Section duplicable.
   Proof. intros tid. apply _. Qed.
 
 End duplicable.
+
+Section has_type.
+
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+
+  Lemma has_type_value (v : val) ty tid :
+    (v ◁ ty)%P tid ⊣⊢ ty.(ty_own) tid [v].
+  Proof.
+    destruct v as [|f xl e ?]. done.
+    unfold has_type, eval_expr, of_val.
+    assert (Rec f xl e = RecV f xl e) as -> by done. by rewrite to_of_val.
+  Qed.
+
+  Lemma has_type_wp E (ν : expr) ty tid (Φ : val -> iProp _) :
+    (ν ◁ ty)%P tid ★ (∀ (v : val), eval_expr ν = Some v ★ (v ◁ ty)%P tid -★ Φ v)
+    ⊢ WP ν @ E {{ Φ }}.
+  Proof.
+    iIntros "[H◁ HΦ]". setoid_rewrite has_type_value. unfold has_type.
+    destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
+    iSpecialize ("HΦ" $! v with "[$H◁]"). done.
+    iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
+      forall (Φ v EQν); try done.
+    - inversion EQν. subst. wp_value. auto.
+    - wp_value. auto.
+    - wp_bind e. simpl in EQν. destruct (eval_expr e) as [[[|l|]|]|]; try done.
+      iApply ("IH" with "[] [HΦ]"). done. simpl. wp_op. inversion EQν. eauto.
+  Qed.
+
+End has_type.
\ No newline at end of file
diff --git a/perm_incl.v b/perm_incl.v
index 035e1d86..8ba71f50 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -104,10 +104,11 @@ Section props.
   Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ★ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
   Proof. iIntros (tid) "[#?#?]!>". iApply lft_incl_trans. auto. Qed.
 
-  Lemma perm_incl_share q v κ ty :
-    v ◁ &uniq{κ} ty ★ [κ]{q} ⇒ v ◁ &shr{κ} ty ★ [κ]{q}.
+  Lemma perm_incl_share q ν κ ty :
+    ν ◁ &uniq{κ} ty ★ [κ]{q} ⇒ ν ◁ &shr{κ} ty ★ [κ]{q}.
   Proof.
-    iIntros (tid) "[Huniq [Htok Hlft]]". destruct v; last by iDestruct "Huniq" as "[]".
+    iIntros (tid) "[Huniq [Htok Hlft]]". unfold has_type.
+    destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
     iDestruct "Huniq" as (l) "[% Hown]".
     iMod (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown Htok]".
     apply disjoint_union_l; solve_ndisj. set_solver. iModIntro.
@@ -140,23 +141,22 @@ Section props.
       rewrite !big_sepL_cons IH //.
   Qed.
 
-  Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) v :
+  Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) ν :
     length tyl = length ql →
     foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
-    v ◁ own q (Π tyl) ⇔
+    ν ◁ own q (Π tyl) ⇔
       foldr (λ qtyoffs acc,
-             Valuable.proj (Z.of_nat (qtyoffs.2.2)) v ◁
-                           own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
+             (ν +ₗ #(qtyoffs.2.2:nat))%E ◁ own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
             ⊤ (combine ql (combine_offs tyl 0)).
   Proof.
     intros Hlen Hq. assert (ql ≠ []).
     { destruct ql as [|q0 ql]; last done. destruct q. simpl in *. by subst. }
-    destruct v as [[[|l|]|]|];
+    unfold has_type. simpl eval_expr. destruct (eval_expr ν) as [[[|l|]|]|];
       try by (destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done;
         by split; iIntros (tid) "H"; try done;
           [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
            iDestruct "H" as "[[]_]"]).
-    destruct (@exists_last _ ql) as (ql'&q0&->). done.
+    destruct (@exists_last _ ql) as (ql'&q0&->); first done.
     apply uPred_equiv_perm_equiv=>tid.
     assert (foldr Qp_plus (q0/2) (ql' ++ [q0/2]) = q)%Qp as <-.
     { destruct q as [q ?]. apply Qp_eq. simpl in *. subst. clear. induction ql'.
@@ -176,14 +176,14 @@ Section props.
       by iSplit; iIntros "[$[$[$[$$]]]]".
   Qed.
 
-  Lemma perm_split_uniq_borrow_prod tyl κ v :
-    v ◁ &uniq{κ} (Π tyl) ⇒
+  Lemma perm_split_uniq_borrow_prod tyl κ ν :
+    ν ◁ &uniq{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
-             Valuable.proj (Z.of_nat (tyoffs.2)) v ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
+             (ν +ₗ #(tyoffs.2:nat))%E ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
-    intros tid.
-    destruct v as [[[|l|]|]|];
+    intros tid. unfold has_type. simpl eval_expr.
+    destruct (eval_expr ν) as [[[|l|]|]|];
       iIntros "H"; try iDestruct "H" as "[]";
         iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
     rewrite split_prod_mt.
@@ -193,14 +193,14 @@ Section props.
     iMod ("IH" with "H") as "$". iModIntro. iExists _. eauto.
   Qed.
 
-  Lemma perm_split_shr_borrow_prod tyl κ v :
-    v ◁ &shr{κ} (Π tyl) ⇒
+  Lemma perm_split_shr_borrow_prod tyl κ ν :
+    ν ◁ &shr{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
-             Valuable.proj (Z.of_nat (tyoffs.2)) v ◁ &shr{κ} (tyoffs.1) ★ acc)%P
+             (ν +ₗ #(tyoffs.2:nat))%E ◁ &shr{κ} (tyoffs.1) ★ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
-    intros tid.
-    destruct v as [[[|l|]|]|];
+    intros tid. unfold has_type. simpl eval_expr.
+    destruct (eval_expr ν) as [[[|l|]|]|];
       iIntros "H"; try iDestruct "H" as "[]";
         iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
     simpl. iModIntro.
@@ -221,11 +221,11 @@ Section props.
     iApply lft_extract_combine. set_solver. by iFrame.
   Qed.
 
-  Lemma own_uniq_borrowing v q ty κ :
-    borrowing κ ⊤ (v ◁ own q ty) (v ◁ &uniq{κ} ty).
+  Lemma own_uniq_borrowing ν q ty κ :
+    borrowing κ ⊤ (ν ◁ own q ty) (ν ◁ &uniq{κ} ty).
   Proof.
-    iIntros (tid) "#Hκ _ Hown".
-    destruct v as [[[|l|]|]|];
+    iIntros (tid) "#Hκ _ Hown". unfold has_type.
+    destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
     iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
     iMod (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done.
@@ -236,11 +236,11 @@ Section props.
     iIntros "H/=". iExists _. iSplit. done. by iDestruct "H" as "[$$]".
   Qed.
 
-  Lemma reborrow_uniq_borrowing κ κ' v ty :
-    borrowing κ (κ ⊑ κ') (v ◁ &uniq{κ'}ty) (v ◁ &uniq{κ}ty).
+  Lemma reborrow_uniq_borrowing κ κ' ν ty :
+    borrowing κ (κ ⊑ κ') (ν ◁ &uniq{κ'}ty) (ν ◁ &uniq{κ}ty).
   Proof.
-    iIntros (tid) "_ #Hord H".
-    destruct v as [[[|l|]|]|];
+    iIntros (tid) "_ #Hord H". unfold has_type.
+    destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
     iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
     iMod (lft_reborrow with "Hord H") as "[H Hextr]". done.
@@ -251,11 +251,11 @@ Section props.
     - iExists _. eauto.
   Qed.
 
-  Lemma reborrow_shr_perm_incl κ κ' v ty :
-    κ ⊑ κ' ★ v ◁ &shr{κ'}ty ⇒ v ◁ &shr{κ}ty.
+  Lemma reborrow_shr_perm_incl κ κ' ν ty :
+    κ ⊑ κ' ★ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
   Proof.
-    iIntros (tid) "[#Hord #Hκ']".
-    destruct v as [[[|l|]|]|];
+    iIntros (tid) "[#Hord #Hκ']". unfold has_type.
+    destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
     iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
     iModIntro. iExists _. iSplit. done.
diff --git a/proofmode.v b/proofmode.v
index 232c9d01..3518c758 100644
--- a/proofmode.v
+++ b/proofmode.v
@@ -28,7 +28,7 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
     (Δ'' ⊢ |={E}=> Φ (LitV $ LitLoc l))) →
   Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
+  intros ???? HΔ. rewrite -wp_fupd -wp_alloc // -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound; apply later_mono, forall_intro=> l;
   apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
@@ -48,10 +48,11 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   (Δ''' ⊢ |={E}=> Φ (LitV LitUnit)) →
   Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
-  intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_free // -always_and_sep_l.
+  intros ?? -> ?? <- ? <- -> HΔ.
+  rewrite -wp_fupd -wp_free // -!assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -!later_sep; apply later_mono.
-  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ.
+  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True.
 Qed.
 
 Lemma tac_wp_read Δ Δ' E i l q v o Φ :
@@ -62,10 +63,12 @@ Lemma tac_wp_read Δ Δ' E i l q v o Φ :
   Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   intros ??[->| ->]???.
-  - rewrite -wp_read_na // -always_and_sep_l. apply and_intro; first done.
+  - rewrite -wp_fupd -wp_read_na // -!assoc -always_and_sep_l.
+    apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_read_sc // -always_and_sep_l. apply and_intro; first done.
+  - rewrite -wp_fupd -wp_read_sc // -!assoc -always_and_sep_l.
+    apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -80,10 +83,10 @@ Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
   Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
 Proof.
   intros ???[->| ->]????.
-  - rewrite -wp_write_na // -always_and_sep_l. apply and_intro; first done.
+  - rewrite -wp_fupd -wp_write_na // -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_write_sc // -always_and_sep_l. apply and_intro; first done.
+  - rewrite -wp_fupd -wp_write_sc // -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
diff --git a/type_incl.v b/type_incl.v
index b6999e2d..90a19164 100644
--- a/type_incl.v
+++ b/type_incl.v
@@ -241,11 +241,11 @@ Section ty_incl.
       iIntros (x vl). by iApply "H".
   Qed.
 
-  Lemma ty_incl_perm_incl ρ ty1 ty2 v :
-    ty_incl ρ ty1 ty2 → ρ ★ v ◁ ty1 ⇒ v ◁ ty2.
+  Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
+    ty_incl ρ ty1 ty2 → ρ ★ ν ◁ ty1 ⇒ ν ◁ ty2.
   Proof.
     iIntros (Hincl tid) "[Hρ Hty1]". iMod (Hincl with "Hρ") as "[#Hownincl _]".
-    destruct v; last done. by iApply "Hownincl".
+    unfold Perm.has_type. destruct (Perm.eval_expr ν); last done. by iApply "Hownincl".
   Qed.
 
 End ty_incl.
\ No newline at end of file
diff --git a/typing.v b/typing.v
index dbe15b5d..33126f47 100644
--- a/typing.v
+++ b/typing.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import thread_local hoare.
 From lrust Require Export type perm notation memcpy.
-From lrust Require Import type_incl perm_incl proofmode.
+From lrust Require Import perm_incl proofmode.
 
 Import Types Perm.
 
@@ -9,9 +9,9 @@ Section typing.
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
-  Definition typed_step (ρ : perm) e (θ : Valuable.t → perm) :=
-    ∀ tid,
-      heap_ctx ⊢ {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, θ (Some v) tid ★ tl_own tid ⊤ }}.
+  Definition typed_step (ρ : perm) e (θ : val → perm) :=
+    ∀ tid, {{ heap_ctx ★ ρ tid ★ tl_own tid ⊤ }} e
+           {{ v, θ v tid ★ tl_own tid ⊤ }}.
 
   (* FIXME : why isn't the notation context on the last parameter not
      taken into account? *)
@@ -21,39 +21,39 @@ Section typing.
     typed_step ρ e (λ ν, ν ◁ ty)%P.
 
   Definition typed_program (ρ : perm) e :=
-    ∀ tid, heap_ctx ⊢  {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, False }}.
+    ∀ tid, {{ heap_ctx ★ ρ tid ★ tl_own tid ⊤ }} e {{ _, False }}.
 
   Lemma typed_frame ρ e θ ξ:
     typed_step ρ e θ → typed_step (ρ ★ ξ) e (λ ν, θ ν ★ ξ)%P.
   Proof.
-    iIntros (Hwt tid) "#HEAP!#[[?$]?]". iApply (Hwt with "HEAP"). by iFrame.
+    iIntros (Hwt tid) "!#(#HEAP&[?$]&?)". iApply Hwt. by iFrame.
   Qed.
 
   Lemma typed_step_exists {A} ρ θ e ξ:
     (∀ x:A, typed_step (ρ ★ θ x) e ξ) →
     typed_step (ρ ★ ∃ x, θ x) e ξ.
   Proof.
-    iIntros (Hwt tid) "#HEAP!#[[Hρ Hθ]?]". iDestruct "Hθ" as (x) "Hθ".
-    iApply (Hwt with "HEAP"). by iFrame.
+    iIntros (Hwt tid) "!#(#HEAP&[Hρ Hθ]&?)". iDestruct "Hθ" as (x) "Hθ".
+    iApply Hwt. by iFrame.
   Qed.
 
-  Lemma typed_bool ρ (b:Datatypes.bool) :
-    typed_step_ty ρ #b bool.
-  Proof. iIntros (tid) "_!#[_$]". wp_value. simpl. eauto. Qed.
+  Lemma typed_bool ρ (b:Datatypes.bool): typed_step_ty ρ #b bool.
+  Proof. iIntros (tid) "!#(_&_&$)". wp_value. by iExists _. Qed.
 
   Lemma typed_int ρ (z:Datatypes.nat) :
     typed_step_ty ρ #z int.
-  Proof. iIntros (tid) "_!#[_$]". wp_value. simpl. eauto. Qed.
+  Proof. iIntros (tid) "!#(_&_&$)". wp_value. by iExists _. Qed.
 
   Lemma typed_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ :
     length xl = n →
     (∀ (a : A) (vl : vec val n) (fv : val) e',
         subst_l xl (map of_val vl) e = Some e' →
-        typed_program (Some fv ◁ fn θ ★ (θ a vl) ★ ρ) (subst' f fv e')) →
+        typed_program (fv ◁ fn θ ★ (θ a vl) ★ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (fn θ).
   Proof.
-    iIntros (Hn He tid) "#HEAP !# [#Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
-    { simpl. destruct decide as [CL|?]. repeat f_equal. apply proof_irrel. done. }
+    iIntros (Hn He tid) "!#(#HEAP&#Hρ&$)".
+    assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
+    rewrite has_type_value.
     iLöb as "IH". iExists _. iSplit. done. iIntros (a vl) "!#[Hθ?]".
     assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
     { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
@@ -61,18 +61,19 @@ Section typing.
     iApply wp_rec; try done.
     { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
       rewrite to_of_val. eauto. }
-    iNext. iApply (He with "HEAP"). done. by iFrame "★#".
+    iNext. iApply He. done. iFrame "★#". by rewrite has_type_value.
   Qed.
 
   Lemma typed_cont {n} `{Closed (f :b: xl +b+ []) e} ρ θ :
     length xl = n →
-    (∀ (vl : vec val n) (fv : val) e',
+    (∀ (fv : val) (vl : vec val n) e',
         subst_l xl (map of_val vl) e = Some e' →
-        typed_program (Some fv ◁ cont (λ vl, ρ ★ θ vl)%P ★ (θ vl) ★ ρ) (subst' f fv e')) →
+        typed_program (fv ◁ cont (λ vl, ρ ★ θ vl)%P ★ (θ vl) ★ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (cont θ).
   Proof.
-    iIntros (Hn He tid) "#HEAP !# [Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
-    { simpl. destruct decide as [CL|?]. repeat f_equal. apply proof_irrel. done. }
+    iIntros (Hn He tid) "!#(#HEAP&Hρ&$)". specialize (He (RecV f xl e)).
+    assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
+    rewrite has_type_value.
     iLöb as "IH". iExists _. iSplit. done. iIntros (vl) "Hθ ?".
     assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
     { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
@@ -80,69 +81,69 @@ Section typing.
     iApply wp_rec; try done.
     { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
       rewrite to_of_val. eauto. }
-    iNext. iApply (He with "HEAP"). done. iFrame. simpl.
+    iNext. iApply He. done. iFrame "★#". rewrite has_type_value.
     iExists _. iSplit. done. iIntros (vl') "[Hρ Hθ] Htl".
     iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
     iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
   Qed.
 
-  Lemma typed_valuable e ty:
-    typed_step_ty (Valuable.of_expr e ◁ ty) e ty.
+  Lemma typed_valuable (ν : expr) ty:
+    typed_step_ty (ν ◁ ty) ν ty.
   Proof.
-    iIntros (tid) "_!#[H$]".
-    destruct (Valuable.of_expr e) as [v|] eqn:Hv. 2:by iDestruct "H" as "[]".
-    by iApply Valuable.of_expr_wp.
+    iIntros (tid) "!#(_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "[_$]".
   Qed.
 
   Lemma typed_plus e1 e2 ρ1 ρ2:
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ★ ρ2) (BinOp PlusOp e1 e2) int.
+    typed_step_ty (ρ1 ★ ρ2) (e1 + e2) int.
   Proof.
-    iIntros (He1 He2 tid) "#HEAP!#[[H1 H2]?]".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply (He1 with "HEAP"); by iFrame.
+    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
+    iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply (He2 with "HEAP"); by iFrame.
-    iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op. iFrame. by iExists _.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
+    wp_op. by iExists _.
   Qed.
 
   Lemma typed_minus e1 e2 ρ1 ρ2:
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ★ ρ2) (BinOp MinusOp e1 e2) int.
+    typed_step_ty (ρ1 ★ ρ2) (e1 - e2) int.
   Proof.
-    iIntros (He1 He2 tid) "#HEAP!#[[H1 H2]?]".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply (He1 with "HEAP"); by iFrame.
+    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
+    iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply (He2 with "HEAP"); by iFrame.
-    iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op. iFrame. by iExists _.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
+    wp_op. by iExists _.
   Qed.
 
   Lemma typed_le e1 e2 ρ1 ρ2:
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ★ ρ2) (BinOp LeOp e1 e2) bool.
+    typed_step_ty (ρ1 ★ ρ2) (e1 ≤ e2) bool.
   Proof.
-    iIntros (He1 He2 tid) "#HEAP!#[[H1 H2]?]".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply (He1 with "HEAP"); by iFrame.
+    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
+    iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply (He2 with "HEAP"); by iFrame.
-    iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    iFrame. wp_op; intros _; by iExists _.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
+    wp_op; intros _; by iExists _.
   Qed.
 
   Lemma typed_newlft ρ:
     typed_step ρ Newlft (λ _, ∃ α, [α]{1} ★ α ∋ top)%P.
   Proof.
-    iIntros (tid) "_!#[_$]". wp_value. iMod lft_begin as (α) "[?#?]". done.
+    iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_begin as (α) "[?#?]". done.
     iMod (lft_borrow_create with "[][]") as "[_?]". done. done.
-    2:by iModIntro; iExists α; iFrame. eauto.
+    2:by iExists α; iFrame. eauto.
   Qed.
 
   Lemma typed_endlft κ ρ:
     typed_step (κ ∋ ρ ★ [κ]{1}) Endlft (λ _, ρ)%P.
   Proof.
-    iIntros (tid) "_!#[[Hextr [Htok #Hlft]]$]".
-    wp_bind (#() ;; #())%E.
+    iIntros (tid) "!#(_&[Hextr [Htok #Hlft]]&$)". wp_bind (#() ;; #())%E.
     iApply (wp_wand_r _ _ (λ _, _ ★ True)%I). iSplitR "Hextr".
     iApply (wp_frame_step_l with "[-]"); try done.
     iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq.
@@ -153,27 +154,31 @@ Section typing.
   Lemma typed_alloc ρ (n : nat):
     0 < n → typed_step_ty ρ (Alloc #n) (own 1 (uninit n)).
   Proof.
-    iIntros (? tid) "#HEAP!#[_$]". wp_alloc l vl as "H↦" "H†". iIntros "!>".
+    iIntros (? tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
     iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iFrame.
-    apply (inj Z.of_nat) in H3. iExists _. iFrame. eauto.
+    apply (inj Z.of_nat) in H3. iExists _. iFrame. auto.
   Qed.
 
-  Lemma typed_free ty e:
-    typed_step (Valuable.of_expr e ◁ own 1 ty) (Free #ty.(ty_size) e) (λ _, top).
+  Lemma typed_free ty (ν : expr):
+    typed_step (ν ◁ own 1 ty) (Free #ty.(ty_size) ν) (λ _, top).
   Proof.
-    iIntros (tid) "#HEAP!#[Hown$]".
-    destruct (Valuable.of_expr e) as [v|] eqn:EQv; last by iDestruct "Hown" as "[]".
-    wp_bind e. iApply Valuable.of_expr_wp. done.
-    iDestruct "Hown" as (l) "(Hv & >H† & H↦★:)". iDestruct "Hv" as %[=->].
+    iIntros (tid) "!#(#HEAP&H◁&$)". wp_bind ν.
+    iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]".
+    rewrite has_type_value.
+    iDestruct "H◁" as (l) "(Hv & >H† & H↦★:)". iDestruct "Hv" as %[=->].
     iDestruct "H↦★:" as (vl) "[>H↦ Hown]".
     rewrite ty_size_eq. iDestruct "Hown" as ">%". wp_free; eauto.
   Qed.
 
-  Definition consumes (ty : type) (ρ1 ρ2 : Valuable.t → perm) : Prop :=
-    ∀ v tid, ρ1 v tid ★ tl_own tid ⊤ ={mgmtE ∪ lrustN}=★
-      ∃ (l : loc) vl q, v = Some #l ★ length vl = ty.(ty_size) ★ l ↦★{q} vl ★
-        |={mgmtE ∪ lrustN}▷=> (ty.(ty_own) tid vl ★
-           (l ↦★{q} vl ={mgmtE ∪ lrustN}=★ ρ2 v tid ★ tl_own tid ⊤)).
+  Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
+    ∀ ν tid Φ,
+      ρ1 ν tid ★ tl_own tid ⊤ ★
+      (∀ (l:loc) vl q,
+        (length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★{q} vl ★
+         |={mgmtE ∪ lrustN}▷=> (ty.(ty_own) tid vl ★
+            (l ↦★{q} vl ={mgmtE ∪ lrustN}=★ ρ2 ν tid ★ tl_own tid ⊤)))
+       -★ Φ #l)
+      ⊢ WP ν @ mgmtE ∪ lrustN {{ Φ }}.
   (* FIXME : why isn't the notation context on the two last parameters not
      taken into account? *)
   Arguments consumes _%T _%P _%P.
@@ -181,25 +186,27 @@ Section typing.
   Lemma consumes_copy_own ty q:
     ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
   Proof.
-    iIntros (? [v|] tid) "[Hown Htl]"; last by iDestruct "Hown" as "[]".
-    iDestruct "Hown" as (l) "[Heq [>H† H↦]]".
+    iIntros (? ν tid Φ) "(H◁ & Htl & HΦ)". iApply wp_fupd.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq [>H† H↦]]".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iModIntro. iExists _, _, _. iFrame "★#%". iSplit. done. iIntros "!>!>!>H↦!>".
-    iExists _. iSplit. done. iFrame. iExists vl. eauto.
+    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
+    rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
   Lemma consumes_move ty q:
     consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q (uninit ty.(ty_size)))%P.
   Proof.
-    iIntros ([v|] tid) "[Hown Htl]"; last by iDestruct "Hown" as "[]".
-    iDestruct "Hown" as (l) "[Heq [>H† H↦]]".
+    iIntros (ν tid Φ) "(H◁ & Htl & HΦ)". iApply wp_fupd.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iModIntro. iExists _, _, _. iFrame "★#%". iSplit. done. iIntros "!>!>!>H↦!>".
-    iExists _. iSplit. done. iFrame. iExists vl. eauto.
+    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
+    rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
   Lemma consumes_copy_uniq_borrow ty κ κ' q:
@@ -207,17 +214,18 @@ Section typing.
     consumes ty (λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
                 (λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (? [v|] tid) "[(H◁ & #H⊑ & [Htok #Hκ']) Htl]"; last by iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (l') "[Heq H↦]". iDestruct "Heq" as %[=->].
+    iIntros (? ν tid Φ) "((H◁ & #H⊑ & Htok & #Hκ') & Htl & HΦ)". iApply wp_fupd.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l') "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iModIntro. iExists _, _, _. iFrame "★#%". iSplit. done. iIntros "!>!>!>H↦".
+    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
     iMod (lft_borrow_close with "[H↦] Hclose'") as "[H↦ Htok]". set_solver.
     { iExists _. by iFrame. }
-    iMod ("Hclose" with "Htok") as "$". iExists _. eauto.
+    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
   Lemma consumes_copy_shr_borrow ty κ κ' q:
@@ -225,74 +233,72 @@ Section typing.
     consumes ty (λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
                 (λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (? [v|] tid) "[(H◁ & #H⊑ & [Htok #Hκ']) Htl]"; last by iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
+    iIntros (? ν tid Φ) "((H◁ & #H⊑ & [Htok #Hκ']) & Htl & HΦ)". iApply wp_fupd.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     rewrite (union_difference_L (nclose lrustN) ⊤); last done.
     setoid_rewrite ->tl_own_union; try set_solver.
-    iDestruct "Htl" as "[Htl $]".
-    iMod (ty_shr_acc with "Hshr [Htok Htl]") as (q'') "[H↦ Hclose']";
-      try set_solver. by iFrame.
+    iDestruct "Htl" as "[Htl ?]".
+    iMod (ty_shr_acc with "Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iModIntro. iExists _, _, _. iFrame "★#%". iSplit. done. iIntros "!>!>!>H↦".
+    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
     iMod ("Hclose'" with "[H↦]") as "[Htok $]".
     { iExists _. by iFrame. }
-    iMod ("Hclose" with "Htok") as "$". iExists _. eauto.
+    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
-  Lemma typed_deref ty ρ1 ρ2 e:
+  Lemma typed_deref ty ρ1 ρ2 (ν:expr) :
     ty.(ty_size) = 1%nat → consumes ty ρ1 ρ2 →
-    typed_step (ρ1 (Valuable.of_expr e)) (!e) (λ v, v ◁ ty ★ ρ2 (Valuable.of_expr e))%P.
+    typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ★ ρ2 ν)%P.
   Proof.
+    iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν. iApply wp_mask_mono. done.
+    iApply Hconsumes. iFrame. iIntros (l vl q) "(%&%&H↦&Hupd)".
     (* FIXME : I need to use [fupd_mask_mono], but I do not expect so. *)
-    iIntros (Hsz Hconsumes tid) "#HEAP!#H". iApply fupd_wp. iApply fupd_mask_mono.
-    done. iMod (Hconsumes with "H") as (l vl q) "(%&%&H↦&Hupd)".
-    iMod "Hupd". iModIntro. wp_bind e. iApply Valuable.of_expr_wp. done.
+    iApply fupd_wp. iApply fupd_mask_mono. done. iMod "Hupd". iModIntro.
     rewrite ->Hsz in *. destruct vl as [|v [|]]; try done.
-    rewrite heap_mapsto_vec_singleton. wp_read.
-    iApply fupd_mask_mono. 2:iMod "Hupd" as "[$ Hclose]". done.
-    by iApply "Hclose".
+    rewrite heap_mapsto_vec_singleton. wp_read. rewrite /sep has_type_value.
+    (* FIXME : Idem. *)
+    iApply fupd_mask_mono. done. iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
   Qed.
 
-  Lemma typed_deref_uniq_borrow_own ty e κ κ' q q':
-    typed_step (Valuable.of_expr e ◁ &uniq{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
-               (!e)
+  Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
+    typed_step (ν ◁ &uniq{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
+               (!ν)
                (λ v, v ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (tid) "#HEAP !# [(H◁ & #H⊑ & Htok & #Hκ') Htl]".
-    destruct (Valuable.of_expr e) eqn:He; last by iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & Htl)". wp_bind ν.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
     iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & H† & Hown)".
-    subst. rewrite heap_mapsto_vec_singleton.
-    wp_bind e. iApply Valuable.of_expr_wp. done. wp_read.
+    subst. rewrite heap_mapsto_vec_singleton. wp_read.
     iMod (lft_borrow_close_stronger with "[H↦ H† Hown] Hclose' []") as "[Hbor Htok]". done.
     { iCombine "H†" "Hown" as "H". iCombine "H↦" "H" as "H". iNext. iExact "H". }
     { iIntros "!>(?&?&?)!>". iNext. rewrite -heap_mapsto_vec_singleton. iExists _.
-      iFrame. iExists _. iSplit. done. by iFrame. }
+      iFrame. iExists _. by iFrame. }
     iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
     iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
     iMod ("Hclose" with "Htok"). iFrame "#★". iIntros "!>". iExists _. eauto.
   Qed.
 
-  Lemma typed_deref_shr_borrow_own ty e κ κ' q q':
-    typed_step (Valuable.of_expr e ◁ &shr{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
-               (!e)
+  Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
+    typed_step (ν ◁ &shr{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
+               (!ν)
                (λ v, v ◁ &shr{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (tid) "#HEAP !# [(H◁ & #H⊑ & Htok & #Hκ') Htl]".
-    destruct (Valuable.of_expr e) eqn:He; last by iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & Htl)". wp_bind ν.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
     iMod (lft_frac_borrow_open with "[] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
-    wp_bind e. iApply Valuable.of_expr_wp. done.
-    iSpecialize ("Hown" $! _ with "Htok2").
-    iApply wp_strong_mono. reflexivity. iSplitL "Htl Hclose Hclose'"; last first.
+    iSpecialize ("Hown" $! _ with "Htok2"). iFrame "#★".
+    iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
     - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ★ v = #vl)%I); try done.
       iSplitL "Hown"; last by wp_read; eauto.
       (* TODO : solving this goal is way too complicated compared
@@ -306,20 +312,20 @@ Section typing.
       iApply fupd_trans. iApply fupd_mask_frame_r. set_solver.
       iMod "Hown". iModIntro. iMod "H". iModIntro. iNext.
       iMod "H". iApply fupd_mask_frame_r. set_solver. done.
-    - iFrame "★#". iIntros (v) "[[#Hshr Htok][H↦ %]]". subst.
+    - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
       iMod ("Hclose'" with "[H↦]") as "Htok'". by eauto.
       iCombine "Htok" "Htok'" as "Htok". iMod ("Hclose" with "Htok") as "$".
-      iModIntro. iExists _. eauto.
+      iExists _. eauto.
   Qed.
 
-  Lemma typed_deref_uniq_borrow_borrow ty e κ κ' κ'' q:
-    typed_step (Valuable.of_expr e ◁ &uniq{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
-               (!e)
+  Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
+    typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
+               (!ν)
                (λ v, v ◁ &uniq{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
   Proof.
-    iIntros (tid) "#HEAP !# [(H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) Htl]".
-    destruct (Valuable.of_expr e) eqn:He; last by iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & Htl)". wp_bind ν.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
     iMod (lft_borrow_exists with "H↦ Htok") as (vl) "[Hbor Htok]". done.
     iMod (lft_borrow_split with "Hbor") as "[H↦ Hbor]". done.
@@ -328,27 +334,28 @@ Section typing.
     iMod (lft_borrow_persistent with "Heq Htok") as "[>% [Htok1 Htok2]]". done. subst.
     iMod (lft_borrow_open with "H↦ Htok1") as "[>H↦ Hclose']". done.
     iMod (lft_borrow_open with "Hbor Htok2") as "[Hbor Hclose'']". done.
-    rewrite heap_mapsto_vec_singleton.
-    wp_bind e. iApply Valuable.of_expr_wp. done. wp_read.
+    rewrite heap_mapsto_vec_singleton. wp_read.
     iMod (lft_borrow_close with "[H↦] Hclose'") as "[_ Htok1]". done. by auto.
     iMod (lft_borrow_unnest with "H⊑2 [Hbor Hclose'']") as "[Htok2 Hbor]". done. by iFrame.
     iCombine "Htok1" "Htok2" as "Htok". iMod ("Hclose" with "Htok") as "$". iFrame "★#".
-    iModIntro. iExists _. eauto.
+    iExists _. eauto.
   Qed.
 
-  Lemma typed_deref_shr_borrow_borrow ty e κ κ' κ'' q:
-    typed_step (Valuable.of_expr e ◁ &shr{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
-               (!e)
+  Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
+    typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
+               (!ν)
                (λ v, v ◁ &shr{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
   Proof.
     (* TODO : fix the definition of sharing unique borrows before. *)
   Admitted.
 
-  Definition update (ty : type) (ρ1 ρ2 : Valuable.t → perm) : Prop :=
-    ∀ v tid, ρ1 v tid ={mgmtE ∪ lrustN}=★
-      ∃ (l : loc) vl, v = Some #l ★ length vl = ty.(ty_size) ★ l ↦★ vl ★
-      ∀ vl', l ↦★ vl' ★ ▷ (ty.(ty_own) tid vl')
-        ={mgmtE ∪ lrustN}=★ ρ2 v tid.
+  Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
+    ∀ ν tid Φ, ρ1 ν tid ★
+      (∀ (l:loc) vl,
+         (length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★ vl ★
+         ∀ vl', l ↦★ vl' ★ ▷ (ty.(ty_own) tid vl') ={mgmtE ∪ lrustN}=★ ρ2 ν tid)
+         -★ Φ #l)
+      ⊢ WP ν @ mgmtE ∪ lrustN {{ Φ }}.
   (* FIXME : why isn't the notation context on the two last parameters not
      taken into account? *)
   Arguments update _%T _%P _%P.
@@ -357,61 +364,58 @@ Section typing.
     ty1.(ty_size) = ty2.(ty_size) →
     update ty1 (λ ν, ν ◁ own q ty2)%P (λ ν, ν ◁ own q ty1)%P.
   Proof.
-    iIntros (Hsz [v|] tid) "H◁"; last by iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (l) "(Heq & >H† & H↦)". iDestruct "Heq" as %[= ->].
-    iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty2.(ty_size_eq) -Hsz.
-    iDestruct "Hown" as ">%". iExists l, vl. iModIntro. iFrame "★%". iSplit. done.
-    iIntros (vl') "[H↦ Hown']!>". iExists _. iSplit. done. iFrame. iExists _. iFrame.
+    iIntros (Hsz ν tid Φ) "[H◁ HΦ]". iApply wp_fupd.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
+    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
+    rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "★%".
+    iIntros (vl') "[H↦ Hown']!>". rewrite /has_type Hνv.
+    iExists _. iSplit. done. iFrame. iExists _. iFrame.
   Qed.
 
   Lemma update_weak ty q κ κ':
     update ty (λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P
               (λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros ([v|] tid) "(H◁ & #H⊑ & Htok & #Hκ)"; last by iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (l) "(Heq & H↦)". iDestruct "Heq" as %[= ->].
+    iIntros (ν tid Φ) "[(H◁ & #H⊑ & Htok & #Hκ) HΦ]". iApply wp_fupd.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦)". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
-    iDestruct "Hown" as ">%". iExists _, _. iModIntro. iFrame "★%#". iSplit. done.
-    iIntros (vl') "[H↦ Hown]".
+    iDestruct "Hown" as ">%". iApply "HΦ". iFrame "★%#". iIntros (vl') "[H↦ Hown]".
     iMod (lft_borrow_close with "[H↦ Hown] Hclose'") as "[Hbor Htok]". set_solver.
     { iExists _. iFrame. }
-    iMod ("Hclose" with "Htok") as "$". iExists _. eauto.
+    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
-  Lemma typed_assign ρ1 ρ2 ty e1 e2:
-    ty.(ty_size) = 1%nat →
-    update ty ρ1 ρ2 →
-    typed_step (ρ1 (Valuable.of_expr e1) ★ Valuable.of_expr e2 ◁ ty) (e1 <- e2)
-               (λ _, ρ2 (Valuable.of_expr e1)).
+  Lemma typed_assign ρ1 ρ2 ty ν1 ν2:
+    ty.(ty_size) = 1%nat → update ty ρ1 ρ2 →
+    typed_step (ρ1 ν1 ★ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
   Proof.
     (* FIXME : I need to use [fupd_mask_mono], but I do not expect so. *)
-    iIntros (Hsz Hupd tid) "#HEAP!#[[Hρ1 H◁]$]". iApply fupd_wp. iApply fupd_mask_mono.
-    done. iMod (Hupd with "Hρ1") as (l vl) "(% & % & H↦ & Hupd)".
+    iIntros (Hsz Hupd tid) "!#(#HEAP & [Hρ1 H◁] & $)". wp_bind ν1.
+    iApply wp_mask_mono. done. iApply Hupd. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
     rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
-    iModIntro. rewrite heap_mapsto_vec_singleton.
-    destruct (Valuable.of_expr e2) eqn:He2; last by iDestruct "H◁" as "[]".
-    wp_bind e1. iApply Valuable.of_expr_wp. done.
-    wp_bind e2. iApply Valuable.of_expr_wp. done.
-    wp_write. iApply fupd_mask_mono. done. iApply "Hupd". iFrame.
-    by rewrite heap_mapsto_vec_singleton.
+    wp_bind ν2. iApply (has_type_wp with "[- $H◁]"). iIntros (v') "[% H◁]".
+    rewrite heap_mapsto_vec_singleton. wp_write.
+    iApply fupd_mask_mono. done. iApply ("Hupd" $! [_]).
+    rewrite heap_mapsto_vec_singleton has_type_value. iFrame.
   Qed.
 
-  Lemma typed_memcpy ρ1 ρ1' ρ2 ρ2' ty e1 e2:
+  Lemma typed_memcpy ρ1 ρ1' ρ2 ρ2' ty ν1 ν2:
     update ty ρ1' ρ1 → consumes ty ρ2' ρ2 →
-    typed_step (ρ1' (Valuable.of_expr e1) ★ ρ2' (Valuable.of_expr e2))
-               (e1 <-{ty.(ty_size)} !e2)
-               (λ _, ρ1 (Valuable.of_expr e1) ★ ρ2 (Valuable.of_expr e2))%P.
+    typed_step (ρ1' ν1 ★ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ★ ρ2 ν2)%P.
   Proof.
+    iIntros (Hupd Hcons tid) "!#(#HEAP&[H1 H2]&Htl)". wp_bind ν1.
+    iApply wp_mask_mono. done. iApply (Hupd with "[- $H1]").
+    iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
+    iApply wp_mask_mono. done. iApply (Hcons with "[- $H2 $Htl]").
+    iIntros (l' vl' q) "(% & % & H↦' & Hcons)".
     (* FIXME : I need to use [fupd_mask_mono], but I do not expect so. *)
-    iIntros (Hupd Hcons tid) "#HEAP!#[[H1 H2]Htl]". iApply fupd_wp. iApply fupd_mask_mono.
-    done. iMod (Hupd with "H1") as (l vl) "(% & % & H↦ & Hupd)".
-    iMod (Hcons with "[H2 Htl]") as (l' vl' q) "(% & % & H↦' & Hcons)". by iFrame.
-    iMod "Hcons". iModIntro.
-    wp_bind e1. iApply Valuable.of_expr_wp. done.
-    wp_bind e2. iApply Valuable.of_expr_wp. done.
+    iApply wp_fupd. iApply fupd_wp. iApply fupd_mask_mono. done. iMod "Hcons".
     iApply wp_memcpy; last iFrame "★#"; try done. iNext. iIntros "[H↦ H↦']".
+    (* FIXME : Idem. *)
     iApply fupd_mask_mono. done. iMod "Hcons" as "[Hown' Hcons]".
     iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame.
   Qed.
@@ -419,38 +423,36 @@ Section typing.
   Lemma typed_weaken ρ1 ρ2 e:
     typed_program ρ2 e → (ρ1 ⇒ ρ2) → typed_program ρ1 e.
   Proof.
-    iIntros (Hρ2 Hρ12 tid) "#HEAP!#[Hρ1 Htl]".
-    iMod (Hρ12 with "Hρ1"). iApply (Hρ2 with "HEAP"). by iFrame.
+    iIntros (Hρ2 Hρ12 tid) "!#(#HEAP & Hρ1 & Htl)".
+    iMod (Hρ12 with "Hρ1"). iApply Hρ2. by iFrame.
   Qed.
 
   Lemma typed_program_exists {A} ρ θ e:
     (∀ x:A, typed_program (ρ ★ θ x) e) →
     typed_program (ρ ★ ∃ x, θ x) e.
   Proof.
-    iIntros (Hwt tid) "#HEAP!#[[Hρ Hθ]?]". iDestruct "Hθ" as (x) "Hθ".
-    iApply (Hwt with "HEAP"). by iFrame.
+    iIntros (Hwt tid) "!#(#HEAP & [Hρ Hθ] & ?)". iDestruct "Hθ" as (x) "Hθ".
+    iApply Hwt. by iFrame.
   Qed.
 
   Lemma typed_step_program ρ θ e K:
     typed_step ρ e θ →
-    (∀ v, typed_program (θ (Some v)) (fill K (of_val v))) →
+    (∀ v, typed_program (θ v) (fill K (of_val v))) →
     typed_program ρ (fill K e).
   Proof.
-    iIntros (He HK tid) "#HEAP!#[Hρ Htl]".
-    iApply wp_bind. iApply wp_wand_r. iSplitL.
-    iApply (He with "HEAP [-]"); by iFrame.
-    iIntros (v) "[Hθ Htl]". iApply (HK with "HEAP"). by iFrame.
+    iIntros (He HK tid) "!#(#HEAP & Hρ & Htl)".
+    iApply wp_bind. iApply wp_wand_r. iSplitL. iApply He; by iFrame.
+    iIntros (v) "[Hθ Htl]". iApply HK. by iFrame.
   Qed.
 
-  Lemma typed_if ρ e1 e2 e:
+  Lemma typed_if ρ e1 e2 ν:
     typed_program ρ e1 → typed_program ρ e2 →
-    typed_program (ρ ★ Valuable.of_expr e ◁ bool) (if: e then e1 else e2).
+    typed_program (ρ ★ ν ◁ bool) (if: ν then e1 else e2).
   Proof.
-    iIntros (He1 He2 tid) "#HEAP!#[[Hρ H◁]Htl]".
-    destruct (Valuable.of_expr e) eqn:He; try iDestruct "H◁" as "[]".
-    iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
-    wp_bind e. iApply Valuable.of_expr_wp. done. wp_if. destruct b; iNext.
-    iApply (He1 with "HEAP"); by iFrame. iApply (He2 with "HEAP"); by iFrame.
+    iIntros (He1 He2 tid) "!#(#HEAP & [Hρ H◁] & Htl)".
+    wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% H◁]".
+    rewrite has_type_value. iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
+    wp_if. destruct b; iNext. iApply He1; by iFrame. iApply He2; by iFrame.
   Qed.
 
 End typing.
diff --git a/valuable.v b/valuable.v
deleted file mode 100644
index 47cc322f..00000000
--- a/valuable.v
+++ /dev/null
@@ -1,30 +0,0 @@
-From lrust Require Export lang notation proofmode wp_tactics.
-
-Module Valuable.
-
-Definition t := option val.
-Definition proj (n : Z) : t → t :=
-  (≫= λ v, match v with LitV (LitLoc l) => Some (#(shift_loc l n)) | _ => None end).
-
-Fixpoint of_expr (e : expr) : t :=
-  match e with
-  | BinOp ProjOp e (Lit (LitInt n)) => proj n (of_expr e)
-  | e => to_val e
-  end.
-
-Lemma of_expr_wp `{irisG lrust_lang Σ} e v Φ :
-  of_expr e = Some v → Φ v ⊢ WP e {{ Φ }}.
-Proof.
-  revert v Φ. induction e=>v Φ Hv; iIntros; try done.
-  - inversion Hv; subst. by wp_value.
-  - by wp_value.
-  - destruct op; try done.
-    destruct e2; try done.
-    destruct l; try done.
-    wp_bind e1. simpl in Hv.
-    destruct (of_expr e1) as [v1|]; last done.
-    iApply IHe1. done. destruct v1; try done. destruct l; try done.
-    inversion Hv. subst. wp_op. eauto.
-Qed.
-
-End Valuable.
\ No newline at end of file
-- 
GitLab