at_borrow.v

From iris.algebra Require Import gmap auth frac.
From iris.proofmode Require Import tactics.
From lrust.lifetime Require Export lifetime.
From iris.prelude Require Import options.

(** Atomic persistent borrows  *)
(* JH : at_bor has to depend on the view. Otherwise, we could open
   them at a view which is earlier than the one at which it has been
   created, and the payload could be weakened without synchronizing
   with the end of the lifetime (remember that the underlying payload
   is not necessarily independent of the view for views older than V). *)
Definition at_bor `{!invGS Σ, !lftG Σ Lat userE} κ N (P : monPred _ _) : monPred _ _ :=
  (∃ i, ⌜N ## lftN⌝ ∗ &{κ,i}P ∗ ⎡inv N (∃ V', idx_bor_own i V')⎤)%I.
Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.

Section atomic_bors.
  Context `{!invGS Σ, !lftG Σ Lat userE}.

  Global Instance at_bor_ne κ n N : Proper (dist n ==> dist n) (at_bor κ N).
  Proof. solve_proper. Qed.
  Global Instance at_bor_contractive κ N : Contractive (at_bor κ N).
  Proof. solve_contractive. Qed.
  Global Instance at_bor_proper κ N : Proper ((⊣⊢) ==> (⊣⊢)) (at_bor κ N).
  Proof. solve_proper. Qed.
  Global Instance at_bor_persistent κ N P : Persistent (&at{κ, N} P) := _.

  Lemma at_bor_iff N P P' κ :
    ▷ □ (P ↔ P') -∗ &at{κ, N}P -∗ &at{κ, N}P'.
  Proof.
    iIntros "#HPP' H". iDestruct "H" as (i) "#(% & HP & ?)".
    iExists i. iFrame "#%". iApply (idx_bor_iff with "[HPP'] HP")=>/=. auto.
  Qed.

  Lemma bor_share N P E κ :
    N ## lftN → &{κ}P ={E}=∗ &at{κ, N}P.
  Proof.
    iIntros (HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
    iExists i. iFrame "#%". iMod (inv_alloc with "[Hown]") as "$"; [|done]. iNext.
    iDestruct (monPred_in_intro with "Hown") as (V) "[_ Hown]". by iExists _.
  Qed.

  Lemma at_bor_acc N P E q κ :
    ↑lftN ⊆ E → ↑N ⊆ E →
    ⎡lft_ctx⎤ -∗ &at{κ,N}P -∗ q.[κ] ={E,E∖↑N}=∗
      ∃ Vb, (monPred_in Vb → ▷ P) ∗ ((monPred_in Vb → ▷ P) ={E∖↑N,E}=∗ q.[κ]).
  Proof.
    iIntros (??) "#LFT #HP Htok". iDestruct "HP" as (i) "#(% & Hidx & Hinv)".
    iInv N as (V) ">Hi" "Hclose". iCombine "Hidx Htok" as "HH".
    iDestruct (monPred_in_intro with "HH") as (V') "(#HV' & #Hidx' & Htok)".
    iMod (idx_bor_acc with "LFT Hidx' Hi Htok") as (V'') "(% & HP & Hclose')".
    { solve_ndisj. } iExists V''. iModIntro. iSplitL "HP"; iIntros "H".
    - iApply (monPred_in_elim with "H"). by iNext.
    - iCombine "HV' H" as "HH".
      iDestruct (monPred_in_intro with "HH") as (V''') "(#HV''' & % & HP)".
      iMod ("Hclose'" $! V''' with "[//] [HP]") as "[Hown Htok]".
      { rewrite -monPred_at_later. iApply "HP". solve_lat. }
      iMod ("Hclose" with "[Hown]") as "_"; [by iNext; iExists _|].
      iModIntro. by iApply monPred_in_elim.
  Qed.

  Lemma at_bor_shorten N P κ κ' : κ ⊑ κ' -∗ &at{κ',N}P -∗ &at{κ,N}P.
  Proof.
    iIntros "#H⊑ H". iDestruct "H" as (i) "(% & ? & ?)".
    iExists i. iFrame "%∗". by iApply idx_bor_shorten.
  Qed.

  Lemma at_bor_fake `{LatBottom Lat} N P E κ :
    ↑lftN ⊆ E → N ## lftN → ⎡lft_ctx⎤ -∗ <subj> [†κ] ={E}=∗ &at{κ,N}P.
  Proof.
    iIntros (??) "#LFT#H†". iApply (bor_share with "[>]"); try done.
    by iApply (bor_fake with "LFT H†").
  Qed.
End atomic_bors.

Global Typeclasses Opaque at_bor.