Library zoo_std.queue_1

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  queue_1__code.
From zoo_std Require Import
  option
  chain
  queue_1__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_1_model t vs : iProp Σ :=
    ∃ l front back,
    ⌜t = #l⌝ ∗
    l.[front] ↦ front ∗
    l.[back] ↦ back ∗
    chain_model None front vs back ∗
    chain_model None back [()%V] ().
  #[local] Instance : CustomIpat "model" :=
    " ( %l & %front & %back & -> & Hl_front & Hl_back & Hfront & Hback ) ".

  #[global] Instance queue_1_model_timeless t vs :
    Timeless (queue_1_model t vs).

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

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

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

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

From zoo_std Require
  queue_1__opaque.

#[global] Opaque queue_1_model.