Theory CT_Proofs

(*<*)
theory CT_Proofs
imports Three_Step_MRU "../HO_Transition_System" Heard_Of.Majorities "../Quorums" CT_Defs
begin
(*>*)

subsection ‹Proofs›
type_synonym ct_TS_state = "(nat × (process ⇒ (val pstate)))"

definition CT_TS ::
  "(round ⇒ process HO)
  ⇒ (round ⇒ process HO)
  ⇒ (round ⇒ process ⇒ process)
  ⇒ ct_TS_state TS"
where
  "CT_TS HOs SHOs crds = CHO_to_TS CT_Alg HOs SHOs crds"

lemmas CT_TS_defs = CT_TS_def CHO_to_TS_def CT_Alg_def CHOinitConfig_def
  CT_initState_def

definition CT_trans_step where
  "CT_trans_step HOs SHOs crds nxt_f snd_f stp ≡ ⋃r μ.
    {((r, cfg), (Suc r, cfg'))|cfg cfg'. three_step r = stp  ∧ (∀p.
      μ p ∈ get_msgs (snd_f r) cfg (HOs r) (SHOs r) p
      ∧ nxt_f r p (cfg p) (μ p) (crds r p) (cfg' p)
    )}"

lemma three_step_less_D:
  "0 < three_step r ⟹ three_step r = 1 ∨ three_step r = 2"
  by(unfold three_step_def, arith)

lemma CT_trans:
  "CSHO_trans_alt CT_sendMsg CT_nextState HOs SHOs crds = 
  CT_trans_step HOs SHOs crds next0 send0 0
  ∪ CT_trans_step HOs SHOs crds next1 send1 1
  ∪ CT_trans_step HOs SHOs crds next2 send2 2
  "
proof(rule equalityI)
  show "CSHO_trans_alt CT_sendMsg CT_nextState HOs SHOs crds
    ⊆ CT_trans_step HOs SHOs crds next0 send0 0 ∪
       CT_trans_step HOs SHOs crds next1 send1 1 ∪
       CT_trans_step HOs SHOs crds next2 send2 2"
  by(force simp add: CSHO_trans_alt_def CT_sendMsg_def CT_nextState_def 
    CT_trans_step_def K_def dest!: three_step_less_D)
next
  show "CT_trans_step HOs SHOs crds next0 send0 0 ∪
    CT_trans_step HOs SHOs crds next1 send1 1 ∪
    CT_trans_step HOs SHOs crds next2 send2 2
    ⊆ CSHO_trans_alt CT_sendMsg CT_nextState HOs SHOs crds"
  by(force simp add: CSHO_trans_alt_def CT_sendMsg_def CT_nextState_def 
    CT_trans_step_def K_def)
qed

type_synonym rHO = "nat ⇒ process HO"

subsubsection ‹Refinement›
(******************************************************************************)

definition ct_ref_rel :: "(three_step_mru_state × ct_TS_state)set" where
  "ct_ref_rel = {(sa, (r, sc)).
    opt_mru_state.next_round sa = r
    ∧ opt_mru_state.decisions sa = pstate.decide o sc
    ∧ opt_mru_state.mru_vote sa = pstate.mru_vote o sc
    ∧ (three_step r = Suc 0 ⟶ three_step_mru_state.candidates sa = {commt (sc (coord r))})
  }"

text ‹Now we need to use the fact that SHOs = HOs (i.e. the setting is non-Byzantine), and
  also the fact that the coordinator receives enough messages in each round›

lemma mru_vote_evolution0:
  "∀p. next0 r p (s p) (msgs p) (crd p) (s' p) ⟹ mru_vote o s' = mru_vote o s"
  apply(rule_tac[!] ext, rename_tac x, erule_tac[!] x=x in allE)
  by(auto simp add: next0_def next2_def Let_def)

lemma mru_vote_evolution2:
  "∀p. next2 r p (s p) (msgs p) (crd p) (s' p) ⟹ mru_vote o s' = mru_vote o s"
  apply(rule_tac[!] ext, rename_tac x, erule_tac[!] x=x in allE)
  by(auto simp add: next0_def next2_def Let_def)

lemma decide_evolution:
  "∀p. next0 r p (s p) (msgs p) (crd p) (s' p) ⟹ decide o s = decide o s'"
  "∀p. next1 r p (s p) (msgs p) (crd p) (s' p) ⟹ decide o s = decide o s'"
  apply(rule_tac[!] ext, rename_tac x, erule_tac[!] x=x in allE)
  by(auto simp add: next0_def next1_def Let_def)

lemma msgs_mru_vote: 
  assumes
  "μ (coord r) ∈ get_msgs (send0 r) cfg (HOs r) (HOs r) (coord r)" (is "μ ?p ∈ _")
  shows "((msgs_to_lvs (μ ?p)) |` HOs r ?p) = (mru_vote o cfg) |` HOs r ?p" using assms
  by(auto simp add: get_msgs_benign send0_def restrict_map_def msgs_to_lvs_def
      mru_vote_to_msg_def map_comp_def intro!: ext split: option.split)

context
  fixes
    HOs :: "nat ⇒ process ⇒ process set"
    and crds :: "nat ⇒ process ⇒process"
  assumes
    per_rd: "∀r. CT_commPerRd r (HOs r) (crds r)"
begin

lemma step0_ref:
  "{ct_ref_rel} 
    (⋃r C. majorities.opt_mru_step0 r C), 
    CT_trans_step HOs HOs crds next0 send0 0 {> ct_ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
  fix r sa sc sc' μ
  assume R: "(sa, (r, sc)) ∈ ct_ref_rel"
    and r: "three_step r = 0"
    and μ: "∀p. μ p ∈ get_msgs (send0 r) sc (HOs r) (HOs r) p"
        and nxt: "∀p. next0 r p (sc p) (μ p) (crds r p) (sc' p)"
  note μnxt = μ nxt
  have r_phase_step: "nr_steps * three_phase r = r" using r three_phase_step[of r]
    by(auto)
  from r have same_coord: "coord (Suc r) = coord r"
    by(auto simp add: three_step_phase_Suc intro: coord_phase)
  define cand where "cand = commt (sc' (coord (Suc r)))"
  define C where "C = {cand}"
  have guard: "∀cand∈C. ∃Q. majorities.opt_mru_guard (mru_vote ∘ sc) Q cand"
  proof(simp add: C_def)
    let ?Q = "HOs r (coord r)"
    let ?lvs0 = "mru_vote o sc"
    have "?Q ∈ majs" using per_rd μnxt[THEN spec, where x="coord r"]
      per_rd[simplified CT_commPerRd_def, rule_format, OF r]
      by(auto simp add: Let_def majs_def next0_def same_coord get_msgs_dom r_phase_step)
    moreover have
      "map_option snd (option_Max_by fst (ran (?lvs |` ?Q))) ∈ {None, Some cand}"
      using nxt[THEN spec, where x="coord r"]
      msgs_mru_vote[where HOs=HOs and μ=μ, OF μ[THEN spec, where x="coord r"]] 
      get_msgs_dom[OF μ[THEN spec, of "coord r"]]
      by(auto simp add: next0_def Let_def cand_def same_coord split: option.split_asm)
    ultimately have "majorities.opt_mru_guard ?lvs0 ?Q cand"
      by(auto simp add: majorities.opt_mru_guard_def Let_def majorities.opt_mru_vote_def)
    thus "∃Q. majorities.opt_mru_guard ?lvs0 Q cand"
      by blast
  qed

  define sa' where "sa' = sa⦇
      next_round := Suc r,
      candidates := C
    ⦈"
  have "(sa, sa') ∈ majorities.opt_mru_step0 r C" using R r nxt guard
    by(auto simp add: majorities.opt_mru_step0_def sa'_def ct_ref_rel_def)
  moreover have "(sa', (Suc r, sc')) ∈ ct_ref_rel" using R nxt
    apply(auto simp add: sa'_def ct_ref_rel_def intro!:
      mru_vote_evolution0[OF nxt, symmetric] decide_evolution(1)[OF nxt])
       apply(auto simp add: Let_def C_def cand_def o_def intro!: ext)
    done
  ultimately show 
    "∃sa'. (∃r C. (sa, sa') ∈ majorities.opt_mru_step0 r C) 
        ∧ (sa', Suc r, sc') ∈ ct_ref_rel"
    by blast
qed

lemma step1_ref:
  "{ct_ref_rel} 
    (⋃r S v. majorities.opt_mru_step1 r S v), 
    CT_trans_step HOs HOs crds next1 send1 (Suc 0) {> ct_ref_rel}"
proof(clarsimp  simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
  fix r sa sc sc' μ
  assume R: "(sa, (r, sc)) ∈ ct_ref_rel"
    and r: "three_step r = Suc 0"
    and μ: "∀p. μ p ∈ get_msgs (send1 r) sc (HOs r) (HOs r) p"
        and nxt: "∀p. next1 r p (sc p) (μ p) (crds r p) (sc' p)"
  note μnxt = μ nxt

  define v where "v = commt (sc (coord r))"
  define S where "S = {p. coord r ∈ HOs r p}"
  define sa' where "sa' = sa⦇ next_round := Suc r, 
    opt_mru_state.mru_vote := opt_mru_state.mru_vote sa ++ const_map (three_phase r, v) S
  ⦈"
  have "(sa, sa') ∈ majorities.opt_mru_step1 r S v" using r R 
    by(clarsimp simp add: majorities.opt_mru_step1_def sa'_def  S_def v_def 
      ct_ref_rel_def)
  moreover have "(sa', (Suc r, sc')) ∈ ct_ref_rel" using r R
  proof-
    have "mru_vote o sc' = ((mru_vote ∘ sc) ++ const_map (three_phase r, v) S)"
    proof(rule ext, simp)
      fix p
      show "mru_vote (sc' p) = ((mru_vote ∘ sc) ++ const_map (three_phase r, v) S) p"
        using μnxt[THEN spec, of p]
        by(auto simp add: get_msgs_benign next1_def send1_def S_def v_def map_add_def 
          const_map_is_None const_map_is_Some restrict_map_def isVote_def split: option.split)
    qed
    thus ?thesis using R r nxt
      by(force simp add: ct_ref_rel_def sa'_def three_step_Suc intro: decide_evolution)
  qed      
  ultimately show 
    "∃sa'. (∃r S v. (sa, sa') ∈ majorities.opt_mru_step1 r S v) 
        ∧ (sa', Suc r, sc') ∈ ct_ref_rel"
    by blast
qed

lemma step2_ref:
  "{ct_ref_rel} 
    (⋃r dec_f. majorities.opt_mru_step2 r dec_f), 
    CT_trans_step HOs HOs crds next2 send2 2 {> ct_ref_rel}"
proof(clarsimp  simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
  fix r sa sc sc' μ
  assume R: "(sa, (r, sc)) ∈ ct_ref_rel"
    and r: "three_step r = 2"
    and μ: "∀p. μ p ∈ get_msgs (send2 r) sc (HOs r) (HOs r) p"
        and nxt: "∀p. next2 r p (sc p) (μ p) (crds r p) (sc' p)"
  note μnxt = μ nxt

  define dec_f
    where "dec_f p = (if decide (sc' p) ≠ decide (sc p) then decide (sc' p) else None)" for p

  have dec_f: "(decide ∘ sc) ++ dec_f = decide ∘ sc'"
  proof
    fix p
    show "((decide ∘ sc) ++ dec_f) p = (decide ∘ sc') p" using nxt[THEN spec, of p]
      by(auto simp add: map_add_def dec_f_def next2_def split: option.split intro!: ext)
  qed

  define sa' where "sa' = sa⦇
    next_round := Suc r,
    decisions := decisions sa ++ dec_f
  ⦈"

  have "(sa', (Suc r, sc')) ∈ ct_ref_rel" using R r nxt
    by(auto simp add: ct_ref_rel_def sa'_def dec_f three_step_Suc 
      mru_vote_evolution2[OF nxt])
  moreover have "(sa, sa') ∈ majorities.opt_mru_step2 r dec_f" using r R
  proof-
    define sc_r_votes where "sc_r_votes p = (if (∃v. mru_vote (sc p) = Some (three_phase r, v))
        then map_option snd (mru_vote (sc p))
        else None)" for p
    have sc_r_votes: "sc_r_votes = majorities.r_votes sa r" using R r
      by(auto simp add: ct_ref_rel_def sc_r_votes_def majorities.r_votes_def intro!: ext)
    have "majorities.step2_d_guard dec_f sc_r_votes"
    proof(clarsimp simp add: majorities.step2_d_guard_def)
      fix p v
      assume d_f_p: "dec_f p = Some v"
      let ?Qv = "votes_rcvd (μ p)"
      have Qv: "card ?Qv > N div 2" 
        "v = the_rcvd_vote (μ p)" using nxt[THEN spec, of p] d_f_p
        by(auto simp add: next2_def dec_f_def)

      hence "v ∈ snd ` votes_rcvd (μ p)"
        by(fastforce simp add: the_rcvd_vote_def ex_in_conv[symmetric]
          dest!: card_gt_0_iff[THEN iffD1, OF le_less_trans[OF le0]] elim!: imageI intro: someI)
      moreover have "?Qv = map_graph (sc_r_votes) ∩ (HOs r p × UNIV)" using μ[THEN spec, of p]
        by(auto simp add: get_msgs_benign send2_def restrict_map_def votes_rcvd_def
          sc_r_votes_def image_def split: option.split_asm)
      ultimately show "v ∈ ran sc_r_votes ∧ dom sc_r_votes ∈ majs" using Qv(1)
        by(auto simp add: majs_def inj_on_def map_graph_def fun_graph_def sc_r_votes_def
          the_rcvd_vote_def majs_def intro: ranI
          elim!: less_le_trans intro!: card_inj_on_le[where f=fst])
    qed

    thus ?thesis using r R
      by(auto simp add: majorities.opt_mru_step2_def sa'_def ct_ref_rel_def sc_r_votes)
  qed

  ultimately show 
    "∃sa'. (∃r dec_f. (sa, sa') ∈ majorities.opt_mru_step2 r dec_f) 
        ∧ (sa', Suc r, sc') ∈ ct_ref_rel"
    by blast

qed

lemma CT_Refines_ThreeStep_MRU:
  "PO_refines ct_ref_rel majorities.ts_mru_TS (CT_TS HOs HOs crds)"
proof(rule refine_basic)
  show "init (CT_TS HOs HOs crds) ⊆ ct_ref_rel `` init majorities.ts_mru_TS"
    by(auto simp add: CT_TS_defs majorities.ts_mru_TS_defs ct_ref_rel_def)
next
  show 
    "{ct_ref_rel} TS.trans majorities.ts_mru_TS, 
      TS.trans (CT_TS HOs HOs crds) {> ct_ref_rel}"
    apply(simp add: majorities.ts_mru_TS_defs CT_TS_defs)
    apply(auto simp add: CHO_trans_alt CT_trans intro!: step0_ref step1_ref step2_ref)
    done
qed

end (* HO context *)

subsubsection ‹Termination›
(******************************************************************************)

theorem CT_termination:
  assumes run: "CHORun CT_Alg rho HOs crds"
      and commR: "∀r. CHOcommPerRd CT_M r (HOs r) (crds r)"
      and commG: "CHOcommGlobal CT_M HOs crds"
  shows "∃r v. decide (rho r p) = Some v"
proof -
  from commG commR obtain ph c where 
    HOs:
       "coord (nr_steps*ph) = c
         ∧ (∀p. c ∈ HOs (nr_steps*ph+1) p)
         ∧ (∀p. card (HOs (nr_steps*ph+2) p) > N div 2)"
    by(auto simp add: CT_CHOMachine_def CT_commGlobal_def CT_commPerRd_def three_step_def)

  ― ‹The tedious bit: obtain three consecutive rounds linked by send/next functions›
  define r0 where "r0 = nr_steps * ph"
  define cfg0 where "cfg0 = rho r0"
  define r1 where "r1 = Suc r0"
  define cfg1 where "cfg1 = rho r1"
  define r2 where "r2 = Suc r1"
  define cfg2 where "cfg2 = rho r2"
  define cfg3 where "cfg3 = rho (Suc r2)"

  from   
    run[simplified CHORun_def, THEN CSHORun_step, THEN spec, where x="r0"] 
    run[simplified CHORun_def, THEN CSHORun_step, THEN spec, where x="r1"]
    run[simplified CHORun_def, THEN CSHORun_step, THEN spec, where x="r2"] 
    obtain μ0 μ1 μ2 where
    send0: "∀p. μ0 p ∈ get_msgs (send0 r0) cfg0 (HOs r0) (HOs r0) p"
    and three_step0: "∀p. next0 r0 p (cfg0 p) (μ0 p) (crds (Suc r0) p) (cfg1 p)"
    and send1: "∀p. μ1 p ∈ get_msgs (send1 r1) cfg1 (HOs r1) (HOs r1) p"
    and three_step1: "∀p. next1 r1 p (cfg1 p) (μ1 p) (crds (Suc r1) p) (cfg2 p)"
    and send2: "∀p. μ2 p ∈ get_msgs (send2 r2) cfg2 (HOs r2) (HOs r2) p"
    and three_step2: "∀p. next2 r2 p (cfg2 p) (μ2 p) (crds (Suc r2) p) (cfg3 p)"
    apply(auto simp add: CT_Alg_def three_step_def CT_nextState_def CT_sendMsg_def all_conj_distrib
      r0_def r1_def r2_def
      cfg0_def cfg1_def cfg2_def cfg3_def mod_Suc
      )
    done
    
  ― ‹The proof: the coordinator hears enough messages in r0 and thus selects a value.›

  obtain dec_v where dec_v: "commt (cfg1 c) = dec_v"
    by simp

  have step_r0: "three_step r0 = 0"
    by(auto simp add: r0_def three_step_def)
  hence same_coord: 
    "coord r1 = coord r0"
    "coord r2 = coord r0"
    by(auto simp add: three_step_phase_Suc r2_def r1_def r0_def intro!: coord_phase)

  ― ‹All processes hear from the coordinator, and thus set their vote to @{term dec_v}.›  
  hence all_vote: "∀p. mru_vote (cfg2 p) = Some (three_phase r2, dec_v)"
    using HOs three_step1 send1 step_r0 dec_v
    by(auto simp add: next1_def Let_def get_msgs_benign send1_def restrict_map_def isVote_def
      r2_def r1_def r0_def[symmetric] same_coord[simplified r2_def r1_def] three_step_phase_Suc)

  ― ‹And finally, everybody will also decide @{term dec_v}.›
  have all_decide: "∀p. decide (cfg3 p) = Some dec_v"
  proof
    fix p
    have "votes_rcvd (μ2 p) = HOs r2 p × {dec_v}" using send2[THEN spec, where x=p] all_vote
      by(auto simp add: send2_def get_msgs_benign votes_rcvd_def restrict_map_def image_def o_def)

    moreover from HOs have "N div 2 < card (HOs r2 p)"
      by(auto simp add: r2_def r1_def r0_def)

    moreover then have "HOs r2 p ≠ {}"
      by (metis card.empty less_nat_zero_code)
    ultimately show "decide (cfg3 p) = Some dec_v" 
    using three_step2[THEN spec, where x=p] send2[THEN spec, where x=p] all_vote
      by(auto simp add: next2_def send2_def Let_def get_msgs_benign 
        the_rcvd_vote_def restrict_map_def image_def o_def)
  qed
    
  thus ?thesis 
    by(auto simp add: cfg3_def)

qed

end