# Theory MRU_Vote_Opt

```section ‹Optimized MRU Vote Model›

theory MRU_Vote_Opt
imports MRU_Vote
begin

subsection ‹Model definition›
(******************************************************************************)

record opt_mru_state =
next_round :: round
mru_vote :: "(process, round × val) map"
decisions :: "(process, val)map"

definition opt_mru_init where
"opt_mru_init = { ⦇ next_round = 0, mru_vote = Map.empty, decisions = Map.empty ⦈ }"

context quorum_process begin

definition opt_mru_vote :: "(process, round × val)map ⇒ (process set, round × val)map" where
"opt_mru_vote lvs Q = option_Max_by fst (ran (lvs |` Q))"

definition opt_mru_guard :: "(process, round × val)map ⇒ process set ⇒ val ⇒ bool" where
"opt_mru_guard mru_votes Q v ≡ Q ∈ Quorum ∧
(let mru = opt_mru_vote mru_votes Q in mru = None ∨ (∃r. mru = Some (r, v)))"

definition opt_mru_round
:: "round ⇒ process set ⇒ process set ⇒ val ⇒ (process, val)map ⇒ (opt_mru_state × opt_mru_state) set"
where
"opt_mru_round r Q S v r_decisions = {(s, s').
― ‹guards›
r = next_round s
∧ (S ≠ {} ⟶ opt_mru_guard (mru_vote s) Q v)
∧ d_guard r_decisions (const_map v S)
∧ ― ‹actions›
s' = s⦇
mru_vote := mru_vote s ++ const_map (r, v) S
, next_round := Suc r
, decisions := decisions s ++ r_decisions
⦈
}"

lemmas lv_evt_defs = opt_mru_round_def opt_mru_guard_def

definition mru_opt_trans :: "(opt_mru_state × opt_mru_state) set" where
"mru_opt_trans = (⋃r Q S v D. opt_mru_round r Q S v D) ∪ Id"

definition mru_opt_TS :: "opt_mru_state TS" where
"mru_opt_TS = ⦇ init = opt_mru_init, trans = mru_opt_trans ⦈"

lemmas mru_opt_TS_defs = mru_opt_TS_def opt_mru_init_def mru_opt_trans_def

subsection ‹Refinement›
(******************************************************************************)

definition lv_ref_rel :: "(v_state × opt_mru_state)set" where
"lv_ref_rel = {(sa, sc).
sc = ⦇
next_round = v_state.next_round sa
, mru_vote = process_mru (votes sa)
, decisions = v_state.decisions sa
⦈
}"

subsubsection ‹The concrete guard implies the abstract guard›
(******************************************************************************)

definition voters :: "(round ⇒ (process, val)map) ⇒ process set" where
"voters vs = {a|a r v. ((r, a), v) ∈ map_graph (case_prod vs)}"

lemma vote_set_as_Union:
"vote_set vs Q = (⋃a∈(Q ∩ voters vs). vote_set vs {a})"

lemma empty_ran:
"(ran f = {}) = (∀x. f x = None)"
by (metis option.collapse)

lemma empty_ran_restrict:
"(ran (f |` A) = {}) = (∀x ∈ A. f x = None)"

lemma option_Max_by_eqI:
"⟦ (S = {}) ⟷ (S' = {}); S ≠ {} ∧ S' ≠ {} ⟹ Max_by f S = Max_by g S' ⟧
⟹  option_Max_by f S = option_Max_by g S'"

lemma ran_process_mru_only_voters:
"ran (process_mru vs |` Q) = ran (process_mru vs |` (Q ∩ voters vs))"
by(auto simp add: ran_def restrict_map_def voters_def process_mru_def
mru_of_set_def option_Max_by_def vote_set_def)

lemma SV_inv3_inj_on_fst_vote_set:
"s ∈ SV_inv3 ⟹ inj_on fst (vote_set (votes s) Q)"
by(clarsimp simp add: SV_inv3_def inj_on_def vote_set_def)

lemma opt_mru_vote_mru_of_set:
assumes
inv1: "s ∈ Vinv1"
and inv3: "s ∈ SV_inv3"
shows
"opt_mru_vote (process_mru vs) Q = mru_of_set vs Q"
proof(simp add: opt_mru_vote_def mru_of_set_def, intro option_Max_by_eqI, clarsimp_all)
show "(ran (process_mru vs |` Q) = {}) = (vote_set vs Q = {})"
apply(clarsimp simp add: empty_ran_restrict process_mru_def mru_of_set_def option_Max_by_def
vote_set_def)
by (metis option.collapse option.distinct(1))
next
assume nempty: "ran (process_mru vs |` Q) ≠ {}" "vote_set vs Q ≠ {}"

hence nempty': "Q ∩ voters vs ≠ {}"

have nempty'': "{} ∉ (λa. vote_set vs {a}) ` (Q ∩ voters vs)"

note fin=Vinv1_finite_vote_set[OF inv1]

