Library zoo_parabs.pool

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.ghost_list.
Require Import zoo.iris.base_logic.lib.mono_gmultiset.
Require Import zoo.iris.base_logic.lib.saved_prop.
Require Import zoo.iris.base_logic.lib.prop_spsc.
Require Import zoo.base.
Require Export zoo_parabs.base.
Require Export zoo_parabs.pool__code.
Require Import zoo_parabs.pool__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type v ctx hub task notification notify pred ivar waiter : val.
Implicit Type empty : emptiness.
Implicit Type own : ownership.
Implicit Type η : prop_spsc ۰ name.
Implicit Type ω : gname.

#[local] Definition max_round_noyield :=
  val ۰ to_nat' pool ٠ max_round_noyield.
#[local] Lemma pool ٠ max_round_noyield ｰ unfold :
  pool ٠ max_round_noyield = #max_round_noyield.
Opaque pool ٠ max_round_noyield.
Opaque max_round_noyield.

#[local] Definition max_round_yield :=
  val ۰ to_nat' pool ٠ max_round_yield.
#[local] Lemma pool ٠ max_round_yield ｰ unfold :
  pool ٠ max_round_yield = #max_round_yield.
Opaque pool ٠ max_round_yield.
Opaque max_round_yield.

Record job :=
  { job ۰ val : val
  ; job ۰ name : gname
  }.
Implicit Type job local global : job.

#[local] Instance job ｰ inhabited : Inhabited job :=
  populate
  {|job ۰ val := inhabitant
  ; job ۰ name := inhabitant
  |}.
#[local] Instance job ｰ eq_dec : EqDecision job :=
  ltac:(solve_decision).
#[local] Instance job ｰ countable :
  Countable job.

Implicit Type jobs locals ulocals globals : gmultiset job.
Implicit Type localss : list $ gmultiset job.

Definition pool ۰ scope :=
  gmultiset job.

#[global] Instance pool ۰ scope ｰ eq_dec : EqDecision pool ۰ scope :=
  _.
#[global] Instance pool ۰ scope ｰ countable :
  Countable pool ۰ scope.

Class PoolG Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] pool ۰ G ۰ domain ۰ G :: DomainG Σ
  ; #[local] pool ۰ G ۰ ws_hub ۰ G :: WsHubStdG Σ
  ; #[local] pool ۰ G ۰ saved_prop ۰ G :: SavedPropG Σ
  ; #[local] pool ۰ G ۰ jobs ۰ G :: MonoGmultisetG Σ job
  ; #[local] pool ۰ G ۰ locals ۰ G :: GhostListG Σ (gmultiset job)
  ; #[local] pool ۰ G ۰ consumer ۰ G :: PropSpscG Σ
  }.

Definition pool ۰ Σ :=
  #[domain ۰ Σ
  ; ws_hub_std ۰ Σ
  ; saved_prop ۰ Σ
  ; mono_gmultiset ۰ Σ job
  ; ghost_list ۰ Σ (gmultiset job)
  ; prop_spsc ۰ Σ
  ].
#[global] Instance subG ｰ pool ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG pool ۰ Σ Σ →
  PoolG Σ.

