Library zoo_saturn.queue_mpmc_1

Require Import iris.base_logic.lib.ghost_map.

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.auth_nat_max.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Import zoo.base.
Require Import zoo_std.option.
Require Import zoo_std.xtchain.
Require Export zoo_saturn.queue_mpmc_1__code.
Require Import zoo_saturn.queue_mpmc_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 vs : list val.
Implicit Type waiter : gname.
Implicit Type waiters : gmap gname nat.

Class QueueMpmc1G Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] queue_mpmc_1۰G۰history۰G :: MonoListG Σ location
  ; #[local] queue_mpmc_1۰G۰front۰G :: AuthNatMaxG Σ
  ; #[local] queue_mpmc_1۰G۰model۰G :: TwinsG Σ (leibnizO (list val))
  ; #[local] queue_mpmc_1۰G۰waiters۰G :: ghost_mapG Σ gname nat
  ; #[local] queue_mpmc_1۰G۰saved_pred۰G :: SavedPredG Σ bool
  }.

Definition queue_mpmc_1۰Σ :=
  #[mono_list۰Σ location
  ; auth_nat_max۰Σ
  ; twins۰Σ (leibnizO (list val))
  ; ghost_mapΣ gname nat
  ; saved_pred۰Σ bool
  ].
#[global] Instance subGｰqueue_mpmc_1۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG queue_mpmc_1۰Σ Σ →
  QueueMpmc1G Σ.

