Quelle  Reduction.thy

theory Reduction
imports HOModel Stuttering_Equivalence.StutterEquivalence
begin

section ‹Reduction Theorem›

text ‹
 We have defined the semantics of HO algorithms such that rounds are executed
 atomically, by all processes. This definition is surprising for a model of
 asynchronous distributed algorithms since it models a synchronous execution
 of rounds. However, it simplifies representing and reasoning about the algorithms.
 For example, the communication network does not have to be modeled explicitly,
 since the possible sets of messages received by processes can be computed
 from the global configuration and the collections of HO and SHO sets.

 We will now define a more conventional ``fine-grained'' semantics where
 communication is modeled explicitly and rounds of processes can be arbitrarily
 interleaved (subject to the constraints of the communication predicates).
 We will then establish a \emph{reduction theorem} that shows that for every
 fine-grained run there exists an equivalent round-based (``coarse-grained'')
 run in the sense that the two runs exhibit the same sequences of local states
 of all processes, modulo stuttering. We prove the reduction theorem for the
 most general class of coordinated SHO algorithms. It is easy to see that the
 theorem equally holds for the special cases of uncoordinated or HO algorithms,
 and since we have in fact defined these classes of algorithms from the more
 general ones, we can directly apply the general theorem.

 As a corollary, interesting properties remain valid in the fine-grained semantics
 if they hold in the coarse-grained semantics. It is therefore enough to
 verify such properties in the coarse-grained semantics, which is much easier
 to reason about. The essential restriction is that properties may not depend
 on states of different processes occurring simultaneously. (For example, the
 coarse-grained semantics ensures by definition that all processes execute the
 same round at any instant, which is obviously not true of the fine-grained
 semantics.) We claim that all ``reasonable'' properties of fault-tolerant
 distributed algorithms are preserved by our reduction. For example, the
 Consensus (and Weak Consensus) problems fall into this class.

 The proofs follow Chaouch-Saad et al.~cite‹"saad:reduction"›, where the
 reduction theorem was proved for uncoordinated HO algorithms.
 ›

subsection ‹Fine-Grained Semantics›

text ‹
 In the fine-grained semantics, a run of an HO algorithm is represented
 as an $\omega$-sequence of system configurations. Each configuration
 is represented as a record carrying the following information:
 \begin{itemize}
 \item for every process $p$, the current round that process $p$ is executing,
 \item the local state of every process,
 \item for every process $p$, the set of processes to which $p$ has already
 sent a message for the current round,
 \item for all processes $p$ and $q$, the message (if any) that $p$ has
 received from $q$ for the round that $p$ is currently executing, and
 \item the set of messages in transit, represented as triples of the form
 $(p,r,q,m)$ meaning that process $p$ sent message $m$ to process $q$
 for round $r$, but $q$ has not yet received that message.
 \end{itemize}

 As explained earlier, the coordinators of processes are not recorded in
 the configuration, but algorithms may record them as part of the process states.
 ›

record ('pst, 'proc, 'msg) config =
  round :: "'proc ==> nat"
  state :: "'proc ==> 'pst"
  sent  :: "'proc ==> 'proc set"
  rcvd  :: "'proc ==> 'proc ==> 'msg option"
  network :: " ('proc * nat * 'proc * 'msg) set"

type_synonym ('pst ,'proc , 'msg) fgrun = "nat ==> ('pst, 'proc, 'msg) config"

text ‹
 In an initial configuration for an algorithm, the local state of every process
 satisfies the algorithm's initial-state predicate, and all other components
 have obvious default values.
 ›

definition fg_init_config where
  "fg_init_config A (config::('pst,'proc, 'msg) config) (coord::'proc coord) ≡
     round config = (λp. 0)
   ∧ (∀p. CinitState A p (state config p) (coord p))
   ∧ sent config = (λp. {})
   ∧ rcvd config = (λp q. None)
   ∧ network config = {}"

text ‹
 In the fine-grained semantics, we have three types of transitions due to
 \begin{itemize}
 \item some process sending a message,
 \item some process receiving a message, and
 \item some process executing a local transition.
 \end{itemize}

 The following definition models process ‹p› sending a message to
 process ‹q›. The transition is enabled if ‹p› has not yet
 sent any message to ‹q› for the current round. The message to be
 sent is computed according to the algorithm's ‹sendMsg› function.
 The effect of the transition is to add ‹q› to the ‹sent›
 component of the configuration and the message quadruple to the
 ‹network› component.
 ›

definition fg_send_msg where
  "fg_send_msg A p q config config' ≡
     q ∉ (sent config p)
   ∧ config' = config (
        sent := (sent config)(p := (sent config p) ∪ {q}),
        network := network config ∪
                   {(p, round config p, q,
                     sendMsg A (round config p) p q (state config p))} )"

