Library zoo_std.bqueue

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  bqueue__code.
From zoo_std Require Import
  bqueue__types
  option
  array.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types l : location.
Implicit Types front back : nat.
Implicit Types v t : val.
Implicit Types 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.

From zoo_std Require
  bqueue__opaque.

#[global] Opaque bqueue_model.