Module base.
  Section queue_mpmc_1۰G.
    Context `{queue_mpmc_1۰G : QueueMpmc1G Σ}.

    Implicit Type t : location.

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

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

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

    #[local] Definition front۰auth' γ_front i :=
      auth_nat_max۰auth γ_front (DfracOwn 1) i.
    #[local] Definition front۰auth γ i :=
      front۰auth' γ.(queue_mpmc_1۰name۰front) i.
    #[local] Definition front۰lb γ i :=
      auth_nat_max۰lb γ.(queue_mpmc_1۰name۰front) i.

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

    #[local] Definition waiters۰auth' γ_waiters waiters :=
      ghost_map_auth γ_waiters 1 waiters.
    #[local] Definition waiters۰auth γ waiters :=
      waiters۰auth' γ.(queue_mpmc_1۰name۰waiters) waiters.
    #[local] Definition waiters۰at γ waiter i :=
      ghost_map_elem γ.(queue_mpmc_1۰name۰waiters) waiter (DfracOwn 1) i.

    #[local] Definition node۰model γ node i b : iProp Σ :=
      node ↦ₕ Header §Node 2 ∗
      history۰at γ i node ∗
      if b then front۰lb γ i else True%I.
    #[local] Instance : CustomIpat "node۰model" :=
      " ( #H{}_header & #Hhistory_at_{} & {{front}#Hfront_lb_{};_} ) ".

    #[local] Definition waiter۰au γ (Ψ : bool → iProp Σ) : iProp Σ :=
      AU <{
        ∃∃ vs,
        model₁ γ vs
      }> @ ⊤ ∖ ↑γ.(queue_mpmc_1۰name۰inv), ∅ <{
        model₁ γ vs
      , COMM
        Ψ (bool_decide (vs = []))
      }>.
    #[local] Definition waiter۰model γ past waiter i : iProp Σ :=
      ∃ Ψ,
      saved_pred waiter Ψ ∗
      if decide (i < length past) then
        Ψ false
      else
        waiter۰au γ Ψ.

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

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

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

    #[global] Instance queue_mpmc_1۰invｰpersistent t γ ι :
      Persistent (queue_mpmc_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 frontｰalloc :
      ⊢ |==>
        ∃ γ_front,
        front۰auth' γ_front 0.
    #[local] Lemma front۰lbｰget γ i :
      front۰auth γ i ⊢
      front۰lb γ i.
    #[local] Lemma front۰lbｰvalid γ i1 i2 :
      front۰auth γ i1 -∗
      front۰lb γ i2 -∗
      ⌜i2 ≤ i1⌝.
    #[local] Lemma frontｰupdate {γ i} i' :
      i ≤ i' →
      front۰auth γ i ⊢ |==>
      front۰auth γ i'.

    #[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 waitersｰalloc :
      ⊢ |==>
        ∃ γ_waiters,
        waiters۰auth' γ_waiters ∅.
    #[local] Lemma waitersｰinsert {γ waiters} i Ψ :
      waiters۰auth γ waiters ⊢ |==>
        ∃ waiter,
        waiters۰auth γ (<[waiter := i]> waiters) ∗
        saved_pred waiter Ψ ∗
        waiters۰at γ waiter i.
    #[local] Lemma waitersｰdelete γ waiters waiter i :
      waiters۰auth γ waiters -∗
      waiters۰at γ waiter i ==∗
        ⌜waiters !! waiter = Some i⌝ ∗
        waiters۰auth γ (delete waiter waiters).

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

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

    #[local] Lemma frontｰspec_strong Ψ t γ :
      {{{
        inv' t γ ∗
        if Ψ is Some Ψ then
          waiter۰au γ Ψ
        else
          True
      }}}
        (#t).{front}
      {{{
        front i
      , RET #front;
        node۰model γ front i true ∗
        if Ψ is Some Ψ then
          ∃ waiter,
          saved_pred waiter Ψ ∗
          waiters۰at γ waiter i
        else
          True
      }}}.
    #[local] Lemma frontｰspec t γ :
      {{{
        inv' t γ
      }}}
        (#t).{front}
      {{{
        front i
      , RET #front;
        node۰model γ front i true
      }}}.

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

    Variant operation :=
      | IsEmpty waiter (Ψ : 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 pop۰au γ (Ψ : option val → iProp Σ) : iProp Σ :=
      AU <{
        ∃∃ vs,
        model₁ γ vs
      }> @ ⊤ ∖ ↑γ.(queue_mpmc_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
            front۰lb γ i
        ) ∗
        match op with
        | IsEmpty waiter Ψ ⇒
            saved_pred waiter Ψ ∗
            waiters۰at γ waiter i ∗
            £ 1
        | Pop Ψ ⇒
            pop۰au γ Ψ
        | Other ⇒
            True
        end
      }}}
        (#node).{next}
      {{{
        res
      , RET res;
          ⌜res = §Null%V⌝ ∗
          match op with
          | IsEmpty waiter Ψ ⇒
              Ψ true
          | Pop Ψ ⇒
              Ψ None
          | Other ⇒
              True
          end
        ∨ ∃ node',
          ⌜res = #node'⌝ ∗
          node۰model γ node' ˖i false ∗
          match op with
          | IsEmpty waiter Ψ ⇒
              Ψ 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 false
      }}}.
    #[local] Lemma nextｰspecｰis_empty {t γ i node} waiter Ψ :
      {{{
        inv' t γ ∗
        history۰at γ i node ∗
        front۰lb γ i ∗
        saved_pred waiter Ψ ∗
        waiters۰at γ waiter i ∗
        £ 1
      }}}
        (#node).{next}
      {{{
        res
      , RET res;
          ⌜res = §Null%V⌝ ∗
          Ψ true
        ∨ ∃ node',
          ⌜res = #node'⌝ ∗
          node۰model γ node' ˖i false ∗
          Ψ false
      }}}.
    #[local] Lemma nextｰspecｰpop {t γ i node} Ψ :
      {{{
        inv' t γ ∗
        history۰at γ i node ∗
        front۰lb γ i ∗
        pop۰au γ Ψ
      }}}
        (#node).{next}
      {{{
        res
      , RET res;
          ⌜res = §Null%V⌝ ∗
          Ψ None
        ∨ ∃ node',
          ⌜res = #node'⌝ ∗
          node۰model γ node' ˖i false ∗
          pop۰au γ Ψ
      }}}.

    Lemma queue_mpmc_1٠is_emptyｰspec t γ ι :
      <<<
        queue_mpmc_1۰inv t γ ι
      | ∀∀ vs,
        queue_mpmc_1۰model γ vs
      >>>
        queue_mpmc_1٠is_empty #t @ ↑ι
      <<<
        queue_mpmc_1۰model γ vs
      | RET #(bool_decide (vs = []%list));
        £ 1
      >>>.
    Lemma queue_mpmc_1٠is_emptyｰspec' t γ ι :
      {{{
        queue_mpmc_1۰inv t γ ι
      }}}
        queue_mpmc_1٠is_empty #t
      {{{
        b
      , RET #b;
        True
      }}}.

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

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

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

    Lemma queue_mpmc_1٠popｰspec t γ ι :
      <<<
        queue_mpmc_1۰inv t γ ι
      | ∀∀ vs,
        queue_mpmc_1۰model γ vs
      >>>
        queue_mpmc_1٠pop #t @ ↑ι
      <<<
        queue_mpmc_1۰model γ (tail vs)
      | RET head vs;
        £ 1
      >>>.
  End queue_mpmc_1۰G.

  #[global] Opaque queue_mpmc_1۰inv.
  #[global] Opaque queue_mpmc_1۰model.
End base.

Require zoo_saturn.queue_mpmc_1__opaque.

Section queue_mpmc_1۰G.
  Context `{queue_mpmc_1۰G : QueueMpmc1G Σ}.

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

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

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

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

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

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

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

  Lemma queue_mpmc_1٠is_emptyｰspec t ι :
    <<<
      queue_mpmc_1۰inv t ι
    | ∀∀ vs,
      queue_mpmc_1۰model t vs
    >>>
      queue_mpmc_1٠is_empty t @ ↑ι
    <<<
      queue_mpmc_1۰model t vs
    | RET #(bool_decide (vs = []%list));
      £ 1
    >>>.
  Lemma queue_mpmc_1٠is_emptyｰspec' t ι :
    {{{
      queue_mpmc_1۰inv t ι
    }}}
      queue_mpmc_1٠is_empty t
    {{{
      b
    , RET #b;
      True
    }}}.

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

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

