Library zoo_std.xdlchain

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.base.
Require Export zoo_std.xdlchain__code.
Require Import zoo_std.xdlchain__types.
Require Import zoo.options.

Implicit Type node : location.
Implicit Type nodes : list location.
Implicit Type 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.[prev] ↦ src ∗
        match nodes with
        | [] ⇒
            node.[next] ↦ dst
        | node' :: _ ⇒
            node.[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.[prev] ↦ src ∗
      node.[next] ↦ dst.
  Lemma xdlchainｰsingleton₁ src node dst :
    xdlchain src [node] dst ⊢
      node.[prev] ↦ src ∗
      node.[next] ↦ dst.
  Lemma xdlchainｰsingleton₂ src node dst :
    node.[prev] ↦ src -∗
    node.[next] ↦ dst -∗
    xdlchain src [node] dst.

  #[local] Lemma xdlchainｰconsｰunfold {src} node nodes dst :
    xdlchain src (node :: nodes) dst ⊣⊢
      node.[prev] ↦ src ∗
      match nodes with
      | [] ⇒
          node.[next] ↦ dst
      | node' :: _ ⇒
          node.[next] ↦ #node' ∗
          xdlchain #node nodes dst
      end.

  Lemma xdlchainｰcons {src} nodes node nodes' dst :
    nodes = node :: nodes' →
    xdlchain src nodes dst ⊣⊢
      node.[prev] ↦ src ∗
      node.[next] ↦ from_option #@{location} dst (head nodes') ∗
      xdlchain #node nodes' dst.
  Lemma xdlchainｰcons₁ {src} nodes node nodes' dst :
    nodes = node :: nodes' →
    xdlchain src nodes dst ⊢
      node.[prev] ↦ src ∗
      node.[next] ↦ from_option #@{location} dst (head nodes') ∗
      xdlchain #node nodes' dst.
  Lemma xdlchainｰcons₂ src node nodes dst :
    node.[prev] ↦ src -∗
    node.[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₁ {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₂ 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.[prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[next] ↦ dst.
  Lemma xdlchainｰsnoc₁ {src} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xdlchain src nodes dst ⊢
      xdlchain src nodes' #node ∗
      node.[prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[next] ↦ dst.
  Lemma xdlchainｰsnoc₂ src nodes node dst :
    xdlchain src nodes #node -∗
    node.[prev] ↦ from_option #@{location} src (last nodes) -∗
    node.[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.[prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[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.[prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[next] ↦ from_option #@{location} dst (head $ drop ˖i nodes) ∗
      xdlchain #node (drop ˖i nodes) dst.
  Lemma xdlchainｰlookup₁ {src nodes} i node dst :
    nodes !! i = Some node →
    xdlchain src nodes dst ⊢
      xdlchain src (take i nodes) #node ∗
      node.[prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[next] ↦ from_option #@{location} dst (head $ drop ˖i nodes) ∗
      xdlchain #node (drop ˖i nodes) dst.
  Lemma xdlchainｰlookup₂ {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 ˖i nodes) →
    xdlchain src (take i nodes) #node -∗
    node.[prev] ↦ prev -∗
    node.[next] ↦ next -∗
    xdlchain #node (drop ˖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.[prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[next] ↦ from_option #@{location} dst (head $ drop ˖i nodes) ∗
      ( node.[prev] ↦ from_option #@{location} src (last $ take i nodes) -∗
        node.[next] ↦ from_option #@{location} dst (head $ drop ˖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).{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).{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).{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).{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).{next} @ E
    {{{
      RET from_option #@{location} dst (head $ drop ˖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).{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 <-{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 <-{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 <-{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 <-{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 <-{next} v @ E
    {{{
      RET ();
      xdlchain src (take ˖i nodes) v ∗
      xdlchain #node (drop ˖i nodes) dst
    }}}.
  Lemma xdlchain٠set_nextｰspecｰlast {src nodes} node dst v E :
    last nodes = Some node →
    {{{
      xdlchain src nodes dst
    }}}
      #node <-{next} v @ E
    {{{
      RET ();
      xdlchain src nodes v
    }}}.
End zoo۰G.

Require zoo_std.xdlchain__opaque.

#[global] Opaque xdlchain.