Theory MRU_Vote_Opt

section ‹Optimized MRU Vote Model›

theory MRU_Vote_Opt
imports MRU_Vote

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" 
  "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})"
  by(auto simp add: vote_set_def voters_def)

lemma empty_ran:
  "(ran f = {}) = (x. f x = None)"
  apply(auto simp add: ran_def)
  by (metis option.collapse)

lemma empty_ran_restrict:
  "(ran (f |` A) = {}) = (x  A. f x = None)"
  by(auto simp add: empty_ran restrict_map_def)

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'"
  by(auto simp add: option_Max_by_def)

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:
    inv1: "s  Vinv1"
    and inv3: "s  SV_inv3"
  defines "vs  votes s"
    "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 
    by (metis option.collapse option.distinct(1))
  assume nempty: "ran (process_mru vs |` Q)  {}" "vote_set vs Q  {}"

  hence nempty': "Q  voters vs  {}"
    by(auto simp add: vote_set_def voters_def)

  have nempty'': "{}  (λa. vote_set vs {a}) ` (Q  voters vs)"
    by(auto simp add: vote_set_def voters_def)

  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)

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:
    "s  Vinv1"
    "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))"
    by(auto simp add: process_mru_map_add[OF assms(1)] map_add_def const_map_def 

subsubsection ‹The complete refinement› 

lemma opt_mru_guard_imp_Quorum:
  "opt_mru_guard vs Q v  Q  Quorum"
  by (simp add: opt_mru_guard_def Let_def)

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)
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)
    "{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)
    "{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]