Theory New_Algorithm_Proofs

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

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

definition New_Algo_TS ::
  "(round ⇒ process HO) ⇒ (round ⇒ process HO) ⇒ (round ⇒ process) ⇒ p_TS_state TS"
where
  "New_Algo_TS HOs SHOs crds = CHO_to_TS New_Algo_Alg HOs SHOs (K o crds)"

lemmas New_Algo_TS_defs = New_Algo_TS_def CHO_to_TS_def New_Algo_Alg_def CHOinitConfig_def
  NA_initState_def

definition New_Algo_trans_step where
  "New_Algo_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) (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 New_Algo_trans:
  "CSHO_trans_alt NA_sendMsg NA_nextState HOs SHOs (K ∘ crds) = 
  New_Algo_trans_step HOs SHOs crds next0 send0 0
  ∪ New_Algo_trans_step HOs SHOs crds next1 send1 1
  ∪ New_Algo_trans_step HOs SHOs crds next2 send2 2
  "
proof(rule equalityI)
  show "CSHO_trans_alt NA_sendMsg NA_nextState HOs SHOs (K ∘ crds)
    ⊆ New_Algo_trans_step HOs SHOs crds next0 send0 0 ∪
       New_Algo_trans_step HOs SHOs crds next1 send1 1 ∪
       New_Algo_trans_step HOs SHOs crds next2 send2 2"
  by(force simp add: CSHO_trans_alt_def NA_sendMsg_def NA_nextState_def 
    New_Algo_trans_step_def K_def dest!: three_step_less_D)
next
  show "New_Algo_trans_step HOs SHOs crds next0 send0 0 ∪
    New_Algo_trans_step HOs SHOs crds next1 send1 1 ∪
    New_Algo_trans_step HOs SHOs crds next2 send2 2
    ⊆ CSHO_trans_alt NA_sendMsg NA_nextState HOs SHOs (K ∘ crds)"
  by(force simp add: CSHO_trans_alt_def NA_sendMsg_def NA_nextState_def 
    New_Algo_trans_step_def K_def)
qed

type_synonym rHO = "nat ⇒ process HO"

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

definition new_algo_ref_rel :: "(three_step_mru_state × p_TS_state)set" where
  "new_algo_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 = ran (prop_vote o sc))
  }"

text ‹
  Different types seem to be derived for the two ‹mru_vote_evolution› lemmas,
  so we state them separately.›
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
  "μ p ∈ get_msgs (send0 r) cfg (HOs r) (HOs r) 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
      map_comp_def intro!: ext split: option.split)

lemma step0_ref:
  "{new_algo_ref_rel} 
    (⋃r C. majorities.opt_mru_step0 r C), 
    New_Algo_trans_step HOs HOs crds next0 send0 0 {> new_algo_ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distrib)
  fix r sa sc sc' μ
  assume R: "(sa, (r, sc)) ∈ new_algo_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) (sc' p)"
  note μnxt = μ nxt
  have r_phase_step: "nr_steps * three_phase r = r" using r three_phase_step[of r]
    by(auto)
  define C where "C = ran (prop_vote o sc')"
  have guard: "∀cand∈C. ∃Q. majorities.opt_mru_guard (mru_vote ∘ sc) Q cand"
  proof(simp add: C_def ran_def, safe)
    fix p cand
    assume Some: "prop_vote (sc' p) = Some cand"

    let ?Q = "HOs r p"
    let ?lvs0 = "mru_vote o sc"

    have "?Q ∈ majs" using Some μnxt[THEN spec, where x=p]
      by(auto simp add: Let_def majs_def next0_def get_msgs_dom)

    moreover have
      "map_option snd (option_Max_by fst (ran (?lvs |` ?Q))) ∈ {None, Some cand}"
      using Some nxt[THEN spec, where x=p]
      msgs_mru_vote[where HOs=HOs and μ=μ, OF μ[THEN spec, of p]]
      get_msgs_dom[OF μ[THEN spec, of p]]
      by(auto simp add: next0_def Let_def 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 new_algo_ref_rel_def)
  moreover have "(sa', (Suc r, sc')) ∈ new_algo_ref_rel" using R nxt
    apply(auto simp add: sa'_def new_algo_ref_rel_def intro!:
      mru_vote_evolution0[OF nxt, symmetric] decide_evolution(1)[OF nxt]
    )
       apply(auto simp add: Let_def C_def o_def intro!: ext)
    done
  ultimately show 
    "∃sa'. (∃r C. (sa, sa') ∈ majorities.opt_mru_step0 r C) 
        ∧ (sa', Suc r, sc') ∈ new_algo_ref_rel"
    by blast
qed

lemma step1_ref:
  "{new_algo_ref_rel} 
    (⋃r S v. majorities.opt_mru_step1 r S v), 
    New_Algo_trans_step HOs HOs crds next1 send1 (Suc 0) {> new_algo_ref_rel}"
