Theory DiskPaxos
theory DiskPaxos imports DiskPaxos_Invariant begin
subsection ‹Inner Module›
record
Istate =
iinput :: "Proc ⇒ InputsOrNi"
ioutput :: "Proc ⇒ InputsOrNi"
ichosen :: InputsOrNi
iallInput :: "InputsOrNi set"
definition IInit :: "Istate ⇒ bool"
where
"IInit s = (range (iinput s) ⊆ Inputs
∧ ioutput s = (λp. NotAnInput)
∧ ichosen s = NotAnInput
∧ iallInput s = range (iinput s))"
definition IChoose :: "Istate ⇒ Istate ⇒ Proc ⇒ bool"
where
"IChoose s s' p = (ioutput s p = NotAnInput
∧ (if (ichosen s = NotAnInput)
then (∃ip ∈ iallInput s. ichosen s' = ip
∧ ioutput s' = (ioutput s) (p := ip))
else ( ioutput s' = (ioutput s) (p:= ichosen s)
∧ ichosen s' = ichosen s))
∧ iinput s' = iinput s ∧ iallInput s'= iallInput s)"
definition IFail :: "Istate ⇒ Istate ⇒ Proc ⇒ bool"
where
"IFail s s' p = (ioutput s' = (ioutput s) (p:= NotAnInput)
∧ (∃ip ∈ Inputs. iinput s' = (iinput s)(p:= ip)
∧ iallInput s' = iallInput s ∪ {ip})
∧ ichosen s' = ichosen s)"
definition INext :: "Istate ⇒ Istate ⇒ bool"
where "INext s s' = (∃p. IChoose s s' p ∨ IFail s s' p)"
definition s2is :: "state ⇒ Istate"
where
"s2is s = ⦇iinput = inpt s,
ioutput = outpt s,
ichosen=chosen s,
iallInput = allInput s⦈"
theorem R1:
"⟦ HInit s; is = s2is s⟧ ⟹ IInit is"
by(auto simp add: HInit_def IInit_def s2is_def Init_def)
theorem R2b:
assumes inv: "HInv s"
and inv': "HInv s'"
and nxt: "HNext s s'"
and srel: "is=s2is s ∧ is'=s2is s'"
shows "(∃p. IFail is is' p ∨ IChoose is is' p) ∨ is = is'"
proof(auto)
assume chg_vars: "is≠is'"
with srel
have s_change: " inpt s ≠ inpt s' ∨ outpt s ≠ outpt s'
∨ chosen s ≠ chosen s' ∨ allInput s ≠ allInput s'"
by(auto simp add: s2is_def)
from inv
have inv2c5: "∀p. inpt s p ∈ allInput s
∧ (chosen s = NotAnInput ⟶ outpt s p = NotAnInput)"
by(auto simp add: HInv_def HInv2_def Inv2c_def Inv2c_inner_def)
from nxt s_change inv2c5
have "inpt s' ≠ inpt s ∨ outpt s' ≠ outpt s"
by(auto simp add: HNext_def Next_def HNextPart_def)
with nxt
have "∃p. Fail s s' p ∨ EndPhase2 s s' p"
by(auto simp add: HNext_def Next_def
StartBallot_def Phase0Read_def Phase1or2Write_def
Phase1or2Read_def Phase1or2ReadThen_def Phase1or2ReadElse_def
EndPhase1or2_def EndPhase1_def EndPhase0_def)
then obtain p where fail_or_endphase2: "Fail s s' p ∨ EndPhase2 s s' p"
by auto
from inv
have inv2c: "Inv2c_inner s p"
by(auto simp add: HInv_def HInv2_def Inv2c_def)
from fail_or_endphase2 have "IFail is is' p ∨ IChoose is is' p"
proof
assume fail: "Fail s s' p "
hence phase': "phase s' p = 0"
and outpt: "outpt s' = (outpt s) (p:= NotAnInput)"
by(auto simp add: Fail_def)
have "IFail is is' p"
proof -
from fail srel
have "ioutput is' = (ioutput is) (p:= NotAnInput)"
by(auto simp add: Fail_def s2is_def)
moreover
from nxt
have all_nxt: "allInput s'= allInput s ∪ (range (inpt s'))"
by(auto simp add: HNext_def HNextPart_def)
from fail srel
have "∃ip ∈ Inputs. iinput is' = (iinput is)(p:= ip)"
by(auto simp add: Fail_def s2is_def)
then obtain ip where ip_Input: "ip∈Inputs" and "iinput is' = (iinput is)(p:= ip)"
by auto
with inv2c5 srel all_nxt
have " iinput is' = (iinput is)(p:= ip)
∧ iallInput is' = iallInput is ∪ {ip}"
by(auto simp add: s2is_def)
moreover
from outpt srel nxt inv2c
have "ichosen is' = ichosen is"
by(auto simp add: HNext_def HNextPart_def s2is_def Inv2c_inner_def)
ultimately
show ?thesis
using ip_Input
by(auto simp add: IFail_def)
qed
thus ?thesis
by auto
next
assume endphase2: "EndPhase2 s s' p"
from endphase2
have "phase s p =2"
by(auto simp add: EndPhase2_def)
with inv2c Ballot_nzero
have bal_dblk_nzero: "bal(dblock s p)≠ 0"
by(auto simp add: Inv2c_inner_def)
moreover
from inv
have inv2a_dblock: "Inv2a_innermost s p (dblock s p)"
by(auto simp add: HInv_def HInv2_def Inv2a_def Inv2a_inner_def blocksOf_def)
ultimately
have p22: "inp (dblock s p) ∈ allInput s"
by(auto simp add: Inv2a_innermost_def)
from inv
have "allInput s ⊆ Inputs"
by(auto simp add: HInv_def HInv1_def)
with p22 NotAnInput endphase2
have outpt_nni: "outpt s' p ≠ NotAnInput"
by(auto simp add: EndPhase2_def)
show ?thesis
proof(cases "chosen s = NotAnInput")
case True
with inv2c5
have p31: "∀q. outpt s q = NotAnInput"
by auto
with endphase2
have p32: "∀q ∈ UNIV -{p}. outpt s' q = NotAnInput"
by(auto simp add: EndPhase2_def)
hence some_eq: "(⋀x. outpt s' x ≠ NotAnInput ⟹ x = p)"
by auto
from p32 True nxt some_equality[of "λp. outpt s' p ≠ NotAnInput", OF outpt_nni some_eq]
have p33: "chosen s' = outpt s' p"
by(auto simp add: HNext_def HNextPart_def)
with endphase2
have "chosen s' = inp(dblock s p) ∧ outpt s' = (outpt s)(p:=inp(dblock s p))"
by(auto simp add: EndPhase2_def)
with True p22
have "if (chosen s = NotAnInput)
then (∃ip ∈ allInput s. chosen s' = ip
∧ outpt s' = (outpt s) (p := ip))
else ( outpt s' = (outpt s) (p:= chosen s)
∧ chosen s' = chosen s)"
by auto
moreover
from endphase2 inv2c5 nxt
have "inpt s' = inpt s ∧ allInput s'= allInput s"
by(auto simp add: EndPhase2_def HNext_def HNextPart_def)
ultimately
show ?thesis
using srel p31
by(auto simp add: IChoose_def s2is_def)
next
case False
with nxt
have p31: "chosen s' = chosen s"
by(auto simp add: HNext_def HNextPart_def)
from inv'
have inv6: "HInv6 s'"
by(auto simp add: HInv_def)
have p32: "outpt s' p = chosen s"
proof-
from endphase2
have "outpt s' p = inp(dblock s p)"
by(auto simp add: EndPhase2_def)
moreover
from inv6 p31
have "outpt s' p ∈ {chosen s, NotAnInput}"
by(auto simp add: HInv6_def)
ultimately
show ?thesis
using outpt_nni
by auto
qed
from srel False
have "IChoose is is' p"
proof(clarsimp simp add: IChoose_def s2is_def)
from endphase2 inv2c
have "outpt s p = NotAnInput"
by(auto simp add: EndPhase2_def Inv2c_inner_def)
moreover
from endphase2 p31 p32 False
have "outpt s' = (outpt s) (p:= chosen s) ∧ chosen s' = chosen s"
by(auto simp add: EndPhase2_def)
moreover
from endphase2 nxt inv2c5
have "inpt s' = inpt s ∧ allInput s'= allInput s"
by(auto simp add: EndPhase2_def HNext_def HNextPart_def)
ultimately
show " outpt s p = NotAnInput
∧ outpt s' = (outpt s)(p := chosen s) ∧ chosen s' = chosen s
∧ inpt s' = inpt s ∧ allInput s' = allInput s"
by auto
qed
thus ?thesis
by auto
qed
qed
thus "∃p. IFail is is' p ∨ IChoose is is' p"
by auto
qed
end