Quelle  RGA.thy

(* 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
  text-editing) algorithm. In this section we prove that
  satisfies our list specification. The Isabelle/HOL definition of
  in this section is based on our prior work on formally verifying
  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