Quelle  Trace.thy

section ‹Traces›

text ‹Traces extend transitions to finitely many intermediate events.›

theory Trace
  imports
    "HOL-Library.Sublist"
    Distributed_System

begin

context distributed_system

begin

text ‹We can think of a trace as the transitive closure of the next
 . A trace consists of initial and final configurations $c$ and
 c'$, with an ordered list of events $t$ occurring sequentially on $c$,
  $c'$.›

inductive (in distributed_system) trace where
    tr_init: "trace c [] c"
  | tr_step: "[ c ⊨ ev ↦ c'; trace c' t c'' ]
              ==> trace c (ev # t) c''"

subsection ‹Properties of traces›

lemma trace_trans:
  shows
    "[ trace c t c';
       trace c' t' c''
     ] ==> trace c (t @ t') c''"
proof (induct c t c' rule:trace.induct)
  case tr_init
  then show ?case by simp
next
  case tr_step
  then show ?case using trace.tr_step by auto
qed

lemma trace_decomp_head:
  assumes
    "trace c (ev # t) c'"
  shows
    "∃c''. c ⊨ ev ↦ c'' ∧ trace c'' t c'"
  using assms trace.simps by blast

lemma trace_decomp_tail:
  shows
    "trace c (t @ [ev]) c' ==> ∃c''. trace c t c'' ∧ c'' ⊨ ev ↦ c'"
proof (induct t arbitrary: c)
  case Nil
  then show ?case 
    by (metis (mono_tags, lifting) append_Nil distributed_system.trace.simps distributed_system_axioms list.discI list.sel(1) list.sel(3))
next
  case (Cons ev' t)
  then obtain d where step: "c ⊨ ev' ↦ d" and "trace d (t @ [ev]) c'" using trace_decomp_head by force
  then obtain d' where tr: "trace d t d'" and "d' ⊨ ev ↦ c'" using Cons.hyps by blast
  moreover have "trace c (ev' # t) d'" using step tr trace.tr_step by simp
  ultimately show ?case by auto
qed

lemma trace_snoc: 
  assumes
    "trace c t c'" and
    "c' ⊨ ev ↦ c''"
  shows
    "trace c (t @ [ev]) c''"
  using assms(1) assms(2) tr_init tr_step trace_trans by auto

lemma trace_rev_induct [consumes 1, case_names tr_rev_init tr_rev_step]:
  "[ trace c t c';
     (∧c. P c [] c);
     (∧c t c' ev c''. trace c t c' ==> P c t c' ==> c' ⊨ ev ↦ c'' ==> P c (t @ [ev]) c'')
   ] ==> P c t c'"
proof (induct t arbitrary: c' rule:rev_induct)
  case Nil
  then show ?case 
    using distributed_system.trace.cases distributed_system_axioms by blast
next
  case (snoc ev t)
  then obtain c'' where "trace c t c''" "c'' ⊨ ev ↦ c'" using trace_decomp_tail by blast
  then show ?case using snoc by simp
qed

lemma trace_and_start_determines_end:
  shows
    "trace c t c' ==> trace c t d' ==> c' = d'"
proof (induct c t c' arbitrary: d' rule:trace_rev_induct)
  case tr_rev_init
  then show ?case using trace.cases by fastforce
next
  case (tr_rev_step c t c' ev c'')
  then obtain d'' where "trace c t d''" "d'' ⊨ ev ↦ d'" using trace_decomp_tail by blast
  then show ?case using tr_rev_step state_and_event_determine_next by simp
qed

lemma suffix_split_trace:
  shows
    "[ trace c t c';
       suffix t' t
     ] ==> ∃c''. trace c'' t' c'"
proof (induct t arbitrary: c)
  case Nil
  then have "t' = []" by simp
  then have "trace c' t' c'" using tr_init by simp
  then show ?case by blast
next
  case (Cons ev t'')
  from Cons.prems have q: "suffix t' t'' ∨ t' = ev # t''" by (meson suffix_Cons)
  thus ?case
  proof (cases "suffix t' t''")
    case True
    then show ?thesis using Cons.hyps Cons.prems(1) trace.simps by blast
  next
    case False
    hence "t' = ev # t''" using q by simp
    thus ?thesis using Cons.hyps Cons.prems by blast
  qed
qed

lemma prefix_split_trace:
  fixes
    c :: "('p, 's, 'm) configuration" and
    t :: "('p, 's, 'm) trace"
  shows
    "[ ∃c'. trace c t c';
       prefix t' t
     ] ==> ∃c''. trace c t' c''"
proof (induct t rule:rev_induct)
  case Nil
  then show ?case by simp
next
  case (snoc ev t'')
  from snoc.prems have q: "prefix t' t'' ∨ t' = t'' @ [ev]" by auto
  thus ?case
  proof (cases "prefix t' t''")
    case True
    thus ?thesis using trace_decomp_tail using snoc.hyps snoc.prems(1) trace.simps by blast
  next
    case False
    thus ?thesis using q snoc.prems by fast
  qed
qed

lemma split_trace:
  shows
    "[ trace c t c';
       t = t' @ t''
     ] ==> ∃c''. trace c t' c'' ∧ trace c'' t'' c'"
proof (induct t'' arbitrary: t')
  case Nil
  then show ?case using tr_init by auto
next
  case (Cons ev t'')
  obtain c'' where p: "trace c (t' @ [ev]) c''"
    using Cons.prems prefix_split_trace rotate1.simps(2) by force
  then have "trace c'' t'' c'"
    using Cons.hyps Cons.prems trace_and_start_determines_end by force
  then show ?case
    by (meson distributed_system.tr_step distributed_system.trace_decomp_tail distributed_system_axioms p)
qed

subsection ‹Describing intermediate configurations›

definition construct_fun_from_rel :: "('a * 'b) set ==> 'a ==> 'b" where
  "construct_fun_from_rel R x = (THE y. (x,y) ∈ R)"

definition trace_rel where
  "trace_rel ≡ {((x, t'), y). trace x t' y}"

lemma fun_must_admit_trace:
  shows
    "single_valued R ==> x ∈ Domain R
     ==> (x, construct_fun_from_rel R x) ∈ R"
  unfolding construct_fun_from_rel_def
  by (rule theI') (auto simp add: single_valued_def)

lemma single_valued_trace_rel:
  shows
    "single_valued trace_rel"
proof (rule single_valuedI)
  fix x y y'
  assume asm: "(x, y) ∈ trace_rel" "(x, y') ∈ trace_rel"
  then obtain x' t where "x = (x', t)"
    by (meson surj_pair)
  then have "trace x' t y" "trace x' t y'"
    using asm trace_rel_def by auto
  then show "y = y'"
    using trace_and_start_determines_end by blast
qed

definition run_trace where
  "run_trace ≡ construct_fun_from_rel trace_rel"

text ‹In order to describe intermediate configurations
  a trace we introduce the $s$ function definition, which,
  an initial configuration $c$, a trace $t$ and an index $i \in \mathbb{N}$,
  the unique state after the first $i$ events of $t$.›

definition s where
  "s c t i = (THE c'. trace c (take i t) c')"

lemma s_is_partial_execution:
  shows
    "s c t i = run_trace (c, take i t)"
  unfolding s_def run_trace_def
            construct_fun_from_rel_def trace_rel_def
  by auto

lemma exists_trace_for_any_i:
  assumes
    "∃c'. trace c t c'"
  shows
    "trace c (take i t) (s c t i)"
proof -
  have "prefix (take i t) t" using take_is_prefix by auto
  then obtain c'' where tr: "trace c (take i t) c''" using assms prefix_split_trace by blast
  then show ?thesis
  proof -
    have "((c, take i t), s c t i) ∈ trace_rel"
      unfolding s_def trace_rel_def construct_fun_from_rel_def 
      by (metis case_prod_conv distributed_system.trace_and_start_determines_end distributed_system_axioms mem_Collect_eq the_equality tr)
    then show ?thesis by (simp add: trace_rel_def)
  qed
qed

lemma exists_trace_for_any_i_j:
  assumes
    "∃c'. trace c t c'" and
    "i ≤ j"
  shows
    "trace (s c t i) (take (j - i) (drop i t)) (s c t j)"
proof -
  have "trace c (take j t) (s c t j)" using exists_trace_for_any_i assms by simp
  from ‹j ≥ i› have "take j t = take i t @ (take (j - i) (drop i t))"
    by (metis le_add_diff_inverse take_add)
  then have "trace c (take i t) (s c t i) ∧ trace (s c t i) (take (j - i) (drop i t)) (s c t j)"
    by (metis (no_types, lifting) assms(1) exists_trace_for_any_i split_trace trace_and_start_determines_end)
  then show ?thesis by simp
qed

lemma step_Suc:
  assumes
    "i < length t" and
    valid: "trace c t c'"
  shows "(s c t i) ⊨ (t ! i) ↦ (s c t (Suc i))"
proof -
  have ex_trace: "trace (s c t i) (take (Suc i - i) (drop i t)) (s c t (Suc i))"
    using exists_trace_for_any_i_j le_less valid by blast
  moreover have "Suc i - i = 1" by auto
  moreover have "take 1 (drop i t) = [t ! i]"
    by (metis ‹Suc i - i = 1› assms(1) hd_drop_conv_nth le_add_diff_inverse lessI nat_less_le same_append_eq take_add take_hd_drop)
  ultimately show ?thesis
    by (metis list.discI trace.simps trace_decomp_head)
qed

subsection ‹Trace-related lemmas›

lemma snapshot_state_unchanged_trace:
  assumes
    "trace c t c'" and
    "ps c p = Some u"
  shows
    "ps c' p = Some u"
  using assms snapshot_state_unchanged by (induct c t c', auto)

lemma no_state_change_if_only_nonregular_events:
  shows
    "[ trace c t c';
       ∄ev. ev ∈ set t ∧ regular_event ev ∧ occurs_on ev = p;
       states c p = st
     ] ==> states c' p = st"
proof (induct c t c' rule:trace_rev_induct)
  case (tr_rev_init c)
  then show ?case by simp
next
  case (tr_rev_step c t c' ev c'')
  then have "states c' p = st"
  proof -
    have "∄ev. ev : set t ∧ regular_event ev ∧ occurs_on ev = p" 
      using tr_rev_step by auto
    then show ?thesis using tr_rev_step by blast
  qed
  then show ?case
    using tr_rev_step no_state_change_if_no_event no_state_change_if_nonregular_event
    by auto
qed

lemma message_must_be_delivered_2_trace:
  assumes
    "trace c t c'" and
    "m : set (msgs c i)" and
    "m ∉ set (msgs c' i)" and
    "channel i = Some (q, p)"
  shows
    "∃ev ∈ set t. (∃p q. ev = RecvMarker i p q ∧ m = Marker) ∨ (∃p q s s' m'. ev = Recv i q p s s' m' ∧ m = Msg m')"
proof (rule ccontr)
  assume "~ (∃ev ∈ set t. (∃p q. ev = RecvMarker i p q ∧ m = Marker) ∨ (∃p q s s' m'. ev = Recv i q p s s' m' ∧ m = Msg m'))" (is ?P)
  have "[ trace c t c'; m : set (msgs c i); ?P ] ==> m : set (msgs c' i)"
  proof (induct c t c' rule:trace_rev_induct)
    case (tr_rev_init c)
    then show ?case by simp
  next
    case (tr_rev_step c t d ev c')
    then have m_in_set: "m : set (msgs d i)" 
      using tr_rev_step by auto
    then show ?case
    proof (cases ev)
      case (Snapshot r)
      then show ?thesis 
        using distributed_system.message_must_be_delivered_2 distributed_system_axioms m_in_set tr_rev_step.hyps(3) by blast
    next
      case (RecvMarker i' r s)
      then show ?thesis
      proof (cases "m = Marker")
        case True
        then have "i' ≠ i" using tr_rev_step RecvMarker by simp
        then show ?thesis 
          using RecvMarker m_in_set message_must_be_delivered_2 tr_rev_step.hyps(3) by blast
      next
        case False
        then show ?thesis 
          using RecvMarker tr_rev_step.hyps(3) m_in_set message_must_be_delivered_2 by blast
      qed
    next
      case (Trans r u u')
      then show ?thesis 
        using tr_rev_step.hyps(3) m_in_set by auto
    next
      case (Send i' r s u u' m')
      then show ?thesis 
        using distributed_system.message_must_be_delivered_2 distributed_system_axioms m_in_set tr_rev_step.hyps(3) by blast
    next
      case (Recv i' r s u u' m')
      then show ?thesis
      proof (cases "Msg m' = m")
        case True
        then have "i' ≠ i" using Recv tr_rev_step by auto
        then show ?thesis 
          using Recv m_in_set tr_rev_step(3) by auto
      next
        case False
        then show ?thesis 
          by (metis Recv event.distinct(17) event.inject(3) m_in_set message_must_be_delivered_2 tr_rev_step.hyps(3))
      qed
    qed
  qed
  then have "m : set (msgs c' i)" using assms ‹?P› by auto
  then show False using assms by simp
qed

lemma marker_must_be_delivered_2_trace:
  assumes
    "trace c t c'" and
    "Marker : set (msgs c i)" and
    "Marker ∉ set (msgs c' i)" and
    "channel i = Some (p, q)"
  shows
    "∃ev ∈ set t. (∃p q. ev = RecvMarker i p q)"
proof -
  show "∃ev ∈ set t. (∃p q. ev = RecvMarker i p q)"
    using assms message_must_be_delivered_2_trace by fast
qed

lemma snapshot_stable:
  shows
    "[ trace c t c';
       has_snapshotted c p
     ] ==> has_snapshotted c' p"
proof (induct c t c' rule:trace_rev_induct)
  case (tr_rev_init c)
  then show ?case by blast
next
  case (tr_rev_step c t c' ev c'')
  then show ?case
  proof (cases ev)
    case (Snapshot q)
    then have "p ≠ q" using tr_rev_step next_snapshot can_occur_def by auto
    then show ?thesis using Snapshot tr_rev_step by auto
  next
    case (RecvMarker i q r)
    with tr_rev_step show ?thesis
      by (cases "p = q"; auto)
  qed simp_all
qed

lemma snapshot_stable_2:
  shows
    "trace c t c' ==> ~ has_snapshotted c' p ==> ~ has_snapshotted c p"
  using snapshot_stable by blast

lemma no_markers_if_all_snapshotted:
  shows
    "[ trace c t c';
      ∀p. has_snapshotted c p;
      Marker ∉ set (msgs c i)
     ] ==> Marker ∉ set (msgs c' i)"
proof (induct c t c' rule:trace_rev_induct)
  case (tr_rev_init c)
  then show ?case by simp
next
  case (tr_rev_step c t c' ev c'')
  have all_snapshotted: "∀p. has_snapshotted c' p" using snapshot_stable tr_rev_step by auto
  have no_marker: "Marker ∉ set (msgs c' i)" using tr_rev_step by blast
  then show ?case
  proof (cases ev)
    case (Snapshot r)
    then show ?thesis using can_occur_def tr_rev_step all_snapshotted by auto
  next
    case (RecvMarker i' r s)
    have "i' ≠ i"
    proof (rule ccontr)
      assume "~ i' ≠ i"
      then have "Marker : set (msgs c i)"
        using can_occur_def RecvMarker tr_rev_step  RecvMarker_implies_Marker_in_set by blast
      then show False using tr_rev_step by simp
    qed
    then show ?thesis using tr_rev_step all_snapshotted no_marker RecvMarker by auto
  next
    case (Trans p s s')
    then show ?thesis using tr_rev_step no_marker by auto
  next
   case (Send i' r s u u' m)
   then show ?thesis
   proof (cases "i' = i")
     case True
     then have "msgs c'' i = msgs c' i @ [Msg m]" using tr_rev_step Send by auto
     then show ?thesis using no_marker by auto
   next
     case False
     then show ?thesis using Send tr_rev_step no_marker by auto
   qed
  next
    case (Recv i' r s u u' m)
    then show ?thesis
    proof (cases "i = i'")
      case True
      then have "msgs c'' i = tl (msgs c' i)" using tr_rev_step Recv by auto
      then show ?thesis using no_marker by (metis list.sel(2) list.set_sel(2))
    next
      case False
      then show ?thesis using Recv tr_rev_step no_marker by auto
    qed
  qed
qed

lemma event_stays_valid_if_no_occurrence_trace:
  shows
    "[ trace c t c';
       list_all (λev. occurs_on ev ≠ occurs_on ev') t;
       can_occur ev' c
     ] ==> can_occur ev' c'"
proof (induct c t c' rule:trace_rev_induct)
  case tr_rev_init
  then show ?case by blast
next
  case tr_rev_step
  then show ?case using event_stays_valid_if_no_occurrence by auto
qed

lemma event_can_go_back_if_no_sender_trace:
  shows
    "[ trace c t c';
       list_all (λev. occurs_on ev ≠ occurs_on ev') t;
       can_occur ev' c';
       ~ isRecvMarker ev';
       list_all (λev. ~ isSend ev) t
     ] ==> can_occur ev' c"
proof (induct c t c' rule:trace_rev_induct)
  case tr_rev_init
  then show ?case by blast
next
  case tr_rev_step
  then show ?case using event_can_go_back_if_no_sender by auto
qed

lemma done_only_from_recv_marker_trace:
  assumes
    "trace c t c'" and
    "t ≠ []" and
    "snd (cs c cid) ≠ Done" and
    "snd (cs c' cid) = Done" and
    "channel cid = Some (p, q)"
  shows
    "RecvMarker cid q p ∈ set t"
proof (rule ccontr)
  assume "~ RecvMarker cid q p ∈ set t"
  moreover have "[ trace c t c'; ~ RecvMarker cid q p ∈ set t; snd (cs c cid) ≠ Done; channel cid = Some (p, q) ]
                 ==> snd (cs c' cid) ≠ Done"
  proof (induct t arbitrary: c' rule:rev_induct)
    case Nil
    then show ?case 
      by (metis list.discI trace.simps)
  next
    case (snoc ev t)
    then obtain d where ind: "trace c t d" and step: "d ⊨ ev ↦ c'" 
      using trace_decomp_tail by blast
    then have "snd (cs d cid) ≠ Done"
    proof -
      have "~ RecvMarker cid q p ∈ set t" 
        using snoc.prems(2) by auto
      then show ?thesis using snoc ind by blast
    qed
    then show ?case 
      using done_only_from_recv_marker local.step snoc.prems(2) snoc.prems(4) by auto
  qed
  ultimately have "snd (cs c' cid) ≠ Done" using assms by blast
  then show False using assms by simp
qed

lemma cs_not_not_started_stable_trace:
  shows
    "[ trace c t c'; snd (cs c cid) ≠ NotStarted; channel cid = Some (p, q) ] ==> snd (cs c' cid) ≠ NotStarted"
proof (induct t arbitrary:c' rule:rev_induct)
  case Nil
  then show ?case 
    by (metis list.discI trace.simps)
next
  case (snoc ev t)
  then obtain d where tr: "trace c t d" and step: "d ⊨ ev ↦ c'" 
    using trace_decomp_tail by blast
  then have "snd (cs d cid) ≠ NotStarted" using snoc by blast
  then show ?case using cs_not_not_started_stable snoc step by blast
qed

lemma no_messages_introduced_if_no_channel:
  assumes
    trace: "trace init t final" and
    no_msgs_if_no_channel: "∀i. channel i = None ⟶ msgs init i = []"
  shows
    "channel cid = None ==> msgs (s init t i) cid = []"
proof (induct i)
  case 0
  then show ?case
    by (metis assms exists_trace_for_any_i no_msgs_if_no_channel take0 tr_init trace_and_start_determines_end)
next
  case (Suc n)
  have f: "trace (s init t n) (take ((Suc n) - n) (drop n t)) (s init t (Suc n))"
    using exists_trace_for_any_i_j order_le_less trace assms by blast
  then show ?case
  proof (cases "drop n t = Nil")
    case True
    then show ?thesis using Suc.hyps Suc.prems
      by (metis f tr_init trace_and_start_determines_end take_Nil) 
  next
    case False
    have suc_n_minus_n: "Suc n - n = 1" by auto
    then have "length (take ((Suc n) - n) (drop n t)) = 1" using False by auto
    then obtain ev where "ev # Nil = take ((Suc n) - n) (drop n t)"
      by (metis False One_nat_def suc_n_minus_n length_greater_0_conv self_append_conv2 take_eq_Nil take_hd_drop)
    then have g: "(s init t n) ⊨ ev ↦ (s init t (Suc n))"
      by (metis f tr_init trace_and_start_determines_end trace_decomp_head)
    then show ?thesis
    proof (cases ev)
      case (Snapshot r)
      then show ?thesis 
        using Suc.hyps Suc.prems g by auto
    next
      case (RecvMarker cid' sr r)
      have "cid' ≠ cid" using RecvMarker can_occur_def g Suc by auto
      with RecvMarker Suc g show ?thesis by (cases "has_snapshotted (s init t n) sr", auto)
    next
      case (Trans r u u')
      then show ?thesis
        by (metis Suc.hyps Suc.prems g next_trans)
    next
      case (Send cid' r s u u' m)
      have "cid' ≠ cid" using Send can_occur_def g Suc by auto
      then show ?thesis using Suc g Send by simp
    next
      case (Recv cid' s r u u' m)
      have "cid' ≠ cid" using Recv can_occur_def g Suc by auto
      then show ?thesis using Suc g Recv by simp
    qed
  qed
qed

end (* context distributed_system *)

end (* theory Trace *)