From 96e99db913a6c2caec26788de9afd5f2b6dd4f41 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 30 Sep 2020 09:13:56 +0200
Subject: [PATCH] update Iris; adjust for auth change

---
 opam                                             |  2 +-
 theories/lang/heap.v                             |  6 +++---
 theories/lang/lib/arc.v                          | 16 ++++++++--------
 theories/lifetime/model/accessors.v              | 14 +++++++-------
 theories/lifetime/model/borrow_sep.v             |  6 +++---
 theories/lifetime/model/creation.v               |  4 ++--
 theories/lifetime/model/faking.v                 |  4 ++--
 theories/lifetime/model/primitive.v              |  6 +++---
 theories/lifetime/model/reborrow.v               |  6 +++---
 theories/typing/lib/rc/rc.v                      | 14 +++++++-------
 theories/typing/lib/rc/weak.v                    | 10 +++++-----
 theories/typing/lib/refcell/ref_code.v           |  4 ++--
 theories/typing/lib/refcell/refmut_code.v        |  4 ++--
 .../typing/lib/rwlock/rwlockreadguard_code.v     |  2 +-
 .../typing/lib/rwlock/rwlockwriteguard_code.v    |  2 +-
 15 files changed, 50 insertions(+), 50 deletions(-)

diff --git a/opam b/opam
index 56908a20..d573b899 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-09-15.1.5a2a5bec") | (= "dev") }
+  "coq-iris" { (= "dev.2020-09-29.7.19ba2bc0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index a53280d1..9ad9af67 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -406,7 +406,7 @@ Section heap.
   Proof.
     iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
     iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
-    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid.
+    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid_discrete.
     move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
     apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
     { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
@@ -429,7 +429,7 @@ Section heap.
         σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
     iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
@@ -446,7 +446,7 @@ Section heap.
     ⌜σ !! l = Some (ls, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
     iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 67b08374..99d783ff 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -189,7 +189,7 @@ Section arc.
     iIntros "Hl1 Hl2 [HP1 HP1']".
     iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
                       â—¯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
-      as (γ) "[H● H◯]"; first by apply auth_both_valid.
+      as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
     iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
     rewrite Qp_div_2. auto.
   Qed.
@@ -199,7 +199,7 @@ Section arc.
   Proof.
     iIntros "Hl1 Hl2 HP2".
     iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]";
-      first by apply auth_both_valid.
+      first by apply auth_both_valid_discrete.
     iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
   Qed.
 
@@ -210,7 +210,7 @@ Section arc.
                              else ∃ q'', q' = (q + q'')%Qp⌝.
   Proof.
     iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
-        %[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid.
+        %[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
     destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
       simpl in *; subst.
     - setoid_subst. iExists _, _, _, _. by iSplit.
@@ -337,7 +337,7 @@ Section arc.
   Proof.
     iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
         %[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
-         %auth_both_valid.
+         %auth_both_valid_discrete.
     destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
   Qed.
 
@@ -492,7 +492,7 @@ Section arc.
   Proof.
     iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose".
     iDestruct (own_valid_2 with "H● H◯")
-      as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
+      as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
     simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
         try done; try apply _. setoid_subst.
     iMod (own_update_2 with "H● H◯") as "[H● $]".
@@ -589,7 +589,7 @@ Section arc.
       iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
       iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
       iDestruct (own_valid_2 with "H● H◯") as
-        %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
+        %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
       simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
       + apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
         destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
@@ -599,7 +599,7 @@ Section arc.
         iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
         iInv N as ([st w]) "[>H● H]" "Hclose".
         iDestruct (own_valid_2 with "H● H◯") as
-           %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid.
+           %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
         simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
         assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
         { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
@@ -651,7 +651,7 @@ Section arc.
       clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
       iInv N as ([st w']) "[>H● H]" "Hclose".
       iDestruct (own_valid_2 with "H● H◯")
-        as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
+        as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
       simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
         [|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
       wp_read. destruct w'.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 980fa111..f23850bc 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -19,7 +19,7 @@ Proof.
   iIntros (?) "Hslice Halive Hbor Htok". unfold lft_bor_alive, idx_bor_own.
   iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
   iDestruct (own_bor_valid_2 with "Hown Hbor")
-    as %[EQB%to_borUR_included _]%auth_both_valid.
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (slice_empty _ _ true with "Hslice Hbox") as "[$ Hbox]".
     solve_ndisj. by rewrite lookup_fmap EQB.
   rewrite -(fmap_insert bor_filled _ _ (Bor_open q)).
@@ -41,7 +41,7 @@ Proof.
   iIntros (?) "Hslice Halive Hbor HP". unfold lft_bor_alive, idx_bor_own.
   iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
   iDestruct (own_bor_valid_2 with "Hown Hbor")
-    as %[EQB%to_borUR_included _]%auth_both_valid.
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (slice_fill _ _ true with "Hslice HP Hbox") as "Hbox".
     solve_ndisj. by rewrite lookup_fmap EQB.
   rewrite -(fmap_insert bor_filled _ _ Bor_in).
@@ -100,7 +100,7 @@ Proof.
       iLeft. iFrame "%". iExists _, _. iFrame.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hf")
-        as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
+        as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
@@ -124,7 +124,7 @@ Proof.
     unfold lft_bor_alive.
     iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor")
-      as %[EQB%to_borUR_included _]%auth_both_valid.
+      as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
     iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
       solve_ndisj. by rewrite lookup_fmap EQB.
     iDestruct ("HPP'" with "HP'") as "$".
@@ -176,7 +176,7 @@ Proof.
       iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
       iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
       iDestruct (own_bor_valid_2 with "Hown Hbor")
-        as %[EQB%to_borUR_included _]%auth_both_valid.
+        as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
       iMod (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
         solve_ndisj. by rewrite lookup_fmap EQB.
       iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
@@ -204,7 +204,7 @@ Proof.
       iExists Q. rewrite -bi.iff_refl. eauto.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
-        as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
+        as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
@@ -231,7 +231,7 @@ Proof.
     unfold lft_bor_alive, idx_bor_own.
     iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor")
-      as %[EQB%to_borUR_included _]%auth_both_valid.
+      as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
     iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
       solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
     iMod fupd_intro_mask' as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index a54b3c8e..3a4348e8 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -25,7 +25,7 @@ Proof.
     iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
     iDestruct "H" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor")
-        as %[EQB%to_borUR_included _]%auth_both_valid.
+        as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
     iMod (slice_iff _ _ true with "HPP' Hslice Hbox")
       as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
     { by rewrite lookup_fmap EQB. }
@@ -93,9 +93,9 @@ Proof.
     iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
     iDestruct "H" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor1")
-        as %[EQB1%to_borUR_included _]%auth_both_valid.
+        as %[EQB1%to_borUR_included _]%auth_both_valid_discrete.
     iDestruct (own_bor_valid_2 with "Hown Hbor2")
-        as %[EQB2%to_borUR_included _]%auth_both_valid.
+        as %[EQB2%to_borUR_included _]%auth_both_valid_discrete.
     iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
     { iIntros (->). iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2.
       exfalso; revert Hj1j2.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index f74160d1..b8cc1b5c 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -32,7 +32,7 @@ Proof.
     iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; first by eauto.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
-      as %[?%nat_included _]%auth_both_valid; lia. }
+      as %[?%nat_included _]%auth_both_valid_discrete; lia. }
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//.
   { (* FIXME [solve_ndisj] fails *) set_solver-. }
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
@@ -138,7 +138,7 @@ Proof.
     assert (↑mgmtN ⊆ ↑lftN) by solve_ndisj. set_solver. }
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
-    as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid.
+    as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid_discrete.
   iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
   { by eapply auth_update, singleton_local_update,
       (exclusive_local_update _ (Cinr ())). }
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index ae9c563a..5636fc4e 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -16,10 +16,10 @@ Proof.
   iIntros "HA HI Hinv".
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
   { iModIntro. iExists A, I. by iFrame. }
-  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid.
+  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid_discrete.
   iMod (own_alloc (● (∅ : gmap slice_name
     (frac * agree bor_stateO)) ⋅ ◯ ∅)) as (γbor) "[Hbor Hbor']".
-  { by apply auth_both_valid. }
+  { by apply auth_both_valid_discrete. }
   iMod (own_alloc (● (ε : gset_disj slice_name)))
      as (γinh) "Hinh"; first by apply auth_auth_valid.
   set (γs := LftNames γbor γcnt γinh).
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 8a0d62ae..0f5673c4 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -37,7 +37,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
     own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
-    as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid.
+    as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
   unfold to_ilftUR in *. simplify_map_eq.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
@@ -47,7 +47,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
     own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
 Proof.
   iIntros "HA HΛ".
-  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid.
+  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid_discrete.
   iPureIntro. move: HA=> /singleton_included_l [qs [/leibniz_equiv_iff]].
   rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
   move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
@@ -457,7 +457,7 @@ Proof.
   { iIntros (I) "HI". iApply (own_inh_auth with "HI HEâ—¯'"). }
   iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
   iDestruct (own_inh_valid_2 with "HE HEâ—¯")
-    as %[Hle%gset_disj_included _]%auth_both_valid.
+    as %[Hle%gset_disj_included _]%auth_both_valid_discrete.
   iMod (own_inh_update_2 with "HE HEâ—¯") as "HE".
   { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
   iMod (slice_delete_full _ _ true with "Hslice Hbox")
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index b3e9f4fd..8d85d84c 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -34,7 +34,7 @@ Proof.
     iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
   rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
   iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_both_valid.
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
@@ -75,7 +75,7 @@ Proof.
   iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
   rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
   iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_both_valid.
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
   { eapply auth_update, singleton_local_update,
      (exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
@@ -119,7 +119,7 @@ Proof.
   iDestruct "Hinvκ" as (Pb Pi) "(Halive & Hvs & Hinh)".
   iDestruct "Halive" as (B) "(Hbox & >H● & HB)".
   iDestruct (own_bor_valid_2 with "H● Hbor")
-    as %[EQB%to_borUR_included _]%auth_both_valid.
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
     solve_ndisj. by rewrite lookup_fmap EQB.
   iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e017caaf..ee8022b1 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -159,7 +159,7 @@ Section rc.
         iMod (bor_create with "LFT Hown") as "[HP HPend]"; first solve_ndisj.
         iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
                          ◯ (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat))) as (γ) "[Ha Hf]".
-        { by apply auth_both_valid. }
+        { by apply auth_both_valid_discrete. }
         iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty)
               with "[Ha Hν2 Hl'1 Hl'2 H† HPend]") as "#?".
         { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame. iExists _.
@@ -282,7 +282,7 @@ Section code.
       iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
       iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
-        %option_included _]%prod_included [Hval _]]%auth_both_valid.
+        %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
       simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl].
       + destruct st' as [[]| |]; try by inversion Hincl. apply (inj Cinl) in Hincl.
         apply (inj2 pair) in Hincl. destruct Hincl as [<-%leibniz_equiv <-%leibniz_equiv].
@@ -346,7 +346,7 @@ Section code.
           iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
           iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
           iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
-            %option_included _]%prod_included [Hval _]]%auth_both_valid.
+            %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
           simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl]; first last.
           { apply csum_included in Hincl. destruct Hincl as
              [->|[(?&?&[=]&?)|(?&?&[=<-]&->&?%exclusive_included)]]; try done. apply _. }
@@ -417,7 +417,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -476,7 +476,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -581,7 +581,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -1076,7 +1076,7 @@ Section code.
       { iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]"; last done.
         iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
                          rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]";
-          first by apply auth_both_valid.
+          first by apply auth_both_valid_discrete.
         iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"=>//.
         iApply (fupd_mask_mono (↑lftN))=>//. iExists γ, ν, (1/2)%Qp. iFrame.
         iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 6c3e1e05..5d61d108 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -158,7 +158,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hwtok") as
-      %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
+      %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
     destruct st as [[[q'' strong]| |]|]; try done.
     - (* Success case. *)
       iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >Hq''q0 & [Hν1 Hν2] & Hν†)".
@@ -261,7 +261,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -327,7 +327,7 @@ Section code.
       iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
       iDestruct (own_valid_2 with "Hrc● Hwtok") as
-        %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
+        %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
       iMod (own_update with "Hrc●") as "[Hrc● $]".
       { by apply auth_update_alloc, prod_local_update_2,
            (op_local_update_discrete _ _ 1%nat). }
@@ -400,7 +400,7 @@ Section code.
       iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
       iDestruct (own_valid_2 with "Hrc● Hwtok") as
-          %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
+          %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
       destruct weakc; first by simpl in *; lia.
       iMod (own_update_2 with "Hrc● Hwtok") as "Hrc●".
       { apply auth_update_dealloc, prod_local_update_2,
@@ -473,7 +473,7 @@ Section code.
     { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
       iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
       iMod (own_alloc (● _ ⋅ ◯ _)) as (γ) "[??]"; last (iExists _, _; iFrame).
-      { apply auth_both_valid. by split. }
+      { apply auth_both_valid_discrete. by split. }
       iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
       iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
       iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 172ae8ee..9a2bb702 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -26,7 +26,7 @@ Section ref_functions.
     { destruct st as [[[[??]?]?]|];
       iDestruct (own_valid_2 with "H● H◯")
         as %[[[=]|(?&[[? q'] n]&[=<-]&[=]&[[[Eq_ag ?%leibniz_equiv]_]|Hle])]
-               %option_included Hv]%auth_both_valid; simpl in *; subst.
+               %option_included Hv]%auth_both_valid_discrete; simpl in *; subst.
       - apply (inj to_agree), (inj2 pair) in Eq_ag.
         destruct Eq_ag. setoid_subst. eauto.
       - revert Hle=> /prod_included [/= /prod_included
@@ -166,7 +166,7 @@ Section ref_functions.
       with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
     { iDestruct (own_valid with "H●◯") as
           %[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
-              %Some_included _]%auth_both_valid.
+              %Some_included _]%auth_both_valid_discrete.
       - simpl in *. setoid_subst.
         iExists None. iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 46f484d6..69b894f1 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -131,7 +131,7 @@ Section refmut_functions.
       with "[H↦lrc H● H◯ Hν INV]" as "INV".
     { iDestruct (own_valid_2 with "H● H◯") as
         %[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
-         %auth_both_valid.
+         %auth_both_valid_discrete.
       destruct st as [[[[??]?]?]|]; [|done]. move: Hst=>-[= ???]. subst.
       destruct INCL as [[[[ν' ?]%to_agree_inj ?] ?]|
             [[[??]%to_agree_included [q'' Hq'']]%prod_included [n' Hn']]%prod_included].
@@ -300,7 +300,7 @@ Section refmut_functions.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
     wp_seq. wp_op. wp_read.
     iDestruct "INV" as (st) "(Hlrc & H● & Hst)".
-    iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_both_valid.
+    iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_both_valid_discrete.
     destruct st as [[[[??]?]?]|]; last by destruct Hst as [[?|] Hst]; inversion Hst.
     move:Hst=>/Some_pair_included [/Some_pair_included_total_1
               [/to_agree_included /(leibniz_equiv _ _) [= <- <-] _] _].
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index f5f3804c..303ab8dd 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -87,7 +87,7 @@ Section rwlockreadguard_functions.
                (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
         with "[H● H◯ Hx' Hν Hst H†]" as "INV".
       { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
-           %option_included Hv]%auth_both_valid.
+           %option_included Hv]%auth_both_valid_discrete.
         - destruct st0 as [|[[agν q']n]|]; try by inversion Heq. revert Heq. simpl.
           intros [[EQ <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv]
                  %(inj Cinr)%(inj2 pair).
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 45c9edd7..7aa33fb3 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -126,7 +126,7 @@ Section rwlockwriteguard_functions.
     iDestruct "INV" as (st) "(H↦ & H● & INV)". wp_write.
     iMod ("Hcloseβ" with "[> H↦ H● H◯ INV Hx']") as "Hβ".
     { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> &
-         [Heq|Hle])]%option_included Hv]%auth_both_valid;
+         [Heq|Hle])]%option_included Hv]%auth_both_valid_discrete;
       last by destruct (exclusive_included _ _ Hle).
       destruct st0 as [[[]|]| |]; try by inversion Heq.
       iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
-- 
GitLab