# Theory Voting

```section ‹The Voting Model›

theory Voting imports Refinement Consensus_Misc Quorums
begin

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

record v_state =
(* We want 0 to be the first round, and we also have to use something in the initial state
- hence next_round *)
next_round :: round
votes :: "round ⇒ (process, val) map"
decisions :: "(process, val)map"

text ‹Initially, no rounds have been executed (the next round is 0), no votes have been
cast, and no decisions have been made.›

definition v_init :: "v_state set" where
"v_init = { ⦇ next_round = 0, votes = λr a. None, decisions = Map.empty ⦈ }"

context quorum_process begin

definition quorum_for :: "process set ⇒ val ⇒ (process, val)map ⇒ bool" where
quorum_for_def':
"quorum_for Q v v_f ≡ Q ∈ Quorum ∧ v_f ` Q = {Some v}"

text ‹The following definition of @{term quorum_for} is easier to reason about in Isabelle.›

lemma quorum_for_def:
"quorum_for Q v v_f = (Q ∈ Quorum ∧ (∀p ∈ Q. v_f p = Some v))"
by(auto simp add: quorum_for_def' image_def dest: quorum_non_empty)

definition locked_in_vf :: "(process, val)map ⇒ val ⇒ bool" where
"locked_in_vf v_f v ≡ ∃Q. quorum_for Q v v_f"

definition locked_in :: "v_state ⇒ round ⇒ val ⇒ bool" where
"locked_in s r v = locked_in_vf (votes s r) v"

definition d_guard :: "(process ⇒ val option) ⇒ (process ⇒ val option) ⇒ bool" where
"d_guard r_decisions r_votes ≡ ∀p v.
r_decisions p = Some v ⟶ locked_in_vf r_votes v"

definition no_defection :: "v_state ⇒ (process, val)map ⇒ round ⇒ bool" where
no_defection_def':
∀r' < r. ∀Q ∈ Quorum. ∀v. (votes s r') ` Q = {Some v} ⟶ r_votes ` Q ⊆ {None, Some v}"

text ‹The following definition of @{term no_defection} is easier to reason about in Isabelle.›

lemma no_defection_def:
(∀r' < r. ∀a Q v. quorum_for Q v (votes s r') ∧ a ∈ Q ⟶ round_votes a ∈ {None, Some v})"
apply(auto simp add: no_defection_def' Ball_def quorum_for_def')
apply(blast)
by (metis option.discI option.inject)

definition locked :: "v_state ⇒ val set" where
"locked s = {v. ∃r. locked_in s r v}"

text ‹The sole system event.›

definition v_round :: "round ⇒ (process, val)map ⇒ (process, val)map ⇒ (v_state × v_state) set" where
"v_round r r_votes r_decisions = {(s, s').
― ‹guards›
r = next_round s
∧ ― ‹actions›
s' = s⦇
next_round := Suc r,
decisions := (decisions s) ++ r_decisions
⦈
}"

lemmas v_evt_defs = v_round_def

definition v_trans :: "(v_state × v_state) set" where
"v_trans = (⋃r v_f d_f. v_round r v_f d_f) ∪ Id"

definition v_TS :: "v_state TS" where
"v_TS = ⦇ init = v_init, trans = v_trans ⦈"

lemmas v_TS_defs = v_TS_def v_init_def v_trans_def

subsection ‹Invariants›
(******************************************************************************)

text ‹The only rounds where votes could have been cast are the ones
preceding the next round.›
definition Vinv1 where
"Vinv1 = {s. ∀r. next_round s ≤ r ⟶ votes s r = Map.empty }"

lemmas Vinv1I = Vinv1_def [THEN setc_def_to_intro, rule_format]
lemmas Vinv1E [elim] = Vinv1_def [THEN setc_def_to_elim, rule_format]
lemmas Vinv1D = Vinv1_def [THEN setc_def_to_dest, rule_format]

text ‹The votes cast must respect the @{term no_defection} property.›
definition Vinv2 where
"Vinv2 = {s. ∀r. no_defection s (votes s r) r }"

