Theory Stellar_Quorums

text 
‹This theory formalizes some of the results appearing in the paper "Stellar Consensus By Reduction"cite‹"disc_paper"›.
We prove static properties of personal Byzantine quorum systems and Stellar quorum systems.›

theory Stellar_Quorums
  imports Main 
begin

section "Personal Byzantine quorum systems"

locale personal_quorums =
  fixes quorum_of :: "'node ⇒ 'node set ⇒ bool" 
  assumes quorum_assm:"⋀ p p' . ⟦quorum_of p Q; p' ∈ Q⟧ ⟹ quorum_of p' Q"
    ― ‹In other words, a quorum (of some participant) is a quorum of all its members.›
begin

definition blocks where
  ― ‹Set @{term R} blocks participant @{term p}.›
  "blocks R p ≡ ∀ Q . quorum_of p Q ⟶ Q ∩ R ≠ {}"

abbreviation blocked_by where "blocked_by R ≡ {p . blocks R p}"

lemma blocked_blocked_subset_blocked:
  "blocked_by (blocked_by R) ⊆ blocked_by R"
proof -
  have False if "p ∈ blocked_by (blocked_by R)" and "p ∉ blocked_by R" for p
  proof -
    have "Q ∩ blocked_by R ≠ {}" if "quorum_of p Q" for Q
      using ‹p ∈ blocked_by (blocked_by R)› that unfolding blocks_def by auto
    have "Q ∩ R ≠ {}" if " quorum_of p Q" for Q
    proof -
      obtain p' where "p' ∈ blocked_by R" and "p' ∈ Q"
        by (meson Int_emptyI ‹⋀Q. quorum_of p Q ⟹ Q ∩ blocked_by R ≠ {}› ‹quorum_of p Q›)
      hence "quorum_of p' Q"
        using quorum_assm that by blast
      with ‹p' ∈ blocked_by R› show "Q ∩ R ≠ {}"
        using blocks_def by auto
    qed
    hence "p ∈ blocked_by R" by (simp add: blocks_def)
    thus False using that(2) by auto
  qed
  thus "blocked_by (blocked_by R) ⊆ blocked_by R"
    by blast
qed

end

text ‹We now add the set of correct participants to the model.›

locale with_w = personal_quorums quorum_of for quorum_of  :: "'node ⇒ 'node set ⇒ bool" +
  fixes W::"'node set" ― ‹@{term W} is the set of correct participants›
begin

abbreviation B where "B ≡ -W"
  ― ‹@{term B} is the set of malicious participants.›

definition quorum_of_set where "quorum_of_set S Q ≡ ∃ p ∈ S . quorum_of p Q"

subsection "The set of participants not blocked by malicious participants"

definition L where "L ≡ W - (blocked_by B)"

lemma l2: "p ∈ L ⟹ ∃ Q  ⊆ W. quorum_of p Q" 
  unfolding L_def blocks_def using DiffD2 by auto
 
lemma l3: ―  ‹If a participant is not blocked by the malicious participants, then it has a quorum consisting exclusively of correct 
participants which are not blocked by the malicious participants.›
  assumes "p ∈ L" shows "∃ Q ⊆ L . quorum_of p Q"
proof -
  have False if "⋀ Q . quorum_of p Q ⟹ Q ∩ (-L) ≠ {}"
  proof -
    obtain Q where "quorum_of p Q" and "Q ⊆ W" 
      using l2 ‹p ∈ L› by auto 
    have "Q ∩ (-L) ≠ {}"  using that ‹quorum_of p Q› by simp
    obtain p' where "p' ∈ Q ∩ (-L)" and "quorum_of p' Q"
      using ‹Q ∩ - L ≠ {}› ‹quorum_of p Q› inf.left_idem quorum_assm by fastforce 
    hence "Q ∩ B ≠ {}" unfolding L_def
      using CollectD Compl_Diff_eq Int_iff inf_le1 personal_quorums.blocks_def personal_quorums_axioms subset_empty by fastforce
    thus False using ‹Q ⊆ W› by auto  
  qed 
  thus ?thesis by (metis disjoint_eq_subset_Compl double_complement)
qed

subsection "Consensus clusters and intact sets"

