Library zoo_saturn.queue_mpsc_3

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.iris.base_logic.lib.oneshot.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_saturn.queue_mpsc_3__code.
Require Import zoo_saturn.queue_mpsc_3__types.
Require Import zoo.options.

Implicit Type b closed : bool.
Implicit Type l : location.
Implicit Type v t : val.
Implicit Type vs front back : list val.
Implicit Type ws : option (list val).

Class QueueMpsc3G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] queue_mpsc_3 ۰ G ۰ twins ۰ G :: TwinsG Σ (leibnizO (list val))
  ; #[local] queue_mpsc_3 ۰ G ۰ lstate ۰ G :: OneshotG Σ () ()
  }.

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

Section queue_mpsc_3 ۰ G.
  Context `{queue_mpsc_3 ۰ G : QueueMpsc3G Σ}.

  Record metadata :=
    { metadata ۰ model : gname
    ; metadata ۰ front : gname
    ; metadata ۰ lstate : 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 lstate ۰ open₁' γ_lstate :=
    oneshot ۰ pending γ_lstate (DfracOwn (1/2)) ().
  #[local] Definition lstate ۰ open₁ γ :=
    lstate ۰ open₁' γ.(metadata ۰ lstate).
  #[local] Definition lstate ۰ open₂' γ_lstate :=
    oneshot ۰ pending γ_lstate (DfracOwn (1/2)) ().
  #[local] Definition lstate ۰ open₂ γ :=
    lstate ۰ open₂' γ.(metadata ۰ lstate).
  #[local] Definition lstate ۰ closed γ :=
    oneshot ۰ shot γ.(metadata ۰ lstate) ().

  #[local] Definition inv ۰ inner l γ : iProp Σ :=
    ∃ front v_back ,
    front₂ γ front ∗
    l .[back ] ↦ v_back ∗
    ( ( lstate ۰ open₂ γ ∗
          ∃ back ,
          ⌜v_back = list ۰ to_clist_open back ⌝ ∗
          model₂ γ (front ++ reverse back)
      ) ∨ (
        lstate ۰ closed γ ∗
        ⌜v_back = §clist ٠ Closed%V⌝
      )
    ).
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %front{} & %v_back & >Hfront₂ & >Hl_back & [(>Hopen₂ & %back{} & >-> & >Hmodel₂{_{suff}}) | (>Hclosed{_{suff}} & >->)] ) ".
  Definition queue_mpsc_3 ۰ inv t ι : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    inv ι (inv ۰ inner l γ).
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & #Hmeta & #Hinv ) ".

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

  Definition queue_mpsc_3 ۰ consumer t ws : iProp Σ :=
    ∃ l γ v_front front ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    l .[front ] ↦ v_front ∗
    front₁ γ front ∗
    match ws with
    | None ⇒
        ⌜v_front = list ۰ to_clist_open front ⌝ ∗
        lstate ۰ open₁ γ
    | Some ws ⇒
        ⌜ws = front ⌝ ∗
        ⌜v_front = list ۰ to_clist_closed front ⌝ ∗
        lstate ۰ closed γ ∗
        model₂ γ front
    end.
  #[local] Instance : CustomIpat "consumer" :=
    " ( %l_ & %γ_ & %v_front & %front & %Heq & Hmeta_ & Hl_front & Hfront₁ & {{open}(-> & Hopen₁);{closed}(-> & -> & Hclosed & Hmodel₂);Hlstate} ) ".

  Definition queue_mpsc_3 ۰ closed t : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    lstate ۰ closed γ.
  #[local] Instance : CustomIpat "closed" :=
    " ( %l_ & %γ_ & %Heq & Hmeta_ & Hclosed ) ".

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

  #[global] Instance queue_mpsc_3 ۰ inv ｰ persistent t ι :
    Persistent (queue_mpsc_3 ۰ inv t ι).
  #[global] Instance queue_mpsc_3 ۰ closed ｰ persistent t :
    Persistent (queue_mpsc_3 ۰ closed 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.

  #[local] Lemma lstate ｰ alloc :
    ⊢ |==>
      ∃ γ_lstate ,
      lstate ۰ open₁' γ_lstate ∗
      lstate ۰ open₂' γ_lstate.
  #[local] Lemma lstate ｰ open₁ ｰ closed γ :
    lstate ۰ open₁ γ -∗
    lstate ۰ closed γ -∗
    False.
  #[local] Lemma lstate ｰ open₂ ｰ closed γ :
    lstate ۰ open₂ γ -∗
    lstate ۰ closed γ -∗
    False.
  #[local] Lemma lstate ｰ update γ :
    lstate ۰ open₁ γ -∗
    lstate ۰ open₂ γ ==∗
    lstate ۰ closed γ.

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

  Lemma queue_mpsc_3 ۰ consumer ｰ exclusive t ws1 ws2 :
    queue_mpsc_3 ۰ consumer t ws1 -∗
    queue_mpsc_3 ۰ consumer t ws2 -∗
    False.
  Lemma queue_mpsc_3 ｰ consumer ｰ closed t vs :
    queue_mpsc_3 ۰ consumer t (Some vs) ⊢
    queue_mpsc_3 ۰ closed t.

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

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

  Lemma queue_mpsc_3 ٠ push_front ｰ spec ｰ open t ι v :
    <<<
      queue_mpsc_3 ۰ inv t ι ∗
      queue_mpsc_3 ۰ consumer t None
    | ∀∀ vs ,
      queue_mpsc_3 ۰ model t vs
    >>>
      queue_mpsc_3 ٠ push_front t v @ ↑ι
    <<<
      queue_mpsc_3 ۰ model t (v :: vs)
    | RET false ;
      queue_mpsc_3 ۰ consumer t None
    >>>.
  Lemma queue_mpsc_3 ٠ push_front ｰ spec ｰ closed t ι vs v :
    <<<
      queue_mpsc_3 ۰ inv t ι ∗
      queue_mpsc_3 ۰ consumer t (Some vs)
    | ∀∀ vs',
      queue_mpsc_3 ۰ model t vs'
    >>>
      queue_mpsc_3 ٠ push_front t v @ ↑ι
    <<<
      ∃∃ b ,
      ⌜b = bool_decide (vs = [])⌝ ∗
      ⌜vs' = vs ⌝ ∗
      queue_mpsc_3 ۰ model t (if b then [] else v :: vs)
    | RET #b ;
      queue_mpsc_3 ۰ consumer t (Some $ if b then [] else v :: vs)
    >>>.

  Lemma queue_mpsc_3 ٠ push_back ｰ spec ｰ open closed t ι v :
    <<<
      queue_mpsc_3 ۰ inv t ι
    | ∀∀ vs ,
      queue_mpsc_3 ۰ model t vs
    >>>
      queue_mpsc_3 ٠ push_back t v @ ↑ι
    <<<
      ∃∃ closed ,
      if closed then
        queue_mpsc_3 ۰ model t vs
      else
        queue_mpsc_3 ۰ model t (vs ++ [v])
    | RET #closed ;
      if closed then
        queue_mpsc_3 ۰ closed t
      else
        True
    >>>.
  Lemma queue_mpsc_3 ٠ push_back ｰ spec ｰ closed closed t ι v :
    {{{
      queue_mpsc_3 ۰ inv t ι ∗
      queue_mpsc_3 ۰ closed t
    }}}
      queue_mpsc_3 ٠ push_back t v
    {{{
      RET true ;
      True
    }}}.

  Lemma queue_mpsc_3 ٠ pop ｰ spec ｰ open t ι :
    <<<
      queue_mpsc_3 ۰ inv t ι ∗
      queue_mpsc_3 ۰ consumer t None
    | ∀∀ vs ,
      queue_mpsc_3 ۰ model t vs
    >>>
      queue_mpsc_3 ٠ pop t @ ↑ι
    <<<
      queue_mpsc_3 ۰ model t (tail vs)
    | RET head vs ;
      queue_mpsc_3 ۰ consumer t None
    >>>.
  Lemma queue_mpsc_3 ٠ pop ｰ spec ｰ closed t ι vs :
    <<<
      queue_mpsc_3 ۰ inv t ι ∗
      queue_mpsc_3 ۰ consumer t (Some vs)
    | ∀∀ vs',
      queue_mpsc_3 ۰ model t vs'
    >>>
      queue_mpsc_3 ٠ pop t @ ↑ι
    <<<
      ⌜vs' = vs ⌝ ∗
      queue_mpsc_3 ۰ model t (tail vs)
    | RET head vs ;
      queue_mpsc_3 ۰ consumer t (Some $ tail vs)
    >>>.

  Lemma queue_mpsc_3 ٠ close ｰ spec ｰ open t ι :
    <<<
      queue_mpsc_3 ۰ inv t ι ∗
      queue_mpsc_3 ۰ consumer t None
    | ∀∀ vs ,
      queue_mpsc_3 ۰ model t vs
    >>>
      queue_mpsc_3 ٠ close t @ ↑ι
    <<<
      queue_mpsc_3 ۰ model t vs
    | RET false ;
      queue_mpsc_3 ۰ consumer t (Some vs)
    >>>.
  Lemma queue_mpsc_3 ٠ close ｰ spec ｰ closed t ι vs :
    {{{
      queue_mpsc_3 ۰ inv t ι ∗
      queue_mpsc_3 ۰ consumer t (Some vs)
    }}}
      queue_mpsc_3 ٠ close t
    {{{
      RET true ;
      queue_mpsc_3 ۰ consumer t (Some vs)
    }}}.
End queue_mpsc_3 ۰ G.

Require zoo_saturn.queue_mpsc_3__opaque.

#[global] Opaque queue_mpsc_3 ۰ inv.
#[global] Opaque queue_mpsc_3 ۰ model.
#[global] Opaque queue_mpsc_3 ۰ consumer.
#[global] Opaque queue_mpsc_3 ۰ closed.