Quelle  UvDefs.thy

theory UvDefs
imports "../HOModel"
begin

section ‹Verification of the \emph{UniformVoting} Consensus Algorithm›

text ‹
 Algorithm \emph{UniformVoting} is presented in~cite‹"charron:heardof"›.
 It can be considered as a deterministic version of Ben-Or's well-known
 probabilistic Consensus algorithm~cite‹"ben-or:advantage"›. We formalize
 in Isabelle the correctness proof given in~cite‹"charron:heardof"›,
 using the framework of theory ‹HOModel›.
 ›


subsection ‹Model of the Algorithm›

text ‹
 We begin by introducing an anonymous type of processes of finite
 cardinality that will instantiate the type variable ‹'proc›
 of the generic HO model.
 ›

typedecl Proc ― ‹the set of processes›
axiomatization where Proc_finite: "OFCLASS(Proc, finite_class)"
instance Proc :: finite by (rule Proc_finite)

abbreviation
  "N ≡ card (UNIV::Proc set)"   ― ‹number of processes›

text ‹
 The algorithm proceeds in \emph{phases} of $2$ rounds each (we call
 \emph{steps} the individual rounds that constitute a phase).
 The following utility functions compute the phase and step of a round,
 given the round number.
 ›

abbreviation "nSteps ≡ 2"

definition phase where "phase (r::nat) ≡ r div nSteps"

definition step where "step (r::nat) ≡ r mod nSteps"

text ‹
 The following record models the local state of a process.
 ›

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›

text ‹
 Possible messages sent during the execution of the algorithm, and characteristic
 predicates to distinguish types of messages.
 ›

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

definition isValVote where "isValVote m ≡ ∃z v. m = ValVote z v"

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

text ‹
 Selector functions to retrieve components of messages. These functions
 have a meaningful result only when the message is of appropriate kind.
 ›

fun getvote where
  "getvote (ValVote z v) = v"

fun getval where
  "getval (ValVote z v) = z"
| "getval (Val z) = z"


text ‹
 The ‹x› field of the initial state is unconstrained, all other
 fields are initialized appropriately.
 ›

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

text ‹
 We separately define the transition predicates and the send functions
 for each step and later combine them to define the overall next-state relation.
 ›

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

definition smallestValRcvd where
  "smallestValRcvd (msgs::Proc ⇀ ('val::linorder) msg) ≡
   Min {v. ∃q. msgs q = Some (Val v)}"

text ‹
 In step 0, each process sends its current ‹x› value.

 It updates its ‹x› field to the smallest value it has received.
 If the process has received the same value ‹v› from all processes
 from which it has heard, it updates its ‹vote› field to ‹v›.
 ›

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

definition next0 where
  "next0 r p st (msgs::Proc ⇀ ('val::linorder) msg) st' ≡
       (∃v. (∀q ∈ msgRcvd msgs. msgs q = Some (Val v))
           ∧ st' = st ( vote := Some v, x := smallestValRcvd msgs ))
    ∨ ¬(∃v. ∀q ∈ msgRcvd msgs. msgs q = Some (Val v))
       ∧ st' = st ( x := smallestValRcvd msgs )"

text ‹
 In step 1, each process sends its current ‹x› and ‹vote› values.
 ›

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

definition valVoteRcvd where
  ― ‹processes from which values and votes were received›
  "valVoteRcvd (msgs :: Proc ⇀ 'val msg) ≡
   {q . ∃z v. msgs q = Some (ValVote z v)}"

definition smallestValNoVoteRcvd where
  "smallestValNoVoteRcvd (msgs::Proc ⇀ ('val::linorder) msg) ≡
   Min {v. ∃q. msgs q = Some (ValVote v None)}"

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

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

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

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 st msgs st'
   ∧ dec_update st msgs st'
   ∧ vote st' = None"

text ‹
 The overall send function and next-state relation are simply obtained as
 the composition of the individual relations defined above.
 ›

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

definition UV_nextState where
  "UV_nextState r ≡ if step r = 0 then next0 r else next1 r"


subsection ‹Communication Predicate for \emph{UniformVoting}›

text ‹
 We now define the communication predicate for the \emph{UniformVoting}
 algorithm to be correct.

 The round-by-round predicate requires that for any two processes
 there is always one process heard by both of them. In other words,
 no ``split rounds'' occur during the execution of the algorithm~cite‹"charron:heardof"›.
 Note that in particular, heard-of sets are never empty.
 ›

definition UV_commPerRd where
  "UV_commPerRd HOrs ≡ ∀p q. ∃pq. pq ∈ HOrs p ∩ HOrs q"

text ‹
 The global predicate requires the existence of a (space-)uniform round
 during which the heard-of sets of all processes are equal.
 (Observe that cite‹"charron:heardof"› requires infinitely many uniform
 rounds, but the correctness proof uses just one such round.)
 ›

definition UV_commGlobal where
  "UV_commGlobal HOs ≡ ∃r. ∀p q. HOs r p = HOs r q"


subsection ‹The \emph{UniformVoting} Heard-Of Machine›

text ‹
 We now define the HO machine for \emph{Uniform Voting} by assembling the
 algorithm definition and its communication predicate. Notice that the
 coordinator arguments for the initialization and transition functions are
 unused since \emph{UniformVoting} is not a coordinated algorithm.
 ›

definition UV_HOMachine where
  "UV_HOMachine = (
    CinitState = (λp st crd. UV_initState p st),
    sendMsg = UV_sendMsg,
    CnextState = (λr p st msgs crd st'. UV_nextState r p st msgs st'),
    HOcommPerRd = UV_commPerRd,
    HOcommGlobal = UV_commGlobal
  )"

abbreviation
  "UV_M ≡ (UV_HOMachine::(Proc, 'val::linorder pstate, 'val msg) HOMachine)"

end