Module base.
  Section pool ۰ G.
    Context `{pool ۰ G : PoolG Σ}.

    Implicit Type t : location.
    Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.
    Implicit Type Ψ : val → iProp Σ.

    Record pool ۰ name :=
      { pool ۰ name ۰ size : nat
      ; pool ۰ name ۰ hub : val
      ; pool ۰ name ۰ domains : val
      ; pool ۰ name ۰ jobs : gname
      ; pool ۰ name ۰ locals : gname
      }.
    Implicit Type γ : pool ۰ name.
    Implicit Type γ_tokens : list gname.

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

    #[local] Definition pool ۰ name ۰ context γ (i : nat) :=
      ( #γ.(pool ۰ name ۰ size),
        γ.(pool ۰ name ۰ hub),
        #i
      )%V.
    #[local] Instance pool ۰ name ۰ context ｰ inj γ :
      Inj (=) (=) (pool ۰ name ۰ context γ).

    #[local] Definition jobs ۰ auth' γ_jobs own :=
      mono_gmultiset ۰ auth γ_jobs own.
    #[local] Definition jobs ۰ auth γ :=
      jobs ۰ auth' γ.(pool ۰ name ۰ jobs).
    #[local] Definition jobs ۰ elem γ :=
      mono_gmultiset ۰ elem γ.(pool ۰ name ۰ jobs).

    #[local] Definition jobs ۰ finished jobs : iProp Σ :=
      [∗ mset ] job ∈ jobs ,
        ∃ P ,
        saved_prop job.(job ۰ name) P ∗
        □ P.

    #[local] Definition locals ۰ auth' sz γ_locals ulocals : iProp Σ :=
      ∃ localss ,
      ⌜length localss = ˖sz ⌝ ∗
      ghost_list ۰ auth γ_locals localss ∗
      ⌜ulocals = ⋃+ localss ⌝.
    #[local] Definition locals ۰ auth γ :=
      locals ۰ auth' γ.(pool ۰ name ۰ size) γ.(pool ۰ name ۰ locals).
    #[local] Instance : CustomIpat "locals۰auth" :=
      " ( %localss{} & %Hlocalss{} & Hauth{_{}} & -> ) ".
    #[local] Definition locals ۰ at ۰ running γ_locals i scope : iProp Σ :=
      ∃ locals ,
      ghost_list ۰ at γ_locals i Own (scope ⊎ locals) ∗
      jobs ۰ finished locals.
    #[local] Instance : CustomIpat "locals۰at۰running" :=
      " ( %locals{} & Hat{_{}} & Hjobs_finished_locals{} ) ".
    #[local] Definition locals ۰ at ۰ finished γ_locals i : iProp Σ :=
      ∃ locals ,
      ghost_list ۰ at γ_locals i Own locals.
    #[local] Instance : CustomIpat "locals۰at۰finished" :=
      " ( %locals{} & Hat{_{}} ) ".
    #[local] Definition locals ۰ at' γ_locals i scope : iProp Σ :=
      match scope with
      | Some scope ⇒
          locals ۰ at ۰ running γ_locals i scope
      | None ⇒
          locals ۰ at ۰ finished γ_locals i
      end.
    #[local] Definition locals ۰ at γ :=
      locals ۰ at' γ.(pool ۰ name ۰ locals).

    #[local] Definition globals ۰ model ۰ running γ globals : iProp Σ :=
      ∃ jobs ulocals ,
      ⌜jobs = globals ⊎ ulocals ⌝ ∗
      jobs ۰ auth γ Own jobs ∗
      locals ۰ auth γ ulocals.
    #[local] Instance : CustomIpat "globals۰model۰running" :=
      " ( %jobs & %ulocals & -> & Hjobs_auth & Hlocals_auth ) ".
    #[local] Definition globals ۰ model ۰ finished γ : iProp Σ :=
      [∗ list ] i ∈ seq 0 ˖(γ.(pool ۰ name ۰ size)),
        locals ۰ at γ i None.
    #[local] Instance : CustomIpat "globals۰model۰finished" :=
      " Hlocals_ats ".
    #[local] Definition globals ۰ model γ globals : iProp Σ :=
        globals ۰ model ۰ running γ globals
      ∨ globals ۰ model ۰ finished γ.
    #[local] Instance : CustomIpat "globals۰model" :=
      " [ (:globals۰model۰running) | (:globals۰model۰finished) ] ".

    #[local] Definition context₁ γ i (scope : pool ۰ scope) : iProp Σ :=
      ∃ empty ,
      ws_hub_std ۰ owner γ.(pool ۰ name ۰ hub) i Nonblocked empty ∗
      locals ۰ at γ i (Some scope).
    #[local] Instance : CustomIpat "context₁" :=
      " ( %empty{} & Hhub_owner{_{}} & Hlocals_at{_{}} ) ".

    #[local] Definition task ۰ model γ task Ψ : iProp Σ :=
      ∀ i scope ,
      ⌜i ≤ γ.(pool ۰ name ۰ size)⌝ -∗
      context₁ γ i scope -∗
      WP task (pool ۰ name ۰ context γ i) {{ v ,
        context₁ γ i scope ∗
        Ψ v
      }}.

    #[local] Definition inv ۰ inner γ : iProp Σ :=
      ∃ globals 𝑔𝑙𝑜𝑏𝑎𝑙𝑠 ,
      ⌜𝑔𝑙𝑜𝑏𝑎𝑙𝑠 = gmultiset_map job ۰ val globals ⌝ ∗
      globals ۰ model γ globals ∗
      ws_hub_std ۰ model γ.(pool ۰ name ۰ hub) 𝑔𝑙𝑜𝑏𝑎𝑙𝑠 ∗
      [∗ mset ] global ∈ globals ,
        task ۰ model γ global.(job ۰ val) (λ _,
          ∃ P ,
          saved_prop global.(job ۰ name) P ∗
          ▷ □ P
        ).
    #[local] Instance : CustomIpat "inv۰inner" :=
      " ( %globals & %𝑔𝑙𝑜𝑏𝑎𝑙𝑠 & >%H𝑔𝑙𝑜𝑏𝑎𝑙𝑠 & >Hglobals_model & >Hhub_model & Hglobals ) ".
    #[local] Definition inv₁ γ : iProp Σ :=
      inv (nroot .@"inv") (inv ۰ inner γ).
    #[local] Definition inv₂ γ : iProp Σ :=
      ws_hub_std ۰ inv γ.(pool ۰ name ۰ hub) (nroot .@"hub") ˖(γ.(pool ۰ name ۰ size)) ∗
      inv₁ γ.
    #[local] Instance : CustomIpat "inv₂" :=
      " ( #Hhub_inv{_{}} & #Hinv{_{}} ) ".
    Definition pool ۰ inv γ sz : iProp Σ :=
      ⌜sz = γ.(pool ۰ name ۰ size)⌝ ∗
      inv₂ γ.
    #[local] Instance : CustomIpat "inv" :=
      " ( -> & {#Hinv_{};(:inv₂)} ) ".

    #[local] Definition context ۰ finished γ i : iProp Σ :=
      ws_hub_std ۰ owner γ.(pool ۰ name ۰ hub) i Nonblocked Empty ∗
      locals ۰ at γ i (Some ∅).
    #[local] Instance : CustomIpat "context۰finished" :=
      " ( Hhub_owner{_{}} & Hlocals_at{_{}} ) ".
    #[local] Definition context₂ γ i scope : iProp Σ :=
      ⌜i ≤ γ.(pool ۰ name ۰ size)⌝ ∗
      inv₂ γ ∗
      context₁ γ i scope.
    #[local] Instance : CustomIpat "context₂" :=
      " ( %Hi{} & {#Hinv_{};(:inv₂)} & { {lazy} Hctx{} ; {lazy} Hctx ; (:context₁ ={}) ; (:context₁) } ) ".
    Definition pool ۰ context γ ctx scope : iProp Σ :=
      ∃ i ,
      ⌜ctx = pool ۰ name ۰ context γ i ⌝ ∗
      context₂ γ i scope.
    #[local] Instance : CustomIpat "context" :=
      " ( %i{} & {%Heq{};->} & (:context₂) ) ".

    #[local] Definition worker ۰ post γ i res : iProp Σ :=
      ⌜res = ()%V⌝ ∗
      context ۰ finished γ i.
    #[local] Instance : CustomIpat "worker۰post" :=
      " ( -> & (:context۰finished) ) ".

    Definition pool ۰ model t γ : iProp Σ :=
      ∃ empty doms ,
      ⌜length doms = γ.(pool ۰ name ۰ size)⌝ ∗
      t .[size ] ↦□ #γ.(pool ۰ name ۰ size) ∗
      t .[hub ] ↦□ γ.(pool ۰ name ۰ hub) ∗
      t .[domains ] ↦□ γ.(pool ۰ name ۰ domains) ∗
      inv₂ γ ∗
      array ۰ model γ.(pool ۰ name ۰ domains) DfracDiscarded doms ∗
      ( [∗ list ] i ↦ dom ∈ doms ,
        domain ۰ model dom (worker ۰ post γ ˖i)
      ) ∗
      ws_hub_std ۰ owner γ.(pool ۰ name ۰ hub) 0 Blocked empty ∗
      locals ۰ at γ 0 (Some ∅).
    #[local] Instance : CustomIpat "model" :=
      " ( %empty{} & %doms{} & %Hdoms{} & #Hl{}_size & #Hl{}_hub & #Hl{}_domains & {#Hinv{};(:inv₂)} & Hdomains{} & Hdoms{} & Hhub{}_owner & Hlocals_at{_{}} ) ".

    Definition pool ۰ finished γ : iProp Σ :=
      ∃ jobs ,
      jobs ۰ auth γ Discard jobs ∗
      jobs ۰ finished jobs.
    #[local] Instance : CustomIpat "finished" :=
      " ( %jobs{} & Hjobs_auth{_{}} & Hjobs_finished{_jobs{}} ) ".

    Definition pool ۰ consumer γ P : iProp Σ :=
      pool ۰ finished γ ={⊤}=∗
      P.

    Definition pool ۰ obligation γ P : iProp Σ :=
      □ (
        pool ۰ finished γ -∗
        ▷ □ P
      ).

    #[global] Instance pool ۰ obligation ｰ proper γ :
      Proper ((≡) ==> (≡)) (pool ۰ obligation γ).
    #[global] Instance pool ۰ consumer ｰ proper γ :
      Proper ((≡) ==> (≡)) (pool ۰ consumer γ).

    #[local] Instance globals ۰ model ｰ timeless γ globals :
      Timeless (globals ۰ model γ globals).

    #[local] Instance jobs ۰ elem ｰ persistent γ job :
      Persistent (jobs ۰ elem γ job).
    #[local] Instance jobs ۰ finished ｰ persistent jobs :
      Persistent (jobs ۰ finished jobs).
    #[global] Instance pool ۰ inv ｰ persistent γ sz :
      Persistent (pool ۰ inv γ sz).
    #[global] Instance pool ۰ obligation ｰ persistent γ P :
      Persistent (pool ۰ obligation γ P).
    #[global] Instance pool ۰ finished ｰ persistent γ :
      Persistent (pool ۰ finished γ).

    #[local] Lemma jobs ｰ alloc :
      ⊢ |==>
        ∃ γ_jobs ,
        jobs ۰ auth' γ_jobs Own ∅.
    #[local] Lemma jobs ۰ auth ｰ discard γ jobs :
      jobs ۰ auth γ Own jobs ⊢ |==>
      jobs ۰ auth γ Discard jobs.
    #[local] Lemma jobs ۰ elem ｰ valid γ own jobs job :
      jobs ۰ auth γ own jobs -∗
      jobs ۰ elem γ job -∗
      ⌜job ∈ jobs ⌝.
    #[local] Lemma jobs ｰ insert {γ jobs} 𝑗𝑜𝑏 P :
      jobs ۰ auth γ Own jobs ⊢ |==>
        ∃ job ,
        ⌜job.(job ۰ val) = 𝑗𝑜𝑏 ⌝ ∗
        jobs ۰ auth γ Own ({[+job +]} ⊎ jobs) ∗
        jobs ۰ elem γ job ∗
        saved_prop job.(job ۰ name) P.
    Opaque jobs ۰ elem.

    #[local] Lemma jobs ۰ finished ｰ empty :
      ⊢ jobs ۰ finished ∅.
    #[local] Lemma jobs ۰ finished ｰ elem_of job jobs :
      job ∈ jobs →
      jobs ۰ finished jobs ⊢
        ∃ P ,
        saved_prop job.(job ۰ name) P ∗
        □ P.
    #[local] Lemma jobs ۰ finished ｰ insert {jobs} job P :
      jobs ۰ finished jobs -∗
      saved_prop job.(job ۰ name) P -∗
      □ P -∗
      jobs ۰ finished ({[+job +]} ⊎ jobs).
    #[local] Lemma jobs ۰ finished ｰ union localss :
      ( [∗ list ] locals ∈ localss ,
        jobs ۰ finished locals
      ) ⊢
      jobs ۰ finished (⋃+ localss).
    Opaque jobs ۰ finished.

    #[local] Lemma locals ｰ alloc sz :
      ⊢ |==>
        ∃ γ_locals ,
        locals ۰ auth' sz γ_locals ∅ ∗
        [∗ list ] i ∈ seq 0 ˖sz ,
          locals ۰ at' γ_locals i (Some ∅).
    #[local] Lemma locals ۰ at ｰ exclusive γ i scope1 scope2 :
      locals ۰ at γ i scope1 -∗
      locals ۰ at γ i scope2 -∗
      False.
    #[local] Lemma locals ｰ insert {γ ulocals i scope} local :
      locals ۰ auth γ ulocals -∗
      locals ۰ at γ i (Some scope) ==∗
        locals ۰ auth γ ({[+local +]} ⊎ ulocals) ∗
        locals ۰ at γ i (Some ({[+local +]} ⊎ scope)).
    #[local] Lemma locals ۰ at ｰ finish γ i local P scope :
      locals ۰ at γ i (Some ({[+local +]} ⊎ scope)) -∗
      saved_prop local.(job ۰ name) P -∗
      □ P -∗
      locals ۰ at γ i (Some scope).
    #[local] Lemma locals ｰ close γ ulocals :
      locals ۰ auth γ ulocals -∗
      ( [∗ list ] i ∈ seq 0 ˖(γ.(pool ۰ name ۰ size)),
        locals ۰ at γ i (Some ∅)
      ) -∗
        locals ۰ auth γ ulocals ∗
        ( [∗ list ] i ∈ seq 0 ˖(γ.(pool ۰ name ۰ size)),
          locals ۰ at γ i None
        ) ∗
        jobs ۰ finished ulocals.
    Opaque locals ۰ auth'.
    Opaque locals ۰ at'.

    #[local] Lemma globals ۰ model ｰ init γ :
      jobs ۰ auth γ Own ∅ -∗
      locals ۰ auth γ ∅ -∗
      globals ۰ model γ ∅.
    #[local] Lemma globals ۰ model ｰ locals ۰ at γ globals i scope :
      i ≤ γ.(pool ۰ name ۰ size) →
      globals ۰ model γ globals -∗
      locals ۰ at γ i scope -∗
        globals ۰ model ۰ running γ globals ∗
        locals ۰ at γ i scope.
    #[local] Lemma globals ۰ model ｰ push {γ globals} 𝑔𝑙𝑜𝑏𝑎𝑙 P i scope :
      i ≤ γ.(pool ۰ name ۰ size) →
      globals ۰ model γ globals -∗
      locals ۰ at γ i scope ==∗
        ∃ global ,
        ⌜global.(job ۰ val) = 𝑔𝑙𝑜𝑏𝑎𝑙 ⌝ ∗
        globals ۰ model γ ({[+global +]} ⊎ globals) ∗
        locals ۰ at γ i scope ∗
        jobs ۰ elem γ global ∗
        saved_prop global.(job ۰ name) P.
    #[local] Lemma globals ۰ model ｰ pop {γ globals} global globals' i scope :
      i ≤ γ.(pool ۰ name ۰ size) →
      globals = {[+global +]} ⊎ globals' →
      globals ۰ model γ globals -∗
      locals ۰ at γ i (Some scope) ==∗
        globals ۰ model γ globals' ∗
        locals ۰ at γ i (Some ({[+global +]} ⊎ scope)).
    #[local] Lemma globals ۰ model ｰ close γ :
      globals ۰ model γ ∅ -∗
      ( [∗ list ] i ∈ seq 0 ˖(γ.(pool ۰ name ۰ size)),
        locals ۰ at γ i (Some ∅)
      ) ==∗
        ∃ jobs ,
        globals ۰ model γ ∅ ∗
        jobs ۰ auth γ Discard jobs ∗
        jobs ۰ finished jobs.
    Opaque globals ۰ model.

    Lemma pool ۰ inv ｰ agree γ sz1 sz2 :
      pool ۰ inv γ sz1 -∗
      pool ۰ inv γ sz2 -∗
      ⌜sz1 = sz2 ⌝.

    Lemma pool ۰ obligation ｰ wand {γ P1} P2 :
      pool ۰ obligation γ P1 -∗
      □ (P1 -∗ P2 ) -∗
      pool ۰ obligation γ P2.
    Lemma pool ۰ obligation ｰ split γ P1 P2 :
      pool ۰ obligation γ (P1 ∗ P2) ⊢
        pool ۰ obligation γ P1 ∗
        pool ۰ obligation γ P2.
    Lemma pool ۰ obligation ｰ combine γ P1 P2 :
      pool ۰ obligation γ P1 -∗
      pool ۰ obligation γ P2 -∗
      pool ۰ obligation γ (P1 ∗ P2).
    Lemma pool ۰ obligation ｰ finished γ P :
      pool ۰ obligation γ P -∗
      pool ۰ finished γ -∗
      ▷ □ P.

    #[local] Lemma pool ٠ context ｰ spec {sz : Z} {hub} {i : Z} γ (i_ : nat) :
      sz = γ.(pool ۰ name ۰ size) →
      hub = γ.(pool ۰ name ۰ hub) →
      i = i_ →
      {{{
        True
      }}}
        pool__code.pool ٠ context #sz hub #i
      {{{
        RET pool ۰ name ۰ context γ i_;
        True
      }}}.

    #[local] Lemma pool ٠ context_main ｰ spec t γ :
      {{{
        t .[size ] ↦□ #γ.(pool ۰ name ۰ size) ∗
        t .[hub ] ↦□ γ.(pool ۰ name ۰ hub)
      }}}
        pool ٠ context_main #t
      {{{
        RET pool ۰ name ۰ context γ 0;
        True
      }}}.

    #[local] Lemma pool ٠ execute ｰ spec γ i scope task Ψ :
      i ≤ γ.(pool ۰ name ۰ size) →
      {{{
        context₁ γ i scope ∗
        task ۰ model γ task Ψ
      }}}
        pool ٠ execute (pool ۰ name ۰ context γ i) task
      {{{
        v
      , RET v ;
        context₁ γ i scope ∗
        Ψ v
      }}}.

    #[local] Lemma pool ٠ worker ｰ spec γ i :
      {{{
        context₂ γ i ∅
      }}}
        pool ٠ worker (pool ۰ name ۰ context γ i)
      {{{
        res
      , RET res ;
        worker ۰ post γ i res
      }}}.

    Lemma pool ٠ create ｰ spec sz :
      (0 ≤ sz)%Z →
      {{{
        True
      }}}
        pool ٠ create #sz
      {{{
        t γ
      , RET #t ;
        pool ۰ inv γ ₊sz ∗
        pool ۰ model t γ ∗
        meta_token t ⊤
      }}}.

    Lemma pool ٠ run_on ｰ spec Ψ t γ task :
      {{{
        pool ۰ model t γ ∗
        ( ∀ ctx scope ,
          pool ۰ context γ ctx scope -∗
          WP task ctx {{ v ,
            pool ۰ context γ ctx scope ∗
            Ψ v
          }}
        )
      }}}
        pool ٠ run_on #t task
      {{{
        v
      , RET v ;
        pool ۰ model t γ ∗
        Ψ v
      }}}.

    Lemma pool ٠ close ｰ spec t γ :
      {{{
        pool ۰ model t γ
      }}}
        pool ٠ close #t
      {{{
        RET ();
        pool ۰ finished γ
      }}}.

    Lemma pool ٠ run ｰ spec (Ψ : location → pool ۰ name → val → iProp Σ) sz task :
      (0 ≤ sz)%Z →
      {{{
        ∀ t γ ctx scope ,
        pool ۰ inv γ ₊sz -∗
        meta_token t ⊤ -∗
        pool ۰ context γ ctx scope -∗
        WP task ctx {{ v ,
          pool ۰ context γ ctx scope ∗
          Ψ t γ v
        }}
      }}}
        pool ٠ run #sz task
      {{{
        t γ v
      , RET v ;
        pool ۰ finished γ ∗
        Ψ t γ v
      }}}.

    Lemma pool ٠ size ｰ spec γ sz ctx scope :
      {{{
        pool ۰ inv γ sz ∗
        pool ۰ context γ ctx scope
      }}}
        pool ٠ size ctx
      {{{
        RET #sz ;
        pool ۰ context γ ctx scope
      }}}.

    Lemma pool ٠ async ｰ spec P Q γ ctx scope task :
      {{{
        pool ۰ context γ ctx scope ∗
        ( ∀ ctx scope ,
          pool ۰ context γ ctx scope -∗
          WP task ctx {{ res ,
            pool ۰ context γ ctx scope ∗
            ▷ P ∗
            ▷ □ Q
          }}
        )
      }}}
        pool ٠ async ctx task
      {{{
        RET ();
        pool ۰ context γ ctx scope ∗
        pool ۰ consumer γ P ∗
        pool ۰ obligation γ Q
      }}}.

    #[local] Lemma pool ٠ wait₁ ｰ spec P_notification P_pred Q_pred γ ctx scope notification pred :
      {{{
        pool ۰ context γ ctx scope ∗
        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
          }}
        )
      }}}
        pool ٠ wait₁ ctx notification pred
      {{{
        RET ();
        pool ۰ context γ ctx scope ∗
        Q_pred
      }}}.

    Lemma pool ٠ wait ｰ spec P_notification P_pred Q_pred γ ctx scope notification pred :
      {{{
        pool ۰ context γ ctx scope ∗
        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
          }}
        )
      }}}
        pool ٠ wait ctx notification pred
      {{{
        RET ();
        pool ۰ context γ ctx scope ∗
        Q_pred
      }}}.

    Lemma pool ٠ wait_ivar ｰ spec `{ivar ۰ G : !Ivar4G Σ} {context_name} γ ctx scope ivar Ψ Ξ (Γ : _ → context_name → _) :
      {{{
        pool ۰ context γ ctx scope ∗
        ivar_4 ۰ inv ivar Ψ Ξ Γ
      }}}
        pool ٠ wait_ivar ctx ivar
      {{{
        RET ();
        £ 2 ∗
        pool ۰ context γ ctx scope ∗
        ivar_4 ۰ resolved ivar
      }}}.
  End pool ۰ G.

  #[global] Opaque pool ۰ scope.
  #[global] Opaque pool ۰ inv.
  #[global] Opaque pool ۰ model.
  #[global] Opaque pool ۰ context.
  #[global] Opaque pool ۰ consumer.
  #[global] Opaque pool ۰ obligation.
  #[global] Opaque pool ۰ finished.
