Theory FLPSystem
section‹FLPSystem›
text ‹
\file{FLPSystem} extends \file{AsynchronousSystem} with concepts of consensus
and decisions. It develops a concept of non-uniformity regarding pending
decision possibilities, where non-uniform configurations can always
reach other non-uniform ones.
›
theory FLPSystem
imports AsynchronousSystem ListUtilities
begin
subsection‹Locale for the FLP consensus setting›
locale flpSystem =
asynchronousSystem trans sends start
for trans :: "'p ⇒ 's ⇒ 'v messageValue ⇒'s"
and sends :: "'p ⇒ 's ⇒ 'v messageValue ⇒ ('p, 'v) message multiset"
and start :: "'p ⇒ 's" +
assumes finiteProcs: "finite Proc"
and minimalProcs: "card Proc ≥ 2"
and finiteSends: "finite {v. v ∈# (sends p s m)}"
and noInSends: "sends p s m <p2, inM v> = 0"
begin
subsection‹Decidedness and uniformity of configurations›
abbreviation vDecided ::
"bool ⇒ ('p, 'v, 's) configuration ⇒ bool"
where
"vDecided v cfg ≡ initReachable cfg ∧ (<⊥, outM v> ∈# msgs cfg)"
abbreviation decided ::
"('p, 'v, 's) configuration ⇒ bool"
where
"decided cfg ≡ (∃v . vDecided v cfg)"
definition pSilDecVal ::
"bool ⇒ 'p ⇒ ('p, 'v, 's) configuration ⇒ bool"
where
"pSilDecVal v p c ≡ initReachable c ∧
(∃ c'::('p, 'v, 's) configuration . (withoutQReachable c {p} c')
∧ vDecided v c')"
abbreviation pSilentDecisionValues ::
"'p ⇒ ('p, 'v, 's) configuration ⇒ bool set" ("val[_,_]")
where
"val[p, c] ≡ {v. pSilDecVal v p c}"
definition vUniform ::
"bool ⇒ ('p, 'v, 's) configuration ⇒ bool"
where
"vUniform v c ≡ initReachable c ∧ (∀p. val[p,c] = {v})"
abbreviation nonUniform ::
"('p, 'v, 's) configuration ⇒ bool"
where
"nonUniform c ≡ initReachable c ∧
¬(vUniform False c) ∧
¬(vUniform True c)"
subsection‹Agreement, validity, termination›
text‹
Völzer defines consensus in terms of the classical notions
of agreement, validity, and termination. The proof then mostly applies a
weakened notion of termination, which we refer to as ,,pseudo termination''.
›
definition agreement ::
"('p, 'v, 's) configuration ⇒ bool"
where
"agreement c ≡
(∀v1. (<⊥, outM v1> ∈# msgs c)
⟶ (∀v2. (<⊥, outM v2> ∈# msgs c)
⟷ v2 = v1))"
definition agreementInit ::
"('p, 'v, 's) configuration ⇒ ('p, 'v, 's) configuration ⇒ bool"
where
"agreementInit i c ≡
initial i ∧ reachable i c ⟶
(∀v1. (<⊥, outM v1> ∈# msgs c)
⟶ (∀v2. (<⊥, outM v2> ∈# msgs c)
⟷ v2 = v1))"
definition validity ::
"('p, 'v, 's) configuration ⇒ ('p, 'v, 's) configuration ⇒ bool"
where
"validity i c ≡
initial i ∧ reachable i c ⟶
(∀v. (<⊥, outM v> ∈# msgs c)
⟶ (∃p. (<p, inM v> ∈# msgs i)))"
text‹
The termination concept which is implied by the concept of "pseudo-consensus"
in the paper.
›
definition terminationPseudo ::
"nat ⇒ ('p, 'v, 's) configuration ⇒ 'p set ⇒ bool"
where
"terminationPseudo t c Q ≡ ((initReachable c ∧ card Q + t ≥ card Proc)
⟶ (∃c'. qReachable c Q c' ∧ decided c'))"
subsection ‹Propositions about decisions›
text‹
For every process \var{p} and every configuration that is reachable from an
initial configuration (i.e. \isb{initReachable} \var{c}) we have
$\var{val(p,c)} \neq \emptyset$.
This follows directly from the definition of \var{val} and the definition of
\isb{terminationPseudo}, which has to be assumed to ensure that there is a
reachable configuration that is decided.
\voelzer{Proposition 2(a)}
›
lemma DecisionValuesExist:
fixes
c :: "('p, 'v, 's) configuration" and
p :: "'p"
assumes
Termination: "⋀cc Q . terminationPseudo 1 cc Q" and
Reachable: "initReachable c"
shows
"val[p,c] ≠ {}"
proof -
from Termination
have "(initReachable c ∧ card Proc ≤ card (UNIV - {p}) + 1)
⟶ (∃c'. qReachable c (UNIV-{p}) c' ∧ initReachable c'
∧ (∃v. 0 < msgs c' <⊥, outM v>))"
unfolding terminationPseudo_def by simp
with Reachable minimalProcs finiteProcs
have "∃c'. qReachable c (UNIV - {p}) c' ∧ initReachable c'
∧ (∃v. 0 < msgs c' <⊥, outM v>)"
unfolding terminationPseudo_def initReachable_def by simp
thus ?thesis
unfolding pSilDecVal_def
using Reachable by auto
qed
text‹
The lemma \isb{DecidedImpliesUniform} proves that every \isb{vDecided}
configuration \var{c} is also \isb{vUniform}. Völzer claims that this
follows directly from the definitions of \isb{vDecided} and \isb{vUniform}.
But this is not quite enough: One must also assume \isb{terminationPseudo}
and \isb{agreement} for all reachable configurations.
\voelzer{Proposition 2(b)}
›
lemma DecidedImpliesUniform:
fixes
c :: "('p, 'v, 's) configuration" and
v :: "bool"
assumes
AllAgree: "∀ cfg . reachable c cfg ⟶ agreement cfg" and
Termination: "⋀cc Q . terminationPseudo 1 cc Q" and
VDec: "vDecided v c"
shows
"vUniform v c"
using AllAgree VDec unfolding agreement_def vUniform_def pSilDecVal_def
proof simp
assume
Agree: "∀cfg. reachable c cfg ⟶
(∀v1. 0 < msgs cfg <⊥, outM v1>
⟶ (∀v2. (0 < msgs cfg <⊥, outM v2>) = (v2 = v1)))" and
vDec: "initReachable c ∧ 0 < msgs c <⊥, outM v>"
show
"(∀p. {v. ∃c'. qReachable c (Proc - {p}) c' ∧ initReachable c' ∧
0 < msgs c' <⊥, outM v>} = {v})"
proof clarify
fix p
have "val[p,c] ≠ {}" using Termination DecisionValuesExist vDec
by simp
hence NotEmpty: "{v. ∃c'. qReachable c (UNIV - {p}) c'
∧ initReachable c' ∧ 0 < msgs c' <⊥, outM v>} ≠ {}"
using pSilDecVal_def by simp
have U: "∀ u . u ∈ {v. ∃c'. qReachable c (UNIV - {p}) c'
∧ initReachable c' ∧ 0 < msgs c' <⊥, outM v>} ⟶ (u = v)"
proof clarify
fix u c'
assume "qReachable c (UNIV - {p}) c'" "initReachable c'"
hence Reach: "reachable c c'" using QReachImplReach by simp
from VDec have Msg: "0 < msgs c <⊥, outM v>" by simp
from Reach NoOutMessageLoss have
"msgs c <⊥, outM v> ≤ msgs c' <⊥, outM v>" by simp
with Msg have VMsg: "0 < msgs c' <⊥, outM v>"
using NoOutMessageLoss Reach by (metis less_le_trans)
assume "0 < msgs c' <⊥, outM u>"
with Agree VMsg Reach show "u = v" by simp
qed
thus " {v. ∃c'. qReachable c (UNIV - {p}) c' ∧ initReachable c' ∧
0 < msgs c' <⊥, outM v>} = {v}" using NotEmpty U by auto
qed
qed
corollary NonUniformImpliesNotDecided:
fixes
c :: "('p, 'v, 's) configuration" and
v :: "bool"
assumes
"∀ cfg . reachable c cfg ⟶ agreement cfg"
"⋀cc Q . terminationPseudo 1 cc Q"
"nonUniform c"
"vDecided v c"
shows
"False"
using DecidedImpliesUniform[OF assms(1,2,4)] assms(3)
by (cases v, simp_all)
text‹
All three parts of Völzer's Proposition 3 consider a single step from an
arbitrary \isb{initReachable} configuration \var{c} with a message
$\var{msg}$ to a succeeding configuration \var{c'}.
›
text‹
The silent decision values of a process which is not active in a step only
decrease or stay the same.
This follows directly from the definitions and the transitivity of the
reachability properties \isb{reachable} and \isb{qReachable}.
\voelzer{Proposition 3(a)}
›
lemma InactiveProcessSilentDecisionValuesDecrease:
fixes
p q :: 'p and
c c' :: "('p, 'v, 's) configuration" and
msg :: "('p, 'v) message"
assumes
"p ≠ q" and
"c ⊢ msg ↦ c'" and
"isReceiverOf p msg" and
"initReachable c"
shows
"val[q,c'] ⊆ val[q,c]"
proof(auto simp add: pSilDecVal_def assms(4))
fix x cfg'
assume
Msg: "0 < msgs cfg' <⊥, outM x>" and
Cfg': "qReachable c' (Proc - {q}) cfg'"
have "initReachable c'"
using assms initReachable_def reachable.simps
by blast
hence Init: "initReachable cfg'"
using Cfg' initReachable_def QReachImplReach[of c' "(Proc - {q})" cfg']
ReachableTrans by blast
have "p ∈ Proc - {q}"
using assms by blast
hence "qReachable c (Proc - {q}) c'"
using assms qReachable.simps by metis
hence "qReachable c (Proc - {q}) cfg'"
using Cfg' QReachableTrans
by blast
with Msg Init show
"∃c'a. qReachable c (Proc - {q}) c'a
∧ initReachable c'a ∧
0 < msgs c'a <⊥, outM x>" by blast
qed
text‹
...while the silent decision values of the process which is active in
a step may only increase or stay the same.
This follows as stated in \<^cite>‹"Voelzer"› from the \emph{diamond property}
for a reachable configuration and a single step, i.e. \isb{DiamondTwo},
and in addition from the fact that output messages cannot get lost, i.e.
\isb{NoOutMessageLoss}.
\voelzer{Proposition 3(b)}
›
lemma ActiveProcessSilentDecisionValuesIncrease :
fixes
p q :: 'p and
c c' :: "('p, 'v, 's) configuration" and
msg :: "('p, 'v) message"
assumes
"p = q" and
"c ⊢ msg ↦ c'" and
"isReceiverOf p msg" and
"initReachable c"
shows "val[q,c] ⊆ val[q,c']"
proof (auto simp add: pSilDecVal_def assms(4))
from assms initReachable_def reachable.simps show "initReachable c'"
by meson
fix x cv
assume Cv: "qReachable c (Proc - {q}) cv" "initReachable cv"
"0 < msgs cv <⊥, outM x>"
have "∃c'a. (cv ⊢ msg ↦ c'a) ∧ qReachable c' (Proc - {q}) c'a"
using DiamondTwo Cv(1) assms
by blast
then obtain c'' where C'': "(cv ⊢ msg ↦ c'')"
"qReachable c' (Proc - {q}) c''" by auto
with Cv(2) initReachable_def reachable.simps
have Init: "initReachable c''" by blast
have "reachable cv c''" using C''(1) reachable.intros by blast
hence "msgs cv <⊥, outM x> ≤ msgs c'' <⊥, outM x>" using NoOutMessageLoss
by simp
hence "0 < msgs c'' <⊥, outM x>" using Cv(3) by auto
thus "∃c'a. qReachable c' (Proc - {q}) c'a
∧ initReachable c'a ∧ 0 < msgs c'a <⊥, outM x>"
using C''(2) Init by blast
qed
text‹
As a result from the previous two propositions, the silent decision values
of a process cannot go from {0} to {1} or vice versa in a step.
This is a slightly more generic version of Proposition 3 (c) from
\<^cite>‹"Voelzer"› since it is proven for both values, while Völzer is only
interested in the situation starting with $\var{val(q,c) = \{0\}}$.
\voelzer{Proposition 3(c)}
›
lemma SilentDecisionValueNotInverting:
fixes
p q :: 'p and
c c' :: "('p, 'v, 's) configuration" and
msg :: "('p, 'v) message" and
v :: bool
assumes
Val: "val[q,c] = {v}" and
Step: "c ⊢ msg ↦ c'" and
Rec: "isReceiverOf p msg" and
Init: "initReachable c"
shows
"val[q,c'] ≠ {¬ v}"
proof(cases "p = q")
case False
hence "val[q,c'] ⊆ val[q,c]"
using Step Rec InactiveProcessSilentDecisionValuesDecrease Init by simp
with Val show "val[q,c'] ≠ {¬ v}" by auto
next
case True
hence "val[q,c] ⊆ val[q,c']"
using Step Rec ActiveProcessSilentDecisionValuesIncrease Init by simp
with Val show "val[q,c'] ≠ {¬ v}" by auto
qed
subsection‹Towards a proof of FLP›
text‹
There is an \isb{initial} configuration that is \isb{nonUniform} under
the assumption of \isb{validity}, \isb{agreement} and \isb{terminationPseudo}.
The lemma is used in the proof of the main theorem to construct the
\isb{non\-Uni\-form} and \isb{initial} configuration that leads to the
final contradiction.
\voelzer{Lemma 1}
›
lemma InitialNonUniformCfg:
assumes
Termination: "⋀cc Q . terminationPseudo 1 cc Q" and
Validity: "∀ i c . validity i c" and
Agreement: "∀ i c . agreementInit i c"
shows
"∃ cfg . initial cfg ∧ nonUniform cfg"
proof-
obtain n::nat where N: "n = card Proc" by blast
hence "∃ procList::('p list). length procList = n ∧ set procList = Proc
∧ distinct procList"
using finiteProcs
by (metis distinct_card finite_distinct_list)
then obtain procList where
ProcList: "length procList = n" "set procList = Proc"
"distinct procList" by blast
have AllPInProclist: "∀p. ∃i<n. procList ! i = p"
using ProcList N
proof auto
fix p
assume Asm: "set procList = Proc" "length procList = card Proc"
have "p ∈ set procList" using ProcList by auto
with Asm in_set_conv_nth
show "∃i<card Proc. procList ! i = p" by metis
qed
have NGr0: "n > 0"
using N finiteProcs minimalProcs by auto
define initMsg :: "nat ⇒ ('p, 'v) message ⇒ nat"
where "initMsg ind m = (if ∃p. m = <p, inM (∃i<ind. procList!i = p)> then 1 else 0)" for ind m
define initCfgList
where "initCfgList = map (λind. ⦇states = start, msgs = initMsg ind⦈) [0..<(n+1)]"
have InitCfgLength: "length initCfgList = n + 1"
unfolding initCfgList_def by auto
have InitCfgNonEmpty: "initCfgList ≠ []"
unfolding initCfgList_def by auto
hence InitCfgStart: "(∀c ∈ set initCfgList. states c = start)"
unfolding initCfgList_def by auto
have InitCfgSet: "set initCfgList =
{x. ∃ind < n+1. x = ⦇states = start, msgs = initMsg ind⦈}"
unfolding initCfgList_def
proof auto
fix ind
assume "ind < n"
hence "∃inda<Suc n. inda = ind ∧ initMsg ind = initMsg inda" by auto
thus "∃inda<Suc n. initMsg ind = initMsg inda" by blast
next
fix ind
assume Asm:
"⦇states = start, msgs = initMsg ind⦈ ∉ (λind::nat. ⦇states = start, msgs = initMsg ind⦈) ` {0..<n}"
"ind < Suc n"
hence "ind ≥ n" by auto
with Asm have "ind = n" by auto
thus "initMsg ind = initMsg n" by auto
qed
have InitInitial: "∀c ∈ set initCfgList . initial c"
unfolding initial_def initCfgList_def initMsg_def using InitCfgStart
by auto
with InitCfgSet have InitInitReachable:
"∀ c ∈ set initCfgList . initReachable c"
using reachable.simps
unfolding initReachable_def
by blast
define c0 where "c0 = initCfgList ! 0"
hence "c0 = ⦇ states = start, msgs = initMsg 0 ⦈"
using InitCfgLength nth_map_upt[of 0 "n+1" 0]
unfolding initCfgList_def by auto
hence MsgC0: "msgs c0 = (λm. if ∃p. m = <p, inM False> then 1 else 0)"
unfolding initMsg_def by simp
define cN where "cN = initCfgList ! n"
hence "cN = ⦇ states = start, msgs = initMsg n⦈"
using InitCfgLength nth_map_upt[of n "n+1" 0]
unfolding initCfgList_def
by auto
hence MsgCN: "msgs cN = (λm. if ∃p. m = <p, inM True> then 1 else 0)"
unfolding initMsg_def
using AllPInProclist
by auto
have C0NotCN: "c0 ≠ cN"
proof
assume "c0 = cN"
hence StrangeEq: "(λm::('p, 'v) message.
if ∃p. m = <p, inM False> then 1 else 0 :: nat) =
(λm. if ∃p. m = <p, inM True> then 1 else 0)"
using InitCfgLength N minimalProcs MsgC0 MsgCN
unfolding c0_def cN_def by auto
thus "False"
by (metis message.inject(1) zero_neq_one)
qed
have C0NAreUniform: "⋀ cX . (cX = c0) ∨ (cX = cN)
⟹ vUniform (cX = cN) cX"
proof-
fix cX
assume xIs0OrN: "(cX = c0) ∨ (cX = cN)"
have xInit: "initial cX"
using InitCfgLength InitCfgSet set_conv_nth[of initCfgList] xIs0OrN
unfolding c0_def cN_def
by (auto simp add: InitInitial)
from Validity
have COnlyReachesOneDecision:
"∀ c . reachable cX c ∧ decided c ⟶ (vDecided (cX = cN) c)"
unfolding validity_def initReachable_def
proof auto
fix c cfg0 v
assume
Validity: "(∀i c. ((initial i) ∧ (reachable i c)) ⟶
(∀v. (0 < msgs c (<⊥, outM v>))
⟶ (∃p. (0 < msgs i (<p, inM v>)))))" and
OutMsg: "0 < msgs c <⊥, outM v>" and
InitCXReachable: "reachable cX c"
thus "0 < msgs c <⊥, outM (cX = cN)>"
using xIs0OrN
proof (cases "v = (cX = cN)", simp)
assume "v ≠ (cX = cN)"
hence vDef: "v = (cX ≠ cN)" by auto
with Validity InitCXReachable OutMsg xInit
have ExistMsg: "∃p. (0 < msgs cX (<p, inM (cX ≠ cN)>))" by auto
with initMsg_def have False
using xIs0OrN
by (auto simp add: MsgC0 MsgCN C0NotCN)
thus "0 < msgs c <⊥, outM cX = cN>" by simp
qed
qed
have InitRInitC: "initReachable cX" using xInit InitialIsInitReachable
by auto
have NoWrongDecs: "⋀ v p cc::('p, 'v, 's) configuration.
qReachable cX (Proc - {p}) cc ∧ initReachable cc
∧ 0 < msgs cc <⊥, outM v>
⟹ v = (cX = cN)"
proof clarify
fix v p cc
assume Asm: "qReachable cX (Proc - {p}) cc" "initReachable cc"
"0 < msgs cc <⊥, outM v>"
hence "reachable cX cc" "decided cc" using QReachImplReach by auto
hence "¬(vDecided (cX ≠ cN) cc)"
using COnlyReachesOneDecision Agreement Asm C0NotCN xInit xIs0OrN
unfolding agreementInit_def by metis
with Asm C0NotCN xIs0OrN show "v = (cX = cN)"
by (auto, metis (full_types) neq0_conv)
qed
have ExRightDecs: "⋀p. ∃cc. qReachable (cX) (Proc - {p}) cc
∧ initReachable cc ∧ 0 < msgs cc <⊥, outM (cX = cN)>"
proof-
fix p
show "∃cc::('p, 'v, 's) configuration.
qReachable cX (Proc - {p}) cc ∧ initReachable cc
∧ (0::nat) < msgs cc <⊥, outM cX = cN>"
using Termination[of "cX" "Proc - {p}"] finiteProcs minimalProcs
InitRInitC
unfolding terminationPseudo_def
proof auto
fix cc v
assume
Asm: "initReachable cX" "qReachable (cX) (Proc - {p}) cc"
"initReachable cc" "0 < msgs cc <⊥, outM v>"
with COnlyReachesOneDecision[rule_format, of "cc"] QReachImplReach
have "0 < msgs cc <⊥, outM cX = cN>" by auto
with Asm
show "∃cc::('p, 'v, 's) configuration.
qReachable cX (Proc - {p}) cc
∧ initReachable cc ∧ (0::nat) < msgs cc <⊥, outM cX = cN>"
by blast
qed
qed
have ZeroinPSilent: "∀ p v . v ∈ val[p, cX] ⟷ v = (cX = cN)"
proof clarify
fix p v
show "v ∈ val[p, cX] ⟷ v = (cX = cN)"
unfolding pSilDecVal_def
using InitRInitC xIs0OrN C0NotCN NoWrongDecs ExRightDecs by auto
qed
thus "vUniform (cX = cN) cX" using InitRInitC
unfolding vUniform_def by auto
qed
hence
C0Is0Uniform: "vUniform False c0" and
CNNot0Uniform: "¬ vUniform False cN"
using C0NAreUniform unfolding vUniform_def using C0NotCN by auto
hence "∃ j < n. vUniform False (initCfgList ! j)
∧ ¬(vUniform False (initCfgList ! Suc j))"
unfolding c0_def cN_def
using NatPredicateTippingPoint
[of n "λx. vUniform False (initCfgList ! x)"] NGr0 by auto
then obtain j
where J: "j < n"
"vUniform False (initCfgList ! j)"
"¬(vUniform False (initCfgList ! Suc j))" by blast
define pJ where "pJ = procList ! j"
define cJ where "cJ = initCfgList ! j"
hence cJDef: "cJ = ⦇ states = start, msgs = initMsg j⦈"
using J(1) InitCfgLength nth_map_upt[of 0 "j- 1" 1]
nth_map_upt[of "j" "n + 1" 0]
unfolding initCfgList_def
by auto
hence MsgCJ: "msgs cJ = (λm::('p, 'v) message.
if ∃p::'p. m = <p, inM ∃i<j. procList ! i = p> then 1::nat
else (0::nat))"
unfolding initMsg_def
using AllPInProclist
by auto
define cJ1 where "cJ1 = initCfgList ! (Suc j)"
hence cJ1Def: "cJ1 = ⦇ states = start, msgs = initMsg (Suc j)⦈"
using J(1) InitCfgLength nth_map_upt[of 0 "j" 1]
nth_map_upt[of "j + 1" "n + 1" 0]
unfolding initCfgList_def
by auto
hence MsgCJ1: "msgs cJ1 = (λm::('p, 'v) message.
if ∃p::'p. m = <p, inM ∃i<(Suc j). procList ! i = p> then 1::nat
else (0::nat))"
unfolding initMsg_def
using AllPInProclist
by auto
have CJ1Init: "initial cJ1"
using InitInitial[rule_format, of cJ1] J(1) InitCfgLength
unfolding cJ1_def by auto
hence CJ1InitR: "initReachable cJ1"
using InitialIsInitReachable by simp
have ValPj0: "False ∈ val[pJ, cJ]"
using J(2) unfolding cJ_def vUniform_def by auto
hence "∃cc. vDecided False cc ∧ withoutQReachable cJ {pJ} cc"
unfolding pSilDecVal_def by auto
then obtain cc
where CC: "vDecided False cc" "withoutQReachable cJ {pJ} cc"
by blast
hence "∃Q. qReachable cJ Q cc ∧ Q = Proc - {pJ}" by blast
then obtain ccQ where CCQ: "qReachable cJ ccQ cc" "ccQ = Proc - {pJ}"
by blast
have StatescJcJ1: "states cJ = states cJ1"
using cJ_def cJ1_def initCfgList_def
by (metis InitCfgLength InitCfgStart J(1) Suc_eq_plus1 Suc_mono
less_SucI nth_mem)
have Distinct: "⋀ i . distinct procList ⟹ i<j
⟹ procList ! i = procList ! j ⟹ False"
by (metis J(1) ProcList(1) distinct_conv_nth less_trans
not_less_iff_gr_or_eq)
have A: "msgs cJ (<pJ ,inM False>) = 1"
using pJ_def ProcList J(1) MsgCJ using Distinct by auto
have B: "msgs cJ1 (<pJ ,inM True>) = 1"
using pJ_def ProcList J(1) MsgCJ1 by auto
have C: "msgs cJ (<pJ ,inM True>) = 0"
using pJ_def ProcList J(1) MsgCJ using Distinct by auto
have D: "msgs cJ1 (<pJ ,inM False>) = 0"
using pJ_def ProcList J(1) MsgCJ1 by auto
define msgsCJ' where
"msgsCJ' m = (if m = (<pJ ,inM False>) ∨ m = (<pJ ,inM True>) then 0 else (msgs cJ) m)" for m
have MsgsCJ': "msgsCJ' = ((msgs cJ) -# (<pJ ,inM False>))"
using A C msgsCJ'_def by auto
have AllOther: "∀ m . msgsCJ' m = ((msgs cJ1) -# (<pJ ,inM True>)) m"
using B D MsgCJ1 MsgCJ J(1) N ProcList AllPInProclist
unfolding msgsCJ'_def pJ_def
proof(clarify)
fix m
show "(if m = <procList ! j, inM False> ∨
m = <procList ! j, inM True> then 0 else msgs cJ m)
= (msgs cJ1 -# <procList ! j, inM True>) m"
proof(cases "m = <procList ! j, inM False> ∨ m
= <procList ! j, inM True>",auto)
assume "0 < (msgs cJ1 <procList ! j, inM False>)"
thus False using D pJ_def by (metis less_nat_zero_code)
next
show "msgs cJ1 <procList ! j, inM True> ≤ Suc 0"
by (metis B One_nat_def order_refl pJ_def)
next
assume AssumpMJ: "m ≠ <procList ! j, inM False>"
"m ≠ <procList ! j, inM True>"
hence "(if ∃p. m = <p, inM ∃i<j. procList ! i = p> then 1 else 0)
= (if ∃p. m = <p, inM ∃i<Suc j. procList ! i = p> then 1 else 0)"
by (induct m, auto simp add: less_Suc_eq)
thus "msgs cJ m = msgs cJ1 m"
using MsgCJ MsgCJ1 by auto
qed
qed
with MsgsCJ' have InitMsgs: "((msgs cJ) -# (<pJ ,inM False>))
= ((msgs cJ1) -# (<pJ, inM True>))"
by simp
hence F: "(((msgs cJ) -# (<pJ ,inM False>)) ∪# ({#<pJ, inM True>})) =
(((msgs cJ1) -# (<pJ, inM True>)) ∪# ({#<pJ, inM True>}))"
by (metis (full_types))
from B have One: "(((msgs cJ1) -# (<pJ, inM True>))
∪# ({#<pJ, inM True>})) <pJ, inM True> = 1" by simp
with B have "∀ m :: ('p, 'v) message . (msgs cJ1) m
= (((msgs cJ1) -# (<pJ, inM True>)) ∪#
({#<pJ, inM True>})) m" by simp
with B have "(((msgs cJ1) -# (<pJ, inM True>)) ∪# ({#<pJ, inM True>}))
= (msgs cJ1)" by simp
with F have InitMsgs: "(((msgs cJ) -# (<pJ ,inM False>))
∪# ({#<pJ, inM True>})) = (msgs cJ1)"
by simp
define cc' where "cc' = ⦇states = (states cc),
msgs = (((msgs cc) -# (<pJ,inM False>)) ∪# {# (<pJ, inM True>)})⦈"
have "⟦qReachable cJ ccQ cc; ccQ = Proc - {pJ};
(((msgs cJ) -# (<pJ ,inM False>)) ∪# ({#<pJ, inM True>}))
= (msgs cJ1); states cJ = states cJ1⟧
⟹ withoutQReachable cJ1 {pJ} ⦇states = (states cc),
msgs = (((msgs cc) -# (<pJ,inM False>)) ∪# {# (<pJ, inM True>)}) ⦈"
proof (induct rule: qReachable.induct)
fix cfg1::"('p, 'v, 's) configuration"
fix Q
assume
Assm: "(((msgs cfg1) -#(<pJ, inM False>)) ∪# {# <pJ, inM True> })
= msgs cJ1"
"states cfg1 = states cJ1"
hence CJ1: "cJ1 = ⦇states = states cfg1,
msgs = ((msgs cfg1) -# <pJ, inM False>) ∪# {# <pJ, inM True> }⦈" by auto
have "qReachable cJ1 (Proc - {pJ}) cJ1" using qReachable.simps
by blast
with Assm show "qReachable cJ1 (Proc - {pJ})
⦇states = states cfg1, msgs = ((msgs cfg1) -# <pJ, inM False>)
∪# {# <pJ, inM True> }⦈" using CJ1 by blast
fix cfg1 cfg2 cfg3 :: "('p, 'v, 's) configuration"
fix msg
assume Q: "Q = (Proc - {pJ})"
assume "(((msgs cfg1) -# <pJ, inM False>) ∪# {# <pJ, inM True> })
= (msgs cJ1)"
"(states cfg1) = (states cJ1)"
"Q = (Proc - {pJ}) ⟹
(((msgs cfg1) -# <pJ, inM False>) ∪# {# <pJ, inM True> })
= (msgs cJ1)
⟹ (states cfg1) = (states cJ1)
⟹ qReachable cJ1 (Proc - {pJ})
⦇states = (states cfg2),
msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })⦈"
with Q have Cfg2:
"qReachable cJ1 (Proc - {pJ}) ⦇states = (states cfg2),
msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })⦈"
by simp
assume "qReachable cfg1 Q cfg2"
"cfg2 ⊢ msg ↦ cfg3"
"∃(p::'p)∈Q. (isReceiverOf p msg)"
with Q have Step: "qReachable cfg1 (Proc - {pJ}) cfg2"
"cfg2 ⊢ msg ↦ cfg3"
"∃(p::'p)∈(Proc - {pJ}). (isReceiverOf p msg)" by auto
then obtain p where P: "p∈(Proc - {pJ})" "isReceiverOf p msg" by blast
hence NotEq: "pJ ≠ p" by blast
with UniqueReceiverOf[of "p" "msg" "pJ"] P(2)
have notRec: "¬ (isReceiverOf pJ msg)" by blast
hence MsgNoIn:"msg ≠ <pJ, inM False> ∧ msg ≠ <pJ, inM True>"
by auto
from Step(2) have "enabled cfg2 msg" using steps.simps
by (auto, cases msg, auto)
hence MsgEnabled: "enabled ⦇states = (states cfg2),
msgs = (((msgs cfg2) -# <pJ, inM False>)
∪# {# <pJ, inM True> })⦈ msg"
using MsgNoIn by (simp add: enabled_def)
have "⦇states = (states cfg2),
msgs = (((msgs cfg2) -# <pJ, inM False>)
∪# {# <pJ, inM True> })⦈
⊢ msg ↦ ⦇states = (states cfg3),
msgs = (((msgs cfg3) -# <pJ, inM False>)
∪# {# <pJ, inM True> })⦈"
proof (cases msg)
fix p' bool
assume MsgIn :"(msg = <p', inM bool>)"
with noInSends MsgIn MsgNoIn MsgEnabled
show "⦇states = (states cfg2),
msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })⦈
⊢ msg ↦ ⦇states = (states cfg3),
msgs = (((msgs cfg3) -# <pJ, inM False>)
∪# {# <pJ, inM True> })⦈"
using steps.simps(1) Step(2) select_convs(2) select_convs(1)
by auto
next
fix bool
assume "(msg = <⊥, outM bool>)"
thus "⦇states = (states cfg2),
msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })⦈
⊢ msg ↦ ⦇states = (states cfg3),
msgs = (((msgs cfg3) -# <pJ, inM False>)
∪# {# <pJ, inM True> })⦈"
using steps_def Step(2) by auto
next
fix p v
assume "(msg = <p, v>)"
with noInSends MsgNoIn MsgEnabled show "⦇states = (states cfg2),
msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })⦈
⊢ msg ↦ ⦇states = (states cfg3),
msgs = (((msgs cfg3) -# <pJ, inM False>)
∪# {# <pJ, inM True> })⦈"
using steps.simps(1) Step(2) select_convs(2) select_convs(1) by auto
qed
with Cfg2 Step(3) show "qReachable cJ1 (Proc - {pJ})
⦇states = (states cfg3),
msgs = (((msgs cfg3) -# <pJ, inM False>) ∪# {# <pJ, inM True> })⦈"
using
qReachable.simps[of "cJ1" "(Proc - {pJ})"
"⦇states = (states cfg3),
msgs = (((msgs cfg3) -# <pJ, inM False>)
∪# {# <pJ, inM True> })⦈"] by auto
qed
with CCQ(1) CCQ(2) InitMsgs StatescJcJ1 have CC':
"withoutQReachable cJ1 {pJ} ⦇states = (states cc),
msgs = (((msgs cc) -# (<pJ,inM False>))
∪# {# (<pJ, inM True>)}) ⦈" by auto
with QReachImplReach CJ1InitR initReachable_def reachable.simps
ReachableTrans
have "initReachable ⦇states = (states cc),
msgs = (((msgs cc) -# (<pJ,inM False>))
∪# {# (<pJ, inM True>)}) ⦈" by meson
with CC' have "False ∈ val[pJ, cJ1]"
unfolding pSilDecVal_def
using CJ1InitR CC(1) select_convs(2) by auto
hence "¬(vUniform True (cJ1))"
unfolding vUniform_def
using CJ1InitR by blast
hence "nonUniform cJ1"
using J(3) CJ1InitR unfolding cJ1_def by auto
thus ?thesis
using CJ1Init by blast
qed
text‹
Völzer's Lemma 2 proves that for every process $p$ in the consensus setting
\isb{nonUniform} configurations can reach a configuration where the silent
decision values of $p$ are True and False. This is key to the construction of
non-deciding executions.
\voelzer{Lemma 2}
›
lemma NonUniformCanReachSilentBivalence:
fixes
p:: 'p and
c:: "('p, 'v, 's) configuration"
assumes
NonUni: "nonUniform c" and
PseudoTermination: "⋀cc Q . terminationPseudo 1 cc Q" and
Agree: "⋀ cfg . reachable c cfg ⟶ agreement cfg"
shows
"∃ c' . reachable c c' ∧ val[p,c'] = {True, False}"
proof(cases "val[p,c] = {True, False}")
case True
have "reachable c c" using reachable.simps by metis
thus ?thesis
using True by blast
next
case False
hence notEq: "val[p,c] ≠ {True, False}" by simp
from NonUni PseudoTermination DecisionValuesExist
have notE: "∀q. val[q,c] ≠ {}" by simp
hence notEP: "val[p,c] ≠ {}" by blast
have valType: "∀q. val[q,c] ⊆ {True, False}" using pSilDecVal_def
by (metis (full_types) insertCI subsetI)
hence "val[p,c] ⊆ {True, False}" by blast
with notEq notEP have "∃b:: bool. val[p,c] = {b}" by blast
then obtain b where B: "val[p,c] = {b}" by auto
from NonUni vUniform_def have
NonUni: "(∃q. val[q,c] ≠ {True}) ∧ (∃q. val[q,c] ≠ {False})" by simp
have Bool: "b = True ∨ b = False" by simp
with NonUni have "∃q. val[q,c] ≠ {b}" by blast
then obtain q where Q: "val[q,c] ≠ {b}" by auto
from notE valType
have "val[q,c] = {True} ∨ val[q,c] = {False} ∨ val[q,c] = {True, False}"
by auto
with Bool Q have "val[q,c] = {¬b} ∨ val[q,c] = {b, ¬b}" by blast
hence "(¬b) ∈ val[q,c]" by blast
with pSilDecVal_def
have "∃ c'::('p, 'v, 's) configuration . (withoutQReachable c {q} c') ∧
vDecided (¬b) c'" by simp
then obtain c' where C': "withoutQReachable c {q} c'" "vDecided (¬b) c'"
by auto
hence Reach: "reachable c c'" using QReachImplReach by simp
have "∀ cfg . reachable c' cfg ⟶ agreement cfg"
proof clarify
fix cfg
assume "reachable c' cfg"
with Reach have "reachable c cfg"
using ReachableTrans[of c c'] by simp
with Agree show "agreement cfg" by simp
qed
with PseudoTermination C'(2) DecidedImpliesUniform have "vUniform (¬b) c'"
by simp
hence notB: "val[p,c'] = {¬b}" using vUniform_def by simp
with Reach B show "∃ cfg. reachable c cfg ∧ val[p,cfg] = {True, False}"
proof(induct rule: reachable.induct, simp)
fix cfg1 cfg2 cfg3 msg
assume
IV: "val[p,cfg1] = {b} ⟹
val[p,cfg2] = {¬ b} ⟹
∃cfg::('p, 'v, 's) configuration. reachable cfg1 cfg
∧ val[p,cfg] = {True, False}" and
Reach: "reachable cfg1 cfg2" and
Step: "cfg2 ⊢ msg ↦ cfg3" and
ValCfg1: "val[p,cfg1] = {b}" and
ValCfg3: "val[p,cfg3] = {¬ b}"
from ValCfg1 have InitCfg1: "initReachable cfg1"
using pSilDecVal_def by auto
from Reach InitCfg1 initReachable_def reachable.simps ReachableTrans
have InitCfg2: "initReachable cfg2" by blast
with PseudoTermination DecisionValuesExist
have notE: "∀q. val[q,cfg2] ≠ {}" by simp
have valType: "∀q. val[q,cfg2] ⊆ {True, False}" using pSilDecVal_def
by (metis (full_types) insertCI subsetI)
from notE valType
have "val[p,cfg2] = {True} ∨ val[p,cfg2] = {False}
∨ val[p,cfg2] = {True, False}"
by auto
with Bool have Val: "val[p,cfg2] = {b} ∨ val[p,cfg2] = {¬b}
∨ val[p,cfg2] = {True, False}"
by blast
show "∃cfg::('p, 'v, 's) configuration. reachable cfg1 cfg
∧ val[p,cfg] = {True, False}"
proof(cases "val[p,cfg2] = {b}")
case True
hence B: "val[p,cfg2] = {b}" by simp
from Step have RecOrOut: "∃q. isReceiverOf q msg" by(cases msg, auto)
then obtain q where Rec: "isReceiverOf q msg" by auto
with B Step InitCfg2 SilentDecisionValueNotInverting
have "val[p,cfg3] ≠ {¬b}" by simp
with ValCfg3 have "False" by simp
thus "∃cfg::('p, 'v, 's) configuration. reachable cfg1 cfg ∧
val[p,cfg] = {True, False}" by simp
next
case False
with Val have Val: "val[p,cfg2] = {¬b} ∨ val[p,cfg2] = {True, False}"
by simp
show "∃cfg::('p, 'v, 's) configuration. reachable cfg1 cfg ∧
val[p,cfg] = {True, False}"
proof(cases "val[p,cfg2] = {¬b}")
case True
hence "val[p,cfg2] = {¬b}" by simp
with ValCfg1 IV show
"∃cfg::('p, 'v, 's) configuration.
reachable cfg1 cfg ∧ val[p,cfg] = {True, False}"
by simp
next
case False
with Val have "val[p,cfg2] = {True, False}" by simp
with Reach have "reachable cfg1 cfg2 ∧ val[p,cfg2] = {True, False}"
by blast
from this show "∃cfg::('p, 'v, 's) configuration.
reachable cfg1 cfg ∧ val[p,cfg] = {True, False}" by blast
qed
qed
qed
qed
end
end