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':
    "opt_no_defection s round_votes ≡ 
    ∀v. ∀Q. quorum_for Q v (last_vote s) ⟶ round_votes ` Q ⊆ {None, Some v}"

lemma opt_no_defection_def:
  "opt_no_defection s round_votes =
    (∀a Q v. quorum_for Q v (last_vote s) ∧ a ∈ Q ⟶ round_votes a ∈ {None, Some v})"
  apply(auto simp add: opt_no_defection_def')
  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
     ∧ opt_no_defection s r_votes
     ∧ d_guard r_decisions r_votes
     ∧ ― ‹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]] 
        simp add: process_mru_def mru_of_set_def option_Max_by_def)
    thus "votes sa r' p = None"
      by(auto simp add: vote_set_def)
  qed
  thus ?thesis using r(2)
    by(auto)
qed

lemma opt_no_defection_imp_no_defection:
  assumes
    conc_guard: "opt_no_defection sc round_votes"
    and R: "(sa, sc) ∈ flv_ref_rel"
    and ainv: "sa ∈ Vinv1" "sa ∈ Vinv2"
  shows
    "no_defection sa round_votes r"
proof(unfold no_defection_def, safe)
  fix r' v a Q w
  assume
    r'_less: "r' < r"
    and a_votes_w: "round_votes a = Some w"
    and Q: "quorum_for Q v (votes sa r')"
    and a_in_Q: "a ∈ Q"
  have "Q ∈ Quorum" using Q
    by(auto simp add: quorum_for_def)
  hence "quorum_for Q v (last_vote sc)"
  proof(clarsimp simp add: quorum_for_def)
    fix q
    assume "q ∈ Q"
    with Q have q_r': "votes sa r' q = Some v"
      by(auto simp add: quorum_for_def)
    hence votes: "vote_set (votes sa) {q} ≠ {}"
      by(auto simp add: vote_set_def)
    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)"
      by(clarsimp simp add: flv_ref_rel_def)
    from process_mru_Max[OF ainv(1) this] q_r' have
      "votes sa r_max q = Some w" 
      "r' ≤ r_max"
      using q_r'
      by(auto simp add: not_less[symmetric])
    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
  thus "round_votes a = Some v" using conc_guard a_in_Q a_votes_w r'_less
    by(fastforce simp add: opt_no_defection_def)
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)"
    by(auto simp add: process_mru_map_add[OF inv] map_add_def split: option.split)

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