Theory Ate_Proofs

(*<*)
theory Ate_Proofs
imports "../Voting_Opt" Ate_Defs Heard_Of.Majorities 
  "../HO_Transition_System"
begin
(*>*)

subsection ‹Proofs›
axiomatization where val_linorder: 
  "OFCLASS(val, linorder_class)"

instance val :: linorder by (rule val_linorder)

context ate_parameters
begin

definition majs :: "(process set) set" where
  "majs ≡ {S. card S > E}"

interpretation majorities: quorum_process majs
proof
  fix Q Q' assume "Q ∈ majs" "Q' ∈ majs"
  hence "N < card Q + card Q'" using majE
    by(auto simp add: majs_def)
  thus "Q ∩ Q' ≠ {}"
    apply (intro majorities_intersect)
    apply(auto)
    done
next
  from EltN
  show "∃Q. Q ∈ majs" 
    apply(rule_tac x=UNIV in exI)
    apply(auto simp add: majs_def intro!: div_less_dividend)
    done
qed

type_synonym p_TS_state = "(nat × (process ⇒ (val pstate)))"

definition K where
  "K y ≡ λx. y"

definition Ate_Alg where
  "Ate_Alg =
    ⦇ CinitState =  (λ p st crd. Ate_initState p st),
     sendMsg =  Ate_sendMsg,
     CnextState = (λ r p st msgs crd st'. Ate_nextState r p st msgs st')
   ⦈"

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

lemmas Ate_TS_defs = Ate_TS_def CHO_to_TS_def Ate_Alg_def CHOinitConfig_def
  Ate_initState_def