proof(clarsimp  simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distrib)
  fix r sa sc sc' μ
  assume R: "(sa, (r, sc)) ∈ new_algo_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) (sc' p)"
  note μnxt = μ nxt

  define S where "S = {p. mru_vote (sc' p) ≠ mru_vote (sc p)}"

  have S: "S ⊆ {p. ∃Q v. Q ⊆ HOs r p
      ∧ (∀q ∈ Q. prop_vote (sc q) = Some v)
      ∧ Q ∈ majs
      ∧ (mru_vote (sc' p) = Some (three_phase r, v))
    }"
  proof(safe)
    fix p
    assume "p ∈ S"
    then obtain Q v 
      where 
      "∀q ∈ Q. μ p q = Some (PreVote v)"
      and maj_Q: "Q ∈ majs"
      and Q_HOs: "Q ⊆ dom (μ p)"
      and lv: "mru_vote (sc' p) = Some (three_phase r, v)" (is "?LV v")
      using nxt[THEN spec, where x=p]
      by(clarsimp simp add: next1_def Let_def S_def majs_def Q_prevotes_v_def)
  
    then have 
      "∀q ∈ Q. prop_vote (sc q) = Some v" (is "?P Q v")
      "Q ⊆ HOs r p"
      using μ[THEN spec, where x=p]
      by(auto simp add: get_msgs_benign send1_def restrict_map_def split: option.split_asm)
    
    with maj_Q and lv show "∃Q v. Q ⊆ HOs r p ∧ ?P Q v ∧ Q ∈ majs ∧ ?LV v" by blast
  qed    

  obtain v where 
    v: "∀p ∈ S. mru_vote (sc' p) = Some (three_phase r, v) ∧ v ∈ ran (prop_vote o sc)"
  proof(cases "S = {}")
    case False
    assume asm: 
      "⋀v. ∀p∈S. pstate.mru_vote (sc' p) = Some (three_phase r, v) ∧ v ∈ ran (prop_vote o sc)  
        ⟹ thesis"
    from False obtain p where "p ∈ S" by auto
    with S nxt
      obtain Q v 
      where prop_vote: "(∀q ∈ Q. prop_vote (sc q) = Some v)" and maj_Q: "Q ∈ majs" 
      by auto
      
    hence "∀p∈S. pstate.mru_vote (sc' p) = Some (three_phase r, v)" (is "?LV(v)")
      using S
      by(fastforce dest!: subsetD dest: majorities.qintersect)
    
    with asm prop_vote maj_Q show thesis
      by (metis all_not_in_conv comp_eq_dest_lhs majorities.empty_not_quorum ranI)
  qed(auto)

  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 v
    by(clarsimp simp add: majorities.opt_mru_step1_def sa'_def 
      new_algo_ref_rel_def ball_conj_distrib)

  moreover have "(sa', (Suc r, sc')) ∈ new_algo_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 v
        by(auto simp add: S_def map_add_def const_map_is_None const_map_is_Some split: option.split)
    qed
    thus ?thesis using R r nxt
      by(force simp add: new_algo_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') ∈ new_algo_ref_rel"
    by blast
qed

lemma step2_ref:
  "{new_algo_ref_rel} 
    (⋃r dec_f. majorities.opt_mru_step2 r dec_f), 
    New_Algo_trans_step HOs HOs crds next2 send2 2 {> new_algo_ref_rel}"
proof(clarsimp  simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distrib)
  fix r sa sc sc' μ
  assume R: "(sa, (r, sc)) ∈ new_algo_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) (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 Let_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')) ∈ new_algo_ref_rel" using R r nxt
    by(auto simp add: new_algo_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: new_algo_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"
      then obtain Q where Q: 
        "Q ∈ majs"
        and vote: "Q ⊆ HOs r p" "∀q∈Q. μ p q = Some (Vote v)"
        using nxt[THEN spec, of p] d_f_p
        by(auto simp add: next2_def dec_f_def Q'_votes_v_def Let_def majs_def)
      have mru_vote: "∀q∈Q. mru_vote (sc q) = Some (three_phase r, v)"  using vote μ[THEN spec, of p]
        by(fastforce simp add: get_msgs_benign send2_def sc_r_votes_def restrict_map_def 
          split: option.split_asm if_split_asm)
      hence "dom sc_r_votes ∈ majs"
        by(auto intro!:  majorities.mono_quorum[OF Q] simp add: sc_r_votes_def)
      moreover have "v ∈ ran sc_r_votes" using Q[THEN majorities.quorum_non_empty] mru_vote
        by(force simp add: sc_r_votes_def ex_in_conv[symmetric] intro: ranI)
      ultimately show "v ∈ ran sc_r_votes ∧ dom sc_r_votes ∈ majs" 
        by blast
    qed

    thus ?thesis using r R
      by(auto simp add: majorities.opt_mru_step2_def sa'_def new_algo_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') ∈ new_algo_ref_rel"
    by blast

qed

lemma New_Algo_Refines_votes:
  "PO_refines new_algo_ref_rel
    majorities.ts_mru_TS (New_Algo_TS HOs HOs crds)"
proof(rule refine_basic)
  show "init (New_Algo_TS HOs HOs crds) ⊆ new_algo_ref_rel `` init majorities.ts_mru_TS"
    by(auto simp add: New_Algo_TS_defs majorities.ts_mru_TS_defs new_algo_ref_rel_def)
next
  show 
    "{new_algo_ref_rel} TS.trans majorities.ts_mru_TS, 
      TS.trans (New_Algo_TS HOs HOs crds) {> new_algo_ref_rel}"
    apply(simp add: majorities.ts_mru_TS_defs New_Algo_TS_defs)
    apply(auto simp add: CHO_trans_alt New_Algo_trans intro!: step0_ref step1_ref step2_ref)
    done
qed

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

theorem New_Algo_termination:
  assumes run: "HORun New_Algo_Alg rho HOs"
      and commR: "∀r. HOcommPerRd New_Algo_M (HOs r)"
      and commG: "HOcommGlobal New_Algo_M HOs"
  shows "∃r v. decide (rho r p) = Some v"
proof -
  from commG obtain ph where 
    HOs: "∀i ∈ {0..2}. 
      (∀p. card (HOs (nr_steps*ph+i) p) > N div 2)
      ∧ (∀p q. HOs (nr_steps*ph+i) p = HOs (nr_steps*ph) q)"
    by(auto simp add: New_Algo_HOMachine_def NA_commGlobal_def)

  ― ‹The tedious bit: obtain four 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 HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r0"] 
    run[simplified HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r1"]
    run[simplified HORun_def SHORun_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) undefined (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) undefined (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) undefined (cfg3 p)"
    apply(auto simp add: New_Algo_Alg_def three_step_def NA_nextState_def NA_sendMsg_def all_conj_distrib
      r0_def r1_def r2_def
      cfg0_def cfg1_def cfg2_def cfg3_def mod_Suc
      )
    done

  ― ‹The proof: everybody hears the same messages (non-empty!) in r0...›

  from HOs[THEN bspec, where x=0, simplified] send0
    have 
    "∀p q. μ0 p = μ0 q" "∀p. N div 2 < card (dom (μ0 p))"
    apply(auto simp add: get_msgs_benign send0_def r1_def r0_def dom_def restrict_map_def intro!: ext)
      apply(blast)+
    done

  ― ‹...hence everybody sets @{term prop_vote} to the same value...›    
  hence same_prevote: 
    "∀p. prop_vote (cfg1 p) ≠ None"
    "∀p q. prop_vote (cfg1 p) = prop_vote (cfg1 q)" using three_step0
    apply(auto simp add: next1_def Let_def all_conj_distrib intro!: ext)
     apply(clarsimp simp add: next0_def all_conj_distrib Let_def)
    apply(clarsimp simp add: next0_def all_conj_distrib Let_def)
    by (metis (full_types) dom_eq_empty_conv empty_iff majoritiesE')

  ― ‹...which will become our decision value.›
  then obtain dec_v where dec_v: "∀p. prop_vote (cfg1 p) = Some dec_v"
    by (metis option.collapse)

  ― ‹...and since everybody hears from majority in r1...›
  from HOs[THEN bspec, where x="Suc 0", simplified] send1
  have "∀p q. μ1 p = μ1 q" "∀p. N div 2 < card (dom (μ1 p))"
    apply(auto simp add: get_msgs_benign send1_def r1_def r0_def dom_def restrict_map_def intro!: ext)
     apply(blast)+
    done

  ― ‹and since everybody casts a pre-vote for @{term dec_v}, everybody will vote @{term dec_v}› 
  have all_vote: "∀p. mru_vote (cfg2 p) = Some (three_phase r2, dec_v)"
  proof
    fix p
    have r0_step: "three_step r0 = 0"
      by(auto simp add: r0_def three_step_def)
    from HOs[THEN bspec, where x="Suc 0", simplified] 
    obtain Q where Q: "N div 2 < card Q" "Q ⊆ HOs r1 p"
      by(auto simp add: r1_def r0_def)
    hence "Q_prevotes_v (μ1 p) Q dec_v" using dec_v send1[THEN spec, where x=p]
      by(auto simp add: Q_prevotes_v_def get_msgs_benign restrict_map_def send1_def)
    thus "mru_vote (cfg2 p) = Some (three_phase r2, dec_v)" using 
      three_step1[THEN spec, where x=p] r0_step
      by(auto simp add: next1_def r2_def r1_def three_step_phase_Suc)
  qed

  ― ‹And finally, everybody will also decide @{term dec_v}›
  have all_decide: "∀p. decide (cfg3 p) = Some dec_v"
  proof
    fix p
    from HOs[THEN bspec, where x="Suc (Suc 0)", simplified] 
    obtain Q where Q: "N div 2 < card Q" "Q ⊆ HOs r2 p"
      by(auto simp add: r2_def r1_def r0_def)
    thus "decide (cfg3 p) = Some dec_v" 
    using three_step2[THEN spec, where x=p] send2[THEN spec, where x=p]
      by(auto simp add: next2_def send2_def Let_def)
  qed

  thus ?thesis 
    by(auto simp add: cfg3_def)
qed

end