Library zoo_std.queue_3

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.queue_3__code.
Require Import zoo_std.queue_3__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.

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

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

  #[local] Definition model' t vs extra : iProp Σ :=
    ∃ l data cap front back ,
    ⌜t = #l ⌝ ∗
    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⌝ ∗
    ⌜cap ≠ 0⌝.
  #[local] Instance : CustomIpat "model'" :=
    " ( %l & %data & %cap & %front & %back & -> & Hl_data & Hl_front & Hl_back & Hvs & Hextra & %Hback & %Hcap & % ) ".
  Definition queue_3 ۰ model t vs : iProp Σ :=
    ∃ extra ,
    model' t vs extra.
  #[local] Instance : CustomIpat "model" :=
    " ( %extra & {{lazy}Hmodel;(:model')} ) ".

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

  Lemma queue_3 ۰ model ｰ exclusive t vs1 vs2 :
    queue_3 ۰ model t vs1 -∗
    queue_3 ۰ model t vs2 -∗
    False.

  Lemma queue_3 ٠ create ｰ spec :
    {{{
      True
    }}}
      queue_3 ٠ create ()
    {{{
      t
    , RET t ;
      queue_3 ۰ model t []
    }}}.

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

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

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

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

  #[local] Lemma queue_3 ٠ next_capacity ｰ spec n :
    (0 ≤ n)%Z →
    {{{
      True
    }}}
      queue_3 ٠ next_capacity #n
    {{{
      m
    , RET #m ;
      ⌜n ≤ m ⌝%Z
    }}}.
  #[local] Lemma queue_3 ٠ grow ｰ spec t vs extra :
    {{{
      model' t vs extra
    }}}
      queue_3 ٠ grow t
    {{{
      extra
    , RET ();
      ⌜0 < extra ⌝ ∗
      model' t vs extra
    }}}.

  Lemma queue_3 ٠ push ｰ spec t vs v :
    {{{
      queue_3 ۰ model t vs
    }}}
      queue_3 ٠ push t v
    {{{
      RET ();
      queue_3 ۰ model t (vs ++ [v])
    }}}.

  #[local] Lemma queue_3 ٠ shrink ｰ spec t vs :
    {{{
      queue_3 ۰ model t vs
    }}}
      queue_3 ٠ shrink t
    {{{
      RET ();
      queue_3 ۰ model t vs
    }}}.

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

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

Require zoo_std.queue_3__opaque.

#[global] Opaque queue_3 ۰ model.