Library zoo_std.xchain

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.base.
Require Export zoo_std.xchain__code.
Require Import zoo_std.xchain__types.
Require Import zoo.options.

Implicit Type node : location.
Implicit Type nodes : list location.
Implicit Type 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.[next] ↦{dq} dst
        | node' :: _ ⇒
            node.[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.[next] ↦{dq} dst.
  Lemma xchainｰsingleton₁ dq node dst :
    xchain dq [node] dst ⊢
    node.[next] ↦{dq} dst.
  Lemma xchainｰsingleton₂ dq node dst :
    node.[next] ↦{dq} dst ⊢
    xchain dq [node] dst.

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

Require zoo_std.xchain__opaque.

#[global] Opaque xchain.