Library zoo_parabs.ws_hub_fifo

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.ghost_list.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.ws_hub_fifo__code.
Require Import zoo_parabs.ws_hub_fifo__types.
Require Import zoo.options.

Implicit Type b closed : bool.
Implicit Type num_active : Z.
Implicit Type 𝑡 : location.
Implicit Type v t notification notify pred : val.
Implicit Type ws : list val.
Implicit Type vs : gmultiset val.
Implicit Type status : status.
Implicit Type empty : emptiness.
Implicit Type emptys : list emptiness.

Class WsHubFifoG Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] ws_hub_fifo۰G۰queue۰G :: QueueMpmc1G Σ
  ; #[local] ws_hub_fifo۰G۰waiters۰G :: WaitersG Σ
  ; #[local] ws_hub_fifo۰G۰owner۰G :: ExclG Σ unitO
  ; #[local] ws_hub_fifo۰G۰emptiness۰G :: GhostListG Σ emptiness
  }.

Definition ws_hub_fifo۰Σ :=
  #[queue_mpmc_1۰Σ
  ; waiters۰Σ
  ; excl۰Σ unitO
  ; ghost_list۰Σ emptiness
  ].
#[global] Instance subGｰws_hub_fifo۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG ws_hub_fifo۰Σ Σ →
  WsHubFifoG Σ.

Section consistent.
  #[local] Definition consistent vs ws :=
    vs = list_to_set_disj ws.

  #[local] Lemma consistentｰnilｰinv vs :
    consistent vs [] →
    vs = ∅.

  #[local] Lemma consistentｰpush {vs ws} v :
    consistent vs ws →
    consistent ({[+v+]} ⊎ vs) (ws ++ [v]).
  #[local] Lemma consistentｰpop vs v ws :
    consistent vs (v :: ws) →
      ∃ vs',
      vs = {[+v+]} ⊎ vs' ∧
      consistent vs' ws.
End consistent.

Opaque consistent.

