Theory Paxos_Defs

section ‹The Paxos Algorithm›

theory Paxos_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Consensus_Misc" Three_Steps

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 
  constant instead.›

consts coord :: "nat  process"
specification (coord)
  coord_phase[rule_format]: "r r'. three_phase r = three_phase r'  coord r = coord r'"

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"
  "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 
   'val pstate 
   (process  'val msg)
   'val pstate
  "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 
   'val pstate 
   (process  'val msg)
   'val pstate
  "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›
definition votes_rcvd where
  "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"

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

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

  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
     CinitState = Paxos_initState,
      sendMsg = Paxos_sendMsg,
      CnextState = Paxos_nextState "

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

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