Library zoo_std.xchain

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
  xchain__types.
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 Σ}.

  Fixpoint xchain dq nodes dst : iProp Σ :=
    match nodes with
    | [] ⇒
        True
    | node :: nodes ⇒
        match nodes with
        | [] ⇒
            node.[xchain_next] ↦{dq} dst
        | node' :: _ ⇒
            node.[xchain_next] ↦{dq} #node' ∗
            xchain dq nodes dst
        end
    end.
  #[global] Arguments xchain _ !_ _ / : assert.

  #[global] Instance xchain_timeless dq nodes dst :
    Timeless (xchain dq nodes dst).

  #[global] Instance xchain_persistent nodes dst :
    Persistent (xchain DfracDiscarded nodes dst).

  Lemma xchain_nil dst :
    ⊢ xchain (DfracOwn 1) [] dst.

  Lemma xchain_singleton dq node dst :
    xchain dq [node] dst ⊣⊢
    node.[xchain_next] ↦{dq} dst.
  Lemma xchain_singleton_1 dq node dst :
    xchain dq [node] dst ⊢
    node.[xchain_next] ↦{dq} dst.
  Lemma xchain_singleton_2 dq node dst :
    node.[xchain_next] ↦{dq} dst ⊢
    xchain dq [node] dst.

  Lemma xchain_cons {dq} nodes node nodes' dst :
    nodes = node :: nodes' →
    xchain dq nodes dst ⊣⊢
      node.[xchain_next] ↦{dq} from_option #@{location} dst (head nodes') ∗
      xchain dq nodes' dst.
  Lemma xchain_cons' {dq} node nodes dst :
    xchain dq (node :: nodes) dst ⊣⊢
      node.[xchain_next] ↦{dq} from_option #@{location} dst (head nodes) ∗
      xchain dq nodes dst.
  Lemma xchain_cons_1 {dq} nodes node nodes' dst :
    nodes = node :: nodes' →
    xchain dq nodes dst ⊢
      node.[xchain_next] ↦{dq} from_option #@{location} dst (head nodes') ∗
      xchain dq nodes' dst.
  Lemma xchain_cons_1' {dq} node nodes dst :
    xchain dq (node :: nodes) dst ⊢
      node.[xchain_next] ↦{dq} from_option #@{location} dst (head nodes) ∗
      xchain dq nodes dst.
  Lemma xchain_cons_2 dq node nodes dst :
    node.[xchain_next] ↦{dq} from_option #@{location} dst (head nodes) -∗
    xchain dq nodes dst -∗
    xchain dq (node :: nodes) dst.

  Lemma xchain_app {dq} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xchain dq nodes dst ⊣⊢
      xchain dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xchain dq nodes2 dst.
  Lemma xchain_app' {dq} nodes1 nodes2 dst :
    xchain dq (nodes1 ++ nodes2) dst ⊣⊢
      xchain dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xchain dq nodes2 dst.
  Lemma xchain_app_1 {dq} nodes nodes1 nodes2 dst :
    nodes = nodes1 ++ nodes2 →
    xchain dq nodes dst ⊢
      xchain dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xchain dq nodes2 dst.
  Lemma xchain_app_1' {dq} nodes1 nodes2 dst :
    xchain dq (nodes1 ++ nodes2) dst ⊢
      xchain dq nodes1 (from_option #@{location} dst (head nodes2)) ∗
      xchain dq nodes2 dst.
  Lemma xchain_app_2 dq nodes1 nodes2 dst :
    xchain dq nodes1 (from_option #@{location} dst (head nodes2)) -∗
    xchain dq nodes2 dst -∗
    xchain dq (nodes1 ++ nodes2) dst.

  Lemma xchain_snoc {dq} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xchain dq nodes dst ⊣⊢
      xchain dq nodes' #node ∗
      node.[xchain_next] ↦{dq} dst.
  Lemma xchain_snoc' {dq} nodes node dst :
    xchain dq (nodes ++ [node]) dst ⊣⊢
      xchain dq nodes #node ∗
      node.[xchain_next] ↦{dq} dst.
  Lemma xchain_snoc_1 {dq} nodes nodes' node dst :
    nodes = nodes' ++ [node] →
    xchain dq nodes dst ⊢
      xchain dq nodes' #node ∗
      node.[xchain_next] ↦{dq} dst.
  Lemma xchain_snoc_1' {dq} nodes node dst :
    xchain dq (nodes ++ [node]) dst ⊢
      xchain dq nodes #node ∗
      node.[xchain_next] ↦{dq} dst.
  Lemma xchain_snoc_2 dq nodes node dst :
    xchain dq nodes #node -∗
    node.[xchain_next] ↦{dq} dst -∗
    xchain dq (nodes ++ [node]) dst.

  Lemma xchain_lookup {dq nodes} i node dst :
    nodes !! i = Some node →
    xchain dq nodes dst ⊣⊢
      xchain dq (take i nodes) #node ∗
      node.[xchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) ∗
      xchain dq (drop (S i) nodes) dst.
  Lemma xchain_lookup_1 {dq nodes} i node dst :
    nodes !! i = Some node →
    xchain dq nodes dst ⊢
      xchain dq (take i nodes) #node ∗
      node.[xchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) ∗
      xchain dq (drop (S i) nodes) dst.
  Lemma xchain_lookup_2 {dq nodes} i node next dst :
    nodes !! i = Some node →
    next = from_option #@{location} dst (nodes !! S i) →
    xchain dq (take i nodes) #node -∗
    node.[xchain_next] ↦{dq} next -∗
    xchain dq (drop (S i) nodes) dst -∗
    xchain dq nodes dst.
  Lemma xchain_lookup_acc {dq nodes} i node dst :
    nodes !! i = Some node →
    xchain dq nodes dst ⊢
      node.[xchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) ∗
      ( node.[xchain_next] ↦{dq} from_option #@{location} dst (nodes !! S i) -∗
        xchain dq nodes dst
      ).

  Lemma xchain_last {dq nodes dst} node :
    last nodes = Some node →
    xchain dq nodes dst ⊣⊢
      xchain dq (removelast nodes) #node ∗
      node.[xchain_next] ↦{dq} dst.
  Lemma xchain_last_acc {dq nodes dst} node :
    last nodes = Some node →
    xchain dq nodes dst ⊢
      node.[xchain_next] ↦{dq} dst ∗
      ( ∀ dst,
        node.[xchain_next] ↦{dq} dst -∗
        xchain dq nodes dst
      ).

  Lemma xchain_valid dq nodes dst :
    0 < length nodes →
    xchain dq nodes dst ⊢
    ⌜✓ dq⌝.
  Lemma xchain_combine nodes dq1 dst1 dq2 dst2 :
    0 < length nodes →
    xchain dq1 nodes dst1 -∗
    xchain dq2 nodes dst2 -∗
      ⌜dst1 = dst2⌝ ∗
      xchain (dq1 ⋅ dq2) nodes dst1.
  Lemma xchain_valid_2 nodes dq1 dst1 dq2 dst2 :
    0 < length nodes →
    xchain dq1 nodes dst1 -∗
    xchain dq2 nodes dst2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜dst1 = dst2⌝.
  Lemma xchain_agree nodes dq1 dst1 dq2 dst2 :
    0 < length nodes →
    xchain dq1 nodes dst1 -∗
    xchain dq2 nodes dst2 -∗
    ⌜dst1 = dst2⌝.
  Lemma xchain_dfrac_ne dq1 nodes1 dst1 dq2 nodes2 dst2 :
    0 < length nodes1 →
    ¬ ✓ (dq1 ⋅ dq2) →
    xchain dq1 nodes1 dst1 -∗
    xchain dq2 nodes2 dst2 -∗
    ⌜nodes1 ≠ nodes2⌝.
  Lemma xchain_ne nodes1 dst1 dq2 nodes2 dst2 :
    0 < length nodes1 →
    xchain (DfracOwn 1) nodes1 dst1 -∗
    xchain dq2 nodes2 dst2 -∗
    ⌜nodes1 ≠ nodes2⌝.
  Lemma xchain_exclusive nodes dst1 dq2 dst2 :
    0 < length nodes →
    xchain (DfracOwn 1) nodes dst1 -∗
    xchain dq2 nodes dst2 -∗
    False.
  Lemma xchain_persist dq nodes dst :
    xchain dq nodes dst ⊢ |==>
    xchain DfracDiscarded nodes dst.

  Lemma xchain_NoDup nodes dst :
    xchain (DfracOwn 1) nodes dst ⊢
    ⌜NoDup nodes⌝.

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

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

From zoo_std Require xchain__opaque.

#[global] Opaque xchain.