Library zoo_saturn.queue_mpsc_1

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Import zoo_std.xtchain.
Require Export zoo_saturn.queue_mpsc_1__code.
Require Import zoo_saturn.queue_mpsc_1__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type front node back new_back : location.
Implicit Type hist past nodes : list location.
Implicit Type v : val.
Implicit Type o : option val.
Implicit Type vs : list val.

Class QueueMpsc1G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] queue_mpsc_1 ۰ G ۰ history ۰ G :: MonoListG Σ location
  ; #[local] queue_mpsc_1 ۰ G ۰ model ۰ G :: TwinsG Σ (leibnizO (list val))
  }.

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

Module base.
  Section queue_mpsc_1 ۰ G.
    Context `{queue_mpsc_1 ۰ G : QueueMpsc1G Σ}.

    Implicit Type t : location.

    Record queue_mpsc_1 ۰ name :=
      { queue_mpsc_1 ۰ name ۰ inv : namespace
      ; queue_mpsc_1 ۰ name ۰ history : gname
      ; queue_mpsc_1 ۰ name ۰ model : gname
      }.
    Implicit Type γ : queue_mpsc_1 ۰ name.

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

    #[local] Definition history ۰ auth' γ_history hist :=
      mono_list ۰ auth γ_history (DfracOwn 1) hist.
    #[local] Definition history ۰ auth γ hist :=
      history ۰ auth' γ.(queue_mpsc_1 ۰ name ۰ history) hist.
    #[local] Definition history ۰ at γ i node :=
      mono_list ۰ at γ.(queue_mpsc_1 ۰ name ۰ history) i node.

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

    #[local] Definition node ۰ model γ node i : iProp Σ :=
      node ↦ₕ Header §Node 2 ∗
      history ۰ at γ i node.
    #[local] Instance : CustomIpat "node۰model" :=
      " ( #H{}_header & #Hhistory_at_{} ) ".

    #[local] Definition inv ۰ inner t γ : iProp Σ :=
      ∃ hist past front nodes back vs ,
      ⌜hist = past ++ front :: nodes ⌝ ∗
      ⌜back ∈ hist ⌝ ∗
      t .[front ] ↦{#1/4} #front ∗
      t .[back ] ↦ #back ∗
      xtchain (Header §Node 2) (DfracOwn 1) hist §Null ∗
      ([∗ list ] node ; v ∈ nodes ; vs , node .[data ] ↦ v ) ∗
      history ۰ auth γ hist ∗
      model₂ γ vs.
    #[local] Instance : CustomIpat "inv۰inner" :=
      " ( %hist{} & %past{} & %front{} & %nodes{} & %back{} & %vs{} & >%Hhist{} & >%Hback{} & >Ht_front & >Ht_back & >Hhist & >Hnodes & >Hhistory_auth & >Hmodel₂ ) ".
    #[local] Definition inv' t γ :=
      inv γ.(queue_mpsc_1 ۰ name ۰ inv) (inv ۰ inner t γ).
    Definition queue_mpsc_1 ۰ inv t γ ι : iProp Σ :=
      ⌜ι = γ.(queue_mpsc_1 ۰ name ۰ inv)⌝ ∗
      inv' t γ.
    #[local] Instance : CustomIpat "inv" :=
      " ( -> & #Hinv ) ".

    Definition queue_mpsc_1 ۰ model :=
      model₁.
    #[local] Instance : CustomIpat "model" :=
      " Hmodel₁{_{}} ".

    #[local] Definition consumer₁ t front : iProp Σ :=
      t .[front ] ↦{#3/4} #front.
    #[local] Definition consumer₂ t : iProp Σ :=
      ∃ front ,
      consumer₁ t front.
    #[local] Instance : CustomIpat "consumer₂" :=
      " ( %front{} & Hconsumer{_{}} ) ".
    Definition queue_mpsc_1 ۰ consumer :=
      consumer₂.
    #[local] Instance : CustomIpat "consumer" :=
      " (:consumer₂) ".

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

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

    #[local] Lemma history ｰ alloc front :
      ⊢ |==>
        ∃ γ_history ,
        history ۰ auth' γ_history [front].
    #[local] Lemma history ۰ at ｰ get {γ hist} i node :
      hist !! i = Some node →
      history ۰ auth γ hist ⊢
      history ۰ at γ i node.
    #[local] Lemma history ۰ at ｰ lookup γ hist i node :
      history ۰ auth γ hist -∗
      history ۰ at γ i node -∗
      ⌜hist !! i = Some node ⌝.
    #[local] Lemma history ｰ update {γ hist} node :
      history ۰ auth γ hist ⊢ |==>
        history ۰ auth γ (hist ++ [node]) ∗
        history ۰ at γ (length hist) node.

    #[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 inv ۰ inner ｰ history ۰ at t γ front :
      inv' t γ -∗
      consumer₁ t front ={⊤}=∗
        ∃ i ,
        consumer₁ t front ∗
        node ۰ model γ front i.

    Lemma queue_mpsc_1 ۰ model ｰ exclusive γ vs1 vs2 :
      queue_mpsc_1 ۰ model γ vs1 -∗
      queue_mpsc_1 ۰ model γ vs2 -∗
      False.

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

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

    #[local] Lemma queue_mpsc_1 ٠ front ｰ spec t γ :
      {{{
        inv' t γ
      }}}
        (#t ).{front }
      {{{
        front i
      , RET #front ;
        node ۰ model γ front i
      }}}.

    #[local] Lemma back ｰ spec t γ :
      {{{
        inv' t γ
      }}}
        (#t ).{back }
      {{{
        back i
      , RET #back ;
        node ۰ model γ back i
      }}}.

    Variant operation :=
      | IsEmpty (Ψ : bool → iProp Σ)
      | Pop (Ψ : option val → iProp Σ)
      | Other.
    Implicit Type op : operation.
    Variant operation' :=
      | IsEmpty'
      | Pop'
      | Other'.
    #[local] Instance operation'ｰ eq_dec : EqDecision operation' :=
      ltac:(solve_decision).
    #[local] Coercion operation ۰ to_operation' op :=
      match op with
      | IsEmpty _ ⇒
          IsEmpty'
      | Pop _ ⇒
          Pop'
      | Other ⇒
          Other'
      end.
    #[local] Definition is_empty ۰ au γ (Ψ : bool → iProp Σ) : iProp Σ :=
      AU <{
        ∃∃ vs ,
        model₁ γ vs
      }> @ ⊤ ∖ ↑γ.(queue_mpsc_1 ۰ name ۰ inv), ∅ <{
        model₁ γ vs
      , COMM
        Ψ (bool_decide (vs = []))
      }>.
    #[local] Definition pop ۰ au γ (Ψ : option val → iProp Σ) : iProp Σ :=
      AU <{
        ∃∃ vs ,
        model₁ γ vs
      }> @ ⊤ ∖ ↑γ.(queue_mpsc_1 ۰ name ۰ inv), ∅ <{
        model₁ γ (tail vs)
      , COMM
        Ψ (head vs)
      }>.
    #[local] Lemma next ｰ spec ｰ aux op t γ i node :
      {{{
        inv' t γ ∗
        history ۰ at γ i node ∗
        ( if decide (op = Other' :> operation') then True else
            consumer₁ t node
        ) ∗
        match op with
        | IsEmpty Ψ ⇒
            is_empty ۰ au γ Ψ
        | Pop Ψ ⇒
            pop ۰ au γ Ψ
        | Other ⇒
            True
        end
      }}}
        (#node ).{next }
      {{{
        res
      , RET res ;
        ( if decide (op = Other' :> operation') then True else
            consumer₁ t node
        ) ∗
        ( ⌜res = §Null%V⌝ ∗
          match op with
          | IsEmpty Ψ ⇒
              Ψ true
          | Pop Ψ ⇒
              Ψ None
          | Other ⇒
              True
          end
        ∨ ∃ node',
          ⌜res = #node'⌝ ∗
          node ۰ model γ node' ˖i ∗
          match op with
          | IsEmpty Ψ ⇒
              Ψ false
          | Pop Ψ ⇒
              pop ۰ au γ Ψ
          | Other ⇒
              True
          end
        )
      }}}.
    #[local] Lemma next ｰ spec {t γ i} node :
      {{{
        inv' t γ ∗
        history ۰ at γ i node
      }}}
        (#node ).{next }
      {{{
        res
      , RET res ;
          ⌜res = §Null%V⌝
        ∨ ∃ node',
          ⌜res = #node'⌝ ∗
          node ۰ model γ node' ˖i
      }}}.
    #[local] Lemma next ｰ spec ｰ is_empty {t γ i node} Ψ :
      {{{
        inv' t γ ∗
        history ۰ at γ i node ∗
        consumer₁ t node ∗
        is_empty ۰ au γ Ψ
      }}}
        (#node ).{next }
      {{{
        res
      , RET res ;
        consumer₁ t node ∗
        ( ⌜res = §Null%V⌝ ∗
          Ψ true
        ∨ ∃ node',
          ⌜res = #node'⌝ ∗
          node ۰ model γ node' ˖i ∗
          Ψ false
        )
      }}}.
    #[local] Lemma next ｰ spec ｰ pop {t γ i node} Ψ :
      {{{
        inv' t γ ∗
        history ۰ at γ i node ∗
        consumer₁ t node ∗
        pop ۰ au γ Ψ
      }}}
        (#node ).{next }
      {{{
        res
      , RET res ;
        consumer₁ t node ∗
        ( ⌜res = §Null%V⌝ ∗
          Ψ None
        ∨ ∃ node',
          ⌜res = #node'⌝ ∗
          node ۰ model γ node' ˖i ∗
          pop ۰ au γ Ψ
        )
      }}}.

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

    #[local] Lemma queue_mpsc_1 ٠ push₁ ｰ spec t γ i node new_back v :
      <<<
        inv' t γ ∗
        node ۰ model γ node i ∗
        new_back ↦ₕ Header §Node 2 ∗
        new_back .[next ] ↦ §Null ∗
        new_back .[data ] ↦ v
      | ∀∀ vs ,
        queue_mpsc_1 ۰ model γ vs
      >>>
        queue_mpsc_1 ٠ push₁ #node #new_back @ ↑γ.(queue_mpsc_1 ۰ name ۰ inv)
      <<<
        queue_mpsc_1 ۰ model γ (vs ++ [v])
      | RET ();
        ∃ j ,
        history ۰ at γ j new_back
      >>>.

    #[local] Lemma queue_mpsc_1 ٠ fix_back ｰ spec t γ i back j new_back :
      {{{
        inv' t γ ∗
        history ۰ at γ i back ∗
        node ۰ model γ new_back j
      }}}
        queue_mpsc_1 ٠ fix_back #t #back #new_back
      {{{
        RET ();
        True
      }}}.

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

    #[local] Lemma queue_mpsc_1 ٠ pop ｰ spec ｰ aux t γ :
      <<<
        inv' t γ ∗
        consumer₂ t
      | ∀∀ vs ,
        model₁ γ vs
      >>>
        queue_mpsc_1 ٠ pop #t @ ↑γ.(queue_mpsc_1 ۰ name ۰ inv)
      <<<
        model₁ γ (tail vs)
      | RET head vs ;
        consumer₂ t
      >>>.
    Lemma queue_mpsc_1 ٠ pop ｰ spec t γ ι :
      <<<
        queue_mpsc_1 ۰ inv t γ ι ∗
        queue_mpsc_1 ۰ consumer t
      | ∀∀ vs ,
        queue_mpsc_1 ۰ model γ vs
      >>>
        queue_mpsc_1 ٠ pop #t @ ↑ι
      <<<
        queue_mpsc_1 ۰ model γ (tail vs)
      | RET head vs ;
        queue_mpsc_1 ۰ consumer t
      >>>.
  End queue_mpsc_1 ۰ G.

  #[global] Opaque queue_mpsc_1 ۰ inv.
  #[global] Opaque queue_mpsc_1 ۰ model.
  #[global] Opaque queue_mpsc_1 ۰ consumer.
End base.

Require zoo_saturn.queue_mpsc_1__opaque.

Section queue_mpsc_1 ۰ G.
  Context `{queue_mpsc_1 ۰ G : QueueMpsc1G Σ}.

  Implicit Type 𝑡 : location.
  Implicit Type t : val.

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

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

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

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

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

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

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

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

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

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

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

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