diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index c6f57bb4ff1b169a60fc2207abdb5e67fd8a4d8b..755f2d4ef778d568a55ce516e98530f7a98443ae 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -32,6 +32,13 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
+Declare Scope dfrac_scope.
+Delimit Scope dfrac_scope with dfrac.
+
+Notation "# q" := (DfracOwn q%Qp) (at level 8, format "# q") : dfrac_scope.
+Notation "#â–¡" := (DfracDiscarded) : dfrac_scope.
+Notation "â–¡" := (DfracDiscarded) : dfrac_scope.
+
 Section dfrac.
   Canonical Structure dfracO := leibnizO dfrac.
 
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 1963deca972323d493aa4ad4e5553ecd83174172..b1ec17e94e365f278b8facf6cd080b4ec0d0abd1 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -1,5 +1,6 @@
 From stdpp Require Export namespaces.
 From iris.algebra Require Import gmap_view namespace_map agree frac.
+From iris.algebra Require Export dfrac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
@@ -100,8 +101,8 @@ Section definitions.
     own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V))) ∗
     own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L gnameO)).
 
-  Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
-    own (gen_heap_name hG) (gmap_view_frag l (DfracOwn q) (v : leibnizO V)).
+  Definition mapsto_def (l : L) (q : dfrac) (v: V) : iProp Σ :=
+    own (gen_heap_name hG) (gmap_view_frag l q (v : leibnizO V)).
   Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
   Definition mapsto := mapsto_aux.(unseal).
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
@@ -122,9 +123,9 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
-Local Notation "l ↦{ q } v" := (mapsto l q v)
+Local Notation "l ↦{ q } v" := (mapsto l q%dfrac v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
-Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
+Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
 
 Section gen_heap.
   Context {L V} `{Countable L, !gen_heapG L V Σ}.
@@ -137,25 +138,27 @@ Section gen_heap.
 
   (** General properties of mapsto *)
   Global Instance mapsto_timeless l q v : Timeless (l ↦{q} v).
-  Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
-  Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
+  Proof. rewrite mapsto_eq. apply _. Qed.
+  Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{#q} v)%I.
   Proof.
     intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_add //.
   Qed.
   Global Instance mapsto_as_fractional l q v :
-    AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
+    AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
   Proof. split; [done|]. apply _. Qed.
+  Global Instance mapsto_persistent l v : Persistent (l ↦{#□} v).
+  Proof. rewrite mapsto_eq. apply _. Qed.
 
-  Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜q ≤ 1⌝%Qp.
+  Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜✓ q⌝%Qp.
   Proof.
     rewrite mapsto_eq. iIntros "Hl".
     iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
   Qed.
-  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ v1 = v2⌝.
+  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 ⋅ q2) ∧ v1 = v2⌝.
   Proof.
     rewrite mapsto_eq. iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
-    eauto.
+    auto.
   Qed.
   (** Almost all the time, this is all you really need. *)
   Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
@@ -166,20 +169,27 @@ Section gen_heap.
   Qed.
 
   Lemma mapsto_combine l q1 q2 v1 v2 :
-    l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 + q2} v1 ∗ ⌜v1 = v2⌝.
+    l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 ⋅ q2} v1 ∗ ⌜v1 = v2⌝.
   Proof.
     iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
-    iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
+    iCombine "Hl1 Hl2" as "Hl".
+    rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_op.
+    auto.
   Qed.
 
   Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
-    ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+    ¬ ✓(q1 ⋅ q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof.
     iIntros (?) "Hl1 Hl2"; iIntros (->).
     by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
   Qed.
   Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
-  Proof. apply mapsto_frac_ne, Qp_not_add_le_l. Qed.
+  Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
+
+  (** Permanently turn a fractional points-to predicate into a persistent
+      points-to predicate. *)
+  Lemma mapsto_persist l q v : l ↦{#q} v ==∗ l ↦{#□} v.
+  Proof. rewrite mapsto_eq. apply own_update, gmap_view_persist. Qed.
 
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
@@ -273,9 +283,8 @@ Section gen_heap.
   Lemma gen_heap_valid σ l q v : gen_heap_interp σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
-    rewrite /gen_heap_interp mapsto_eq /mapsto_def.
-    iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
-    iPureIntro. done.
+    rewrite /gen_heap_interp mapsto_eq.
+    by iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
   Qed.
 
   Lemma gen_heap_update σ l v1 v2 :
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index da06674624ff70d661a9629958d63ca4a672fd69..ff8b540fdd9ded5387ff645dd9c2f65a11636f50 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -20,7 +20,7 @@ using a separate assertion [inv_mapsto_own] for "invariant" locations, we can
 keep all the other proofs that do not need it conservative.  *)
 
 Definition inv_heapN: namespace := nroot .@ "inv_heap".
-Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
+Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
 
 Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmraT := gmapUR L $ prodR
   (optionR $ exclR $ leibnizO V)
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index addf300bad70e2ce2290ef2449e2956b792fe269..18f4a1fe1a8ea69641402447cc30f2c0472b1e45 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -14,11 +14,11 @@ From iris.prelude Require Import options.
 (** The [array] connective is a version of [mapsto] that works
 with lists of values. *)
 
-Definition array `{!heapG Σ} (l : loc) (q : Qp) (vs : list val) : iProp Σ :=
+Definition array `{!heapG Σ} (l : loc) (q : dfrac) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{q} v)%I.
-Notation "l ↦∗{ q } vs" := (array l q vs)
+Notation "l ↦∗{ q } vs" := (array l q%dfrac vs)
   (at level 20, q at level 50, format "l  ↦∗{ q }  vs") : bi_scope.
-Notation "l ↦∗ vs" := (array l 1 vs)
+Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
   (at level 20, format "l  ↦∗  vs") : bi_scope.
 
 (** We have [FromSep] and [IntoSep] instances to split the fraction (via the
@@ -32,15 +32,14 @@ Implicit Types Φ : val → iProp Σ.
 Implicit Types σ : state.
 Implicit Types v : val.
 Implicit Types vs : list val.
-Implicit Types q : Qp.
 Implicit Types l : loc.
 Implicit Types sz off : nat.
 
 Global Instance array_timeless l q vs : Timeless (array l q vs) := _.
 
-Global Instance array_fractional l vs : Fractional (λ q, l ↦∗{q} vs)%I := _.
+Global Instance array_fractional l vs : Fractional (λ q, l ↦∗{#q} vs)%I := _.
 Global Instance array_as_fractional l q vs :
-  AsFractional (l ↦∗{q} vs) (λ q, l ↦∗{q} vs)%I q.
+  AsFractional (l ↦∗{#q} vs) (λ q, l ↦∗{#q} vs)%I q.
 Proof. split; done || apply _. Qed.
 
 Lemma array_nil l q : l ↦∗{q} [] ⊣⊢ emp.
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 0679e493f1fee8ea436cf78da9558db95e85fe8f..08c8a4412910fb5b50aba3e1183222b596211ab3 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -14,23 +14,23 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   store : val;
   cmpxchg : val;
   (* -- predicates -- *)
-  mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
+  mapsto (l : loc) (q: dfrac) (v : val) : iProp Σ;
   (* -- mapsto properties -- *)
   mapsto_timeless l q v :> Timeless (mapsto l q v);
-  mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
+  mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
   mapsto_as_fractional l q v :>
-    AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
+    AsFractional (mapsto l (DfracOwn q) v) (λ q, mapsto l (DfracOwn q) v) q;
   mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
   (* -- operation specs -- *)
   alloc_spec (v : val) :
-    {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
+    {{{ True }}} alloc v {{{ l, RET #l; mapsto l (DfracOwn 1) v }}};
   free_spec (l : loc) (v : val) :
-    {{{ mapsto l 1 v }}} free #l {{{ l, RET #l; True }}};
+    {{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
   load_spec (l : loc) :
     ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀ v, mapsto l 1 v >>> store #l w @ ⊤
-      <<< mapsto l 1 w, RET #() >>>;
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ⊤
+      <<< mapsto l (DfracOwn 1) w, RET #() >>>;
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
   is outside the atomic triple, which makes it much easier to use -- and the
@@ -39,17 +39,17 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   [destruct (decide (a = b))] and it will simplify in both places. *)
   cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ ⊤
-      <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ⊤
+      <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
 Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
 Module notation.
-Notation "l ↦{ q } v" := (mapsto l q v)
+Notation "l ↦{ q } v" := (mapsto l q%dfrac v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
-Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
+Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
 
 Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
@@ -70,8 +70,8 @@ Section derived.
 
   Lemma cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l 1 v >>> CAS #l w1 w2 @ ⊤
-    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ⊤
+    <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET #if decide (v = w1) then true else false >>>.
   Proof.
     iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 604ecac1bb2543ff22b08b45fe4e3fc80e9249e4..80ac951ce2e9503bae64f9dd9e70e2d68db49f5b 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -111,8 +111,8 @@ Section increment.
   (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
      connective that works on [option Qp] (the type of 1-q). *)
   Lemma weak_incr_spec (l: loc) (v : Z) :
-    l ↦{1/2} #v -∗
-    <<< ∀ (v' : Z), l ↦{1/2} #v' >>>
+    l ↦{#(1/2)} #v -∗
+    <<< ∀ (v' : Z), l ↦{#(1/2)} #v' >>>
       weak_incr #l @ ⊤
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 1caa7591696f623babe3b781ba4c7cbf9d4061be..7952803e879ad8cb931e17b55723a3c342fcb56e 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,9 +28,9 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
 
 (** Since we use an [option val] instance of [gen_heap], we need to overwrite
 the notations.  That also helps for scopes and coercions. *)
-Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q (Some v%V))
+Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q%dfrac (Some v%V))
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
-Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l 1%Qp (Some v%V))
+Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
   (at level 20) : bi_scope.
 
 (** Same for [gen_inv_heap], except that these are higher-order notations so to
@@ -277,10 +277,10 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
-Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜q ≤ 1⌝%Qp.
+Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜✓ q⌝%Qp.
 Proof. apply mapsto_valid. Qed.
 Lemma mapsto_valid_2 l q1 q2 v1 v2 :
-  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ v1 = v2⌝.
+  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 ⋅ q2) ∧ v1 = v2⌝.
 Proof.
   iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
 Qed.
@@ -288,18 +288,21 @@ Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v
 Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
 
 Lemma mapsto_combine l q1 q2 v1 v2 :
-  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 + q2} v1 ∗ ⌜v1 = v2⌝.
+  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 ⋅ q2} v1 ∗ ⌜v1 = v2⌝.
 Proof.
-  iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
-  iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
+  iIntros "Hl1 Hl2". iDestruct (mapsto_combine with "Hl1 Hl2") as "[$ Heq]".
+  by iDestruct "Heq" as %[= ->].
 Qed.
 
 Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
-  ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+  ¬ ✓(q1 ⋅ q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_frac_ne. Qed.
 Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_ne. Qed.
 
+Lemma mapsto_persist l q v : l ↦{#q} v ==∗ l ↦{#□} v.
+Proof. apply mapsto_persist. Qed.
+
 Global Instance inv_mapsto_own_proper l v :
   Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto_own l v).
 Proof.
@@ -372,7 +375,7 @@ Proof.
 Qed.
 
 Lemma heap_array_to_seq_mapsto l v (n : nat) :
-  ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.mapsto l' 1 ov) -∗
+  ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.mapsto l' (DfracOwn 1) ov) -∗
   [∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v.
 Proof.
   iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
@@ -458,7 +461,7 @@ Lemma wp_load s E l q v :
   {{{ ▷ l ↦{q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{q} v }}}.
 Proof.
   iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
-  iApply (twp_load with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+  iApply (twp_load with "H"). iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_store s E l v' v :
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index f2441bbaa6392a9db2b608fa552c6636b653f58a..6bf7a0fe078535cff948b9a7ae5249ced9fc106c 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -218,7 +218,7 @@ Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
   (0 < n)%Z →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀ l,
-    match envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ' with
+    match envs_app false (Esnoc Enil j (array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ' with
     | Some Δ'' =>
        envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Φ }})
     | None => False
@@ -236,7 +236,7 @@ Qed.
 Lemma tac_twp_allocN Δ s E j K v n Φ :
   (0 < n)%Z →
   (∀ l,
-    match envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ with
+    match envs_app false (Esnoc Enil j (array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ with
     | Some Δ' =>
        envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }])
     | None => False
@@ -314,26 +314,31 @@ Proof.
   apply sep_mono_r, wand_intro_r. rewrite right_id //.
 Qed.
 
-Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
+Lemma tac_wp_load Δ Δ' s E i K b l q v Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
+  envs_lookup i Δ' = Some (b, l ↦{q} v)%I →
   envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ???.
+  rewrite envs_entails_eq=> ?? Hi.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-  by apply later_mono, sep_mono_r, wand_mono.
+  apply later_mono.
+  destruct b; simpl.
+  * iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
+  * by apply sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_load Δ s E i K l q v Φ :
-  envs_lookup i Δ = Some (false, l ↦{q} v)%I →
+Lemma tac_twp_load Δ s E i K b l q v Φ :
+  envs_lookup i Δ = Some (b, l ↦{q} v)%I →
   envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_eq=> ??.
+  rewrite envs_entails_eq=> ? Hi.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
   rewrite envs_lookup_split //; simpl.
-  by apply sep_mono_r, wand_mono.
+  destruct b; simpl.
+  - iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
+  - iIntros "[$ He]". iIntros "Hl". iApply Hi. iApply "He". iFrame "Hl".
 Qed.
 
 Lemma tac_wp_store Δ Δ' s E i K l v v' Φ :
diff --git a/tests/atomic.ref b/tests/atomic.ref
index c9e56f2c4d8c7f34b554616b798d6daf90597732..eb691fb7fadba8cba614547a193c1cf15b945e83 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -9,7 +9,7 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
+  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
        << l ↦{q} v0, COMM Q -∗ Q >>
   
 "non_laterable"
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 457f073b79d226abe150ab03648fb22948d1e5a7..57f3cc49e6ec9a58dfe135b2b782894a0a289605 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -74,8 +74,8 @@
   heapG0 : heapG Σ
   l : loc
   ============================
-  "Hl1" : l ↦{1 / 2} #0
-  "Hl2" : l ↦{1 / 2} #0
+  "Hl1" : l ↦{#(1 / 2)} #0
+  "Hl2" : l ↦{#(1 / 2)} #0
   --------------------------------------∗
   |={⊤}=> True
   
@@ -124,10 +124,10 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   l : loc
   vs : list val
   ============================
-  "Hl1" : l ↦∗{1 / 2} vs
-  "Hl2" : l ↦∗{1 / 2} vs
+  "Hl1" : l ↦∗{#(1 / 2)} vs
+  "Hl2" : l ↦∗{#(1 / 2)} vs
   --------------------------------------∗
-  l ↦∗{1 / 2} vs ∗ l ↦∗{1 / 2} vs
+  l ↦∗{#(1 / 2)} vs ∗ l ↦∗{#(1 / 2)} vs
   
 "test_wp_finish_fupd"
      : string
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4ae4e64032e79eb540609e5aaa4273644f7f7422..eea231e956cd444a16ddd3eb838e460e87c76ea2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -212,14 +212,14 @@ Section tests.
 
   Check "test_array_fraction_destruct".
   Lemma test_array_fraction_destruct l vs :
-    l ↦∗ vs -∗ l ↦∗{1/2} vs ∗ l ↦∗{1/2} vs.
+    l ↦∗ vs -∗ l ↦∗{#(1/2)} vs ∗ l ↦∗{#(1/2)} vs.
   Proof.
     iIntros "[Hl1 Hl2]". Show.
     by iFrame.
   Qed.
 
   Lemma test_array_fraction_combine l vs :
-    l ↦∗{1/2} vs -∗ l↦∗{1/2} vs -∗ l ↦∗ vs.
+    l ↦∗{#(1/2)} vs -∗ l↦∗{#(1/2)} vs -∗ l ↦∗ vs.
   Proof.
     iIntros "Hl1 Hl2".
     iSplitL "Hl1"; by iFrame.
@@ -233,7 +233,7 @@ Section tests.
   Qed.
 
   Lemma test_array_app_split l vs1 vs2 :
-    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗{1/2} (vs1 ++ vs2).
+    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗{#(1/2)} (vs1 ++ vs2).
   Proof.
     iIntros "[$ _]". (* splits the fraction, not the app *)
   Qed.
@@ -265,6 +265,38 @@ Section tests.
   Abort.
 End tests.
 
+Section persistent_mapsto_tests.
+  Context `{!heapG Σ}.
+
+  (* Loading from a persistent points-to predicate in the _persistent_ context. *)
+  Lemma persistent_mapsto_load_persistent l v :
+    {{{ l ↦{#□} v }}} ! #l {{{ RET v; True }}}.
+  Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.
+
+  (* Loading from a persistent points-to predicate in the _spatial_ context. *)
+  Lemma persistent_mapsto_load_spatial l v :
+    {{{ l ↦{#□} v }}} ! #l {{{ RET v; True }}}.
+  Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.
+
+  Lemma persistent_mapsto_twp_load_persistent l v :
+    [[{ l ↦{#□} v }]] ! #l [[{ RET v; True }]].
+  Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.
+
+  Lemma persistent_mapsto_twp_load_spatial l v :
+    [[{ l ↦{#□} v }]] ! #l [[{ RET v; True }]].
+  Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.
+
+  Lemma persistent_mapsto_load l (n : nat) :
+    {{{ l ↦ #n }}} Store #l (! #l + #5) ;; ! #l {{{ RET #(n + 5); l ↦{#□} #(n + 5) }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ".
+    wp_load. wp_store.
+    iMod (mapsto_persist with "Hl") as "#Hl".
+    wp_load. by iApply "HΦ".
+  Qed.
+
+End persistent_mapsto_tests.
+
 Section inv_mapsto_tests.
   Context `{!heapG Σ}.