Theory Network
section‹Axiomatic network models›
text‹In this section we develop a formal definition of an \emph{asynchronous unreliable causal broadcast network}.
We choose this model because it satisfies the causal delivery requirements of many operation-based
CRDTs~\<^cite>‹"Almeida:2015fc" and "Baquero:2014ed"›. Moreover, it is suitable for use in decentralised settings,
as motivated in the introduction, since it does not require waiting for communication with
a central server or a quorum of nodes.›
theory
Network
imports
Convergence
begin
subsection‹Node histories›
text‹We model a distributed system as an unbounded number of communicating nodes.
We assume nothing about the communication pattern of nodes---we assume only that each node is
uniquely identified by a natural number, and that the flow of execution at each node consists
of a finite, totally ordered sequence of execution steps (events).
We call that sequence of events at node $i$ the \emph{history} of that node.
For convenience, we assume that every event or execution step is unique within a node's history.›
locale node_histories =
fixes history :: "nat ⇒ 'evt list"
assumes histories_distinct [intro!, simp]: "distinct (history i)"
lemma (in node_histories) history_finite:
shows "finite (set (history i))"
by auto
definition (in node_histories) history_order :: "'evt ⇒ nat ⇒ 'evt ⇒ bool" (‹_/ ⊏⇧_/ _› [50,1000,50]50) where
"x ⊏⇧i z ≡ ∃xs ys zs. xs@x#ys@z#zs = history i"
lemma (in node_histories) node_total_order_trans:
assumes "e1 ⊏⇧i e2"
and "e2 ⊏⇧i e3"
shows "e1 ⊏⇧i e3"
proof -
obtain xs1 xs2 ys1 ys2 zs1 zs2 where *: "xs1 @ e1 # ys1 @ e2 # zs1 = history i"
"xs2 @ e2 # ys2 @ e3 # zs2 = history i"
using history_order_def assms by auto
hence "xs1 @ e1 # ys1 = xs2 ∧ zs1 = ys2 @ e3 # zs2"
by(rule_tac xs="history i" and ys="[e2]" in pre_suf_eq_distinct_list) auto
thus ?thesis
by(clarsimp simp: history_order_def) (metis "*"(2) append.assoc append_Cons)
qed
lemma (in node_histories) local_order_carrier_closed:
assumes "e1 ⊏⇧i e2"
shows "{e1,e2} ⊆ set (history i)"
using assms by (clarsimp simp add: history_order_def)
(metis in_set_conv_decomp Un_iff Un_subset_iff insert_subset list.simps(15)
set_append set_subset_Cons)+
lemma (in node_histories) node_total_order_irrefl:
shows "¬ (e ⊏⇧i e)"
by(clarsimp simp add: history_order_def)
(metis Un_iff histories_distinct distinct_append distinct_set_notin
list.set_intros(1) set_append)
lemma (in node_histories) node_total_order_antisym:
assumes "e1 ⊏⇧i e2"
and "e2 ⊏⇧i e1"
shows "False"
using assms node_total_order_irrefl node_total_order_trans by blast
lemma (in node_histories) node_order_is_total:
assumes "e1 ∈ set (history i)"
and "e2 ∈ set (history i)"
and "e1 ≠ e2"
shows "e1 ⊏⇧i e2 ∨ e2 ⊏⇧i e1"
using assms unfolding history_order_def by(metis list_split_two_elems histories_distinct)
definition (in node_histories) prefix_of_node_history :: "'evt list ⇒ nat ⇒ bool" (infix ‹prefix of› 50) where
"xs prefix of i ≡ ∃ys. xs@ys = history i"
lemma (in node_histories) carriers_head_lt:
assumes "y#ys = history i"
shows "¬(x ⊏⇧i y)"
using assms
apply(clarsimp simp add: history_order_def)
apply(rename_tac xs1 ys1 zs1)
apply (subgoal_tac "xs1 @ x # ys1 = [] ∧ zs1 = ys")
apply clarsimp
apply (rule_tac xs="history i" and ys="[y]" in pre_suf_eq_distinct_list)
apply auto
done
lemma (in node_histories) prefix_of_ConsD [dest]:
assumes "x # xs prefix of i"
shows "[x] prefix of i"
using assms by(auto simp: prefix_of_node_history_def)
lemma (in node_histories) prefix_of_appendD [dest]:
assumes "xs @ ys prefix of i"
shows "xs prefix of i"
using assms by(auto simp: prefix_of_node_history_def)
lemma (in node_histories) prefix_distinct:
assumes "xs prefix of i"
shows "distinct xs"
using assms by(clarsimp simp: prefix_of_node_history_def) (metis histories_distinct distinct_append)
lemma (in node_histories) prefix_to_carriers [intro]:
assumes "xs prefix of i"
shows "set xs ⊆ set (history i)"
using assms by(clarsimp simp: prefix_of_node_history_def) (metis Un_iff set_append)
lemma (in node_histories) prefix_elem_to_carriers:
assumes "xs prefix of i"
and "x ∈ set xs"
shows "x ∈ set (history i)"
using assms by(clarsimp simp: prefix_of_node_history_def) (metis Un_iff set_append)
lemma (in node_histories) local_order_prefix_closed:
assumes "x ⊏⇧i y"
and "xs prefix of i"
and "y ∈ set xs"
shows "x ∈ set xs"
proof -
obtain ys where "xs @ ys = history i"
using assms prefix_of_node_history_def by blast
moreover obtain as bs cs where "as @ x # bs @ y # cs = history i"
using assms history_order_def by blast
moreover obtain pre suf where *: "xs = pre @ y # suf"
using assms split_list by fastforce
ultimately have "pre = as @ x # bs ∧ suf @ ys = cs"
by (rule_tac xs="history i" and ys="[y]" in pre_suf_eq_distinct_list) auto
thus ?thesis
using assms * by clarsimp
qed
lemma (in node_histories) local_order_prefix_closed_last:
assumes "x ⊏⇧i y"
and "xs@[y] prefix of i"
shows "x ∈ set xs"
proof -
have "x ∈ set (xs @ [y])"
using assms by (force dest: local_order_prefix_closed)
thus ?thesis
using assms by(force simp add: node_total_order_irrefl prefix_to_carriers)
qed
lemma (in node_histories) events_before_exist:
assumes "x ∈ set (history i)"
shows "∃pre. pre @ [x] prefix of i"
proof -
have "∃idx. idx < length (history i) ∧ (history i) ! idx = x"
using assms by(simp add: set_elem_nth)
thus ?thesis
by(metis append_take_drop_id take_Suc_conv_app_nth prefix_of_node_history_def)
qed
lemma (in node_histories) events_in_local_order:
assumes "pre @ [e2] prefix of i"
and "e1 ∈ set pre"
shows "e1 ⊏⇧i e2"
using assms split_list unfolding history_order_def prefix_of_node_history_def by fastforce
subsection‹Asynchronous broadcast networks›
text‹We define a new locale $\isa{network}$ containing three axioms that define how broadcast
and deliver events may interact, with these axioms defining the properties of our network model.›