Theory OneThirdRule_Defs

section ‹The OneThirdRule Algorithm›

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

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
  changed.›


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)
  qed
  thus ?thesis ..
qed

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

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 
  processes.
›

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"

end