From 757490f77145b41ccda652fb740cbdf5f915650b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 31 Mar 2020 10:29:09 +0200
Subject: [PATCH] make a user-mask available inside lifetime logic view shifts

---
 theories/lifetime/lifetime.v                  |  4 ++--
 theories/lifetime/lifetime_sig.v              |  9 +++++---
 theories/lifetime/model/accessors.v           |  6 ++---
 theories/lifetime/model/creation.v            | 14 +++++++-----
 theories/lifetime/model/definitions.v         |  8 ++++---
 theories/lifetime/model/primitive.v           |  2 +-
 theories/typing/lft_contexts.v                |  2 +-
 theories/typing/lib/arc.v                     | 22 ++++++++++++++-----
 theories/typing/lib/rc/rc.v                   | 14 ++++++------
 theories/typing/lib/refcell/ref_code.v        |  8 +++----
 theories/typing/lib/refcell/refcell.v         |  4 ++--
 theories/typing/lib/refcell/refmut_code.v     |  6 ++---
 theories/typing/lib/rwlock/rwlock.v           |  2 +-
 theories/typing/lib/rwlock/rwlock_code.v      |  2 +-
 theories/typing/lib/rwlock/rwlockreadguard.v  |  2 +-
 .../typing/lib/rwlock/rwlockreadguard_code.v  |  5 +++--
 theories/typing/programs.v                    |  2 +-
 17 files changed, 65 insertions(+), 47 deletions(-)

diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 6f08298d..07bc591e 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -29,7 +29,7 @@ Implicit Types κ : lft.
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-    (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    (▷ P ∗ ∀ Q, ▷ (▷ Q ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
     ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (?) "#LFT HP".
@@ -55,7 +55,7 @@ Qed.
 Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ} Q ∗ q.[κ].
+    ∀ Q, ▷ (▷ Q ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ} Q ∗ q.[κ].
 Proof.
   iIntros (?) "#LFT HP Htok".
   iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 8ae5bd7e..ddc0db15 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -6,6 +6,9 @@ From iris.bi Require Import fractional.
 Set Default Proof Using "Type".
 
 Definition lftN : namespace := nroot .@ "lft".
+(** A mask inside the lifetime logic namespace that users may use.
+This is still available in the "consequence" view shift of borrow accessors. *)
+Definition lft_userN : namespace := nroot .@ "lft" .@ "usr".
 
 Module Type lifetime_sig.
   (** CMRAs needed by the lifetime logic  *)
@@ -93,7 +96,7 @@ Module Type lifetime_sig.
   Parameter lft_dead_static : [† static] -∗ False.
 
   Parameter lft_create : ∀ E, ↑lftN ⊆ E →
-    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,∅}▷=∗ [†κ]).
+    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,↑lft_userN}▷=∗ [†κ]).
   Parameter bor_create : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
   Parameter bor_fake : ∀ E κ P,
