Theory EigbyzProof
theory EigbyzProof
imports EigbyzDefs "../Majorities" "../Reduction"
begin
subsection ‹Preliminary Lemmas›
text ‹Some technical lemmas about labels and trees.›
lemma not_leaf_length:
assumes l: "¬(is_leaf l)"
shows "length_lbl l ≤ f"
using l length_lbl[of l] by (simp add: is_leaf_def)
lemma nil_is_Label: "[] ∈ Label"
by (auto simp: Label_def)
lemma card_set_lbl: "card (set_lbl l) = length_lbl l"
unfolding set_lbl_def length_lbl_def
using Rep_Label[of l, unfolded Label_def]
by (auto elim: distinct_card)
lemma Rep_Label_root_node [simp]: "Rep_Label root_node = []"
using nil_is_Label by (simp add: root_node_def Abs_Label_inverse)
lemma root_node_length [simp]: "length_lbl root_node = 0"
by (simp add: length_lbl_def)
lemma root_node_not_leaf: "¬(is_leaf root_node)"
by (simp add: is_leaf_def)
text ‹Removing the last element of a non-root label gives a label.›
lemma butlast_rep_in_label:
assumes l:"l ≠ root_node"
shows "butlast (Rep_Label l) ∈ Label"
proof -
have "Rep_Label l ≠ []"
proof
assume "Rep_Label l = []"
hence "Rep_Label l = Rep_Label root_node" by simp
with l show "False" by (simp only: Rep_Label_inject)
qed
with Rep_Label[of l] show ?thesis
by (auto simp: Label_def elim: distinct_butlast)
qed
text ‹
The label of a child is well-formed.
›
lemma Rep_Label_append:
assumes l: "¬(is_leaf l)"
shows "(Rep_Label l @ [p] ∈ Label) = (p ∉ set_lbl l)"
(is "?lhs = ?rhs" is "(?l' ∈ _) = _")
proof
assume lhs: "?lhs" thus ?rhs
by (auto simp: Label_def set_lbl_def)
next
assume p: "?rhs"
from l[THEN not_leaf_length] have "length ?l' ≤ Suc f"
by (simp add: length_lbl_def)
moreover
from Rep_Label[of l] have "distinct (Rep_Label l)"
by (simp add: Label_def)
with p have "distinct ?l'" by (simp add: set_lbl_def)
ultimately
show ?lhs by (simp add: Label_def)
qed
text ‹
The label of a child is the label of the parent, extended by a process.
›
lemma label_children:
assumes c: "c ∈ children l"
shows "∃p. p ∉ set_lbl l ∧ Rep_Label c = Rep_Label l @ [p]"
proof -
from c obtain p
where p: "p ∉ set_lbl l" and l: "¬(is_leaf l)"
and c: "c = Abs_Label (Rep_Label l @ [p])"
by (auto simp: children_def)
with Rep_Label_append[OF l] show ?thesis
by (auto simp: Abs_Label_inverse)
qed
text ‹
The label of any child node is one longer than the label of its parent.
›
lemma children_length:
assumes "l ∈ children h"
shows "length_lbl l = Suc (length_lbl h)"
using label_children[OF assms] by (auto simp: length_lbl_def)
text ‹The root node is never a child.›
lemma children_not_root:
assumes "root_node ∈ children l"
shows "P"
using label_children[OF assms] Abs_Label_inverse[OF nil_is_Label]
by (auto simp: root_node_def)
text ‹
The label of a child with the last element removed is the label of
the parent.
›
lemma children_butlast_lbl:
assumes "c ∈ children l"
shows "butlast_lbl c = l"
using label_children[OF assms]
by (auto simp: butlast_lbl_def Rep_Label_inverse)
text ‹
The root node is not a child, and it is the only such node.
›
lemma root_iff_no_child: "(l = root_node) = (∀l'. l ∉ children l')"
proof
assume "l = root_node"
thus "∀l'. l ∉ children l'" by (auto elim: children_not_root)
next
assume rhs: "∀l'. l ∉ children l'"
show "l = root_node"
proof (rule rev_exhaust[of "Rep_Label l"])
assume "Rep_Label l = []"
hence "Rep_Label l = Rep_Label root_node" by simp
thus ?thesis by (simp only: Rep_Label_inject)
next
fix l' q
assume l': "Rep_Label l = l' @ [q]"
let ?l' = "Abs_Label l'"
from Rep_Label[of l] l' have "l' ∈ Label" by (simp add: Label_def)
hence repl': "Rep_Label ?l' = l'" by (rule Abs_Label_inverse)
from Rep_Label[of l] l' have "l' @ [q] ∈ Label" by (simp add: Label_def)
with l' have "Rep_Label l = Rep_Label (Abs_Label (l' @ [q]))"
by (simp add: Abs_Label_inverse)
hence "l = Abs_Label (l' @ [q])" by (simp add: Rep_Label_inject)
moreover
from Rep_Label[of l] l' have "length l' < Suc f" "q ∉ set l'"
by (auto simp: Label_def)
moreover
note repl'
ultimately have "l ∈ children ?l'"
by (auto simp: children_def is_leaf_def length_lbl_def set_lbl_def)
with rhs show ?thesis by blast
qed
qed
text ‹
If some label ‹l› is not a leaf, then the set of processes that
appear at the end of the labels of its children is the set of all
processes that do not appear in ‹l›.
›
lemma children_last_set:
assumes l: "¬(is_leaf l)"
shows "last_lbl ` (children l) = UNIV - set_lbl l"
proof
show "last_lbl ` (children l) ⊆ UNIV - set_lbl l"
by (auto dest: label_children simp: last_lbl_def)
next
show "UNIV - set_lbl l ⊆ last_lbl ` (children l)"
proof (auto simp: image_def)
fix p
assume p: "p ∉ set_lbl l"
with l have c: "Abs_Label (Rep_Label l @ [p]) ∈ children l"
by (auto simp: children_def)
with Rep_Label_append[OF l] p
show "∃c ∈ children l. p = last_lbl c"
by (force simp: last_lbl_def Abs_Label_inverse)
qed
qed
text ‹
The function returning the last element of a label is injective on the
set of children of some given label.
›
lemma last_lbl_inj_on_children:"inj_on last_lbl (children l)"
proof (auto simp: inj_on_def)
fix c c'
assume c: "c ∈ children l" and c': "c' ∈ children l"
and eq: "last_lbl c = last_lbl c'"
from c c' obtain p p'
where p: "Rep_Label c = Rep_Label l @ [p]"
and p': "Rep_Label c' = Rep_Label l @ [p']"
by (auto dest!: label_children)
from p p' eq have "p = p'" by (simp add: last_lbl_def)
with p p' have "Rep_Label c = Rep_Label c'" by simp
thus "c = c'" by (simp add: Rep_Label_inject)
qed
text ‹
The number of children of any non-leaf label ‹l› is the
number of processes that do not appear in ‹l›.
›
lemma card_children:
assumes "¬(is_leaf l)"
shows "card (children l) = N - (length_lbl l)"
proof -
from assms
have "last_lbl ` (children l) = UNIV - set_lbl l"
by (rule children_last_set)
moreover
have "card (UNIV - set_lbl l) = card (UNIV::Proc set) - card (set_lbl l)"
by (auto simp: card_Diff_subset_Int)
moreover
from last_lbl_inj_on_children
have "card (children l) = card (last_lbl ` children l)"
by (rule sym[OF card_image])
moreover
note card_set_lbl[of l]
ultimately
show ?thesis by auto
qed
text ‹
Suppose a non-root label ‹l'› of length ‹r+1› ending in ‹q›,
and suppose that ‹q› is well heard by process ‹p› in round
‹r›. Then the value with which ‹p› decorates ‹l› is the one
that ‹q› associates to the parent of ‹l›.
›
lemma sho_correct_vals:
assumes run: "SHORun EIG_M rho HOs SHOs"
and l': "l' ∈ children l"
and shop: "last_lbl l' ∈ SHOs (length_lbl l) p ∩ HOs (length_lbl l) p"
(is "?q ∈ SHOs (?len l) p ∩ _")
shows "vals (rho (?len l') p) l' = vals (rho (?len l) ?q) l"
proof -
let ?r = "?len l"
from run obtain μp
where nxt: "nextState EIG_M ?r p (rho ?r p) μp (rho (Suc ?r) p)"
and mu: "μp ∈ SHOmsgVectors EIG_M ?r p (rho ?r) (HOs ?r p) (SHOs ?r p)"
by (auto simp: EIG_SHOMachine_def SHORun_eq SHOnextConfig_eq)
with shop
have msl:"μp ?q = Some (vals (rho ?r ?q))"
by (auto simp: EIG_SHOMachine_def EIG_sendMsg_def SHOmsgVectors_def)
from nxt length_lbl[of l'] children_length[OF l']
have "extend_vals ?r p (rho ?r p) μp (rho (Suc ?r) p)"
by (auto simp: EIG_SHOMachine_def nextState_def EIG_nextState_def
next_main_def next_end_def)
with msl l' show ?thesis
by (auto simp: extend_vals_def children_length children_butlast_lbl)
qed
text ‹
A process fixes the value ‹vals l› of a label at state
‹length_lbl l›, and then never modifies the value.
›
lemma keep_vals:
assumes run: "SHORun EIG_M rho HOs SHOs"
shows "vals (rho (length_lbl l + n) p) l = vals (rho (length_lbl l) p) l"
(is "?v n = ?vl")
proof (induct n)
show "?v 0 = ?vl" by simp
next
fix n
assume ih: "?v n = ?vl"
let ?r = "length_lbl l + n"
from run obtain μp
where nxt: "nextState EIG_M ?r p (rho ?r p) μp (rho (Suc ?r) p)"
by (auto simp: EIG_SHOMachine_def SHORun_eq SHOnextConfig_eq)
with ih show "?v (Suc n) = ?vl"
by (auto simp: EIG_SHOMachine_def nextState_def EIG_nextState_def
next_main_def next_end_def extend_vals_def)
qed
subsection ‹Lynch's Lemmas and Theorems›
text ‹
If some process is safely heard by all processes at round ‹r›,
then all processes agree on the value associated to labels of length
‹r+1› ending in that process.
›
lemma lynch_6_15:
assumes run: "SHORun EIG_M rho HOs SHOs"
and l': "l' ∈ children l"
and skr: "last_lbl l' ∈ SKr (HOs (length_lbl l)) (SHOs (length_lbl l))"
shows "vals (rho (length_lbl l') p) l' = vals (rho (length_lbl l') q) l'"
using assms unfolding SKr_def by (auto simp: sho_correct_vals)
text ‹
Suppose that ‹l› is a non-root label whose last element was well
heard by all processes at round ‹r›, and that ‹l'› is a
child of ‹l› corresponding to process ‹q› that is also
well heard by all processes at round ‹r+1›. Then the values
associated with ‹l› and ‹l'› by any process ‹p›
are identical.
›
lemma lynch_6_16_a:
assumes run: "SHORun EIG_M rho HOs SHOs"
and l: "l ∈ children t"
and skrl: "last_lbl l ∈ SKr (HOs (length_lbl t)) (SHOs (length_lbl t))"
and l': "l' ∈ children l"
and skrl':"last_lbl l' ∈ SKr (HOs (length_lbl l)) (SHOs (length_lbl l))"
shows "vals (rho (length_lbl l') p) l' = vals (rho (length_lbl l) p) l"
using assms by (auto simp: SKr_def sho_correct_vals)
text ‹
For any non-leaf label ‹l›, more than half of its children end with a
process that is well heard by everyone at round ‹length_lbl l›.
›
lemma lynch_6_16_c:
assumes commR: "EIG_commPerRd (HOs (length_lbl l)) (SHOs (length_lbl l))"
(is "EIG_commPerRd (HOs ?r) _")
and l: "¬(is_leaf l)"
shows "card {l' ∈ children l. last_lbl l' ∈ SKr (HOs ?r) (SHOs ?r)}
> card (children l) div 2"
(is "card ?lhs > _")
proof -
let ?skr = "SKr (HOs ?r) (SHOs ?r)"
have "last_lbl ` ?lhs = ?skr - set_lbl l"
proof
from children_last_set[OF l]
show "last_lbl ` ?lhs ⊆ ?skr - set_lbl l"
by (auto simp: children_length)
next
{
fix p
assume p: "p ∈ ?skr" "p ∉ set_lbl l"
with children_last_set[OF l]
have "p ∈ last_lbl ` children l" by auto
with p have "p ∈ last_lbl ` ?lhs"
by (auto simp: image_def children_length)
}
thus "?skr - set_lbl l ⊆ last_lbl ` ?lhs" by auto
qed
moreover
from last_lbl_inj_on_children[of l]
have "inj_on last_lbl ?lhs" by (auto simp: inj_on_def)
ultimately
have "card ?lhs = card (?skr - set_lbl l)" by (auto dest: card_image)
also have "… ≥ (card ?skr) - (card (set_lbl l))"
by (simp add: diff_card_le_card_Diff)
finally have "card ?lhs ≥ (card ?skr) - ?r"
using card_set_lbl[of l] by simp
moreover
from commR have "card ?skr > (N + f) div 2"
by (auto simp: EIG_commPerRd_def)
with not_leaf_length[OF l] f
have "(card ?skr) - ?r > (N - ?r) div 2" by auto
with card_children[OF l]
have "(card ?skr) - ?r > card (children l) div 2" by simp
ultimately show ?thesis by simp
qed
text ‹
If ‹l› is a non-leaf label such that all of its children corresponding
to well-heard processes at round ‹length_lbl l› have a uniform
‹newvals› decoration at round ‹f+1›, then ‹l›
itself is decorated with that same value.
›
lemma newvals_skr_uniform:
assumes run: "SHORun EIG_M rho HOs SHOs"
and commR: "EIG_commPerRd (HOs (length_lbl l)) (SHOs (length_lbl l))"
(is "EIG_commPerRd (HOs ?r) _")
and notleaf: "¬(is_leaf l)"
and unif: "⋀l'. ⟦l' ∈ children l;
last_lbl l' ∈ SKr (HOs (length_lbl l)) (SHOs (length_lbl l))
⟧ ⟹ newvals (rho (Suc f) p) l' = v"
shows "newvals (rho (Suc f) p) l = v"
proof -
from unif
have "card {l' ∈ children l. last_lbl l' ∈ SKr (HOs ?r) (SHOs ?r)}
≤ card {l' ∈ children l. newvals (rho (Suc f) p) l' = v}"
by (auto intro: card_mono)
with lynch_6_16_c[of HOs l SHOs, OF commR notleaf]
have maj: "has_majority v (newvals (rho (Suc f) p)) (children l)"
by (simp add: has_majority_def)
from run have "check_newvals (rho (Suc f) p)"
by (auto simp: EIG_SHOMachine_def SHORun_eq SHOnextConfig_eq
nextState_def EIG_nextState_def next_end_def)
with maj notleaf obtain w
where wmaj: "has_majority w (newvals (rho (Suc f) p)) (children l)"
and wupd: "newvals (rho (Suc f) p) l = w"
by (auto simp: check_newvals_def)
from maj wmaj have "w = v"
by (auto simp: has_majority_def elim: abs_majoritiesE')
with wupd show ?thesis by simp
qed
text ‹
A node whose label ‹l› ends with a process which is well heard
at round ‹length_lbl l› will have its ‹newvals› field set
(at round ‹f+1›) to the ``fixed-up'' value given by ‹vals›.
›
lemma lynch_6_16_d:
assumes run: "SHORun EIG_M rho HOs SHOs"
and commR: "∀r. EIG_commPerRd (HOs r) (SHOs r)"
and notroot: "l ∈ children t"
and skr: "last_lbl l ∈ SKr (HOs (length_lbl t)) (SHOs (length_lbl t))"
(is "_ ∈ SKr (HOs (?len t)) _")
shows "newvals (rho (Suc f) p) l = fixupval (vals (rho (?len l) p) l)"
(is "?P l")
using notroot skr proof (induct "Suc f - (?len l)" arbitrary: l t)
fix l t
assume "0 = Suc f - ?len l"
with length_lbl[of l] have leaf: "is_leaf l" by (simp add: is_leaf_def)
from run have "check_newvals (rho (Suc f) p)"
by (auto simp: EIG_SHOMachine_def SHORun_eq SHOnextConfig_eq
nextState_def EIG_nextState_def next_end_def)
with leaf show "?P l"
by (auto simp: check_newvals_def is_leaf_def)
next
fix k l t
assume ih: "⋀ l' t'.
⟦k = Suc f - length_lbl l'; l' ∈ children t';
last_lbl l' ∈ SKr (HOs (?len t')) (SHOs (?len t'))⟧
⟹ ?P l'"
and flk: "Suc k = Suc f - ?len l"
and notroot: "l ∈ children t"
and skr: "last_lbl l ∈ SKr (HOs (?len t)) (SHOs (?len t))"
let ?v = "fixupval (vals (rho (?len l) p) l)"
from flk have notlf: "¬(is_leaf l)" by (simp add: is_leaf_def)
{
fix l'
assume l': "l' ∈ children l"
and skr': "last_lbl l' ∈ SKr (HOs (?len l)) (SHOs (?len l))"
from run notroot skr l' skr'
have "vals (rho (?len l') p) l' = vals (rho (?len l) p) l"
by (rule lynch_6_16_a)
moreover
from flk l' have "k = Suc f - ?len l'" by (simp add: children_length)
from this l' skr' have "?P l'" by (rule ih)
ultimately
have "newvals (rho (Suc f) p) l' = ?v"
using notroot l' by (simp add: children_length)
}
with run commR notlf show "?P l" by (auto intro: newvals_skr_uniform)
qed
text ‹
Following Lynch~\<^cite>‹"lynch:distributed"›, we introduce some more useful
concepts for reasoning about the data structure.
›
text ‹
A label is \emph{common} if all processes agree on the final value it is
decorated with.
›
definition common where
"common rho l ≡
∀p q. newvals (rho (Suc f) p) l = newvals (rho (Suc f) q) l"
text ‹
The subtrees of a given label are all its possible extensions.
›
definition subtrees where
"subtrees h ≡ { l . ∃t. Rep_Label l = (Rep_Label h) @ t }"
lemma children_in_subtree:
assumes "l ∈ children h"
shows "l ∈ subtrees h"
using label_children[OF assms] by (auto simp: subtrees_def)
lemma subtrees_refl [iff]: "l ∈ subtrees l"
by (auto simp: subtrees_def)
lemma subtrees_root [iff]: "l ∈ subtrees root_node"
by (auto simp: subtrees_def)
lemma subtrees_trans:
assumes "l'' ∈ subtrees l'" and "l' ∈ subtrees l"
shows "l'' ∈ subtrees l"
using assms by (auto simp: subtrees_def)
lemma subtrees_antisym:
assumes "l ∈ subtrees l'" and "l' ∈ subtrees l"
shows "l' = l"
using assms by (auto simp: subtrees_def Rep_Label_inject)
lemma subtrees_tree:
assumes l': "l ∈ subtrees l'" and l'': "l ∈ subtrees l''"
shows "l' ∈ subtrees l'' ∨ l'' ∈ subtrees l'"
using assms proof (auto simp: subtrees_def append_eq_append_conv2)
fix xs
assume "Rep_Label l'' @ xs = Rep_Label l'"
hence "Rep_Label l' = Rep_Label l'' @ xs" by (rule sym)
thus "∃ys. Rep_Label l' = Rep_Label l'' @ ys" ..
qed
lemma subtrees_cases:
assumes l': "l' ∈ subtrees l"
and self: "l' = l ⟹ P"
and child: "⋀c. ⟦ c ∈ children l; l' ∈ subtrees c ⟧ ⟹ P"
shows "P"
proof -
from l' obtain t where t: "Rep_Label l' = (Rep_Label l) @ t"
by (auto simp: subtrees_def)
have "l' = l ∨ (∃c ∈ children l. l' ∈ subtrees c)"
proof (cases t)
assume "t = []"
with t show ?thesis by (simp add: Rep_Label_inject)
next
fix p t'
assume cons: "t = p # t'"
from Rep_Label[of l'] t have "length (Rep_Label l @ t) ≤ Suc f"
by (simp add: Label_def)
with cons have notleaf: "¬(is_leaf l)"
by (auto simp: is_leaf_def length_lbl_def)
let ?c = "Abs_Label (Rep_Label l @ [p])"
from t cons Rep_Label[of l'] have p: "p ∉ set_lbl l"
by (auto simp: Label_def set_lbl_def)
with notleaf have c: "?c ∈ children l"
by (auto simp: children_def)
moreover
from notleaf p have "Rep_Label l @ [p] ∈ Label"
by (simp add: Rep_Label_append)
hence "Rep_Label ?c = (Rep_Label l @ [p])"
by (simp add: Abs_Label_inverse)
with cons t have "l' ∈ subtrees ?c"
by (auto simp: subtrees_def)
ultimately show ?thesis by blast
qed
thus ?thesis by (auto elim!: self child)
qed
lemma subtrees_leaf:
assumes l: "is_leaf l" and l': "l' ∈ subtrees l"
shows "l' = l"
using l' proof (rule subtrees_cases)
fix c
assume "c ∈ children l"
with l show ?thesis by (simp add: children_def)
qed
lemma children_subtrees_equal:
assumes c: "c ∈ children l" and c': "c' ∈ children l"
and sub: "c' ∈ subtrees c"
shows "c' = c"
proof -
from assms have "Rep_Label c' = Rep_Label c"
by (auto simp: subtrees_def dest!: label_children)
thus ?thesis by (simp add: Rep_Label_inject)
qed
text ‹
A set ‹C› of labels is a \emph{subcovering} w.r.t. label ‹l›
if for all leaf subtrees ‹s› of ‹l› there
exists some label ‹h ∈ C› such that ‹s› is a subtree of
‹h› and ‹h› is a subtree of ‹l›.
›
definition subcovering where
"subcovering C l ≡
∀s ∈ subtrees l. is_leaf s ⟶ (∃h ∈ C. h ∈ subtrees l ∧ s ∈ subtrees h)"
text ‹
A \emph{covering} is a subcovering w.r.t. the root node.
›
abbreviation covering where
"covering C ≡ subcovering C root_node"
text ‹
The set of labels whose last element is well heard by all processes
throughout the execution forms a covering, and all these labels are common.
›
lemma lynch_6_18_a:
assumes "SHORun EIG_M rho HOs SHOs"
and "∀r. EIG_commPerRd (HOs r) (SHOs r)"
and "l ∈ children t"
and "last_lbl l ∈ SKr (HOs (length_lbl t)) (SHOs (length_lbl t))"
shows "common rho l"
using assms
by (auto simp: common_def lynch_6_16_d lynch_6_15
intro: arg_cong[where f="fixupval"])
lemma lynch_6_18_b:
assumes run: "SHORun EIG_M rho HOs SHOs"
and commG: "EIG_commGlobal HOs SHOs"
and commR: "∀r. EIG_commPerRd (HOs r) (SHOs r)"
shows "covering {l. ∃t. l ∈ children t ∧ last_lbl l ∈ (SK HOs SHOs)}"
proof (clarsimp simp: subcovering_def)
fix l
assume "is_leaf l"
with card_set_lbl[of l] have "card (set_lbl l) = Suc f"
by (simp add: is_leaf_def)
with commG have "N < card (SK HOs SHOs) + card (set_lbl l)"
by (simp add: EIG_commGlobal_def)
hence "∃q ∈ set_lbl l . q ∈ SK HOs SHOs"
by (auto dest: majorities_intersect)
then obtain l1 q l2 where
l: "Rep_Label l = (l1 @ [q]) @ l2" and q: "q ∈ SK HOs SHOs"
unfolding set_lbl_def by (auto intro: split_list_propE)
let ?h = "Abs_Label (l1 @ [q])"
from Rep_Label[of l] l have "l1 @ [q] ∈ Label" by (simp add: Label_def)
hence reph: "Rep_Label ?h = l1 @ [q]" by (rule Abs_Label_inverse)
hence "length_lbl ?h ≠ 0" by (simp add: length_lbl_def)
hence "?h ≠ root_node" by auto
then obtain t where t: "?h ∈ children t"
by (auto simp: root_iff_no_child)
moreover
from reph q have "last_lbl ?h ∈ SK HOs SHOs" by (simp add: last_lbl_def)
moreover
from reph l have "l ∈ subtrees ?h" by (simp add: subtrees_def)
ultimately
show "∃h. (∃t. h ∈ children t) ∧ last_lbl h ∈ SK HOs SHOs ∧ l ∈ subtrees h"
by blast
qed
text ‹
If ‹C› covers the subtree rooted at label ‹l› and if
‹l ∉ C› then ‹C› also covers subtrees rooted at
‹l›'s children.
›
lemma lynch_6_19_a:
assumes cov: "subcovering C l"
and l: "l ∉ C"
and e: "e ∈ children l"
shows "subcovering C e"
proof (clarsimp simp: subcovering_def)
fix s
assume s: "s ∈ subtrees e" and leaf: "is_leaf s"
from s children_in_subtree[OF e] have "s ∈ subtrees l"
by (rule subtrees_trans)
with leaf cov obtain h where h: "h ∈ C" "h ∈ subtrees l" "s ∈ subtrees h"
by (auto simp: subcovering_def)
with l obtain e' where e': "e' ∈ children l" "h ∈ subtrees e'"
by (auto elim: subtrees_cases)
from ‹s ∈ subtrees h› ‹h ∈ subtrees e'› have "s ∈ subtrees e'"
by (rule subtrees_trans)
with s have "e ∈ subtrees e' ∨ e' ∈ subtrees e"
by (rule subtrees_tree)
with e e' have "e' = e"
by (auto dest: children_subtrees_equal)
with e' h show "∃h∈C. h ∈ subtrees e ∧ s ∈ subtrees h" by blast
qed
text ‹
If there is a subcovering ‹C› for a label ‹l› such that all labels
in ‹C› are common, then ‹l› itself is common as well.
›
lemma lynch_6_19_b:
assumes run: "SHORun EIG_M rho HOs SHOs"
and cov: "subcovering C l"
and com: "∀l' ∈ C. common rho l'"
shows "common rho l"
using cov proof (induct "Suc f - length_lbl l" arbitrary: l)
fix l
assume 0: "0 = Suc f - length_lbl l"
and C: "subcovering C l"
from 0 length_lbl[of l] have "is_leaf l"
by (simp add: is_leaf_def)
with C obtain h where h: "h ∈ C" "h ∈ subtrees l" "l ∈ subtrees h"
by (auto simp: subcovering_def)
hence "l ∈ C" by (auto dest: subtrees_antisym)
with com show "common rho l" ..
next
fix k l
assume k: "Suc k = Suc f - length_lbl l"
and C: "subcovering C l"
and ih: "⋀l'. ⟦k = Suc f - length_lbl l'; subcovering C l'⟧ ⟹ common rho l'"
show "common rho l"
proof (cases "l ∈ C")
case True
with com show ?thesis ..
next
case False
with C have "∀e ∈ children l. subcovering C e"
by (blast intro: lynch_6_19_a)
moreover
from k have "∀e ∈ children l. k = Suc f - length_lbl e"
by (auto simp: children_length)
ultimately
have com_ch: "∀e ∈ children l. common rho e"
by (blast intro: ih)
show ?thesis
proof (clarsimp simp: common_def)
fix p q
from k have notleaf: "¬(is_leaf l)" by (simp add: is_leaf_def)
let ?r = "Suc f"
from com_ch
have "∀e ∈ children l. newvals (rho ?r p) e = newvals (rho ?r q) e"
by (auto simp: common_def)
hence "∀w. {e ∈ children l. newvals (rho ?r p) e = w}
= {e ∈ children l. newvals (rho ?r q) e = w}"
by auto
moreover
from run
have "check_newvals (rho ?r p)" "check_newvals (rho ?r q)"
by (auto simp: EIG_SHOMachine_def SHORun_eq SHOnextConfig_eq nextState_def
EIG_nextState_def next_end_def)
with notleaf have
"(∃w. has_majority w (newvals (rho ?r p)) (children l)
∧ newvals (rho ?r p) l = w)
∨ ¬(∃w. has_majority w (newvals (rho ?r p)) (children l))
∧ newvals (rho ?r p) l = undefined"
"(∃w. has_majority w (newvals (rho ?r q)) (children l)
∧ newvals (rho ?r q) l = w)
∨ ¬(∃w. has_majority w (newvals (rho ?r q)) (children l))
∧ newvals (rho ?r q) l = undefined"
by (auto simp: check_newvals_def)
ultimately show "newvals (rho ?r p) l = newvals (rho ?r q) l"
by (auto simp: has_majority_def elim: abs_majoritiesE')
qed
qed
qed
text ‹The root of the tree is a common node.›
lemma lynch_6_20:
assumes run: "SHORun EIG_M rho HOs SHOs"
and commG: "EIG_commGlobal HOs SHOs"
and commR: "∀r. EIG_commPerRd (HOs r) (SHOs r)"
shows "common rho root_node"
using run lynch_6_18_b[OF assms]
proof (rule lynch_6_19_b, clarify)
fix l t
assume "l ∈ children t" "last_lbl l ∈ SK HOs SHOs"
thus "common rho l" by (auto simp: SK_def elim: lynch_6_18_a[OF run commR])
qed
text ‹
A decision is taken only at state ‹f+1› and then stays stable.
›
lemma decide:
assumes run: "SHORun EIG_M rho HOs SHOs"
shows "decide (rho r p) =
(if r < Suc f then None
else Some (newvals (rho (Suc f) p) root_node))"
(is "?P r")
proof (induct r)
from run show "?P 0"
by (auto simp: EIG_SHOMachine_def SHORun_eq HOinitConfig_eq
initState_def EIG_initState_def)
next
fix r
assume ih: "?P r"
from run obtain μp
where "EIG_nextState r p (rho r p) μp (rho (Suc r) p)"
by (auto simp: EIG_SHOMachine_def SHORun_eq SHOnextConfig_eq
nextState_def)
thus "?P (Suc r)"
proof (auto simp: EIG_nextState_def next_main_def next_end_def)
assume "¬(r < f)" "r ≠ f"
with ih
show "decide (rho r p) = Some (newvals (rho (Suc f) p) root_node)"
by simp
qed
qed
subsection ‹Proof of Agreement, Validity, and Termination›
text ‹
The Agreement property is an immediate consequence of lemma ‹lynch_6_20›.
›
theorem Agreement:
assumes run: "SHORun EIG_M rho HOs SHOs"
and commG: "EIG_commGlobal HOs SHOs"
and commR: "∀r. EIG_commPerRd (HOs r) (SHOs r)"
and p: "decide (rho m p) = Some v"
and q: "decide (rho n q) = Some w"
shows "v = w"
using p q lynch_6_20[OF run commG commR]
by (auto simp: decide[OF run] common_def)
text ‹
We now show the Validity property: if all processes initially
propose the same value ‹v›, then no other value may be decided.
By lemma ‹sho_correct_vals›, value ‹v› must propagate to
all children of the root that are well heard at round ‹0›, and
lemma ‹lynch_6_16_d› implies that ‹v› is the value assigned
to all these children by ‹newvals›. Finally, lemma
‹newvals_skr_uniform› lets us conclude.
›
theorem Validity:
assumes run: "SHORun EIG_M rho HOs SHOs"
and commR: "∀r. EIG_commPerRd (HOs r) (SHOs r)"
and initv: "∀q. the (vals (rho 0 q) root_node) = v"
and dp: "decide (rho r p) = Some w"
shows "v = w"
proof -
have v: "∀q. vals (rho 0 q) root_node = Some v"
proof
fix q
from run have "vals (rho 0 q) root_node ≠ None"
by (auto simp: EIG_SHOMachine_def SHORun_eq HOinitConfig_eq
initState_def EIG_initState_def)
then obtain w where w: "vals (rho 0 q) root_node = Some w"
by auto
from initv have "the (vals (rho 0 q) root_node) = v" ..
with w show "vals (rho 0 q) root_node = Some v" by simp
qed
let ?len = length_lbl
let ?r = "Suc f"
{
fix l'
assume l': "l' ∈ children root_node"
and skr: "last_lbl l' ∈ SKr (HOs 0) (SHOs 0)"
with run v have "vals (rho (?len l') p) l' = Some v"
by (auto dest: sho_correct_vals simp: SKr_def)
moreover
from run commR l' skr
have "newvals (rho ?r p) l' = fixupval (vals (rho (?len l') p) l')"
by (auto intro: lynch_6_16_d)
ultimately
have "newvals (rho ?r p) l' = v" by simp
}
with run commR root_node_not_leaf
have "newvals (rho ?r p) root_node = v"
by (auto intro: newvals_skr_uniform)
with dp show ?thesis by (simp add: decide[OF run])
qed
text ‹Termination is trivial for \eigbyz{}.›
theorem Termination:
assumes "SHORun EIG_M rho HOs SHOs"
shows "∃r v. decide (rho r p) = Some v"
using assms by (auto simp: decide)
subsection ‹\eigbyz{} Solves Weak Consensus›
text ‹
Summing up, all (coarse-grained) runs of \eigbyz{} for
HO and SHO collections that satisfy the communication predicate
satisfy the Weak Consensus property.
›
theorem eig_weak_consensus:
assumes run: "SHORun EIG_M rho HOs SHOs"
and commR: "∀r. EIG_commPerRd (HOs r) (SHOs r)"
and commG: "EIG_commGlobal HOs SHOs"
shows "weak_consensus (λp. the (vals (rho 0 p) root_node)) decide rho"
unfolding weak_consensus_def
using Validity[OF run commR]
Agreement[OF run commG commR]
Termination[OF run]
by auto
text ‹
By the reduction theorem, the correctness of the algorithm carries over
to the fine-grained model of runs.
›
theorem eig_weak_consensus_fg:
assumes run: "fg_run EIG_M rho HOs SHOs (λr q. undefined)"
and commR: "∀r. EIG_commPerRd (HOs r) (SHOs r)"
and commG: "EIG_commGlobal HOs SHOs"
shows "weak_consensus (λp. the (vals (state (rho 0) p) root_node))
decide (state ∘ rho)"
(is "weak_consensus ?inits _ _")
proof (rule local_property_reduction[OF run weak_consensus_is_local])
fix crun
assume crun: "CSHORun EIG_M crun HOs SHOs (λr q. undefined)"
and init: "crun 0 = state (rho 0)"
from crun have "SHORun EIG_M crun HOs SHOs" by (unfold SHORun_def)
from this commR commG
have "weak_consensus (λp. the (vals (crun 0 p) root_node)) decide crun"
by (rule eig_weak_consensus)
with init show "weak_consensus ?inits decide crun"
by (simp add: o_def)
qed
end