# Theory CT_Defs

section ‹Chandra-Toueg $\diamond S$ Algorithm›

theory CT_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Consensus_Misc" Three_Steps
begin

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

record 'val pstate =
x :: 'val                ― ‹current value held by process›
mru_vote :: "(nat × 'val) option"
commt :: "'val"   ― ‹for coordinators: the value processes are asked to commit to›
decide :: "'val option"  ― ‹value the process has decided on, if any›

text ‹The algorithm relies on a coordinator for each phase of the algorithm.
A phase lasts three rounds. The HO model formalization already provides the
infrastructure for this, but unfortunately the coordinator is not passed to
the @{term sendMsg} function. Using the infrastructure would thus require
additional invariants and proofs; for simplicity, we use a global

consts coord :: "nat ⇒ process"
specification (coord)
coord_phase[rule_format]: "∀r r'. three_phase r = three_phase r' ⟶ coord r = coord r'"
by(auto)

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

datatype 'val msg =
ValStamp "'val" "nat"
| NeverVoted
| Vote "'val"
| Null  ― ‹dummy message in case nothing needs to be sent›

text ‹
Characteristic predicates on messages.
›

definition isValStamp where "isValStamp m ≡ ∃v ts. m = ValStamp v ts"

definition isVote where "isVote m ≡ ∃v. m = Vote v"

text ‹
Selector functions to retrieve components of messages. These functions
have a meaningful result only when the message is of an appropriate kind.
›

fun val where
"val (ValStamp v ts) = v"
| "val (Vote v) = v"

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

definition CT_initState where
"CT_initState p st crd ≡
mru_vote st = None
∧ decide st = None
"

definition mru_vote_to_msg :: "'val pstate ⇒ 'val msg" where
"mru_vote_to_msg st ≡ case mru_vote st of
Some (ts, v) ⇒ ValStamp v ts
| None ⇒ NeverVoted"

fun msg_to_val_stamp :: "'val msg ⇒ (round × 'val)option" where
"msg_to_val_stamp (ValStamp v ts) = Some (ts, v)"
| "msg_to_val_stamp _ = None"

definition msgs_to_lvs ::
"(process ⇀ 'val msg)
⇒ (process, round × 'val) map"
where
"msgs_to_lvs msgs ≡ msg_to_val_stamp ∘⇩m msgs"

definition send0 where
"send0 r p q st ≡
if q = coord r then mru_vote_to_msg st else Null"

definition next0
:: "nat
⇒ process
⇒ 'val pstate
⇒ (process ⇀ 'val msg)
⇒ process
⇒ 'val pstate
⇒ bool"
where
"next0 r p st msgs crd st' ≡ let Q = dom msgs; lvs = msgs_to_lvs msgs in
if p = coord r
then (st' = st ⦇ commt := (case_option (x st) snd (option_Max_by fst (ran (lvs | Q)))) ⦈ )
else st' = st"

definition send1 where
"send1 r p q st ≡
if p = coord r then Vote (commt st) else Null"

definition next1
:: "nat
⇒ process
⇒ 'val pstate
⇒ (process ⇀ 'val msg)
⇒ process
⇒ 'val pstate
⇒ bool"
where
"next1 r p st msgs crd st' ≡
if msgs (coord r) ≠ None
then st' = st ⦇ mru_vote := Some (three_phase r, val (the (msgs (coord r))))  ⦈
else st' = st"

definition send2 where
"send2 r p q st ≡ (case mru_vote st of
Some (phs, v) ⇒ (if phs = three_phase r then Vote v else Null)
| _ ⇒ Null
)"

― ‹processes from which a vote was received›
"votes_rcvd (msgs :: process ⇀ 'val msg) ≡
{ (q, v) . msgs q = Some (Vote v) }"

definition the_rcvd_vote where
"the_rcvd_vote (msgs :: process ⇀ 'val msg) ≡ SOME v. v ∈ snd  votes_rcvd msgs"

definition next2 where
"next2 r p st msgs crd st' ≡
if card (votes_rcvd msgs) > N div 2
then st' = st ⦇ decide := Some (the_rcvd_vote msgs) ⦈
else st' = st
"

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

definition CT_sendMsg :: "nat ⇒ process ⇒ process ⇒ 'val pstate ⇒ 'val msg" where
"CT_sendMsg (r::nat) ≡
if three_step r = 0 then send0 r
else if three_step r = 1 then send1 r
else send2 r"

definition
CT_nextState :: "nat ⇒ process ⇒ 'val pstate ⇒ (process ⇀ 'val msg)
⇒ process ⇒ 'val pstate ⇒ bool"
where
"CT_nextState r ≡
if three_step r = 0 then next0 r
else if three_step r = 1 then next1 r
else next2 r"

subsection ‹The \emph{CT} Heard-Of machine›

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

definition CT_Alg where
"CT_Alg ≡
⦇ CinitState = CT_initState,
sendMsg = CT_sendMsg,
CnextState = CT_nextState ⦈"

text ‹The CT algorithm relies on \emph{waiting}: in each round, the
coordinator waits until it hears from $\frac{N}{2}$ processes. This
it reflected in the following per-round predicate.›

definition
CT_commPerRd :: "nat ⇒ process HO ⇒ process coord ⇒ bool"
where
"CT_commPerRd r HOs crds ≡
three_step r = 0 ⟶ card (HOs (coord r)) > N div 2"

definition
CT_commGlobal where
"CT_commGlobal HOs coords ≡
∃ph::nat. ∃c::process.
coord (nr_steps*ph) = c
∧ (∀p. c ∈ HOs (nr_steps*ph+1) p)
∧ (∀p. card (HOs (nr_steps*ph+2) p) > N div 2)"

definition CT_CHOMachine where
"CT_CHOMachine ≡
⦇ CinitState = CT_initState,
sendMsg = CT_sendMsg,
CnextState = CT_nextState,
CHOcommPerRd = CT_commPerRd,
CHOcommGlobal = CT_commGlobal ⦈"

abbreviation
"CT_M ≡ (CT_CHOMachine::(process, 'val pstate, 'val msg) CHOMachine)"

end