Theory BenOr_Defs

section ‹The Ben-Or Algorithm›

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

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)"