Library zoo_std.xtchain
Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo_std.xchain.
Require Export zoo_std.xtchain__code.
Require Import zoo_std.xtchain__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 Σ}.
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.[next] ↦{dq} dst.
Lemma xtchainｰsingleton₁ hdr dq node dst :
xtchain hdr dq [node] dst ⊢
node ↦ₕ hdr ∗
node.[next] ↦{dq} dst.
Lemma xtchainｰsingleton₂ hdr dq node dst :
node ↦ₕ hdr ∗
node.[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.[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.[next] ↦{dq} from_option #@{location} dst (head nodes) ∗
xtchain hdr dq nodes dst.
Lemma xtchainｰcons₁ {hdr dq} nodes node nodes' dst :
nodes = node :: nodes' →
xtchain hdr dq nodes dst ⊢
node ↦ₕ hdr ∗
node.[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.[next] ↦{dq} from_option #@{location} dst (head nodes) ∗
xtchain hdr dq nodes dst.
Lemma xtchainｰcons₂ hdr dq node nodes dst :
node ↦ₕ hdr -∗
node.[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₁ {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₂ 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.[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.[next] ↦{dq} 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.[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.[next] ↦{dq} dst.
Lemma xtchainｰsnoc₂ hdr dq nodes node dst :
xtchain hdr dq nodes #node -∗
node ↦ₕ hdr -∗
node.[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.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖i) ∗
xtchain hdr dq (drop ˖i nodes) 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.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖i) ∗
xtchain hdr dq (drop ˖i nodes) dst.
Lemma xtchainｰlookup₂ {hdr dq nodes} i node next dst :
nodes !! i = Some node →
next = from_option #@{location} dst (nodes !! ˖i) →
xtchain hdr dq (take i nodes) #node -∗
node ↦ₕ hdr -∗
node.[next] ↦{dq} next -∗
xtchain hdr dq (drop ˖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.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖i) ∗
( node.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖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.[next] ↦{dq} dst ∗
node ↦ₕ hdr.
Lemma xtchainｰlastｰacc {hdr dq nodes dst} node :
last nodes = Some node →
xtchain hdr dq nodes dst ⊢
node.[next] ↦{dq} dst ∗
node ↦ₕ hdr ∗
( ∀ dst,
node.[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).{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).{next} @ E
{{{
RET from_option #@{location} dst (nodes !! ˖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).{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) <-{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 <-{next} v @ E
{{{
RET ();
xtchain hdr (DfracOwn 1) (take ˖i nodes) v ∗
xtchain hdr (DfracOwn 1) (drop ˖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 <-{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'.[next] ↦ dst' ∗
node' ↦ₕ hdr
}}}
#node <-{next} #node' @ E
{{{
RET ();
xtchain hdr (DfracOwn 1) (nodes ++ [node']) dst'
}}}.
End zoo۰G.
Require zoo_std.xtchain__opaque.
#[global] Opaque xtchain.
Require Import zoo.base.
Require Import zoo_std.xchain.
Require Export zoo_std.xtchain__code.
Require Import zoo_std.xtchain__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 Σ}.
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.[next] ↦{dq} dst.
Lemma xtchainｰsingleton₁ hdr dq node dst :
xtchain hdr dq [node] dst ⊢
node ↦ₕ hdr ∗
node.[next] ↦{dq} dst.
Lemma xtchainｰsingleton₂ hdr dq node dst :
node ↦ₕ hdr ∗
node.[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.[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.[next] ↦{dq} from_option #@{location} dst (head nodes) ∗
xtchain hdr dq nodes dst.
Lemma xtchainｰcons₁ {hdr dq} nodes node nodes' dst :
nodes = node :: nodes' →
xtchain hdr dq nodes dst ⊢
node ↦ₕ hdr ∗
node.[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.[next] ↦{dq} from_option #@{location} dst (head nodes) ∗
xtchain hdr dq nodes dst.
Lemma xtchainｰcons₂ hdr dq node nodes dst :
node ↦ₕ hdr -∗
node.[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₁ {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₂ 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.[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.[next] ↦{dq} 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.[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.[next] ↦{dq} dst.
Lemma xtchainｰsnoc₂ hdr dq nodes node dst :
xtchain hdr dq nodes #node -∗
node ↦ₕ hdr -∗
node.[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.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖i) ∗
xtchain hdr dq (drop ˖i nodes) 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.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖i) ∗
xtchain hdr dq (drop ˖i nodes) dst.
Lemma xtchainｰlookup₂ {hdr dq nodes} i node next dst :
nodes !! i = Some node →
next = from_option #@{location} dst (nodes !! ˖i) →
xtchain hdr dq (take i nodes) #node -∗
node ↦ₕ hdr -∗
node.[next] ↦{dq} next -∗
xtchain hdr dq (drop ˖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.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖i) ∗
( node.[next] ↦{dq} from_option #@{location} dst (nodes !! ˖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.[next] ↦{dq} dst ∗
node ↦ₕ hdr.
Lemma xtchainｰlastｰacc {hdr dq nodes dst} node :
last nodes = Some node →
xtchain hdr dq nodes dst ⊢
node.[next] ↦{dq} dst ∗
node ↦ₕ hdr ∗
( ∀ dst,
node.[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).{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).{next} @ E
{{{
RET from_option #@{location} dst (nodes !! ˖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).{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) <-{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 <-{next} v @ E
{{{
RET ();
xtchain hdr (DfracOwn 1) (take ˖i nodes) v ∗
xtchain hdr (DfracOwn 1) (drop ˖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 <-{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'.[next] ↦ dst' ∗
node' ↦ₕ hdr
}}}
#node <-{next} #node' @ E
{{{
RET ();
xtchain hdr (DfracOwn 1) (nodes ++ [node']) dst'
}}}.
End zoo۰G.
Require zoo_std.xtchain__opaque.
#[global] Opaque xtchain.