# Theory Two_Step_Observing

```section ‹Two-Step Observing Quorums Model›

theory Two_Step_Observing
imports "../Observing_Quorums_Opt" "../Two_Steps"
begin

text ‹To make the coming proofs of concrete algorithms easier, in this model we split
the @{term olv_round} into two steps.›

subsection ‹Model definition›
(******************************************************************************)
record tso_state = opt_obsv_state +
r_votes :: "process ⇒ val option"

context mono_quorum
begin

definition tso_round0
:: "round ⇒ process set ⇒ val ⇒ (tso_state × tso_state)set"
where
"tso_round0 r S v ≡ {(s, s').
― ‹guards›
r = next_round s
∧ two_step r = 0
∧ (S ≠ {} ⟶ opt_obs_safe (last_obs s) v)
― ‹actions›
∧ s' = s⦇
next_round := Suc r
, r_votes := const_map v S
⦈
}"

definition obs_guard :: "(process, val)map ⇒ (process, val)map ⇒ bool" where
"obs_guard r_obs r_v ≡ ∀p.
(∀v. r_obs p = Some v ⟶ (∃q. r_v q = Some v))
∧ (dom r_v ∈ Quorum ⟶ (∃q ∈ dom r_v. r_obs p = r_v q))"

definition tso_round1
:: "round ⇒ (process, val)map ⇒ (process, val)map ⇒ (tso_state × tso_state)set"
where
"tso_round1 r r_decisions r_obs ≡ {(s, s').
― ‹guards›
r = next_round s
∧ two_step r = 1
― ‹actions›
∧ s' = s⦇
next_round := Suc r
, decisions := decisions s ++ r_decisions
, last_obs := last_obs s ++ r_obs
⦈
}"

definition tso_init where
"tso_init = { ⦇ next_round = 0, decisions = Map.empty, last_obs = Map.empty, r_votes = Map.empty ⦈ }"

definition tso_trans :: "(tso_state × tso_state) set" where
"tso_trans = (⋃r S v. tso_round0 r S v) ∪ (⋃r d_f o_f. tso_round1 r d_f o_f) ∪ Id"

definition tso_TS :: "tso_state TS" where
"tso_TS = ⦇ init = tso_init, trans = tso_trans ⦈"

lemmas tso_TS_defs = tso_TS_def tso_init_def tso_trans_def

subsection ‹Refinement›
(******************************************************************************)

definition basic_rel :: "(opt_obsv_state × tso_state)set" where
"basic_rel = {(sa, sc).
next_round sa = two_phase (next_round sc)
∧ last_obs sc = last_obs sa
∧ decisions sc = decisions sa
}"

definition step0_rel :: "(opt_obsv_state × tso_state)set" where
"step0_rel = basic_rel"

definition step1_add_rel :: "(opt_obsv_state × tso_state)set" where
"step1_add_rel = {(sa, sc). ∃S v.
r_votes sc = const_map v S
∧ (S ≠ {} ⟶ opt_obs_safe (last_obs sc) v)
}"

definition step1_rel :: "(opt_obsv_state × tso_state)set" where

definition tso_ref_rel :: "(opt_obsv_state × tso_state)set" where
"tso_ref_rel ≡ {(sa, sc).
(two_step (next_round sc) = 0 ⟶ (sa, sc) ∈ step0_rel)
∧ (two_step (next_round sc) = 1 ⟶
(sa, sc) ∈ step1_rel
∧ (∃sc' r S v. (sc', sc) ∈ tso_round0 r S v ∧ (sa, sc') ∈ step0_rel))
}"

lemma const_map_equality:
"(const_map v S = const_map v' S') = (S = S' ∧ (S = {} ∨ v = v'))"
by (metis equals0D option.distinct(2) option.inject subsetI subset_antisym)

lemma rhoare_skipI:
"⟦ ⋀sa sc sc'. ⟦ (sa, sc) ∈ Pre; (sc, sc') ∈ Tc ⟧ ⟹ (sa, sc') ∈ Post ⟧ ⟹ {Pre} Id, Tc {>Post}"

lemma tso_round0_refines:
"{tso_ref_rel} Id, tso_round0 r S v {>tso_ref_rel}"
apply(rule rhoare_skipI)
apply(auto simp add: tso_ref_rel_def basic_rel_def step1_rel_def
ex_disj_distrib two_step_phase_Suc)
done

lemma tso_round1_refines:
"{tso_ref_rel} ⋃r S v dec_f Ob. olv_round r S v dec_f Ob, tso_round1 r dec_f o_f {>tso_ref_rel}"
fix sa sc and sc'
assume
R: "(sa, sc) ∈ tso_ref_rel"
and step1: "(sc, sc') ∈ tso_round1 r dec_f o_f"

hence step_r: "two_step r = 1" and r_next: "next_round sc = r" by (auto simp add: tso_round1_def)
then obtain r0 sc0 S0 v0 where
R0: "(sa, sc0) ∈ step0_rel" and step0: "(sc0, sc) ∈ tso_round0 r0 S0 v0"
using R

from step_r r_next R obtain S v where
v: "r_votes sc = const_map v S"
and safe: "S ≠ {} ⟶ opt_obs_safe (last_obs sc) v"

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

have "S ∈ Quorum ⟶ dom o_f = UNIV" using step1 v
by(auto simp add: tso_round1_def obs_guard_def const_map_def)
moreover have "o_f ≠ Map.empty ⟶ S ≠ {}" using step1 v
by(auto simp add: tso_round1_def obs_guard_def dom_const_map)
ultimately have
abs_step:
"(sa, sa') ∈ olv_round (next_round sa) S v dec_f (dom o_f)" using R safe v step_r r_next step1
by(clarsimp simp add: tso_ref_rel_def step1_rel_def basic_rel_def sa'_def
olv_round_def tso_round1_def)

from v have post_rel: "(sa', sc') ∈ tso_ref_rel" using R step1
step0_rel_def basic_rel_def  sa'_def tso_ref_rel_def two_step_phase_Suc o_def
const_map_is_Some const_map_is_None const_map_equality obs_guard_def
apply(auto simp add: const_map_def restrict_map_def intro!: ext)
done

from abs_step post_rel show
"∃sa'. (∃r' S' w dec_f' Ob'. (sa, sa') ∈ olv_round r' S' w dec_f' Ob') ∧ (sa', sc') ∈ tso_ref_rel"
by blast
qed

lemma TS_Observing_Refines:
"PO_refines tso_ref_rel olv_TS tso_TS"
apply(auto simp add: PO_refines_def olv_TS_defs tso_TS_defs
intro!: tso_round0_refines tso_round1_refines)
apply(auto simp add: tso_ref_rel_def step0_rel_def basic_rel_def tso_init_def quorum_for_def
dest: empty_not_quorum)
done

subsection ‹Invariants›
(******************************************************************************)

definition TSO_inv1 where
"TSO_inv1 = {s. two_step (next_round s) = Suc 0 ⟶
(∃v. ∀p w. r_votes s p = Some w ⟶ w = v)}"

lemmas TSO_inv1I = TSO_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas TSO_inv1E [elim] = TSO_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas TSO_inv1D = TSO_inv1_def [THEN setc_def_to_dest, rule_format]

definition TSO_inv2 where
"TSO_inv2 = {s. two_step (next_round s) = Suc 0 ⟶
(∀p v. (r_votes s p = Some v ⟶ (∃q. last_obs s q ∈ {None, Some v})))}"

lemmas TSO_inv2I = TSO_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas TSO_inv2E [elim] = TSO_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas TSO_inv2D = TSO_inv2_def [THEN setc_def_to_dest, rule_format]

subsubsection ‹Proofs of invariants›
(******************************************************************************)

lemma TSO_inv1_inductive:
"init tso_TS ⊆ TSO_inv1"
"{TSO_inv1} TS.trans tso_TS {> TSO_inv1}"
by(auto simp add: TSO_inv1_def tso_TS_defs PO_hoare_def
tso_round0_def tso_round1_def const_map_is_Some two_step_phase_Suc)

lemma TSO_inv1_invariant:
"reach tso_TS ⊆ TSO_inv1"
by(intro inv_rule_basic TSO_inv1_inductive)

lemma TSO_inv2_inductive:
"init tso_TS ⊆ TSO_inv2"
"{TSO_inv2} TS.trans tso_TS {> TSO_inv2}"
by(auto simp add: TSO_inv2_def tso_TS_defs PO_hoare_def
opt_obs_safe_def tso_round0_def tso_round1_def const_map_is_Some two_step_phase_Suc)

lemma TSO_inv2_invariant:
"reach tso_TS ⊆ TSO_inv2"
by(intro inv_rule_basic TSO_inv2_inductive)

end

end
```