Library zoo.iris.base_logic.lib.oneshot

From zoo Require Import
  prelude.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris.base_logic Require Import
  lib.ghost_var.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  options.

Class OneshotG Σ A B :=
  { #[local] oneshot_G_var_G :: GhostVarG Σ (leibnizO (A + B))
  }.

Definition oneshot_Σ A B :=
  #[ghost_var_Σ (leibnizO (A + B))
  ].
#[global] Instance subG_oneshot_Σ Σ A B :
  subG (oneshot_Σ A B) Σ →
  OneshotG Σ A B.

Section oneshot_G.
  Context `{oneshot_G : !OneshotG Σ A B}.

  Implicit Types a : A.
  Implicit Types b : B.

  Definition oneshot_pending γ dq a :=
    ghost_var γ dq (inl a).
  Definition oneshot_shot γ b :=
    ghost_var γ DfracDiscarded (inr b).

  #[global] Instance oneshot_pending_timeless γ dq a :
    Timeless (oneshot_pending γ dq a).
  #[global] Instance oneshot_shot_timeless γ b :
    Timeless (oneshot_shot γ b).

  #[global] Instance oneshot_shot_persistent γ b :
    Persistent (oneshot_shot γ b).

  #[global] Instance oneshot_pending_fractional γ a :
    Fractional (λ q, oneshot_pending γ (DfracOwn q) a).
  #[global] Instance oneshot_pending_as_fractional γ q a :
    AsFractional (oneshot_pending γ (DfracOwn q) a) (λ q, oneshot_pending γ (DfracOwn q) a) q.

  Lemma oneshot_alloc a :
    ⊢ |==>
      ∃ γ,
      oneshot_pending γ (DfracOwn 1) a.

  Lemma oneshot_pending_valid γ dq a :
    oneshot_pending γ dq a ⊢
    ⌜✓ dq⌝.
  Lemma oneshot_pending_combine γ dq1 a1 dq2 a2 :
    oneshot_pending γ dq1 a1 -∗
    oneshot_pending γ dq2 a2 -∗
      ⌜a1 = a2⌝ ∗
      oneshot_pending γ (dq1 ⋅ dq2) a1.
  Lemma oneshot_pending_valid_2 γ dq1 a1 dq2 a2 :
    oneshot_pending γ dq1 a1 -∗
    oneshot_pending γ dq2 a2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜a1 = a2⌝.
  Lemma oneshot_pending_agree γ dq1 a1 dq2 a2 :
    oneshot_pending γ dq1 a1 -∗
    oneshot_pending γ dq2 a2 -∗
    ⌜a1 = a2⌝.
  Lemma oneshot_pending_dfrac_ne γ1 dq1 a1 γ2 dq2 a2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    oneshot_pending γ1 dq1 a1 -∗
    oneshot_pending γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma oneshot_pending_ne γ1 a1 γ2 dq2 a2 :
    oneshot_pending γ1 (DfracOwn 1) a1 -∗
    oneshot_pending γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma oneshot_pending_exclusive γ a1 dq2 a2 :
    oneshot_pending γ (DfracOwn 1) a1 -∗
    oneshot_pending γ dq2 a2 -∗
    False.
  Lemma oneshot_pending_persist γ dq a :
    oneshot_pending γ dq a ⊢ |==>
    oneshot_pending γ DfracDiscarded a.

  Lemma oneshot_shot_agree γ b1 b2 :
    oneshot_shot γ b1 -∗
    oneshot_shot γ b2 -∗
    ⌜b1 = b2⌝.

  Lemma oneshot_pending_shot γ dq a b :
    oneshot_pending γ dq a -∗
    oneshot_shot γ b -∗
    False.

  Lemma oneshot_update_pending γ a a' :
    oneshot_pending γ (DfracOwn 1) a ⊢ |==>
    oneshot_pending γ (DfracOwn 1) a'.
  Lemma oneshot_update_shot {γ a} b :
    oneshot_pending γ (DfracOwn 1) a ⊢ |==>
    oneshot_shot γ b.
End oneshot_G.

#[global] Opaque oneshot_pending.
#[global] Opaque oneshot_shot.