definition
  "Ate_trans_step HOs ≡ ⋃r μ.
   {((r, cfg), Suc r, cfg')|cfg cfg'.
    (∀p. μ p ∈ get_msgs (Ate_sendMsg r) cfg (HOs r) (HOs r) p) ∧
    (∀p. Ate_nextState r p (cfg p) (μ p) (cfg' p))}"

definition CSHOnextConfig where
  "CSHOnextConfig A r cfg HO SHO coord cfg' ≡
   ∀p. ∃μ ∈ SHOmsgVectors A r p cfg (HO p) (SHO p).
          CnextState A r p (cfg p) μ (coord p) (cfg' p)"

type_synonym rHO = "nat ⇒ process HO"

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

definition ate_ref_rel :: "(opt_v_state × p_TS_state)set" where
  "ate_ref_rel =  {(sa, (r, sc)).
    r = next_round sa
    ∧ (∀p. decisions sa p = Ate_Defs.decide (sc p))
    ∧ majorities.opt_no_defection sa (Some o x o sc)
  }"

lemma decide_origin:
  assumes 
    send: "μ p ∈ get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) p"
    and nxt: "Ate_nextState r p (sc p) (μ p) (sc' p)"
    and new_dec: "decide (sc' p) ≠ decide (sc p)"
  shows
    "∃v. decide (sc' p) = Some v ∧ {q. x (sc q) = v} ∈ majs" using assms
  by(auto simp add: get_msgs_benign Ate_sendMsg_def Ate_nextState_def
    majs_def restrict_map_def elim!: order.strict_trans2 intro!: card_mono)

lemma other_values_received:
  assumes nxt: "Ate_nextState  r q (sc q) μq ((sc') q)"
  and muq: "μq ∈ get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) q"
  and vsent: "card {qq. sendMsg Ate_M r qq q (sc qq) = v} > E - α"
             (is "card ?vsent > _")
  shows "card ({qq. μq qq ≠ Some v} ∩ HOs r q) ≤ N + 2*α - E"
proof -
  from nxt muq
  have "({qq. μq qq ≠ Some v} ∩ HOs r q) - (HOs r q - HOs r q)
        ⊆  {qq. sendMsg Ate_M r qq q (sc qq) ≠ v}"
    (is "?notvrcvd - ?aho ⊆ ?notvsent") 
    unfolding get_msgs_def SHOmsgVectors_def Ate_SHOMachine_def by auto
  hence "card ?notvsent ≥ card (?notvrcvd - ?aho)"
    and "card (?notvrcvd - ?aho) ≥ card ?notvrcvd - card ?aho"
    by (auto simp: card_mono diff_card_le_card_Diff)
  moreover
  have 1: "card ?notvsent + card ?vsent = card (?notvsent ∪ ?vsent)"
    by (subst card_Un_Int) auto
  have "?notvsent ∪ ?vsent = (UNIV::process set)" by auto
  hence "card (?notvsent ∪ ?vsent) = N" by simp
  with 1 vsent have "card ?notvsent ≤  N - (E + 1 - α)" by auto
  ultimately
  show ?thesis using EltN Egta by auto
qed

text ‹
  If more than ‹E - α› processes send a value ‹v› to some
  process ‹q› at some round ‹r›, and if ‹q› receives more than
  ‹T› messages in ‹r›, then ‹v› is the most frequently
  received value by ‹q› in ‹r›.
›

lemma mostOftenRcvd_v:
  assumes nxt: "Ate_nextState  r q (sc q) μq ((sc') q)"
  and muq: "μq ∈ get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) q"
  and threshold_T: "card {qq. μq qq ≠ None} > T"
  and threshold_E: "card {qq. sendMsg Ate_M r qq q (sc qq) = v} > E - α"
  shows "mostOftenRcvd μq = {v}"
proof -
  from muq have hodef:"HOs r q = {qq. μq qq ≠ None}"
    unfolding get_msgs_def SHOmsgVectors_def by auto

  from nxt muq threshold_E
  have "card ({qq. μq qq ≠ Some v} ∩ HOs r q) ≤ N + 2*α - E"
    (is "card ?heardnotv ≤ _")
    by (rule other_values_received)
  moreover
  have "card ?heardnotv ≥ T + 1 - card {qq. μq qq = Some v}"
  proof -
    from muq
    have "?heardnotv = (HOs r q) - {qq. μq qq = Some v}"
      and "{qq. μq qq = Some v} ⊆ HOs r q"
      unfolding SHOmsgVectors_def get_msgs_def by auto
    hence "card ?heardnotv = card (HOs r q) - card {qq. μq qq = Some v}"
      by (auto simp: card_Diff_subset)
    with hodef threshold_T show ?thesis by auto
  qed
  ultimately
  have "card {qq. μq qq = Some v} > card ?heardnotv"
    using TNaE by auto
  moreover
  {
    fix w
    assume w: "w ≠ v"
    with hodef have "{qq. μq qq = Some w} ⊆ ?heardnotv" by auto
    hence "card {qq. μq qq = Some w} ≤ card ?heardnotv" by (auto simp: card_mono)
  }
  ultimately
  have "{w. card {qq. μq qq = Some w} ≥ card {qq. μq qq = Some v}} = {v}"
    by force
  thus ?thesis unfolding mostOftenRcvd_def by auto
qed

lemma step_ref:
  "{ate_ref_rel} 
      (⋃r v_f d_f. majorities.flv_round r v_f d_f), 
      Ate_trans_step HOs 
    {> ate_ref_rel}"
proof(simp add: PO_rhoare_defs Ate_trans_step_def, safe)
  fix sa r sc sc' μ
  assume
    R: "(sa, r, sc) ∈ ate_ref_rel"
    and send: "∀p. μ p ∈ get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) p"
    and nxt: "∀p. Ate_nextState r p (sc p) (μ p) (sc' p)"
  note step=send nxt
  define d_f
    where "d_f p = (if decide (sc' p) ≠ decide (sc p) then decide (sc' p) else None)" for p

  define sa' where "sa' = ⦇ 
    opt_v_state.next_round = Suc r
    , opt_v_state.last_vote = opt_v_state.last_vote sa ++ (Some o x o sc) 
    , opt_v_state.decisions = opt_v_state.decisions sa ++ d_f
    ⦈"
  
  have "majorities.d_guard d_f (Some o x o sc)"
  proof(clarsimp simp add: majorities.d_guard_def d_f_def)
    fix p v
    assume
      "Some v ≠ decide (sc p)" 
      "decide (sc' p) = Some v"
    from this and 
      decide_origin[where μ=μ and HOs=HOs and sc'=sc', OF send[THEN spec, of p] nxt[THEN spec, of p]]
    show "quorum_process.locked_in_vf majs (Some ∘ x ∘ sc) v"
      by(auto simp add: majorities.locked_in_vf_def majorities.quorum_for_def)
  qed
  hence
    "(sa, sa') ∈ majorities.flv_round r (Some o x o sc) d_f" using R
    by(auto simp add: majorities.flv_round_def ate_ref_rel_def sa'_def)
  moreover have "(sa', Suc r, sc') ∈ ate_ref_rel"
  proof(unfold ate_ref_rel_def, safe)
    fix p
    show "opt_v_state.decisions sa' p = decide (sc' p)" using R nxt[THEN spec, of p]
      by(auto simp add: ate_ref_rel_def sa'_def map_add_def d_f_def Ate_nextState_def
        split: option.split)
  next
    show "quorum_process.opt_no_defection majs sa' (Some ∘ x ∘ sc')"
    proof(clarsimp simp add: sa'_def majorities.opt_no_defection_def map_add_def majorities.quorum_for_def)
      fix Q p v
      assume Q: "Q ∈ majs" and Q_v: "∀q ∈ Q. x (sc q) = v" and p_Q: "p ∈ Q"
      hence old: "x (sc p) = v" by simp

      have v_maj: "{q. x (sc q) = v} ∈ majs" using Q Q_v
        apply(simp add: majs_def)
        apply(erule less_le_trans, rule card_mono, auto)
        done
      show "x (sc' p) = v"
      proof(cases "T < card {qq. μ p qq ≠ None}")
        case True
        have
          "E - α < card {qq. sendMsg Ate_M r qq p (sc qq) = v}" using v_maj
          by(auto simp add: Ate_SHOMachine_def Ate_sendMsg_def majs_def)
        from mostOftenRcvd_v[where HOs=HOs and sc=sc and sc'=sc', 
          OF nxt[THEN spec, of p] send[THEN spec, of p] True this]
        show ?thesis using nxt[THEN spec, of p] old
          by(clarsimp simp add: Ate_nextState_def)
      next
        case False
        thus ?thesis using nxt[THEN spec, of p] old
          by(clarsimp simp add: Ate_nextState_def)
      qed
    qed
  qed(auto simp add: sa'_def)

  ultimately show 
    "∃sa'. (∃ra v_f d_f. (sa, sa') ∈ quorum_process.flv_round majs ra v_f d_f) 
    ∧ (sa', Suc r, sc') ∈ ate_ref_rel"
    by blast
qed

lemma Ate_Refines_LV_VOting:
  "PO_refines (ate_ref_rel) 
    majorities.flv_TS (Ate_TS HOs HOs crds)"
proof(rule refine_basic)
  show "init (Ate_TS HOs HOs crds) ⊆ ate_ref_rel `` init (quorum_process.flv_TS majs)"
    by(auto simp add: Ate_TS_def CHO_to_TS_def Ate_Alg_def CHOinitConfig_def Ate_initState_def
      majorities.flv_TS_def flv_init_def majorities.opt_no_defection_def majorities.quorum_for_def'
      ate_ref_rel_def)
next
  show 
    "{ate_ref_rel} TS.trans (quorum_process.flv_TS majs), TS.trans (Ate_TS HOs HOs crds) {> ate_ref_rel}"
    using step_ref
    by(simp add: majorities.flv_TS_defs Ate_TS_def CHO_to_TS_def Ate_Alg_def 
      CSHO_trans_alt_def CHO_trans_alt Ate_trans_step_def)
qed

end   ― ‹context @{text "ate_parameters"}›

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

text ‹The termination proof for the algorithm is already given in the Heard-Of Model AFP
  entry, and we do not repeat it here.›

end   (* theory AteProof *)