definition is_intertwined where
  ― ‹This definition is not used in this theory,
    but we include it to formalize the notion of intertwined set appearing in the DISC paper.›
  "is_intertwined S ≡ S ⊆ W 
    ∧ (∀ Q Q' . quorum_of_set S Q ∧ quorum_of_set S Q' ⟶ W ∩ Q ∩ Q' ≠ {})"

definition is_cons_cluster where
  ― ‹Consensus clusters›
  "is_cons_cluster C ≡ C ⊆ W ∧ (∀ p ∈ C . ∃ Q ⊆ C . quorum_of p Q)
      ∧ (∀ Q Q' . quorum_of_set C Q ∧ quorum_of_set C Q' ⟶ W ∩ Q ∩ Q' ≠ {})"

definition strong_consensus_cluster where
  "strong_consensus_cluster I ≡ I ⊆ W ∧ (∀ p ∈ I . ∃ Q ⊆ I . quorum_of p Q)
      ∧ (∀ Q Q' . quorum_of_set I Q ∧ quorum_of_set I Q' ⟶ I ∩ Q ∩ Q' ≠ {})"

lemma strong_consensus_cluster_imp_cons_cluster:
― ‹Every intact set is a consensus cluster›
  shows "strong_consensus_cluster I ⟹ is_cons_cluster I" 
  unfolding strong_consensus_cluster_def is_cons_cluster_def
  by blast 

lemma cons_cluster_neq_cons_cluster:
  ― ‹Some consensus clusters are not strong consensus clusters and have no superset that is a strong consensus cluster.›
  shows "is_cons_cluster I ∧ (∀ J . I ⊆ J ⟶ ¬strong_consensus_cluster J)" nitpick[falsify=false, card 'node=3, expect=genuine]
  oops

text ‹Next we show that the union of two consensus clusters that intersect is a consensus cluster.›

theorem cluster_union:
  assumes "is_cons_cluster C1" and "is_cons_cluster C2" and "C1 ∩ C2 ≠ {}"
  shows "is_cons_cluster (C1∪ C2)"
proof -
  have "C1 ∪ C2 ⊆ W"
    using assms(1) assms(2) is_cons_cluster_def by auto 
  moreover
  have "∀ p ∈ (C1∪C2) . ∃ Q ⊆ (C1∪C2) . quorum_of p Q" 
    using ‹is_cons_cluster C1› ‹is_cons_cluster C2› unfolding is_cons_cluster_def
    by (meson UnE le_supI1 le_supI2)
  moreover
  have "W ∩ Q1 ∩ Q2 ≠ {}"
    if "quorum_of_set (C1∪C2) Q1" and "quorum_of_set (C1∪C2) Q2" 
    for Q1 Q2
  proof -
    have "W ∩ Q1 ∩ Q2 ≠ {}" if "quorum_of_set C Q1" and "quorum_of_set C Q2" and "C = C1 ∨ C = C2" for C
      using ‹is_cons_cluster C1› ‹is_cons_cluster C2› ‹quorum_of_set (C1∪C2) Q1› ‹quorum_of_set (C1∪C2) Q2› that
      unfolding quorum_of_set_def is_cons_cluster_def by metis
    moreover
    have ‹W ∩ Q1 ∩ Q2 ≠ {}›  if "is_cons_cluster C1" and "is_cons_cluster C2"
      and "C1 ∩ C2 ≠ {}" and "quorum_of_set C1 Q1" and "quorum_of_set C2 Q2"
    for C1 C2 ― ‹We generalize to avoid repeating the argument twice›
    proof -
      obtain p Q where "quorum_of p Q" and "p ∈ C1 ∩ C2" and "Q ⊆ C2" 
        using ‹C1 ∩ C2 ≠ {}› ‹is_cons_cluster C2› unfolding is_cons_cluster_def by blast
      have "Q ∩ Q1 ≠ {}" using ‹is_cons_cluster C1› ‹quorum_of_set C1 Q1› ‹quorum_of p Q› ‹p ∈ C1 ∩ C2›
        unfolding is_cons_cluster_def quorum_of_set_def
        by (metis Int_assoc Int_iff inf_bot_right)
      hence "quorum_of_set C2 Q1"  using ‹Q ⊆ C2› ‹quorum_of_set C1 Q1› quorum_assm unfolding quorum_of_set_def by blast 
      thus "W ∩ Q1 ∩ Q2 ≠ {}" using ‹is_cons_cluster C2› ‹quorum_of_set C2 Q2›
        unfolding is_cons_cluster_def by blast
    qed
    ultimately show ?thesis using assms that unfolding quorum_of_set_def by auto 
  qed
  ultimately show ?thesis using assms
    unfolding is_cons_cluster_def by simp
qed

text ‹Similarly, the union of two strong consensus clusters is a strong consensus cluster.›
lemma strong_cluster_union:
  assumes "strong_consensus_cluster C1" and "strong_consensus_cluster C2" and "C1 ∩ C2 ≠ {}"
  shows "strong_consensus_cluster (C1∪ C2)"
proof -
  have "C1 ∪ C2 ⊆ W"
    using assms(1) assms(2) strong_consensus_cluster_def by auto 
  moreover
  have "∀ p ∈ (C1∪C2) . ∃ Q ⊆ (C1∪C2) . quorum_of p Q" 
    using ‹strong_consensus_cluster C1› ‹strong_consensus_cluster C2› unfolding strong_consensus_cluster_def
    by (meson UnE le_supI1 le_supI2)
  moreover
  have "(C1∪C2) ∩ Q1 ∩ Q2 ≠ {}"
    if "quorum_of_set (C1∪C2) Q1" and "quorum_of_set (C1∪C2) Q2" 
    for Q1 Q2
  proof -
    have "C ∩ Q1 ∩ Q2 ≠ {}" if "quorum_of_set C Q1" and "quorum_of_set C Q2" and "C = C1 ∨ C = C2" for C
      using ‹strong_consensus_cluster C1› ‹strong_consensus_cluster C2› that
      unfolding quorum_of_set_def strong_consensus_cluster_def by metis
    hence "(C1∪C2) ∩ Q1 ∩ Q2 ≠ {}" if "quorum_of_set C Q1" and "quorum_of_set C Q2" and "C = C1 ∨ C = C2" for C
      by (metis Int_Un_distrib2 disjoint_eq_subset_Compl sup.boundedE that)
    moreover
    have ‹(C1∪C2) ∩ Q1 ∩ Q2 ≠ {}›  if "strong_consensus_cluster C1" and "strong_consensus_cluster C2"
      and "C1 ∩ C2 ≠ {}" and "quorum_of_set C1 Q1" and "quorum_of_set C2 Q2"
    for C1 C2 ― ‹We generalize to avoid repeating the argument twice›
    proof -
      obtain p Q where "quorum_of p Q" and "p ∈ C1 ∩ C2" and "Q ⊆ C2" 
        using ‹C1 ∩ C2 ≠ {}› ‹strong_consensus_cluster C2› unfolding strong_consensus_cluster_def by blast
      have "Q ∩ Q1 ≠ {}" using ‹strong_consensus_cluster C1› ‹quorum_of_set C1 Q1› ‹quorum_of p Q› ‹p ∈ C1 ∩ C2›
        unfolding strong_consensus_cluster_def quorum_of_set_def
        by (metis Int_assoc Int_iff inf_bot_right)
      hence "quorum_of_set C2 Q1"  using ‹Q ⊆ C2› ‹quorum_of_set C1 Q1› quorum_assm unfolding quorum_of_set_def by blast 
      thus "(C1∪C2) ∩ Q1 ∩ Q2 ≠ {}" using ‹strong_consensus_cluster C2› ‹quorum_of_set C2 Q2›
        unfolding strong_consensus_cluster_def by blast
    qed
    ultimately show ?thesis using assms that unfolding quorum_of_set_def by auto 
  qed
  ultimately show ?thesis using assms
    unfolding strong_consensus_cluster_def by simp
qed

end

section "Stellar quorum systems"

locale stellar =
  fixes slices :: "'node ⇒ 'node set set" ― ‹the quorum slices›
    and W :: "'node set" ― ‹the well-behaved nodes›
  assumes slices_ne:"⋀p . p ∈ W ⟹ slices p ≠ {}"
begin

definition quorum where
  "quorum Q ≡ ∀ p ∈ Q ∩ W . (∃ Sl ∈ slices p . Sl ⊆ Q)"

definition quorum_of where "quorum_of p Q ≡ quorum Q ∧ (p ∉ W ∨ (∃ Sl ∈ slices p . Sl ⊆ Q))"
  ― ‹TODO: @{term "p∉W"} needed?›

lemma quorum_union:"quorum Q ⟹ quorum Q' ⟹ quorum (Q ∪ Q')"
  unfolding quorum_def
  by (metis IntE Int_iff UnE inf_sup_aci(1) sup.coboundedI1 sup.coboundedI2)

lemma l1:
  assumes "⋀ p . p ∈ S ⟹ ∃ Q ⊆ S . quorum_of p Q" and "p∈ S"
  shows "quorum_of p S" using assms unfolding quorum_of_def quorum_def
  by (meson Int_iff subset_trans)

lemma is_pbqs:
  assumes "quorum_of p Q" and "p' ∈ Q"
  shows "quorum_of p' Q" 
  ― ‹This is the property required of a PBQS.›
  using assms
  by (simp add: quorum_def quorum_of_def)

interpretation with_w quorum_of 
  ― ‹Stellar quorums form a personal quorum system.›
  unfolding with_w_def personal_quorums_def 
  quorum_def quorum_of_def by simp

lemma quorum_is_quorum_of_some_slice:
  assumes "quorum_of p Q" and "p ∈ W"
  obtains S where "S ∈ slices p" and "S ⊆ Q"
    and "⋀ p' . p' ∈ S ∩ W ⟹ quorum_of p' Q"
  using assms unfolding quorum_def quorum_of_def by fastforce

lemma "is_cons_cluster C ⟹ quorum C" 
  ― ‹Every consensus cluster is a quorum.›
  unfolding is_cons_cluster_def
  by (metis inf.order_iff l1 quorum_of_def stellar.quorum_def stellar_axioms) 

subsection ‹Properties of blocking sets›

inductive blocking_min where
  ― ‹This is the set of correct participants that are eventually blocked by a set @{term R} when byzantine processors do not take steps.›
  "⟦p ∈ W; ∀ Sl ∈ slices p . ∃ q ∈ Sl∩W . q ∈ R ∨ blocking_min R q⟧ ⟹ blocking_min R p"
inductive_cases blocking_min_elim:"blocking_min R p"

inductive blocking_max where
  ― ‹This is the set of participants that are eventually blocked by a set @{term R} when byzantine processors help epidemic propagation.›
  "⟦p ∈ W; ∀ Sl ∈ slices p . ∃ q ∈ Sl . q ∈ R∪B ∨ blocking_max R q⟧ ⟹ blocking_max R p"
inductive_cases "blocking_max R p"

text ‹Next we show that if @{term ‹R›} blocks @{term ‹p›} and @{term p} belongs to a consensus cluster @{term S}, then @{term ‹R ∩ S ≠ {}›}.›

text ‹We first prove two auxiliary lemmas:›

lemma cons_cluster_wb:"p ∈ C ⟹ is_cons_cluster C ⟹ p∈W"
  using is_cons_cluster_def  by fastforce 

lemma cons_cluster_has_ne_slices:
  assumes "is_cons_cluster C" and "p∈C"
    and "Sl ∈ slices p" 
  shows "Sl ≠ {}"
  using assms unfolding is_cons_cluster_def quorum_of_set_def quorum_of_def quorum_def
  by (metis empty_iff inf_bot_left inf_bot_right subset_refl)

lemma cons_cluster_has_cons_cluster_slice:
  assumes "is_cons_cluster C" and "p∈C"
  obtains Sl where "Sl ∈ slices p" and "Sl ⊆ C"
  using assms unfolding is_cons_cluster_def quorum_of_set_def quorum_of_def quorum_def
  by (metis Int_commute  empty_iff inf.order_iff  inf_bot_right le_infI1)

theorem blocking_max_intersects_intact:
  ― ‹if @{term ‹R›} blocks @{term ‹p›} when malicious participants help epidemic propagation, 
and @{term p} belongs to a consensus cluster @{term C}, then @{term ‹R ∩ C ≠ {}›}›
  assumes  "blocking_max R p" and "is_cons_cluster C" and "p ∈ C"
  shows "R ∩ C ≠ {}" using assms
proof (induct)
  case (1 p R)
  obtain Sl where "Sl ∈ slices p" and "Sl ⊆ C" using cons_cluster_has_cons_cluster_slice
    using "1.prems" by blast
  moreover have "Sl ⊆ W" using assms(2) calculation(2) is_cons_cluster_def by auto 
  ultimately show ?case
    using "1.hyps" assms(2) by fastforce
qed

text ‹Now we show that if @{term ‹p ∈ C›}, @{term C} is a consensus cluster, and quorum @{term Q} is such that @{term ‹Q ∩ C ≠ {}›},
    then @{term ‹Q ∩ W›} blocks @{term p}. 

We start by defining the set of participants reachable from a participant through correct participants.
Their union trivially forms a quorum. 
Moreover, if @{term p} is not blocked by a set @{term R}, 
then we show that the set of participants reachable from @{term p} and not blocked by @{term R} forms a quorum disjoint from @{term R}.
It follows that if @{term p } is a member of a consensus cluster @{term C} and @{term Q} is a quorum of a member of @{term C}, then @{term "Q∩W"}
 must block @{term p}, as otherwise quorum intersection would be violated. ›

inductive not_blocked for p R where
  "⟦Sl ∈ slices p; ∀ q ∈ Sl∩W . q ∉ R ∧ ¬blocking_min R q; q ∈ Sl⟧ ⟹ not_blocked p R q"
| "⟦not_blocked p R p'; p' ∈ W; Sl ∈ slices p'; ∀ q ∈ Sl∩W . q ∉ R ∧ ¬blocking_min R q; q ∈ Sl⟧ ⟹ not_blocked p R q"
inductive_cases not_blocked_cases:"not_blocked p R q"

lemma l4:
  fixes Q p R
  defines "Q ≡ {q . not_blocked p R q}"
  shows "quorum Q"
proof -
  have "∃ S ∈ slices n . S ⊆ Q" if "n∈Q∩W" for n
  proof-
    have "not_blocked p R n" using assms that by blast
    hence "n ∉ R" and "¬blocking_min R n" by (metis Int_iff not_blocked.simps that)+
    thus ?thesis  using blocking_min.intros not_blocked.intros(2) that unfolding Q_def 
      by (simp; metis mem_Collect_eq subsetI)
  qed
  thus ?thesis by (simp add: quorum_def)
qed


lemma l5:
  fixes Q p R
  defines "Q ≡ {q . not_blocked p R q}"
  assumes  "¬blocking_min R p" and ‹p∈C› and ‹is_cons_cluster C›
  shows "quorum_of p Q" 
proof -
  have "p∈W"
    using assms(3,4) cons_cluster_wb by blast 
  obtain Sl where "Sl ∈ slices p" and "∀ q ∈ Sl∩W . q ∉ R ∧ ¬blocking_min R q"
    by (meson ‹p ∈ W› assms(2) blocking_min.intros)
  hence "Sl ⊆ Q" unfolding Q_def using not_blocked.intros(1) by blast
  with l4 ‹Sl ∈ slices p› show "quorum_of p Q"
    using Q_def  quorum_of_def by blast
qed

lemma cons_cluster_ne_slices:
  assumes "is_cons_cluster C" and "p∈C" and "Sl ∈ slices p"
  shows "Sl≠{}"
  using assms cons_cluster_has_ne_slices cons_cluster_wb stellar.quorum_of_def stellar_axioms by fastforce

lemma l6:
  fixes Q p R
  defines "Q ≡ {q . not_blocked p R q}"
  shows "Q ∩ R ∩ W = {}"
proof -
  have "q ∉ R" if "not_blocked p R q" and "q∈ W" for q using that
    by (metis Int_iff not_blocked.simps)
  thus ?thesis unfolding Q_def by auto
qed

theorem quorum_blocks_cons_cluster:
  assumes "quorum_of_set C Q" and "p∈C" and "is_cons_cluster C"
  shows "blocking_min (Q ∩ W) p"
proof (rule ccontr) 
  assume "¬ blocking_min (Q ∩ W) p"
  have "p∈W" using assms(2,3) is_cons_cluster_def by auto 
  define Q' where "Q' ≡ {q . not_blocked p (Q∩W) q}"
  have "quorum_of p Q'" using Q'_def ‹¬ blocking_min (Q ∩ W) p› assms(2) assms(3) l5(1) by blast
  moreover have "Q' ∩ Q ∩ W = {}"
    using Q'_def l6 by fastforce
  ultimately show False using assms unfolding is_cons_cluster_def
    by (metis Int_commute inf_sup_aci(2) quorum_of_set_def) 
qed

subsection ‹Reachability through a set›

text ‹Here we define the part of a quorum @{term Q} of @{term p} that is reachable through correct
participants from @{term p}. We show that if @{term p} and @{term p'} are members of the same consensus cluster and @{term Q} is a quorum of @{term p}
 and @{term Q'} is a quorum of @{term p'},
then the intersection @{term "Q∩Q'∩W"} is reachable from both @{term p} and @{term p'} through the consensus cluster.›

inductive reachable_through for p S where
  "reachable_through p S p"
| "⟦reachable_through p S p'; p' ∈ W; Sl ∈ slices p'; Sl ⊆ S; p'' ∈ Sl⟧ ⟹ reachable_through p S p''"

definition truncation where "truncation p S ≡ {p' . reachable_through p S p'}"

lemma l13:
  assumes "quorum_of p Q" and "p ∈ W" and "reachable_through p Q p'"
  shows "quorum_of p' Q"
  using assms using quorum_assm reachable_through.cases
  by (metis is_pbqs subset_iff)

lemma l14:
  assumes "quorum_of p Q" and "p ∈ W"
  shows "quorum (truncation p Q)"
proof -
  have "∃ S ∈ slices p' . ∀ q ∈ S . reachable_through p Q q" if "reachable_through p Q p'" and "p' ∈ W" for p'
    by (meson assms l13 quorum_is_quorum_of_some_slice stellar.reachable_through.intros(2) stellar_axioms that)
  thus ?thesis
    by (metis IntE mem_Collect_eq stellar.quorum_def stellar_axioms subsetI truncation_def)  
qed

lemma l15:
  assumes "is_cons_cluster I" and "quorum_of p Q" and "quorum_of p' Q'" and "p ∈ I" and "p' ∈ I" and "Q ∩ Q' ∩ W ≠ {}"
  shows "W ∩ (truncation p Q) ∩ (truncation p' Q') ≠ {}" 
proof -
  have "quorum (truncation p Q)" and "quorum (truncation p' Q')" using l14 assms is_cons_cluster_def by auto
  moreover have "quorum_of_set I (truncation p Q)" and "quorum_of_set I (truncation p' Q')"
    by (metis IntI assms(4,5) calculation mem_Collect_eq quorum_def quorum_of_def quorum_of_set_def reachable_through.intros(1) truncation_def)+
  moreover note ‹is_cons_cluster I›
  ultimately show ?thesis unfolding is_cons_cluster_def by auto
qed

end

subsection "Elementary quorums"

text ‹In this section we define the notion of elementary quorum, which is a quorum that has no strict subset that is a quorum.
  It follows directly from the definition that every finite quorum contains an elementary quorum. Moreover, we show 
that if @{term Q} is an elementary quorum and @{term n1} and @{term n2} are members of @{term Q}, then @{term n2} is reachable from @{term n1} 
in the directed graph over participants defined as the set of edges @{term "(n,m)"} such that @{term m} is a member of a slice of @{term n}.
This lemma is used in the companion paper to show that probabilistic leader-election is feasible.›

locale elementary = stellar
begin 

definition elementary where
  "elementary s ≡ quorum s ∧ (∀ s' . s' ⊂ s ⟶ ¬quorum s')"

lemma finite_subset_wf:
  shows "wf {(X, Y). X ⊂ Y ∧ finite Y}"
  by (metis finite_psubset_def wf_finite_psubset)

lemma quorum_contains_elementary:
  assumes "finite s" and  "¬ elementary s" and "quorum s" 
  shows "∃ s' . s' ⊂ s ∧ elementary s'" using assms
proof (induct s rule:wf_induct[where ?r="{(X, Y). X ⊂ Y ∧ finite Y}"])
  case 1
  then show ?case using finite_subset_wf by simp
next
  case (2 x)
  then show ?case
    by (metis (full_types) elementary_def finite_psubset_def finite_subset in_finite_psubset less_le psubset_trans)
qed

inductive path where
  "path []"
| "⋀ x . path [x]"
| "⋀ l n . ⟦path l; S ∈ Q (hd l); n ∈ S⟧ ⟹ path (n#l)"

theorem elementary_connected:
  assumes "elementary s" and "n1 ∈ s" and "n2 ∈ s" and "n1 ∈ W" and "n2 ∈ W"
  shows "∃ l . hd (rev l) = n1 ∧ hd l = n2 ∧ path l" (is ?P)
proof -
  { assume "¬?P"
    define x where "x ≡ {n ∈ s . ∃ l . l ≠ [] ∧ hd (rev l) = n1 ∧ hd l = n ∧ path l}"
    have "n2 ∉ x" using ‹¬?P› x_def by auto 
    have "n1 ∈ x" unfolding x_def using assms(2) path.intros(2) by force
    have "quorum x"
    proof -
      { fix n
        assume "n ∈ x"
        have "∃ S . S ∈ slices n ∧ S ⊆ x"
        proof -
          obtain S where "S ∈ slices n" and "S ⊆ s" using ‹elementary s› ‹n ∈ x› unfolding x_def
            by (force simp add:elementary_def quorum_def)
          have "S ⊆ x"
          proof -
            { assume "¬ S ⊆ x"
              obtain m where "m ∈ S" and "m ∉ x" using ‹¬ S ⊆ x› by auto
              obtain l' where "hd (rev l') = n1" and "hd l' = n" and "path l'" and "l' ≠ []"
                using ‹n ∈ x› x_def by blast 
              have "path (m # l')" using ‹path l'› ‹m∈ S› ‹S ∈ slices n› ‹hd l' = n›
                using path.intros(3) by fastforce
              moreover have "hd (rev (m # l')) = n1" using ‹hd (rev l') = n1› ‹l' ≠ []› by auto
              ultimately have "m ∈ x" using ‹m ∈ S› ‹S ⊆ s› x_def by auto 
              hence False using ‹m ∉ x› by blast }
            thus ?thesis by blast
          qed
          thus ?thesis
            using ‹S ∈ slices n› by blast
        qed }
      thus ?thesis by (meson Int_iff quorum_def)
    qed 
    moreover have "x ⊂ s"
      using ‹n2 ∉ x› assms(3) x_def by blast
    ultimately have False using ‹elementary s›
      using elementary_def by auto
  }
  thus ?P by blast  
qed


end

subsection ‹The intact sets of the Stellar Whitepaper›

definition project where 
  "project slices S n ≡ {Sl ∩ S | Sl . Sl ∈ slices n}" 
  ― ‹Projecting on @{term S} is the same as deleting the complement of @{term S}, where deleting is understood as in the Stellar Whitepaper.›

subsubsection ‹Intact and the Cascade Theorem›

locale intact = ― ‹Here we fix an intact set @{term I} and prove the cascade theorem.›
  orig:stellar slices W 
  + proj:stellar "project slices I" W ― ‹We consider the projection of the system on @{term I}.›
  for slices W I +  ― ‹An intact set is a set @{term I} satisfying the three assumptions below:›
  assumes intact_wb:"I ⊆ W"
    and q_avail:"orig.quorum I" ― ‹@{term I} is a quorum in the original system.›
    and q_inter:"⋀ Q Q' . ⟦proj.quorum Q; proj.quorum Q'; Q ∩ I ≠ {}; Q' ∩ I ≠ {}⟧  ⟹ Q ∩ Q' ∩ I ≠ {}" 
    ― ‹Any two sets that intersect @{term I} and that are quorums in the projected system intersect in @{term I}.
Note that requiring that @{text ‹Q ∩ Q' ≠ {}›} instead of @{text ‹Q ∩ Q' ∩ I ≠ {}›} would be equivalent.›
begin

theorem blocking_safe: ― ‹A set that blocks an intact node contains an intact node. 
If this were not the case, quorum availability would trivially be violated.›
  fixes S n
  assumes "n∈I" and "∀ Sl∈ slices n .Sl∩S ≠ {}"
  shows "S ∩ I ≠ {}"
  using assms q_avail intact_wb unfolding orig.quorum_def 
  by auto (metis inf.absorb_iff2 inf_assoc inf_bot_right inf_sup_aci(1)) 

theorem cascade:
― ‹If @{term U} is a quorum of an intact node and @{term S} is a super-set of @{term U}, then either @{term S} includes 
all intact nodes or there is an intact node outside of @{term S} which is blocked by the intact members of @{term S}.
This shows that, in SCP, once the intact members of a quorum accept a statement, 
a cascading effect occurs and all intact nodes eventually accept it regardless of what befouled and faulty nodes do.›
  fixes U S
  assumes "orig.quorum U" and "U ∩ I ≠ {}" and "U ⊆ S"
  obtains "I ⊆ S" | "∃ n ∈ I - S . ∀ Sl ∈ slices n . Sl ∩ S ∩ I ≠ {}"
proof -
  have False if 1:"∀ n ∈ I - S . ∃ Sl ∈ slices n . Sl ∩ S ∩ I = {}" and 2:"¬(I ⊆ S)"
  proof -
    text ‹First we show that @{term ‹I-S›} is a quorum in the projected system. This is immediate from the definition of quorum and assumption 1.›
    have "proj.quorum (I-S)" using 1
      by (simp add: proj.quorum_def project_def) (metis DiffI IntE IntI empty_iff subsetI)
    text ‹Then we show that U is also a quorum in the projected system:›
    moreover have "proj.quorum U" using ‹orig.quorum U› 
      unfolding proj.quorum_def orig.quorum_def project_def 
      by (simp; meson Int_commute inf.coboundedI2)
    text ‹Since quorums of @{term I} must intersect, we get a contradiction:›
    ultimately show False using ‹U ⊆ S› ‹U ∩ I ≠ {}› ‹¬(I⊆S)› q_inter by auto
  qed
  thus ?thesis using that by blast
qed

end

subsubsection "The Union Theorem"

text ‹Here we prove that the union of two intact sets that intersect is intact.
This implies that maximal intact sets are disjoint.›

locale intersecting_intact = 
  i1:intact slices W I1 + i2:intact slices W I2 ― ‹We fix two intersecting intact sets @{term I1} and @{term I2}.›
  + proj:stellar "project slices (I1∪I2)" W ― ‹We consider the projection of the system on @{term ‹I1∪I2›}.›
  for slices W I1 I2 +
assumes inter:"I1 ∩ I2 ≠ {}"
begin

theorem union_quorum: "i1.orig.quorum (I1∪I2)" ― ‹@{term ‹I1∪I2›} is a quorum in the original system.›
  using i1.intact_axioms i2.intact_axioms
  unfolding  intact_def stellar_def intact_axioms_def i1.orig.quorum_def
  by (metis Int_iff Un_iff le_supI1 le_supI2)

theorem union_quorum_intersection: 
  assumes "proj.quorum Q1" and "proj.quorum Q2" and "Q1 ∩ (I1∪I2) ≠ {}" and "Q2 ∩ (I1∪I2) ≠ {}"
  shows "Q1 ∩ Q2 ∩ (I1∪I2) ≠ {}"
    ― ‹Any two sets that intersect @{term ‹I1∪I2›} and that are quorums in the system projected on @{term ‹I1∪I2›} intersect in @{term ‹I1∪I2›}.›
proof -
  text ‹First we show that @{term Q1} and @{term Q2} are quorums in the projections on @{term I1} and @{term I2}.›
  have "i1.proj.quorum Q1" using ‹proj.quorum Q1› 
    unfolding i1.proj.quorum_def proj.quorum_def project_def
    by auto (metis Int_Un_distrib Int_iff Un_subset_iff) 
  moreover have "i2.proj.quorum Q2" using ‹proj.quorum Q2› 
    unfolding i2.proj.quorum_def proj.quorum_def project_def
    by auto (metis Int_Un_distrib Int_iff Un_subset_iff) 
  moreover have "i2.proj.quorum Q1" using ‹proj.quorum Q1›
    unfolding proj.quorum_def i2.proj.quorum_def project_def
    by auto (metis Int_Un_distrib Int_iff Un_subset_iff) 
  moreover have "i1.proj.quorum Q2" using ‹proj.quorum Q2›
    unfolding proj.quorum_def i1.proj.quorum_def project_def
    by auto (metis Int_Un_distrib Int_iff Un_subset_iff) 
  text ‹Next we show that @{term Q1} and @{term Q2} intersect if they are quorums of, respectively, @{term I1} and @{term I2}. 
This is the only interesting part of the proof.› 
  moreover have "Q1 ∩ Q2 ∩ (I1∪I2) ≠ {}" 
    if "i1.proj.quorum Q1" and "i2.proj.quorum Q2" and "i2.proj.quorum Q1"
      and "Q1 ∩ I1 ≠ {}" and "Q2 ∩ I2 ≠ {}"
    for Q1 Q2
  proof -
    have "i1.proj.quorum I2" 
    proof -
      have "i1.orig.quorum I2" by (simp add: i2.q_avail)
      thus ?thesis unfolding i1.orig.quorum_def i1.proj.quorum_def project_def
        by auto (meson Int_commute Int_iff inf_le2 subset_trans)
    qed
    moreover note ‹i1.proj.quorum Q1›
    ultimately have "Q1 ∩ I2 ≠ {}" using i1.q_inter inter ‹Q1 ∩ I1 ≠ {}› by blast

    moreover note ‹i2.proj.quorum Q2›  
    moreover note ‹i2.proj.quorum Q1›
    ultimately have "Q1 ∩ Q2 ∩ I2 ≠ {}" using i2.q_inter ‹Q2 ∩ I2 ≠ {}› by blast 
    thus ?thesis by (simp add: inf_sup_distrib1)
  qed
  text ‹Next  we show that @{term Q1} and @{term Q2} intersect if they are quorums of the same intact set. This is obvious.›
  moreover
  have "Q1 ∩ Q2 ∩ (I1∪I2) ≠ {}" 
    if "i1.proj.quorum Q1" and "i1.proj.quorum Q2" and "Q1 ∩ I1 ≠ {}" and "Q2 ∩ I1 ≠ {}"
    for Q1 Q2
    by (simp add: Int_Un_distrib i1.q_inter that)  
  moreover
  have "Q1 ∩ Q2 ∩ (I1∪I2) ≠ {}"
    if "i2.proj.quorum Q1" and "i2.proj.quorum Q2" and "Q1 ∩ I2 ≠ {}" and "Q2 ∩ I2 ≠ {}"
    for Q1 Q2
    by (simp add: Int_Un_distrib i2.q_inter that)
  text ‹Finally we have covered all the cases and get the final result:›
  ultimately
  show ?thesis
    by (smt (verit, best) Int_Un_distrib Int_commute assms(3) assms(4) sup_eq_bot_iff)
qed

end

end