# Theory ORSet

(* 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‹Observed-Remove Set›

text‹The ORSet is a well-known CRDT for implementing replicated sets, supporting two operations:
the \emph{insertion} and \emph{deletion} of an arbitrary element in the shared set.›

theory
ORSet
imports
Network
begin

datatype ('id, 'a) operation = Add "'id" "'a" | Rem "'id set" "'a"

type_synonym ('id, 'a) state = "'a ⇒ 'id set"

definition op_elem :: "('id, 'a) operation ⇒ 'a" where
"op_elem oper ≡ case oper of Add i e ⇒ e | Rem is e ⇒ e"

definition interpret_op :: "('id, 'a) operation ⇒ ('id, 'a) state ⇀ ('id, 'a) state" ("⟨_⟩" [0] 1000) where
"interpret_op oper state ≡
let before = state (op_elem oper);
after  = case oper of Add i e ⇒ before ∪ {i} | Rem is e ⇒ before - is
in  Some (state ((op_elem oper) := after))"

definition valid_behaviours :: "('id, 'a) state ⇒ 'id × ('id, 'a) operation ⇒ bool" where
"valid_behaviours state msg ≡
case msg of
(i, Add j  e) ⇒ i = j |
(i, Rem is e) ⇒ is = state e"

locale orset = network_with_constrained_ops _ interpret_op "λx. {}" valid_behaviours

by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

assumes "i ∉ is"
shows "⟨Add i e1⟩ ⊳ ⟨Rem is e2⟩ = ⟨Rem is e2⟩ ⊳ ⟨Add i e1⟩"
using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in orset) 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)
using snoc by force
next
case (Deliver e) thus ?thesis
using snoc by (clarsimp, metis interpret_op_def interp_msg_def bind.bind_lunit prefix_of_appendD)
qed
qed

assumes "xs prefix of j"
and "Deliver (i1, Add i2 e) ∈ set xs"
shows "i1 = i2"
proof -
have "∃s. valid_behaviours s (i1, Add i2 e)"
using assms deliver_in_prefix_is_valid by blast
thus ?thesis
qed

definition (in orset) 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, Add j e) ⇒ if e = p then Some j else None | _ ⇒ None) es"

lemma (in orset) [simp]:
shows "added_ids [] e = []"

lemma (in orset) [simp]:

by (auto simp: added_ids_def map_filter_append map_filter_def)

shows "added_ids ([Deliver (i, Rem is e)]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)

shows "e ≠ e' ⟹ added_ids ([Deliver (i, Add j e)]) e' = []"
by (auto simp: added_ids_def map_filter_append map_filter_def)

by (auto simp: added_ids_def map_filter_append map_filter_def)

shows "i1 ≠ i2"
using assms by simp

assumes "es prefix of j"
and "apply_operations es = Some f"
shows "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

assumes "xs prefix of j"
and "i ∈ set (added_ids xs e)"
shows "Deliver (i, Add i e) ∈ set xs"
using assms proof (induct xs rule: rev_induct, clarsimp)
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 apply (case_tac b; clarsimp)
empty_iff list.set(1) set_ConsD add_id_valid in_set_conv_decomp prefix_of_appendD)
apply force
done
qed
qed

assumes "xs @ [Broadcast (r, Rem ix e)] prefix of j"
and "i ∈ ix"
shows "Deliver (i, Add i e) ∈ set xs"
proof -
obtain y where "apply_operations xs = Some y"
moreover hence "ix = 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
qed

assumes "xs prefix of j"
and "Broadcast (r, Rem ix e) ∈ set xs"
and "i ∈ ix"
shows "Deliver (i, Add i e) ∈ set xs"
using assms Broadcast_Deliver_prefix_closed by (induction xs rule: rev_induct; force)

assumes "i ∈ is"
and "xs prefix of j"
and "(i, Add i e) ∈ set (node_deliver_messages xs)" and "(ir, Rem is e) ∈ set (node_deliver_messages xs)"
shows "hb (i, Add i e) (ir, Rem is e)"
proof -
obtain pre k where "pre@[Broadcast (ir, Rem is e)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence "Deliver (i, Add i e) ∈ set pre"
ultimately show ?thesis
using hb.intros(2) events_in_local_order by blast
qed

assumes "Deliver (i, Add i e1) ∈ set (history j)" and "Deliver (i, Add i e2) ∈ set (history j)"
shows "e1 = e2"
proof -
obtain pre1 pre2 k1 k2 where *: "pre1@[Broadcast (i, Add i e1)] prefix of k1" "pre2@[Broadcast (i, Add i e2)] prefix of k2"
using assms delivery_has_a_cause events_before_exist by meson
using node_histories.prefix_to_carriers node_histories_axioms by force+
ultimately show ?thesis
using msg_id_unique by fastforce
qed

lemma (in orset) ids_imply_messages_same:
assumes "i ∈ is"
and "xs prefix of j"
and "(i, Add i e1) ∈ set (node_deliver_messages xs)" and "(ir, Rem is e2) ∈ set (node_deliver_messages xs)"
shows "e1 = e2"
proof -
obtain pre k where "pre@[Broadcast (ir, Rem is e2)] prefix of k"
using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
moreover hence "Deliver (i, Add i e2) ∈ set pre"
moreover have "Deliver (i, Add i e1) ∈ set (history j)"
using assms(2) assms(3) prefix_msg_in_history by blast
ultimately show ?thesis
by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms operation.inject(1)
prefix_elem_to_carriers prefix_of_appendD prod.inject)
qed

assumes "¬ hb (i, Add i e1) (ir, Rem is e2)" and "¬ hb (ir, Rem is e2) (i, Add i e1)"
and "xs prefix of j"
and "(i, Add i e1) ∈ set (node_deliver_messages xs)" and "(ir, Rem is e2) ∈ set (node_deliver_messages xs)"
shows "i ∉ is"
using assms ids_imply_messages_same concurrent_add_remove_independent_technical by fastforce

lemma (in orset) rem_rem_commute:
shows "⟨Rem i1 e1⟩ ⊳ ⟨Rem i2 e2⟩ = ⟨Rem i2 e2⟩ ⊳ ⟨Rem i1 e1⟩"
by(unfold interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in orset) 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)"
done
} thus ?thesis
by(fastforce simp: hb.concurrent_ops_commute_def)
qed

theorem (in orset) 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 orset 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