End base.

Require zoo_parabs.pool__opaque.

Section pool ۰ G.
  Context `{pool ۰ G : PoolG Σ}.

  Implicit Type 𝑡 : location.
  Implicit Type t : val.
  Implicit Type γ : base.pool ۰ name.
  Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.
  Implicit Type Ψ : val → iProp Σ.

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

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

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

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

  Definition pool ۰ consumer t P : iProp Σ :=
    pool ۰ finished t ={⊤}=∗
    P.

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

  #[global] Instance pool ۰ obligation ｰ proper t :
    Proper ((≡) ==> (≡)) (pool ۰ obligation t).
  #[global] Instance pool ۰ consumer ｰ proper t :
    Proper ((≡) ==> (≡)) (pool ۰ consumer t).

  #[global] Instance pool ۰ inv ｰ persistent t sz :
    Persistent (pool ۰ inv t sz).
  #[global] Instance pool ۰ obligation ｰ persistent t P :
    Persistent (pool ۰ obligation t P).
  #[global] Instance pool ۰ finished ｰ persistent t :
    Persistent (pool ۰ finished t).

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

  Lemma pool ۰ consumer ｰ intro {t} P :
    (pool ۰ finished t ={⊤}=∗ P ) ⊢
    pool ۰ consumer t P.
  Lemma pool ۰ consumer ｰ wand {t P1} P2 :
    pool ۰ consumer t P1 -∗
    (P1 -∗ P2 ) -∗
    pool ۰ consumer t P2.
  Lemma pool ۰ consumer ｰ combine t P1 P2 :
    pool ۰ consumer t P1 -∗
    pool ۰ consumer t P2 -∗
    pool ۰ consumer t (P1 ∗ P2).
  Lemma pool ۰ consumer ｰ or t P1 P2 :
    ( pool ۰ consumer t P1
    ∨ pool ۰ consumer t P2
    ) ⊢
    pool ۰ consumer t (P1 ∨ P2).
  Lemma pool ۰ consumer ｰ exist {A} {t} (Φ : A → iProp Σ) x :
    pool ۰ consumer t (Φ x) ⊢
    pool ۰ consumer t (∃ x , Φ x).
  Lemma pool ۰ consumer ｰ ∀ {A} {t} (Φ : A → iProp Σ) x :
    pool ۰ consumer t (∀ x , Φ x) ⊢
    pool ۰ consumer t (Φ x).
  Lemma pool ۰ consumer ｰ finished t P :
    pool ۰ consumer t P -∗
    pool ۰ finished t ={⊤}=∗
    P.
  #[global] Instance pool ۰ consumer ｰ mono t :
    Proper ((⊢) ==> (⊢)) (pool ۰ consumer t).
  #[global] Instance pool ۰ consumer ｰ flip ｰ mono t :
    Proper (flip (⊢) ==> flip (⊢)) (pool ۰ consumer t).

  Lemma pool ۰ obligation ｰ wand {t P1} P2 :
    pool ۰ obligation t P1 -∗
    □ (P1 -∗ P2 ) -∗
    pool ۰ obligation t P2.
  Lemma pool ۰ obligation ｰ split t P1 P2 :
    pool ۰ obligation t (P1 ∗ P2) ⊢
      pool ۰ obligation t P1 ∗
      pool ۰ obligation t P2.
  Lemma pool ۰ obligation ｰ combine t P1 P2 :
    pool ۰ obligation t P1 -∗
    pool ۰ obligation t P2 -∗
    pool ۰ obligation t (P1 ∗ P2).
  Lemma pool ۰ obligation ｰ finished t P :
    pool ۰ obligation t P -∗
    pool ۰ finished t -∗
    ▷ □ P.

  Lemma pool ٠ create ｰ spec sz :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      pool ٠ create #sz
    {{{
      t
    , RET t ;
      pool ۰ inv t ₊sz ∗
      pool ۰ model t
    }}}.

  Lemma pool ٠ run_on ｰ spec Ψ t task :
    {{{
      pool ۰ model t ∗
      ( ∀ ctx scope ,
        pool ۰ context t ctx scope -∗
        WP task ctx {{ v ,
          pool ۰ context t ctx scope ∗
          Ψ v
        }}
      )
    }}}
      pool ٠ run_on t task
    {{{
      v
    , RET v ;
      pool ۰ model t ∗
      Ψ v
    }}}.

  Lemma pool ٠ close ｰ spec t :
    {{{
      pool ۰ model t
    }}}
      pool ٠ close t
    {{{
      RET ();
      pool ۰ finished t
    }}}.

  Lemma pool ٠ run ｰ spec (Ψ : val → val → iProp Σ) sz task :
    (0 ≤ sz)%Z →
    {{{
      ∀ t ctx scope ,
      pool ۰ inv t ₊sz -∗
      pool ۰ context t ctx scope -∗
      WP task ctx {{ v ,
        pool ۰ context t ctx scope ∗
        Ψ t v
      }}
    }}}
      pool ٠ run #sz task
    {{{
      t v
    , RET v ;
      pool ۰ finished t ∗
      Ψ t v
    }}}.

  Lemma pool ٠ size ｰ spec t sz ctx scope :
    {{{
      pool ۰ inv t sz ∗
      pool ۰ context t ctx scope
    }}}
      pool ٠ size ctx
    {{{
      RET #sz ;
      pool ۰ context t ctx scope
    }}}.

  Lemma pool ٠ async ｰ spec P Q t ctx scope task :
    {{{
      pool ۰ context t ctx scope ∗
      ( ∀ ctx scope ,
        pool ۰ context t ctx scope -∗
        WP task ctx {{ res ,
          pool ۰ context t ctx scope ∗
          ▷ P ∗
          ▷ □ Q
        }}
      )
    }}}
      pool ٠ async ctx task
    {{{
      RET ();
      pool ۰ context t ctx scope ∗
      pool ۰ consumer t P ∗
      pool ۰ obligation t Q
    }}}.

  Lemma pool ٠ wait ｰ spec P_notification P_pred Q_pred t ctx scope notification pred :
    {{{
      pool ۰ context t ctx scope ∗
      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
        }}
      )
    }}}
      pool ٠ wait ctx notification pred
    {{{
      RET ();
      pool ۰ context t ctx scope ∗
      Q_pred
    }}}.

  Lemma pool ٠ wait_ivar ｰ spec `{ivar ۰ G : !Ivar4G Σ} {context_name} t ctx scope ivar Ψ Ξ (Γ : _ → context_name → _) :
    {{{
      pool ۰ context t ctx scope ∗
      ivar_4 ۰ inv ivar Ψ Ξ Γ
    }}}
      pool ٠ wait_ivar ctx ivar
    {{{
      RET ();
      £ 2 ∗
      pool ۰ context t ctx scope ∗
      ivar_4 ۰ resolved ivar
    }}}.
