Library zoo_saturn.bqueue_spsc

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.relations.
Require Import zoo.common.list.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.auth_twins.
Require Import zoo.iris.base_logic.lib.auth_nat_max.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_saturn.bqueue_spsc__code.
Require Import zoo_saturn.bqueue_spsc__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type i front front_cache back back_cache : nat.
Implicit Type l : location.
Implicit Type v w t : val.
Implicit Type vs ws hist : list val.

Variant stability :=
  | Stable
  | Unstable.
Implicit Type stable : stability.

#[local] Instance stabilityｰinhabited : Inhabited stability :=
  populate Stable.

Class BqueueSpscG Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] bqueue_spsc۰G۰model۰G :: AuthTwinsG Σ (leibnizO (list val)) suffix
  ; #[local] bqueue_spsc۰G۰history۰G :: MonoListG Σ val
  ; #[local] bqueue_spsc۰G۰stability۰G :: TwinsG Σ (leibnizO stability)
  ; #[local] bqueue_spsc۰G۰mono_nat۰G :: AuthNatMaxG Σ
  }.

Definition bqueue_spsc۰Σ :=
  #[auth_twins۰Σ (leibnizO (list val)) suffix
  ; mono_list۰Σ val
  ; twins۰Σ (leibnizO stability)
  ; auth_nat_max۰Σ
  ].
#[global] Instance subGｰbqueue_spsc۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG bqueue_spsc۰Σ Σ →
  BqueueSpscG Σ.

