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