Library zoo_parabs.waiters

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_parabs.base.
Require Export zoo_parabs.waiters__code.
Require Import zoo_parabs.waiters__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type v t waiters queue : val.
Implicit Type π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿπ‘  π‘žπ‘’π‘’π‘’π‘’ : list val.

Class WaitersG Ξ£ `{zooΫ°G : !ZooG Ξ£} :=
  { #[local] waitersΫ°GΫ°queueΫ°G :: QueueMpmc1G Ξ£
  ; #[local] waitersΫ°GΫ°waiterΫ°G :: WaiterG Ξ£
  }.

Definition waitersΫ°Ξ£ :=
  #[queue_mpmc_1Ϋ°Ξ£
  ; waiterΫ°Ξ£
  ].
#[global] Instance subGο½°ws_hub_Ξ£ Ξ£ `{zooΫ°G : !ZooG Ξ£} :
  subG waitersΫ°Ξ£ Ξ£ β†’
  WaitersG Ξ£.

Section waitersΫ°G.
  Context `{waitersΫ°G : WaitersG Ξ£}.

  #[local] Definition waitersΫ°invΫ°inner queue : iProp Ξ£ :=
    βˆƒ π‘žπ‘’π‘’π‘’π‘’,
    queue_mpmc_1Ϋ°model queue π‘žπ‘’π‘’π‘’π‘’ βˆ—
    [βˆ— list] π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿ ∈ π‘žπ‘’π‘’π‘’π‘’,
      waiterΫ°inv π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿ.
  #[local] Instance : CustomIpat "invΫ°inner" :=
    " ( %π‘žπ‘’π‘’π‘’π‘’ & >Hqueue_model & Hπ‘žπ‘’π‘’π‘’π‘’ ) ".
  Definition waitersΫ°inv t sz : iProp Ξ£ :=
    βˆƒ waiters π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿπ‘  queue,
    βŒœt = (waiters, queue)%V⌝ βˆ—
    arrayΫ°model waiters Discard π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿπ‘  βˆ—
    βŒœlength π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿπ‘  = sz⌝ βˆ—
    ([βˆ— list] π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿ ∈ π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿπ‘ , waiterΫ°inv π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿ) βˆ—
    queue_mpmc_1Ϋ°inv queue (nroot.@"queue") βˆ—
    inv (nroot.@"inv") (waitersΫ°invΫ°inner queue).
  #[local] Instance : CustomIpat "inv" :=
    " ( %waiters & %π‘€π‘Žπ‘–π‘‘π‘’π‘Ÿπ‘  & %queue & -> & #Hwaiters & %Hπ‘€π‘Žπ‘–π‘‘π‘’π‘Ÿs & #Hπ‘€π‘Žπ‘–π‘‘π‘’π‘Ÿπ‘  & #Hqueue_inv & #Hinv ) ".

  #[global] Instance waitersΫ°invο½°persistent t sz :
    Persistent (waitersΫ°inv t sz).

  Lemma waitersΩ createο½°spec sz :
    (0 ≀ sz)%Z β†’
    {{{
      True
    }}}
      waitersΩ create #sz
    {{{
      t
    , RET t;
      waitersΫ°inv t β‚Šsz
    }}}.

  Lemma waitersΩ notifyο½°spec t (sz : nat) i :
    (0 ≀ i < sz)%Z β†’
    {{{
      waitersΫ°inv t sz
    }}}
      waitersΩ notify t #i
    {{{
      RET ();
      True
    }}}.

  Lemma waitersΩ notify_oneο½°spec t sz :
    {{{
      waitersΫ°inv t sz
    }}}
      waitersΩ notify_one t
    {{{
      RET ();
      True
    }}}.

  Lemma waitersΩ notify_allο½°spec t sz :
    {{{
      waitersΫ°inv t sz
    }}}
      waitersΩ notify_all t
    {{{
      RET ();
      True
    }}}.

  Lemma waitersΩ prepare_waitο½°spec t (sz : nat) i :
    (0 ≀ i < sz)%Z β†’
    {{{
      waitersΫ°inv t sz
    }}}
      waitersΩ prepare_wait t #i
    {{{
      RET ();
      True
    }}}.

  Lemma waitersΩ cancel_waitο½°spec t (sz : nat) i :
    (0 ≀ i < sz)%Z β†’
    {{{
      waitersΫ°inv t sz
    }}}
      waitersΩ cancel_wait t #i
    {{{
      b
    , RET #b;
      True
    }}}.

  Lemma waitersΩ commit_waitο½°spec t (sz : nat) i :
    (0 ≀ i < sz)%Z β†’
    {{{
      waitersΫ°inv t sz
    }}}
      waitersΩ commit_wait t #i
    {{{
      RET ();
      True
    }}}.
End waitersΫ°G.

Require zoo_parabs.waiters__opaque.

#[global] Opaque waitersΫ°inv.