Theory UteDefs

theory UteDefs
imports "../HOModel"
begin

section ‹Verification of the \ute{} Consensus Algorithm›

text ‹
  Algorithm \ute{} is presented in~\<^cite>‹"biely:tolerating"›. It is an
  uncoordinated algorithm that tolerates value (a.k.a.\ Byzantine) faults,
  and can be understood as a variant of \emph{UniformVoting}. The parameters
  $T$, $E$, and $\alpha$ appear as thresholds of the algorithm and in the
  communication predicates. Their values can be chosen within certain bounds
  in order to adapt the algorithm to the characteristics of different systems.

  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 algorithm proceeds in \emph{phases} of $2$ rounds each (we call
  \emph{steps} the individual rounds that constitute a phase).
  The following utility functions compute the phase and step of a round,
  given the round number.
›

abbreviation
 "nSteps ≡ 2"
definition phase where "phase (r::nat) ≡ r div nSteps"
definition step where "step (r::nat) ≡ r mod nSteps"

lemma phase_zero [simp]: "phase 0 = 0"
by (simp add: phase_def)

lemma step_zero [simp]: "step 0 = 0"
by (simp add: step_def)

lemma phase_step: "(phase r * nSteps) + step r = r"
  by (auto simp add: phase_def step_def)

text ‹The following record models the local state of a process.›

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

text ‹Possible messages sent during the execution of the algorithm.›

datatype 'val msg =
   Val "'val"
 | Vote "'val option"

text ‹
  The ‹x› field of the initial state is unconstrained, all other
  fields are initialized appropriately.
›

definition Ute_initState where
  "Ute_initState p st ≡
   (vote st = None) ∧ (decide st = None)"

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

locale ute_parameters =
  fixes α::nat and T::nat and E::nat
  assumes majE: "2*E ≥ N + 2*α"
      and majT: "2*T ≥ N + 2*α"
      and EltN: "E < N"
      and TltN: "T < N"
begin

text ‹Simple consequences of the above parameter constraints.›

lemma alpha_lt_N: "α < N"
using EltN majE by auto

lemma alpha_lt_T: "α < T"
using majT alpha_lt_N by auto

lemma alpha_lt_E: "α < E"
using majE alpha_lt_N by auto

text ‹
  We separately define the transition predicates and the send functions
  for each step and later combine them to define the overall next-state relation.
›

text ‹
  In step 0, each process sends its current ‹x›.
  If it receives the value $v$ more than $T$ times, it votes for $v$,
  otherwise it doesn't vote.
›

definition
  send0 :: "nat ⇒ Proc ⇒ Proc ⇒ 'val pstate ⇒ 'val msg"
where
  "send0 r p q st ≡ Val (x st)"

definition
  next0 :: "nat ⇒ Proc ⇒ 'val pstate ⇒ (Proc ⇒ 'val msg option) 
                ⇒ 'val pstate ⇒ bool" 
