Library zoo_parabs.ws_hub_hybrid

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable
  gmultiset
  list.
From zoo.iris.bi Require Import
  big_op.
From zoo.iris.base_logic Require Import
  lib.ghost_list.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  int
  option
  optional
  array
  random_round
  domain.
From zoo_saturn Require Import
  mpmc_queue_1.
From zoo_parabs Require Export
  base
  ws_hub_hybrid__code.
From zoo_parabs Require Import
  ws_hub_hybrid__types
  ws_bdeques_public
  waiters.
From zoo Require Import
  options.

Implicit Types b yield closed : bool.
Implicit Types num_active : Z.
Implicit Types 𝑡 : location.
Implicit Types v t notification notify pred : val.
Implicit Types vs : gmultiset val.
Implicit Types ws us vs_queue : list val.
Implicit Types vss : list $ list val.
Implicit Types status : status.
Implicit Types empty : emptiness.

Class WsHubHybridG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] ws_hub_hybrid_G_deques_G :: WsBdequesPublicG Σ
  ; #[local] ws_hub_hybrid_G_queue_G :: MpmcQueue1G Σ
  ; #[local] ws_hub_hybrid_G_waiters_G :: WaitersG Σ
  ; #[local] ws_hub_hybrid_G_emptiness_G :: GhostListG Σ emptiness
  }.

Definition ws_hub_hybrid_Σ :=
  #[ws_bdeques_public_Σ
  ; mpmc_queue_1_Σ
  ; waiters_Σ
  ; ghost_list_Σ emptiness
  ].
#[global] Instance subG_ws_hub_hybrid_Σ Σ `{zoo_G : !ZooG Σ} :
  subG ws_hub_hybrid_Σ Σ →
  WsHubHybridG Σ.

Section consistent.
  #[local] Definition consistent vs vss vs_queue :=
    vs =
      ⋃+ (list_to_set_disj <$> vss) ⊎
      list_to_set_disj vs_queue.

  #[local] Lemma consistent_alloc sz :
    consistent ∅ (replicate sz []) [].

  #[local] Lemma consistent_empty vs vss vs_queue :
    consistent vs vss vs_queue →
    vs = ∅ ↔
      ( ∀ i us,
        vss !! i = Some us →
        us = []
      ) ∧
      vs_queue = [].

  #[local] Lemma consistent_deque_push {vs vss vs_queue i us} v :
    vss !! i = Some us →
    consistent vs vss vs_queue →
    consistent ({[+v+]} ⊎ vs) (<[i := us ++ [v]]> vss) vs_queue.
  #[local] Lemma consistent_deque_remove {vs vss vs_queue i us} us1 v us2 :
    vss !! i = Some us →
    us = us1 ++ v :: us2 →
    consistent vs vss vs_queue →
      ∃ vs',
      vs = {[+v+]} ⊎ vs' ∧
      consistent vs' (<[i := us1 ++ us2]> vss) vs_queue.
  #[local] Lemma consistent_deque_pop vs vss vs_queue i us v :
    vss !! i = Some (us ++ [v]) →
    consistent vs vss vs_queue →
      ∃ vs',
      vs = {[+v+]} ⊎ vs' ∧
      consistent vs' (<[i := us]> vss) vs_queue.
  #[local] Lemma consistent_deque_steal vs vss vs_queue i v us :
    vss !! i = Some (v :: us) →
    consistent vs vss vs_queue →
      ∃ vs',
      vs = {[+v+]} ⊎ vs' ∧
      consistent vs' (<[i := us]> vss) vs_queue.

  #[local] Lemma consistent_queue_push {vs vss vs_queue} v :
    consistent vs vss vs_queue →
    consistent ({[+v+]} ⊎ vs) vss (vs_queue ++ [v]).
  #[local] Lemma consistent_queue_pop vs vss v vs_queue :
    consistent vs vss (v :: vs_queue) →
      ∃ vs',
      vs = {[+v+]} ⊎ vs' ∧
      consistent vs' vss vs_queue.
End consistent.

Opaque consistent.

