Theory Co_Snapshot

theory Co_Snapshot

section ‹Extension to infinite traces›

text ‹The computation locale assumes that there already exists a known
final configuration $c'$ to the given initial $c$ and trace $t$. However,
we can show that the snapshot algorithm must terminate correctly even if
the underlying computation itself does not terminate. We relax
the trace relation to allow for a potentially infinite number of ``intermediate'' events, and
show that the algorithm's correctness still holds when imposing the same constraints
as in the computation locale.

We use a preexisting theory of lazy list chains by Schlichtkrull, Blanchette,
Traytel and Waldmann~cite"Ordered_Resolution_Prover-AFP" to construct infinite traces.›

primrec ltake where
  "ltake 0 t = []"
| "ltake (Suc i) t = (case t of LNil  [] | LCons x t'  x # ltake i t')"

primrec ldrop where
  "ldrop 0 t = t"
| "ldrop (Suc i) t = (case t of LNil  LNil | LCons x t'  ldrop i t')"

lemma ltake_LNil[simp]: "ltake i LNil = []"
  by (induct i) auto

lemma ltake_LCons: "0 < i  ltake i (LCons x t) = x # ltake (i - 1) t"
  by (induct i) auto

lemma take_ltake: "i  j  take i (ltake j xs) = ltake i xs"
  by (induct j arbitrary: i xs) (auto simp: le_Suc_eq take_Cons' ltake_LCons split: llist.splits if_splits)

lemma nth_ltake [simp]: "i < min n (llength xs)  (ltake n xs) ! i = lnth xs i"
  by (induct n arbitrary: i xs)
    (auto simp: nth_Cons' gr0_conv_Suc eSuc_enat[symmetric] split: llist.splits)

lemma length_ltake[simp]: "length (ltake i xs) = (case llength xs of   i | enat m  min i m)"
  by (induct i arbitrary: xs)
    (auto simp: zero_enat_def[symmetric] eSuc_enat split: llist.splits enat.splits)

lemma ltake_prepend:
  "ltake i (prepend xs t) = (if i  length xs then take i xs else xs @ ltake (i - length xs) t)"
proof (induct i arbitrary: xs t)
  case 0
  then show ?case 
    by (cases xs) auto
  case (Suc i)
  then show ?case
    by (cases xs) auto

lemma prepend_ltake_ldrop_id: "prepend (ltake i t) (ldrop i t) = t"
  by (induct i arbitrary: t) (auto split: llist.splits)

context distributed_system

coinductive cotrace where
    cotr_init: "cotrace c LNil"
  | cotr_step: " c  ev  c'; cotrace c' t   cotrace c (LCons ev t)"

lemma cotrace_trace: "cotrace c t  ∃!c'. trace c (ltake i t) c'"
proof (induct i arbitrary: c t)
  case (Suc i)
  then show ?case
  proof (cases t)
    case (LCons ev t')
    with Suc(2) obtain c' where "c  ev  c'" "cotrace c' t'"
      by (auto elim: cotrace.cases)
    with Suc(1)[OF cotrace c' t'] show ?thesis
      by (auto simp: LCons elim: trace.intros(2) elim: trace.cases trace_and_start_determines_end)
  qed (auto intro: trace.intros elim: trace.cases)
qed (auto simp: zero_enat_def[symmetric] intro: trace.intros elim: trace.cases)

lemma cotrace_trace': "cotrace c t  c'. trace c (ltake i t) c'"
  by (metis cotrace_trace)

definition cos where "cos c t i = s c (ltake i t) i"

lemma cotrace_trace_cos: "cotrace c t  trace c (ltake i t) (cos c t i)"
  unfolding cos_def s_def
  by (subst take_ltake, auto dest!: cotrace_trace[of _ _ i] elim!: theI')

lemma s_0[simp]: "s c t 0 = c"
  unfolding s_def
  by (auto intro!: the_equality[where P = "trace c []"] trace.intros elim: trace.cases)

lemma s_chop: "i  length t  s c t i = s c (take i t) i"
  unfolding s_def
  by auto

lemma cotrace_prepend: "trace c t c'  cotrace c' u  cotrace c (prepend t u)"
  by (induct c t c' rule: trace.induct) (auto intro: cotrace.intros)

lemma s_Cons: "c''. trace c' xs c''  c  ev  c'  s c (ev # xs) (Suc i) = s c' xs i"
  by (smt exists_trace_for_any_i take_Suc_Cons tr_step trace_and_start_determines_end)

lemma cotrace_ldrop: "cotrace c t  i  llength t  cotrace (cos c t i) (ldrop i t)"
proof (induct i arbitrary: c t)
  case (Suc i)
  then show ?case
  proof (cases t)
    case (LCons ev t')
    with Suc(2) obtain c' where "c  ev  c'" "cotrace c' t'"
      by (auto elim: cotrace.cases)
    with Suc(1)[OF cotrace c' t'] Suc(3) show ?thesis
      by (auto simp: LCons cos_def eSuc_enat[symmetric] s_chop[symmetric] s_Cons[OF cotrace_trace'])
  qed (auto intro: cotrace.intros)
qed (auto simp: zero_enat_def[symmetric] cos_def intro: cotrace.intros)


locale cocomputation = distributed_system +
    init :: "('a, 'b, 'c) configuration"
      "finite {i. p q. channel i = Some (p, q)}" and
      "p q. (p  q) 
         (tranclp (λp q. (i. channel i = Some (p, q)))) p q" and

      "card (UNIV :: 'a set) > 1" and
      "finite (UNIV :: 'a set)" and

      "i. (p q. channel i = Some (p, q))
       Marker  set (msgs init i)" and
      "i. channel i = None  msgs init i = []" and
      "p. ¬ has_snapshotted init p" and
      "i. channel_snapshot init i = ([], NotStarted)" and

    valid: "t. cotrace init t" and
    l1: "t i cid. cotrace init t
                  Marker  set (msgs (cos init t i) cid)
       (j  llength t. j  i  Marker  set (msgs (cos init t j) cid))" and
    l2: "t p. cotrace init t
       (i  llength t. has_snapshotted (cos init t i) p)"

abbreviation coS where "coS  cos init"

definition "some_snapshot t p = (SOME i. has_snapshotted (coS t i) p  i  llength t)"

lemma has_snapshotted: 
  "cotrace init t  has_snapshotted (coS t (some_snapshot t p)) p  some_snapshot t p  llength t"
  unfolding some_snapshot_def by (rule someI_ex) (auto dest!: l2[rule_format])

lemma cotrace_cos: "cotrace init t  j < llength t  
  (coS t j)  lnth t j  (coS t (Suc j))"
  apply (drule cotrace_trace_cos[of _ _ "Suc j"])
  apply (drule step_Suc[rotated, of _ _ _ "j"])
   apply (auto split: enat.splits llist.splits) []
  apply (auto simp: s_chop[of j "_ # ltake j _"] cos_def nth_Cons' ltake_LCons lnth_LCons'
    take_Cons' take_ltake
    split: llist.splits enat.splits if_splits elim: order.strict_trans2[rotated])
  apply (subst (asm) s_chop[of j "_ # ltake j _"])
   apply (auto simp: take_Cons' take_ltake split: enat.splits)

lemma snapshot_stable:
  "cotrace init t  i  j  has_snapshotted (coS t i) p  has_snapshotted (coS t j) p"
  apply (drule cotrace_trace_cos[of _ _ j])
  unfolding cos_def
  by (metis exists_trace_for_any_i_j order_refl s_def snapshot_stable take_ltake)

lemma no_markers_if_all_snapshotted:
  "cotrace init t  i  j  p. has_snapshotted (coS t i) p 
      Marker  set (msgs (coS t i) c)  Marker  set (msgs (coS t j) c)"  
  apply (drule cotrace_trace_cos[of _ _ j])
  unfolding cos_def
  by (metis exists_trace_for_any_i_j no_markers_if_all_snapshotted order_refl s_def take_ltake)

lemma cotrace_all_have_snapshotted:
  assumes "cotrace init t"
  shows "i  llength t. p. has_snapshotted (coS t i) p"
proof -
  let ?i = "Max (range (some_snapshot t))"
  show ?thesis
    using has_snapshotted[OF assms] snapshot_stable[OF assms, of "some_snapshot t _" ?i _]
    apply (intro exI[of _ ?i])
    apply (auto simp: finite_processes)
     apply (cases "llength t"; auto simp: )
     apply (subst Max_le_iff)
       apply (auto simp: finite_processes)
    apply blast

lemma no_messages_if_no_channel:
  assumes "cotrace init t"
  shows "channel cid = None  msgs (coS t i) cid = []"
  using no_messages_introduced_if_no_channel[OF assms[THEN cotrace_trace_cos, of i] no_msgs_if_no_channel, of cid i]
  by (auto simp: cos_def)

lemma cotrace_all_have_snapshotted_and_no_markers:
  assumes "cotrace init t"
  shows "i  llength t. (p. has_snapshotted (coS t i) p)  
                         (c. Marker  set (msgs (coS t i) c))"
proof -
  from cotrace_all_have_snapshotted[OF assms] obtain j :: nat where
    j: "j  llength t" "p. has_snapshotted (coS t j) p" by blast
  from j(2) have *: "has_snapshotted (coS t k) p" if "k  j" for k p
      using snapshot_stable[OF assms, of j k p] that by auto
  define C where "C = {c. Marker  set (msgs (coS t j) c)}"
  have "finite C"
    using no_messages_if_no_channel[OF assms, of _ j] unfolding C_def
    by (intro finite_subset[OF _ finite_channels]) fastforce
  define pick where "pick = (λc. SOME k. k  llength t  k  j  Marker  set (msgs (coS t k) c))"
  { fix c
    assume "c  C"
    then have "k  llength t. k  j  Marker  set (msgs (coS t k) c)"
      using l1[rule_format, of t j c] assms unfolding C_def by blast
    then have "pick c  llength t  pick c  j  Marker  set (msgs (coS t (pick c)) c)"
      unfolding pick_def
      by (rule someI_ex)
  } note pick = conjunct1[OF this] conjunct1[OF conjunct2[OF this]] conjunct2[OF conjunct2[OF this]]
  show ?thesis
  proof (cases "C = {}")
    case True
    with j show ?thesis
      by (auto intro!: exI[of _ j] simp: C_def)
    define m where "m = Max (pick ` C)"
    case False
    with finite C have m: "m  pick ` C" "x  pick ` C. m  x"
      unfolding m_def by auto
    then have "j  m" using pick(2) by auto
    from *[OF j  m] have "Marker  set (msgs (coS t m) c)" for c
    proof (cases "c  C")
      case True
      then show ?thesis
        using no_markers_if_all_snapshotted[OF assms, of "pick c" m c] pick[of c] m *
        by auto
      case False
      then show ?thesis
        using no_markers_if_all_snapshotted[OF assms j  m j(2), of c]
        by (auto simp: C_def)
    with *[OF j  m] m pick show ?thesis by auto

  fixes t
  assumes cotrace: "cotrace init t"

definition "final_i 
  (SOME i. i  llength t  (p. has_snapshotted (coS t i) p)  (c. Marker  set (msgs (coS t i) c)))"

definition final where
  "final = coS t final_i"

lemma final_i: "final_i  llength t" "(p. has_snapshotted (coS t final_i) p)" "(c. Marker  set (msgs (coS t final_i) c))"
  unfolding final_i_def
  by (rule someI2_ex[OF cotrace_all_have_snapshotted_and_no_markers[OF cotrace]]; auto intro: cotrace_trace_cos[OF cotrace])+

lemma final: "t. trace init t final" "(p. has_snapshotted final p)" "(c. Marker  set (msgs final c))"
  unfolding final_def
  by (rule cotrace_trace_cos[OF cotrace] final_i exI)+

interpretation computation channel trans send recv init final
  apply standard
            apply (rule finite_channels)
           apply (rule strongly_connected_raw)
          apply (rule at_least_two_processes)
         apply (rule finite_processes)
        apply (rule no_initial_Marker)
       apply (rule no_msgs_if_no_channel)
      apply (rule no_initial_process_snapshot)
     apply (rule no_initial_channel_snapshot)
    apply (rule final(1))
   apply (intro allI impI)
  subgoal for t i cid
    apply (rule exI[of _ "length t"])
    apply (metis exists_trace_for_any_i final(3) le_cases take_all trace_and_start_determines_end)
  apply (intro allI impI)
  subgoal for t p
    apply (rule exI[of _ "length t"])
    apply (metis exists_trace_for_any_i final(2) order_refl take_all trace_and_start_determines_end)

definition coperm where
  "coperm l r = (xs ys z. mset xs = mset ys  l = prepend xs z  r = prepend ys z)"

lemma copermIL: "mset ys = mset xs  t = prepend xs z  coperm (prepend ys z) t"
  unfolding coperm_def by auto

lemma snapshot_algorithm_is_cocorrect:
  "t' i. cotrace init t'  coperm t' t  state_equal_to_snapshot (coS t' i) final  i  final_i"
proof -
  define prefix where "prefix = ltake final_i t"
  define suffix where "suffix = ldrop final_i t"
  have [simp]: "prepend prefix suffix = t"
    unfolding prefix_def suffix_def prepend_ltake_ldrop_id ..
  have [simp]: "cotrace final suffix"
    unfolding suffix_def final_def
    by (auto simp: cotrace final_i(1) intro!: cotrace_ldrop)
  from cotrace_trace_cos[OF cotrace] have "trace init prefix final"
    unfolding final_def prefix_def by blast
  with snapshot_algorithm_is_correct obtain prefix' i where
    "trace init prefix' final" "mset prefix' = mset prefix" "state_equal_to_snapshot (S prefix' i) final"
    "i  length prefix'"
    by blast
  moreover from mset prefix' = mset prefix i  length prefix' have "i  final_i"
    by (auto dest!: mset_eq_length simp: prefix_def split: enat.splits)
  ultimately show ?thesis
    by (intro exI[of _ "prepend prefix' suffix"] exI[of _ i])
      (auto simp: cos_def ltake_prepend s_chop[symmetric] intro!: cotrace_prepend elim!: copermIL)


print_statement snapshot_algorithm_is_cocorrect