phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/gen_heap.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 σ ⌝ ∗
    gen_heap_name hG ↪●MAP σ ∗
    gen_meta_name hG ↪●MAP m.
(* iris/base_logic/lib/gen_heap.v *)
Definition pointsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ
:=
    gen_heap_name hG ↪◯MAP[l]{dq} v.
(* iris/base_logic/lib/gen_heap.v *)
Definition pointsto_aux : seal (@pointsto_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Definition pointsto
:= pointsto_aux.(unseal).
(* iris/base_logic/lib/gen_heap.v *)
Definition pointsto_unseal : @pointsto = @pointsto_def
:=
    pointsto_aux.(seal_eq).
(* iris/base_logic/lib/gen_heap.v *)
Definition meta_token_def (l : L) (E : coPset) : iProp Σ
:=
    ∃ γm, gen_meta_name hG ↪◯MAP[l]□ γm ∗ own γm (reservation_map_token E).
(* iris/base_logic/lib/gen_heap.v *)
Definition meta_token_aux : seal (@meta_token_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Definition meta_token
:= meta_token_aux.(unseal).
(* iris/base_logic/lib/gen_heap.v *)
Definition meta_token_unseal :
    @meta_token = @meta_token_def
:= meta_token_aux.(seal_eq).
(* iris/base_logic/lib/gen_heap.v *)
(* [reservation_map_data] uses a [positive] instead of a [namespace] as key.
  For [meta_set] to hold, we can pick any positive in [↑ N], which we obtain
  using [coPpick]. *)
Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ
:=
    ∃ γm, gen_meta_name hG ↪◯MAP[l]□ γm ∗
          own γm (reservation_map_data (coPpick (↑ N)) (to_agree (encode x))).
(* iris/base_logic/lib/gen_heap.v *)
Definition meta_aux : seal (@meta_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Definition meta
:= meta_aux.(unseal).
(* iris/base_logic/lib/gen_heap.v *)
Definition meta_unseal : @meta = @meta_def
:= meta_aux.(seal_eq).
(* iris/base_logic/lib/gen_heap.v *)
Notation "l ↦ dq v"
:= (pointsto l dq v)
  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
(* iris/base_logic/lib/gen_heap.v *)
(* General properties of pointsto *)
Instance pointsto_timeless l dq v : Timeless (l ↦{dq} v).
Proof. rewrite pointsto_unseal. apply _. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance pointsto_fractional l v : Fractional (λ q, l ↦{#q} v)%I.
Proof. rewrite pointsto_unseal. apply _. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance pointsto_as_fractional l q v :
    AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
Proof. rewrite pointsto_unseal. apply _. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance pointsto_persistent l v : Persistent (l ↦□ v).
Proof. rewrite pointsto_unseal. apply _. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Lemma pointsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_valid. Qed.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
(* 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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
(* 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.
(* iris/base_logic/lib/gen_heap.v *)
(* 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.
(* iris/base_logic/lib/gen_heap.v *)
(* Framing support *)
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.
(* iris/base_logic/lib/gen_heap.v *)
(* General properties of [meta] and [meta_token] *)
Instance meta_token_timeless l N : Timeless (meta_token l N).
Proof. rewrite meta_token_unseal. apply _. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
Proof. rewrite meta_unseal. apply _. Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
Proof. rewrite meta_unseal. apply _. Qed.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
Lemma meta_token_valid_2 l E1 E2 :
    meta_token l E1 -∗ meta_token l E2 -∗ ⌜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 %[_ ->].
    by iCombine "Hm1 Hm2" gives %?%reservation_map_token_valid_op.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance meta_token_combine_as l E1 E2 :
    CombineSepGives (meta_token l E1) (meta_token l E2) ⌜E1 ## E2⌝.
Proof.
    rewrite /CombineSepGives. iIntros "[H1 H2]".
    iDestruct (meta_token_valid_2 with "H1 H2") as %?; auto.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
Lemma meta_token_ne l1 l2 E :
    E ≠ ∅ → meta_token l1 ⊤ -∗ meta_token l2 E -∗ ⌜l1 ≠ l2⌝.
Proof.
    iIntros "%HE H1 H2" (->). iCombine "H1 H2" gives %Hdisj.
    destruct HE. by apply disjoint_top_l_L.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
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.
    pose proof (coPpick_elem_of (↑ N) (nclose_non_empty _)); set_solver.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
Lemma meta_meta_token_valid `{Countable A} l (x : A) N E :
    meta l N x -∗ meta_token l E -∗ ⌜↑N ⊈ E⌝.
Proof.
    rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
    iIntros "(%γm & #Hγm & Hm1) (%γm' & #Hγm' & Hm2) %Hsub".
    iCombine "Hγm Hγm'" gives %[_ <-].
    iCombine "Hm1 Hm2" gives %Hvalid. iPureIntro.
    rewrite reservation_map_valid_eq /= left_id_L right_id_L in Hvalid.
    destruct Hvalid as [_ Hvalid]. specialize (Hvalid (coPpick (↑ N))).
    rewrite lookup_singleton_eq in Hvalid.
    pose proof (coPpick_elem_of (↑ N) (nclose_non_empty _)); set_solver.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
Lemma meta_meta_token_valid' `{Countable A} l (x : A) N E :
    ↑N ⊆ E → meta l N x -∗ meta_token l E -∗ False.
Proof.
    iIntros (?) "#Hmeta Htoken".
    by iDestruct (meta_meta_token_valid with "Hmeta Htoken") as %?.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance combine_sep_gives_meta_meta_token_1
      `{Countable A} l (x : A) N E :
    CombineSepGives (meta l N x) (meta_token l E) ⌜↑N ⊈ E⌝.
Proof.
    rewrite /CombineSepGives. iIntros "[#Hmeta Htoken]".
    iDestruct (meta_meta_token_valid with "Hmeta Htoken") as %?. by eauto.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
Instance combine_sep_gives_meta_meta_token_2
      `{Countable A} l (x : A) N E :
    CombineSepGives (meta_token l E) (meta l N x) ⌜↑N ⊈ E⌝.
Proof.
    rewrite /CombineSepGives. iIntros "[Htoken #Hmeta]".
    iCombine "Hmeta Htoken" gives %?; eauto.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
(* 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.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
Lemma gen_heap_valid σ l dq v : gen_heap_interp σ -∗ l ↦{dq} v -∗ ⌜σ !! l = Some v⌝.
Proof.
    iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
    rewrite /gen_heap_interp pointsto_unseal.
    by iCombine "Hσ Hl" gives %?.
  Qed.
(* iris/base_logic/lib/gen_heap.v *)
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.
(* iris/base_logic/lib/gen_heap.v *)
(* 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.
(* iris/base_logic/lib/gen_heap.v *)
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 *)
(* 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".
(* iris/base_logic/lib/gen_inv_heap.v *)
Notation "l ↦ v"
:= (pointsto l (DfracOwn 1) v) (at level 20) : bi_scope.
(* iris/base_logic/lib/gen_inv_heap.v *)
Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmra
:= gmapUR L $ prodR
  (optionR $ exclR $ leibnizO V)
  (agreeR (V -d> PropO)).
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L}
:= {
  #[local] inv_heapGpreS_inG :: inG Σ (authR (inv_heap_mapUR L V))
}.
(* iris/base_logic/lib/gen_inv_heap.v *)
Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L}
:= Inv_HeapG {
  #[local] inv_heap_inG :: inv_heapGpreS L V Σ;
  inv_heap_name : gname
}.
(* iris/base_logic/lib/gen_inv_heap.v *)
Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors
:=
  #[ GFunctor (authR (inv_heap_mapUR L V)) ].
(* iris/base_logic/lib/gen_inv_heap.v *)
Instance subG_inv_heapGpreS (L V : Type) `{Countable L} {Σ} :
  subG (inv_heapΣ L V) Σ → inv_heapGpreS L V Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/gen_inv_heap.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.
(* iris/base_logic/lib/gen_inv_heap.v *)
Definition inv_heap_inv : iProp Σ
:= inv inv_heapN inv_heap_inv_P.
(* iris/base_logic/lib/gen_inv_heap.v *)
Definition inv_pointsto_own (l : L) (v : V) (I : V → Prop) : iProp Σ
:=
    own (inv_heap_name gG) (◯ {[l := (Excl' v, to_agree I) ]}).
(* iris/base_logic/lib/gen_inv_heap.v *)
Definition inv_pointsto (l : L) (I : V → Prop) : iProp Σ
:=
    own (inv_heap_name gG) (◯ {[l := (None, to_agree I)]}).
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
Notation "l '↦_' I □"
:= (inv_pointsto l I%stdpp%type)
  (at level 20, I at level 9, format "l  '↦_' I  '□'") : bi_scope.
(* iris/base_logic/lib/gen_inv_heap.v *)
Instance : Params (@inv_pointsto_own) 8
:= {}.
(* iris/base_logic/lib/gen_inv_heap.v *)
Instance : Params (@inv_pointsto) 7
:= {}.
(* iris/base_logic/lib/gen_inv_heap.v *)
Lemma to_inv_heap_valid h : ✓ to_inv_heap h.
Proof. intros l. rewrite lookup_fmap. by case: (h !! l). Qed.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
(* * 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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
(* 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. *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V).
Proof. apply _. Qed.
(* iris/base_logic/lib/gen_inv_heap.v *)
Instance inv_pointsto_persistent l I : Persistent (l ↦_I □).
Proof. apply _. Qed.
(* iris/base_logic/lib/gen_inv_heap.v *)
Instance inv_pointsto_timeless l I : Timeless (l ↦_I □).
Proof. apply _. Qed.
(* iris/base_logic/lib/gen_inv_heap.v *)
Instance inv_pointsto_own_timeless l v I : Timeless (l ↦_I v).
Proof. apply _. Qed.
(* iris/base_logic/lib/gen_inv_heap.v *)
(* * 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.
(* iris/base_logic/lib/gen_inv_heap.v *)
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.
(* iris/base_logic/lib/gen_inv_heap.v *)
(* 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_eq. }
    rewrite insert_delete_eq -to_inv_heap_insert. iIntros "!> {$H◯}".
    iApply ("Hclose" with "[H● HsepM]"). iExists _; by iFrame.
  Qed.