(* Victor B. F. Gomes, University of Cambridge Martin Kleppmann, University of Cambridge Dominic P. Mulligan, University of Cambridge Alastair R. Beresford, University of Cambridge *) 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.›