Library zoo_std.flag_mpsc

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.base.
Require Export zoo_std.flag_mpsc__code.
Require Import zoo_std.flag_mpsc__types.
Require Import zoo.options.

Implicit Type b : bool.

Class FlagMpscG Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] flag_mpsc۰G۰state۰G :: OneshotG Σ () ()
  ; #[local] flag_mpsc۰G۰consumer۰G :: ExclG Σ unitO
  }.

Definition flag_mpsc۰Σ :=
  #[oneshot۰Σ () ()
  ; excl۰Σ unitO
  ].
#[global] Instance subGｰflag_mpsc۰Σ `{zoo۰G : !ZooG Σ} :
  subG flag_mpsc۰Σ Σ →
  FlagMpscG Σ.

Module base.
  Section flag_mpsc۰G.
    Context `{flag_mpsc۰G : FlagMpscG Σ}.

    Implicit Type t : location.
    Implicit Type P : iProp Σ.

    Record flag_mpsc۰name :=
      { flag_mpsc۰name۰state : gname
      ; flag_mpsc۰name۰consumer : gname
      }.
    Implicit Type γ : flag_mpsc۰name.

    #[global] Instance flag_mpsc۰nameｰeq_dec : EqDecision flag_mpsc۰name :=
      ltac:(solve_decision).
    #[global] Instance flag_mpsc۰nameｰcountable :
      Countable flag_mpsc۰name.

    #[local] Definition state۰unset' γ_state :=
      oneshot۰pending γ_state Own ().
    #[local] Definition state۰unset γ :=
      state۰unset' γ.(flag_mpsc۰name۰state).
    #[local] Definition state۰set' γ_state :=
      oneshot۰shot γ_state ().
    #[local] Definition state۰set γ :=
      state۰set' γ.(flag_mpsc۰name۰state).

    #[local] Definition consumer' γ_consumer :=
      excl γ_consumer ().
    #[local] Definition consumer γ :=
      consumer' γ.(flag_mpsc۰name۰consumer).

    #[local] Definition inv۰consumer γ P : iProp Σ :=
      P ∨ consumer γ.
    #[local] Instance : CustomIpat "inv۰consumer" :=
      " [ HP | Hconsumer{_{!}} ] ".
    #[local] Definition inv۰set γ P : iProp Σ :=
      state۰set γ ∗
      inv۰consumer γ P.
    #[local] Instance : CustomIpat "inv۰set" :=
      " ( #Hstate_set & Hinv_consumer ) ".
    #[local] Definition inv۰inner t γ P : iProp Σ :=
      ∃ b,
      t ↦ᵣ #b ∗
      if b then
        inv۰set γ P
      else
        state۰unset γ.
    #[local] Instance : CustomIpat "inv۰inner" :=
      " ( %b & >Ht & Hb ) ".
    Definition flag_mpsc۰inv t γ P :=
      inv nroot (inv۰inner t γ P).
    #[local] Instance : CustomIpat "inv" :=
      " #Hinv ".

    Definition flag_mpsc۰consumer :=
      consumer.
    #[local] Instance : CustomIpat "consumer" :=
      " Hconsumer ".

    Definition flag_mpsc۰resolved :=
      state۰set.
    #[local] Instance : CustomIpat "resolved" :=
      " #Hstate_set ".

    #[global] Instance flag_mpsc۰invｰcontractive t γ :
      Contractive (flag_mpsc۰inv t γ).
    #[global] Instance flag_mpsc۰invｰne t γ :
      NonExpansive (flag_mpsc۰inv t γ).
    #[global] Instance flag_mpsc۰invｰproper t γ :
      Proper ((≡) ==> (≡)) (flag_mpsc۰inv t γ).

    #[global] Instance flag_mpsc۰consumerｰtimeless γ :
      Timeless (flag_mpsc۰consumer γ).
    #[global] Instance flag_mpsc۰resolvedｰtimeless γ :
      Timeless (flag_mpsc۰resolved γ).

    #[global] Instance flag_mpsc۰invｰpersistent t γ P :
      Persistent (flag_mpsc۰inv t γ P).
    #[global] Instance flag_mpsc۰resolvedｰpersistent γ :
      Persistent (flag_mpsc۰resolved γ).

    #[local] Lemma stateｰalloc :
      ⊢ |==>
        ∃ γ_state,
        state۰unset' γ_state.
    #[local] Lemma stateｰunsetｰset γ :
      state۰unset γ -∗
      state۰set γ -∗
      False.
    #[local] Lemma stateｰupdate γ :
      state۰unset γ ⊢ |==>
      state۰set γ.

    #[local] Lemma consumerｰalloc :
      ⊢ |==>
        ∃ γ_consumer,
        consumer' γ_consumer.
    #[local] Lemma consumerｰexclusive γ :
      consumer γ -∗
      consumer γ -∗
      False.

    Lemma flag_mpsc۰consumerｰexclusive γ :
      flag_mpsc۰consumer γ -∗
      flag_mpsc۰consumer γ -∗
      False.

    Lemma flag_mpsc٠createｰspec P :
      {{{
        True
      }}}
        flag_mpsc٠create ()
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        flag_mpsc۰inv t γ P ∗
        flag_mpsc۰consumer γ
      }}}.

    Lemma flag_mpsc٠getｰspec t γ P :
      {{{
        flag_mpsc۰inv t γ P ∗
        flag_mpsc۰consumer γ
      }}}
        flag_mpsc٠get #t
      {{{
        b
      , RET #b;
        if b then
          P
        else
          flag_mpsc۰consumer γ
      }}}.

    Lemma flag_mpsc٠setｰspec t γ P :
      {{{
        flag_mpsc۰inv t γ P ∗
        ▷ P
      }}}
        flag_mpsc٠set #t
      {{{
        RET ();
        flag_mpsc۰resolved γ
      }}}.
  End flag_mpsc۰G.

  #[global] Opaque flag_mpsc۰inv.
  #[global] Opaque flag_mpsc۰consumer.
  #[global] Opaque flag_mpsc۰resolved.
End base.

Require zoo_std.flag_mpsc__opaque.

Section flag_mpsc۰G.
  Context `{flag_mpsc۰G : FlagMpscG Σ}.

  Implicit Type 𝑡 : location.
  Implicit Type t : val.
  Implicit Type P : iProp Σ.

  Definition flag_mpsc۰inv t P : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    base.flag_mpsc۰inv 𝑡 γ P.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".

  Definition flag_mpsc۰consumer t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    base.flag_mpsc۰consumer γ.
  #[local] Instance : CustomIpat "consumer" :=
    " ( %l{;_} & %γ{;_} & {%Heq{};->} & #Hmeta{_{}} & Hconsumer{_{}} ) ".

  Definition flag_mpsc۰resolved t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    base.flag_mpsc۰resolved γ.
  #[local] Instance : CustomIpat "resolved" :=
    " ( %l{;_} & %γ{;_} & {%Heq{};->} & #Hmeta{_{}} & Hresolved{_{}} ) ".

  #[global] Instance flag_mpsc۰invｰcontractive t :
    Contractive (flag_mpsc۰inv t).
  #[global] Instance flag_mpsc۰invｰne t :
    NonExpansive (flag_mpsc۰inv t).
  #[global] Instance flag_mpsc۰invｰproper t :
    Proper ((≡) ==> (≡)) (flag_mpsc۰inv t).

  #[global] Instance flag_mpsc۰consumerｰtimeless t :
    Timeless (flag_mpsc۰consumer t).
  #[global] Instance flag_mpsc۰resolvedｰtimeless t :
    Timeless (flag_mpsc۰resolved t).

  #[global] Instance flag_mpsc۰invｰpersistent t P :
    Persistent (flag_mpsc۰inv t P).
  #[global] Instance flag_mpsc۰resolvedｰpersistent t :
    Persistent (flag_mpsc۰resolved t).

  Lemma flag_mpsc۰consumerｰexclusive t :
    flag_mpsc۰consumer t -∗
    flag_mpsc۰consumer t -∗
    False.

  Lemma flag_mpsc٠createｰspec P :
    {{{
      True
    }}}
      flag_mpsc٠create ()
    {{{
      t
    , RET t;
      flag_mpsc۰inv t P ∗
      flag_mpsc۰consumer t
    }}}.

  Lemma flag_mpsc٠getｰspec t P :
    {{{
      flag_mpsc۰inv t P ∗
      flag_mpsc۰consumer t
    }}}
      flag_mpsc٠get t
    {{{
      b
    , RET #b;
      if b then
        P
      else
        flag_mpsc۰consumer t
    }}}.

  Lemma flag_mpsc٠setｰspec t P :
    {{{
      flag_mpsc۰inv t P ∗
      ▷ P
    }}}
      flag_mpsc٠set t
    {{{
      RET ();
      flag_mpsc۰resolved t
    }}}.
End flag_mpsc۰G.

#[global] Opaque flag_mpsc۰inv.
#[global] Opaque flag_mpsc۰consumer.
#[global] Opaque flag_mpsc۰resolved.