# Theory Paxos_Defs

section ‹The Paxos Algorithm›

theory Paxos_Defs
imports Heard_Of.HOModel   Three_Steps
begin

text ‹
This is a modified version (closer to the original Paxos) of PaxosDefs from the Heard Of
entry in the AFP.›

subsection ‹Model of the algorithm›

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 option"   ― ‹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› field of the initial state is unconstrained, all other
fields are initialized appropriately.
›

definition Paxos_initState where
"Paxos_initState p st crd
mru_vote st = None
commt 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  card Q > N div 2
then (st' = st  commt := Some (case_option (x st) snd (option_Max_by fst (ran (lvs | Q))))  )
else st' = st commt := None "

definition send1 where
"send1 r p q st
if p = coord r  commt st  None then Vote (the (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  isVote (the (msgs (coord r)))
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 Paxos_sendMsg :: "nat  process  process  'val pstate  'val msg" where
"Paxos_sendMsg (r::nat)
if three_step r = 0 then send0 r
else if three_step r = 1 then send1 r
else send2 r"

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

definition
Paxos_commPerRd where
"Paxos_commPerRd r (HO::process HO) (crd::process coord)  True"

definition
Paxos_commGlobal where
"Paxos_commGlobal HOs coords
ph::nat. c::process.
coord (nr_steps*ph) = c
card (HOs (nr_steps*ph) c) > N div 2
(p. c  HOs (nr_steps*ph+1) p)
(p. card (HOs (nr_steps*ph+2) p) > N div 2)"

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

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

definition Paxos_Alg where
"Paxos_Alg
CinitState = Paxos_initState,
sendMsg = Paxos_sendMsg,
CnextState = Paxos_nextState "

definition Paxos_CHOMachine where
"Paxos_CHOMachine
CinitState = Paxos_initState,
sendMsg = Paxos_sendMsg,
CnextState = Paxos_nextState,
CHOcommPerRd = Paxos_commPerRd,
CHOcommGlobal = Paxos_commGlobal "

abbreviation
"Paxos_M  (Paxos_CHOMachine::(process, 'val pstate, 'val msg) CHOMachine)"

end