# Theory OneThirdRule_Defs

section ‹The OneThirdRule Algorithm›

theory OneThirdRule_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 state of each process consists of two fields: ‹last_vote› holds
the current value proposed by the process and ‹decision› the
value (if any, hence the option type) it has decided.
›

record 'val pstate =
last_vote :: "'val"
decision :: "'val option"

text ‹
The initial value of field ‹last_vote› is unconstrained, but no decision
has been taken initially.
›

definition OTR_initState where
"OTR_initState p st ≡ decision st = None"

text ‹
Given a vector ‹msgs› of values (possibly null) received from
each process, @{term "HOV msgs v"} denotes the set of processes from
›

definition HOV :: "(process ⇒ 'val option) ⇒ 'val ⇒ process set" where
"HOV msgs v ≡ { q . msgs q = Some v }"

text ‹
@{term "MFR msgs v"} (most frequently received'') holds for
vector ‹msgs› if no value has been received more frequently
than ‹v›.

Some such value always exists, since there is only a finite set of
processes and thus a finite set of possible cardinalities of the
sets @{term "HOV msgs v"}.
›

definition MFR :: "(process ⇒ 'val option) ⇒ 'val ⇒ bool" where
"MFR msgs v ≡ ∀w. card (HOV msgs w) ≤ card (HOV msgs v)"

lemma MFR_exists: "∃v. MFR msgs v"
proof -
let ?cards = "{ card (HOV msgs v) | v . True }"
let ?mfr = "Max ?cards"
have "∀v. card (HOV msgs v) ≤ N" by (auto intro: card_mono)
hence "?cards ⊆ { 0 .. N }" by auto
hence fin: "finite ?cards" by (metis atLeast0AtMost finite_atMost finite_subset)
hence "?mfr ∈ ?cards" by (rule Max_in) auto
then obtain v where v: "?mfr = card (HOV msgs v)" by auto
have "MFR msgs v"
proof (auto simp: MFR_def)
fix w
from fin have "card (HOV msgs w) ≤ ?mfr" by (rule Max_ge) auto
thus "card (HOV msgs w) ≤ card (HOV msgs v)" by (unfold v)
qed
thus ?thesis ..
qed

text ‹
Also, if a process has heard from at least one other process,
›

lemma MFR_in_msgs:
assumes HO:"HOs m p ≠ {}"
and v: "MFR (HOrcvdMsgs OTR_M m p (HOs m p) (rho m)) v"
(is "MFR ?msgs v")
shows "∃q ∈ HOs m p. v = the (?msgs q)"
proof -
from HO obtain q where q: "q ∈ HOs m p"
by auto
with v have "HOV ?msgs (the (?msgs q)) ≠ {}"
by (auto simp: HOV_def HOrcvdMsgs_def)
hence HOp: "0 < card (HOV ?msgs (the (?msgs q)))"
by auto
also from v have "… ≤ card (HOV ?msgs v)"
finally have "HOV ?msgs v ≠ {}"
by auto
thus ?thesis
by (auto simp: HOV_def HOrcvdMsgs_def)
qed

text ‹
@{term "TwoThirds msgs v"} holds if value ‹v› has been
received from more than $2/3$ of all processes.
›

definition TwoThirds where
"TwoThirds msgs v ≡ (2*N) div 3 < card (HOV msgs v)"

text ‹
The next-state relation of algorithm \emph{One-Third Rule} for every process
is defined as follows:
if the process has received values from more than $2/3$ of all processes,
the ‹last_vote› field is set to the smallest among the most frequently received
values, and the process decides value $v$ if it received $v$ from more than
$2/3$ of all processes. If ‹p› hasn't heard from more than $2/3$ of
all processes, the state remains unchanged.
(Note that ‹Some› is the constructor of the option datatype, whereas
‹ϵ› is Hilbert's choice operator.)
We require the type of values to be linearly ordered so that the minimum
is guaranteed to be well-defined.
›

definition OTR_nextState where
"OTR_nextState r p (st::('val::linorder) pstate) msgs st' ≡
if (2*N) div 3 < card {q. msgs q ≠ None}
then st' = ⦇ last_vote = Min {v . MFR msgs v},
decision = (if (∃v. TwoThirds msgs v)
then Some (ϵv. TwoThirds msgs v)
else decision st) ⦈
else st' = st"

text ‹
The message sending function is very simple: at every round, every process
sends its current proposal (field ‹last_vote› of its local state) to all
processes.
›

definition OTR_sendMsg where
"OTR_sendMsg r p q st ≡ last_vote st"

subsection ‹Communication predicate for \emph{One-Third Rule}›

text ‹
We now define the communication predicate for the \emph{One-Third Rule}
algorithm to be correct.
It requires that, infinitely often, there is a round where all processes
receive messages from the same set ‹Π› of processes where ‹Π›
contains more than two thirds of all processes.
The per-round'' part of the communication predicate is trivial.
›

definition OTR_commPerRd where
"OTR_commPerRd HOrs ≡ True"

definition OTR_commGlobal where
"OTR_commGlobal HOs ≡
∀r. ∃r0 Π. r0 ≥ r ∧ (∀p. HOs r0 p = Π) ∧ card Π > (2*N) div 3"

subsection ‹The \emph{One-Third Rule} Heard-Of machine›

text ‹
We now define the HO machine for the \emph{One-Third Rule} algorithm
by assembling the algorithm definition and its communication-predicate.
Because this is an uncoordinated algorithm, the ‹crd› arguments
of the initial- and next-state predicates are unused.
›

definition OTR_HOMachine where
"OTR_HOMachine =
⦇ CinitState =  (λ p st crd. OTR_initState p st),
sendMsg =  OTR_sendMsg,
CnextState = (λ r p st msgs crd st'. OTR_nextState r p st msgs st'),
HOcommPerRd = OTR_commPerRd,
HOcommGlobal = OTR_commGlobal ⦈"

abbreviation "OTR_M ≡ OTR_HOMachine::(process, 'val::linorder pstate, 'val) HOMachine"

end