Theory BenOr_Proofs

(*<*)
theory BenOr_Proofs
imports Heard_Of.Reduction
  Two_Step_Observing "../HO_Transition_System" BenOr_Defs
begin
(*>*)

subsection ‹Proofs›

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

consts 
  val0 :: val 
  val1 :: val

text ‹Ben-Or works only on binary values.›
axiomatization where 
  val_exhaust: "v = val0 ∨ v = val1"
  and val_diff: "val0 ≠ val1"

context mono_quorum
begin

definition BenOr_Alg :: "(process, val pstate, val msg)CHOAlgorithm" where
  "BenOr_Alg = CHOAlgorithm.truncate BenOr_M"

definition BenOr_TS ::
  "(round ⇒ process HO) ⇒ (round ⇒ process HO) ⇒ (round ⇒ process) ⇒ ben_or_TS_state TS"
where
  "BenOr_TS HOs SHOs crds = CHO_to_TS BenOr_Alg HOs SHOs (K o crds)"

lemmas BenOr_TS_defs = BenOr_TS_def CHO_to_TS_def BenOr_Alg_def CHOinitConfig_def
  BenOr_initState_def

type_synonym rHO = "nat ⇒ process HO"

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

lemma two_step_less_D:
  "0 < two_step r ⟹ two_step r = Suc 0"
  by(auto simp add: two_step_def)

lemma BenOr_trans:
  "CSHO_trans_alt BenOr_sendMsg (λr p st msgs crd st'. BenOr_nextState r p st msgs st') HOs SHOs crds = 
  BenOr_trans_step HOs SHOs next0 send0 0
  ∪ BenOr_trans_step HOs SHOs  next1 send1 1
  "
proof
  show "CSHO_trans_alt BenOr_sendMsg (λr p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds
    ⊆ BenOr_trans_step HOs SHOs next0 send0 0 ∪ BenOr_trans_step HOs SHOs next1 send1 1"
  by(force simp add: CSHO_trans_alt_def BenOr_sendMsg_def BenOr_nextState_def BenOr_trans_step_def 
    K_def dest!: two_step_less_D)
next
  show " BenOr_trans_step HOs SHOs next0 send0 0 ∪
    BenOr_trans_step HOs SHOs next1 send1 1
    ⊆ CSHO_trans_alt BenOr_sendMsg
        (λr p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds"
  by(force simp add: CSHO_trans_alt_def BenOr_sendMsg_def BenOr_nextState_def BenOr_trans_step_def)
qed

definition "BenOr_A = CHOAlgorithm.truncate BenOr_M"

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

text ‹Agreement for BenOr only holds if the communication predicates hold›
context
  fixes
    HOs :: "nat ⇒ process ⇒ process set"
    and rho :: "nat ⇒ process ⇒ val pstate"
  assumes comm_global: "BenOr_commGlobal HOs"
  and per_rd: "∀r. BenOr_commPerRd (HOs r)"
  and run: "HORun BenOr_A rho HOs"
begin
(******************************************************************************)

definition no_vote_diff where
  "no_vote_diff sc p ≡ vote (sc p) = None ⟶
            (∃q q'. x (sc q) ≠ x (sc q'))"

definition ref_rel :: "(tso_state × ben_or_TS_state)set" where
  "ref_rel ≡ {(sa, (r, sc)).
    r = next_round sa
    ∧ (two_step r = 1 ⟶ r_votes sa = vote o sc)
    ∧ (two_step r = 1 ⟶ (∀p. no_vote_diff sc p))
    ∧ (∀p v. x (sc p) = v ⟶ (∃q. last_obs sa q ∈ {None, Some v}))
    ∧ decisions sa = decide o sc
  }"

lemma HOs_intersect:
  "HOs r p ∩ HOs r' q ≠ {}" using per_rd
  apply(simp add: BenOr_commPerRd_def)
  apply(blast dest: qintersect)
  done

lemma HOs_nonempty:
  "HOs r p ≠ {}" 
  using HOs_intersect
  by blast

lemma vote_origin:
  assumes
  send: "∀p. μ p ∈ get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "∀p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows 
    "vote (cfg' p) = Some v ⟷ (∀q ∈ HOs r p. x (cfg q) = v)" 
  using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty
  by(auto simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)
  
