(* Martin Kleppmann, University of Cambridge Victor B. F. Gomes, University of Cambridge Dominic P. Mulligan, Arm Research, Cambridge Alastair Beresford, University of Cambridge *) section‹The Replicated Growable Array (RGA)› text‹The RGA algorithm \<^cite>‹"Roh:2011dw"› is a replicated list (or collaborative text-editing) algorithm. In this section we prove that RGA satisfies our list specification. The Isabelle/HOL definition of RGA in this section is based on our prior work on formally verifying CRDTs \<^cite>‹"Gomes:2017gy" and "Gomes:2017vo"›.› theory RGA imports Insert_Spec begin fun insert_body :: "'oid::{linorder} list ⇒ 'oid ⇒ 'oid list" where "insert_body [] e = [e]" | "insert_body (x # xs) e = (if x < e then e # x # xs else x # insert_body xs e)" fun insert_rga :: "'oid::{linorder} list ⇒ ('oid × 'oid option) ⇒ 'oid list" where "insert_rga xs (e, None) = insert_body xs e" | "insert_rga [] (e, Some i) = []" | "insert_rga (x # xs) (e, Some i) = (if x = i then x # insert_body xs e else x # insert_rga xs (e, Some i))" definition interp_rga :: "('oid::{linorder} × 'oid option) list ⇒ 'oid list" where "interp_rga ops ≡ foldl insert_rga [] ops" subsection‹Commutativity of \isa{insert-rga}› lemma insert_body_set_ins [simp]: shows "set (insert_body xs e) = insert e (set xs)" by (induction xs, auto) lemma insert_rga_set_ins: assumes "i ∈ set xs" shows "set (insert_rga xs (oid, Some i)) = insert oid (set xs)" using assms by (induction xs, auto) lemma insert_body_commutes: shows "insert_body (insert_body xs e1) e2 = insert_body (insert_body xs e2) e1" by (induction xs, auto) lemma insert_rga_insert_body_commute: assumes "i2 ≠ Some e1" shows "insert_rga (insert_body xs e1) (e2, i2) = insert_body (insert_rga xs (e2, i2)) e1" using assms by (induction xs; cases i2) (auto simp add: insert_body_commutes) lemma insert_rga_None_commutes: assumes "i2 ≠ Some e1" shows "insert_rga (insert_rga xs (e1, None)) (e2, i2 ) = insert_rga (insert_rga xs (e2, i2 )) (e1, None)" using assms by (induction xs; cases i2) (auto simp add: insert_body_commutes) lemma insert_rga_nonexistent: assumes "i ∉ set xs" shows "insert_rga xs (e, Some i) = xs" using assms by (induction xs, auto) lemma insert_rga_Some_commutes: assumes "i1 ∈ set xs" and "i2 ∈ set xs" and "e1 ≠ i2" and "e2 ≠ i1" shows "insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1)" using assms proof (induction xs, simp) case (Cons a xs) then show ?case by (cases "a = i1"; cases "a = i2"; auto simp add: insert_body_commutes insert_rga_insert_body_commute) qed lemma insert_rga_commutes: assumes "i2 ≠ Some e1" and "i1 ≠ Some e2" shows "insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)" proof(cases i1) case None then show ?thesis using assms(1) insert_rga_None_commutes by (cases i2, fastforce, blast) next case some_r1: (Some r1) then show ?thesis proof(cases i2) case None then show ?thesis using assms(2) insert_rga_None_commutes by fastforce next case some_r2: (Some r2) then show ?thesis proof(cases "r1 ∈ set xs ∧ r2 ∈ set xs") case True then show ?thesis using assms some_r1 some_r2 by (simp add: insert_rga_Some_commutes) next case False then show ?thesis using assms some_r1 some_r2 by (metis insert_iff insert_rga_nonexistent insert_rga_set_ins) qed qed qed lemma insert_body_split: shows "∃p s. xs = p @ s ∧ insert_body xs e = p @ e # s" proof(induction xs, force) case (Cons a xs) then obtain p s where IH: "xs = p @ s ∧ insert_body xs e = p @ e # s" by blast then show "∃p s. a # xs = p @ s ∧ insert_body (a # xs) e = p @ e # s" proof(cases "a < e") case True then have "a # xs = [] @ (a # p @ s) ∧ insert_body (a # xs) e = [] @ e # (a # p @ s)" by (simp add: IH) then show ?thesis by blast next case False then have "a # xs = (a # p) @ s ∧ insert_body (a # xs) e = (a # p) @ e # s" using IH by auto then show ?thesis by blast qed qed lemma insert_between_elements: assumes "xs = pre @ ref # suf" and "distinct xs" and "⋀i. i ∈ set xs ⟹ i < e" shows "insert_rga xs (e, Some ref) = pre @ ref # e # suf" using assms proof(induction xs arbitrary: pre, force) case (Cons a xs) then show "insert_rga (a # xs) (e, Some ref) = pre @ ref # e # suf" proof(cases pre) case pre_nil: Nil then have "a = ref" using Cons.prems(1) by auto then show ?thesis using Cons.prems pre_nil by (cases suf, auto) next case (Cons b pre') then have "insert_rga xs (e, Some ref) = pre' @ ref # e # suf" using Cons.IH Cons.prems by auto then show ?thesis using Cons.prems(1) Cons.prems(2) local.Cons by auto qed qed lemma insert_rga_after_ref: assumes "∀x∈set as. a ≠ x" and "insert_body (cs @ ds) e = cs @ e # ds" shows "insert_rga (as @ a # cs @ ds) (e, Some a) = as @ a # cs @ e # ds" using assms by (induction as; auto) lemma insert_rga_preserves_order: assumes "i = None ∨ (∃i'. i = Some i' ∧ i' ∈ set xs)" and "distinct xs" shows "∃pre suf. xs = pre @ suf ∧ insert_rga xs (e, i) = pre @ e # suf" proof(cases i) case None then show "∃pre suf. xs = pre @ suf ∧ insert_rga xs (e, i) = pre @ e # suf" using insert_body_split by auto next case (Some r) moreover from this obtain as bs where "xs = as @ r # bs ∧ (∀x ∈ set as. x ≠ r)" using assms(1) split_list_first by fastforce moreover have "∃cs ds. bs = cs @ ds ∧ insert_body bs e = cs @ e # ds" by (simp add: insert_body_split) then obtain cs ds where "bs = cs @ ds ∧ insert_body bs e = cs @ e # ds" by blast ultimately have "xs = (as @ r # cs) @ ds ∧ insert_rga xs (e, i) = (as @ r # cs) @ e # ds" using insert_rga_after_ref by fastforce then show ?thesis by blast qed subsection‹Lemmas about the \isa{rga-ops} predicate› definition rga_ops :: "('oid::{linorder} × 'oid option) list ⇒ bool" where "rga_ops list ≡ crdt_ops list set_option" lemma rga_ops_rem_last: assumes "rga_ops (xs @ [x])" shows "rga_ops xs" using assms crdt_ops_rem_last rga_ops_def by blast lemma rga_ops_rem_penultimate: assumes "rga_ops (xs @ [(i1, r1), (i2, r2)])" and "⋀r. r2 = Some r ⟹ r ≠ i1" shows "rga_ops (xs @ [(i2, r2)])" using assms proof - have "crdt_ops (xs @ [(i2, r2)]) set_option" using assms crdt_ops_rem_penultimate rga_ops_def by fastforce thus "rga_ops (xs @ [(i2, r2)])" by (simp add: rga_ops_def) qed lemma rga_ops_ref_exists: assumes "rga_ops (pre @ (oid, Some ref) # suf)" shows "ref ∈ fst ` set pre" proof - from assms have "crdt_ops (pre @ (oid, Some ref) # suf) set_option" by (simp add: rga_ops_def) moreover have "set_option (Some ref) = {ref}" by simp ultimately show "ref ∈ fst ` set pre" using crdt_ops_ref_exists by fastforce qed subsection‹Lemmas about the \isa{interp-rga} function› lemma interp_rga_tail_unfold: shows "interp_rga (xs@[x]) = insert_rga (interp_rga (xs)) x" by (clarsimp simp add: interp_rga_def) lemma interp_rga_ids: assumes "rga_ops xs" shows "set (interp_rga xs) = set (map fst xs)" using assms proof(induction xs rule: List.rev_induct) case Nil then show "set (interp_rga []) = set (map fst [])" by (simp add: interp_rga_def) next case (snoc x xs) hence IH: "set (interp_rga xs) = set (map fst xs)" using rga_ops_rem_last by blast obtain xi xr where x_pair: "x = (xi, xr)" by force then show "set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))" proof(cases xr) case None then show ?thesis using IH x_pair by (clarsimp simp add: interp_rga_def) next case (Some r) moreover from this have "r ∈ set (interp_rga xs)" using IH rga_ops_ref_exists by (metis x_pair list.set_map snoc.prems) ultimately have "set (interp_rga (xs @ [(xi, xr)])) = insert xi (set (interp_rga xs))" by (simp add: insert_rga_set_ins interp_rga_tail_unfold) then show "set (interp_rga (xs @ [x])) = set (map fst (xs @ [x]))" using IH x_pair by auto qed qed lemma interp_rga_distinct: assumes "rga_ops xs" shows "distinct (interp_rga xs)" using assms proof(induction xs rule: List.rev_induct) case Nil then show "distinct (interp_rga [])" by (simp add: interp_rga_def) next case (snoc x xs) hence IH: "distinct (interp_rga xs)" using rga_ops_rem_last by blast moreover obtain xi xr where x_pair: "x = (xi, xr)" by force moreover from this have "xi ∉ set (interp_rga xs)" using interp_rga_ids crdt_ops_unique_last rga_ops_rem_last by (metis rga_ops_def snoc.prems) moreover have "∃pre suf. interp_rga xs = pre@suf ∧ insert_rga (interp_rga xs) (xi, xr) = pre @ xi # suf" proof - have "⋀r. r ∈ set_option xr ⟹ r ∈ set (map fst xs)" using crdt_ops_ref_exists rga_ops_def snoc.prems x_pair by fastforce hence "xr = None ∨ (∃r. xr = Some r ∧ r ∈ set (map fst xs))" using option.set_sel by blast hence "xr = None ∨ (∃r. xr = Some r ∧ r ∈ set (interp_rga xs))" using interp_rga_ids rga_ops_rem_last snoc.prems by blast thus ?thesis using IH insert_rga_preserves_order by blast qed ultimately show "distinct (interp_rga (xs @ [x]))" by (metis Un_iff disjoint_insert(1) distinct.simps(2) distinct_append interp_rga_tail_unfold list.simps(15) set_append) qed subsection‹Proof that RGA satisfies the list specification› lemma final_insert: assumes "set (xs @ [x]) = set (ys @ [x])" and "rga_ops (xs @ [x])" and "insert_ops (ys @ [x])" and "interp_rga xs = interp_ins ys" shows "interp_rga (xs @ [x]) = interp_ins (ys @ [x])" proof - obtain oid ref where x_pair: "x = (oid, ref)" by force have "distinct (xs @ [x])" and "distinct (ys @ [x])" using assms crdt_ops_distinct spec_ops_distinct rga_ops_def insert_ops_def by blast+ then have "set xs = set ys" using assms(1) by force have oid_greatest: "⋀i. i ∈ set (interp_rga xs) ⟹ i < oid" proof - have "⋀i. i ∈ set (map fst ys) ⟹ i < oid" using assms(3) by (simp add: spec_ops_id_inc x_pair insert_ops_def) hence "⋀i. i ∈ set (map fst xs) ⟹ i < oid" using ‹set xs = set ys› by auto thus "⋀i. i ∈ set (interp_rga xs) ⟹ i < oid" using assms(2) interp_rga_ids rga_ops_rem_last by blast qed thus "interp_rga (xs @ [x]) = interp_ins (ys @ [x])" proof(cases ref) case None moreover from this have "insert_rga (interp_rga xs) (oid, ref) = oid # interp_rga xs" using oid_greatest hd_in_set insert_body.elims insert_body.simps(1) insert_rga.simps(1) list.sel(1) by metis ultimately show "interp_rga (xs @ [x]) = interp_ins (ys @ [x])" using assms(4) by (simp add: interp_ins_tail_unfold interp_rga_tail_unfold x_pair) next case (Some r) have "∃as bs. interp_rga xs = as @ r # bs" proof - have "r ∈ set (map fst xs)" using assms(2) Some by (simp add: rga_ops_ref_exists x_pair) hence "r ∈ set (interp_rga xs)" using assms(2) interp_rga_ids rga_ops_rem_last by blast thus ?thesis by (simp add: split_list) qed from this obtain as bs where as_bs: "interp_rga xs = as @ r # bs" by force hence "distinct (as @ r # bs)" by (metis assms(2) interp_rga_distinct rga_ops_rem_last) hence "insert_rga (as @ r # bs) (oid, Some r) = as @ r # oid # bs" by (metis as_bs insert_between_elements oid_greatest) moreover have "insert_spec (as @ r # bs) (oid, Some r) = as @ r # oid # bs" by (meson ‹distinct (as @ r # bs)› insert_after_ref) ultimately show "interp_rga (xs @ [x]) = interp_ins (ys @ [x])" by (metis assms(4) Some as_bs interp_ins_tail_unfold interp_rga_tail_unfold x_pair) qed qed lemma interp_rga_reorder: assumes "rga_ops (pre @ suf @ [(oid, ref)])" and "⋀i r. (i, Some r) ∈ set suf ⟹ r ≠ oid" and "⋀r. ref = Some r ⟹ r ∉ fst ` set suf" shows "interp_rga (pre @ (oid, ref) # suf) = interp_rga (pre @ suf @ [(oid, ref)])" using assms proof(induction suf rule: List.rev_induct) case Nil then show ?case by simp next case (snoc x xs) have ref_not_x: "⋀r. ref = Some r ⟹ r ≠ fst x" using snoc.prems(3) by auto have IH: "interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])" proof - have "rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])" using snoc.prems(1) by auto moreover have "⋀r. ref = Some r ⟹ r ≠ fst x" by (simp add: ref_not_x) ultimately have "rga_ops ((pre @ xs) @ [(oid, ref)])" using rga_ops_rem_penultimate by (metis (no_types, lifting) Cons_eq_append_conv prod.collapse) thus ?thesis using snoc by force qed obtain xi xr where x_pair: "x = (xi, xr)" by force have "interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) = insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)" using IH interp_rga_tail_unfold by (metis append.assoc append_Cons) moreover have "... = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)" using interp_rga_tail_unfold by (metis append_assoc) moreover have "... = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)" proof - have "⋀xrr. xr = Some xrr ⟹ xrr ≠ oid" using x_pair snoc.prems(2) by auto thus ?thesis using insert_rga_commutes ref_not_x by (metis fst_conv x_pair) qed moreover have "... = interp_rga (pre @ xs @ [x] @ [(oid, ref)])" by (metis append_assoc interp_rga_tail_unfold x_pair) ultimately show "interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])" by (simp add: x_pair) qed lemma rga_spec_equal: assumes "set xs = set ys" and "insert_ops xs" and "rga_ops ys" shows "interp_ins xs = interp_rga ys" using assms proof(induction xs arbitrary: ys rule: rev_induct) case Nil then show ?case by (simp add: interp_rga_def interp_ins_def) next case (snoc x xs) hence "x ∈ set ys" by (metis last_in_set snoc_eq_iff_butlast) from this obtain pre suf where ys_split: "ys = pre @ [x] @ suf" using split_list_first by fastforce have IH: "interp_ins xs = interp_rga (pre @ suf)" proof - have "crdt_ops (pre @ suf) set_option" proof - have "crdt_ops (pre @ [x] @ suf) set_option" using rga_ops_def snoc.prems(3) ys_split by blast thus "crdt_ops (pre @ suf) set_option" using crdt_ops_rem_spec snoc.prems ys_split insert_ops_def by blast qed hence "rga_ops (pre @ suf)" using rga_ops_def by blast moreover have "set xs = set (pre @ suf)" by (metis append_set_rem_last crdt_ops_distinct insert_ops_def rga_ops_def snoc.prems spec_ops_distinct ys_split) ultimately show ?thesis using insert_ops_rem_last ys_split snoc by metis qed have valid_rga: "rga_ops (pre @ suf @ [x])" proof - have "crdt_ops (pre @ suf @ [x]) set_option" using snoc.prems ys_split by (simp add: crdt_ops_reorder_spec insert_ops_def rga_ops_def) thus "rga_ops (pre @ suf @ [x])" by (simp add: rga_ops_def) qed have "interp_ins (xs @ [x]) = interp_rga (pre @ suf @ [x])" proof - have "set (xs @ [x]) = set (pre @ suf @ [x])" using snoc.prems(1) ys_split by auto thus ?thesis using IH snoc.prems(2) valid_rga final_insert append_assoc by metis qed moreover have "... = interp_rga (pre @ [x] @ suf)" proof - obtain oid ref where x_pair: "x = (oid, ref)" by force have "⋀op2 r. op2 ∈ snd ` set suf ⟹ r ∈ set_option op2 ⟹ r ≠ oid" using snoc.prems by (simp add: crdt_ops_independent_suf insert_ops_def rga_ops_def x_pair ys_split) hence "⋀i r. (i, Some r) ∈ set suf ⟹ r ≠ oid" by fastforce moreover have "⋀r. ref = Some r ⟹ r ∉ fst ` set suf" using crdt_ops_no_future_ref snoc.prems(3) x_pair ys_split by (metis option.set_intros rga_ops_def) ultimately show "interp_rga (pre @ suf @ [x]) = interp_rga (pre @ [x] @ suf)" using interp_rga_reorder valid_rga x_pair by force qed ultimately show "interp_ins (xs @ [x]) = interp_rga ys" by (simp add: ys_split) qed lemma insert_ops_exist: assumes "rga_ops xs" shows "∃ys. set xs = set ys ∧ insert_ops ys" using assms by (simp add: crdt_ops_spec_ops_exist insert_ops_def rga_ops_def) theorem rga_meets_spec: assumes "rga_ops xs" shows "∃ys. set ys = set xs ∧ insert_ops ys ∧ interp_ins ys = interp_rga xs" using assms rga_spec_equal insert_ops_exist by metis end