lemmas Vinv2I = Vinv2_def [THEN setc_def_to_intro, rule_format]
lemmas Vinv2E [elim] = Vinv2_def [THEN setc_def_to_elim, rule_format]
lemmas Vinv2D = Vinv2_def [THEN setc_def_to_dest, rule_format]

definition Vinv3 where
"Vinv3 = {s. ran (decisions s) ⊆ locked s}"

lemmas Vinv3I = Vinv3_def [THEN setc_def_to_intro, rule_format]
lemmas Vinv3E [elim] = Vinv3_def [THEN setc_def_to_elim, rule_format]
lemmas Vinv3D = Vinv3_def [THEN setc_def_to_dest, rule_format]

subsubsection ‹Proofs of invariants›
(******************************************************************************)

(*************************)
lemma Vinv1_v_round:
"{Vinv1} v_round r v_f d_f {> Vinv1}"
by(auto simp add: PO_hoare_defs v_round_def intro!: Vinv1I)

lemmas Vinv1_event_pres = Vinv1_v_round

lemma Vinv1_inductive:
"init v_TS ⊆ Vinv1"
"{Vinv1} trans v_TS {> Vinv1}"
by (auto simp add: v_TS_defs Vinv1_event_pres)

lemma Vinv1_invariant: "reach v_TS ⊆ Vinv1"
by (rule inv_rule_basic, auto intro!: Vinv1_inductive)

text ‹The following two lemmas will be useful later, when we
start taking votes with the maximum timestamp.›

lemma Vinv1_finite_map_graph:
"s ∈ Vinv1 ⟹ finite (map_graph (case_prod (votes 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: Vinv1_def dom_def not_le[symmetric])
done

lemma Vinv1_finite_vote_set:
"s ∈ Vinv1 ⟹ finite (vote_set (votes s) Q)"
apply(drule Vinv1_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)"])

assumes
"s ∈ Vinv1"
shows
"process_mru ((votes s)(next_round s := v_f)) =
(process_mru (votes s) ++ (λp. map_option (Pair (next_round s)) (v_f p)))"
proof-
from assms[THEN Vinv1D] have empty: "∀r' ≥ next_round s. votes s r' = Map.empty"
by simp
show ?thesis
qed

(*************************)

lemma no_defection_empty:
"no_defection s Map.empty r'"

lemma no_defection_preserved:
assumes
"s ∈ Vinv1"
"r = next_round s"
"no_defection s v_f r"
"no_defection s (votes s r') r'"
shows
"no_defection s' (votes s' r') r'" using assms

(********)

lemma Vinv2_v_round:
"{Vinv2 ∩ Vinv1} v_round r v_f d_f {> Vinv2}"
apply(auto simp add: PO_hoare_defs intro!: Vinv2I)
apply(rename_tac s' r' s)
apply(erule no_defection_preserved)
apply(auto simp add: v_round_def intro!: v_state.equality)
done

lemmas Vinv2_event_pres = Vinv2_v_round

lemma Vinv2_inductive:
"init v_TS ⊆ Vinv2"
"{Vinv2 ∩ Vinv1} trans v_TS {> Vinv2}"
by (auto simp add: v_TS_defs Vinv2_event_pres)

lemma Vinv2_invariant: "reach v_TS ⊆ Vinv2"
by (rule inv_rule_incr, auto intro: Vinv2_inductive Vinv1_invariant del: subsetI)

(*************************)
lemma locked_preserved:
assumes
"s ∈ Vinv1"
"r = next_round s"
shows
"locked s ⊆ locked s'" using assms
apply(auto simp add: locked_def locked_in_def locked_in_vf_def quorum_for_def dest!: Vinv1D)
by (metis option.distinct(1))

(*************************)

lemma Vinv3_v_round:
"{Vinv3 ∩ Vinv1} v_round r v_f d_f {> Vinv3}"
proof(clarsimp simp add: PO_hoare_defs, intro Vinv3I, safe)
fix s s' v
assume step: "(s, s') ∈ v_round r v_f d_f" and inv3: "s ∈ Vinv3" and inv1: "s ∈ Vinv1"
and dec: "v ∈ ran (decisions s')"
have "locked s ⊆ locked s'" using step
by(intro locked_preserved[OF inv1, where s'=s']) (auto simp add: v_round_def)
with Vinv3D[OF inv3] step dec
show "v ∈ locked s'"
apply(auto simp add: locked_def locked_in_def d_guard_def ran_def)
done
qed

