Library zoo_std.xtchain

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  xtchain__types.
From zoo_std Require Import
  xchain.
From zoo Require Import
  options.

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

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

  Definition xtchain hdr dq nodes dst : iProp Σ :=
    xchain dq nodes dst ∗
    [∗ list] node ∈ nodes, node ↦ₕ hdr.

  #[global] Instance xtchain_timeless hdr dq nodes dst :
    Timeless (xtchain hdr dq nodes dst).

  #[global] Instance xtchain_persistent hdr nodes dst :
    Persistent (xtchain hdr DfracDiscarded nodes dst).

  Lemma xtchain_nil hdr dq dst :
    ⊢ xtchain hdr dq [] dst.

  Lemma xtchain_singleton hdr dq node dst :
    xtchain hdr dq [node] dst ⊣⊢
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} dst.
  Lemma xtchain_singleton_1 hdr dq node dst :
    xtchain hdr dq [node] dst ⊢
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} dst.
  Lemma xtchain_singleton_2 hdr dq node dst :
    node ↦ₕ hdr ∗
    node.[xtchain_next] ↦{dq} dst -∗
    xtchain hdr dq [node] dst.

  Lemma xtchain_cons {hdr dq} nodes node nodes' dst :
    nodes = node :: nodes' →
    xtchain hdr dq nodes dst ⊣⊢
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} from_option #@{location} dst (head nodes') ∗
      xtchain hdr dq nodes' dst.
  Lemma xtchain_cons' {hdr dq} node nodes dst :
    xtchain hdr dq (node :: nodes) dst ⊣⊢
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} from_option #@{location} dst (head nodes) ∗
      xtchain hdr dq nodes dst.
  Lemma xtchain_cons_1 {hdr dq} nodes node nodes' dst :
    nodes = node :: nodes' →
    xtchain hdr dq nodes dst ⊢
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} from_option #@{location} dst (head nodes') ∗
      xtchain hdr dq nodes' dst.
  Lemma xtchain_cons_1' {hdr dq} node nodes dst :
    xtchain hdr dq (node :: nodes) dst ⊢
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} from_option #@{location} dst (head nodes) ∗
      xtchain hdr dq nodes dst.
  Lemma xtchain_cons_2 hdr dq node nodes dst :
    node ↦ₕ hdr -∗
    node.[xtchain_next] ↦{dq} from_option #@{location} dst (head nodes) -∗
    xtchain hdr dq nodes dst -∗
    xtchain hdr dq (node :: nodes) dst.

  Lemma xtchain_app {hdr dq} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xtchain hdr dq nodes dst ⊣⊢
      xtchain hdr dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xtchain hdr dq nodes2 dst.
  Lemma xtchain_app' {hdr dq} nodes1 nodes2 dst :
    xtchain hdr dq (nodes1 ++ nodes2) dst ⊣⊢
      xtchain hdr dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xtchain hdr dq nodes2 dst.
  Lemma xtchain_app_1 {hdr dq} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xtchain hdr dq nodes dst ⊢
      xtchain hdr dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xtchain hdr dq nodes2 dst.
  Lemma xtchain_app_1' {hdr dq} nodes1 nodes2 dst :
    xtchain hdr dq (nodes1 ++ nodes2) dst ⊢
      xtchain hdr dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xtchain hdr dq nodes2 dst.
  Lemma xtchain_app_2 hdr dq nodes1 nodes2 dst :
    xtchain hdr dq nodes1 (from_option #@{location} dst (head nodes2)) -∗
    xtchain hdr dq nodes2 dst -∗
    xtchain hdr dq (nodes1 ++ nodes2) dst.

  Lemma xtchain_snoc {hdr dq} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xtchain hdr dq nodes dst ⊣⊢
      xtchain hdr dq nodes' #node ∗
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} dst.
  Lemma xtchain_snoc' {hdr dq} nodes node dst :
    xtchain hdr dq (nodes ++ [node]) dst ⊣⊢
      xtchain hdr dq nodes #node ∗
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} dst.
  Lemma xtchain_snoc_1 {hdr dq} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xtchain hdr dq nodes dst ⊢
      xtchain hdr dq nodes' #node ∗
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} dst.
  Lemma xtchain_snoc_1' {hdr dq} nodes node dst :
    xtchain hdr dq (nodes ++ [node]) dst ⊢
      xtchain hdr dq nodes #node ∗
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} dst.
  Lemma xtchain_snoc_2 hdr dq nodes node dst :
    xtchain hdr dq nodes #node -∗
    node ↦ₕ hdr -∗
    node.[xtchain_next] ↦{dq} dst -∗
    xtchain hdr dq (nodes ++ [node]) dst.

  Lemma xtchain_lookup {hdr dq nodes} i node dst :
    nodes !! i = Some node →
    xtchain hdr dq nodes dst ⊣⊢
      xtchain hdr dq (take i nodes) #node ∗
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) ∗
      xtchain hdr dq (drop (S i) nodes) dst.
  Lemma xtchain_lookup_1 {hdr dq nodes} i node dst :
    nodes !! i = Some node →
    xtchain hdr dq nodes dst ⊢
      xtchain hdr dq (take i nodes) #node ∗
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) ∗
      xtchain hdr dq (drop (S i) nodes) dst.
  Lemma xtchain_lookup_2 {hdr dq nodes} i node next dst :
    nodes !! i = Some node →
    next = from_option #@{location} dst (nodes !! S i) →
    xtchain hdr dq (take i nodes) #node -∗
    node ↦ₕ hdr -∗
    node.[xtchain_next] ↦{dq} next -∗
    xtchain hdr dq (drop (S i) nodes) dst -∗
    xtchain hdr dq nodes dst.
  Lemma xtchain_lookup_acc {hdr dq nodes} i node dst :
    nodes !! i = Some node →
    xtchain hdr dq nodes dst ⊢
      node ↦ₕ hdr ∗
      node.[xtchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) ∗
      ( node.[xtchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) -∗
        xtchain hdr dq nodes dst
      ).

  Lemma xtchain_lookup_header {hdr dq nodes} i node dst :
    nodes !! i = Some node →
    xtchain hdr dq nodes dst ⊢
    node ↦ₕ hdr.

  Lemma xtchain_last {hdr dq nodes dst} node :
    last nodes = Some node →
    xtchain hdr dq nodes dst ⊣⊢
      xtchain hdr dq (removelast nodes) #node ∗
      node.[xtchain_next] ↦{dq} dst ∗
      node ↦ₕ hdr.
  Lemma xtchain_last_acc {hdr dq nodes dst} node :
    last nodes = Some node →
    xtchain hdr dq nodes dst ⊢
      node.[xtchain_next] ↦{dq} dst ∗
      node ↦ₕ hdr ∗
      ( ∀ dst,
        node.[xtchain_next] ↦{dq} dst -∗
        xtchain hdr dq nodes dst
      ).

  Lemma xtchain_valid hdr dq nodes dst :
    0 < length nodes →
    xtchain hdr dq nodes dst ⊢
    ⌜✓ dq⌝.
  Lemma xtchain_combine hdr nodes dq1 dst1 dq2 dst2 :
    0 < length nodes →
    xtchain hdr dq1 nodes dst1 -∗
    xtchain hdr dq2 nodes dst2 -∗
      ⌜dst1 = dst2⌝ ∗
      xtchain hdr (dq1 ⋅ dq2) nodes dst1.
  Lemma xtchain_valid_2 hdr nodes dq1 dst1 dq2 dst2 :
    0 < length nodes →
    xtchain hdr dq1 nodes dst1 -∗
    xtchain hdr dq2 nodes dst2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜dst1 = dst2⌝.
  Lemma xtchain_agree hdr nodes dq1 dst1 dq2 dst2 :
    0 < length nodes →
    xtchain hdr dq1 nodes dst1 -∗
    xtchain hdr dq2 nodes dst2 -∗
    ⌜dst1 = dst2⌝.
  Lemma xtchain_dfrac_ne hdr dq1 nodes1 dst1 dq2 nodes2 dst2 :
    0 < length nodes1 →
    ¬ ✓ (dq1 ⋅ dq2) →
    xtchain hdr dq1 nodes1 dst1 -∗
    xtchain hdr dq2 nodes2 dst2 -∗
    ⌜nodes1 ≠ nodes2⌝.
  Lemma xtchain_ne hdr nodes1 dst1 dq2 nodes2 dst2 :
    0 < length nodes1 →
    xtchain hdr (DfracOwn 1) nodes1 dst1 -∗
    xtchain hdr dq2 nodes2 dst2 -∗
    ⌜nodes1 ≠ nodes2⌝.
  Lemma xtchain_exclusive hdr nodes dst1 dq2 dst2 :
    0 < length nodes →
    xtchain hdr (DfracOwn 1) nodes dst1 -∗
    xtchain hdr dq2 nodes dst2 -∗
    False.
  Lemma xtchain_persist hdr dq nodes dst :
    xtchain hdr dq nodes dst ⊢ |==>
    xtchain hdr DfracDiscarded nodes dst.

  Lemma xtchain_NoDup hdr nodes dst :
    xtchain hdr (DfracOwn 1) nodes dst ⊢
    ⌜NoDup nodes⌝.

  Lemma xtchain٠next𑁒spec {hdr dq nodes dst node} nodes' E :
    nodes = node :: nodes' →
    {{{
      xtchain dq hdr nodes dst
    }}}
      (#node).{xtchain_next} @ E
    {{{
      RET from_option #@{location} dst (head nodes');
      xtchain dq hdr nodes dst
    }}}.
  Lemma xtchain٠next𑁒spec_lookup {hdr dq nodes dst} i node E :
    nodes !! i = Some node →
    {{{
      xtchain hdr dq nodes dst
    }}}
      (#node).{xtchain_next} @ E
    {{{
      RET from_option #@{location} dst (nodes !! S i);
      xtchain hdr dq nodes dst
    }}}.
  Lemma xtchain٠next𑁒spec_last hdr dq nodes dst node E :
    last nodes = Some node →
    {{{
      xtchain hdr dq nodes dst
    }}}
      (#node).{xtchain_next} @ E
    {{{
      RET dst;
      xtchain hdr dq nodes dst
    }}}.

  Lemma xtchain٠set_next𑁒spec {hdr nodes dst node} nodes' v E :
    nodes = node :: nodes' →
    {{{
      xtchain hdr (DfracOwn 1) nodes dst
    }}}
      (#node) <-{xtchain_next} v @ E
    {{{
      RET ();
      xtchain hdr (DfracOwn 1) [node] v ∗
      xtchain hdr (DfracOwn 1) nodes' dst
    }}}.
  Lemma xtchain٠set_next𑁒spec_lookup {hdr nodes dst} i node v E :
    nodes !! i = Some node →
    {{{
      xtchain hdr (DfracOwn 1) nodes dst
    }}}
      #node <-{xtchain_next} v @ E
    {{{
      RET ();
      xtchain hdr (DfracOwn 1) (take (S i) nodes) v ∗
      xtchain hdr (DfracOwn 1) (drop (S i) nodes) dst
    }}}.
  Lemma xtchain٠set_next𑁒spec_last hdr nodes dst node v E :
    last nodes = Some node →
    {{{
      xtchain hdr (DfracOwn 1) nodes dst
    }}}
      #node <-{xtchain_next} v @ E
    {{{
      RET ();
      xtchain hdr (DfracOwn 1) nodes v
    }}}.
  Lemma xtchain٠set_next𑁒spec_last' {hdr nodes dst node} node' dst' E :
    last nodes = Some node →
    {{{
      xtchain hdr (DfracOwn 1) nodes dst ∗
      node'.[xtchain_next] ↦ dst' ∗
      node' ↦ₕ hdr
    }}}
      #node <-{xtchain_next} #node' @ E
    {{{
      RET ();
      xtchain hdr (DfracOwn 1) (nodes ++ [node']) dst'
    }}}.
End zoo_G.

From zoo_std Require
  xtchain__opaque.

#[global] Opaque xtchain.