text ‹
 The following definition models the reception of a message by process
 ‹p› from process ‹q›. The action is enabled if ‹q›
 is in the heard-of set ‹HO› of process ‹p› for the current
 round, and if the network contains some message from ‹q› to
 ‹p› for the round that ‹p› is currently executing.
 W.l.o.g., we model message corruption at reception: if ‹q› is not
 in ‹p›'s SHO set (parameter ‹SHO›), then an arbitrary value
 ‹m'› is received instead of ‹m›.
 ›

definition fg_rcv_msg where
  "fg_rcv_msg p q HO SHO config config' ≡
   ∃m m'. (q, (round config p), p, m) ∈ network config
     ∧ q ∈ HO
     ∧ config' = config (
          rcvd := (rcvd config)(p := (rcvd config p)(q :=
                    if q ∈ SHO then Some m else Some m')),
          network := network config - {(q, (round config p), p, m)} )"

text ‹
 Finally, we consider local state transition of process ‹p›.
 A local transition is enabled only after ‹p› has sent all messages
 for its current round and has received all messages that it is supposed
 to receive according to its current HO set (parameter ‹HO›). The
 local state is updated according to the algorithm's ‹CnextState›
 relation, which may depend on the coordinator ‹crd› of the following
 round. The round of process ‹p› is incremented, and the
 ‹sent› and ‹rcvd› components for process ‹p› are
 reset to initial values for the new round.
 ›

definition fg_local where
  "fg_local A p HO crd config config' ≡
     sent config p = UNIV
   ∧ dom (rcvd config p) = HO
   ∧ (∃s. CnextState A (round config p) p (state config p) (rcvd config p) crd s
        ∧ config' = config (
             round := (round config)(p := Suc (round config p)),
             state := (state config)(p := s),
             sent := (sent config)(p := {}),
             rcvd := (rcvd config)(p := λq. None) ))"

text ‹
 The next-state relation for process ‹p› is just the disjunction of
 the above three types of transitions.
 ›

