Library zoo_saturn.queue_mpsc_2

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.list.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_saturn.queue_mpsc_2__code.
Require Import zoo_saturn.queue_mpsc_2__types.
Require Import zoo.options.

Implicit Type l : location.
Implicit Type v t : val.
Implicit Type vs front back : list val.
Implicit Type o : option val.

Class QueueMpsc2G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] queue_mpsc_2 ۰ G ۰ twins ۰ G :: TwinsG Σ (leibnizO (list val))
  }.

Definition queue_mpsc_2 ۰ Σ :=
  #[twins ۰ Σ (leibnizO (list val))
  ].
#[global] Instance subG ｰ queue_mpsc_2 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG queue_mpsc_2 ۰ Σ Σ →
  QueueMpsc2G Σ.

Section queue_mpsc_2 ۰ G.
  Context `{queue_mpsc_2 ۰ G : QueueMpsc2G Σ}.

  Record metadata :=
    { metadata ۰ model : gname
    ; metadata ۰ front : gname
    }.
  Implicit Type γ : metadata.

  #[local] Instance metadata ｰ eq_dec : EqDecision metadata :=
    ltac:(solve_decision).
  #[local] Instance metadata ｰ countable :
    Countable metadata.

  #[local] Definition model₁' γ_model vs :=
    twins ۰ twin₁ γ_model (DfracOwn 1) vs.
  #[local] Definition model₁ γ vs :=
    model₁' γ.(metadata ۰ model) vs.
  #[local] Definition model₂' γ_model vs :=
    twins ۰ twin₂ γ_model vs.
  #[local] Definition model₂ γ vs :=
    model₂' γ.(metadata ۰ model) vs.

  #[local] Definition front₁' γ_front front :=
    twins ۰ twin₁ γ_front (DfracOwn 1) front.
  #[local] Definition front₁ γ front :=
    front₁' γ.(metadata ۰ front) front.
  #[local] Definition front₂' γ_model front :=
    twins ۰ twin₂ γ_model front.
  #[local] Definition front₂ γ front :=
    front₂' γ.(metadata ۰ front) front.

  #[local] Definition inv ۰ inner l γ : iProp Σ :=
    ∃ front back ,
    front₂ γ front ∗
    l .[back ] ↦ glist ۰ to_val back ∗
    model₂ γ (front ++ reverse back).
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %front{} & %back{} & >Hfront₂ & >Hl_back & >Hmodel₂ ) ".
  Definition queue_mpsc_2 ۰ inv t ι : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    inv ι (inv ۰ inner l γ).
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & #Hmeta & #Hinv ) ".

  Definition queue_mpsc_2 ۰ model t vs : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    model₁ γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %l{;_} & %γ{;_} & %Heq{} & Hmeta_{} & Hmodel₁{_{}} ) ".

  Definition queue_mpsc_2 ۰ consumer t : iProp Σ :=
    ∃ l γ front ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    l .[front ] ↦ glist ۰ to_val front ∗
    front₁ γ front.
  #[local] Instance : CustomIpat "consumer" :=
    " ( %l_ & %γ_ & %front & %Heq & Hmeta_ & Hl_front & Hfront₁ ) ".

  #[global] Instance queue_mpsc_2 ۰ model ｰ timeless t vs :
    Timeless (queue_mpsc_2 ۰ model t vs).
  #[global] Instance queue_mpsc_2 ۰ consumer ｰ timeless t :
    Timeless (queue_mpsc_2 ۰ consumer t ).

  #[global] Instance queue_mpsc_2 ۰ inv ｰ persistent t ι :
    Persistent (queue_mpsc_2 ۰ inv t ι).

  #[local] Lemma model ｰ alloc :
    ⊢ |==>
      ∃ γ_model ,
      model₁' γ_model [] ∗
      model₂' γ_model [].
  #[local] Lemma model₁ ｰ exclusive γ vs1 vs2 :
    model₁ γ vs1 -∗
    model₁ γ vs2 -∗
    False.
  #[local] Lemma model ｰ agree γ vs1 vs2 :
    model₁ γ vs1 -∗
    model₂ γ vs2 -∗
    ⌜vs1 = vs2 ⌝.
  #[local] Lemma model ｰ update {γ vs1 vs2} vs :
    model₁ γ vs1 -∗
    model₂ γ vs2 ==∗
      model₁ γ vs ∗
      model₂ γ vs.

  #[local] Lemma front ｰ alloc :
    ⊢ |==>
      ∃ γ_front ,
      front₁' γ_front [] ∗
      front₂' γ_front [].
  #[local] Lemma front ｰ agree γ front1 front2 :
    front₁ γ front1 -∗
    front₂ γ front2 -∗
    ⌜front1 = front2 ⌝.
  #[local] Lemma front ｰ update {γ front1 front2} front :
    front₁ γ front1 -∗
    front₂ γ front2 ==∗
      front₁ γ front ∗
      front₂ γ front.

  Lemma queue_mpsc_2 ۰ model ｰ exclusive t vs1 vs2 :
    queue_mpsc_2 ۰ model t vs1 -∗
    queue_mpsc_2 ۰ model t vs2 -∗
    False.

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

  Lemma queue_mpsc_2 ٠ create ｰ spec ι :
    {{{
      True
    }}}
      queue_mpsc_2 ٠ create ()
    {{{
      t
    , RET t ;
      queue_mpsc_2 ۰ inv t ι ∗
      queue_mpsc_2 ۰ model t [] ∗
      queue_mpsc_2 ۰ consumer t
    }}}.

  Lemma queue_mpsc_2 ٠ is_empty ｰ spec t ι :
    <<<
      queue_mpsc_2 ۰ inv t ι ∗
      queue_mpsc_2 ۰ consumer t
    | ∀∀ vs ,
      queue_mpsc_2 ۰ model t vs
    >>>
      queue_mpsc_2 ٠ is_empty t @ ↑ι
    <<<
      queue_mpsc_2 ۰ model t vs
    | RET #(bool_decide (vs = []%list));
      queue_mpsc_2 ۰ consumer t
    >>>.

  Lemma queue_mpsc_2 ٠ push_front ｰ spec t ι v :
    <<<
      queue_mpsc_2 ۰ inv t ι ∗
      queue_mpsc_2 ۰ consumer t
    | ∀∀ vs ,
      queue_mpsc_2 ۰ model t vs
    >>>
      queue_mpsc_2 ٠ push_front t v @ ↑ι
    <<<
      queue_mpsc_2 ۰ model t (v :: vs)
    | RET ();
      queue_mpsc_2 ۰ consumer t
    >>>.

  Lemma queue_mpsc_2 ٠ push_back ｰ spec t ι v :
    <<<
      queue_mpsc_2 ۰ inv t ι
    | ∀∀ vs ,
      queue_mpsc_2 ۰ model t vs
    >>>
      queue_mpsc_2 ٠ push_back t v @ ↑ι
    <<<
      queue_mpsc_2 ۰ model t (vs ++ [v])
    | RET ();
      True
    >>>.

  Lemma queue_mpsc_2 ٠ pop ｰ spec t ι :
    <<<
      queue_mpsc_2 ۰ inv t ι ∗
      queue_mpsc_2 ۰ consumer t
    | ∀∀ vs ,
      queue_mpsc_2 ۰ model t vs
    >>>
      queue_mpsc_2 ٠ pop t @ ↑ι
    <<<
      queue_mpsc_2 ۰ model t (tail vs)
    | RET head vs ;
      queue_mpsc_2 ۰ consumer t
    >>>.
End queue_mpsc_2 ۰ G.

Require zoo_saturn.queue_mpsc_2__opaque.

#[global] Opaque queue_mpsc_2 ۰ inv.
#[global] Opaque queue_mpsc_2 ۰ model.
#[global] Opaque queue_mpsc_2 ۰ consumer.