where
  "next0 r p st msgs st' ≡
     (∃v. card {q. msgs q = Some (Val v)} > T ∧ st' = st ⦇ vote := Some v ⦈)
   ∨ ¬(∃v. card {q. msgs q = Some (Val v)} > T) ∧ st' = st ⦇ vote := None ⦈"

text ‹
  In step 1, each process sends its current ‹vote›.

  If it receives more than ‹α› votes for a given value ‹v›,
  it sets its ‹x› field to ‹v›, else it sets ‹x› to a
  default value.

  If the process receives more than ‹E› votes for ‹v›, it decides
  ‹v›, otherwise it leaves its decision unchanged.
›

definition
  send1 :: "nat ⇒ Proc ⇒ Proc ⇒ 'val pstate ⇒ 'val msg" 
where
  "send1 r p q st ≡ Vote (vote st)"

definition
  next1 :: "nat ⇒ Proc ⇒ 'val pstate ⇒ (Proc ⇒ 'val msg option) 
                ⇒ 'val pstate ⇒ bool" 
where
  "next1 r p st msgs st' ≡
    ( (∃v. card {q. msgs q = Some (Vote (Some v))} > α ∧ x st' = v)
     ∨ ¬(∃v. card {q. msgs q = Some (Vote (Some v))} > α) 
         ∧ x st' = undefined  )
  ∧ ( (∃v. card {q. msgs q = Some (Vote (Some v))} > E ∧ decide st' = Some v)
     ∨ ¬(∃v. card {q. msgs q = Some (Vote (Some v))} > E) 
         ∧ decide st' = decide st )
  ∧ vote st' = None"

text ‹
  The overall send function and next-state relation are simply obtained as
  the composition of the individual relations defined above.
›

definition 
  Ute_sendMsg :: "nat ⇒ Proc ⇒ Proc ⇒ 'val pstate ⇒ 'val msg" 
where
  "Ute_sendMsg (r::nat) ≡ if step r = 0 then send0 r else send1 r"

definition 
  Ute_nextState :: "nat ⇒ Proc ⇒ 'val pstate ⇒ (Proc ⇒ 'val msg option)
                        ⇒ 'val pstate ⇒ bool" 
where
  "Ute_nextState r ≡ if step r = 0 then next0 r else next1 r"


subsection ‹Communication Predicate for \ute{}›

text ‹
  Following~\<^cite>‹"biely:tolerating"›, we now define the communication predicate
  for the \ute{} algorithm to be correct.

  The round-by-round predicate stipulates the following conditions:
  \begin{itemize}
  \item no process may receive more than ‹α› corrupted messages, and
  \item every process should receive more than ‹max(T, N + 2*α - E - 1)› 
    correct messages.
  \end{itemize}
  \<^cite>‹"biely:tolerating"› also requires that every process should receive more
  than ‹α› correct messages, but this is implied, since ‹T > α›
  (cf. lemma ‹alpha_lt_T›).
›

definition Ute_commPerRd where
  "Ute_commPerRd HOrs SHOrs ≡
   ∀p. card (HOrs p - SHOrs p) ≤ α
     ∧ card (SHOrs p ∩ HOrs p) > N + 2*α - E - 1
     ∧ card (SHOrs p ∩ HOrs p) > T"

text ‹
  The global communication predicate requires there exists some phase
  ‹Φ› such that:
  \begin{itemize}
  \item all HO and SHO sets of all processes are equal in the second step
    of phase ‹Φ›, i.e.\ all processes receive messages from the 
    same set of processes, and none of these messages is corrupted,
  \item every process receives more than ‹T› correct messages in
    the first step of phase ‹Φ+1›, and
  \item every process receives more than ‹E› correct messages in the
    second step of phase ‹Φ+1›.
  \end{itemize}
  The predicate in the article~\<^cite>‹"biely:tolerating"› requires infinitely
  many such phases, but one is clearly enough.
›

definition Ute_commGlobal where
  "Ute_commGlobal HOs SHOs ≡
    ∃Φ. (let r = Suc (nSteps*Φ)
         in  (∃π. ∀p. π = HOs r p ∧ π = SHOs r p)
           ∧ (∀p. card (SHOs (Suc r) p ∩ HOs (Suc r) p) > T)
           ∧ (∀p. card (SHOs (Suc (Suc r)) p ∩ HOs (Suc (Suc r)) p) > E))"


subsection ‹The \ute{} Heard-Of Machine›

text ‹
  We now define the coordinated HO machine for the \ute{} algorithm
  by assembling the algorithm definition and its communication-predicate.
›

definition Ute_SHOMachine where
  "Ute_SHOMachine = ⦇
     CinitState =  (λ p st crd. Ute_initState p st),
     sendMsg =  Ute_sendMsg,
     CnextState = (λ r p st msgs crd st'. Ute_nextState r p st msgs st'),
     SHOcommPerRd = Ute_commPerRd,
     SHOcommGlobal = Ute_commGlobal 
   ⦈"

abbreviation
  "Ute_M ≡ (Ute_SHOMachine::(Proc, 'val pstate, 'val msg) SHOMachine)"

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

end   (* theory UteDefs *)