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
    ∧ d_guard r_decisions (r_votes s)
    ∧ obs_guard r_obs (r_votes s)
    ― ‹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
  "step1_rel = basic_rel ∩ step1_add_rel"

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'))"
  apply(simp add: const_map_def restrict_map_def)
  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}"
  by(auto simp add: PO_rhoare_defs)

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 
     step1_add_rel_def  step0_rel_def tso_round0_def const_map_equality conj_disj_distribR
     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}"
proof(clarsimp simp add: PO_rhoare_defs)
  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
    by(auto simp add: tso_ref_rel_def) 

  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"
    by(auto simp add: tso_ref_rel_def step1_rel_def step1_add_rel_def)

  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
    apply(clarsimp simp add: tso_round0_def tso_round1_def 
      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 
      intro!: arg_cong2[where f=map_add, OF refl])
    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