Library zoo_std.bqueue

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.bqueue__code.
Require Import zoo_std.bqueue__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type l : location.
Implicit Type front back : nat.
Implicit Type v t : val.
Implicit Type o : option val.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Definition bqueue ۰ model t (cap : nat) vs : iProp Σ :=
    ∃ l data front back extra ,
    ⌜t = #l ⌝ ∗
    l .[capacity ] ↦□ #cap ∗
    l .[data ] ↦□ data ∗
    l .[front ] ↦ #front ∗
    l .[back ] ↦ #back ∗
    array ۰ cslice data cap front (DfracOwn 1) vs ∗
    array ۰ cslice data cap back (DfracOwn 1) (replicate extra ()%V) ∗
    ⌜back = (front + length vs)%nat⌝ ∗
    ⌜cap = (length vs + extra)%nat⌝.
  #[local] Instance : CustomIpat "model" :=
    " ( %l & %data & %front & %back & %extra & -> & Hl_capacity & Hl_data & Hl_front & Hl_back & Hvs & Hextra & % & % ) ".

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

  Lemma bqueue ۰ model ｰ valid t cap vs :
    bqueue ۰ model t cap vs ⊢
    ⌜length vs ≤ cap ⌝.
  Lemma bqueue ۰ model ｰ exclusive t cap1 vs1 cap2 vs2 :
    bqueue ۰ model t cap1 vs1 -∗
    bqueue ۰ model t cap2 vs2 -∗
    False.

  Lemma bqueue ٠ create ｰ spec cap :
    (0 ≤ cap)%Z →
    {{{
      True
    }}}
      bqueue ٠ create #cap
    {{{
      t
    , RET t ;
      bqueue ۰ model t ₊cap []
    }}}.

  Lemma bqueue ٠ size ｰ spec t cap vs :
    {{{
      bqueue ۰ model t cap vs
    }}}
      bqueue ٠ size t
    {{{
      RET #(length vs );
      bqueue ۰ model t cap vs
    }}}.

  Lemma bqueue ٠ is_empty ｰ spec t cap vs :
    {{{
      bqueue ۰ model t cap vs
    }}}
      bqueue ٠ is_empty t
    {{{
      RET #(bool_decide (vs = []%list));
      bqueue ۰ model t cap vs
    }}}.

  Lemma bqueue ٠ unsafe_get ｰ spec {t cap vs i} v :
    (0 ≤ i)%Z →
    vs !! ₊i = Some v →
    {{{
      bqueue ۰ model t cap vs
    }}}
      bqueue ٠ unsafe_get t #i
    {{{
      RET v ;
      bqueue ۰ model t cap vs
    }}}.

  Lemma bqueue ٠ unsafe_set ｰ spec t cap vs i v :
    (0 ≤ i < length vs)%Z →
    {{{
      bqueue ۰ model t cap vs
    }}}
      bqueue ٠ unsafe_set t #i v
    {{{
      RET ();
      bqueue ۰ model t cap (<[₊i := v ]> vs)
    }}}.

  Lemma bqueue ٠ push ｰ spec t cap vs v :
    {{{
      bqueue ۰ model t cap vs
    }}}
      bqueue ٠ push t v
    {{{
      b
    , RET #b ;
      ⌜if b then True else length vs = cap ⌝ ∗
      bqueue ۰ model t cap (if b then vs ++ [v] else vs)
    }}}.

  Lemma bqueue ٠ pop_front ｰ spec t cap vs :
    {{{
      bqueue ۰ model t cap vs
    }}}
      bqueue ٠ pop_front t
    {{{
      RET head vs ;
      bqueue ۰ model t cap (tail vs)
    }}}.

  Lemma bqueue ٠ pop_back ｰ spec t cap vs :
    {{{
      bqueue ۰ model t cap vs
    }}}
      bqueue ٠ pop_back t
    {{{
      o
    , RET o ;
      match o with
      | None ⇒
          ⌜vs = []⌝ ∗
          bqueue ۰ model t cap []
      | Some v ⇒
          ∃ vs',
          ⌜vs = vs' ++ [v]⌝ ∗
          bqueue ۰ model t cap vs'
      end
    }}}.
End zoo ۰ G.

Require zoo_std.bqueue__opaque.

#[global] Opaque bqueue ۰ model.