# Theory BenOr_Defs

section ‹The Ben-Or Algorithm›

theory BenOr_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Quorums" "../Two_Steps"
begin

consts coin :: "round ⇒ process ⇒ val"

record 'val pstate =
x :: 'val                ― ‹current value held by process›
vote :: "'val option"    ― ‹value the process voted for, if any›
decide :: "'val option"  ― ‹value the process has decided on, if any›

datatype 'val msg =
Val 'val
| Vote "'val option"
| Null  ― ‹dummy message in case nothing needs to be sent›

definition isVote where "isVote m ≡ ∃v. m = Vote v"

definition isVal where "isVal m ≡ ∃v. m = Val v"

fun getvote where
"getvote (Vote v) = v"

fun getval where
"getval (Val z) = z"

definition BenOr_initState where
"BenOr_initState p st ≡ (vote st = None) ∧ (decide st = None)"

definition msgRcvd where  ― ‹processes from which some message was received›
"msgRcvd (msgs:: process ⇀ 'val msg) = {q . msgs q ≠ None}"

definition send0 where
"send0 r p q st ≡ Val (x st)"

definition next0 where
"next0 r p st (msgs::process ⇀ 'val msg) st' ≡
(∃v. (∀q ∈ msgRcvd msgs. msgs q = Some (Val v))
∧ st' = st ⦇ vote := Some v ⦈)
∨ ¬(∃v. ∀q ∈ msgRcvd msgs. msgs q = Some (Val v))
∧ st' = st ⦇ vote := None ⦈"

definition send1 where
"send1 r p q st ≡ Vote (vote st)"

definition someVoteRcvd where
― ‹set of processes from which some vote was received›
"someVoteRcvd (msgs :: process ⇀ 'val msg) ≡
{ q . q ∈ msgRcvd msgs ∧ isVote (the (msgs q)) ∧ getvote (the (msgs q)) ≠ None }"

definition identicalVoteRcvd where
"identicalVoteRcvd (msgs :: process ⇀ 'val msg) v ≡
∀q ∈ msgRcvd msgs. isVote (the (msgs q)) ∧ getvote (the (msgs q)) = Some v"

definition x_update where
"x_update r p msgs st' ≡
(∃q ∈ someVoteRcvd msgs . x st' = the (getvote (the (msgs q))))
∨ someVoteRcvd msgs = {} ∧ x st' = coin r p"

definition dec_update where
"dec_update st msgs st' ≡
(∃v. identicalVoteRcvd msgs v ∧ decide st' = Some v)
∨ ¬(∃v. identicalVoteRcvd msgs v) ∧ decide st' = decide st"

definition next1 where
"next1 r p st msgs st' ≡
x_update r p msgs st'
∧ dec_update st msgs st'
∧ vote st' = None"

definition BenOr_sendMsg where
"BenOr_sendMsg (r::nat) ≡ if two_step r = 0 then send0 r else send1 r"

definition BenOr_nextState where
"BenOr_nextState r ≡ if two_step r = 0 then next0 r else next1 r"

subsection ‹The \emph{Ben-Or} Heard-Of machine›
(******************************************************************************)

definition (in quorum_process) BenOr_commPerRd where
"BenOr_commPerRd HOrs ≡ ∀p. HOrs p ∈ Quorum"

definition BenOr_commGlobal where
"BenOr_commGlobal HOs ≡ ∃r. two_step r = 1
∧ (∀p q. HOs r p = HOs r q ∧ (coin r p :: val) = coin r q)"

definition (in quorum_process) BenOr_HOMachine where
"BenOr_HOMachine = ⦇
CinitState =  (λp st crd. BenOr_initState p st),
sendMsg =  BenOr_sendMsg,
CnextState = (λr p st msgs crd st'. BenOr_nextState r p st msgs st'),
HOcommPerRd = BenOr_commPerRd,
HOcommGlobal = BenOr_commGlobal
⦈"

abbreviation (in quorum_process)
"BenOr_M ≡ (BenOr_HOMachine::(process, val pstate, val msg) HOMachine)"

end