Library zoo_std.xtdlchain

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo_std.xdlchain.
Require Export zoo_std.xtdlchain__code.
Require Import zoo_std.xtdlchain__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 Σ}.

  Definition xtdlchain hdr src nodes dst : iProp Σ :=
    xdlchain src nodes dst ∗
    [∗ list] node ∈ nodes, headers۰at node hdr.

  #[global] Instance xtdlchainｰtimeless hdr src nodes dst :
    Timeless (xtdlchain hdr src nodes dst).

  Lemma xtdlchainｰnil hdr src dst :
    ⊢ xtdlchain hdr src [] dst.

  Lemma xtdlchainｰsingleton hdr src node dst :
    xtdlchain hdr src [node] dst ⊣⊢
      node ↦ₕ hdr ∗
      node.[prev] ↦ src ∗
      node.[next] ↦ dst.
  Lemma xtdlchainｰsingleton₁ hdr src node dst :
    xtdlchain hdr src [node] dst ⊢
      node ↦ₕ hdr ∗
      node.[prev] ↦ src ∗
      node.[next] ↦ dst.
  Lemma xtdlchainｰsingleton₂ hdr src node dst :
    node ↦ₕ hdr ∗
    node.[prev] ↦ src -∗
    node.[next] ↦ dst -∗
    xtdlchain hdr src [node] dst.

  Lemma xtdlchainｰcons {hdr src} nodes node nodes' dst :
    nodes = node :: nodes' →
    xtdlchain hdr src nodes dst ⊣⊢
      node ↦ₕ hdr ∗
      node.[prev] ↦ src ∗
      node.[next] ↦ from_option #@{location} dst (head nodes') ∗
      xtdlchain hdr #node nodes' dst.
  Lemma xtdlchainｰcons₁ {hdr src} nodes node nodes' dst :
    nodes = node :: nodes' →
    xtdlchain hdr src nodes dst ⊢
      node ↦ₕ hdr ∗
      node.[prev] ↦ src ∗
      node.[next] ↦ from_option #@{location} dst (head nodes') ∗
      xtdlchain hdr #node nodes' dst.
  Lemma xtdlchainｰcons₂ hdr src node nodes dst :
    node ↦ₕ hdr ∗
    node.[prev] ↦ src -∗
    node.[next] ↦ from_option #@{location} dst (head nodes) -∗
    xtdlchain hdr #node nodes dst -∗
    xtdlchain hdr src (node :: nodes) dst.

  Lemma xtdlchainｰapp {hdr src} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xtdlchain hdr src nodes dst ⊣⊢
      xtdlchain hdr src nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xtdlchain hdr (from_option #@{location} src (last nodes1)) nodes2 dst.
  Lemma xtdlchainｰapp₁ {hdr src} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xtdlchain hdr src nodes dst ⊢
      xtdlchain hdr src nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xtdlchain hdr (from_option #@{location} src (last nodes1)) nodes2 dst.
  Lemma xtdlchainｰapp₂ hdr src nodes1 nodes2 dst :
    xtdlchain hdr src nodes1 (from_option #@{location} dst (head nodes2)) -∗
    xtdlchain hdr (from_option #@{location} src (last nodes1)) nodes2 dst -∗
    xtdlchain hdr src (nodes1 ++ nodes2) dst.

  Lemma xtdlchainｰsnoc {hdr src} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xtdlchain hdr src nodes dst ⊣⊢
      xtdlchain hdr src nodes' #node ∗
      node ↦ₕ hdr ∗
      node.[prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[next] ↦ dst.
  Lemma xtdlchainｰsnoc₁ {hdr src} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xtdlchain hdr src nodes dst ⊢
      xtdlchain hdr src nodes' #node ∗
      node ↦ₕ hdr ∗
      node.[prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[next] ↦ dst.
  Lemma xtdlchainｰsnoc₂ hdr src nodes node dst :
    xtdlchain hdr src nodes #node -∗
    node ↦ₕ hdr -∗
    node.[prev] ↦ from_option #@{location} src (last nodes) -∗
    node.[next] ↦ dst -∗
    xtdlchain hdr src (nodes ++ [node]) dst.

  Lemma xtdlchainｰlast {hdr src nodes} node dst :
    last nodes = Some node →
    xtdlchain hdr src nodes dst ⊢
      ∃ nodes',
      ⌜nodes = nodes' ++ [node]⌝ ∗
      xtdlchain hdr src nodes' #node ∗
      node ↦ₕ hdr ∗
      node.[prev] ↦ from_option #@{location} src (last nodes') ∗
      node.[next] ↦ dst.

  Lemma xtdlchainｰlookup {hdr src nodes} i node dst :
    nodes !! i = Some node →
    xtdlchain hdr src nodes dst ⊣⊢
      xtdlchain hdr src (take i nodes) #node ∗
      node ↦ₕ hdr ∗
      node.[prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[next] ↦ from_option #@{location} dst (head $ drop ˖i nodes) ∗
      xtdlchain hdr #node (drop ˖i nodes) dst.
  Lemma xtdlchainｰlookup₁ {hdr src nodes} i node dst :
    nodes !! i = Some node →
    xtdlchain hdr src nodes dst ⊢
      xtdlchain hdr src (take i nodes) #node ∗
      node ↦ₕ hdr ∗
      node.[prev] ↦ from_option #@{location} src (last $ take i nodes) ∗
      node.[next] ↦ from_option #@{location} dst (head $ drop ˖i nodes) ∗
      xtdlchain hdr #node (drop ˖i nodes) dst.
  Lemma xtdlchainｰlookup₂ {hdr 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) →
    xtdlchain hdr src (take i nodes) #node -∗
    node ↦ₕ hdr -∗
    node.[prev] ↦ prev -∗
    node.[next] ↦ next -∗
    xtdlchain hdr #node (drop ˖i nodes) dst -∗
    xtdlchain hdr src nodes dst.

  Lemma xtdlchainｰlookupｰacc {hdr src nodes} i node dst :
    nodes !! i = Some node →
    xtdlchain hdr src nodes dst ⊢
      node ↦ₕ hdr ∗
      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) -∗
        xtdlchain hdr src nodes dst
      ).

  Lemma xtdlchainｰlookupｰheader {hdr src nodes} i node dst :
    nodes !! i = Some node →
    xtdlchain hdr src nodes dst ⊢
    node ↦ₕ hdr.

  Lemma xtdlchainｰexclusive hdr src1 src2 nodes dst1 dst2 :
    0 < length nodes →
    xtdlchain hdr src1 nodes dst1 -∗
    xtdlchain hdr src2 nodes dst2 -∗
    False.

  Lemma xtdlchainｰNoDup hdr src nodes dst :
    xtdlchain hdr src nodes dst ⊢
    ⌜NoDup nodes⌝.

  Lemma xtdlchain٠prevｰspec {hdr src nodes node} nodes' dst E :
    nodes = node :: nodes' →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      (#node).{prev} @ E
    {{{
      RET src;
      xtdlchain hdr src nodes dst
    }}}.
  Lemma xtdlchain٠prevｰspecｰlookup {hdr src nodes} i node dst E :
    nodes !! i = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      (#node).{prev} @ E
    {{{
      RET from_option #@{location} src (last $ take i nodes);
      xtdlchain hdr src nodes dst
    }}}.
  Lemma xtdlchain٠prevｰspecｰhead {hdr src nodes} node dst E :
    head nodes = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      (#node).{prev} @ E
    {{{
      RET src;
      xtdlchain hdr src nodes dst
    }}}.

  Lemma xtdlchain٠nextｰspec {hdr src nodes node} nodes' dst E :
    nodes = node :: nodes' →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      (#node).{next} @ E
    {{{
      RET from_option #@{location} dst (head nodes');
      xtdlchain hdr src nodes dst
    }}}.
  Lemma xtdlchain٠nextｰspecｰlookup {hdr src nodes} i node dst E :
    nodes !! i = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      (#node).{next} @ E
    {{{
      RET from_option #@{location} dst (head $ drop ˖i nodes);
      xtdlchain hdr src nodes dst
    }}}.
  Lemma xtdlchain٠nextｰspecｰlast {hdr src nodes} node dst E :
    last nodes = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      (#node).{next} @ E
    {{{
      RET dst;
      xtdlchain hdr src nodes dst
    }}}.

  Lemma xtdlchain٠set_prevｰspec {hdr src nodes node} nodes' dst v E :
    nodes = node :: nodes' →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      #node <-{prev} v @ E
    {{{
      RET ();
      xtdlchain hdr v nodes dst
    }}}.
  Lemma xtdlchain٠set_prevｰspecｰlookup {hdr src nodes} i node dst v E :
    nodes !! i = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      #node <-{prev} v @ E
    {{{
      RET ();
      xtdlchain hdr src (take i nodes) #node ∗
      xtdlchain hdr v (drop i nodes) dst
    }}}.
  Lemma xtdlchain٠set_prevｰspecｰhead {hdr src nodes} node dst v E :
    head nodes = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      #node <-{prev} v @ E
    {{{
      RET ();
      xtdlchain hdr v nodes dst
    }}}.

  Lemma xtdlchain٠set_nextｰspec {hdr src nodes node} nodes' dst v E :
    nodes = node :: nodes' →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      #node <-{next} v @ E
    {{{
      RET ();
      xtdlchain hdr src [node] v ∗
      xtdlchain hdr #node nodes' dst
    }}}.
  Lemma xtdlchain٠set_nextｰspecｰlookup {hdr src nodes} i node dst v E :
    nodes !! i = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      #node <-{next} v @ E
    {{{
      RET ();
      xtdlchain hdr src (take ˖i nodes) v ∗
      xtdlchain hdr #node (drop ˖i nodes) dst
    }}}.
  Lemma xtdlchain٠set_nextｰspecｰlast {hdr src nodes} node dst v E :
    last nodes = Some node →
    {{{
      xtdlchain hdr src nodes dst
    }}}
      #node <-{next} v @ E
    {{{
      RET ();
      xtdlchain hdr src nodes v
    }}}.
End zoo۰G.

Require zoo_std.xtdlchain__opaque.

#[global] Opaque xtdlchain.