From iris.algebra Require Export auth upred_tactics.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import invariants ghost_ownership.
Import uPred.

(* The CMRA we need. *)
Class authG Λ Σ (A : ucmraT) := AuthG {
  auth_inG :> inG Λ Σ (authR A);
  auth_timeless :> CMRADiscrete A;
}.
(* The Functor we need. *)
Definition authGF (A : ucmraT) : gFunctor := GFunctor (constRF (authR A)).
(* Show and register that they match. *)
Instance authGF_inGF (A : ucmraT) `{inGF Λ Σ (authGF A)}
  `{CMRADiscrete A} : authG Λ Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed.

Section definitions.
  Context `{authG Λ Σ A} (γ : gname).
  Definition auth_own (a : A) : iPropG Λ Σ :=
    own γ (◯ a).
  Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
    (∃ a, own γ (● a) ★ φ a)%I.
  Definition auth_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
    inv N (auth_inv φ).

  Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
  Proof. solve_proper. Qed.
  Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
  Proof. solve_proper. Qed.
  Global Instance auth_own_timeless a : TimelessP (auth_own a).
  Proof. apply _. Qed.
  Global Instance auth_inv_ne n : 
    Proper (pointwise_relation A (dist n) ==> dist n) (auth_inv).
  Proof. solve_proper. Qed.
  Global Instance auth_ctx_ne n N :
    Proper (pointwise_relation A (dist n) ==> dist n) (auth_ctx N).
  Proof. solve_proper. Qed.
  Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ).
  Proof. apply _. Qed.
End definitions.

Typeclasses Opaque auth_own auth_ctx.
Instance: Params (@auth_inv) 6.
Instance: Params (@auth_own) 6.
Instance: Params (@auth_ctx) 7.

Section auth.
  Context `{AuthI : authG Λ Σ A}.
  Context (φ : A → iPropG Λ Σ) {φ_proper : Proper ((≡) ==> (⊣⊢)) φ}.
  Implicit Types N : namespace.
  Implicit Types P Q R : iPropG Λ Σ.
  Implicit Types a b : A.
  Implicit Types γ : gname.

  Lemma auth_own_op γ a b :
    auth_own γ (a ⋅ b) ⊣⊢ (auth_own γ a ★ auth_own γ b).
  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
  Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
  Proof. by rewrite /auth_own own_valid auth_validI. Qed.

  Lemma auth_alloc_strong N E a (G : gset gname) :
    ✓ a → nclose N ⊆ E →
    ▷ φ a ={E}=> ∃ γ, ■(γ ∉ G) ∧ auth_ctx γ N φ ∧ auth_own γ a.
  Proof.
    iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
    iPvs (own_alloc_strong (Auth (Excl' a) a) _ G) as {γ} "[% Hγ]"; first done.
    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
    iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
    { iNext. iExists a. by iFrame "Hφ". }
    iPvsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame "Hγ'".
  Qed.

  Lemma auth_alloc N E a :
    ✓ a → nclose N ⊆ E →
    ▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a.
  Proof.
    iIntros {??} "Hφ".
    iPvs (auth_alloc_strong N E a ∅ with "Hφ") as {γ} "[_ ?]"; [done..|].
    by iExists γ.
  Qed.

  Lemma auth_empty γ E : True ={E}=> auth_own γ ∅.
  Proof. by rewrite -own_empty. Qed.

  Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.

  Lemma auth_fsa E N (Ψ : V → iPropG Λ Σ) γ a :
    fsaV → nclose N ⊆ E →
    auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
      ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
      fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
        ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
        (auth_own γ (L a) -★ Ψ x)))
     ⊢ fsa E Ψ.
  Proof.
    iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
    iInv N as {a'} "[Hγ Hφ]".
    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
    iDestruct (own_valid _ with "#Hγ") as "Hvalid".
    iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
    iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
    rewrite ->(left_id _ _) in Ha'; setoid_subst.
    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
    { iApply "HΨ"; by iSplit. }
    iIntros {v} "HL". iDestruct "HL" as {L Lv ?} "(% & Hφ & HΨ)".
    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]".
    { apply (auth_local_update_l L); tauto. }
    iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
    iNext. iExists (L a ⋅ b). by iFrame "Hφ".
  Qed.

  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V → iPropG Λ Σ) γ a :
    fsaV → nclose N ⊆ E →
    auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
      ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
      fsa (E ∖ nclose N) (λ x,
        ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
        (auth_own γ (L a) -★ Ψ x)))
    ⊢ fsa E Ψ.
  Proof.
    iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto.
    iFrame "Ha Hγf". iIntros {a'} "H".
    iApply fsa_wand_r; iSplitL; first by iApply "HΨ".
    iIntros {v} "?"; by iExists L, Lv, _.
  Qed.
End auth.