Section bqueue_spsc۰G.
  Context `{bqueue_spsc۰G : BqueueSpscG Σ}.

  Record metadata :=
    { metadata۰capacity : nat
    ; metadata۰data : val
    ; metadata۰inv : namespace
    ; metadata۰model : auth_twins۰name
    ; metadata۰history : gname
    ; metadata۰producer : gname
    ; metadata۰back : gname
    ; metadata۰consumer : 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 :=
    auth_twins۰twin₁ (auth_twins۰G := bqueue_spsc۰G۰model۰G) _ γ_model vs.
  #[local] Definition model₁ γ :=
    model₁' γ.(metadata۰model).
  #[local] Definition model₂' γ_model vs :=
    auth_twins۰twin₂ (auth_twins۰G := bqueue_spsc۰G۰model۰G) _ γ_model vs.
  #[local] Definition model₂ γ :=
    model₂' γ.(metadata۰model).

  #[local] Definition history۰auth' γ_history :=
    mono_list۰auth γ_history (DfracOwn 1).
  #[local] Definition history۰auth γ :=
    history۰auth' γ.(metadata۰history).
  #[local] Definition history۰at γ :=
    mono_list۰at γ.(metadata۰history).

  #[local] Definition producer₁' γ_producer γ_back γ_model stable back ws : iProp Σ :=
    twins۰twin₁ γ_producer (DfracOwn 1) stable ∗
    auth_nat_max۰auth γ_back (DfracOwn (1/2)) back ∗
    auth_twins۰auth _ (auth_twins۰G := bqueue_spsc۰G۰model۰G) γ_model ws.
  #[local] Definition producer₁ γ :=
    producer₁' γ.(metadata۰producer) γ.(metadata۰back) γ.(metadata۰model).
  #[local] Instance : CustomIpat "producer₁" :=
    " ( Hproducer₁ & Hback_auth₁ & Hmodel_auth ) ".
  #[local] Definition producer₂' γ_producer γ_back stable back : iProp Σ :=
    twins۰twin₂ γ_producer stable ∗
    auth_nat_max۰auth γ_back (DfracOwn (1/2)) back.
  #[local] Definition producer₂ γ :=
    producer₂' γ.(metadata۰producer) γ.(metadata۰back).
  #[local] Instance : CustomIpat "producer₂" :=
    " ( Hproducer₂ & Hback_auth₂ ) ".
  #[local] Definition back۰lb γ :=
    auth_nat_max۰lb γ.(metadata۰back).

  #[local] Definition consumer₁' γ_consumer γ_front stable front : iProp Σ :=
    twins۰twin₁ γ_consumer (DfracOwn 1) stable ∗
    auth_nat_max۰auth γ_front (DfracOwn (1/2)) front.
  #[local] Definition consumer₁ γ :=
    consumer₁' γ.(metadata۰consumer) γ.(metadata۰front).
  #[local] Instance : CustomIpat "consumer₁" :=
    " ( Hconsumer₁ & Hfront_auth₁ ) ".
  #[local] Definition consumer₂' γ_consumer γ_front stable front : iProp Σ :=
    twins۰twin₂ γ_consumer stable ∗
    auth_nat_max۰auth γ_front (DfracOwn (1/2)) front.
  #[local] Definition consumer₂ γ :=
    consumer₂' γ.(metadata۰consumer) γ.(metadata۰front).
  #[local] Instance : CustomIpat "consumer₂" :=
    " ( Hconsumer₂ & Hfront_auth₂ ) ".
  #[local] Definition front۰lb γ :=
    auth_nat_max۰lb γ.(metadata۰front).

  #[local] Definition inv۰inner l γ : iProp Σ :=
    ∃ cstable front pstable back vs hist,
    ⌜back = (front + length vs)%nat⌝ ∗
    ⌜back ≤ front + γ.(metadata۰capacity)⌝ ∗
    ⌜length hist = back⌝ ∗
    ⌜vs = drop front hist⌝ ∗
    l.[front] ↦ #front ∗
    consumer₂ γ cstable front ∗
    l.[back] ↦ #back ∗
    producer₂ γ pstable back ∗
    model₂ γ vs ∗
    history۰auth γ hist ∗
    ( if cstable then
        array۰cslice γ.(metadata۰data) γ.(metadata۰capacity) front (DfracOwn 1) ((λ v, ‘Some( v )%V) <$> take 1 vs)
      else
        True
    ) ∗
    array۰cslice γ.(metadata۰data) γ.(metadata۰capacity) ˖front (DfracOwn 1) ((λ v, ‘Some( v )%V) <$> drop 1 vs) ∗
    ( if pstable then
        array۰cslice γ.(metadata۰data) γ.(metadata۰capacity) back (DfracOwn 1) (if decide (back = front + γ.(metadata۰capacity)) then [] else [§None%V])
      else
        True
    ) ∗
    array۰cslice γ.(metadata۰data) γ.(metadata۰capacity) ˖back (DfracOwn 1) (replicate (γ.(metadata۰capacity) - (back - front) - 1) §None%V).
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %cstable{} & %front{} & %pstable{} & %back{} & %vs{} & %hist{} & >%Hback{} & >%Hback{}_le & >%Hhist{}_len & >%Hvs{} & >Hl_front & >Hconsumer₂ & >Hl_back & >Hproducer₂ & >Hmodel₂ & >Hhistory_auth & >Hfront & >Hvs & >Hback & >Hextra ) ".
  #[local] Definition inv' l γ : iProp Σ :=
    l ↪ γ ∗
    l.[data] ↦□ γ.(metadata۰data) ∗
    array۰inv γ.(metadata۰data) γ.(metadata۰capacity) ∗
    inv γ.(metadata۰inv) (inv۰inner l γ).
  #[local] Instance : CustomIpat "inv'" :=
    " ( #Hmeta{_{}} & #Hl_data & #Hdata_inv & #Hinv ) ".
  Definition bqueue_spsc۰inv t ι cap : iProp Σ :=
    ∃ l γ,
    ⌜t = #l⌝ ∗
    ⌜ι = γ.(metadata۰inv)⌝ ∗
    ⌜cap = γ.(metadata۰capacity)⌝ ∗
    inv' l γ.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l{} & %γ{} & {%Heq{};->} & -> & -> & (:inv') ) ".

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

  Definition bqueue_spsc۰producer t ws : iProp Σ :=
    ∃ l γ front_cache back,
    ⌜t = #l⌝ ∗
    l ↪ γ ∗
    l.[front_cache] ↦ #front_cache ∗
    producer₁ γ Stable back ws ∗
    front۰lb γ front_cache.
  #[local] Instance : CustomIpat "producer" :=
    " ( %l{;_} & %γ{;_} & %front_cache & %back & %Heq{} & #Hmeta_{} & Hl_front_cache & Hproducer₁ & #Hfront_lb ) ".

  Definition bqueue_spsc۰consumer t : iProp Σ :=
    ∃ l γ front back_cache,
    ⌜t = #l⌝ ∗
    l ↪ γ ∗
    l.[back_cache] ↦ #back_cache ∗
    consumer₁ γ Stable front ∗
    back۰lb γ back_cache.
  #[local] Instance : CustomIpat "consumer" :=
    " ( %l{;_} & %γ{;_} & %front & %back_cache & %Heq{} & #Hmeta_{} & Hl_back_cache & Hconsumer₁ & #Hback_lb ) ".

  #[global] Instance bqueue_spsc۰invｰpersistent t ι cap :
    Persistent (bqueue_spsc۰inv t ι cap).
  #[global] Instance bqueue_spsc۰modelｰtimeless t vs :
    Timeless (bqueue_spsc۰model t vs).
  #[local] Instance producer₂ｰtimeless γ stable back :
    Timeless (producer₂ γ stable back).
  #[global] Instance bqueue_spsc۰producerｰtimeless t ws :
    Timeless (bqueue_spsc۰producer t ws).
  #[local] Instance consumer₂ｰtimeless γ stable front :
    Timeless (consumer₂ γ stable front).
  #[global] Instance bqueue_spsc۰consumerｰtimeless t :
    Timeless (bqueue_spsc۰consumer t).

  #[local] Lemma modelｰproducerｰalloc :
    ⊢ |==>
      ∃ γ_model γ_producer γ_back,
      model₁' γ_model [] ∗
      model₂' γ_model [] ∗
      producer₁' γ_producer γ_back γ_model Stable 0 [] ∗
      producer₂' γ_producer γ_back Stable 0.
  #[local] Lemma modelｰvalid γ stable back ws vs :
    producer₁ γ stable back ws -∗
    model₁ γ vs -∗
    ⌜vs `suffix_of` ws⌝.
  #[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ｰpush {γ stable back ws vs1 vs2} v :
    producer₁ γ stable back ws -∗
    model₁ γ vs1 -∗
    model₂ γ vs2 ==∗
      producer₁ γ stable back (vs1 ++ [v]) ∗
      model₁ γ (vs1 ++ [v]) ∗
      model₂ γ (vs1 ++ [v]).
  #[local] Lemma modelｰpop γ v vs1 vs2 :
    model₁ γ (v :: vs1) -∗
    model₂ γ vs2 ==∗
      model₁ γ vs1 ∗
      model₂ γ vs1.

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

  #[local] Lemma producerｰagree γ stable1 back1 ws stable2 back2 :
    producer₁ γ stable1 back1 ws -∗
    producer₂ γ stable2 back2 -∗
      ⌜stable1 = stable2⌝ ∗
      ⌜back1 = back2⌝.
  #[local] Lemma producerｰupdateｰstability {γ stable1 back1 ws stable2 back2} stable :
    producer₁ γ stable1 back1 ws -∗
    producer₂ γ stable2 back2 ==∗
      producer₁ γ stable back1 ws ∗
      producer₂ γ stable back2.
  #[local] Lemma producerｰupdateｰback {γ stable1 back1 ws stable2 back2} back :
    back1 ≤ back →
    producer₁ γ stable1 back1 ws -∗
    producer₂ γ stable2 back2 ==∗
      producer₁ γ stable1 back ws ∗
      producer₂ γ stable2 back.
  #[local] Lemma back۰lbｰget γ stable back :
    producer₂ γ stable back ⊢
    back۰lb γ back.
  #[local] Lemma back۰lbｰvalid γ stable back1 back2 :
    producer₂ γ stable back1 -∗
    back۰lb γ back2 -∗
    ⌜back2 ≤ back1⌝.

  #[local] Lemma consumerｰalloc :
    ⊢ |==>
      ∃ γ_consumer γ_front,
      consumer₁' γ_consumer γ_front Stable 0 ∗
      consumer₂' γ_consumer γ_front Stable 0.
  #[local] Lemma consumerｰagree γ stable1 front1 stable2 front2 :
    consumer₁ γ stable1 front1 -∗
    consumer₂ γ stable2 front2 -∗
      ⌜stable1 = stable2⌝ ∗
      ⌜front1 = front2⌝.
  #[local] Lemma consumerｰupdateｰfront {γ stable1 front1 stable2 front2} front :
    front1 ≤ front →
    consumer₁ γ stable1 front1 -∗
    consumer₂ γ stable2 front2 ==∗
      consumer₁ γ stable1 front ∗
      consumer₂ γ stable2 front.
  #[local] Lemma consumerｰupdateｰstability {γ stable1 front1 stable2 front2} stable :
    consumer₁ γ stable1 front1 -∗
    consumer₂ γ stable2 front2 ==∗
      consumer₁ γ stable front1 ∗
      consumer₂ γ stable front2.
  #[local] Lemma front۰lbｰget γ stable front :
    consumer₂ γ stable front ⊢
    front۰lb γ front.
  #[local] Lemma front۰lbｰvalid γ stable front1 front2 :
    consumer₂ γ stable front1 -∗
    front۰lb γ front2 -∗
    ⌜front2 ≤ front1⌝.

  Opaque producer₁'.
  Opaque producer₂'.
  Opaque consumer₁'.
  Opaque consumer₂'.

  Lemma bqueue_spsc۰modelｰvalid t ι cap vs :
    bqueue_spsc۰inv t ι cap -∗
    bqueue_spsc۰model t vs -∗
    ⌜length vs ≤ cap⌝.
  Lemma bqueue_spsc۰modelｰexclusive t vs1 vs2 :
    bqueue_spsc۰model t vs1 -∗
    bqueue_spsc۰model t vs2 -∗
    False.

  Lemma bqueue_spsc۰producerｰexclusive t ws :
    bqueue_spsc۰producer t ws -∗
    bqueue_spsc۰producer t ws -∗
    False.
  Lemma bqueue_spscｰproducerｰmodel t ws vs :
    bqueue_spsc۰producer t ws -∗
    bqueue_spsc۰model t vs -∗
    ⌜vs `suffix_of` ws⌝.

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

  #[local] Instance hintｰarray۰csliceｰnil t cap i dq :
    HINT ε₁ ✱ [- ;
      array۰inv t cap
    ] ⊫ [id];
      array۰cslice t cap i dq []
    ✱ [
      emp
    ].

  Lemma bqueue_spsc٠createｰspec ι cap :
    (0 ≤ cap)%Z →
    {{{
      True
    }}}
      bqueue_spsc٠create #cap
    {{{
      t
    , RET t;
      bqueue_spsc۰inv t ι ₊cap ∗
      bqueue_spsc۰model t [] ∗
      bqueue_spsc۰producer t [] ∗
      bqueue_spsc۰consumer t
    }}}.

  Lemma bqueue_spsc٠capacityｰspec t ι cap :
    {{{
      bqueue_spsc۰inv t ι cap
    }}}
      bqueue_spsc٠capacity t
    {{{
      RET #cap;
      True
    }}}.

  #[local] Lemma frontｰspec l γ stable front :
    {{{
      inv' l γ ∗
      consumer₁ γ stable front
    }}}
      (#l).{front}
    {{{
      RET #front;
      consumer₁ γ stable front
    }}}.

  #[local] Lemma backｰspec l γ stable back ws :
    {{{
      inv' l γ ∗
      producer₁ γ stable back ws
    }}}
      (#l).{back}
    {{{
      RET #back;
      producer₁ γ stable back ws
    }}}.

  Lemma bqueue_spsc٠sizeｰspecｰproducer t ι cap ws :
    <<<
      bqueue_spsc۰inv t ι cap ∗
      bqueue_spsc۰producer t ws
    | ∀∀ vs,
      bqueue_spsc۰model t vs
    >>>
      bqueue_spsc٠size t @ ↑ι
    <<<
      bqueue_spsc۰model t vs
    | RET #(length vs);
      bqueue_spsc۰producer t ws
    >>>.
  Lemma bqueue_spsc٠sizeｰspecｰconsumer t ι cap :
    <<<
      bqueue_spsc۰inv t ι cap ∗
      bqueue_spsc۰consumer t
    | ∀∀ vs,
      bqueue_spsc۰model t vs
    >>>
      bqueue_spsc٠size t @ ↑ι
    <<<
      bqueue_spsc۰model t vs
    | RET #(length vs);
      bqueue_spsc۰consumer t
    >>>.

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

  #[local] Definition push۰au l γ v Ψ : iProp Σ :=
    AU <{
      ∃∃ vs,
      bqueue_spsc۰model #l vs
    }> @ ⊤ ∖ ↑γ.(metadata۰inv), ∅ <{
      ∀∀ b,
      ⌜b = bool_decide (length vs = γ.(metadata۰capacity))⌝ ∗
      bqueue_spsc۰model #l (if b then vs else vs ++ [v]),
    COMM
      Ψ vs b
    }>.
  #[local] Lemma bqueue_spsc٠push₁ｰspec l γ front_cache stable back ws v Ψ :
    {{{
      inv' l γ ∗
      l.[front_cache] ↦ #front_cache ∗
      producer₁ γ stable back ws ∗
      front۰lb γ front_cache ∗
      push۰au l γ v Ψ
    }}}
      bqueue_spsc٠push₁ #l γ.(metadata۰data) #back
    {{{
      b front_cache
    , RET #b;
      ⌜b = bool_decide (back < front_cache + γ.(metadata۰capacity))⌝ ∗
      l.[front_cache] ↦ #front_cache ∗
      producer₁ γ stable back ws ∗
      front۰lb γ front_cache ∗
      if b then
        push۰au l γ v Ψ
      else
        ∃ vs,
        ⌜length vs = γ.(metadata۰capacity)⌝ ∗
        Ψ vs true
    }}}.
  Lemma bqueue_spsc٠pushｰspec t ι cap ws v :
    <<<
      bqueue_spsc۰inv t ι cap ∗
      bqueue_spsc۰producer t ws
    | ∀∀ vs,
      bqueue_spsc۰model t vs
    >>>
      bqueue_spsc٠push t v @ ↑ι
    <<<
      ∃∃ b,
      ⌜b = bool_decide (length vs = cap)⌝ ∗
      bqueue_spsc۰model t (if b then vs else vs ++ [v])
    | RET #b;
      bqueue_spsc۰producer t (if b then ws else vs ++ [v])
    >>>.

  #[local] Definition pop۰au l γ Ψ : iProp Σ :=
    AU <{
      ∃∃ vs,
      bqueue_spsc۰model #l vs
    }> @ ⊤ ∖ ↑γ.(metadata۰inv), ∅ <{
      bqueue_spsc۰model #l (tail vs),
    COMM
      bqueue_spsc۰consumer #l -∗
      Ψ (head vs : val)
    }>.
  #[local] Lemma bqueue_spsc٠pop₁ｰspec l γ back_cache stable front Ψ :
    {{{
      inv' l γ ∗
      l.[back_cache] ↦ #back_cache ∗
      consumer₁ γ stable front ∗
      back۰lb γ back_cache ∗
      pop۰au l γ Ψ
    }}}
      bqueue_spsc٠pop₁ #l #front
    {{{
      b back_cache
    , RET #b;
      ⌜b = bool_decide (front < back_cache)⌝ ∗
      l.[back_cache] ↦ #back_cache ∗
      consumer₁ γ stable front ∗
      back۰lb γ back_cache ∗
      if b then
        pop۰au l γ Ψ
      else
        bqueue_spsc۰consumer #l -∗
        Ψ None
    }}}.
  Lemma bqueue_spsc٠popｰspec t ι cap :
    <<<
      bqueue_spsc۰inv t ι cap ∗
      bqueue_spsc۰consumer t
    | ∀∀ vs,
      bqueue_spsc۰model t vs
    >>>
      bqueue_spsc٠pop t @ ↑ι
    <<<
      bqueue_spsc۰model t (tail vs)
    | RET head vs;
      bqueue_spsc۰consumer t
    >>>.
End bqueue_spsc۰G.

Require zoo_saturn.bqueue_spsc__opaque.

#[global] Opaque bqueue_spsc۰inv.
#[global] Opaque bqueue_spsc۰model.
#[global] Opaque bqueue_spsc۰producer.
#[global] Opaque bqueue_spsc۰consumer.