@@ -123,11 +126,11 @@ Module Type lifetime_sig.
                 ([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
   Parameter bor_acc_strong : ∀ E q κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
+      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
   Parameter bor_acc_atomic_strong : ∀ E κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
       (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-         ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+         ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
            ([†κ] ∗ |={E∖↑lftN,E}=> True).
 
   (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 0bd9c9b7..7a17291d 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -55,7 +55,7 @@ Proof.
 Qed.
 
 Lemma add_vs Pb Pb' P Q Pi κ :
-  ▷ (Pb ≡ (P ∗ Pb')) -∗ lft_vs κ Pb Pi -∗ (▷ Q -∗ [†κ] ={∅}=∗ ▷ P) -∗
+  ▷ (Pb ≡ (P ∗ Pb')) -∗ lft_vs κ Pb Pi -∗ (▷ Q -∗ [†κ] ={↑lft_userN}=∗ ▷ P) -∗
   lft_vs κ (Q ∗ Pb') Pi.
 Proof.
   iIntros "#HEQ Hvs HvsQ". iApply (lft_vs_cons with "[-Hvs] Hvs").
@@ -148,7 +148,7 @@ Qed.
 Lemma bor_acc_strong E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-    ∀ Q, ▷(▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
+    ∀ Q, ▷(▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
 Proof.
   unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
   iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
@@ -215,7 +215,7 @@ Lemma bor_acc_atomic_strong E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
    (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
     ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index a9b1c3f6..5e3902e6 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -16,7 +16,7 @@ Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
     ([∗ set] κ' ∈ K', lft_inv_alive κ'))%I in
   (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K) →
   (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K') →
-  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
+  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑lft_userN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
 Proof.
   iIntros (Iinv HK HK') "(HI & Hdead & Halive) Hlalive Hκ".
   rewrite lft_inv_alive_unfold;
@@ -33,7 +33,9 @@ Proof.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
       as %[?%nat_included _]%auth_both_valid; lia. }
-  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
+  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//.
+  { (* FIXME [solve_ndisj] fails *)
+    etrans; last exact: union_subseteq_l. solve_ndisj. }
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
   iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
@@ -61,7 +63,7 @@ Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lf
   (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
   (∀ κ, lft_alive_in A κ → is_Some (I !! κ) → κ ∉ K → κ ∈ K') →
   Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
-    ={↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
+    ={↑lft_userN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
 Proof.
   intros Iinv. revert K'.
   induction (set_wf K) as [K _ IH]=> K' HKK' HK HK'.
@@ -108,7 +110,7 @@ Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
 
 Lemma lft_create E :
   ↑lftN ⊆ E →
-  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,∅}▷=∗ [†κ]).
+  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,↑lft_userN}▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -126,7 +128,7 @@ Proof.
   iModIntro; iExists {[ Λ ]}.
   rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
   clear I A HΛ. iIntros "!# HΛ".
-  iApply (step_fupd_mask_mono (↑lftN) _ _ (↑lftN∖↑mgmtN));  [set_solver..|].
+  iApply (step_fupd_mask_mono (↑lftN) _ _ (↑lftN∖↑mgmtN)); [solve_ndisj..|].
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
@@ -148,7 +150,7 @@ Proof.
   iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK".
   { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
     iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
-  iApply fupd_trans. iApply (fupd_mask_mono (↑borN ∪ ↑inhN));
+  iApply fupd_trans. iApply (fupd_mask_mono (↑lft_userN ∪ ↑inhN));
                        first by apply union_least; solve_ndisj.
   iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
   { done. }
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 35d886ee..44a336f5 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -4,9 +4,11 @@ From lrust.lifetime Require Export lifetime_sig.
 Set Default Proof Using "Type".
 Import uPred.
 
-Definition borN : namespace := lftN .@ "bor".
 Definition inhN : namespace := lftN .@ "inh".
 Definition mgmtN : namespace := lftN .@ "mgmt".
+(** We put borrows into the "user" namespace, so that they are available
+in [lft_vs]. *)
+Definition borN : namespace := lft_userN .@ "bor".
 
 Definition atomic_lft := positive.
 (* HACK : We need to make sure this is not in the top-level context,
@@ -140,7 +142,7 @@ Section defs.
        own_cnt κ (● n) ∗
        ∀ I : gmap lft lft_names,
          lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ
-           ={↑borN}=∗
+           ={↑lft_userN}=∗
          lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
 
   Definition lft_inv_alive_go (κ : lft)
@@ -268,7 +270,7 @@ Lemma lft_vs_unfold κ Pb Pi :
   lft_vs κ Pb Pi ⊣⊢ ∃ n : nat,
     own_cnt κ (● n) ∗
     ∀ I : gmap lft lft_names,
-      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑borN}=∗
+      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑lft_userN}=∗
       lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
 Proof. done. Qed.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 6951aeaf..b4f16f1c 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -490,7 +490,7 @@ Proof.
 Qed.
 
 Lemma lft_vs_cons κ Pb Pb' Pi :
-  (▷ Pb'-∗ [†κ] ={↑borN}=∗ ▷ Pb) -∗
+  (▷ Pb'-∗ [†κ] ={↑lft_userN}=∗ ▷ Pb) -∗
   lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi.
 Proof.
   iIntros "Hcons Hvs". rewrite !lft_vs_unfold.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index d0b9063f..033c00f6 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -41,7 +41,7 @@ Section lft_contexts.
   (* Local lifetime contexts. *)
   Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
     let κ' := lft_intersect_list (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,∅}▷=∗ [†κ0]))%I.
+    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,↑lft_userN}▷=∗ [†κ0]))%I.
   Global Instance llctx_elt_interp_fractional x :
     Fractional (llctx_elt_interp x).
   Proof.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index a252a860..7a0f07c2 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -27,7 +27,7 @@ Section arc.
      (*    because [weak_new] cannot prove ty_shr, even for a dead *)
      (*    lifetime. *)
      (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-     □ (1.[ν] ={↑lftN ∪ ↑arc_endN,∅}▷=∗
+     □ (1.[ν] ={↑lftN ∪ ↑arc_endN,↑lft_userN}▷=∗
           [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
 
   Global Instance arc_persist_ne tid ν γ l n :
@@ -767,7 +767,9 @@ Section arc.
       rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
       iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
       iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); try solve_ndisj.
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
+      { (* FIXME [solve_ndisj] fails *)
+        etrans; last exact: union_subseteq_l. solve_ndisj. }
       iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
       wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
@@ -870,7 +872,9 @@ Section arc.
       rewrite heap_mapsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
       iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
       iSpecialize ("H†" with "Hν").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); try solve_ndisj.
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
+      { (* FIXME [solve_ndisj] fails *)
+        etrans; last exact: union_subseteq_l. solve_ndisj. }
       wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
       rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
       iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
@@ -944,7 +948,9 @@ Section arc.
     iDestruct "Hrc" as (γ ν q') "[#(Hi & Hs & #Hc) Htoks]".
     wp_apply (is_unique_spec with "Hi Htoks"). iIntros ([]) "H"; wp_if.
     - iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); try solve_ndisj.
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
+      { (* FIXME [solve_ndisj] fails *)
+        etrans; last exact: union_subseteq_l. solve_ndisj. }
       wp_seq. iIntros "(#Hν & Hown & H†) !>". wp_seq.
       iMod ("Hclose2" with "[Hrc Hrc1 H†] Hown") as "[Hb Hα]".
       { iIntros "!> Hown !>". iLeft. iFrame. }
@@ -1029,7 +1035,9 @@ Section arc.
     pose proof (fin_to_nat_lt x). destruct (fin_to_nat x) as [|[|[]]]; last lia.
     - iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ +â‚— _)%E.
       iSpecialize ("Hc" with "HP1").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
+      { (* FIXME [solve_ndisj] fails *)
+        etrans; last exact: union_subseteq_l. solve_ndisj. }
       wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
       iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
       { iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -1044,7 +1052,9 @@ Section arc.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
     - iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _). 
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
+      { (* FIXME [solve_ndisj] fails *)
+        etrans; last exact: union_subseteq_l. solve_ndisj. }
       wp_apply wp_new=>//. lia. iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>".
       rewrite -!lock Nat2Z.id.
       wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 03e65d8a..d2428f7b 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -85,7 +85,7 @@ Section rc.
                  because [weak_new] cannot prove ty_shr, even for a dead
                  lifetime. *)
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-              □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I.
+              □ (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]))%I.
 
   Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
   Proof. unfold rc_persist, tc_opaque. apply _. Qed.
@@ -247,16 +247,16 @@ Section code.
         (((⌜strong = 1%positive⌝ ∗
            (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
              ((⌜weak = 1⌝ ∗
-               |={⊤,∅}▷=> † l…(2 + ty.(ty_size)) ∗
+               |={⊤,↑lft_userN}▷=> † l…(2 + ty.(ty_size)) ∗
                           ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨
              (⌜weak > 1⌝ ∗
               ((l ↦ #1 -∗ (l +ₗ 1) ↦ #weak
                 ={⊤}=∗ na_own tid F ∗ ty_own (rc ty) tid [ #l ]) ∧
                (l ↦ #0 -∗ (l +ₗ 1) ↦ #(weak - 1)
-                ={⊤,∅}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
+                ={⊤,↑lft_userN}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
                 ((l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
                  ={⊤}=∗ na_own tid F)))))) ∧
-           (l ↦ #0 ={⊤,∅}▷=∗
+           (l ↦ #0 ={⊤,↑lft_userN}▷=∗
              ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗
              (na_own tid F ={⊤}=∗ ∃ weak : Z,
                 (l +ₗ 1) ↦ #weak ∗
@@ -295,7 +295,7 @@ Section code.
              iMod (own_update_2 with "Hst Htok") as "Hst".
              { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
                apply cancel_local_update_unit, _. }
-             rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans.
+             rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans.
              iApply step_fupd_mask_mono;
                last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
              iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
@@ -307,7 +307,7 @@ Section code.
                 iMod ("Hclose" with "[-Htok Hν1]") as "$"; last by auto 10 with iFrame.
                 iFrame. iExists _. auto with iFrame.
              ++ iIntros "Hl1 Hl2".
-                rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans.
+                rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans.
                 iApply step_fupd_mask_mono;
                   last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
                 iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
@@ -325,7 +325,7 @@ Section code.
           { apply auth_update. etrans.
             - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_unit, _.
             - apply (op_local_update _ _ (Some (Cinr (Excl tt)), 0%nat)). auto. }
-          rewrite -[(|={∅,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
+          rewrite -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
           iApply step_fupd_mask_mono;
             last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
           iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 14f5aa39..87fae82d 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -15,7 +15,7 @@ Section ref_functions.
     own γ (◯ reading_stR q ν) -∗
     ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
             own γ (● (refcell_st_to_R $ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν) ∗
-            ((1).[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
+            ((1).[ν] ={↑lftN,↑lft_userN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
             ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1).
   Proof.
@@ -162,7 +162,7 @@ Section ref_functions.
       as (q' n) "(H↦lrc & >% & H●◯ & H† & Hq' & Hshr)".
     iDestruct "Hq'" as (q'') ">[% Hν']".
     wp_read. wp_let. wp_op. wp_write.
-    iAssert (|={↑lftN,∅}▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN,↑lft_userN}▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
     { iDestruct (own_valid with "H●◯") as
           %[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
@@ -180,10 +180,10 @@ Section ref_functions.
         { apply auth_update_dealloc.
           rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
           apply (cancel_local_update_unit (reading_stR q ν)), _. }
-        iApply step_fupd_intro; first set_solver. iExists (q+q'')%Qp. iFrame.
+        iApply step_fupd_intro; first solve_ndisj. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
     wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
-    iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
+    iApply (wp_step_fupd with "INV"); [solve_ndisj..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)] with "[] LFT HE Hna HL Hk");
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 0eb37efc..ac94210f 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -49,7 +49,7 @@ Section refcell_inv.
         (* Not borrowed. *)
         &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
       | Some (ν, rw, q, _) =>
-        (1.[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+        (1.[ν] ={↑lftN,↑lft_userN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
         (∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]) ∗
         if rw then (* Mutably borrowed. *) True
         else       (* Immutably borrowed. *) ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1)
@@ -155,7 +155,7 @@ Section refcell.
     - iMod (own_alloc (● (refcell_st_to_R $ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
       iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
-      { rewrite -step_fupd_intro. auto. set_solver+. }
+      { rewrite -step_fupd_intro. auto. solve_ndisj. }
       iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
       iApply lft_tok_static.
   Qed.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index c9b45260..f40cfa8a 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -127,7 +127,7 @@ Section refmut_functions.
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
     iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_read. wp_let. wp_op. wp_write.
-    iAssert (|={↑lftN,∅}▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN,↑lft_userN}▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H● H◯ Hν INV]" as "INV".
     { iDestruct (own_valid_2 with "H● H◯") as
         %[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
@@ -148,11 +148,11 @@ Section refmut_functions.
         iDestruct "INV" as "(H† & Hq & _)".
         rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
           last (rewrite pos_op_plus; lia). iFrame.
-        iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
+        iApply step_fupd_intro; [solve_ndisj|]. iSplitL; [|done].
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
     wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
-    iApply (wp_step_fupd with "INV"); [set_solver|]. wp_seq. iIntros "{Hb} Hb !>".
+    iApply (wp_step_fupd with "INV"); [solve_ndisj|]. wp_seq. iIntros "{Hb} Hb !>".
     iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 45a3c81c..027bc151 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -39,7 +39,7 @@ Section rwlock_inv.
       | Some (Cinr (agν, q, n)) =>
         (* Locked for read. *)
         ∃ (ν : lft) q', agν ≡ to_agree ν ∗
-                □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
+                □ (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]) ∗
                 ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
                 ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
                 ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index a53ac9e4..932987cc 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -183,7 +183,7 @@ Section rwlock_functions.
         iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
                          ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
                          own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
-                         ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
+                         ((1).[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]))%I
           with "[> Hlx Hownst Hst Hβtok2]"
           as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
         { destruct st' as [[|[[agν q] n]|]|]; try done.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e8878646..0967717b 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
            ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
              α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
              q.[ν] ∗ own γ (◯ reading_st q ν) ∗
-             (1.[ν] ={↑lftN,∅}▷=∗ [†ν])
+             (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν])
          | _ => False
          end;
        ty_shr κ tid l :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index b1a160c9..2eb1f1c2 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -95,8 +95,9 @@ Section rwlockreadguard_functions.
           rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
           iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
           iApply (step_fupd_mask_mono (↑lftN ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN)));
-            last iApply (step_fupd_mask_frame_r _ ∅); [try set_solver..|];
-            [apply union_least; solve_ndisj|].
+            last iApply (step_fupd_mask_frame_r _ (↑lft_userN)); [set_solver+ || solve_ndisj..| |].
+          { (* FIXME [solve_ndisj] fails. *)
+            apply: disjoint_difference_r1. solve_ndisj. }
           iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
           iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 7892eb97..371164d3 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -182,7 +182,7 @@ Section typing_rules.
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_mask_mono _ (↑lftN)); first done.
-    iApply (wp_step_fupd with "Hend"); first set_solver. wp_seq.
+    iApply (wp_step_fupd with "Hend"); first solve_ndisj. wp_seq.
     iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
-- 
GitLab