theory AteDefs
imports "../HOModel"
begin

section ‹Verification of the \ate{} Consensus algorithm›

text ‹
 Algorithm \ate{} is presented in~cite‹"biely:tolerating"›. Like \ute{},
 it is an uncoordinated algorithm that tolerates value faults, and it
 is parameterized by values $T$, $E$, and $\alpha$ that serve a similar
 function as in \ute{}, allowing the algorithm to be adapted to the
 characteristics of different systems. \ate{} can be understood as a
 variant of \emph{OneThirdRule} tolerating Byzantine faults.

 We formalize in Isabelle the correctness proof of the algorithm that
 appears in~cite‹"biely:tolerating"›, 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 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)"

text ‹
 The following locale introduces the parameters used for the \ate{}
 algorithm and their constraints~cite‹"biely:tolerating"›.
 ›

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::Proc → 'val option) ≡
   {v. ∀w. card {qq. msgs qq = Some w} ≤ card {qq. msgs qq = Some v}}"

definition 
  Ate_sendMsg :: "nat → Proc → Proc → 'val pstate → 'val"
where
  "Ate_sendMsg r p q st ≡ x st"

definition
  Ate_nextState :: "nat → Proc → ('val::linorder) pstate → (Proc → '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 \ate{}›

text ‹
 Following~cite‹"biely:tolerating"›, we now define the communication
 predicate for the \ate{} algorithm. The round-by-round predicate
 requires that no process may receive more than ‹α› corrupted
 messages at any round.
 ›
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 \ate{} 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:: Proc HO → Proc HO → bool),
    SHOcommGlobal = Ate_commGlobal
   )"

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

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

end   (* theory AteDefs *)