Library zoo_std.xdeque

From zoo Require Import
  prelude.
From zoo.common Require Import
  option
  list.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  xdeque__types
  xdeque__code.
From zoo_std Require Import
  option
  xdlchain.
From zoo Require Import
  options.

Implicit Types l node : location.
Implicit Types nodes : list location.
Implicit Types fn : val.

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

  Definition xdeque_model t nodes : iProp Σ :=
    ∃ l,
    ⌜t = #l⌝ ∗
    l.[xdeque_prev] ↦ from_option #@{location} t (last nodes) ∗
    l.[xdeque_next] ↦ from_option #@{location} t (head nodes) ∗
    xdlchain t nodes t.

  #[global] Instance xdeque_model_timeless t nodes :
    Timeless (xdeque_model t nodes).

  Lemma xdeque_model_exclusive t nodes1 nodes2 :
    xdeque_model t nodes1 -∗
    xdeque_model t nodes2 -∗
    False.

  Lemma xdeque_model_NoDup t nodes :
    xdeque_model t nodes ⊢
    ⌜NoDup nodes⌝.

  Lemma xdeque٠create𑁒spec :
    {{{
      True
    }}}
      xdeque٠create ()
    {{{
      t
    , RET t;
      (∃ l, ⌜t = #l⌝ ∗ meta_token l ⊤) ∗
      xdeque_model t []
    }}}.

  Lemma xdeque٠is_empty𑁒spec t nodes :
    {{{
      xdeque_model t nodes
    }}}
      xdeque٠is_empty t
    {{{
      RET #(bool_decide (nodes = []%list));
      xdeque_model t nodes
    }}}.

  #[local] Lemma xdeque٠link𑁒spec node1 v1 node2 v2 :
    {{{
      node1.[xdeque_next] ↦ v1 ∗
      node2.[xdeque_prev] ↦ v2
    }}}
      xdeque٠link #node1 #node2
    {{{
      RET ();
      node1.[xdeque_next] ↦ #node2 ∗
      node2.[xdeque_prev] ↦ #node1
    }}}.

  Lemma xdeque٠push_front𑁒spec t nodes node prev next :
    {{{
      xdeque_model t nodes ∗
      node.[xdeque_prev] ↦ prev ∗
      node.[xdeque_next] ↦ next
    }}}
      xdeque٠push_front t #node
    {{{
      RET ();
      xdeque_model t (node :: nodes)
    }}}.

  Lemma xdeque٠push_back𑁒spec t nodes node prev next :
    {{{
      xdeque_model t nodes ∗
      node.[xdeque_prev] ↦ prev ∗
      node.[xdeque_next] ↦ next
    }}}
      xdeque٠push_back t #node
    {{{
      RET ();
      xdeque_model t (nodes ++ [node])
    }}}.

  Lemma xdeque٠pop_front𑁒spec t nodes :
    {{{
      xdeque_model t nodes
    }}}
      xdeque٠pop_front t
    {{{
      RET #*@{location} $ head nodes : option val;
      xdeque_model t (tail nodes)
    }}}.

  Lemma xdeque٠pop_back𑁒spec t nodes :
    {{{
      xdeque_model t nodes
    }}}
      xdeque٠pop_back t
    {{{
      o
    , RET #*@{location} o : option val;
      match o with
      | None ⇒
          ⌜nodes = []⌝ ∗
          xdeque_model t []
      | Some node ⇒
          ∃ nodes',
          ⌜nodes = nodes' ++ [node]⌝ ∗
          xdeque_model t nodes'
      end
    }}}.

  Lemma xdeque٠remove𑁒spec {t nodes} i node :
    nodes !! i = Some node →
    {{{
      xdeque_model t nodes
    }}}
      xdeque٠remove #node
    {{{
      RET ();
      xdeque_model t (delete i nodes)
    }}}.

  #[local] Lemma xdeque٠iter_aux𑁒spec Ψ i fn l nodes node :
    (nodes ++ [l]) !! i = Some node →
    {{{
      ▷ Ψ (take i nodes) ∗
      xdeque_model #l nodes ∗
      □ (
        ∀ nodes_done node nodes_todo,
        ⌜nodes = nodes_done ++ node :: nodes_todo⌝ -∗
        Ψ nodes_done -∗
        WP fn #node {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (nodes_done ++ [#node])
        }}
      )
    }}}
      xdeque٠iter_aux fn #l #node
    {{{
      RET ();
      xdeque_model #l nodes ∗
      Ψ nodes
    }}}.
  Lemma xdeque٠iter𑁒spec Ψ fn t nodes :
    {{{
      ▷ Ψ [] ∗
      xdeque_model t nodes ∗
      □ (
        ∀ nodes_done node nodes_todo,
        ⌜nodes = nodes_done ++ node :: nodes_todo⌝ -∗
        Ψ nodes_done -∗
        WP fn #node {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (nodes_done ++ [#node])
        }}
      )
    }}}
      xdeque٠iter fn t
    {{{
      RET ();
      xdeque_model t nodes ∗
      Ψ nodes
    }}}.
End zoo_G.

From zoo_std Require
  xdeque__opaque.

#[global] Opaque xdeque_model.