Library zoo_parabs.waiters

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  array.
From zoo_saturn Require Import
  mpmc_queue_1.
From zoo_parabs Require Export
  base
  waiters__code.
From zoo_parabs Require Import
  waiter
  waiters__types.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types v t waiters queue : val.
Implicit Types 𝑤𝑎𝑖𝑡𝑒𝑟𝑠 𝑞𝑢𝑒𝑢𝑒 : list val.

Class WaitersG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] waiters_G_queue_G :: MpmcQueue1G Σ
  ; #[local] waiters_G_waiter_G :: WaiterG Σ
  }.

Definition waiters_Σ :=
  #[mpmc_queue_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 Σ :=
    ∃ 𝑞𝑢𝑒𝑢𝑒,
    mpmc_queue_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 𝑤𝑎𝑖𝑡𝑒𝑟) ∗
    mpmc_queue_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.

From zoo_parabs Require
  waiters__opaque.

#[global] Opaque waiters_inv.