lemma same_new_vote:
  assumes 
  send: "∀p. μ p ∈ get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "∀p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  obtains v where "∀p w. vote (cfg' p) = Some w ⟶ w = v" 
proof(cases "∃p v. vote (cfg' p) = Some v")
  case True
  assume asm: "⋀v. ∀p w. vote (cfg' p) = Some w ⟶ w = v ⟹ thesis"
  from True obtain p v where "vote (cfg' p) = Some v" by auto

  hence "∀p w. vote (cfg' p) = Some w ⟶ w = v" (is "?LV(v)")
    using vote_origin[OF send step step_r] HOs_intersect
    by(force)

  from asm[OF this] show ?thesis .
qed(auto)

lemma no_x_change:
  assumes
  send: "∀p. μ p ∈ get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "∀p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows 
    "x (cfg' p) = x (cfg p)" 
  using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty
  by(auto simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)

lemma no_vote:
  assumes 
  send: "∀p. μ p ∈ get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "∀p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows
    "no_vote_diff cfg' p" 
    unfolding no_vote_diff_def
proof
  assume
    "vote (cfg' p) = None"
  hence "(∃q q'. x (cfg q) ≠ x (cfg q'))"
   using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty 
   apply(clarsimp simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)
   by metis
  thus "(∃q q'. x (cfg' q) ≠ x (cfg' q'))" 
    using no_x_change[OF send step step_r]
    by(simp)
qed
  

