Theory OneThirdRule_Defs

section ‹The OneThirdRule Algorithm›

theory OneThirdRule_Defs
imports Heard_Of.HOModel "../Consensus_Types"

text ‹The contents of this file have been taken almost verbatim from the
  Heard Of Model AFP entry. The only difference is that the types have been

subsection ‹Model of the algorithm›

text ‹
  The state of each process consists of two fields: last_vote› holds
  the current value proposed by the process and decision› the
  value (if any, hence the option type) it has decided.

record 'val pstate =
  last_vote :: "'val"
  decision :: "'val option"

text ‹
  The initial value of field last_vote› is unconstrained, but no decision
  has been taken initially.

definition OTR_initState where
  "OTR_initState p st  decision st = None"

text ‹
  Given a vector msgs› of values (possibly null) received from 
  each process, @{term "HOV msgs v"} denotes the set of processes from
  which value v› was received.

definition HOV :: "(process  'val option)  'val  process set" where
  "HOV msgs v  { q . msgs q = Some v }"

text @{term "MFR msgs v"} (``most frequently received'') holds for
  vector msgs› if no value has been received more frequently
  than v›.

  Some such value always exists, since there is only a finite set of
  processes and thus a finite set of possible cardinalities of the
  sets @{term "HOV msgs v"}.

definition MFR :: "(process  'val option)  'val  bool" where
  "MFR msgs v  w. card (HOV msgs w)  card (HOV msgs v)"

lemma MFR_exists: "v. MFR msgs v"
proof -
  let ?cards = "{ card (HOV msgs v) | v . True }"
  let ?mfr = "Max ?cards"
  have "v. card (HOV msgs v)  N" by (auto intro: card_mono)
  hence "?cards  { 0 .. N }" by auto
  hence fin: "finite ?cards" by (metis atLeast0AtMost finite_atMost finite_subset)
  hence "?mfr  ?cards" by (rule Max_in) auto
  then obtain v where v: "?mfr = card (HOV msgs v)" by auto
  have "MFR msgs v"
  proof (auto simp: MFR_def)
    fix w
    from fin have "card (HOV msgs w)  ?mfr" by (rule Max_ge) auto
    thus "card (HOV msgs w)  card (HOV msgs v)" by (unfold v)
  thus ?thesis ..

text ‹
  Also, if a process has heard from at least one other process,
  the most frequently received values are among the received messages.

lemma MFR_in_msgs:
  assumes HO:"HOs m p  {}"
      and v: "MFR (HOrcvdMsgs OTR_M m p (HOs m p) (rho m)) v"
             (is "MFR ?msgs v")
  shows "q  HOs m p. v = the (?msgs q)"
proof -
  from HO obtain q where q: "q  HOs m p"
    by auto
  with v have "HOV ?msgs (the (?msgs q))  {}"
    by (auto simp: HOV_def HOrcvdMsgs_def)
  hence HOp: "0 < card (HOV ?msgs (the (?msgs q)))"
    by auto
  also from v have "  card (HOV ?msgs v)"
    by (simp add: MFR_def)
  finally have "HOV ?msgs v  {}"
    by auto
  thus ?thesis
    by (auto simp: HOV_def HOrcvdMsgs_def)

text @{term "TwoThirds msgs v"} holds if value v› has been
  received from more than $2/3$ of all processes.

definition TwoThirds where
  "TwoThirds msgs v  (2*N) div 3 < card (HOV msgs v)"

text ‹
  The next-state relation of algorithm \emph{One-Third Rule} for every process
  is defined as follows:
  if the process has received values from more than $2/3$ of all processes,
  the last_vote› field is set to the smallest among the most frequently received
  values, and the process decides value $v$ if it received $v$ from more than
  $2/3$ of all processes. If p› hasn't heard from more than $2/3$ of
  all processes, the state remains unchanged.
  (Note that Some› is the constructor of the option datatype, whereas
  ϵ› is Hilbert's choice operator.)
  We require the type of values to be linearly ordered so that the minimum
  is guaranteed to be well-defined.

definition OTR_nextState where
  "OTR_nextState r p (st::('val::linorder) pstate) msgs st'  
   if (2*N) div 3 < card {q. msgs q  None}
   then st' =  last_vote = Min {v . MFR msgs v},
          decision = (if (v. TwoThirds msgs v)
                    then Some (ϵv. TwoThirds msgs v)
                    else decision st) 
   else st' = st"

text ‹
  The message sending function is very simple: at every round, every process
  sends its current proposal (field last_vote› of its local state) to all 

definition OTR_sendMsg where
  "OTR_sendMsg r p q st  last_vote st"

subsection ‹Communication predicate for \emph{One-Third Rule}›

text ‹
  We now define the communication predicate for the \emph{One-Third Rule}
  algorithm to be correct.
  It requires that, infinitely often, there is a round where all processes
  receive messages from the same set Π› of processes where Π›
  contains more than two thirds of all processes.
  The ``per-round'' part of the communication predicate is trivial.

definition OTR_commPerRd where
  "OTR_commPerRd HOrs  True"

definition OTR_commGlobal where
  "OTR_commGlobal HOs 
    r. r0 Π. r0  r  (p. HOs r0 p = Π)  card Π > (2*N) div 3"

subsection ‹The \emph{One-Third Rule} Heard-Of machine›

text ‹
  We now define the HO machine for the \emph{One-Third Rule} algorithm
  by assembling the algorithm definition and its communication-predicate.
  Because this is an uncoordinated algorithm, the crd› arguments
  of the initial- and next-state predicates are unused.

definition OTR_HOMachine where
  "OTR_HOMachine =
     CinitState =  (λ p st crd. OTR_initState p st),
     sendMsg =  OTR_sendMsg,
     CnextState = (λ r p st msgs crd st'. OTR_nextState r p st msgs st'),
     HOcommPerRd = OTR_commPerRd,
     HOcommGlobal = OTR_commGlobal "

abbreviation "OTR_M  OTR_HOMachine::(process, 'val::linorder pstate, 'val) HOMachine"