Theory Same_Vote

section ‹The Same Vote Model›
theory Same_Vote
imports Voting

context quorum_process begin

subsection ‹Model definition›

text ‹The system state remains the same as in the Voting model, but the
  voting event is changed.›

definition safe :: "v_state  round  val  bool" where
  safe_def': "safe s r v  
    r' < r. Q  Quorum. w. (votes s r') ` Q = {Some w}  v = w"

text ‹This definition of @{term safe} is easier to reason about in Isabelle.›
lemma safe_def:
  "safe s r v =
    (r' < r. Q w. quorum_for Q w (votes s r')   v = w)"
  by(auto simp add: safe_def' quorum_for_def' Ball_def)

definition sv_round :: "round  process set  val  (process, val)map  (v_state × v_state) set" where
  "sv_round r S v r_decisions = {(s, s').
     ― ‹guards›
     r = next_round s
      (S  {}  safe s r v)
      d_guard r_decisions (const_map v S)
      ― ‹actions›
     s' = s 
       next_round := Suc r
       , votes := (votes s)(r := const_map v S)
       , decisions := (decisions s ++ r_decisions)

definition sv_trans :: "(v_state × v_state) set" where
  "sv_trans = (r S v D. sv_round r S v D)  Id"

definition sv_TS :: "v_state TS" where
  "sv_TS =  init = v_init, trans = sv_trans "

lemmas sv_TS_defs = sv_TS_def v_init_def sv_trans_def

subsection ‹Refinement›

lemma safe_imp_no_defection:
  "safe s (next_round s) v  no_defection s (const_map v S) (next_round s)" 
  by(auto simp add: safe_def no_defection_def restrict_map_def const_map_def)
lemma const_map_quorum_locked:
  "S  Quorum  locked_in_vf (const_map v S) v"
  by(auto simp add: locked_in_vf_def const_map_def quorum_for_def)

lemma sv_round_refines:
  "{Id} v_round r (const_map v S) r_decisions, sv_round r S v r_decisions {> Id}"
  by(auto simp add: PO_rhoare_defs sv_round_def v_round_def  no_defection_empty
    dest!: safe_imp_no_defection const_map_quorum_locked)

lemma Same_Vote_Refines:
  "PO_refines Id v_TS sv_TS"
  by(auto simp add: PO_refines_def sv_TS_def sv_trans_def v_TS_defs intro!: 
    sv_round_refines relhoare_refl)

subsection ‹Invariants›

definition SV_inv3 where
  "SV_inv3 = {s. r a b v w. 
    votes s r a = Some v  votes s r b = Some w  v = w

lemmas SV_inv3I = SV_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas SV_inv3E [elim] = SV_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas SV_inv3D = SV_inv3_def [THEN setc_def_to_dest, rule_format]
subsubsection ‹Proof of invariants›

lemma SV_inv3_v_round: 
  "{SV_inv3} sv_round r S v D {> SV_inv3}" 
  apply(clarsimp simp add: PO_hoare_defs intro!: SV_inv3I)
  apply(force simp add: sv_round_def const_map_def restrict_map_def SV_inv3_def)

lemmas SV_inv3_event_pres = SV_inv3_v_round 

lemma SV_inv3_inductive:
  "init sv_TS  SV_inv3" 
  "{SV_inv3} trans sv_TS {> SV_inv3}" 
  apply (simp add: sv_TS_defs SV_inv3_def)
  by (auto simp add: sv_TS_defs SV_inv3_event_pres)

lemma SV_inv3_invariant: "reach sv_TS  SV_inv3"
  by (auto intro!: inv_rule_basic SV_inv3_inductive del: subsetI)

text ‹

This is a different characterization of @{term safe}, due to Lampson~cite"lampson_abcds_2001":
  @{term "safe' s r v = (r'< r. (Q  Quorum. a  Q. w. votes s r' a = Some w  w = v))"}

It is, however, strictly stronger than our characterization, since we do not at this point assume
the "completeness" of our quorum system (for any set S, either S or the complement of S is a
quorum), and the following is thus not provable: @{term "s  SV_inv3  safe' s = safe s"}.


subsubsection ‹Transfer of abstract invariants›

lemma SV_inv1_inductive:
  "init sv_TS  Vinv1"
  "{Vinv1} trans sv_TS {> Vinv1}" 
  apply(rule abs_INV_init_transfer[OF Same_Vote_Refines Vinv1_inductive(1), simplified])
  apply(rule abs_INV_trans_transfer[OF Same_Vote_Refines Vinv1_inductive(2), simplified])

lemma SV_inv1_invariant:
  "reach sv_TS  Vinv1"
  by(rule abs_INV_transfer[OF Same_Vote_Refines Vinv1_invariant, simplified])

lemma SV_inv2_inductive:
  "init sv_TS  Vinv2"
  "{Vinv2  Vinv1} trans sv_TS {> Vinv2}" 
  apply(rule abs_INV_init_transfer[OF Same_Vote_Refines Vinv2_inductive(1), simplified])
  apply(rule abs_INV_trans_transfer[OF Same_Vote_Refines Vinv2_inductive(2), simplified])

lemma SV_inv2_invariant:
  "reach sv_TS  Vinv2"
  by(rule abs_INV_transfer[OF Same_Vote_Refines Vinv2_invariant, simplified])

subsubsection ‹Additional invariants›

text ‹With Same Voting, the voted values are safe in the next round.›

definition SV_inv4 :: "v_state set" where
  "SV_inv4 = {s. v a r. votes s r a = Some v  safe s (Suc r) v }"

lemmas SV_inv4I = SV_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas SV_inv4E [elim] = SV_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas SV_inv4D = SV_inv4_def [THEN setc_def_to_dest, rule_format]

lemma SV_inv4_sv_round: 
  "{SV_inv4  (Vinv1  Vinv2)} sv_round r S v D {> SV_inv4}" 
proof(clarsimp simp add: PO_hoare_defs intro!: SV_inv4I)
  fix s v' a r' s'
    step: "(s, s')  sv_round r S v D"
    and invs: "s  SV_inv4" "s  Vinv1" "s  Vinv2"
    and vote: "votes s' r' a = Some v'"
  thus "safe s' (Suc r') v'"
  proof(cases "r=r'")
    case True
    moreover hence safe: "safe s' r' v'" using step vote
      by(force simp add: sv_round_def const_map_is_Some safe_def quorum_for_def)
    ultimately show ?thesis using step vote
      by(force simp add: safe_def less_Suc_eq sv_round_def quorum_for_def const_map_is_Some 
        dest: quorum_non_empty)
  qed(clarsimp simp add: sv_round_def safe_def Vinv2_def Vinv1_def  SV_inv4_def
      intro: Quorum_not_empty)

lemmas SV_inv4_event_pres = SV_inv4_sv_round 

lemma SV_inv4_inductive:
  "init sv_TS  SV_inv4" 
  "{SV_inv4  (Vinv1  Vinv2)} trans sv_TS {> SV_inv4}"
  apply(simp add: sv_TS_defs SV_inv4_def)
  by (auto simp add: sv_TS_defs SV_inv4_event_pres)

lemma SV_inv4_invariant: "reach sv_TS  SV_inv4"
  by (rule inv_rule_incr)
  (auto intro: SV_inv4_inductive SV_inv2_invariant SV_inv1_invariant del: subsetI)

end (* context quorum_process *)