Theory HOModel

theory HOModel
imports Main
begin

declare if_split_asm [split] ― ‹perform default perform case splitting on conditionals›

section ‹Heard-Of Algorithms›

subsection ‹The Consensus Problem›

text ‹
  We are interested in the verification of fault-tolerant distributed algorithms.
  The Consensus problem is paradigmatic in this area. Stated
  informally, it assumes that all processes participating in the algorithm
  initially propose some value, and that they may at some point decide some value.
  It is required that every process eventually decides, and that all processes
  must decide the same value.

  More formally, we represent runs of algorithms as ‹ω›-sequences of
  configurations (vectors of process states). Hence, a run is modeled as
  a function of type ‹nat ⇒ 'proc ⇒ 'pst› where type variables 
  ‹'proc› and ‹'pst› represent types of processes and process
  states, respectively. The Consensus property is expressed with respect
  to a collection ‹vals› of initially proposed values (one per process) 
  and an observer function ‹dec::'pst ⇒ val option› that retrieves the decision
  (if any) from a process state. The Consensus problem is stated as the conjunction
  of the following properties:
  \begin{description}
  \item[Integrity.] Processes can only decide initially proposed values.
  \item[Agreement.] Whenever processes ‹p› and ‹q› decide,
    their decision values must be the same. (In particular, process ‹p›
    may never change the value it decides, which is referred to as Irrevocability.)
  \item[Termination.] Every process decides eventually.
  \end{description}

  The above properties are sometimes only required of non-faulty processes, since
  nothing can be required of a faulty process.
  The Heard-Of model does not attribute faults to processes, and therefore the
  above formulation is appropriate in this framework.
›

type_synonym
  ('proc,'pst) run = "nat ⇒ 'proc ⇒ 'pst"

definition
  consensus :: "('proc ⇒ 'val) ⇒ ('pst ⇒ 'val option) ⇒ ('proc,'pst) run ⇒ bool"
where
  "consensus vals dec rho ≡
     (∀n p v. dec (rho n p) = Some v ⟶ v ∈ range vals)
   ∧ (∀m n p q v w. dec (rho m p) = Some v ∧ dec (rho n q) = Some w 
         ⟶ v = w)
   ∧ (∀p. ∃n. dec (rho n p) ≠ None)"

text ‹
  A variant of the Consensus problem replaces the Integrity requirement by
  \begin{description}
  \item[Validity.] If all processes initially propose the same value ‹v›
    then every process may only decide ‹v›.
  \end{description}
›

definition weak_consensus where
  "weak_consensus vals dec rho ≡
     (∀v. (∀p. vals p = v) ⟶ (∀n p w. dec (rho n p) = Some w ⟶ w = v))
   ∧ (∀m n p q v w. dec (rho m p) = Some v ∧ dec (rho n q) = Some w 
         ⟶ v = w)
   ∧ (∀p. ∃n. dec (rho n p) ≠ None)"

text ‹
  Clearly, ‹consensus› implies ‹weak_consensus›.
›

lemma consensus_then_weak_consensus:
  assumes "consensus vals dec rho"
  shows "weak_consensus vals dec rho"
  using assms by (auto simp: consensus_def weak_consensus_def image_def)

text ‹
  Over Boolean values (``binary Consensus''), ‹weak_consensus›
  implies ‹consensus›, hence the two problems are equivalent.
  In fact, this theorem holds more generally whenever at most two
  different values are proposed initially (i.e., ‹card (range vals) ≤ 2›).
›

lemma binary_weak_consensus_then_consensus:
  assumes bc: "weak_consensus (vals::'proc ⇒ bool) dec rho"
  shows "consensus vals dec rho"
proof -
  { ― ‹Show the Integrity property, the other conjuncts are the same.›
    fix n p v
    assume dec: "dec (rho n p) = Some v"
    have "v ∈ range vals"
    proof (cases "∃w. ∀p. vals p = w")
      case True
      then obtain w where w: "∀p. vals p = w" ..
      with bc have "dec (rho n p) ∈ {Some w, None}" by (auto simp: weak_consensus_def)
      with dec w show ?thesis by (auto simp: image_def)
    next
      case False
      ― ‹In this case both possible values occur in @{text "vals"}, and the result is trivial.›
      thus ?thesis by (auto simp: image_def)
    qed
  } note integrity = this
  from bc show ?thesis
    unfolding consensus_def weak_consensus_def by (auto elim!: integrity)