Section ws_hub_fifo۰G.
  Context `{ws_hub_fifo۰G : WsHubFifoG Σ}.

  Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.

  Record metadata :=
    { metadata۰size : nat
    ; metadata۰queue : val
    ; metadata۰waiters : val
    ; metadata۰owners : list gname
    ; metadata۰emptiness : gname
    }.
  Implicit Type γ : metadata.
  Implicit Type γ_owners : list gname.

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

  #[local] Definition owner' γ_owners sz i : iProp Σ :=
    ∃ γ_owner,
    ⌜γ_owners !! i = Some γ_owner⌝ ∗
    ⌜length γ_owners = sz⌝ ∗
    excl γ_owner ().
  #[local] Definition owner γ i :=
    owner' γ.(metadata۰owners) γ.(metadata۰size) i.
  #[local] Instance : CustomIpat "owner_" :=
    " ( %γ_owner{} & %Hlookup{} & %Hlength{_{}} & Howner{} ) ".

  #[local] Definition emptiness۰auth' γ_emptiness sz vs : iProp Σ :=
    ∃ emptys,
    ghost_list۰auth γ_emptiness emptys ∗
    ⌜length emptys = sz⌝ ∗
    ⌜ vs = ∅
    ∨ ∃ i,
      emptys !! i = Some Nonempty
    ⌝.
  #[local] Definition emptiness۰auth γ :=
    emptiness۰auth' γ.(metadata۰emptiness) γ.(metadata۰size).
  #[local] Instance : CustomIpat "emptiness۰auth" :=
    " ( %emptys & Hauth & %Hemptys & %Hemptiness ) ".
  #[local] Definition emptiness۰at' γ_emptiness i :=
    ghost_list۰at γ_emptiness i (DfracOwn 1).
  #[local] Definition emptiness۰at γ :=
    emptiness۰at' γ.(metadata۰emptiness).

  #[local] Definition inv۰inner 𝑡 : iProp Σ :=
    ∃ num_active,
    𝑡.[num_active] ↦ #num_active.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %num_active & H𝑡_num_active ) ".
  Definition ws_hub_fifo۰inv t ι (sz : nat) : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    ⌜sz = γ.(metadata۰size)⌝ ∗
    𝑡 ↪ γ ∗
    𝑡.[size] ↦□ #γ.(metadata۰size) ∗
    𝑡.[queue] ↦□ γ.(metadata۰queue) ∗
    𝑡.[waiters] ↦□ γ.(metadata۰waiters) ∗
    queue_mpmc_1۰inv γ.(metadata۰queue) ι ∗
    waiters۰inv γ.(metadata۰waiters) sz ∗
    inv nroot (inv۰inner 𝑡).
  #[local] Instance : CustomIpat "inv" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & -> & #Hmeta{} & #H𝑡{}_size & #H𝑡{}_queue & #H𝑡{}_waiters & #Hqueue{}_inv & #Hwaiters{}_inv & #Hinv{} ) ".

  Definition ws_hub_fifo۰model t vs : iProp Σ :=
    ∃ 𝑡 γ ws,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    queue_mpmc_1۰model γ.(metadata۰queue) ws ∗
    ⌜consistent vs ws⌝ ∗
    emptiness۰auth γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %l_ & %γ_ & %ws & %Heq & Hmeta_ & Hqueue_model & %Hconsistent & Hemptiness_auth ) ".

  Definition ws_hub_fifo۰owner t i status empty : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    owner γ i ∗
    emptiness۰at γ i empty.
  #[local] Instance : CustomIpat "owner" :=
    " ( %𝑡{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Howner{_{}} & Hemptiness_at{_{}} ) ".

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

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

  #[local] Lemma ownerｰalloc sz :
    ⊢ |==>
      ∃ γ_owners,
      [∗ list] i ∈ seq 0 sz,
        owner' γ_owners sz i.
  #[local] Lemma ownerｰvalid γ i :
    owner γ i ⊢
    ⌜i < γ.(metadata۰size)⌝.
  #[local] Lemma ownerｰexclusive γ i :
    owner γ i -∗
    owner γ i -∗
    False.

  Opaque owner'.

  #[local] Lemma emptinessｰalloc sz :
    ⊢ |==>
      ∃ γ_emptiness,
      emptiness۰auth' γ_emptiness sz ∅ ∗
      [∗ list] i ∈ seq 0 sz,
        emptiness۰at' γ_emptiness i Empty.
  #[local] Lemma emptiness۰atｰvalid γ vs i empty :
    emptiness۰auth γ vs -∗
    emptiness۰at γ i empty -∗
    ⌜i < γ.(metadata۰size)⌝.
  #[local] Lemma emptinessｰempty γ vs :
    emptiness۰auth γ vs -∗
    ( [∗ list] i ∈ seq 0 γ.(metadata۰size),
      emptiness۰at γ i Empty
    ) -∗
    ⌜vs = ∅⌝.
  #[local] Lemma emptinessｰupdateｰauth γ v vs :
    emptiness۰auth γ ({[+v+]} ⊎ vs) ⊢
    emptiness۰auth γ vs.
  #[local] Lemma emptinessｰupdateｰNonempty {γ vs i empty} vs' :
    emptiness۰auth γ vs -∗
    emptiness۰at γ i empty ==∗
      emptiness۰auth γ vs' ∗
      emptiness۰at γ i Nonempty.
  #[local] Lemma emptinessｰupdateｰEmpty γ i empty :
    emptiness۰auth γ ∅ -∗
    emptiness۰at γ i empty ==∗
      emptiness۰auth γ ∅ ∗
      emptiness۰at γ i Empty.

  Opaque emptiness۰auth'.

  Lemma ws_hub_fifo۰invｰagree t ι sz1 sz2 :
    ws_hub_fifo۰inv t ι sz1 -∗
    ws_hub_fifo۰inv t ι sz2 -∗
    ⌜sz1 = sz2⌝.

  Lemma ws_hub_fifo۰ownerｰexclusive t i status1 empty1 status2 empty2 :
    ws_hub_fifo۰owner t i status1 empty1 -∗
    ws_hub_fifo۰owner t i status2 empty2 -∗
    False.

  Lemma ws_hub_fifoｰinvｰowner t ι sz i status empty :
    ws_hub_fifo۰inv t ι sz -∗
    ws_hub_fifo۰owner t i status empty -∗
    ⌜i < sz⌝.

  Lemma ws_hub_fifo۰modelｰempty t ι sz vs :
    ws_hub_fifo۰inv t ι sz -∗
    ws_hub_fifo۰model t vs -∗
    ( [∗ list] i ∈ seq 0 sz,
      ∃ status,
      ws_hub_fifo۰owner t i status Empty
    ) -∗
    ⌜vs = ∅⌝.

  Lemma ws_hub_fifo٠createｰspec ι sz :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      ws_hub_fifo٠create #sz
    {{{
      t
    , RET t;
      ws_hub_fifo۰inv t ι ₊sz ∗
      ws_hub_fifo۰model t ∅ ∗
      [∗ list] i ∈ seq 0 ₊sz,
        ws_hub_fifo۰owner t i Nonblocked Empty
    }}}.

  Lemma ws_hub_fifo٠sizeｰspec t ι sz :
    {{{
      ws_hub_fifo۰inv t ι sz
    }}}
      ws_hub_fifo٠size t
    {{{
      RET #sz;
      True
    }}}.

  #[local] Lemma ws_hub_fifo٠begin_inactiveｰspec t ι sz :
    {{{
      ws_hub_fifo۰inv t ι sz
    }}}
      ws_hub_fifo٠begin_inactive t
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma ws_hub_fifo٠end_inactiveｰspec t ι sz :
    {{{
      ws_hub_fifo۰inv t ι sz
    }}}
      ws_hub_fifo٠end_inactive t
    {{{
      RET ();
      True
    }}}.

  Lemma ws_hub_fifo٠blockｰspec t ι sz i i_ empty :
    i = ⁺i_ →
    {{{
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Nonblocked empty
    }}}
      ws_hub_fifo٠block t #i
    {{{
      RET ();
      ws_hub_fifo۰owner t i_ Blocked empty
    }}}.

  Lemma ws_hub_fifo٠unblockｰspec t ι sz i i_ empty :
    i = ⁺i_ →
    {{{
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Blocked empty
    }}}
      ws_hub_fifo٠unblock t #i
    {{{
      RET ();
      ws_hub_fifo۰owner t i_ Nonblocked empty
    }}}.

  Lemma ws_hub_fifo٠closedｰspec t ι sz :
    {{{
      ws_hub_fifo۰inv t ι sz
    }}}
      ws_hub_fifo٠closed t
    {{{
      closed
    , RET #closed;
      True
    }}}.

  #[local] Lemma ws_hub_fifo٠notifyｰspec t ι sz :
    {{{
      ws_hub_fifo۰inv t ι sz
    }}}
      ws_hub_fifo٠notify t
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma ws_hub_fifo٠notify_allｰspec t ι sz :
    {{{
      ws_hub_fifo۰inv t ι sz
    }}}
      ws_hub_fifo٠notify_all t
    {{{
      RET ();
      True
    }}}.

  Lemma ws_hub_fifo٠pushｰspec t ι sz i i_ empty v :
    i = ⁺i_ →
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Nonblocked empty
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠push t #i v @ ↑ι
    <<<
      ws_hub_fifo۰model t ({[+v+]} ⊎ vs)
    | RET ();
      ws_hub_fifo۰owner t i_ Nonblocked Nonempty
    >>>.

  #[local] Lemma ws_hub_fifo٠pop'ｰspecｰaux (owner : option (nat × emptiness)) t ι sz :
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      match owner with
      | None ⇒
          True
      | Some (i, empty) ⇒
          ws_hub_fifo۰owner t i Nonblocked empty
      end
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠pop' t @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | RET o;
      match owner with
      | None ⇒
          True
      | Some (i, empty) ⇒
          ws_hub_fifo۰owner t i Nonblocked (if o then empty else Empty)
      end
    >>>.
  #[local] Lemma ws_hub_fifo٠pop'ｰspec t ι sz :
    <<<
      ws_hub_fifo۰inv t ι sz
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠pop' t @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | RET o;
      True
    >>>.
  #[local] Lemma ws_hub_fifo٠pop'ｰspecｰowner t ι sz i empty :
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i Nonblocked empty
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠pop' t @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | RET o;
      ws_hub_fifo۰owner t i Nonblocked (if o then empty else Empty)
    >>>.

  Lemma ws_hub_fifo٠popｰspec t ι sz i i_ empty :
    i = ⁺i_ →
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Nonblocked empty
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠pop t #i @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | RET o;
      ws_hub_fifo۰owner t i_ Nonblocked (if o then empty else Empty)
    >>>.

  #[local] Lemma ws_hub_fifo٠steal_auxｰspec P_notification P_pred Q_pred t ι (sz : nat) i notification pred :
    (0 ≤ i < sz)%Z →
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      P_notification ∗
      ( ∀ notify,
        P_notification -∗
        WP notify () {{ itype۰unit }} -∗
        WP notification notify {{ res,
          ⌜res = ()%V⌝ ∗
          P_notification
        }}
      ) ∗
      P_pred ∗
      □ (
        P_pred -∗
        WP pred () {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          if b then Q_pred else P_pred
        }}
      )
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠steal_aux t #i notification pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | RET o;
      P_notification ∗
      if o then P_pred else Q_pred
    >>>.

  Lemma ws_hub_fifo٠steal_untilｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
    i = ⁺i_ →
    (0 ≤ max_round_noyield)%Z →
    (0 ≤ max_round_yield)%Z →
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Nonblocked empty ∗
      P_notification ∗
      ( ∀ notify,
        P_notification -∗
        WP notify () {{ itype۰unit }} -∗
        WP notification notify {{ res,
          ⌜res = ()%V⌝ ∗
          P_notification
        }}
      ) ∗
      P_pred ∗
      □ (
        P_pred -∗
        WP pred () {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          if b then Q_pred else P_pred
        }}
      )
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | RET o;
      ws_hub_fifo۰owner t i_ Nonblocked empty ∗
      P_notification ∗
      if o then P_pred else Q_pred
    >>>.

  Lemma ws_hub_fifo٠stealｰspec t ι sz i i_ empty max_round_noyield max_round_yield :
    i = ⁺i_ →
    (0 ≤ max_round_noyield)%Z →
    (0 ≤ max_round_yield)%Z →
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Nonblocked empty
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠steal t #i #max_round_noyield #max_round_yield @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | RET o;
      ws_hub_fifo۰owner t i_ (if o then Nonblocked else Blocked) empty
    >>>.

  Lemma ws_hub_fifo٠closeｰspec t ι sz :
    {{{
      ws_hub_fifo۰inv t ι sz
    }}}
      ws_hub_fifo٠close t
    {{{
      RET ();
      True
    }}}.
End ws_hub_fifo۰G.

#[global] Opaque ws_hub_fifo۰inv.
#[global] Opaque ws_hub_fifo۰model.
#[global] Opaque ws_hub_fifo۰owner.

Section ws_hub_fifo۰G.
  Context `{ws_hub_fifo۰G : WsHubFifoG Σ}.

  Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.

  Lemma ws_hub_fifo٠pop_steal_untilｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
    i = ⁺i_ →
    (0 ≤ max_round_noyield)%Z →
    (0 ≤ max_round_yield)%Z →
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Nonblocked empty ∗
      P_notification ∗
      ( ∀ notify,
        P_notification -∗
        WP notify () {{ itype۰unit }} -∗
        WP notification notify {{ res,
          ⌜res = ()%V⌝ ∗
          P_notification
        }}
      ) ∗
      P_pred ∗
      □ (
        P_pred -∗
        WP pred () {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          if b then Q_pred else P_pred
        }}
      )
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠pop_steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | empty,
      RET o;
      ws_hub_fifo۰owner t i_ Nonblocked empty ∗
      P_notification ∗
      if o then P_pred else Q_pred
    >>>.

  Lemma ws_hub_fifo٠pop_stealｰspec t ι sz i i_ empty max_round_noyield max_round_yield :
    i = ⁺i_ →
    (0 ≤ max_round_noyield)%Z →
    (0 ≤ max_round_yield)%Z →
    <<<
      ws_hub_fifo۰inv t ι sz ∗
      ws_hub_fifo۰owner t i_ Nonblocked empty
    | ∀∀ vs,
      ws_hub_fifo۰model t vs
    >>>
      ws_hub_fifo٠pop_steal t #i #max_round_noyield #max_round_yield @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_fifo۰model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_fifo۰model t vs'
      end
    | empty,
      RET o;
      ws_hub_fifo۰owner t i_ (if o then Nonblocked else Blocked) empty ∗
      if o then
        True
      else
        ⌜empty = Empty⌝
    >>>.
End ws_hub_fifo۰G.

Require zoo_parabs.ws_hub_fifo__opaque.