Theory UteProof
theory UteProof
imports UteDefs "../Majorities" "../Reduction"
begin
context ute_parameters
begin
subsection ‹Preliminary Lemmas›
text ‹Processes can make a vote only at first round of each phase.›
lemma vote_step:
assumes nxt: "nextState Ute_M r p (rho r p) μ (rho (Suc r) p)"
and "vote (rho (Suc r) p) ≠ None"
shows "step r = 0"
proof (rule ccontr)
assume "step r ≠ 0"
with assms have "vote (rho (Suc r) p) = None"
by (auto simp:Ute_SHOMachine_def nextState_def Ute_nextState_def next1_def)
with assms show False by auto
qed
text ‹Processes can make a new decision only at second round of each phase.›
lemma decide_step:
assumes run: "SHORun Ute_M rho HOs SHOs"
and d1: "decide (rho r p) ≠ Some v"
and d2: "decide (rho (Suc r) p) = Some v"
shows "step r ≠ 0"
proof
assume sr:"step r = 0"
from run obtain μ where "Ute_nextState r p (rho r p) μ (rho (Suc r) p)"
unfolding Ute_SHOMachine_def nextState_def SHORun_eq SHOnextConfig_eq
by force
with sr have "next0 r p (rho r p) μ (rho (Suc r) p)"
unfolding Ute_nextState_def by auto
hence "decide (rho r p) = decide (rho (Suc r) p)"
by (auto simp:next0_def)
with d1 d2 show False by auto
qed
lemma unique_majority_E:
assumes majv: "card {qq::Proc. F qq = Some m} > E"
and majw: "card {qq::Proc. F qq = Some m'} > E"
shows "m = m'"
proof -
from majv majw majE
have "card {qq::Proc. F qq = Some m} > N div 2"
and "card {qq::Proc. F qq = Some m'} > N div 2"
by auto
then obtain qq
where "qq ∈ {qq::Proc. F qq = Some m}"
and "qq ∈ {qq::Proc. F qq = Some m'}"
by (rule majoritiesE')
thus ?thesis by auto
qed
lemma unique_majority_E_α:
assumes majv: "card {qq::Proc. F qq = m} > E - α"
and majw: "card {qq::Proc. F qq = m'} > E - α"
shows "m = m'"
proof -
from majE alpha_lt_N majv majw
have "card {qq::Proc. F qq = m} > N div 2"
and "card {qq::Proc. F qq = m'} > N div 2"
by auto
then obtain qq
where "qq ∈ {qq::Proc. F qq = m}"
and "qq ∈ {qq::Proc. F qq = m'}"
by (rule majoritiesE')
thus ?thesis by auto
qed
lemma unique_majority_T:
assumes majv: "card {qq::Proc. F qq = Some m} > T"
and majw: "card {qq::Proc. F qq = Some m'} > T"
shows "m = m'"
proof -
from majT majv majw
have "card {qq::Proc. F qq = Some m} > N div 2"
and "card {qq::Proc. F qq = Some m'} > N div 2"
by auto
then obtain qq
where "qq ∈ {qq::Proc. F qq = Some m}"
and "qq ∈ {qq::Proc. F qq = Some m'}"
by (rule majoritiesE')
thus ?thesis by auto
qed
text ‹No two processes may vote for different values in the same round.›
lemma common_vote:
assumes usafe: "SHOcommPerRd Ute_M HO SHO"
and nxtp: "nextState Ute_M r p (rho r p) μp (rho (Suc r) p)"
and mup: "μp ∈ SHOmsgVectors Ute_M r p (rho r) (HO p) (SHO p)"
and nxtq: "nextState Ute_M r q (rho r q) μq (rho (Suc r) q)"
and muq: "μq ∈ SHOmsgVectors Ute_M r q (rho r) (HO q) (SHO q)"
and vp: "vote (rho (Suc r) p) = Some vp"
and vq: "vote (rho (Suc r) q) = Some vq"
shows "vp = vq"
using assms proof -
have gtn: "card {qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
+ card {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq} > N"
proof -
have "card {qq. sendMsg Ute_M r qq p (rho r qq) = Val vp} > T - α
∧ card {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq} > T - α"
(is "card ?vsentp > _ ∧ card ?vsentq > _")
proof -
from nxtp vp have stp:"step r = 0" by (auto simp: vote_step)
from mup
have "{qq. μp qq = Some (Val vp)} - (HO p - SHO p)
⊆ {qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}"
(is "?vrcvdp - ?ahop ⊆ ?vsentp")
by (auto simp: SHOmsgVectors_def)
hence "card (?vrcvdp - ?ahop) ≤ card ?vsentp"
and "card (?vrcvdp - ?ahop) ≥ card ?vrcvdp - card ?ahop"
by (auto simp: card_mono diff_card_le_card_Diff)
hence "card ?vsentp ≥ card ?vrcvdp - card ?ahop" by auto
moreover
from nxtp stp have "next0 r p (rho r p) μp (rho (Suc r) p)"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
with vp have "card ?vrcvdp > T"
unfolding next0_def by auto
moreover
from muq
have "{qq. μq qq = Some (Val vq)} - (HO q - SHO q)
⊆ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq}"
(is "?vrcvdq - ?ahoq ⊆ ?vsentq")
by (auto simp: SHOmsgVectors_def)
hence "card (?vrcvdq - ?ahoq) ≤ card ?vsentq"
and "card (?vrcvdq - ?ahoq) ≥ card ?vrcvdq - card ?ahoq"
by (auto simp: card_mono diff_card_le_card_Diff)
hence "card ?vsentq ≥ card ?vrcvdq - card ?ahoq" by auto
moreover
from nxtq stp have "next0 r q (rho r q) μq (rho (Suc r) q)"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
with vq have "card {qq. μq qq = Some (Val vq)} > T"
by (unfold next0_def, auto)
moreover
from usafe have "card ?ahop ≤ α" and "card ?ahoq ≤ α"
by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
ultimately
show ?thesis using alpha_lt_T by auto
qed
thus ?thesis using majT by auto
qed
show ?thesis
proof (rule ccontr)
assume vpq:"vp ≠ vq"
have "∀qq. sendMsg Ute_M r qq p (rho r qq)
= sendMsg Ute_M r qq q (rho r qq)"
by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def
step_def send0_def send1_def)
with vpq
have "{qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
∩ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq} = {}"
by auto
with gtn
have "card ({qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
∪ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq}) > N"
by (auto simp: card_Un_Int)
moreover
have "card ({qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
∪ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq}) ≤ N"
by (auto simp: card_mono)
ultimately
show "False" by auto
qed
qed
text ‹
No decision may be taken by a process unless it received enough messages
holding the same value.
›
lemma decide_with_threshold_E:
assumes run: "SHORun Ute_M rho HOs SHOs"
and usafe: "SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and d1: "decide (rho r p) ≠ Some v"
and d2: "decide (rho (Suc r) p) = Some v"
shows "card {q. sendMsg Ute_M r q p (rho r q) = Vote (Some v)}
> E - α"
proof -
from run obtain μp
where nxt:"nextState Ute_M r p (rho r p) μp (rho (Suc r) p)"
and "∀qq. qq ∈ HOs r p ⟷ μp qq ≠ None"
and "∀qq. qq ∈ SHOs r p ∩ HOs r p
⟶ μp qq = Some (sendMsg Ute_M r qq p (rho r qq))"
unfolding Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq SHOmsgVectors_def
by blast
hence "{qq. μp qq = Some (Vote (Some v))} - (HOs r p - SHOs r p)
⊆ {qq. sendMsg Ute_M r qq p (rho r qq) = Vote (Some v)}"
(is "?vrcvdp - ?ahop ⊆ ?vsentp") by auto
hence "card (?vrcvdp - ?ahop) ≤ card ?vsentp"
and "card (?vrcvdp - ?ahop) ≥ card ?vrcvdp - card ?ahop"
by (auto simp: card_mono diff_card_le_card_Diff)
hence "card ?vsentp ≥ card ?vrcvdp - card ?ahop" by auto
moreover
from usafe have "card (HOs r p - SHOs r p) ≤ α"
by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
moreover
from run d1 d2 have "step r ≠ 0" by (rule decide_step)
with nxt have "next1 r p (rho r p) μp (rho (Suc r) p)"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
with run d1 d2 have "card {qq. μp qq = Some (Vote (Some v))} > E"
unfolding next1_def by auto
ultimately
show ?thesis using alpha_lt_E by auto
qed
subsection ‹Proof of Agreement and Validity›
text ‹
If more than ‹E - α› messages holding ‹v› are sent to
some process ‹p› at round ‹r›, then every process ‹pp›
correctly receives more than ‹α› such messages.
›
lemma common_x_argument_1:
assumes usafe:"SHOcommPerRd Ute_M (HOs (Suc r)) (SHOs (Suc r))"
and threshold: "card {q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
= Vote (Some v)} > E - α"
(is "card (?msgs p v) > _")
shows "card (?msgs pp v ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)) > α"
proof -
have "card (?msgs pp v) + card (SHOs (Suc r) pp ∩ HOs (Suc r) pp) > N + α"
proof -
have "∀q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
= sendMsg Ute_M (Suc r) q pp (rho (Suc r) q)"
by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def
step_def send0_def send1_def)
moreover
from usafe
have "card (SHOs (Suc r) pp ∩ HOs (Suc r) pp) > N + 2*α - E - 1"
by (auto simp: Ute_SHOMachine_def step_def Ute_commPerRd_def)
ultimately
show ?thesis using threshold by auto
qed
moreover
have "card (?msgs pp v) + card (SHOs (Suc r) pp ∩ HOs (Suc r) pp)
= card (?msgs pp v ∪ (SHOs (Suc r) pp ∩ HOs (Suc r) pp))
+ card (?msgs pp v ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp))"
by (auto intro: card_Un_Int)
moreover
have "card (?msgs pp v ∪ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)) ≤ N"
by (auto simp: card_mono)
ultimately
show ?thesis by auto
qed
text ‹
If more than ‹E - α› messages holding ‹v› are sent to ‹p›
at some round ‹r›, then any process ‹pp› will set its ‹x› to
value ‹v› in ‹r›.
›
lemma common_x_argument_2:
assumes run: "SHORun Ute_M rho HOs SHOs"
and usafe: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and nxtpp: "nextState Ute_M (Suc r) pp (rho (Suc r) pp)
μpp (rho (Suc (Suc r)) pp)"
and mupp: "μpp ∈ SHOmsgVectors Ute_M (Suc r) pp (rho (Suc r))
(HOs (Suc r) pp) (SHOs (Suc r) pp)"
and threshold: "card {q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
= Vote (Some v)} > E - α"
(is "card (?sent p v) > _")
shows "x (rho (Suc (Suc r)) pp) = v"
proof -
have stp:"step (Suc r) ≠ 0"
proof
assume sr: "step (Suc r) = 0"
hence "∀q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
= Val (x (rho (Suc r) q))"
by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def send0_def)
moreover
from threshold obtain qq where
"sendMsg Ute_M (Suc r) qq p (rho (Suc r) qq) = Vote (Some v)"
by force
ultimately
show False by simp
qed
have va: "card {qq. μpp qq = Some (Vote (Some v))} > α"
(is "card (?msgs v) > α")
proof -
from mupp
have "SHOs (Suc r) pp ∩ HOs (Suc r) pp
⊆ {qq. μpp qq = Some (sendMsg Ute_M (Suc r) qq pp (rho (Suc r) qq))}"
unfolding SHOmsgVectors_def by auto
moreover
hence "(?msgs v) ⊇ (?sent pp v) ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)"
by auto
hence "card (?msgs v)
≥ card ((?sent pp v) ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp))"
by (auto intro: card_mono)
moreover
from usafe threshold
have alph:"card ((?sent pp v) ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)) > α"
by (blast dest: common_x_argument_1)
ultimately
show ?thesis by auto
qed
moreover
from nxtpp stp
have "next1 (Suc r) pp (rho (Suc r) pp) μpp (rho (Suc (Suc r)) pp)"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
ultimately
obtain w where wa:"card (?msgs w) > α" and xw:"x (rho (Suc (Suc r)) pp) = w"
unfolding next1_def by auto
have "v = w"
proof -
note usafe
moreover
obtain qv where "qv ∈ SHOs (Suc r) pp" and "μpp qv = Some (Vote (Some v))"
proof -
have "¬ (?msgs v ⊆ HOs (Suc r) pp - SHOs (Suc r) pp)"
proof
assume "?msgs v ⊆ HOs (Suc r) pp - SHOs (Suc r) pp"
hence "card (?msgs v) ≤ card ((HOs (Suc r) pp) - (SHOs (Suc r) pp))"
by (auto simp: card_mono)
moreover
from usafe
have "card (HOs (Suc r) pp - SHOs (Suc r) pp) ≤ α"
by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
moreover
note va
ultimately
show False by auto
qed
then obtain qv
where "qv ∉ HOs (Suc r) pp - SHOs (Suc r) pp"
and qsv:"μpp qv = Some (Vote (Some v))"
by auto
with mupp have "qv ∈ SHOs (Suc r) pp"
unfolding SHOmsgVectors_def by auto
with qsv that show ?thesis by auto
qed
with stp mupp have "vote (rho (Suc r) qv) = Some v"
by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def
Ute_sendMsg_def send1_def)
moreover
obtain qw where
"qw ∈ SHOs (Suc r) pp" and "μpp qw = Some (Vote (Some w))"
proof -
have "¬ (?msgs w ⊆ HOs (Suc r) pp - SHOs (Suc r) pp)"
proof
assume "?msgs w ⊆ HOs (Suc r) pp - SHOs (Suc r) pp"
hence "card (?msgs w) ≤ card ((HOs (Suc r) pp) - (SHOs (Suc r) pp))"
by (auto simp: card_mono)
moreover
from usafe
have "card (HOs (Suc r) pp - SHOs (Suc r) pp) ≤ α"
by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
moreover
note wa
ultimately
show False by auto
qed
then obtain qw
where "qw ∉ HOs (Suc r) pp - SHOs (Suc r) pp"
and qsw: "μpp qw = Some (Vote (Some w))"
by auto
with mupp have "qw ∈ SHOs (Suc r) pp"
unfolding SHOmsgVectors_def by auto
with qsw that show ?thesis by auto
qed
with stp mupp have "vote (rho (Suc r) qw) = Some w"
by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def
Ute_sendMsg_def send1_def)
moreover
from run obtain μqv μqw
where "nextState Ute_M r qv ((rho r) qv) μqv (rho (Suc r) qv)"
and "μqv ∈ SHOmsgVectors Ute_M r qv (rho r) (HOs r qv) (SHOs r qv)"
and "nextState Ute_M r qw ((rho r) qw) μqw (rho (Suc r) qw)"
and "μqw ∈ SHOmsgVectors Ute_M r qw (rho r) (HOs r qw) (SHOs r qw)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq) blast
ultimately
show ?thesis using usafe by (auto dest: common_vote)
qed
with xw show "x (rho (Suc (Suc r)) pp) = v" by auto
qed
text ‹
Inductive argument for the agreement and validity theorems.
›
lemma safety_inductive_argument:
assumes run: "SHORun Ute_M rho HOs SHOs"
and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and ih: "E - α < card {q. sendMsg Ute_M r' q p (rho r' q) = Vote (Some v)}"
and stp1: "step r' = Suc 0"
shows "E - α <
card {q. sendMsg Ute_M (Suc (Suc r')) q p (rho (Suc (Suc r')) q)
= Vote (Some v)}"
proof -
from stp1 have "r' > 0" by (auto simp: step_def)
with stp1 obtain r where rr':"r' = Suc r" and stpr:"step (Suc r) = Suc 0"
by (auto dest: gr0_implies_Suc)
have "∀pp. x (rho (Suc (Suc r)) pp) = v"
proof
fix pp
from run obtain μpp
where "μpp ∈ SHOmsgVectors Ute_M r' pp (rho r') (HOs r' pp) (SHOs r' pp)"
and "nextState Ute_M r' pp (rho r' pp) μpp (rho (Suc r') pp)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
with run comm ih rr' show "x (rho (Suc (Suc r)) pp) = v"
by (auto dest: common_x_argument_2)
qed
with run stpr
have "∀pp p. sendMsg Ute_M (Suc (Suc r)) pp p (rho (Suc (Suc r)) pp) = Val v"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq
Ute_sendMsg_def send0_def mod_Suc step_def)
with rr'
have "⋀p μp'. μp' ∈ SHOmsgVectors Ute_M (Suc r') p (rho (Suc r'))
(HOs (Suc r') p) (SHOs (Suc r') p)
⟹ SHOs (Suc r') p ∩ HOs (Suc r') p
⊆ {q. μp' q = Some (Val v)}"
by (auto simp: SHOmsgVectors_def)
hence "⋀p μp'. μp' ∈ SHOmsgVectors Ute_M (Suc r') p (rho (Suc r'))
(HOs (Suc r') p) (SHOs (Suc r') p)
⟹ card (SHOs (Suc r') p ∩ HOs (Suc r') p)
≤ card {q. μp' q = Some (Val v)}"
by (auto simp: card_mono)
moreover
from comm have "⋀p. T < card (SHOs (Suc r') p ∩ HOs (Suc r') p)"
by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
ultimately
have vT:"⋀p μp'. μp' ∈ SHOmsgVectors Ute_M (Suc r') p (rho (Suc r'))
(HOs (Suc r') p) (SHOs (Suc r') p)
⟹ T < card {q. μp' q = Some (Val v)}"
by (auto dest: less_le_trans)
show ?thesis
proof -
have "∀pp. vote ((rho (Suc (Suc r'))) pp) = Some v"
proof
fix pp
from run obtain μpp
where nxtpp: "nextState Ute_M (Suc r') pp (rho (Suc r') pp) μpp
(rho (Suc (Suc r')) pp)"
and mupp: "μpp ∈ SHOmsgVectors Ute_M (Suc r') pp (rho (Suc r'))
(HOs (Suc r') pp) (SHOs (Suc r') pp)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
with vT have vT':"card {q. μpp q = Some (Val v)} > T"
by auto
moreover
from stpr rr' have "step (Suc r') = 0"
by (auto simp: mod_Suc step_def)
with nxtpp
have "next0 (Suc r') pp (rho (Suc r') pp) μpp (rho (Suc (Suc r')) pp)"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
ultimately
obtain w
where wT:"card {q. μpp q = Some (Val w)} > T"
and votew:"vote (rho (Suc (Suc r')) pp) = Some w"
by (auto simp: next0_def)
from vT' wT have "v = w"
by (auto dest: unique_majority_T)
with votew show "vote (rho (Suc (Suc r')) pp) = Some v" by simp
qed
with run stpr rr'
have "∀p. N = card {q. sendMsg Ute_M (Suc (Suc (Suc r))) q p
((rho (Suc (Suc (Suc r)))) q) = Vote (Some v)}"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq
Ute_sendMsg_def send1_def step_def mod_Suc)
with rr' majE EltN show ?thesis by auto
qed
qed
text ‹
A process that holds some decision ‹v› has decided ‹v›
sometime in the past.
›
lemma decisionNonNullThenDecided:
assumes run:"SHORun Ute_M rho HOs SHOs" and dec: "decide (rho n p) = Some v"
shows "∃m<n. decide (rho (Suc m) p) ≠ decide (rho m p)
∧ decide (rho (Suc m) p) = Some v"
proof -
let "?dec k" = "decide ((rho k) p)"
have "(∀m<n. ?dec (Suc m) ≠ ?dec m ⟶ ?dec (Suc m) ≠ Some v)
⟶ ?dec n ≠ Some v"
(is "?P n" is "?A n ⟶ _")
proof (induct n)
from run show "?P 0"
by (auto simp: Ute_SHOMachine_def SHORun_eq HOinitConfig_eq
initState_def Ute_initState_def)
next
fix n
assume ih: "?P n" thus "?P (Suc n)" by force
qed
with dec show ?thesis by auto
qed
text ‹
If process ‹p1› has decided value ‹v1› and process
‹p2› later decides, then ‹p2› must decide ‹v1›.
›
lemma laterProcessDecidesSameValue:
assumes run:"SHORun Ute_M rho HOs SHOs"
and comm:"∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and dv1:"decide (rho (Suc r) p1) = Some v1"
and dn2:"decide (rho (r + k) p2) ≠ Some v2"
and dv2:"decide (rho (Suc (r + k)) p2) = Some v2"
shows "v2 = v1"
proof -
from run dv1 obtain r1
where r1r:"r1 < Suc r"
and dn1:"decide (rho r1 p1) ≠ Some v1"
and dv1':"decide (rho (Suc r1) p1) = Some v1"
by (auto dest: decisionNonNullThenDecided)
from r1r obtain s where rr1:"Suc r = Suc (r1 + s)"
by (auto dest: less_imp_Suc_add)
then obtain k' where kk':"r + k = r1 + k'"
by auto
with dn2 dv2
have dn2': "decide (rho (r1 + k') p2) ≠ Some v2"
and dv2': "decide (rho (Suc (r1 + k')) p2) = Some v2"
by auto
from run dn1 dv1' dn2' dv2'
have rs0:"step r1 = Suc 0" and rks0:"step (r1 + k') = Suc 0"
by (auto simp: mod_Suc step_def dest: decide_step)
have "step (r1 + k') = step (step r1 + k')"
unfolding step_def by (simp add: mod_add_left_eq)
with rs0 rks0 have "step k' = 0" by (auto simp: step_def mod_Suc)
then obtain k'' where "k' = k''*nSteps" by (auto simp: step_def)
with dn2' dv2'
have dn2'':"decide (rho (r1 + k''*nSteps) p2) ≠ Some v2"
and dv2'':"decide (rho (Suc (r1 + k''*nSteps)) p2) = Some v2"
by auto
from rs0 have stp:"step (r1 + k''*nSteps) = Suc 0"
unfolding step_def by auto
have inv:"card {q. sendMsg Ute_M (r1 + k''*nSteps) q p1 (rho (r1 + k''*nSteps) q)
= Vote (Some v1)} > E - α"
proof (induct k'')
from stp have "step (r1 + 0*nSteps) = Suc 0"
by (auto simp: step_def)
from run comm dn1 dv1'
show "card {q. sendMsg Ute_M (r1 + 0*nSteps) q p1 (rho (r1 + 0*nSteps) q)
= Vote (Some v1)} > E - α"
by (intro decide_with_threshold_E) auto
next
fix k''
assume ih: "E - α <
card {q. sendMsg Ute_M (r1 + k''*nSteps) q p1 (rho (r1 + k''*nSteps) q)
= Vote (Some v1)}"
from rs0 have stps: "step (r1 + k''*nSteps) = Suc 0"
by (auto simp: step_def)
with run comm ih
have "E - α <
card {q. sendMsg Ute_M (Suc (Suc (r1 + k''*nSteps))) q p1
(rho (Suc (Suc (r1 + k''*nSteps))) q)
= Vote (Some v1)}"
by (rule safety_inductive_argument)
thus "E - α <
card {q. sendMsg Ute_M (r1 + Suc k'' * nSteps) q p1
(rho (r1 + Suc k'' * nSteps) q)
= Vote (Some v1)}"
by auto
qed
moreover
from run
have "∀q. sendMsg Ute_M (r1 + k''*nSteps) q p1 (rho (r1 + k''*nSteps) q)
= sendMsg Ute_M (r1 + k''*nSteps) q p2 (rho (r1 + k''*nSteps) q)"
by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def
step_def send0_def send1_def)
moreover
from run comm dn2'' dv2''
have "E - α <
card {q. sendMsg Ute_M (r1 + k''*nSteps) q p2 (rho (r1 + k''*nSteps) q)
= Vote (Some v2)}"
by (auto dest: decide_with_threshold_E)
ultimately
show "v2 = v1" by (auto dest: unique_majority_E_α)
qed
text ‹
The Agreement property is an immediate consequence of the two
preceding lemmas.
›
theorem ute_agreement:
assumes run: "SHORun Ute_M rho HOs SHOs"
and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and p: "decide (rho m p) = Some v"
and q: "decide (rho n q) = Some w"
shows "v = w"
proof -
from run p obtain k
where k1: "decide (rho (Suc k) p) ≠ decide (rho k p)"
and k2: "decide (rho (Suc k) p) = Some v"
by (auto dest: decisionNonNullThenDecided)
from run q obtain l
where l1: "decide (rho (Suc l) q) ≠ decide (rho l q)"
and l2: "decide (rho (Suc l) q) = Some w"
by (auto dest: decisionNonNullThenDecided)
show ?thesis
proof (cases "k ≤ l")
case True
then obtain m where m: "l = k+m" by (auto simp add: le_iff_add)
from run comm k2 l1 l2 m have "w = v"
by (auto elim!: laterProcessDecidesSameValue)
thus ?thesis by simp
next
case False
hence "l ≤ k" by simp
then obtain m where m: "k = l+m" by (auto simp add: le_iff_add)
from run comm l2 k1 k2 m show ?thesis
by (auto elim!: laterProcessDecidesSameValue)
qed
qed
text ‹
Main lemma for the proof of the Validity property.
›
lemma validity_argument:
assumes run: "SHORun Ute_M rho HOs SHOs"
and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and init: "∀p. x ((rho 0) p) = v"
and dw: "decide (rho r p) = Some w"
and stp: "step r' = Suc 0"
shows "card {q. sendMsg Ute_M r' q p (rho r' q) = Vote (Some v)} > E - α"
proof -
define k where "k = r' div nSteps"
with stp have stp: "r' = Suc 0 + k * nSteps"
using div_mult_mod_eq [of r' nSteps]
by (simp add: step_def)
moreover
have "E - α <
card {q. sendMsg Ute_M (Suc 0 + k*nSteps) q p ((rho (Suc 0 + k*nSteps)) q)
= Vote (Some v)}"
proof (induct k)
have "∀pp. vote ((rho (Suc 0)) pp) = Some v"
proof
fix pp
from run obtain μpp
where nxtpp:"nextState Ute_M 0 pp (rho 0 pp) μpp (rho (Suc 0) pp)"
and mupp:"μpp ∈ SHOmsgVectors Ute_M 0 pp (rho 0) (HOs 0 pp) (SHOs 0 pp)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
have majv:"card {q. μpp q = Some (Val v)} > T"
proof -
from run init have "∀q. sendMsg Ute_M 0 q pp (rho 0 q) = Val v"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq
Ute_sendMsg_def send0_def step_def)
moreover
from comm have shoT:"card (SHOs 0 pp ∩ HOs 0 pp) > T"
by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
moreover
from mupp
have "SHOs 0 pp ∩ HOs 0 pp
⊆ {q. μpp q = Some (sendMsg Ute_M 0 q pp (rho 0 q))}"
by (auto simp: SHOmsgVectors_def)
hence "card (SHOs 0 pp ∩ HOs 0 pp)
≤ card {q. μpp q = Some (sendMsg Ute_M 0 q pp (rho 0 q))}"
by (auto simp: card_mono)
ultimately
show ?thesis by (auto simp: less_le_trans)
qed
moreover
from nxtpp have "next0 0 pp ((rho 0) pp) μpp (rho (Suc 0) pp)"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def step_def)
ultimately
obtain w where majw:"card {q. μpp q = Some (Val w)} > T"
and votew:"vote (rho (Suc 0) pp) = Some w"
by (auto simp: next0_def)
from majv majw have "v = w" by (auto dest: unique_majority_T)
with votew show "vote ((rho (Suc 0)) pp) = Some v" by simp
qed
with run
have "card {q. sendMsg Ute_M (Suc 0) q p (rho (Suc 0) q) = Vote (Some v)} = N"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq
Ute_nextState_def step_def Ute_sendMsg_def send1_def)
thus "E - α <
card {q. sendMsg Ute_M (Suc 0 + 0 * nSteps) q p (rho (Suc 0 + 0 * nSteps) q)
= Vote (Some v)}"
using majE EltN by auto
next
fix k
assume ih:"E - α <
card {q. sendMsg Ute_M (Suc 0 + k * nSteps) q p (rho (Suc 0 + k * nSteps) q)
= Vote (Some v)}"
have "step (Suc 0 + k * nSteps) = Suc 0"
by (auto simp: mod_Suc step_def)
from run comm ih this
have "E - α <
card {q. sendMsg Ute_M (Suc (Suc (Suc 0 + k * nSteps))) q p
(rho (Suc (Suc (Suc 0 + k * nSteps))) q)
= Vote (Some v)}"
by (rule safety_inductive_argument)
thus "E - α <
card {q. sendMsg Ute_M (Suc 0 + Suc k * nSteps) q p
(rho (Suc 0 + Suc k * nSteps) q)
= Vote (Some v)}" by simp
qed
ultimately
show ?thesis by simp
qed
text ‹
The following theorem shows the Validity property of algorithm \ute{}.
›
theorem ute_validity:
assumes run: "SHORun Ute_M rho HOs SHOs"
and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and init: "∀p. x (rho 0 p) = v"
and dw: "decide (rho r p) = Some w"
shows "v = w"
proof -
from run dw obtain r1
where dnr1:"decide ((rho r1) p) ≠ Some w"
and dwr1:"decide ((rho (Suc r1)) p) = Some w"
by (force dest: decisionNonNullThenDecided)
with run have "step r1 ≠ 0" by (rule decide_step)
hence "step r1 = Suc 0" by (simp add: step_def mod_Suc)
with assms
have "E - α <
card {q. sendMsg Ute_M r1 q p (rho r1 q) = Vote (Some v)}"
by (rule validity_argument)
moreover
from run comm dnr1 dwr1
have "card {q. sendMsg Ute_M r1 q p (rho r1 q) = Vote (Some w)} > E - α"
by (auto dest: decide_with_threshold_E)
ultimately
show "v = w" by (auto dest: unique_majority_E_α)
qed
subsection ‹Proof of Termination›
text ‹
At the second round of a phase that satisfies the conditions expressed in
the global communication predicate, processes update their ‹x› variable
with the value ‹v› they receive in more than ‹α› messages.
›
lemma set_x_from_vote:
assumes run: "SHORun Ute_M rho HOs SHOs"
and comm: "SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and stp: "step (Suc r) = Suc 0"
and π: "∀p. HOs (Suc r) p = SHOs (Suc r) p"
and nxt: "nextState Ute_M (Suc r) p (rho (Suc r) p) μ (rho (Suc (Suc r)) p)"
and mu: "μ ∈ SHOmsgVectors Ute_M (Suc r) p (rho (Suc r))
(HOs (Suc r) p) (SHOs (Suc r) p)"
and vp: "α < card {qq. μ qq = Some (Vote (Some v))}"
shows "x ((rho (Suc (Suc r))) p) = v"
proof -
from nxt stp vp obtain wp
where xwp:"α < card {qq. μ qq = Some (Vote (Some wp))}"
and xp:"x (rho (Suc (Suc r)) p) = wp"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def next1_def)
have "wp = v"
proof -
from xwp obtain pp where smw:"μ pp = Some (Vote (Some wp))"
by force
have "vote (rho (Suc r) pp) = Some wp"
proof -
from smw mu π
have "μ pp = Some (sendMsg Ute_M (Suc r) pp p (rho (Suc r) pp))"
unfolding SHOmsgVectors_def by force
with stp have "μ pp = Some (Vote (vote (rho (Suc r) pp)))"
by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def send1_def)
with smw show ?thesis by auto
qed
moreover
from vp obtain qq where smv:"μ qq = Some (Vote (Some v))"
by force
have "vote (rho (Suc r) qq) = Some v"
proof -
from smv mu π
have "μ qq = Some (sendMsg Ute_M (Suc r) qq p (rho (Suc r) qq))"
unfolding SHOmsgVectors_def by force
with stp have "μ qq = Some (Vote (vote (rho (Suc r) qq)))"
by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def send1_def)
with smv show ?thesis by auto
qed
moreover
from run obtain μpp μqq
where "nextState Ute_M r pp (rho r pp) μpp (rho (Suc r) pp)"
and "μpp ∈ SHOmsgVectors Ute_M r pp (rho r) (HOs r pp) (SHOs r pp)"
and "nextState Ute_M r qq ((rho r) qq) μqq (rho (Suc r) qq)"
and "μqq ∈ SHOmsgVectors Ute_M r qq (rho r) (HOs r qq) (SHOs r qq)"
unfolding Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq by blast
ultimately
show ?thesis using comm by (auto dest: common_vote)
qed
with xp show ?thesis by simp
qed
text ‹
Assume that HO and SHO sets are uniform at the second step of some
phase. Then at the subsequent round there exists some value ‹v›
such that any received message which is not corrupted holds ‹v›.
›
lemma termination_argument_1:
assumes run: "SHORun Ute_M rho HOs SHOs"
and comm: "SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and stp: "step (Suc r) = Suc 0"
and π: "∀p. π0 = HOs (Suc r) p ∧ π0 = SHOs (Suc r) p"
obtains v where
"⋀p μp' q.
⟦ q ∈ SHOs (Suc (Suc r)) p ∩ HOs (Suc (Suc r)) p;
μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r)) p (rho (Suc (Suc r)))
(HOs (Suc (Suc r)) p) (SHOs (Suc (Suc r)) p)
⟧ ⟹ μp' q = (Some (Val v))"
proof -
from π have hosho:"∀p. SHOs (Suc r) p = SHOs (Suc r) p ∩ HOs (Suc r) p"
by simp
have "⋀p q. x (rho (Suc (Suc r)) p) = x (rho (Suc (Suc r)) q)"
proof -
fix p q
from run obtain μp
where nxt: "nextState Ute_M (Suc r) p (rho (Suc r) p)
μp (rho (Suc (Suc r)) p)"
and mu: "μp ∈ SHOmsgVectors Ute_M (Suc r) p (rho (Suc r))
(HOs (Suc r) p) (SHOs (Suc r) p)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
from run obtain μq
where nxtq: "nextState Ute_M (Suc r) q (rho (Suc r) q)
μq (rho (Suc (Suc r)) q)"
and muq: "μq ∈ SHOmsgVectors Ute_M (Suc r) q (rho (Suc r))
(HOs (Suc r) q) (SHOs (Suc r) q)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
have "∀qq. μp qq = μq qq"
proof
fix qq
show "μp qq = μq qq"
proof (cases "μp qq = None")
case False
with mu π have 1:"qq ∈ SHOs (Suc r) p" and 2:"qq ∈ SHOs (Suc r) q"
unfolding SHOmsgVectors_def by auto
from mu π 1
have "μp qq = Some (sendMsg Ute_M (Suc r) qq p (rho (Suc r) qq))"
unfolding SHOmsgVectors_def by auto
moreover
from muq π 2
have "μq qq = Some (sendMsg Ute_M (Suc r) qq q (rho (Suc r) qq))"
unfolding SHOmsgVectors_def by auto
ultimately
show ?thesis
by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def step_def
send0_def send1_def)
next
case True
with mu have "qq ∉ HOs (Suc r) p" unfolding SHOmsgVectors_def by auto
with π muq have "μq qq = None" unfolding SHOmsgVectors_def by auto
with True show ?thesis by simp
qed
qed
hence vsets:"⋀v. {qq. μp qq = Some (Vote (Some v))}
= {qq. μq qq = Some (Vote (Some v))}"
by auto
show "x (rho (Suc (Suc r)) p) = x (rho (Suc (Suc r)) q)"
proof (cases "∃v. α < card {qq. μp qq = Some (Vote (Some v))}", clarify)
fix v
assume vp: "α < card {qq. μp qq = Some (Vote (Some v))}"
with run comm stp π nxt mu have "x (rho (Suc (Suc r)) p) = v"
by (auto dest: set_x_from_vote)
moreover
from vsets vp
have "α < card {qq. μq qq = Some (Vote (Some v))}" by auto
with run comm stp π nxtq muq have "x (rho (Suc (Suc r)) q) = v"
by (auto dest: set_x_from_vote)
ultimately
show "x (rho (Suc (Suc r)) p) = x (rho (Suc (Suc r)) q)"
by auto
next
assume nov: "¬ (∃v. α < card {qq. μp qq = Some (Vote (Some v))})"
with nxt stp have "x (rho (Suc (Suc r)) p) = undefined"
by (auto simp: Ute_SHOMachine_def nextState_def
Ute_nextState_def next1_def)
moreover
from vsets nov
have "¬ (∃v. α < card {qq. μq qq = Some (Vote (Some v))})" by auto
with nxtq stp have "x (rho (Suc (Suc r)) q) = undefined"
by (auto simp: Ute_SHOMachine_def nextState_def
Ute_nextState_def next1_def)
ultimately
show ?thesis by simp
qed
qed
then obtain v where "⋀q. x (rho (Suc (Suc r)) q) = v" by blast
moreover
from stp have "step (Suc (Suc r)) = 0"
by (auto simp: step_def mod_Suc)
hence "⋀p μp' q.
⟦ q ∈ SHOs (Suc (Suc r)) p ∩ HOs (Suc (Suc r)) p;
μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r)) p (rho (Suc (Suc r)))
(HOs (Suc (Suc r)) p) (SHOs (Suc (Suc r)) p)
⟧ ⟹ μp' q = Some (Val (x (rho (Suc (Suc r)) q)))"
by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def Ute_sendMsg_def send0_def)
ultimately
have "⋀p μp' q.
⟦ q ∈ SHOs (Suc (Suc r)) p ∩ HOs (Suc (Suc r)) p;
μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r)) p (rho (Suc (Suc r)))
(HOs (Suc (Suc r)) p) (SHOs (Suc (Suc r)) p)
⟧ ⟹ μp' q = (Some (Val v))"
by auto
with that show thesis by blast
qed
text ‹
If a process ‹p› votes ‹v› at some round ‹r›,
then all messages received by ‹p› in ‹r› that are not
corrupted hold ‹v›.
›
lemma termination_argument_2:
assumes mup: "μp ∈ SHOmsgVectors Ute_M (Suc r) p (rho (Suc r))
(HOs (Suc r) p) (SHOs (Suc r) p)"
and nxtq: "nextState Ute_M r q (rho r q) μq (rho (Suc r) q)"
and vq: "vote (rho (Suc r) q) = Some v"
and qsho: "q ∈ SHOs (Suc r) p ∩ HOs (Suc r) p"
shows "μp q = Some (Vote (Some v))"
proof -
from nxtq vq have "step r = 0" by (auto simp: vote_step)
with mup qsho have "μp q = Some (Vote (vote (rho (Suc r) q)))"
by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def Ute_sendMsg_def
step_def send1_def mod_Suc)
with vq show "μp q = Some (Vote (Some v))" by auto
qed
text‹
We now prove the Termination property.
›
theorem ute_termination:
assumes run: "SHORun Ute_M rho HOs SHOs"
and commR: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and commG: "SHOcommGlobal Ute_M HOs SHOs"
shows "∃r v. decide (rho r p) = Some v"
proof -
from commG
obtain Φ π r0
where rr: "r0 = Suc (nSteps * Φ)"
and π: "∀p. π = HOs r0 p ∧ π = SHOs r0 p"
and t: "∀p. card (SHOs (Suc r0) p ∩ HOs (Suc r0) p) > T"
and e: "∀p. card (SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p) > E"
by (auto simp: Ute_SHOMachine_def Ute_commGlobal_def Let_def)
from rr have stp:"step r0 = Suc 0" by (auto simp: step_def)
obtain w where votew:"∀p. (vote (rho (Suc (Suc r0)) p)) = Some w"
proof -
have abc:"∀p. ∃w. vote (rho (Suc (Suc r0)) p) = Some w"
proof
fix p
from run stp obtain μp
where nxt:"nextState Ute_M (Suc r0) p (rho (Suc r0) p) μp
(rho (Suc (Suc r0)) p)"
and mup:"μp ∈ SHOmsgVectors Ute_M (Suc r0) p (rho (Suc r0))
(HOs (Suc r0) p) (SHOs (Suc r0) p)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
have "∃v. T < card {qq. μp qq = Some (Val v)}"
proof -
from t have "card (SHOs (Suc r0) p ∩ HOs (Suc r0) p) > T" ..
moreover
from run commR stp π rr
obtain v where
"⋀p μp' q.
⟦ q ∈ SHOs (Suc r0) p ∩ HOs (Suc r0) p;
μp' ∈ SHOmsgVectors Ute_M (Suc r0) p (rho (Suc r0))
(HOs (Suc r0) p) (SHOs (Suc r0) p)
⟧ ⟹ μp' q = Some (Val v)"
using termination_argument_1 by blast
with mup obtain v where
"⋀qq. qq ∈ SHOs (Suc r0) p ∩ HOs (Suc r0) p ⟹ μp qq = Some (Val v)"
by auto
hence "SHOs (Suc r0) p ∩ HOs (Suc r0) p ⊆ {qq. μp qq = Some (Val v)}"
by auto
hence "card (SHOs (Suc r0) p ∩ HOs (Suc r0) p)
≤ card {qq. μp qq = Some (Val v)}"
by (auto intro: card_mono)
ultimately
have "T < card {qq. μp qq = Some (Val v)}" by auto
thus ?thesis by auto
qed
with stp nxt show "∃w. vote ((rho (Suc (Suc r0))) p) = Some w"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def
step_def mod_Suc next0_def)
qed
then obtain qq w where qqw:"vote (rho (Suc (Suc r0)) qq) = Some w"
by blast
have "∀pp. vote (rho (Suc (Suc r0)) pp) = Some w"
proof
fix pp
from abc obtain wp where pwp:"vote ((rho (Suc (Suc r0))) pp) = Some wp"
by blast
from run obtain μpp μqq
where nxtp: "nextState Ute_M (Suc r0) pp (rho (Suc r0) pp)
μpp (rho (Suc (Suc r0)) pp)"
and mup: "μpp ∈ SHOmsgVectors Ute_M (Suc r0) pp (rho (Suc r0))
(HOs (Suc r0) pp) (SHOs (Suc r0) pp)"
and nxtq: "nextState Ute_M (Suc r0) qq (rho (Suc r0) qq)
μqq (rho (Suc (Suc r0)) qq)"
and muq: "μqq ∈ SHOmsgVectors Ute_M (Suc r0) qq (rho (Suc r0))
(HOs (Suc r0) qq) (SHOs (Suc r0) qq)"
unfolding Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq by blast
from commR this pwp qqw have "wp = w"
by (auto dest: common_vote)
with pwp show "vote ((rho (Suc (Suc r0))) pp) = Some w"
by auto
qed
with that show ?thesis by auto
qed
from run obtain μp'
where nxtp: "nextState Ute_M (Suc (Suc r0)) p (rho (Suc (Suc r0)) p)
μp' (rho (Suc (Suc (Suc r0))) p)"
and mup': "μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r0)) p (rho (Suc (Suc r0)))
(HOs (Suc (Suc r0)) p) (SHOs (Suc (Suc r0)) p)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
have "⋀qq. qq ∈ SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p
⟹ μp' qq = Some (Vote (Some w))"
proof -
fix qq
assume qqsho:"qq ∈ SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p"
from run obtain μqq where
nxtqq:"nextState Ute_M (Suc r0) qq (rho (Suc r0) qq)
μqq (rho (Suc (Suc r0)) qq)"
by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
from commR mup' nxtqq votew qqsho show "μp' qq = Some (Vote (Some w))"
by (auto dest: termination_argument_2)
qed
hence "SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p
⊆ {qq. μp' qq = Some (Vote (Some w))}"
by auto
hence wsho: "card (SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p)
≤ card {qq. μp' qq = Some (Vote (Some w))}"
by (auto simp: card_mono)
from stp have "step (Suc (Suc r0)) = Suc 0"
unfolding step_def by auto
with nxtp have "next1 (Suc (Suc r0)) p (rho (Suc (Suc r0)) p) μp'
(rho (Suc (Suc (Suc r0))) p)"
by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
moreover
from e have "E < card (SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p)"
by auto
with wsho have majv:"card {qq. μp' qq = Some (Vote (Some w))} > E"
by auto
ultimately
show ?thesis by (auto simp: next1_def)
qed
subsection ‹\ute{} Solves Weak Consensus›
text ‹
Summing up, all (coarse-grained) runs of \ute{} for
HO and SHO collections that satisfy the communication predicate
satisfy the Weak Consensus property.
›
theorem ute_weak_consensus:
assumes run: "SHORun Ute_M rho HOs SHOs"
and commR: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and commG: "SHOcommGlobal Ute_M HOs SHOs"
shows "weak_consensus (x ∘ (rho 0)) decide rho"
unfolding weak_consensus_def
using ute_validity[OF run commR]
ute_agreement[OF run commR]
ute_termination[OF run commR commG]
by auto
text ‹
By the reduction theorem, the correctness of the algorithm carries over
to the fine-grained model of runs.
›
theorem ute_weak_consensus_fg:
assumes run: "fg_run Ute_M rho HOs SHOs (λr q. undefined)"
and commR: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
and commG: "SHOcommGlobal Ute_M HOs SHOs"
shows "weak_consensus (λp. x (state (rho 0) p)) decide (state ∘ rho)"
(is "weak_consensus ?inits _ _")
proof (rule local_property_reduction[OF run weak_consensus_is_local])
fix crun
assume crun: "CSHORun Ute_M crun HOs SHOs (λr q. undefined)"
and init: "crun 0 = state (rho 0)"
from crun have "SHORun Ute_M crun HOs SHOs" by (unfold SHORun_def)
from this commR commG
have "weak_consensus (x ∘ (crun 0)) decide crun"
by (rule ute_weak_consensus)
with init show "weak_consensus ?inits decide crun"
by (simp add: o_def)
qed
end
end