Theory IMAP-proof-helpers
section ‹Proof Helpers›
text‹In this section we define and prove lemmas that help to show that all identified critical
conditions hold for concurrent operations. Many of the following parts are derivations from the
definitions and lemmas of Gomes et al.›
theory
"IMAP-proof-helpers"
imports
"IMAP-def"
begin
lemma (in imap) apply_operations_never_fails:
assumes "xs prefix of i"
shows "apply_operations xs ≠ None"
using assms proof(induction xs rule: rev_induct, clarsimp)
case (snoc x xs) thus ?case
proof (cases x)
case (Broadcast e) thus ?thesis
using snoc by force
next
case (Deliver e) thus ?thesis
using snoc apply clarsimp unfolding interp_msg_def apply_operations_def
by (metis (no_types, lifting) bind.bind_lunit interpret_op_def prefix_of_appendD)
qed
qed
lemma (in imap) create_id_valid:
assumes "xs prefix of j"
and "Deliver (i1, Create i2 e) ∈ set xs"
shows "i1 = i2"
proof -
have "∃s. valid_behaviours s (i1, Create i2 e)"
using assms deliver_in_prefix_is_valid by blast
thus ?thesis
by(simp add: valid_behaviours_def)
qed
lemma (in imap) append_id_valid:
assumes "xs prefix of j"
and "Deliver (i1, Append i2 e) ∈ set xs"
shows "i1 = i2"
proof -
have "∃s. valid_behaviours s (i1, Append i2 e)"
using assms deliver_in_prefix_is_valid by blast
thus ?thesis
by(simp add: valid_behaviours_def)
qed
lemma (in imap) expunge_id_valid:
assumes "xs prefix of j"
and "Deliver (i1, Expunge e mo i2) ∈ set xs"
shows "i1 = i2"
proof -
have "∃s. valid_behaviours s (i1, Expunge e mo i2)"
using assms deliver_in_prefix_is_valid by blast
thus ?thesis
by(simp add: valid_behaviours_def)
qed
lemma (in imap) store_id_valid:
assumes "xs prefix of j"
and "Deliver (i1, Store e mo i2) ∈ set xs"
shows "i1 = i2"
proof -
have "∃s. valid_behaviours s (i1, Store e mo i2)"
using assms deliver_in_prefix_is_valid by blast
thus ?thesis
by(simp add: valid_behaviours_def)
qed
definition (in imap) added_ids :: "('id × ('id, 'b) operation) event list ⇒ 'b ⇒ 'id list" where
"added_ids es p ≡ List.map_filter (λx. case x of
Deliver (i, Create j e) ⇒ if e = p then Some j else None |
Deliver (i, Expunge e mo j) ⇒ if e = p then Some j else None |
_ ⇒ None) es"
definition (in imap) added_files :: "('id × ('id, 'b) operation) event list ⇒ 'b ⇒ 'id list" where
"added_files es p ≡ List.map_filter (λx. case x of
Deliver (i, Append j e) ⇒ if e = p then Some j else None |
Deliver (i, Store e mo j) ⇒ if e = p then Some j else None |
_ ⇒ None) es"
lemma (in imap) [simp]:
shows "added_files [] e = []"
by (auto simp: added_files_def map_filter_def)
lemma (in imap) [simp]:
shows "added_files (xs @ ys) e = added_files xs e @ added_files ys e"
by (auto simp: added_files_def map_filter_append)
lemma (in imap) added_files_Broadcast_collapse [simp]:
shows "added_files ([Broadcast e]) e' = []"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) added_files_Deliver_Delete_collapse [simp]:
shows "added_files ([Deliver (i, Delete is e)]) e' = []"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) added_files_Deliver_Create_collapse [simp]:
shows "added_files ([Deliver (i, Create j e)]) e' = []"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) added_files_Deliver_Expunge_collapse [simp]:
shows "added_files ([Deliver (i, Expunge e mo j)]) e' = []"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) added_files_Deliver_Append_diff_collapse [simp]:
shows "e ≠ e' ⟹ added_files ([Deliver (i, Append j e)]) e' = []"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) added_files_Deliver_Append_same_collapse [simp]:
shows "added_files ([Deliver (i, Append j e)]) e = [j]"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) added_files_Deliver_Store_diff_collapse [simp]:
shows "e ≠ e' ⟹ added_files ([Deliver (i, Store e mo j)]) e' = []"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) added_files_Deliver_Store_same_collapse [simp]:
shows "added_files ([Deliver (i, Store e mo j)]) e = [j]"
by (auto simp: added_files_def map_filter_append map_filter_def)
lemma (in imap) [simp]:
shows "added_ids [] e = []"
by (auto simp: added_ids_def map_filter_def)
lemma (in imap) split_ids [simp]:
shows "added_ids (xs @ ys) e = added_ids xs e @ added_ids ys e"
by (auto simp: added_ids_def map_filter_append)
lemma (in imap) added_ids_Broadcast_collapse [simp]:
shows "added_ids ([Broadcast e]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) added_ids_Deliver_Delete_collapse [simp]:
shows "added_ids ([Deliver (i, Delete is e)]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) added_ids_Deliver_Append_collapse [simp]:
shows "added_ids ([Deliver (i, Append j e)]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) added_ids_Deliver_Store_collapse [simp]:
shows "added_ids ([Deliver (i, Store e mo j)]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) added_ids_Deliver_Create_diff_collapse [simp]:
shows "e ≠ e' ⟹ added_ids ([Deliver (i, Create j e)]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) added_ids_Deliver_Expunge_diff_collapse [simp]:
shows "e ≠ e' ⟹ added_ids ([Deliver (i, Expunge e mo j)]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) added_ids_Deliver_Create_same_collapse [simp]:
shows "added_ids ([Deliver (i, Create j e)]) e = [j]"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) added_ids_Deliver_Expunge_same_collapse [simp]:
shows "added_ids ([Deliver (i, Expunge e mo j)]) e = [j]"
by (auto simp: added_ids_def map_filter_append map_filter_def)
lemma (in imap) expunge_id_not_in_set:
assumes "i1 ∉ set (added_ids [Deliver (i, Expunge e mo i2)] e)"
shows "i1 ≠ i2"
using assms by simp
lemma (in imap) apply_operations_added_ids:
assumes "es prefix of j"
and "apply_operations es = Some f"
shows "fst (f x) ⊆ set (added_ids es x)"
using assms proof (induct es arbitrary: f rule: rev_induct, force)
case (snoc x xs) thus ?case
proof (cases x, force)
case (Deliver e)
moreover obtain a b where "e = (a, b)" by force
ultimately show ?thesis
using snoc by(case_tac b; clarsimp simp: interp_msg_def split: bind_splits,
force split: if_split_asm simp add: op_elem_def interpret_op_def)
qed
qed
lemma (in imap) apply_operations_added_files:
assumes "es prefix of j"
and "apply_operations es = Some f"
shows "snd (f x) ⊆ set (added_files es x)"
using assms proof (induct es arbitrary: f rule: rev_induct, force)
case (snoc x xs) thus ?case
proof (cases x, force)
case (Deliver e)
moreover obtain a b where "e = (a, b)" by force
ultimately show ?thesis
using snoc by(case_tac b; clarsimp simp: interp_msg_def split: bind_splits,
force split: if_split_asm simp add: op_elem_def interpret_op_def)
qed
qed
lemma (in imap) Deliver_added_files:
assumes "xs prefix of j"
and "i ∈ set (added_files xs e)"
shows "Deliver (i, Append i e) ∈ set xs ∨ (∃ mo . Deliver (i, Store e mo i) ∈ set xs)"
using assms proof (induct xs rule: rev_induct, clarsimp)
case (snoc x xs) thus ?case
proof (cases x, force)
case X: (Deliver e')
moreover obtain a b where E: "e' = (a, b)" by force
ultimately show ?thesis using snoc
apply (case_tac b; clarify) apply (simp,metis prefix_of_appendD,force)
using append_id_valid apply simp
using E apply (metis
added_files_Deliver_Append_diff_collapse added_files_Deliver_Append_same_collapse
empty_iff in_set_conv_decomp list.set(1) prefix_of_appendD set_ConsD, simp)
using E apply_operations_added_files apply (blast,simp)
using E apply_operations_added_files
by (metis Un_iff
added_files_Deliver_Store_diff_collapse added_files_Deliver_Store_same_collapse empty_iff
empty_set list.set_intros(1) prefix_of_appendD set_ConsD set_append store_id_valid)
qed
qed
end
Theory IMAP-proof-independent
section ‹Independence of IMAP Commands›
text‹In this section we show that two concurrent operations that reference to the same tag must be
identical.›
theory
"IMAP-proof-independent"
imports
"IMAP-def"
"IMAP-proof-helpers"
begin
lemma (in imap) Broadcast_Expunge_Deliver_prefix_closed:
assumes "xs @ [Broadcast (i, Expunge e mo i)] prefix of j"
shows "Deliver (mo, Append mo e) ∈ set xs ∨
(∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set xs)"
proof -
obtain y where "apply_operations xs = Some y"
using assms broadcast_only_valid_msgs by blast
moreover hence "mo ∈ snd (y e)"
using broadcast_only_valid_msgs[of xs "(i, Expunge e mo i)" j]
valid_behaviours_def[of y "(i, Expunge e mo i)"] assms by auto
ultimately show ?thesis
using assms Deliver_added_files apply_operations_added_files by blast
qed
lemma (in imap) Broadcast_Store_Deliver_prefix_closed:
assumes "xs @ [Broadcast (i, Store e mo i)] prefix of j"
shows "Deliver (mo, Append mo e) ∈ set xs ∨
(∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set xs)"
proof -
obtain y where "apply_operations xs = Some y"
using assms broadcast_only_valid_msgs by blast
moreover hence "mo ∈ snd (y e)"
using broadcast_only_valid_msgs[of xs "(i, Store e mo i)" j]
valid_behaviours_def[of y "(i, Store e mo i)"] assms by auto
ultimately show ?thesis
using assms Deliver_added_files apply_operations_added_files by blast
qed
lemma (in imap) Deliver_added_ids:
assumes "xs prefix of j"
and "i ∈ set (added_ids xs e)"
shows "Deliver (i, Create i e) ∈ set xs ∨
(∃ mo . Deliver (i, Expunge e mo i) ∈ set xs)"
using assms proof (induct xs rule: rev_induct, clarsimp)
case (snoc x xs) thus ?case
proof (cases x, force)
case X: (Deliver e')
moreover obtain a b where "e' = (a, b)" by force
ultimately show ?thesis
using snoc apply (case_tac b; clarify)
apply (simp, metis added_ids_Deliver_Create_diff_collapse
added_ids_Deliver_Create_same_collapse empty_iff list.set(1) set_ConsD create_id_valid
in_set_conv_decomp prefix_of_appendD, force)
using append_id_valid apply (simp, metis (no_types, lifting) prefix_of_appendD, simp, metis
Un_iff added_ids_Deliver_Expunge_diff_collapse added_ids_Deliver_Expunge_same_collapse
empty_iff expunge_id_valid list.set(1) list.set_intros(1) prefix_of_appendD set_ConsD
set_append)
by (simp, blast)
qed
qed
lemma (in imap) Broadcast_Deliver_prefix_closed:
assumes "xs @ [Broadcast (r, Delete ix e)] prefix of j"
and "i ∈ ix"
shows "Deliver (i, Create i e) ∈ set xs ∨
Deliver (i, Append i e) ∈ set xs ∨
(∃ mo . Deliver (i, Expunge e mo i) ∈ set xs) ∨
(∃ mo . Deliver (i, Store e mo i) ∈ set xs)"
proof -
obtain y where "apply_operations xs = Some y"
using assms broadcast_only_valid_msgs by blast
moreover hence "ix = fst (y e) ∪ snd (y e)"
by (metis (mono_tags, lifting) assms(1) broadcast_only_valid_msgs operation.case(2)
option.simps(1) valid_behaviours_def case_prodD)
ultimately show ?thesis
using assms Deliver_added_ids apply_operations_added_ids
by (metis Deliver_added_files Un_iff apply_operations_added_files le_iff_sup prefix_of_appendD)
qed
lemma (in imap) concurrent_create_delete_independent_technical:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Create i e) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
shows "hb (i, Create i e) (ir, Delete is e)"
proof -
have f1: "Deliver (i, Create i e) ∈ set (history j)"
using assms prefix_msg_in_history by blast
obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence f2: "Deliver (i, Create i e) ∈ set pre ∨
Deliver (i, Append i e) ∈ set pre ∨
(∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨
(∃ mo . Deliver (i, Store e mo i) ∈ set pre)"
using Broadcast_Deliver_prefix_closed assms by auto
have f3: "Deliver (i, Append i e) ∉ set pre" using f1 P
by (metis (full_types) Pair_inject fst_conv network.delivery_has_a_cause network.msg_id_unique
network_axioms operation.simps(9) prefix_elem_to_carriers prefix_of_appendD)
have f4: "∀ mo . Deliver (i, Expunge e mo i) ∉ set pre" using f1 P
by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.simps(11)
prefix_elem_to_carriers prefix_of_appendD)
have "∀ mo . Deliver (i, Store e mo i) ∉ set pre" using f1 P
by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.simps(13)
prefix_elem_to_carriers prefix_of_appendD)
thus ?thesis using f2 f3 f4 P events_in_local_order hb_deliver by blast
qed
lemma (in imap) concurrent_store_expunge_independent_technical:
assumes "xs prefix of j"
and "(i, Store e mo i) ∈ set (node_deliver_messages xs)"
and "(r, Expunge e i r) ∈ set (node_deliver_messages xs)"
shows "hb (i, Store e mo i) (r, Expunge e i r)"
proof -
obtain pre k where P: "pre@[Broadcast (r, Expunge e i r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence f1: "Deliver (i, Append i e) ∈ set pre ∨
(∃ mo2 . Deliver (i, Store e mo2 i) ∈ set pre)"
using Broadcast_Expunge_Deliver_prefix_closed assms(1) by auto
hence f2: "Deliver (i, Append i e) ∉ set (history k)"
by (metis Pair_inject assms(1) assms(2) fst_conv msg_id_unique network.delivery_has_a_cause
network_axioms operation.distinct(17) prefix_msg_in_history)
from f1 obtain mo2 :: 'a where
"Deliver (i, Store e mo2 i) ∈ set (history k)" using f2
using P prefix_elem_to_carriers by blast
hence "Deliver (i, Store e mo i) ∈ set (history k)" using assms f1 f2 P
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms
prefix_msg_in_history)
then show ?thesis
using hb.intros(2) events_in_local_order f1 f2 P
by (metis delivery_has_a_cause fst_conv msg_id_unique node_histories.prefix_of_appendD
node_histories_axioms prefix_elem_to_carriers)
qed
lemma (in imap) concurrent_store_expunge_independent_technical2:
assumes "xs prefix of j"
and "(i, Store e1 mo2 i) ∈ set (node_deliver_messages xs)"
and "(r, Expunge e mo r) ∈ set (node_deliver_messages xs)"
shows "mo2 ≠ r"
proof -
obtain oid :: "'a × ('a, 'b) operation ⇒ nat" where
oid: "∀p n. Deliver p ∉ set (history n) ∨ Broadcast p ∈ set (history (oid p))"
by (metis (no_types) delivery_has_a_cause)
hence f1: "Broadcast (r, Expunge e mo r) ∈ set (history (oid (r, Expunge e mo r)))"
using assms(1) assms(3) prefix_msg_in_history by blast
obtain k :: "'a ⇒ 'b ⇒ ('a × ('a, 'b) operation) event list ⇒ 'a" where k:
"∀i e pre. (∃mo. Deliver (i, Store e mo i) ∈ set pre) =
(Deliver (i, Store e (k i e pre) i) ∈ set pre)"
by moura
obtain pre :: "nat ⇒ ('a × ('a, 'b) operation) event ⇒ ('a × ('a, 'b) operation) event list"
where pre: "∀k op1. (∃op2. op2 @ [op1] prefix of k) = (pre k op1 @ [op1] prefix of k)"
by moura
hence f2: "∀e n. e ∉ set (history n) ∨ pre n e @ [e] prefix of n"
using events_before_exist by simp
hence f3: "pre (oid (i, Store e1 mo2 i)) (Broadcast (i, Store e1 mo2 i))
prefix of oid (i, Store e1 mo2 i)"
using oid assms(1) assms(2) prefix_msg_in_history by blast
have f4: "Deliver (r, Append r e1) ∉ set (history (oid (i, Store e1 mo2 i)))"
by (metis (no_types) oid f1 fst_conv msg_id_unique old.prod.inject operation.distinct(15))
have "Deliver (r, Store e1 (k r e1 (pre (oid (i, Store e1 mo2 i))
(Broadcast (i, Store e1 mo2 i)))) r) ∉ set (history (oid (i, Store e1 mo2 i)))"
by (metis (no_types) oid f1 fst_conv msg_id_unique old.prod.inject operation.distinct(19))
thus ?thesis using oid k f2 f3 f4 assms
by (metis (no_types, lifting) Broadcast_Store_Deliver_prefix_closed
network.prefix_msg_in_history network_axioms prefix_elem_to_carriers)
qed
lemma (in imap) concurrent_store_delete_independent_technical:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Store e mo i) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
shows "hb (i, Store e mo i) (ir, Delete is e)"
proof -
have f1: "Deliver (i, Store e mo i) ∈ set (history j)" using assms prefix_msg_in_history by auto
obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence f2: "Deliver (i, Create i e) ∈ set pre ∨
Deliver (i, Append i e) ∈ set pre ∨
(∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨
(∃ mo . Deliver (i, Store e mo i) ∈ set pre)"
using Broadcast_Deliver_prefix_closed assms(1) by auto
have f3: "Deliver (i, Create i e) ∉ set pre" using f1 P
by (metis Pair_inject delivery_has_a_cause fst_conv msg_id_unique operation.distinct(7)
prefix_elem_to_carriers prefix_of_appendD)
have f4: "Deliver (i, Append i e) ∉ set pre" using f1 P
by (metis delivery_has_a_cause fst_conv msg_id_unique operation.distinct(17)
prefix_elem_to_carriers prefix_of_appendD prod.inject)
have "∀ mo . Deliver (i, Expunge e mo i) ∉ set pre" using f1 P
by (metis Pair_inject delivery_has_a_cause fst_conv msg_id_unique operation.simps(25)
prefix_elem_to_carriers prefix_of_appendD)
hence "Deliver (i, Store e mo i) ∈ set pre" using f1 f2 f3 f4 P
by (metis delivery_has_a_cause fst_conv msg_id_unique node_histories.prefix_of_appendD
node_histories_axioms prefix_elem_to_carriers)
thus ?thesis using P events_in_local_order hb_deliver by blast
qed
lemma (in imap) concurrent_append_delete_independent_technical:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Append i e) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
shows "hb (i, Append i e) (ir, Delete is e)"
proof -
obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence f1: "Deliver (i, Create i e) ∈ set pre ∨
Deliver (i, Append i e) ∈ set pre ∨
(∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨
(∃ mo . Deliver (i, Store e mo i) ∈ set pre)"
using Broadcast_Deliver_prefix_closed assms(1) by auto
hence "Deliver (i, Append i e) ∈ set pre" using assms P f1
by (metis (no_types, hide_lams) delivery_has_a_cause events_in_local_order fst_conv
hb_broadcast_exists1 hb_deliver msg_id_unique prefix_msg_in_history)
thus ?thesis using P events_in_local_order hb_deliver by blast
qed
lemma (in imap) concurrent_append_expunge_independent_technical:
assumes "i = mo"
and "xs prefix of j"
and "(i, Append i e) ∈ set (node_deliver_messages xs)"
and "(r, Expunge e mo r) ∈ set (node_deliver_messages xs)"
shows "hb (i, Append i e) (r, Expunge e mo r)"
proof -
obtain pre k where P: "pre@[Broadcast (r, Expunge e mo r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence f1: "Deliver (mo, Append mo e) ∈ set pre ∨
(∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set pre)"
using Broadcast_Expunge_Deliver_prefix_closed assms(1) by auto
hence "(∀ mo2 . Deliver (mo, Store e mo2 mo) ∉ set pre)" using P assms
proof -
have "Deliver (mo, Append mo e) ∈ set (history j)"
using assms(1) assms(2) assms(3) prefix_msg_in_history by blast
thus ?thesis
by (metis (no_types) P Pair_inject delivery_has_a_cause fst_conv msg_id_unique
operation.simps(23) prefix_elem_to_carriers prefix_of_appendD)
qed
thus ?thesis
using hb.intros(2) events_in_local_order assms(1) P f1 by blast
qed
lemma (in imap) concurrent_append_store_independent_technical:
assumes "i = mo"
and "xs prefix of j"
and "(i, Append i e) ∈ set (node_deliver_messages xs)"
and "(r, Store e mo r) ∈ set (node_deliver_messages xs)"
shows "hb (i, Append i e) (r, Store e mo r)"
proof -
obtain pre k where pre: "pre@[Broadcast (r, Store e mo r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence f1: "Deliver (mo, Append mo e) ∈ set pre ∨
(∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set pre)"
using Broadcast_Store_Deliver_prefix_closed assms(1) by auto
have f2: "Deliver (i, Append i e) ∈ set (history j)"
by (meson assms network.prefix_msg_in_history network_axioms)
then show ?thesis using assms f1
by (metis pre delivery_has_a_cause events_in_local_order fst_conv hb_deliver
msg_id_unique node_histories.prefix_of_appendD node_histories_axioms
prefix_elem_to_carriers)
qed
lemma (in imap) concurrent_expunge_delete_independent_technical:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Expunge e mo i) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
shows "hb (i, Expunge e mo i) (ir, Delete is e)"
proof -
obtain pre k where pre: "pre@[Broadcast (ir, Delete is e)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence A: "Deliver (i, Create i e) ∈ set pre ∨
Deliver (i, Append i e) ∈ set pre ∨
(∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨
(∃ mo . Deliver (i, Store e mo i) ∈ set pre)"
using Broadcast_Deliver_prefix_closed assms(1) by auto
hence "Deliver (i, Expunge e mo i) ∈ set pre" using assms
proof -
have f1: "⋀e. e ∉ set pre ∨ e ∈ set (history k)"
using pre prefix_elem_to_carriers by blast
have f2: "Deliver (i, Expunge e mo i) ∈ set (history j)"
by (meson assms network.prefix_msg_in_history network_axioms)
then show ?thesis using f1 A
by (metis (no_types, lifting) fst_conv msg_id_unique network.delivery_has_a_cause
network_axioms)
qed
ultimately show ?thesis
using hb.intros(2) events_in_local_order by blast
qed
lemma (in imap) concurrent_store_store_independent_technical:
assumes "xs prefix of j"
and "(i, Store e mo i) ∈ set (node_deliver_messages xs)"
and "(r, Store e i r) ∈ set (node_deliver_messages xs)"
shows "hb (i, Store e mo i) (r, Store e i r)"
proof -
obtain pre k where P: "pre@[Broadcast (r, Store e i r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence f1: "∀e. e ∉ set pre ∨ e ∈ set (history k)"
using prefix_elem_to_carriers by blast
have f2: "Deliver (i, Append i e) ∈ set pre ∨ (∃ mo2 . Deliver (i, Store e mo2 i) ∈ set pre)"
using Broadcast_Store_Deliver_prefix_closed assms(1) P by auto
hence "Deliver (i, Store e mo i) ∈ set pre" using assms f1
by (metis delivery_has_a_cause fst_conv msg_id_unique prefix_msg_in_history)
then show ?thesis
using hb.intros(2) events_in_local_order P by blast
qed
lemma (in imap) expunge_delete_tag_causality:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Expunge e1 mo i) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
and "pre@[Broadcast (ir, Delete is e2)] prefix of k"
shows "Deliver (i, Expunge e2 mo i) ∈ set (history k)"
proof-
have f1: "Deliver (i, Append i e2) ∉ set (history k)" using assms
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject
operation.distinct(15) prefix_msg_in_history)
have f2: "Deliver (i, Create i e2) ∉ set (history k)" using assms
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject
operation.distinct(5) prefix_msg_in_history)
have f3: "∀ mo. Deliver (i, Store e2 mo i) ∉ set (history k)" using assms
by (metis Pair_inject fst_conv msg_id_unique network.delivery_has_a_cause network_axioms
operation.simps(25) prefix_msg_in_history)
hence "∃ mo1. Deliver (i, Expunge e2 mo1 i) ∈ set (history k)" using assms f1 f2
by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms node_histories.prefix_of_appendD
node_histories_axioms prefix_elem_to_carriers)
then obtain mo1 :: 'a where
"Deliver (i, Expunge e2 mo1 i) ∈ set (history k)" by blast
then show ?thesis using assms f1 f2 f3
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject
operation.inject(4) prefix_msg_in_history)
qed
lemma (in imap) expunge_delete_ids_imply_messages_same:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Expunge e1 mo i) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence "Deliver (i, Expunge e2 mo i) ∈ set (history k)" using assms expunge_delete_tag_causality
by blast
then show ?thesis using assms
by (metis delivery_has_a_cause fst_conv network.msg_id_unique network_axioms
operation.inject(4) prefix_msg_in_history prod.inject)
qed
lemma (in imap) store_delete_ids_imply_messages_same:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
have f1: "Deliver (i, Append i e2) ∉ set (history k)" using assms
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject
operation.distinct(17) prefix_msg_in_history)
have f2: "∀ mo. Deliver (i, Expunge e2 mo i) ∉ set (history k)" using assms
by (metis Pair_inject fst_conv msg_id_unique network.delivery_has_a_cause network_axioms
operation.distinct(19) prefix_msg_in_history)
have f3: "Deliver (i, Create i e2) ∉ set (history k)" using assms
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject
operation.distinct(8) prefix_msg_in_history)
hence "(∃ mo1. Deliver (i, Store e2 mo1 i) ∈ set pre)" using assms P f1 f2 imap_axioms
by (meson imap.Broadcast_Deliver_prefix_closed prefix_elem_to_carriers prefix_of_appendD)
then obtain mo1 :: 'a where
f3: "Deliver (i, Store e2 mo1 i) ∈ set pre" by blast
then have f4: "Deliver (i, Store e2 mo1 i) ∈ set (history k)"
using P prefix_elem_to_carriers by blast
hence "Deliver (i, Store e2 mo i) ∈ set pre" using f2 f3 assms
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject
operation.inject(5) prefix_msg_in_history)
moreover have "Deliver(i, Store e1 mo i) ∈ set (history j)"
using assms(2) assms(3) prefix_msg_in_history by blast
ultimately show ?thesis using f4
by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.inject(5))
qed
lemma (in imap) create_delete_ids_imply_messages_same:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Create i e1) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
have f1: "Deliver (i, Append i e2) ∉ set (history k)"
by (metis assms(2) assms(3) delivery_has_a_cause fst_conv network.msg_id_unique
network.prefix_msg_in_history network_axioms operation.distinct(3) prod.inject)
have f2: "∀ mo. Deliver (i, Expunge e2 mo i) ∉ set (history k)"
by (metis assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause network_axioms
old.prod.inject operation.distinct(5) prefix_msg_in_history)
have f3: "∀ mo. Deliver (i, Store e2 mo i) ∉ set (history k)"
by (metis Pair_inject assms(2) assms(3) delivery_has_a_cause fst_conv msg_id_unique
operation.distinct(7) prefix_msg_in_history)
hence "Deliver (i, Create i e2) ∈ set pre" using assms P f2 f1 imap_axioms
by (meson imap.Broadcast_Deliver_prefix_closed prefix_elem_to_carriers prefix_of_appendD)
then show ?thesis using f1 f2 f3
by (metis (no_types, lifting) P assms(2) assms(3) delivery_has_a_cause fst_conv msg_id_unique
node_histories.prefix_of_appendD node_histories_axioms old.prod.inject operation.inject(1)
prefix_elem_to_carriers prefix_msg_in_history)
qed
lemma (in imap) append_delete_ids_imply_messages_same:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Append i e1) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence f1: "⋀e. e ∈ set pre ⟹ e ∈ set (history k)" using prefix_elem_to_carriers by blast
have f2: "Deliver (i, Create i e2) ∉ set pre" using P f1
by (metis assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause network_axioms
old.prod.inject operation.distinct(3) prefix_msg_in_history)
moreover have D1: "∀ mo. Deliver (i, Expunge e2 mo i) ∉ set pre" using P f1
by (metis Pair_inject assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause
network_axioms operation.distinct(15) prefix_msg_in_history)
moreover have D2: "∀ mo. Deliver (i, Store e2 mo i) ∉ set pre" using P f1
by (metis Pair_inject assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause
network_axioms operation.simps(23) prefix_msg_in_history)
moreover hence "Deliver (i, Append i e2) ∈ set pre"
using P D1 D2 f2 assms(1) Broadcast_Deliver_prefix_closed by blast
moreover have "Deliver (i, Append i e1) ∈ set (history j)"
using assms(2) assms(3) prefix_msg_in_history by blast
ultimately show ?thesis using assms
by (metis f1 msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject
operation.inject(3) prod.sel(1))
qed
lemma (in imap) append_expunge_ids_imply_messages_same:
assumes "i = mo"
and "xs prefix of j"
and "(i, Append i e1) ∈ set (node_deliver_messages xs)"
and "(r, Expunge e2 mo r) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where pre: "pre@[Broadcast (r, Expunge e2 mo r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence "Deliver (mo, Append mo e2) ∈ set pre ∨
(∃ mo2 . Deliver (mo, Store e2 mo2 mo) ∈ set pre)"
using Broadcast_Expunge_Deliver_prefix_closed assms(1)
by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms)
hence "Deliver (i, Append i e2) ∈ set pre" using assms
by (metis (no_types, lifting) pre delivery_has_a_cause fst_conv hb_broadcast_exists1
msg_id_unique network.hb_deliver network.prefix_msg_in_history network_axioms
node_histories.events_in_local_order node_histories_axioms operation.distinct(17)
prod.inject)
moreover have "Deliver (i, Append i e1) ∈ set (history j)"
using assms(2) assms(3) prefix_msg_in_history by blast
ultimately show ?thesis
by (metis (no_types, lifting) fst_conv network.delivery_has_a_cause network.msg_id_unique
network_axioms operation.inject(3) prefix_elem_to_carriers prefix_of_appendD prod.inject)
qed
lemma (in imap) append_store_ids_imply_messages_same:
assumes "i = mo"
and "xs prefix of j"
and "(i, Append i e1) ∈ set (node_deliver_messages xs)"
and "(r, Store e2 mo r) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where P: "pre@[Broadcast (r, Store e2 mo r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence A: "Deliver (mo, Append mo e2) ∈ set pre ∨
(∃ mo2 . Deliver (mo, Store e2 mo2 mo) ∈ set pre)"
using Broadcast_Store_Deliver_prefix_closed assms(1)
by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms)
have f1: "Deliver (i, Append i e1) ∈ set (history j)"
using assms(2) assms(3) prefix_msg_in_history by blast
hence "Deliver (i, Append i e2) ∈ set pre" using assms P A
by (metis Pair_inject assms(1) P delivery_has_a_cause fst_conv msg_id_unique
operation.simps(23) prefix_elem_to_carriers prefix_of_appendD)
then show ?thesis using f1
by (metis P delivery_has_a_cause fst_conv msg_id_unique
node_histories.prefix_of_appendD node_histories_axioms operation.inject(3)
prefix_elem_to_carriers prod.inject)
qed
lemma (in imap) expunge_store_ids_imply_messages_same:
assumes "xs prefix of j"
and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)"
and "(r, Expunge e2 i r) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where P: "pre@[Broadcast (r, Expunge e2 i r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
hence pprefix: "pre prefix of k"
using P by blast
have A: "Deliver (i, Append i e2) ∈ set pre ∨
(∃ mo2 . Deliver (i, Store e2 mo2 i) ∈ set pre)"
using Broadcast_Expunge_Deliver_prefix_closed assms(1) P by blast
have "Deliver (i, Store e2 mo i) ∈ set pre" using assms A P
proof -
obtain op1 :: "'a × ('a, 'b) operation ⇒ nat" where
f1: "Broadcast (i, Store e1 mo i) ∈ set (history (op1 (i, Store e1 mo i)))"
by (meson assms(1) assms(2) delivery_has_a_cause prefix_msg_in_history)
then show ?thesis
using f1 A pprefix delivery_has_a_cause network.msg_id_unique network_axioms
node_histories.prefix_to_carriers node_histories_axioms
by fastforce
qed
moreover have "Deliver (i, Store e1 mo i) ∈ set (history j)"
using assms(1) assms(2) prefix_msg_in_history by auto
ultimately show ?thesis using assms P
by (metis delivery_has_a_cause fst_conv msg_id_unique operation.inject(5)
prefix_elem_to_carriers prefix_of_appendD prod.inject)
qed
lemma (in imap) store_store_ids_imply_messages_same:
assumes "xs prefix of j"
and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)"
and "(r, Store e2 i r) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where P: "pre@[Broadcast (r, Store e2 i r)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence A: "Deliver (i, Append i e2) ∈ set pre ∨
(∃ mo2 . Deliver (i, Store e2 mo2 i) ∈ set pre)"
using Broadcast_Store_Deliver_prefix_closed assms(1) by blast
have "∀e. e ∉ set pre ∨ e ∈ set (history k)"
using P prefix_elem_to_carriers by auto
hence "Deliver (i, Store e2 mo i) ∈ set pre"
by (metis A assms(1) assms(2) delivery_has_a_cause fst_conv msg_id_unique
operation.distinct(17) operation.inject(5) prefix_msg_in_history prod.inject)
moreover have "Deliver (i, Store e1 mo i) ∈ set (history j)"
using assms(1) assms(2) prefix_msg_in_history by auto
ultimately show ?thesis using assms
by (metis Pair_inject delivery_has_a_cause msg_id_unique operation.simps(5)
prefix_elem_to_carriers prefix_of_appendD prod.sel(1))
qed
end
Theory IMAP-proof
section ‹Convergence of the IMAP-CRDT›
text‹In this final section show that concurrent updates commute and thus Strong Eventual
Convergence is achieved.›
theory
"IMAP-proof"
imports
"IMAP-def"
"IMAP-proof-commute"
"IMAP-proof-helpers"
"IMAP-proof-independent"
begin
corollary (in imap) concurrent_create_delete_independent:
assumes "¬ hb (i, Create i e1) (ir, Delete is e2)"
and "¬ hb (ir, Delete is e2) (i, Create i e1)"
and "xs prefix of j"
and "(i, Create i e1) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "i ∉ is"
using assms create_delete_ids_imply_messages_same concurrent_create_delete_independent_technical
by fastforce
corollary (in imap) concurrent_append_delete_independent:
assumes "¬ hb (i, Append i e1) (ir, Delete is e2)"
and "¬ hb (ir, Delete is e2) (i, Append i e1)"
and "xs prefix of j"
and "(i, Append i e1) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "i ∉ is"
using assms append_delete_ids_imply_messages_same concurrent_append_delete_independent_technical
by fastforce
corollary (in imap) concurrent_append_expunge_independent:
assumes "¬ hb (i, Append i e1) (r, Expunge e2 mo r)"
and "¬ hb (r, Expunge e2 mo r) (i, Append i e1)"
and "xs prefix of j"
and "(i, Append i e1) ∈ set (node_deliver_messages xs)"
and "(r, Expunge e2 mo r) ∈ set (node_deliver_messages xs)"
shows "i ≠ mo"
using assms append_expunge_ids_imply_messages_same concurrent_append_expunge_independent_technical
by fastforce
corollary (in imap) concurrent_append_store_independent:
assumes "¬ hb (i, Append i e1) (r, Store e2 mo r)"
and "¬ hb (r, Store e2 mo r) (i, Append i e1)"
and "xs prefix of j"
and "(i, Append i e1) ∈ set (node_deliver_messages xs)"
and "(r, Store e2 mo r) ∈ set (node_deliver_messages xs)"
shows "i ≠ mo"
using assms append_store_ids_imply_messages_same concurrent_append_store_independent_technical
by fastforce
corollary (in imap) concurrent_expunge_delete_independent:
assumes "¬ hb (i, Expunge e1 mo i) (ir, Delete is e2)"
and "¬ hb (ir, Delete is e2) (i, Expunge e1 mo i)"
and "xs prefix of j"
and "(i, Expunge e1 mo i) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "i ∉ is"
using assms expunge_delete_ids_imply_messages_same concurrent_expunge_delete_independent_technical
by fastforce
corollary (in imap) concurrent_store_delete_independent:
assumes "¬ hb (i, Store e1 mo i) (ir, Delete is e2)"
and "¬ hb (ir, Delete is e2) (i, Store e1 mo i)"
and "xs prefix of j"
and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)"
and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
shows "i ∉ is"
using assms store_delete_ids_imply_messages_same concurrent_store_delete_independent_technical
by fastforce
corollary (in imap) concurrent_store_expunge_independent:
assumes "¬ hb (i, Store e1 mo i) (r, Expunge e2 mo2 r)"
and "¬ hb (r, Expunge e2 mo2 r) (i, Store e1 mo i)"
and "xs prefix of j"
and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)"
and "(r, Expunge e2 mo2 r) ∈ set (node_deliver_messages xs)"
shows "i ≠ mo2 ∧ r ≠ mo"
using assms expunge_store_ids_imply_messages_same concurrent_store_expunge_independent_technical2
concurrent_store_expunge_independent_technical by metis
corollary (in imap) concurrent_store_store_independent:
assumes "¬ hb (i, Store e1 mo i) (r, Store e2 mo2 r)"
and "¬ hb (r, Store e2 mo2 r) (i, Store e1 mo i)"
and "xs prefix of j"
and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)"
and "(r, Store e2 mo2 r) ∈ set (node_deliver_messages xs)"
shows "i ≠ mo2 ∧ r ≠ mo"
using assms store_store_ids_imply_messages_same concurrent_store_store_independent_technical
by metis
lemma (in imap) concurrent_operations_commute:
assumes "xs prefix of i"
shows "hb.concurrent_ops_commute (node_deliver_messages xs)"
proof -
{ fix a b x y
assume "(a, b) ∈ set (node_deliver_messages xs)"
"(x, y) ∈ set (node_deliver_messages xs)"
"hb.concurrent (a, b) (x, y)"
hence "interp_msg (a, b) ⊳ interp_msg (x, y) = interp_msg (x, y) ⊳ interp_msg (a, b)"
apply(unfold interp_msg_def, case_tac "b"; case_tac "y";
simp add: create_create_commute delete_delete_commute append_append_commute
create_append_commute create_expunge_commute create_store_commute
expunge_expunge_commute hb.concurrent_def)
using assms prefix_contains_msg apply (metis (full_types)
create_id_valid create_delete_commute concurrent_create_delete_independent)
using assms prefix_contains_msg apply (metis (full_types)
create_id_valid create_delete_commute concurrent_create_delete_independent)
using assms prefix_contains_msg apply (metis
append_id_valid append_delete_ids_imply_messages_same
concurrent_append_delete_independent_technical delete_append_commute)
using assms prefix_contains_msg apply (metis
concurrent_expunge_delete_independent expunge_id_valid imap.delete_expunge_commute
imap_axioms)
using assms prefix_contains_msg apply (metis
concurrent_store_delete_independent delete_store_commute store_id_valid)
using assms prefix_contains_msg apply (metis
append_id_valid append_delete_ids_imply_messages_same
concurrent_append_delete_independent_technical delete_append_commute)
using assms prefix_contains_msg apply (metis
append_id_valid expunge_id_valid append_expunge_ids_imply_messages_same
concurrent_append_expunge_independent_technical append_expunge_commute)
using assms prefix_contains_msg apply (metis
append_id_valid append_store_commute concurrent_append_store_independent store_id_valid)
using assms prefix_contains_msg apply (metis
concurrent_expunge_delete_independent expunge_id_valid delete_expunge_commute)
using assms prefix_contains_msg apply (metis
append_expunge_commute append_id_valid concurrent_append_expunge_independent
expunge_id_valid)
using assms prefix_contains_msg apply (metis
expunge_id_valid expunge_store_commute imap.concurrent_store_expunge_independent
imap_axioms store_id_valid)
using assms prefix_contains_msg apply (metis
concurrent_store_delete_independent delete_store_commute store_id_valid)
using assms prefix_contains_msg apply (metis
append_id_valid append_store_commute imap.concurrent_append_store_independent imap_axioms
store_id_valid)
using assms prefix_contains_msg apply (metis
expunge_id_valid expunge_store_commute imap.concurrent_store_expunge_independent
imap_axioms store_id_valid)
using assms prefix_contains_msg by (metis concurrent_store_store_independent store_id_valid
store_store_commute)
} thus ?thesis
by(fastforce simp: hb.concurrent_ops_commute_def)
qed
theorem (in imap) convergence:
assumes "set (node_deliver_messages xs) = set (node_deliver_messages ys)"
and "xs prefix of i"
and "ys prefix of j"
shows "apply_operations xs = apply_operations ys"
using assms by(auto simp add: apply_operations_def intro: hb.convergence_ext
concurrent_operations_commute node_deliver_messages_distinct hb_consistent_prefix)
context imap begin
sublocale sec: strong_eventual_consistency weak_hb hb interp_msg
"λops.∃xs i. xs prefix of i ∧ node_deliver_messages xs = ops" "λx.({},{})"
apply(standard; clarsimp simp add: hb_consistent_prefix node_deliver_messages_distinct
concurrent_operations_commute)
apply(metis (no_types, lifting) apply_operations_def bind.bind_lunit not_None_eq
hb.apply_operations_Snoc kleisli_def apply_operations_never_fails interp_msg_def)
using drop_last_message apply blast
done
end
end