Library zoo_std.xdlchain

From zoo Require Import
  prelude.
From zoo.common Require Import
  list.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  xdlchain__types.
From zoo Require Import
  options.

Implicit Types node : location.
Implicit Types nodes : list location.
Implicit Types v next prev src dst : val.

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

  Fixpoint xdlchain src nodes dst : iProp Σ :=
    match nodes with
    | [] ⇒
        True
    | node :: nodes ⇒
        node.[xdlchain_prev] ↦ src ∗
        match nodes with
        | [] ⇒
            node.[xdlchain_next] ↦ dst
        | node' :: _ ⇒
            node.[xdlchain_next] ↦ #node' ∗
            xdlchain #node nodes dst
        end
    end.
  #[global] Arguments xdlchain _ !_ _ / : assert.

  #[global] Instance xdlchain_timeless src nodes dst :
    Timeless (xdlchain src nodes dst).

  Lemma xdlchain_nil src dst :
    ⊢ xdlchain src [] dst.

  Lemma xdlchain_singleton src node dst :
    xdlchain src [node] dst ⊣⊢
      node.[xdlchain_prev] ↦ src ∗
      node.[xdlchain_next] ↦ dst.
  Lemma xdlchain_singleton_1 src node dst :
    xdlchain src [node] dst ⊢
      node.[xdlchain_prev] ↦ src ∗
      node.[xdlchain_next] ↦ dst.
  Lemma xdlchain_singleton_2 src node dst :
    node.[xdlchain_prev] ↦ src -∗
    node.[xdlchain_next] ↦ dst -∗
    xdlchain src [node] dst.

  #[local] Lemma xdlchain_cons_unfold {src} node nodes dst :
    xdlchain src (node :: nodes) dst ⊣⊢
      node.[xdlchain_prev] ↦ src ∗
      match nodes with
      | [] ⇒
          node.[xdlchain_next] ↦ dst
      | node' :: _ ⇒
          node.[xdlchain_next] ↦ #node' ∗
          xdlchain #node nodes dst
      end.

  Lemma xdlchain_cons {src} nodes node nodes' dst :
    nodes = node :: nodes' →
    xdlchain src nodes dst ⊣⊢
      node.[xdlchain_prev] ↦ src ∗
      node.[xdlchain_next] ↦ from_option #@{location} dst (head nodes') ∗
      xdlchain #node nodes' dst.
  Lemma xdlchain_cons_1 {src} nodes node nodes' dst :
    nodes = node :: nodes' →
    xdlchain src nodes dst ⊢
      node.[xdlchain_prev] ↦ src ∗
      node.[xdlchain_next] ↦ from_option #@{location} dst (head nodes') ∗
      xdlchain #node nodes' dst.
  Lemma xdlchain_cons_2 src node nodes dst :
    node.[xdlchain_prev] ↦ src -∗
    node.[xdlchain_next] ↦ from_option #@{location} dst (head nodes) -∗
    xdlchain #node nodes dst -∗
    xdlchain src (node :: nodes) dst.

  Lemma xdlchain_app {src} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xdlchain src nodes dst ⊣⊢
      xdlchain src nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xdlchain (from_option #@{location} src (last nodes1)) nodes2 dst.
  Lemma xdlchain_app_1 {src} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xdlchain src nodes dst ⊢
      xdlchain src nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xdlchain (from_option #@{location} src (last nodes1)) nodes2 dst.
  Lemma xdlchain_app_2 src nodes1 nodes2 dst :
    xdlchain src nodes1 (from_option #@{location} dst (head nodes2)) -∗
    xdlchain (from_option #@{location} src (last nodes1)) nodes2 dst -∗
    xdlchain src (nodes1 ++ nodes2) dst.

  Lemma xdlchain_snoc {src} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xdlchain src nodes dst ⊣⊢
      xdlchain src nodes' #node ∗
      node.[xdlchain_prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[xdlchain_next] ↦ dst.
  Lemma xdlchain_snoc_1 {src} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xdlchain src nodes dst ⊢
      xdlchain src nodes' #node ∗
      node.[xdlchain_prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[xdlchain_next] ↦ dst.
  Lemma xdlchain_snoc_2 src nodes node dst :
    xdlchain src nodes #node -∗
    node.[xdlchain_prev] ↦ from_option #@{location} src (last nodes) -∗
    node.[xdlchain_next] ↦ dst -∗
    xdlchain src (nodes ++ [node]) dst.

  Lemma xdlchain_last {src nodes} node dst :
    last nodes = Some node →
    xdlchain src nodes dst ⊢
      ∃ nodes',
      ⌜nodes = nodes' ++ [node]⌝ ∗
      xdlchain src nodes' #node ∗
      node.[xdlchain_prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[xdlchain_next] ↦ dst.

  Lemma xdlchain_lookup {src nodes} i node dst :
    nodes !! i = Some node →
    xdlchain src nodes dst ⊣⊢
      xdlchain src (take i nodes) #node ∗
      node.[xdlchain_prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[xdlchain_next] ↦ from_option #@{location} dst (head $ drop (S i) nodes) ∗
      xdlchain #node (drop (S i) nodes) dst.
  Lemma xdlchain_lookup_1 {src nodes} i node dst :
    nodes !! i = Some node →
    xdlchain src nodes dst ⊢
      xdlchain src (take i nodes) #node ∗
      node.[xdlchain_prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[xdlchain_next] ↦ from_option #@{location} dst (head $ drop (S i) nodes) ∗
      xdlchain #node (drop (S i) nodes) dst.
  Lemma xdlchain_lookup_2 {src nodes} i node prev next dst :
    nodes !! i = Some node →
    prev = from_option #@{location} src (last $ take i nodes) →
    next = from_option #@{location} dst (head $ drop (S i) nodes) →
    xdlchain src (take i nodes) #node -∗
    node.[xdlchain_prev] ↦ prev -∗
    node.[xdlchain_next] ↦ next -∗
    xdlchain #node (drop (S i) nodes) dst -∗
    xdlchain src nodes dst.

  Lemma xdlchain_lookup_acc {src nodes} i node dst :
    nodes !! i = Some node →
    xdlchain src nodes dst ⊢
      node.[xdlchain_prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[xdlchain_next] ↦ from_option #@{location} dst (head $ drop (S i) nodes) ∗
      ( node.[xdlchain_prev] ↦ from_option #@{location} src (last $ take i nodes) -∗
        node.[xdlchain_next] ↦ from_option #@{location} dst (head $ drop (S i) nodes) -∗
        xdlchain src nodes dst
      ).

  Lemma xdlchain_exclusive src1 src2 nodes dst1 dst2 :
    0 < length nodes →
    xdlchain src1 nodes dst1 -∗
    xdlchain src2 nodes dst2 -∗
    False.

  Lemma xdlchain_NoDup src nodes dst :
    xdlchain src nodes dst ⊢
    ⌜NoDup nodes⌝.

  Lemma xdlchain٠prev𑁒spec {src nodes node} nodes' dst E :
    nodes = node :: nodes' →
    {{{
      xdlchain src nodes dst
    }}}
      (#node).{xdlchain_prev} @ E
    {{{
      RET src;
      xdlchain src nodes dst
    }}}.
  Lemma xdlchain٠prev𑁒spec_lookup {src nodes} i node dst E :
    nodes !! i = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      (#node).{xdlchain_prev} @ E
    {{{
      RET from_option #@{location} src (last $ take i nodes);
      xdlchain src nodes dst
    }}}.
  Lemma xdlchain٠prev𑁒spec_head {src nodes} node dst E :
    head nodes = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      (#node).{xdlchain_prev} @ E
    {{{
      RET src;
      xdlchain src nodes dst
    }}}.

  Lemma xdlchain٠next𑁒spec {src nodes node} nodes' dst E :
    nodes = node :: nodes' →
    {{{
      xdlchain src nodes dst
    }}}
      (#node).{xdlchain_next} @ E
    {{{
      RET from_option #@{location} dst (head nodes');
      xdlchain src nodes dst
    }}}.
  Lemma xdlchain٠next𑁒spec_lookup {src nodes} i node dst E :
    nodes !! i = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      (#node).{xdlchain_next} @ E
    {{{
      RET from_option #@{location} dst (head $ drop (S i) nodes);
      xdlchain src nodes dst
    }}}.
  Lemma xdlchain٠next𑁒spec_last {src nodes} node dst E :
    last nodes = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      (#node).{xdlchain_next} @ E
    {{{
      RET dst;
      xdlchain src nodes dst
    }}}.

  Lemma xdlchain٠set_prev𑁒spec {src nodes node} nodes' dst v E :
    nodes = node :: nodes' →
    {{{
      xdlchain src nodes dst
    }}}
      #node <-{xdlchain_prev} v @ E
    {{{
      RET ();
      xdlchain v nodes dst
    }}}.
  Lemma xdlchain٠set_prev𑁒spec_lookup {src nodes} i node dst v E :
    nodes !! i = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      #node <-{xdlchain_prev} v @ E
    {{{
      RET ();
      xdlchain src (take i nodes) #node ∗
      xdlchain v (drop i nodes) dst
    }}}.
  Lemma xdlchain٠set_prev𑁒spec_head {src nodes} node dst v E :
    head nodes = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      #node <-{xdlchain_prev} v @ E
    {{{
      RET ();
      xdlchain v nodes dst
    }}}.

  Lemma xdlchain٠set_next𑁒spec {src nodes node} nodes' dst v E :
    nodes = node :: nodes' →
    {{{
      xdlchain src nodes dst
    }}}
      #node <-{xdlchain_next} v @ E
    {{{
      RET ();
      xdlchain src [node] v ∗
      xdlchain #node nodes' dst
    }}}.
  Lemma xdlchain٠set_next𑁒spec_lookup {src nodes} i node dst v E :
    nodes !! i = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      #node <-{xdlchain_next} v @ E
    {{{
      RET ();
      xdlchain src (take (S i) nodes) v ∗
      xdlchain #node (drop (S i) nodes) dst
    }}}.
  Lemma xdlchain٠set_next𑁒spec_last {src nodes} node dst v E :
    last nodes = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      #node <-{xdlchain_next} v @ E
    {{{
      RET ();
      xdlchain src nodes v
    }}}.
End zoo_G.

From zoo_std Require
  xdlchain__opaque.

#[global] Opaque xdlchain.