Theory Two_Step_Observing

section ‹Two-Step Observing Quorums Model›

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

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

definition tso_round0 
  :: "round  process set  val  (tso_state × tso_state)set"
  "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" 
  "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)

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'
    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 
    "(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)

  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
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)

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)