Library zoo_std.queue_2

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  queue_2__code.
From zoo_std Require Import
  option
  chain
  queue_2__types.
From zoo Require Import
  options.

Implicit Types l : location.
Implicit Types t v front back : val.
Implicit Types vs : list val.

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Definition queue_2_model t vs : iProp Σ :=
    ∃ l front back,
    ⌜t = #l⌝ ∗
    l.[front] ↦ front ∗
    l.[back] ↦ back ∗
    chain_model (Some §Node) front vs back ∗
    chain_model (Some §Node) back [()%V] ().
  #[local] Instance : CustomIpat "model" :=
    " ( %l & %front & %back & -> & Hl_front & Hl_back & Hfront & Hback ) ".

  #[global] Instance queue_2_model_timeless t vs :
    Timeless (queue_2_model t vs).

  Lemma queue_2٠create𑁒spec :
    {{{
      True
    }}}
      queue_2٠create ()
    {{{
      t
    , RET t;
      queue_2_model t []
    }}}.

  Lemma queue_2٠is_empty𑁒spec t vs :
    {{{
      queue_2_model t vs
    }}}
      queue_2٠is_empty t
    {{{
      RET #(bool_decide (vs = []%list));
      queue_2_model t vs
    }}}.

  Lemma queue_2٠push𑁒spec t vs v :
    {{{
      queue_2_model t vs
    }}}
      queue_2٠push t v
    {{{
      RET ();
      queue_2_model t (vs ++ [v])
    }}}.

  Lemma queue_2٠pop𑁒spec t vs :
    {{{
      queue_2_model t vs
    }}}
      queue_2٠pop t
    {{{
      RET head vs;
      queue_2_model t (tail vs)
    }}}.
End zoo_G.

From zoo_std Require
  queue_2__opaque.

#[global] Opaque queue_2_model.