Theory Same_Vote
section ‹The Same Vote Model›
theory Same_Vote
imports Voting
begin
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').
r = next_round s
∧ (S ≠ {} ⟶ safe s r v)
∧ d_guard r_decisions (const_map v S)
∧
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)
done
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])
done
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])
done
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'
assume
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)
qed
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
end