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