lemmas Vinv3_event_pres = Vinv3_v_round

lemma Vinv3_inductive:
"init v_TS ⊆ Vinv3"
"{Vinv3 ∩ Vinv1} trans v_TS {> Vinv3}"
by (auto simp add: v_TS_defs Vinv3_event_pres)

lemma Vinv3_invariant: "reach v_TS ⊆ Vinv3"
by (rule inv_rule_incr, auto intro: Vinv3_inductive Vinv1_invariant del: subsetI)

subsection ‹Agreement and stability›
(******************************************************************************)

text ‹Only a singe value can be locked within the votes for one round.›
lemma locked_in_vf_same:
"⟦ locked_in_vf v_f v; locked_in_vf v_f w ⟧ ⟹ v = w" using qintersect
apply(auto simp add: locked_in_vf_def quorum_for_def image_iff)
by (metis Int_iff all_not_in_conv option.inject)

text ‹In any reachable state, no two different values can be locked in
different rounds.›
theorem locked_in_different:
assumes
"s ∈ Vinv2"
"locked_in s r1 v"
"locked_in s r2 w"
"r1 < r2"
shows
"v = w"
proof-
― ‹To be locked, @{term v} and @{term w} must each have received votes from a quorum.›
from assms(2-3) obtain Q1 Q2
where Q12: "Q1 ∈ Quorum" "Q2 ∈ Quorum" "quorum_for Q1 v (votes s r1)" "quorum_for Q2 w (votes s r2)"
by(auto simp add: locked_in_def locked_in_vf_def quorum_for_def)
― ‹By the quorum intersection property, some process from @{term Q1} voted for @{term w}:›
then obtain a where "a ∈ Q1" "votes s r2 a = Some w"
using qintersect[OF ‹Q1 ∈ Quorum› ‹Q2 ∈ Quorum›]
― ‹But from @{term Vinv2} we conclude that @{term a} could not have defected by voting
@{term w}, so @{term ?thesis}:›
thus ?thesis using ‹s ∈ Vinv2› ‹quorum_for Q1 v (votes s r1)› ‹r1 < r2›
by(fastforce simp add: Vinv2_def no_defection_def quorum_for_def')
qed

text ‹It is simple to extend the previous theorem to any two (not necessarily different) rounds.›
theorem locked_unique:
assumes
"s ∈ Vinv2"
"v ∈ locked s" "w ∈ locked s"
shows
"v = w"
proof -
from assms(2-3) obtain r1 r2 where quoIn: "locked_in s r1 v" "locked_in s r2 w"
have "r1 < r2 ∨ r1 = r2 ∨ r2 < r1" by (rule linorder_less_linear)
thus ?thesis
proof (elim disjE)
assume "r1 = r2"
with quoIn show ?thesis
qed(auto intro: locked_in_different[OF ‹s ∈ Vinv2›] quoIn sym)
qed

text ‹We now prove that decisions are stable; once a process makes a decision, it never
changes it, and it does not go back to an undecided state. Note that behaviors grow at
the front; hence @{term "tr ! (i-j)"} is later in the trace than @{term "tr ! i"}.›
lemma stable_decision:
assumes beh: "tr ∈ beh v_TS"
and len: "i < length tr"
and s: "s = nth tr i"
and t: "t = nth tr (i - j)"
and dec:
"decisions s p = Some v"
shows
"decisions t p = Some v"
proof-
― ‹First, we show that the both @{term s} and @{term t} respect the invariants.›
have reach: "s ∈ reach v_TS" "t ∈ reach v_TS" using beh s t len
apply (metis len nth_mem)
apply (metis less_imp_diff_less nth_mem)
done
hence invs2: "s ∈ Vinv2" and invs3: "s ∈ Vinv3"
by(blast dest: Vinv2_invariant[THEN subsetD] Vinv3_invariant[THEN subsetD])+

show ?thesis using t
proof(induction j arbitrary: t)
case (Suc j)
hence dec_j: "decisions (tr ! (i - j)) p = Some v"
by simp
thus "decisions t p = Some v" using Suc
― ‹As @{term "(-)"} is a total function on naturals, we perform a case distinction;
if @{term "i < j"}, the induction step is trivial.›
proof(cases "i ≤ j")
― ‹The non-trivial case.›
case False
define t' where "t' = tr ! (i - j)"
― ‹Both @{term t} and @{term t'} are reachable, thus respect the invariants, and
they are related by the transition relation.›
hence "t' ∈ reach v_TS" "t ∈ reach v_TS" using beh len Suc
by (metis beh_in_reach less_imp_diff_less nth_mem)+
hence invs: "t' ∈ Vinv1" "t' ∈ Vinv3" "t ∈ Vinv2" "t ∈ Vinv3"
by(blast dest: Vinv1_invariant[THEN subsetD] Vinv2_invariant[THEN subsetD]
Vinv3_invariant[THEN subsetD])+
hence locked_v: "v ∈ locked t'" using Suc
by(auto simp add: t'_def intro: ranI)
have "i - j = Suc (i - (Suc j))" using False
by simp
hence trans: "(t', t) ∈ trans v_TS" using beh len Suc
by(auto simp add: t'_def intro!: beh_consecutive_in_trans)
― ‹Thus @{term v} also remains locked in @{term t}, and @{term p} does not
revoke, nor change its decision.›
hence locked_v_t: "v ∈ locked t" using locked_v
intro: locked_preserved[OF invs(1), THEN subsetD, OF _ _ locked_v])
from trans obtain w where "decisions t p = Some w" using dec_j
by(fastforce simp add: t'_def v_TS_defs v_round_def
split: option.split option.split_asm)
thus ?thesis using invs(4)[THEN Vinv3D] locked_v_t locked_unique[OF invs(3)]
by (metis contra_subsetD ranI)
qed(auto)
next
case 0
thus "decisions t p = Some v" using assms
by auto
qed
qed

text ‹Finally, we prove that the Voting model ensures agreement. Without a loss
of generality, we assume that ‹t› preceeds ‹s› in the trace.›
lemma Voting_agreement:
assumes beh: "tr ∈ beh v_TS"
and len: "i < length tr"
and s: "s = nth tr i"
and t: "t = nth tr (i - j)"
and dec:
"decisions s p = Some v"
"decisions t q = Some w"
shows "w = v"
proof-
― ‹Again, we first prove that the invariants hold for @{term s}.›
have reach: "s ∈ reach v_TS" using beh s t len
by (metis nth_mem)
hence invs2: "s ∈ Vinv2" and invs3: "s ∈ Vinv3"
by(blast dest: Vinv2_invariant[THEN subsetD] Vinv3_invariant[THEN subsetD])+

― ‹We now proceed to prove the thesis by induction.›
thus ?thesis using assms
proof(induction j arbitrary: t)
case 0
hence
"v ∈ locked (tr ! i)"
"w ∈ locked (tr ! i)"
by(auto intro: ranI)
thus ?thesis using invs2 using assms 0
by(auto dest: locked_unique)
next
case (Suc j)
thus ?thesis
― ‹Again, the totality of @{term "(-)"} makes the claim trivial if @{term "i < j"}.›
proof(cases "i ≤ j")
case False
― ‹In the non-trivial case, the proof follows from the decision stability theorem
and the uniqueness of locked values.›
have dec_t: "decisions t p = Some v" using Suc
by(auto intro: stable_decision[OF beh len s ])
have "t ∈ reach v_TS" using beh len Suc
by (metis beh_in_reach less_imp_diff_less nth_mem)
hence invs: "t ∈ Vinv2" "t ∈ Vinv3"
by(blast dest: Vinv2_invariant[THEN subsetD] Vinv3_invariant[THEN subsetD])+
from dec_t have "v ∈ locked t" using invs(2)
by(auto intro: ranI)
moreover have locked_w_t: "w ∈ locked t" using Suc ‹t ∈ Vinv3›[THEN Vinv3D]
by(auto intro: ranI)
ultimately show ?thesis using locked_unique[OF ‹t ∈ Vinv2›]
by blast
qed(auto)
qed
qed

end (* context quorum *)

end
```