End pool ۰ G.

#[global] Opaque pool ۰ scope.
#[global] Opaque pool ۰ inv.
#[global] Opaque pool ۰ model.
#[global] Opaque pool ۰ context.
#[global] Opaque pool ۰ obligation.
#[global] Opaque pool ۰ consumer.
#[global] Opaque pool ۰ finished.

Section pool ۰ G.
  Context `{pool ۰ G : PoolG Σ}.

  Implicit Type P Q R : iProp Σ.

  #[global] Instance from_assumption ｰ pool ۰ consumer t p P Q :
    FromAssumption p P Q →
    KnownRFromAssumption p P (pool ۰ consumer t Q).

  #[global] Instance from_pure ｰ pool ۰ consumer t a P ϕ :
    FromPure a P ϕ →
    FromPure a (pool ۰ consumer t P) ϕ.

  #[global] Instance into_wand ｰ pool ۰ consumer t p q R P Q :
    IntoWand false false R P Q →
    IntoWand p q (pool ۰ consumer t R) (pool ۰ consumer t P) (pool ۰ consumer t Q).
  #[global] Instance into_wand ｰ pool ۰ consumer ｰ persistent t p q R P Q :
    IntoWand false q R P Q →
    IntoWand p q (pool ۰ consumer t R) P (pool ۰ consumer t Q).
  #[global] Instance into_wand ｰ pool ۰ consumer ｰ args t p q R P Q :
    IntoWand p false R P Q →
    IntoWand' p q R (pool ۰ consumer t P) (pool ۰ consumer t Q).

  #[global] Instance from_sep ｰ pool ۰ consumer t P Q1 Q2 :
    FromSep P Q1 Q2 →
    FromSep (pool ۰ consumer t P) (pool ۰ consumer t Q1) (pool ۰ consumer t Q2).

  #[global] Instance from_or ｰ pool ۰ consumer t P Q1 Q2 :
    FromOr P Q1 Q2 →
    FromOr (pool ۰ consumer t P) (pool ۰ consumer t Q1) (pool ۰ consumer t Q2).

  #[global] Instance from_exist ｰ pool ۰ consumer t {A} P (Φ : A → iProp Σ) :
    FromExist P Φ →
    FromExist (pool ۰ consumer t P) (λ a, pool ۰ consumer t (Φ a)).

  #[global] Instance into_forall ｰ pool ۰ consumer t {A} P (Φ : A → iProp Σ) :
    IntoForall P Φ →
    IntoForall (pool ۰ consumer t P) (λ a, pool ۰ consumer t (Φ a)).

  #[global] Instance from_modal ｰ pool ۰ consumer t P :
    FromModal True modality_id (pool ۰ consumer t P) (pool ۰ consumer t P) P.

  #[global] Instance elim_modal ｰ pool ۰ consumer t p P Q :
    ElimModal True p false (pool ۰ consumer t P) P (pool ۰ consumer t Q) (pool ۰ consumer t Q).

  #[global] Instance add_modal ｰ pool ۰ consumer t P Q :
    AddModal (pool ۰ consumer t P) P (pool ۰ consumer t Q).

  #[global] Instance frame ｰ pool ۰ consumer t p R P Q :
    Frame p R P Q →
    Frame p R (pool ۰ consumer t P) (pool ۰ consumer t Q)
  | 2.
End pool ۰ G.