Library zoo_std.queue_3

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  queue_3__code.
From zoo_std Require Import
  queue_3__types
  option
  int
  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.

#[local] Definition min_capacity :=
  val_to_nat' queue_3٠min_capacity.
#[local] Lemma queue_3_min_capacity :
  queue_3٠min_capacity = #min_capacity.
Opaque queue_3__code.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.

From zoo_std Require
  queue_3__opaque.

#[global] Opaque queue_3_model.