# Theory Co_Snapshot

```theory Co_Snapshot
imports
Snapshot
Ordered_Resolution_Prover.Lazy_List_Chain
begin

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
next
case (Suc i)
then show ?case
by (cases xs) auto
qed

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
begin

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)

end

locale cocomputation = distributed_system +
fixes
init :: "('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. 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)"
begin

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)
done

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
done
qed

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)
next
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
next
case False
then show ?thesis
using no_markers_if_all_snapshotted[OF assms ‹j ≤ m› j(2), of c]
by (auto simp: C_def)
qed
with *[OF ‹j ≤ m›] m pick show ?thesis by auto
qed
qed

context
fixes t
assumes cotrace: "cotrace init t"
begin

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)
done
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)
done
done

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)
qed

end

print_statement snapshot_algorithm_is_cocorrect

end

end
```