Theory New_Algorithm_Defs

section ‹The New Algorithm›

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

subsection ‹Model of the algorithm›
text ‹We assume that the values are linearly ordered, to be able to have each process
  select the smallest value.›
axiomatization where val_linorder: 
  "OFCLASS(val, linorder_class)"

instance val :: linorder by (rule val_linorder)

record pstate =
  x :: val                ― ‹current value held by process›
  prop_vote :: "val option"
  mru_vote :: "(nat × val) option"
  decide :: "val option"  ― ‹value the process has decided on, if any›

datatype msg =
  MruVote "(nat × val) option" "val"
| PreVote "val"
| Vote val
| Null  ― ‹dummy message in case nothing needs to be sent›

text ‹
  Characteristic predicates on messages.
›

definition isLV where "isLV m  rv. m = Vote rv"

definition isPreVote where "isPreVote m  px. m = PreVote px"

definition NA_initState where
  "NA_initState p st _ 
   mru_vote st = None
    prop_vote st = None
    decide st = None
  "

definition send0 where
  "send0 r p q st  MruVote (mru_vote st) (x st)"

fun msg_to_val_stamp :: "msg  (round × val)option" where
  "msg_to_val_stamp (MruVote rv _) = rv"

definition msgs_to_lvs ::
  "(process  msg)
   (process, round × val) map"
where
  "msgs_to_lvs msgs  msg_to_val_stamp m msgs"

definition smallest_proposal where
  "smallest_proposal (msgs::process  msg) 
   Min {v. q mv. msgs q = Some (MruVote mv v)}"

definition next0
  :: "nat 
   process 
   pstate 
   (process  msg)
   process
   pstate
   bool"
where
  "next0 r p st msgs crd st'  let 
      Q = dom msgs; 
      lvs = msgs_to_lvs msgs;
      smallest = if Q = {} then x st else smallest_proposal msgs
    in
    st' = st 
      prop_vote := if card Q > N div 2
        then Some (case_option smallest snd (option_Max_by fst (ran (lvs |` Q))))
        else None
    "

definition send1 where
  "send1 r p q st  case prop_vote st of
    None  Null
    | Some v  PreVote v"

definition Q_prevotes_v where
  "Q_prevotes_v msgs Q v  let D = dom msgs in
    Q  D  card Q > N div 2  (q  Q. msgs q = Some (PreVote v))"

definition next1 
  :: "nat 
   process 
   pstate 
   (process  msg)
   process
   pstate
   bool"
where
  "next1 r p st msgs crd st'  
      decide st' = decide st
       x st' = x st 
       (Q v. Q_prevotes_v msgs Q v
         mru_vote st' = Some (three_phase r, v))
       (¬ (Q v. Q_prevotes_v msgs Q v)
         mru_vote st' = mru_vote st)
  "

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

definition Q'_votes_v where
  "Q'_votes_v r msgs Q Q' v  
    Q'  Q  card Q' > N div 2  (q  Q'. msgs q = Some (Vote v))"

definition next2 
  :: "nat 
   process 
   pstate 
   (process  msg)
   process
   pstate
   bool"
where
  "next2 r p st msgs crd st'  let Q = dom msgs; lvs = msgs_to_lvs msgs in
    x st' = x st
     mru_vote st' = mru_vote st
     (Q' v. Q'_votes_v r msgs Q Q' v  decide st' = Some v)
     (¬(Q' v. Q'_votes_v r msgs Q Q' v  decide st' = decide st))
  "
    
definition NA_sendMsg :: "nat  process  process  pstate  msg" where
  "NA_sendMsg (r::nat) 
   if three_step r = 0 then send0 r
   else if three_step r = 1 then send1 r
   else send2 r"

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

subsection ‹The Heard-Of machine›
definition
  NA_commPerRd where
  "NA_commPerRd (HOrs::process HO)   True"

definition
  NA_commGlobal where
  "NA_commGlobal HOs  
      ph::nat. i  {0..2}. 
        (p. card (HOs (nr_steps*ph+i) p) > N div 2)
         (p q. HOs (nr_steps*ph+i) p = HOs (nr_steps*ph) q)
    "

definition New_Algo_Alg where
  "New_Algo_Alg 
     CinitState = NA_initState,
      sendMsg = NA_sendMsg,
      CnextState = NA_nextState "

definition New_Algo_HOMachine where
  "New_Algo_HOMachine 
     CinitState = NA_initState,
      sendMsg = NA_sendMsg,
      CnextState = NA_nextState,
      HOcommPerRd = NA_commPerRd,
      HOcommGlobal = NA_commGlobal "

abbreviation 
  "New_Algo_M  (New_Algo_HOMachine::(process, pstate, msg) HOMachine)"

end