Section ws_hub_hybrid_G.
  Context `{ws_hub_hybrid_G : WsHubHybridG Σ}.

  Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.

  Record metadata :=
    { metadata_size : nat
    ; metadata_deques : val
    ; metadata_rounds : val
    ; metadata_queue : val
    ; metadata_waiters : val
    ; metadata_emptiness : gname
    }.
  Implicit Types γ : metadata.

  #[local] Instance metadata_eq_dec :
    EqDecision metadata.
  #[local] Instance metadata_countable :
    Countable metadata.

  #[local] Definition emptiness_auth' γ_emptiness sz vs_queue : iProp Σ :=
    ∃ emptys,
    ghost_list_auth γ_emptiness emptys ∗
    ⌜length emptys = sz⌝ ∗
    ⌜ vs_queue = []
    ∨ ∃ 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_hybrid_inv t ι sz : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    ⌜sz = γ.(metadata_size)⌝ ∗
    𝑡.[deques] ↦□ γ.(metadata_deques) ∗
    𝑡.[rounds] ↦□ γ.(metadata_rounds) ∗
    𝑡.[queue] ↦□ γ.(metadata_queue) ∗
    𝑡.[waiters] ↦□ γ.(metadata_waiters) ∗
    ws_bdeques_public_inv γ.(metadata_deques) ι γ.(metadata_size) ∗
    array_inv γ.(metadata_rounds) γ.(metadata_size) ∗
    mpmc_queue_1_inv γ.(metadata_queue) ι ∗
    waiters_inv γ.(metadata_waiters) sz ∗
    inv nroot (inv_inner 𝑡).
  #[local] Instance : CustomIpat "inv" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{} & -> & #H𝑡{}_deques & #H𝑡{}_queue & #H𝑡{}_rounds & #H𝑡{}_waiters & #Hdeques{}_inv & #Hrounds{}_inv & #Hqueue{}_inv & #Hwaiters{}_inv & #Hinv{} ) ".

  Definition ws_hub_hybrid_model t vs : iProp Σ :=
    ∃ 𝑡 γ vss vs_queue,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    ws_bdeques_public_model γ.(metadata_deques) vss ∗
    mpmc_queue_1_model γ.(metadata_queue) vs_queue ∗
    ⌜consistent vs vss vs_queue⌝ ∗
    emptiness_auth γ vs_queue.
  #[local] Instance : CustomIpat "model" :=
    " ( %𝑡_ & %γ_ & %vss & %vs_queue & %Heq & Hmeta_ & Hdeques_model & Hqueue_model & %Hconsistent & Hemptiness_auth ) ".

  Definition ws_hub_hybrid_owner t i status empty : iProp Σ :=
    ∃ 𝑡 γ ws round n,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    ws_bdeques_public_owner γ.(metadata_deques) i status ws ∗
    ⌜empty = Empty → ws = []⌝ ∗
    array_slice γ.(metadata_rounds) i DfracDiscarded [round] ∗
    random_round_model' round (γ.(metadata_size) - 1) n ∗
    emptiness_at γ i empty.
  #[local] Instance : CustomIpat "owner" :=
    " ( %𝑡{;_} & %γ{;_} & %ws{} & %round{} & %n{} & %Heq{} & Hmeta{;_} & Hdeques_owner{} & %Hempty{} & #Hrounds{} & Hround{} & Hemptiness_at{_{}} ) ".

  #[global] Instance ws_hub_hybrid_model_timeless t vs :
    Timeless (ws_hub_hybrid_model t vs).

  #[global] Instance ws_hub_hybrid_inv_persistent t ι sz :
    Persistent (ws_hub_hybrid_inv t ι sz).

  #[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_queue i empty :
    emptiness_auth γ vs_queue -∗
    emptiness_at γ i empty -∗
    ⌜i < γ.(metadata_size)⌝.
  #[local] Lemma emptiness_empty γ vs_queue :
    emptiness_auth γ vs_queue -∗
    ( [∗ list] i ∈ seq 0 γ.(metadata_size),
      emptiness_at γ i Empty
    ) -∗
    ⌜vs_queue = []⌝.
  #[local] Lemma emptiness_update_auth γ v vs_queue :
    emptiness_auth γ (v :: vs_queue) ⊢
    emptiness_auth γ vs_queue.
  #[local] Lemma emptiness_update_Nonempty {γ vs_queue i empty} vs_queue' :
    emptiness_auth γ vs_queue -∗
    emptiness_at γ i empty ==∗
      emptiness_auth γ vs_queue' ∗
      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_hybrid_inv_agree t ι sz1 sz2 :
    ws_hub_hybrid_inv t ι sz1 -∗
    ws_hub_hybrid_inv t ι sz2 -∗
    ⌜sz1 = sz2⌝.

  Lemma ws_hub_hybrid_owner_exclusive t i status1 empty1 status2 empty2 :
    ws_hub_hybrid_owner t i status1 empty1 -∗
    ws_hub_hybrid_owner t i status2 empty2 -∗
    False.

  Lemma ws_hub_hybrid_inv_owner t ι sz i status empty :
    ws_hub_hybrid_inv t ι sz -∗
    ws_hub_hybrid_owner t i status empty -∗
    ⌜i < sz⌝.

  Lemma ws_hub_hybrid_model_empty t ι sz vs :
    ws_hub_hybrid_inv t ι sz -∗
    ws_hub_hybrid_model t vs -∗
    ( [∗ list] i ∈ seq 0 sz,
      ∃ status,
      ws_hub_hybrid_owner t i status Empty
    ) -∗
    ⌜vs = ∅⌝.

  Lemma ws_hub_hybrid٠create𑁒spec ι sz :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      ws_hub_hybrid٠create #sz
    {{{
      t
    , RET t;
      ws_hub_hybrid_inv t ι ₊sz ∗
      ws_hub_hybrid_model t ∅ ∗
      [∗ list] i ∈ seq 0 ₊sz,
        ws_hub_hybrid_owner t i Nonblocked Empty
    }}}.

  Lemma ws_hub_hybrid٠size𑁒spec t ι sz :
    {{{
      ws_hub_hybrid_inv t ι sz
    }}}
      ws_hub_hybrid٠size t
    {{{
      RET #sz;
      True
    }}}.

  #[local] Lemma ws_hub_hybrid٠begin_inactive𑁒spec t ι sz :
    {{{
      ws_hub_hybrid_inv t ι sz
    }}}
      ws_hub_hybrid٠begin_inactive t
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma ws_hub_hybrid٠end_inactive𑁒spec t ι sz :
    {{{
      ws_hub_hybrid_inv t ι sz
    }}}
      ws_hub_hybrid٠end_inactive t
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma ws_hub_hybrid٠block_active𑁒spec t ι sz i i_ empty :
    i = ⁺i_ →
    {{{
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Nonblocked empty
    }}}
      ws_hub_hybrid٠block_active t #i
    {{{
      RET ();
      ws_hub_hybrid_owner t i_ Blocked empty
    }}}.

  #[local] Lemma ws_hub_hybrid٠unblock_active𑁒spec t ι sz i i_ empty :
    i = ⁺i_ →
    {{{
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Blocked empty
    }}}
      ws_hub_hybrid٠unblock_active t #i
    {{{
      RET ();
      ws_hub_hybrid_owner t i_ Nonblocked empty
    }}}.

  Lemma ws_hub_hybrid٠block𑁒spec t ι sz i i_ empty :
    i = ⁺i_ →
    {{{
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Nonblocked empty
    }}}
      ws_hub_hybrid٠block t #i
    {{{
      RET ();
      ws_hub_hybrid_owner t i_ Blocked empty
    }}}.

  Lemma ws_hub_hybrid٠unblock𑁒spec t ι sz i i_ empty :
    i = ⁺i_ →
    {{{
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Blocked empty
    }}}
      ws_hub_hybrid٠unblock t #i
    {{{
      RET ();
      ws_hub_hybrid_owner t i_ Nonblocked empty
    }}}.

  Lemma ws_hub_hybrid٠closed𑁒spec t ι sz :
    {{{
      ws_hub_hybrid_inv t ι sz
    }}}
      ws_hub_hybrid٠closed t
    {{{
      closed
    , RET #closed;
      True
    }}}.

  #[local] Lemma ws_hub_hybrid٠notify𑁒spec t ι sz :
    {{{
      ws_hub_hybrid_inv t ι sz
    }}}
      ws_hub_hybrid٠notify t
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma ws_hub_hybrid٠notify_all𑁒spec t ι sz :
    {{{
      ws_hub_hybrid_inv t ι sz
    }}}
      ws_hub_hybrid٠notify_all t
    {{{
      RET ();
      True
    }}}.

  Lemma ws_hub_hybrid٠push𑁒spec t ι sz i i_ empty v :
    i = ⁺i_ →
    <<<
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Nonblocked empty
    | ∀∀ vs,
      ws_hub_hybrid_model t vs
    >>>
      ws_hub_hybrid٠push t #i v @ ↑ι
    <<<
      ws_hub_hybrid_model t ({[+v+]} ⊎ vs)
    | RET ();
      ws_hub_hybrid_owner t i_ Nonblocked Nonempty
    >>>.

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

  #[local] Lemma ws_hub_hybrid٠try_steal_once𑁒spec t ι sz i i_ empty :
    i = ⁺i_ →
    <<<
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Blocked empty
    | ∀∀ vs,
      ws_hub_hybrid_model t vs
    >>>
      ws_hub_hybrid٠try_steal_once t #i @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_hybrid_model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | RET o;
      ws_hub_hybrid_owner t i_ Blocked empty
    >>>.

  #[local] Lemma ws_hub_hybrid_try_steal₀𑁒spec P Q t ι sz i i_ empty yield max_round pred :
    i = ⁺i_ →
    (0 ≤ max_round)%Z →
    <<<
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Blocked empty ∗
      P ∗
      □ (
        P -∗
        WP pred () {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          if b then Q else P
        }}
      )
    | ∀∀ vs,
      ws_hub_hybrid_model t vs
    >>>
      ws_hub_hybrid٠try_steal₀ t #i #yield #max_round pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | Nothing
      | Anything ⇒
          ws_hub_hybrid_model t vs
      | Something v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | RET o;
      ws_hub_hybrid_owner t i_ Blocked empty ∗
      if o is Anything then Q else P
    >>>.

  #[local] Lemma ws_hub_hybrid٠try_steal𑁒spec P Q t ι sz i i_ empty max_round_noyield max_round_yield pred :
    i = ⁺i_ →
    (0 ≤ max_round_noyield)%Z →
    (0 ≤ max_round_yield)%Z →
    <<<
      ws_hub_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Blocked empty ∗
      P ∗
      □ (
        P -∗
        WP pred () {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          if b then Q else P
        }}
      )
    | ∀∀ vs,
      ws_hub_hybrid_model t vs
    >>>
      ws_hub_hybrid٠try_steal t #i #max_round_noyield #max_round_yield pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | Nothing
      | Anything ⇒
          ws_hub_hybrid_model t vs
      | Something v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | RET o;
      ws_hub_hybrid_owner t i_ Blocked empty ∗
      if o is Anything then Q else P
    >>>.

  #[local] Lemma ws_hub_hybrid٠steal_aux𑁒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_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Blocked 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_hybrid_model t vs
    >>>
      ws_hub_hybrid٠steal_aux t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_hybrid_model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | RET o;
      ws_hub_hybrid_owner t i_ (if o then Nonblocked else Blocked) empty ∗
      P_notification ∗
      if o then P_pred else Q_pred
    >>>.

  Lemma ws_hub_hybrid٠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_hybrid_inv t ι sz ∗
      ws_hub_hybrid_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_hybrid_model t vs
    >>>
      ws_hub_hybrid٠steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_hybrid_model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | RET o;
      ws_hub_hybrid_owner t i_ Nonblocked empty ∗
      P_notification ∗
      if o then P_pred else Q_pred
    >>>.

  Lemma ws_hub_hybrid٠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_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Nonblocked empty
    | ∀∀ vs,
      ws_hub_hybrid_model t vs
    >>>
      ws_hub_hybrid٠steal t #i #max_round_noyield #max_round_yield @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_hybrid_model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | RET o;
      ws_hub_hybrid_owner t i_ (if o then Nonblocked else Blocked) empty
    >>>.

  Lemma ws_hub_hybrid٠close𑁒spec t ι sz :
    {{{
      ws_hub_hybrid_inv t ι sz
    }}}
      ws_hub_hybrid٠close t
    {{{
      RET ();
      True
    }}}.
End ws_hub_hybrid_G.

#[global] Opaque ws_hub_hybrid_inv.
#[global] Opaque ws_hub_hybrid_model.
#[global] Opaque ws_hub_hybrid_owner.

Section ws_hub_hybrid_G.
  Context `{ws_hub_hybrid_G : WsHubHybridG Σ}.

  Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.

  Lemma ws_hub_hybrid٠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_hybrid_inv t ι sz ∗
      ws_hub_hybrid_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_hybrid_model t vs
    >>>
      ws_hub_hybrid٠pop_steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_hybrid_model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | empty,
      RET o;
      ws_hub_hybrid_owner t i_ Nonblocked empty ∗
      P_notification ∗
      if o then P_pred else Q_pred
    >>>.

  Lemma ws_hub_hybrid٠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_hybrid_inv t ι sz ∗
      ws_hub_hybrid_owner t i_ Nonblocked empty
    | ∀∀ vs,
      ws_hub_hybrid_model t vs
    >>>
      ws_hub_hybrid٠pop_steal t #i #max_round_noyield #max_round_yield @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          ws_hub_hybrid_model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = {[+v+]} ⊎ vs'⌝ ∗
          ws_hub_hybrid_model t vs'
      end
    | empty,
      RET o;
      ws_hub_hybrid_owner t i_ (if o then Nonblocked else Blocked) empty ∗
      if o then
        True
      else
        ⌜empty = Empty⌝
    >>>.
End ws_hub_hybrid_G.

From zoo_parabs Require
  ws_hub_hybrid__opaque.