Library zoo_std.deque

From zoo Require Import
  prelude.
From zoo.iris.bi Require Import
  big_op.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  deque__code.
From zoo_std Require Import
  option
  xdeque.
From zoo Require Import
  options.

Implicit Types fn : val.

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

  Definition deque_model t vs : iProp Σ :=
    ∃ nodes ,
    xdeque_model t nodes ∗
    [∗ list ] node ; v ∈ nodes ; vs , node .[xdeque_data ] ↦ v.

  #[global] Instance deque_model_timeless t vs :
    Timeless (deque_model t vs).

  Lemma deque_model_exclusive t vs1 vs2 :
    deque_model t vs1 -∗
    deque_model t vs2 -∗
    False.

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

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

  Lemma deque ٠ push_front 𑁒 spec t vs v :
    {{{
      deque_model t vs
    }}}
      deque ٠ push_front t v
    {{{
      RET ();
      deque_model t (v :: vs)
    }}}.

  Lemma deque ٠ push_back 𑁒 spec t vs v :
    {{{
      deque_model t vs
    }}}
      deque ٠ push_back t v
    {{{
      RET ();
      deque_model t (vs ++ [v])
    }}}.

  Lemma deque ٠ pop_front 𑁒 spec t vs :
    {{{
      deque_model t vs
    }}}
      deque ٠ pop_front t
    {{{
      RET head vs ;
      deque_model t (tail vs)
    }}}.

  Lemma deque ٠ pop_back 𑁒 spec t vs :
    {{{
      deque_model t vs
    }}}
      deque ٠ pop_back t
    {{{
      o
    , RET o ;
      match o with
      | None ⇒
          ⌜vs = []⌝ ∗
          deque_model t []
      | Some v ⇒
          ∃ vs',
          ⌜vs = vs' ++ [v]⌝ ∗
          deque_model t vs'
      end
    }}}.

  Lemma deque ٠ iter 𑁒 spec Ψ fn t vs :
    {{{
      ▷ Ψ [] ∗
      deque_model t vs ∗
      □ (
        ∀ vs_done v vs_todo ,
        ⌜vs = vs_done ++ v :: vs_todo ⌝ -∗
        Ψ vs_done -∗
        WP fn v {{ res ,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (vs_done ++ [v])
        }}
      )
    }}}
      deque ٠ iter fn t
    {{{
      RET ();
      deque_model t vs ∗
      Ψ vs
    }}}.
End zoo_G.

From zoo_std Require
  deque__opaque.

#[global] Opaque deque_model.