iris/base_logic/lib/boxes.v

+From iris.algebra Require Import lib.excl_auth gmap agree.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export invariants.
+From iris.prelude Require Import options.
+Import uPred.
+
+(** The CMRAs we need. *)
+Class boxG Σ :=
+  #[local] boxG_inG :: inG Σ (prodR
+    (excl_authR boolO)
+    (optionR (agreeR (laterO (iPropO Σ))))).
+
+Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
+                                            optionRF (agreeRF (▶ ∙)) ) ].
+
+Global Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
+Proof. solve_inG. Qed.
+
+Section box_defs.
+  Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
+
+  Definition slice_name := gname.
+
+  Definition box_own_auth (γ : slice_name) (a : excl_authR boolO) : iProp Σ :=
+    own γ (a, None).
+
+  Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
+    own γ (ε, Some (to_agree (Next P))).
+
+  Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
+    ∃ b, box_own_auth γ (●E b) ∗ if b then P else True.
+
+  Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
+    box_own_prop γ P ∗ inv N (slice_inv γ P).
+
+  Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
+    tc_opaque (∃ Φ : slice_name → iProp Σ,
+      ▷ (P ≡ [∗ map] γ ↦ _ ∈ f, Φ γ) ∗
+      [∗ map] γ ↦ b ∈ f, box_own_auth γ (◯E b) ∗ box_own_prop γ (Φ γ) ∗
+                         inv N (slice_inv γ (Φ γ)))%I.
+End box_defs.
+
+Global Instance: Params (@box_own_prop) 3 := {}.
+Global Instance: Params (@slice_inv) 3 := {}.
+Global Instance: Params (@slice) 5 := {}.
+Global Instance: Params (@box) 5 := {}.
+
+Section box.
+Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
+Implicit Types P Q : iProp Σ.
+
+Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
+Proof. solve_proper. Qed.
+Global Instance box_own_prop_contractive γ : Contractive (box_own_prop γ).
+Proof. solve_contractive. Qed.
+
+Global Instance box_inv_ne γ : NonExpansive (slice_inv γ).
+Proof. solve_proper. Qed.
+
+Global Instance slice_ne γ : NonExpansive (slice N γ).
+Proof. solve_proper. Qed.
+Global Instance slice_contractive γ : Contractive (slice N γ).
+Proof. solve_contractive. Qed.
+Global Instance slice_proper γ : Proper ((≡) ==> (≡)) (slice N γ).
+Proof. apply ne_proper, _. Qed.
+
+Global Instance slice_persistent γ P : Persistent (slice N γ P).
+Proof. apply _. Qed.
+
+Global Instance box_contractive f : Contractive (box N f).
+Proof. solve_contractive. Qed.
+Global Instance box_ne f : NonExpansive (box N f).
+Proof. apply (contractive_ne _). Qed.
+Global Instance box_proper f : Proper ((≡) ==> (≡)) (box N f).
+Proof. apply ne_proper, _. Qed.
+
+Lemma box_own_auth_agree γ b1 b2 :
+  box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2) ⊢ ⌜b1 = b2⌝.
+Proof.
+  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
+  by iDestruct 1 as %?%excl_auth_agree_L.
+Qed.
+
+Lemma box_own_auth_update γ b1 b2 b3 :
+  box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2)
+  ==∗ box_own_auth γ (●E b3) ∗ box_own_auth γ (◯E b3).
+Proof.
+  rewrite /box_own_auth -!own_op. iApply own_update. apply prod_update; last done.
+  apply excl_auth_update.
+Qed.
+
+Lemma box_own_agree γ Q1 Q2 :
+  box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
+Proof.
+  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
+  by rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
+Qed.
+
+Lemma box_alloc : ⊢ box N ∅ True.
+Proof.
+  iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
+Qed.
+
+Lemma slice_insert_empty E q f Q P :
+  ▷?q box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
+    slice N γ Q ∗ ▷?q box N (<[γ:=false]> f) (Q ∗ P).
+Proof.
+  iDestruct 1 as (Φ) "[#HeqP Hf]".
+  iMod (own_alloc_cofinite (●E false ⋅ ◯E false,
+    Some (to_agree (Next Q))) (dom f))
+    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]).
+  rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
+  iDestruct "Hdom" as % ?%not_elem_of_dom.
+  iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
+  { iNext. iExists false; eauto. }
+  iModIntro; iExists γ; repeat iSplit; auto.
+  iNext. iExists (<[γ:=Q]> Φ); iSplit.
+  - iNext. iRewrite "HeqP". by rewrite big_opM_fn_insert'.
+  - rewrite (big_opM_fn_insert (λ _ _ P',  _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //.
+    iFrame; eauto.
+Qed.
+
+Lemma slice_delete_empty E q f P Q γ :
+  ↑N ⊆ E →
+  f !! γ = Some false →
+  slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ P',
+    ▷?q (▷ (P ≡ (Q ∗ P')) ∗ box N (delete γ f) P').
+Proof.
+  iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
+  iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
+  iInv N as (b) "[>Hγ _]".
+  iDestruct (big_sepM_delete _ f _ false with "Hf")
+    as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
+  iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
+  iModIntro. iSplitL "Hγ"; first iExists false; eauto.
+  iModIntro. iNext. iSplit.
+  - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
+    iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
+  - iExists Φ; eauto.
+Qed.
+
+Lemma slice_fill E q f γ P Q :
+  ↑N ⊆ E →
+  f !! γ = Some false →
+  slice N γ Q -∗ ▷ Q -∗ ▷?q box N f P ={E}=∗ ▷?q box N (<[γ:=true]> f) P.
+Proof.
+  iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
+  iInv N as (b') "[>Hγ _]".
+  iDestruct (big_sepM_delete _ f _ false with "Hf")
+    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
+  iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
+  iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
+  iModIntro; iNext; iExists Φ; iSplit.
+  - by rewrite big_opM_insert_override.
+  - rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
+    iFrame; eauto.
+Qed.
+
+Lemma slice_empty E q f P Q γ :
+  ↑N ⊆ E →
+  f !! γ = Some true →
+  slice N γ Q -∗ ▷?q box N f P ={E}=∗ ▷ Q ∗ ▷?q box N (<[γ:=false]> f) P.
+Proof.
+  iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
+  iInv N as (b) "[>Hγ HQ]".
+  iDestruct (big_sepM_delete _ f with "Hf")
+    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
+  iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
+  iFrame "HQ".
+  iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
+  iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
+  iModIntro; iNext; iExists Φ; iSplit.
+  - by rewrite big_opM_insert_override.
+  - rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
+    iFrame; eauto.
+Qed.
+
+Lemma slice_insert_full E q f P Q :
+  ↑N ⊆ E →
+  ▷ Q -∗ ▷?q box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
+    slice N γ Q ∗ ▷?q box N (<[γ:=true]> f) (Q ∗ P).
+Proof.
+  iIntros (?) "HQ Hbox".
+  iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
+  iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
+  - by apply lookup_insert.
+  - by rewrite insert_insert.
+Qed.
+
+Lemma slice_delete_full E q f P Q γ :
+  ↑N ⊆ E →
+  f !! γ = Some true →
+  slice N γ Q -∗ ▷?q box N f P ={E}=∗
+  ∃ P', ▷ Q ∗ ▷?q ▷ (P ≡ (Q ∗ P')) ∗ ▷?q box N (delete γ f) P'.
+Proof.
+  iIntros (??) "#Hslice Hbox".
+  iMod (slice_empty with "Hslice Hbox") as "[$ Hbox]"; try done.
+  iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; first done.
+  { by apply lookup_insert. }
+  iExists P'. iFrame. rewrite -insert_delete_insert delete_insert ?lookup_delete //.
+Qed.
+
+Lemma box_fill E f P :
+  ↑N ⊆ E →
+  box N f P -∗ ▷ P ={E}=∗ box N (const true <$> f) P.
+Proof.
+  iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
+  iExists Φ; iSplitR; first by rewrite big_opM_fmap.
+  iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
+  iDestruct ("HeqP" with "HP") as "HP".
+  iCombine "Hf" "HP" as "Hf".
+  rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
+  iApply (@big_sepM_impl with "Hf").
+  iIntros "!>" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
+  iInv N as (b) "[>Hγ _]".
+  iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
+  iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
+Qed.
+
+Lemma box_empty E f P :
+  ↑N ⊆ E →
+  map_Forall (λ _, (true =.)) f →
+  box N f P ={E}=∗ ▷ P ∗ box N (const false <$> f) P.
+Proof.
+  iDestruct 1 as (Φ) "[#HeqP Hf]".
+  iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ) ∗
+    [∗ map] γ↦b ∈ f, box_own_auth γ (◯E false) ∗  box_own_prop γ (Φ γ) ∗
+      inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
+  { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
+    iIntros "!>" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
+    assert (true = b) as <- by eauto.
+    iInv N as (b) "[>Hγ HΦ]".
+    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
+    iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
+    iModIntro. iSplitL "Hγ"; first (iNext; iExists false; iFrame; eauto).
+    iFrame "HγΦ Hinv". by iApply "HΦ". }
+  iModIntro; iSplitL "HΦ".
+  - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
+  - iExists Φ; iSplit; by rewrite big_opM_fmap.
+Qed.
+
+Lemma slice_iff E q f P Q Q' γ b :
+  ↑N ⊆ E → f !! γ = Some b →
+  ▷ □ (Q ↔ Q') -∗ slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ γ' P',
+    ⌜delete γ f !! γ' = None⌝ ∗ ▷?q ▷ □ (P ↔ P') ∗
+    slice N γ' Q' ∗ ▷?q box N (<[γ' := b]>(delete γ f)) P'.
+Proof.
+  iIntros (??) "#HQQ' #Hs Hb". destruct b.
+  - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
+    iDestruct ("HQQ'" with "HQ") as "HQ'".
+    iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
+    iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
+    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
+  - iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
+    iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
+    iExists γ', (Q' ∗ P')%I. iIntros "{$∗ $# $%} !>".  do 2 iNext. iRewrite "Heq".
+    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
+Qed.
+
+Lemma slice_split E q f P Q1 Q2 γ b :
+  ↑N ⊆ E → f !! γ = Some b →
+  slice N γ (Q1 ∗ Q2) -∗ ▷?q box N f P ={E}=∗ ∃ γ1 γ2,
+    ⌜delete γ f !! γ1 = None⌝ ∗ ⌜delete γ f !! γ2 = None⌝ ∗ ⌜γ1 ≠ γ2⌝ ∗
+    slice N γ1 Q1 ∗ slice N γ2 Q2 ∗ ▷?q box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P.
+Proof.
+  iIntros (??) "#Hslice Hbox". destruct b.
+  - iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
+    iMod (slice_insert_full with "HQ1 Hbox") as (γ1 ?) "[#Hslice1 Hbox]"; first done.
+    iMod (slice_insert_full with "HQ2 Hbox") as (γ2 ?) "[#Hslice2 Hbox]"; first done.
+    iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
+    { by eapply lookup_insert_None. }
+    { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
+    iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
+    iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
+  - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
+    iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
+    iMod (slice_insert_empty with "Hbox") as (γ2 ?) "[#Hslice2 Hbox]".
+    iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
+    { by eapply lookup_insert_None. }
+    { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
+    iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
+    iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
+Qed.
+
+Lemma slice_combine E q f P Q1 Q2 γ1 γ2 b :
+  ↑N ⊆ E → γ1 ≠ γ2 → f !! γ1 = Some b → f !! γ2 = Some b →
+  slice N γ1 Q1 -∗ slice N γ2 Q2 -∗ ▷?q box N f P ={E}=∗ ∃ γ,
+    ⌜delete γ2 (delete γ1 f) !! γ = None⌝ ∗ slice N γ (Q1 ∗ Q2) ∗
+    ▷?q box N (<[γ := b]>(delete γ2 (delete γ1 f))) P.
+Proof.
+  iIntros (????) "#Hslice1 #Hslice2 Hbox". destruct b.
+  - iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done.
+    iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
+    { by simplify_map_eq. }
+    iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2) with "[$HQ1 $HQ2] Hbox")
+      as (γ ?) "[#Hslice Hbox]"; first done.
+    iExists γ. iIntros "{$% $#} !>". iNext.
+    iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
+    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
+  - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
+    iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
+    { by simplify_map_eq. }
+    iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
+    iExists γ. iIntros "{$% $#} !>". iNext.
+    iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
+    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
+Qed.
+End box.
+
+Global Typeclasses Opaque slice box.

iris/base_logic/lib/cancelable_invariants.v

+From iris.algebra Require Export frac.
+From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export invariants.
+From iris.prelude Require Import options.
+
+Class cinvG Σ := { #[local] cinv_inG :: inG Σ fracR }.
+
+Definition cinvΣ : gFunctors := #[GFunctor fracR].
+
+Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
+Proof. solve_inG. Qed.
+
+Section defs.
+  Context `{!invGS_gen hlc Σ, !cinvG Σ}.
+
+  Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
+
+  Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ :=
+    inv N (P ∨ cinv_own γ 1).
+End defs.
+
+Global Instance: Params (@cinv) 5 := {}.
+
+Section proofs.
+  Context `{!invGS_gen hlc Σ, !cinvG Σ}.
+
+  Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
+  Proof. rewrite /cinv_own; apply _. Qed.
+
+  Global Instance cinv_contractive N γ : Contractive (cinv N γ).
+  Proof. solve_contractive. Qed.
+  Global Instance cinv_ne N γ : NonExpansive (cinv N γ).
+  Proof. exact: contractive_ne. Qed.
+  Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ).
+  Proof. exact: ne_proper. Qed.
+
+  Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
+  Proof. rewrite /cinv; apply _. Qed.
+
+  Global Instance cinv_own_fractional γ : Fractional (cinv_own γ).
+  Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
+  Global Instance cinv_own_as_fractional γ q :
+    AsFractional (cinv_own γ q) (cinv_own γ) q.
+  Proof. split; [done|]. apply _. Qed.
+
+  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
+  Proof. rewrite -frac_valid -uPred.discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
+
+  Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
+  Qed.
+
+  Lemma cinv_iff N γ P Q : cinv N γ P -∗ ▷ □ (P ↔ Q) -∗ cinv N γ Q.
+  Proof.
+    iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
+    iSplit; iIntros "[?|$]"; iLeft; by iApply "HPQ".
+  Qed.
+
+  (*** Allocation rules. *)
+  (** The "strong" variants permit any infinite [I], and choosing [P] is delayed
+  until after [γ] was chosen.*)
+  Lemma cinv_alloc_strong (I : gname → Prop) E N :
+    pred_infinite I →
+    ⊢ |={E}=> ∃ γ, ⌜ I γ ⌝ ∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P.
+  Proof.
+    iIntros (?). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
+    iExists γ. iIntros "!> {$Hγ $Hfresh}" (P) "HP".
+    iMod (inv_alloc N _ (P ∨ cinv_own γ 1) with "[HP]"); eauto.
+  Qed.
+
+  (** The "open" variants create the invariant in the open state, and delay
+  having to prove [P].
+  These do not imply the other variants because of the extra assumption [↑N ⊆ E]. *)
+  Lemma cinv_alloc_strong_open (I : gname → Prop) E N :
+    pred_infinite I →
+    ↑N ⊆ E →
+    ⊢ |={E}=> ∃ γ, ⌜ I γ ⌝ ∗ cinv_own γ 1 ∗ ∀ P,
+      |={E,E∖↑N}=> cinv N γ P ∗ (▷ P ={E∖↑N,E}=∗ True).
+  Proof.
+    iIntros (??). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
+    iExists γ. iIntros "!> {$Hγ $Hfresh}" (P).
+    iMod (inv_alloc_open N _ (P ∨ cinv_own γ 1)) as "[Hinv Hclose]"; first by eauto.
+    iIntros "!>". iFrame. iIntros "HP". iApply "Hclose". iLeft. done.
+  Qed.
+
+  Lemma cinv_alloc_cofinite (G : gset gname) E N :
+    ⊢ |={E}=> ∃ γ, ⌜ γ ∉ G ⌝ ∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P.
+  Proof.
+    apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
+    exists (fresh (G ∪ E')). apply not_elem_of_union, is_fresh.
+  Qed.
+
+  Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
+  Proof.
+    iIntros "HP". iMod (cinv_alloc_cofinite ∅ E N) as (γ _) "[Hγ Halloc]".
+    iExists γ. iFrame "Hγ". by iApply "Halloc".
+  Qed.
+
+  Lemma cinv_alloc_open E N P :
+    ↑N ⊆ E → ⊢ |={E,E∖↑N}=> ∃ γ, cinv N γ P ∗ cinv_own γ 1 ∗ (▷ P ={E∖↑N,E}=∗ True).
+  Proof.
+    iIntros (?). iMod (cinv_alloc_strong_open (λ _, True)) as (γ) "(_ & Htok & Hmake)"; [|done|].
+    { apply pred_infinite_True. }
+    iMod ("Hmake" $! P) as "[Hinv Hclose]". iIntros "!>". iExists γ. iFrame.
+  Qed.
+
+  (*** Accessors *)
+  Lemma cinv_acc_strong E N γ p P :
+    ↑N ⊆ E →
+    cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗
+    ▷ P ∗ cinv_own γ p ∗ (∀ E' : coPset, ▷ P ∨ cinv_own γ 1 ={E',↑N ∪ E'}=∗ True)).
+  Proof.
+    iIntros (?) "Hinv Hown".
+    iMod (inv_acc_strong with "Hinv") as "[[$ | >Hown'] H]"; first done.
+    - iIntros "{$Hown} !>" (E') "HP". iApply "H". by iNext.
+    - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
+  Qed.
+
+  Lemma cinv_acc E N γ p P :
+    ↑N ⊆ E →
+    cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
+  Proof.
+    iIntros (?) "#Hinv Hγ".
+    iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
+    iIntros "!> HP".
+    iMod ("H" with "[$HP]") as "_".
+    rewrite -union_difference_L //.
+  Qed.
+
+  (*** Other *)
+  Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
+  Proof.
+    iIntros (?) "#Hinv Hγ".
+    iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
+    iMod ("H" with "[$Hγ]") as "_".
+    rewrite -union_difference_L //.
+  Qed.
+
+  Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
+
+  Global Instance into_acc_cinv E N γ P p :
+    IntoAcc (X:=unit) (cinv N γ P)
+            (↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
+            (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
+  Proof.
+    rewrite /IntoAcc /accessor bi.exist_unit -assoc.
+    iIntros (?) "#Hinv Hown". by iApply cinv_acc.
+  Qed.
+End proofs.
+
+Global Typeclasses Opaque cinv_own cinv.

iris/base_logic/lib/fancy_updates.v

+From stdpp Require Export coPset.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import wsat.
+From iris.base_logic Require Export later_credits.
+From iris.prelude Require Import options.
+Export wsatGS.
+Import uPred.
+Import le_upd_if.
+
+(** The definition of fancy updates (and in turn the logic built on top of it) is parameterized
+    by whether it supports elimination of laters via later credits or not.
+    This choice is necessary as the fancy update *with* later credits does *not* support
+    the interaction laws with the plainly modality in [BiFUpdPlainly]. While these laws are
+    seldomly used, support for them is required for backwards compatibility.
+
+    Thus, the [invGS_gen] typeclass ("gen" for "generalized") is parameterized by
+    a parameter of type [has_lc] that determines whether later credits are
+    available or not. [invGS] is provided as a convenient notation for the default [HasLc].
+    We don't use that notation in this file to avoid confusion.
+ *)
+Inductive has_lc := HasLc | HasNoLc.
+
+Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
+  #[local] invGpreS_wsat :: wsatGpreS Σ;
+  #[local] invGpreS_lc :: lcGpreS Σ;
+}.
+
+(* [invGS_lc] needs to be global in order to enable the use of lemmas like
+[lc_split] that require [lcGS], and not [invGS]. [invGS_wsat] also needs to be
+global as the lemmas in [invariants.v] require it. *)
+Class invGS_gen (hlc : has_lc) (Σ : gFunctors) : Set := InvG {
+  #[global] invGS_wsat :: wsatGS Σ;
+  #[global] invGS_lc :: lcGS Σ;
+}.
+Global Hint Mode invGS_gen - - : typeclass_instances.
+Global Hint Mode invGpreS - : typeclass_instances.
+
+Notation invGS := (invGS_gen HasLc).
+
+Definition invΣ : gFunctors :=
+  #[wsatΣ; lcΣ].
+Global Instance subG_invΣ {Σ} : subG invΣ Σ → invGpreS Σ.
+Proof. solve_inG. Qed.
+
+Local Definition uPred_fupd_def `{!invGS_gen hlc Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+  wsat ∗ ownE E1 -∗ le_upd_if (if hlc is HasLc then true else false) (◇ (wsat ∗ ownE E2 ∗ P)).
+Local Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
+Definition uPred_fupd := uPred_fupd_aux.(unseal).
+Global Arguments uPred_fupd {hlc Σ _}.
+Local Lemma uPred_fupd_unseal `{!invGS_gen hlc Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
+
+Lemma uPred_fupd_mixin `{!invGS_gen hlc Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
+Proof.
+  split.
+  - rewrite uPred_fupd_unseal. solve_proper.
+  - intros E1 E2 (E1''&->&?)%subseteq_disjoint_union_L.
+    rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
+    by iIntros "($ & $ & HE) !> !> [$ $] !> !>".
+  - rewrite uPred_fupd_unseal.
+    iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
+  - rewrite uPred_fupd_unseal.
+    iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
+  - rewrite uPred_fupd_unseal. iIntros (E1 E2 E3 P) "HP HwE".
+    iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
+  - intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
+    iIntros "Hvs (Hw & HE1 &HEf)".
+    iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
+    iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
+    iIntros "!> !>". by iApply "HP".
+  - rewrite uPred_fupd_unseal /uPred_fupd_def. by iIntros (????) "[HwP $]".
+Qed.
+Global Instance uPred_bi_fupd `{!invGS_gen hlc Σ} : BiFUpd (uPredI (iResUR Σ)) :=
+  {| bi_fupd_mixin := uPred_fupd_mixin |}.
+
+Global Instance uPred_bi_bupd_fupd `{!invGS_gen hlc Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
+Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>". Qed.
+
+(** The interaction laws with the plainly modality are only supported when
+  we opt out of the support for later credits. *)
+Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS_gen HasNoLc Σ} :
+  BiFUpdPlainly (uPredI (iResUR Σ)).
+Proof.
+  split; rewrite uPred_fupd_unseal /uPred_fupd_def.
+  - iIntros (E E' P Q) "[H HQ] [Hw HE]".
+    iAssert (◇ ■ P)%I as "#>HP".
+    { by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
+    by iFrame.
+  - iIntros (E P) "H [Hw HE]".
+    iAssert (▷ ◇ ■ P)%I as "#HP".
+    { iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
+    iFrame. iIntros "!> !> !>". by iMod "HP".
+  - iIntros (E A Φ) "HΦ [Hw HE]".
+    iAssert (◇ ■ ∀ x : A, Φ x)%I as "#>HP".
+    { iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
+    by iFrame.
+Qed.
+
+(** Later credits: the laws are only available when we opt into later credit support.*)
+
+(** [lc_fupd_elim_later] allows to eliminate a later from a hypothesis at an update.
+  This is typically used as [iMod (lc_fupd_elim_later with "Hcredit HP") as "HP".],
+  where ["Hcredit"] is a credit available in the context and ["HP"] is the
+  assumption from which a later should be stripped. *)
+Lemma lc_fupd_elim_later `{!invGS_gen HasLc Σ} E P :
+   £ 1 -∗ (▷ P) -∗ |={E}=> P.
+Proof.
+  iIntros "Hf Hupd".
+  rewrite uPred_fupd_unseal /uPred_fupd_def.
+  iIntros "[$ $]". iApply (le_upd_later with "Hf").
+  iNext. by iModIntro.
+Qed.
+
+(** If the goal is a fancy update, this lemma can be used to make a later appear
+  in front of it in exchange for a later credit.
+  This is typically used as [iApply (lc_fupd_add_later with "Hcredit")],
+  where ["Hcredit"] is a credit available in the context. *)
+Lemma lc_fupd_add_later `{!invGS_gen HasLc Σ} E1 E2 P :
+  £ 1 -∗ (▷ |={E1, E2}=> P) -∗ |={E1, E2}=> P.
+Proof.
+  iIntros "Hf Hupd". iApply (fupd_trans E1 E1).
+  iApply (lc_fupd_elim_later with "Hf Hupd").
+Qed.
+
+(** Similar to above, but here we are adding [n] laters. *)
+Lemma lc_fupd_add_laterN `{!invGS_gen HasLc Σ} E1 E2 P n :
+  £ n -∗ (▷^n |={E1, E2}=> P) -∗ |={E1, E2}=> P.
+Proof.
+  iIntros "Hf Hupd". iInduction n as [|n] "IH"; first done.
+  iDestruct "Hf" as "[H1 Hf]".
+  iApply (lc_fupd_add_later with "H1"); iNext.
+  iApply ("IH" with "[$] [$]").
+Qed.
+
+(** * [fupd] soundness lemmas *)
+
+(** "Unfolding" soundness stamement for no-LC fupd:
+This exposes that when initializing the [invGS_gen], we can provide
+a general lemma that lets one unfold a [|={E1, E2}=> P] into a basic update
+while also carrying around some frame [ω E] that tracks the current mask.
+We also provide a bunch of later credits for consistency,
+but there is no way to use them since this is a [HasNoLc] lemma. *)
+Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} m E :
+  ⊢ |==> ∃ `(Hws: invGS_gen HasNoLc Σ) (ω : coPset → iProp Σ),
+    £ m ∗ ω E ∗ □ (∀ E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ ◇ (ω E2 ∗ P)).
+Proof.
+  iMod wsat_alloc as (Hw) "[Hw HE]".
+  (* We don't actually want any credits, but we need the [lcGS]. *)
+  iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hlc]".
+  set (Hi := InvG HasNoLc _ Hw Hc).
+  iExists Hi, (λ E, wsat ∗ ownE E)%I.
+  rewrite (union_difference_L E ⊤); [|set_solver].
+  rewrite ownE_op; [|set_solver].
+  iDestruct "HE" as "[HE _]". iFrame.
+  iIntros "!>!>" (E1 E2 P) "HP HwE".
+  rewrite fancy_updates.uPred_fupd_unseal
+          /fancy_updates.uPred_fupd_def -assoc /=.
+  by iApply ("HP" with "HwE").
+Qed.
+
+(** Note: the [_no_lc] soundness lemmas also allow generating later credits, but
+  these cannot be used for anything. They are merely provided to enable making
+  the adequacy proof generic in whether later credits are used. *)
+Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={E1,E2}=∗ P) → ⊢ P.
+Proof.
+  intros Hfupd. apply later_soundness, bupd_soundness; [by apply later_plain|].
+  iMod fupd_soundness_no_lc_unfold as (hws ω) "(Hlc & Hω & #H)".
+  iMod ("H" with "[Hlc] Hω") as "H'".
+  { iMod (Hfupd with "Hlc") as "H'". iModIntro. iApply "H'". }
+  iDestruct "H'" as "[>H1 >H2]". by iFrame.
+Qed.
+
+Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
+  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ n ={E1,E2}=∗ P) → ⊢ P.
+Proof.
+  intros Hfupd. eapply (lc_soundness (S n)); first done.
+  intros Hc. rewrite lc_succ.
+  iIntros "[Hone Hn]". rewrite -le_upd_trans. iApply bupd_le_upd.
+  iMod wsat_alloc as (Hw) "[Hw HE]".
+  set (Hi := InvG HasLc _ Hw Hc).
+  iAssert (|={⊤,E2}=> P)%I with "[Hn]" as "H".
+  { iMod (fupd_mask_subseteq E1) as "_"; first done. by iApply (Hfupd Hi). }
+  rewrite uPred_fupd_unseal /uPred_fupd_def.
+  iModIntro. iMod ("H" with "[$Hw $HE]") as "H".
+  iPoseProof (except_0_into_later with "H") as "H".
+  iApply (le_upd_later with "Hone"). iNext.
+  iDestruct "H" as "(_ & _ & $)".
+Qed.
+
+(** Generic soundness lemma for the fancy update, parameterized by [use_credits]
+  on whether to use credits or not. *)
+Lemma fupd_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
+  (hlc : has_lc) n E1 E2 :
+  (∀ `{Hinv : invGS_gen hlc Σ},
+    £ n ={E1,E2}=∗ P) →
+  ⊢ P.
+Proof.
+  destruct hlc.
+  - apply fupd_soundness_lc. done.
+  - apply fupd_soundness_no_lc. done.
+Qed.
+
+(** [step_fupdN] soundness lemmas *)
+
+Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
+  ⊢ P.
+Proof.
+  intros Hiter.
+  apply (laterN_soundness _  (S n)); simpl.
+  apply (fupd_soundness_no_lc ⊤ ⊤ _ m)=> Hinv. iIntros "Hc".
+  iPoseProof (Hiter Hinv) as "H". clear Hiter.
+  iApply fupd_plainly_mask. iSpecialize ("H" with "Hc").
+  iMod (step_fupdN_plain with "H") as "H". iMod "H". iModIntro.
+  rewrite -later_plainly -laterN_plainly -later_laterN laterN_later.
+  iNext. iMod "H" as "#H". auto.
+Qed.
+
+Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={⊤}[∅]▷=∗^n P) →
+  ⊢ P.
+Proof.
+  intros Hiter. eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
+  iIntros "Hcred". destruct n as [|n].
+  { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
+   simpl in Hiter |- *. iMod (Hiter with "Hcred") as "H". iIntros "!>!>!>".
+  iMod "H". clear. iInduction n as [|n] "IH"; [by iApply fupd_mask_intro_discard|].
+  simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
+Qed.
+
+Lemma step_fupdN_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
+  ⊢ P.
+Proof.
+  intros Hiter.
+  eapply (fupd_soundness_lc (m + n)); [apply _..|].
+  iIntros (Hinv) "Hlc". rewrite lc_split.
+  iDestruct "Hlc" as "[Hm Hn]". iMod (Hiter with "Hm") as "Hupd".
+  clear Hiter.
+  iInduction n as [|n] "IH"; simpl.
+  - by iModIntro.
+  - rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
+    iMod "Hupd". iMod (lc_fupd_elim_later with "Hone Hupd") as "> Hupd".
+    by iApply ("IH" with "Hn Hupd").
+Qed.
+
+Lemma step_fupdN_soundness_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+  (∀ `{Hinv: !invGS_gen hlc Σ}, £ m ={⊤}[∅]▷=∗^n P) →
+  ⊢ P.
+Proof.
+  intros Hiter.
+  eapply (fupd_soundness_lc (m + n) ⊤ ⊤); [apply _..|].
+  iIntros (Hinv) "Hlc". rewrite lc_split.
+  iDestruct "Hlc" as "[Hm Hn]". iPoseProof (Hiter with "Hm") as "Hupd".
+  clear Hiter.
+  (* FIXME can we reuse [step_fupdN_soundness_lc] instead of redoing the induction? *)
+  iInduction n as [|n] "IH"; simpl.
+  - by iModIntro.
+  - rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
+    iMod "Hupd". iMod (lc_fupd_elim_later with "Hone Hupd") as "> Hupd".
+    by iApply ("IH" with "Hn Hupd").
+Qed.
+
+(** Generic soundness lemma for the fancy update, parameterized by [use_credits]
+  on whether to use credits or not. *)
+Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
+  (hlc : has_lc) (n m : nat) :
+  (∀ `{Hinv : invGS_gen hlc Σ},
+    £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
+  ⊢ P.
+Proof.
+  destruct hlc.
+  - apply step_fupdN_soundness_lc. done.
+  - apply step_fupdN_soundness_no_lc. done.
+Qed.

iris/base_logic/lib/fancy_updates_from_vs.v

+(* This file shows that the fancy update can be encoded in terms of the
+view shift, and that the laws of the fancy update can be derived from the
+laws of the view shift. *)
+From stdpp Require Export coPset.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic Require Export base_logic.
+From iris.prelude Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
+Set Default Proof Using "Type*".
+
+Section fupd.
+Context {M} (vs : coPset → coPset → uPred M → uPred M → uPred M).
+
+Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=>  Q") : bi_scope.
+
+Context (vs_ne : ∀ E1 E2, NonExpansive2 (vs E1 E2)).
+Context (vs_persistent : ∀ E1 E2 P Q, Persistent (P ={E1,E2}=> Q)).
+
+Context (vs_impl : ∀ E P Q, □ (P → Q) ⊢ P ={E,E}=> Q).
+Context (vs_transitive : ∀ E1 E2 E3 P Q R,
+  (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R).
+Context (vs_mask_frame_r : ∀ E1 E2 Ef P Q,
+  E1 ## Ef → (P ={E1,E2}=> Q) ⊢ P ={E1 ∪ Ef,E2 ∪ Ef}=> Q).
+Context (vs_frame_r : ∀ E1 E2 P Q R, (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q ∗ R).
+Context (vs_exists : ∀ {A} E1 E2 (Φ : A → uPred M) Q,
+  (∀ x, Φ x ={E1,E2}=> Q) ⊢ (∃ x, Φ x) ={E1,E2}=> Q).
+Context (vs_persistent_intro_r : ∀ E1 E2 P Q R,
+  Persistent R →
+  (R -∗ (P ={E1,E2}=> Q)) ⊢ P ∗ R ={E1,E2}=> Q).
+
+Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
+  ∃ R, R ∗ vs E1 E2 R P.
+
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
+
+Global Instance fupd_ne E1 E2 : NonExpansive (@fupd E1 E2).
+Proof. solve_proper. Qed.
+
+Lemma fupd_intro E P : P ⊢ |={E,E}=> P.
+Proof. iIntros "HP". iExists P. iFrame "HP". iApply vs_impl; auto. Qed.
+
+Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
+Proof.
+  iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
+  iExists R; iFrame "HR". iApply (vs_transitive with "[$Hvs]").
+  iApply vs_impl. iIntros "!> HP". by iApply HPQ.
+Qed.
+
+Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
+Proof.
+  iDestruct 1 as (R) "[HR Hvs]". iExists R. iFrame "HR".
+  iApply (vs_transitive with "[$Hvs]"). clear R.
+  iApply vs_exists; iIntros (R). iApply vs_persistent_intro_r; iIntros "Hvs".
+  iApply (vs_transitive with "[$Hvs]"). iApply vs_impl; auto.
+Qed.
+
+Lemma fupd_mask_frame_r E1 E2 Ef P :
+  E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P.
+Proof.
+  iIntros (HE); iDestruct 1 as (R) "[HR Hvs]". iExists R; iFrame "HR".
+  by iApply vs_mask_frame_r.
+Qed.
+
+Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ⊢ |={E1,E2}=> P ∗ Q.
+Proof.
+  iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
+  iExists (R ∗ Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
+Qed.
+End fupd.

iris/base_logic/lib/gen_heap.v

+From stdpp Require Export namespaces.
+From iris.algebra Require Import reservation_map agree frac.
+From iris.algebra Require Export dfrac.
+From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import ghost_map.
+From iris.prelude Require Import options.
+Import uPred.
+
+(** This file provides a generic mechanism for a language-level point-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_heapGS] typeclass providing the ghost names of that unique
+instance.  That way, [pointsto] does not need an explicit [gname] parameter.
+This mechanism can be plugged into a language and related to the physical heap
+by using [gen_heap_interp σ] in the state interpretation of the weakest
+precondition. See heap-lang for an example.
+
+If you are looking for a library providing "ghost heaps" independent of the
+physical state, you will likely want explicit ghost names to disambiguate
+multiple heaps and are thus better off using [ghost_map], or (if you need more
+flexibility), directly using the underlying [algebra.lib.gmap_view].
+
+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 ↦{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:
+
+- When one allocates a location, in addition to the point-to connective [l ↦ v],
+  one also obtains the token [meta_token l ⊤]. This token is an exclusive
+  resource that denotes that no meta data has been associated with the
+  namespaces in the mask [⊤] for the location [l].
+- Meta data tokens can be split w.r.t. namespace masks, i.e.
+  [meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2] if [E1 ## E2].
+- Meta data can be set using the update [meta_token l E ==∗ meta l N x] provided
+  [↑N ⊆ E], and [x : A] for any countable [A]. The [meta l N x] connective is
+  persistent and denotes the knowledge that the meta data [x] has been
+  associated with namespace [N] to the location [l].
+
+To make the mechanism as flexible as possible, the [x : A] in [meta l N x] can
+be of any countable type [A]. This means that you can associate e.g. single
+ghost names, but also tuples of ghost names, etc.
+
+To further increase flexibility, the [meta l N x] and [meta_token l E]
+connectives are annotated with a namespace [N] and mask [E]. That way, one can
+assign a map of meta information to a location. This is particularly useful when
+building abstractions, then one can gradually assign more ghost information to a
+location instead of having to do all of this at once. We use namespaces so that
+these can be matched up with the invariant namespaces. *)
+
+(** To implement this mechanism, we use three pieces of ghost state:
+
+- A [ghost_map L V], which keeps track of the values of locations.
+- A [ghost_map L gname], which keeps track of the meta information of
+  locations. More specifically, this RA introduces an indirection: it keeps
+  track of a ghost name for each location.
+- The ghost names in the aforementioned authoritative RA refer to namespace maps
+  [reservation_map (agree positive)], which store the actual meta information.
+  This indirection is needed because we cannot perform frame preserving updates
+  in an authoritative fragment without owning the full authoritative element
+  (in other words, without the indirection [meta_set] would need [gen_heap_interp]
+  as a premise).
+ *)
+
+(** The CMRAs we need, and the global ghost names we are using. *)
+
+Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
+  #[local] gen_heapGpreS_meta :: ghost_mapG Σ L gname;
+  #[local] gen_heapGpreS_meta_data :: inG Σ (reservation_mapR (agreeR positiveO));
+}.
+
+Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
+  #[local] gen_heap_inG :: gen_heapGpreS L V Σ;
+  gen_heap_name : gname;
+  gen_meta_name : gname
+}.
+Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
+Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
+Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
+
+Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
+  ghost_mapΣ L V;
+  ghost_mapΣ L gname;
+  GFunctor (reservation_mapR (agreeR positiveO))
+].
+
+Global Instance subG_gen_heapGpreS {Σ L V} `{Countable L} :
+  subG (gen_heapΣ L V) Σ → gen_heapGpreS L V Σ.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context `{Countable L, hG : !gen_heapGS L V Σ}.
+
+  Definition gen_heap_interp (σ : gmap L V) : iProp Σ := ∃ m : gmap L gname,
+    (* The [⊆] is used to avoid assigning ghost information to the locations in
+    the initial heap (see [gen_heap_init]). *)
+    ⌜ dom m ⊆ dom σ ⌝ ∗
+    ghost_map_auth (gen_heap_name hG) 1 σ ∗
+    ghost_map_auth (gen_meta_name hG) 1 m.
+
+  Local Definition pointsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
+    l ↪[gen_heap_name hG]{dq} v.
+  Local Definition pointsto_aux : seal (@pointsto_def). Proof. by eexists. Qed.
+  Definition pointsto := pointsto_aux.(unseal).
+  Local Definition pointsto_unseal : @pointsto = @pointsto_def :=
+    pointsto_aux.(seal_eq).
+
+  Local Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
+    ∃ γm, l ↪[gen_meta_name hG]□ γm ∗ own γm (reservation_map_token E).
+  Local Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
+  Definition meta_token := meta_token_aux.(unseal).
+  Local Definition meta_token_unseal :
+    @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
+
+  (** TODO: The use of [positives_flatten] violates the namespace abstraction
+  (see the proof of [meta_set]. *)
+  Local Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
+    ∃ γm, l ↪[gen_meta_name hG]□ γm ∗
+          own γm (reservation_map_data (positives_flatten N) (to_agree (encode x))).
+  Local Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
+  Definition meta := meta_aux.(unseal).
+  Local Definition meta_unseal : @meta = @meta_def := meta_aux.(seal_eq).
+End definitions.
+Global Arguments meta {L _ _ V Σ _ A _ _} l N x.
+
+Local Notation "l ↦ dq v" := (pointsto l dq v)
+  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
+
+Section gen_heap.
+  Context {L V} `{Countable L, !gen_heapGS L V Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : V → iProp Σ.
+  Implicit Types σ : gmap L V.
+  Implicit Types m : gmap L gname.
+  Implicit Types l : L.
+  Implicit Types v : V.
+
+  (** General properties of pointsto *)
+  Global Instance pointsto_timeless l dq v : Timeless (l ↦{dq} v).
+  Proof. rewrite pointsto_unseal. apply _. Qed.
+  Global Instance pointsto_fractional l v : Fractional (λ q, l ↦{#q} v)%I.
+  Proof. rewrite pointsto_unseal. apply _. Qed.
+  Global Instance pointsto_as_fractional l q v :
+    AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
+  Proof. rewrite pointsto_unseal. apply _. Qed.
+  Global Instance pointsto_persistent l v : Persistent (l ↦□ v).
+  Proof. rewrite pointsto_unseal. apply _. Qed.
+
+  Lemma pointsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_valid. Qed.
+  Lemma pointsto_valid_2 l dq1 dq2 v1 v2 :
+    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_valid_2. Qed.
+  (** Almost all the time, this is all you really need. *)
+  Lemma pointsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_agree. Qed.
+
+  Global Instance pointsto_combine_sep_gives l dq1 dq2 v1 v2 :
+    CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝ | 30.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (pointsto_valid_2 with "H1 H2") as %?. eauto.
+  Qed.
+
+  Lemma pointsto_combine l dq1 dq2 v1 v2 :
+    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_combine. Qed.
+
+  Global Instance pointsto_combine_as l dq1 dq2 v1 v2 :
+    CombineSepAs (l ↦{dq1} v1) (l ↦{dq2} v2) (l ↦{dq1 ⋅ dq2} v1) | 60.
+    (* higher cost than the Fractional instance, which kicks in for #qs *)
+  Proof.
+    rewrite /CombineSepAs. iIntros "[H1 H2]".
+    iDestruct (pointsto_combine with "H1 H2") as "[$ _]".
+  Qed.
+
+  Lemma pointsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
+    ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_frac_ne. Qed.
+  Lemma pointsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_ne. Qed.
+
+  (** Permanently turn any points-to predicate into a persistent
+      points-to predicate. *)
+  Lemma pointsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_persist. Qed.
+
+  (** Recover fractional ownership for read-only element. *)
+  Lemma pointsto_unpersist l v :
+    l ↦□ v ==∗ ∃ q, l ↦{# q} v.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_unpersist. Qed.
+
+  (** Framing support *)
+  Global Instance frame_pointsto p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦{#q1} v) (l ↦{#q2} v) (l ↦{#q} v) | 5.
+  Proof. apply: frame_fractional. Qed.
+
+  (** General properties of [meta] and [meta_token] *)
+  Global Instance meta_token_timeless l N : Timeless (meta_token l N).
+  Proof. rewrite meta_token_unseal. apply _. Qed.
+  Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
+  Proof. rewrite meta_unseal. apply _. Qed.
+  Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
+  Proof. rewrite meta_unseal. apply _. Qed.
+
+  Lemma meta_token_union_1 l E1 E2 :
+    E1 ## E2 → meta_token l (E1 ∪ E2) -∗ meta_token l E1 ∗ meta_token l E2.
+  Proof.
+    rewrite meta_token_unseal /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
+    rewrite reservation_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
+    iSplitL "Hm1"; eauto.
+  Qed.
+  Lemma meta_token_union_2 l E1 E2 :
+    meta_token l E1 -∗ meta_token l E2 -∗ meta_token l (E1 ∪ E2).
+  Proof.
+    rewrite meta_token_unseal /meta_token_def.
+    iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
+    iCombine "Hγm1 Hγm2" gives %[_ ->].
+    iCombine "Hm1 Hm2" gives %?%reservation_map_token_valid_op.
+    iExists γm2. iFrame "Hγm2". rewrite reservation_map_token_union //. by iSplitL "Hm1".
+  Qed.
+  Lemma meta_token_union l E1 E2 :
+    E1 ## E2 → meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2.
+  Proof.
+    intros; iSplit; first by iApply meta_token_union_1.
+    iIntros "[Hm1 Hm2]". by iApply (meta_token_union_2 with "Hm1 Hm2").
+  Qed.
+
+  Lemma meta_token_difference l E1 E2 :
+    E1 ⊆ E2 → meta_token l E2 ⊣⊢ meta_token l E1 ∗ meta_token l (E2 ∖ E1).
+  Proof.
+    intros. rewrite {1}(union_difference_L E1 E2) //.
+    by rewrite meta_token_union; last set_solver.
+  Qed.
+
+  Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
+    meta l i x1 -∗ meta l i x2 -∗ ⌜x1 = x2⌝.
+  Proof.
+    rewrite meta_unseal /meta_def.
+    iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
+    iCombine "Hγm1 Hγm2" gives %[_ ->].
+    iCombine "Hm1 Hm2" gives %Hγ; iPureIntro.
+    move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
+    move=> /to_agree_op_inv_L. naive_solver.
+  Qed.
+  Lemma meta_set `{Countable A} E l (x : A) N :
+    ↑ N ⊆ E → meta_token l E ==∗ meta l N x.
+  Proof.
+    rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
+    iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
+    iApply (own_update with "Hm").
+    apply reservation_map_alloc; last done.
+    cut (positives_flatten N ∈@{coPset} ↑N); first by set_solver.
+    (* TODO: Avoid unsealing here. *)
+    rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
+    exists 1%positive. by rewrite left_id_L.
+  Qed.
+
+  (** Update lemmas *)
+  Lemma gen_heap_alloc σ l v :
+    σ !! l = None →
+    gen_heap_interp σ ==∗ gen_heap_interp (<[l:=v]>σ) ∗ l ↦ v ∗ meta_token l ⊤.
+  Proof.
+    iIntros (Hσl). rewrite /gen_heap_interp pointsto_unseal /pointsto_def
+      meta_token_unseal /meta_token_def /=.
+    iDestruct 1 as (m Hσm) "[Hσ Hm]".
+    iMod (ghost_map_insert l with "Hσ") as "[Hσ Hl]"; first done.
+    iMod (own_alloc (reservation_map_token ⊤)) as (γm) "Hγm".
+    { apply reservation_map_token_valid. }
+    iMod (ghost_map_insert_persist l with "Hm") as "[Hm Hlm]".
+    { move: Hσl. rewrite -!not_elem_of_dom. set_solver. }
+    iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
+    iExists (<[l:=γm]> m). iFrame. iPureIntro.
+    rewrite !dom_insert_L. set_solver.
+  Qed.
+
+  Lemma gen_heap_alloc_big σ σ' :
+    σ' ##ₘ σ →
+    gen_heap_interp σ ==∗
+    gen_heap_interp (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤).
+  Proof.
+    revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
+    { rewrite left_id_L. auto. }
+    iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
+    decompose_map_disjoint.
+    rewrite !big_opM_insert // -insert_union_l //.
+    by iMod (gen_heap_alloc with "Hσ'σ") as "($ & $ & $)";
+      first by apply lookup_union_None.
+  Qed.
+
+  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 pointsto_unseal.
+    by iCombine "Hσ Hl" gives %?.
+  Qed.
+
+  Lemma gen_heap_update σ l v1 v2 :
+    gen_heap_interp σ -∗ l ↦ v1 ==∗ gen_heap_interp (<[l:=v2]>σ) ∗ l ↦ v2.
+  Proof.
+    iDestruct 1 as (m Hσm) "[Hσ Hm]".
+    iIntros "Hl". rewrite /gen_heap_interp pointsto_unseal /pointsto_def.
+    iCombine "Hσ Hl" gives %Hl.
+    iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
+    iModIntro. iFrame "Hl". iExists m. iFrame.
+    iPureIntro. apply elem_of_dom_2 in Hl.
+    rewrite dom_insert_L. set_solver.
+  Qed.
+End gen_heap.
+
+(** This variant of [gen_heap_init] should only be used when absolutely needed.
+The key difference to [gen_heap_init] is that the [inG] instances in the new
+[gen_heapGS] instance are related to the original [gen_heapGpreS] instance,
+whereas [gen_heap_init] forgets about that relation. *)
+Lemma gen_heap_init_names `{Countable L, !gen_heapGpreS L V Σ} σ :
+  ⊢ |==> ∃ γh γm : gname,
+    let hG := GenHeapGS L V Σ γh γm in
+    gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
+Proof.
+  iMod (ghost_map_alloc_empty (K:=L) (V:=V)) as (γh) "Hh".
+  iMod (ghost_map_alloc_empty (K:=L) (V:=gname)) as (γm) "Hm".
+  iExists γh, γm.
+  iAssert (gen_heap_interp (hG:=GenHeapGS _ _ _ γh γm) ∅) with "[Hh Hm]" as "Hinterp".
+  { iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
+  iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
+  { apply map_disjoint_empty_r. }
+  rewrite right_id_L. done.
+Qed.
+
+Lemma gen_heap_init `{Countable L, !gen_heapGpreS L V Σ} σ :
+  ⊢ |==> ∃ _ : gen_heapGS L V Σ,
+    gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
+Proof.
+  iMod (gen_heap_init_names σ) as (γh γm) "Hinit".
+  iExists (GenHeapGS _ _ _ γh γm).
+  done.
+Qed.

iris/base_logic/lib/gen_inv_heap.v

+From iris.algebra Require Import auth excl gmap.
+From iris.base_logic.lib Require Import own invariants gen_heap.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+(** An "invariant" location is a location that has some invariant about its
+value attached to it, and that can never be deallocated explicitly by the
+program.  It provides a persistent witness that will always allow reading the
+location, guaranteeing that the value read will satisfy the invariant.
+
+This is useful for data structures like RDCSS that need to read locations long
+after their ownership has been passed back to the client, but do not care *what*
+it is that they are reading in that case. In that extreme case, the invariant
+may just be [True].
+
+Since invariant locations cannot be deallocated, they only make sense when
+modeling languages with garbage collection.  HeapLang can be used to model
+either language by choosing whether or not to use the [Free] operation.  By
+using a separate assertion [inv_pointsto_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" := (pointsto l (DfracOwn 1) v) (at level 20) : bi_scope.
+
+Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmra := gmapUR L $ prodR
+  (optionR $ exclR $ leibnizO V)
+  (agreeR (V -d> PropO)).
+
+Definition to_inv_heap {L V : Type} `{Countable L}
+    (h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
+  prod_map (λ x, Excl' x) to_agree <$> h.
+
+Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  #[local] inv_heapGpreS_inG :: inG Σ (authR (inv_heap_mapUR L V))
+}.
+
+Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
+  #[local] inv_heap_inG :: inv_heapGpreS L V Σ;
+  inv_heap_name : gname
+}.
+Global Arguments Inv_HeapG _ _ {_ _ _ _}.
+Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
+
+Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
+  #[ GFunctor (authR (inv_heap_mapUR L V)) ].
+
+Global Instance subG_inv_heapGpreS (L V : Type) `{Countable L} {Σ} :
+  subG (inv_heapΣ L V) Σ → inv_heapGpreS L V Σ.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context {L V : Type} `{Countable L}.
+  Context `{!invGS_gen hlc Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
+
+  Definition inv_heap_inv_P : iProp Σ :=
+    ∃ h : gmap L (V * (V -d> PropO)),
+       own (inv_heap_name gG) (● to_inv_heap h) ∗
+       [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1.
+
+  Definition inv_heap_inv : iProp Σ := inv inv_heapN inv_heap_inv_P.
+
+  Definition inv_pointsto_own (l : L) (v : V) (I : V → Prop) : iProp Σ :=
+    own (inv_heap_name gG) (◯ {[l := (Excl' v, to_agree I) ]}).
+
+  Definition inv_pointsto (l : L) (I : V → Prop) : iProp Σ :=
+    own (inv_heap_name gG) (◯ {[l := (None, to_agree I)]}).
+
+End definitions.
+
+Local Notation "l '↦_' I v" := (inv_pointsto_own l v I%stdpp%type)
+  (at level 20, I at level 9, format "l  '↦_' I  v") : bi_scope.
+
+Local Notation "l '↦_' I □" := (inv_pointsto l I%stdpp%type)
+  (at level 20, I at level 9, format "l  '↦_' I  '□'") : bi_scope.
+
+(* [inv_heap_inv] has no parameters to infer the types from, so we need to
+   make them explicit. *)
+Global Arguments inv_heap_inv _ _ {_ _ _ _ _ _ _}.
+
+Global Instance: Params (@inv_pointsto_own) 8 := {}.
+Global Instance: Params (@inv_pointsto) 7 := {}.
+
+Section to_inv_heap.
+  Context {L V : Type} `{Countable L}.
+  Implicit Types (h : gmap L (V * (V -d> PropO))).
+
+  Lemma to_inv_heap_valid h : ✓ to_inv_heap h.
+  Proof. intros l. rewrite lookup_fmap. by case: (h !! l). Qed.
+
+  Lemma to_inv_heap_singleton l v I :
+    to_inv_heap {[l := (v, I)]} =@{inv_heap_mapUR L V} {[l := (Excl' v, to_agree I)]}.
+  Proof. by rewrite /to_inv_heap fmap_insert fmap_empty. Qed.
+
+  Lemma to_inv_heap_insert l v I h :
+    to_inv_heap (<[l := (v, I)]> h) = <[l := (Excl' v, to_agree I)]> (to_inv_heap h).
+  Proof. by rewrite /to_inv_heap fmap_insert. Qed.
+
+  Lemma lookup_to_inv_heap_None h l :
+    h !! l = None → to_inv_heap h !! l = None.
+  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.
+
+  Lemma lookup_to_inv_heap_Some h l v I :
+    h !! l = Some (v, I) → to_inv_heap h !! l = Some (Excl' v, to_agree I).
+  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.
+
+  Lemma lookup_to_inv_heap_Some_2 h l v' I' :
+    to_inv_heap h !! l ≡ Some (v', I') →
+    ∃ v I, v' = Excl' v ∧ I' ≡ to_agree I ∧ h !! l = Some (v, I).
+  Proof.
+    rewrite /to_inv_heap /prod_map lookup_fmap. rewrite fmap_Some_equiv.
+    intros ([] & Hsome & [Heqv HeqI]); simplify_eq/=; eauto.
+  Qed.
+End to_inv_heap.
+
+Lemma inv_heap_init (L V : Type) `{Countable L, !invGS_gen hlc Σ, !gen_heapGS L V Σ, !inv_heapGpreS L V Σ} E :
+  ⊢ |==> ∃ _ : inv_heapGS L V Σ, |={E}=> inv_heap_inv L V.
+Proof.
+  iMod (own_alloc (● (to_inv_heap ∅))) as (γ) "H●".
+  { rewrite auth_auth_valid. exact: to_inv_heap_valid. }
+  iModIntro.
+  iExists (Inv_HeapG L V γ).
+  iAssert (inv_heap_inv_P (gG := Inv_HeapG L V γ)) with "[H●]" as "P".
+  { iExists _. iFrame. done. }
+  iApply (inv_alloc inv_heapN E inv_heap_inv_P with "P").
+Qed.
+
+Section inv_heap.
+  Context {L V : Type} `{Countable L}.
+  Context `{!invGS_gen hlc Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
+  Implicit Types (l : L) (v : V) (I : V → Prop).
+  Implicit Types (h : gmap L (V * (V -d> PropO))).
+
+  (** * Helpers *)
+
+  Lemma inv_pointsto_lookup_Some l h I :
+    l ↦_I □ -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
+    ⌜∃ v I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
+  Proof.
+    iIntros "Hl_inv H◯".
+    iCombine "H◯ Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
+    iPureIntro.
+    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
+    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
+    move: Hincl; rewrite HI Some_included_total pair_included
+      to_agree_included; intros [??]; eauto.
+  Qed.
+
+  Lemma inv_pointsto_own_lookup_Some l v h I :
+    l ↦_I v -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
+    ⌜ ∃ I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
+  Proof.
+    iIntros "Hl_inv H●".
+    iCombine "H● Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
+    iPureIntro.
+    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
+    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
+    move: Hincl; rewrite HI Some_included_total pair_included
+      Excl_included to_agree_included; intros [-> ?]; eauto.
+  Qed.
+
+  (** * Typeclass instances *)
+
+  (* FIXME(Coq #6294): needs new unification
+  The uses of [apply:] and [move: ..; rewrite ..] (by lack of [apply: .. in ..])
+  in this file are needed because Coq's default unification algorithm fails. *)
+  Global Instance inv_pointsto_own_proper l v :
+    Proper (pointwise_relation _ iff ==> (≡)) (inv_pointsto_own l v).
+  Proof.
+    intros I1 I2 ?. rewrite /inv_pointsto_own. do 2 f_equiv.
+    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
+  Qed.
+  Global Instance inv_pointsto_proper l :
+    Proper (pointwise_relation _ iff ==> (≡)) (inv_pointsto l).
+  Proof.
+    intros I1 I2 ?. rewrite /inv_pointsto. do 2 f_equiv.
+    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
+  Qed.
+
+  Global Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V).
+  Proof. apply _. Qed.
+
+  Global Instance inv_pointsto_persistent l I : Persistent (l ↦_I □).
+  Proof. apply _. Qed.
+
+  Global Instance inv_pointsto_timeless l I : Timeless (l ↦_I □).
+  Proof. apply _. Qed.
+
+  Global Instance inv_pointsto_own_timeless l v I : Timeless (l ↦_I v).
+  Proof. apply _. Qed.
+
+  (** * Public lemmas *)
+
+  Lemma make_inv_pointsto l v I E :
+    ↑inv_heapN ⊆ E →
+    I v →
+    inv_heap_inv L V -∗ l ↦ v ={E}=∗ l ↦_I v.
+  Proof.
+    iIntros (HN HI) "#Hinv Hl".
+    iMod (inv_acc_timeless _ inv_heapN with "Hinv") as "[HP Hclose]"; first done.
+    iDestruct "HP" as (h) "[H● HsepM]".
+    destruct (h !! l) as [v'| ] eqn: Hlookup.
+    - (* auth map contains l --> contradiction *)
+      iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
+      by iCombine "Hl Hl'" gives %[??].
+    - iMod (own_update with "H●") as "[H● H◯]".
+      { apply lookup_to_inv_heap_None in Hlookup.
+        apply (auth_update_alloc _
+          (to_inv_heap (<[l:=(v,I)]> h)) (to_inv_heap ({[l:=(v,I)]}))).
+        rewrite to_inv_heap_insert to_inv_heap_singleton.
+        by apply: alloc_singleton_local_update. }
+      iMod ("Hclose" with "[H● HsepM Hl]").
+      + iExists _.
+        iDestruct (big_sepM_insert _ _ _ (_,_) with "[$HsepM $Hl]")
+          as "HsepM"; auto with iFrame.
+      + iModIntro. by rewrite /inv_pointsto_own to_inv_heap_singleton.
+  Qed.
+
+  Lemma inv_pointsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
+  Proof.
+    iApply own_mono. apply auth_frag_mono.
+    rewrite singleton_included_total pair_included.
+    split; [apply: ucmra_unit_least|done].
+  Qed.
+
+  (** An accessor to make use of [inv_pointsto_own].
+    This opens the invariant *before* consuming [inv_pointsto_own] so that you can use
+    this before opening an atomic update that provides [inv_pointsto_own]!. *)
+  Lemma inv_pointsto_own_acc_strong E :
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv L V ={E, E ∖ ↑inv_heapN}=∗ ∀ l v I, l ↦_I v -∗
+      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗
+        inv_pointsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
+  Proof.
+    iIntros (HN) "#Hinv".
+    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
+    iIntros "!>" (l v I) "Hl_inv".
+    iDestruct "HP" as (h) "[H● HsepM]".
+    iDestruct (inv_pointsto_own_lookup_Some with "Hl_inv H●") as %(I'&?&HI').
+    setoid_rewrite HI'.
+    iDestruct (big_sepM_delete with "HsepM") as "[[HI Hl] HsepM]"; first done.
+    iIntros "{$HI $Hl}" (w ?) "Hl".
+    iMod (own_update_2 with "H● Hl_inv") as "[H● H◯]".
+    { apply (auth_update _ _ (<[l := (Excl' w, to_agree I')]> (to_inv_heap h))
+             {[l := (Excl' w, to_agree I)]}).
+      apply: singleton_local_update.
+      { by apply lookup_to_inv_heap_Some. }
+      apply: prod_local_update_1. apply: option_local_update.
+      apply: exclusive_local_update. done. }
+    iDestruct (big_sepM_insert _ _ _ (w, I') with "[$HsepM $Hl //]") as "HsepM".
+    { apply lookup_delete. }
+    rewrite insert_delete_insert -to_inv_heap_insert. iIntros "!> {$H◯}".
+    iApply ("Hclose" with "[H● HsepM]"). iExists _; by iFrame.
+  Qed.
+
+  (** Derive a more standard accessor. *)
+  Lemma inv_pointsto_own_acc E l v I:
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv L V -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
+      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
+  Proof.
+    iIntros (?) "#Hinv Hl".
+    iMod (inv_pointsto_own_acc_strong with "Hinv") as "Hacc"; first done.
+    iDestruct ("Hacc" with "Hl") as "(HI & Hl & Hclose)".
+    iIntros "!> {$HI $Hl}" (w) "HI Hl".
+    iMod ("Hclose" with "HI Hl") as "[$ $]".
+  Qed.
+
+  Lemma inv_pointsto_acc l I E :
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv L V -∗ l ↦_I □ ={E, E ∖ ↑inv_heapN}=∗
+    ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
+  Proof.
+    iIntros (HN) "#Hinv Hl_inv".
+    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
+    iModIntro.
+    iDestruct "HP" as (h) "[H● HsepM]".
+    iDestruct (inv_pointsto_lookup_Some with "Hl_inv H●") as %(v&I'&?&HI').
+    iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"; first done.
+    setoid_rewrite HI'.
+    iExists _. iIntros "{$HI $Hl} Hl".
+    iMod ("Hclose" with "[H● HsepM Hl]"); last done.
+    iExists _. iFrame "H●". iApply ("HsepM" with "[$Hl //]").
+  Qed.
+
+End inv_heap.
+
+Global Typeclasses Opaque inv_heap_inv inv_pointsto inv_pointsto_own.

iris/base_logic/lib/ghost_map.v

+(** A "ghost map" (or "ghost heap") with a proposition controlling authoritative
+ownership of the entire heap, and a "points-to-like" proposition for (mutable,
+fractional, or persistent read-only) ownership of individual elements. *)
+From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import proofmode.
+From iris.algebra Require Import gmap_view.
+From iris.algebra Require Export dfrac.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Import options.
+
+(** The CMRA we need.
+FIXME: This is intentionally discrete-only, but
+should we support setoids via [Equiv]? *)
+Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
+  #[local] ghost_map_inG :: inG Σ (gmap_viewR K (agreeR (leibnizO V)));
+}.
+
+Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
+  #[ GFunctor (gmap_viewR K (agreeR (leibnizO V))) ].
+
+Global Instance subG_ghost_mapΣ Σ (K V : Type) `{Countable K} :
+  subG (ghost_mapΣ K V) Σ → ghost_mapG Σ K V.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context `{ghost_mapG Σ K V}.
+
+  Local Definition ghost_map_auth_def
+      (γ : gname) (q : Qp) (m : gmap K V) : iProp Σ :=
+    own γ (gmap_view_auth (V:=agreeR $ leibnizO V) (DfracOwn q) (to_agree <$> m)).
+  Local Definition ghost_map_auth_aux : seal (@ghost_map_auth_def).
+  Proof. by eexists. Qed.
+  Definition ghost_map_auth := ghost_map_auth_aux.(unseal).
+  Local Definition ghost_map_auth_unseal :
+    @ghost_map_auth = @ghost_map_auth_def := ghost_map_auth_aux.(seal_eq).
+
+  Local Definition ghost_map_elem_def
+      (γ : gname) (k : K) (dq : dfrac) (v : V) : iProp Σ :=
+    own γ (gmap_view_frag (V:=agreeR $ leibnizO V) k dq (to_agree v)).
+  Local Definition ghost_map_elem_aux : seal (@ghost_map_elem_def).
+  Proof. by eexists. Qed.
+  Definition ghost_map_elem := ghost_map_elem_aux.(unseal).
+  Local Definition ghost_map_elem_unseal :
+    @ghost_map_elem = @ghost_map_elem_def := ghost_map_elem_aux.(seal_eq).
+End definitions.
+
+Notation "k ↪[ γ ] dq v" := (ghost_map_elem γ k dq v)
+  (at level 20, γ at level 50, dq custom dfrac at level 1,
+   format "k  ↪[ γ ] dq  v") : bi_scope.
+
+Local Ltac unseal := rewrite
+  ?ghost_map_auth_unseal /ghost_map_auth_def
+  ?ghost_map_elem_unseal /ghost_map_elem_def.
+
+Section lemmas.
+  Context `{ghost_mapG Σ K V}.
+  Implicit Types (k : K) (v : V) (dq : dfrac) (q : Qp) (m : gmap K V).
+
+  (** * Lemmas about the map elements *)
+  Global Instance ghost_map_elem_timeless k γ dq v : Timeless (k ↪[γ]{dq} v).
+  Proof. unseal. apply _. Qed.
+  Global Instance ghost_map_elem_persistent k γ v : Persistent (k ↪[γ]□ v).
+  Proof. unseal. apply _. Qed.
+  Global Instance ghost_map_elem_fractional k γ v :
+    Fractional (λ q, k ↪[γ]{#q} v)%I.
+  Proof. unseal=> p q. rewrite -own_op -gmap_view_frag_add agree_idemp //. Qed.
+  Global Instance ghost_map_elem_as_fractional k γ q v :
+    AsFractional (k ↪[γ]{#q} v) (λ q, k ↪[γ]{#q} v)%I q.
+  Proof. split; first done. apply _. Qed.
+
+  Local Lemma ghost_map_elems_unseal γ m dq :
+    ([∗ map] k ↦ v ∈ m, k ↪[γ]{dq} v) ==∗
+    own γ ([^op map] k↦v ∈ m,
+      gmap_view_frag (V:=agreeR (leibnizO V)) k dq (to_agree v)).
+  Proof.
+    unseal. destruct (decide (m = ∅)) as [->|Hne].
+    - rewrite !big_opM_empty. iIntros "_". iApply own_unit.
+    - rewrite big_opM_own //. iIntros "?". done.
+  Qed.
+
+  Lemma ghost_map_elem_valid k γ dq v : k ↪[γ]{dq} v -∗ ⌜✓ dq⌝.
+  Proof.
+    unseal. iIntros "Helem".
+    iDestruct (own_valid with "Helem") as %?%gmap_view_frag_valid.
+    naive_solver.
+  Qed.
+  Lemma ghost_map_elem_valid_2 k γ dq1 dq2 v1 v2 :
+    k ↪[γ]{dq1} v1 -∗ k ↪[γ]{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+  Proof.
+    unseal. iIntros "H1 H2".
+    iCombine "H1 H2" gives %[? Hag]%gmap_view_frag_op_valid.
+    rewrite to_agree_op_valid_L in Hag. done.
+  Qed.
+  Lemma ghost_map_elem_agree k γ dq1 dq2 v1 v2 :
+    k ↪[γ]{dq1} v1 -∗ k ↪[γ]{dq2} v2 -∗ ⌜v1 = v2⌝.
+  Proof.
+    iIntros "Helem1 Helem2".
+    iDestruct (ghost_map_elem_valid_2 with "Helem1 Helem2") as %[_ ?].
+    done.
+  Qed.
+
+  Global Instance ghost_map_elem_combine_gives γ k v1 dq1 v2 dq2 :
+    CombineSepGives (k ↪[γ]{dq1} v1) (k ↪[γ]{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (ghost_map_elem_valid_2 with "H1 H2") as %[H1 H2].
+    eauto.
+  Qed.
+
+  Lemma ghost_map_elem_combine k γ dq1 dq2 v1 v2 :
+    k ↪[γ]{dq1} v1 -∗ k ↪[γ]{dq2} v2 -∗ k ↪[γ]{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
+  Proof.
+    iIntros "Hl1 Hl2". iDestruct (ghost_map_elem_agree with "Hl1 Hl2") as %->.
+    unseal. iCombine "Hl1 Hl2" as "Hl". rewrite agree_idemp. eauto with iFrame.
+  Qed.
+
+  Global Instance ghost_map_elem_combine_as k γ dq1 dq2 v1 v2 :
+    CombineSepAs (k ↪[γ]{dq1} v1) (k ↪[γ]{dq2} v2) (k ↪[γ]{dq1 ⋅ dq2} v1) | 60.
+    (* higher cost than the Fractional instance [combine_sep_fractional_bwd],
+       which kicks in for #qs *)
+  Proof.
+    rewrite /CombineSepAs. iIntros "[H1 H2]".
+    iDestruct (ghost_map_elem_combine with "H1 H2") as "[$ _]".
+  Qed.
+
+  Lemma ghost_map_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
+    ¬ ✓ (dq1 ⋅ dq2) → k1 ↪[γ]{dq1} v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
+  Proof.
+    iIntros (?) "H1 H2"; iIntros (->).
+    by iCombine "H1 H2" gives %[??].
+  Qed.
+  Lemma ghost_map_elem_ne γ k1 k2 dq2 v1 v2 :
+    k1 ↪[γ] v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
+  Proof. apply ghost_map_elem_frac_ne. apply: exclusive_l. Qed.
+
+  (** Make an element read-only. *)
+  Lemma ghost_map_elem_persist k γ dq v :
+    k ↪[γ]{dq} v ==∗ k ↪[γ]□ v.
+  Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
+
+  (** Recover fractional ownership for read-only element. *)
+  Lemma ghost_map_elem_unpersist k γ v :
+    k ↪[γ]□ v ==∗ ∃ q, k ↪[γ]{# q} v.
+  Proof.
+    unseal. iIntros "H".
+    iMod (own_updateP with "H") as "H";
+      first by apply gmap_view_frag_unpersist.
+    iDestruct "H" as (? (q&->)) "H".
+    iIntros "!>". iExists q. done.
+  Qed.
+
+  (** * Lemmas about [ghost_map_auth] *)
+  Lemma ghost_map_alloc_strong P m :
+    pred_infinite P →
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_map_auth γ 1 m ∗ [∗ map] k ↦ v ∈ m, k ↪[γ] v.
+  Proof.
+    unseal. intros.
+    iMod (own_alloc_strong
+      (gmap_view_auth (V:=agreeR (leibnizO V)) (DfracOwn 1) ∅) P)
+      as (γ) "[% Hauth]"; first done.
+    { apply gmap_view_auth_valid. }
+    iExists γ. iSplitR; first done.
+    rewrite -big_opM_own_1 -own_op. iApply (own_update with "Hauth").
+    etrans; first apply (gmap_view_alloc_big _ (to_agree <$> m) (DfracOwn 1)).
+    - apply map_disjoint_empty_r.
+    - done.
+    - by apply map_Forall_fmap.
+    - rewrite right_id big_opM_fmap. done.
+  Qed.
+  Lemma ghost_map_alloc_strong_empty P :
+    pred_infinite P →
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_map_auth γ 1 (∅ : gmap K V).
+  Proof.
+    intros. iMod (ghost_map_alloc_strong P ∅) as (γ) "(% & Hauth & _)"; eauto.
+  Qed.
+  Lemma ghost_map_alloc m :
+    ⊢ |==> ∃ γ, ghost_map_auth γ 1 m ∗ [∗ map] k ↦ v ∈ m, k ↪[γ] v.
+  Proof.
+    iMod (ghost_map_alloc_strong (λ _, True) m) as (γ) "[_ Hmap]".
+    - by apply pred_infinite_True.
+    - eauto.
+  Qed.
+  Lemma ghost_map_alloc_empty :
+    ⊢ |==> ∃ γ, ghost_map_auth γ 1 (∅ : gmap K V).
+  Proof.
+    intros. iMod (ghost_map_alloc ∅) as (γ) "(Hauth & _)"; eauto.
+  Qed.
+
+  Global Instance ghost_map_auth_timeless γ q m : Timeless (ghost_map_auth γ q m).
+  Proof. unseal. apply _. Qed.
+  Global Instance ghost_map_auth_fractional γ m : Fractional (λ q, ghost_map_auth γ q m)%I.
+  Proof. intros p q. unseal. rewrite -own_op -gmap_view_auth_dfrac_op //. Qed.
+  Global Instance ghost_map_auth_as_fractional γ q m :
+    AsFractional (ghost_map_auth γ q m) (λ q, ghost_map_auth γ q m)%I q.
+  Proof. split; first done. apply _. Qed.
+
+  Lemma ghost_map_auth_valid γ q m : ghost_map_auth γ q m -∗ ⌜q ≤ 1⌝%Qp.
+  Proof.
+    unseal. iIntros "Hauth".
+    iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_dfrac_valid.
+    done.
+  Qed.
+  Lemma ghost_map_auth_valid_2 γ q1 q2 m1 m2 :
+    ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
+  Proof.
+    unseal. iIntros "H1 H2".
+    (* We need to explicitly specify the Inj instances instead of
+    using inj _ since we need to specify [leibnizO] for [to_agree_inj]. *)
+    iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _
+      (to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
+    iPureIntro. split; first done. by fold_leibniz.
+  Qed.
+  Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
+    ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ ⌜m1 = m2⌝.
+  Proof.
+    iIntros "H1 H2".
+    iDestruct (ghost_map_auth_valid_2 with "H1 H2") as %[_ ?].
+    done.
+  Qed.
+
+  (** * Lemmas about the interaction of [ghost_map_auth] with the elements *)
+  Lemma ghost_map_lookup {γ q m k dq v} :
+    ghost_map_auth γ q m -∗ k ↪[γ]{dq} v -∗ ⌜m !! k = Some v⌝.
+  Proof.
+    unseal. iIntros "Hauth Hel".
+    iCombine "Hauth Hel" gives
+      %(av' & _ & _ & Hav' & _ & Hincl)%gmap_view_both_dfrac_valid_discrete_total.
+    iPureIntro.
+    apply lookup_fmap_Some in Hav' as [v' [<- Hv']].
+    (* FIXME: Why do we need [(SI:=natSI) (A:=leibnizO V)]
+    https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555 seems to resolve
+    the problem? *)
+    apply (to_agree_included_L (SI:=natSI) (A:=leibnizO V)) in Hincl.
+    by rewrite Hincl.
+  Qed.
+
+  Global Instance ghost_map_lookup_combine_gives_1 {γ q m k dq v} :
+    CombineSepGives (ghost_map_auth γ q m) (k ↪[γ]{dq} v) ⌜m !! k = Some v⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (ghost_map_lookup with "H1 H2") as %->. eauto.
+  Qed.
+
+  Global Instance ghost_map_lookup_combine_gives_2 {γ q m k dq v} :
+    CombineSepGives (k ↪[γ]{dq} v) (ghost_map_auth γ q m) ⌜m !! k = Some v⌝.
+  Proof.
+    rewrite /CombineSepGives comm. apply ghost_map_lookup_combine_gives_1.
+  Qed.
+
+  Lemma ghost_map_insert {γ m} k v :
+    m !! k = None →
+    ghost_map_auth γ 1 m ==∗ ghost_map_auth γ 1 (<[k := v]> m) ∗ k ↪[γ] v.
+  Proof.
+    unseal. intros Hm. rewrite -own_op.
+    iApply own_update. rewrite fmap_insert. apply: gmap_view_alloc; [|done..].
+    rewrite lookup_fmap Hm //.
+  Qed.
+  Lemma ghost_map_insert_persist {γ m} k v :
+    m !! k = None →
+    ghost_map_auth γ 1 m ==∗ ghost_map_auth γ 1 (<[k := v]> m) ∗ k ↪[γ]□ v.
+  Proof.
+    iIntros (?) "Hauth".
+    iMod (ghost_map_insert k with "Hauth") as "[$ Helem]"; first done.
+    iApply ghost_map_elem_persist. done.
+  Qed.
+
+  Lemma ghost_map_delete {γ m k v} :
+    ghost_map_auth γ 1 m -∗ k ↪[γ] v ==∗ ghost_map_auth γ 1 (delete k m).
+  Proof.
+    unseal. iApply bi.wand_intro_r. rewrite -own_op.
+    iApply own_update. rewrite fmap_delete. apply: gmap_view_delete.
+  Qed.
+
+  Lemma ghost_map_update {γ m k v} w :
+    ghost_map_auth γ 1 m -∗ k ↪[γ] v ==∗ ghost_map_auth γ 1 (<[k := w]> m) ∗ k ↪[γ] w.
+  Proof.
+    unseal. iApply bi.wand_intro_r. rewrite -!own_op.
+    iApply own_update. rewrite fmap_insert. apply: gmap_view_replace; done.
+  Qed.
+
+  (** Big-op versions of above lemmas *)
+  Lemma ghost_map_lookup_big {γ q m} m0 :
+    ghost_map_auth γ q m -∗
+    ([∗ map] k↦v ∈ m0, k ↪[γ] v) -∗
+    ⌜m0 ⊆ m⌝.
+  Proof.
+    iIntros "Hauth Hfrag". rewrite map_subseteq_spec. iIntros (k v Hm0).
+    iDestruct (ghost_map_lookup with "Hauth [Hfrag]") as %->.
+    { rewrite big_sepM_lookup; done. }
+    done.
+  Qed.
+
+  Lemma ghost_map_insert_big {γ m} m' :
+    m' ##ₘ m →
+    ghost_map_auth γ 1 m ==∗
+    ghost_map_auth γ 1 (m' ∪ m) ∗ ([∗ map] k ↦ v ∈ m', k ↪[γ] v).
+  Proof.
+    unseal. intros ?. rewrite -big_opM_own_1 -own_op. iApply own_update.
+    etrans; first apply: (gmap_view_alloc_big _ (to_agree <$> m') (DfracOwn 1)).
+    - apply map_disjoint_fmap. done.
+    - done.
+    - by apply map_Forall_fmap.
+    - rewrite map_fmap_union big_opM_fmap. done.
+  Qed.
+  Lemma ghost_map_insert_persist_big {γ m} m' :
+    m' ##ₘ m →
+    ghost_map_auth γ 1 m ==∗
+    ghost_map_auth γ 1 (m' ∪ m) ∗ ([∗ map] k ↦ v ∈ m', k ↪[γ]□ v).
+  Proof.
+    iIntros (Hdisj) "Hauth".
+    iMod (ghost_map_insert_big m' with "Hauth") as "[$ Helem]"; first done.
+    iApply big_sepM_bupd. iApply (big_sepM_impl with "Helem").
+    iIntros "!#" (k v) "_". iApply ghost_map_elem_persist.
+  Qed.
+
+  Lemma ghost_map_delete_big {γ m} m0 :
+    ghost_map_auth γ 1 m -∗
+    ([∗ map] k↦v ∈ m0, k ↪[γ] v) ==∗
+    ghost_map_auth γ 1 (m ∖ m0).
+  Proof.
+    iIntros "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
+    unseal. iApply (own_update_2 with "Hauth Hfrag").
+    rewrite map_fmap_difference.
+    etrans; last apply: gmap_view_delete_big.
+    rewrite big_opM_fmap. done.
+  Qed.
+
+  Theorem ghost_map_update_big {γ m} m0 m1 :
+    dom m0 = dom m1 →
+    ghost_map_auth γ 1 m -∗
+    ([∗ map] k↦v ∈ m0, k ↪[γ] v) ==∗
+    ghost_map_auth γ 1 (m1 ∪ m) ∗
+        [∗ map] k↦v ∈ m1, k ↪[γ] v.
+  Proof.
+    iIntros (?) "Hauth Hfrag".
+    iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
+    unseal. rewrite -big_opM_own_1 -own_op.
+    iApply (own_update_2 with "Hauth Hfrag").
+    rewrite map_fmap_union.
+    rewrite -!(big_opM_fmap to_agree (λ k, gmap_view_frag k (DfracOwn 1))).
+    apply: gmap_view_replace_big.
+    - rewrite !dom_fmap_L. done.
+    - by apply map_Forall_fmap.
+  Qed.
+
+End lemmas.

iris/base_logic/lib/ghost_var.v

+(** A simple "ghost variable" of arbitrary type with fractional ownership.
+Can be mutated when fully owned. *)
+From iris.algebra Require Import dfrac_agree proofmode_classes frac.
+From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Import options.
+
+(** The CMRA we need. *)
+Class ghost_varG Σ (A : Type) := GhostVarG {
+  #[local] ghost_var_inG :: inG Σ (dfrac_agreeR $ leibnizO A);
+}.
+Global Hint Mode ghost_varG - ! : typeclass_instances.
+
+Definition ghost_varΣ (A : Type) : gFunctors :=
+  #[ GFunctor (dfrac_agreeR $ leibnizO A) ].
+
+Global Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
+Proof. solve_inG. Qed.
+
+Local Definition ghost_var_def `{!ghost_varG Σ A}
+    (γ : gname) (q : Qp) (a : A) : iProp Σ :=
+  own γ (to_frac_agree (A:=leibnizO A) q a).
+Local Definition ghost_var_aux : seal (@ghost_var_def). Proof. by eexists. Qed.
+Definition ghost_var := ghost_var_aux.(unseal).
+Local Definition ghost_var_unseal :
+  @ghost_var = @ghost_var_def := ghost_var_aux.(seal_eq).
+Global Arguments ghost_var {Σ A _} γ q a.
+
+Local Ltac unseal := rewrite ?ghost_var_unseal /ghost_var_def.
+
+Section lemmas.
+  Context `{!ghost_varG Σ A}.
+  Implicit Types (a b : A) (q : Qp).
+
+  Global Instance ghost_var_timeless γ q a : Timeless (ghost_var γ q a).
+  Proof. unseal. apply _. Qed.
+
+  Global Instance ghost_var_fractional γ a : Fractional (λ q, ghost_var γ q a).
+  Proof. intros q1 q2. unseal. rewrite -own_op -frac_agree_op //. Qed.
+  Global Instance ghost_var_as_fractional γ a q :
+    AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
+  Proof. split; [done|]. apply _. Qed.
+
+  Lemma ghost_var_alloc_strong a (P : gname → Prop) :
+    pred_infinite P →
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_var γ 1 a.
+  Proof. unseal. intros. iApply own_alloc_strong; done. Qed.
+  Lemma ghost_var_alloc a :
+    ⊢ |==> ∃ γ, ghost_var γ 1 a.
+  Proof. unseal. iApply own_alloc. done. Qed.
+
+  Lemma ghost_var_valid_2 γ a1 q1 a2 q2 :
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
+  Proof.
+    unseal. iIntros "Hvar1 Hvar2".
+    iCombine "Hvar1 Hvar2" gives %[Hq Ha]%frac_agree_op_valid.
+    done.
+  Qed.
+  (** Almost all the time, this is all you really need. *)
+  Lemma ghost_var_agree γ a1 q1 a2 q2 :
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2⌝.
+  Proof.
+    iIntros "Hvar1 Hvar2".
+    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
+  Qed.
+
+  Global Instance ghost_var_combine_gives γ a1 q1 a2 q2 :
+    CombineSepGives (ghost_var γ q1 a1) (ghost_var γ q2 a2)
+      ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (ghost_var_valid_2 with "H1 H2") as %[H1 H2].
+    eauto.
+  Qed.
+
+  Global Instance ghost_var_combine_as γ a1 q1 a2 q2 q :
+    IsOp q q1 q2 →
+    CombineSepAs (ghost_var γ q1 a1) (ghost_var γ q2 a2)
+      (ghost_var γ q a1) | 60.
+  (* higher cost than the Fractional instance, which is used for a1 = a2 *)
+  Proof.
+    rewrite /CombineSepAs /IsOp => ->. iIntros "[H1 H2]".
+    (* This can't be a single [iCombine] since the instance providing that is
+    exactly what we are proving here. *)
+    iCombine "H1 H2" gives %[_ ->].
+    by iCombine "H1 H2" as "H".
+  Qed.
+
+  (** This is just an instance of fractionality above, but that can be hard to find. *)
+  Lemma ghost_var_split γ a q1 q2 :
+    ghost_var γ (q1 + q2) a -∗ ghost_var γ q1 a ∗ ghost_var γ q2 a.
+  Proof. iIntros "[$$]". Qed.
+
+  (** Update the ghost variable to new value [b]. *)
+  Lemma ghost_var_update b γ a :
+    ghost_var γ 1 a ==∗ ghost_var γ 1 b.
+  Proof.
+    unseal. iApply own_update. apply cmra_update_exclusive. done.
+  Qed.
+  Lemma ghost_var_update_2 b γ a1 q1 a2 q2 :
+    (q1 + q2 = 1)%Qp →
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 ==∗ ghost_var γ q1 b ∗ ghost_var γ q2 b.
+  Proof.
+    intros Hq. unseal. rewrite -own_op. iApply own_update_2.
+    apply frac_agree_update_2. done.
+  Qed.
+  Lemma ghost_var_update_halves b γ a1 a2 :
+    ghost_var γ (1/2) a1 -∗
+    ghost_var γ (1/2) a2 ==∗
+    ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
+  Proof. iApply ghost_var_update_2. apply Qp.half_half. Qed.
+
+  (** Framing support *)
+  Global Instance frame_ghost_var p γ a q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (ghost_var γ q1 a) (ghost_var γ q2 a) (ghost_var γ q a) | 5.
+  Proof. apply: frame_fractional. Qed.
+
+End lemmas.

iris/base_logic/lib/gset_bij.v

+(** Propositions for reasoning about monotone partial bijections.
+
+This library provides two propositions [gset_bij_own_auth γ L] and
+[gset_bij_own_elem γ a b], where [L] is a bijection between types [A] and [B]
+represented by a set of associations [gset (A * B)]. The idea is that
+[gset_bij_own_auth γ L] is an authoritative bijection [L], while
+[gset_bij_own_elem γ a b] is a persistent resource saying [L] associates [a]
+and [b].
+
+The main use case is in a logical relation-based proof where [L] maintains the
+association between locations [A] in one execution and [B] in another (perhaps
+of different types, if the logical relation relates two different semantics).
+
+The association [L] is always bijective, so that if [a] is mapped to [b], there
+should be no other mappings for either [a] or [b]; the [gset_bij_own_extend]
+update theorem enforces that new mappings respect this property, and
+[gset_bij_own_elem_agree] allows the user to exploit bijectivity. The bijection
+grows monotonically, so that the set of associations only grows; this is
+captured by the persistence of [gset_bij_own_elem].
+
+This library is a logical, ownership-based wrapper around [gset_bij]. *)
+
+From iris.algebra.lib Require Import gset_bij.
+From iris.bi.lib Require Import fractional.
+From iris.base_logic.lib Require Import own.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+(* The uCMRA we need. *)
+Class gset_bijG Σ A B `{Countable A, Countable B} :=
+  GsetBijG { #[local] gset_bijG_inG :: inG Σ (gset_bijR A B); }.
+Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
+
+Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
+  #[ GFunctor (gset_bijR A B) ].
+Global Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
+  subG (gset_bijΣ A B) Σ → gset_bijG Σ A B.
+Proof. solve_inG. Qed.
+
+Definition gset_bij_own_auth_def `{gset_bijG Σ A B} (γ : gname)
+    (dq : dfrac) (L : gset (A * B)) : iProp Σ :=
+  own γ (gset_bij_auth dq L).
+Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexists. Qed.
+Definition gset_bij_own_auth := unseal gset_bij_own_auth_aux.
+Definition gset_bij_own_auth_eq :
+  @gset_bij_own_auth = @gset_bij_own_auth_def := seal_eq gset_bij_own_auth_aux.
+Global Arguments gset_bij_own_auth {_ _ _ _ _ _ _ _}.
+
+Definition gset_bij_own_elem_def `{gset_bijG Σ A B} (γ : gname)
+  (a : A) (b : B) : iProp Σ := own γ (gset_bij_elem a b).
+Definition gset_bij_own_elem_aux : seal (@gset_bij_own_elem_def). Proof. by eexists. Qed.
+Definition gset_bij_own_elem := unseal gset_bij_own_elem_aux.
+Definition gset_bij_own_elem_eq :
+  @gset_bij_own_elem = @gset_bij_own_elem_def := seal_eq gset_bij_own_elem_aux.
+Global Arguments gset_bij_own_elem {_ _ _ _ _ _ _ _}.
+
+Section gset_bij.
+  Context `{gset_bijG Σ A B}.
+  Implicit Types (L : gset (A * B)) (a : A) (b : B).
+
+  Global Instance gset_bij_own_auth_timeless γ q L :
+    Timeless (gset_bij_own_auth γ q L).
+  Proof. rewrite gset_bij_own_auth_eq. apply _. Qed.
+  Global Instance gset_bij_own_elem_timeless γ a b :
+    Timeless (gset_bij_own_elem γ a b).
+  Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
+  Global Instance gset_bij_own_elem_persistent γ a b :
+    Persistent (gset_bij_own_elem γ a b).
+  Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
+
+  Global Instance gset_bij_own_auth_fractional γ L :
+    Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L).
+  Proof.
+    intros p q. rewrite gset_bij_own_auth_eq -own_op gset_bij_auth_dfrac_op //.
+  Qed.
+  Global Instance gset_bij_own_auth_as_fractional γ q L :
+    AsFractional (gset_bij_own_auth γ (DfracOwn q) L) (λ q, gset_bij_own_auth γ (DfracOwn q) L) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma gset_bij_own_auth_agree γ dq1 dq2 L1 L2 :
+    gset_bij_own_auth γ dq1 L1 -∗ gset_bij_own_auth γ dq2 L2 -∗
+    ⌜✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1⌝.
+  Proof.
+    rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
+    by iCombine "H1 H2" gives %?%gset_bij_auth_dfrac_op_valid.
+  Qed.
+  Lemma gset_bij_own_auth_exclusive γ L1 L2 :
+    gset_bij_own_auth γ (DfracOwn 1) L1 -∗ gset_bij_own_auth γ (DfracOwn 1) L2 -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    by iDestruct (gset_bij_own_auth_agree with "H1 H2") as %[[] _].
+  Qed.
+
+  Lemma gset_bij_own_valid γ q L :
+    gset_bij_own_auth γ q L -∗ ⌜✓ q ∧ gset_bijective L⌝.
+  Proof.
+    rewrite gset_bij_own_auth_eq. iIntros "Hauth".
+    by iDestruct (own_valid with "Hauth") as %?%gset_bij_auth_dfrac_valid.
+  Qed.
+
+  Lemma gset_bij_own_elem_agree γ a a' b b' :
+    gset_bij_own_elem γ a b -∗ gset_bij_own_elem γ a' b' -∗
+    ⌜a = a' ↔ b = b'⌝.
+  Proof.
+    rewrite gset_bij_own_elem_eq. iIntros "Hel1 Hel2".
+    by iCombine "Hel1 Hel2" gives %?%gset_bij_elem_agree.
+  Qed.
+
+  Lemma gset_bij_own_elem_get {γ q L} a b :
+    (a, b) ∈ L →
+    gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b.
+  Proof.
+    intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
+    iApply own_mono. by apply bij_view_included.
+  Qed.
+
+  Lemma gset_bij_elem_of {γ q L} a b :
+    gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b -∗ ⌜(a, b) ∈ L⌝.
+  Proof.
+    iIntros "Hauth Helem". rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
+    iCombine "Hauth Helem" gives "%Ha".
+    iPureIntro. revert Ha. rewrite bij_both_dfrac_valid. intros (_ & _ & ?); done.
+  Qed.
+
+  Lemma gset_bij_own_elem_get_big γ q L :
+    gset_bij_own_auth γ q L -∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
+  Proof.
+    iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
+    by iApply gset_bij_own_elem_get.
+  Qed.
+
+  Lemma gset_bij_own_alloc L :
+    gset_bijective L →
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ (DfracOwn 1) L ∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
+  Proof.
+    intro. iAssert (∃ γ, gset_bij_own_auth γ (DfracOwn 1) L)%I with "[>]" as (γ) "Hauth".
+    { rewrite gset_bij_own_auth_eq. iApply own_alloc. by apply gset_bij_auth_valid. }
+    iExists γ. iModIntro. iSplit; [done|].
+    by iApply gset_bij_own_elem_get_big.
+  Qed.
+  Lemma gset_bij_own_alloc_empty :
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ (DfracOwn 1) (∅ : gset (A * B)).
+  Proof. iMod (gset_bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
+
+  Lemma gset_bij_own_extend {γ L} a b :
+    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
+    gset_bij_own_auth γ (DfracOwn 1) L ==∗
+    gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+  Proof.
+    iIntros (??) "Hauth".
+    iAssert (gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L)) with "[> Hauth]" as "Hauth".
+    { rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
+      by apply gset_bij_auth_extend. }
+    iModIntro. iSplit; [done|].
+    iApply (gset_bij_own_elem_get with "Hauth"). set_solver.
+  Qed.
+
+  Lemma gset_bij_own_extend_internal {γ L} a b :
+    (∀ b', gset_bij_own_elem γ a b' -∗ False) -∗
+    (∀ a', gset_bij_own_elem γ a' b -∗ False) -∗
+    gset_bij_own_auth γ (DfracOwn 1) L ==∗
+    gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+  Proof.
+    iIntros "Ha Hb HL".
+    iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.
+    { iIntros (b' ?). iApply ("Ha" $! b'). by iApply gset_bij_own_elem_get. }
+    iAssert ⌜∀ a', (a', b) ∉ L⌝%I as %?.
+    { iIntros (a' ?). iApply ("Hb" $! a'). by iApply gset_bij_own_elem_get. }
+    by iApply (gset_bij_own_extend with "HL").
+  Qed.
+End gset_bij.

iris/base_logic/lib/invariants.v

+From stdpp Require Export namespaces.
+From iris.algebra Require Import gmap.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export fancy_updates.
+From iris.base_logic.lib Require Import wsat.
+From iris.prelude Require Import options.
+Import le_upd_if.
+
+(** Semantic Invariants *)
+Local Definition inv_def `{!invGS_gen hlc Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+  □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
+Local Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
+Definition inv := inv_aux.(unseal).
+Global Arguments inv {hlc Σ _} N P.
+Local Definition inv_unseal : @inv = @inv_def := inv_aux.(seal_eq).
+Global Instance: Params (@inv) 3 := {}.
+
+(** * Invariants *)
+Section inv.
+  Context `{!invGS_gen hlc Σ}.
+  Implicit Types i : positive.
+  Implicit Types N : namespace.
+  Implicit Types E : coPset.
+  Implicit Types P Q R : iProp Σ.
+
+  (** ** Internal model of invariants *)
+  Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
+    ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧ ownI i P.
+
+  Lemma own_inv_acc E N P :
+    ↑N ⊆ E → own_inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
+  Proof.
+    rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
+    iDestruct 1 as (i) "[Hi #HiP]".
+    iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
+    rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver.
+    rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver.
+    iIntros "(Hw & [HE $] & $) !> !>".
+    iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & $ & HD)".
+    iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P). by iFrame.
+  Qed.
+
+  Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset).
+  Proof.
+    exists (coPpick (↑ N ∖ gset_to_coPset E)).
+    rewrite -elem_of_gset_to_coPset (comm and) -elem_of_difference.
+    apply coPpick_elem_of=> Hfin.
+    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+    apply gset_to_coPset_finite.
+  Qed.
+
+  Lemma own_inv_alloc N E P : ▷ P ={E}=∗ own_inv N P.
+  Proof.
+    rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
+    iIntros "HP [Hw $]".
+    iMod (ownI_alloc (.∈ (↑N : coPset)) P with "[$HP $Hw]")
+      as (i ?) "[$ ?]"; auto using fresh_inv_name.
+    do 2 iModIntro. iExists i. auto.
+  Qed.
+
+  (* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
+  Lemma own_inv_alloc_open N E P :
+    ↑N ⊆ E → ⊢ |={E, E∖↑N}=> own_inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
+  Proof.
+    rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
+    iIntros (Sub) "[Hw HE]".
+    iMod (ownI_alloc_open (.∈ (↑N : coPset)) P with "Hw")
+      as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
+    iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
+      with "[HE]" as "(HEi & HEN\i & HE\N)".
+    { rewrite -?ownE_op; [|set_solver..].
+      rewrite assoc_L -!union_difference_L //. set_solver. }
+    do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
+    iSplitL "Hi".
+    { iExists i. auto. }
+    iIntros "HP [Hw HE\N]".
+    iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
+    do 2 iModIntro. iSplitL; [|done].
+    iCombine "HEi HEN\i HE\N" as "HEN".
+    rewrite -?ownE_op; [|set_solver..].
+    rewrite assoc_L -!union_difference_L //; set_solver.
+  Qed.
+
+  Lemma own_inv_to_inv M P: own_inv M P -∗ inv M P.
+  Proof.
+    iIntros "#I". rewrite inv_unseal. iIntros (E H).
+    iPoseProof (own_inv_acc with "I") as "H"; eauto.
+  Qed.
+
+  (** ** Public API of invariants *)
+  Global Instance inv_contractive N : Contractive (inv N).
+  Proof. rewrite inv_unseal. solve_contractive. Qed.
+
+  Global Instance inv_ne N : NonExpansive (inv N).
+  Proof. apply contractive_ne, _. Qed.
+
+  Global Instance inv_proper N : Proper (equiv ==> equiv) (inv N).
+  Proof. apply ne_proper, _. Qed.
+
+  Global Instance inv_persistent N P : Persistent (inv N P).
+  Proof. rewrite inv_unseal. apply _. Qed.
+
+  Lemma inv_alter N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
+  Proof.
+    rewrite inv_unseal. iIntros "#HI #HPQ !>" (E H).
+    iMod ("HI" $! E H) as "[HP Hclose]".
+    iDestruct ("HPQ" with "HP") as "[$ HQP]".
+    iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
+  Qed.
+
+  Lemma inv_iff N P Q : inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q.
+  Proof.
+    iIntros "#HI #HPQ". iApply (inv_alter with "HI").
+    iIntros "!> !> HP". iSplitL "HP".
+    - by iApply "HPQ".
+    - iIntros "HQ". by iApply "HPQ".
+  Qed.
+
+  Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
+  Proof.
+    iIntros "HP". iApply own_inv_to_inv.
+    iApply (own_inv_alloc N E with "HP").
+  Qed.
+
+  Lemma inv_alloc_open N E P :
+    ↑N ⊆ E → ⊢ |={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
+  Proof.
+    iIntros (?). iMod own_inv_alloc_open as "[HI $]"; first done.
+    iApply own_inv_to_inv. done.
+  Qed.
+
+  Lemma inv_acc E N P :
+    ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
+  Proof.
+    rewrite inv_unseal /inv_def; iIntros (?) "#HI". by iApply "HI".
+  Qed.
+
+  Lemma inv_combine N1 N2 N P Q :
+    N1 ## N2 →
+    ↑N1 ∪ ↑N2 ⊆@{coPset} ↑N →
+    inv N1 P -∗ inv N2 Q -∗ inv N (P ∗ Q).
+  Proof.
+    rewrite inv_unseal. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
+    iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
+    iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
+    iApply fupd_mask_intro; first set_solver.
+    iIntros "Hclose [HP HQ]".
+    iMod "Hclose" as % _. iMod ("HcloseQ" with "HQ") as % _. by iApply "HcloseP".
+  Qed.
+
+  Lemma inv_combine_dup_l N P Q :
+    □ (P -∗ P ∗ P) -∗
+    inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
+  Proof.
+    rewrite inv_unseal. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
+    iMod ("HinvP" with "[//]") as "[HP HcloseP]".
+    iDestruct ("HPdup" with "HP") as "[$ HP]".
+    iMod ("HcloseP" with "HP") as % _.
+    iMod ("HinvQ" with "[//]") as "[$ HcloseQ]".
+    iIntros "!> [HP HQ]". by iApply "HcloseQ".
+  Qed.
+
+  Lemma except_0_inv N P : ◇ inv N P ⊢ inv N P.
+  Proof.
+    rewrite inv_unseal /inv_def. iIntros "#H !>" (E ?).
+    iMod "H". by iApply "H".
+  Qed.
+
+  (** ** Proof mode integration *)
+  Global Instance is_except_0_inv N P : IsExcept0 (inv N P).
+  Proof. apply except_0_inv. Qed.
+
+  Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
+
+  Global Instance into_acc_inv N P E:
+    IntoAcc (X := unit) (inv N P)
+            (↑N ⊆ E) True (fupd E (E ∖ ↑N)) (fupd (E ∖ ↑N) E)
+            (λ _ : (), (▷ P)%I) (λ _ : (), (▷ P)%I) (λ _ : (), None).
+  Proof.
+    rewrite /IntoAcc /accessor bi.exist_unit.
+    iIntros (?) "#Hinv _". by iApply inv_acc.
+  Qed.
+
+  (** ** Derived properties *)
+  Lemma inv_acc_strong E N P :
+    ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ▷ P ={E',↑N ∪ E'}=∗ True.
+  Proof.
+    iIntros (?) "Hinv".
+    iPoseProof (inv_acc (↑ N) N with "Hinv") as "H"; first done.
+    rewrite difference_diag_L.
+    iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
+    rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
+    iIntros (E') "HP".
+    iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
+    by rewrite left_id_L.
+  Qed.
+
+  Lemma inv_acc_timeless E N P `{!Timeless P} :
+    ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
+  Proof.
+    iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
+    iIntros "!> {$HP} HP". iApply "Hclose"; auto.
+  Qed.
+
+  Lemma inv_split_l N P Q : inv N (P ∗ Q) -∗ inv N P.
+  Proof.
+    iIntros "#HI". iApply inv_alter; eauto.
+    iIntros "!> !> [$ $] $".
+  Qed.
+  Lemma inv_split_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
+  Proof.
+    rewrite (comm _ P Q). eapply inv_split_l.
+  Qed.
+  Lemma inv_split N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
+  Proof.
+    iIntros "#H".
+    iPoseProof (inv_split_l with "H") as "$".
+    iPoseProof (inv_split_r with "H") as "$".
+  Qed.
+
+End inv.

iris/base_logic/lib/iprop.v

+From iris.algebra Require Import gmap.
+From iris.algebra Require cofe_solver.
+From iris.base_logic Require Export base_logic.
+From iris.prelude Require Import options.
+
+(** In this file we construct the type [iProp] of propositions of the Iris
+logic. This is done by solving the following recursive domain equation:
+
+  iProp ≈ uPred (∀ i : gid, gname -fin-> (Σ i) iProp)
+
+where:
+
+  Σ : gFunctors  := lists of locally constractive functors
+  i : gid        := indexes addressing individual functors in [Σ]
+  γ : gname      := ghost variable names
+
+The Iris logic is parametrized by a list of locally contractive functors [Σ]
+from the category of COFEs to the category of CMRAs. These functors are
+instantiated with [iProp], the type of Iris propositions, which allows one to
+construct impredicate CMRAs, such as invariants and stored propositions using
+the agreement CMRA. *)
+
+
+(** * Locally contractive functors *)
+(** The type [gFunctor] bundles a functor from the category of COFEs to the
+category of CMRAs with a proof that it is locally contractive. *)
+Structure gFunctor := GFunctor {
+  gFunctor_F :> rFunctor;
+  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
+}.
+Global Arguments GFunctor _ {_}.
+Global Existing Instance gFunctor_map_contractive.
+Add Printing Constructor gFunctor.
+
+(** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
+of [gFunctor]s.
+
+Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
+alternative way to avoid universe inconsistencies with respect to the universe
+monomorphic [list] type.
+
+Defining [gFunctors] as a dependent record instead of a [sigT] avoids other
+universe inconsistencies. *)
+Record gFunctors := GFunctors {
+  gFunctors_len : nat;
+  gFunctors_lookup : fin gFunctors_len → gFunctor
+}.
+
+Definition gid (Σ : gFunctors) := fin (gFunctors_len Σ).
+
+Definition gname := positive.
+Canonical Structure gnameO := leibnizO gname.
+
+(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
+Definition iResF (Σ : gFunctors) : urFunctor :=
+  discrete_funURF (λ i, gmapURF gname (gFunctors_lookup Σ i)).
+
+
+(** We define functions for the empty list of functors, the singleton list of
+functors, and the append operator on lists of functors. These are used to
+compose [gFunctors] out of smaller pieces. *)
+Module gFunctors.
+  Definition nil : gFunctors := GFunctors 0 (fin_0_inv _).
+
+  Definition singleton (F : gFunctor) : gFunctors :=
+    GFunctors 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
+
+  Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
+    GFunctors (gFunctors_len Σ1 + gFunctors_len Σ2)
+              (fin_add_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
+End gFunctors.
+
+Coercion gFunctors.singleton : gFunctor >-> gFunctors.
+Notation "#[ ]" := gFunctors.nil (format "#[ ]").
+Notation "#[ Σ1 ; .. ; Σn ]" :=
+  (gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..).
+
+
+(** * Subfunctors *)
+(** In order to make proofs in the Iris logic modular, they are not done with
+respect to some concrete list of functors [Σ], but are instead parametrized by
+an arbitrary list of functors [Σ] that contains at least certain functors. For
+example, the lock library is parameterized by a functor [Σ] that should have
+the functors corresponding to the heap and the exclusive monoid to manage to
+lock invariant.
+
+The contraints to can be expressed using the type class [subG Σ1 Σ2], which
+expresses that the functors [Σ1] are contained in [Σ2]. *)
+Class subG (Σ1 Σ2 : gFunctors) := in_subG i :
+  { j | gFunctors_lookup Σ1 i = gFunctors_lookup Σ2 j }.
+
+(** Avoid trigger happy type class search: this line ensures that type class
+search is only triggered if the arguments of [subG] do not contain evars. Since
+instance search for [subG] is restrained, instances should persistently have [subG] as
+their first parameter to avoid loops. For example, the instances [subG_authΣ]
+and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
+Global Hint Mode subG ! + : typeclass_instances.
+
+Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
+Proof.
+  move=> H; split.
+  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
+  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
+Qed.
+
+Global Instance subG_refl Σ : subG Σ Σ.
+Proof. move=> i; by exists i. Qed.
+Global Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
+Proof.
+  move=> H i; move: H=> /(_ i) [j ?].
+  exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
+Qed.
+Global Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
+Proof.
+  move=> H i; move: H=> /(_ i) [j ?].
+  exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
+Qed.
+
+
+(** * Solution of the recursive domain equation *)
+(** We first declare a module type and then an instance of it so as to seal all of
+the construction, this way we are sure we do not use any properties of the
+construction, and also avoid Coq from blindly unfolding it. *)
+Module Type iProp_solution_sig.
+  Parameter iPrePropO : gFunctors → ofe.
+  Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
+
+  Definition iResUR (Σ : gFunctors) : ucmra :=
+    discrete_funUR (λ i,
+      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
+  Notation iProp Σ := (uPred (iResUR Σ)).
+  Notation iPropO Σ := (uPredO (iResUR Σ)).
+  Notation iPropI Σ := (uPredI (iResUR Σ)).
+
+  Parameter iProp_unfold: ∀ {Σ}, iPropO Σ -n> iPrePropO Σ.
+  Parameter iProp_fold: ∀ {Σ}, iPrePropO Σ -n> iPropO Σ.
+  Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
+    iProp_fold (iProp_unfold P) ≡ P.
+  Parameter iProp_unfold_fold: ∀ {Σ} (P : iPrePropO Σ),
+    iProp_unfold (iProp_fold P) ≡ P.
+End iProp_solution_sig.
+
+Module Export iProp_solution : iProp_solution_sig.
+  Import cofe_solver.
+  Definition iProp_result (Σ : gFunctors) :
+    solution (uPredOF (iResF Σ)) := solver.result _.
+  Definition iPrePropO (Σ : gFunctors) : ofe := iProp_result Σ.
+  Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
+
+  Definition iResUR (Σ : gFunctors) : ucmra :=
+    discrete_funUR (λ i,
+      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
+  Notation iProp Σ := (uPred (iResUR Σ)).
+  Notation iPropO Σ := (uPredO (iResUR Σ)).
+
+  Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
+    ofe_iso_1 (iProp_result Σ).
+  Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ :=
+    ofe_iso_2 (iProp_result Σ).
+  Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
+  Proof. apply ofe_iso_21. Qed.
+  Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
+  Proof. apply ofe_iso_12. Qed.
+End iProp_solution.
+
+
+(** * Properties of the solution to the recursive domain equation *)
+Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
+  iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q.
+Proof.
+  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: f_equivI.
+Qed.

iris/base_logic/lib/later_credits.v

+(** This file implements later credits, in particular the later-elimination update.
+That update is used internally to define the Iris [fupd]; it should not
+usually be directly used unless you are defining your own [fupd]. *)
+From iris.prelude Require Import options.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Export auth numbers.
+From iris.base_logic.lib Require Import iprop own.
+Import uPred.
+
+
+(** The ghost state for later credits *)
+Class lcGpreS (Σ : gFunctors) := LcGpreS {
+  #[local] lcGpreS_inG :: inG Σ (authR natUR)
+}.
+
+Class lcGS (Σ : gFunctors) := LcGS {
+  #[local] lcGS_inG :: inG Σ (authR natUR);
+  lcGS_name : gname;
+}.
+Global Hint Mode lcGS - : typeclass_instances.
+
+Definition lcΣ := #[GFunctor (authR (natUR))].
+Global Instance subG_lcΣ {Σ} : subG lcΣ Σ → lcGpreS Σ.
+Proof. solve_inG. Qed.
+
+
+(** The user-facing credit resource, denoting ownership of [n] credits. *)
+Local Definition lc_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name (◯ n).
+Local Definition lc_aux : seal (@lc_def). Proof. by eexists. Qed.
+Definition lc := lc_aux.(unseal).
+Local Definition lc_unseal :
+  @lc = @lc_def := lc_aux.(seal_eq).
+Global Arguments lc {Σ _} n.
+
+Notation "'£'  n" := (lc n) (at level 1).
+
+(** The internal authoritative part of the credit ghost state,
+  tracking how many credits are available in total.
+  Users should not directly interface with this. *)
+Local Definition lc_supply_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name (● n).
+Local Definition lc_supply_aux : seal (@lc_supply_def). Proof. by eexists. Qed.
+Local Definition lc_supply := lc_supply_aux.(unseal).
+Local Definition lc_supply_unseal :
+  @lc_supply = @lc_supply_def := lc_supply_aux.(seal_eq).
+Global Arguments lc_supply {Σ _} n.
+
+
+Section later_credit_theory.
+  Context `{!lcGS Σ}.
+  Implicit Types (P Q : iProp Σ).
+
+  (** Later credit rules *)
+  Lemma lc_split n m :
+    £ (n + m) ⊣⊢ £ n ∗ £ m.
+  Proof.
+    rewrite lc_unseal /lc_def.
+    rewrite -own_op auth_frag_op //=.
+  Qed.
+
+  Lemma lc_zero : ⊢ |==> £ 0.
+  Proof.
+    rewrite lc_unseal /lc_def. iApply own_unit.
+  Qed.
+
+  Lemma lc_supply_bound n m :
+    lc_supply m -∗ £ n -∗ ⌜n ≤ m⌝.
+  Proof.
+    rewrite lc_unseal /lc_def.
+    rewrite lc_supply_unseal /lc_supply_def.
+    iIntros "H1 H2".
+    iCombine "H1 H2" gives %Hop.
+    iPureIntro. eapply auth_both_valid_discrete in Hop as [Hlt _].
+    by eapply nat_included.
+  Qed.
+
+  Lemma lc_decrease_supply n m :
+    lc_supply (n + m) -∗ £ n -∗ |==> lc_supply m.
+  Proof.
+    rewrite lc_unseal /lc_def.
+    rewrite lc_supply_unseal /lc_supply_def.
+    iIntros "H1 H2".
+    iMod (own_update_2 with "H1 H2") as "Hown".
+    { eapply auth_update. eapply (nat_local_update _ _ m 0). lia. }
+    by iDestruct "Hown" as "[Hm _]".
+  Qed.
+
+  Lemma lc_succ n :
+    £ (S n) ⊣⊢ £ 1 ∗ £ n.
+  Proof. rewrite -lc_split //=. Qed.
+
+  Lemma lc_weaken {n} m :
+    m ≤ n → £ n -∗ £ m.
+  Proof.
+    intros [k ->]%Nat.le_sum. rewrite lc_split. iIntros "[$ _]".
+  Qed.
+
+  Global Instance lc_timeless n : Timeless (£ n).
+  Proof.
+    rewrite lc_unseal /lc_def. apply _.
+  Qed.
+
+  Global Instance lc_0_persistent : Persistent (£ 0).
+  Proof.
+    rewrite lc_unseal /lc_def. apply _.
+  Qed.
+
+  (** Make sure that the rule for [+] is used before [S], otherwise Coq's
+  unification applies the [S] hint too eagerly. See Iris issue #470. *)
+  Global Instance from_sep_lc_add n m :
+    FromSep (£ (n + m)) (£ n) (£ m) | 0.
+  Proof.
+    by rewrite /FromSep lc_split.
+  Qed.
+  Global Instance from_sep_lc_S n :
+    FromSep (£ (S n)) (£ 1) (£ n) | 1.
+  Proof.
+    by rewrite /FromSep (lc_succ n).
+  Qed.
+  (** When combining later credits with [iCombine], the priorities are
+  reversed when compared to [FromSep] and [IntoSep]. This causes
+  [£ n] and [£ 1] to be combined as [£ (S n)], not as [£ (n + 1)]. *)
+  Global Instance combine_sep_lc_add n m :
+    CombineSepAs (£ n) (£ m) (£ (n + m)) | 1.
+  Proof.
+    by rewrite /CombineSepAs lc_split.
+  Qed.
+  Global Instance combine_sep_lc_S_l n :
+    CombineSepAs (£ n) (£ 1) (£ (S n)) | 0.
+  Proof.
+    by rewrite /CombineSepAs comm (lc_succ n).
+  Qed.
+
+  Global Instance into_sep_lc_add n m :
+    IntoSep (£ (n + m)) (£ n) (£ m) | 0.
+  Proof.
+    by rewrite /IntoSep lc_split.
+  Qed.
+  Global Instance into_sep_lc_S n :
+    IntoSep (£ (S n)) (£ 1) (£ n) | 1.
+  Proof.
+    by rewrite /IntoSep (lc_succ n).
+  Qed.
+End later_credit_theory.
+
+(** Let users import the above without also getting the below laws.
+  This should only be imported by the internal development of fancy updates. *)
+Module le_upd.
+  (** Definition of the later-elimination update *)
+  Definition le_upd_pre `{!lcGS Σ}
+      (le_upd : iProp Σ -d> iPropO Σ) : iProp Σ -d> iPropO Σ := λ P,
+    (∀ n, lc_supply n ==∗
+          (lc_supply n ∗ P) ∨ (∃ m, ⌜m < n⌝ ∗ lc_supply m ∗ ▷ le_upd P))%I.
+
+  Local Instance le_upd_pre_contractive `{!lcGS Σ} : Contractive le_upd_pre.
+  Proof. solve_contractive. Qed.
+  Local Definition le_upd_def `{!lcGS Σ} :
+    iProp Σ -d> iPropO Σ := fixpoint le_upd_pre.
+  Local Definition le_upd_aux : seal (@le_upd_def). Proof. by eexists. Qed.
+  Definition le_upd := le_upd_aux.(unseal).
+  Local Definition le_upd_unseal : @le_upd = @le_upd_def := le_upd_aux.(seal_eq).
+  Global Arguments le_upd {_ _} _.
+  Notation "'|==£>' P" := (le_upd P%I) (at level 99, P at level 200, format "|==£>  P") : bi_scope.
+
+  Local Lemma le_upd_unfold `{!lcGS Σ} P:
+    (|==£> P) ⊣⊢
+    ∀ n, lc_supply n ==∗
+         (lc_supply n ∗ P) ∨ (∃ m, ⌜m < n⌝ ∗ lc_supply m ∗ ▷ le_upd P).
+  Proof.
+    by rewrite le_upd_unseal
+      /le_upd_def {1}(fixpoint_unfold le_upd_pre P) {1}/le_upd_pre.
+  Qed.
+
+  Section le_upd.
+    Context `{!lcGS Σ}.
+    Implicit Types (P Q : iProp Σ).
+
+    (** Rules for the later elimination update *)
+    Global Instance le_upd_ne : NonExpansive le_upd.
+    Proof.
+      intros n; induction (lt_wf n) as [n _ IH].
+      intros P1 P2 HP. rewrite (le_upd_unfold P1) (le_upd_unfold P2).
+      do 9 (done || f_equiv). f_contractive. by eapply IH, dist_lt.
+    Qed.
+
+    Lemma bupd_le_upd P : (|==> P) ⊢ (|==£> P).
+    Proof.
+      rewrite le_upd_unfold; iIntros "Hupd" (x) "Hpr".
+      iMod "Hupd" as "P". iModIntro. iLeft. by iFrame.
+    Qed.
+
+    Lemma le_upd_intro P : P ⊢ |==£> P.
+    Proof.
+      iIntros "H"; by iApply bupd_le_upd.
+    Qed.
+
+    Lemma le_upd_bind P Q :
+      (P -∗ |==£> Q) -∗ (|==£> P) -∗ (|==£> Q).
+    Proof.
+      iLöb as "IH". iIntros "PQ".
+      iEval (rewrite (le_upd_unfold P) (le_upd_unfold Q)).
+      iIntros "Hupd" (x) "Hpr". iMod ("Hupd" with "Hpr") as "[Hupd|Hupd]".
+      - iDestruct "Hupd" as "[Hpr Hupd]".
+        iSpecialize ("PQ" with "Hupd").
+        iEval (rewrite le_upd_unfold) in "PQ".
+        iMod ("PQ" with "Hpr") as "[Hupd|Hupd]".
+        + iModIntro. by iLeft.
+        + iModIntro. iRight. iDestruct "Hupd" as  (x'' Hstep'') "[Hpr Hupd]".
+          iExists _; iFrame. by iPureIntro.
+      - iModIntro. iRight. iDestruct "Hupd" as (x') "(Hstep & Hpr & Hupd)".
+        iExists _; iFrame. iNext. by iApply ("IH" with "PQ Hupd").
+    Qed.
+
+    Lemma le_upd_later_elim P :
+      £ 1 -∗ (▷ |==£> P) -∗ |==£> P.
+    Proof.
+      iIntros "Hc Hl".
+      iEval (rewrite le_upd_unfold). iIntros (n) "Hs".
+      iDestruct (lc_supply_bound with "Hs Hc") as "%".
+      destruct n as [ | n]; first by lia.
+      replace (S n) with (1 + n) by lia.
+      iMod (lc_decrease_supply with "Hs Hc") as "Hs". eauto 10 with iFrame lia.
+    Qed.
+
+    (** Derived lemmas *)
+    Lemma le_upd_mono P Q : (P ⊢ Q) → (|==£> P) ⊢ (|==£> Q).
+    Proof.
+      intros Hent. iApply le_upd_bind.
+      iIntros "P"; iApply le_upd_intro; by iApply Hent.
+    Qed.
+
+    Global Instance le_upd_mono' : Proper ((⊢) ==> (⊢)) le_upd.
+    Proof. intros P Q PQ; by apply le_upd_mono. Qed.
+    Global Instance le_upd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) le_upd.
+    Proof. intros P Q PQ; by apply le_upd_mono. Qed.
+    Global Instance le_upd_equiv_proper : Proper ((≡) ==> (≡)) le_upd.
+    Proof. apply ne_proper. apply _. Qed.
+
+    Lemma le_upd_trans P :  (|==£> |==£> P) ⊢ |==£> P.
+    Proof.
+      iIntros "HP". iApply le_upd_bind; eauto.
+    Qed.
+    Lemma le_upd_frame_r P R : (|==£> P) ∗ R ⊢ |==£> P ∗ R.
+    Proof.
+      iIntros "[Hupd R]". iApply (le_upd_bind with "[R]"); last done.
+      iIntros "P". iApply le_upd_intro. by iFrame.
+    Qed.
+    Lemma le_upd_frame_l P R : R ∗ (|==£> P) ⊢ |==£> R ∗ P.
+    Proof. rewrite comm le_upd_frame_r comm //. Qed.
+
+    Lemma le_upd_later P :
+      £ 1 -∗ ▷ P -∗ |==£> P.
+    Proof.
+      iIntros "H1 H2". iApply (le_upd_later_elim with "H1").
+      iNext. by iApply le_upd_intro.
+    Qed.
+
+    Lemma except_0_le_upd P : ◇ (le_upd P) ⊢ le_upd (◇ P).
+    Proof.
+      rewrite /bi_except_0. apply or_elim; eauto using le_upd_mono, or_intro_r.
+      by rewrite -le_upd_intro -or_intro_l.
+    Qed.
+
+    (** A safety check that later-elimination updates can replace basic updates *)
+    (** We do not use this to build an instance, because it would conflict
+       with the basic updates. *)
+    Local Lemma bi_bupd_mixin_le_upd : BiBUpdMixin (iPropI Σ) le_upd.
+    Proof.
+      split; rewrite /bupd.
+      - apply _.
+      - apply le_upd_intro.
+      - apply le_upd_mono.
+      - apply le_upd_trans.
+      - apply le_upd_frame_r.
+    Qed.
+
+    (** unfolding the later elimination update *)
+    Lemma le_upd_elim n P :
+      lc_supply n -∗
+      (|==£> P) -∗
+      Nat.iter n (λ P, |==> ▷ P) (|==> ◇ (∃ m, ⌜m ≤ n⌝ ∗ lc_supply m ∗ P)).
+    Proof.
+      induction (Nat.lt_wf_0 n) as [n _ IH].
+      iIntros "Ha". rewrite (le_upd_unfold P) //=.
+      iIntros "Hupd". iSpecialize ("Hupd" with "Ha").
+      destruct n as [|n]; simpl.
+      - iMod "Hupd" as "[[H● ?]| Hf]".
+        { do 2 iModIntro. iExists 0. iFrame. done. }
+        iDestruct "Hf" as (x' Hlt) "_". lia.
+      - iMod "Hupd" as "[[Hc P]|Hupd]".
+        + iModIntro. iNext. iApply iter_modal_intro; last first.
+          { do 2 iModIntro. iExists (S n); iFrame; done. }
+          iIntros (Q) "Q"; iModIntro; by iNext.
+        + iModIntro. iDestruct "Hupd" as (m Hstep) "[Hown Hupd]". iNext.
+          iPoseProof (IH with "Hown Hupd") as "Hit"; first done.
+          clear IH.
+          assert (m ≤ n) as [k ->]%Nat.le_sum by lia.
+          rewrite Nat.add_comm Nat.iter_add.
+          iApply iter_modal_intro.
+          { by iIntros (Q) "$". }
+          iApply (iter_modal_mono with "[] Hit").
+          { iIntros (R S) "Hent H". by iApply "Hent". }
+          iIntros "H". iMod "H". iModIntro. iMod "H" as (m' Hle) "H".
+          iModIntro. iExists m'. iFrame. iPureIntro. lia.
+    Qed.
+
+    Lemma le_upd_elim_complete n P :
+      lc_supply n -∗
+      (|==£> P) -∗
+      Nat.iter (S n) (λ Q, |==> ▷ Q) P.
+    Proof.
+      iIntros "Hlc Hupd". iPoseProof (le_upd_elim with "Hlc Hupd") as "Hit".
+      rewrite Nat.iter_succ_r. iApply (iter_modal_mono with "[] Hit").
+      { clear. iIntros (P Q) "Hent HP". by iApply "Hent". }
+      iIntros "Hupd". iMod "Hupd". iModIntro. iMod "Hupd".
+      iNext. iDestruct "Hupd" as "[%m (_ & _ & $)]".
+    Qed.
+
+    (** Proof mode class instances internally needed for people defining their
+    [fupd] with [le_upd]. *)
+    Global Instance elim_bupd_le_upd p P Q :
+      ElimModal True p false (bupd P) P (le_upd Q) (le_upd Q)%I.
+    Proof.
+      rewrite /ElimModal bi.intuitionistically_if_elim //=.
+      rewrite bupd_le_upd. iIntros "_ [HP HPQ]".
+      iApply (le_upd_bind with "HPQ HP").
+    Qed.
+
+    Global Instance from_assumption_le_upd p P Q :
+      FromAssumption p P Q → KnownRFromAssumption p P (le_upd Q).
+    Proof.
+      rewrite /KnownRFromAssumption /FromAssumption=>->. apply le_upd_intro.
+    Qed.
+
+    Global Instance from_pure_le_upd a P φ :
+      FromPure a P φ → FromPure a (le_upd P) φ.
+    Proof. rewrite /FromPure=> <-. apply le_upd_intro. Qed.
+
+    Global Instance is_except_0_le_upd P : IsExcept0 P → IsExcept0 (le_upd P).
+    Proof.
+      rewrite /IsExcept0=> HP.
+      by rewrite -{2}HP -(except_0_idemp P) -except_0_le_upd -(except_0_intro P).
+    Qed.
+
+    Global Instance from_modal_le_upd P :
+      FromModal True modality_id (le_upd P) (le_upd P) P.
+    Proof. by rewrite /FromModal /= -le_upd_intro. Qed.
+
+    Global Instance elim_modal_le_upd p P Q :
+      ElimModal True p false (le_upd P) P (le_upd Q) (le_upd Q).
+    Proof.
+      by rewrite /ElimModal
+        intuitionistically_if_elim le_upd_frame_r wand_elim_r le_upd_trans.
+    Qed.
+
+    Global Instance frame_le_upd p R P Q :
+      Frame p R P Q → Frame p R (le_upd P) (le_upd Q).
+    Proof. rewrite /Frame=><-. by rewrite le_upd_frame_l. Qed.
+  End le_upd.
+
+  (** You probably do NOT want to use this lemma; use [lc_soundness] if you want
+  to actually use [le_upd]! *)
+  Local Lemma lc_alloc `{!lcGpreS Σ} n :
+    ⊢ |==> ∃ _ : lcGS Σ, lc_supply n ∗ £ n.
+  Proof.
+    rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
+    iMod (own_alloc (● n ⋅ ◯ n)) as (γLC) "[H● H◯]";
+      first (apply auth_both_valid; split; done).
+    pose (C := LcGS _ _ γLC).
+    iModIntro. iExists C. iFrame.
+  Qed.
+
+  Lemma lc_soundness `{!lcGpreS Σ} m (P : iProp Σ) `{!Plain P} :
+    (∀ {Hc: lcGS Σ}, £ m -∗ |==£> P) → ⊢ P.
+  Proof.
+    intros H. apply (laterN_soundness _ (S m)).
+    eapply bupd_soundness; first apply _.
+    iStartProof.
+    iMod (lc_alloc m) as (C) "[H● H◯]".
+    iPoseProof (H C) as "Hc". iSpecialize ("Hc" with "H◯").
+    iPoseProof (le_upd_elim_complete m with "H● Hc") as "H".
+    simpl. iMod "H". iModIntro. iNext.
+    clear H. iInduction m as [|m IH]; simpl; [done|].
+    iMod "H". iNext. by iApply "IH".
+  Qed.
+End le_upd.
+
+(** This should only be imported by the internal development of fancy updates. *)
+Module le_upd_if.
+  Export le_upd.
+
+  Section le_upd_if.
+    Context `{!lcGS Σ}.
+
+    Definition le_upd_if (b : bool) : iProp Σ → iProp Σ :=
+      if b then le_upd else bupd.
+
+    Global Instance le_upd_if_mono' b : Proper ((⊢) ==> (⊢)) (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+    Global Instance le_upd_if_flip_mono' b :
+      Proper (flip (⊢) ==> flip (⊢)) (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+    Global Instance le_upd_if_proper b : Proper ((≡) ==> (≡)) (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+    Global Instance le_upd_if_ne b : NonExpansive (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+
+    Lemma le_upd_if_intro b P : P ⊢ le_upd_if b P.
+    Proof.
+      destruct b; [apply le_upd_intro | apply bupd_intro].
+    Qed.
+
+    Lemma le_upd_if_bind b P Q :
+      (P -∗ le_upd_if b Q) -∗ (le_upd_if b P) -∗ (le_upd_if b Q).
+    Proof.
+      destruct b; first apply le_upd_bind. simpl.
+      iIntros "HPQ >HP". by iApply "HPQ".
+    Qed.
+
+    Lemma le_upd_if_mono b P Q : (P ⊢ Q) → (le_upd_if b P) ⊢ (le_upd_if b Q).
+    Proof.
+      destruct b; [apply le_upd_mono | apply bupd_mono].
+    Qed.
+    Lemma le_upd_if_trans b P : (le_upd_if b (le_upd_if b P)) ⊢ le_upd_if b P.
+    Proof.
+      destruct b; [apply le_upd_trans | apply bupd_trans].
+    Qed.
+    Lemma le_upd_if_frame_r b P R : (le_upd_if b P) ∗ R ⊢ le_upd_if b (P ∗ R).
+    Proof.
+      destruct b; [apply le_upd_frame_r | apply bupd_frame_r].
+    Qed.
+
+    Lemma bupd_le_upd_if b P : (|==> P) ⊢ (le_upd_if b P).
+    Proof.
+      destruct b; [apply bupd_le_upd | done].
+    Qed.
+
+    Lemma le_upd_if_frame_l b R Q : (R ∗ le_upd_if b Q) ⊢ le_upd_if b (R ∗ Q).
+    Proof.
+      rewrite comm le_upd_if_frame_r comm //.
+    Qed.
+
+    Lemma except_0_le_upd_if b P : ◇ (le_upd_if b P) ⊢ le_upd_if b (◇ P).
+    Proof.
+      rewrite /bi_except_0. apply or_elim; eauto using le_upd_if_mono, or_intro_r.
+      by rewrite -le_upd_if_intro -or_intro_l.
+    Qed.
+
+    (** Proof mode class instances that we need for the internal development,
+    i.e. for the definition of fancy updates. *)
+    Global Instance elim_bupd_le_upd_if b p P Q :
+      ElimModal True p false (bupd P) P (le_upd_if b Q) (le_upd_if b Q)%I.
+    Proof.
+      rewrite /ElimModal bi.intuitionistically_if_elim //=.
+      rewrite bupd_le_upd_if. iIntros "_ [HP HPQ]".
+      iApply (le_upd_if_bind with "HPQ HP").
+    Qed.
+
+    Global Instance from_assumption_le_upd_if b p P Q :
+      FromAssumption p P Q → KnownRFromAssumption p P (le_upd_if b Q).
+    Proof.
+      rewrite /KnownRFromAssumption /FromAssumption=>->. apply le_upd_if_intro.
+    Qed.
+
+    Global Instance from_pure_le_upd_if b a P φ :
+      FromPure a P φ → FromPure a (le_upd_if b P) φ.
+    Proof. rewrite /FromPure=> <-. apply le_upd_if_intro. Qed.
+
+    Global Instance is_except_0_le_upd_if b P : IsExcept0 P → IsExcept0 (le_upd_if b P).
+    Proof.
+      rewrite /IsExcept0=> HP.
+      by rewrite -{2}HP -(except_0_idemp P) -except_0_le_upd_if -(except_0_intro P).
+    Qed.
+
+    Global Instance from_modal_le_upd_if b P :
+      FromModal True modality_id (le_upd_if b P) (le_upd_if b P) P.
+    Proof. by rewrite /FromModal /= -le_upd_if_intro. Qed.
+
+    Global Instance elim_modal_le_upd_if b p P Q :
+      ElimModal True p false (le_upd_if b P) P (le_upd_if b Q) (le_upd_if b Q).
+    Proof.
+      by rewrite /ElimModal
+        intuitionistically_if_elim le_upd_if_frame_r wand_elim_r le_upd_if_trans.
+    Qed.
+
+    Global Instance frame_le_upd_if b p R P Q :
+      Frame p R P Q → Frame p R (le_upd_if b P) (le_upd_if b Q).
+    Proof. rewrite /Frame=><-. by rewrite le_upd_if_frame_l. Qed.
+  End le_upd_if.
+End le_upd_if.

iris/base_logic/lib/mono_Z.v

+(** Ghost state for a monotonically increasing non-negative integer.
+This is basically a [Z]-typed wrapper over [mono_nat], which can be useful when
+one wants to use [Z] consistently for everything.
+Provides an authoritative proposition [mono_Z_auth_own γ q n] for the
+underlying number [n] and a persistent proposition [mono_nat_lb_own γ m]
+witnessing that the authoritative nat is at least [m].
+
+The key rules are [mono_Z_lb_own_valid], which asserts that an auth at [n] and
+a lower-bound at [m] imply that [m ≤ n], and [mono_Z_update], which allows to
+increase the auth element. At any time the auth nat can be "snapshotted" with
+[mono_Z_get_lb] to produce a persistent lower-bound proposition.
+
+Note: This construction requires the integers to be non-negative, i.e., to have
+the lower bound 0, which gives [mono_Z_lb_own_0 : |==> mono_Z_lb_own γ 0]. This
+rule would be false if we were to generalize to negative integers. See
+https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/889 for a discussion about
+the generalization to negative integers. *)
+From iris.proofmode Require Import proofmode.
+From iris.algebra.lib Require Import mono_nat.
+From iris.bi.lib Require Import fractional.
+From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import mono_nat.
+From iris.prelude Require Import options.
+
+Local Open Scope Z_scope.
+
+Class mono_ZG Σ :=
+  MonoZG { #[local] mono_ZG_natG :: mono_natG Σ; }.
+Definition mono_ZΣ := mono_natΣ.
+
+Local Definition mono_Z_auth_own_def `{!mono_ZG Σ}
+    (γ : gname) (q : Qp) (n : Z) : iProp Σ :=
+  ⌜0 ≤ n⌝ ∗ mono_nat_auth_own γ q (Z.to_nat n).
+Local Definition mono_Z_auth_own_aux : seal (@mono_Z_auth_own_def).
+Proof. by eexists. Qed.
+Definition mono_Z_auth_own := mono_Z_auth_own_aux.(unseal).
+Local Definition mono_Z_auth_own_unseal :
+  @mono_Z_auth_own = @mono_Z_auth_own_def := mono_Z_auth_own_aux.(seal_eq).
+Global Arguments mono_Z_auth_own {Σ _} γ q n.
+
+Local Definition mono_Z_lb_own_def `{!mono_ZG Σ} (γ : gname) (n : Z) : iProp Σ :=
+  ⌜0 ≤ n⌝ ∗ mono_nat_lb_own γ (Z.to_nat n).
+Local Definition mono_Z_lb_own_aux : seal (@mono_Z_lb_own_def). Proof. by eexists. Qed.
+Definition mono_Z_lb_own := mono_Z_lb_own_aux.(unseal).
+Local Definition mono_Z_lb_own_unseal :
+  @mono_Z_lb_own = @mono_Z_lb_own_def := mono_Z_lb_own_aux.(seal_eq).
+Global Arguments mono_Z_lb_own {Σ _} γ n.
+
+Local Ltac unseal := rewrite
+  ?mono_Z_auth_own_unseal /mono_Z_auth_own_def
+  ?mono_Z_lb_own_unseal /mono_Z_lb_own_def.
+
+Section mono_Z.
+  Context `{!mono_ZG Σ}.
+  Implicit Types (n m : Z).
+
+  Global Instance mono_Z_auth_own_timeless γ q n : Timeless (mono_Z_auth_own γ q n).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_Z_lb_own_timeless γ n : Timeless (mono_Z_lb_own γ n).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_Z_lb_own_persistent γ n : Persistent (mono_Z_lb_own γ n).
+  Proof. unseal. apply _. Qed.
+
+  Global Instance mono_Z_auth_own_fractional γ n :
+    Fractional (λ q, mono_Z_auth_own γ q n).
+  Proof.
+    unseal. intros p q. iSplit.
+    - iIntros "[% [$ $]]". eauto.
+    - iIntros "[[% H1] [% H2]]". iCombine "H1 H2" as "$". eauto.
+  Qed.
+  Global Instance mono_Z_auth_own_as_fractional γ q n :
+    AsFractional (mono_Z_auth_own γ q n) (λ q, mono_Z_auth_own γ q n) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma mono_Z_auth_own_agree γ q1 q2 n1 n2 :
+    mono_Z_auth_own γ q1 n1 -∗
+    mono_Z_auth_own γ q2 n2 -∗
+    ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
+  Proof.
+    unseal. iIntros "[% H1] [% H2]".
+    iDestruct (mono_nat_auth_own_agree with "H1 H2") as %?.
+    iPureIntro. naive_solver lia.
+  Qed.
+  Lemma mono_Z_auth_own_exclusive γ n1 n2 :
+    mono_Z_auth_own γ 1 n1 -∗ mono_Z_auth_own γ 1 n2 -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    by iDestruct (mono_Z_auth_own_agree with "H1 H2") as %[[] _].
+  Qed.
+
+  Lemma mono_Z_lb_own_valid γ q n m :
+    mono_Z_auth_own γ q n -∗ mono_Z_lb_own γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
+  Proof.
+    unseal. iIntros "[% Hauth] [% Hlb]".
+    iDestruct (mono_nat_lb_own_valid with "Hauth Hlb") as %Hvalid.
+    iPureIntro. naive_solver lia.
+  Qed.
+
+  (** The conclusion of this lemma is persistent; the proofmode will preserve
+  the [mono_Z_auth_own] in the premise as long as the conclusion is introduced
+  to the persistent context, for example with [iDestruct (mono_Z_lb_own_get
+  with "Hauth") as "#Hfrag"]. *)
+  Lemma mono_Z_lb_own_get γ q n :
+    mono_Z_auth_own γ q n -∗ mono_Z_lb_own γ n.
+  Proof. unseal. iIntros "[% ?]". iSplit; first done. by iApply mono_nat_lb_own_get. Qed.
+
+  Lemma mono_Z_lb_own_le {γ n} n' :
+    n' ≤ n →
+    0 ≤ n' →
+    mono_Z_lb_own γ n -∗ mono_Z_lb_own γ n'.
+  Proof.
+    unseal. iIntros "% % [% ?]". iSplit; first done.
+    iApply mono_nat_lb_own_le; last done. lia.
+  Qed.
+
+  Lemma mono_Z_lb_own_0 γ :
+    ⊢ |==> mono_Z_lb_own γ 0.
+  Proof. unseal. iMod mono_nat_lb_own_0 as "$". eauto. Qed.
+
+  Lemma mono_Z_own_alloc n :
+    0 ≤ n →
+    ⊢ |==> ∃ γ, mono_Z_auth_own γ 1 n ∗ mono_Z_lb_own γ n.
+  Proof.
+    unseal. intros. iMod mono_nat_own_alloc as (γ) "[??]".
+    iModIntro. iExists _. iFrame. eauto.
+  Qed.
+
+  Lemma mono_Z_own_update {γ n} n' :
+    n ≤ n' →
+    mono_Z_auth_own γ 1 n ==∗ mono_Z_auth_own γ 1 n' ∗ mono_Z_lb_own γ n'.
+  Proof.
+    iIntros (?) "Hauth".
+    iAssert (mono_Z_auth_own γ 1 n') with "[> Hauth]" as "Hauth".
+    { unseal. iDestruct "Hauth" as "[% Hauth]".
+      iMod (mono_nat_own_update with "Hauth") as "[$ _]"; auto with lia. }
+    iModIntro. iSplit; [done|]. by iApply mono_Z_lb_own_get.
+  Qed.
+End mono_Z.

iris/base_logic/lib/mono_nat.v

+(** Ghost state for a monotonically increasing nat, wrapping the [mono_natR]
+RA. Provides an authoritative proposition [mono_nat_auth_own γ q n] for the
+underlying number [n] and a persistent proposition [mono_nat_lb_own γ m]
+witnessing that the authoritative nat is at least [m].
+
+The key rules are [mono_nat_lb_own_valid], which asserts that an auth at [n] and
+a lower-bound at [m] imply that [m ≤ n], and [mono_nat_update], which allows to
+increase the auth element. At any time the auth nat can be "snapshotted" with
+[mono_nat_get_lb] to produce a persistent lower-bound proposition. *)
+From iris.proofmode Require Import proofmode.
+From iris.algebra.lib Require Import mono_nat.
+From iris.bi.lib Require Import fractional.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Import options.
+
+Class mono_natG Σ :=
+  MonoNatG { #[local] mono_natG_inG :: inG Σ mono_natR; }.
+
+Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
+Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
+Proof. solve_inG. Qed.
+
+Local Definition mono_nat_auth_own_def `{!mono_natG Σ}
+    (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
+  own γ (●MN{#q} n).
+Local Definition mono_nat_auth_own_aux : seal (@mono_nat_auth_own_def).
+Proof. by eexists. Qed.
+Definition mono_nat_auth_own := mono_nat_auth_own_aux.(unseal).
+Local Definition mono_nat_auth_own_unseal :
+  @mono_nat_auth_own = @mono_nat_auth_own_def := mono_nat_auth_own_aux.(seal_eq).
+Global Arguments mono_nat_auth_own {Σ _} γ q n.
+
+Local Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
+  own γ (◯MN n).
+Local Definition mono_nat_lb_own_aux : seal (@mono_nat_lb_own_def). Proof. by eexists. Qed.
+Definition mono_nat_lb_own := mono_nat_lb_own_aux.(unseal).
+Local Definition mono_nat_lb_own_unseal :
+  @mono_nat_lb_own = @mono_nat_lb_own_def := mono_nat_lb_own_aux.(seal_eq).
+Global Arguments mono_nat_lb_own {Σ _} γ n.
+
+Local Ltac unseal := rewrite
+  ?mono_nat_auth_own_unseal /mono_nat_auth_own_def
+  ?mono_nat_lb_own_unseal /mono_nat_lb_own_def.
+
+Section mono_nat.
+  Context `{!mono_natG Σ}.
+  Implicit Types (n m : nat).
+
+  Global Instance mono_nat_auth_own_timeless γ q n : Timeless (mono_nat_auth_own γ q n).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_nat_lb_own_timeless γ n : Timeless (mono_nat_lb_own γ n).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_nat_lb_own_persistent γ n : Persistent (mono_nat_lb_own γ n).
+  Proof. unseal. apply _. Qed.
+
+  Global Instance mono_nat_auth_own_fractional γ n :
+    Fractional (λ q, mono_nat_auth_own γ q n).
+  Proof. unseal. intros p q. rewrite -own_op -mono_nat_auth_dfrac_op //. Qed.
+  Global Instance mono_nat_auth_own_as_fractional γ q n :
+    AsFractional (mono_nat_auth_own γ q n) (λ q, mono_nat_auth_own γ q n) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma mono_nat_auth_own_agree γ q1 q2 n1 n2 :
+    mono_nat_auth_own γ q1 n1 -∗
+    mono_nat_auth_own γ q2 n2 -∗
+    ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
+  Proof.
+    unseal. iIntros "H1 H2".
+    iCombine "H1 H2" gives %?%mono_nat_auth_dfrac_op_valid; done.
+  Qed.
+  Lemma mono_nat_auth_own_exclusive γ n1 n2 :
+    mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    by iDestruct (mono_nat_auth_own_agree with "H1 H2") as %[[] _].
+  Qed.
+
+  Lemma mono_nat_lb_own_valid γ q n m :
+    mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
+  Proof.
+    unseal. iIntros "Hauth Hlb".
+    iCombine "Hauth Hlb" gives %Hvalid%mono_nat_both_dfrac_valid.
+    auto.
+  Qed.
+
+  (** The conclusion of this lemma is persistent; the proofmode will preserve
+  the [mono_nat_auth_own] in the premise as long as the conclusion is introduced
+  to the persistent context, for example with [iDestruct (mono_nat_lb_own_get
+  with "Hauth") as "#Hfrag"]. *)
+  Lemma mono_nat_lb_own_get γ q n :
+    mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ n.
+  Proof. unseal. iApply own_mono. apply mono_nat_included. Qed.
+
+  Lemma mono_nat_lb_own_le {γ n} n' :
+    n' ≤ n →
+    mono_nat_lb_own γ n -∗ mono_nat_lb_own γ n'.
+  Proof. unseal. intros. iApply own_mono. by apply mono_nat_lb_mono. Qed.
+
+  Lemma mono_nat_lb_own_0 γ :
+    ⊢ |==> mono_nat_lb_own γ 0.
+  Proof. unseal. iApply own_unit. Qed.
+
+  Lemma mono_nat_own_alloc_strong P n :
+    pred_infinite P →
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
+  Proof.
+    unseal. intros.
+    iMod (own_alloc_strong (●MN n ⋅ ◯MN n) P) as (γ) "[% [??]]"; first done.
+    { apply mono_nat_both_valid; auto. }
+    auto with iFrame.
+  Qed.
+  Lemma mono_nat_own_alloc n :
+    ⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
+  Proof.
+    iMod (mono_nat_own_alloc_strong (λ _, True) n) as (γ) "[_ ?]".
+    - by apply pred_infinite_True.
+    - eauto.
+  Qed.
+
+  Lemma mono_nat_own_update {γ n} n' :
+    n ≤ n' →
+    mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n' ∗ mono_nat_lb_own γ n'.
+  Proof.
+    iIntros (?) "Hauth".
+    iAssert (mono_nat_auth_own γ 1 n') with "[> Hauth]" as "Hauth".
+    { unseal. iApply (own_update with "Hauth"). by apply mono_nat_update. }
+    iModIntro. iSplit; [done|]. by iApply mono_nat_lb_own_get.
+  Qed.
+End mono_nat.

iris/base_logic/lib/na_invariants.v

+From iris.algebra Require Import gset coPset.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export invariants.
+From iris.prelude Require Import options.
+Import uPred.
+
+(* Non-atomic ("thread-local") invariants. *)
+
+Definition na_inv_pool_name := gname.
+
+Class na_invG Σ :=
+  #[local] na_inv_inG :: inG Σ (prodR coPset_disjR (gset_disjR positive)).
+
+Definition na_invΣ : gFunctors :=
+  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
+Global Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
+Proof. solve_inG. Qed.
+
+Section defs.
+  Context `{!invGS_gen hlc Σ, !na_invG Σ}.
+
+  Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
+    own p (CoPset E, GSet ∅).
+
+  Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
+    ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
+         inv N (P ∗ own p (ε, GSet {[i]}) ∨ na_own p {[i]}).
+End defs.
+
+Global Instance: Params (@na_inv) 3 := {}.
+Global Typeclasses Opaque na_own na_inv.
+
+Section proofs.
+  Context `{!invGS_gen hlc Σ, !na_invG Σ}.
+
+  Global Instance na_own_timeless p E : Timeless (na_own p E).
+  Proof. rewrite /na_own; apply _. Qed.
+
+  Global Instance na_inv_ne p N : NonExpansive (na_inv p N).
+  Proof. rewrite /na_inv. solve_proper. Qed.
+  Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
+  Proof. apply (ne_proper _). Qed.
+
+  Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
+  Proof. rewrite /na_inv; apply _. Qed.
+
+  Global Instance na_own_empty_persistent p : Persistent (na_own p ∅).
+  Proof. rewrite /na_own; apply _. Qed.
+
+  Lemma na_inv_iff p N P Q : na_inv p N P -∗ ▷ □ (P ↔ Q) -∗ na_inv p N Q.
+  Proof.
+    rewrite /na_inv. iIntros "(%i & % & HI) #HPQ".
+    iExists i. iSplit; first done. iApply (inv_iff with "HI").
+    iIntros "!> !>".
+    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
+  Qed.
+
+  Lemma na_alloc : ⊢ |==> ∃ p, na_own p ⊤.
+  Proof. by apply own_alloc. Qed.
+
+  Lemma na_own_disjoint p E1 E2 : na_own p E1 -∗ na_own p E2 -∗ ⌜E1 ## E2⌝.
+  Proof.
+    iApply wand_intro_r.
+    rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
+  Qed.
+
+  Lemma na_own_union p E1 E2 :
+    E1 ## E2 → na_own p (E1 ∪ E2) ⊣⊢ na_own p E1 ∗ na_own p E2.
+  Proof.
+    intros. rewrite /na_own -own_op -pair_op. by rewrite coPset_disj_union.
+  Qed.
+
+  Lemma na_own_acc E2 E1 tid :
+    E2 ⊆ E1 → na_own tid E1 -∗ na_own tid E2 ∗ (na_own tid E2 -∗ na_own tid E1).
+  Proof.
+    intros HF. assert (E1 = E2 ∪ (E1 ∖ E2)) as -> by exact: union_difference_L.
+    rewrite na_own_union; last by set_solver+. iIntros "[$ $]". auto.
+  Qed.
+
+  Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
+  Proof.
+    iIntros "HP".
+    iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
+    iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
+    { apply prod_updateP'.
+      - apply cmra_updateP_id, (reflexivity (R:=eq)).
+      - apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset)))=> Ef.
+        apply fresh_inv_name. }
+    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
+    rewrite /na_inv.
+    iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
+    iNext. iLeft. by iFrame.
+  Qed.
+
+  Lemma na_inv_acc p E F N P :
+    ↑N ⊆ E → ↑N ⊆ F →
+    na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
+                       (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
+  Proof.
+    rewrite /na_inv. iIntros (??) "#(%i & % & Hinv) Htoks".
+    rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
+    rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
+    iDestruct "Htoks" as "[[Htoki $] $]".
+    iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
+    - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
+      iIntros "!> [HP $]".
+      iInv N as "[[_ >Hdis2]|>Hitok]".
+      + iCombine "Hdis Hdis2" gives %[_ Hval%gset_disj_valid_op].
+        set_solver.
+      + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
+    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
+  Qed.
+
+  Lemma na_own_empty p : ⊢ |==> na_own p ∅.
+  Proof. apply: own_unit. Qed.
+
+  Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.
+
+  Global Instance into_acc_na p F E N P :
+    IntoAcc (X:=unit) (na_inv p N P)
+            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
+            (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
+              (λ _, Some (na_own p F))%I.
+  Proof.
+    rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
+    rewrite exist_unit -assoc /=.
+    iApply (na_inv_acc with "Hinv"); done.
+  Qed.
+End proofs.

iris/base_logic/lib/own.v

+From iris.algebra Require Import functions gmap proofmode_classes.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export iprop.
+From iris.prelude Require Import options.
+Import uPred.
+
+(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
+[Σ]. This class is similar to the [subG] class, but written down in terms of
+individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
+needed because Coq is otherwise unable to solve type class constraints due to
+higher-order unification problems. *)
+Class inG (Σ : gFunctors) (A : cmra) := InG {
+  inG_id : gid Σ;
+  inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
+  inG_prf : A = inG_apply (iPropO Σ) _;
+}.
+Global Arguments inG_id {_ _} _.
+Global Arguments inG_apply {_ _} _ _ {_}.
+
+(** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
+mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
+not want Coq to pick one arbitrarily. *)
+Global Hint Mode inG - ! : typeclass_instances.
+
+Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
+Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
+
+(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
+Ltac solve_inG :=
+  (* Get all assumptions *)
+  intros;
+  (* Unfold the top-level xΣ. We need to support this to be a function. *)
+  lazymatch goal with
+  | H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
+  | H : subG ?xΣ _ |- _ => try unfold xΣ in H
+  end;
+  (* Take apart subG for non-"atomic" lists *)
+  repeat match goal with
+         | H : subG (gFunctors.app _ _) _ |- _ => apply subG_inv in H; destruct H
+         end;
+  (* Try to turn singleton subG into inG; but also keep the subG for typeclass
+     resolution -- to keep them, we put them onto the goal. *)
+  repeat match goal with
+         | H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
+         end;
+  (* Again get all assumptions and simplify the functors *)
+  intros; simpl in *;
+  (* We support two kinds of goals: Things convertible to inG;
+     and records with inG and typeclass fields. Try to solve the
+     first case. *)
+  try assumption;
+  (* That didn't work, now we're in for the second case. *)
+  split; (assumption || by apply _).
+
+(** * Definition of the connective [own] *)
+Local Definition inG_unfold {Σ A} {i : inG Σ A} :
+    inG_apply i (iPropO Σ) -n> inG_apply i (iPrePropO Σ) :=
+  rFunctor_map _ (iProp_fold, iProp_unfold).
+Local Definition inG_fold {Σ A} {i : inG Σ A} :
+    inG_apply i (iPrePropO Σ) -n> inG_apply i (iPropO Σ) :=
+  rFunctor_map _ (iProp_unfold, iProp_fold).
+
+Local Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
+  discrete_fun_singleton (inG_id i)
+    {[ γ := inG_unfold (cmra_transport inG_prf a) ]}.
+Global Instance: Params (@iRes_singleton) 4 := {}.
+
+Local Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
+  uPred_ownM (iRes_singleton γ a).
+Local Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
+Definition own := own_aux.(unseal).
+Global Arguments own {Σ A _} γ a.
+Local Definition own_eq : @own = @own_def := own_aux.(seal_eq).
+Local Instance: Params (@own) 4 := {}.
+
+(** * Properties about ghost ownership *)
+Section global.
+Context `{i : !inG Σ A}.
+Implicit Types a : A.
+
+(** ** Properties of [iRes_singleton] *)
+Local Lemma inG_unfold_fold (x : inG_apply i (iPrePropO Σ)) :
+  inG_unfold (inG_fold x) ≡ x.
+Proof.
+  rewrite /inG_unfold /inG_fold -rFunctor_map_compose -{2}[x]rFunctor_map_id.
+  apply (ne_proper (rFunctor_map _)); split=> ?; apply iProp_unfold_fold.
+Qed.
+Local Lemma inG_fold_unfold (x : inG_apply i (iPropO Σ)) :
+  inG_fold (inG_unfold x) ≡ x.
+Proof.
+  rewrite /inG_unfold /inG_fold -rFunctor_map_compose -{2}[x]rFunctor_map_id.
+  apply (ne_proper (rFunctor_map _)); split=> ?; apply iProp_fold_unfold.
+Qed.
+Local Lemma inG_unfold_validN n (x : inG_apply i (iPropO Σ)) :
+  ✓{n} (inG_unfold x) ↔ ✓{n} x.
+Proof.
+  split; [|apply (cmra_morphism_validN _)].
+  move=> /(cmra_morphism_validN inG_fold). by rewrite inG_fold_unfold.
+Qed.
+
+Local Instance iRes_singleton_ne γ : NonExpansive (@iRes_singleton Σ A _ γ).
+Proof. by intros n a a' Ha; apply discrete_fun_singleton_ne; rewrite Ha. Qed.
+Local Lemma iRes_singleton_validI γ a : ✓ (iRes_singleton γ a) ⊢@{iPropI Σ} ✓ a.
+Proof.
+  rewrite /iRes_singleton.
+  rewrite discrete_fun_validI (forall_elim (inG_id i)) discrete_fun_lookup_singleton.
+  rewrite singleton_validI.
+  trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last by destruct inG_prf.
+  apply valid_entails=> n. apply inG_unfold_validN.
+Qed.
+Local Lemma iRes_singleton_op γ a1 a2 :
+  iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
+Proof.
+  rewrite /iRes_singleton discrete_fun_singleton_op singleton_op cmra_transport_op.
+  f_equiv. apply: singletonM_proper. apply (cmra_morphism_op _).
+Qed.
+
+Local Instance iRes_singleton_discrete γ a :
+  Discrete a → Discrete (iRes_singleton γ a).
+Proof.
+  intros ?. rewrite /iRes_singleton.
+  apply discrete_fun_singleton_discrete, gmap_singleton_discrete; [apply _|].
+  intros x Hx. assert (cmra_transport inG_prf a ≡ inG_fold x) as Ha.
+  { apply (discrete_0 _). by rewrite -Hx inG_fold_unfold. }
+  by rewrite Ha inG_unfold_fold.
+Qed.
+Local Instance iRes_singleton_core_id γ a :
+  CoreId a → CoreId (iRes_singleton γ a).
+Proof.
+  intros. apply discrete_fun_singleton_core_id, gmap_singleton_core_id.
+  by rewrite /CoreId -cmra_morphism_pcore core_id.
+Qed.
+
+Local Lemma later_internal_eq_iRes_singleton γ a r :
+  ▷ (r ≡ iRes_singleton γ a) ⊢@{iPropI Σ}
+  ◇ ∃ b r', r ≡ iRes_singleton γ b ⋅ r' ∧ ▷ (a ≡ b).
+Proof.
+  assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
+  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id i)). }
+  rewrite (f_equivI (λ r : iResUR Σ, r (inG_id i) !! γ) r).
+  rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton.
+  rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
+  { by rewrite /bi_except_0 -or_intro_l. }
+  rewrite -except_0_intro.
+  rewrite -(exist_intro (cmra_transport (eq_sym inG_prf) (inG_fold b))).
+  rewrite -(exist_intro (discrete_fun_insert (inG_id _) (delete γ (r (inG_id i))) r)).
+  apply and_intro.
+  - apply equiv_internal_eq. rewrite /iRes_singleton.
+    rewrite cmra_transport_trans eq_trans_sym_inv_l /=.
+    intros i'. rewrite discrete_fun_lookup_op.
+    destruct (decide (i' = inG_id i)) as [->|?].
+    + rewrite discrete_fun_lookup_insert discrete_fun_lookup_singleton.
+      intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
+      * by rewrite lookup_singleton lookup_delete Hb inG_unfold_fold.
+      * by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
+    + rewrite discrete_fun_lookup_insert_ne //.
+      by rewrite discrete_fun_lookup_singleton_ne // left_id.
+  - apply later_mono. rewrite (f_equivI inG_fold) inG_fold_unfold.
+    apply: (internal_eq_rewrite' _ _ (λ b, a ≡ cmra_transport (eq_sym inG_prf) b)%I);
+      [solve_proper|apply internal_eq_sym|].
+    rewrite cmra_transport_trans eq_trans_sym_inv_r /=. apply internal_eq_refl.
+Qed.
+
+(** ** Properties of [own] *)
+Global Instance own_ne γ : NonExpansive (@own Σ A _ γ).
+Proof. rewrite !own_eq. solve_proper. Qed.
+Global Instance own_proper γ :
+  Proper ((≡) ==> (⊣⊢)) (@own Σ A _ γ) := ne_proper _.
+
+Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ∗ own γ a2.
+Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
+Lemma own_mono γ a1 a2 : a2 ≼ a1 → own γ a1 ⊢ own γ a2.
+Proof. move=> [c ->]. by rewrite own_op sep_elim_l. Qed.
+
+Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
+Proof. intros a1 a2. apply own_mono. Qed.
+
+Lemma own_valid γ a : own γ a ⊢ ✓ a.
+Proof. by rewrite !own_eq /own_def ownM_valid iRes_singleton_validI. Qed.
+Lemma own_valid_2 γ a1 a2 : own γ a1 -∗ own γ a2 -∗ ✓ (a1 ⋅ a2).
+Proof. apply entails_wand, wand_intro_r. by rewrite -own_op own_valid. Qed.
+Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
+Proof. apply entails_wand. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
+Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
+Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
+Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
+Proof. by rewrite comm -own_valid_r. Qed.
+
+Global Instance own_timeless γ a : Discrete a → Timeless (own γ a).
+Proof. rewrite !own_eq /own_def. apply _. Qed.
+Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
+Proof. rewrite !own_eq /own_def; apply _. Qed.
+
+Lemma later_own γ a : ▷ own γ a ⊢ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
+Proof.
+  rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
+  assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
+  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id i)). }
+  rewrite internal_eq_sym later_internal_eq_iRes_singleton.
+  rewrite (except_0_intro (uPred_ownM r)) -except_0_and. f_equiv.
+  rewrite and_exist_l. f_equiv=> b. rewrite and_exist_l. apply exist_elim=> r'.
+  rewrite assoc. apply and_mono_l.
+  etrans; [|apply ownM_mono, (cmra_included_l _ r')].
+  eapply (internal_eq_rewrite' _ _ uPred_ownM _); [apply and_elim_r|].
+  apply and_elim_l.
+Qed.
+
+(** ** Allocation *)
+(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
+   assertion. However, the map_updateP_alloc does not suffice to show this. *)
+Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
+  pred_infinite P →
+  (∀ γ, P γ → ✓ (f γ)) →
+  ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ (f γ).
+Proof.
+  intros HPinf Hf.
+  rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ (f γ)⌝ ∧ uPred_ownM m)%I).
+  - rewrite /bi_emp_valid (ownM_unit emp).
+    apply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty _ (λ m, ∃ γ,
+      m = {[ γ := inG_unfold (cmra_transport inG_prf (f γ)) ]} ∧ P γ));
+      [|naive_solver].
+    apply (alloc_updateP_strong_dep _ P _ (λ γ,
+      inG_unfold (cmra_transport inG_prf (f γ)))); [done| |naive_solver].
+    intros γ _ ?.
+    by apply (cmra_morphism_valid inG_unfold), cmra_transport_valid, Hf.
+  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
+    by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
+Qed.
+Lemma own_alloc_cofinite_dep (f : gname → A) (G : gset gname) :
+  (∀ γ, γ ∉ G → ✓ (f γ)) → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ (f γ).
+Proof.
+  intros Ha.
+  apply (own_alloc_strong_dep f (λ γ, γ ∉ G))=> //.
+  apply (pred_infinite_set (C:=gset gname)).
+  intros E. set (γ := fresh (G ∪ E)).
+  exists γ. apply not_elem_of_union, is_fresh.
+Qed.
+Lemma own_alloc_dep (f : gname → A) :
+  (∀ γ, ✓ (f γ)) → ⊢ |==> ∃ γ, own γ (f γ).
+Proof.
+  intros Ha. rewrite /bi_emp_valid (own_alloc_cofinite_dep f ∅) //; [].
+  apply bupd_mono, exist_mono=>?. apply: sep_elim_r.
+Qed.
+
+Lemma own_alloc_strong a (P : gname → Prop) :
+  pred_infinite P →
+  ✓ a → ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ a.
+Proof. intros HP Ha. eapply (own_alloc_strong_dep (λ _, a)); eauto. Qed.
+Lemma own_alloc_cofinite a (G : gset gname) :
+  ✓ a → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ a.
+Proof. intros Ha. eapply (own_alloc_cofinite_dep (λ _, a)); eauto. Qed.
+Lemma own_alloc a : ✓ a → ⊢ |==> ∃ γ, own γ a.
+Proof. intros Ha. eapply (own_alloc_dep (λ _, a)); eauto. Qed.
+
+(** ** Frame preserving updates *)
+Lemma own_updateP P γ a : a ~~>: P → own γ a ⊢ |==> ∃ a', ⌜P a'⌝ ∗ own γ a'.
+Proof.
+  intros Hupd. rewrite !own_eq.
+  rewrite -(bupd_mono (∃ m,
+    ⌜ ∃ a', m = iRes_singleton γ a' ∧ P a' ⌝ ∧ uPred_ownM m)%I).
+  - apply bupd_ownM_updateP, (discrete_fun_singleton_updateP _ (λ m, ∃ x,
+      m = {[ γ := x ]} ∧ ∃ x',
+      x = inG_unfold x' ∧ ∃ a',
+      x' = cmra_transport inG_prf a' ∧ P a')); [|naive_solver].
+    apply singleton_updateP', (iso_cmra_updateP' inG_fold).
+    { apply inG_unfold_fold. }
+    { apply (cmra_morphism_op _). }
+    { apply inG_unfold_validN. }
+    by apply cmra_transport_updateP'.
+  - apply exist_elim=> m; apply pure_elim_l=> -[a' [-> HP]].
+    rewrite -(exist_intro a'). rewrite -persistent_and_sep.
+    by apply and_intro; [apply pure_intro|].
+Qed.
+
+Lemma own_update γ a a' : a ~~> a' → own γ a ⊢ |==> own γ a'.
+Proof.
+  intros. iIntros "?".
+  iMod (own_updateP (a' =.) with "[$]") as (a'') "[-> $]".
+  { by apply cmra_update_updateP. }
+  done.
+Qed.
+Lemma own_update_2 γ a1 a2 a' :
+  a1 ⋅ a2 ~~> a' → own γ a1 -∗ own γ a2 ==∗ own γ a'.
+Proof. intros. apply entails_wand, wand_intro_r. rewrite -own_op. by iApply own_update. Qed.
+Lemma own_update_3 γ a1 a2 a3 a' :
+  a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 -∗ own γ a2 -∗ own γ a3 ==∗ own γ a'.
+Proof. intros. apply entails_wand. do 2 apply wand_intro_r. rewrite -!own_op. by iApply own_update. Qed.
+End global.
+
+Global Arguments own_valid {_ _} [_] _ _.
+Global Arguments own_valid_2 {_ _} [_] _ _ _.
+Global Arguments own_valid_3 {_ _} [_] _ _ _ _.
+Global Arguments own_valid_l {_ _} [_] _ _.
+Global Arguments own_valid_r {_ _} [_] _ _.
+Global Arguments own_updateP {_ _} [_] _ _ _ _.
+Global Arguments own_update {_ _} [_] _ _ _ _.
+Global Arguments own_update_2 {_ _} [_] _ _ _ _ _.
+Global Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
+
+Lemma own_unit A `{i : !inG Σ (A:ucmra)} γ : ⊢ |==> own γ (ε:A).
+Proof.
+  rewrite /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
+  apply bupd_ownM_update, discrete_fun_singleton_update_empty.
+  apply (alloc_unit_singleton_update (inG_unfold (cmra_transport inG_prf ε))).
+  - apply (cmra_morphism_valid _), cmra_transport_valid, ucmra_unit_valid.
+  - intros x. rewrite -(inG_unfold_fold x) -(cmra_morphism_op inG_unfold).
+    f_equiv. generalize (inG_fold x)=> x'.
+    destruct inG_prf=> /=. by rewrite left_id.
+  - done.
+Qed.
+
+(** Big op class instances *)
+Section big_op_instances.
+  Context `{!inG Σ (A:ucmra)}.
+
+  Global Instance own_cmra_sep_homomorphism γ :
+    WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
+  Proof. split; try apply _. apply own_op. Qed.
+
+  Lemma big_opL_own {B} γ (f : nat → B → A) (l : list B) :
+    l ≠ [] →
+    own γ ([^op list] k↦x ∈ l, f k x) ⊣⊢ [∗ list] k↦x ∈ l, own γ (f k x).
+  Proof. apply (big_opL_commute1 _). Qed.
+  Lemma big_opM_own `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) :
+    m ≠ ∅ →
+    own γ ([^op map] k↦x ∈ m, g k x) ⊣⊢ [∗ map] k↦x ∈ m, own γ (g k x).
+  Proof. apply (big_opM_commute1 _). Qed.
+  Lemma big_opS_own `{Countable B} γ (g : B → A) (X : gset B) :
+    X ≠ ∅ →
+    own γ ([^op set] x ∈ X, g x) ⊣⊢ [∗ set] x ∈ X, own γ (g x).
+  Proof. apply (big_opS_commute1 _). Qed.
+  Lemma big_opMS_own `{Countable B} γ (g : B → A) (X : gmultiset B) :
+    X ≠ ∅ →
+    own γ ([^op mset] x ∈ X, g x) ⊣⊢ [∗ mset] x ∈ X, own γ (g x).
+  Proof. apply (big_opMS_commute1 _). Qed.
+
+  Global Instance own_cmra_sep_entails_homomorphism γ :
+    MonoidHomomorphism op uPred_sep (⊢) (own γ).
+  Proof.
+    split; [split|]; try apply _.
+    - intros. by rewrite own_op.
+    - apply (affine _).
+  Qed.
+
+  Lemma big_opL_own_1 {B} γ (f : nat → B → A) (l : list B) :
+    own γ ([^op list] k↦x ∈ l, f k x) ⊢ [∗ list] k↦x ∈ l, own γ (f k x).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma big_opM_own_1 `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) :
+    own γ ([^op map] k↦x ∈ m, g k x) ⊢ [∗ map] k↦x ∈ m, own γ (g k x).
+  Proof. apply (big_opM_commute _). Qed.
+  Lemma big_opS_own_1 `{Countable B} γ (g : B → A) (X : gset B) :
+    own γ ([^op set] x ∈ X, g x) ⊢ [∗ set] x ∈ X, own γ (g x).
+  Proof. apply (big_opS_commute _). Qed.
+  Lemma big_opMS_own_1 `{Countable B} γ (g : B → A) (X : gmultiset B) :
+    own γ ([^op mset] x ∈ X, g x) ⊢ [∗ mset] x ∈ X, own γ (g x).
+  Proof. apply (big_opMS_commute _). Qed.
+End big_op_instances.
+
+(** Proofmode class instances *)
+Section proofmode_instances.
+  Context `{!inG Σ A}.
+  Implicit Types a b : A.
+
+  Global Instance into_sep_own γ a b1 b2 :
+    IsOp a b1 b2 → IntoSep (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. by rewrite /IntoSep (is_op a) own_op. Qed.
+  Global Instance into_and_own p γ a b1 b2 :
+    IsOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. by rewrite /IntoAnd (is_op a) own_op sep_and. Qed.
+
+  Global Instance from_sep_own γ a b1 b2 :
+    IsOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. by rewrite /FromSep -own_op -is_op. Qed.
+  (* TODO: Improve this instance with generic own simplification machinery
+  once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  (* Cost > 50 to give priority to [combine_sep_as_fractional]. *)
+  Global Instance combine_sep_as_own γ a b1 b2 :
+    IsOp a b1 b2 → CombineSepAs (own γ b1) (own γ b2) (own γ a) | 60.
+  Proof. intros. by rewrite /CombineSepAs -own_op -is_op. Qed.
+  (* TODO: Improve this instance with generic own validity simplification
+  machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  Global Instance combine_sep_gives_own γ b1 b2 :
+    CombineSepGives (own γ b1) (own γ b2) (✓ (b1 ⋅ b2)).
+  Proof.
+    intros. rewrite /CombineSepGives -own_op own_valid.
+    by apply: bi.persistently_intro.
+  Qed.
+  Global Instance from_and_own_persistent γ a b1 b2 :
+    IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
+    FromAnd (own γ a) (own γ b1) (own γ b2).
+  Proof.
+    intros ? Hb. rewrite /FromAnd (is_op a) own_op.
+    destruct Hb; by rewrite persistent_and_sep.
+  Qed.
+End proofmode_instances.
+
+Section own_forall.
+  Context `{i : !inG Σ A}.
+  Implicit Types a c : A.
+  Implicit Types x z : iResUR Σ.
+
+  (** Our main goal in this section is to prove [own_forall]:
+
+    (∀ b, own γ (f b)) ⊢ ∃ c : A, own γ c ∗ (∀ b, Some (f b) ≼ Some c)
+
+  We have the analogue in the global ucmra, from [ownM_forall]:
+
+    (∀ a, uPred_ownM (f a)) ⊢ ∃ z : iRes Σ, uPred_ownM z ∧ (∀ a, f a ≼ z)
+
+  We need to relate [uPred_ownM (iRes_singleton γ _)] to [own γ _] so that we
+  can bring this theorem from the global ucmra world to the [A] world.
+  In particular, [ownM_forall] gives us some [z] in the ucmra world, but to prove
+  the theorem in the end, we need to supply a witness [z'] in the [A] world.
+  We start by defining the [iRes_project] function to map from the ucmra world
+  to the [A] world, basically an inverse of [iRes_singleton]: *)
+
+  Local Definition iRes_project (γ : gname) (x : iResUR Σ) : option A :=
+    cmra_transport (eq_sym inG_prf) ∘ inG_fold <$> x (inG_id i) !! γ.
+
+  (* Now we prove some properties about [iRes_project] *)
+  Local Lemma iRes_project_op γ x y :
+    iRes_project γ (x ⋅ y) ≡@{option A} iRes_project γ x ⋅ iRes_project γ y.
+  Proof.
+    rewrite /iRes_project lookup_op.
+    case: (x (inG_id i) !! γ)=> [x1|]; case: (y (inG_id i) !! γ)=> [y1|] //=.
+    rewrite -Some_op -cmra_transport_op. do 2 f_equiv. apply: cmra_morphism_op.
+  Qed.
+
+  Local Instance iRes_project_ne γ : NonExpansive (iRes_project γ).
+  Proof. intros n x1 x2 Hx. rewrite /iRes_project. do 2 f_equiv. apply Hx. Qed.
+
+  Local Lemma iRes_project_singleton γ a :
+    iRes_project γ (iRes_singleton γ a) ≡ Some a.
+  Proof.
+    rewrite /iRes_project /iRes_singleton discrete_fun_lookup_singleton.
+    rewrite lookup_singleton /= inG_fold_unfold.
+    by rewrite cmra_transport_trans eq_trans_sym_inv_r.
+  Qed.
+
+  (** The singleton result [c] of [iRes_project γ z] is below [z] *)
+  Local Lemma iRes_project_below γ z c :
+    iRes_project γ z = Some c → iRes_singleton γ c ≼ z.
+  Proof.
+    rewrite /iRes_project /iRes_singleton fmap_Some.
+    intros (a' & Hγ & ->). rewrite cmra_transport_trans eq_trans_sym_inv_l /=.
+    exists (discrete_fun_insert (inG_id i) (delete γ (z (inG_id i))) z).
+    intros j. rewrite discrete_fun_lookup_op.
+    destruct (decide (j = inG_id i)) as [->|]; last first.
+    { rewrite discrete_fun_lookup_singleton_ne //.
+      rewrite discrete_fun_lookup_insert_ne //. by rewrite left_id. }
+    rewrite discrete_fun_lookup_singleton discrete_fun_lookup_insert.
+    intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|].
+    - by rewrite lookup_singleton lookup_delete Hγ inG_unfold_fold.
+    - by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
+  Qed.
+
+  (** If another singleton [c] is below [z], [iRes_project] is above [c]. *)
+  Local Lemma iRes_project_above γ z c :
+    iRes_singleton γ c ≼ z ⊢@{iProp Σ} Some c ≼ iRes_project γ z.
+  Proof.
+    iIntros "#[%x Hincl]". iExists (iRes_project γ x).
+    rewrite -(iRes_project_singleton γ) -iRes_project_op.
+    by iRewrite "Hincl".
+  Qed.
+
+  (** Finally we tie it all together.
+  As usual, we use [Some a ≼ Some c] for the reflexive closure of [a ≼ c]. *)
+  Lemma own_forall `{!Inhabited B} γ (f : B → A) :
+    (∀ b, own γ (f b)) ⊢ ∃ c, own γ c ∗ (∀ b, Some (f b) ≼ Some c).
+  Proof.
+    rewrite own_eq /own_def. iIntros "Hown".
+    iDestruct (ownM_forall with "Hown") as (z) "[Hown Hincl]".
+    destruct (iRes_project γ z) as [c|] eqn:Hc.
+    - iExists c. iSplitL "Hown".
+      { iApply (ownM_mono with "Hown"). by apply iRes_project_below. }
+      iIntros (b). rewrite -Hc. by iApply iRes_project_above.
+    - iDestruct ("Hincl" $! inhabitant) as "Hincl".
+      iDestruct (iRes_project_above with "Hincl") as "Hincl".
+      rewrite Hc. iDestruct "Hincl" as (mx) "H".
+      rewrite option_equivI. by destruct mx.
+  Qed.
+
+  (** Now some corollaries. *)
+  Lemma own_forall_total `{!CmraTotal A, !Inhabited B} γ (f : B → A) :
+    (∀ b, own γ (f b)) ⊢ ∃ c, own γ c ∗ (∀ b, f b ≼ c).
+  Proof. setoid_rewrite <-Some_included_totalI. apply own_forall. Qed.
+
+  Lemma own_and γ a1 a2 :
+    own γ a1 ∧ own γ a2 ⊢ ∃ c, own γ c ∗ Some a1 ≼ Some c ∗ Some a2 ≼ Some c.
+  Proof.
+    iIntros "Hown". iDestruct (own_forall γ (λ b, if b : bool then a1 else a2)
+      with "[Hown]") as (c) "[$ Hincl]".
+    { rewrite and_alt.
+      iIntros ([]); [iApply ("Hown" $! true)|iApply ("Hown" $! false)]. }
+    iSplit; [iApply ("Hincl" $! true)|iApply ("Hincl" $! false)].
+  Qed.
+  Lemma own_and_total `{!CmraTotal A} γ a1 a2 :
+    own γ a1 ∧ own γ a2 ⊢ ∃ c, own γ c ∗ a1 ≼ c ∗ a2 ≼ c.
+  Proof. setoid_rewrite <-Some_included_totalI. apply own_and. Qed.
+
+  (** A version of [own_forall] for bounded quantification. Here [φ : B → Prop]
+  is a pure predicate that restricts the elements of [B]. *)
+  Lemma own_forall_pred {B} γ (φ : B → Prop) (f : B → A) :
+    (∃ b, φ b) → (* [φ] is non-empty *)
+    (∀ b, ⌜ φ b ⌝ -∗ own γ (f b)) ⊢
+    ∃ c, own γ c ∗ (∀ b, ⌜ φ b ⌝ -∗ Some (f b) ≼ Some c).
+  Proof.
+    iIntros ([b0 pb0]) "Hown".
+    iAssert (∀ b : { b | φ b }, own γ (f (`b)))%I with "[Hown]" as "Hown".
+    { iIntros ([b pb]). by iApply ("Hown" $! b). }
+    iDestruct (@own_forall _ with "Hown") as (c) "[$ Hincl]".
+    { split. apply (b0 ↾ pb0). }
+    iIntros (b pb). iApply ("Hincl" $! (b ↾ pb)).
+  Qed.
+  Lemma own_forall_pred_total `{!CmraTotal A} {B} γ (φ : B → Prop) (f : B → A) :
+    (∃ b, φ b) →
+    (∀ b, ⌜ φ b ⌝ -∗ own γ (f b)) ⊢ ∃ c, own γ c ∗ (∀ b, ⌜ φ b ⌝ -∗ f b ≼ c).
+  Proof. setoid_rewrite <-Some_included_totalI. apply own_forall_pred. Qed.
+
+  Lemma own_and_discrete_total `{!CmraDiscrete A, !CmraTotal A} γ a1 a2 c :
+    (∀ c', ✓ c' → a1 ≼ c' → a2 ≼ c' → c ≼ c') →
+    own γ a1 ∧ own γ a2 ⊢ own γ c.
+  Proof.
+    iIntros (Hvalid) "Hown".
+    iDestruct (own_and_total with "Hown") as (c') "[Hown [%Ha1 %Ha2]]".
+    iDestruct (own_valid with "Hown") as %?.
+    iApply (own_mono with "Hown"); eauto.
+  Qed.
+  Lemma own_and_discrete_total_False `{!CmraDiscrete A, !CmraTotal A} γ a1 a2 :
+    (∀ c', ✓ c' → a1 ≼ c' → a2 ≼ c' → False) →
+    own γ a1 ∧ own γ a2 ⊢ False.
+  Proof.
+    iIntros (Hvalid) "Hown".
+    iDestruct (own_and_total with "Hown") as (c) "[Hown [%Ha1 %Ha2]]".
+    iDestruct (own_valid with "Hown") as %?; eauto.
+  Qed.
+End own_forall.

iris/base_logic/lib/proph_map.v

+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import ghost_map.
+From iris.prelude Require Import options.
+Import uPred.
+
+Local Notation proph_map P V := (gmap P (list V)).
+Definition proph_val_list (P V : Type) := list (P * V).
+
+(** The CMRA we need. *)
+Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
+  #[local] proph_map_GpreS_inG :: ghost_mapG Σ P (list V)
+}.
+
+Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
+  #[local] proph_map_inG :: proph_mapGpreS P V Σ;
+  proph_map_name : gname
+}.
+Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
+
+Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
+  #[ghost_mapΣ P (list V)].
+
+Global Instance subG_proph_mapGpreS {Σ P V} `{Countable P} :
+  subG (proph_mapΣ P V) Σ → proph_mapGpreS P V Σ.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context `{pG : proph_mapGS P V Σ}.
+  Implicit Types pvs : proph_val_list P V.
+  Implicit Types R : proph_map P V.
+  Implicit Types p : P.
+
+  (** The list of resolves for [p] in [pvs]. *)
+  Fixpoint proph_list_resolves pvs p : list V :=
+    match pvs with
+    | []         => []
+    | (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
+                    else proph_list_resolves pvs p
+    end.
+
+  Definition proph_resolves_in_list R pvs :=
+    map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
+
+  Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
+    ∃ R, ⌜proph_resolves_in_list R pvs ∧
+         dom R ⊆ ps⌝ ∗ ghost_map_auth (proph_map_name pG) 1 R.
+
+  Local Definition proph_def (p : P) (vs : list V) : iProp Σ :=
+    p ↪[proph_map_name pG] vs.
+  Local Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
+  Definition proph := proph_aux.(unseal).
+  Local Definition proph_unseal : @proph = @proph_def := proph_aux.(seal_eq).
+End definitions.
+
+Section list_resolves.
+  Context {P V : Type} `{Countable P}.
+  Implicit Type pvs : proph_val_list P V.
+  Implicit Type p : P.
+  Implicit Type R : proph_map P V.
+
+  Lemma resolves_insert pvs p R :
+    proph_resolves_in_list R pvs →
+    p ∉ dom R →
+    proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
+  Proof.
+    intros Hinlist Hp q vs HEq.
+    destruct (decide (p = q)) as [->|NEq].
+    - rewrite lookup_insert in HEq. by inversion HEq.
+    - rewrite lookup_insert_ne in HEq; last done. by apply Hinlist.
+  Qed.
+End list_resolves.
+
+Lemma proph_map_init `{Countable P, !proph_mapGpreS P V Σ} pvs ps :
+  ⊢ |==> ∃ _ : proph_mapGS P V Σ, proph_map_interp pvs ps.
+Proof.
+  iMod (ghost_map_alloc_empty) as (γ) "Hh".
+  iModIntro. iExists (ProphMapGS P V _ _ _ _ γ), ∅. iSplit; last by iFrame.
+  iPureIntro. done.
+Qed.
+
+Section proph_map.
+  Context `{proph_mapGS P V Σ}.
+  Implicit Types p : P.
+  Implicit Types v : V.
+  Implicit Types vs : list V.
+  Implicit Types R : proph_map P V.
+  Implicit Types ps : gset P.
+
+  (** General properties of pointsto *)
+  Global Instance proph_timeless p vs : Timeless (proph p vs).
+  Proof. rewrite proph_unseal /proph_def. apply _. Qed.
+
+  Lemma proph_exclusive p vs1 vs2 :
+    proph p vs1 -∗ proph p vs2 -∗ False.
+  Proof.
+    rewrite proph_unseal /proph_def. iIntros "Hp1 Hp2".
+    by iDestruct (ghost_map_elem_ne with "Hp1 Hp2") as %?.
+  Qed.
+
+  Lemma proph_map_new_proph p ps pvs :
+    p ∉ ps →
+    proph_map_interp pvs ps ==∗
+    proph_map_interp pvs ({[p]} ∪ ps) ∗ proph p (proph_list_resolves pvs p).
+  Proof.
+    iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
+    rewrite proph_unseal /proph_def.
+    iMod (ghost_map_insert p (proph_list_resolves pvs p) with "H●") as "[H● H◯]".
+    { apply not_elem_of_dom. set_solver. }
+    iFrame. iPureIntro. split.
+    - apply resolves_insert; first done. set_solver.
+    - rewrite dom_insert. set_solver.
+  Qed.
+
+  Lemma proph_map_resolve_proph p v pvs ps vs :
+    proph_map_interp ((p,v) :: pvs) ps ∗ proph p vs ==∗
+    ∃vs', ⌜vs = v::vs'⌝ ∗ proph_map_interp pvs ps ∗ proph p vs'.
+  Proof.
+    iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
+    rewrite /proph_map_interp proph_unseal /proph_def.
+    iCombine "H● Hp" gives %HR.
+    assert (vs = v :: proph_list_resolves pvs p) as ->.
+    { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
+    iMod (ghost_map_update (proph_list_resolves pvs p) with "H● Hp") as "[H● H◯]".
+    iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
+    - iPureIntro. done.
+    - iPureIntro. split.
+      + intros q ws HEq. destruct (decide (p = q)) as [<-|NEq].
+        * rewrite lookup_insert in HEq. by inversion HEq.
+        * rewrite lookup_insert_ne in HEq; last done.
+          rewrite (Hres q ws HEq).
+          simpl. rewrite decide_False; done.
+      + assert (p ∈ dom R) by exact: elem_of_dom_2.
+        rewrite dom_insert. set_solver.
+  Qed.
+End proph_map.

iris/base_logic/lib/saved_prop.v

+From stdpp Require Import gmap.
+From iris.algebra Require Import dfrac_agree.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic Require Export own.
+From iris.bi Require Import fractional.
+From iris.prelude Require Import options.
+Import uPred.
+
+(* "Saved anything" -- this can give you saved propositions, saved predicates,
+   saved whatever-you-like. *)
+
+Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
+  #[local] saved_anything_inG :: inG Σ (dfrac_agreeR (oFunctor_apply F (iPropO Σ)));
+  saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
+}.
+
+Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
+  #[ GFunctor (dfrac_agreeRF F) ].
+
+Global Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
+  subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
+Proof. solve_inG. Qed.
+
+Definition saved_anything_own `{!savedAnythingG Σ F}
+    (γ : gname) (dq : dfrac) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
+  own γ (to_dfrac_agree dq x).
+Global Typeclasses Opaque saved_anything_own.
+Global Instance: Params (@saved_anything_own) 4 := {}.
+
+Section saved_anything.
+  Context `{!savedAnythingG Σ F}.
+  Implicit Types x y : oFunctor_apply F (iPropO Σ).
+  Implicit Types (γ : gname) (dq : dfrac).
+
+  Global Instance saved_anything_discarded_persistent γ x :
+    Persistent (saved_anything_own γ DfracDiscarded x).
+  Proof. rewrite /saved_anything_own; apply _. Qed.
+
+  Global Instance saved_anything_ne γ dq : NonExpansive (saved_anything_own γ dq).
+  Proof. solve_proper. Qed.
+  Global Instance saved_anything_proper γ dq : Proper ((≡) ==> (≡)) (saved_anything_own γ dq).
+  Proof. solve_proper. Qed.
+
+  Global Instance saved_anything_fractional γ x : Fractional (λ q, saved_anything_own γ (DfracOwn q) x).
+  Proof. intros q1 q2. rewrite /saved_anything_own -own_op -dfrac_agree_op //. Qed.
+  Global Instance saved_anything_as_fractional γ x q :
+    AsFractional (saved_anything_own γ (DfracOwn q) x) (λ q, saved_anything_own γ (DfracOwn q) x) q.
+  Proof. split; [done|]. apply _. Qed.
+
+  (** Allocation *)
+  Lemma saved_anything_alloc_strong x (I : gname → Prop) dq :
+    ✓ dq →
+    pred_infinite I →
+    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_anything_own γ dq x.
+  Proof. intros ??. by apply own_alloc_strong. Qed.
+
+  Lemma saved_anything_alloc_cofinite x (G : gset gname) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_anything_own γ dq x.
+  Proof. intros ?. by apply own_alloc_cofinite. Qed.
+
+  Lemma saved_anything_alloc x dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, saved_anything_own γ dq x.
+  Proof. intros ?. by apply own_alloc. Qed.
+
+  (** Validity *)
+  Lemma saved_anything_valid γ dq x :
+    saved_anything_own γ dq x -∗ ⌜✓ dq⌝.
+  Proof.
+    rewrite /saved_anything_own own_valid dfrac_agree_validI //. eauto.
+  Qed.
+  Lemma saved_anything_valid_2 γ dq1 dq2 x y :
+    saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ x ≡ y.
+  Proof.
+    iIntros "Hx Hy". rewrite /saved_anything_own.
+    iCombine "Hx Hy" gives "Hv".
+    rewrite dfrac_agree_validI_2. iDestruct "Hv" as "[$ $]".
+  Qed.
+  Lemma saved_anything_agree γ dq1 dq2 x y :
+    saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ x ≡ y.
+  Proof. iIntros "Hx Hy". iPoseProof (saved_anything_valid_2 with "Hx Hy") as "[_ $]". Qed.
+
+  Global Instance saved_anything_combine_gives γ dq1 dq2 x y :
+    CombineSepGives (saved_anything_own γ dq1 x) (saved_anything_own γ dq2 y)
+      (⌜✓ (dq1 ⋅ dq2)⌝ ∗ x ≡ y).
+  Proof.
+    rewrite /CombineSepGives. iIntros "[Hx Hy]".
+    iPoseProof (saved_anything_valid_2 with "Hx Hy") as "[% #$]". eauto.
+  Qed.
+
+  Global Instance saved_anything_combine_as γ dq1 dq2 x y :
+    CombineSepAs (saved_anything_own γ dq1 x) (saved_anything_own γ dq2 y)
+      (saved_anything_own γ (dq1 ⋅ dq2) x).
+  (* higher cost than the Fractional instance, which kicks in for #qs *)
+  Proof.
+    rewrite /CombineSepAs. iIntros "[Hx Hy]".
+    iCombine "Hx Hy" gives "[_ #H]".
+    iRewrite -"H" in "Hy". rewrite /saved_anything_own.
+    iCombine "Hx Hy" as "Hxy". by rewrite -dfrac_agree_op.
+  Qed.
+
+  (** Make an element read-only. *)
+  Lemma saved_anything_persist γ dq v :
+    saved_anything_own γ dq v ==∗ saved_anything_own γ DfracDiscarded v.
+  Proof.
+    iApply own_update. apply dfrac_agree_persist.
+  Qed.
+
+  (** Recover fractional ownership for read-only element. *)
+  Lemma saved_anything_unpersist γ v :
+    saved_anything_own γ DfracDiscarded v ==∗ ∃ q, saved_anything_own γ (DfracOwn q) v.
+  Proof.
+    iIntros "H".
+    iMod (own_updateP with "H") as "H";
+      first by apply dfrac_agree_unpersist.
+    iDestruct "H" as (? (q&->)) "H".
+    iIntros "!>". iExists q. done.
+  Qed.
+
+  (** Updates *)
+  Lemma saved_anything_update y γ x :
+    saved_anything_own γ (DfracOwn 1) x ==∗ saved_anything_own γ (DfracOwn 1) y.
+  Proof.
+    iApply own_update. apply cmra_update_exclusive. done.
+  Qed.
+  Lemma saved_anything_update_2 y γ q1 q2 x1 x2 :
+    (q1 + q2 = 1)%Qp →
+    saved_anything_own γ (DfracOwn q1) x1 -∗ saved_anything_own γ (DfracOwn q2) x2 ==∗
+    saved_anything_own γ (DfracOwn q1) y ∗ saved_anything_own γ (DfracOwn q2) y.
+  Proof.
+    intros Hq. rewrite -own_op. iApply own_update_2.
+    apply dfrac_agree_update_2.
+    rewrite dfrac_op_own Hq //.
+  Qed.
+  Lemma saved_anything_update_halves y γ x1 x2 :
+    saved_anything_own γ (DfracOwn (1/2)) x1 -∗
+    saved_anything_own γ (DfracOwn (1/2)) x2 ==∗
+    saved_anything_own γ (DfracOwn (1/2)) y ∗ saved_anything_own γ (DfracOwn (1/2)) y.
+  Proof. iApply saved_anything_update_2. apply Qp.half_half. Qed.
+End saved_anything.
+
+(** Provide specialized versions of this for convenience. **)
+
+(* Saved propositions. *)
+Notation savedPropG Σ := (savedAnythingG Σ (▶ ∙)).
+Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
+
+Section saved_prop.
+  Context `{!savedPropG Σ}.
+
+  Definition saved_prop_own (γ : gname) (dq : dfrac) (P: iProp Σ) :=
+    saved_anything_own (F := ▶ ∙) γ dq (Next P).
+
+  Global Instance saved_prop_own_contractive γ dq :
+    Contractive (saved_prop_own γ dq).
+  Proof. solve_contractive. Qed.
+
+  Global Instance saved_prop_discarded_persistent γ P :
+    Persistent (saved_prop_own γ DfracDiscarded P).
+  Proof. apply _. Qed.
+
+  Global Instance saved_prop_fractional γ P : Fractional (λ q, saved_prop_own γ (DfracOwn q) P).
+  Proof. apply _. Qed.
+  Global Instance saved_prop_as_fractional γ P q :
+    AsFractional (saved_prop_own γ (DfracOwn q) P) (λ q, saved_prop_own γ (DfracOwn q) P) q.
+  Proof. apply _. Qed.
+
+  (** Allocation *)
+  Lemma saved_prop_alloc_strong (I : gname → Prop) (P: iProp Σ) dq :
+    ✓ dq →
+    pred_infinite I →
+    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_prop_own γ dq P.
+  Proof. intros ??. by apply saved_anything_alloc_strong. Qed.
+
+  Lemma saved_prop_alloc_cofinite (G : gset gname) (P: iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_prop_own γ dq P.
+  Proof. by apply saved_anything_alloc_cofinite. Qed.
+
+  Lemma saved_prop_alloc (P : iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, saved_prop_own γ dq P.
+  Proof. apply saved_anything_alloc. Qed.
+
+  (** Validity *)
+  Lemma saved_prop_valid γ dq P :
+    saved_prop_own γ dq P -∗ ⌜✓ dq⌝.
+  Proof. apply saved_anything_valid. Qed.
+  Lemma saved_prop_valid_2 γ dq1 dq2 P Q :
+    saved_prop_own γ dq1 P -∗ saved_prop_own γ dq2 Q -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (P ≡ Q).
+  Proof.
+    iIntros "HP HQ".
+    iCombine "HP HQ" gives "($ & Hag)".
+    by iApply later_equivI.
+  Qed.
+  Lemma saved_prop_agree γ dq1 dq2 P Q :
+    saved_prop_own γ dq1 P -∗ saved_prop_own γ dq2 Q -∗ ▷ (P ≡ Q).
+  Proof. iIntros "HP HQ". iCombine "HP" "HQ" gives "[_ $]". Qed.
+
+  (** Make an element read-only. *)
+  Lemma saved_prop_persist γ dq P :
+    saved_prop_own γ dq P ==∗ saved_prop_own γ DfracDiscarded P.
+  Proof. apply saved_anything_persist. Qed.
+
+  (** Recover fractional ownership for read-only element. *)
+  Lemma saved_prop_unpersist γ v :
+    saved_prop_own γ DfracDiscarded v ==∗ ∃ q, saved_prop_own γ (DfracOwn q) v.
+  Proof. apply saved_anything_unpersist. Qed.
+
+  (** Updates *)
+  Lemma saved_prop_update Q γ P :
+    saved_prop_own γ (DfracOwn 1) P ==∗ saved_prop_own γ (DfracOwn 1) Q.
+  Proof. apply saved_anything_update. Qed.
+  Lemma saved_prop_update_2 Q γ q1 q2 P1 P2 :
+    (q1 + q2 = 1)%Qp →
+    saved_prop_own γ (DfracOwn q1) P1 -∗ saved_prop_own γ (DfracOwn q2) P2 ==∗
+    saved_prop_own γ (DfracOwn q1) Q ∗ saved_prop_own γ (DfracOwn q2) Q.
+  Proof. apply saved_anything_update_2. Qed.
+  Lemma saved_prop_update_halves Q γ P1 P2 :
+    saved_prop_own γ (DfracOwn (1/2)) P1 -∗
+    saved_prop_own γ (DfracOwn (1/2)) P2 ==∗
+    saved_prop_own γ (DfracOwn (1/2)) Q ∗ saved_prop_own γ (DfracOwn (1/2)) Q.
+  Proof. apply saved_anything_update_halves. Qed.
+End saved_prop.
+
+(* Saved predicates. *)
+Notation savedPredG Σ A := (savedAnythingG Σ (A -d> ▶ ∙)).
+Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ ∙)).
+
+Section saved_pred.
+  Context `{!savedPredG Σ A}.
+
+  Definition saved_pred_own (γ : gname) (dq : dfrac) (Φ : A → iProp Σ) :=
+    saved_anything_own (F := A -d> ▶ ∙) γ dq (Next ∘ Φ).
+
+  Global Instance saved_pred_own_contractive `{!savedPredG Σ A} γ dq :
+    Contractive (saved_pred_own γ dq : (A -d> iPropO Σ) → iProp Σ).
+  Proof.
+    solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
+  Qed.
+
+  Global Instance saved_pred_discarded_persistent γ Φ :
+    Persistent (saved_pred_own γ DfracDiscarded Φ).
+  Proof. apply _. Qed.
+
+  Global Instance saved_pred_fractional γ Φ : Fractional (λ q, saved_pred_own γ (DfracOwn q) Φ).
+  Proof. apply _. Qed.
+  Global Instance saved_pred_as_fractional γ Φ q :
+    AsFractional (saved_pred_own γ (DfracOwn q) Φ) (λ q, saved_pred_own γ (DfracOwn q) Φ) q.
+  Proof. apply _. Qed.
+
+  (** Allocation *)
+  Lemma saved_pred_alloc_strong (I : gname → Prop) (Φ : A → iProp Σ) dq :
+    ✓ dq →
+    pred_infinite I →
+    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_pred_own γ dq Φ.
+  Proof. intros ??. by apply saved_anything_alloc_strong. Qed.
+
+  Lemma saved_pred_alloc_cofinite (G : gset gname) (Φ : A → iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_pred_own γ dq Φ.
+  Proof. by apply saved_anything_alloc_cofinite. Qed.
+
+  Lemma saved_pred_alloc (Φ : A → iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, saved_pred_own γ dq Φ.
+  Proof. apply saved_anything_alloc. Qed.
+
+  (** Validity *)
+  Lemma saved_pred_valid γ dq Φ :
+    saved_pred_own γ dq Φ -∗ ⌜✓ dq⌝.
+  Proof. apply saved_anything_valid. Qed.
+  Lemma saved_pred_valid_2 γ dq1 dq2 Φ Ψ x :
+    saved_pred_own γ dq1 Φ -∗ saved_pred_own γ dq2 Ψ -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (Φ x ≡ Ψ x).
+  Proof.
+    iIntros "HΦ HΨ".
+    iCombine "HΦ HΨ" gives "($ & Hag)".
+    iApply later_equivI. by iApply (discrete_fun_equivI with "Hag").
+  Qed.
+  Lemma saved_pred_agree γ dq1 dq2 Φ Ψ x :
+    saved_pred_own γ dq1 Φ -∗ saved_pred_own γ dq2 Ψ -∗ ▷ (Φ x ≡ Ψ x).
+  Proof. iIntros "HΦ HΨ". iPoseProof (saved_pred_valid_2 with "HΦ HΨ") as "[_ $]". Qed.
+
+  (** Make an element read-only. *)
+  Lemma saved_pred_persist γ dq Φ :
+    saved_pred_own γ dq Φ ==∗ saved_pred_own γ DfracDiscarded Φ.
+  Proof. apply saved_anything_persist. Qed.
+
+  (** Recover fractional ownership for read-only element. *)
+  Lemma saved_pred_unpersist γ Φ:
+    saved_pred_own γ DfracDiscarded Φ ==∗ ∃ q, saved_pred_own γ (DfracOwn q) Φ.
+  Proof. apply saved_anything_unpersist. Qed.
+
+  (** Updates *)
+  Lemma saved_pred_update Ψ γ Φ :
+    saved_pred_own γ (DfracOwn 1) Φ ==∗ saved_pred_own γ (DfracOwn 1) Ψ.
+  Proof. apply saved_anything_update. Qed.
+  Lemma saved_pred_update_2 Ψ γ q1 q2 Φ1 Φ2 :
+    (q1 + q2 = 1)%Qp →
+    saved_pred_own γ (DfracOwn q1) Φ1 -∗ saved_pred_own γ (DfracOwn q2) Φ2 ==∗
+    saved_pred_own γ (DfracOwn q1) Ψ ∗ saved_pred_own γ (DfracOwn q2) Ψ.
+  Proof. apply saved_anything_update_2. Qed.
+  Lemma saved_pred_update_halves Ψ γ Φ1 Φ2 :
+    saved_pred_own γ (DfracOwn (1/2)) Φ1 -∗
+    saved_pred_own γ (DfracOwn (1/2)) Φ2 ==∗
+    saved_pred_own γ (DfracOwn (1/2)) Ψ ∗ saved_pred_own γ (DfracOwn (1/2)) Ψ.
+  Proof. apply saved_anything_update_halves. Qed.
+End saved_pred.

iris/base_logic/lib/token.v

+(** This library provides assertions that represent "unique tokens".
+The [token γ] assertion provides ownership of the token named [γ],
+and the key lemma [token_exclusive] proves only one token exists. *)
+From iris.algebra Require Import excl.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Import options.
+
+(** The CMRA we need. *)
+Class tokenG Σ := TokenG {
+  #[local] token_inG :: inG Σ (exclR unitO);
+}.
+Global Hint Mode tokenG - : typeclass_instances.
+
+Definition tokenΣ : gFunctors :=
+  #[ GFunctor (exclR unitO) ].
+
+Global Instance subG_tokenΣ Σ : subG tokenΣ Σ → tokenG Σ.
+Proof. solve_inG. Qed.
+
+Local Definition token_def `{!tokenG Σ} (γ : gname) : iProp Σ :=
+  own γ (Excl ()).
+Local Definition token_aux : seal (@token_def). Proof. by eexists. Qed.
+Definition token := token_aux.(unseal).
+Local Definition token_unseal :
+  @token = @token_def := token_aux.(seal_eq).
+Global Arguments token {Σ _} γ.
+
+Local Ltac unseal := rewrite ?token_unseal /token_def.
+
+Section lemmas.
+  Context `{!tokenG Σ}.
+
+  Global Instance token_timeless γ : Timeless (token γ).
+  Proof. unseal. apply _. Qed.
+
+  Lemma token_alloc_strong (P : gname → Prop) :
+    pred_infinite P →
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ token γ.
+  Proof. unseal. intros. iApply own_alloc_strong; done. Qed.
+  Lemma token_alloc :
+    ⊢ |==> ∃ γ, token γ.
+  Proof. unseal. iApply own_alloc. done. Qed.
+
+  Lemma token_exclusive γ :
+    token γ -∗ token γ -∗ False.
+  Proof.
+    unseal. iIntros "Htok1 Htok2".
+    iCombine "Htok1 Htok2" gives %[].
+  Qed.
+  Global Instance token_combine_gives γ :
+    CombineSepGives (token γ) (token γ) ⌜False⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (token_exclusive with "H1 H2") as %[].
+  Qed.
+
+End lemmas.
+

iris/base_logic/lib/wsat.v

+From stdpp Require Export coPset.
+From iris.algebra Require Import gmap_view gset coPset.
+From iris.bi Require Import lib.cmra.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Import options.
+
+(** All definitions in this file are internal to [fancy_updates] with the
+exception of what's in the [wsatGS] module. The module [wsatGS] is thus exported in
+[fancy_updates], where [wsat] is only imported. *)
+Module wsatGS.
+  Class wsatGpreS (Σ : gFunctors) : Set := WsatGpreS {
+    wsatGpreS_inv : inG Σ (gmap_viewR positive (agreeR $ laterO (iPropO Σ)));
+    wsatGpreS_enabled : inG Σ coPset_disjR;
+    wsatGpreS_disabled : inG Σ (gset_disjR positive);
+  }.
+
+  Class wsatGS (Σ : gFunctors) : Set := WsatG {
+    wsat_inG : wsatGpreS Σ;
+    invariant_name : gname;
+    enabled_name : gname;
+    disabled_name : gname;
+  }.
+
+  Definition wsatΣ : gFunctors :=
+    #[GFunctor (gmap_viewRF positive (agreeRF $ laterOF idOF));
+      GFunctor coPset_disjR;
+      GFunctor (gset_disjR positive)].
+
+  Global Instance subG_wsatΣ {Σ} : subG wsatΣ Σ → wsatGpreS Σ.
+  Proof. solve_inG. Qed.
+End wsatGS.
+Import wsatGS.
+
+(* Make the instances local to this file. We cannot use #[local] in the code
+above, as that would make the instances local to the module. *)
+Local Existing Instances wsat_inG wsatGpreS_inv wsatGpreS_enabled wsatGpreS_disabled.
+
+Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
+  Next P.
+Definition ownI `{!wsatGS Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+  own invariant_name
+    (gmap_view_frag i DfracDiscarded (to_agree $ invariant_unfold P)).
+Global Typeclasses Opaque ownI.
+Global Instance: Params (@invariant_unfold) 1 := {}.
+Global Instance: Params (@ownI) 3 := {}.
+
+Definition ownE `{!wsatGS Σ} (E : coPset) : iProp Σ :=
+  own enabled_name (CoPset E).
+Global Typeclasses Opaque ownE.
+Global Instance: Params (@ownE) 3 := {}.
+
+Definition ownD `{!wsatGS Σ} (E : gset positive) : iProp Σ :=
+  own disabled_name (GSet E).
+Global Typeclasses Opaque ownD.
+Global Instance: Params (@ownD) 3 := {}.
+
+Definition wsat `{!wsatGS Σ} : iProp Σ :=
+  locked (∃ I : gmap positive (iProp Σ),
+    own invariant_name
+      (gmap_view_auth (DfracOwn 1) (to_agree <$> (invariant_unfold <$> I))) ∗
+    [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
+
+Section wsat.
+Context `{!wsatGS Σ}.
+Implicit Types P : iProp Σ.
+
+(* Invariants *)
+Local Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
+Proof. solve_contractive. Qed.
+Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
+Proof. solve_contractive. Qed.
+Global Instance ownI_persistent i P : Persistent (ownI i P).
+Proof. rewrite /ownI. apply _. Qed.
+
+Lemma ownE_empty : ⊢ |==> ownE ∅.
+Proof.
+  rewrite /bi_emp_valid.
+  by rewrite (own_unit (coPset_disjUR) enabled_name).
+Qed.
+Lemma ownE_op E1 E2 : E1 ## E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
+Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
+Lemma ownE_disjoint E1 E2 : ownE E1 ∗ ownE E2 ⊢ ⌜E1 ## E2⌝.
+Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
+Lemma ownE_op' E1 E2 : ⌜E1 ## E2⌝ ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
+Proof.
+  iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
+  iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
+  iSplit; first done. iApply ownE_op; by try iFrame.
+Qed.
+Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False.
+Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
+
+Lemma ownD_empty : ⊢ |==> ownD ∅.
+Proof.
+  rewrite /bi_emp_valid.
+  by rewrite (own_unit (gset_disjUR positive) disabled_name).
+Qed.
+Lemma ownD_op E1 E2 : E1 ## E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
+Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
+Lemma ownD_disjoint E1 E2 : ownD E1 ∗ ownD E2 ⊢ ⌜E1 ## E2⌝.
+Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
+Lemma ownD_op' E1 E2 : ⌜E1 ## E2⌝ ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
+Proof.
+  iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
+  iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
+  iSplit; first done. iApply ownD_op; by try iFrame.
+Qed.
+Lemma ownD_singleton_twice i : ownD {[i]} ∗ ownD {[i]} ⊢ False.
+Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
+
+Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
+  own invariant_name (gmap_view_auth (DfracOwn 1) (to_agree <$> (invariant_unfold <$> I))) ∗
+  own invariant_name (gmap_view_frag i DfracDiscarded (to_agree $ invariant_unfold P)) ⊢
+  ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
+Proof.
+  rewrite -own_op own_valid gmap_view_both_validI_total.
+  iIntros "[%Q' (_& _ & HQ' & Hval & Hincl)]". rewrite !lookup_fmap.
+  case: (I !! i)=> [Q|] /=; last first.
+  { iDestruct "HQ'" as %?. done. }
+  iDestruct "HQ'" as %[= <-]. iExists Q; iSplit; first done.
+  rewrite to_agree_includedI internal_eq_sym -later_equivI. done.
+Qed.
+
+Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
+Proof.
+  rewrite /ownI /wsat -!lock.
+  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
+  iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
+  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
+  - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
+    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
+    iFrame "HI"; eauto.
+  - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
+Qed.
+Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}.
+Proof.
+  rewrite /ownI /wsat -!lock.
+  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
+  iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
+  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
+  - iDestruct (ownD_singleton_twice with "[$]") as %[].
+  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
+    iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
+Qed.
+
+Lemma ownI_alloc φ P :
+  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
+  wsat ∗ ▷ P ==∗ ∃ i, ⌜φ i⌝ ∗ wsat ∗ ownI i P.
+Proof.
+  iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
+  iDestruct "Hw" as (I) "[Hw HI]".
+  iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
+  iMod (own_updateP with "[$]") as "HE".
+  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
+    intros E. destruct (Hfresh (E ∪ dom I))
+      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
+  iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
+  iMod (own_update with "Hw") as "[Hw HiP]".
+  { eapply (gmap_view_alloc _ i DfracDiscarded (to_agree _)); [|done..].
+    by rewrite /= !lookup_fmap HIi. }
+  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
+  iExists (<[i:=P]>I); iSplitL "Hw".
+  { by rewrite !fmap_insert. }
+  iApply (big_sepM_insert _ I); first done.
+  iFrame "HI". iLeft. by rewrite /ownD; iFrame.
+Qed.
+
+Lemma ownI_alloc_open φ P :
+  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
+  wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
+Proof.
+  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
+  iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
+  iMod (own_updateP with "[$]") as "HD".
+  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
+    intros E. destruct (Hfresh (E ∪ dom I))
+      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
+  iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
+  iMod (own_update with "Hw") as "[Hw HiP]".
+  { eapply (gmap_view_alloc _ i DfracDiscarded (to_agree _)); [|done..].
+    by rewrite /= !lookup_fmap HIi. }
+  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
+  rewrite -/(ownD _). iFrame "HD".
+  iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
+  { by rewrite !fmap_insert. }
+  iApply (big_sepM_insert _ I); first done.
+  iFrame "HI". by iRight.
+Qed.
+End wsat.
+
+(* Allocation of an initial world *)
+Lemma wsat_alloc `{!wsatGpreS Σ} : ⊢ |==> ∃ _ : wsatGS Σ, wsat ∗ ownE ⊤.
+Proof.
+  iIntros.
+  iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γI) "HI";
+    first by apply gmap_view_auth_valid.
+  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
+  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
+  iModIntro; iExists (WsatG _ _ γI γE γD).
+  rewrite /wsat /ownE -lock; iFrame.
+  iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
+Qed.