Theory Paxos_Defs

section ‹The Paxos Algorithm›

theory Paxos_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Consensus_Misc" 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 
  constant instead.›

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›
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"

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