(* iris_deprecated/base_logic/sts.v *)
From iris.algebra Require Export sts
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Export invariants
From iris.prelude Require Import options

Class stsGΣ (sts : stsT) := StsG {
  #[local] sts_inG :: inG Σ (sts_resR sts);
  #[global] sts_inhabited :: Inhabited (sts.state sts);
}.

Definition stsΣ(sts : stsT) : gFunctors := #[ GFunctor (sts_resR sts) ].

Global InstancesubG_stsΣ Σ sts :
  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
Proof. solve_inG. Qed.

Definition sts_ownS(S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
    own γ (sts_frag S T).

Definition sts_own(s : sts.state sts) (T : sts.tokens sts) : iProp Σ :=
    own γ (sts_frag_up s T).

Definition sts_inv(φ : sts.state sts → iProp Σ) : iProp Σ :=
    ∃ s, own γ (sts_auth s ∅) ∗ φ s.

Definition sts_ctx`{!invGS Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ :=
    inv N (sts_inv φ).

Global Instancests_inv_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) sts_inv.
  Proof. solve_proper. Qed.

Global Instancests_inv_proper :
    Proper (pointwise_relation _ (≡) ==> (≡)) sts_inv.
  Proof. solve_proper. Qed.

Global Instancests_ownS_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) sts_ownS.
  Proof. solve_proper. Qed.

Global Instancests_own_proper s : Proper ((≡) ==> (⊣⊢)) (sts_own s).
  Proof. solve_proper. Qed.

Global Instancests_ctx_ne `{!invGS Σ} n N :
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
  Proof. solve_proper. Qed.

Global Instancests_ctx_proper `{!invGS Σ} N :
    Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
  Proof. solve_proper. Qed.

Global Instancests_ctx_persistent `{!invGS Σ} N φ : Persistent (sts_ctx N φ).
  Proof. apply _. Qed.

Global Instancests_own_persistent s : Persistent (sts_own s ∅).
  Proof. apply _. Qed.

Global Instancests_ownS_persistent S : Persistent (sts_ownS S ∅).
  Proof. apply _. Qed.

Global Instance: Params (@sts_inv) 4 := {}.

Global Instance: Params (@sts_ownS) 4 := {}.

Global Instance: Params (@sts_own) 5 := {}.

Global Instance: Params (@sts_ctx) 6 := {}.

Lemma sts_ownS_weakenγ S1 S2 T1 T2 :
    T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
    sts_ownS γ S1 T1 ==∗ sts_ownS γ S2 T2.
  Proof. intros ???. iApply own_update. by apply sts_update_frag. Qed.

Lemma sts_own_weakenγ s S T1 T2 :
    T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
    sts_own γ s T1 ==∗ sts_ownS γ S T2.
  Proof. intros ???. iApply own_update. by apply sts_update_frag_up. Qed.

Lemma sts_own_weaken_stateγ s1 s2 T :
    sts.frame_steps T s2 s1 → sts.tok s2 ## T →
    sts_own γ s1 T ==∗ sts_own γ s2 T.
  Proof.
    intros ??. iApply own_update. apply sts_update_frag_up; [|done..].
    intros Hdisj. apply sts.closed_up. done.
  Qed.

Lemma sts_own_weaken_tokγ s T1 T2 :
    T2 ⊆ T1 → sts_own γ s T1 ==∗ sts_own γ s T2.
  Proof.
    intros ?. iApply own_update. apply sts_update_frag_up; last done.
    - intros. apply sts.closed_up. set_solver.
    - apply sts.elem_of_up.
  Qed.

Lemma sts_ownS_opγ S1 S2 T1 T2 :
    T1 ## T2 → sts.closed S1 T1 → sts.closed S2 T2 →
    sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2).
  Proof. intros. by rewrite /sts_ownS -own_op sts_frag_op. Qed.

Lemma sts_own_opγ s T1 T2 :
    T1 ## T2 → sts_own γ s (T1 ∪ T2) ==∗ sts_own γ s T1 ∗ sts_own γ s T2.

Local TypeclassesOpaque sts_own sts_ownS sts_inv sts_ctx.

Lemma sts_allocφ E N s :
    ▷ φ s ={E}=∗ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
  Proof.
    iIntros "Hφ". rewrite /sts_ctx /sts_own.
    iMod (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
    { apply sts_auth_valid; set_solver. }
    iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
    iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
    rewrite /sts_inv. iNext. iExists s. by iFrame.
  Qed.

Lemma sts_inv_accSφ E γ S T :
    ▷ sts_inv γ φ ∗ sts_ownS γ S T ={E}=∗ ∃ s,
      ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
  Proof.
    iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
    iDestruct "Hinv" as (s) "[>Hγ Hφ]".
    iDestruct (own_valid_2 with "Hγ Hγf") as %Hvalid.
    assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
    assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
    iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
    iIntros (s' T') "[% Hφ]".
    iMod (own_update_2 with "Hγ Hγf") as "Hγ".
    { rewrite sts_auth_frag_op; [|done..]. by apply sts_update_auth. }
    iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
    iModIntro. iNext. iExists s'; by iFrame.
  Qed.

Lemma sts_inv_accφ E γ s0 T :
    ▷ sts_inv γ φ ∗ sts_own γ s0 T ={E}=∗ ∃ s,
      ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
  Proof. by apply sts_inv_accS. Qed.

Lemma sts_accSφ E N γ S T :
    ↑N ⊆ E →
    sts_ctx γ N φ ∗ sts_ownS γ S T ={E,E∖↑N}=∗ ∃ s,
      ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
  Proof.
    iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".

Lemma sts_accφ E N γ s0 T :
    ↑N ⊆ E →
    sts_ctx γ N φ ∗ sts_own γ s0 T ={E,E∖↑N}=∗ ∃ s,
      ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
  Proof. by apply sts_accS. Qed.

Global TypeclassesOpaque sts_own sts_ownS sts_inv sts_ctx.