Theory Ate_Defs

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

theory Ate_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 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"

begin

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}}"

definition 
  Ate_sendMsg :: "nat ⇒ process ⇒ process ⇒ 'val pstate ⇒ 'val"
where
  "Ate_sendMsg r p q st ≡ x st"

definition
  Ate_nextState :: "nat ⇒ process ⇒ ('val::linorder) pstate ⇒ (process ⇒ 'val option)
                        ⇒ 'val pstate ⇒ bool"
where
  "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
  conditions:
  \begin{itemize}
  \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.
  \end{itemize}
›
definition
  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
   ⦈"

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

end   ― ‹locale @{text "ate_parameters"}›

end   (* theory AteDefs *)