# Theory Observing_Quorums_Opt

```section ‹The Optimized Observing Quorums Model›

theory Observing_Quorums_Opt
imports Observing_Quorums
begin

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

record opt_obsv_state =
next_round :: round
decisions :: "(process, val)map"
last_obs :: "(process, val)map"

context mono_quorum
begin

definition opt_obs_safe where
"opt_obs_safe obs_f v ≡ ∃p. obs_f p ∈ {None, Some v}"

definition olv_round where
"olv_round r S v r_decisions Ob ≡ {(s, s').
― ‹guards›
r = next_round s
∧ (S ≠ {} ⟶ opt_obs_safe (last_obs s) v)
∧ (S ∈ Quorum ⟶ Ob = UNIV)
∧ d_guard r_decisions (const_map v S)
∧ (Ob ≠ {} ⟶ S ≠ {})
∧ ― ‹actions›
s' = s⦇
next_round := Suc r
, decisions := decisions s ++ r_decisions
, last_obs := last_obs s ++ const_map v Ob
⦈
}"

definition olv_init where
"olv_init = { ⦇ next_round = 0, decisions = Map.empty, last_obs = Map.empty ⦈ }"

definition olv_trans :: "(opt_obsv_state × opt_obsv_state) set" where
"olv_trans = (⋃r S v D Ob. olv_round r S v D Ob) ∪ Id"

definition olv_TS :: "opt_obsv_state TS" where
"olv_TS = ⦇ init = olv_init, trans = olv_trans ⦈"

lemmas olv_TS_defs = olv_TS_def olv_init_def olv_trans_def

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

definition olv_ref_rel where
"olv_ref_rel ≡ {(sa, sc).
next_round sc = v_state.next_round sa
∧ decisions sc = v_state.decisions sa
∧ last_obs sc = map_option snd o process_mru (obsv_state.obs sa)
}"

lemma OV_inv2_finite_map_graph:
"s ∈ OV_inv2 ⟹ finite (map_graph (case_prod (obsv_state.obs s)))"
apply(rule finite_dom_finite_map_graph)
apply(rule finite_subset[where B="{0..< v_state.next_round s} × UNIV"])
apply(auto simp add: OV_inv2_def dom_def not_le[symmetric])
done

lemma OV_inv2_finite_obs_set:
"s ∈ OV_inv2 ⟹ finite (vote_set (obsv_state.obs s) Q)"
apply(drule OV_inv2_finite_map_graph)
apply(clarsimp simp add: map_graph_def fun_graph_def vote_set_def)
apply(erule finite_surj[where f="λ((r, a), v). (r, v)"])

lemma olv_round_refines:
"{olv_ref_rel ∩ (OV_inv2 ∩ OV_inv3 ∩ OV_inv4) × UNIV} obsv_round r S v D Ob, olv_round r S v D Ob {>olv_ref_rel}"
fix sa :: obsv_state and sc sc'
assume
ainv: "sa ∈ OV_inv2" "sa ∈ OV_inv3" "sa ∈ OV_inv4"
and step: "(sc, sc') ∈ olv_round r S v D Ob"
and R: "(sa, sc) ∈ olv_ref_rel"

― ‹Abstract guard.›
have "S ≠ {} ⟶ obs_safe (v_state.next_round sa) sa v"
proof(rule impI, rule ccontr)
assume S_nonempty: "S ≠ {}" and no_Q: "¬ obs_safe (v_state.next_round sa) sa v"
from no_Q obtain r_w w where
r_w: "r_w < v_state.next_round sa"
and all_obs: "∀p. obsv_state.obs sa r_w p = Some w"
and diff: "w ≠ v" using ainv(3)[THEN OV_inv4D]
from diff step R obtain p where
p_w: "S ≠ {} ⟶ (map_option snd ∘ process_mru (obsv_state.obs sa)) p ≠ Some w"
by (simp add: opt_obs_safe_def quorum_for_def olv_round_def  olv_ref_rel_def)
(metis option.distinct(1) option.sel snd_conv)
from all_obs have nempty: "vote_set (obsv_state.obs sa) {p} ≠ {}"
then obtain r_w' w' where w': "process_mru (obsv_state.obs sa) p = Some (r_w', w')"
(metis option_Max_by_def surj_pair)
hence max: "(r_w', w') = Max_by fst (vote_set (obsv_state.obs sa) {p})"
by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def)
hence w'_obs: "(r_w', w') ∈ vote_set (obsv_state.obs sa) {p}"
using Max_by_in[OF OV_inv2_finite_obs_set[OF ainv(1), of "{p}"] nempty]
by fastforce
have "r_w ≤ r_w'" using all_obs
apply -
apply(rule Max_by_ge[OF OV_inv2_finite_obs_set[OF ainv(1), of "{p}"], of "(r_w, w)" fst,
simplified max[symmetric], simplified])
done
moreover have "w' ≠ w" using p_w w' S_nonempty
by(auto)
ultimately have "r_w < r_w'" using all_obs w'_obs
apply(elim le_neq_implies_less)
done
thus False using ainv(2)[THEN OV_inv3D] w'_obs all_obs ‹w' ≠ w›
qed

― ‹Action refinement.›
moreover have
"(map_option snd ∘ process_mru (obsv_state.obs sa)) ++ const_map v Ob =
map_option snd ∘ process_mru ((obsv_state.obs sa)(v_state.next_round sa := const_map v Ob))"
proof-
from ‹sa ∈ OV_inv2›[THEN OV_inv2D]
have empty: "∀r'≥v_state.next_round sa. obsv_state.obs sa r' = Map.empty"
by simp
show ?thesis
qed

ultimately show "∃sa'. (sa, sa') ∈ obsv_round r S v D Ob ∧ (sa', sc') ∈ olv_ref_rel"
using R step
by(clarsimp simp add: obsv_round_def olv_round_def olv_ref_rel_def)

qed

lemma OLV_Refines:
"PO_refines (olv_ref_rel ∩ (OV_inv2 ∩ OV_inv3 ∩ OV_inv4) × UNIV) obsv_TS olv_TS"
proof(rule refine_using_invariants)
show "init olv_TS ⊆ olv_ref_rel `` init obsv_TS"
by(auto simp add: obsv_TS_defs olv_TS_defs olv_ref_rel_def process_mru_def mru_of_set_def
vote_set_def option_Max_by_def intro!: ext)
next
show
"{olv_ref_rel ∩ (OV_inv2 ∩ OV_inv3 ∩ OV_inv4) × UNIV} TS.trans obsv_TS, TS.trans olv_TS {> olv_ref_rel}"
by(auto simp add: PO_refines_def obsv_TS_defs olv_TS_defs
intro!: olv_round_refines)
qed (auto intro: OV_inv2_inductive OV_inv3_inductive OV_inv4_inductive
OV_inv2_inductive(1)[THEN subsetD] OV_inv3_inductive(1)[THEN subsetD]
OV_inv4_inductive(1)[THEN subsetD])

end

end
```