definition fg_next_config where
  "fg_next_config A p HO SHO crd config config' ≡
     (∃q. fg_send_msg A p q config config')
   ∨ (∃q. fg_rcv_msg p q HO SHO config config')
   ∨ fg_local A p HO crd config config'"

text ‹
 Fine-grained runs are infinite sequences of configurations that start
 in an initial configuration and where each step corresponds to some process
 sending a message, receiving a message or performing a local step. We also
 require that every process eventually executes every round -- note that
 this condition is implicit in the definition of coarse-grained runs.
 ›

definition fg_run where
  "fg_run A rho HOs SHOs coords ≡
      fg_init_config A (rho 0) (coords 0)
    ∧ (∀i. ∃p. fg_next_config A p
                                    (HOs (round (rho i) p) p)
                                    (SHOs (round (rho i) p) p)
                                    (coords (round (rho (Suc i)) p) p)
                                    (rho i) (rho (Suc i)))
    ∧ (∀p r. ∃n. round (rho n) p = r)"

text ‹
 The following function computes at which ``time point'' (index in the
 fine-grained computation) process ‹p› starts executing round
 ‹r›. This function plays an important role in the correspondence
 between the two semantics, and in the subsequent proofs.
 ›

definition fg_start_round where
  "fg_start_round rho p r ≡ LEAST (n::nat). round (rho n) p = r"


subsection ‹Properties of the Fine-Grained Semantics›

text ‹
 In preparation for the proof of the reduction theorem, we establish a
 number of consequences of the above definitions.
 ›

text ‹
 Process states change only when round numbers change during a
 fine-grained run.
 ›
lemma fg_state_change:
  assumes rho: "fg_run A rho HOs SHOs coords"
      and rd: "round (rho (Suc n)) p = round (rho n) p"
  shows "state (rho (Suc n)) p = state (rho n) p"
proof -
  from rho have "∃p'. fg_next_config A p' (HOs (round (rho n) p') p')
                                          (SHOs (round (rho n) p') p')
                                          (coords (round (rho (Suc n)) p') p')
                                          (rho n) (rho (Suc n))"
    by (auto simp: fg_run_def)
  with rd show ?thesis
    by (auto simp: fg_next_config_def fg_send_msg_def fg_rcv_msg_def fg_local_def)
qed

text ‹
 Round numbers never decrease.
 ›
lemma fg_round_numbers_increase:
  assumes rho: "fg_run A rho HOs SHOs coords" and n: "n ≤ m"
  shows "round (rho n) p ≤ round (rho m) p"
proof -
  from n obtain k where k: "m = n+k" by (auto simp: le_iff_add)
  {
    fix i
    have "round (rho n) p ≤ round (rho (n+i)) p" (is "?P i")
    proof (induct i)
      show "?P 0" by simp
    next
      fix j
      assume ih: "?P j"
      from rho have "∃p'. fg_next_config A p' (HOs (round (rho (n+j)) p') p')
                                              (SHOs (round (rho (n+j)) p') p')
                                              (coords (round (rho (Suc (n+j))) p') p')
                                              (rho (n+j)) (rho (Suc (n+j)))"
        by (auto simp: fg_run_def)
      hence "round (rho (n+j)) p ≤ round (rho (n + Suc j)) p"
        by (auto simp: fg_next_config_def fg_send_msg_def fg_rcv_msg_def fg_local_def)
      with ih show "?P (Suc j)" by auto
    qed
  }
  with k show ?thesis by simp
qed

text ‹
 Combining the two preceding lemmas, it follows that the local states
 of process ‹p› at two configurations are the same if these
 configurations have the same round number.
 ›
lemma fg_same_round_same_state:
  assumes rho: "fg_run A rho HOs SHOs coords"
      and rd: "round (rho m) p = round (rho n) p"
  shows "state (rho m) p = state (rho n) p"
proof -
  {
    fix k i
    have "round (rho (k+i)) p = round (rho k) p
          ==> state (rho (k+i)) p = state (rho k) p"
      (is "?R i ==> ?S i")
    proof (induct i)
      show "?S 0" by simp
    next
      fix j
      assume ih: "?R j ==> ?S j" 
         and r: "round (rho (k + Suc j)) p = round (rho k) p"
      from rho have 1: "round (rho k) p ≤ round (rho (k+j)) p"
        by (auto elim: fg_round_numbers_increase)
      from rho have 2: "round (rho (k+j)) p ≤ round (rho (k + Suc j)) p"
        by (auto elim: fg_round_numbers_increase)
      from 1 2 r have 3: "round (rho (k+j)) p = round (rho k) p" by auto
      with r have "round (rho (Suc (k+j))) p = round (rho (k+j)) p" by simp
      with rho have "state (rho (Suc (k+j))) p = state (rho (k+j)) p"
        by (auto elim: fg_state_change)
      with 3 ih show "?S (Suc j)" by simp
    qed
  }
  note aux = this
  show ?thesis
  proof (cases "n ≤ m")
    case True
    then obtain k where "m = n+k" by (auto simp: le_iff_add)
    with rd show ?thesis by (auto simp: aux)
  next
    case False
    hence "m ≤ n" by simp
    then obtain k where "n = m+k" by (auto simp: le_iff_add)
    with rd show ?thesis by (auto simp: aux)
  qed
qed

text ‹
 Since every process executes every round, function ‹fg_startRound›
 is well-defined. We also list a few facts about ‹fg_startRound› that
 will be used to show that it is a ``stuttering sampling function'',
 a notion introduced in the theories about stuttering equivalence.
 ›
lemma fg_start_round:
  assumes "fg_run A rho HOs SHOs coords"
  shows "round (rho (fg_start_round rho p r)) p = r"
using assms by (auto simp: fg_run_def fg_start_round_def intro: LeastI_ex)

lemma fg_start_round_smallest:
  assumes "round (rho k) p = r"
  shows "fg_start_round rho p r ≤ (k::nat)"
using assms unfolding fg_start_round_def by (rule Least_le)

lemma fg_start_round_later:
  assumes rho: "fg_run A rho HOs SHOs coords"
      and r: "round (rho n) p = r" and r': "r < r'"
  shows "n < fg_start_round rho p r'" (is "_ < ?start")
proof (rule ccontr)
  assume "¬ ?thesis"
  hence start: "?start ≤ n" by simp
  from rho this have "round (rho ?start) p ≤ round (rho n) p"
    by (rule fg_round_numbers_increase)
  with r have "r' ≤ r" by (simp add: fg_start_round[OF rho])
  with r' show "False" by simp
qed

lemma fg_start_round_0:
  assumes rho: "fg_run A rho HOs SHOs coords"
  shows "fg_start_round rho p 0 = 0"
proof -
  from rho have "round (rho 0) p = 0" by (auto simp: fg_run_def fg_init_config_def)
  hence "fg_start_round rho p 0 ≤ 0" by (rule fg_start_round_smallest)
  thus ?thesis by simp
qed

lemma fg_start_round_strict_mono:
  assumes rho: "fg_run A rho HOs SHOs coords"
  shows "strict_mono (fg_start_round rho p)"
proof
  fix r r'
  assume r: "(r::nat) < r'"
  from rho have "round (rho (fg_start_round rho p r)) p = r" by (rule fg_start_round)
  from rho this r show "fg_start_round rho p r < fg_start_round rho p r'"
    by (rule fg_start_round_later)
qed

text ‹
 Process ‹p› is at round ‹r› at all configurations between
 the start of round ‹r› and the start of round ‹r+1›.
 By lemma ‹fg_same_round_same_state›, this implies that the
 local state of process ‹p› is the same at all these configurations.
 ›
lemma fg_round_between_start_rounds:
assumes rho: "fg_run A rho HOs SHOs coords"
    and 1: "fg_start_round rho p r ≤ n"
    and 2: "n < fg_start_round rho p (Suc r)"
shows "round (rho n) p = r" (is "?rd = r")
proof (rule antisym)
  from 1 have "round (rho (fg_start_round rho p r)) p ≤ ?rd"
    by (rule fg_round_numbers_increase[OF rho])
  thus "r ≤ ?rd" by (simp add: fg_start_round[OF rho])
next
  show "?rd ≤ r"
  proof (rule ccontr)
    assume "¬ ?thesis"
    hence "Suc r ≤ ?rd" by simp
    hence "fg_start_round rho p (Suc r) ≤ fg_start_round rho p ?rd"
      by (rule rho[THEN fg_start_round_strict_mono, THEN strict_mono_mono, 
                   THEN monoD])
    also have "... ≤ n" by (auto intro: fg_start_round_smallest)
    also note 2
    finally show "False" by simp
  qed
qed

text ‹
 For any process ‹p› and round ‹r› there is some instant ‹n›
 where ‹p› executes a local transition from round ‹r›. In fact,
 ‹n+1› marks the start of round ‹r+1›.
 ›
lemma fg_local_transition_from_round:
assumes rho: "fg_run A rho HOs SHOs coords"
obtains n where "round (rho n) p = r"
            and "fg_start_round rho p (Suc r) = Suc n"
            and "fg_local A p (HOs r p) (coords (Suc r) p) (rho n) (rho (Suc n))"
proof -
  have "fg_start_round rho p (Suc r) ≠ 0" (is "?start ≠ 0")
  proof
    assume contr: "?start = 0"
    from rho have "round (rho ?start) p = Suc r" by (rule fg_start_round)
    with contr rho show "False" by (auto simp: fg_run_def fg_init_config_def)
  qed
  then obtain n where n: "?start = Suc n" by (auto simp: gr0_conv_Suc)
  with fg_start_round[OF rho, of p "Suc r"]
  have 0: "round (rho (Suc n)) p = Suc r" by simp
  have 1: "round (rho n) p = r"
  proof (rule fg_round_between_start_rounds[OF rho])
    have "fg_start_round rho p r < fg_start_round rho p (Suc r)"
      by (rule fg_start_round_strict_mono[OF rho, THEN strict_monoD]) simp
    with n show "fg_start_round rho p r ≤ n" by simp
  next
    from n show "n < ?start" by simp
  qed
  from rho obtain p' where
    "fg_next_config A p' (HOs (round (rho n) p') p')
                         (SHOs (round (rho n) p') p')
                         (coords (round (rho (Suc n)) p') p')
                         (rho n) (rho (Suc n))"
    (is "fg_next_config _ _ ?HO ?SHO ?crd ?cfg ?cfg'")
    by (force simp: fg_run_def)
  hence "fg_local A p (HOs r p) (coords (Suc r) p) (rho n) (rho (Suc n))"
  proof (auto simp: fg_next_config_def)
    fix q
    assume "fg_send_msg A p' q ?cfg ?cfg'"
      ― ‹impossible because round changes›
    with 0 1 show ?thesis by (auto simp: fg_send_msg_def)
  next
    fix q
    assume "fg_rcv_msg p' q ?HO ?SHO ?cfg ?cfg'"
      ― ‹impossible because round changes›
    with 0 1 show ?thesis by (auto simp: fg_rcv_msg_def)
  next
    assume "fg_local A p' ?HO ?crd ?cfg ?cfg'"
    with 0 1 show ?thesis by (cases "p' = p") (auto simp: fg_local_def)
  qed
  with 1 n that show ?thesis by auto
qed

text ‹
 We now prove two invariants asserted in cite‹"saad:reduction"›. The first
 one states that any message ‹m› in transit from process ‹p›
 to process ‹q› for round ‹r› corresponds to the message
 computed by ‹p› for ‹q›, given ‹p›'s state at its
 ‹r›th local transition.
 ›

lemma fg_invariant1:
  assumes rho: "fg_run A rho HOs SHOs coords"
      and m: "(p,r,q,m) ∈ network (rho n)" (is "?msg n")
  shows "m = sendMsg A r p q (state (rho (fg_start_round rho p r)) p)"
using m proof (induct n)
  ― ‹the base case is trivial because the network is empty›
  assume "?msg 0" with rho show "?thesis"
    by (auto simp: fg_run_def fg_init_config_def)
next
  fix n
  assume m': "?msg (Suc n)" and ih: "?msg n ==> ?thesis"
  from rho obtain p' where
    "fg_next_config A p' (HOs (round (rho n) p') p')
                         (SHOs (round (rho n) p') p')
                         (coords (round (rho (Suc n)) p') p')
                         (rho n) (rho (Suc n))"
    (is "fg_next_config _ _ ?HO ?SHO ?crd ?cfg ?cfg'")
    by (force simp: fg_run_def)
  thus "?thesis"
  proof (auto simp: fg_next_config_def)
    txt ‹
 Only ‹fg_send_msg› transitions for process ‹p› are interesting,
 since all other transitions cannot add a message for ‹p›, hence we can
 apply the induction hypothesis.
 ›
    fix q'
    assume send: "fg_send_msg A p' q' ?cfg ?cfg'"
    show ?thesis
    proof (cases "?msg n")
      case True
      with ih show ?thesis .
    next
      case False
      with send m' have 1: "p' = p" "round ?cfg p = r"
                    and 2: "m = sendMsg A r p q (state ?cfg p)"
        by (auto simp: fg_send_msg_def)
      from rho 1 have "state ?cfg p = state (rho (fg_start_round rho p r)) p"
        by (auto simp: fg_start_round fg_same_round_same_state)
      with 1 2 show ?thesis by simp
    qed
  next
    fix q'
    assume "fg_rcv_msg p' q' ?HO ?SHO ?cfg ?cfg'"
    with m' have "?msg n" by (auto simp: fg_rcv_msg_def)
    with ih show ?thesis .
  next
    assume "fg_local A p' ?HO ?crd ?cfg ?cfg'"
    with m' have "?msg n" by (auto simp: fg_local_def)
    with ih show ?thesis .
  qed
qed

text ‹
 The second invariant states that if process ‹q› received message
 ‹m› from process ‹p›, then (a) ‹p› is in ‹q›'s
 HO set for that round ‹m›, and (b) if ‹p› is moreover in
 ‹q›'s SHO set, then ‹m› is the message that ‹p› computed
 at the start of that round.
 ›

lemma fg_invariant2a:
  assumes rho: "fg_run A rho HOs SHOs coords"
      and m: "rcvd (rho n) q p = Some m" (is "?rcvd n")
  shows "p ∈ HOs (round (rho n) q) q"
  (is "p ∈ HOs (?rd n) q" is "?P n")
using m proof (induct n)
  ― ‹The base case is trivial because @{text q} has not received any message initially›
  assume "?rcvd 0" with rho show "?P 0"
    by (auto simp: fg_run_def fg_init_config_def)
next
  fix n
  assume rcvd: "?rcvd (Suc n)" and ih: "?rcvd n ==> ?P n"
  ― ‹For the inductive step we distinguish the possible transitions›
  from rho obtain p' where
    "fg_next_config A p' (HOs (round (rho n) p') p')
                         (SHOs (round (rho n) p') p')
                         (coords (round (rho (Suc n)) p') p')
                         (rho n) (rho (Suc n))"
    (is "fg_next_config _ _ ?HO ?SHO ?crd ?cfg ?cfg'")
    by (force simp: fg_run_def)
  thus "?P (Suc n)"
  proof (auto simp: fg_next_config_def)
    txt ‹
 Except for ‹fg_rcv_msg› steps of process ‹q›, the proof
 is immediately reduced to the induction hypothesis.
 ›
    fix q'
    assume rcvmsg: "fg_rcv_msg p' q' ?HO ?SHO ?cfg ?cfg'"
    hence rd: "?rd (Suc n) = ?rd n" by (auto simp: fg_rcv_msg_def)
    show "?P (Suc n)"
    proof (cases "?rcvd n")
      case True
      with ih rd show ?thesis by simp
    next
      case False
      with rcvd rcvmsg rd show ?thesis by (auto simp: fg_rcv_msg_def)
    qed
  next
    fix q'
    assume "fg_send_msg A p' q' ?cfg ?cfg'"
    with rcvd have "?rcvd n" and "?rd (Suc n) = ?rd n"
      by (auto simp: fg_send_msg_def)
    with ih show "?P (Suc n)" by simp
  next
    assume "fg_local A p' ?HO ?crd ?cfg ?cfg'"
    with rcvd have "?rcvd n" and "?rd (Suc n) = ?rd n"
      ― ‹in fact, @{text "p' = q"} is impossible because the @{text rcvd} field of @{text p'} is cleared›
      by (auto simp: fg_local_def)
    with ih show "?P (Suc n)" by simp
  qed
qed

lemma fg_invariant2b:
  assumes rho: "fg_run A rho HOs SHOs coords"
      and m: "rcvd (rho n) q p = Some m" (is "?rcvd n")
      and sho: "p ∈ SHOs (round (rho n) q) q" (is "p ∈ SHOs (?rd n) q")
  shows "m = sendMsg A (?rd n) p q
                     (state (rho (fg_start_round rho p (?rd n))) p)"
        (is "?P n")
using m sho proof (induct n)
  ― ‹The base case is trivial because @{text q} has not received any message initially›
  assume "?rcvd 0" with rho show "?P 0"
    by (auto simp: fg_run_def fg_init_config_def)
next
  fix n
  assume rcvd: "?rcvd (Suc n)" and p: "p ∈ SHOs (?rd (Suc n)) q"
     and ih: "?rcvd n ==> p ∈ SHOs (?rd n) q ==> ?P n"
  ― ‹For the inductive step we again distinguish the possible transitions›
  from rho obtain p' where
    "fg_next_config A p' (HOs (round (rho n) p') p')
                         (SHOs (round (rho n) p') p')
                         (coords (round (rho (Suc n)) p') p')
                         (rho n) (rho (Suc n))"
    (is "fg_next_config _ _ ?HO ?SHO ?crd ?cfg ?cfg'")
    by (force simp: fg_run_def)
  thus "?P (Suc n)"
  proof (auto simp: fg_next_config_def)
    txt ‹
 Except for ‹fg_rcv_msg› steps of process ‹q›, the proof
 is immediately reduced to the induction hypothesis.
 ›
    fix q'
    assume rcvmsg: "fg_rcv_msg p' q' ?HO ?SHO ?cfg ?cfg'"
    hence rd: "?rd (Suc n) = ?rd n" by (auto simp: fg_rcv_msg_def)
    show "?P (Suc n)"
    proof (cases "?rcvd n")
      case True
      with ih p rd show ?thesis by simp
    next
      case False
      from rcvmsg obtain m' m'' where
        "(q', round ?cfg p', p', m') ∈ network ?cfg"
        "rcvd ?cfg' = (rcvd ?cfg)(p' := (rcvd ?cfg p')(q' :=
                          if q' ∈ ?SHO then Some m' else Some m''))"
        by (auto simp: fg_rcv_msg_def split del: if_split_asm)
      with False rcvd p rd have "(p, ?rd n, q, m) ∈ network ?cfg" by auto
      with rho rd show ?thesis by (auto simp: fg_invariant1)
    qed
  next
    fix q'
    assume "fg_send_msg A p' q' ?cfg ?cfg'"
    with rcvd have "?rcvd n" and "?rd (Suc n) = ?rd n"
      by (auto simp: fg_send_msg_def)
    with p ih show "?P (Suc n)" by simp
  next
    assume "fg_local A p' ?HO ?crd ?cfg ?cfg'"
    with rcvd have "?rcvd n" and "?rd (Suc n) = ?rd n"
      ― ‹in fact, @{text "p' = q"} is impossible because the @{text rcvd} field of @{text p'} is cleared›
      by (auto simp: fg_local_def)
    with p ih show "?P (Suc n)" by simp
  qed
qed

subsection ‹From Fine-Grained to Coarse-Grained Runs›

text ‹
 The reduction theorem asserts that for any fine-grained run ‹rho›
 there is a coarse-grained run such that every process sees the same
 sequence of local states in the two runs, modulo stuttering. In other words,
 no process can locally distinguish the two runs.

 Given fine-grained run ‹rho›, the corresponding coarse-grained run ‹sigma› is
 defined as the sequence of state vectors at the beginning of every round.
 Notice in particular that the local states ‹sigma r p› and
 ‹sigma r q› of two different processes ‹p› and ‹q›
 appear at different instants in the original run ‹rho›. Nevertheless,
 we prove that ‹sigma› is a coarse-grained run of the algorithm for
 the same HO, SHO, and coordinator assignments. By definition (and the
 fact that local states remain equal between ‹fg_start_round›
 instants), the sequences of process states in ‹rho› and
 ‹sigma› are easily seen to be stuttering equivalent, and this
 will be formally stated below.
 ›

definition coarse_run where
  "coarse_run rho r p ≡ state (rho (fg_start_round rho p r)) p"

theorem reduction:
  assumes rho: "fg_run A rho HOs SHOs coords"
  shows "CSHORun A (coarse_run rho) HOs SHOs coords"
        (is "CSHORun _ ?cr _ _ _")
proof (auto simp: CSHORun_def)
  from rho show "CHOinitConfig A (?cr 0) (coords 0)"
    by (auto simp: fg_run_def fg_init_config_def CHOinitConfig_def 
                   coarse_run_def fg_start_round_0[OF rho])
next
  fix r
  show "CSHOnextConfig A r (?cr r) (HOs r) (SHOs r) (coords (Suc r))
                       (?cr (Suc r))"
  proof (auto simp add: CSHOnextConfig_def)
    fix p
    from rho[THEN fg_local_transition_from_round] obtain n
      where n: "round (rho n) p = r"
        and start: "fg_start_round rho p (Suc r) = Suc n" (is "?start = _")
        and loc: "fg_local A p (HOs r p) (coords (Suc r) p) (rho n) (rho (Suc n))"
                 (is "fg_local _ _ ?HO ?crd ?cfg ?cfg'")
      by blast
    have cfg: "?cr r p = state ?cfg p"
      unfolding coarse_run_def proof (rule fg_same_round_same_state[OF rho])
      from n show "round (rho (fg_start_round rho p r)) p = round ?cfg p"
        by (simp add: fg_start_round[OF rho])
    qed
    from start have cfg': "?cr (Suc r) p = state ?cfg' p"
      by (simp add: coarse_run_def)
    have rcvd: "rcvd ?cfg p ∈ SHOmsgVectors A r p (?cr r) ?HO (SHOs r p)"
    proof (auto simp: SHOmsgVectors_def)
      fix q
      assume "q ∈ ?HO"
      with n loc show "∃m. rcvd ?cfg p q = Some m" by (auto simp: fg_local_def)
    next
      fix q m
      assume "rcvd ?cfg p q = Some m"
      with rho n show "q ∈ ?HO" by (auto simp: fg_invariant2a)
    next
      fix q
      assume sho: "q ∈ SHOs r p" and ho: "q ∈ ?HO"
      from ho n loc obtain m where "rcvd ?cfg p q = Some m"
        by (auto simp: fg_local_def)
      with rho n sho show "rcvd ?cfg p q = Some (sendMsg A r q p (?cr r q))"
        by (auto simp: fg_invariant2b coarse_run_def)
    qed
    with n loc cfg cfg'
    show "∃μ ∈ SHOmsgVectors A r p (?cr r) ?HO (SHOs r p).
             CnextState A r p (?cr r p) μ ?crd (?cr (Suc r) p)"
      by (auto simp: fg_local_def)
  qed
qed


subsection ‹Locally Similar Runs and Local Properties›

text ‹
 We say that two sequences of configurations (vectors of process states)
 are \emph{locally similar} if for every process the sequences of its
 process states are stuttering equivalent. Observe that different stuttering
 reduction may be applied for every process, hence the original sequences of
 configurations need not be stuttering equivalent and can indeed differ
 wildly in the combinations of local states that occur.

 A property of a sequence of configurations is called \emph{local} if it
 is insensitive to local similarity.
 ›

definition locally_similar where
  "locally_similar (σ::nat ==> 'proc ==> 'pst) τ ≡
   ∀p::'proc. (λn. σ n p) ≈ (λn. τ n p)"

definition local_property where
  "local_property P ≡
   ∀σ τ. locally_similar σ τ ⟶ P σ ⟶ P τ"

text ‹
 Local similarity is an equivalence relation.
 ›

lemma locally_similar_refl: "locally_similar σ σ"
  by (simp add: locally_similar_def stutter_equiv_refl)

lemma locally_similar_sym: "locally_similar σ τ ==> locally_similar τ σ"
  by (simp add: locally_similar_def stutter_equiv_sym)

lemma locally_similar_trans [trans]:
  "locally_similar ρ σ ==> locally_similar σ τ ==> locally_similar ρ τ"
  by (force simp add: locally_similar_def elim: stutter_equiv_trans)

lemma local_property_eq:
  "local_property P = (∀σ τ. locally_similar σ τ ⟶ P σ = P τ)"
  by (auto simp: local_property_def dest: locally_similar_sym)

text ‹
 Consider any fine-grained run ‹rho›. The projection of ‹rho›
 to vectors of process states is locally similar to the coarse-grained run
 computed from ‹rho›.
 ›

lemma coarse_run_locally_similar:
  assumes rho: "fg_run A rho HOs SHOs coords"
  shows "locally_similar (state ∘ rho) (coarse_run rho)"
proof (auto simp: locally_similar_def)
  fix p
  show "(λn. state (rho n) p) ≈ (λn. coarse_run rho n p)" (is "?fgr ≈ ?cgr")
  proof (rule stutter_equivI)
    show "stutter_sampler (fg_start_round rho p) ?fgr"
    proof (auto simp: stutter_sampler_def)
      from rho show "fg_start_round rho p 0 = 0"
        by (rule fg_start_round_0)
    next
      show "strict_mono (fg_start_round rho p)"
        by (rule fg_start_round_strict_mono[OF rho])
    next
      fix r n
      assume "fg_start_round rho p r < n" and "n < fg_start_round rho p (Suc r)"
      with rho have "round (rho n) p = round (rho (fg_start_round rho p r)) p"
        by (simp add: fg_start_round fg_round_between_start_rounds)
      with rho show "state (rho n) p = state (rho (fg_start_round rho p r)) p"
        by (rule fg_same_round_same_state)
    qed
  next
    show "stutter_sampler id ?cgr"
      by (rule id_stutter_sampler)
  next
    show "?fgr ∘ fg_start_round rho p = ?cgr ∘ id"
      by (auto simp: coarse_run_def)
  qed
qed

text ‹
 Therefore, in order to verify a local property ‹P› for a
 fine-grained run over given ‹HO›, ‹SHO›, and ‹coord›
 collections, it is enough to show that ‹P› holds for all
 coarse-grained runs for these same collections.
 Indeed, one may restrict attention to coarse-grained runs whose
 initial states agree with that of the given fine-grained run.
 ›

theorem local_property_reduction:
  assumes rho: "fg_run A rho HOs SHOs coords"
      and P: "local_property P"
      and coarse_correct: 
            "∧ crho. [ CSHORun A crho HOs SHOs coords; crho 0 = state (rho 0)]
                      ==> P crho"
  shows "P (state ∘ rho)"
proof -
  have "coarse_run rho 0 = state (rho 0)"
    by (rule ext, simp add: coarse_run_def fg_start_round_0[OF rho])
  from rho[THEN reduction] this 
  have "P (coarse_run rho)" by (rule coarse_correct)
  with coarse_run_locally_similar[OF rho] P 
  show ?thesis by (auto simp: local_property_eq)
qed


subsection ‹Consensus as a Local Property›

text ‹
 Consensus and Weak Consensus are local properties and can therefore
 be verified just over coarse-grained runs, according to theorem
 ‹local_property_reduction›.
 ›

lemma integrity_is_local:
  assumes sim: "locally_similar σ τ"
      and val: "∧n. dec (σ n p) = Some v ==> v ∈ range vals"
      and dec: "dec (τ n p) = Some v"
  shows "v ∈ range vals"
proof -
  from sim have "(λr. σ r p) ≈ (λr. τ r p)" by (simp add: locally_similar_def)
  then obtain m where "σ m p = τ n p" by (rule stutter_equiv_element_left)
  from sym[OF this] dec show ?thesis by (auto elim: val)
qed

lemma validity_is_local:
  assumes sim: "locally_similar σ τ"
      and val: "∧n. dec (σ n p) = Some w ==> w = v"
      and dec: "dec (τ n p) = Some w"
  shows "w = v"
proof -
  from sim have "(λr. σ r p) ≈ (λr. τ r p)" by (simp add: locally_similar_def)
  then obtain m where "σ m p = τ n p" by (rule stutter_equiv_element_left)
  from sym[OF this] dec show ?thesis by (auto elim: val)
qed

lemma agreement_is_local:
  assumes sim: "locally_similar σ τ"
  and agr: "∧m n. [dec (σ m p) = Some v; dec (σ n q) = Some w] ==> v=w"
  and v: "dec (τ m p) = Some v" and w: "dec (τ n q) = Some w"
  shows "v = w"
proof -
  from sim have "(λr. σ r p) ≈ (λr. τ r p)" by (simp add: locally_similar_def)
  then obtain m' where m': "σ m' p = τ m p" by (rule stutter_equiv_element_left)
  from sim have "(λr. σ r q) ≈ (λr. τ r q)" by (simp add: locally_similar_def)
  then obtain n' where n': "σ n' q = τ n q" by (rule stutter_equiv_element_left)
  from sym[OF m'] sym[OF n'] v w show "v = w" by (auto elim: agr)
qed

lemma termination_is_local:
  assumes sim: "locally_similar σ τ"
      and trm: "dec (σ m p) = Some v"
  shows "∃n. dec (τ n p) = Some v"
proof -
  from sim have "(λr. σ r p) ≈ (λr. τ r p)" by (simp add: locally_similar_def)
  then obtain n where "σ m p = τ n p" by (rule stutter_equiv_element_right)
  with trm show ?thesis by auto
qed

theorem consensus_is_local: "local_property (consensus vals dec)"
proof (auto simp: local_property_def consensus_def)
  fix σ τ n p v
  assume "locally_similar σ τ"
  and "∀n p v. dec (σ n p) = Some v ⟶ v ∈ range vals"
  and "dec (τ n p) = Some v"
  thus "v ∈ range vals" by (blast intro: integrity_is_local)
next
  fix σ τ m n p q v w
  assume "locally_similar σ τ"
  and "∀m n p q v w. dec (σ m p) = Some v ∧ dec (σ n q) = Some w ⟶ v = w"
  and "dec (τ m p) = Some v" and "dec (τ n q) = Some w"
  thus "v = w" by (blast intro: agreement_is_local)
next
  fix σ τ p
  assume "locally_similar σ τ"
  and "∀p. ∃m v. dec (σ m p) = Some v"
  thus "∃n w. dec (τ n p) = Some w" by (blast dest: termination_is_local)
qed

theorem weak_consensus_is_local: "local_property (weak_consensus vals dec)"
proof (auto simp: local_property_def weak_consensus_def)
  fix σ τ n p v w
  assume "locally_similar σ τ"
  and "∀n p w. dec (σ n p) = Some w ⟶ w = v"
  and "dec (τ n p) = Some w"
  thus "w = v" by (blast intro: validity_is_local)
next
  fix σ τ m n p q v w
  assume "locally_similar σ τ"
  and "∀m n p q v w. dec (σ m p) = Some v ∧ dec (σ n q) = Some w ⟶ v = w"
  and "dec (τ m p) = Some v" and w: "dec (τ n q) = Some w"
  thus "v = w" by (blast intro: agreement_is_local)
next
  fix σ τ p
  assume "locally_similar σ τ"
  and "∀p. ∃m v. dec (σ m p) = Some v"
  thus "∃n w. dec (τ n p) = Some w" by (blast dest: termination_is_local)
qed


end