qed

text ‹
  The algorithms that we are going to verify solve the Consensus or weak Consensus
  problem, under different hypotheses about the kinds and number of faults.
›


subsection ‹A Generic Representation of Heard-Of Algorithms›

text ‹
  Charron-Bost and Schiper~\<^cite>‹"charron:heardof"› introduce
  the Heard-Of (HO) model for representing fault-tolerant
  distributed algorithms. In this model, algorithms execute in communication-closed
  rounds: at any round~$r$, processes only receive messages that were sent for
  that round. For every process~$p$ and round~$r$, the ``heard-of set'' $HO(p,r)$
  denotes the set of processes from which~$p$ receives a message in round~$r$.
  Since every process is assumed to send a message to all processes in each round,
  the complement of $HO(p,r)$ represents the set of faults that may affect~$p$ in
  round~$r$ (messages that were not received, e.g. because the sender crashed,
  because of a network problem etc.).

  The HO model expresses hypotheses on the faults tolerated by an algorithm
  through ``communication predicates'' that constrain the sets $HO(p,r)$
  that may occur during an execution. Charron-Bost and Schiper show that
  standard fault models can be represented in this form.

  The original HO model is sufficient for representing algorithms
  tolerating benign failures such as process crashes or message loss. A later
  extension for algorithms tolerating Byzantine (or value) failures~\<^cite>‹"biely:tolerating"› 
  adds a second collection of sets $SHO(p,r) \subseteq HO(p,r)$ that contain those
  processes $q$ from which process $p$ receives the message that $q$ was indeed
  supposed to send for round $r$ according to the algorithm. In other words, 
  messages from processes in $HO(p,r) \setminus SHO(p,r)$ were corrupted, be it
  due to errors during message transmission or because of the sender was faulty or
  lied deliberately. For both benign and Byzantine errors, the HO model registers
  the fault but does not try to identify the faulty component (i.e., designate the
  sending or receiving process, or the communication channel as the ``culprit'').

  Executions of HO algorithms are defined with respect to collections
  $HO(p,r)$ and $SHO(p,r)$. However, the code of a process does not have
  access to these sets. In particular, process $p$ has no way of determining
  if a message it received from another process $q$ corresponds to what $q$
  should have sent or if it has been corrupted.

  Certain algorithms rely on the assignment of ``coordinator'' processes for
  each round. Just as the collections $HO(p,r)$, the definitions assume an
  external coordinator assignment such that $coord(p,r)$ denotes the coordinator
  of process $p$ and round $r$. Again, the correctness of algorithms may depend
  on hypotheses about coordinator assignments -- e.g., it may be assumed that
  processes agree sufficiently often on who the current coordinator is.

  The following definitions provide a generic representation of HO and SHO algorithms
  in Isabelle/HOL. A (coordinated) HO algorithm is described by the following parameters:
  \begin{itemize}
  \item a finite type ‹'proc› of processes,
  \item a type ‹'pst› of local process states,
  \item a type ‹'msg› of messages sent in the course of the algorithm,
  \item a predicate ‹CinitState› such that ‹CinitState p st crd› is
    true precisely of the initial states ‹st› of process ‹p›, assuming
    that ‹crd› is the initial coordinator of ‹p›,
  \item a function ‹sendMsg› where ‹sendMsg r p q st› yields
    the message that process ‹p› sends to process ‹q› at round
    ‹r›, given its local state ‹st›, and
  \item a predicate ‹CnextState› where ‹CnextState r p st msgs crd st'›
    characterizes the successor states ‹st'› of process ‹p› at round
    ‹r›, given current state ‹st›, the vector
    ‹msgs :: 'proc ⇒ 'msg option› of messages that ‹p› received at
    round ‹r› (‹msgs q = None› indicates that no message has been
    received from process ‹q›),
    and process ‹crd› as the coordinator for the following round.
  \end{itemize}
  Note that every process can store the coordinator for the current round in its
  local state, and it is therefore not necessary to make the coordinator a parameter
  of the message sending function ‹sendMsg›.

  We represent an algorithm by a record as follows.