lemma step0_ref:
  "{ref_rel} ⋃r S v. tso_round0 r S v, 
    BenOr_trans_step HOs HOs next0 send0 0 {> ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs BenOr_trans_step_def all_conj_distrib)
  fix sa r cfg μ cfg'
  assume
    R: "(sa, (r, cfg)) ∈ ref_rel"
    and step_r: "two_step r = 0" 
    and send: "∀p. μ p ∈ get_msgs (send0 r) cfg (HOs r) (HOs r) p"
    and step: "∀p. next0 r p (cfg p) (μ p) (cfg' p)"

  from R have next_r: "next_round sa = r"
    by(simp add: ref_rel_def)

  from HOs_nonempty send have "∀p. ∃q. q ∈ msgRcvd (μ p)"
    by(fastforce simp add: get_msgs_benign send0_def msgRcvd_def restrict_map_def)
  with step have same_dec: "decide o cfg' = decide o cfg"
    apply(simp add: next0_def o_def)
    by (metis pstate.select_convs(3) pstate.surjective pstate.update_convs(2))
 
  define S where "S = {p. ∃v. vote (cfg' p) = Some v}"
  from same_new_vote[OF send step step_r] 
  obtain v where v: "∀p ∈ S. vote (cfg' p) = Some v"
    by(simp add: S_def) (metis)
  hence vote_const_map: "vote o cfg' = const_map v S"
    by(auto simp add: S_def const_map_def restrict_map_def intro!: ext)

  define sa' where "sa' = sa⦇ next_round := Suc r, r_votes := const_map v S ⦈"

  have "∀p. p ∈ S ⟶ opt_obs_safe (last_obs sa) v"
    using vote_origin[OF send step step_r] R per_rd[THEN spec, of r] v
    apply(clarsimp simp add: BenOr_commPerRd_def opt_obs_safe_def ref_rel_def)
    by metis
    
  hence "(sa, sa') ∈ tso_round0 r S v" using next_r step_r v R 
    vote_origin[OF send step step_r]
    by(auto simp add: tso_round0_def sa'_def all_conj_distrib)


  moreover have "(sa', Suc r, cfg') ∈ ref_rel" using step send v R same_dec step_r next_r
    apply(auto simp add: ref_rel_def sa'_def  two_step_phase_Suc vote_const_map next0_def
      all_conj_distrib no_vote[OF send step step_r])
    by (metis pstate.select_convs(1) pstate.surjective pstate.update_convs(2))

  ultimately show
    "∃sa'. (∃r S v. (sa, sa') ∈ tso_round0 r S v) ∧ (sa', Suc r, cfg') ∈ ref_rel"
    by blast
qed

definition D where
  "D cfg cfg' ≡ {p. decide (cfg' p) ≠ decide (cfg p) }"

lemma decide_origin:
  assumes
  send: "∀p. μ p ∈ get_msgs (send1 r) cfg (HOs r) (HOs r) p"
  and step: "∀p. next1 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = Suc 0"
  shows 
    "D cfg cfg' ⊆ {p. ∃v. decide (cfg' p) = Some v ∧ (∀q ∈ HOs r p. vote (cfg q) = Some v)}" 
  using assms
  by(fastforce simp add: D_def next1_def get_msgs_benign send1_def msgRcvd_def o_def restrict_map_def
    x_update_def dec_update_def identicalVoteRcvd_def all_conj_distrib someVoteRcvd_def isVote_def)
  
lemma step1_ref:
  "{ref_rel ∩ (TSO_inv1 ∩ TSO_inv2) × UNIV} ⋃r d_f o_f. tso_round1 r d_f o_f, 
    BenOr_trans_step HOs HOs next1 send1 (Suc 0) {> ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs BenOr_trans_step_def all_conj_distrib)
  fix sa r cfg μ and cfg' :: "process ⇒ val pstate"
  assume
    R: "(sa, (r, cfg)) ∈ ref_rel"
    and step_r: "two_step r = Suc 0" 
    and send: "∀p. μ p ∈ get_msgs (send1 r) cfg (HOs r) (HOs r) p"
    and step: "∀p. next1 r p (cfg p) (μ p) (cfg' p)"
    and ainv: "sa ∈ TSO_inv1"
    and ainv2: "sa ∈ TSO_inv2"

  from R have next_r: "next_round sa = r"
    by(simp add: ref_rel_def)

  define S where "S = {p. ∃v. vote (cfg p) = Some v}"
  from R obtain v where v: "∀p ∈ S. vote (cfg p) = Some v" using ainv step_r
    by(auto simp add: ref_rel_def TSO_inv1_def S_def)

  define Ob where "Ob = {p. x (cfg' p) = v}"
  define o_f where "o_f p = (if S ∈ Quorum then Some v else None)" for p :: process

  define dec_f where "dec_f p = (if p ∈ D cfg cfg' then decide (cfg' p) else None)" for p

  {
    fix p w
    assume "vote (cfg p) = Some w"
    hence "w = v" using v
      by(unfold S_def, auto)
  } note v'=this
    
  have d_guard: "d_guard dec_f (vote ∘ cfg)" using per_rd[THEN spec, of r]
    by(fastforce simp add: d_guard_def locked_in_vf_def quorum_for_def dec_f_def
      BenOr_commPerRd_def dest!: decide_origin[OF send step step_r, THEN subsetD])

  have "dom (vote ∘ cfg) ∈ Quorum ⟶ Ob = UNIV"
  proof(auto simp add: Ob_def)
    fix p
    assume Q: "dom (vote ∘ cfg) ∈ Quorum" (is "?Q ∈ Quorum")
    hence "?Q ∩ HOs r p ≠ {}"  using per_rd[THEN spec, of r]
      by(auto simp add: BenOr_commPerRd_def dest: qintersect)
    hence "someVoteRcvd (μ p) ≠ {}" using send[THEN spec, of p]
      by(force simp add: someVoteRcvd_def get_msgs_benign msgRcvd_def restrict_map_def 
        isVote_def send1_def)
    moreover have "∀q ∈ someVoteRcvd (μ p). ∃x'. μ p q = Some (Vote (Some v))"
       using send[THEN spec, of p]
      by(auto simp add: someVoteRcvd_def get_msgs_benign msgRcvd_def restrict_map_def
        isVote_def send1_def dest: v')
    ultimately show "x (cfg' p) = v" using step[THEN spec, of p]
      by(auto simp add: next1_def x_update_def)
  qed
  note Ob_UNIV=this[rule_format]

  have obs_guard: "obs_guard o_f (vote ∘ cfg)"
    apply(auto simp add: obs_guard_def o_f_def S_def dom_def
      dest: v' Ob_UNIV quorum_non_empty) 
    apply (metis S_def all_not_in_conv  empty_not_quorum v)
    done

  define sa' where "sa' = sa⦇ 
    next_round := Suc (next_round sa)
    , decisions := decisions sa ++ dec_f
    , last_obs := last_obs sa ++ o_f
    ⦈"

  ― ‹Abstract step›
  have abs_step: "(sa, sa') ∈ tso_round1 r dec_f o_f"  using next_r step_r R d_guard obs_guard
    by(auto simp add: tso_round1_def sa'_def ref_rel_def)

  ― ‹Relation preserved›
  have "∀p. ((decide ∘ cfg) ++ dec_f) p = decide (cfg' p)"
  proof
    fix p
    show "((decide ∘ cfg) ++ dec_f) p = decide (cfg' p)" using step[THEN spec, of p]
      by(auto simp add: dec_f_def D_def next1_def dec_update_def map_add_def)
  qed
  note dec_rel=this[rule_format]

  have "∀p. (∃q. o_f q = None ∧ opt_obsv_state.last_obs sa q = None 
        ∨ (opt_obsv_state.last_obs sa ++ o_f) q = Some (x (cfg' p)))"
  proof(intro allI impI, cases "S ∈ Quorum")
    fix p 
    case True 
    hence "x (cfg' p) = v" using Ob_UNIV
      by(auto simp add: S_def Ob_def dom_def)
    thus "(∃q. o_f q = None ∧ opt_obsv_state.last_obs sa q = None 
        ∨ (opt_obsv_state.last_obs sa ++ o_f) q = Some (x (cfg' p)))"
      using True
      by(auto simp add: o_f_def)
  next
    fix p
    case False
    hence empty: "o_f = Map.empty"
      by(auto simp add: o_f_def)
    from False have "S ≠ UNIV" using UNIV_quorum
      by auto
    then obtain q where q: "vote (cfg q) = None" using False
      by(auto simp add: o_f_def S_def)
    then obtain q1 q2 where 
      "x (cfg q1) ≠ x (cfg q2)" using R step_r
      by(auto simp add: ref_rel_def no_vote_diff_def)
    then obtain q1' q2' where
      "x (cfg q1') = val0"
      "x (cfg q2') = val1"
      by (metis (poly_guards_query) val_exhaust)
    hence "∀v. ∃q. opt_obsv_state.last_obs sa q ∈ {None, Some v}" using R step_r
      apply(auto simp add: ref_rel_def)
      by (metis (poly_guards_query) val_exhaust)
    (* note x = x_origin2[OF send step step_r refl, of p] *)
    thus "(∃q. o_f q = None ∧ opt_obsv_state.last_obs sa q = None 
        ∨ (opt_obsv_state.last_obs sa ++ o_f) q = Some (x (cfg' p)))" using empty
        by(auto)
  qed
  note obs_rel=this[rule_format]

  have post_rel: 
    "(sa', Suc r, cfg') ∈ ref_rel" using step send next_r R step_r
    by(auto simp add: sa'_def ref_rel_def 
      two_step_phase_Suc dec_rel obs_rel)
    
  from abs_step post_rel show
    "∃sa'. (∃r d_f o_f. (sa, sa') ∈ tso_round1 r d_f o_f) ∧ (sa', Suc r, cfg') ∈ ref_rel"
    by blast
qed

lemma BenOr_Refines_Two_Step_Obs:
  "PO_refines (ref_rel ∩ (TSO_inv1 ∩ TSO_inv2) × UNIV)
    tso_TS (BenOr_TS HOs HOs crds)"
proof(rule refine_using_invariants)
  show "init (BenOr_TS HOs HOs crds) ⊆ ref_rel `` init tso_TS"
    by(auto simp add: BenOr_TS_defs BenOr_HOMachine_def CHOAlgorithm.truncate_def 
      tso_TS_defs ref_rel_def tso_init_def Let_def o_def)
next
  show 
    "{ref_rel ∩ (TSO_inv1 ∩ TSO_inv2) × UNIV} TS.trans tso_TS, 
      TS.trans (BenOr_TS HOs HOs crds) {> ref_rel}"
    apply(simp add: tso_TS_defs BenOr_TS_defs BenOr_HOMachine_def CHOAlgorithm.truncate_def)
    apply(auto simp add: CHO_trans_alt BenOr_trans intro!: step0_ref step1_ref)
    done
qed(auto intro!: TSO_inv1_inductive TSO_inv2_inductive)

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

text ‹The full termination proof for Ben-Or is probabilistic, and depends on the state
of the processes, and a "favorable" coin toss, where "favorable" is relative to this state.
As this termination pre-condition is state-dependent, we cannot capture it in an HO 
predicate.

Instead, we prove a variant of the argument, where we assume that there exists a 
round where all the processes hear from the same set of other processes, and all toss the 
same coin.
›

theorem BenOr_termination:
  shows "∃r v. decide (rho r p) = Some v"
proof -
  from comm_global obtain r1 where r1: 
    "∀q. HOs r1 p = HOs r1 q"
    "∀q. (coin r1 p :: val) = coin r1 q"
    "two_step r1 = 1"
    by(simp add: BenOr_commGlobal_def all_conj_distrib, blast)

  from r1 obtain r0 where r1_def: "r1 = Suc r0" and step_r0: "two_step r0 = 0"
    by (cases r1) (auto simp add: two_step_phase_Suc two_step_def mod_Suc)

  define cfg0 where "cfg0 = rho r0"
  define cfg1 where "cfg1 = rho r1"
  define r2 where "r2 = Suc r1"
  define cfg2 where "cfg2 = rho r2"
  define r3 where "r3 = Suc r2"
  define cfg3 where "cfg3 = rho r3"
  define cfg4 where "cfg4 = rho (Suc r3)"

  have step_r2: "two_step r2 = 0" using r1
    by(auto simp add: r2_def two_step_phase_Suc)

  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"] 
    run[simplified HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r3"]
    obtain μ0 μ1 μ2 μ3 where
    send0: "∀p. μ0 p ∈ get_msgs (send0 r0) cfg0 (HOs r0) (HOs r0) p"
    and step0: "∀p. next0 r0 p (cfg0 p) (μ0 p) (cfg1 p)"
    and send1: "∀p. μ1 p ∈ get_msgs (send1 r1) cfg1 (HOs r1) (HOs r1) p"
    and step1: "∀p. next1 r1 p (cfg1 p) (μ1 p) (cfg2 p)"
    and send2: "∀p. μ2 p ∈ get_msgs (send0 r2) cfg2 (HOs r2) (HOs r2) p"
    and step2: "∀p. next0 r2 p (cfg2 p) (μ2 p) (cfg3 p)"
    and send3: "∀p. μ3 p ∈ get_msgs (send1 r3) cfg3 (HOs r3) (HOs r3) p"
    and step3: "∀p. next1 r3 p (cfg3 p) (μ3 p) (cfg4 p)"
    by(auto simp add: BenOr_A_def BenOr_HOMachine_def 
      two_step_phase_Suc BenOr_nextState_def BenOr_sendMsg_def all_conj_distrib
      CHOAlgorithm.truncate_def step_r0 r1_def r2_def r3_def
      cfg0_def cfg1_def cfg2_def cfg3_def cfg4_def 
      )
  
  let ?v = "x (cfg2 p)"
  from per_rd r1 have xs: "∀q. x (cfg2 q) = ?v"
  proof(cases "∃q w. q ∈ HOs r1 p ∧ vote (cfg1 q) = Some w")
    case True
    then obtain q w where q_w: "q ∈ HOs r1 p ∧ vote (cfg1 q) = Some w"
      by auto
    then have "∀q'. vote (cfg1 q') ∈ {None, Some w}" using  same_new_vote[OF send0 step0 step_r0]
      by (metis insert_iff not_None_eq)
    hence "∀q'. x (cfg2 q') = w"  using step1 send1 q_w
      apply(auto simp add: next1_def all_conj_distrib dec_update_def x_update_def
        get_msgs_benign send1_def isVote_def msgRcvd_def identicalVoteRcvd_def 
        someVoteRcvd_def restrict_map_def)
      by (metis (erased, opaque_lifting) option.distinct(2) option.sel r1(1))
    thus ?thesis
      by auto
  next
    case False
    hence "∀q'. x (cfg2 q') = coin r1 q'" using r1 step1 send1
      apply(auto simp add: next1_def all_conj_distrib dec_update_def x_update_def
        get_msgs_benign send1_def isVote_def msgRcvd_def identicalVoteRcvd_def 
        someVoteRcvd_def restrict_map_def)
      by (metis False)
    thus ?thesis using r1
      by(metis)      
  qed
  
  hence "∀q. vote (cfg3 q) = Some ?v"
    by(simp add: vote_origin[OF send2 step2 step_r2])

  hence "decide (cfg4 p) = Some ?v" using send3[THEN spec, of p] step3[THEN spec, of p] HOs_nonempty
    by(auto simp add: next1_def send1_def get_msgs_benign dec_update_def
      restrict_map_def identicalVoteRcvd_def msgRcvd_def isVote_def)

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

end (* HO predicate context *)

end (* mono_quorum context *)

end (* theory *)