Theory Snapshot
section ‹The Chandy--Lamport algorithm›
theory Snapshot
imports
"HOL-Library.Sublist"
Distributed_System
Trace
Util
Swap
begin
subsection ‹The computation locale›
text ‹We extend the distributed system locale presented
earlier: Now we are given a trace t of the distributed system between
two configurations, the initial and final configuartions of t. Our objective
is to show that the Chandy--Lamport algorithm terminated successfully and
exhibits the same properties as claimed in~\<^cite>‹"chandy"›. In the initial state
no snapshotting must have taken place yet, however the computation itself may
have progressed arbitrarily far already.
We assume that there exists at least one process, that the
total number of processes in the system is finite, and that there
are only finitely many channels between the processes. The process graph
is strongly connected. Finally there are Chandy and Lamport's core assumptions:
every process snapshots at some time and no marker may remain in a channel forever.›
locale computation = distributed_system +
fixes
init final :: "('a, 'b, 'c) configuration"
assumes
finite_channels:
"finite {i. ∃p q. channel i = Some (p, q)}" and
strongly_connected_raw:
"∀p q. (p ≠ q) ⟶
(tranclp (λp q. (∃i. channel i = Some (p, q)))) p q" and
at_least_two_processes:
"card (UNIV :: 'a set) > 1" and
finite_processes:
"finite (UNIV :: 'a set)" and
no_initial_Marker:
"∀i. (∃p q. channel i = Some (p, q))
⟶ Marker ∉ set (msgs init i)" and
no_msgs_if_no_channel:
"∀i. channel i = None ⟶ msgs init i = []" and
no_initial_process_snapshot:
"∀p. ~ has_snapshotted init p" and
no_initial_channel_snapshot:
"∀i. channel_snapshot init i = ([], NotStarted)" and
valid: "∃t. trace init t final" and
l1: "∀t i cid. trace init t final
∧ Marker ∈ set (msgs (s init t i) cid)
⟶ (∃j. j ≥ i ∧ Marker ∉ set (msgs (s init t j) cid))" and
l2: "∀t p. trace init t final
⟶ (∃i. has_snapshotted (s init t i) p ∧ i ≤ length t)"
begin
definition has_channel where
"has_channel p q ⟷ (∃i. channel i = Some (p, q))"
lemmas strongly_connected = strongly_connected_raw[folded has_channel_def]
lemma exists_some_channel:
shows "∃i p q. channel i = Some (p, q)"
proof -
obtain p q where "p : (UNIV :: 'a set) ∧ q : (UNIV :: 'a set) ∧ p ≠ q"
by (metis (mono_tags) One_nat_def UNIV_eq_I all_not_in_conv at_least_two_processes card_Suc_Diff1 card.empty finite_processes insert_iff iso_tuple_UNIV_I less_numeral_extra(4) n_not_Suc_n)
then have "(tranclp has_channel) p q" using strongly_connected by simp
then obtain r s where "has_channel r s"
by (meson tranclpD)
then show ?thesis using has_channel_def by auto
qed
abbreviation S where
"S ≡ s init"
lemma no_messages_if_no_channel:
assumes "trace init t final"
shows "channel cid = None ⟹ msgs (s init t i) cid = []"
using no_messages_introduced_if_no_channel[OF assms no_msgs_if_no_channel] by blast
lemma S_induct [consumes 3, case_names S_init S_step]:
"⟦ trace init t final; i ≤ j; j ≤ length t;
⋀i. P i i;
⋀i j. i < j ⟹ j ≤ length t ⟹ (S t i) ⊢ (t ! i) ↦ (S t (Suc i)) ⟹ P (Suc i) j ⟹ P i j
⟧ ⟹ P i j"
proof (induct "j - i" arbitrary: i)
case 0
then show ?case by simp
next
case (Suc n)
then have "(S t i) ⊢ (t ! i) ↦ (S t (Suc i))" using Suc step_Suc by simp
then show ?case using Suc by simp
qed
lemma exists_index:
assumes
"trace init t final" and
"ev ∈ set (take (j - i) (drop i t))"
shows
"∃k. i ≤ k ∧ k < j ∧ ev = t ! k"
proof -
have "trace (S t i) (take (j - i) (drop i t)) (S t j)"
by (metis assms(1) assms(2) diff_is_0_eq' exists_trace_for_any_i_j list.distinct(1) list.set_cases nat_le_linear take_eq_Nil)
obtain l where "ev = (take (j - i) (drop i t)) ! l" "l < length (take (j - i) (drop i t))"
by (metis assms(2) in_set_conv_nth)
let ?k = "l + i"
have "(take (j - i) (drop i t)) ! l = drop i t ! l"
using ‹l < length (take (j - i) (drop i t))› by auto
also have "... = t ! ?k"
by (metis add.commute assms(2) drop_all empty_iff list.set(1) nat_le_linear nth_drop take_Nil)
finally have "ev = t ! ?k"
using ‹ev = take (j - i) (drop i t) ! l› by blast
moreover have "i ≤ ?k ∧ ?k < j"
using ‹l < length (take (j - i) (drop i t))› by auto
ultimately show ?thesis by blast
qed
lemma no_change_if_ge_length_t:
assumes
"trace init t final" and
"i ≥ length t" and
"j ≥ i"
shows
"S t i = S t j"
proof -
have "trace (S t i) (take (j - i) (drop i t)) (S t j)"
using assms(1) assms(3) exists_trace_for_any_i_j by blast
moreover have "(take (j - i) (drop i t)) = Nil"
by (simp add: assms(2))
ultimately show ?thesis
by (metis tr_init trace_and_start_determines_end)
qed
lemma no_marker_if_no_snapshot:
shows
"⟦ trace init t final; channel cid = Some (p, q);
~ has_snapshotted (S t i) p ⟧
⟹ Marker ∉ set (msgs (S t i) cid)"
proof (induct i)
case 0
then show ?case
by (metis exists_trace_for_any_i no_initial_Marker take_eq_Nil tr_init trace_and_start_determines_end)
next
case (Suc n)
then have IH: "Marker ∉ set (msgs (S t n) cid)"
by (meson distributed_system.exists_trace_for_any_i_j distributed_system.snapshot_stable_2 distributed_system_axioms eq_iff le_Suc_eq)
then obtain tr where decomp: "trace (S t n) tr (S t (Suc n))" "tr = take (Suc n - n) (drop n t)"
using Suc exists_trace_for_any_i_j le_Suc_eq by blast
have "Marker ∉ set (msgs (S t (Suc n)) cid)"
proof (cases "tr = []")
case True
then show ?thesis
by (metis IH decomp(1) tr_init trace_and_start_determines_end)
next
case False
then obtain ev where step: "tr = [ev]" "(S t n) ⊢ ev ↦ (S t (Suc n))"
by (metis One_nat_def Suc_eq_plus1 Suc_leI ‹tr = take (Suc n - n) (drop n t)› ‹trace (S t n) tr (S t (Suc n))› add_diff_cancel_left' append.simps(1) butlast_take cancel_comm_monoid_add_class.diff_cancel length_greater_0_conv list.distinct(1) list.sel(3) snoc_eq_iff_butlast take0 take_Nil trace.cases)
then show ?thesis
proof (cases ev)
case (Snapshot p')
then show ?thesis
by (metis IH Suc.prems(2) Suc.prems(3) local.step(2) new_Marker_in_set_implies_nonregular_occurence new_msg_in_set_implies_occurrence nonregular_event_induces_snapshot snapshot_state_unchanged)
next
case (RecvMarker cid' p' q')
have "p' ≠ p"
proof (rule ccontr)
assume asm: "~ p' ≠ p"
then have "has_snapshotted (S t (Suc n)) p"
proof -
have "~ regular_event ev" using RecvMarker by auto
moreover have "occurs_on ev = p" using asm RecvMarker by auto
ultimately show ?thesis using step(2) Suc.hyps Suc.prems
by (metis nonregular_event_induces_snapshot snapshot_state_unchanged)
qed
then show False using Suc.prems by blast
qed
moreover have "cid ≠ cid'"
proof (rule ccontr)
assume "~ cid ≠ cid'"
then have "hd (msgs (S t n) cid) = Marker ∧ length (msgs (S t n) cid) > 0"
using step RecvMarker can_occur_def by auto
then have "Marker : set (msgs (S t n) cid)"
using list.set_sel(1) by fastforce
then show False using IH by simp
qed
ultimately have "msgs (S t (Suc n)) cid = msgs (S t n) cid"
proof -
have "∄r. channel cid = Some (p', r)"
using Suc.prems(2) ‹p' ≠ p› by auto
with ‹cid ≠ cid'› RecvMarker step show ?thesis by (cases "has_snapshotted (S t n) p'", auto)
qed
then show ?thesis by (simp add: IH)
next
case (Trans p' s s')
then show ?thesis
using IH local.step(2) by force
next
case (Send cid' p' q' s s' m)
with step IH show ?thesis by (cases "cid' = cid", auto)
next
case (Recv cid' p' q' s s' m)
with step IH show ?thesis by (cases "cid' = cid", auto)
qed
qed
then show ?case by blast
qed
subsection ‹Termination›
text ‹We prove that the snapshot algorithm terminates, as exhibited
by lemma \texttt{snapshot\_algorithm\_must\_terminate}. In the final configuration all
processes have snapshotted, and no markers remain in the channels.›
lemma must_exist_snapshot:
assumes
"trace init t final"
shows
"∃p i. Snapshot p = t ! i"
proof (rule ccontr)
assume "∄p i. Snapshot p = t ! i"
have "∀i p. ~ has_snapshotted (S t i) p"
proof (rule allI)
fix i
show "∀p. ~ has_snapshotted (S t i) p"
proof (induct i)
case 0
then show ?case
by (metis assms distributed_system.trace_and_start_determines_end distributed_system_axioms exists_trace_for_any_i computation.no_initial_process_snapshot computation_axioms take0 tr_init)
next
case (Suc n)
then have IH: "∀p. ~ has_snapshotted (S t n) p" by auto
then obtain tr where "trace (S t n) tr (S t (Suc n))" "tr = take (Suc n - n) (drop n t)"
using assms exists_trace_for_any_i_j le_Suc_eq by blast
show "∀p. ~ has_snapshotted (S t (Suc n)) p"
proof (cases "tr = []")
case True
then show ?thesis
by (metis IH ‹trace (S t n) tr (S t (Suc n))› tr_init trace_and_start_determines_end)
next
case False
then obtain ev where step: "tr = [ev]" "(S t n) ⊢ ev ↦ (S t (Suc n))"
by (metis One_nat_def Suc_eq_plus1 Suc_leI ‹tr = take (Suc n - n) (drop n t)› ‹trace (S t n) tr (S t (Suc n))› add_diff_cancel_left' append.simps(1) butlast_take cancel_comm_monoid_add_class.diff_cancel length_greater_0_conv list.distinct(1) list.sel(3) snoc_eq_iff_butlast take0 take_Nil trace.cases)
then show ?thesis
using step Suc.hyps proof (cases ev)
case (Snapshot q)
then show ?thesis
by (metis ‹∄p i. Snapshot p = t ! i› ‹tr = [ev]› ‹tr = take (Suc n - n) (drop n t)› append_Cons append_take_drop_id nth_append_length)
next
case (RecvMarker cid' q r)
then have m: "Marker ∈ set (msgs (S t n) cid')"
using RecvMarker_implies_Marker_in_set step by blast
have "~ has_snapshotted (S t n) q" using Suc by auto
then have "Marker ∉ set (msgs (S t n) cid')"
proof -
have "channel cid' = Some (r, q)" using step can_occur_def RecvMarker by auto
then show ?thesis
using IH assms no_marker_if_no_snapshot by blast
qed
then show ?thesis using m by auto
qed auto
qed
qed
qed
obtain j p where "has_snapshotted (S t j) p" using l2 assms by blast
then show False
using ‹∀i p. ¬ has_snapshotted (S t i) p› by blast
qed
lemma recv_marker_means_snapshotted:
assumes
"trace init t final" and
"ev = RecvMarker cid p q" and
"(S t i) ⊢ ev ↦ (S t (Suc i))"
shows
"has_snapshotted (S t i) q"
proof -
have "Marker = hd (msgs (S t i) cid) ∧ length (msgs (S t i) cid) > 0"
proof -
have "Marker # msgs (S t (Suc i)) cid = msgs (S t i) cid"
using assms(2) assms(3) next_recv_marker by blast
then show ?thesis
by (metis length_greater_0_conv list.discI list.sel(1))
qed
then have "Marker ∈ set (msgs (S t i) cid)"
using hd_in_set by fastforce
then show "has_snapshotted (S t i) q"
proof -
have "channel cid = Some (q, p)" using assms can_occur_def by auto
then show ?thesis
using ‹Marker ∈ set (msgs (S t i) cid)› assms(1) no_marker_if_no_snapshot by blast
qed
qed
lemma recv_marker_means_cs_Done:
assumes
"trace init t final" and
"t ! i = RecvMarker cid p q" and
"i < length t"
shows
"snd (cs (S t (i+1)) cid) = Done"
proof -
have "(S t i) ⊢ (t ! i) ↦ (S t (i+1))"
using assms(1) assms(3) step_Suc by auto
then show ?thesis
by (simp add: assms(2))
qed
lemma snapshot_produces_marker:
assumes
"trace init t final" and
"~ has_snapshotted (S t i) p" and
"has_snapshotted (S t (Suc i)) p" and
"channel cid = Some (p, q)"
shows
"Marker : set (msgs (S t (Suc i)) cid) ∨ has_snapshotted (S t i) q"
proof -
obtain ev where ex_ev: "(S t i) ⊢ ev ↦ (S t (Suc i))"
by (metis append_Nil2 append_take_drop_id assms(1) assms(2) assms(3) distributed_system.step_Suc distributed_system_axioms drop_eq_Nil less_Suc_eq_le nat_le_linear not_less_eq s_def)
then have "occurs_on ev = p"
using assms(2) assms(3) no_state_change_if_no_event by force
then show ?thesis
using assms ex_ev proof (cases ev)
case (Snapshot r)
then have "Marker ∈ set (msgs (S t (Suc i)) cid)"
using ex_ev assms(2) assms(3) assms(4) by fastforce
then show ?thesis by simp
next
case (RecvMarker cid' r s)
have "r = p" using ‹occurs_on ev = p›
by (simp add: RecvMarker)
then show ?thesis
proof (cases "cid = cid'")
case True
then have "has_snapshotted (S t i) q"
using RecvMarker RecvMarker_implies_Marker_in_set assms(1) assms(2) assms(4) ex_ev no_marker_if_no_snapshot by blast
then show ?thesis by simp
next
case False
then have "∃s. channel cid = Some (r, s)" using RecvMarker assms can_occur_def ‹r = p› by simp
then have "msgs (S t (Suc i)) cid = msgs (S t i) cid @ [Marker]"
using RecvMarker assms ex_ev ‹r = p› False by simp
then show ?thesis by simp
qed
qed auto
qed
lemma exists_snapshot_for_all_p:
assumes
"trace init t final"
shows
"∃i. ~ has_snapshotted (S t i) p ∧ has_snapshotted (S t (Suc i)) p" (is ?Q)
proof -
obtain i where "has_snapshotted (S t i) p" using l2 assms by blast
let ?j = "LEAST j. has_snapshotted (S t j) p"
have "?j ≠ 0"
proof -
have "~ has_snapshotted (S t 0) p"
by (metis exists_trace_for_any_i list.discI no_initial_process_snapshot s_def take_eq_Nil trace.simps)
then show ?thesis
by (metis (mono_tags, lifting) ‹has_snapshotted (S t i) p› wellorder_Least_lemma(1))
qed
have "?j ≤ i"
by (meson Least_le ‹has_snapshotted (S t i) p›)
have "¬ has_snapshotted (S t (?j - 1)) p" (is ?P)
proof (rule ccontr)
assume "¬ ?P"
then have "has_snapshotted (S t (?j - 1)) p" by simp
then have "∃j. j < ?j ∧ has_snapshotted (S t j) p"
by (metis One_nat_def ‹(LEAST j. ps (S t j) p ≠ None) ≠ 0› diff_less lessI not_gr_zero)
then show False
using not_less_Least by blast
qed
show ?thesis
proof (rule ccontr)
assume "¬ ?Q"
have "∀i. ¬ has_snapshotted (S t i) p"
proof (rule allI)
fix i'
show "¬ has_snapshotted (S t i') p"
proof (induct i')
case 0
then show ?case
using ‹(LEAST j. ps (S t j) p ≠ None) ≠ 0› by force
next
case (Suc i'')
then show ?case
using ‹∄i. ¬ ps (S t i) p ≠ None ∧ ps (S t (Suc i)) p ≠ None› by blast
qed
qed
then show False
using ‹ps (S t i) p ≠ None› by blast
qed
qed
lemma all_processes_snapshotted_in_final_state:
assumes
"trace init t final"
shows
"has_snapshotted final p"
proof -
obtain i where "has_snapshotted (S t i) p ∧ i ≤ length t"
using assms l2 by blast
moreover have "final = (S t (length t))"
by (metis (no_types, lifting) assms exists_trace_for_any_i le_Suc_eq length_Cons take_Nil take_all trace.simps trace_and_start_determines_end)
ultimately show ?thesis
using assms exists_trace_for_any_i_j snapshot_stable by blast
qed
definition next_marker_free_state where
"next_marker_free_state t i cid = (LEAST j. j ≥ i ∧ Marker ∉ set (msgs (S t j) cid))"
lemma exists_next_marker_free_state:
assumes
"channel cid = Some (p, q)"
"trace init t final"
shows
"∃!j. next_marker_free_state t i cid = j ∧ j ≥ i ∧ Marker ∉ set (msgs (S t j) cid)"
proof (cases "Marker ∈ set (msgs (S t i) cid)")
case False
then have "next_marker_free_state t i cid = i" unfolding next_marker_free_state_def
by (metis (no_types, lifting) Least_equality order_refl)
then show ?thesis using False assms by blast
next
case True
then obtain j where "j ≥ i" "Marker ∉ set (msgs (S t j) cid)" using l1 assms by blast
then show ?thesis
by (metis (no_types, lifting) LeastI_ex next_marker_free_state_def)
qed
theorem snapshot_algorithm_must_terminate:
assumes
"trace init t final"
shows
"∃phi. ((∀p. has_snapshotted (S t phi) p)
∧ (∀cid. Marker ∉ set (msgs (S t phi) cid)))"
proof -
let ?i = "{i. i ≤ length t ∧ (∀p. has_snapshotted (S t i) p)}"
have fin_i: "finite ?i" by auto
moreover have "?i ≠ empty"
proof -
have "∀p. has_snapshotted (S t (length t)) p"
by (meson assms exists_trace_for_any_i_j l2 snapshot_stable_2)
then show ?thesis by blast
qed
then obtain i where asm: "∀p. has_snapshotted (S t i) p" by blast
have f: "∀j. j ≥ i ⟶ (∀p. has_snapshotted (S t j) p)"
using snapshot_stable asm exists_trace_for_any_i_j valid assms by blast
let ?s = "(λcid. (next_marker_free_state t i cid)) ` { cid. channel cid ≠ None }"
have "?s ≠ empty" using exists_some_channel by auto
have fin_s: "finite ?s" using finite_channels by simp
let ?phi = "Max ?s"
have "?phi ≥ i"
proof (rule ccontr)
assume asm: "¬ ?phi ≥ i"
obtain cid p q where g: "channel cid = Some (p, q)" using exists_some_channel by auto
then have "next_marker_free_state t i cid ≥ i" using exists_next_marker_free_state assms by blast
then have "Max ?s ≥ i" using Max_ge_iff g fin_s by fast
then show False using asm by simp
qed
then have "⋀cid. Marker ∉ set (msgs (S t ?phi) cid)"
proof -
fix cid
show "Marker ∉ set (msgs (S t ?phi) cid)"
proof (cases "Marker : set (msgs (S t i) cid)")
case False
then show ?thesis
using ‹i ≤ Max ?s› asm assms exists_trace_for_any_i_j no_markers_if_all_snapshotted by blast
next
case True
then have cpq: "channel cid ≠ None" using no_messages_if_no_channel assms by fastforce
then obtain p q where chan: "channel cid = Some (p, q)" by auto
then obtain j where i: "j = next_marker_free_state t i cid" "Marker ∉ set (msgs (S t j) cid)"
using exists_next_marker_free_state assms by fast
have "j ≤ ?phi" using cpq fin_s i(1) pair_imageI by simp
then show "Marker ∉ set (msgs (S t ?phi) cid)"
proof -
have "trace (S t j) (take (?phi - j) (drop j t)) (S t ?phi)"
using ‹j ≤ ?phi› assms exists_trace_for_any_i_j by blast
moreover have "∀p. has_snapshotted (S t j) p"
by (metis assms chan f computation.exists_next_marker_free_state computation_axioms i(1))
ultimately show ?thesis
using i(2) no_markers_if_all_snapshotted by blast
qed
qed
qed
thus ?thesis using f ‹?phi ≥ i› by blast
qed
subsection ‹Correctness›
text ‹The greatest part of this work is spent on the correctness
of the Chandy-Lamport algorithm. We prove that the snapshot is
consistent, i.e.\ there exists a permutation $t'$ of the trace $t$ and an intermediate
configuration $c'$ of $t'$ such that the configuration recorded in the snapshot
corresponds to the snapshot taken during execution of $t$, which is given as Theorem 1
in~\<^cite>‹"chandy"›.›
lemma snapshot_stable_ver_2:
shows "trace init t final ⟹ has_snapshotted (S t i) p ⟹ j ≥ i ⟹ has_snapshotted (S t j) p"
using exists_trace_for_any_i_j snapshot_stable by blast
lemma snapshot_stable_ver_3:
shows "trace init t final ⟹ ~ has_snapshotted (S t i) p ⟹ i ≥ j ⟹ ~ has_snapshotted (S t j) p"
using snapshot_stable_ver_2 by blast
lemma marker_must_stay_if_no_snapshot:
assumes
"trace init t final" and
"has_snapshotted (S t i) p" and
"~ has_snapshotted (S t i) q" and
"channel cid = Some (p, q)"
shows
"Marker : set (msgs (S t i) cid)"
proof -
obtain j where "~ has_snapshotted (S t j) p ∧ has_snapshotted (S t (Suc j)) p"
using exists_snapshot_for_all_p assms by blast
have "j ≤ i"
proof (rule ccontr)
assume asm: "~ j ≤ i"
then have "~ has_snapshotted (S t i) p"
using ‹¬ has_snapshotted (S t j) p ∧ has_snapshotted (S t (Suc j)) p› assms(1) less_imp_le_nat snapshot_stable_ver_3
by (meson nat_le_linear)
then show False using assms(2) by simp
qed
have "i ≤ length t"
proof (rule ccontr)
assume "~ i ≤ length t"
then have "i > length t"
using not_less by blast
obtain i' where a: "∀p. has_snapshotted (S t i') p" using assms snapshot_algorithm_must_terminate by blast
have "i' ≥ i"
using ‹∀p. has_snapshotted (S t i') p› assms(1) assms(3) nat_le_linear snapshot_stable_ver_3 by blast
have "(S t i') ≠ (S t i)" using assms a by force
then have "i ≤ length t"
using ‹i ≤ i'› assms(1) computation.no_change_if_ge_length_t computation_axioms nat_le_linear by fastforce
then show False using ‹~ i ≤ length t› by simp
qed
have marker_in_set: "Marker : set (msgs (S t (Suc j)) cid)"
using ‹¬ has_snapshotted (S t j) p ∧ has_snapshotted (S t (Suc j)) p› ‹j ≤ i› assms(1) assms(3) assms(4) snapshot_produces_marker snapshot_stable_ver_3 by blast
show ?thesis
proof (rule ccontr)
assume asm: "Marker ∉ set (msgs (S t i) cid)"
then have range: "(Suc j) < i"
by (metis Suc_lessI ‹¬ ps (S t j) p ≠ None ∧ ps (S t (Suc j)) p ≠ None› ‹j ≤ i› assms(2) marker_in_set order.order_iff_strict)
let ?k = "LEAST k. k ≥ (Suc j) ∧ Marker ∉ set (msgs (S t k) cid)"
have range_k: "(Suc j) < ?k ∧ ?k ≤ i"
proof -
have "j < (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid))"
by (metis (full_types) Suc_le_eq assms(1) assms(4) exists_next_marker_free_state next_marker_free_state_def)
then show ?thesis
proof -
assume a1: "j < (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid))"
have "j < i"
using local.range by linarith
then have "(Suc j ≤ i ∧ Marker ∉ set (msgs (S t i) cid)) ∧ (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) ≠ Suc j"
by (metis (lifting) Suc_leI asm marker_in_set wellorder_Least_lemma(1))
then show ?thesis
using a1 by (simp add: wellorder_Least_lemma(2))
qed
qed
have a: "Marker : set (msgs (S t (?k-1)) cid)"
proof -
obtain nn :: "nat ⇒ nat ⇒ nat" where
"∀x0 x1. (∃v2. x0 = Suc (x1 + v2)) = (x0 = Suc (x1 + nn x0 x1))"
by moura
then have f1: "(LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) = Suc (Suc j + nn (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) (Suc j))"
using ‹Suc j < (LEAST k. Suc j ≤ k ∧ Marker ∉ set (msgs (S t k) cid)) ∧ (LEAST k. Suc j ≤ k ∧ Marker ∉ set (msgs (S t k) cid)) ≤ i› less_iff_Suc_add by fastforce
have f2: "Suc j ≤ Suc j + nn (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) (Suc j)"
by simp
have f3: "∀p n. ¬ p (n::nat) ∨ Least p ≤ n"
by (meson wellorder_Least_lemma(2))
have "¬ (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) ≤ Suc j + nn (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) (Suc j)"
using f1 by linarith
then have f4: "¬ (Suc j ≤ Suc j + nn (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) (Suc j) ∧ Marker ∉ set (msgs (S t (Suc j + nn (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) (Suc j))) cid))"
using f3 by force
have "Suc j + nn (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) (Suc j) = (LEAST n. Suc j ≤ n ∧ Marker ∉ set (msgs (S t n) cid)) - 1"
using f1 by linarith
then show ?thesis
using f4 f2 by presburger
qed
have b: "Marker ∉ set (msgs (S t ?k) cid)"
using assms(1) assms(4) exists_next_marker_free_state next_marker_free_state_def by fastforce
have "?k - 1 < i" using range_k by auto
then obtain ev where step: "(S t (?k-1)) ⊢ ev ↦ (S t (Suc (?k-1)))"
by (meson Suc_le_eq ‹i ≤ length t› assms(1) le_trans step_Suc)
then show False
using a assms(1) assms(3) assms(4) b computation.snapshot_stable_ver_3 computation_axioms less_iff_Suc_add range_k recv_marker_means_snapshotted_2 by fastforce
qed
qed
subsubsection ‹Pre- and postrecording events›
definition prerecording_event:
"prerecording_event t i ≡
i < length t ∧ regular_event (t ! i)
∧ ~ has_snapshotted (S t i) (occurs_on (t ! i))"
definition postrecording_event:
"postrecording_event t i ≡
i < length t ∧ regular_event (t ! i)
∧ has_snapshotted (S t i) (occurs_on (t ! i))"
abbreviation neighboring where
"neighboring t i j ≡ i < j ∧ j < length t ∧ regular_event (t ! i) ∧ regular_event (t ! j)
∧ (∀k. i < k ∧ k < j ⟶ ~ regular_event (t ! k))"
lemma pre_if_regular_and_not_post:
assumes
"regular_event (t ! i)" and
"~ postrecording_event t i" and
"i < length t"
shows
"prerecording_event t i"
using assms computation.postrecording_event computation_axioms prerecording_event by metis
lemma post_if_regular_and_not_pre:
assumes
"regular_event (t ! i)" and
"~ prerecording_event t i" and
"i < length t"
shows
"postrecording_event t i"
using assms computation.postrecording_event computation_axioms prerecording_event by metis
lemma post_before_pre_different_processes:
assumes
"i < j" and
"j < length t" and
neighboring: "∀k. (i < k ∧ k < j) ⟶ ~ regular_event (t ! k)" and
post_ei: "postrecording_event t i" and
pre_ej: "prerecording_event t j" and
valid: "trace init t final"
shows
"occurs_on (t ! i) ≠ occurs_on (t ! j)"
proof -
let ?p = "occurs_on (t ! i)"
let ?q = "occurs_on (t ! j)"
have sp: "has_snapshotted (S t i) ?p"
using assms postrecording_event prerecording_event by blast
have nsq: "~ has_snapshotted (S t j) ?q"
using assms postrecording_event prerecording_event by blast
show "?p ≠ ?q"
proof -
have "~ has_snapshotted (S t i) ?q"
proof (rule ccontr)
assume sq: "~ ~ has_snapshotted (S t i) ?q"
from ‹i < j› have "i ≤ j" using less_imp_le by blast
then obtain tr where ex_trace: "trace (S t i) tr (S t j)"
using exists_trace_for_any_i_j valid by blast
then have "has_snapshotted (S t j) ?q" using ex_trace snapshot_stable sq by blast
then show False using nsq by simp
qed
then show ?thesis using sp by auto
qed
qed
lemma post_before_pre_neighbors:
assumes
"i < j" and
"j < length t" and
neighboring: "∀k. (i < k ∧ k < j) ⟶ ~ regular_event (t ! k)" and
post_ei: "postrecording_event t i" and
pre_ej: "prerecording_event t j" and
valid: "trace init t final"
shows
"Ball (set (take (j - (i+1)) (drop (i+1) t))) (%ev. ~ regular_event ev ∧ ~ occurs_on ev = occurs_on (t ! j))"
proof -
let ?p = "occurs_on (t ! i)"
let ?q = "occurs_on (t ! j)"
let ?between = "take (j - (i+1)) (drop (i+1) t)"
show ?thesis
proof (unfold Ball_def, rule allI, rule impI)
fix ev
assume "ev : set ?between"
have len_nr: "length ?between = (j - (i+1))" using assms(2) by auto
then obtain l where "?between ! l = ev" and range_l: "0 ≤ l ∧ l < (j - (i+1))"
by (metis ‹ev ∈ set (take (j - (i + 1)) (drop (i + 1) t))› gr_zeroI in_set_conv_nth le_numeral_extra(3) less_le)
let ?k = "l + (i+1)"
have "?between ! l = (t ! ?k)"
proof -
have "j < length t"
by (metis assms(2))
then show ?thesis
by (metis (no_types) Suc_eq_plus1 Suc_leI add.commute assms(1) drop_take length_take less_diff_conv less_imp_le_nat min.absorb2 nth_drop nth_take range_l)
qed
have "~ regular_event ev"
by (metis (no_types, lifting) assms(3) range_l One_nat_def Suc_eq_plus1 ‹take (j - (i + 1)) (drop (i + 1) t) ! l = ev› ‹take (j - (i + 1)) (drop (i + 1) t) ! l = t ! (l + (i + 1))› add.left_commute add_lessD1 lessI less_add_same_cancel2 less_diff_conv order_le_less)
have step_ev: "(S t ?k) ⊢ ev ↦ (S t (?k+1))"
proof -
have "j ≤ length t"
by (metis assms(2) less_or_eq_imp_le)
then have "l + (i + 1) < length t"
by (meson less_diff_conv less_le_trans range_l)
then show ?thesis
by (metis (no_types) Suc_eq_plus1 ‹take (j - (i + 1)) (drop (i + 1) t) ! l = ev› ‹take (j - (i + 1)) (drop (i + 1) t) ! l = t ! (l + (i + 1))› distributed_system.step_Suc distributed_system_axioms valid)
qed
obtain cid s r where f: "ev = RecvMarker cid s r ∨ ev = Snapshot r" using ‹~ regular_event ev›
by (meson isRecvMarker_def isSnapshot_def nonregular_event)
from f have "occurs_on ev ≠ ?q"
proof (elim disjE)
assume snapshot: "ev = Snapshot r"
show ?thesis
proof (rule ccontr)
assume occurs_on_q: "~ occurs_on ev ≠ ?q"
then have "?q = r" using snapshot by auto
then have q_snapshotted: "has_snapshotted (S t (?k+1)) ?q"
using snapshot step_ev by auto
then show False
proof -
have "l + (i + 1) < j"
by (meson less_diff_conv range_l)
then show ?thesis
by (metis (no_types) Suc_eq_plus1 Suc_le_eq computation.snapshot_stable_ver_2 computation_axioms pre_ej prerecording_event q_snapshotted valid)
qed
qed
next
assume RecvMarker: "ev = RecvMarker cid s r"
show ?thesis
proof (rule ccontr)
assume occurs_on_q: "~ occurs_on ev ≠ ?q"
then have "s = ?q" using RecvMarker by auto
then have q_snapshotted: "has_snapshotted (S t (?k+1)) ?q"
proof (cases "has_snapshotted (S t ?k) ?q")
case True
then show ?thesis using snapshot_stable_ver_2 step_Suc step_ev valid by auto
next
case False
then show "has_snapshotted (S t (?k+1)) ?q"
using ‹s = ?q› next_recv_marker RecvMarker step_ev by auto
qed
then show False
proof -
have "l + (i + 1) < j"
using less_diff_conv range_l by blast
then show ?thesis
by (metis (no_types) Suc_eq_plus1 Suc_le_eq computation.snapshot_stable_ver_2 computation_axioms pre_ej prerecording_event q_snapshotted valid)
qed
qed
qed
then show "¬ regular_event ev ∧ occurs_on ev ≠ ?q"
using ‹~ regular_event ev› by simp
qed
qed
lemma can_swap_neighboring_pre_and_postrecording_events:
assumes
"i < j" and
"j < length t" and
"occurs_on (t ! i) = p" and
"occurs_on (t ! j) = q" and
neighboring: "∀k. (i < k ∧ k < j)
⟶ ~ regular_event (t ! k)" and
post_ei: "postrecording_event t i" and
pre_ej: "prerecording_event t j" and
valid: "trace init t final"
shows
"can_occur (t ! j) (S t i)"
proof -
have "p ≠ q" using post_before_pre_different_processes assms by auto
have sp: "has_snapshotted (S t i) p"
using assms(3) post_ei postrecording_event prerecording_event by blast
have nsq: "~ has_snapshotted (S t j) q"
using assms(4) pre_ej prerecording_event by auto
let ?nr = "take (j - (Suc i)) (drop (Suc i) t)"
have valid_subtrace: "trace (S t (Suc i)) ?nr (S t j)"
using assms(1) exists_trace_for_any_i_j valid by fastforce
have "Ball (set ?nr) (%ev. ~ occurs_on ev = q ∧ ~ regular_event ev)"
proof -
have "?nr = take (j - (i+1)) (drop (i+1) t)" by auto
then show ?thesis
by (metis assms(1) assms(2) assms(4) neighboring post_ei pre_ej valid post_before_pre_neighbors)
qed
then have la: "list_all (%ev. ~ occurs_on ev = q) ?nr"
by (meson list_all_length nth_mem)
have tj_to_tSi: "can_occur (t ! j) (S t (Suc i))"
proof -
have "list_all (%ev. ~ isSend ev) ?nr"
proof -
have "list_all (%ev. ~ regular_event ev) ?nr"
using ‹∀ev∈set (take (j - (Suc i)) (drop (Suc i) t)). occurs_on ev ≠ q ∧ ¬ regular_event ev› ‹list_all (λev. occurs_on ev ≠ q) (take (j - (Suc i)) (drop (Suc i) t))› list.pred_mono_strong by fastforce
then show ?thesis
by (simp add: list.pred_mono_strong)
qed
moreover have "~ isRecvMarker (t ! j)" using prerecording_event assms by auto
moreover have "can_occur (t ! j) (S t j)"
proof -
have "(S t j) ⊢ (t ! j) ↦ (S t (Suc j))"
using assms(2) step_Suc valid by auto
then show ?thesis
using happen_implies_can_occur by blast
qed
ultimately show "can_occur (t ! j) (S t (Suc i))"
using assms(4) event_can_go_back_if_no_sender_trace valid_subtrace la by blast
qed
show "can_occur (t ! j) (S t i)"
proof (cases "isSend (t ! i)")
case False
have "~ isRecvMarker (t ! j)" using assms prerecording_event by auto
moreover have "~ isSend (t ! i)" using False by simp
ultimately show ?thesis
by (metis ‹p ≠ q› assms(3) assms(4) event_can_go_back_if_no_sender post_ei postrecording_event step_Suc tj_to_tSi valid)
next
case True
obtain cid s u u' m where Send: "t ! i = Send cid p s u u' m"
by (metis True isSend_def assms(3) event.sel(2))
have chan: "channel cid = Some (p, s)"
proof -
have "can_occur (t ! i) (S t i)"
by (meson computation.postrecording_event computation_axioms happen_implies_can_occur post_ei step_Suc valid)
then show ?thesis using can_occur_def Send by simp
qed
have n: "(S t i) ⊢ (t ! i) ↦ (S t (Suc i))"
using assms(1) assms(2) step_Suc valid True by auto
have st: "states (S t i) q = states (S t (Suc i)) q"
using Send ‹p ≠ q› n by auto
have "isTrans (t ! j) ∨ isSend (t ! j) ∨ isRecv (t ! j)"
using assms(7) computation.prerecording_event computation_axioms regular_event by blast
then show ?thesis
proof (elim disjE)
assume "isTrans (t ! j)"
then show ?thesis
by (metis (no_types, lifting) tj_to_tSi st can_occur_def assms(4) event.case(1) event.collapse(1))
next
assume "isSend (t ! j)"
then obtain cid' s' u'' u''' m' where Send: "t ! j = Send cid' q s' u'' u''' m'"
by (metis (no_types, lifting) assms(4) event.sel(2) isSend_def)
have co_tSi: "can_occur (Send cid' q s' u'' u''' m') (S t (Suc i))"
using Send tj_to_tSi by auto
then have "channel cid' = Some (q, s') ∧ send cid' q s' u'' u''' m'"
using Send can_occur_def by simp
then show ?thesis using can_occur_def st Send assms co_tSi by auto
next
assume "isRecv (t ! j)"
then obtain cid' s' u'' u''' m' where Recv: "t ! j = Recv cid' q s' u'' u''' m'"
by (metis assms(4) event.sel(3) isRecv_def)
have co_tSi: "can_occur (Recv cid' q s' u'' u''' m') (S t (Suc i))"
using Recv tj_to_tSi by auto
then have a: "channel cid' = Some (s', q) ∧ length (msgs (S t (Suc i)) cid') > 0
∧ hd (msgs (S t (Suc i)) cid') = Msg m'"
using can_occur_def co_tSi by fastforce
show "can_occur (t ! j) (S t i)"
proof (cases "cid = cid'")
case False
with Send n have "msgs (S t (Suc i)) cid' = msgs (S t i) cid'" by auto
then have b: "length (msgs (S t i) cid') > 0 ∧ hd (msgs (S t i) cid') = Msg m'"
using a by simp
with can_occur_Recv co_tSi st a Recv show ?thesis
unfolding can_occur_def by auto
next
case True
have stu: "states (S t i) q = u''"
using can_occur_Recv co_tSi st by blast
show ?thesis
proof (rule ccontr)
have marker_in_set: "Marker ∈ set (msgs (S t i) cid)"
proof -
have "(s', q) = (p, q)"
using True a chan by auto
then show ?thesis
by (metis (no_types, lifting) True ‹p ≠ q› a assms(3) marker_must_stay_if_no_snapshot n no_state_change_if_no_event nsq snapshot_stable_2 sp valid valid_subtrace)
qed
assume asm: "~ can_occur (t ! j) (S t i)"
then show False
proof (unfold can_occur_def, (auto simp add: marker_in_set True Recv stu))
assume "msgs (S t i) cid' = []"
then show False using marker_in_set
by (simp add: True)
next
assume "hd (msgs (S t i) cid') ≠ Msg m'"
have "msgs (S t i) cid ≠ []" using marker_in_set by auto
then have "msgs (S t (Suc i)) cid = msgs (S t i) cid @ [Msg m]"
using Send True n chan by auto
then have "hd (msgs (S t (Suc i)) cid) ≠ Msg m'"
using True ‹hd (msgs (S t i) cid') ≠ Msg m'› ‹msgs (S t i) cid ≠ []› by auto
then have "~ can_occur (t ! j) (S t (Suc i))"
using True a by blast
then show False
using tj_to_tSi by blast
next
assume "~ recv cid' q s' u'' u''' m'"
then show False
using can_occur_Recv co_tSi by blast
next
assume "channel cid' ≠ Some (s', q)"
then show False using can_occur_def tj_to_tSi Recv by simp
qed
qed
qed
qed
qed
qed
subsubsection ‹Event swapping›
lemma swap_events:
shows "⟦ i < j; j < length t;
∀k. (i < k ∧ k < j) ⟶ ~ regular_event (t ! k);
postrecording_event t i; prerecording_event t j;
trace init t final ⟧
⟹ trace init (swap_events i j t) final
∧ (∀k. k ≥ j + 1 ⟶ S (swap_events i j t) k = S t k)
∧ (∀k. k ≤ i ⟶ S (swap_events i j t) k = S t k)
∧ prerecording_event (swap_events i j t) i
∧ postrecording_event (swap_events i j t) (i+1)
∧ (∀k. k > i+1 ∧ k < j+1
⟶ ~ regular_event ((swap_events i j t) ! k))"
proof (induct "j - (i+1)" arbitrary: j t)
case 0
let ?p = "occurs_on (t ! i)"
let ?q = "occurs_on (t ! j)"
have "j = (i+1)"
using "0.prems" "0.hyps" by linarith
let ?subt = "take (j - (i+1)) (drop (i+1) t)"
have "t = take i t @ [t ! i] @ ?subt @ [t ! j] @ drop (j+1) t"
proof -
have "take (Suc i) t = take i t @ [t ! i]"
using "0.prems"(2) ‹j = i + 1› add_lessD1 take_Suc_conv_app_nth by blast
then show ?thesis
by (metis (no_types) "0.hyps" "0.prems"(2) Suc_eq_plus1 ‹j = i + 1› append_assoc append_take_drop_id self_append_conv2 take_Suc_conv_app_nth take_eq_Nil)
qed
have sp: "has_snapshotted (S t i) ?p"
using "0.prems" postrecording_event prerecording_event by blast
have nsq: "~ has_snapshotted (S t j) ?q"
using "0.prems" postrecording_event prerecording_event by blast
have "?p ≠ ?q"
using "0.prems" computation.post_before_pre_different_processes computation_axioms by blast
have "?subt = Nil"
by (simp add: ‹j = i + 1›)
have reg_step_1: "(S t i) ⊢ (t ! i) ↦ (S t j)"
by (metis "0.prems"(2) "0.prems"(6) Suc_eq_plus1 ‹j = i + 1› add_lessD1 step_Suc)
have reg_step_2: "(S t j) ⊢ (t ! j) ↦ (S t (j+1))"
using "0.prems"(2) "0.prems"(6) step_Suc by auto
have "can_occur (t ! j) (S t i)"
using "0.prems" can_swap_neighboring_pre_and_postrecording_events by blast
then obtain d' where new_step1: "(S t i) ⊢ (t ! j) ↦ d'"
using exists_next_if_can_occur by blast
have st: "states d' ?p = states (S t i) ?p"
using ‹(S t i) ⊢ t ! j ↦ d'› ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› no_state_change_if_no_event by auto
then have "can_occur (t ! i) d'"
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› event_stays_valid_if_no_occurrence happen_implies_can_occur new_step1 reg_step_1 by auto
then obtain e where new_step2: "d' ⊢ (t ! i) ↦ e"
using exists_next_if_can_occur by blast
have "states e = states (S t (j+1))"
proof (rule ext)
fix p
show "states e p = states (S t (j+1)) p"
proof (cases "p = ?p ∨ p = ?q")
case True
then show ?thesis
proof (elim disjE)
assume "p = ?p"
then have "states d' p = states (S t i) p"
by (simp add: st)
thm same_state_implies_same_result_state
then have "states e p = states (S t j) p"
using "0.prems"(2) "0.prems"(6) new_step2 reg_step_1 by (blast intro:same_state_implies_same_result_state[symmetric])
moreover have "states (S t j) p = states (S t (j+1)) p"
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› ‹p = occurs_on (t ! i)› no_state_change_if_no_event reg_step_2 by auto
ultimately show ?thesis by simp
next
assume "p = ?q"
then have "states (S t j) p = states (S t i) p"
using reg_step_1 ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› no_state_change_if_no_event by auto
then have "states d' p = states (S t (j+1)) p"
using "0.prems"(5) prerecording_event computation_axioms new_step1 reg_step_2 same_state_implies_same_result_state by blast
moreover have "states e p = states (S t (j+1)) p"
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› ‹p = occurs_on (t ! j)› calculation new_step2 no_state_change_if_no_event by auto
ultimately show ?thesis by simp
qed
next
case False
then have "states (S t i) p = states (S t j) p"
using no_state_change_if_no_event reg_step_1 by auto
moreover have "... = states (S t (j+1)) p"
using False no_state_change_if_no_event reg_step_2 by auto
moreover have "... = states d' p"
using False calculation new_step1 no_state_change_if_no_event by auto
moreover have "... = states e p"
using False new_step2 no_state_change_if_no_event by auto
ultimately show ?thesis by simp
qed
qed
moreover have "msgs e = msgs (S t (j+1))"
proof (rule ext)
fix cid
have "isTrans (t ! i) ∨ isSend (t ! i) ∨ isRecv (t ! i)"
using "0.prems"(4) computation.postrecording_event computation_axioms regular_event by blast
moreover have "isTrans (t ! j) ∨ isSend (t ! j) ∨ isRecv (t ! j)"
using "0.prems"(5) computation.prerecording_event computation_axioms regular_event by blast
ultimately show "msgs e cid = msgs (S t (j+1)) cid"
proof (elim disjE, goal_cases)
case 1
then have "msgs d' cid = msgs (S t j) cid"
by (metis Trans_msg new_step1 reg_step_1)
then show ?thesis
using Trans_msg ‹isTrans (t ! i)› ‹isTrans (t ! j)› new_step2 reg_step_2 by auto
next
case 2
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 swap_msgs_Trans_Send by auto
next
case 3
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 swap_msgs_Trans_Recv by auto
next
case 4
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 swap_msgs_Send_Trans by auto
next
case 5
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 swap_msgs_Recv_Trans by auto
next
case 6
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 by (blast intro:swap_msgs_Send_Send[symmetric])
next
case 7
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 swap_msgs_Send_Recv by auto
next
case 8
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 swap_msgs_Send_Recv by simp
next
case 9
then show ?thesis
using ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› new_step1 new_step2 reg_step_1 reg_step_2 by (blast intro:swap_msgs_Recv_Recv[symmetric])
qed
qed
moreover have "process_snapshot e = process_snapshot (S t (j+1))"
proof (rule ext)
fix p
have "process_snapshot d' p = process_snapshot (S t j) p"
by (metis "0.prems"(4) "0.prems"(5) computation.postrecording_event computation.prerecording_event computation_axioms new_step1 reg_step_1 regular_event_preserves_process_snapshots)
then show "process_snapshot e p = process_snapshot (S t (j+1)) p"
by (metis "0.prems"(4) "0.prems"(5) computation.postrecording_event computation.prerecording_event computation_axioms new_step2 reg_step_2 regular_event_preserves_process_snapshots)
qed
moreover have "channel_snapshot e = channel_snapshot (S t (j+1))"
proof (rule ext)
fix cid
show "cs e cid = cs (S t (j+1)) cid"
proof (cases "isRecv (t ! i)"; cases "isRecv (t ! j)", goal_cases)
case 1
then show ?thesis
using ‹?p ≠ ?q› new_step1 new_step2 reg_step_1 reg_step_2
by (blast intro:regular_event_implies_same_channel_snapshot_Recv_Recv[symmetric])
next
case 2
moreover have "regular_event (t ! j)" using prerecording_event 0 by simp
ultimately show ?thesis
using ‹?p ≠ ?q› new_step1 new_step2 reg_step_1 reg_step_2 regular_event_implies_same_channel_snapshot_Recv by auto
next
assume 3: "~ isRecv (t ! i)" "isRecv (t ! j)"
moreover have "regular_event (t ! i)" using postrecording_event 0 by simp
ultimately show ?thesis
using ‹?p ≠ ?q› new_step1 new_step2 reg_step_1 reg_step_2 regular_event_implies_same_channel_snapshot_Recv by auto
next
assume 4: "~ isRecv (t ! i)" "~ isRecv (t ! j)"
moreover have "regular_event (t ! j)" using prerecording_event 0 by simp
moreover have "regular_event (t ! i)" using postrecording_event 0 by simp
ultimately show ?thesis
using ‹?p ≠ ?q› new_step1 new_step2 reg_step_1 reg_step_2
by (metis no_cs_change_if_no_event)
qed
qed
ultimately have "e = S t (j+1)" by simp
then have "(S t i) ⊢ (t ! j) ↦ d' ∧ d' ⊢ (t ! i) ↦ (S t (j+1))"
using new_step1 new_step2 by blast
then have swap: "trace (S t i) [t ! j, t ! i] (S t (j+1))"
by (meson trace.simps)
have "take (j-1) t @ [t ! j, t ! i] = ((take (j+1) t)[i := t ! j])[j := t ! i]"
proof -
have "i = j - 1"
by (simp add: ‹j = i + 1›)
show ?thesis
proof (subst (1 2 3) ‹i = j - 1›)
have "j < length t" using "0.prems" by auto
then have "take (j - 1) t @ [t ! j, t ! (j - 1)] @ drop (j + 1) t = t[j - 1 := t ! j, j := t ! (j - 1)]"
by (metis Suc_eq_plus1 ‹i = j - 1› ‹j = i + 1› add_Suc_right arith_special(3) swap_neighbors)
then show "take (j - 1) t @ [t ! j, t ! (j - 1)] = (take (j+1) t)[j - 1 := t ! j, j := t ! (j - 1)]"
proof -
assume a1: "take (j - 1) t @ [t ! j, t ! (j - 1)] @ drop (j + 1) t = t [j - 1 := t ! j, j := t ! (j - 1)]"
have f2: "t[j - 1 := t ! j, j := t ! (j - 1)] = take j (t[j - 1 := t ! j]) @ t ! (j - 1) # drop (Suc j) (t[j - 1 := t ! j])"
by (metis (no_types) "0.prems"(2) length_list_update upd_conv_take_nth_drop)
have f3: "∀n na. ¬ n < na ∨ Suc n ≤ na"
using Suc_leI by blast
then have "min (length t) (j + 1) = j + 1"
by (metis (no_types) "0.prems"(2) Suc_eq_plus1 min.absorb2)
then have f4: "length ((take (j + 1) t)[j - 1 := t ! j]) = j + 1"
by simp
have f5: "j + 1 ≤ length (t[j - 1 := t ! j])"
using f3 by (metis (no_types) "0.prems"(2) Suc_eq_plus1 length_list_update)
have "Suc j ≤ j + 1"
by linarith
then have "(take (j + 1) (t[j - 1 := t ! j]))[j := t ! (j - 1)] = take j (t[j - 1 := t ! j]) @ t ! (j - 1) # [] @ []"
using f5 f4 by (metis (no_types) Suc_eq_plus1 add_diff_cancel_right' butlast_conv_take butlast_take drop_eq_Nil lessI self_append_conv2 take_update_swap upd_conv_take_nth_drop)
then show ?thesis
using f2 a1 by (simp add: take_update_swap)
qed
qed
qed
have s: "trace init (take i t) (S t i)"
using "0.prems"(6) exists_trace_for_any_i by blast
have e: "trace (S t (j+1)) (take (length t - (j+1)) (drop (j+1) t)) final"
proof -
have "trace init (take (length t) t) final"
by (simp add: "0.prems"(6))
then show ?thesis
by (metis "0.prems"(2) Suc_eq_plus1 Suc_leI exists_trace_for_any_i exists_trace_for_any_i_j nat_le_linear take_all trace_and_start_determines_end)
qed
have "trace init (take i t @ [t ! j] @ [t ! i] @ drop (j+1) t) final"
proof -
from s swap have "trace init (take i t @ [t ! j,t ! i]) (S t (j+1))" using trace_trans by blast
then have "trace init (take i t @ [t ! j, t ! i] @ (take (length t - (j+1)) (drop (j+1) t))) final"
using e trace_trans by fastforce
moreover have "take (length t - (j+1)) (drop (j+1) t) = drop (j+1) t" by simp
ultimately show ?thesis by simp
qed
moreover have "take i t @ [t ! j] @ [t ! i] @ drop (j+1) t = (t[i := t ! j])[j := t ! i]"
proof -
have "length (take i t @ [t ! j] @ [t ! i] @ drop (j+1) t) = length ((t[i := t ! j])[j := t ! i])"
by (metis (mono_tags, lifting) ‹t = take i t @ [t ! i] @ take (j - (i + 1)) (drop (i + 1) t) @ [t ! j] @ drop (j + 1) t› ‹take (j - (i + 1)) (drop (i + 1) t) = []› length_append length_list_update list.size(4) self_append_conv2)
moreover have "⋀k. k < length ((t[i := t ! j])[j := t ! i]) ⟹ (take i t @ [t ! j] @ [t ! i] @ drop (j+1) t) ! k = ((t[i := t ! j])[j := t ! i]) ! k"
proof -
fix k
assume "k < length ((t[i := t ! j])[j := t ! i])"
show "(take i t @ [t ! j] @ [t ! i] @ drop (j+1) t) ! k = ((t[i := t ! j])[j := t ! i]) ! k"
proof (cases "k = i ∨ k = j")
case True
then show ?thesis
proof (elim disjE)
assume "k = i"
then show ?thesis
by (metis (no_types, lifting) ‹k < length (t[i := t ! j, j := t ! i])› append_Cons le_eq_less_or_eq length_list_update length_take min.absorb2 nth_append_length nth_list_update_eq nth_list_update_neq)
next
assume "k = j"
then show ?thesis
by (metis (no_types, lifting) "0.prems"(4) Suc_eq_plus1 ‹j = i + 1› ‹k < length (t[i := t ! j, j := t ! i])› append.assoc append_Cons le_eq_less_or_eq length_append_singleton length_list_update length_take min.absorb2 nth_append_length nth_list_update postrecording_event)
qed
next
case knij: False
then show ?thesis
proof (cases "k < i")
case True
then show ?thesis
by (metis (no_types, lifting) "0.prems"(2) ‹j = i + 1› add_lessD1 length_take less_imp_le_nat min.absorb2 not_less nth_append nth_list_update_neq nth_take)
next
case False
then have "k > j"
using ‹j = i + 1› knij by linarith
then have "(take i t @ [t ! j] @ [t ! i] @ drop (j+1) t) ! k = drop (j+1) t ! (k-(j+1))"
proof -
assume a1: "j < k"
have f2: "∀n na. ((n::nat) < na) = (n ≤ na ∧ n ≠ na)"
using nat_less_le by blast
have f3: "i + 0 = min (length t) i + (0 + 0)"
using "0.prems"(2) ‹j = i + 1› by linarith
have f4: "min (length t) i + Suc (0 + 0) = length (take i t) + length [t ! j]"
by force
have f5: "take i t @ [t ! j] @ [] = take i t @ [t ! j]"
by auto
have "j = length (take i t @ [t ! j] @ [])"
using f3 by (simp add: ‹j = i + 1›)
then have "j + 1 = length (take i t @ [t ! j] @ [t ! i])"
by fastforce
then show ?thesis
using f5 f4 f3 f2 a1 by (metis (no_types) One_nat_def ‹j = i + 1› add_Suc_right append.assoc length_append less_antisym list.size(3) not_less nth_append)
qed
moreover have "(t[i := t ! j])[j := t ! i] ! k = drop (j+1) ((t[i := t ! j])[j := t ! i]) ! (k-(j+1))"
using "0.prems"(2) ‹j < k› by auto
moreover have "drop (j+1) ((t[i := t ! j])[j := t ! i]) = drop (j+1) t"
using "0.prems"(1) by auto
ultimately show ?thesis by simp
qed
qed
qed
ultimately show ?thesis by (simp add: list_eq_iff_nth_eq)
qed
moreover have "∀k. k ≥ j + 1 ⟶ S t k = S ((t[i := t ! j])[j := t ! i]) k"
proof (rule allI, rule impI)
fix k
assume "k ≥ j + 1"
let ?newt = "((t[i := t ! j])[j := t ! i])"
have "trace init (take k ?newt) (S ?newt k)"
using calculation(1) calculation(2) exists_trace_for_any_i by auto
have "take k ?newt = take (j+1) ?newt @ take (k - (j+1)) (drop (j+1) ?newt)"
by (metis ‹j + 1 ≤ k› le_add_diff_inverse take_add)
have same_traces: "drop (j+1) t = drop (j+1) ?newt"
by (metis "0.prems"(1) Suc_eq_plus1 ‹j = i + 1› drop_update_cancel less_SucI less_add_same_cancel1)
have "trace init (take (j+1) ((t[i := t ! j])[j := t ! i])) (S t (j+1))"
by (metis (no_types, lifting) ‹j = i + 1› ‹take (j - 1) t @ [t ! j, t ! i] = (take (j + 1) t)[i := t ! j, j := t ! i]› add_diff_cancel_right' local.swap s take_update_swap trace_trans)
moreover have "trace init (take (j+1) ?newt) (S ?newt (j+1))"
using ‹take i t @ [t ! j] @ [t ! i] @ drop (j + 1) t = t[i := t ! j, j := t ! i]› ‹trace init (take i t @ [t ! j] @ [t ! i] @ drop (j + 1) t) final› exists_trace_for_any_i by auto
ultimately have "S ?newt (j+1) = S t (j+1)"
using trace_and_start_determines_end by blast
have "trace (S t (j+1)) (take (k - (j+1)) (drop (j+1) t)) (S t k)"
using "0.prems"(6) ‹j + 1 ≤ k› exists_trace_for_any_i_j by blast
moreover have "trace (S ?newt (j+1)) (take (k - (j+1)) (drop (j+1) ?newt)) (S ?newt k)"
using ‹j + 1 ≤ k› ‹take i t @ [t ! j] @ [t ! i] @ drop (j + 1) t = t[i := t ! j, j := t ! i]› ‹trace init (take i t @ [t ! j] @ [t ! i] @ drop (j + 1) t) final› exists_trace_for_any_i_j by fastforce
ultimately show "S t k = S ?newt k"
using ‹S (t[i := t ! j, j := t ! i]) (j + 1) = S t (j + 1)› same_traces trace_and_start_determines_end by auto
qed
moreover have "∀k. k ≤ i ⟶ S t k = S ((t[i := t ! j])[j := t ! i]) k"
proof (rule allI, rule impI)
fix k
assume "k ≤ i"
let ?newt = "((t[i := t ! j])[j := t ! i])"
have "trace init (take k t) (S t k)"
using "0.prems"(6) exists_trace_for_any_i by blast
moreover have "trace init (take k ?newt) (S ?newt k)"
using ‹take i t @ [t ! j] @ [t ! i] @ drop (j + 1) t = t[i := t ! j, j := t ! i]› ‹trace init (take i t @ [t ! j] @ [t ! i] @ drop (j + 1) t) final› exists_trace_for_any_i by auto
moreover have "take k t = take k ?newt"
using "0.prems"(1) ‹k ≤ i› by auto
ultimately show "S t k = S ?newt k"
by (simp add: trace_and_start_determines_end)
qed
moreover have "prerecording_event (swap_events i j t) i"
proof -
have "~ has_snapshotted (S ((t[i := t ! j])[j := t ! i]) i) ?q"
by (metis "0.prems"(6) ‹j = i + 1› add.right_neutral calculation(4) le_add1 nsq snapshot_stable_ver_3)
moreover have "regular_event ((t[i := t ! j])[j := t ! i] ! i)"
by (metis "0.prems"(4) "0.prems"(5) ‹occurs_on (t ! i) ≠ occurs_on (t ! j)› nth_list_update_eq nth_list_update_neq postrecording_event prerecording_event)
moreover have "i < length ((t[i := t ! j])[j := t ! i])"
using "0.prems"(1) "0.prems"(2) by auto
ultimately show ?thesis unfolding prerecording_event
by (metis (no_types, opaque_lifting) "0.prems"(1) ‹take (j - (i + 1)) (drop (i + 1) t) = []› ‹take i t @ [t ! j] @ [t ! i] @ drop (j + 1) t = t[i := t ! j, j := t ! i]› append_Cons length_list_update nat_less_le nth_list_update_eq nth_list_update_neq self_append_conv2)
qed
moreover have "postrecording_event (swap_events i j t) (i+1)"
proof -
have "has_snapshotted (S ((t[i := t ! j])[j := t ! i]) (i+1)) ?p"
by (metis "0.prems"(4) add.right_neutral calculation(1) calculation(2) calculation(4) le_add1 postrecording_event snapshot_stable_ver_3)
moreover have "regular_event ((t[i := t ! j])[j := t ! i] ! j)"
using "0.prems"(2) "0.prems"(4) length_list_update postrecording_event by auto
moreover have "j < length t" using "0.prems" by auto
ultimately show ?thesis unfolding postrecording_event
by (metis ‹j = i + 1› length_list_update nth_list_update_eq swap_neighbors_2)
qed
moreover have "∀k. k > i+1 ∧ k < j+1 ⟶ ~ regular_event ((swap_events i j t) ! k)" using "0" by force
ultimately show ?case using ‹j = i + 1› by force
next
case (Suc n)
let ?p = "occurs_on (t ! i)"
let ?q = "occurs_on (t ! j)"
let ?t = "take ((j+1) - i) (drop i t)"
let ?subt = "take (j - (i+1)) (drop (i+1) t)"
let ?subt' = "take ((j-1) - (i+1)) (drop (i+1) t)"
have sp: "has_snapshotted (S t i) ?p"
using Suc.prems postrecording_event prerecording_event by blast
have nsq: "~ has_snapshotted (S t j) ?q"
using Suc.prems postrecording_event prerecording_event by blast
have "?p ≠ ?q"
us