Theory Ate_Defs

section ‹The $A_{T,E}$ Algorithm›

theory Ate_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 following record models the local state of a process.›

record 'val pstate =
  x :: "'val"              ― ‹current value held by process›
  decide :: "'val option"  ― ‹value the process has decided on, if any›

text ‹
  The x› field of the initial state is unconstrained, but no
  decision has yet been taken.

definition Ate_initState where
  "Ate_initState p st  (decide st = None)"

locale ate_parameters =
  fixes α::nat and T::nat and E::nat
  assumes TNaE:"T  2*(N + 2*α - E)"
      and TltN:"T < N"
      and EltN:"E < N"


text ‹The following are consequences of the assumptions on the parameters.›

lemma majE: "2 * (E - α)  N"
using TNaE TltN by auto

lemma Egta: "E > α"
using majE EltN by auto

lemma Tge2a: "T  2 * α"
using TNaE EltN by auto

text ‹
  At every round, each process sends its current x›.
  If it received more than T› messages, it selects the smallest value
  and store it in x›. As in algorithm \emph{OneThirdRule}, we
  therefore require values to be linearly ordered.

  If more than E› messages holding the same value are received,
  the process decides that value.

definition mostOftenRcvd where
  "mostOftenRcvd (msgs::process  'val option) 
   {v. w. card {qq. msgs qq = Some w}  card {qq. msgs qq = Some v}}"

  Ate_sendMsg :: "nat  process  process  'val pstate  'val"
  "Ate_sendMsg r p q st  x st"

  Ate_nextState :: "nat  process  ('val::linorder) pstate  (process  'val option)
                         'val pstate  bool"
  "Ate_nextState r p st msgs st' 
     (if card {q. msgs q  None} > T
      then x st' = Min (mostOftenRcvd msgs)
      else x st' = x st)
    (   (v. card {q. msgs q = Some v} > E   decide st' = Some v)
        ¬ (v. card {q. msgs q = Some v} > E) 
          decide st' = decide st)"

subsection ‹Communication predicate for $A_{T,E}$›

definition Ate_commPerRd where
  "Ate_commPerRd HOrs SHOrs 
   p. card (HOrs p - SHOrs p)  α"

text ‹
  The global communication predicate stipulates the three following
  \item for every process p› there are infinitely many rounds 
    where p› receives more than T› messages,
  \item for every process p› there are infinitely many rounds 
    where p› receives more than E› uncorrupted messages,
  \item and there are infinitely many rounds in which more than
    E - α› processes receive uncorrupted messages from the
    same set of processes, which contains more than T› processes.
  Ate_commGlobal where
  "Ate_commGlobal HOs SHOs 
     (r p. r' > r. card (HOs r' p) > T)
    (r p.  r' > r. card (SHOs r' p  HOs r' p) > E)
    (r. r' > r. π1 π2.
        card π1 > E - α
       card π2 > T
       (p  π1. HOs r' p = π2  SHOs r' p  HOs r' p = π2))"

subsection ‹The $A_{T,E}$ Heard-Of machine›

text ‹
  We now define the non-coordinated SHO machine for the Ate algorithm
  by assembling the algorithm definition and its communication-predicate.

definition Ate_SHOMachine where
  "Ate_SHOMachine =  
    CinitState =  (λ p st crd. Ate_initState p (st::('val::linorder) pstate)),
    sendMsg =  Ate_sendMsg,
    CnextState = (λ r p st msgs crd st'. Ate_nextState r p st msgs st'),
    SHOcommPerRd = (Ate_commPerRd:: process HO  process HO  bool),
    SHOcommGlobal = Ate_commGlobal

  "Ate_M  (Ate_SHOMachine::(process, 'val::linorder pstate, 'val) SHOMachine)"

end   ― ‹locale @{text "ate_parameters"}

end   (* theory AteDefs *)