# Theory Voting_Opt

```section ‹The Optimized Voting Model›

theory Voting_Opt
imports Voting
begin

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

record opt_v_state =
next_round :: round
last_vote :: "(process, val) map"
decisions :: "(process, val)map"

definition flv_init where
"flv_init = { ⦇ next_round = 0, last_vote = Map.empty, decisions = Map.empty ⦈ }"

context quorum_process begin

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

definition flv_guard :: "(process, round × val)map ⇒ process set ⇒ val ⇒ bool" where
"flv_guard lvs Q v ≡ Q ∈ Quorum ∧
(let alv = fmru_lv lvs Q in alv = None ∨ (∃r. alv = Some (r, v)))"

definition opt_no_defection :: "opt_v_state ⇒ (process, val)map ⇒ bool" where
opt_no_defection_def':
∀v. ∀Q. quorum_for Q v (last_vote s) ⟶ round_votes ` Q ⊆ {None, Some v}"

lemma opt_no_defection_def:
(∀a Q v. quorum_for Q v (last_vote s) ∧ a ∈ Q ⟶ round_votes a ∈ {None, Some v})"
by (metis option.distinct(1) option.sel)

definition flv_round :: "round ⇒ (process, val)map ⇒  (process, val)map ⇒ (opt_v_state × opt_v_state) set" where
"flv_round r r_votes r_decisions = {(s, s').
― ‹guards›
r = next_round s
∧ ― ‹actions›
s' = s⦇
next_round := Suc r
, last_vote := last_vote s ++ r_votes
, decisions := (decisions s) ++ r_decisions
⦈
}"

lemmas flv_evt_defs = flv_round_def flv_guard_def

definition flv_trans :: "(opt_v_state × opt_v_state) set" where
"flv_trans = (⋃r v_f d_f. flv_round r v_f d_f)"

definition flv_TS :: "opt_v_state TS" where
"flv_TS = ⦇ init = flv_init, trans = flv_trans ⦈"

lemmas flv_TS_defs = flv_TS_def flv_init_def flv_trans_def

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

definition flv_ref_rel :: "(v_state × opt_v_state)set" where
"flv_ref_rel = {(sa, sc).
sc = ⦇
next_round = v_state.next_round sa
, last_vote = map_option snd o (process_mru (votes sa))
, decisions = v_state.decisions sa
⦈
}"

subsubsection ‹Guard strengthening›
(******************************************************************************)

lemma process_mru_Max:
assumes
inv: "sa ∈ Vinv1"
and process_mru: "process_mru (votes sa) p = Some (r, v)"
shows
"votes sa r p = Some v ∧ (∀r' > r. votes sa r' p = None)"
proof-
from process_mru have not_empty: "vote_set (votes sa) {p} ≠ {}"
by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def)
note Max_by_conds = Vinv1_finite_vote_set[OF inv] this
from Max_by_dest[OF Max_by_conds, where f=fst]
have
r:
"(r, v) = Max_by fst (vote_set (votes sa) {p})"
"votes sa r p = Some v"
using process_mru
by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def vote_set_def)
have "∀r' >r . votes sa r' p = None"
proof(safe)
fix r'
assume less: "r < r'"
hence "∀v. (r', v) ∉ vote_set (votes sa) {p}" using process_mru
by(auto dest!: Max_by_ge[where f=fst, OF Vinv1_finite_vote_set[OF inv]]
thus "votes sa r' p = None"
qed
thus ?thesis using r(2)
by(auto)
qed

lemma opt_no_defection_imp_no_defection:
assumes
and R: "(sa, sc) ∈ flv_ref_rel"
and ainv: "sa ∈ Vinv1" "sa ∈ Vinv2"
shows
proof(unfold no_defection_def, safe)
fix r' v a Q w
assume
r'_less: "r' < r"
and Q: "quorum_for Q v (votes sa r')"
and a_in_Q: "a ∈ Q"
have "Q ∈ Quorum" using Q
hence "quorum_for Q v (last_vote sc)"
fix q
assume "q ∈ Q"
with Q have q_r': "votes sa r' q = Some v"
then obtain w where w: "last_vote sc q = Some w" using R
by(clarsimp simp add: flv_ref_rel_def process_mru_def mru_of_set_def
option_Max_by_def)
with R obtain r_max where "process_mru (votes sa) q = Some (r_max, w)"
from process_mru_Max[OF ainv(1) this] q_r' have
"votes sa r_max q = Some w"
"r' ≤ r_max"
using q_r'
thus "last_vote sc q = Some v" using ainv(2) Q ‹q ∈ Q›
apply(case_tac "r_max = r'")
apply(clarsimp simp add: w Vinv2_def no_defection_def q_r' dest: le_neq_implies_less)
apply(fastforce simp add: w Vinv2_def no_defection_def q_r' dest!: le_neq_implies_less)
done
qed
qed

subsubsection ‹Action refinement›
(******************************************************************************)

lemma act_ref:
assumes
inv: "s ∈ Vinv1"
shows
"map_option snd o (process_mru ((votes s)(v_state.next_round s := v_f)))
= ((map_option snd o (process_mru (votes s))) ++ v_f)"

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

lemma flv_round_refines:
"{flv_ref_rel ∩ (Vinv1 ∩ Vinv2) × UNIV}
v_round r v_f  d_f, flv_round r v_f d_f
{> flv_ref_rel}"
by(auto simp add: PO_rhoare_defs flv_round_def v_round_def
flv_ref_rel_def act_ref
intro: opt_no_defection_imp_no_defection)

lemma Last_Voting_Refines:
"PO_refines (flv_ref_rel ∩ (Vinv1 ∩ Vinv2) × UNIV) v_TS flv_TS"
proof(rule refine_using_invariants)
show "init flv_TS ⊆ flv_ref_rel `` init v_TS"
by(auto simp add: flv_TS_defs v_TS_defs flv_ref_rel_def
process_mru_def mru_of_set_def vote_set_def option_Max_by_def)
next
show
"{flv_ref_rel ∩ (Vinv1 ∩ Vinv2) × UNIV} trans v_TS, trans flv_TS {> flv_ref_rel}"
by(auto simp add: v_TS_defs flv_TS_defs intro!: flv_round_refines)
next
show
"{Vinv1 ∩ Vinv2 ∩ Domain (flv_ref_rel ∩ UNIV × UNIV)}
trans v_TS
{> Vinv1 ∩ Vinv2}"
using Vinv1_inductive(2) Vinv2_inductive(2)
by blast
qed(auto intro!: Vinv1_inductive(1) Vinv2_inductive(1))

end

end
```