diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4fe9f93ba689a48603aa4550f871a257ba0f8bea..cc6beab60057a94ede51a0def6041cf9cee81f8d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -143,6 +143,23 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   initial heap.
 * Rename `mapsto_mapsto_ne` to `mapsto_frac_ne`, and add a simpler
   `mapsto_ne` that does not require reasoning about fractions.
+* Extend the `gen_heap` library with read-only points-to assertions using
+  [discardable fractions](iris/algebra/dfrac.v).
+  + The `mapsto` connective now takes a `dfrac` rather than a `frac` (i.e.,
+    positive rational number `Qp`).
+  + The notation `l ↦{ dq } v` is generalized to discardable fractions
+    `dq : dfrac`.
+  + The new notation `l ↦{# q} v` is used for a concrete fraction `q : frac`
+    (e.g., to enable writing `l ↦{# 1/2} v`).
+  + The new notation `l ↦□ v` is used for the discarded fraction. This
+    persistent proposition provides read-only access to `l`.
+  + The lemma `mapsto_persist : l ↦{dq} v ==∗ l ↦□ v` is used for making the
+    location `l` read-only.
+  + See the changes to HeapLang for an indication on how to adapt your language.
+  + See the changes to iris-examples for an indication on how to adapt your
+    development. In particular, instead of `∃ q, l ↦{q} v` you likely want to
+    use `l ↦□ v`, which has the advantage of being persistent (rather than just
+    duplicable).
 
 **Changes in `program_logic`:**
 
@@ -153,6 +170,9 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   avoid TC search attempting to apply this instance all the time.
 * Merge `wp_value_inv`/`wp_value_inv'` into `wp_value_fupd`/`wp_value_fupd'` by
   making the lemma bidirectional.
+* Generalize HeapLang's `mapsto` (`↦`), `array` (`↦∗`), and atomic heap
+  connectives to discardable fractions. See the CHANGELOG entry in the category
+  `base_logic` for more information.
 
 **Changes in `heap_lang`:**
 
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index c6f57bb4ff1b169a60fc2207abdb5e67fd8a4d8b..d3b668f05421b282a875a53d997ccb7d1f3b983b 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -161,6 +161,16 @@ Section dfrac.
   Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
 
+  Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
+  Proof.
+    destruct dq as [q'| |q']; [|done|].
+    - apply Qp_lt_le_trans, Qp_lt_add_r.
+    - intro Hlt. etrans; last apply Hlt. apply Qp_lt_add_r.
+  Qed.
+
+  Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
+  Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
+
   Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
   Proof. done. Qed.
 
@@ -174,12 +184,11 @@ Section dfrac.
   Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
 
   (** Discarding a fraction is a frame preserving update. *)
-  Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded.
+  Lemma dfrac_discard_update dq : dq ~~> DfracDiscarded.
   Proof.