#[global] Opaque queue_mpmc_1۰inv.
#[global] Opaque queue_mpmc_1۰model.

Section queue_mpmc_1۰G.
  Context `{queue_mpmc_1۰G : QueueMpmc1G Σ}.
  Context τ `{!iType (iProp Σ) τ}.

  #[local] Definition itype۰inner t : iProp Σ :=
    ∃ vs,
    queue_mpmc_1۰model t vs ∗
    [∗ list] v ∈ vs, τ v.
  #[local] Instance : CustomIpat "itype۰inner" :=
    " ( %vs & >Hmodel & #Hvs ) ".
  Definition itype۰queue_mpmc_1 t : iProp Σ :=
    queue_mpmc_1۰inv t (nroot.@"1") ∗
    inv (nroot.@"2") (itype۰inner t).
  #[local] Instance : CustomIpat "itype" :=
    " ( #Hinv1 & #Hinv2 ) ".

  #[global] Instance itype۰queue_mpmc_1ｰitype :
    iType _ itype۰queue_mpmc_1.

  Lemma queue_mpmc_1٠createｰtype :
    {{{
      True
    }}}
      queue_mpmc_1٠create ()
    {{{
      t
    , RET t;
      itype۰queue_mpmc_1 t
    }}}.

  Lemma queue_mpmc_1٠is_emptyｰtype t :
    {{{
      itype۰queue_mpmc_1 t
    }}}
      queue_mpmc_1٠is_empty t
    {{{
      b
    , RET #b;
      True
    }}}.

  Lemma queue_mpmc_1٠pushｰtype t v :
    {{{
      itype۰queue_mpmc_1 t ∗
      τ v
    }}}
      queue_mpmc_1٠push t v
    {{{
      RET ();
      True
    }}}.

  Lemma queue_mpmc_1٠popｰtype t :
    {{{
      itype۰queue_mpmc_1 t
    }}}
      queue_mpmc_1٠pop t
    {{{
      o
    , RET o;
      itype۰option τ o
    }}}.
End queue_mpmc_1۰G.

#[global] Opaque itype۰queue_mpmc_1.