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

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

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