Theory Uv_Proofs

```(*<*)
theory Uv_Proofs
imports Heard_Of.Reduction
Two_Step_Observing "../HO_Transition_System" Uv_Defs
begin
(*>*)

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

axiomatization where val_linorder:
"OFCLASS(val, linorder_class)"

instance val :: linorder by (rule val_linorder)

lemma two_step_step:
"step = two_step"
"phase = two_phase"
by(auto simp add: step_def two_step_def phase_def two_phase_def)

context mono_quorum
begin

definition UV_Alg :: "(process, val pstate, val msg)CHOAlgorithm" where
"UV_Alg = CHOAlgorithm.truncate UV_M"

definition UV_TS ::
"(round ⇒ process HO) ⇒ (round ⇒ process HO) ⇒ (round ⇒ process) ⇒ uv_TS_state TS"
where
"UV_TS HOs SHOs crds = CHO_to_TS UV_Alg HOs SHOs (K o crds)"

lemmas UV_TS_defs = UV_TS_def CHO_to_TS_def UV_Alg_def CHOinitConfig_def
UV_initState_def

type_synonym rHO = "nat ⇒ process HO"

definition UV_trans_step
where
"UV_trans_step HOs SHOs nxt_f snd_f stp ≡ ⋃r μ.
{((r, cfg), (Suc r, cfg'))|cfg cfg'. 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 step_less_D:
"0 < step r ⟹ step r = Suc 0"

lemma UV_trans:
"CSHO_trans_alt UV_sendMsg (λr p st msgs crd st'. UV_nextState r p st msgs st') HOs SHOs crds =
UV_trans_step HOs SHOs next0 send0 0
∪ UV_trans_step HOs SHOs  next1 send1 1
"
proof
show "CSHO_trans_alt UV_sendMsg (λr p st msgs crd. UV_nextState r p st msgs) HOs SHOs crds
⊆ UV_trans_step HOs SHOs next0 send0 0 ∪ UV_trans_step HOs SHOs next1 send1 1"
by(force simp add: CSHO_trans_alt_def UV_sendMsg_def UV_nextState_def UV_trans_step_def
K_def dest!: step_less_D)
next
show " UV_trans_step HOs SHOs next0 send0 0 ∪
UV_trans_step HOs SHOs next1 send1 1
⊆ CSHO_trans_alt UV_sendMsg
(λr p st msgs crd. UV_nextState r p st msgs) HOs SHOs crds"
by(force simp add: CSHO_trans_alt_def UV_sendMsg_def UV_nextState_def UV_trans_step_def)
qed

subsubsection ‹Invariants›
(******************************************************************************)

definition UV_inv1
:: "uv_TS_state set"
where
"UV_inv1  = {(r, s).
two_step r = 0 ⟶ (∀p. agreed_vote (s p) = None)
}"

lemmas UV_inv1I = UV_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas UV_inv1E [elim] = UV_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas UV_inv1D = UV_inv1_def [THEN setc_def_to_dest, rule_format]

lemma UV_inv1_inductive:
"init (UV_TS HOs SHOs crds) ⊆ UV_inv1"
"{UV_inv1} TS.trans (UV_TS HOs SHOs crds) {> UV_inv1}"
by(auto simp add: UV_inv1_def UV_TS_defs CHO_trans_alt UV_trans PO_hoare_def
UV_HOMachine_def CHOAlgorithm.truncate_def UV_trans_step_def
all_conj_distrib two_step_phase_Suc two_step_step next1_def)

lemma UV_inv1_invariant:
"reach (UV_TS HOs SHOs crds) ⊆ UV_inv1"
by(intro inv_rule_basic UV_inv1_inductive)

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

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

(******************************************************************************)
text ‹Agreement for UV only holds if the communication predicates hold›
context
fixes
HOs :: "nat ⇒ process ⇒ process set"
and rho :: "nat ⇒ process ⇒ 'val pstate"
assumes global: "UV_commGlobal HOs"
and per_rd: "∀r. UV_commPerRd (HOs r)"
and run: "HORun fA rho HOs"
begin
(******************************************************************************)

lemma HOs_intersect:
"HOs r p ∩ HOs r' q ≠ {}" using per_rd
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 inv: "(r, cfg) ∈ UV_inv1"
and step_r: "two_step r = 0"
shows
"agreed_vote (cfg' p) = Some v ⟷ (∀q ∈ HOs r p. last_obs (cfg q) = v)"
using send[THEN spec, where x=p] step[THEN spec, where x=p] inv 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 inv: "(r, cfg) ∈ UV_inv1"
and step_r: "two_step r = 0"
obtains v where "∀p w. agreed_vote (cfg' p) = Some w ⟶ w = v"
proof(cases "∃p v. agreed_vote (cfg' p) = Some v")
case True
assume asm: "⋀v. ∀p w. agreed_vote (cfg' p) = Some w ⟶ w = v ⟹ thesis"
from True obtain p v where "agreed_vote (cfg' p) = Some v" by auto

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

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

lemma x_origin1:
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"
and last_obs: "last_obs (cfg' p) = v"
shows
"∃q. last_obs (cfg q) = v"
proof-
have "smallestValRcvd (μ p) ∈ {v. ∃q. μ p q = Some (Val v)}" (is "smallestValRcvd ?msgs ∈ ?vals")
unfolding smallestValRcvd_def
proof(rule Min_in)
have "?vals ⊆ getval ` ((the ∘ ?msgs) ` (HOs r p))"
using send[THEN spec, where x=p]
by (auto simp: image_def get_msgs_benign restrict_map_def send0_def)
thus "finite ?vals" by (auto simp: finite_subset)
next
from send[THEN spec, where x=p]
show "?vals ≠ {}" using HOs_nonempty[of r p]
by (auto simp: image_def get_msgs_benign restrict_map_def send0_def)
qed
hence "v ∈ ?vals" using last_obs step[THEN spec, of p]
thus ?thesis using send[THEN spec, of p]
by(auto simp add: get_msgs_benign send0_def restrict_map_def)
qed

lemma step0_ref:
"{ref_rel ∩ UNIV × UV_inv1} ⋃r S v. tso_round0 r S v,
UV_trans_step HOs HOs next0 send0 0 {> ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs UV_trans_step_def two_step_step 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)"
and inv: "(r, cfg) ∈ UV_inv1"

from R have next_r: "next_round sa = r"

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"
by (metis pstate.select_convs(3) pstate.surjective pstate.update_convs(1) pstate.update_convs(2))

define S where "S = {p. ∃v. agreed_vote (cfg' p) = Some v}"
from same_new_vote[OF send step inv step_r]
obtain v where v: "∀p ∈ S. agreed_vote (cfg' p) = Some v"
hence vote_const_map: "agreed_vote o cfg' = const_map v S"
by(auto simp add: S_def const_map_def restrict_map_def intro!: ext)

note x_origin = x_origin1[OF send step step_r]

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

have "∀p. p ∈ S ⟶ opt_obs_safe (opt_obsv_state.last_obs sa) v"
using vote_origin[OF send step inv step_r] R per_rd[THEN spec, of r] v
apply(clarsimp simp add: UV_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 inv 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(clarsimp simp add: ref_rel_def sa'_def two_step_step two_step_phase_Suc vote_const_map)
by (metis x_origin)
ultimately show
"∃sa'. (∃r S v. (sa, sa') ∈ tso_round0 r S v) ∧ (sa', Suc r, cfg') ∈ ref_rel"
by blast
qed

lemma x_origin2:
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"
and last_obs: "last_obs (cfg' p) = v"
shows
"(∃q. last_obs (cfg q) = v) ∨ (∃q. agreed_vote (cfg q) = Some v)"
proof(cases "∀q ∈ HOs r p. ∃w. μ p q = Some (ValVote w None)")
case True
hence empty: "someVoteRcvd (μ p) = {}" using send[THEN spec, of p] HOs_nonempty[of r p]
by(auto simp add: someVoteRcvd_def msgRcvd_def isValVote_def
get_msgs_benign send1_def restrict_map_def)
have "smallestValNoVoteRcvd (μ p) ∈ {v. ∃q. μ p q = Some (ValVote v None)}"
(is "smallestValNoVoteRcvd ?msgs ∈ ?vals")
unfolding smallestValNoVoteRcvd_def
proof(rule Min_in)
have "?vals ⊆ getval ` ((the ∘ ?msgs) ` (HOs r p))"
using send[THEN spec, where x=p]
by (auto simp: image_def get_msgs_benign restrict_map_def send0_def)
thus "finite ?vals" by (auto simp: finite_subset)
next
from send[THEN spec, where x=p] True HOs_nonempty[of r p]
show "?vals ≠ {}"
by (auto simp: image_def get_msgs_benign restrict_map_def send1_def)
qed
hence "v ∈ ?vals" using empty step[THEN spec, of p] last_obs
thus ?thesis using send[THEN spec, of p]
by(auto simp add: get_msgs_benign restrict_map_def send1_def)
next
case False
hence "someVoteRcvd (μ p) ≠ {}" using send[THEN spec, of p] HOs_nonempty[of r p]
by(auto simp add: someVoteRcvd_def msgRcvd_def isValVote_def
get_msgs_benign send1_def restrict_map_def)
hence "∃q ∈ someVoteRcvd (μ p). v = the (getvote (the (μ p q)))" using step[THEN spec, of p] last_obs
thus ?thesis using send[THEN spec, of p]
by(auto simp add: next1_def x_update_def someVoteRcvd_def isValVote_def
send1_def get_msgs_benign msgRcvd_def restrict_map_def)
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. agreed_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 isValVote_def
smallestValNoVoteRcvd_def)

lemma step1_ref:
"{ref_rel ∩ (TSO_inv1 ∩ TSO_inv2) × UNIV} ⋃r d_f o_f. tso_round1 r d_f o_f,
UV_trans_step HOs HOs next1 send1 (Suc 0) {> ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs UV_trans_step_def two_step_step 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"

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

define Ob where "Ob = {p. last_obs (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 "agreed_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 (agreed_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
UV_commPerRd_def dest!: decide_origin[OF send step step_r, THEN subsetD])

have "dom (agreed_vote ∘ cfg) ∈ Quorum ⟶ Ob = UNIV"
fix p
assume Q: "dom (agreed_vote ∘ cfg) ∈ Quorum" (is "?Q ∈ Quorum")
hence "?Q ∩ HOs r p ≠ {}"  using per_rd[THEN spec, of r]
by(auto simp add: UV_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
isValVote_def send1_def)
moreover have "∀q ∈ someVoteRcvd (μ p). ∃x'. μ p q = Some (ValVote x' (Some v))"
using send[THEN spec, of p]
by(auto simp add: someVoteRcvd_def get_msgs_benign msgRcvd_def restrict_map_def
isValVote_def send1_def dest: v')
ultimately show "last_obs (cfg' p) = v" using step[THEN spec, of p]
qed
note Ob_UNIV=this[rule_format]

have obs_guard: "obs_guard o_f (agreed_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
, opt_obsv_state.last_obs := opt_obsv_state.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 two_step_step)

― ‹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]
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 (last_obs (cfg' p)))"
proof(intro allI impI, cases "S ∈ Quorum")
fix p
case True
hence "last_obs (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 (last_obs (cfg' p)))"
using True
next
fix p
case False
hence empty: "o_f = Map.empty"
note last_obs = 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 (last_obs (cfg' p)))"
proof(elim disjE exE)
fix q
assume "last_obs (cfg q) = last_obs (cfg' p)"
from this[symmetric] show ?thesis using R step_r empty
next
fix q
assume "agreed_vote (cfg q) = Some (last_obs (cfg' p))"
from this[symmetric] show ?thesis using R ainv2 step_r empty
apply(auto simp add: ref_rel_def two_step_step TSO_inv2_def)
by metis
qed
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_step
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

"PO_refines (ref_rel ∩ (TSO_inv1 ∩ TSO_inv2) × UV_inv1)
tso_TS (UV_TS HOs HOs crds)"
proof(rule refine_using_invariants)
show "init (UV_TS HOs HOs crds) ⊆ ref_rel `` init tso_TS"
by(auto simp add: UV_TS_defs UV_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) × UV_inv1} TS.trans tso_TS,
TS.trans (UV_TS HOs HOs crds) {> ref_rel}"
apply(simp add: tso_TS_defs UV_TS_defs UV_HOMachine_def CHOAlgorithm.truncate_def)
apply(auto simp add: CHO_trans_alt UV_trans intro!: step0_ref step1_ref)
done
qed(auto intro!: TSO_inv1_inductive TSO_inv2_inductive UV_inv1_inductive)

end (* HO predicate context *)

end (* mono_quorum context *)

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

text ‹As the model of the algorithm is taken verbatim from the HO Model AFP, we
do not repeat the termination proof here and refer to that AFP entry.›

end (* theory *)
```