have ran_eq:
"ran (process_mru vs |` Q) = Max_by fst ` (λa. ⋃a∈{a} ∩ voters vs. vote_set vs {a}) ` (Q ∩ voters vs)"
apply(subst ran_process_mru_only_voters)
apply(auto simp add: image_def process_mru_def ran_def restrict_map_def mru_of_set_def option_Max_by_def)
by (metis (erased, lifting) Set.set_insert image_eqI insertI1 insert_inter_insert nempty'')

note inj=inv3[THEN SV_inv3_inj_on_fst_vote_set]

show "Max_by fst (ran (process_mru vs |` Q)) = Max_by fst (vote_set vs Q)"
apply(subst vs_def
Max_by_UNION_distrib[OF fin vote_set_as_Union nempty'[simplified vs_def]
nempty''[simplified vs_def] inj])+
apply(subst vote_set_as_Union)
by(metis ran_eq vs_def)
qed

lemma opt_mru_guard_imp_mru_guard:
assumes invs:
"s ∈ Vinv1" "s ∈ SV_inv3"
and c_guard: "opt_mru_guard (process_mru (votes s)) Q v"
shows "mru_guard s Q v" using c_guard
by(simp add: opt_mru_vote_mru_of_set[OF invs] opt_mru_guard_def mru_guard_def Let_def)

subsubsection ‹The concrete action refines the abstract action›
(******************************************************************************)

lemma act_ref:
assumes
"s ∈ Vinv1"
shows
"process_mru (votes s) ++ const_map (v_state.next_round s, v) S
= process_mru ((votes s)(v_state.next_round s := const_map v S))"
restrict_map_def
split:option.split)

subsubsection ‹The complete refinement›
(******************************************************************************)

lemma opt_mru_guard_imp_Quorum:
"opt_mru_guard vs Q v ⟹ Q ∈ Quorum"

lemma opt_mru_round_refines:
"{lv_ref_rel ∩ (Vinv1 ∩ SV_inv3 ∩ SV_inv4) × UNIV}
sv_round r S v d_f, opt_mru_round r Q S v d_f
{> lv_ref_rel}"
apply(clarsimp simp add: PO_rhoare_defs lv_ref_rel_def opt_mru_round_def sv_round_def
act_ref del: disjCI)
apply(auto intro!: opt_mru_guard_imp_mru_guard[where Q=Q]  mru_vote_implies_safe[where Q=Q]
dest: opt_mru_guard_imp_Quorum)
done

lemma Opt_MRU_Vote_Refines:
"PO_refines (lv_ref_rel ∩ (Vinv1 ∩ Vinv2 ∩ SV_inv3 ∩ SV_inv4) × UNIV) sv_TS mru_opt_TS"
proof(rule refine_using_invariants)
show "init mru_opt_TS ⊆ lv_ref_rel `` init sv_TS"
by(auto simp add: mru_opt_TS_defs sv_TS_defs lv_ref_rel_def
process_mru_def mru_of_set_def vote_set_def option_Max_by_def)
next
show
"{lv_ref_rel ∩ (Vinv1 ∩ Vinv2 ∩ SV_inv3 ∩ SV_inv4) × UNIV} trans sv_TS, trans mru_opt_TS {> lv_ref_rel}"
by(auto simp add: sv_TS_defs mru_opt_TS_defs intro!: opt_mru_round_refines)
next
show
"{Vinv1 ∩ Vinv2 ∩ SV_inv3 ∩ SV_inv4 ∩ Domain (lv_ref_rel ∩ UNIV × UNIV)}
trans sv_TS
{> Vinv1 ∩ Vinv2 ∩ SV_inv3 ∩ SV_inv4}"
using SV_inv1_inductive(2) SV_inv2_inductive(2) SV_inv3_inductive(2) SV_inv4_inductive(2)
by blast
qed(auto intro!: SV_inv1_inductive(1) SV_inv2_inductive(1) SV_inv3_inductive(1) SV_inv4_inductive(1))

subsection ‹Invariants›
(******************************************************************************)

definition OMRU_inv1 :: "opt_mru_state set" where
"OMRU_inv1 = {s. ∀p. (case mru_vote s p of
Some (r, _) ⇒ r < next_round s
| None ⇒ True)
}"

lemma OMRU_inv1_inductive:
"init mru_opt_TS ⊆ OMRU_inv1"
"{OMRU_inv1} trans mru_opt_TS {> OMRU_inv1}"
by(fastforce simp add: mru_opt_TS_def opt_mru_init_def PO_hoare_def OMRU_inv1_def mru_opt_trans_def
opt_mru_round_def const_map_is_Some less_Suc_eq
split: option.split_asm option.split)+

lemmas OMRU_inv1I = OMRU_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas OMRU_inv1E [elim] = OMRU_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas OMRU_inv1D = OMRU_inv1_def [THEN setc_def_to_dest, rule_format]

end

end
```