-    intros n [[q'| |q']|];
-      rewrite /op /cmra_op -!cmra_discrete_valid_iff /valid /cmra_valid //=.
-    - intros. apply Qp_lt_le_trans with (q + q')%Qp; [|done]. apply Qp_lt_add_r.
-    - intros. apply Qp_le_lt_trans with (q + q')%Qp; [|done]. apply Qp_le_add_r.
+    intros n [[q'| |q']|]; rewrite -!cmra_discrete_valid_iff //=.
+    - apply dfrac_valid_own_r.
+    - apply cmra_valid_op_r.
   Qed.
 
 End dfrac.
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index a70dd4db1e05963492d8dde6416a97e67d916a75..137e1cd55d72af58f5296b6474dc6ac481d0847a 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -378,13 +378,13 @@ Section lemmas.
       rewrite lookup_insert_ne //.
   Qed.
 
-  Lemma gmap_view_persist k q v :
-    gmap_view_frag k (DfracOwn q) v ~~> gmap_view_frag k DfracDiscarded v.
+  Lemma gmap_view_persist k dq v :
+    gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.
     apply view_update_frag=>m n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
     - rewrite lookup_singleton.
-      edestruct (Hrel k ((DfracOwn q, to_agree v) â‹…? bf !! k)) as (v' & Hdf & Hva & Hm).
+      edestruct (Hrel k ((dq, to_agree v) â‹…? bf !! k)) as (v' & Hdf & Hva & Hm).
       { rewrite lookup_op lookup_singleton.
         destruct (bf !! k) eqn:Hbf; by rewrite Hbf. }
       rewrite Some_op_opM. intros [= Hbf].
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 1963deca972323d493aa4ad4e5553ecd83174172..41c7652b25021e29bdafe5fff15b70d8ae7ae198 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.
@@ -7,7 +8,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 (** This file provides a generic mechanism for a language-level point-to
-connective [l ↦{q} v] reflecting the physical heap.  This library is designed to
+connective [l ↦{dq} v] reflecting the physical heap.  This library is designed to
 be used as a singleton (i.e., with only a single instance existing in any
 proof), with the [gen_heapG] typeclass providing the ghost names of that unique
 instance.  That way, [mapsto] does not need an explicit [gname] parameter.
@@ -20,7 +21,7 @@ physical state, you will likely want explicit ghost names and are thus better
 off using [algebra.lib.gmap_view] together with [base_logic.lib.own].
 
 This library is generic in the types [L] for locations and [V] for values and
-supports fractional permissions.  Next to the point-to connective [l ↦{q} v],
+supports fractional permissions.  Next to the point-to connective [l ↦{dq} v],
 which keeps track of the value [v] of a location [l], this library also provides
 a way to attach "meta" or "ghost" data to locations. This is done as follows:
 
@@ -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) (dq : dfrac) (v: V) : iProp Σ :=
+    own (gen_heap_name hG) (gmap_view_frag l dq (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,16 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
-Local Notation "l ↦{ q } v" := (mapsto l q 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.
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Local Notation "l ↦{ dq } v" := (mapsto l dq v)
+  (at level 20, format "l  ↦{ dq }  v") : bi_scope.
+Local Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
+  (at level 20, format "l  ↦□  v") : bi_scope.
+Local Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
+  (at level 20, format "l  ↦{# q }  v") : bi_scope.
+Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
+  (at level 20, format "l  ↦  v") : bi_scope.
 
 Section gen_heap.
   Context {L V} `{Countable L, !gen_heapG L V Σ}.
@@ -136,50 +144,59 @@ Section gen_heap.
   Implicit Types v : V.
 
   (** 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.
+  Global Instance mapsto_timeless l dq v : Timeless (l ↦{dq} v).
+  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 dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%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 dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ 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⌝.
+  Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     iIntros "H1 H2".
     iDestruct (mapsto_valid_2 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⌝.
+  Lemma mapsto_combine l dq1 dq2 v1 v2 :
+    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} 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⌝.
+  Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
+    ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} 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.
+  Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
+
+  (** Permanently turn any points-to predicate into a persistent
+      points-to predicate. *)
+  Lemma mapsto_persist l dq v : l ↦{dq} 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).
@@ -270,12 +287,11 @@ Section gen_heap.
       first by apply lookup_union_None.
   Qed.
 
-  Lemma gen_heap_valid σ l q v : gen_heap_interp σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
+  Lemma gen_heap_valid σ l dq v : gen_heap_interp σ -∗ l ↦{dq} 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..72ce1856a03c5ceff3499ddfcdb43719a8538daf 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -14,11 +14,18 @@ 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 Σ :=
-  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{q} v)%I.
-Notation "l ↦∗{ q } vs" := (array l q vs)
-  (at level 20, q at level 50, format "l  ↦∗{ q }  vs") : bi_scope.
-Notation "l ↦∗ vs" := (array l 1 vs)
+Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
+  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I.
+
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Notation "l ↦∗{ dq } vs" := (array l dq vs)
+  (at level 20, format "l  ↦∗{ dq }  vs") : bi_scope.
+Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)
+  (at level 20, format "l  ↦∗□  vs") : bi_scope.
+Notation "l ↦∗{# q } vs" := (array l (DfracOwn q) vs)
+  (at level 20, format "l  ↦∗{# q }  vs") : bi_scope.
+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,32 +39,31 @@ 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.
+Lemma array_nil l dq : l ↦∗{dq} [] ⊣⊢ emp.
 Proof. by rewrite /array. Qed.
 
-Lemma array_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
+Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
 Proof. by rewrite /array /= right_id loc_add_0. Qed.
 
-Lemma array_app l q vs ws :
-  l ↦∗{q} (vs ++ ws) ⊣⊢ l ↦∗{q} vs ∗ (l +ₗ length vs) ↦∗{q} ws.
+Lemma array_app l dq vs ws :
+  l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ length vs) ↦∗{dq} ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
   by setoid_rewrite loc_add_assoc.
 Qed.
 
-Lemma array_cons l q v vs : l ↦∗{q} (v :: vs) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vs.
+Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) ⊣⊢ l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs.
 Proof.
   rewrite /array big_sepL_cons loc_add_0.
   setoid_rewrite loc_add_assoc.
@@ -65,14 +71,14 @@ Proof.
   by setoid_rewrite Z.add_1_l.
 Qed.
 
-Global Instance array_cons_frame l q v vs R Q :
-  Frame false R (l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vs) Q →
-  Frame false R (l ↦∗{q} (v :: vs)) Q.
+Global Instance array_cons_frame l dq v vs R Q :
+  Frame false R (l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs) Q →
+  Frame false R (l ↦∗{dq} (v :: vs)) Q.
 Proof. by rewrite /Frame array_cons. Qed.
 
-Lemma update_array l q vs off v :
+Lemma update_array l dq vs off v :
   vs !! off = Some v →
-  ⊢ l ↦∗{q} vs -∗ ((l +ₗ off) ↦{q} v ∗ ∀ v', (l +ₗ off) ↦{q} v' -∗ l ↦∗{q} <[off:=v']>vs).
+  ⊢ l ↦∗{dq} vs -∗ ((l +ₗ off) ↦{dq} v ∗ ∀ v', (l +ₗ off) ↦{dq} v' -∗ l ↦∗{dq} <[off:=v']>vs).
 Proof.
   iIntros (Hlookup) "Hl".
   rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
@@ -90,9 +96,9 @@ Proof.
 Qed.
 
 (** * Rules for allocation *)
-Lemma mapsto_seq_array l q v n :
-  ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{q} v) -∗
-  l ↦∗{q} replicate n v.
+Lemma mapsto_seq_array l dq v n :
+  ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{dq} v) -∗
+  l ↦∗{dq} replicate n v.
 Proof.
   rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
   { done. }
@@ -144,9 +150,9 @@ Proof.
 Qed.
 
 (** * Rules for accessing array elements *)
-Lemma twp_load_offset s E l q off vs v :
+Lemma twp_load_offset s E l dq off vs v :
   vs !! off = Some v →
-  [[{ l ↦∗{q} vs }]] ! #(l +ₗ off) @ s; E [[{ RET v; l ↦∗{q} vs }]].
+  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
 Proof.
   iIntros (Hlookup Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -154,19 +160,19 @@ Proof.
   iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
   iApply "Hl2". iApply "Hl1".
 Qed.
-Lemma wp_load_offset s E l q off vs v :
+Lemma wp_load_offset s E l dq off vs v :
   vs !! off = Some v →
-  {{{ ▷ l ↦∗{q} vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗{q} vs }}}.
+  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
 Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_load_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
-  [[{ l ↦∗{q} vs }]] ! #(l +ₗ off) @ s; E [[{ RET vs !!! off; l ↦∗{q} vs }]].
+Lemma twp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
+  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
 Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
-Lemma wp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
-  {{{ ▷ l ↦∗{q} vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗{q} vs }}}.
+Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
+  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
 Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
 
 Lemma twp_store_offset s E l off vs v :
@@ -245,13 +251,13 @@ Proof.
   iApply (twp_cmpxchg_suc_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
+Lemma twp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
   vs !! off = Some v0 →
   v0 ≠ v1 →
   vals_compare_safe v0 v1 →
-  [[{ l ↦∗{q} vs }]]
+  [[{ l ↦∗{dq} vs }]]
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  [[{ RET (v0, #false); l ↦∗{q} vs }]].
+  [[{ RET (v0, #false); l ↦∗{dq} vs }]].
 Proof.
   iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -260,31 +266,31 @@ Proof.
   iIntros "Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
   rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
 Qed.
-Lemma wp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
+Lemma wp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
   vs !! off = Some v0 →
   v0 ≠ v1 →
   vals_compare_safe v0 v1 →
-  {{{ ▷ l ↦∗{q} vs }}}
+  {{{ ▷ l ↦∗{dq} vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (v0, #false); l ↦∗{q} vs }}}.
+  {{{ RET (v0, #false); l ↦∗{dq} vs }}}.
 Proof.
   iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_cmpxchg_fail_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma twp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
   vs !!! off ≠ v1 →
   vals_compare_safe (vs !!! off) v1 →
-  [[{ l ↦∗{q} vs }]]
+  [[{ l ↦∗{dq} vs }]]
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  [[{ RET (vs !!! off, #false); l ↦∗{q} vs }]].
+  [[{ RET (vs !!! off, #false); l ↦∗{dq} vs }]].
 Proof. intros. eapply twp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
-Lemma wp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma wp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
   vs !!! off ≠ v1 →
   vals_compare_safe (vs !!! off) v1 →
-  {{{ ▷ l ↦∗{q} vs }}}
+  {{{ ▷ l ↦∗{dq} vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (vs !!! off, #false); l ↦∗{q} vs }}}.
+  {{{ RET (vs !!! off, #false); l ↦∗{dq} vs }}}.
 Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
 
 Lemma twp_faa_offset s E l off vs (i1 i2 : Z) :
@@ -349,11 +355,11 @@ Proof.
   iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
 Qed.
 
-Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
+Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) dq v' v1 v2 v :
   v' ≠ v1 → vals_compare_safe v' v1 →
-  {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
+  {{{ proph p pvs ∗ ▷ l ↦{dq} v' }}}
     Resolve (CmpXchg #l v1 v2) #p v @ s; E
-  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
+  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{dq} v' }}}.
 Proof.
   iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
   iApply (wp_resolve with "Hp"); first done.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index e8d64a3c764b6e845446b2168844b3994dad1232..94a7fc428df86b00308bea70bc87b43f1f8831c9 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -70,11 +70,11 @@ Section proof.
     iApply (twp_array_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
   Qed.
 
-  Lemma twp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
+  Lemma twp_array_copy_to stk E (dst src : loc) vdst vsrc dq (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
-    [[{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }]]
+    [[{ dst ↦∗ vdst ∗ src ↦∗{dq} vsrc }]]
       array_copy_to #dst #src #n @ stk; E
-    [[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{q} vsrc }]].
+    [[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }]].
   Proof.
     iIntros (Hvdst Hvsrc Φ) "[Hdst Hsrc] HΦ".
     iInduction vdst as [|v1 vdst] "IH" forall (n dst src vsrc Hvdst Hvsrc);
@@ -87,22 +87,22 @@ Section proof.
     iIntros "[Hvdst Hvsrc]".
     iApply "HΦ"; by iFrame.
   Qed.
-  Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
+  Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc dq (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
-    {{{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }}}
+    {{{ dst ↦∗ vdst ∗ src ↦∗{dq} vsrc }}}
       array_copy_to #dst #src #n @ stk; E
-    {{{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{q} vsrc }}}.
+    {{{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }}}.
   Proof.
     iIntros (? ? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
     iApply (twp_array_copy_to with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
   Qed.
 
-  Lemma twp_array_clone stk E l q vl n :
+  Lemma twp_array_clone stk E l dq vl n :
     Z.of_nat (length vl) = n →
     (0 < n)%Z →
-    [[{ l ↦∗{q} vl }]]
+    [[{ l ↦∗{dq} vl }]]
       array_clone #l #n @ stk; E
-    [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }]].
+    [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{dq} vl }]].
   Proof.
     iIntros (Hvl Hn Φ) "Hvl HΦ".
     wp_lam.
@@ -114,12 +114,12 @@ Section proof.
       wp_pures.
       iApply "HΦ"; by iFrame.
   Qed.
-  Lemma wp_array_clone stk E l q vl n :
+  Lemma wp_array_clone stk E l dq vl n :
     Z.of_nat (length vl) = n →
     (0 < n)%Z →
-    {{{ l ↦∗{q} vl }}}
+    {{{ l ↦∗{dq} vl }}}
       array_clone #l #n @ stk; E
-    {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }}}.
+    {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{dq} vl }}}.
   Proof.
     iIntros (? ? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
     iApply (twp_array_clone with "H"); [auto..|]; iIntros (l') "H HΦ". by iApply "HΦ".
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 0679e493f1fee8ea436cf78da9558db95e85fe8f..85255d1272e8bdb04839c389477127e592ff5a6e 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -14,23 +14,25 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   store : val;
   cmpxchg : val;
   (* -- predicates -- *)
-  mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
+  mapsto (l : loc) (dq: 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_persistent l v :> Persistent (mapsto l DfracDiscarded v);
   mapsto_as_fractional l q v :>
-    AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
-  mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
+    AsFractional (mapsto l (DfracOwn q) v) (λ q, mapsto l (DfracOwn q) v) q;
+  mapsto_agree l dq1 dq2 v1 v2 : mapsto l dq1 v1 -∗ mapsto l dq2 v2 -∗ ⌜v1 = v2⌝;
+  mapsto_persist l dq v : mapsto l dq v ==∗ mapsto l DfracDiscarded v;
   (* -- 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,27 +41,30 @@ 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. *)
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Module notation.
-Notation "l ↦{ q } v" := (mapsto l q 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 ↦{ dq } v" := (mapsto l dq v)
+    (at level 20, format "l  ↦{ dq }  v") : bi_scope.
+  Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
+    (at level 20, format "l  ↦□  v") : bi_scope.
+  Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
+    (at level 20, format "l  ↦{# q }  v") : bi_scope.
+  Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
+    (at level 20, format "l  ↦  v") : bi_scope.
 
-Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
-  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
-Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
+  Notation "'ref' e" := (alloc e) : expr_scope.
+  Notation "! e" := (load e) : expr_scope.
+  Notation "e1 <- e2" := (store e1 e2) : expr_scope.
 
-Notation "'ref' e" := (alloc e) : expr_scope.
-Notation "! e" := (load e) : expr_scope.
-Notation "e1 <- e2" := (store e1 e2) : expr_scope.
-
-Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
+  Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
 
 End notation.
 
@@ -70,8 +75,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.
@@ -149,4 +154,5 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
      load_spec := primitive_load_spec;
      store_spec := primitive_store_spec;
      cmpxchg_spec := primitive_cmpxchg_spec;
+     mapsto_persist := primitive_laws.mapsto_persist;
      mapsto_agree := primitive_laws.mapsto_agree |}.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 604ecac1bb2543ff22b08b45fe4e3fc80e9249e4..174257263f0237b8275311182e200cb766b43447 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..0f168abe0db1c3653d00d26d89edb7a6693bd112 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,10 +28,16 @@ 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))
-  (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))
-  (at level 20) : bi_scope.
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
+  (at level 20, format "l  ↦{ dq }  v") : bi_scope.
+Notation "l ↦□ v" := (mapsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))
+  (at level 20, format "l  ↦□  v") : bi_scope.
+Notation "l ↦{# q } v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn q) (Some v%V))
+  (at level 20, format "l  ↦{# q }  v") : bi_scope.
+Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
+  (at level 20, format "l  ↦  v") : bi_scope.
 
 (** Same for [gen_inv_heap], except that these are higher-order notations so to
 make setoid rewriting in the predicate [I] work we need actual definitions
@@ -277,29 +283,32 @@ 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 dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
 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⌝.
+Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
+  l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
 Proof.
   iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
 Qed.
-Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
+Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
 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⌝.
+Lemma mapsto_combine l dq1 dq2 v1 v2 :
+  l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} 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⌝.
+Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
+  ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_frac_ne. Qed.
-Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_ne. Qed.
 
+Lemma mapsto_persist l dq v : l ↦{dq} 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 +381,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.
@@ -446,19 +455,19 @@ Proof.
   iApply (twp_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_load s E l q v :
-  [[{ l ↦{q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{q} v }]].
+Lemma twp_load s E l dq v :
+  [[{ l ↦{dq} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{dq} v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
-Lemma wp_load s E l q v :
-  {{{ ▷ l ↦{q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{q} v }}}.
+Lemma wp_load s E l dq v :
+  {{{ ▷ l ↦{dq} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{dq} 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 :
@@ -479,10 +488,10 @@ Proof.
   iApply (twp_store with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
+Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
   v' ≠ v1 → vals_compare_safe v' v1 →
-  [[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }]].
+  [[{ l ↦{dq} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  [[{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -490,10 +499,10 @@ Proof.
   rewrite bool_decide_false //.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
-Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
+Lemma wp_cmpxchg_fail s E l dq v' v1 v2 :
   v' ≠ v1 → vals_compare_safe v' v1 →
-  {{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }}}.
+  {{{ ▷ l ↦{dq} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  {{{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }}}.
 Proof.
   iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_cmpxchg_fail with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
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..0118b3b39b5ee0e3a75e6a0b4b7731637d279d46 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
@@ -151,6 +151,34 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   |={⊤}=> True
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  v : val
+  Φ : val → iPropI Σ
+  ============================
+  "Hl" : l ↦□ v
+  --------------------------------------â–¡
+  "HΦ" : ▷ (True -∗ Φ v)
+  --------------------------------------∗
+  WP ! #l {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  dq : dfrac
+  l : loc
+  v : val
+  Φ : val → iPropI Σ
+  ============================
+  "Hl" : l ↦{dq} v
+  "HΦ" : True -∗ Φ v
+  --------------------------------------∗
+  WP ! #l [{ v, Φ v }]
+  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4ae4e64032e79eb540609e5aaa4273644f7f7422..88c1030244cb0a45123c0ff51d6db82934970ba5 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,48 @@ Section tests.
   Abort.
 End tests.
 
+Section mapsto_tests.
+  Context `{!heapG Σ}.
+
+  (* Test that the different versions of mapsto work with the tactics, parses,
+     and prints correctly. *)
+
+  (* 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Φ". Show. 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.
+
+  (* Loading from the general mapsto for any [dfrac]. *)
+  Lemma general_mapsto dq l v :
+    [[{ l ↦{dq} v }]] ! #l [[{ RET v; True }]].
+  Proof. 
+    iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
+  Qed.
+
+End mapsto_tests.
+
 Section inv_mapsto_tests.
   Context `{!heapG Σ}.