›

record ('proc, 'pst, 'msg) CHOAlgorithm =
  CinitState ::  "'proc ⇒ 'pst ⇒ 'proc ⇒ bool"
  sendMsg ::   "nat ⇒ 'proc ⇒ 'proc ⇒ 'pst ⇒ 'msg"
  CnextState :: "nat ⇒ 'proc ⇒ 'pst ⇒ ('proc ⇒ 'msg option) ⇒ 'proc ⇒ 'pst ⇒ bool"

text ‹
  For non-coordinated HO algorithms, the coordinator argument of functions
  ‹CinitState› and ‹CnextState› is irrelevant, and we
  define utility functions that omit that argument.
›

definition isNCAlgorithm where
  "isNCAlgorithm alg ≡ 
      (∀p st crd crd'. CinitState alg p st crd = CinitState alg p st crd')
   ∧ (∀r p st msgs crd crd' st'. CnextState alg r p st msgs crd st'
                               = CnextState alg r p st msgs crd' st')"

definition initState where
  "initState alg p st ≡ CinitState alg p st undefined"

definition nextState where
  "nextState alg r p st msgs st' ≡ CnextState alg r p st msgs undefined st'"

text ‹
  A \emph{heard-of assignment} associates a set of processes with each
  process. The following type is used to represent the collections $HO(p,r)$
  and $SHO(p,r)$ for fixed round $r$.
%
  Similarly, a \emph{coordinator assignment} associates a process (its coordinator)
  to each process.
›

type_synonym
  'proc HO = "'proc ⇒ 'proc set"

type_synonym
  'proc coord = "'proc ⇒ 'proc"

text ‹
  An execution of an HO algorithm is defined with respect to HO and SHO
  assignments that indicate, for every round ‹r› and every process ‹p›,
  from which sender processes ‹p› receives messages (resp., uncorrupted
  messages) at round ‹r›.

%% That's the intention, but we don't enforce this in the definitions.
%  Obviously, SHO sets are always included in HO sets, for the same process and round.

  The following definitions formalize this idea. We define ``coarse-grained''
  executions whose unit of atomicity is the round of execution. At each round,
  the entire collection of processes performs a transition according to the
  ‹CnextState› function of the algorithm. Consequently, a system state is
  simply described by a configuration, i.e. a function assigning a process state
  to every process. This definition of executions may appear surprising for an
  asynchronous distributed system, but it simplifies system verification,
  compared to a ``fine-grained'' execution model that records individual events
  such as message sending and reception or local transitions. We will justify
  later why the ``coarse-grained'' model is sufficient for verifying interesting
  correctness properties of HO algorithms.

  The predicate ‹CSHOinitConfig› describes the possible initial configurations
  for algorithm ‹A› (remember that a configuration is a function that assigns
  local states to every process).
›

definition CHOinitConfig where
  "CHOinitConfig A cfg (coord::'proc coord) ≡ ∀p. CinitState A p (cfg p) (coord p)"

text ‹
  Given the current configuration ‹cfg› and the HO and SHO sets ‹HOp›
  and ‹SHOp› for process ‹p› at round ‹r›, the function
  ‹SHOmsgVectors› computes the set of possible vectors of messages that
  process ‹p› may receive. For processes ‹q ∉ HOp›, ‹p› 
  receives no message (represented as value ‹None›). For processes
  ‹q ∈ SHOp›, ‹p› receives the message that ‹q› computed
  according to the ‹sendMsg› function of the algorithm. For the remaining
  processes ‹q ∈ HOp - SHOp›, ‹p› may receive some arbitrary value.
›

definition SHOmsgVectors where
  "SHOmsgVectors A r p cfg HOp SHOp ≡
   {μ. (∀q. q ∈ HOp ⟷ μ q ≠ None)
     ∧ (∀q. q ∈ SHOp ∩ HOp ⟶ μ q = Some (sendMsg A r q p (cfg q)))}"

text ‹
  Predicate ‹CSHOnextConfig› uses the preceding function and the algorithm's
  ‹CnextState› function to characterize the possible successor configurations
  in a coarse-grained step, and predicate ‹CSHORun› defines (coarse-grained)
  executions ‹rho› of an HO algorithm.
›

definition CSHOnextConfig where
  "CSHOnextConfig A r cfg HO SHO coord cfg' ≡
   ∀p. ∃μ ∈ SHOmsgVectors A r p cfg (HO p) (SHO p).
          CnextState A r p (cfg p) μ (coord p) (cfg' p)"

definition CSHORun where
  "CSHORun A rho HOs SHOs coords ≡
     CHOinitConfig A (rho 0) (coords 0)
   ∧ (∀r. CSHOnextConfig A r (rho r) (HOs r) (SHOs r) (coords (Suc r))
                             (rho (Suc r)))"

text ‹
  For non-coordinated algorithms. the ‹coord› arguments of the above functions
  are irrelevant. We define similar functions that omit that argument, and relate
  them to the above utility functions for these algorithms.
›

definition HOinitConfig where
  "HOinitConfig A cfg ≡ CHOinitConfig A cfg (λq. undefined)"

lemma HOinitConfig_eq:
  "HOinitConfig A cfg = (∀p. initState A p (cfg p))"
  by (auto simp: HOinitConfig_def CHOinitConfig_def initState_def)

definition SHOnextConfig where
  "SHOnextConfig A r cfg HO SHO cfg' ≡
   CSHOnextConfig A r cfg HO SHO (λq. undefined) cfg'"

lemma SHOnextConfig_eq:
  "SHOnextConfig A r cfg HO SHO cfg' =
   (∀p. ∃μ ∈ SHOmsgVectors A r p cfg (HO p) (SHO p).
             nextState A r p (cfg p) μ (cfg' p))"
  by (auto simp: SHOnextConfig_def CSHOnextConfig_def SHOmsgVectors_def nextState_def)

definition SHORun where
  "SHORun A rho HOs SHOs ≡
   CSHORun A rho HOs SHOs (λr q. undefined)"

lemma SHORun_eq:
  "SHORun A rho HOs SHOs =
     (HOinitConfig A (rho 0)
   ∧ (∀r. SHOnextConfig A r (rho r) (HOs r) (SHOs r) (rho (Suc r))))"
  by (auto simp: SHORun_def CSHORun_def HOinitConfig_def SHOnextConfig_def)

text ‹
  Algorithms designed to tolerate benign failures are not subject to
  message corruption, and therefore the SHO sets are irrelevant (more formally,
  each SHO set equals the corresponding HO set). We define corresponding
  special cases of the definitions of successor configurations and of runs,
  and prove that these are equivalent to simpler definitions that will be more
  useful in proofs. In particular, the vector of messages received by a process
  in a benign execution is uniquely determined from the current configuration
  and the HO sets.
›

definition HOrcvdMsgs where
  "HOrcvdMsgs A r p HO cfg ≡
   λq. if q ∈ HO then Some (sendMsg A r q p (cfg q)) else None"

lemma SHOmsgVectors_HO:
  "SHOmsgVectors A r p cfg HO HO = {HOrcvdMsgs A r p HO cfg}"
  unfolding SHOmsgVectors_def HOrcvdMsgs_def by auto

text ‹With coordinators›

definition CHOnextConfig where
  "CHOnextConfig A r cfg HO coord cfg' ≡ 
   CSHOnextConfig A r cfg HO HO coord cfg'"

lemma CHOnextConfig_eq:
  "CHOnextConfig A r cfg HO coord cfg' =
   (∀p. CnextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg) 
                   (coord p) (cfg' p))"
  by (auto simp: CHOnextConfig_def CSHOnextConfig_def SHOmsgVectors_HO)

definition CHORun where
  "CHORun A rho HOs coords ≡ CSHORun A rho HOs HOs coords"

lemma CHORun_eq:
  "CHORun A rho HOs coords = 
     (CHOinitConfig A (rho 0) (coords 0)
      ∧ (∀r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r))))"
  by (auto simp: CHORun_def CSHORun_def CHOinitConfig_def CHOnextConfig_def)

text ‹Without coordinators›
definition HOnextConfig where
  "HOnextConfig A r cfg HO cfg' ≡ SHOnextConfig A r cfg HO HO cfg'"

lemma HOnextConfig_eq:
  "HOnextConfig A r cfg HO cfg' =
   (∀p. nextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg) (cfg' p))"
  by (auto simp: HOnextConfig_def SHOnextConfig_eq SHOmsgVectors_HO)

definition HORun where
  "HORun A rho HOs ≡ SHORun A rho HOs HOs"

lemma HORun_eq:
  "HORun A rho HOs = 
   (  HOinitConfig A (rho 0)
    ∧ (∀r. HOnextConfig A r (rho r) (HOs r) (rho (Suc r))))"
  by (auto simp: HORun_def SHORun_eq HOnextConfig_def)


text ‹
  The following derived proof rules are immediate consequences of
  the definition of ‹CHORun›; they simplify automatic reasoning.
›

lemma CHORun_0:
  assumes "CHORun A rho HOs coords" 
      and "⋀cfg. CHOinitConfig A cfg (coords 0) ⟹ P cfg"
  shows "P (rho 0)"
using assms unfolding CHORun_eq by blast

lemma CHORun_Suc:
  assumes "CHORun A rho HOs coords"
  and "⋀r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r))
            ⟹ P r"
  shows "P n"
using assms unfolding CHORun_eq by blast

lemma CHORun_induct:
  assumes run: "CHORun A rho HOs coords"
  and init: "CHOinitConfig A (rho 0) (coords 0) ⟹ P 0"
  and step: "⋀r. ⟦ P r; CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) 
                                      (rho (Suc r)) ⟧ ⟹ P (Suc r)"
  shows "P n"
using run unfolding CHORun_eq by (induct n, auto elim: init step)

text ‹
  Because algorithms will not operate for arbitrary HO, SHO, and coordinator
  assignments, these are constrained by a \emph{communication predicate}.
  For convenience, we split this predicate into a \emph{per Round} part that
  is expected to hold at every round and a \emph{global} part that must hold
  of the sequence of (S)HO assignments and may thus express liveness assumptions.

  In the parlance of~\<^cite>‹"charron:heardof"›, a \emph{HO machine} is an HO algorithm
  augmented with a communication predicate. We therefore define (C)(S)HO machines as
  the corresponding extensions of the record defining an HO algorithm.
›

record ('proc, 'pst, 'msg) HOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
  HOcommPerRd::"'proc HO ⇒ bool"
  HOcommGlobal::"(nat ⇒ 'proc HO) ⇒ bool"

record ('proc, 'pst, 'msg) CHOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
  CHOcommPerRd::"nat ⇒ 'proc HO ⇒ 'proc coord ⇒ bool"
  CHOcommGlobal::"(nat ⇒ 'proc HO) ⇒ (nat ⇒ 'proc coord) ⇒ bool"

record ('proc, 'pst, 'msg) SHOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
  SHOcommPerRd::"('proc HO) ⇒ ('proc HO) ⇒ bool"
  SHOcommGlobal::"(nat ⇒ 'proc HO) ⇒ (nat ⇒ 'proc HO) ⇒ bool"

record ('proc, 'pst, 'msg) CSHOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
  CSHOcommPerRd::"('proc HO) ⇒ ('proc HO) ⇒ 'proc coord ⇒ bool"
  CSHOcommGlobal::"(nat ⇒ 'proc HO) ⇒ (nat ⇒ 'proc HO)
                                     ⇒ (nat ⇒ 'proc coord) ⇒ bool"

end ― ‹theory HOModel›